Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
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.
- data Result
- runSymbolic :: Symbolic a -> IO Result
- data SBV a = SBV !(Bool, Size) !(Either CW (Cached SW))
- data CW
- mkConstCW :: Integral a => (Bool, Size) -> a -> CW
- generateGoldCheck :: FilePath -> Bool -> forall a. Show a => IO a -> FilePath -> IO ()
- showsAs :: Show a => a -> String -> Assertion
- ioShowsAs :: Show a => IO a -> String -> Assertion
- mkTestSuite :: ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuite
- data SBVTestSuite = SBVTestSuite ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test)
- module Test.HUnit
Running symbolic programs manually
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.
(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) |
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
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
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
module Test.HUnit