Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Data.SBV.Internals
Contents
- Running symbolic programs manually
- Solver capabilities
- Internal structures useful for low-level programming
- Operations useful for instantiating SBV type classes
- Compilation to C, extras
- Code generation primitives
- The codegen monad
- Specifying inputs, SBV variants
- Specifying inputs, SVal variants
- Settings
- Infrastructure
- Generating collateral
- Various math utilities around floats
- Pretty number printing
- Timing computations
- Coordinating with the solver
Description
Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.
- data Result = Result {
- reskinds :: Set Kind
- resTraces :: [(String, CW)]
- resUISegs :: [(String, [String])]
- resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
- resConsts :: [(SW, CW)]
- resTables :: [((Int, Kind, Kind), [SW])]
- resArrays :: [(Int, ArrayInfo)]
- resUIConsts :: [(String, SBVType)]
- resAxioms :: [(String, [String])]
- resAsgns :: SBVPgm
- resConstraints :: [(Maybe String, SW)]
- resAssertions :: [(String, Maybe CallStack, SW)]
- resOutputs :: [SW]
- data SBVRunMode
- data IStage
- data SolverCapabilities = SolverCapabilities {}
- type SBool = SBV Bool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInteger = SBV Integer
- type SReal = SBV AlgReal
- type SFloat = SBV Float
- type SDouble = SBV Double
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymWord a) => SBV a
- sInfinity :: (Floating a, SymWord a) => SBV a
- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class (HasKind a, Ord a) => SymWord a where
- data CW = CW {}
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data ExtCW
- data GeneralizedCW
- isRegularCW :: GeneralizedCW -> Bool
- cwSameType :: CW -> CW -> Bool
- cwToBool :: CW -> Bool
- mkConstCW :: Integral a => Kind -> a -> CW
- liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b
- mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW
- mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW
- data SW = SW !Kind !NodeId
- trueSW :: SW
- falseSW :: SW
- trueCW :: CW
- falseCW :: CW
- normCW :: CW -> CW
- data SVal = SVal !Kind !(Either CW (Cached SW))
- newtype SBV a = SBV {}
- newtype NodeId = NodeId Int
- mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
- data ArrayContext
- = ArrayFree
- | ArrayMutate Int SW SW
- | ArrayMerge SW Int Int
- type ArrayInfo = (String, (Kind, Kind), ArrayContext)
- class SymArray array where
- newtype SFunArray a b = SFunArray (SBV a -> SBV b)
- mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
- newtype SArray a b = SArray {}
- sbvToSW :: State -> SBV a -> IO SW
- sbvToSymSW :: SBV a -> Symbolic SW
- forceSWArg :: SW -> IO ()
- data SBVExpr = SBVApp !Op ![SW]
- newExpr :: State -> Kind -> SBVExpr -> IO SW
- cache :: (State -> IO a) -> Cached a
- data Cached a
- uncache :: Cached SW -> State -> IO SW
- uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
- class HasKind a where
- data Op
- = Plus
- | Times
- | Minus
- | UNeg
- | Abs
- | Quot
- | Rem
- | Equal
- | NotEqual
- | LessThan
- | GreaterThan
- | LessEq
- | GreaterEq
- | Ite
- | And
- | Or
- | XOr
- | Not
- | Shl
- | Shr
- | Rol Int
- | Ror Int
- | Extract Int Int
- | Join
- | LkUp (Int, Kind, Kind, Int) !SW !SW
- | ArrEq Int Int
- | ArrRead Int
- | KindCast Kind Kind
- | Uninterpreted String
- | Label String
- | IEEEFP FPOp
- | PseudoBoolean PBOp
- data PBOp
- data FPOp
- type NamedSymVar = (SW, String)
- getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
- newtype SBVPgm = SBVPgm {
- pgmAssignments :: Seq (SW, SBVExpr)
- data Symbolic a
- runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
- data State
- getPathCondition :: State -> SBool
- extendPathCondition :: State -> (SBool -> SBool) -> State
- inSMTMode :: State -> IO Bool
- data SBVRunMode
- data Kind
- class Outputtable a where
- data Result = Result {
- reskinds :: Set Kind
- resTraces :: [(String, CW)]
- resUISegs :: [(String, [String])]
- resInputs :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
- resConsts :: [(SW, CW)]
- resTables :: [((Int, Kind, Kind), [SW])]
- resArrays :: [(Int, ArrayInfo)]
- resUIConsts :: [(String, SBVType)]
- resAxioms :: [(String, [String])]
- resAsgns :: SBVPgm
- resConstraints :: [(Maybe String, SW)]
- resAssertions :: [(String, Maybe CallStack, SW)]
- resOutputs :: [SW]
- class SolverContext m where
- internalVariable :: State -> Kind -> IO SW
- internalConstraint :: State -> Maybe String -> SVal -> IO ()
- isCodeGenMode :: State -> IO Bool
- newtype SBVType = SBVType [Kind]
- newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
- addAxiom :: String -> [String] -> Symbolic ()
- data Quantifier
- needsExistentials :: [Quantifier] -> Bool
- data SMTLibPgm = SMTLibPgm SMTLibVersion [String]
- data SMTLibVersion = SMTLib2
- smtLibVersionExtension :: SMTLibVersion -> String
- smtLibReservedNames :: [String]
- data SolverCapabilities = SolverCapabilities {}
- extractSymbolicSimulationState :: State -> IO Result
- data SMTScript = SMTScript {
- scriptBody :: String
- scriptModel :: [String]
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities
- data SMTResult
- data SMTModel = SMTModel {
- modelObjectives :: [(String, GeneralizedCW)]
- modelAssocs :: [(String, CW)]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- isNonModelVar :: String -> Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath
- declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Symbolic (SArray a b)
- declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b)
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)
- data Penalty
- data Objective a
- data QueryState = QueryState {
- queryAsk :: Maybe Int -> String -> IO String
- querySend :: Maybe Int -> String -> IO ()
- queryRetrieveResponse :: Maybe Int -> IO String
- queryConfig :: SMTConfig
- queryTerminate :: IO ()
- queryTimeOutValue :: Maybe Int
- queryAssertionStackDepth :: Int
- newtype Query a = Query (StateT State IO a)
- newtype SMTProblem = SMTProblem {}
- genLiteral :: Integral a => Kind -> a -> SBV b
- genFromCW :: Integral a => CW -> a
- data CW = CW {}
- genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
- checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- showModel :: SMTConfig -> SMTModel -> String
- data SMTModel = SMTModel {
- modelObjectives :: [(String, GeneralizedCW)]
- modelAssocs :: [(String, CW)]
- liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- newtype SBVCodeGen a = SBVCodeGen (StateT CgState Symbolic a)
- cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
- cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]
- cgOutput :: String -> SBV a -> SBVCodeGen ()
- cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()
- cgReturn :: SBV a -> SBVCodeGen ()
- cgReturnArr :: SymWord a => [SBV a] -> 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 ()
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
- class CgTarget a where
- data CgConfig = CgConfig {
- cgRTC :: Bool
- cgInteger :: Maybe Int
- cgReal :: Maybe CgSRealType
- cgDriverVals :: [Integer]
- cgGenDriver :: Bool
- cgGenMakefile :: Bool
- cgIgnoreAsserts :: Bool
- data CgState = CgState {}
- data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
- data CgVal
- defaultCgConfig :: CgConfig
- initCgState :: CgState
- isCgDriver :: CgPgmKind -> Bool
- isCgMakefile :: CgPgmKind -> Bool
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
- renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
- fpRound0 :: (RealFloat a, Integral b) => a -> b
- fpRatio0 :: RealFloat a => a -> Rational
- fpMaxH :: RealFloat a => a -> a -> a
- fpMinH :: RealFloat a => a -> a -> a
- fp2fp :: (RealFloat a, RealFloat b) => a -> b
- fpRemH :: RealFloat a => a -> a -> a
- fpRoundToIntegralH :: RealFloat a => a -> a
- fpIsEqualObjectH :: RealFloat a => a -> a -> Bool
- fpIsNormalizedH :: RealFloat a => a -> Bool
- class PrettyNum a where
- readBin :: Num a => String -> a
- shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
- shexI :: Bool -> Bool -> Integer -> String
- sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
- sbinI :: Bool -> Bool -> Integer -> String
- showCFloat :: Float -> String
- showCDouble :: Double -> String
- showHFloat :: Float -> String
- showHDouble :: Double -> String
- showSMTFloat :: RoundingMode -> Float -> String
- showSMTDouble :: RoundingMode -> Double -> String
- smtRoundingMode :: RoundingMode -> String
- cwToSMTLib :: RoundingMode -> CW -> String
- mkSkolemZero :: RoundingMode -> Kind -> String
- data Timing
- showTDiff :: NominalDiffTime -> String
- sendStringToSolver :: String -> Query ()
- sendRequestToSolver :: String -> Query String
- retrieveResponseFromSolver :: String -> Maybe Int -> Query [String]
Running symbolic programs manually
Result of running a symbolic computation
Constructors
Result | |
Fields
|
data SBVRunMode #
Different means of running a symbolic piece of code
Constructors
SMTMode IStage Bool SMTConfig | In regular mode, with a stage. Bool is True if this is SAT. |
CodeGen | Code generation mode. |
Concrete | Concrete simulation mode. |
Instances
Solver capabilities
data SolverCapabilities #
Translation tricks needed for specific capabilities afforded by each solver
Constructors
SolverCapabilities | |
Fields
|
Internal structures useful for low-level programming
data RoundingMode #
Rounding mode to be used for the IEEE floating-point operations.
Note that Haskell's default is RoundNearestTiesToEven
. If you use
a different rounding mode, then the counter-examples you get may not
match what you observe in Haskell.
Constructors
RoundNearestTiesToEven | Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.) |
RoundNearestTiesToAway | Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.) |
RoundTowardPositive | Round towards positive infinity. (Also known as rounding-up or ceiling.) |
RoundTowardNegative | Round towards negative infinity. (Also known as rounding-down or floor.) |
RoundTowardZero | Round towards zero. (Also known as truncation.) |
Instances
Bounded RoundingMode # | |
Enum RoundingMode # | |
Eq RoundingMode # | |
Data RoundingMode # | |
Ord RoundingMode # | |
Read RoundingMode # | |
Show RoundingMode # | |
HasKind RoundingMode # |
|
SymWord RoundingMode # |
|
SatModel RoundingMode # | A rounding mode, extracted from a model. (Default definition suffices) |
type SRoundingMode = SBV RoundingMode #
The symbolic variant of RoundingMode
sRoundNearestTiesToEven :: SRoundingMode #
Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToAway :: SRoundingMode #
Symbolic variant of RoundNearestTiesToAway
sRoundTowardPositive :: SRoundingMode #
Symbolic variant of RoundNearestPositive
sRoundTowardNegative :: SRoundingMode #
Symbolic variant of RoundTowardNegative
sRoundTowardZero :: SRoundingMode #
Symbolic variant of RoundTowardZero
sRNE :: SRoundingMode #
Alias for sRoundNearestTiesToEven
sRNA :: SRoundingMode #
Alias for sRoundNearestTiesToAway
sRTP :: SRoundingMode #
Alias for sRoundTowardPositive
sRTN :: SRoundingMode #
Alias for sRoundTowardNegative
sRTZ :: SRoundingMode #
Alias for sRoundTowardZero
class (HasKind a, Ord a) => SymWord a where #
A SymWord
is a potential symbolic bitvector that can be created instances of
to be fed to a symbolic program. Note that these methods are typically not needed
in casual uses with prove
, sat
, allSat
etc, as default instances automatically
provide the necessary bits.
Methods
forall :: String -> Symbolic (SBV a) #
Create a user named input (universal)
Create an automatically named input
mkForallVars :: Int -> Symbolic [SBV a] #
Get a bunch of new words
exists :: String -> Symbolic (SBV a) #
Create an existential variable
Create an automatically named existential variable
mkExistVars :: Int -> Symbolic [SBV a] #
Create a bunch of existentials
free :: String -> Symbolic (SBV a) #
Create a free variable, universal in a proof, existential in sat
Create an unnamed free variable, universal in proof, existential in sat
mkFreeVars :: Int -> Symbolic [SBV a] #
Create a bunch of free vars
symbolic :: String -> Symbolic (SBV a) #
Similar to free; Just a more convenient name
symbolics :: [String] -> Symbolic [SBV a] #
Similar to mkFreeVars; but automatically gives names based on the strings
Turn a literal constant to symbolic
unliteral :: SBV a -> Maybe a #
Extract a literal, if the value is concrete
Extract a literal, from a CW representation
isConcrete :: SBV a -> Bool #
Is the symbolic word concrete?
isSymbolic :: SBV a -> Bool #
Is the symbolic word really symbolic?
isConcretely :: SBV a -> (a -> Bool) -> Bool #
Does it concretely satisfy the given predicate?
mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #
One stop allocator
literal :: Show a => a -> SBV a #
Turn a literal constant to symbolic
Extract a literal, from a CW representation
mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #
One stop allocator
Instances
SymWord RoundingMode # |
|
SymWord E # | |
SymWord Word4 # | SymWord instance, allowing this type to be used in proofs/sat etc. |
SymWord Color # | |
SymWord Nationality # | |
SymWord Beverage # | |
SymWord Pet # | |
SymWord Sport # | |
SymWord U2Member # | |
SymWord Location # | |
SymWord Day # | |
SymWord BinOp # | |
SymWord UnOp # | |
SymWord B # | |
SymWord Q # | |
SymWord L # | Declare instances to make |
CW
represents a concrete word of a fixed size:
Endianness is mostly irrelevant (see the FromBits
class).
For signed words, the most significant digit is considered to be the sign.
A constant value
Constructors
CWAlgReal !AlgReal | algebraic real |
CWInteger !Integer | bit-vector/unbounded integer |
CWFloat !Float | float |
CWDouble !Double | double |
CWUserSort !(Maybe Int, String) | value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations |
Instances
Eq CWVal # | Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal 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 CWVal # | Ord instance for CWVal. Same comments as the |
Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation
Constructors
AlgRational Bool Rational | |
AlgPolyRoot (Integer, Polynomial) (Maybe String) |
Instances
Eq AlgReal # | |
Fractional AlgReal # | NB: Following the other types we have, we require `a/0` to be `0` for all a. |
Num AlgReal # | |
Ord AlgReal # | |
Real AlgReal # | |
Show AlgReal # | |
Arbitrary AlgReal # | |
Random AlgReal # | |
HasKind AlgReal # | |
SatModel AlgReal # |
|
SMTValue AlgReal # | |
IEEEFloatConvertable AlgReal # | |
A simple expression type over extendent values, covering infinity, epsilon and intervals.
data GeneralizedCW #
A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
Constructors
ExtendedCW ExtCW | |
RegularCW CW |
Instances
Show GeneralizedCW # | Show instance for Generalized |
HasKind GeneralizedCW # |
|
isRegularCW :: GeneralizedCW -> Bool #
Is this a regular CW?
cwSameType :: CW -> CW -> Bool #
Are two CW's of the same type?
liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b #
Lift a binary function through a CW
mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW #
Map a unary function through a CW.
mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW #
Map a binary function through a CW.
A symbolic word, tracking it's signedness and size.
Normalize a CW. Essentially performs modular arithmetic to make sure the value can fit in the given bit-size. Note that this is rather tricky for negative values, due to asymmetry. (i.e., an 8-bit negative number represents values in the range -128 to 127; thus we have to be careful on the negative side.)
The Symbolic value. Either a constant (Left
) or a symbolic
value (Right Cached
). Note that caching is essential for making
sure sharing is preserved.
The Symbolic value. The parameter a
is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) #
Create a symbolic variable.
data ArrayContext #
The context of a symbolic array as created
Constructors
ArrayFree | A new array, the contents are uninitialized |
ArrayMutate Int SW SW | An array created by mutating another array at a given cell |
ArrayMerge SW Int Int | An array created by symbolically merging two other arrays |
Instances
Flat arrays of symbolic values
An array a b
is an array indexed by the type
, with elements of type SBV
a
.SBV
b
While it's certainly possible for user to create instances of SymArray
, the
SArray
and SFunArray
instances already provided should cover most use cases
in practice. (There are some differences between these models, however, see the corresponding
declaration.)
Minimal complete definition: All methods are required, no defaults.
Minimal complete definition
Methods
newArray_ :: (HasKind a, HasKind b) => Symbolic (array a b) #
Create a new anonymous array
newArray :: (HasKind a, HasKind b) => String -> Symbolic (array a b) #
Create a named new array
readArray :: array a b -> SBV a -> SBV b #
Read the array element at a
writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b #
Update the element at a
to be b
mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b #
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
Arrays implemented internally as functions
- Internally handled by the library and not mapped to SMT-Lib
- Reading an uninitialized value is considered an error (will throw exception)
- Cannot check for equality (internally represented as functions)
- Can quick-check
- Typically faster as it gets compiled away during translation
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b #
Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray
.)
Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
- Maps directly to SMT-lib arrays
- Reading from an unintialized value is OK and yields an unspecified result
- Can check for equality of these arrays
- Cannot quick-check theorems using
SArray
values - Typically slower as it heavily relies on SMT-solving for the array theory
sbvToSymSW :: SBV a -> Symbolic SW #
Convert a symbolic value to an SW, inside the Symbolic monad
forceSWArg :: SW -> IO () #
Forcing an argument; this is a necessary evil to make sure all the arguments to an uninterpreted function are evaluated before called; the semantics of uinterpreted functions is necessarily strict; deviating from Haskell's
A symbolic expression
We implement a peculiar caching mechanism, applicable to the use case in implementation of SBV's. Whenever we do a state based computation, we do not want to keep on evaluating it in the then-current state. That will produce essentially a semantically equivalent value. Thus, we want to run it only once, and reuse that result, capturing the sharing at the Haskell level. This is similar to the "type-safe observable sharing" work, but also takes into the account of how symbolic simulation executes.
See Andy Gill's type-safe obervable sharing trick for the inspiration behind this technique: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09
Note that this is *not* a general memo utility!
A class for capturing values that have a sign and a size (finite or infinite)
minimal complete definition: kindOf. This class can be automatically derived
for data-types that have a Data
instance; this is useful for creating uninterpreted
sorts.
Methods
isUninterpreted :: a -> Bool #
Instances
HasKind Bool # | |
HasKind Double # | |
HasKind Float # | |
HasKind Int8 # | |
HasKind Int16 # | |
HasKind Int32 # | |
HasKind Int64 # | |
HasKind Integer # | |
HasKind Word8 # | |
HasKind Word16 # | |
HasKind Word32 # | |
HasKind Word64 # | |
HasKind AlgReal # | |
HasKind Kind # | |
HasKind ExtCW # | Kind instance for Extended CW |
HasKind GeneralizedCW # |
|
HasKind CW # |
|
HasKind RoundingMode # |
|
HasKind SVal # | |
HasKind SW # | |
HasKind E # | |
HasKind Word4 # | HasKind instance; simply returning the underlying kind for the type |
HasKind Color # | |
HasKind Nationality # | |
HasKind Beverage # | |
HasKind Pet # | |
HasKind Sport # | |
HasKind U2Member # | |
HasKind Location # | |
HasKind Day # | |
HasKind BinOp # | |
HasKind UnOp # | |
HasKind B # | |
HasKind Q # | |
HasKind L # | Similarly, |
HasKind (SBV a) # | |
Symbolic operations
Constructors
Pseudo-boolean operations
Constructors
PB_AtMost Int | At most k |
PB_AtLeast Int | At least k |
PB_Exactly Int | Exactly k |
PB_Le [Int] Int | At most k, with coefficients given. Generalizes PB_AtMost |
PB_Ge [Int] Int | At least k, with coefficients given. Generalizes PB_AtLeast |
PB_Eq [Int] Int | Exactly k, with coefficients given. Generalized PB_Exactly |
Floating point operations
type NamedSymVar = (SW, String) #
NamedSymVar
pairs symbolic words and user given/automatically generated names
getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int #
Create a new table; hash-cons as necessary
A program is a sequence of assignments
Constructors
SBVPgm | |
Fields
|
A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.
runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result) #
Run a symbolic computation, and return a extra value paired up with the Result
Return and clean and incState
The state of the symbolic interpreter
getPathCondition :: State -> SBool #
Get the current path condition
extendPathCondition :: State -> (SBool -> SBool) -> State #
Extend the path condition with the given test value.
data SBVRunMode #
Different means of running a symbolic piece of code
Constructors
SMTMode IStage Bool SMTConfig | In regular mode, with a stage. Bool is True if this is SAT. |
CodeGen | Code generation mode. |
Concrete | Concrete simulation mode. |
Instances
Kind of symbolic value
class Outputtable a where #
A class representing what can be returned from a symbolic computation.
Minimal complete definition
Methods
Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.
Instances
Outputtable () # | |
Outputtable a => Outputtable [a] # | |
Outputtable (SBV a) # | |
(Outputtable a, Outputtable b) => Outputtable (a, b) # | |
(Outputtable a, Outputtable b, Outputtable c) => Outputtable (a, b, c) # | |
(Outputtable a, Outputtable b, Outputtable c, Outputtable d) => Outputtable (a, b, c, d) # | |
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e) => Outputtable (a, b, c, d, e) # | |
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f) => Outputtable (a, b, c, d, e, f) # | |
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g) => Outputtable (a, b, c, d, e, f, g) # | |
(Outputtable a, Outputtable b, Outputtable c, Outputtable d, Outputtable e, Outputtable f, Outputtable g, Outputtable h) => Outputtable (a, b, c, d, e, f, g, h) # | |
Result of running a symbolic computation
Constructors
Result | |
Fields
|
class SolverContext m where #
Actions we can do in a context: Either at problem description
time or while we are dynamically querying. Symbolic
and Query
are
two instances of this class. Note that we use this mechanism
internally and do not export it from SBV.
Minimal complete definition
Methods
Add a constraint, any satisfying instance must satisfy this condition
namedConstraint :: String -> SBool -> m () #
Add a named constraint. The name is used in unsat-core extraction.
setInfo :: String -> [String] -> m () #
Set info. Example: setInfo ":status" ["unsat"]
.
setOption :: SMTOption -> m () #
Set an option.
Set the logic.
setTimeOut :: Integer -> m () #
Set a solver time-out value, in milli-seconds. This function
essentially translates to the SMTLib call (set-info :timeout val)
,
and your backend solver may or may not support it! The amount given
is in milliseconds. Also see the function timeOut
for finer level
control of time-outs, directly from SBV.
internalVariable :: State -> Kind -> IO SW #
Create an internal variable, which acts as an input but isn't visible to the user. Such variables are existentially quantified in a SAT context, and universally quantified in a proof context.
internalConstraint :: State -> Maybe String -> SVal -> IO () #
Require a boolean condition to be true in the state. Only used for internal purposes.
isCodeGenMode :: State -> IO Bool #
Is this a CodeGen run? (i.e., generating code)
A simple type for SBV computations, used mainly for uninterpreted constants. We keep track of the signedness/size of the arguments. A non-function will have just one entry in the list.
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO () #
Create a new uninterpreted symbol, possibly with user given code
addAxiom :: String -> [String] -> Symbolic () #
Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.
needsExistentials :: [Quantifier] -> Bool #
Are there any existential quantifiers?
Representation of an SMT-Lib program. In between pre and post goes the refuted models
Constructors
SMTLibPgm SMTLibVersion [String] |
data SMTLibVersion #
Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.
Constructors
SMTLib2 |
Instances
smtLibVersionExtension :: SMTLibVersion -> String #
The extension associated with the version
smtLibReservedNames :: [String] #
Names reserved by SMTLib. This list is current as of Dec 6 2015; but of course there's no guarantee it'll stay that way.
data SolverCapabilities #
Translation tricks needed for specific capabilities afforded by each solver
Constructors
SolverCapabilities | |
Fields
|
extractSymbolicSimulationState :: State -> IO Result #
Grab the program from a running symbolic simulation state.
A script, to be passed to the solver.
Constructors
SMTScript | |
Fields
|
Solvers that SBV is aware of
An SMT solver
Constructors
SMTSolver | |
Fields
|
The result of an SMT solver call. Each constructor is tagged with
the SMTConfig
that created it so that further tools can inspect it
and build layers of results, if needed. For ordinary uses of the library,
this type should not be needed, instead use the accessor functions on
it. (Custom Show instances and model extractors.)
Constructors
Unsatisfiable SMTConfig | Unsatisfiable |
Satisfiable SMTConfig SMTModel | Satisfiable with model |
SatExtField SMTConfig SMTModel | Prover returned a model, but in an extension field containing Infinite/epsilon |
Unknown SMTConfig String | Prover returned unknown, with the given reason |
ProofError SMTConfig [String] | Prover errored out |
A model, as returned by a solver
Constructors
SMTModel | |
Fields
|
Solver configuration. See also z3
, yices
, cvc4
, boolector
, mathSAT
, etc. which are instantiations of this type for those solvers, with
reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}
.)
Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
precision value on the screen. The field printRealPrec
controls the printing precision, by specifying the number of digits after
the decimal point. The default value is 16, but it can be set to any positive integer.
When printing, SBV will add the suffix ...
at the and of a real-value, if the given bound is not sufficient to represent the real-value
exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
of the real value is not finite, i.e., if it is not rational.
The printBase
field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
Constructors
SMTConfig | |
Fields
|
declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Symbolic (SArray a b) #
Declare a new symbolic array, with a potential initial value
declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b) #
Declare a new functional symbolic array. Note that a read from an uninitialized cell will result in an error.
data OptimizeStyle #
Style of optimization. Note that in the pareto case the user is allowed
to specify a max number of fronts to query the solver for, since there might
potentially be an infinite number of them and there is no way to know exactly
how many ahead of time. If Nothing
is given, SBV will possibly loop forever
if the number is really infinite.
Constructors
Lexicographic | Objectives are optimized in the order given, earlier objectives have higher priority. This is the default. |
Independent | Each objective is optimized independently. |
Pareto (Maybe Int) | Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. |
Instances
Penalty for a soft-assertion. The default penalty is 1
, with all soft-assertions belonging
to the same objective goal. A positive weight and an optional group can be provided by using
the Penalty
constructor.
Constructors
DefaultPenalty | Default: Penalty of |
Penalty Rational (Maybe String) | Penalty with a weight and an optional group |
Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.
data QueryState #
The state we keep track of as we interact with the solver
Constructors
QueryState | |
Fields
|
A query is a user-guided mechanism to directly communicate and extract results from the solver.
newtype SMTProblem #
Internal representation of a symbolic simulation result
Constructors
SMTProblem | SMTLib representation, given the config |
Operations useful for instantiating SBV type classes
genLiteral :: Integral a => Kind -> a -> SBV b #
Generate a finite constant bitvector
CW
represents a concrete word of a fixed size:
Endianness is mostly irrelevant (see the FromBits
class).
For signed words, the most significant digit is considered to be the sign.
genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) #
Generically make a symbolic var
checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a #
Perform a sanity check that we should receive precisely the same number of bits as required by the resulting type. The input is little-endian
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) #
Parse a signed/sized value from a sequence of CWs
showModel :: SMTConfig -> SMTModel -> String #
Show a model in human readable form. Ignore bindings to those variables that start with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes
A model, as returned by a solver
Constructors
SMTModel | |
Fields
|
liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a) #
Lift QRem
to symbolic words. Division by 0 is defined s.t. x/0 = 0
; which
holds even when x
is 0
itself.
liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) #
Lift DMod
to symbolic words. Division by 0 is defined s.t. x/0 = 0
; which
holds even when x
is 0
itself. Essentially, this is conversion from quotRem
(truncate to 0) to divMod (truncate towards negative infinity)
Compilation to C, extras
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle #
Lower level version of compileToC
, producing a CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle #
Lower level version of compileToCLib
, producing a CgPgmBundle
Code generation primitives
The codegen monad
newtype SBVCodeGen a #
The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.
Constructors
SBVCodeGen (StateT CgState Symbolic a) |
Specifying inputs, SBV variants
cgInput :: SymWord a => String -> SBVCodeGen (SBV a) #
Creates an atomic input in the generated code.
cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a] #
Creates an array input in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen () #
Creates an atomic output in the generated code.
cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen () #
Creates an array output in the generated code.
cgReturn :: SBV a -> SBVCodeGen () #
Creates a returned (unnamed) value in the generated code.
cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen () #
Creates a returned (unnamed) array value in the generated code.
Specifying inputs, SVal variants
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] #
Creates an array input in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen () #
Creates an atomic output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen () #
Creates an array output in the generated code.
svCgReturn :: SVal -> SBVCodeGen () #
Creates a returned (unnamed) value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen () #
Creates a returned (unnamed) array value in the generated code.
Settings
cgPerformRTCs :: Bool -> SBVCodeGen () #
Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: False
.
cgSetDriverValues :: [Integer] -> SBVCodeGen () #
Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
cgAddPrototype :: [String] -> SBVCodeGen () #
Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen () #
Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddLDFlags :: [String] -> SBVCodeGen () #
Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
cgIgnoreSAssert :: Bool -> SBVCodeGen () #
Ignore assertions (those generated by sAssert
calls) in the generated C code
cgIntegerSize :: Int -> SBVCodeGen () #
Sets number of bits to be used for representing the SInteger
type in the generated C code.
The argument must be one of 8
, 16
, 32
, or 64
. Note that this is essentially unsafe as
the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as
typical in most C implementations.
cgSRealType :: CgSRealType -> SBVCodeGen () #
Sets the C type to be used for representing the SReal
type in the generated C code.
The setting can be one of C's "float"
, "double"
, or "long double"
, types, depending
on the precision needed. Note that this is essentially unsafe as the semantics of
infinite precision SReal values becomes reduced to the corresponding floating point type in
C, and hence it is subject to rounding errors.
data CgSRealType #
Possible mappings for the SReal
type when translated to C. Used in conjunction
with the function cgSRealType
. Note that the particular characteristics of the
mapped types depend on the platform and the compiler used for compiling the generated
C program. See http://en.wikipedia.org/wiki/C_data_types for details.
Constructors
CgFloat | float |
CgDouble | double |
CgLongDouble | long double |
Instances
Infrastructure
Abstract over code generation for different languages
Minimal complete definition
Methods
targetName :: a -> String #
translate :: a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle #
Options for code-generation.
Constructors
CgConfig | |
Fields
|
data CgPgmBundle #
Representation of a collection of generated programs.
Constructors
CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |
Instances
Different kinds of "files" we can produce. Currently this is quite C specific.
Default options for code generation. The run-time checks are turned-off, and the driver values are completely random.
initCgState :: CgState #
Initial configuration for code-generation
isCgDriver :: CgPgmKind -> Bool #
Is this a driver program?
isCgMakefile :: CgPgmKind -> Bool #
Is this a make file?
Generating collateral
cgGenerateDriver :: Bool -> SBVCodeGen () #
Should we generate a driver program? Default: True
. When a library is generated, it will have
a driver if any of the contituent functions has a driver. (See compileToCLib
.)
cgGenerateMakefile :: Bool -> SBVCodeGen () #
Should we generate a Makefile? Default: True
.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle #
Generate code for a symbolic program, returning a Code-gen bundle, i.e., collection of makefiles, source code, headers, etc.
renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO () #
Render a code-gen bundle to a directory or to stdout
Various math utilities around floats
fpRound0 :: (RealFloat a, Integral b) => a -> b #
A variant of round; except defaulting to 0 when fed NaN or Infinity
fpRatio0 :: RealFloat a => a -> Rational #
A variant of toRational; except defaulting to 0 when fed NaN or Infinity
fpMaxH :: RealFloat a => a -> a -> a #
The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with Haskell's; and also it does not agree with what the hardware does. Sigh.. See: https://ghc.haskell.org/trac/ghc/ticket/10378 https://github.com/Z3Prover/z3/issues/68 So, we codify here what the Z3 (SMTLib) is implementing for fpMax. The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic
fpMinH :: RealFloat a => a -> a -> a #
SMTLib compliant definition for fpMin
. See the comments for fpMax
.
fp2fp :: (RealFloat a, RealFloat b) => a -> b #
Convert double to float and back. Essentially fromRational . toRational
except careful on NaN, Infinities, and -0.
fpRemH :: RealFloat a => a -> a -> a #
Compute the "floating-point" remainder function, the float/double value that
remains from the division of x
and y
. There are strict rules around 0's, Infinities,
and NaN's as coded below, See http://smt-lib.org/papers/BTRW14.pdf, towards the
end of section 4.c.
fpRoundToIntegralH :: RealFloat a => a -> a #
Convert a float to the nearest integral representable in that type
fpIsEqualObjectH :: RealFloat a => a -> a -> Bool #
Check that two floats are the exact same values, i.e., +0/-0 does not compare equal, and NaN's compare equal to themselves.
fpIsNormalizedH :: RealFloat a => a -> Bool #
Check if a number is "normal." Note that +0/-0 is not considered a normal-number and also this is not simply the negation of isDenormalized!
Pretty number printing
PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
Methods
Show a number in hexadecimal (starting with 0x
and type.)
Show a number in binary (starting with 0b
and type.)
Show a number in hex, without prefix, or types.
Show a number in bin, without prefix, or types.
readBin :: Num a => String -> a #
A more convenient interface for reading binary numbers, also supports negative numbers
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String #
Show as a hexadecimal value. First bool controls whether type info is printed while the second boolean controls wether 0x prefix is printed. The tuple is the signedness and the bit-length of the input. The length of the string will not depend on the value, but rather the bit-length.
shexI :: Bool -> Bool -> Integer -> String #
Show as a hexadecimal value, integer version. Almost the same as shex above except we don't have a bit-length so the length of the string will depend on the actual value.
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String #
Similar to shex
; except in binary.
showCFloat :: Float -> String #
A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showCDouble :: Double -> String #
A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showHFloat :: Float -> String #
A version of show for floats that generates correct Haskell literals for nan/infinite
showHDouble :: Double -> String #
A version of show for doubles that generates correct Haskell literals for nan/infinite
showSMTFloat :: RoundingMode -> Float -> String #
A version of show for floats that generates correct SMTLib literals using the rounding mode
showSMTDouble :: RoundingMode -> Double -> String #
A version of show for doubles that generates correct SMTLib literals using the rounding mode
smtRoundingMode :: RoundingMode -> String #
Convert a rounding mode to the format SMT-Lib2 understands.
cwToSMTLib :: RoundingMode -> CW -> String #
Convert a CW to an SMTLib2 compliant value
mkSkolemZero :: RoundingMode -> Kind -> String #
Create a skolem 0 for the kind
Timing computations
Specify how to save timing information, if at all.
Constructors
NoTiming | |
PrintTiming | |
SaveTiming (IORef NominalDiffTime) |
showTDiff :: NominalDiffTime -> String #
Show NominalDiffTime
in human readable form. NominalDiffTime
is
essentially picoseconds (10^-12 seconds). We show it so that
it's represented at the day:hour:minute:second.XXX granularity.
Coordinating with the solver
In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this
should be avoided if at all possible. Users should prefer the provided API. If you do find yourself
needing send
and ask
directly, please get in touch to see if SBV can support a typed API for your use case.
Similarly, the function retrieveResponseFromSolver
might occasionally be necessary to clean-up the communication
buffer. We would like to hear if you do need these functions regularly so we can provide better support.
sendStringToSolver :: String -> Query () #
Send an arbitrary string to the solver in a query. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!
sendRequestToSolver :: String -> Query String #
Send an arbitrary string to the solver in a query, and return a response. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV.
retrieveResponseFromSolver :: String -> Maybe Int -> Query [String] #
Retrieve multiple responses from the solver, until it responds with a user given tag that we shall arrange for internally. The optional timeout is in milliseconds. If the time-out is exceeded, then we will raise an error. Note that this is inherently dangerous as it can put the solver in an arbitrary state and confuse SBV. If you use this feature, you are on your own!