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

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$ \x -> x shiftL 2 .== 2 * (x :: SWord8)
Falsifiable. Counter-example:
s0 = 32 :: Word8


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 types listed below. Functions for checking satisfiability (sat and allSat) are also provided.

The sbv library introduces the following symbolic types:

• SBool: Symbolic Booleans (bits).
• SWord8, SWord16, SWord32, SWord64: Symbolic Words (unsigned).
• SInt8, SInt16, SInt32, SInt64: Symbolic Ints (signed).
• SInteger: Unbounded signed integers.
• SReal: Algebraic-real numbers
• SFloat: IEEE-754 single-precision floating point values
• SDouble: IEEE-754 double-precision floating point values
• 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.

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

The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the following SMT-Solvers out-of-the box:

SBV also allows calling these solvers in parallel, either getting results from multiple solvers or returning the fastest one. (See proveWithAll, proveWithAny, etc.)

Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.

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

Incremental mode: Queries

SBV provides a wide variety of ways to utilize SMT-solvers, without requiring the user to deal with the solvers themselves. While this mode is convenient, advanced users might need access to the underlying solver, using the SMTLib language. For such use cases, SBV allows users to have an interactive session: The user can issue commands to the solver, inspect the values/results, and formulate new constraints. This advanced feature is available through the Data.SBV.Control module, where most SMTLib features are made available via a typed-API.

Symbolic types

Symbolic bit

type SBool = SBV Bool Source #

A symbolic boolean/bit

Unsigned symbolic bit-vectors

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 Int8 Source #

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

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

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

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 (+, -, *, sQuotRem, sQuot, sRem, sDivMod, sDiv, sMod) and logical operations (.<, .<=, .>, .>=, .==, ./=) operations are supported for SInteger fully, both in programming and verification modes.

Infinite precision signed symbolic value

Floating point numbers

Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's Float and Double types. For SMT support with floating-point numbers, see the paper by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.

IEEE-754 single-precision floating point numbers

IEEE-754 double-precision floating point numbers

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://smtlib.cs.uiowa.edu/theories-Reals.shtml.) 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

Instances

 Source # Methods(==) :: AlgReal -> AlgReal -> Bool #(/=) :: AlgReal -> AlgReal -> Bool # Source # NB: Following the other types we have, we require a/0 to be 0 for all a. Methods Source # Methods Source # Methods(<) :: AlgReal -> AlgReal -> Bool #(<=) :: AlgReal -> AlgReal -> Bool #(>) :: AlgReal -> AlgReal -> Bool #(>=) :: AlgReal -> AlgReal -> Bool # Source # Methods Source # MethodsshowList :: [AlgReal] -> ShowS # Random AlgReal Source # MethodsrandomR :: RandomGen g => (AlgReal, AlgReal) -> g -> (AlgReal, g)random :: RandomGen g => g -> (AlgReal, g)randomRs :: RandomGen g => (AlgReal, AlgReal) -> g -> [AlgReal]randoms :: RandomGen g => g -> [AlgReal]randomRIO :: (AlgReal, AlgReal) -> IO AlgReal Arbitrary AlgReal Source # Methodsarbitrary :: Gen AlgRealshrink :: AlgReal -> [AlgReal] Source # Methods Source # AlgReal as extracted from a model MethodsparseCWs :: [CW] -> Maybe (AlgReal, [CW]) Source #cvtModel :: (AlgReal -> Maybe b) -> Maybe (AlgReal, [CW]) -> Maybe (b, [CW]) Source # Source # MethodssexprToVal :: SExpr -> Maybe AlgReal Source # Source # Methods

Convert an SReal to an SInteger. That is, it computes the largest integer n that satisfies sIntegerToSReal n <= r essentially giving us the floor.

For instance, 1.3 will be 1, but -1.3 will be -2.

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

Declare an SReal

Declare an SFloat

Declare an SDouble

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 SBools

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

Declare a list of SWord8s

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

Declare a list of SWord16s

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

Declare a list of SWord32s

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

Declare a list of SWord64s

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

Declare a list of SInt8s

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

Declare a list of SInt16s

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

Declare a list of SInt32s

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

Declare a list of SInt64s

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

Declare a list of SIntegers

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

Declare a list of SReals

sFloats :: [String] -> Symbolic [SFloat] Source #

Declare a list of SFloats

sDoubles :: [String] -> Symbolic [SDouble] Source #

Declare a list of SDoubles

Abstract SBV type

data SBV a Source #

The Symbolic value. The parameter a is phantom, but is extremely important in keeping the user interface strongly typed.

Instances

class HasKind a where Source #

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

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Kind instance for Extended CW Methods Source # Kind instance for generalized CW Methods Source # Kind instance for CW Methods Source # RoundingMode kind Methods Source # Methods Source # Methods Source # Methods Source # HasKind instance; simply returning the underlying kind for the type Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Similarly, HasKinds default implementation is sufficient. Methods HasKind (SBV a) Source # MethodskindOf :: SBV a -> Kind Source #hasSign :: SBV a -> Bool Source #intSizeOf :: SBV a -> Int Source #isBoolean :: SBV a -> Bool Source #isBounded :: SBV a -> Bool Source #isReal :: SBV a -> Bool Source #isFloat :: SBV a -> Bool Source #isDouble :: SBV a -> Bool Source #isInteger :: SBV a -> Bool Source #showType :: SBV a -> String Source #

data Kind Source #

Kind of symbolic value

Constructors

 KBool KBounded !Bool !Int KUnbounded KReal KUserSort String (Either String [String]) KFloat KDouble

Instances

 Source # We want to equate user-sorts only by name Methods(==) :: Kind -> Kind -> Bool #(/=) :: Kind -> Kind -> Bool # Source # We want to order user-sorts only by name Methodscompare :: Kind -> Kind -> Ordering #(<) :: Kind -> Kind -> Bool #(<=) :: Kind -> Kind -> Bool #(>) :: Kind -> Kind -> Bool #(>=) :: Kind -> Kind -> Bool #max :: Kind -> Kind -> Kind #min :: Kind -> Kind -> Kind # Source # MethodsshowsPrec :: Int -> Kind -> ShowS #show :: Kind -> String #showList :: [Kind] -> ShowS # Source # Methods

Arrays of symbolic values

class SymArray array where Source #

Flat arrays of symbolic values An array a b is an array indexed by the type SBV a, with elements of type SBV b.

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.

Minimal complete definition

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (array a b) Source #

Create a new anonymous array

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

Create a named new array

readArray :: array a b -> SBV a -> SBV b Source #

Read the array element at a

writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b Source #

Update the element at a to be b

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b Source #

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

 Source # MethodsnewArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b) Source #newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b) Source #readArray :: SArray a b -> SBV a -> SBV b Source #writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source #

data SArray a b Source #

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 SArray values
• Typically slower as it heavily relies on SMT-solving for the array theory

Instances

 Source # MethodsnewArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b) Source #newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b) Source #readArray :: SArray a b -> SBV a -> SBV b Source #writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b Source #mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source # (HasKind a, HasKind b) => Show (SArray a b) Source # MethodsshowsPrec :: Int -> SArray a b -> ShowS #show :: SArray a b -> String #showList :: [SArray a b] -> ShowS # (HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) Source # MethodsforAll_ :: (SArray a b -> p) -> Predicate Source #forAll :: [String] -> (SArray a b -> p) -> Predicate Source #forSome_ :: (SArray a b -> p) -> Predicate Source #forSome :: [String] -> (SArray a b -> p) -> Predicate Source #prove :: (SArray a b -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> (SArray a b -> p) -> IO ThmResult Source #sat :: (SArray a b -> p) -> IO SatResult Source #satWith :: SMTConfig -> (SArray a b -> p) -> IO SatResult Source #allSat :: (SArray a b -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> (SArray a b -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult Source #isVacuous :: (SArray a b -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #isTheorem :: (SArray a b -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #isSatisfiable :: (SArray a b -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> (SArray a b -> p) -> IO String Source # SymWord b => Mergeable (SArray a b) Source # MethodssymbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #select :: (SymWord b, Num b) => [SArray a b] -> SArray a b -> SBV b -> SArray a b Source # EqSymbolic (SArray a b) Source # Methods(.==) :: SArray a b -> SArray a b -> SBool Source #(./=) :: SArray a b -> SArray a b -> SBool Source #distinct :: [SArray a b] -> SBool Source #allEqual :: [SArray a b] -> SBool Source #sElem :: SArray a b -> [SArray a b] -> SBool Source #

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

 (HasKind a, HasKind b) => Show (SFunArray a b) Source # MethodsshowsPrec :: Int -> SFunArray a b -> ShowS #show :: SFunArray a b -> String #showList :: [SFunArray a b] -> ShowS # (HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) Source # MethodsforAll_ :: (SFunArray a b -> p) -> Predicate Source #forAll :: [String] -> (SFunArray a b -> p) -> Predicate Source #forSome_ :: (SFunArray a b -> p) -> Predicate Source #forSome :: [String] -> (SFunArray a b -> p) -> Predicate Source #prove :: (SFunArray a b -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> (SFunArray a b -> p) -> IO ThmResult Source #sat :: (SFunArray a b -> p) -> IO SatResult Source #satWith :: SMTConfig -> (SFunArray a b -> p) -> IO SatResult Source #allSat :: (SFunArray a b -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> (SFunArray a b -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult Source #isVacuous :: (SFunArray a b -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #isTheorem :: (SFunArray a b -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #isSatisfiable :: (SFunArray a b -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> (SFunArray a b -> p) -> IO String Source # SymWord b => Mergeable (SFunArray a b) Source # MethodssymbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #select :: (SymWord b, Num b) => [SFunArray a b] -> SFunArray a b -> SBV b -> SFunArray a b Source #

mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source #

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

Operations on symbolic values

Word level

sTestBit :: SBV a -> Int -> SBool Source #

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.

sExtractBits :: SBV a -> [Int] -> [SBool] Source #

Variant of sTestBit, where we want to extract multiple bit positions.

sPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8 Source #

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

sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Generalization of shiftL, when the shift-amount is symbolic. Since Haskell's shiftL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Generalization of shiftR, when the shift-amount is symbolic. Since Haskell's shiftR only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical, following the usual Haskell convention. See sSignedShiftArithRight for a variant that explicitly uses the msb as the sign bit, even for unsigned underlying types.

sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a Source #

Generalization of rotateL, when the shift-amount is symbolic. Since Haskell's rotateL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a Source #

Generalization of rotateR, when the shift-amount is symbolic. Since Haskell's rotateR only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with. The first argument should be a bounded quantity.

sSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #

Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent to sShiftRight when the argument is signed. However, if the argument is unsigned, then it explicitly treats its msb as a sign-bit, and uses it as the bit that gets shifted in. Useful when using the underlying unsigned bit representation to implement custom signed operations. Note that there is no direct Haskell analogue of this function.

sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b Source #

Conversion between integral-symbolic values, akin to Haskell's fromIntegral

setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a Source #

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 a Source #

Returns 1 if the boolean is true, otherwise 0.

lsb :: SBV a -> SBool Source #

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

msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool Source #

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

label :: SymWord a => String -> SBV a -> SBV a Source #

label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy.

fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a) Source #

N.B. Only works for unsigned types. Signed arguments will be rejected.

fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a) Source #

Full multiplier: Returns both the high-order and the low-order bits in a tuple, thus fully accounting for the overflow.

N.B. Only works for unsigned types. Signed arguments will be rejected.

N.B. The higher-order bits are determined using a simple shift-add multiplier, thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently with properties involving this function, at least with the current state of the art.

Exponentiation

(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b Source #

Symbolic exponentiation using bit blasting and repeated squaring.

N.B. The exponent must be unsigned. Signed exponents will be rejected.

Blasting/Unblasting

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

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

blastLE :: (Num a, 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 where Source #

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 definition: fromBitsLE

Minimal complete definition

fromBitsLE

Methods

fromBitsLE, fromBitsBE :: [SBool] -> a Source #

Instances

 Source # MethodsfromBitsLE :: [SBool] -> SInt64 Source #fromBitsBE :: [SBool] -> SInt64 Source # Source # MethodsfromBitsLE :: [SBool] -> SInt32 Source #fromBitsBE :: [SBool] -> SInt32 Source # Source # MethodsfromBitsLE :: [SBool] -> SInt16 Source #fromBitsBE :: [SBool] -> SInt16 Source # Source # MethodsfromBitsLE :: [SBool] -> SInt8 Source #fromBitsBE :: [SBool] -> SInt8 Source # Source # MethodsfromBitsLE :: [SBool] -> SWord64 Source #fromBitsBE :: [SBool] -> SWord64 Source # Source # MethodsfromBitsLE :: [SBool] -> SWord32 Source #fromBitsBE :: [SBool] -> SWord32 Source # Source # MethodsfromBitsLE :: [SBool] -> SWord16 Source #fromBitsBE :: [SBool] -> SWord16 Source # Source # MethodsfromBitsLE :: [SBool] -> SWord8 Source #fromBitsBE :: [SBool] -> SWord8 Source # Source # MethodsfromBitsLE :: [SBool] -> SBool Source #fromBitsBE :: [SBool] -> SBool Source # Source # Conversion from bits MethodsfromBitsLE :: [SBool] -> SWord4 Source #fromBitsBE :: [SBool] -> SWord4 Source #

Splitting, joining, and extending

class Splittable a b | b -> a where Source #

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.

Minimal complete definition

Methods

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

(#) :: b -> b -> a infixr 5 Source #

extend :: b -> a Source #

Instances

 Source # Joiningsplitting tofrom Word8 Methodssplit :: Word8 -> (Word4, Word4) Source # Source # Methodssplit :: Word16 -> (Word8, Word8) Source # Source # Methodssplit :: Word32 -> (Word16, Word16) Source # Source # Methodssplit :: Word64 -> (Word32, Word32) Source # Source # Methods Source # Methods Source # Methodssplit :: SWord16 -> (SWord8, SWord8) Source #

Conditionals: Mergeable values

class Mergeable a where Source #

Symbolic conditionals are modeled by the Mergeable class, describing how to merge the results of an if-then-else call with a symbolic test. SBV provides all basic types as instances of this class, so users only need to declare instances for custom data-types of their programs as needed.

A Mergeable instance may be automatically derived for a custom data-type with a single constructor where the type of each field is an instance of Mergeable, such as a record of symbolic values. Users only need to add Generic and Mergeable to the deriving clause for the data-type. See Status for an example and an illustration of what the instance would look like if written by hand.

The function select is a total-indexing function out of a list of choices with a default value, simulating array/list indexing. It's an n-way generalization of the ite function.

Minimal complete definition: None, if the type is instance of Generic. Otherwise symbolicMerge. Note that most types subject to merging are likely to be trivial instances of Generic.

Methods

symbolicMerge :: Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a Source #

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

symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a Source #

Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.

Instances

 Source # MethodssymbolicMerge :: Bool -> SBool -> () -> () -> () Source #select :: (SymWord b, Num b) => [()] -> () -> SBV b -> () Source # Source # Methodsselect :: (SymWord b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek Source # Source # Methodsselect :: (SymWord b, Num b) => [Status] -> Status -> SBV b -> Status Source # Mergeable a => Mergeable [a] Source # MethodssymbolicMerge :: Bool -> SBool -> [a] -> [a] -> [a] Source #select :: (SymWord b, Num b) => [[a]] -> [a] -> SBV b -> [a] Source # Mergeable a => Mergeable (Maybe a) Source # MethodssymbolicMerge :: Bool -> SBool -> Maybe a -> Maybe a -> Maybe a Source #select :: (SymWord b, Num b) => [Maybe a] -> Maybe a -> SBV b -> Maybe a Source # SymWord a => Mergeable (SBV a) Source # MethodssymbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a Source #select :: (SymWord b, Num b) => [SBV a] -> SBV a -> SBV b -> SBV a Source # Mergeable a => Mergeable (Move a) Source # Mergeable instance for Move simply pushes the merging the data after run of each branch starting from the same state. MethodssymbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a Source #select :: (SymWord b, Num b) => [Move a] -> Move a -> SBV b -> Move a Source # Mergeable b => Mergeable (a -> b) Source # MethodssymbolicMerge :: Bool -> SBool -> (a -> b) -> (a -> b) -> a -> b Source #select :: (SymWord b, Num b) => [a -> b] -> (a -> b) -> SBV b -> a -> b Source # (Mergeable a, Mergeable b) => Mergeable (Either a b) Source # MethodssymbolicMerge :: Bool -> SBool -> Either a b -> Either a b -> Either a b Source #select :: (SymWord b, Num b) => [Either a b] -> Either a b -> SBV b -> Either a b Source # (Mergeable a, Mergeable b) => Mergeable (a, b) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b) -> (a, b) -> (a, b) Source #select :: (SymWord b, Num b) => [(a, b)] -> (a, b) -> SBV b -> (a, b) Source # (Ix a, Mergeable b) => Mergeable (Array a b) Source # MethodssymbolicMerge :: Bool -> SBool -> Array a b -> Array a b -> Array a b Source #select :: (SymWord b, Num b) => [Array a b] -> Array a b -> SBV b -> Array a b Source # SymWord b => Mergeable (SFunArray a b) Source # MethodssymbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b Source #select :: (SymWord b, Num b) => [SFunArray a b] -> SFunArray a b -> SBV b -> SFunArray a b Source # SymWord b => Mergeable (SArray a b) Source # MethodssymbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b Source #select :: (SymWord b, Num b) => [SArray a b] -> SArray a b -> SBV b -> SArray a b Source # (SymWord e, Mergeable (SBV e)) => Mergeable (STree i e) Source # MethodssymbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e Source #select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e Source # (Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b, c) -> (a, b, c) -> (a, b, c) Source #select :: (SymWord b, Num b) => [(a, b, c)] -> (a, b, c) -> SBV b -> (a, b, c) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #select :: (SymWord b, Num b) => [(a, b, c, d)] -> (a, b, c, d) -> SBV b -> (a, b, c, d) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #select :: (SymWord b, Num b) => [(a, b, c, d, e)] -> (a, b, c, d, e) -> SBV b -> (a, b, c, d, e) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #select :: (SymWord b, Num b) => [(a, b, c, d, e, f)] -> (a, b, c, d, e, f) -> SBV b -> (a, b, c, d, e, f) Source # (Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) Source # MethodssymbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #select :: (SymWord b, Num b) => [(a, b, c, d, e, f, g)] -> (a, b, c, d, e, f, g) -> SBV b -> (a, b, c, d, e, f, g) Source #

ite :: Mergeable a => SBool -> a -> a -> a Source #

If-then-else. This is by definition symbolicMerge with both branches forced. This is typically the desired behavior, but also see iteLazy should you need more laziness.

iteLazy :: Mergeable a => SBool -> a -> a -> a Source #

A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.

Symbolic integral numbers

class (SymWord a, Num a, Bits a) => SIntegral a Source #

Symbolic Numbers. This is a simple class that simply incorporates all number like base types 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 :: SIntegral a => [SBV a] -> SBV a
mm = foldr1 (a b -> ite (a .<= b) a b)


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

Instances

 Source # Source # Source # Source # Source # Source # Source # Source # Source # Source # SIntegral instance, using default methods

Division

class SDivisible a where Source #

The SDivisible class captures the essence of division. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic bit-vectors. However, quotRem and divMod makes perfect sense, and the SDivisible 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 pair of laws:

     x sQuotRem 0 = (0, x)
x sDivMod  0 = (0, x)


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

NB. quot truncates toward zero, while div truncates toward negative infinity.

Minimal complete definition: sQuotRem, sDivMod

Minimal complete definition

Methods

sQuotRem :: a -> a -> (a, a) Source #

sDivMod :: a -> a -> (a, a) Source #

sQuot :: a -> a -> a Source #

sRem :: a -> a -> a Source #

sDiv :: a -> a -> a Source #

sMod :: a -> a -> a Source #

Instances

 Source # MethodssQuotRem :: Int8 -> Int8 -> (Int8, Int8) Source #sDivMod :: Int8 -> Int8 -> (Int8, Int8) Source #sQuot :: Int8 -> Int8 -> Int8 Source #sRem :: Int8 -> Int8 -> Int8 Source #sDiv :: Int8 -> Int8 -> Int8 Source #sMod :: Int8 -> Int8 -> Int8 Source # Source # MethodssQuotRem :: Int16 -> Int16 -> (Int16, Int16) Source #sDivMod :: Int16 -> Int16 -> (Int16, Int16) Source # Source # MethodssQuotRem :: Int32 -> Int32 -> (Int32, Int32) Source #sDivMod :: Int32 -> Int32 -> (Int32, Int32) Source # Source # MethodssQuotRem :: Int64 -> Int64 -> (Int64, Int64) Source #sDivMod :: Int64 -> Int64 -> (Int64, Int64) Source # Source # Methods Source # MethodssQuotRem :: Word8 -> Word8 -> (Word8, Word8) Source #sDivMod :: Word8 -> Word8 -> (Word8, Word8) Source # Source # MethodssQuotRem :: Word16 -> Word16 -> (Word16, Word16) Source #sDivMod :: Word16 -> Word16 -> (Word16, Word16) Source # Source # MethodssQuotRem :: Word32 -> Word32 -> (Word32, Word32) Source #sDivMod :: Word32 -> Word32 -> (Word32, Word32) Source # Source # MethodssQuotRem :: Word64 -> Word64 -> (Word64, Word64) Source #sDivMod :: Word64 -> Word64 -> (Word64, Word64) Source # Source # MethodssQuotRem :: CW -> CW -> (CW, CW) Source #sDivMod :: CW -> CW -> (CW, CW) Source #sQuot :: CW -> CW -> CW Source #sRem :: CW -> CW -> CW Source #sDiv :: CW -> CW -> CW Source #sMod :: CW -> CW -> CW Source # Source # Methods Source # MethodssQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64) Source #sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64) Source # Source # MethodssQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32) Source #sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32) Source # Source # MethodssQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16) Source #sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16) Source # Source # MethodssQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8) Source #sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8) Source # Source # Methods Source # Methods Source # Methods Source # MethodssQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8) Source #sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8) Source # Source # SDvisible instance, using default methods MethodssQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4) Source #sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4) Source # Source # SDvisible instance, using 0-extension MethodssQuotRem :: Word4 -> Word4 -> (Word4, Word4) Source #sDivMod :: Word4 -> Word4 -> (Word4, Word4) Source #

The Boolean class

class Boolean b where Source #

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.

Minimal complete definition

Methods

true :: b Source #

logical true

false :: b Source #

logical false

bnot :: b -> b Source #

complement

(&&&) :: b -> b -> b infixr 3 Source #

and

(|||) :: b -> b -> b infixr 2 Source #

or

(~&) :: b -> b -> b infixr 3 Source #

nand

(~|) :: b -> b -> b infixr 2 Source #

nor

(<+>) :: b -> b -> b infixl 6 Source #

xor

(==>) :: b -> b -> b infixr 1 Source #

implies

(<=>) :: b -> b -> b infixr 1 Source #

equivalence

fromBool :: Bool -> b Source #

cast from Bool

Instances

 Source # Methods(&&&) :: Bool -> Bool -> Bool Source #(|||) :: Bool -> Bool -> Bool Source #(~&) :: Bool -> Bool -> Bool Source #(~|) :: Bool -> Bool -> Bool Source #(<+>) :: Bool -> Bool -> Bool Source #(==>) :: Bool -> Bool -> Bool Source #(<=>) :: Bool -> Bool -> Bool Source # Source # Methods

Generalizations of boolean operations

bAnd :: Boolean b => [b] -> b Source #

Generalization of and

bOr :: Boolean b => [b] -> b Source #

Generalization of or

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

Generalization of any

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

Generalization of all

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, Show, Read, Data, SymWord, HasKind, SatModel)


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

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. Note that the () argument is important to distinguish it from enumerations, which will be translated to proper SMT data-types.

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

class Uninterpreted a where Source #

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.

Minimal complete definition

sbvUninterpret

Methods

uninterpret :: String -> a Source #

cgUninterpret :: String -> [String] -> a -> a Source #

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 -> a Source #

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

Instances

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.

Symbolic Equality and Comparisons

class EqSymbolic a where Source #

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 -> SBool infix 4 Source #

Symbolic equality.

(./=) :: a -> a -> SBool infix 4 Source #

Symbolic inequality.

distinct :: [a] -> SBool Source #

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

allEqual :: [a] -> SBool Source #

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

sElem :: a -> [a] -> SBool Source #

Symbolic membership test.

Instances

 Source # Methodsdistinct :: [Bool] -> SBool Source #allEqual :: [Bool] -> SBool Source #sElem :: Bool -> [Bool] -> SBool Source # EqSymbolic a => EqSymbolic [a] Source # Methods(.==) :: [a] -> [a] -> SBool Source #(./=) :: [a] -> [a] -> SBool Source #distinct :: [[a]] -> SBool Source #allEqual :: [[a]] -> SBool Source #sElem :: [a] -> [[a]] -> SBool Source # EqSymbolic a => EqSymbolic (Maybe a) Source # Methods(.==) :: Maybe a -> Maybe a -> SBool Source #(./=) :: Maybe a -> Maybe a -> SBool Source #distinct :: [Maybe a] -> SBool Source #allEqual :: [Maybe a] -> SBool Source #sElem :: Maybe a -> [Maybe a] -> SBool Source # Source # Methods(.==) :: SBV a -> SBV a -> SBool Source #(./=) :: SBV a -> SBV a -> SBool Source #distinct :: [SBV a] -> SBool Source #allEqual :: [SBV a] -> SBool Source #sElem :: SBV a -> [SBV a] -> SBool Source # (EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # Methods(.==) :: Either a b -> Either a b -> SBool Source #(./=) :: Either a b -> Either a b -> SBool Source #distinct :: [Either a b] -> SBool Source #allEqual :: [Either a b] -> SBool Source #sElem :: Either a b -> [Either a b] -> SBool Source # (EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # Methods(.==) :: (a, b) -> (a, b) -> SBool Source #(./=) :: (a, b) -> (a, b) -> SBool Source #distinct :: [(a, b)] -> SBool Source #allEqual :: [(a, b)] -> SBool Source #sElem :: (a, b) -> [(a, b)] -> SBool Source # EqSymbolic (SArray a b) Source # Methods(.==) :: SArray a b -> SArray a b -> SBool Source #(./=) :: SArray a b -> SArray a b -> SBool Source #distinct :: [SArray a b] -> SBool Source #allEqual :: [SArray a b] -> SBool Source #sElem :: SArray a b -> [SArray a b] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # Methods(.==) :: (a, b, c) -> (a, b, c) -> SBool Source #(./=) :: (a, b, c) -> (a, b, c) -> SBool Source #distinct :: [(a, b, c)] -> SBool Source #allEqual :: [(a, b, c)] -> SBool Source #sElem :: (a, b, c) -> [(a, b, c)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # Methods(.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #(./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #distinct :: [(a, b, c, d)] -> SBool Source #allEqual :: [(a, b, c, d)] -> SBool Source #sElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # Methods(.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #(./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #distinct :: [(a, b, c, d, e)] -> SBool Source #allEqual :: [(a, b, c, d, e)] -> SBool Source #sElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source # Methods(.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #(./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #distinct :: [(a, b, c, d, e, f)] -> SBool Source #allEqual :: [(a, b, c, d, e, f)] -> SBool Source #sElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source # Methods(.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #(./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #distinct :: [(a, b, c, d, e, f, g)] -> SBool Source #allEqual :: [(a, b, c, d, e, f, g)] -> SBool Source #sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source #

class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #

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 -> SBool infix 4 Source #

Symbolic less than.

(.<=) :: a -> a -> SBool infix 4 Source #

Symbolic less than or equal to.

(.>) :: a -> a -> SBool infix 4 Source #

Symbolic greater than.

(.>=) :: a -> a -> SBool infix 4 Source #

Symbolic greater than or equal to.

smin :: a -> a -> a Source #

Symbolic minimum.

smax :: a -> a -> a Source #

Symbolic maximum.

inRange :: a -> (a, a) -> SBool Source #

Is the value withing the allowed inclusive range?

Instances

 OrdSymbolic a => OrdSymbolic [a] Source # Methods(.<) :: [a] -> [a] -> SBool Source #(.<=) :: [a] -> [a] -> SBool Source #(.>) :: [a] -> [a] -> SBool Source #(.>=) :: [a] -> [a] -> SBool Source #smin :: [a] -> [a] -> [a] Source #smax :: [a] -> [a] -> [a] Source #inRange :: [a] -> ([a], [a]) -> SBool Source # OrdSymbolic a => OrdSymbolic (Maybe a) Source # Methods(.<) :: Maybe a -> Maybe a -> SBool Source #(.<=) :: Maybe a -> Maybe a -> SBool Source #(.>) :: Maybe a -> Maybe a -> SBool Source #(.>=) :: Maybe a -> Maybe a -> SBool Source #smin :: Maybe a -> Maybe a -> Maybe a Source #smax :: Maybe a -> Maybe a -> Maybe a Source #inRange :: Maybe a -> (Maybe a, Maybe a) -> SBool Source # SymWord a => OrdSymbolic (SBV a) Source # Methods(.<) :: SBV a -> SBV a -> SBool Source #(.<=) :: SBV a -> SBV a -> SBool Source #(.>) :: SBV a -> SBV a -> SBool Source #(.>=) :: SBV a -> SBV a -> SBool Source #smin :: SBV a -> SBV a -> SBV a Source #smax :: SBV a -> SBV a -> SBV a Source #inRange :: SBV a -> (SBV a, SBV a) -> SBool Source # (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # Methods(.<) :: Either a b -> Either a b -> SBool Source #(.<=) :: Either a b -> Either a b -> SBool Source #(.>) :: Either a b -> Either a b -> SBool Source #(.>=) :: Either a b -> Either a b -> SBool Source #smin :: Either a b -> Either a b -> Either a b Source #smax :: Either a b -> Either a b -> Either a b Source #inRange :: Either a b -> (Either a b, Either a b) -> SBool Source # (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # Methods(.<) :: (a, b) -> (a, b) -> SBool Source #(.<=) :: (a, b) -> (a, b) -> SBool Source #(.>) :: (a, b) -> (a, b) -> SBool Source #(.>=) :: (a, b) -> (a, b) -> SBool Source #smin :: (a, b) -> (a, b) -> (a, b) Source #smax :: (a, b) -> (a, b) -> (a, b) Source #inRange :: (a, b) -> ((a, b), (a, b)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # Methods(.<) :: (a, b, c) -> (a, b, c) -> SBool Source #(.<=) :: (a, b, c) -> (a, b, c) -> SBool Source #(.>) :: (a, b, c) -> (a, b, c) -> SBool Source #(.>=) :: (a, b, c) -> (a, b, c) -> SBool Source #smin :: (a, b, c) -> (a, b, c) -> (a, b, c) Source #smax :: (a, b, c) -> (a, b, c) -> (a, b, c) Source #inRange :: (a, b, c) -> ((a, b, c), (a, b, c)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # Methods(.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #(.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #(.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #(.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source #smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source #inRange :: (a, b, c, d) -> ((a, b, c, d), (a, b, c, d)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # Methods(.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #(.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #(.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #(.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source #smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source #inRange :: (a, b, c, d, e) -> ((a, b, c, d, e), (a, b, c, d, e)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source # Methods(.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #(.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #(.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #(.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source #smin :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #smax :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #inRange :: (a, b, c, d, e, f) -> ((a, b, c, d, e, f), (a, b, c, d, e, f)) -> SBool Source # (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source # Methods(.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #(.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #(.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #(.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source #smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool Source #

class Equality a where Source #

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

Minimal complete definition

(===)

Methods

(===) :: a -> a -> IO ThmResult infix 4 Source #

Instances

 (SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z) Source # Methods(===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z) Source # Methods(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z) Source # Methods(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) Source # Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z) -> IO ThmResult Source # (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) Source # Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> z) -> IO ThmResult Source # (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) Source # Methods(===) :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> z) -> IO ThmResult Source # (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) Source # Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> z) -> IO ThmResult Source # (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) Source # Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) Source # Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z) Source # Methods(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult Source # (SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z) Source # Methods(===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult Source # (SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z) Source # Methods(===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult Source # (SymWord a, EqSymbolic z) => Equality (SBV a -> z) Source # Methods(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult Source #

Constraints

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.) Named constraints and unsat cores Constraints can be given names:  namedConstraint "a is at least 5"$ a .>= 5

Such constraints are useful when used in conjunction with getUnsatCore function where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable. This feature is enabled by the following tactic:

 tactic $SetOptions [ProduceUnsatCores True] See Data.SBV.Examples.Misc.UnsatCore for an example use case. Constraint vacuity When adding constraints, one has to be careful about making sure they are not inconsistent. The function isVacuous can be use for this purpose. Here is an example. Consider the following predicate: >>> let pred = do { x <- free "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 <- free "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  Checking for vacuity As we discussed SBV does not check that a given constraints is not vacuous. That is, that it can never be satisfied. This is usually the right behavior, since checking vacuity can be costly. The functions isVacuous and isVacuousWith should be used to explicitly check for constraint vacuity if desired. Alternatively, the tactic:  tactic$  CheckConstrVacuity True

can be given which will force SBV to run an explicit check that constraints are not vacuous. (And complain if they are!) Note that this adds an extra call to the solver for each constraint, and thus can be rather costly.

constrain :: SolverContext m => SBool -> m () Source #

Add a constraint, any satisfying instance must satisfy this condition

namedConstraint :: SolverContext m => String -> SBool -> m () Source #

Add a named constraint. The name is used in unsat-core extraction.

Cardinality constraints

A pseudo-boolean function (http://en.wikipedia.org/wiki/Pseudo-Boolean_function) is a function from booleans to reals, basically treating True as 1 and False as 0. They are typically expressed in polynomial form. Such functions can be used to express cardinality constraints, where we want to count how many things satisfy a certain condition.

One can code such constraints using regular SBV programming: Simply walk over the booleans and the corresponding coefficients, and assert the required relation. For instance:

[b0, b1, b2, b3] pbAtMost 2

is precisely equivalent to:

sum (map (\b -> ite b 1 0) [b0, b1, b2, b3]) .<= 2

and they both express that at most two of b0, b1, b2, and b3 can be true. However, the equivalent forms give rise to long formulas and the cardinality constraint can get lost in the translation. The idea here is that if you use these functions instead, SBV will produce better translations to SMTLib for more efficient solving of cardinality constraints, assuming the backend solver supports them. Currently, only Z3 supports pseudo-booleans directly. For all other solvers, SBV will translate these to equivalent terms that do not require special functions.

pbAtMost :: [SBool] -> Int -> SBool Source #

true if at most k of the input arguments are true

pbAtLeast :: [SBool] -> Int -> SBool Source #

true if at least k of the input arguments are true

pbExactly :: [SBool] -> Int -> SBool Source #

true if exactly k of the input arguments are true

pbLe :: [(Int, SBool)] -> Int -> SBool Source #

true if the sum of coefficients for true elements is at most k. Generalizes pbAtMost.

pbGe :: [(Int, SBool)] -> Int -> SBool Source #

true if the sum of coefficients for true elements is at least k. Generalizes pbAtLeast.

pbEq :: [(Int, SBool)] -> Int -> SBool Source #

true if the sum of coefficients for true elements is exactly least k. Useful for coding exactly K-of-N constraints, and in particular mutex constraints.

pbMutexed :: [SBool] -> SBool Source #

true if there is at most one set bit

true if there is exactly one set bit

Enumerations

If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually translate that as just such a data-type to SMT-Lib, and will use the constructors as the inhabitants of the said sort. A simple example is:

    data X = A | B | C
mkSymbolicEnumeration ''X


Note the magic incantation mkSymbolicEnumeration ''X. For this to work, you need to have the following options turned on:

  LANGUAGE TemplateHaskell
LANGUAGE StandaloneDeriving
LANGUAGE DeriveDataTypeable
LANGUAGE DeriveAnyClass

Now, the user can define

    type SX = SBV X


and treat SX as a regular symbolic type ranging over the values A, B, and C. Such values can be compared for equality, and with the usual other comparison operators, such as .==, ./=, .>, .>=, <, and <=.

Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple query would look like:

     allSat $x -> x .== (x :: SX)  which would list all three elements of this domain as satisfying solutions.  Solution #1: s0 = A :: X Solution #2: s0 = B :: X Solution #3: s0 = C :: X Found 3 different solutions.  Note that the result is properly typed as X elements; these are not mere strings. So, in a getModelAssignment scenario, the user can recover actual elements of the domain and program further with those values as usual. See Data.SBV.Examples.Misc.Enumerate for an extended example on how to use symbolic enumerations. Make an enumeration a symbolic type. Properties, proofs, satisfiability, and safety 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://smtlib.cs.uiowa.edu/) to communicate with arbitrary SMT solvers. A note on reasoning in the presence of quantifers Note that SBV allows reasoning with quantifiers: Inputs can be existentially or universally quantified. Predicates can be built with arbitrary nesting of such quantifiers as well. However, SBV always assumes that the input is in prenex-normal form: https://en.wikipedia.org/wiki/Prenex_normal_form. That is, all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately, the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers. SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested quantification, you will manually have to first convert to prenex-normal form (which produces an equisatisfiable but not necessarily equivalent formula), and code that explicitly in SBV. See https://github.com/LeventErkok/sbv/issues/256 for a detailed discussion of this issue. On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers, using parallel threads. Even with machines with single-cores, threading can be helpful if you want to try out multiple-solvers but do not know which one would work the best for the problem at hand ahead of time. The functions in this section allow proving/satisfiability-checking with multiple backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one. The All variants, (i.e., proveWithAll, satWithAll) run all solvers and return all the results. SBV internally makes sure that the result is lazily generated; so, the order of solvers given does not matter. In other words, the order of results will follow the order of the solvers as they finish, not as given by the user. These variants are useful when you want to make sure multiple-solvers agree (or disagree!) on a given problem. The Any variants, (i.e., proveWithAny, satWithAny) will run all the solvers in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants are useful when you do not care if the solvers produce the same result, but rather want to get the solution as quickly as possible, taking advantage of modern many-core machines. Note that the function sbvAvailableSolvers will return all the installed solvers, which can be used as the first argument to all these functions, if you simply want to try all available solvers on a machine. 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. type Goal = Symbolic () Source # A goal is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as appropriate directives for sat/prove calls. class Provable a where Source # 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.) Minimal complete definition Methods forAll_ :: a -> Predicate Source # 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 -> Predicate Source #

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 -> Predicate Source #

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 -> Predicate Source #

Version of forSome that allows user defined names.

prove :: a -> IO ThmResult Source #

Prove a predicate, using the default solver.

proveWith :: SMTConfig -> a -> IO ThmResult Source #

Prove the predicate using the given SMT-solver.

sat :: a -> IO SatResult Source #

Find a satisfying assignment for a predicate, using the default solver.

satWith :: SMTConfig -> a -> IO SatResult Source #

Find a satisfying assignment using the given SMT-solver.

allSat :: a -> IO AllSatResult Source #

Find all satisfying assignments, using the default solver. See allSatWith for details.

Return all satisfying assignments for a predicate, equivalent to allSatWith defaultSMTCfg. Note that this call will block until all satisfying assignments are found. If you have a problem with infinitely many satisfying models (consider SInteger) or a very large number of them, you might have to wait for a long time. To avoid such cases, use the allSatMaxModelCount parameter in the configuration.

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. Find all satisfying assignments using the given SMT-solver

Optimize a given collection of Objectives

Optimizes the objectives using the given SMT-solver.

isVacuous :: a -> IO Bool Source #

Check if the constraints given are consistent, using the default solver.

isVacuousWith :: SMTConfig -> a -> IO Bool Source #

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

isTheorem :: a -> IO Bool Source #

Checks theoremhood using the default solver.

isTheoremWith :: SMTConfig -> a -> IO Bool Source #

Check whether a given property is a theorem.

isSatisfiable :: a -> IO Bool Source #

Checks satisfiability using the default solver.

Check whether a given property is satisfiable.

proveWithAll :: [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

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

proveWithAny :: [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult) Source #

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. Note that we send a ThreadKilled to the losing processes, but we do *not* actually wait for them to finish. In rare cases this can lead to zombie processes. In previous experiments, we found that some processes take their time to terminate. So, this solution favors quick turnaround.

satWithAll :: [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)] Source #

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

satWithAny :: [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult) Source #

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. Note that we send a ThreadKilled to the losing processes, but we do *not* actually wait for them to finish. In rare cases this can lead to zombie processes. In previous experiments, we found that some processes take their time to terminate. So, this solution favors quick turnaround.

Create an SMT-Lib2 benchmark. The Bool argument controls whether this is a SAT instance, i.e., translate the query directly, or a PROVE instance, i.e., translate the negated query.

Instances

 Source # MethodsforAll :: [String] -> SBool -> Predicate Source #forSome :: [String] -> SBool -> Predicate Source #satWithAll :: [SMTConfig] -> SBool -> IO [(Solver, NominalDiffTime, SatResult)] Source # Source # MethodsforAll :: [String] -> Predicate -> Predicate Source #forSome :: [String] -> Predicate -> Predicate Source # (SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source # MethodsforAll_ :: ((SBV a, SBV b) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate Source #prove :: ((SBV a, SBV b) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> ((SBV a, SBV b) -> p) -> IO String Source # (SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source # MethodsforAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate Source #prove :: ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b, SBV c) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c) -> p) -> IO String Source # (SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # MethodsforAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate Source #prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO String Source # (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # MethodsforAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate Source #prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO String Source # (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) Source # MethodsforAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate Source #prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)] Source #proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, ThmResult) Source #satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, SatResult)] Source #satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, SatResult) Source #generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO String Source # (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) Source # MethodsforAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate Source #prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult Source #proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult Source #sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult Source #satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult Source #allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult Source #allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult Source #optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult Source #optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult Source #isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool Source #proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver,