Copyright  (c) Brian Huffman 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
 Programming with symbolic values
 Uninterpreted sorts, constants, and functions
 Properties, proofs, and satisfiability
 Proving properties using multiple solvers
 Quickcheck
 Model extraction
 SMT Interface: Configurations and solvers
 Symbolic computations
 Getting SMTLib output (for offline analysis)
 Code generation from symbolic programs
Dynamically typed lowlevel API to the SBV library, for users who want to generate symbolic values at runtime. Note that with this API it is possible to create terms that are not type correct; use at your own risk!
 data SVal
 class HasKind a where
 data Kind
 data CW = CW {}
 data CWVal
 cwToBool :: CW > Bool
 data SArr
 readSArr :: SArr > SVal > SVal
 resetSArr :: SArr > SVal > SArr
 writeSArr :: SArr > SVal > SVal > SArr
 mergeSArr :: SVal > SArr > SArr > SArr
 newSArr :: (Kind, Kind) > (Int > String) > Maybe SVal > Symbolic SArr
 eqSArr :: SArr > SArr > SVal
 data Symbolic a
 data Quantifier
 svMkSymVar :: Maybe Quantifier > Kind > Maybe String > Symbolic 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
 svLessThan :: SVal > SVal > SVal
 svGreaterThan :: SVal > SVal > SVal
 svLessEq :: SVal > SVal > SVal
 svGreaterEq :: 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
 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
 svSelect :: [SVal] > SVal > SVal > SVal
 svToWord1 :: SVal > SVal
 svFromWord1 :: SVal > SVal
 svTestBit :: SVal > Int > SVal
 svShiftLeft :: SVal > SVal > SVal
 svShiftRight :: SVal > SVal > SVal
 svRotateLeft :: SVal > SVal > SVal
 svRotateRight :: SVal > SVal > SVal
 svIte :: SVal > SVal > SVal > SVal
 svLazyIte :: Kind > SVal > SVal > SVal > SVal
 svSymbolicMerge :: Kind > Bool > SVal > SVal > SVal > SVal
 svIsSatisfiableInCurrentPath :: SVal > Symbolic Bool
 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, ThmResult)]
 proveWithAny :: [SMTConfig] > Symbolic SVal > IO (Solver, ThmResult)
 satWithAll :: [SMTConfig] > Symbolic SVal > IO [(Solver, SatResult)]
 satWithAny :: [SMTConfig] > Symbolic SVal > IO (Solver, SatResult)
 svQuickCheck :: Symbolic SVal > IO Bool
 newtype ThmResult = ThmResult SMTResult
 newtype SatResult = SatResult SMTResult
 newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
 newtype AllSatResult = AllSatResult (Bool, [SMTResult])
 data SMTResult
 genParse :: Integral a => Kind > [CW] > Maybe (a, [CW])
 getModel :: SMTResult > Either String (Bool, [CW])
 getModelDictionary :: SMTResult > Map String CW
 data SMTConfig = SMTConfig {
 verbose :: Bool
 timing :: Bool
 sBranchTimeOut :: Maybe Int
 timeOut :: Maybe Int
 printBase :: Int
 printRealPrec :: Int
 solverTweaks :: [String]
 satCmd :: String
 smtFile :: Maybe FilePath
 smtLibVersion :: SMTLibVersion
 solver :: SMTSolver
 roundingMode :: RoundingMode
 useLogic :: Maybe Logic
 data SMTLibVersion = SMTLib2
 data SMTLibLogic
 data Logic
 data OptimizeOpts
 data Solver
 data SMTSolver = SMTSolver {
 name :: Solver
 executable :: String
 options :: [String]
 engine :: SMTEngine
 capabilities :: SolverCapabilities
 boolector :: SMTConfig
 cvc4 :: SMTConfig
 yices :: SMTConfig
 z3 :: SMTConfig
 mathSAT :: SMTConfig
 abc :: SMTConfig
 defaultSolverConfig :: Solver > SMTConfig
 sbvCurrentSolver :: SMTConfig
 defaultSMTCfg :: SMTConfig
 sbvCheckSolverInstallation :: SMTConfig > IO Bool
 sbvAvailableSolvers :: IO [SMTConfig]
 outputSVal :: SVal > Symbolic ()
 compileToSMTLib :: SMTLibVersion > Bool > Symbolic SVal > IO String
 generateSMTBenchmarks :: Bool > FilePath > Symbolic SVal > IO ()
 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 () > IO ()
 compileToCLib :: Maybe FilePath > String > [(String, SBVCodeGen ())] > IO ()
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.
Eq SVal Source  Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do. 
Show SVal Source  Show instance for 
NFData SVal Source  
HasKind SVal Source 
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 datatypes that have a Data
instance; this is useful for creating uninterpreted
sorts.
Nothing
isUninterpreted :: a > Bool Source
HasKind Bool Source  
HasKind Double Source  
HasKind Float Source  
HasKind Int8 Source  
HasKind Int16 Source  
HasKind Int32 Source  
HasKind Int64 Source  
HasKind Integer Source  
HasKind Word8 Source  
HasKind Word16 Source  
HasKind Word32 Source  
HasKind Word64 Source  
HasKind AlgReal Source  
HasKind Kind Source  
HasKind CW Source 

HasKind RoundingMode Source 

HasKind SVal Source  
HasKind E Source  
HasKind Word4 Source  HasKind instance; simply returning the underlying kind for the type 
HasKind Sport Source  
HasKind Pet Source  
HasKind Beverage Source  
HasKind Nationality Source  
HasKind Color Source  
HasKind Location Source  
HasKind U2Member Source  
HasKind B Source  
HasKind Q Source  
HasKind L Source  Similarly, 
HasKind a => HasKind (SBV a) Source 
Kind of symbolic value
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
CWAlgReal AlgReal  algebraic real 
CWInteger Integer  bitvector/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 
Eq CWVal Source  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 Source  Ord instance for CWVal. Same comments as the 
Arrays of symbolic values
Arrays implemented in terms of SMTarrays: http://smtlib.cs.uiowa.edu/theories/ArraysEx.smt2
 Maps directly to SMTlib arrays
 Reading from an unintialized value is OK and yields an unspecified result
 Can check for equality of these arrays
 Cannot quickcheck theorems using
SArr
values  Typically slower as it heavily relies on SMTsolving for the array theory
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 ifthenelse choice down on to elements
newSArr :: (Kind, Kind) > (Int > String) > Maybe SVal > Symbolic SArr Source
Create a named new array, with an optional initial value
Creating a symbolic variable
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.
data Quantifier Source
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
svMkSymVar :: Maybe Quantifier > Kind > Maybe String > Symbolic 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 existential for SAT calls and universal for everything else.
randomCW
is used for generating random values for this variable
when used for quickCheck
purposes.
Operations on symbolic values
Boolean literals
Integer literals
svAsInteger :: SVal > Maybe Integer Source
Extract an integer from a concrete value.
Float literals
Algrebraic 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
svNotEqual :: SVal > SVal > SVal Source
Inequality.
Symbolic ordering
svLessThan :: SVal > SVal > SVal Source
Less than.
svGreaterThan :: SVal > SVal > SVal Source
Greater than.
svGreaterEq :: SVal > SVal > SVal Source
Greater than or equal to.
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 SMTLib
"div" operator (Euclidean division, which always has a
nonnegative remainder). For unsigned bitvectors, it is "bvudiv";
and for signed bitvectors it is "bvsdiv", which rounds toward zero.
All operations have unspecified semantics in case y = 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 SMTLib
"mod" operator (always nonnegative). For unsigned bitvectors, it
is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds
toward zero (sign of remainder matches that of x
). All operations
have unspecified semantics in case y = 0
.
Logical operations
svShl :: SVal > Int > SVal Source
Shift left by a constant amount. Translates to the "bvshl" operation in SMTLib.
svShr :: SVal > Int > SVal Source
Shift right by a constant amount. Translates to either "bvlshr"
(logical shift right) or "bvashr" (arithmetic shift right) in
SMTLib, depending on whether x
is a signed bitvector.
Splitting, joining, and extending
Signcasting
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 SMTLib tables.
Wordlevel operations
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 bitvectors.
svShiftLeft :: SVal > SVal > SVal Source
Generalization of svShl
, where the shiftamount is symbolic.
The first argument should be a bounded quantity.
svShiftRight :: SVal > SVal > SVal Source
Generalization of svShr
, where the shiftamount is symbolic.
The first argument should be a bounded quantity.
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.
The first argument should be a bounded quantity.
svRotateRight :: SVal > SVal > SVal Source
Generalization of svRor
, where the rotation amount is symbolic.
The first argument should be a bounded quantity.
Conditionals: Mergeable values
svLazyIte :: Kind > SVal > SVal > SVal > SVal Source
Lazy Ifthenelse. 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.
svIsSatisfiableInCurrentPath :: SVal > Symbolic Bool Source
Reduce a condition (i.e., try to concretize it) under the given path
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 uninterpretedfunctions as a general means of blackbox'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 SMTsolver
Checking satisfiability
satWith :: SMTConfig > Symbolic SVal > IO SatResult Source
Find a satisfying assignment using the given SMTsolver
allSatWith :: SMTConfig > Symbolic SVal > IO AllSatResult Source
Find all satisfying assignments using the given SMTsolver
Checking safety
safeWith :: SMTConfig > Symbolic SVal > IO [SafeResult] Source
Check safety using the given SMTsolver
Proving properties using multiple solvers
proveWithAll :: [SMTConfig] > Symbolic SVal > IO [(Solver, 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, 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, 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, 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.
Quickcheck
Model extraction
Inspecting proof results
A prove
call results in a ThmResult
newtype SafeResult Source
A safe
call results in a SafeResult
Show SafeResult Source  User friendly way of printing safety results 
newtype AllSatResult Source
An allSat
call results in a AllSatResult
. The boolean says whether
we should warn the user about prefixexistentials.
AllSatResult (Bool, [SMTResult]) 
Show AllSatResult Source  The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available. 
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.)
Unsatisfiable SMTConfig  Unsatisfiable 
Satisfiable SMTConfig SMTModel  Satisfiable with model 
Unknown SMTConfig SMTModel  Prover returned unknown, with a potential (possibly bogus) model 
ProofError SMTConfig [String]  Prover errored out 
TimeOut SMTConfig  Computation timed out (see the 
Programmable model extraction
genParse :: Integral a => Kind > [CW] > Maybe (a, [CW]) Source
Parse a signed/sized value from a sequence of CWs
getModel :: SMTResult > Either String (Bool, [CW]) Source
Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModelDictionary :: SMTResult > Map String CW Source
Extract a model dictionary. Extract a dictionary mapping the variables to
their respective values as returned by the SMT solver. Also see getModelDictionaries
.
SMT Interface: Configurations and solvers
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 realvalue, if the given bound is not sufficient to represent the realvalue
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 floatingpoint values will
be printed in their internal memorylayout format as well, which can come in handy for bitprecise analysis.
SMTConfig  

data SMTLibVersion Source
Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this datatype around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.
data SMTLibLogic Source
SMTLib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
user can override this choice using the useLogic
parameter to the configuration. This is especially handy if
one is experimenting with custom logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml
for the official list.
AUFLIA  Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values 
AUFLIRA  Linear formulas with free sort and function symbols over one and twodimentional arrays of integer index and real value 
AUFNIRA  Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value 
LRA  Linear formulas in linear real arithmetic 
QF_ABV  Quantifierfree formulas over the theory of bitvectors and bitvector arrays 
QF_AUFBV  Quantifierfree formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols 
QF_AUFLIA  Quantifierfree linear formulas over the theory of integer arrays extended with free sort and function symbols 
QF_AX  Quantifierfree formulas over the theory of arrays with extensionality 
QF_BV  Quantifierfree formulas over the theory of fixedsize bitvectors 
QF_IDL  Difference Logic over the integers. Boolean combinations of inequations of the form x  y < b where x and y are integer variables and b is an integer constant 
QF_LIA  Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables 
QF_LRA  Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. 
QF_NIA  Quantifierfree integer arithmetic. 
QF_NRA  Quantifierfree real arithmetic. 
QF_RDL  Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x  y < b where x and y are real variables and b is a rational constant. 
QF_UF  Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. 
QF_UFBV  Unquantified formulas over bitvectors with uninterpreted sort function and symbols. 
QF_UFIDL  Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. 
QF_UFLIA  Unquantified linear integer arithmetic with uninterpreted sort and function symbols. 
QF_UFLRA  Unquantified linear real arithmetic with uninterpreted sort and function symbols. 
QF_UFNRA  Unquantified nonlinear real arithmetic with uninterpreted sort and function symbols. 
UFLRA  Linear real arithmetic with uninterpreted sort and function symbols. 
UFNIA  Nonlinear integer arithmetic with uninterpreted sort and function symbols. 
QF_FPBV  Quantifierfree formulas over the theory of floating point numbers, arrays, and bitvectors 
QF_FP  Quantifierfree formulas over the theory of floating point numbers 
Chosen logic for the solver
PredefinedLogic SMTLibLogic  Use one of the logics as defined by the standard 
CustomLogic String  Use this name for the logic 
data OptimizeOpts Source
Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.
Iterative Bool  Iteratively search. if True, it will be reporting progress 
Quantified  Use quantifiers 
Solvers that SBV is aware of
An SMT solver
SMTSolver  

defaultSolverConfig :: Solver > SMTConfig Source
The default configs corresponding to supported SMT solvers
sbvCurrentSolver :: SMTConfig Source
The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.
defaultSMTCfg :: SMTConfig Source
The default solver used by SBV. This is currently set to z3.
sbvCheckSolverInstallation :: SMTConfig > IO Bool Source
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.
sbvAvailableSolvers :: IO [SMTConfig] Source
Return the known available solver configs, installed on your machine.
Symbolic computations
outputSVal :: SVal > Symbolic () Source
Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.
Getting SMTLib output (for offline analysis)
:: SMTLibVersion  If True, output SMTLib2, otherwise SMTLib1 
> Bool  If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.) 
> Symbolic SVal  
> IO String 
Compiles to SMTLib and returns the resulting program as a string. Useful for saving the result to a file for offline analysis, for instance if you have an SMT solver that's not natively supported outofthe box by the SBV library. It takes two arguments:
 version: The SMTLibversion to produce. Note that we currently only support SMTLib2.
 isSat : If
True
, will translate it as a SAT query, i.e., in the positive. IfFalse
, will translate as a PROVE query, i.e., it will negate the result. (In this case, the checksat call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)
generateSMTBenchmarks :: Bool > FilePath > Symbolic SVal > IO () Source
Create both SMTLib1 and SMTLib2 benchmarks. The first argument is the basename of the file,
SMTLib1 version will be written with suffix ".smt1" and SMTLib2 version will be written with
suffix ".smt2". The Bool
argument controls whether this is a SAT instance, i.e., translate the query
directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to
compileToSMTLib
for details.)
Code generation from symbolic programs
data SBVCodeGen a Source
The codegeneration monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.
Setting codegeneration options
cgPerformRTCs :: Bool > SBVCodeGen () Source
Sets RTC (runtimechecks) for indexoutofbounds, shiftwithlarge value etc. on/off. Default: False
.
cgSetDriverValues :: [Integer] > SBVCodeGen () Source
Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
cgGenerateDriver :: Bool > SBVCodeGen () Source
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 () Source
Should we generate a Makefile? Default: True
.
Designating inputs
svCgInputArr :: Kind > Int > String > SBVCodeGen [SVal] Source
Creates an array input in the generated code.
Designating outputs
svCgOutput :: String > SVal > SBVCodeGen () Source
Creates an atomic output in the generated code.
svCgOutputArr :: String > [SVal] > SBVCodeGen () Source
Creates an array output in the generated code.
Designating return values
svCgReturn :: SVal > SBVCodeGen () Source
Creates a returned (unnamed) value in the generated code.
svCgReturnArr :: [SVal] > SBVCodeGen () Source
Creates a returned (unnamed) array value in the generated code.
Code generation with uninterpreted functions
cgAddPrototype :: [String] > SBVCodeGen () Source
Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] > SBVCodeGen () Source
Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddLDFlags :: [String] > SBVCodeGen () Source
Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
cgIgnoreSAssert :: Bool > SBVCodeGen () Source
Ignore assertions (those generated by sAssert
calls) in the generated C code
Code generation with SInteger
and SReal
types
cgIntegerSize :: Int > SBVCodeGen () Source
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 () Source
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 Source
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.
CgFloat  float 
CgDouble  double 
CgLongDouble  long double 
Eq CgSRealType Source  
Show CgSRealType Source 

Compilation to C
compileToC :: Maybe FilePath > String > SBVCodeGen () > IO () Source
Given a symbolic computation, render it as an equivalent collection of files that make up a C program:
 The first argument is the directory name under which the files will be saved. To save
files in the current directory pass
. UseJust
"."Nothing
for printing to stdout.  The second argument is the name of the C function to generate.
 The final argument is the function to be compiled.
Compilation will also generate a Makefile
, a header file, and a driver (test) program, etc.
compileToCLib :: Maybe FilePath > String > [(String, SBVCodeGen ())] > IO () Source
Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.
 The first argument is the directory name under which the files will be saved. To save
files in the current directory pass
. UseJust
"."Nothing
for printing to stdout.  The second argument is the name of the archive to generate.
 The third argument is the list of functions to include, in the form of functionname/code pairs, similar
to the second and third arguments of
compileToC
, except in a list.