    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Client
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Cross-cutting toplevel client functions
    -----------------------------------------------------------------------------

    {-# LANGUAGE PackageImports      #-}
    {-# LANGUAGE QuasiQuotes         #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE StandaloneDeriving  #-}
    {-# LANGUAGE TemplateHaskell     #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Client
      ( sbvCheckSolverInstallation
      , defaultSolverConfig
      , sbvAvailableSolvers
      , mkSymbolicEnumeration
      ) where

    import Control.Monad (filterM)
    import Data.Generics

    import qualified Control.Exception   as C

    import qualified "template-haskell" Language.Haskell.TH as TH

    import Data.SBV.Core.Data
    import Data.SBV.Core.Model
    import Data.SBV.Provers.Prover

    -- | Check whether the given solver is installed and is ready to go. This call does a
    -- simple call to the solver to ensure all is well.
    sbvCheckSolverInstallation :: SMTConfig -> IO Bool
    sbvCheckSolverInstallation :: SMTConfig -> IO Bool
    sbvCheckSolverInstallation cfg :: SMTConfig
    cfg = IO Bool
    check IO Bool -> (SomeException -> IO Bool) -> IO Bool
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `C.catch` (\(SomeException
    _ :: C.SomeException) -> Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False)
      where check :: IO Bool
    check = do ThmResult r :: SMTResult
    r <- SMTConfig -> (SWord8 -> SBool) -> IO ThmResult
    forall (m :: * -> *) a.
    MProvable m a =>
    SMTConfig -> a -> m ThmResult
    proveWith SMTConfig
    cfg ((SWord8 -> SBool) -> IO ThmResult)
    -> (SWord8 -> SBool) -> IO ThmResult
    forall a b. (a -> b) -> a -> b
    $ \x :: SWord8
    x -> (SWord8
    xSWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    +SWord8
    x) SWord8 -> SWord8 -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== ((SWord8
    xSWord8 -> SWord8 -> SWord8
    forall a. Num a => a -> a -> a
    *2) :: SWord8)
                       case SMTResult
    r of
                         Unsatisfiable{} -> Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
                         _               -> Bool -> IO Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

    -- | The default configs corresponding to supported SMT solvers
    defaultSolverConfig :: Solver -> SMTConfig
    defaultSolverConfig :: Solver -> SMTConfig
    defaultSolverConfig Z3        = SMTConfig
    z3
    defaultSolverConfig Yices     = SMTConfig
    yices
    defaultSolverConfig Boolector = SMTConfig
    boolector
    defaultSolverConfig CVC4      = SMTConfig
    cvc4
    defaultSolverConfig MathSAT   = SMTConfig
    mathSAT
    defaultSolverConfig ABC       = SMTConfig
    abc

    -- | Return the known available solver configs, installed on your machine.
    sbvAvailableSolvers :: IO [SMTConfig]
    sbvAvailableSolvers :: IO [SMTConfig]
    sbvAvailableSolvers = (SMTConfig -> IO Bool) -> [SMTConfig] -> IO [SMTConfig]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM SMTConfig -> IO Bool
    sbvCheckSolverInstallation ((Solver -> SMTConfig) -> [Solver] -> [SMTConfig]
    forall a b. (a -> b) -> [a] -> [b]
    map Solver -> SMTConfig
    defaultSolverConfig [Solver
    forall a. Bounded a => a
    minBound .. Solver
    forall a. Bounded a => a
    maxBound])

    -- | Make an enumeration a symbolic type.
    mkSymbolicEnumeration :: TH.Name -> TH.Q [TH.Dec]
    mkSymbolicEnumeration :: Name -> Q [Dec]
    mkSymbolicEnumeration typeName :: Name
    typeName = do
        let typeCon :: TypeQ
    typeCon = Name -> TypeQ
    TH.conT Name
    typeName
        [d| deriving instance Eq       $(typeCon)
            deriving instance Show     $(typeCon)
            deriving instance Ord      $(typeCon)
            deriving instance Read     $(typeCon)
            deriving instance Data     $(typeCon)
            deriving instance SymVal   $(typeCon)
            deriving instance HasKind  $(typeCon)
            deriving instance SatModel $(typeCon)
          |]