| 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
- 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!
- data SVal
- class HasKind a where
- data Kind
- data CW = CW {}
- data CWVal
- cwToBool :: CW -> Bool
- data SArr
- readSArr :: SArr -> SVal -> SVal
- writeSArr :: SArr -> SVal -> SVal -> SArr
- mergeSArr :: SVal -> SArr -> SArr -> SArr
- newSArr :: (Kind, Kind) -> (Int -> String) -> Symbolic SArr
- eqSArr :: SArr -> SArr -> SVal
- data Symbolic a
- data Quantifier
- svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO 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
- 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
- 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)
- svQuickCheck :: Symbolic SVal -> IO Bool
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult (Bool, Bool, [SMTResult])
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- data SMTResult
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- getModelAssignment :: SMTResult -> Either String (Bool, [CW])
- getModelDictionary :: SMTResult -> Map 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
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: 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 :: SVal -> Symbolic ()
- 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 ()
- 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.
class HasKind a where 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 data-types that have a Data instance; this is useful for creating uninterpreted
sorts.
Methods
intSizeOf :: a -> Int Source #
isBoolean :: a -> Bool Source #
isBounded :: a -> Bool Source #
isDouble :: a -> Bool Source #
isInteger :: a -> Bool Source #
isUninterpreted :: a -> Bool Source #
Instances
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
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 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 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
SArrvalues - Typically slower as it heavily relies on SMT-solving 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 if-then-else choice down on to elements
newSArr :: (Kind, Kind) -> (Int -> String) -> 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.
Instances
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.
randomCW is used for generating random values for this variable
when used for quickCheck or genTest purposes.
Operations on symbolic values
Boolean literals
Integer literals
Float literals
Algebraic reals (only from rationals)
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
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.
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.
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.
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.
The first argument should be a bounded quantity.
svShiftRight :: SVal -> SVal -> SVal Source #
Generalization of svShr, where the shift-amount 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.
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.
Quick-check
Model extraction
Inspecting proof results
A prove call results in a ThmResult
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.
Constructors
| AllSatResult (Bool, Bool, [SMTResult]) |
Instances
newtype SafeResult Source #
A safe call results in a SafeResult
Constructors
| SafeResult (Maybe String, String, SMTResult) |
Instances
data OptimizeResult Source #
An optimize call results in a OptimizeResult. In the ParetoResult case, the boolean is True
if we reached pareto-query limit and so there might be more unqueried results remaining. If False,
it means that we have all the pareto fronts returned. See the Pareto OptimizeStyle for details.
Constructors
| LexicographicResult SMTResult | |
| ParetoResult (Bool, [SMTResult]) | |
| IndependentResult [(String, SMTResult)] |
Instances
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 |
Programmable model extraction
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) Source #
Parse a signed/sized value from a sequence of CWs
getModelAssignment :: 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 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
| |
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 data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.
Constructors
| SMTLib2 |
Solvers that SBV is aware of
An SMT solver
Constructors
| SMTSolver | |
Fields
| |
defaultSolverConfig :: Solver -> SMTConfig Source #
The default configs corresponding to supported SMT solvers
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.
Code generation from symbolic programs
data SBVCodeGen a Source #
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.
Instances
Setting code-generation options
cgPerformRTCs :: Bool -> SBVCodeGen () Source #
Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large 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
svCgInput :: Kind -> String -> SBVCodeGen SVal Source #
Creates an atomic input in the generated code.
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.
Constructors
| CgFloat | float |
| CgDouble | double |
| CgLongDouble | long double |
Instances
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
Just"."Nothingfor 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
Just"."Nothingfor 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 function-name/code pairs, similar
to the second and third arguments of
compileToC, except in a list.
Compilation to SMTLib
generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String Source #
Create SMT-Lib benchmarks. The first argument is the basename of the file, we will automatically
add ".smt2" per SMT-Lib2 convention. 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.