{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Dynamic
(
SVal
, HasKind(..), Kind(..), CV(..), CVal(..), cvToBool
, SArr, readSArr, writeSArr, mergeSArr, newSArr, eqSArr
, SFunArr, readSFunArr, writeSFunArr, mergeSFunArr, newSFunArr
, Symbolic
, Quantifier(..)
, svMkSymVar
, sWordN, sWordN_, sIntN, sIntN_
, svTrue, svFalse, svBool, svAsBool
, svInteger, svAsInteger
, svFloat, svDouble, svFloatingPoint
, svReal, svNumerator, svDenominator
, svEqual, svNotEqual
, svEnumFromThenTo
, svLessThan, svGreaterThan, svLessEq, svGreaterEq, svStructuralLessThan
, svPlus, svTimes, svMinus, svUNeg, svAbs
, svDivide, svQuot, svRem, svQuotRem, svExp
, svAddConstant, svIncrement, svDecrement
, svAnd, svOr, svXOr, svNot
, svShl, svShr, svRol, svRor
, svExtract, svJoin
, svSign, svUnsign
, svFromIntegral
, svSelect
, svToWord1, svFromWord1, svTestBit, svSetBit
, svShiftLeft, svShiftRight
, svRotateLeft, svRotateRight
, svBarrelRotateLeft, svBarrelRotateRight
, svWordFromBE, svWordFromLE
, svBlastLE, svBlastBE
, svIte, svLazyIte, svSymbolicMerge
, svUninterpreted
, proveWith
, satWith, allSatWith
, safeWith
, proveWithAll, proveWithAny, satWithAll, satWithAny
, proveConcurrentWithAll, proveConcurrentWithAny
, satConcurrentWithAny, satConcurrentWithAll
, svQuickCheck
, ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
, genParse, getModelAssignment, getModelDictionary
, SMTConfig(..), SMTLibVersion(..), Solver(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, abc, defaultSolverConfig, defaultSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers
, outputSVal
, SBVCodeGen
, cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
, svCgInput, svCgInputArr
, svCgOutput, svCgOutputArr
, svCgReturn, svCgReturnArr
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
, cgIntegerSize, cgSRealType, CgSRealType(..)
, compileToC, compileToCLib
, generateSMTBenchmark
) where
import Data.Map.Strict (Map)
import Data.SBV.Core.Kind
import Data.SBV.Core.Concrete
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Operations
import Data.SBV.Compilers.CodeGen ( SBVCodeGen
, svCgInput, svCgInputArr
, svCgOutput, svCgOutputArr
, svCgReturn, svCgReturnArr
, cgPerformRTCs, cgSetDriverValues, cgGenerateDriver, cgGenerateMakefile
, cgAddPrototype, cgAddDecl, cgAddLDFlags, cgIgnoreSAssert
, cgIntegerSize, cgSRealType, CgSRealType(..)
)
import Data.SBV.Compilers.C (compileToC, compileToCLib)
import Data.SBV.Provers.Prover (boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg)
import Data.SBV.SMT.SMT (ThmResult(..), SatResult(..), SafeResult(..), OptimizeResult(..), AllSatResult(..), genParse)
import Data.SBV (sbvCheckSolverInstallation, defaultSolverConfig, getAvailableSolvers)
import qualified Data.SBV as SBV (SBool, proveWithAll, proveWithAny, satWithAll, satWithAny
, proveConcurrentWithAll, proveConcurrentWithAny
, satConcurrentWithAny, satConcurrentWithAll
)
import qualified Data.SBV.Core.Data as SBV (SBV(..))
import qualified Data.SBV.Core.Model as SBV (sbvQuickCheck)
import qualified Data.SBV.Provers.Prover as SBV (proveWith, satWith, safeWith, allSatWith, generateSMTBenchmark)
import qualified Data.SBV.SMT.SMT as SBV (Modelable(getModelAssignment, getModelDictionary))
import Data.Time (NominalDiffTime)
svQuickCheck :: Symbolic SVal -> IO Bool
svQuickCheck :: Symbolic SVal -> IO Bool
svQuickCheck = Symbolic SBool -> IO Bool
SBV.sbvQuickCheck (Symbolic SBool -> IO Bool)
-> (Symbolic SVal -> Symbolic SBool) -> Symbolic SVal -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool
toSBool :: SVal -> SBV.SBool
toSBool :: SVal -> SBool
toSBool = SVal -> SBool
forall a. SVal -> SBV a
SBV.SBV
generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String
generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String
generateSMTBenchmark Bool
isSat Symbolic SVal
s = Bool -> Symbolic SBool -> IO String
forall (m :: * -> *) a.
(MonadIO m, MProvable m a) =>
Bool -> a -> m String
SBV.generateSMTBenchmark Bool
isSat ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
proveWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> Symbolic SBool -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
SBV.proveWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
satWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> Symbolic SBool -> IO SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
SBV.satWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
safeWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> Symbolic SBool -> IO [SafeResult]
forall (m :: * -> *) a.
SExecutable m a =>
SMTConfig -> a -> m [SafeResult]
SBV.safeWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
allSatWith SMTConfig
cfg Symbolic SVal
s = SMTConfig -> Symbolic SBool -> IO AllSatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m AllSatResult
SBV.allSatWith SMTConfig
cfg ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll :: [SMTConfig]
-> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> Symbolic SBool -> IO [(Solver, NominalDiffTime, ThmResult)]
forall a.
Provable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
SBV.proveWithAll [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny :: [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> Symbolic SBool -> IO (Solver, NominalDiffTime, ThmResult)
forall a.
Provable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
SBV.proveWithAny [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll :: SMTConfig
-> Symbolic SVal
-> [Query SVal]
-> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll SMTConfig
cfg Symbolic SVal
s [Query SVal]
queries = SMTConfig
-> [Query SVal]
-> Symbolic SBool
-> IO [(Solver, NominalDiffTime, ThmResult)]
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
SBV.proveConcurrentWithAll SMTConfig
cfg [Query SVal]
queries ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny :: SMTConfig
-> Symbolic SVal
-> [Query SVal]
-> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny SMTConfig
cfg Symbolic SVal
s [Query SVal]
queries = SMTConfig
-> [Query SVal]
-> Symbolic SBool
-> IO (Solver, NominalDiffTime, ThmResult)
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
SBV.proveConcurrentWithAny SMTConfig
cfg [Query SVal]
queries ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll :: [SMTConfig]
-> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> Symbolic SBool -> IO [(Solver, NominalDiffTime, SatResult)]
forall a.
Provable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
SBV.satWithAll [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satWithAny :: [SMTConfig]
-> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satWithAny [SMTConfig]
cfgs Symbolic SVal
s = [SMTConfig]
-> Symbolic SBool -> IO (Solver, NominalDiffTime, SatResult)
forall a.
Provable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
SBV.satWithAny [SMTConfig]
cfgs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny :: SMTConfig
-> [Query b]
-> Symbolic SVal
-> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny SMTConfig
cfg [Query b]
qs Symbolic SVal
s = SMTConfig
-> [Query b]
-> Symbolic SBool
-> IO (Solver, NominalDiffTime, SatResult)
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
SBV.satConcurrentWithAny SMTConfig
cfg [Query b]
qs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll :: SMTConfig
-> [Query b]
-> Symbolic SVal
-> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
cfg [Query b]
qs Symbolic SVal
s = SMTConfig
-> [Query b]
-> Symbolic SBool
-> IO [(Solver, NominalDiffTime, SatResult)]
forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
SBV.satConcurrentWithAll SMTConfig
cfg [Query b]
qs ((SVal -> SBool) -> Symbolic SVal -> Symbolic SBool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBool
toSBool Symbolic SVal
s)
getModelAssignment :: SMTResult -> Either String (Bool, [CV])
getModelAssignment :: SMTResult -> Either String (Bool, [CV])
getModelAssignment = SMTResult -> Either String (Bool, [CV])
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
SBV.getModelAssignment
getModelDictionary :: SMTResult -> Map String CV
getModelDictionary :: SMTResult -> Map String CV
getModelDictionary = SMTResult -> Map String CV
forall a. Modelable a => a -> Map String CV
SBV.getModelDictionary