Stability | experimental |
---|---|
Maintainer | erkokl@gmail.com |
Safe Haskell | None |
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
data SBVRunMode Source
Different means of running a symbolic piece of code
runSymbolic :: Bool -> Symbolic a -> IO ResultSource
Run a symbolic computation in Proof mode and return a Result
. The boolean
argument indicates if this is a sat instance or not.
runSymbolic' :: SBVRunMode -> Symbolic a -> IO (a, Result)Source
Run a symbolic computation, and return a extra value paired up with the Result
Other internal structures useful for low-level programming
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 parameter a
is phantom, but is
extremely important in keeping the user interface strongly typed.
slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV bSource
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 slet
combinator
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 FromBits
class).
For signed words, the most significant digit is considered to be the sign.
genVar :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> String -> Symbolic (SBV a)Source
Generate a finite symbolic bitvector, named
genVar_ :: (Random a, SymWord a) => Maybe Quantifier -> Kind -> Symbolic (SBV a)Source
Generate a finite symbolic bitvector, unnamed
Compilation to C
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundleSource
Lower level version of compileToC
, producing a CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundleSource
Lower level version of compileToCLib
, producing a CgPgmBundle
data CgPgmBundle Source
Representation of a collection of generated programs.
CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |