sbv-2.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Stability experimental erkokl@gmail.com Safe-Infered

Data.SBV

Description

(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)

SBV: SMT Based Verification

Express properties about Haskell programs and automatically prove them using SMT solvers.

````>>> ````prove \$ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
```Q.E.D.
```
````>>> ````prove \$ forAll ["x"] \$ \x -> x `shiftL` 2 .== (x :: SWord8)
```Falsifiable. Counter-example:
x = 51 :: SWord8
```

The function `prove` has the following type:

```     `prove` :: `Provable` a => a -> `IO` `ThmResult`
```

The class `Provable` comes with instances for n-ary predicates, for arbitrary n. The predicates are just regular Haskell functions over symbolic signed and unsigned bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided.

In particular, the sbv library introduces the types:

• `SBool`: Symbolic Booleans (bits).
• `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned).
• `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed).
• `SArray`, `SFunArray`: Flat arrays of symbolic values.
• Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
• Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
• Uninterpreted sorts, and proofs over such sorts, potentially with axioms.

The user can construct ordinary Haskell programs using these types, which behave very similar to their concrete counterparts. In particular these types belong to the standard classes `Num`, `Bits`, custom versions of `Eq` (`EqSymbolic`) and `Ord` (`OrdSymbolic`), along with several other custom classes for simplifying programming with symbolic values. The framework takes full advantage of Haskell's type inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return `SBool`) built out of these types can also be:

• proven correct via an external SMT solver (the `prove` function)
• checked for satisfiability (the `sat`, `allSat` functions)
• used in synthesis (the `sat` function with existentials)
• quick-checked

If a predicate is not valid, `prove` will return a counterexample: An assignment to inputs such that the predicate fails. The `sat` function will return a satisfying assignment, if there is one. The `allSat` function returns all satisfying assignments, lazily.

The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://goedel.cs.uiowa.edu/smtlib/.

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the Z3 SMT solver from Microsoft: http://research.microsoft.com/en-us/um/redmond/projects/z3/ and the Yices SMT solver from SRI: http://yices.csl.sri.com/, out-of-the-box. Support for other solvers can be added with relative ease.

Synopsis

# Programming with symbolic values

The SBV library is really two things:

• A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
• A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a seamless experience, i.e., let people program in the usual Haskell style without distractions of symbolic coding. While Haskell helps in some aspects (the `Num` and `Bits` classes simplify coding), it makes life harder in others. For instance, `if-then-else` only takes `Bool` as a test in Haskell, and comparisons (`>` etc.) only return `Bool`s. Clearly we would like these values to be symbolic (i.e., `SBool`), thus stopping us from using some native Haskell constructs. When symbolic versions of operators are needed, they are typically obtained by prepending a dot, for instance `==` becomes `.==`. Care has been taken to make the transition painless. In particular, any Haskell program you build out of symbolic components is fully concretely executable within Haskell, without the need for any custom interpreters. (They are truly Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated feel of the system, one of the original design goals for SBV.

## Symbolic types

### Symbolic bit

type SBool = SBV BoolSource

A symbolic boolean/bit

### Unsigned symbolic bit-vectors

type SWord8 = SBV Word8Source

8-bit unsigned symbolic value

16-bit unsigned symbolic value

32-bit unsigned symbolic value

64-bit unsigned symbolic value

### Signed symbolic bit-vectors

type SInt8 = SBV Int8Source

8-bit signed symbolic value, 2's complement representation

type SInt16 = SBV Int16Source

16-bit signed symbolic value, 2's complement representation

type SInt32 = SBV Int32Source

32-bit signed symbolic value, 2's complement representation

type SInt64 = SBV Int64Source

64-bit signed symbolic value, 2's complement representation

### Signed unbounded integers

The SBV library supports unbounded signed integers with the type `SInteger`, which are not subject to overflow/underflow as it is the case with the bounded types, such as `SWord8`, `SInt16`, etc. However, some bit-vector based operations are not supported for the `SInteger` type while in the verification mode. That is, you can use these operations on `SInteger` values during normal programming/simulation. but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are:

• Rotations and shifts: `rotateL`, `rotateR`, `shiftL`, `shiftR`
• Bitwise logical ops: `.&.`, `.|.`, `xor`, `complement`
• Extraction and concatenation: `split`, '#', and `extend` (see the `Splittable` class)

Usual arithmetic (`+`, `-`, `*`, `bvQuotRem`) and logical operations (`.<`, `.<=`, `.>`, `.>=`, `.==`, `./=`) operations are supported for `SInteger` fully, both in programming and verification modes.

Infinite precision signed symbolic value

### Signed algebraic reals

Algebraic reals are roots of single-variable polynomials with rational coefficients. (See http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite precision numbers, but they do not cover all real numbers. (In particular, they cannot represent transcendentals.) Some irrational numbers are algebraic (such as `sqrt 2`), while others are not (such as pi and e).

SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)

Infinite precision symbolic algebraic real value

data AlgReal Source

Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation

## Creating a symbolic variable

These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms for `free` (specialized at the given type), but they might be easier to use.

Declare an `SBool`

Declare an `SWord8`

Declare an `SWord16`

Declare an `SWord32`

Declare an `SWord64`

Declare an `SInt8`

Declare an `SInt16`

Declare an `SInt32`

Declare an `SInt64`

Declare an `SInteger`

## Creating a list of symbolic variables

These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms for `mapM` `free` (specialized at the given type), but they might be easier to use.

sBools :: [String] -> Symbolic [SBool]Source

Declare a list of `SBool`s

sWord8s :: [String] -> Symbolic [SWord8]Source

Declare a list of `SWord8`s

sWord16s :: [String] -> Symbolic [SWord16]Source

Declare a list of `SWord16`s

sWord32s :: [String] -> Symbolic [SWord32]Source

Declare a list of `SWord32`s

sWord64s :: [String] -> Symbolic [SWord64]Source

Declare a list of `SWord64`s

sInt8s :: [String] -> Symbolic [SInt8]Source

Declare a list of `SInt8`s

sInt16s :: [String] -> Symbolic [SInt16]Source

Declare a list of `SInt16`s

sInt32s :: [String] -> Symbolic [SInt32]Source

Declare a list of `SInt32`s

sInt64s :: [String] -> Symbolic [SInt64]Source

Declare a list of `SInt64`s

sIntegers :: [String] -> Symbolic [SInteger]Source

Declare a list of `SInteger`s

Declare an `SReal`

sReals :: [String] -> Symbolic [SReal]Source

Declare a list of `SReal`s

Promote an SInteger to an SReal

### Abstract SBV type

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.

Instances

 Fractional SReal Testable SBool Boolean SBool BVDivisible SInteger BVDivisible SInt64 BVDivisible SInt32 BVDivisible SInt16 BVDivisible SInt8 BVDivisible SWord64 BVDivisible SWord32 BVDivisible SWord16 BVDivisible SWord8 SNum SInteger SNum SInt64 SNum SInt32 SNum SInt16 SNum SInt8 SNum SWord64 SNum SWord32 SNum SWord16 SNum 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 SignCast SWord64 SInt64 SignCast SWord32 SInt32 SignCast SWord16 SInt16 SignCast SWord8 SInt8 Splittable SWord64 SWord32 Splittable SWord32 SWord16 Splittable SWord16 SWord8 (SymWord a, Bounded a) => Bounded (SBV a) (Show 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) Testable (Symbolic SBool) (SymWord a, Arbitrary a) => Arbitrary (SBV a) (Bits a, SymWord a) => Bits (SBV a) NFData a => NFData (SBV a) (Random a, SymWord a) => Random (SBV a) Outputtable (SBV a) HasKind a => HasKind (SBV a) HasKind 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 c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a) (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) (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)

### Arrays of symbolic values

class SymArray array whereSource

Flat arrays of symbolic values An `array a b` is an array indexed by the type `SBV a`, with elements of type `SBV b` If an initial value is not provided in `newArray_` and `newArray` methods, then the elements are left unspecified, i.e., the solver is free to choose any value. This is the right thing to do if arrays are used as inputs to functions to be verified, typically.

While it's certainly possible for user to create instances of `SymArray`, the `SArray` and `SFunArray` instances already provided should cover most use cases in practice. (There are some differences between these models, however, see the corresponding declaration.)

Minimal complete definition: All methods are required, no defaults.

Methods

newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)Source

Create a new array, with an optional initial value

newArray :: (HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)Source

Create a named new array, with an optional initial value

readArray :: array a b -> SBV a -> SBV bSource

Read the array element at `a`

resetArray :: SymWord b => array a b -> SBV b -> array a bSource

Reset all the elements of the array to the value `b`

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a bSource

Update the element at `a` to be `b`

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a bSource

Merge two given arrays on the symbolic condition Intuitively: `mergeArrays cond a b = if cond then a else b`. Merging pushes the if-then-else choice down on to elements

Instances

 SymArray SFunArray SymArray SArray

data SArray a b Source

Arrays implemented in terms of SMT-arrays: http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2

• Maps directly to SMT-lib arrays
• Reading from an unintialized value is OK and yields an uninterpreted result
• Can check for equality of these arrays
• Cannot quick-check theorems using `SArray` values
• Typically slower as it heavily relies on SMT-solving for the array theory

Instances

 SymArray SArray (HasKind a, HasKind b) => Show (SArray a b) SymWord b => Mergeable (SArray a b) EqSymbolic (SArray a b)

data SFunArray a b Source

Arrays implemented internally as functions

• Internally handled by the library and not mapped to SMT-Lib
• Reading an uninitialized value is considered an error (will throw exception)
• Cannot check for equality (internally represented as functions)
• Can quick-check
• Typically faster as it gets compiled away during translation

Instances

 SymArray SFunArray (HasKind a, HasKind b) => Show (SFunArray a b) (SymWord b, Arbitrary b) => Arbitrary (SFunArray a b) SymWord b => Mergeable (SFunArray a b)

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a bSource

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use `newArray`.)

### Full binary trees

type STree i e = STreeInternal (SBV i) (SBV e)Source

A symbolic tree containing values of type e, indexed by elements of type i. Note that these are full-trees, and their their shapes remain constant. There is no API provided that can change the shape of the tree. These structures are useful when dealing with data-structures that are indexed with symbolic values where access time is important. `STree` structures provide logarithmic time reads and writes.

readSTree :: (Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV eSource

Reading a value. We bit-blast the index and descend down the full tree according to bit-values.

writeSTree :: (Mergeable (SBV e), Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i eSource

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

mkSTree :: forall i e. HasKind i => [SBV e] -> STree i eSource

Construct the fully balanced initial tree using the given values

## Operations on symbolic words

### Word level

sbvTestBit :: (Bits a, SymWord a) => SBV a -> Int -> SBoolSource

Replacement for `testBit`. Since `testBit` requires a `Bool` to be returned, we cannot implement it for symbolic words. Index 0 is the least-significant bit.

sbvPopCount :: (Bits a, SymWord a) => SBV a -> SWord8Source

Replacement for `popCount`. Since `popCount` returns an `Int`, we cannot implement it for symbolic words. Here, we return an `SWord8`, which can overflow when used on quantities that have more than 255 bits. Currently, that's only the `SInteger` type that SBV supports, all other types are safe. Even with `SInteger`, this will only overflow if there are at least 256-bits set in the number, and the smallest such number is 2^256-1, which is a pretty darn big number to worry about for practical purposes. In any case, we do not support `sbvPopCount` for unbounded symbolic integers, as the only possible implementation wouldn't symbolically terminate. So the only overflow issue is with really-really large concrete `SInteger` values

setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV aSource

Generalization of `setBit` based on a symbolic boolean. Note that `setBit` and `clearBit` are still available on Symbolic words, this operation comes handy when the condition to set/clear happens to be symbolic.

oneIf :: (Num a, SymWord a) => SBool -> SBV aSource

Returns 1 if the boolean is true, otherwise 0

lsb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Least significant bit of a word, always stored at index 0

msb :: (Bits a, SymWord a) => SBV a -> SBoolSource

Most significant bit of a word, always stored at the last position

### List level

allEqual :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are the same

allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBoolSource

Returns (symbolic) true if all the elements of the given list are different

### Blasting/Unblasting

blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Big-endian blasting of a word into its bits. Also see the `FromBits` class

blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]Source

Little-endian blasting of a word into its bits. Also see the `FromBits` class

class FromBits a whereSource

Unblasting a value from symbolic-bits. The bits can be given little-endian or big-endian. For a signed number in little-endian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the reverse view of little-big-endian representations

Minimal complete definiton: `fromBitsLE`

### Splitting, joining, and extending

class Splittable a b | b -> a whereSource

Splitting an `a` into two `b`'s and joining back. Intuitively, `a` is a larger bit-size word than `b`, typically double. The `extend` operation captures embedding of a `b` value into an `a` without changing its semantic value.

Minimal complete definition: All, no defaults.

Methods

split :: a -> (b, b)Source

(#) :: b -> b -> aSource

extend :: b -> aSource

### Sign-casting

class SignCast a b | a -> b, b -> a whereSource

Sign casting a value into another. This essentially means forgetting the sign bit and reinterpreting the bits accordingly when converting a signed value to an unsigned one. Similarly, when an unsigned quantity is converted to a signed one, the most significant bit is interpreted as the sign. We only define instances when the source and target types are precisely the same size. The idea is that `signCast` and `unsignCast` must form an isomorphism pair between the types `a` and `b`, i.e., we expect the following two properties to hold:

```    signCast . unsignCast = id
unsingCast . signCast = id
```

Note that one naive way to implement both these operations is simply to compute `fromBitsLE . blastLE`, i.e., first get all the bits of the word and then reconstruct in the target type. While this is semantically correct, it generates a lot of code (both during proofs via SMT-Lib, and when compiled to C). The goal of this class is to avoid that cost, so these operations can be compiled very efficiently, they will essentially become no-op's.

Minimal complete definition: All, no defaults.

Methods

signCast :: a -> bSource

Interpret as a signed word

unsignCast :: b -> aSource

Interpret as an unsigned word

## Polynomial arithmetic and CRCs

class Bits a => Polynomial a whereSource

Implements polynomial addition, multiplication, division, and modulus operations over GF(2^n). NB. Similar to `bvQuotRem`, division by `0` is interpreted as follows:

`x `pDivMod` 0 = (0, x)`

for all `x` (including `0`)

Minimal complete definiton: `pMult`, `pDivMod`, `showPolynomial`

Methods

polynomial :: [Int] -> aSource

Given bit-positions to be set, create a polynomial For instance

`polynomial [0, 1, 3] :: SWord8`

will evaluate to `11`, since it sets the bits `0`, `1`, and `3`. Mathematicans would write this polynomial as `x^3 + x + 1`. And in fact, `showPoly` will show it like that.

pAdd :: a -> a -> aSource

pMult :: (a, a, [Int]) -> aSource

Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)

Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.

pDiv :: a -> a -> aSource

Divide two polynomials in GF(2^n), see above note for division by 0

pMod :: a -> a -> aSource

Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0

pDivMod :: a -> a -> (a, a)Source

Division and modulus packed together

showPoly :: a -> StringSource

Display a polynomial like a mathematician would (over the monomial `x`), with a type

showPolynomial :: Bool -> a -> StringSource

Display a polynomial like a mathematician would (over the monomial `x`), the first argument controls if the final type is shown as well.

crcBV :: Int -> [SBool] -> [SBool] -> [SBool]Source

Compute CRCs over bit-vectors. The call `crcBV n m p` computes the CRC of the message `m` with respect to polynomial `p`. The inputs are assumed to be blasted big-endian. The number `n` specifies how many bits of CRC is needed. Note that `n` is actually the degree of the polynomial `p`, and thus it seems redundant to pass it in. However, in a typical proof context, the polynomial can be symbolic, so we cannot compute the degree easily. While this can be worked-around by generating code that accounts for all possible degrees, the resulting code would be unnecessarily big and complicated, and much harder to reason with. (Also note that a CRC is just the remainder from the polynomial division, but this routine is much faster in practice.)

NB. The `n`th bit of the polynomial `p` must be set for the CRC to be computed correctly. Note that the polynomial argument `p` will not even have this bit present most of the time, as it will typically contain bits `0` through `n-1` as usual in the CRC literature. The higher order `n`th bit is simply assumed to be set, as it does not make sense to use a polynomial of a lesser degree. This is usually not a problem since CRC polynomials are designed and expressed this way.

NB. The literature on CRC's has many variants on how CRC's are computed. We follow the painless guide (http://www.ross.net/crc/download/crc_v3.txt) and compute the CRC as follows:

• Extend the message `m` by adding `n` 0 bits on the right
• Divide the polynomial thus obtained by the `p`
• The remainder is the CRC value.

There are many variants on final XOR's, reversed polynomials etc., so it is essential to double check you use the correct algorithm.

crc :: (FromBits (SBV a), FromBits (SBV b), Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV bSource

Compute CRC's over polynomials, i.e., symbolic words. The first `Int` argument plays the same role as the one in the `crcBV` function.

## Conditionals: Mergeable values

class Mergeable a whereSource

Symbolic choice operator, parameterized via a class `select` is a total-indexing function, with the default.

Minimal complete definition: `symbolicMerge`

Methods

symbolicMerge :: SBool -> a -> a -> aSource

Merge two values based on the condition. This is intended to be a structural copy, walking down the values and merging recursively through the structure of `a`. In particular, symbolicMerge should *not* waste its time testing whether the condition might be a literal; that will be handled by `ite` which should be used in all user code. In particular, any implementation of `symbolicMerge` should just call `symbolicMerge` recursively in the constituents of `a`, instead of `ite`.

ite :: SBool -> a -> a -> aSource

Choose one or the other element, based on the condition. This is similar to `symbolicMerge`, but it has a default implementation that makes sure it's short-cut if the condition is concrete. The idea is that use symbolicMerge if you know the condition is symbolic, otherwise use ite, if there's a chance it might be concrete.

select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> aSource

Total indexing operation. `select xs default index` is intuitively the same as `xs !! index`, except it evaluates to `default` if `index` overflows

Instances

 Mergeable () Mergeable Mostek Mergeable Status Mergeable a => Mergeable [a] Mergeable a => Mergeable (Maybe a) SymWord a => Mergeable (SBV a) Mergeable a => Mergeable (Move a) Mergeable b => Mergeable (a -> b) (Mergeable a, Mergeable b) => Mergeable (Either a b) (Mergeable a, Mergeable b) => Mergeable (a, b) (Ix a, Mergeable b) => Mergeable (Array a b) SymWord b => Mergeable (SFunArray a b) SymWord b => Mergeable (SArray a b) (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g)

## Symbolic equality

class EqSymbolic a whereSource

Symbolic Equality. Note that we can't use Haskell's `Eq` class since Haskell insists on returning Bool Comparing symbolic values will necessarily return a symbolic value.

Minimal complete definition: `.==`

Methods

(.==), (./=) :: a -> a -> SBoolSource

Instances

 EqSymbolic Bool EqSymbolic a => EqSymbolic [a] EqSymbolic a => EqSymbolic (Maybe a) EqSymbolic (SBV a) (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) EqSymbolic (SArray a b) (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g)

## Symbolic ordering

class (Mergeable a, EqSymbolic a) => OrdSymbolic a whereSource

Symbolic Comparisons. Similar to `Eq`, we cannot implement Haskell's `Ord` class since there is no way to return an `Ordering` value from a symbolic comparison. Furthermore, `OrdSymbolic` requires `Mergeable` to implement if-then-else, for the benefit of implementing symbolic versions of `max` and `min` functions.

Minimal complete definition: `.<`

Methods

(.<), (.>=), (.>), (.<=) :: a -> a -> SBoolSource

smin, smax :: a -> a -> aSource

Instances

 OrdSymbolic a => OrdSymbolic [a] OrdSymbolic a => OrdSymbolic (Maybe a) SymWord a => OrdSymbolic (SBV a) (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g)

## Symbolic numbers

class (OrdSymbolic a, Num a) => SNum a Source

Symbolic Numbers. This is a simple class that simply incorporates all `OrdSymbolic` and `Num` values together, simplifying writing polymorphic type-signatures that work for all symbolic numbers, such as `SWord8`, `SInt8` etc. For instance, we can write a generic list-minimum function as follows:

```    mm :: SNum a => [a] -> a
mm = foldr1 (a b -> ite (a .<= b) a b)
```

It is similar to the standard `Num` class, except ranging over symbolic instances.

Instances

 SNum SInteger SNum SInt64 SNum SInt32 SNum SInt16 SNum SInt8 SNum SWord64 SNum SWord32 SNum SWord16 SNum SWord8

## Division

class BVDivisible a whereSource

The `BVDivisible` class captures the essence of division of words. Unfortunately we cannot use Haskell's `Integral` class since the `Real` and `Enum` superclasses are not implementable for symbolic bit-vectors. However, `quotRem` makes perfect sense, and the `BVDivisible` class captures this operation. One issue is how division by 0 behaves. The verification technology requires total functions, and there are several design choices here. We follow Isabelle/HOL approach of assigning the value 0 for division by 0. Therefore, we impose the following law:

` x `bvQuotRem` 0 = (0, x)`

Note that our instances implement this law even when `x` is `0` itself.

Minimal complete definition: `bvQuotRem`

Methods

bvQuotRem :: a -> a -> (a, a)Source

## The Boolean class

class Boolean b whereSource

The `Boolean` class: a generalization of Haskell's `Bool` type Haskell `Bool` and SBV's `SBool` are instances of this class, unifying the treatment of boolean values.

Minimal complete definition: `true`, `bnot`, `&&&` However, it's advisable to define `false`, and `|||` as well (typically), for clarity.

Methods

true :: bSource

logical true

false :: bSource

logical false

bnot :: b -> bSource

complement

(&&&) :: b -> b -> bSource

and

(|||) :: b -> b -> bSource

or

(~&) :: b -> b -> bSource

nand

(~|) :: b -> b -> bSource

nor

(<+>) :: b -> b -> bSource

xor

(==>) :: b -> b -> bSource

implies

(<=>) :: b -> b -> bSource

equivalence

fromBool :: Bool -> bSource

cast from Bool

Instances

 Boolean Bool Boolean SBool

### Generalizations of boolean operations

bAnd :: Boolean b => [b] -> bSource

Generalization of `and`

bOr :: Boolean b => [b] -> bSource

Generalization of `or`

bAny :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of `any`

bAll :: Boolean b => (a -> b) -> [a] -> bSource

Generalization of `all`

## Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a whereSource

PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.

Minimal complete definition: `hexS` and `binS`

Methods

hexS :: a -> StringSource

Show a number in hexadecimal (starting with `0x` and type.)

binS :: a -> StringSource

Show a number in binary (starting with `0b` and type.)

hex :: a -> StringSource

Show a number in hex, without prefix, or types.

bin :: a -> StringSource

Show a number in bin, without prefix, or types.

Instances

 PrettyNum Bool PrettyNum Int8 PrettyNum Int16 PrettyNum Int32 PrettyNum Int64 PrettyNum Integer PrettyNum Word8 PrettyNum Word16 PrettyNum Word32 PrettyNum Word64 PrettyNum CW (SymWord a, PrettyNum a) => PrettyNum (SBV a)

readBin :: Num a => String -> aSource

A more convenient interface for reading binary numbers, also supports negative numbers

# Uninterpreted sorts, constants, and functions

Users can introduce new uninterpreted sorts simply by defining a data-type in Haskell and registering it as such. The following example demonstrates:

```     data B = B deriving (Eq, Ord, Data, Typeable)
instance SymWord  B
```

(Note that you'll also need to use the language pragma `DeriveDataTypeable`, and import `Data.Generics` for the above to work.)

Once GHC implements derivable user classes (http://hackage.haskell.org/trac/ghc/ticket/5462), we will be able to simplify this to:

```     data B = B deriving (Eq, Ord, Data, Typeable, SymWord, HasKind)
```

This is all it takes to introduce `B` as an uninterpreted sort in SBV, which makes the type `SBV B` automagically become available as the type of symbolic values that ranges over `B` values.

Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by the `Uninterpreted` class.

class Uninterpreted a whereSource

Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.

Minimal complete definition: `sbvUninterpret`. However, most instances in practice are already provided by SBV, so end-users should not need to define their own instances.

Methods

uninterpret :: String -> aSource

cgUninterpret :: String -> [String] -> a -> aSource

Uninterpret a value, only for the purposes of code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.

sbvUninterpret :: Maybe ([String], a) -> String -> aSource

Most generalized form of uninterpretation, this function should not be needed by end-user-code, but is rather useful for the library development.

Instances

 HasKind a => Uninterpreted (SBV a) (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) (SymWord h, SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord g, SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord f, SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord e, SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a) (SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a) (SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a)

addAxiom :: String -> [String] -> Symbolic ()Source

Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.

# Properties, proofs, and satisfiability

The SBV library provides a push-button verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://goedel.cs.uiowa.edu/smtlib/) to communicate with arbitrary SMT solvers. Unfortunately, the SMT-Lib version 1.X does not standardize how models are communicated back from solvers, so there is some work in parsing individual SMT solver output. The 2.X version of the SMT-Lib standard (not yet implemented by SMT solvers widely, unfortunately) will bring new standard features for getting models; at which time the SBV framework can be modified into a truly plug-and-play system where arbitrary SMT solvers can be used.

## Predicates

A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The `Symbolic` monad captures the underlying representation, and can/should be ignored by the users of the library, unless you are building further utilities on top of SBV itself. Instead, simply use the `Predicate` type when necessary.

class Provable a whereSource

A type `a` is provable if we can turn it into a predicate. Note that a predicate can be made from a curried function of arbitrary arity, where each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So predicates can be constructed from almost arbitrary Haskell functions that have arbitrary shapes. (See the instance declarations below.)

Methods

forAll_ :: a -> PredicateSource

Turns a value into a universally quantified predicate, internally naming the inputs. In this case the sbv library will use names of the form `s1, s2`, etc. to name these variables Example:

```  forAll_ \$ \(x::SWord8) y -> x `shiftL` 2 .== y
```

is a predicate with two arguments, captured using an ordinary Haskell function. Internally, `x` will be named `s0` and `y` will be named `s1`.

forAll :: [String] -> a -> PredicateSource

Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:

```  forAll ["x", "y"] \$ \(x::SWord8) y -> x `shiftL` 2 .== y
```

This is the same as above, except the variables will be named `x` and `y` respectively, simplifying the counter-examples when they are printed.

forSome_ :: a -> PredicateSource

Turns a value into an existentially quantified predicate. (Indeed, `exists` would have been a better choice here for the name, but alas it's already taken.)

forSome :: [String] -> a -> PredicateSource

Version of `forSome` that allows user defined names

Instances

 Provable SBool Provable Predicate (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) (HasKind a, HasKind b, SymArray array, Provable p) => Provable (array a b -> p) (SymWord a, Provable p) => Provable (SBV a -> p)

class Equality a whereSource

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

Methods

(===) :: a -> a -> IO ThmResultSource

Instances

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

## Proving properties

prove :: Provable a => a -> IO ThmResultSource

Prove a predicate, equivalent to `proveWith defaultSMTCfg`

proveWith :: Provable a => SMTConfig -> a -> IO ThmResultSource

Proves the predicate using the given SMT-solver

isTheorem :: Provable a => a -> IO BoolSource

Checks theoremhood

isTheoremWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks theoremhood within the given time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Checking satisfiability

sat :: Provable a => a -> IO SatResultSource

Find a satisfying assignment for a predicate, equivalent to `satWith defaultSMTCfg`

satWith :: Provable a => SMTConfig -> a -> IO SatResultSource

Find a satisfying assignment using the given SMT-solver

isSatisfiable :: Provable a => a -> IO BoolSource

Checks satisfiability

isSatisfiableWithin :: Provable a => Int -> a -> IO (Maybe Bool)Source

Checks satisfiability within the given time limit of `i` seconds. Returns `Nothing` if times out, or the result wrapped in a `Just` otherwise.

## Finding all satisfying assignments

allSat :: Provable a => a -> IO AllSatResultSource

Return all satisfying assignments for a predicate, equivalent to `allSatWith defaultSMTCfg`. Satisfying assignments are constructed lazily, so they will be available as returned by the solver and on demand.

NB. Uninterpreted constant/function values and counter-examples for array values are ignored for the purposes of `allSat`. That is, only the satisfying assignments modulo uninterpreted functions and array inputs will be returned. This is due to the limitation of not having a robust means of getting a function counter-example back from the SMT solver.

allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResultSource

Find all satisfying assignments using the given SMT-solver

numberOfModels :: Provable a => a -> IO IntSource

Returns the number of models that satisfy the predicate, as it would be returned by `allSat`. Note that the number of models is always a finite number, and hence this will always return a result. Of course, computing it might take quite long, as it literally generates and counts the number of satisfying models.

## Satisfying a sequence of boolean conditions

solve :: [SBool] -> Symbolic SBoolSource

Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:

```   do [x, y, z] <- sIntegers ["x", "y", "z"]
solve [x .> 5, y + z .< x]
```

A constraint is a means for restricting the input domain of a formula. Here's a simple example:

```   do x <- `exists` "x"
y <- `exists` "y"
`constrain` \$ x .> y
`constrain` \$ x + y .>= 12
`constrain` \$ y .>= 3
...
```

The first constraint requires `x` to be larger than `y`. The scond one says that sum of `x` and `y` must be at least `12`, and the final one says that `y` to be at least `3`. Constraints provide an easy way to assert additional properties on the input domain, right at the point of the introduction of variables.

Note that the proper reading of a constraint depends on the context:

• In a `sat` (or `allSat`) call: The constraint added is asserted conjunctively. That is, the resulting satisfying model (if any) will always satisfy all the constraints given.
• In a `prove` call: In this case, the constraint acts as an implication. The property is proved under the assumption that the constraint holds. In other words, the constraint says that we only care about the input space that satisfies the constraint.
• In a `quickCheck` call: The constraint acts as a filter for `quickCheck`; if the constraint does not hold, then the input value is considered to be irrelevant and is skipped. Note that this is similar to `prove`, but is stronger: We do not accept a test case to be valid just because the constraints fail on them, although semantically the implication does hold. We simply skip that test case as a bad test vector.
• In a `genTest` call: Similar to `quickCheck` and `prove`: If a constraint does not hold, the input value is ignored and is not included in the test set.

A good use case (in fact the motivating use case) for `constrain` is attaching a constraint to a `forall` or `exists` variable at the time of its creation. Also, the conjunctive semantics for `sat` and the implicative semantics for `prove` simplify programming by choosing the correct interpretation automatically. However, one should be aware of the semantic difference. For instance, in the presence of constraints, formulas that are provable are not necessarily satisfiable. To wit, consider:

```    do x <- `exists` "x"
`constrain` \$ x .< x
return \$ x .< (x :: `SWord8`)
```

This predicate is unsatisfiable since no element of `SWord8` is less than itself. But it's (vacuously) true, since it excludes the entire domain of values, thus making the proof trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given constraints are not vacuous, the functions `isVacuous` (and `isVacuousWith`) can be used.

Also note that this semantics imply that test case generation (`genTest`) and quick-check can take arbitrarily long in the presence of constraints, if the random input values generated rarely satisfy the constraints. (As an extreme case, consider `constrain false`.)

A probabilistic constraint (see `pConstrain`) attaches a probability threshold for the constraint to be considered. For instance:

```     `pConstrain` 0.8 c
```

will make sure that the condition `c` is satisfied 80% of the time (and correspondingly, falsified 20% of the time), in expectation. This variant is useful for `genTest` and `quickCheck` functions, where we want to filter the test cases according to some probability distribution, to make sure that the test-vectors are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases with the above constraint, we'd expect about 80 of them to satisfy the condition `c`, while about 20 of them will fail it.

The following properties hold:

```    `constrain`      = `pConstrain` 1
`pConstrain` t c = `pConstrain` (1-t) (not c)
```

Note that while `constrain` can be used freely, `pConstrain` is only allowed in the contexts of `genTest` or `quickCheck`. Calls to `pConstrain` in a prove/sat call will be rejected as SBV does not deal with probabilistic constraints when it comes to satisfiability and proofs. Also, both `constrain` and `pConstrain` calls during code-generation will also be rejected, for similar reasons.

Adding a probabilistic constraint. The `Double` argument is the probability threshold. Probabilistic constraints are useful for `genTest` and `quickCheck` calls where we restrict our attention to interesting parts of the input domain.

## Checking constraint vacuity

isVacuous :: Provable a => a -> IO BoolSource

Check if the given constraints are satisfiable, equivalent to `isVacuousWith defaultSMTCfg`. This call can be used to ensure that the specified constraints (via `constrain`) are satisfiable, i.e., that the proof involving these constraints is not passing vacuously. Here is an example. Consider the following predicate:

````>>> ````let pred = do { x <- forall "x"; constrain \$ x .< x; return \$ x .>= (5 :: SWord8) }
``````

This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the values considered satisfy `x .< x`, i.e., they are less than themselves. Since there are no values that satisfy this constraint, the proof will pass vacuously:

````>>> ````prove pred
```Q.E.D.
```

We can use `isVacuous` to make sure to see that the pass was vacuous:

````>>> ````isVacuous pred
```True
```

While the above example is trivial, things can get complicated if there are multiple constraints with non-straightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:

````>>> ````let pred' = do { x <- forall "x"; constrain \$ x .> 6; return \$ x .>= (5 :: SWord8) }
``````

This time the proof passes as expected:

````>>> ````prove pred'
```Q.E.D.
```

And the proof is not vacuous:

````>>> ````isVacuous pred'
```False
```

isVacuousWith :: Provable a => SMTConfig -> a -> IO BoolSource

Determine if the constraints are vacuous using the given SMT-solver

# Optimization

Symbolic optimization. A call of the form:

`minimize Quantified cost n valid`

returns `Just xs`, such that:

• `xs` has precisely `n` elements
• `valid xs` holds
• `cost xs` is minimal. That is, for all sequences `ys` that satisfy the first two criteria above, `cost xs .<= cost ys` holds.

If there is no such sequence, then `minimize` will return `Nothing`.

The function `maximize` is similar, except the comparator is `.>=`. So the value returned has the largest cost (or value, in that case).

The function `optimize` allows the user to give a custom comparison function.

The `OptimizeOpts` argument controls how the optimization is done. If `Quantified` is used, then the SBV optimization engine satisfies the following predicate:

`exists xs. forall ys. valid xs && (valid ys ``implies`` (cost xs ``cmp`` cost ys))`

Note that this may cause efficiency problems as it involves alternating quantifiers. If `OptimizeOpts` is set to `Iterative` `True`, then SBV will programmatically search for an optimal solution, by repeatedly calling the solver appropriately. (The boolean argument controls whether progress reports are given. Use `False` for quiet operation.) Note that the quantified and iterative versions are two different optimization approaches and may not necessarily yield the same results. In particular, the quantified version can find solutions where there is no global optimum value, while the iterative version would simply loop forever in such cases. On the other hand, the iterative version might be more suitable if the quantified version of the problem is too hard to deal with by the SMT solver.

minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])Source

Minimizes a cost function with respect to a constraint. Examples:

````>>> ````minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
```Just [11,11,11]
```

maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])Source

Maximizes a cost function with respect to a constraint. Examples:

````>>> ````maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
```Just [9,9,9]
```

optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])Source

Variant of `optimizeWith` using the default solver

minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])Source

Variant of `minimize` allowing the use of a user specified solver.

maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a])Source

Variant of `maximize` allowing the use of a user specified solver.

Arguments

 :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig SMT configuration -> OptimizeOpts Optimization options -> (SBV c -> SBV c -> SBool) comparator -> ([SBV a] -> SBV c) cost function -> Int how many elements? -> ([SBV a] -> SBool) validity constraint -> IO (Maybe [a])

Symbolic optimization. Generalization on `minimize` and `maximize` that allows arbitrary cost functions and comparisons.

# Computing expected values

expectedValue :: Outputtable a => Symbolic a -> IO [Double]Source

Given a symbolic computation that produces a value, compute the expected value that value would take if this computation is run with its free variables drawn from uniform distributions of its respective values, satisfying the given constraints specified by `constrain` and `pConstrain` calls. This is equivalent to calling `expectedValueWith` the following parameters: verbose, warm-up round count of `10000`, no maximum iteration count, and with convergence margin `0.0001`.

expectedValueWith :: Outputtable a => Bool -> Int -> Maybe Int -> Double -> Symbolic a -> IO [Double]Source

Generalized version of `expectedValue`, allowing the user to specify the warm-up count and the convergence factor. Maximum iteration count can also be specified, at which point convergence won't be sought. The boolean controls verbosity.

# Model extraction

The default `Show` instances for prover calls provide all the counter-example information in a human-readable form and should be sufficient for most casual uses of sbv. However, tools built on top of sbv will inevitably need to look into the constructed models more deeply, programmatically extracting their results and performing actions based on them. The API provided in this section aims at simplifying this task.

## Inspecting proof results

`ThmResult`, `SatResult`, and `AllSatResult` are simple newtype wrappers over `SMTResult`. Their main purpose is so that we can provide custom `Show` instances to print results accordingly.

newtype ThmResult Source

A `prove` call results in a `ThmResult`

Constructors

 ThmResult SMTResult

Instances

 Show ThmResult Modelable ThmResult

newtype SatResult Source

A `sat` call results in a `SatResult` The reason for having a separate `SatResult` is to have a more meaningful `Show` instance.

Constructors

 SatResult SMTResult

Instances

 Show SatResult Modelable SatResult

newtype AllSatResult Source

An `allSat` call results in a `AllSatResult`. The boolean says whether we should warn the user about prefix-existentials.

Constructors

 AllSatResult (Bool, [SMTResult])

Instances

 Show AllSatResult

data SMTResult Source

The result of an SMT solver call. Each constructor is tagged with the `SMTConfig` that created it so that further tools can inspect it and build layers of results, if needed. For ordinary uses of the library, this type should not be needed, instead use the accessor functions on it. (Custom Show instances and model extractors.)

Constructors

 Unsatisfiable SMTConfig Unsatisfiable Satisfiable SMTConfig SMTModel Satisfiable with model Unknown SMTConfig SMTModel Prover returned unknown, with a potential (possibly bogus) model ProofError SMTConfig [String] Prover errored out TimeOut SMTConfig Computation timed out (see the `timeout` combinator)

Instances

 NFData SMTResult Modelable SMTResult

## Programmable model extraction

While default `Show` instances are sufficient for most use cases, it is sometimes desirable (especially for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable extraction allows getting arbitrarily typed models out of SMT models.

class SatModel a whereSource

Instances of `SatModel` can be automatically extracted from models returned by the solvers. The idea is that the sbv infrastructure provides a stream of `CW'`s (constant-words) coming from the solver, and the type `a` is interpreted based on these constants. Many typical instances are already provided, so new instances can be declared with relative ease.

Minimum complete definition: `parseCWs`

Methods

parseCWs :: [CW] -> Maybe (a, [CW])Source

Given a sequence of constant-words, extract one instance of the type `a`, returning the remaining elements untouched. If the next element is not what's expected for this type you should return `Nothing`

cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])Source

Given a parsed model instance, transform it using `f`, and return the result. The default definition for this method should be sufficient in most use cases.

Instances

 SatModel Bool SatModel Int8 SatModel Int16 SatModel Int32 SatModel Int64 SatModel Integer SatModel Word8 SatModel Word16 SatModel Word32 SatModel Word64 SatModel () Base case, that comes in handy if there are no real variables SatModel AlgReal SatModel U2Member SatModel a => SatModel [a] (SatModel a, SatModel b) => SatModel (a, b) (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g)

class Modelable a whereSource

Various SMT results that we can extract models out of.

Methods

modelExists :: a -> BoolSource

Is there a model?

getModel :: SatModel b => a -> Either String (Bool, b)Source

Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was probable. (i.e., if the solver returned unknown.)

extractModel :: SatModel b => a -> Maybe bSource

A simpler variant of `getModel` to get a model out without the fuss.

Instances

 Modelable SatResult Modelable ThmResult Modelable SMTResult

displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO IntSource

Given an `allSat` call, we typically want to iterate over it and print the results in sequence. The `displayModels` function automates this task by calling `disp` on each result, consecutively. The first `Int` argument to `disp` 'is the current model number. The second argument is a tuple, where the first element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)

extractModels :: SatModel a => AllSatResult -> [a]Source

Return all the models from an `allSat` call, similar to `extractModel` but is suitable for the case of multiple results.

# SMT Interface: Configurations and solvers

data SMTConfig Source

Solver configuration. See also `z3` and `yices`, which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as `z3{verbose=True}`.)

Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite precision value on the screen. The field `printRealPrec` controls the printing precision, by specifying the number of digits after the decimal point. The default value is 16, but it can be set to any positive integer.

When printing, SBV will add the suffix `...` at the and of a real-value, if the given bound is not sufficient to represent the real-value exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation of the real value is not finite, i.e., if it is not rational.

Constructors

 SMTConfig Fieldsverbose :: BoolDebug mode timing :: BoolPrint timing information on how long different phases took (construction, solving, etc.) timeOut :: Maybe IntHow much time to give to the solver. (In seconds) printBase :: IntPrint integral literals in this base (2, 8, and 10, and 16 are supported.) printRealPrec :: IntPrint algebraic real values with this precision. (SReal, default: 16) solverTweaks :: [String]Additional lines of script to give to the solver (user specified) smtFile :: Maybe FilePathIf Just, the generated SMT script will be put in this file (for debugging purposes mostly) useSMTLib2 :: BoolIf True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 solver :: SMTSolverThe actual SMT solver.

Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.

Constructors

 Iterative Bool Iteratively search. if True, it will be reporting progress Quantified Use quantifiers

data SMTSolver Source

An SMT solver

Constructors

 SMTSolver Fieldsname :: StringPrintable name of the solver executable :: StringThe path to its executable options :: [String]Options to provide to the solver engine :: SMTEngineThe solver engine, responsible for interpreting solver output

Default configuration for the Yices SMT Solver.

Default configuration for the Z3 SMT solver

The default solver used by SBV. This is currently set to z3.

Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.

# Symbolic computations

data Symbolic a Source

A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.

Instances

output :: Outputtable a => a -> Symbolic aSource

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

class (HasKind a, Ord a) => SymWord a whereSource

A `SymWord` is a potential symbolic bitvector that can be created instances of to be fed to a symbolic program. Note that these methods are typically not needed in casual uses with `prove`, `sat`, `allSat` etc, as default instances automatically provide the necessary bits.

Methods

Create a user named input (universal)

Create an automatically named input

Get a bunch of new words

Create an existential variable

Create an automatically named existential variable

Create a bunch of existentials

free :: String -> Symbolic (SBV a)Source

Create a free variable, universal in a proof, existential in sat

Create an unnamed free variable, universal in proof, existential in sat

Create a bunch of free vars

Similar to free; Just a more convenient name

symbolics :: [String] -> Symbolic [SBV a]Source

Similar to mkFreeVars; but automatically gives names based on the strings

literal :: a -> SBV aSource

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe aSource

Extract a literal, if the value is concrete

fromCW :: CW -> aSource

Extract a literal, from a CW representation

isConcrete :: SBV a -> BoolSource

Is the symbolic word concrete?

isSymbolic :: SBV a -> BoolSource

Is the symbolic word really symbolic?

isConcretely :: SBV a -> (a -> Bool) -> BoolSource

Does it concretely satisfy the given predicate?

max/minbounds, if available. Note that we don't want to impose Bounded on our class as Integer is not Bounded but it is a SymWord

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a)Source

One stop allocator

Instances

 SymWord Bool SymWord Int8 SymWord Int16 SymWord Int32 SymWord Int64 SymWord Integer SymWord Word8 SymWord Word16 SymWord Word32 SymWord Word64 SymWord AlgReal SymWord B SymWord Q We need `SymWord` and `HasKind` instances, but default definitions are always sufficient for uninterpreted sorts, so all we do is to declare them as such. Note that, starting with GHC 7.6.1, we will be able to simply derive these classes as well. (See http://hackage.haskell.org/trac/ghc/ticket/5462.)

# Getting SMT-Lib output (for offline analysis)

compileToSMTLib :: Provable a => Bool -> a -> IO StringSource

Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library. If `smtLib2` parameter is False, then we will generate SMTLib1 output, otherwise we will generate SMTLib2 output

generateSMTBenchmarks :: Provable a => FilePath -> a -> IO ()Source

Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, SMT-Lib1 version will be written with suffix .smt1 and SMT-Lib2 version will be written with suffix .smt2

# Test case generation

genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectorsSource

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function `output` call to indicate what fields should be in the test result. (Also see `constrain` and `pConstrain` for filtering acceptable test values.)

getTestValues :: TestVectors -> [([CW], [CW])]Source

Retrieve the test vectors for further processing. This function is useful in cases where `renderTest` is not sufficient and custom output (or further preprocessing) is needed.

Type of test vectors (abstract)

data TestStyle Source

Test output style

Constructors

 Haskell String As a Haskell value with given name C String As a C array of structs with given name Forte String Bool ([Int], [Int]) As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values

Render the test as a Haskell value with the given name `n`.

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.

Constructors

 CW FieldscwKind :: !Kind cwVal :: !CWVal

Instances

 Eq CW Ord CW Show CW NFData CW HasKind CW BVDivisible CW PrettyNum CW

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf. This class can be automatically derived for data-types that have a `Data` instance; this is useful for creating uninterpreted sorts.

Instances

data Kind Source

Kind of symbolic value

Constructors

 KBounded Bool Int KUnbounded KReal KUninterpreted String

Instances

 Eq Kind Ord Kind Show Kind NFData Kind

Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)

# Code generation from symbolic programs

The SBV library can generate straight-line executable code in C. (While other target languages are certainly possible, currently only C is supported.) The generated code will perform no run-time memory-allocations, (no calls to `malloc`), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the same instructions in all calls, so they have predictable timing properties as well. The generated code has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling, these characteristics make them suitable for use in hard real-time systems, as well as in traditional computing.

data SBVCodeGen a Source

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

Instances

## Setting code-generation options

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: `False`.

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

Should we generate a driver program? Default: `True`. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See `compileToCLib`.)

Should we generate a Makefile? Default: `True`.

## Designating inputs

cgInput :: SymWord a => String -> SBVCodeGen (SBV a)Source

Creates an atomic input in the generated code.

cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]Source

Creates an array input in the generated code.

## Designating outputs

cgOutput :: SymWord a => String -> SBV a -> SBVCodeGen ()Source

Creates an atomic output in the generated code.

cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()Source

Creates an array output in the generated code.

## Designating return values

cgReturn :: SymWord a => SBV a -> SBVCodeGen ()Source

Creates a returned (unnamed) value in the generated code.

cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()Source

Creates a returned (unnamed) array value in the generated code.

## Code generation with uninterpreted functions

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

## Code generation with `SInteger` and `SReal` types

The types `SInteger` and `SReal` are unbounded quantities that have no direct counterparts in the C language. Therefore, it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to overflow/underflows for `SInteger`, and rounding for `SReal`, so there is an implicit loss of precision.

If the user does not specify these mappings, then SBV will refuse to compile programs that involve these types.

Sets number of bits to be used for representing the `SInteger` type in the generated C code. The argument must be one of `8`, `16`, `32`, or `64`. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

Sets the C type to be used for representing the `SReal` type in the generated C code. The setting can be one of C's `float`, `double`, or `long double`, types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

Possible mappings for the `SReal` type when translated to C. Used in conjunction with the function `cgSRealType`. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

 CgFloat `float` CgDouble `double` CgLongDouble `long double`

Instances

 Eq CgSRealType Show CgSRealType

## Compilation to C

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass `Just "."`. Use `Nothing` for printing to stdout.
• The second argument is the name of the C function to generate.
• The final argument is the function to be compiled.

Compilation will also generate a `Makefile`, a header file, and a driver (test) program, etc.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()Source

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass `Just "."`. Use `Nothing` for printing to stdout.
• The second argument is the name of the archive to generate.
• The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of `compileToC`, except in a list.

# Module exports

The SBV library exports the following modules wholesale, as user programs will have to import these modules to make any sensible use of the SBV functionality.

module Data.Bits

module Data.Word

module Data.Int

module Data.Ratio