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)
- compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
- compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
- newtype CgPgmBundle = CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))]
- data CgPgmKind
- = CgMakefile
- | CgHeader [Doc]
- | CgSource
- | CgDriver
- 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) | |
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) | |
(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
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.
CgPgmBundle [(FilePath, (CgPgmKind, [Doc]))] |
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