{-# 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
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
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
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])
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)
|]