| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Internals
Contents
Description
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, Maybe SMTConfig) -> 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 = CW {}
- data Kind
- = KBool
- | KBounded Bool Int
- | KUnbounded
- | KReal
- | KUninterpreted String
- | KFloat
- | KDouble
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- 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, Maybe SMTConfig) -> Symbolic a -> IO Result Source
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.
Instances
slet :: (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b Source
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.
Kind of symbolic value
Constructors
| KBool | |
| KBounded Bool Int | |
| KUnbounded | |
| KReal | |
| KUninterpreted String | |
| KFloat | |
| KDouble |
A constant value
Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation
Constructors
| AlgRational Bool Rational | |
| AlgPolyRoot (Integer, Polynomial) (Maybe String) |
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 CgPgmBundle Source
Lower level version of compileToC, producing a CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle Source
Lower level version of compileToCLib, producing a CgPgmBundle
data CgPgmBundle Source
Representation of a collection of generated programs.
Constructors
| CgPgmBundle (Maybe Int, Maybe CgSRealType) [(FilePath, (CgPgmKind, [Doc]))] |
Instances
| Show CgPgmBundle | A simple way to print bundles, mostly for debugging purposes. |