sbv-0.9.22: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.

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

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 
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) 
(SymWord a, Arbitrary a) => Arbitrary (SBV a) 
(Bits a, SymWord a) => Bits (SBV a) 
NFData a => NFData (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) 
(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 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) 

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 => (Bool, Size) -> a -> CWSource

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

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

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

newtype CgPgmBundle Source

Representation of a collection of generated programs.

Constructors

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

Instances

data CgPgmKind Source

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

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