The Symbolic value. Either a constant (Left) or a symbolic value (Right Cached). Note that caching is essential for making sure sharing is preserved.

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf, unless you can take advantage of the default signature: This class can be automatically derived for data-types that have a Data instance; this is useful for creating uninterpreted sorts. So, in reality, end users should almost never need to define any methods.

Kind of symbolic value

CW represents a concrete word of a fixed size: For signed words, the most significant digit is considered to be the sign.

A constant value

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

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

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

Read the array element at a

Update the element at a to be b

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

Create a named new array, with an optional initial value

Compare two arrays for equality

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.

Quantifiers: forall or exists. Note that we allow arbitrary nestings.

Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. If not, then we pick the quantifier appropriately based on the run-mode. randomCW is used for generating random values for this variable when used for quickCheck or genTest purposes.

Create an N-bit symbolic unsigned named variable

Create an N-bit symbolic unsigned unnamed variable

Create an N-bit symbolic signed named variable

Create an N-bit symbolic signed unnamed variable

Boolean True.

Boolean False.

Convert from a Boolean.

Extract a bool, by properly interpreting the integer stored.

Convert from an Integer.

Extract an integer from a concrete value.

Convert from a Float

Convert from a Float

Convert from a Rational

Grab the numerator of an SReal, if available

Grab the denominator of an SReal, if available

Equality.

Inequality.

Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like [1, 5 .. 200] :: [SInt8] work just fine (end evaluate to empty list), since we see [1, 5 .. -56] in the Integer domain. Also note the explicit check for s /= f below to make sure we don't stutter and produce an infinite list.

Less than.

Greater than.

Less than or equal to.

Greater than or equal to.

Addition.

Multiplication.

Subtraction.

Unary minus.

Absolute value.

Division.

Quotient: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "div" operator (Euclidean division, which always has a non-negative remainder). For unsigned bitvectors, it is "bvudiv"; and for signed bitvectors it is "bvsdiv", which rounds toward zero. Division by 0 is defined s.t. x/0 = 0, which holds even when x itself is 0.

Remainder: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "mod" operator (always non-negative). For unsigned bitvectors, it is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds toward zero (sign of remainder matches that of x). Division by 0 is defined s.t. x/0 = 0, which holds even when x itself is 0.

Combination of quot and rem

Exponentiation.

Add a constant value:

Increment:

Decrement:

Bitwise and.

Bitwise or.

Bitwise xor.

Bitwise complement.

Shift left by a constant amount. Translates to the "bvshl" operation in SMT-Lib.

Shift right by a constant amount. Translates to either "bvlshr" (logical shift right) or "bvashr" (arithmetic shift right) in SMT-Lib, depending on whether x is a signed bitvector.

Rotate-left, by a constant

Rotate-right, by a constant

Extract bit-sequences.

Join two words, by concataneting

Convert a symbolic bitvector from unsigned to signed.

Convert a symbolic bitvector from signed to unsigned.

Convert a symbolic bitvector from one integral kind to another.

Total indexing operation. svSelect xs default index is intuitively the same as xs !! index, except it evaluates to default if index overflows. Translates to SMT-Lib tables.

Convert an SVal from kind Bool to an unsigned bitvector of size 1.

Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.

Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.

Set a given bit at index

Generalization of svShl, where the shift-amount is symbolic.

Generalization of svShr, where the shift-amount is symbolic.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical.

Generalization of svRol, where the rotation amount is symbolic. If the first argument is not bounded, then the this is the same as shift.

Generalization of svRor, where the rotation amount is symbolic. If the first argument is not bounded, then the this is the same as shift.

Un-bit-blast from little-endian representation to a word of the right size. The input is assumed to be unsigned.

Un-bit-blast from big-endian representation to a word of the right size. The input is assumed to be unsigned.

Bit-blast: Little-endian. Assumes the input is a bit-vector.

Bit-blast: Big-endian. Assumes the input is a bit-vector.

If-then-else. This one will force branches.

Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.

Merge two symbolic values, at kind k, possibly force'ing the branches to make sure they do not evaluate to the same result.

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.

Proves the predicate using the given SMT-solver

Find a satisfying assignment using the given SMT-solver

Find all satisfying assignments using the given SMT-solver

Check safety using the given SMT-solver

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

Dynamic variant of quick-check

A prove call results in a ThmResult

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

An allSat call results in a AllSatResult. The first boolean says whether we hit the max-model limit as we searched. The second boolean says whether there were prefix-existentials.

A safe call results in a SafeResult

An optimize call results in a OptimizeResult. In the ParetoResult case, the boolean is True if we reached pareto-query limit and so there might be more unqueried results remaining. If False, it means that we have all the pareto fronts returned. See the Pareto OptimizeStyle for details.

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

Parse a signed/sized value from a sequence of CWs

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

Extract a model dictionary. Extract a dictionary mapping the variables to their respective values as returned by the SMT solver. Also see getModelDictionaries.

Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. 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.

The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.

Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.

Solvers that SBV is aware of