Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
Safe Haskell | Safe-Infered |
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))
- class HasKind a where
- 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
- newtype CgPgmBundle = CgPgmBundle [(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.
A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf
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
newtype CgPgmBundle Source
Representation of a collection of generated programs.
CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))] |