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
- data SBVRunMode
- runSymbolic :: Bool -> Symbolic a -> IO Result
- runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)
- data SBV a = SBV !Kind !(Either CW (Cached SW))
- slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
- data CW
- mkConstCW :: Integral a => Kind -> a -> CW
- genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)
- genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- data CgPgmBundle = CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
Running symbolic programs manually
Different means of running a symbolic piece of code
Run a symbolic computation in Proof mode and return a
Result. The boolean
argument indicates if this is a sat instance or not.
Run a symbolic computation, and return a extra value paired up with the
Other internal structures useful for low-level programming
The Symbolic value. Either a constant (
Left) or a symbolic
Right Cached). Note that caching is essential for making
sure sharing is preserved. The parameter
a is phantom, but is
extremely important in keeping the user interface strongly typed.
Explicit sharing combinator. The SBV library has internal caching/hash-consing mechanisms
built in, based on Andy Gill's type-safe obervable sharing technique (see: http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09).
However, there might be times where being explicit on the sharing can help, especially in experimental code. The
ensures that its first argument is computed once and passed on to its continuation, explicitly indicating the intent of sharing. Most
use cases of the SBV library should simply use Haskell's
let construct for this purpose.
CW represents a concrete word of a fixed size:
Endianness is mostly irrelevant (see the
For signed words, the most significant digit is considered to be the sign.
Generate a finite symbolic bitvector, named
Generate a finite symbolic bitvector, unnamed
Compilation to C
Representation of a collection of generated programs.