| Copyright | (c) Brian Huffman |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Dynamic
Contents
- Programming with symbolic values
- Uninterpreted sorts, constants, and functions
- Properties, proofs, and satisfiability
- Proving properties using multiple solvers
- Proving properties using multiple threads
- Quick-check
- Model extraction
- SMT Interface: Configurations and solvers
- Symbolic computations
- Code generation from symbolic programs
Description
Dynamically typed low-level API to the SBV library, for users who want to generate symbolic values at run-time. Note that with this API it is possible to create terms that are not type correct; use at your own risk!
Synopsis
- data SVal
- class HasKind a where
- kindOf :: a -> Kind
- hasSign :: a -> Bool
- intSizeOf :: a -> Int
- isBoolean :: a -> Bool
- isBounded :: a -> Bool
- isReal :: a -> Bool
- isFloat :: a -> Bool
- isDouble :: a -> Bool
- isUnbounded :: a -> Bool
- isUninterpreted :: a -> Bool
- isChar :: a -> Bool
- isString :: a -> Bool
- isList :: a -> Bool
- isSet :: a -> Bool
- isTuple :: a -> Bool
- isMaybe :: a -> Bool
- isEither :: a -> Bool
- showType :: a -> String
- data Kind
- data CV = CV {}
- data CVal
- cvToBool :: CV -> Bool
- data SArr
- readSArr :: SArr -> SVal -> SVal
- writeSArr :: SArr -> SVal -> SVal -> SArr
- mergeSArr :: SVal -> SArr -> SArr -> SArr
- newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr
- eqSArr :: SArr -> SArr -> SVal
- data SFunArr
- readSFunArr :: SFunArr -> SVal -> SVal
- writeSFunArr :: SFunArr -> SVal -> SVal -> SFunArr
- mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr
- newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr
- type Symbolic = SymbolicT IO
- data Quantifier
- svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
- sWordN :: MonadSymbolic m => Int -> String -> m SVal
- sWordN_ :: MonadSymbolic m => Int -> m SVal
- sIntN :: MonadSymbolic m => Int -> String -> m SVal
- sIntN_ :: MonadSymbolic m => Int -> m SVal
- svTrue :: SVal
- svFalse :: SVal
- svBool :: Bool -> SVal
- svAsBool :: SVal -> Maybe Bool
- svInteger :: Kind -> Integer -> SVal
- svAsInteger :: SVal -> Maybe Integer
- svFloat :: Float -> SVal
- svDouble :: Double -> SVal
- svReal :: Rational -> SVal
- svNumerator :: SVal -> Maybe Integer
- svDenominator :: SVal -> Maybe Integer
- svEqual :: SVal -> SVal -> SVal
- svNotEqual :: SVal -> SVal -> SVal
- svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
- svLessThan :: SVal -> SVal -> SVal
- svGreaterThan :: SVal -> SVal -> SVal
- svLessEq :: SVal -> SVal -> SVal
- svGreaterEq :: SVal -> SVal -> SVal
- svStructuralLessThan :: SVal -> SVal -> SVal
- svPlus :: SVal -> SVal -> SVal
- svTimes :: SVal -> SVal -> SVal
- svMinus :: SVal -> SVal -> SVal
- svUNeg :: SVal -> SVal
- svAbs :: SVal -> SVal
- svDivide :: SVal -> SVal -> SVal
- svQuot :: SVal -> SVal -> SVal
- svRem :: SVal -> SVal -> SVal
- svQuotRem :: SVal -> SVal -> (SVal, SVal)
- svExp :: SVal -> SVal -> SVal
- svAddConstant :: Integral a => SVal -> a -> SVal
- svIncrement :: SVal -> SVal
- svDecrement :: SVal -> SVal
- svAnd :: SVal -> SVal -> SVal
- svOr :: SVal -> SVal -> SVal
- svXOr :: SVal -> SVal -> SVal
- svNot :: SVal -> SVal
- svShl :: SVal -> Int -> SVal
- svShr :: SVal -> Int -> SVal
- svRol :: SVal -> Int -> SVal
- svRor :: SVal -> Int -> SVal
- svExtract :: Int -> Int -> SVal -> SVal
- svJoin :: SVal -> SVal -> SVal
- svSign :: SVal -> SVal
- svUnsign :: SVal -> SVal
- svFromIntegral :: Kind -> SVal -> SVal
- svSelect :: [SVal] -> SVal -> SVal -> SVal
- svToWord1 :: SVal -> SVal
- svFromWord1 :: SVal -> SVal
- svTestBit :: SVal -> Int -> SVal
- svSetBit :: SVal -> Int -> SVal
- svShiftLeft :: SVal -> SVal -> SVal
- svShiftRight :: SVal -> SVal -> SVal
- svRotateLeft :: SVal -> SVal -> SVal
- svRotateRight :: SVal -> SVal -> SVal
- svBarrelRotateLeft :: SVal -> SVal -> SVal
- svBarrelRotateRight :: SVal -> SVal -> SVal
- svWordFromBE :: [SVal] -> SVal
- svWordFromLE :: [SVal] -> SVal
- svBlastLE :: SVal -> [SVal]
- svBlastBE :: SVal -> [SVal]
- svIte :: SVal -> SVal -> SVal -> SVal
- svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
- svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
- svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
- proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
- satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
- allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
- safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
- proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
- satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
- satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
- proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult)
- satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
- satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
- svQuickCheck :: Symbolic SVal -> IO Bool
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- = LexicographicResult SMTResult
- | ParetoResult (Bool, [SMTResult])
- | IndependentResult [(String, SMTResult)]
- data SMTResult
- = Unsatisfiable SMTConfig (Maybe [String])
- | Satisfiable SMTConfig SMTModel
- | SatExtField SMTConfig SMTModel
- | Unknown SMTConfig SMTReasonUnknown
- | ProofError SMTConfig [String] (Maybe SMTResult)
- genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV])
- getModelAssignment :: SMTResult -> Either String (Bool, [CV])
- getModelDictionary :: SMTResult -> Map String CV
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- satTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- allowQuantifiedQueries :: Bool
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: String -> String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- outputSVal :: MonadSymbolic m => SVal -> m ()
- data SBVCodeGen a
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- svCgInput :: Kind -> String -> SBVCodeGen SVal
- svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
- svCgOutput :: String -> SVal -> SBVCodeGen ()
- svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
- svCgReturn :: SVal -> SBVCodeGen ()
- svCgReturnArr :: [SVal] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
- compileToC :: Maybe FilePath -> String -> SBVCodeGen a -> IO a
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen a)] -> IO [a]
- generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String
Programming with symbolic values
Symbolic types
Abstract symbolic value type
The Symbolic value. Either a constant (Left) or a symbolic
value (Right Cached). Note that caching is essential for making
sure sharing is preserved.
Instances
| Eq SVal Source # | This instance is only defined so that we can define an instance for
|
| Show SVal Source # | |
| NFData SVal Source # | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind SVal Source # | |
Defined in Data.SBV.Core.Symbolic Methods kindOf :: SVal -> Kind Source # hasSign :: SVal -> Bool Source # intSizeOf :: SVal -> Int Source # isBoolean :: SVal -> Bool Source # isBounded :: SVal -> Bool Source # isReal :: SVal -> Bool Source # isFloat :: SVal -> Bool Source # isDouble :: SVal -> Bool Source # isUnbounded :: SVal -> Bool Source # isUninterpreted :: SVal -> Bool Source # isChar :: SVal -> Bool Source # isString :: SVal -> Bool Source # isList :: SVal -> Bool Source # isSet :: SVal -> Bool Source # isTuple :: SVal -> Bool Source # isMaybe :: SVal -> Bool Source # | |
| ArithOverflow SVal Source # | |
Defined in Data.SBV.Tools.Overflow | |
| Testable (Symbolic SVal) | |
Defined in Data.SBV.Core.Model | |
class HasKind a where Source #
A class for capturing values that have a sign and a size (finite or infinite)
minimal complete definition: kindOf, unless you can take advantage of the default
signature: This class can be automatically derived for data-types that have
a Data instance; this is useful for creating uninterpreted sorts. So, in
reality, end users should almost never need to define any methods.
Minimal complete definition
Nothing
Methods
intSizeOf :: a -> Int Source #
isBoolean :: a -> Bool Source #
isBounded :: a -> Bool Source #
isDouble :: a -> Bool Source #
isUnbounded :: a -> Bool Source #
isUninterpreted :: a -> Bool Source #
isString :: a -> Bool Source #
Instances
Kind of symbolic value
Constructors
| KBool | |
| KBounded !Bool !Int | |
| KUnbounded | |
| KReal | |
| KUninterpreted String (Either String [String]) | |
| KFloat | |
| KDouble | |
| KChar | |
| KString | |
| KList Kind | |
| KSet Kind | |
| KTuple [Kind] | |
| KMaybe Kind | |
| KEither Kind Kind |
Instances
| Eq Kind Source # | |
| Ord Kind Source # | |
| Show Kind Source # | The interesting about the show instance is that it can tell apart two kinds nicely; since it conveniently
ignores the enumeration constructors. Also, when we construct a |
| NFData Kind | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind Kind Source # | |
Defined in Data.SBV.Core.Kind Methods kindOf :: Kind -> Kind Source # hasSign :: Kind -> Bool Source # intSizeOf :: Kind -> Int Source # isBoolean :: Kind -> Bool Source # isBounded :: Kind -> Bool Source # isReal :: Kind -> Bool Source # isFloat :: Kind -> Bool Source # isDouble :: Kind -> Bool Source # isUnbounded :: Kind -> Bool Source # isUninterpreted :: Kind -> Bool Source # isChar :: Kind -> Bool Source # isString :: Kind -> Bool Source # isList :: Kind -> Bool Source # isSet :: Kind -> Bool Source # isTuple :: Kind -> Bool Source # isMaybe :: Kind -> Bool Source # | |
CV represents a concrete word of a fixed size:
For signed words, the most significant digit is considered to be the sign.
Instances
| Eq CV Source # | |
| Ord CV Source # | |
| Show CV Source # | Show instance for |
| NFData CV | |
Defined in Data.SBV.Core.Symbolic | |
| HasKind CV Source # |
|
Defined in Data.SBV.Core.Concrete Methods hasSign :: CV -> Bool Source # intSizeOf :: CV -> Int Source # isBoolean :: CV -> Bool Source # isBounded :: CV -> Bool Source # isFloat :: CV -> Bool Source # isDouble :: CV -> Bool Source # isUnbounded :: CV -> Bool Source # isUninterpreted :: CV -> Bool Source # isString :: CV -> Bool Source # isTuple :: CV -> Bool Source # isMaybe :: CV -> Bool Source # | |
| PrettyNum CV Source # | |
| SatModel CV Source # |
|
| SDivisible CV Source # | |
A constant value
Constructors
| CAlgReal !AlgReal | Algebraic real |
| CInteger !Integer | Bit-vector/unbounded integer |
| CFloat !Float | Float |
| CDouble !Double | Double |
| CChar !Char | Character |
| CString !String | String |
| CList ![CVal] | List |
| CSet !(RCSet CVal) | Set. Can be regular or complemented. |
| CUserSort !(Maybe Int, String) | Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations |
| CTuple ![CVal] | Tuple |
| CMaybe !(Maybe CVal) | Maybe |
| CEither !(Either CVal CVal) | Disjoint union |
Instances
| Eq CVal Source # | Eq instance for CVVal. Note that we cannot simply derive Eq/Ord, since CVAlgReal doesn't have proper instances for these when values are infinitely precise reals. However, we do need a structural eq/ord for Map indexes; so define custom ones here: |
| Ord CVal Source # | Ord instance for VWVal. Same comments as the |
SMT Arrays of symbolic values
mergeSArr :: SVal -> SArr -> SArr -> SArr Source #
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b.
Merging pushes the if-then-else choice down on to elements
newSArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SArr Source #
Create a named new array
Functional arrays of symbolic values
readSFunArr :: SFunArr -> SVal -> SVal Source #
Read the array element at a. For efficiency purposes, we create a memo-table
as we go along, as otherwise we suffer significant performance penalties. See:
http://github.com/LeventErkok/sbv/issues/402 and
http://github.com/LeventErkok/sbv/issues/396.
mergeSFunArr :: SVal -> SFunArr -> SFunArr -> SFunArr Source #
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b.
Merging pushes the if-then-else choice down on to elements
newSFunArr :: State -> (Kind, Kind) -> (Int -> String) -> Maybe SVal -> IO SFunArr Source #
Create a named new array
Creating a symbolic variable
data Quantifier Source #
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
Instances
| Eq Quantifier Source # | |
Defined in Data.SBV.Core.Symbolic | |
| Show Quantifier Source # | Show instance for |
Defined in Data.SBV.Core.Symbolic Methods showsPrec :: Int -> Quantifier -> ShowS show :: Quantifier -> String showList :: [Quantifier] -> ShowS | |
| NFData Quantifier Source # | |
Defined in Data.SBV.Core.Symbolic Methods rnf :: Quantifier -> () | |
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal Source #
Create a symbolic value, based on the quantifier we have. If an
explicit quantifier is given, we just use that. If not, then we
pick the quantifier appropriately based on the run-mode.
randomCV is used for generating random values for this variable
when used for quickCheck or genTest purposes.
Operations on symbolic values
Boolean literals
Integer literals
svAsInteger :: SVal -> Maybe Integer Source #
Extract an integer from a concrete value.
Float literals
Algebraic reals (only from rationals)
svNumerator :: SVal -> Maybe Integer Source #
Grab the numerator of an SReal, if available
svDenominator :: SVal -> Maybe Integer Source #
Grab the denominator of an SReal, if available
Symbolic equality
Constructing concrete lists
svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal] Source #
Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite
Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping
it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus
the lifting to Integers preserves the bounds; and then going back is just fine. So, things like [1, 5 .. 200] :: [SInt8] work just
fine (end evaluate to empty list), since we see [1, 5 .. -56] in the Integer domain. Also note the explicit check for s /= f
below to make sure we don't stutter and produce an infinite list.
Symbolic ordering
svStructuralLessThan :: SVal -> SVal -> SVal Source #
Given a composite structure, figure out how to compare for less than
Arithmetic operations
svQuot :: SVal -> SVal -> SVal Source #
Quotient: Overloaded operation whose meaning depends on the kind at which
it is used: For unbounded integers, it corresponds to the SMT-Lib
"div" operator (Euclidean division, which always has a
non-negative remainder). For unsigned bitvectors, it is "bvudiv";
and for signed bitvectors it is "bvsdiv", which rounds toward zero.
Division by 0 is defined s.t. x/0 = 0, which holds even when x itself is 0.
svRem :: SVal -> SVal -> SVal Source #
Remainder: Overloaded operation whose meaning depends on the kind at which
it is used: For unbounded integers, it corresponds to the SMT-Lib
"mod" operator (always non-negative). For unsigned bitvectors, it
is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds
toward zero (sign of remainder matches that of x). Division by 0 is
defined s.t. x/0 = 0, which holds even when x itself is 0.
svAddConstant :: Integral a => SVal -> a -> SVal Source #
Add a constant value:
svIncrement :: SVal -> SVal Source #
Increment:
svDecrement :: SVal -> SVal Source #
Decrement:
Logical operations
svShl :: SVal -> Int -> SVal Source #
Shift left by a constant amount. Translates to the "bvshl" operation in SMT-Lib.
NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.
svShr :: SVal -> Int -> SVal Source #
Shift right by a constant amount. Translates to either "bvlshr"
(logical shift right) or "bvashr" (arithmetic shift right) in
SMT-Lib, depending on whether x is a signed bitvector.
NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.
svRol :: SVal -> Int -> SVal Source #
Rotate-left, by a constant.
NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.
svRor :: SVal -> Int -> SVal Source #
Rotate-right, by a constant.
NB. Haskell spec says the behavior is undefined if the shift amount is negative. We arbitrarily return the value unchanged if this is the case.
Splitting, joining, and extending
Sign-casting
Numeric conversions
svFromIntegral :: Kind -> SVal -> SVal Source #
Convert a symbolic bitvector from one integral kind to another.
Indexed lookups
svSelect :: [SVal] -> SVal -> SVal -> SVal Source #
Total indexing operation. svSelect xs default index is
intuitively the same as xs !! index, except it evaluates to
default if index overflows. Translates to SMT-Lib tables.
Word-level operations
svToWord1 :: SVal -> SVal Source #
Convert an SVal from kind Bool to an unsigned bitvector of size 1.
svFromWord1 :: SVal -> SVal Source #
Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.
svTestBit :: SVal -> Int -> SVal Source #
Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.
svShiftLeft :: SVal -> SVal -> SVal Source #
Generalization of svShl, where the shift-amount is symbolic.
svShiftRight :: SVal -> SVal -> SVal Source #
Generalization of svShr, where the shift-amount is symbolic.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical.
svRotateLeft :: SVal -> SVal -> SVal Source #
Generalization of svRol, where the rotation amount is symbolic.
If the first argument is not bounded, then the this is the same as shift.
svRotateRight :: SVal -> SVal -> SVal Source #
Generalization of svRor, where the rotation amount is symbolic.
If the first argument is not bounded, then the this is the same as shift.
svBarrelRotateLeft :: SVal -> SVal -> SVal Source #
A variant of svRotateLeft that uses a barrel-rotate design, which can lead to
better verification code. Only works when both arguments are finite and the second
argument is unsigned.
svBarrelRotateRight :: SVal -> SVal -> SVal Source #
A variant of svRotateLeft that uses a barrel-rotate design, which can lead to
better verification code. Only works when both arguments are finite and the second
argument is unsigned.
svWordFromBE :: [SVal] -> SVal Source #
Un-bit-blast from little-endian representation to a word of the right size. The input is assumed to be unsigned.
svWordFromLE :: [SVal] -> SVal Source #
Un-bit-blast from big-endian representation to a word of the right size. The input is assumed to be unsigned.
Conditionals: Mergeable values
svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal Source #
Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.
svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal Source #
Merge two symbolic values, at kind k, possibly force'ing the branches to make
sure they do not evaluate to the same result.
Uninterpreted sorts, constants, and functions
svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal Source #
Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Properties, proofs, and satisfiability
Proving properties
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult Source #
Proves the predicate using the given SMT-solver
Checking satisfiability
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult Source #
Find a satisfying assignment using the given SMT-solver
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult Source #
Find all satisfying assignments using the given SMT-solver
Checking safety
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult] Source #
Check safety using the given SMT-solver
Proving properties using multiple solvers
proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)] Source #
Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult) Source #
Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)] Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult) Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
Proving properties using multiple threads
proveConcurrentWithAll :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO [(Solver, NominalDiffTime, ThmResult)] Source #
proveConcurrentWithAny :: SMTConfig -> Symbolic SVal -> [Query SVal] -> IO (Solver, NominalDiffTime, ThmResult) Source #
satConcurrentWithAny :: SMTConfig -> [Query b] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult) Source #
satConcurrentWithAll :: SMTConfig -> [Query b] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)] Source #
Quick-check
svQuickCheck :: Symbolic SVal -> IO Bool Source #
Dynamic variant of quick-check
Model extraction
Inspecting proof results
Instances
| Show ThmResult Source # | |
| NFData ThmResult Source # | |
Defined in Data.SBV.SMT.SMT | |
| Modelable ThmResult Source # |
|
Defined in Data.SBV.SMT.SMT Methods modelExists :: ThmResult -> Bool Source # getModelAssignment :: SatModel b => ThmResult -> Either String (Bool, b) Source # getModelDictionary :: ThmResult -> Map String CV Source # getModelValue :: SymVal b => String -> ThmResult -> Maybe b Source # getModelUninterpretedValue :: String -> ThmResult -> Maybe String Source # extractModel :: SatModel b => ThmResult -> Maybe b Source # getModelObjectives :: ThmResult -> Map String GeneralizedCV Source # getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCV Source # getModelUIFuns :: ThmResult -> Map String (SBVType, ([([CV], CV)], CV)) Source # getModelUIFunValue :: String -> ThmResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source # | |
A sat call results in a SatResult
The reason for having a separate SatResult is to have a more meaningful Show instance.
Instances
| Show SatResult Source # | |
| NFData SatResult Source # | |
Defined in Data.SBV.SMT.SMT | |
| Modelable SatResult Source # |
|
Defined in Data.SBV.SMT.SMT Methods modelExists :: SatResult -> Bool Source # getModelAssignment :: SatModel b => SatResult -> Either String (Bool, b) Source # getModelDictionary :: SatResult -> Map String CV Source # getModelValue :: SymVal b => String -> SatResult -> Maybe b Source # getModelUninterpretedValue :: String -> SatResult -> Maybe String Source # extractModel :: SatModel b => SatResult -> Maybe b Source # getModelObjectives :: SatResult -> Map String GeneralizedCV Source # getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCV Source # getModelUIFuns :: SatResult -> Map String (SBVType, ([([CV], CV)], CV)) Source # getModelUIFunValue :: String -> SatResult -> Maybe (SBVType, ([([CV], CV)], CV)) Source # | |
newtype AllSatResult Source #
An allSat call results in a AllSatResult. The first boolean says whether we
hit the max-model limit as we searched. The second boolean says whether
there were prefix-existentials. The third boolean says whether we stopped because
the solver returned Unknown.
Constructors
| AllSatResult (Bool, Bool, Bool, [SMTResult]) |
Instances
| Show AllSatResult Source # | |
Defined in Data.SBV.SMT.SMT | |