Portability	portable
Stability	experimental
Maintainer	erkokl@gmail.com

Data.SBV.Internals

Contents

Running symbolic programs manually
Other internal structures useful for low-level programming
Integrating with the test framework

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

runSymbolic :: Symbolic a -> IO Result Source

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 -> CW Source

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 -> Assertion Source

Checks that a particular result shows as s

ioShowsAs :: Show a => IO a -> String -> Assertion Source

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

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

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