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

Portabilityportable
Stabilityexperimental
Maintainererkokl@gmail.com

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

runSymbolic :: Symbolic a -> IO ResultSource

Run a symbolic computation and return a Result

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

(SymWord a, Bounded a) => Bounded (SBV a) 
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) 
HasSignAndSize (SBV a) 
SymWord a => Mergeable (SBV a) 
SymWord a => OrdSymbolic (SBV a) 
EqSymbolic (SBV a) 
(SymWord a, PrettyNum a) => PrettyNum (SBV a) 
(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) 

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

data SBVTestSuite Source

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

Constructors

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

module Test.HUnit