| 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 :: forall a b. (HasKind a, HasKind b) => SBV a -> (SBV a -> SBV b) -> SBV b
- data CW = CW {}
- data Kind
- data CWVal
- data AlgReal
- = AlgRational Bool Rational
- | AlgPolyRoot (Integer, Polynomial) (Maybe String)
- data Quantifier
- 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)
- liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
- liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
- symbolicMergeWithKind :: SymWord a => Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a
- cache :: (State -> IO a) -> Cached a
- sbvToSW :: State -> SBV a -> IO SW
- newExpr :: State -> Kind -> SBVExpr -> IO SW
- normCW :: CW -> CW
- data SBVExpr = SBVApp !Op ![SW]
- data Op
- mkSymSBVWithRandom :: forall a. SymWord a => IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
- genLiteral :: Integral a => Kind -> a -> SBV b
- genFromCW :: Integral a => CW -> a
- genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
- checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- 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 :: forall a b. (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
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) |
data Quantifier Source
Quantifiers: forall or exists. Note that we allow arbitrary nestings.
Instances
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
liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a) Source
Lift QRem to symbolic words. Division by 0 is defined s.t. x/0 = 0; which
holds even when x is 0 itself.
liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) Source
Lift QMod to symbolic words. Division by 0 is defined s.t. x/0 = 0; which
holds even when x is 0 itself. Essentially, this is conversion from quotRem
(truncate to 0) to divMod (truncate towards negative infinity)
symbolicMergeWithKind :: SymWord a => Kind -> Bool -> SBool -> SBV a -> SBV a -> SBV a Source
Merge two symbolic values, at kind k, possibly force'ing the branches to make
sure they do not evaluate to the same result. This should only be used for internal purposes;
as default definitions provided should suffice in many cases. (i.e., End users should
only need to define symbolicMerge when needed; which should be rare to start with.)
Normalize a CW. Essentially performs modular arithmetic to make sure the value can fit in the given bit-size. Note that this is rather tricky for negative values, due to asymmetry. (i.e., an 8-bit negative number represents values in the range -128 to 127; thus we have to be careful on the negative side.)
A symbolic expression
Symbolic operations
mkSymSBVWithRandom :: forall a. SymWord a => IO (SBV a) -> Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a) 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 existential for SAT calls and universal for everything else. The rand argument is used
in generating random values for this variable when used for quickCheck purposes.
Operations useful for instantiating SBV type classes
genLiteral :: Integral a => Kind -> a -> SBV b Source
Generate a finite constant bitvector
genMkSymVar :: (Random a, SymWord a) => Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source
Generically make a symbolic var
checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a Source
Perform a sanity check that we should receive precisely the same number of bits as required by the resulting type. The input is little-endian
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) Source
Parse a signed/sized value from a sequence of CWs
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. |