sbv-0.9.14: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Portability portable experimental erkokl@gmail.com

Data.SBV.Internals

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

 Show Result NFData Result

Run a symbolic computation and return a `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 !(Bool, Size) !(Either CW (Cached SW))

Instances

 Testable SBool Boolean SBool 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 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) Enum instance. These instances are suitable for use with concrete values, and will be less useful for symbolic values around. Note that `fromEnum` requires a concrete argument for obvious reasons. Other variants (succ, pred, [x..]) etc are similarly limited. While symbolic variants can be defined for many of these, but they will just diverge as final sizes cannot be determined statically. Eq (SBV a) (Ord a, Num a, SymWord a) => Num (SBV a) Show (SBV a) (SymWord a, Arbitrary a) => Arbitrary (SBV a) (Bits a, SymWord a) => Bits (SBV a) Outputtable (SBV 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 a => CgArgs (SBV a) (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV c, SBV b) -> SBV a) (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (HasSignAndSize h, HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize g, HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize f, HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize e, HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize d, HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) (HasSignAndSize c, HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV c -> SBV b -> SBV a) (HasSignAndSize b, HasSignAndSize a) => Uninterpreted (SBV b -> SBV a) (SymWord a, SymWord b) => CgArgs (SBV a, SBV b) (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) (SymWord a, SymWord b, SymWord c) => CgArgs (SBV a, SBV b, SBV c) (SymWord a, SymWord b, SymWord c, SymWord d) => CgArgs (SBV a, SBV b, SBV c, SBV d) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e) => CgArgs (SBV a, SBV b, SBV c, SBV d, SBV e) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f) => CgArgs (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g) => CgArgs (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)

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

Instances

 Eq CW Ord CW Show CW NFData CW HasSignAndSize CW BVDivisible CW PrettyNum CW

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

genFree :: (Bool, Size) -> String -> Symbolic (SBV a)Source

genFree_ :: (Bool, Size) -> Symbolic (SBV a)Source

# Integrating with the test framework

Functionality needed for extending SBV's internal test-suite. Only for developers of further libraries on top of SBV.

generateGoldCheck :: FilePath -> Bool -> forall a. Show a => IO a -> FilePath -> IO ()Source

Create a gold file for the test case

showsAs :: Show a => a -> String -> AssertionSource

Checks that a particular result shows as `s`

ioShowsAs :: Show a => IO a -> String -> AssertionSource

Run an IO computation and check that it's result shows as `s`

mkTestSuite :: ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuiteSource

Wrap over `SBVTestSuite`, avoids exporting the constructor

A Test-suite, parameterized by the gold-check generator/checker

Constructors

 SBVTestSuite ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test)

module Test.HUnit