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

runSymbolic :: Symbolic a -> IO Result

Run a symbolic computation and return a Result

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

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

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

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

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

Create a gold file for the test case

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

Checks that a particular result shows as s

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

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

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

Wrap over SBVTestSuite, avoids exporting the constructor

data SBVTestSuite

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

Constructors

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

module Test.HUnit