Data.SBV.Internals

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.

Running symbolic programs manually

data Result

Result of running a symbolic computation

Instances

Show Result

NFData Result

data SBVRunMode

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

Concrete simulation mode

runSymbolic :: Bool -> Symbolic a -> IO Result

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)

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

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 !(Bool, Size) !(Either CW (Cached SW))

Instances

Testable SBool

Boolean SBool

BVDivisible SInteger

BVDivisible SInt64

BVDivisible SInt32

BVDivisible SInt16

BVDivisible SInt8

BVDivisible SWord64

BVDivisible SWord32

BVDivisible SWord16

BVDivisible 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)

(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)

(Bits a, SymWord a) => Bits (SBV a)

NFData a => NFData (SBV a)

(Random a, SymWord a) => Random (SBV a)

Outputtable (SBV a)

HasSignAndSize a => HasSignAndSize (SBV a)

HasSignAndSize a => Uninterpreted (SBV a)

SymWord a => Mergeable (SBV a)

SymWord a => OrdSymbolic (SBV a)

EqSymbolic (SBV a)

(SymWord a, PrettyNum a) => PrettyNum (SBV a)

(SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a)

(SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a)

(SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a)

(SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize 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, HasSignAndSize 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, HasSignAndSize 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, HasSignAndSize 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, HasSignAndSize 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, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a)

(SymWord e, SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a)

(SymWord d, SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a)

(SymWord c, SymWord b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a)

(SymWord b, HasSignAndSize 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)

class HasSignAndSize a where

Methods

sizeOf :: a -> Size

hasSign :: a -> Bool

intSizeOf :: a -> Int

isInfPrec :: a -> Bool

showType :: a -> String

Instances

HasSignAndSize Bool

HasSignAndSize Int8

HasSignAndSize Int16

HasSignAndSize Int32

HasSignAndSize Int64

HasSignAndSize Integer

HasSignAndSize Word8

HasSignAndSize Word16

HasSignAndSize Word32

HasSignAndSize Word64

HasSignAndSize SW

HasSignAndSize CW

HasSignAndSize a => HasSignAndSize (SBV a)

data CW

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.

Instances

Eq CW

Ord CW

Show CW

NFData CW

HasSignAndSize CW

BVDivisible CW

PrettyNum CW

mkConstCW :: Integral a => (Bool, Size) -> a -> CW

genFinVar :: (Random a, SymWord a) => Maybe Quantifier -> (Bool, Int) -> String -> Symbolic (SBV a)

genFinVar_ :: (Random a, SymWord a) => Maybe Quantifier -> (Bool, Int) -> Symbolic (SBV a)

Compilation to C

compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle

Lower level version of compileToC, producing a CgPgmBundle

compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle

Lower level version of compileToCLib, producing a CgPgmBundle

newtype CgPgmBundle

Representation of a collection of generated programs.

Constructors

CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))]

Instances

Show CgPgmBundle

data CgPgmKind

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

Constructors

CgMakefile [String]

CgHeader [Doc]

CgSource

CgDriver

Integrating with the test framework