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
- genFree :: (Bool, Size) -> String -> Symbolic (SBV a)
- genFree_ :: (Bool, Size) -> Symbolic (SBV a)
- 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
Other internal structures useful for low-level programming
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.
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 |
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) | |
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SymWord h) => CgArgs (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) |
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