sbv-2.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Stabilityexperimental
Maintainererkokl@gmail.com
Safe HaskellNone

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.

Synopsis

Running symbolic programs manually

data Result Source

Result of running a symbolic computation

Instances

data SBVRunMode Source

Different means of running a symbolic piece of code

Constructors

Proof Bool

Symbolic simulation mode, for proof purposes. Bool is True if it's a sat instance

CodeGen

Code generation mode

Concrete StdGen

Concrete simulation mode. The StdGen is for the pConstrain acceptance in cross runs

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

data SBV a Source

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.

Constructors

SBV !Kind !(Either CW (Cached SW)) 

Instances

Fractional SReal 
Testable SBool 
Boolean SBool 
SDivisible SInteger 
SDivisible SInt64 
SDivisible SInt32 
SDivisible SInt16 
SDivisible SInt8 
SDivisible SWord64 
SDivisible SWord32 
SDivisible SWord16 
SDivisible SWord8 
FromBits SInt64 
FromBits SInt32 
FromBits SInt16 
FromBits SInt8 
FromBits SWord64 
FromBits SWord32 
FromBits SWord16 
FromBits SWord8 
FromBits SBool 
Polynomial SWord64 
Polynomial SWord32 
Polynomial SWord16 
Polynomial SWord8 
Provable SBool 
Provable Predicate 
SignCast SWord64 SInt64 
SignCast SWord32 SInt32 
SignCast SWord16 SInt16 
SignCast SWord8 SInt8 
Splittable SWord64 SWord32 
Splittable SWord32 SWord16 
Splittable SWord16 SWord8 
(SymWord a, Bounded a) => Bounded (SBV a) 
(Show a, Bounded a, Integral a, Num a, SymWord a) => Enum (SBV a) 
Eq (SBV a) 
(Ord a, Num a, SymWord a) => Num (SBV a) 
Show (SBV a) 
Testable (Symbolic SBool) 
(SymWord a, Arbitrary a) => Arbitrary (SBV a) 
(Eq (SBV a), Num a, Bits a, SymWord a) => Bits (SBV a) 
NFData a => NFData (SBV a) 
(Random a, SymWord a) => Random (SBV a) 
Outputtable (SBV a) 
HasKind a => HasKind (SBV a) 
HasKind a => Uninterpreted (SBV a) 
SymWord a => Mergeable (SBV a) 
(Mergeable (SBV a), EqSymbolic (SBV a), SymWord a) => OrdSymbolic (SBV a) 
EqSymbolic (SBV a) 
(SymWord a, PrettyNum a) => PrettyNum (SBV a) 
(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) 
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) 
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) 
(SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) 
(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) 
(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) 
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) 
(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) 
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) 
(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) 
(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) 
(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) 
(SymWord a, EqSymbolic z) => Equality (SBV a -> z) 
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) 
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) 
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) 
(SymWord a, Provable p) => Provable (SBV a -> p) 

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.

data CW Source

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.

mkConstCW :: Integral a => Kind -> a -> CWSource

Create a constant word

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.

Instances

data CgPgmKind Source

Different kinds of files we can produce. Currently this is quite C specific.