Data.SBV

(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
• SString, RegExp: Strings and regular expressions
• 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:

• ABC from University of Berkeley: http://www.eecs.berkeley.edu/~alanmi/abc/
• CVC4 from Stanford: http://cvc4.cs.stanford.edu/web/
• Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
• MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
• Yices from SRI: http://yices.csl.sri.com/
• Z3 from Microsoft: http://github.com/Z3Prover/z3/wiki

SBV requires recent versions of these solvers; please see the file SMTSolverVersions.md in the source distribution for specifics.

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.

Documentation

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 query mode: 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 at a lower level. 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

Booleans

type SBool = SBV Bool

A symbolic boolean/bit

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

Returns 1 if the boolean is true, otherwise 0.

The Boolean class

class Boolean b where

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

true, bnot, (&&&)

Methods

true :: b

logical true

false :: b

logical false

bnot :: b -> b

complement

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

and

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

or

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

nand

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

nor

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

xor

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

implies

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

equivalence

fromBool :: Bool -> b

cast from Bool

Instances

Boolean Bool

Methods

true :: Bool

false :: Bool

bnot :: Bool -> Bool

(&&&) :: Bool -> Bool -> Bool

(|||) :: Bool -> Bool -> Bool

(~&) :: Bool -> Bool -> Bool

(~|) :: Bool -> Bool -> Bool

(<+>) :: Bool -> Bool -> Bool

(==>) :: Bool -> Bool -> Bool

(<=>) :: Bool -> Bool -> Bool

fromBool :: Bool -> Bool

Boolean SBool

Methods

true :: SBool

false :: SBool

bnot :: SBool -> SBool

(&&&) :: SBool -> SBool -> SBool

(|||) :: SBool -> SBool -> SBool

(~&) :: SBool -> SBool -> SBool

(~|) :: SBool -> SBool -> SBool

(<+>) :: SBool -> SBool -> SBool

(==>) :: SBool -> SBool -> SBool

(<=>) :: SBool -> SBool -> SBool

fromBool :: Bool -> SBool

Logical operations

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

Generalization of and

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

Generalization of or

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

Generalization of any

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

Generalization of all

Bit-vectors

Unsigned bit-vectors

type SWord8 = SBV Word8

8-bit unsigned symbolic value

type SWord16 = SBV Word16

16-bit unsigned symbolic value

type SWord32 = SBV Word32

32-bit unsigned symbolic value

type SWord64 = SBV Word64

64-bit unsigned symbolic value

Signed bit-vectors

type SInt8 = SBV Int8

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

type SInt16 = SBV Int16

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

type SInt32 = SBV Int32

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

type SInt64 = SBV Int64

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

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.

type SInteger = SBV Integer

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.

type SFloat = SBV Float

IEEE-754 single-precision floating point numbers

type SDouble = SBV Double

IEEE-754 double-precision floating point numbers

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

type SReal = SBV AlgReal

Infinite precision symbolic algebraic real value

data AlgReal

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

Eq AlgReal

Methods

(==) :: AlgReal -> AlgReal -> Bool

(/=) :: AlgReal -> AlgReal -> Bool

Fractional AlgReal

NB: Following the other types we have, we require `a/0` to be `0` for all a.

Methods

(/) :: AlgReal -> AlgReal -> AlgReal

recip :: AlgReal -> AlgReal

fromRational :: Rational -> AlgReal

Num AlgReal

Methods

(+) :: AlgReal -> AlgReal -> AlgReal

(-) :: AlgReal -> AlgReal -> AlgReal

(*) :: AlgReal -> AlgReal -> AlgReal

negate :: AlgReal -> AlgReal

abs :: AlgReal -> AlgReal

signum :: AlgReal -> AlgReal

fromInteger :: Integer -> AlgReal

Ord AlgReal

Methods

compare :: AlgReal -> AlgReal -> Ordering

(<) :: AlgReal -> AlgReal -> Bool

(<=) :: AlgReal -> AlgReal -> Bool

(>) :: AlgReal -> AlgReal -> Bool

(>=) :: AlgReal -> AlgReal -> Bool

max :: AlgReal -> AlgReal -> AlgReal

min :: AlgReal -> AlgReal -> AlgReal

Real AlgReal

Methods

toRational :: AlgReal -> Rational

Show AlgReal

Methods

showsPrec :: Int -> AlgReal -> ShowS

show :: AlgReal -> String

showList :: [AlgReal] -> ShowS

Arbitrary AlgReal

Methods

arbitrary :: Gen AlgReal

shrink :: AlgReal -> [AlgReal]

Random AlgReal

Methods

randomR :: 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

randomIO :: IO AlgReal

HasKind AlgReal

Methods

kindOf :: AlgReal -> Kind

hasSign :: AlgReal -> Bool

intSizeOf :: AlgReal -> Int

isBoolean :: AlgReal -> Bool

isBounded :: AlgReal -> Bool

isReal :: AlgReal -> Bool

isFloat :: AlgReal -> Bool

isDouble :: AlgReal -> Bool

isInteger :: AlgReal -> Bool

isUninterpreted :: AlgReal -> Bool

isChar :: AlgReal -> Bool

isString :: AlgReal -> Bool

showType :: AlgReal -> String

SatModel AlgReal

AlgReal as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (AlgReal, [CW])

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

SMTValue AlgReal

Methods

sexprToVal :: SExpr -> Maybe AlgReal

Metric SReal

Methods

minimize :: String -> SReal -> Symbolic ()

maximize :: String -> SReal -> Symbolic ()

IEEEFloatConvertable AlgReal

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal

toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal

toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble

sRealToSInteger :: SReal -> SInteger

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.

Characters, Strings and Regular Expressions

Support for characters, strings, and regular expressions (intial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml and here: https://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for further related functions.

type SChar = SBV Char

A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV character for the time being. This limitation is due to the SMT-solvers only supporting this particular subset. However, there is a pending proposal to add support for unicode, and SBV will track these changes to have full unicode support as solvers become available. For details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

type SString = SBV String

A symbolic string. Note that a symbolic string is not a list of symbolic characters, that is, it is not the case that SString = [SChar], unlike what one might expect following Haskell strings. An SString is a symbolic value of its own, of possibly arbitrary length, and internally processed as one unit as opposed to a fixed-length list of characters.

(.++) :: SString -> SString -> SString infixr 5

Short cut for concat.

>>> sat $ \x y z -> length x .== 5 &&& length y .== 1 &&& x .++ y .++ z .== "Hello world!"
Satisfiable. Model:
  s0 =  "Hello" :: String
  s1 =      " " :: String
  s2 = "world!" :: String

(.!!) :: SString -> SInteger -> SChar

Short cut for strToCharAt

Arrays of symbolic values

class SymArray array where

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

newArray_, newArray, readArray, writeArray, mergeArrays

Methods

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

Create a new anonymous array

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

Create a named new array

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

Read the array element at a

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

Update the element at a to be b

mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a 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

Instances

SymArray SArray

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b)

newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b)

readArray :: SArray a b -> SBV a -> SBV b

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b

data SArray a b

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

SymArray SArray

Methods

newArray_ :: (HasKind a, HasKind b) => Symbolic (SArray a b)

newArray :: (HasKind a, HasKind b) => String -> Symbolic (SArray a b)

readArray :: SArray a b -> SBV a -> SBV b

writeArray :: SymWord b => SArray a b -> SBV a -> SBV b -> SArray a b

mergeArrays :: SymWord b => SBV Bool -> SArray a b -> SArray a b -> SArray a b

(HasKind a, HasKind b) => Show (SArray a b)

Methods

showsPrec :: 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)

Methods

forAll_ :: (SArray a b -> p) -> Predicate

forAll :: [String] -> (SArray a b -> p) -> Predicate

forSome_ :: (SArray a b -> p) -> Predicate

forSome :: [String] -> (SArray a b -> p) -> Predicate

prove :: (SArray a b -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SArray a b -> p) -> IO ThmResult

sat :: (SArray a b -> p) -> IO SatResult

satWith :: SMTConfig -> (SArray a b -> p) -> IO SatResult

allSat :: (SArray a b -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SArray a b -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult

isVacuous :: (SArray a b -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

isTheorem :: (SArray a b -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

isSatisfiable :: (SArray a b -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SArray a b -> p) -> IO String

SymWord b => Mergeable (SArray a b)

Methods

symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b

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

EqSymbolic (SArray a b)

Methods

(.==) :: SArray a b -> SArray a b -> SBool

(./=) :: SArray a b -> SArray a b -> SBool

distinct :: [SArray a b] -> SBool

allEqual :: [SArray a b] -> SBool

sElem :: SArray a b -> [SArray a b] -> SBool

data SFunArray a b

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). See mkSFunArray on how to avoid this.
• 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)

Methods

showsPrec :: 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)

Methods

forAll_ :: (SFunArray a b -> p) -> Predicate

forAll :: [String] -> (SFunArray a b -> p) -> Predicate

forSome_ :: (SFunArray a b -> p) -> Predicate

forSome :: [String] -> (SFunArray a b -> p) -> Predicate

prove :: (SFunArray a b -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SFunArray a b -> p) -> IO ThmResult

sat :: (SFunArray a b -> p) -> IO SatResult

satWith :: SMTConfig -> (SFunArray a b -> p) -> IO SatResult

allSat :: (SFunArray a b -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SFunArray a b -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult

isVacuous :: (SFunArray a b -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

isTheorem :: (SFunArray a b -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

isSatisfiable :: (SFunArray a b -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SFunArray a b -> p) -> IO String

SymWord b => Mergeable (SFunArray a b)

Methods

symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b

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

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

Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.) A simple way to create an array such that reading an unintialized value is assigned a free variable is to simply use an uninterpreted function. That is, use:

 mkSFunArray (uninterpret "initial")

Note that this will ensure all uninitialized reads to the same location will return the same value, without constraining them otherwise; with different indexes containing different values.

Creating symbolic values

Single value

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.

sBool :: String -> Symbolic SBool

Declare an SBool

sWord8 :: String -> Symbolic SWord8

Declare an SWord8

sWord16 :: String -> Symbolic SWord16

Declare an SWord16

sWord32 :: String -> Symbolic SWord32

Declare an SWord32

sWord64 :: String -> Symbolic SWord64

Declare an SWord64

sInt8 :: String -> Symbolic SInt8

Declare an SInt8

sInt16 :: String -> Symbolic SInt16

Declare an SInt16

sInt32 :: String -> Symbolic SInt32

Declare an SInt32

sInt64 :: String -> Symbolic SInt64

Declare an SInt64

sInteger :: String -> Symbolic SInteger

Declare an SInteger

sReal :: String -> Symbolic SReal

Declare an SReal

sFloat :: String -> Symbolic SFloat

Declare an SFloat

sDouble :: String -> Symbolic SDouble

Declare an SDouble

sChar :: String -> Symbolic SChar

Declare an SChar

sString :: String -> Symbolic SString

Declare an SString

List of values

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]

Declare a list of SBools

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

Declare a list of SWord8s

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

Declare a list of SWord16s

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

Declare a list of SWord32s

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

Declare a list of SWord64s

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

Declare a list of SInt8s

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

Declare a list of SInt16s

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

Declare a list of SInt32s

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

Declare a list of SInt64s

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

Declare a list of SIntegers

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

Declare a list of SReals

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

Declare a list of SFloats

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

Declare a list of SDoubles

sChars :: [String] -> Symbolic [SChar]

Declare a list of SChars

sStrings :: [String] -> Symbolic [SString]

Declare a list of SStrings

Symbolic Equality and Comparisons

class EqSymbolic a where

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

Symbolic equality.

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

Symbolic inequality.

distinct :: [a] -> SBool

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

allEqual :: [a] -> SBool

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

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

Symbolic membership test.

Instances

EqSymbolic Bool

Methods

(.==) :: Bool -> Bool -> SBool

(./=) :: Bool -> Bool -> SBool

distinct :: [Bool] -> SBool

allEqual :: [Bool] -> SBool

sElem :: Bool -> [Bool] -> SBool

EqSymbolic a => EqSymbolic [a]

Methods

(.==) :: [a] -> [a] -> SBool

(./=) :: [a] -> [a] -> SBool

distinct :: [[a]] -> SBool

allEqual :: [[a]] -> SBool

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

EqSymbolic a => EqSymbolic (Maybe a)

Methods

(.==) :: Maybe a -> Maybe a -> SBool

(./=) :: Maybe a -> Maybe a -> SBool

distinct :: [Maybe a] -> SBool

allEqual :: [Maybe a] -> SBool

sElem :: Maybe a -> [Maybe a] -> SBool

EqSymbolic (SBV a)

Methods

(.==) :: SBV a -> SBV a -> SBool

(./=) :: SBV a -> SBV a -> SBool

distinct :: [SBV a] -> SBool

allEqual :: [SBV a] -> SBool

sElem :: SBV a -> [SBV a] -> SBool

(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b)

Methods

(.==) :: Either a b -> Either a b -> SBool

(./=) :: Either a b -> Either a b -> SBool

distinct :: [Either a b] -> SBool

allEqual :: [Either a b] -> SBool

sElem :: Either a b -> [Either a b] -> SBool

(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b)

Methods

(.==) :: (a, b) -> (a, b) -> SBool

(./=) :: (a, b) -> (a, b) -> SBool

distinct :: [(a, b)] -> SBool

allEqual :: [(a, b)] -> SBool

sElem :: (a, b) -> [(a, b)] -> SBool

EqSymbolic (SArray a b)

Methods

(.==) :: SArray a b -> SArray a b -> SBool

(./=) :: SArray a b -> SArray a b -> SBool

distinct :: [SArray a b] -> SBool

allEqual :: [SArray a b] -> SBool

sElem :: SArray a b -> [SArray a b] -> SBool

(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c)

Methods

(.==) :: (a, b, c) -> (a, b, c) -> SBool

(./=) :: (a, b, c) -> (a, b, c) -> SBool

distinct :: [(a, b, c)] -> SBool

allEqual :: [(a, b, c)] -> SBool

sElem :: (a, b, c) -> [(a, b, c)] -> SBool

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d)

Methods

(.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool

(./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool

distinct :: [(a, b, c, d)] -> SBool

allEqual :: [(a, b, c, d)] -> SBool

sElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e)

Methods

(.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

(./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

distinct :: [(a, b, c, d, e)] -> SBool

allEqual :: [(a, b, c, d, e)] -> SBool

sElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f)

Methods

(.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

(./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

distinct :: [(a, b, c, d, e, f)] -> SBool

allEqual :: [(a, b, c, d, e, f)] -> SBool

sElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g)

Methods

(.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

(./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

distinct :: [(a, b, c, d, e, f, g)] -> SBool

allEqual :: [(a, b, c, d, e, f, g)] -> SBool

sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool

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

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

Symbolic less than.

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

Symbolic less than or equal to.

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

Symbolic greater than.

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

Symbolic greater than or equal to.

smin :: a -> a -> a

Symbolic minimum.

smax :: a -> a -> a

Symbolic maximum.

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

Is the value withing the allowed inclusive range?

Instances

OrdSymbolic a => OrdSymbolic [a]

Methods

(.<) :: [a] -> [a] -> SBool

(.<=) :: [a] -> [a] -> SBool

(.>) :: [a] -> [a] -> SBool

(.>=) :: [a] -> [a] -> SBool

smin :: [a] -> [a] -> [a]

smax :: [a] -> [a] -> [a]

inRange :: [a] -> ([a], [a]) -> SBool

OrdSymbolic a => OrdSymbolic (Maybe a)

Methods

(.<) :: Maybe a -> Maybe a -> SBool

(.<=) :: Maybe a -> Maybe a -> SBool

(.>) :: Maybe a -> Maybe a -> SBool

(.>=) :: Maybe a -> Maybe a -> SBool

smin :: Maybe a -> Maybe a -> Maybe a

smax :: Maybe a -> Maybe a -> Maybe a

inRange :: Maybe a -> (Maybe a, Maybe a) -> SBool

SymWord a => OrdSymbolic (SBV a)

Methods

(.<) :: SBV a -> SBV a -> SBool

(.<=) :: SBV a -> SBV a -> SBool

(.>) :: SBV a -> SBV a -> SBool

(.>=) :: SBV a -> SBV a -> SBool

smin :: SBV a -> SBV a -> SBV a

smax :: SBV a -> SBV a -> SBV a

inRange :: SBV a -> (SBV a, SBV a) -> SBool

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b)

Methods

(.<) :: Either a b -> Either a b -> SBool

(.<=) :: Either a b -> Either a b -> SBool

(.>) :: Either a b -> Either a b -> SBool

(.>=) :: Either a b -> Either a b -> SBool

smin :: Either a b -> Either a b -> Either a b

smax :: Either a b -> Either a b -> Either a b

inRange :: Either a b -> (Either a b, Either a b) -> SBool

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b)

Methods

(.<) :: (a, b) -> (a, b) -> SBool

(.<=) :: (a, b) -> (a, b) -> SBool

(.>) :: (a, b) -> (a, b) -> SBool

(.>=) :: (a, b) -> (a, b) -> SBool

smin :: (a, b) -> (a, b) -> (a, b)

smax :: (a, b) -> (a, b) -> (a, b)

inRange :: (a, b) -> ((a, b), (a, b)) -> SBool

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c)

Methods

(.<) :: (a, b, c) -> (a, b, c) -> SBool

(.<=) :: (a, b, c) -> (a, b, c) -> SBool

(.>) :: (a, b, c) -> (a, b, c) -> SBool

(.>=) :: (a, b, c) -> (a, b, c) -> SBool

smin :: (a, b, c) -> (a, b, c) -> (a, b, c)

smax :: (a, b, c) -> (a, b, c) -> (a, b, c)

inRange :: (a, b, c) -> ((a, b, c), (a, b, c)) -> SBool

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d)

Methods

(.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool

(.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool

(.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool

(.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool

smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

inRange :: (a, b, c, d) -> ((a, b, c, d), (a, b, c, d)) -> SBool

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e)

Methods

(.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

(.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

(.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

(.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool

smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

inRange :: (a, b, c, d, e) -> ((a, b, c, d, e), (a, b, c, d, e)) -> SBool

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f)

Methods

(.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

(.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

(.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

(.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool

smin :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

smax :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

inRange :: (a, b, c, d, e, f) -> ((a, b, c, d, e, f), (a, b, c, d, e, f)) -> SBool

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g)

Methods

(.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

(.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

(.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

(.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool

smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool

class Equality a where

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

Instances

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z)

Methods

(===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z)

Methods

(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z)

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z)

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

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

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

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

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

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

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z)

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

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z)

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z)

Methods

(===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult

(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z)

Methods

(===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult

(SymWord a, EqSymbolic z) => Equality (SBV a -> z)

Methods

(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult

Conditionals: Mergeable values

class Mergeable a where

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

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

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

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

Mergeable ()

Methods

symbolicMerge :: Bool -> SBool -> () -> () -> ()

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

Mergeable Mostek

Methods

symbolicMerge :: Bool -> SBool -> Mostek -> Mostek -> Mostek

select :: (SymWord b, Num b) => [Mostek] -> Mostek -> SBV b -> Mostek

Mergeable Status

Methods

symbolicMerge :: Bool -> SBool -> Status -> Status -> Status

select :: (SymWord b, Num b) => [Status] -> Status -> SBV b -> Status

Mergeable a => Mergeable [a]

Methods

symbolicMerge :: Bool -> SBool -> [a] -> [a] -> [a]

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

Mergeable a => Mergeable (Maybe a)

Methods

symbolicMerge :: Bool -> SBool -> Maybe a -> Maybe a -> Maybe a

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

SymWord a => Mergeable (SBV a)

Methods

symbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a

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

Mergeable a => Mergeable (Move a)

Mergeable instance for Move simply pushes the merging the data after run of each branch starting from the same state.

Methods

symbolicMerge :: Bool -> SBool -> Move a -> Move a -> Move a

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

Mergeable b => Mergeable (a -> b)

Methods

symbolicMerge :: Bool -> SBool -> (a -> b) -> (a -> b) -> a -> b

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

(Mergeable a, Mergeable b) => Mergeable (Either a b)

Methods

symbolicMerge :: Bool -> SBool -> Either a b -> Either a b -> Either a b

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

(Mergeable a, Mergeable b) => Mergeable (a, b)

Methods

symbolicMerge :: Bool -> SBool -> (a, b) -> (a, b) -> (a, b)

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

(Ix a, Mergeable b) => Mergeable (Array a b)

Methods

symbolicMerge :: Bool -> SBool -> Array a b -> Array a b -> Array a b

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

SymWord b => Mergeable (SFunArray a b)

Methods

symbolicMerge :: Bool -> SBool -> SFunArray a b -> SFunArray a b -> SFunArray a b

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

SymWord b => Mergeable (SArray a b)

Methods

symbolicMerge :: Bool -> SBool -> SArray a b -> SArray a b -> SArray a b

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

SymWord e => Mergeable (STree i e)

Methods

symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e

select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e

(Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c)

Methods

symbolicMerge :: Bool -> SBool -> (a, b, c) -> (a, b, c) -> (a, b, c)

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

(Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d)

Methods

symbolicMerge :: Bool -> SBool -> (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d)

select :: (SymWord b, Num b) => [(a, b, c, d)] -> (a, b, c, d) -> SBV b -> (a, b, c, d)

(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e)

Methods

symbolicMerge :: Bool -> SBool -> (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e)

select :: (SymWord b, Num b) => [(a, b, c, d, e)] -> (a, b, c, d, e) -> SBV b -> (a, b, c, d, e)

(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f)

Methods

symbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

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)

(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g)

Methods

symbolicMerge :: Bool -> SBool -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

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)

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

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

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, Integral a) => SIntegral a

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

SIntegral Int8

SIntegral Int16

SIntegral Int32

SIntegral Int64

SIntegral Integer

SIntegral Word8

SIntegral Word16

SIntegral Word32

SIntegral Word64

SIntegral Word4

SIntegral instance, using default methods

Division and Modulus

class SDivisible a where

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 both make 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

sQuotRem, sDivMod

Methods

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

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

sQuot :: a -> a -> a

sRem :: a -> a -> a

sDiv :: a -> a -> a

sMod :: a -> a -> a

Instances

SDivisible Int8

Methods

sQuotRem :: Int8 -> Int8 -> (Int8, Int8)

sDivMod :: Int8 -> Int8 -> (Int8, Int8)

sQuot :: Int8 -> Int8 -> Int8

sRem :: Int8 -> Int8 -> Int8

sDiv :: Int8 -> Int8 -> Int8

sMod :: Int8 -> Int8 -> Int8

SDivisible Int16

Methods

sQuotRem :: Int16 -> Int16 -> (Int16, Int16)

sDivMod :: Int16 -> Int16 -> (Int16, Int16)

sQuot :: Int16 -> Int16 -> Int16

sRem :: Int16 -> Int16 -> Int16

sDiv :: Int16 -> Int16 -> Int16

sMod :: Int16 -> Int16 -> Int16

SDivisible Int32

Methods

sQuotRem :: Int32 -> Int32 -> (Int32, Int32)

sDivMod :: Int32 -> Int32 -> (Int32, Int32)

sQuot :: Int32 -> Int32 -> Int32

sRem :: Int32 -> Int32 -> Int32

sDiv :: Int32 -> Int32 -> Int32

sMod :: Int32 -> Int32 -> Int32

SDivisible Int64

Methods

sQuotRem :: Int64 -> Int64 -> (Int64, Int64)

sDivMod :: Int64 -> Int64 -> (Int64, Int64)

sQuot :: Int64 -> Int64 -> Int64

sRem :: Int64 -> Int64 -> Int64

sDiv :: Int64 -> Int64 -> Int64

sMod :: Int64 -> Int64 -> Int64

SDivisible Integer

Methods

sQuotRem :: Integer -> Integer -> (Integer, Integer)

sDivMod :: Integer -> Integer -> (Integer, Integer)

sQuot :: Integer -> Integer -> Integer

sRem :: Integer -> Integer -> Integer

sDiv :: Integer -> Integer -> Integer

sMod :: Integer -> Integer -> Integer

SDivisible Word8

Methods

sQuotRem :: Word8 -> Word8 -> (Word8, Word8)

sDivMod :: Word8 -> Word8 -> (Word8, Word8)

sQuot :: Word8 -> Word8 -> Word8

sRem :: Word8 -> Word8 -> Word8

sDiv :: Word8 -> Word8 -> Word8

sMod :: Word8 -> Word8 -> Word8

SDivisible Word16

Methods

sQuotRem :: Word16 -> Word16 -> (Word16, Word16)

sDivMod :: Word16 -> Word16 -> (Word16, Word16)

sQuot :: Word16 -> Word16 -> Word16

sRem :: Word16 -> Word16 -> Word16

sDiv :: Word16 -> Word16 -> Word16

sMod :: Word16 -> Word16 -> Word16

SDivisible Word32

Methods

sQuotRem :: Word32 -> Word32 -> (Word32, Word32)

sDivMod :: Word32 -> Word32 -> (Word32, Word32)

sQuot :: Word32 -> Word32 -> Word32

sRem :: Word32 -> Word32 -> Word32

sDiv :: Word32 -> Word32 -> Word32

sMod :: Word32 -> Word32 -> Word32

SDivisible Word64

Methods

sQuotRem :: Word64 -> Word64 -> (Word64, Word64)

sDivMod :: Word64 -> Word64 -> (Word64, Word64)

sQuot :: Word64 -> Word64 -> Word64

sRem :: Word64 -> Word64 -> Word64

sDiv :: Word64 -> Word64 -> Word64

sMod :: Word64 -> Word64 -> Word64

SDivisible CW

Methods

sQuotRem :: CW -> CW -> (CW, CW)

sDivMod :: CW -> CW -> (CW, CW)

sQuot :: CW -> CW -> CW

sRem :: CW -> CW -> CW

sDiv :: CW -> CW -> CW

sMod :: CW -> CW -> CW

SDivisible SInteger

Methods

sQuotRem :: SInteger -> SInteger -> (SInteger, SInteger)

sDivMod :: SInteger -> SInteger -> (SInteger, SInteger)

sQuot :: SInteger -> SInteger -> SInteger

sRem :: SInteger -> SInteger -> SInteger

sDiv :: SInteger -> SInteger -> SInteger

sMod :: SInteger -> SInteger -> SInteger

SDivisible SInt64

Methods

sQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64)

sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64)

sQuot :: SInt64 -> SInt64 -> SInt64

sRem :: SInt64 -> SInt64 -> SInt64

sDiv :: SInt64 -> SInt64 -> SInt64

sMod :: SInt64 -> SInt64 -> SInt64

SDivisible SInt32

Methods

sQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32)

sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32)

sQuot :: SInt32 -> SInt32 -> SInt32

sRem :: SInt32 -> SInt32 -> SInt32

sDiv :: SInt32 -> SInt32 -> SInt32

sMod :: SInt32 -> SInt32 -> SInt32

SDivisible SInt16

Methods

sQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16)

sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16)

sQuot :: SInt16 -> SInt16 -> SInt16

sRem :: SInt16 -> SInt16 -> SInt16

sDiv :: SInt16 -> SInt16 -> SInt16

sMod :: SInt16 -> SInt16 -> SInt16

SDivisible SInt8

Methods

sQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8)

sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8)

sQuot :: SInt8 -> SInt8 -> SInt8

sRem :: SInt8 -> SInt8 -> SInt8

sDiv :: SInt8 -> SInt8 -> SInt8

sMod :: SInt8 -> SInt8 -> SInt8

SDivisible SWord64

Methods

sQuotRem :: SWord64 -> SWord64 -> (SWord64, SWord64)

sDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)

sQuot :: SWord64 -> SWord64 -> SWord64

sRem :: SWord64 -> SWord64 -> SWord64

sDiv :: SWord64 -> SWord64 -> SWord64

sMod :: SWord64 -> SWord64 -> SWord64

SDivisible SWord32

Methods

sQuotRem :: SWord32 -> SWord32 -> (SWord32, SWord32)

sDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)

sQuot :: SWord32 -> SWord32 -> SWord32

sRem :: SWord32 -> SWord32 -> SWord32

sDiv :: SWord32 -> SWord32 -> SWord32

sMod :: SWord32 -> SWord32 -> SWord32

SDivisible SWord16

Methods

sQuotRem :: SWord16 -> SWord16 -> (SWord16, SWord16)

sDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)

sQuot :: SWord16 -> SWord16 -> SWord16

sRem :: SWord16 -> SWord16 -> SWord16

sDiv :: SWord16 -> SWord16 -> SWord16

sMod :: SWord16 -> SWord16 -> SWord16

SDivisible SWord8

Methods

sQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8)

sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)

sQuot :: SWord8 -> SWord8 -> SWord8

sRem :: SWord8 -> SWord8 -> SWord8

sDiv :: SWord8 -> SWord8 -> SWord8

sMod :: SWord8 -> SWord8 -> SWord8

SDivisible SWord4

SDvisible instance, using default methods

Methods

sQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4)

sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4)

sQuot :: SWord4 -> SWord4 -> SWord4

sRem :: SWord4 -> SWord4 -> SWord4

sDiv :: SWord4 -> SWord4 -> SWord4

sMod :: SWord4 -> SWord4 -> SWord4

SDivisible Word4

SDvisible instance, using 0-extension

Methods

sQuotRem :: Word4 -> Word4 -> (Word4, Word4)

sDivMod :: Word4 -> Word4 -> (Word4, Word4)

sQuot :: Word4 -> Word4 -> Word4

sRem :: Word4 -> Word4 -> Word4

sDiv :: Word4 -> Word4 -> Word4

sMod :: Word4 -> Word4 -> Word4

Bit-vector operations

Conversions

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

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

Shifts and rotates

Symbolic words (both signed and unsigned) are an instance of Haskell's Bits class, so regular bitwise operations are automatically available for them. Shifts and rotates, however, require specialized type-signatures since Haskell insists on an Int second argument for them.

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

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.

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

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.

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

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

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 :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a

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.

Finite bit-vector operations

class (SymWord a, Num a, Bits a) => SFiniteBits a where

Finite bit-length symbolic values. Essentially the same as SIntegral, but further leaves out Integer. Loosely based on Haskell's FiniteBits class, but with more methods defined and structured differently to fit into the symbolic world view. Minimal complete definition: sFiniteBitSize.

Minimal complete definition

sFiniteBitSize

Methods

sFiniteBitSize :: SBV a -> Int

Bit size.

lsb :: SBV a -> SBool

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

msb :: SBV a -> SBool

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

blastBE :: SBV a -> [SBool]

Big-endian blasting of a word into its bits.

blastLE :: SBV a -> [SBool]

Little-endian blasting of a word into its bits.

fromBitsBE :: [SBool] -> SBV a

Reconstruct from given bits, given in little-endian.

fromBitsLE :: [SBool] -> SBV a

Reconstruct from given bits, given in little-endian.

sTestBit :: SBV a -> Int -> SBool

Replacement for testBit, returning SBool instead of Bool.

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

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

sPopCount :: SBV a -> SWord8

Variant of popCount, returning a symbolic value.

setBitTo :: SBV a -> Int -> SBool -> SBV a

A combo of setBit and clearBit, when the bit to be set is symbolic.

fullAdder :: SBV a -> SBV a -> (SBool, SBV a)

Full adder, returns carry-out from the addition. Only for unsigned quantities.

fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)

Full multipler, returns both high and low-order bits. Only for unsigned quantities.

sCountLeadingZeros :: SBV a -> SWord8

Count leading zeros in a word, big-endian interpretation.

sCountTrailingZeros :: SBV a -> SWord8

Count trailing zeros in a word, big-endian interpretation.

Instances

SFiniteBits Int8

Methods

sFiniteBitSize :: SBV Int8 -> Int

lsb :: SBV Int8 -> SBool

msb :: SBV Int8 -> SBool

blastBE :: SBV Int8 -> [SBool]

blastLE :: SBV Int8 -> [SBool]

fromBitsBE :: [SBool] -> SBV Int8

fromBitsLE :: [SBool] -> SBV Int8

sTestBit :: SBV Int8 -> Int -> SBool

sExtractBits :: SBV Int8 -> [Int] -> [SBool]

sPopCount :: SBV Int8 -> SWord8

setBitTo :: SBV Int8 -> Int -> SBool -> SBV Int8

fullAdder :: SBV Int8 -> SBV Int8 -> (SBool, SBV Int8)

fullMultiplier :: SBV Int8 -> SBV Int8 -> (SBV Int8, SBV Int8)

sCountLeadingZeros :: SBV Int8 -> SWord8

sCountTrailingZeros :: SBV Int8 -> SWord8

SFiniteBits Int16

Methods

sFiniteBitSize :: SBV Int16 -> Int

lsb :: SBV Int16 -> SBool

msb :: SBV Int16 -> SBool

blastBE :: SBV Int16 -> [SBool]

blastLE :: SBV Int16 -> [SBool]

fromBitsBE :: [SBool] -> SBV Int16

fromBitsLE :: [SBool] -> SBV Int16

sTestBit :: SBV Int16 -> Int -> SBool

sExtractBits :: SBV Int16 -> [Int] -> [SBool]

sPopCount :: SBV Int16 -> SWord8

setBitTo :: SBV Int16 -> Int -> SBool -> SBV Int16

fullAdder :: SBV Int16 -> SBV Int16 -> (SBool, SBV Int16)

fullMultiplier :: SBV Int16 -> SBV Int16 -> (SBV Int16, SBV Int16)

sCountLeadingZeros :: SBV Int16 -> SWord8

sCountTrailingZeros :: SBV Int16 -> SWord8

SFiniteBits Int32

Methods

sFiniteBitSize :: SBV Int32 -> Int

lsb :: SBV Int32 -> SBool

msb :: SBV Int32 -> SBool

blastBE :: SBV Int32 -> [SBool]

blastLE :: SBV Int32 -> [SBool]

fromBitsBE :: [SBool] -> SBV Int32

fromBitsLE :: [SBool] -> SBV Int32

sTestBit :: SBV Int32 -> Int -> SBool

sExtractBits :: SBV Int32 -> [Int] -> [SBool]

sPopCount :: SBV Int32 -> SWord8

setBitTo :: SBV Int32 -> Int -> SBool -> SBV Int32

fullAdder :: SBV Int32 -> SBV Int32 -> (SBool, SBV Int32)

fullMultiplier :: SBV Int32 -> SBV Int32 -> (SBV Int32, SBV Int32)

sCountLeadingZeros :: SBV Int32 -> SWord8

sCountTrailingZeros :: SBV Int32 -> SWord8

SFiniteBits Int64

Methods

sFiniteBitSize :: SBV Int64 -> Int

lsb :: SBV Int64 -> SBool

msb :: SBV Int64 -> SBool

blastBE :: SBV Int64 -> [SBool]

blastLE :: SBV Int64 -> [SBool]

fromBitsBE :: [SBool] -> SBV Int64

fromBitsLE :: [SBool] -> SBV Int64

sTestBit :: SBV Int64 -> Int -> SBool

sExtractBits :: SBV Int64 -> [Int] -> [SBool]

sPopCount :: SBV Int64 -> SWord8

setBitTo :: SBV Int64 -> Int -> SBool -> SBV Int64

fullAdder :: SBV Int64 -> SBV Int64 -> (SBool, SBV Int64)

fullMultiplier :: SBV Int64 -> SBV Int64 -> (SBV Int64, SBV Int64)

sCountLeadingZeros :: SBV Int64 -> SWord8

sCountTrailingZeros :: SBV Int64 -> SWord8

SFiniteBits Word8

Methods

sFiniteBitSize :: SBV Word8 -> Int

lsb :: SBV Word8 -> SBool

msb :: SBV Word8 -> SBool

blastBE :: SBV Word8 -> [SBool]

blastLE :: SBV Word8 -> [SBool]

fromBitsBE :: [SBool] -> SBV Word8

fromBitsLE :: [SBool] -> SBV Word8

sTestBit :: SBV Word8 -> Int -> SBool

sExtractBits :: SBV Word8 -> [Int] -> [SBool]

sPopCount :: SBV Word8 -> SWord8

setBitTo :: SBV Word8 -> Int -> SBool -> SBV Word8

fullAdder :: SBV Word8 -> SBV Word8 -> (SBool, SBV Word8)

fullMultiplier :: SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)

sCountLeadingZeros :: SBV Word8 -> SWord8

sCountTrailingZeros :: SBV Word8 -> SWord8

SFiniteBits Word16

Methods

sFiniteBitSize :: SBV Word16 -> Int

lsb :: SBV Word16 -> SBool

msb :: SBV Word16 -> SBool

blastBE :: SBV Word16 -> [SBool]

blastLE :: SBV Word16 -> [SBool]

fromBitsBE :: [SBool] -> SBV Word16

fromBitsLE :: [SBool] -> SBV Word16

sTestBit :: SBV Word16 -> Int -> SBool

sExtractBits :: SBV Word16 -> [Int] -> [SBool]

sPopCount :: SBV Word16 -> SWord8

setBitTo :: SBV Word16 -> Int -> SBool -> SBV Word16

fullAdder :: SBV Word16 -> SBV Word16 -> (SBool, SBV Word16)

fullMultiplier :: SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)

sCountLeadingZeros :: SBV Word16 -> SWord8

sCountTrailingZeros :: SBV Word16 -> SWord8

SFiniteBits Word32

Methods

sFiniteBitSize :: SBV Word32 -> Int

lsb :: SBV Word32 -> SBool

msb :: SBV Word32 -> SBool

blastBE :: SBV Word32 -> [SBool]

blastLE :: SBV Word32 -> [SBool]

fromBitsBE :: [SBool] -> SBV Word32

fromBitsLE :: [SBool] -> SBV Word32

sTestBit :: SBV Word32 -> Int -> SBool

sExtractBits :: SBV Word32 -> [Int] -> [SBool]

sPopCount :: SBV Word32 -> SWord8

setBitTo :: SBV Word32 -> Int -> SBool -> SBV Word32

fullAdder :: SBV Word32 -> SBV Word32 -> (SBool, SBV Word32)

fullMultiplier :: SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)

sCountLeadingZeros :: SBV Word32 -> SWord8

sCountTrailingZeros :: SBV Word32 -> SWord8

SFiniteBits Word64

Methods

sFiniteBitSize :: SBV Word64 -> Int

lsb :: SBV Word64 -> SBool

msb :: SBV Word64 -> SBool

blastBE :: SBV Word64 -> [SBool]

blastLE :: SBV Word64 -> [SBool]

fromBitsBE :: [SBool] -> SBV Word64

fromBitsLE :: [SBool] -> SBV Word64

sTestBit :: SBV Word64 -> Int -> SBool

sExtractBits :: SBV Word64 -> [Int] -> [SBool]

sPopCount :: SBV Word64 -> SWord8

setBitTo :: SBV Word64 -> Int -> SBool -> SBV Word64

fullAdder :: SBV Word64 -> SBV Word64 -> (SBool, SBV Word64)

fullMultiplier :: SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)

sCountLeadingZeros :: SBV Word64 -> SWord8

sCountTrailingZeros :: SBV Word64 -> SWord8

Splitting, joining, and extending

class Splittable a b | b -> a where

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

split, (#), extend

Methods

split :: a -> (b, b)

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

extend :: b -> a

Instances

Splittable Word8 Word4

Joiningsplitting tofrom Word8

Methods

split :: Word8 -> (Word4, Word4)

(#) :: Word4 -> Word4 -> Word8

extend :: Word4 -> Word8

Splittable Word16 Word8

Methods

split :: Word16 -> (Word8, Word8)

(#) :: Word8 -> Word8 -> Word16

extend :: Word8 -> Word16

Splittable Word32 Word16

Methods

split :: Word32 -> (Word16, Word16)

(#) :: Word16 -> Word16 -> Word32

extend :: Word16 -> Word32

Splittable Word64 Word32

Methods

split :: Word64 -> (Word32, Word32)

(#) :: Word32 -> Word32 -> Word64

extend :: Word32 -> Word64

Splittable SWord64 SWord32

Methods

split :: SWord64 -> (SWord32, SWord32)

(#) :: SWord32 -> SWord32 -> SWord64

extend :: SWord32 -> SWord64

Splittable SWord32 SWord16

Methods

split :: SWord32 -> (SWord16, SWord16)

(#) :: SWord16 -> SWord16 -> SWord32

extend :: SWord16 -> SWord32

Splittable SWord16 SWord8

Methods

split :: SWord16 -> (SWord8, SWord8)

(#) :: SWord8 -> SWord8 -> SWord16

extend :: SWord8 -> SWord16

Exponentiation

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

Symbolic exponentiation using bit blasting and repeated squaring.

N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.

IEEE-floating point numbers

class (SymWord a, RealFloat a) => IEEEFloating a where

A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.

Methods

fpAbs :: SBV a -> SBV a

Compute the floating point absolute value.

fpNeg :: SBV a -> SBV a

Compute the unary negation. Note that 0 - x is not equivalent to -x for floating-point, since -0 and 0 are different.

fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a

Add two floating point values, using the given rounding mode

fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a

Subtract two floating point values, using the given rounding mode

fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a

Multiply two floating point values, using the given rounding mode

fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a

Divide two floating point values, using the given rounding mode

fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a

Fused-multiply-add three floating point values, using the given rounding mode. fpFMA x y z = x*y+z but with only one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since Haskell lacks an FMA implementation.

fpSqrt :: SRoundingMode -> SBV a -> SBV a

Compute the square-root of a float, using the given rounding mode

fpRem :: SBV a -> SBV a -> SBV a

Compute the remainder: x - y * n, where n is the truncated integer nearest to x/y. The rounding mode is implicitly assumed to be RoundNearestTiesToEven.

fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a

Round to the nearest integral value, using the given rounding mode.

fpMin :: SBV a -> SBV a -> SBV a

Compute the minimum of two floats, respects infinity and NaN values

fpMax :: SBV a -> SBV a -> SBV a

Compute the maximum of two floats, respects infinity and NaN values

fpIsEqualObject :: SBV a -> SBV a -> SBool

Are the two given floats exactly the same. That is, NaN will compare equal to itself, +0 will not compare equal to -0 etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==.)

fpIsNormal :: SBV a -> SBool

Is the floating-point number a normal value. (i.e., not denormalized.)

fpIsSubnormal :: SBV a -> SBool

Is the floating-point number a subnormal value. (Also known as denormal.)

fpIsZero :: SBV a -> SBool

Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)

fpIsInfinite :: SBV a -> SBool

Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)

fpIsNaN :: SBV a -> SBool

Is the floating-point number a NaN value?

fpIsNegative :: SBV a -> SBool

Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.

fpIsPositive :: SBV a -> SBool

Is the floating-point number positive? Note that +0 satisfies this predicate but -0 does not.

fpIsNegativeZero :: SBV a -> SBool

Is the floating point number -0?

fpIsPositiveZero :: SBV a -> SBool

Is the floating point number +0?

fpIsPoint :: SBV a -> SBool

Is the floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.

Instances

IEEEFloating Double

SDouble instance

Methods

fpAbs :: SBV Double -> SBV Double

fpNeg :: SBV Double -> SBV Double

fpAdd :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double

fpSub :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double

fpMul :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double

fpDiv :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double

fpFMA :: SRoundingMode -> SBV Double -> SBV Double -> SBV Double -> SBV Double

fpSqrt :: SRoundingMode -> SBV Double -> SBV Double

fpRem :: SBV Double -> SBV Double -> SBV Double

fpRoundToIntegral :: SRoundingMode -> SBV Double -> SBV Double

fpMin :: SBV Double -> SBV Double -> SBV Double

fpMax :: SBV Double -> SBV Double -> SBV Double

fpIsEqualObject :: SBV Double -> SBV Double -> SBool

fpIsNormal :: SBV Double -> SBool

fpIsSubnormal :: SBV Double -> SBool

fpIsZero :: SBV Double -> SBool

fpIsInfinite :: SBV Double -> SBool

fpIsNaN :: SBV Double -> SBool

fpIsNegative :: SBV Double -> SBool

fpIsPositive :: SBV Double -> SBool

fpIsNegativeZero :: SBV Double -> SBool

fpIsPositiveZero :: SBV Double -> SBool

fpIsPoint :: SBV Double -> SBool

IEEEFloating Float

SFloat instance

Methods

fpAbs :: SBV Float -> SBV Float

fpNeg :: SBV Float -> SBV Float

fpAdd :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float

fpSub :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float

fpMul :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float

fpDiv :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float

fpFMA :: SRoundingMode -> SBV Float -> SBV Float -> SBV Float -> SBV Float

fpSqrt :: SRoundingMode -> SBV Float -> SBV Float

fpRem :: SBV Float -> SBV Float -> SBV Float

fpRoundToIntegral :: SRoundingMode -> SBV Float -> SBV Float

fpMin :: SBV Float -> SBV Float -> SBV Float

fpMax :: SBV Float -> SBV Float -> SBV Float

fpIsEqualObject :: SBV Float -> SBV Float -> SBool

fpIsNormal :: SBV Float -> SBool

fpIsSubnormal :: SBV Float -> SBool

fpIsZero :: SBV Float -> SBool

fpIsInfinite :: SBV Float -> SBool

fpIsNaN :: SBV Float -> SBool

fpIsNegative :: SBV Float -> SBool

fpIsPositive :: SBV Float -> SBool

fpIsNegativeZero :: SBV Float -> SBool

fpIsPositiveZero :: SBV Float -> SBool

fpIsPoint :: SBV Float -> SBool

data RoundingMode

Rounding mode to be used for the IEEE floating-point operations. Note that Haskell's default is RoundNearestTiesToEven. If you use a different rounding mode, then the counter-examples you get may not match what you observe in Haskell.

Constructors

RoundNearestTiesToEven

Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.)

RoundNearestTiesToAway

Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.)

RoundTowardPositive

Round towards positive infinity. (Also known as rounding-up or ceiling.)

RoundTowardNegative

Round towards negative infinity. (Also known as rounding-down or floor.)

RoundTowardZero

Round towards zero. (Also known as truncation.)

Instances

Bounded RoundingMode

Methods

minBound :: RoundingMode

maxBound :: RoundingMode

Enum RoundingMode

Methods

succ :: RoundingMode -> RoundingMode

pred :: RoundingMode -> RoundingMode

toEnum :: Int -> RoundingMode

fromEnum :: RoundingMode -> Int

enumFrom :: RoundingMode -> [RoundingMode]

enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]

enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]

enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]

Eq RoundingMode

Methods

(==) :: RoundingMode -> RoundingMode -> Bool

(/=) :: RoundingMode -> RoundingMode -> Bool

Data RoundingMode

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c RoundingMode

toConstr :: RoundingMode -> Constr

dataTypeOf :: RoundingMode -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RoundingMode)

gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r

gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode

Ord RoundingMode

Methods

compare :: RoundingMode -> RoundingMode -> Ordering

(<) :: RoundingMode -> RoundingMode -> Bool

(<=) :: RoundingMode -> RoundingMode -> Bool

(>) :: RoundingMode -> RoundingMode -> Bool

(>=) :: RoundingMode -> RoundingMode -> Bool

max :: RoundingMode -> RoundingMode -> RoundingMode

min :: RoundingMode -> RoundingMode -> RoundingMode

Read RoundingMode

Methods

readsPrec :: Int -> ReadS RoundingMode

readList :: ReadS [RoundingMode]

readPrec :: ReadPrec RoundingMode

readListPrec :: ReadPrec [RoundingMode]

Show RoundingMode

Methods

showsPrec :: Int -> RoundingMode -> ShowS

show :: RoundingMode -> String

showList :: [RoundingMode] -> ShowS

HasKind RoundingMode

RoundingMode kind

Methods

kindOf :: RoundingMode -> Kind

hasSign :: RoundingMode -> Bool

intSizeOf :: RoundingMode -> Int

isBoolean :: RoundingMode -> Bool

isBounded :: RoundingMode -> Bool

isReal :: RoundingMode -> Bool

isFloat :: RoundingMode -> Bool

isDouble :: RoundingMode -> Bool

isInteger :: RoundingMode -> Bool

isUninterpreted :: RoundingMode -> Bool

isChar :: RoundingMode -> Bool

isString :: RoundingMode -> Bool

showType :: RoundingMode -> String

SymWord RoundingMode

RoundingMode can be used symbolically

Methods

forall :: String -> Symbolic (SBV RoundingMode)

forall_ :: Symbolic (SBV RoundingMode)

mkForallVars :: Int -> Symbolic [SBV RoundingMode]

exists :: String -> Symbolic (SBV RoundingMode)

exists_ :: Symbolic (SBV RoundingMode)

mkExistVars :: Int -> Symbolic [SBV RoundingMode]

free :: String -> Symbolic (SBV RoundingMode)

free_ :: Symbolic (SBV RoundingMode)

mkFreeVars :: Int -> Symbolic [SBV RoundingMode]

symbolic :: String -> Symbolic (SBV RoundingMode)

symbolics :: [String] -> Symbolic [SBV RoundingMode]

literal :: RoundingMode -> SBV RoundingMode

unliteral :: SBV RoundingMode -> Maybe RoundingMode

fromCW :: CW -> RoundingMode

isConcrete :: SBV RoundingMode -> Bool

isSymbolic :: SBV RoundingMode -> Bool

isConcretely :: SBV RoundingMode -> (RoundingMode -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV RoundingMode)

SatModel RoundingMode

A rounding mode, extracted from a model. (Default definition suffices)

Methods

parseCWs :: [CW] -> Maybe (RoundingMode, [CW])

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

type SRoundingMode = SBV RoundingMode

The symbolic variant of RoundingMode

nan :: Floating a => a

Not-A-Number for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

infinity :: Floating a => a

Infinity for Double and Float. Surprisingly, Haskell Prelude doesn't have this value defined, so we provide it here.

sNaN :: (Floating a, SymWord a) => SBV a

Symbolic variant of Not-A-Number. This value will inhabit both SDouble and SFloat.

sInfinity :: (Floating a, SymWord a) => SBV a

Symbolic variant of infinity. This value will inhabit both SDouble and SFloat.

Rounding modes

sRoundNearestTiesToEven :: SRoundingMode

Symbolic variant of RoundNearestTiesToEven

sRoundNearestTiesToAway :: SRoundingMode

Symbolic variant of RoundNearestTiesToAway

sRoundTowardPositive :: SRoundingMode

Symbolic variant of RoundNearestPositive

sRoundTowardNegative :: SRoundingMode

Symbolic variant of RoundTowardNegative

sRoundTowardZero :: SRoundingMode

Symbolic variant of RoundTowardZero

sRNE :: SRoundingMode

Alias for sRoundNearestTiesToEven

sRNA :: SRoundingMode

Alias for sRoundNearestTiesToAway

sRTP :: SRoundingMode

Alias for sRoundTowardPositive

sRTN :: SRoundingMode

Alias for sRoundTowardNegative

sRTZ :: SRoundingMode

Alias for sRoundTowardZero

Conversion to/from floats

class IEEEFloatConvertable a where

Capture convertability from/to FloatingPoint representations NB. fromSFloat and fromSDouble are underspecified when given when given a NaN, +oo, or -oo value that cannot be represented in the target domain. For these inputs, we define the result to be +0, arbitrarily.

Minimal complete definition

fromSFloat, toSFloat, fromSDouble, toSDouble

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV a

toSFloat :: SRoundingMode -> SBV a -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV a

toSDouble :: SRoundingMode -> SBV a -> SDouble

Instances

IEEEFloatConvertable Double

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Double

toSFloat :: SRoundingMode -> SBV Double -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Double

toSDouble :: SRoundingMode -> SBV Double -> SDouble

IEEEFloatConvertable Float

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Float

toSFloat :: SRoundingMode -> SBV Float -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Float

toSDouble :: SRoundingMode -> SBV Float -> SDouble

IEEEFloatConvertable Int8

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Int8

toSFloat :: SRoundingMode -> SBV Int8 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Int8

toSDouble :: SRoundingMode -> SBV Int8 -> SDouble

IEEEFloatConvertable Int16

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Int16

toSFloat :: SRoundingMode -> SBV Int16 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Int16

toSDouble :: SRoundingMode -> SBV Int16 -> SDouble

IEEEFloatConvertable Int32

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Int32

toSFloat :: SRoundingMode -> SBV Int32 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Int32

toSDouble :: SRoundingMode -> SBV Int32 -> SDouble

IEEEFloatConvertable Int64

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Int64

toSFloat :: SRoundingMode -> SBV Int64 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Int64

toSDouble :: SRoundingMode -> SBV Int64 -> SDouble

IEEEFloatConvertable Integer

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Integer

toSFloat :: SRoundingMode -> SBV Integer -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Integer

toSDouble :: SRoundingMode -> SBV Integer -> SDouble

IEEEFloatConvertable Word8

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Word8

toSFloat :: SRoundingMode -> SBV Word8 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Word8

toSDouble :: SRoundingMode -> SBV Word8 -> SDouble

IEEEFloatConvertable Word16

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Word16

toSFloat :: SRoundingMode -> SBV Word16 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Word16

toSDouble :: SRoundingMode -> SBV Word16 -> SDouble

IEEEFloatConvertable Word32

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Word32

toSFloat :: SRoundingMode -> SBV Word32 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Word32

toSDouble :: SRoundingMode -> SBV Word32 -> SDouble

IEEEFloatConvertable Word64

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV Word64

toSFloat :: SRoundingMode -> SBV Word64 -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV Word64

toSDouble :: SRoundingMode -> SBV Word64 -> SDouble

IEEEFloatConvertable AlgReal

Methods

fromSFloat :: SRoundingMode -> SFloat -> SBV AlgReal

toSFloat :: SRoundingMode -> SBV AlgReal -> SFloat

fromSDouble :: SRoundingMode -> SDouble -> SBV AlgReal

toSDouble :: SRoundingMode -> SBV AlgReal -> SDouble

Bit-pattern conversions

sFloatAsSWord32 :: SFloat -> SWord32

Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the representation for NaNs are not unique, this function will return a symbolic value when given a concrete NaN.

Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.

sWord32AsSFloat :: SWord32 -> SFloat

Reinterpret the bits in a 32-bit word as a single-precision floating point number

sDoubleAsSWord64 :: SDouble -> SWord64

Convert an SDouble to an SWord64, preserving the bit-correspondence. Note that since the representation for NaNs are not unique, this function will return a symbolic value when given a concrete NaN.

See the implementation note for sFloatAsSWord32, as it applies here as well.

sWord64AsSDouble :: SWord64 -> SDouble

Reinterpret the bits in a 32-bit word as a single-precision floating point number

blastSFloat :: SFloat -> (SBool, [SBool], [SBool])

Extract the sign/exponent/mantissa of a single-precision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.

blastSDouble :: SDouble -> (SBool, [SBool], [SBool])

Extract the sign/exponent/mantissa of a single-precision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.

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 Documentation.SBV.Examples.Misc.Enumerate for an extended example on how to use symbolic enumerations.

mkSymbolicEnumeration :: Name -> Q [Dec]

Make an enumeration a symbolic type.

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

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

Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.

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

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

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

Instances

HasKind a => Uninterpreted (SBV a)

Methods

uninterpret :: String -> SBV a

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

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

(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a)

Methods

uninterpret :: String -> (SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a)

Methods

uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a)

Methods

uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a

(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a)

Methods

uninterpret :: String -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a

(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a)

Methods

uninterpret :: String -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a

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

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

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

Properties, proofs, and satisfiability

The SBV library provides a "push-button" verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://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.

Using multiple solvers

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.

SBV allows 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.

type Predicate = Symbolic SBool

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

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

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

forAll_, forAll, forSome_, forSome

Methods

forAll_ :: a -> Predicate

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

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

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

Version of forSome that allows user defined names.

prove :: a -> IO ThmResult

Prove a predicate, using the default solver.

proveWith :: SMTConfig -> a -> IO ThmResult

Prove the predicate using the given SMT-solver.

sat :: a -> IO SatResult

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

satWith :: SMTConfig -> a -> IO SatResult

Find a satisfying assignment using the given SMT-solver.

allSat :: a -> IO AllSatResult

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

allSatWith :: SMTConfig -> a -> IO AllSatResult

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 :: OptimizeStyle -> a -> IO OptimizeResult

Optimize a given collection of Objectives

optimizeWith :: SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult

Optimizes the objectives using the given SMT-solver.

isVacuous :: a -> IO Bool

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

isVacuousWith :: SMTConfig -> a -> IO Bool

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

isTheorem :: a -> IO Bool

Checks theoremhood using the default solver.

isTheoremWith :: SMTConfig -> a -> IO Bool

Check whether a given property is a theorem.

isSatisfiable :: a -> IO Bool

Checks satisfiability using the default solver.

isSatisfiableWith :: SMTConfig -> a -> IO Bool

Check whether a given property is satisfiable.

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

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)

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

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)

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.

generateSMTBenchmark :: Bool -> a -> IO String

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

Provable SBool

Methods

forAll_ :: SBool -> Predicate

forAll :: [String] -> SBool -> Predicate

forSome_ :: SBool -> Predicate

forSome :: [String] -> SBool -> Predicate

prove :: SBool -> IO ThmResult

proveWith :: SMTConfig -> SBool -> IO ThmResult

sat :: SBool -> IO SatResult

satWith :: SMTConfig -> SBool -> IO SatResult

allSat :: SBool -> IO AllSatResult

allSatWith :: SMTConfig -> SBool -> IO AllSatResult

optimize :: OptimizeStyle -> SBool -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> SBool -> IO OptimizeResult

isVacuous :: SBool -> IO Bool

isVacuousWith :: SMTConfig -> SBool -> IO Bool

isTheorem :: SBool -> IO Bool

isTheoremWith :: SMTConfig -> SBool -> IO Bool

isSatisfiable :: SBool -> IO Bool

isSatisfiableWith :: SMTConfig -> SBool -> IO Bool

proveWithAll :: [SMTConfig] -> SBool -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> SBool -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> SBool -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> SBool -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> SBool -> IO String

Provable Predicate

Methods

forAll_ :: Predicate -> Predicate

forAll :: [String] -> Predicate -> Predicate

forSome_ :: Predicate -> Predicate

forSome :: [String] -> Predicate -> Predicate

prove :: Predicate -> IO ThmResult

proveWith :: SMTConfig -> Predicate -> IO ThmResult

sat :: Predicate -> IO SatResult

satWith :: SMTConfig -> Predicate -> IO SatResult

allSat :: Predicate -> IO AllSatResult

allSatWith :: SMTConfig -> Predicate -> IO AllSatResult

optimize :: OptimizeStyle -> Predicate -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> Predicate -> IO OptimizeResult

isVacuous :: Predicate -> IO Bool

isVacuousWith :: SMTConfig -> Predicate -> IO Bool

isTheorem :: Predicate -> IO Bool

isTheoremWith :: SMTConfig -> Predicate -> IO Bool

isSatisfiable :: Predicate -> IO Bool

isSatisfiableWith :: SMTConfig -> Predicate -> IO Bool

proveWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> Predicate -> IO String

(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p)

Methods

forAll_ :: ((SBV a, SBV b) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate

prove :: ((SBV a, SBV b) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO String

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

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO String

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

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO String

(HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p)

Methods

forAll_ :: (SFunArray a b -> p) -> Predicate

forAll :: [String] -> (SFunArray a b -> p) -> Predicate

forSome_ :: (SFunArray a b -> p) -> Predicate

forSome :: [String] -> (SFunArray a b -> p) -> Predicate

prove :: (SFunArray a b -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SFunArray a b -> p) -> IO ThmResult

sat :: (SFunArray a b -> p) -> IO SatResult

satWith :: SMTConfig -> (SFunArray a b -> p) -> IO SatResult

allSat :: (SFunArray a b -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SFunArray a b -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SFunArray a b -> p) -> IO OptimizeResult

isVacuous :: (SFunArray a b -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

isTheorem :: (SFunArray a b -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

isSatisfiable :: (SFunArray a b -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SFunArray a b -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SFunArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SFunArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SFunArray a b -> p) -> IO String

(HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p)

Methods

forAll_ :: (SArray a b -> p) -> Predicate

forAll :: [String] -> (SArray a b -> p) -> Predicate

forSome_ :: (SArray a b -> p) -> Predicate

forSome :: [String] -> (SArray a b -> p) -> Predicate

prove :: (SArray a b -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SArray a b -> p) -> IO ThmResult

sat :: (SArray a b -> p) -> IO SatResult

satWith :: SMTConfig -> (SArray a b -> p) -> IO SatResult

allSat :: (SArray a b -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SArray a b -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SArray a b -> p) -> IO OptimizeResult

isVacuous :: (SArray a b -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

isTheorem :: (SArray a b -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

isSatisfiable :: (SArray a b -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SArray a b -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SArray a b -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SArray a b -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SArray a b -> p) -> IO String

(SymWord a, Provable p) => Provable (SBV a -> p)

Methods

forAll_ :: (SBV a -> p) -> Predicate

forAll :: [String] -> (SBV a -> p) -> Predicate

forSome_ :: (SBV a -> p) -> Predicate

forSome :: [String] -> (SBV a -> p) -> Predicate

prove :: (SBV a -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SBV a -> p) -> IO ThmResult

sat :: (SBV a -> p) -> IO SatResult

satWith :: SMTConfig -> (SBV a -> p) -> IO SatResult

allSat :: (SBV a -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SBV a -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult

isVacuous :: (SBV a -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SBV a -> p) -> IO Bool

isTheorem :: (SBV a -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SBV a -> p) -> IO Bool

isSatisfiable :: (SBV a -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SBV a -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SBV a -> p) -> IO String

solve :: [SBool] -> Symbolic SBool

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

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

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

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

Add a constraint, any satisfying instance must satisfy this condition

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

Named constraints

Constraints can be given names:

 namedConstraint "a is at least 5" $ a .>= 5

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

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

Unsat cores

Named 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 option:

 setOption $ ProduceUnsatCores True

See Documentation.SBV.Examples.Misc.UnsatCore for an example use case.

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

true if at most k of the input arguments are true

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

true if at least k of the input arguments are true

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

true if exactly k of the input arguments are true

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

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

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

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

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

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

true if there is at most one set bit

pbStronglyMutexed :: [SBool] -> SBool

true if there is exactly one set bit

Checking safety

The sAssert function allows users to introduce invariants to make sure certain properties hold at all times. This is another mechanism to provide further documentation/contract info into SBV code. The functions safe and safeWith can be used to statically discharge these proof assumptions. If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.

Here's a simple example. Let's assume we have a function that does subtraction, and requires its first argument to be larger than the second:

>>> let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y)

Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument. We can use safe to statically see if such a violation is possible before we use this function elsewhere.

>>> safe (sub :: SInt8 -> SInt8 -> SInt8)
[sub: x >= y must hold!: Violated. Model:
  s0 = 30 :: Int8
  s1 = 32 :: Int8]

What happens if we make sure to arrange for this invariant? Consider this version:

>>> let safeSub x y = ite (x .>= y) (sub x y) 0

Clearly, safeSub must be safe. And indeed, SBV can prove that:

>>> safe (safeSub :: SInt8 -> SInt8 -> SInt8)
[sub: x >= y must hold!: No violations detected]

Note how we used sub and safeSub polymorphically. We only need to monomorphise our types when a proof attempt is done, as we did in the safe calls.

If required, the user can pass a CallStack through the first argument to sAssert, which will be used by SBV to print a diagnostic info to pinpoint the failure.

Also see Documentation.SBV.Examples.Misc.NoDiv0 for the classic div-by-zero example.

sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a

Symbolic assert. Check that the given boolean condition is always true in the given path. The optional first argument can be used to provide call-stack info via GHC's location facilities.

isSafe :: SafeResult -> Bool

Check if a safe-call was safe or not, turning a SafeResult to a Bool.

class SExecutable a where

Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.

Minimal complete definition

sName_, sName

Methods

sName_ :: a -> Symbolic ()

sName :: [String] -> a -> Symbolic ()

safe :: a -> IO [SafeResult]

Check safety using the default solver.

safeWith :: SMTConfig -> a -> IO [SafeResult]

Check if any of the sAssert calls can be violated.

Instances

SExecutable ()

Methods

sName_ :: () -> Symbolic ()

sName :: [String] -> () -> Symbolic ()

safe :: () -> IO [SafeResult]

safeWith :: SMTConfig -> () -> IO [SafeResult]

SExecutable [SBV a]

Methods

sName_ :: [SBV a] -> Symbolic ()

sName :: [String] -> [SBV a] -> Symbolic ()

safe :: [SBV a] -> IO [SafeResult]

safeWith :: SMTConfig -> [SBV a] -> IO [SafeResult]

NFData a => SExecutable (Symbolic a)

Methods

sName_ :: Symbolic a -> Symbolic ()

sName :: [String] -> Symbolic a -> Symbolic ()

safe :: Symbolic a -> IO [SafeResult]

safeWith :: SMTConfig -> Symbolic a -> IO [SafeResult]

SExecutable (SBV a)

Methods

sName_ :: SBV a -> Symbolic ()

sName :: [String] -> SBV a -> Symbolic ()

safe :: SBV a -> IO [SafeResult]

safeWith :: SMTConfig -> SBV a -> IO [SafeResult]

(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p)

Methods

sName_ :: ((SBV a, SBV b) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult]

(SymWord a, SExecutable p) => SExecutable (SBV a -> p)

Methods

sName_ :: (SBV a -> p) -> Symbolic ()

sName :: [String] -> (SBV a -> p) -> Symbolic ()

safe :: (SBV a -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a -> p) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b)

Methods

sName_ :: (SBV a, SBV b) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b) -> Symbolic ()

safe :: (SBV a, SBV b) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c)

Methods

sName_ :: (SBV a, SBV b, SBV c) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult]

Quick-checking

sbvQuickCheck :: Symbolic SBool -> IO Bool

Quick check an SBV property. Note that a regular quickCheck call will work just as well. Use this variant if you want to receive the boolean result.

Optimization

SBV can optimize metric functions, i.e., those that generate both bounded SIntN, SWordN, and unbounded SInteger types, along with those produce SReals. That is, it can find models satisfying all the constraints while minimizing or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend, and a good review of these features is given in this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.

Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are:

• minimize: Minimize a given arithmetic goal
• maximize: Minimize a given arithmetic goal

Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals).

For instance, a call of the form

 minimize "name-of-goal" $ x + 2*y

minimizes the arithmetic goal x+2*y, where x and y can be signed/unsigned bit-vectors, reals, or integers.

A simple example

Here's an optimization example in action:

>>> optimize Lexicographic $ \x y -> minimize "goal" (x+2*(y::SInteger))
Optimal in an extension field:
  goal = -oo :: Integer

We will describe the role of the constructor Lexicographic shortly.

Of course, this becomes more useful when the result is not in an extension field:

>>> :{
    optimize Lexicographic $ do
                  x <- sInteger "x"
                  y <- sInteger "y"
                  constrain $ x .> 0
                  constrain $ x .< 6
                  constrain $ y .> 2
                  constrain $ y .< 12
                  minimize "goal" $ x + 2 * y
    :}
Optimal model:
  x    = 1 :: Integer
  y    = 3 :: Integer
  goal = 7 :: Integer

As usual, the programmatic API can be used to extract the values of objectives and model-values (getModelObjectives, getModelAssignment, etc.) to access these values and program with them further.

The following examples illustrate the use of basic optimization routines:

• Documentation.SBV.Examples.Optimization.LinearOpt: Simple linear-optimization example.
• Documentation.SBV.Examples.Optimization.Production: Scheduling machines in a shop
• Documentation.SBV.Examples.Optimization.VM: Scheduling virtual-machines in a data-center

Multiple optimization goals

Multiple goals can be specified, using the same syntax. In this case, the user gets to pick what style of optimization to perform, by passing the relevant OptimizeStyle as the first argument to optimize.

• [Lexicographic]. The solver will optimize the goals in the given order, optimizing the latter ones under the model that optimizes the previous ones.
• [Independent]. The solver will optimize the goals independently of each other. In this case the user will be presented a model for each goal given.
• [Pareto]. Finally, the user can query for pareto-fronts. A pareto front is an model such that no goal can be made "better" without making some other goal "worse."

The optional number argument to Pareto specifies the maximum number of pareto-fronts the user is asking to get. If Nothing, SBV will query for all pareto-fronts. Note that pareto-fronts can be infinite in number, so if Nothing is used, there is a potential for infinitely waiting for the SBV-solver interaction to finish. (If you suspect this might be the case, run in verbose mode to see the interaction and put a limiting factor appropriately.)

data OptimizeStyle

Style of optimization. Note that in the pareto case the user is allowed to specify a max number of fronts to query the solver for, since there might potentially be an infinite number of them and there is no way to know exactly how many ahead of time. If Nothing is given, SBV will possibly loop forever if the number is really infinite.

Constructors

Lexicographic

Objectives are optimized in the order given, earlier objectives have higher priority. This is the default.

Independent

Each objective is optimized independently.

Pareto (Maybe Int)

Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.

Instances

Eq OptimizeStyle

Methods

(==) :: OptimizeStyle -> OptimizeStyle -> Bool

(/=) :: OptimizeStyle -> OptimizeStyle -> Bool

Show OptimizeStyle

Methods

showsPrec :: Int -> OptimizeStyle -> ShowS

show :: OptimizeStyle -> String

showList :: [OptimizeStyle] -> ShowS

NFData OptimizeStyle

Methods

rnf :: OptimizeStyle -> ()

Objectives

data Objective a

Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.

Constructors

Minimize String a

Minimize this metric

Maximize String a

Maximize this metric

AssertSoft String a Penalty

A soft assertion, with an associated penalty

Instances

Functor Objective

Methods

fmap :: (a -> b) -> Objective a -> Objective b

(<$) :: a -> Objective b -> Objective a

Show a => Show (Objective a)

Methods

showsPrec :: Int -> Objective a -> ShowS

show :: Objective a -> String

showList :: [Objective a] -> ShowS

NFData a => NFData (Objective a)

Methods

rnf :: Objective a -> ()

class Metric a where

Class of metrics we can optimize for. Currently, bounded signed/unsigned bit-vectors, unbounded integers, and algebraic reals can be optimized. (But not, say, SFloat, SDouble, or SBool.) Minimal complete definition: minimize/maximize.

A good reference on these features is given in the following paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.

Minimal complete definition

minimize, maximize

Methods

minimize :: String -> a -> Symbolic ()

Minimize a named metric

maximize :: String -> a -> Symbolic ()

Maximize a named metric

Instances

Metric SReal

Methods

minimize :: String -> SReal -> Symbolic ()

maximize :: String -> SReal -> Symbolic ()

Metric SInteger

Methods

minimize :: String -> SInteger -> Symbolic ()

maximize :: String -> SInteger -> Symbolic ()

Metric SInt64

Methods

minimize :: String -> SInt64 -> Symbolic ()

maximize :: String -> SInt64 -> Symbolic ()

Metric SInt32

Methods

minimize :: String -> SInt32 -> Symbolic ()

maximize :: String -> SInt32 -> Symbolic ()

Metric SInt16

Methods

minimize :: String -> SInt16 -> Symbolic ()

maximize :: String -> SInt16 -> Symbolic ()

Metric SInt8

Methods

minimize :: String -> SInt8 -> Symbolic ()

maximize :: String -> SInt8 -> Symbolic ()

Metric SWord64

Methods

minimize :: String -> SWord64 -> Symbolic ()

maximize :: String -> SWord64 -> Symbolic ()

Metric SWord32

Methods

minimize :: String -> SWord32 -> Symbolic ()

maximize :: String -> SWord32 -> Symbolic ()

Metric SWord16

Methods

minimize :: String -> SWord16 -> Symbolic ()

maximize :: String -> SWord16 -> Symbolic ()

Metric SWord8

Methods

minimize :: String -> SWord8 -> Symbolic ()

maximize :: String -> SWord8 -> Symbolic ()

Soft assumptions

Related to optimization, SBV implements soft-asserts via assertSoft calls. A soft assertion is a hint to the SMT solver that we would like a particular condition to hold if **possible*. That is, if there is a solution satisfying it, then we would like it to hold, but it can be violated if there is no way to satisfy it. Each soft-assertion can be associated with a numeric penalty for not satisfying it, hence turning it into an optimization problem.

Note that assertSoft works well with optimization goals ('minimize'/'maximize' etc.), and are most useful when we are optimizing a metric and thus some of the constraints can be relaxed with a penalty to obtain a good solution. Again see https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf for a good overview of the features in Z3 that SBV is providing the bridge for.

A soft assertion can be specified in one of the following three main ways:

         assertSoft "bounded_x" (x .< 5) DefaultPenalty
         assertSoft "bounded_x" (x .< 5) (Penalty 2.3 Nothing)
         assertSoft "bounded_x" (x .< 5) (Penalty 4.7 (Just "group-1"))

In the first form, we are saying that the constraint x .< 5 must be satisfied, if possible, but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.

In the second case, we are associating a penalty value of 2.3.

Finally in the third case, we are also associating this constraint with a group. The group name is only needed if we have classes of soft-constraints that should be considered together.

assertSoft :: String -> SBool -> Penalty -> Symbolic ()

Introduce a soft assertion, with an optional penalty

data Penalty

Penalty for a soft-assertion. The default penalty is 1, with all soft-assertions belonging to the same objective goal. A positive weight and an optional group can be provided by using the Penalty constructor.

Constructors

DefaultPenalty

Default: Penalty of 1 and no group attached

Penalty Rational (Maybe String)

Penalty with a weight and an optional group

Instances

Show Penalty

Methods

showsPrec :: Int -> Penalty -> ShowS

show :: Penalty -> String

showList :: [Penalty] -> ShowS

NFData Penalty

Methods

rnf :: Penalty -> ()

Field extensions

If an optimization results in an infinity/epsilon value, the returned CW value will be in the corresponding extension field.

data ExtCW

A simple expression type over extendent values, covering infinity, epsilon and intervals.

Constructors

Infinite Kind

Epsilon Kind

Interval ExtCW ExtCW

BoundedCW CW

AddExtCW ExtCW ExtCW

MulExtCW ExtCW ExtCW

Instances

Show ExtCW

Show instance, shows with the kind

Methods

showsPrec :: Int -> ExtCW -> ShowS

show :: ExtCW -> String

showList :: [ExtCW] -> ShowS

HasKind ExtCW

Kind instance for Extended CW

Methods

kindOf :: ExtCW -> Kind

hasSign :: ExtCW -> Bool

intSizeOf :: ExtCW -> Int

isBoolean :: ExtCW -> Bool

isBounded :: ExtCW -> Bool

isReal :: ExtCW -> Bool

isFloat :: ExtCW -> Bool

isDouble :: ExtCW -> Bool

isInteger :: ExtCW -> Bool

isUninterpreted :: ExtCW -> Bool

isChar :: ExtCW -> Bool

isString :: ExtCW -> Bool

showType :: ExtCW -> String

data GeneralizedCW

A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.

Constructors

ExtendedCW ExtCW

RegularCW CW

Instances

Show GeneralizedCW

Show instance for Generalized CW

Methods

showsPrec :: Int -> GeneralizedCW -> ShowS

show :: GeneralizedCW -> String

showList :: [GeneralizedCW] -> ShowS

HasKind GeneralizedCW

Kind instance for generalized CW

Methods

kindOf :: GeneralizedCW -> Kind

hasSign :: GeneralizedCW -> Bool

intSizeOf :: GeneralizedCW -> Int

isBoolean :: GeneralizedCW -> Bool

isBounded :: GeneralizedCW -> Bool

isReal :: GeneralizedCW -> Bool

isFloat :: GeneralizedCW -> Bool

isDouble :: GeneralizedCW -> Bool

isInteger :: GeneralizedCW -> Bool

isUninterpreted :: GeneralizedCW -> Bool

isChar :: GeneralizedCW -> Bool

isString :: GeneralizedCW -> Bool

showType :: GeneralizedCW -> String

Model extraction

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

Inspecting proof results

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

newtype ThmResult

A prove call results in a ThmResult

Constructors

ThmResult SMTResult

Instances

Show ThmResult

Methods

showsPrec :: Int -> ThmResult -> ShowS

show :: ThmResult -> String

showList :: [ThmResult] -> ShowS

NFData ThmResult

Methods

rnf :: ThmResult -> ()

Modelable ThmResult

ThmResult as a generic model provider

Methods

modelExists :: ThmResult -> Bool

getModelAssignment :: SatModel b => ThmResult -> Either String (Bool, b)

getModelDictionary :: ThmResult -> Map String CW

getModelValue :: SymWord b => String -> ThmResult -> Maybe b

getModelUninterpretedValue :: String -> ThmResult -> Maybe String

extractModel :: SatModel b => ThmResult -> Maybe b

getModelObjectives :: ThmResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCW

newtype SatResult

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

Constructors

SatResult SMTResult

Instances

Show SatResult

Methods

showsPrec :: Int -> SatResult -> ShowS

show :: SatResult -> String

showList :: [SatResult] -> ShowS

NFData SatResult

Methods

rnf :: SatResult -> ()

Modelable SatResult

SatResult as a generic model provider

Methods

modelExists :: SatResult -> Bool

getModelAssignment :: SatModel b => SatResult -> Either String (Bool, b)

getModelDictionary :: SatResult -> Map String CW

getModelValue :: SymWord b => String -> SatResult -> Maybe b

getModelUninterpretedValue :: String -> SatResult -> Maybe String

extractModel :: SatModel b => SatResult -> Maybe b

getModelObjectives :: SatResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCW

newtype AllSatResult

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.

Constructors

AllSatResult (Bool, Bool, [SMTResult])

Instances

Show AllSatResult

Methods

showsPrec :: Int -> AllSatResult -> ShowS

show :: AllSatResult -> String

showList :: [AllSatResult] -> ShowS

newtype SafeResult

A safe call results in a SafeResult

Constructors

SafeResult (Maybe String, String, SMTResult)

Instances

Show SafeResult

Methods

showsPrec :: Int -> SafeResult -> ShowS

show :: SafeResult -> String

showList :: [SafeResult] -> ShowS

data OptimizeResult

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.

Constructors

LexicographicResult SMTResult

ParetoResult (Bool, [SMTResult])

IndependentResult [(String, SMTResult)]

Instances

Show OptimizeResult

Methods

showsPrec :: Int -> OptimizeResult -> ShowS

show :: OptimizeResult -> String

showList :: [OptimizeResult] -> ShowS

data SMTResult

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

Constructors

Unsatisfiable SMTConfig (Maybe [String])

Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.

Satisfiable SMTConfig SMTModel

Satisfiable with model

SatExtField SMTConfig SMTModel

Prover returned a model, but in an extension field containing Infinite/epsilon

Unknown SMTConfig String

Prover returned unknown, with the given reason

ProofError SMTConfig [String]

Prover errored out

Instances

NFData SMTResult

Methods

rnf :: SMTResult -> ()

Modelable SMTResult

SMTResult as a generic model provider

Methods

modelExists :: SMTResult -> Bool

getModelAssignment :: SatModel b => SMTResult -> Either String (Bool, b)

getModelDictionary :: SMTResult -> Map String CW

getModelValue :: SymWord b => String -> SMTResult -> Maybe b

getModelUninterpretedValue :: String -> SMTResult -> Maybe String

extractModel :: SatModel b => SMTResult -> Maybe b

getModelObjectives :: SMTResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SMTResult -> Maybe GeneralizedCW

Observing expressions

The observe command can be used to trace values of arbitrary expressions during a sat, prove, or perhaps more importantly, in a quickCheck call. This is useful for, for instance, recording expected/obtained expressions as a symbolic program is executing.

>>> :{
prove $ do a1 <- free "i1"
           a2 <- free "i2"
           let spec, res :: SWord8
               spec = a1 + a2
               res  = ite (a1 .== 12 &&& a2 .== 22)   -- insert a malicious bug!
                          1
                          (a1 + a2)
           observe "Expected" spec
           observe "Result"   res
           return $ spec .== res
:}
Falsifiable. Counter-example:
  i1       = 12 :: Word8
  i2       = 22 :: Word8
  Expected = 34 :: Word8
  Result   =  1 :: Word8

observe :: SymWord a => String -> SBV a -> Symbolic ()

Observe the value of an expression. Such values are useful in model construction, as they are printed part of a satisfying model, or a counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained pairs in a particular run.

Programmable model extraction

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

class SatModel a where

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

Minimum complete definition: parseCWs

Methods

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

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

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

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

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

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

Instances

SatModel Bool

Bool as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Bool, [CW])

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

SatModel Double

Double as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Double, [CW])

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

SatModel Float

Float as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Float, [CW])

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

SatModel Int8

Int8 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Int8, [CW])

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

SatModel Int16

Int16 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Int16, [CW])

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

SatModel Int32

Int32 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Int32, [CW])

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

SatModel Int64

Int64 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Int64, [CW])

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

SatModel Integer

Integer as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Integer, [CW])

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

SatModel Word8

Word8 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Word8, [CW])

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

SatModel Word16

Word16 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Word16, [CW])

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

SatModel Word32

Word32 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Word32, [CW])

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

SatModel Word64

Word64 as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (Word64, [CW])

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

SatModel ()

Base case for SatModel at unit type. Comes in handy if there are no real variables.

Methods

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

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

SatModel AlgReal

AlgReal as extracted from a model

Methods

parseCWs :: [CW] -> Maybe (AlgReal, [CW])

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

SatModel CW

CW as extracted from a model; trivial definition

Methods

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

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

SatModel RoundingMode

A rounding mode, extracted from a model. (Default definition suffices)

Methods

parseCWs :: [CW] -> Maybe (RoundingMode, [CW])

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

SatModel E

Make E a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (E, [CW])

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

SatModel Word4

SatModel instance, merely uses the generic parsing method.

Methods

parseCWs :: [CW] -> Maybe (Word4, [CW])

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

SatModel Color

Make Color a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Color, [CW])

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

SatModel Nationality

Make Nationality a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Nationality, [CW])

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

SatModel Beverage

Make Beverage a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Beverage, [CW])

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

SatModel Pet

Make Pet a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Pet, [CW])

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

SatModel Sport

Make Sport a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Sport, [CW])

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

SatModel Color

Make Color a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Color, [CW])

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

SatModel U2Member

Make U2Member a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (U2Member, [CW])

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

SatModel Location

Make Location a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Location, [CW])

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

SatModel Day

Make Day a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (Day, [CW])

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

SatModel BinOp

Make BinOp a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (BinOp, [CW])

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

SatModel UnOp

Make UnOp a symbolic value.

Methods

parseCWs :: [CW] -> Maybe (UnOp, [CW])

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

SatModel a => SatModel [a]

A list of values as extracted from a model. When reading a list, we go as long as we can (maximal-munch). Note that this never fails, as we can always return the empty list!

Methods

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

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

(SatModel a, SatModel b) => SatModel (a, b)

Tuples extracted from a model

Methods

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

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

(SatModel a, SatModel b, SatModel c) => SatModel (a, b, c)

3-Tuples extracted from a model

Methods

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

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

(SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d)

4-Tuples extracted from a model

Methods

parseCWs :: [CW] -> Maybe ((a, b, c, d), [CW])

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

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e)

5-Tuples extracted from a model

Methods

parseCWs :: [CW] -> Maybe ((a, b, c, d, e), [CW])

cvtModel :: ((a, b, c, d, e) -> Maybe b) -> Maybe ((a, b, c, d, e), [CW]) -> Maybe (b, [CW])

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f)

6-Tuples extracted from a model

Methods

parseCWs :: [CW] -> Maybe ((a, b, c, d, e, f), [CW])

cvtModel :: ((a, b, c, d, e, f) -> Maybe b) -> Maybe ((a, b, c, d, e, f), [CW]) -> Maybe (b, [CW])

(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g)

7-Tuples extracted from a model

Methods

parseCWs :: [CW] -> Maybe ((a, b, c, d, e, f, g), [CW])

cvtModel :: ((a, b, c, d, e, f, g) -> Maybe b) -> Maybe ((a, b, c, d, e, f, g), [CW]) -> Maybe (b, [CW])

class Modelable a where

Various SMT results that we can extract models out of.

Minimal complete definition

modelExists, getModelAssignment, getModelDictionary, getModelObjectives

Methods

modelExists :: a -> Bool

Is there a model?

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

Extract assignments of 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.)

getModelDictionary :: a -> Map String CW

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

getModelValue :: SymWord b => String -> a -> Maybe b

Extract a model value for a given element. Also see getModelValues.

getModelUninterpretedValue :: String -> a -> Maybe String

Extract a representative name for the model value of an uninterpreted kind. This is supposed to correspond to the value as computed internally by the SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues.

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

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

getModelObjectives :: a -> Map String GeneralizedCW

Extract model objective values, for all optimization goals.

getModelObjectiveValue :: String -> a -> Maybe GeneralizedCW

Extract the value of an objective

Instances

Modelable SMTResult

SMTResult as a generic model provider

Methods

modelExists :: SMTResult -> Bool

getModelAssignment :: SatModel b => SMTResult -> Either String (Bool, b)

getModelDictionary :: SMTResult -> Map String CW

getModelValue :: SymWord b => String -> SMTResult -> Maybe b

getModelUninterpretedValue :: String -> SMTResult -> Maybe String

extractModel :: SatModel b => SMTResult -> Maybe b

getModelObjectives :: SMTResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SMTResult -> Maybe GeneralizedCW

Modelable SatResult

SatResult as a generic model provider

Methods

modelExists :: SatResult -> Bool

getModelAssignment :: SatModel b => SatResult -> Either String (Bool, b)

getModelDictionary :: SatResult -> Map String CW

getModelValue :: SymWord b => String -> SatResult -> Maybe b

getModelUninterpretedValue :: String -> SatResult -> Maybe String

extractModel :: SatModel b => SatResult -> Maybe b

getModelObjectives :: SatResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> SatResult -> Maybe GeneralizedCW

Modelable ThmResult

ThmResult as a generic model provider

Methods

modelExists :: ThmResult -> Bool

getModelAssignment :: SatModel b => ThmResult -> Either String (Bool, b)

getModelDictionary :: ThmResult -> Map String CW

getModelValue :: SymWord b => String -> ThmResult -> Maybe b

getModelUninterpretedValue :: String -> ThmResult -> Maybe String

extractModel :: SatModel b => ThmResult -> Maybe b

getModelObjectives :: ThmResult -> Map String GeneralizedCW

getModelObjectiveValue :: String -> ThmResult -> Maybe GeneralizedCW

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

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

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

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

getModelDictionaries :: AllSatResult -> [Map String CW]

Get dictionaries from an all-sat call. Similar to getModelDictionary.

getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]

Extract value of a variable from an all-sat call. Similar to getModelValue.

getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]

Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.

SMT Interface

data SMTConfig

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.

Constructors

SMTConfig

Fields

• verbose :: Bool

  Debug mode

• timing :: Timing

  Print timing information on how long different phases took (construction, solving, etc.)

• printBase :: Int

  Print integral literals in this base (2, 10, and 16 are supported.)

• printRealPrec :: Int

  Print algebraic real values with this precision. (SReal, default: 16)

• satCmd :: String

  Usually "(check-sat)". However, users might tweak it based on solver characteristics.

• allSatMaxModelCount :: Maybe Int

  In an allSat call, return at most this many models. If nothing, return all.

• isNonModelVar :: String -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

• transcript :: Maybe FilePath

  If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)

• smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

• solver :: SMTSolver

  The actual SMT solver.

• roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

• solverSetOptions :: [SMTOption]

  Options to set as we start the solver

• ignoreExitCode :: Bool

  If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.

• redirectVerbose :: Maybe FilePath

  Redirect the verbose output to this file if given. If Nothing, stdout is implied.

Instances

NFData SMTConfig

Methods

rnf :: SMTConfig -> ()

data Timing

Specify how to save timing information, if at all.

Constructors

NoTiming

PrintTiming

SaveTiming (IORef NominalDiffTime)

data SMTLibVersion

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.

Constructors

SMTLib2

Instances

Bounded SMTLibVersion

Methods

minBound :: SMTLibVersion

maxBound :: SMTLibVersion

Enum SMTLibVersion

Methods

succ :: SMTLibVersion -> SMTLibVersion

pred :: SMTLibVersion -> SMTLibVersion

toEnum :: Int -> SMTLibVersion

fromEnum :: SMTLibVersion -> Int

enumFrom :: SMTLibVersion -> [SMTLibVersion]

enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]

Eq SMTLibVersion

Methods

(==) :: SMTLibVersion -> SMTLibVersion -> Bool

(/=) :: SMTLibVersion -> SMTLibVersion -> Bool

Show SMTLibVersion

Methods

showsPrec :: Int -> SMTLibVersion -> ShowS

show :: SMTLibVersion -> String

showList :: [SMTLibVersion] -> ShowS

NFData SMTLibVersion

Methods

rnf :: SMTLibVersion -> ()

data Solver

Solvers that SBV is aware of

Constructors

Z3

Yices

Boolector

CVC4

MathSAT

ABC

Instances

Bounded Solver

Methods

minBound :: Solver

maxBound :: Solver

Enum Solver

Methods

succ :: Solver -> Solver

pred :: Solver -> Solver

toEnum :: Int -> Solver

fromEnum :: Solver -> Int

enumFrom :: Solver -> [Solver]

enumFromThen :: Solver -> Solver -> [Solver]

enumFromTo :: Solver -> Solver -> [Solver]

enumFromThenTo :: Solver -> Solver -> Solver -> [Solver]

Show Solver

Methods

showsPrec :: Int -> Solver -> ShowS

show :: Solver -> String

showList :: [Solver] -> ShowS

data SMTSolver

An SMT solver

Constructors

SMTSolver

Fields

• name :: Solver

  The solver in use

• executable :: String

  The path to its executable

• options :: SMTConfig -> [String]

  Options to provide to the solver

• engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

• capabilities :: SolverCapabilities

  Various capabilities of the solver

Controlling verbosity

SBV provides various levels of verbosity to aid in debugging, by using the SMTConfig fields:

• [verbose] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise and is good for quick debugging. The output is not supposed to be machine-readable.
• [redirectVerbose] Send the verbose output to a file. Note that you still have to set `verbose=True` for redirection to take effect. Otherwise, the output is the same as what you would see in verbose.
• [transcript] Produce a file that is valid SMTLib2 format, containing everything sent and received. In particular, one can directly feed this file to the SMT-solver outside of the SBV since it is machine-readable. This is good for offline analysis situations, where you want to have a full account of what happened. For instance, it will print time-stamps at every interaction point, so you can see how long each command took.

Solvers

boolector :: SMTConfig

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig

Default configuration for the MathSAT SMT solver

abc :: SMTConfig

Default configuration for the ABC synthesis and verification tool.

Configurations

defaultSolverConfig :: Solver -> SMTConfig

The default configs corresponding to supported SMT solvers

defaultSMTCfg :: SMTConfig

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

sbvCheckSolverInstallation :: SMTConfig -> IO Bool

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

sbvAvailableSolvers :: IO [SMTConfig]

Return the known available solver configs, installed on your machine.

setLogic :: SolverContext m => Logic -> m ()

Set the logic.

setOption :: SolverContext m => SMTOption -> m ()

Set an option.

setInfo :: SolverContext m => String -> [String] -> m ()

Set info. Example: setInfo ":status" ["unsat"].

setTimeOut :: SolverContext m => Integer -> m ()

Set a solver time-out value, in milli-seconds. This function essentially translates to the SMTLib call (set-info :timeout val), and your backend solver may or may not support it! The amount given is in milliseconds. Also see the function timeOut for finer level control of time-outs, directly from SBV.

Solver exceptions

data SMTException

An SMT exception generated by the back-end solver and is thrown from SBV. If the solver ever responds with a non-success value for a command, SBV will throw an SMTException, it so the user can process it as required. The provided Show instance will render the failure nicely. Note that if you ever catch this exception, the solver is no longer alive: You should either throw the exception up, or do other proper clean-up before continuing.

Constructors

SMTException

Fields

• smtExceptionDescription :: String
• smtExceptionSent :: String
• smtExceptionExpected :: String
• smtExceptionReceived :: String
• smtExceptionStdOut :: String
• smtExceptionStdErr :: Maybe String
• smtExceptionExitCode :: Maybe ExitCode
• smtExceptionConfig :: SMTConfig
• smtExceptionReason :: Maybe [String]
• smtExceptionHint :: Maybe [String]

Instances

Show SMTException

A fairly nice rendering of the exception, for display purposes.

Methods

showsPrec :: Int -> SMTException -> ShowS

show :: SMTException -> String

showList :: [SMTException] -> ShowS

Exception SMTException

SMTExceptions are throwable. A simple "show" will render this exception nicely though of course you can inspect the individual fields as necessary.

Methods

toException :: SMTException -> SomeException

fromException :: SomeException -> Maybe SMTException

displayException :: SMTException -> String

Abstract SBV type

data SBV a

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

Instances

Boolean SBool

Methods

true :: SBool

false :: SBool

bnot :: SBool -> SBool

(&&&) :: SBool -> SBool -> SBool

(|||) :: SBool -> SBool -> SBool

(~&) :: SBool -> SBool -> SBool

(~|) :: SBool -> SBool -> SBool

(<+>) :: SBool -> SBool -> SBool

(==>) :: SBool -> SBool -> SBool

(<=>) :: SBool -> SBool -> SBool

fromBool :: Bool -> SBool

Provable SBool

Methods

forAll_ :: SBool -> Predicate

forAll :: [String] -> SBool -> Predicate

forSome_ :: SBool -> Predicate

forSome :: [String] -> SBool -> Predicate

prove :: SBool -> IO ThmResult

proveWith :: SMTConfig -> SBool -> IO ThmResult

sat :: SBool -> IO SatResult

satWith :: SMTConfig -> SBool -> IO SatResult

allSat :: SBool -> IO AllSatResult

allSatWith :: SMTConfig -> SBool -> IO AllSatResult

optimize :: OptimizeStyle -> SBool -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> SBool -> IO OptimizeResult

isVacuous :: SBool -> IO Bool

isVacuousWith :: SMTConfig -> SBool -> IO Bool

isTheorem :: SBool -> IO Bool

isTheoremWith :: SMTConfig -> SBool -> IO Bool

isSatisfiable :: SBool -> IO Bool

isSatisfiableWith :: SMTConfig -> SBool -> IO Bool

proveWithAll :: [SMTConfig] -> SBool -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> SBool -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> SBool -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> SBool -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> SBool -> IO String

Provable Predicate

Methods

forAll_ :: Predicate -> Predicate

forAll :: [String] -> Predicate -> Predicate

forSome_ :: Predicate -> Predicate

forSome :: [String] -> Predicate -> Predicate

prove :: Predicate -> IO ThmResult

proveWith :: SMTConfig -> Predicate -> IO ThmResult

sat :: Predicate -> IO SatResult

satWith :: SMTConfig -> Predicate -> IO SatResult

allSat :: Predicate -> IO AllSatResult

allSatWith :: SMTConfig -> Predicate -> IO AllSatResult

optimize :: OptimizeStyle -> Predicate -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> Predicate -> IO OptimizeResult

isVacuous :: Predicate -> IO Bool

isVacuousWith :: SMTConfig -> Predicate -> IO Bool

isTheorem :: Predicate -> IO Bool

isTheoremWith :: SMTConfig -> Predicate -> IO Bool

isSatisfiable :: Predicate -> IO Bool

isSatisfiableWith :: SMTConfig -> Predicate -> IO Bool

proveWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> Predicate -> IO String

Metric SReal

Methods

minimize :: String -> SReal -> Symbolic ()

maximize :: String -> SReal -> Symbolic ()

Metric SInteger

Methods

minimize :: String -> SInteger -> Symbolic ()

maximize :: String -> SInteger -> Symbolic ()

Metric SInt64

Methods

minimize :: String -> SInt64 -> Symbolic ()

maximize :: String -> SInt64 -> Symbolic ()

Metric SInt32

Methods

minimize :: String -> SInt32 -> Symbolic ()

maximize :: String -> SInt32 -> Symbolic ()

Metric SInt16

Methods

minimize :: String -> SInt16 -> Symbolic ()

maximize :: String -> SInt16 -> Symbolic ()

Metric SInt8

Methods

minimize :: String -> SInt8 -> Symbolic ()

maximize :: String -> SInt8 -> Symbolic ()

Metric SWord64

Methods

minimize :: String -> SWord64 -> Symbolic ()

maximize :: String -> SWord64 -> Symbolic ()

Metric SWord32

Methods

minimize :: String -> SWord32 -> Symbolic ()

maximize :: String -> SWord32 -> Symbolic ()

Metric SWord16

Methods

minimize :: String -> SWord16 -> Symbolic ()

maximize :: String -> SWord16 -> Symbolic ()

Metric SWord8

Methods

minimize :: String -> SWord8 -> Symbolic ()

maximize :: String -> SWord8 -> Symbolic ()

SDivisible SInteger

Methods

sQuotRem :: SInteger -> SInteger -> (SInteger, SInteger)

sDivMod :: SInteger -> SInteger -> (SInteger, SInteger)

sQuot :: SInteger -> SInteger -> SInteger

sRem :: SInteger -> SInteger -> SInteger

sDiv :: SInteger -> SInteger -> SInteger

sMod :: SInteger -> SInteger -> SInteger

SDivisible SInt64

Methods

sQuotRem :: SInt64 -> SInt64 -> (SInt64, SInt64)

sDivMod :: SInt64 -> SInt64 -> (SInt64, SInt64)

sQuot :: SInt64 -> SInt64 -> SInt64

sRem :: SInt64 -> SInt64 -> SInt64

sDiv :: SInt64 -> SInt64 -> SInt64

sMod :: SInt64 -> SInt64 -> SInt64

SDivisible SInt32

Methods

sQuotRem :: SInt32 -> SInt32 -> (SInt32, SInt32)

sDivMod :: SInt32 -> SInt32 -> (SInt32, SInt32)

sQuot :: SInt32 -> SInt32 -> SInt32

sRem :: SInt32 -> SInt32 -> SInt32

sDiv :: SInt32 -> SInt32 -> SInt32

sMod :: SInt32 -> SInt32 -> SInt32

SDivisible SInt16

Methods

sQuotRem :: SInt16 -> SInt16 -> (SInt16, SInt16)

sDivMod :: SInt16 -> SInt16 -> (SInt16, SInt16)

sQuot :: SInt16 -> SInt16 -> SInt16

sRem :: SInt16 -> SInt16 -> SInt16

sDiv :: SInt16 -> SInt16 -> SInt16

sMod :: SInt16 -> SInt16 -> SInt16

SDivisible SInt8

Methods

sQuotRem :: SInt8 -> SInt8 -> (SInt8, SInt8)

sDivMod :: SInt8 -> SInt8 -> (SInt8, SInt8)

sQuot :: SInt8 -> SInt8 -> SInt8

sRem :: SInt8 -> SInt8 -> SInt8

sDiv :: SInt8 -> SInt8 -> SInt8

sMod :: SInt8 -> SInt8 -> SInt8

SDivisible SWord64

Methods

sQuotRem :: SWord64 -> SWord64 -> (SWord64, SWord64)

sDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)

sQuot :: SWord64 -> SWord64 -> SWord64

sRem :: SWord64 -> SWord64 -> SWord64

sDiv :: SWord64 -> SWord64 -> SWord64

sMod :: SWord64 -> SWord64 -> SWord64

SDivisible SWord32

Methods

sQuotRem :: SWord32 -> SWord32 -> (SWord32, SWord32)

sDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)

sQuot :: SWord32 -> SWord32 -> SWord32

sRem :: SWord32 -> SWord32 -> SWord32

sDiv :: SWord32 -> SWord32 -> SWord32

sMod :: SWord32 -> SWord32 -> SWord32

SDivisible SWord16

Methods

sQuotRem :: SWord16 -> SWord16 -> (SWord16, SWord16)

sDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)

sQuot :: SWord16 -> SWord16 -> SWord16

sRem :: SWord16 -> SWord16 -> SWord16

sDiv :: SWord16 -> SWord16 -> SWord16

sMod :: SWord16 -> SWord16 -> SWord16

SDivisible SWord8

Methods

sQuotRem :: SWord8 -> SWord8 -> (SWord8, SWord8)

sDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)

sQuot :: SWord8 -> SWord8 -> SWord8

sRem :: SWord8 -> SWord8 -> SWord8

sDiv :: SWord8 -> SWord8 -> SWord8

sMod :: SWord8 -> SWord8 -> SWord8

SDivisible SWord4

SDvisible instance, using default methods

Methods

sQuotRem :: SWord4 -> SWord4 -> (SWord4, SWord4)

sDivMod :: SWord4 -> SWord4 -> (SWord4, SWord4)

sQuot :: SWord4 -> SWord4 -> SWord4

sRem :: SWord4 -> SWord4 -> SWord4

sDiv :: SWord4 -> SWord4 -> SWord4

sMod :: SWord4 -> SWord4 -> SWord4

Polynomial SWord64

Methods

polynomial :: [Int] -> SWord64

pAdd :: SWord64 -> SWord64 -> SWord64

pMult :: (SWord64, SWord64, [Int]) -> SWord64

pDiv :: SWord64 -> SWord64 -> SWord64

pMod :: SWord64 -> SWord64 -> SWord64

pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)

showPoly :: SWord64 -> String

showPolynomial :: Bool -> SWord64 -> String

Polynomial SWord32

Methods

polynomial :: [Int] -> SWord32

pAdd :: SWord32 -> SWord32 -> SWord32

pMult :: (SWord32, SWord32, [Int]) -> SWord32

pDiv :: SWord32 -> SWord32 -> SWord32

pMod :: SWord32 -> SWord32 -> SWord32

pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)

showPoly :: SWord32 -> String

showPolynomial :: Bool -> SWord32 -> String

Polynomial SWord16

Methods

polynomial :: [Int] -> SWord16

pAdd :: SWord16 -> SWord16 -> SWord16

pMult :: (SWord16, SWord16, [Int]) -> SWord16

pDiv :: SWord16 -> SWord16 -> SWord16

pMod :: SWord16 -> SWord16 -> SWord16

pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)

showPoly :: SWord16 -> String

showPolynomial :: Bool -> SWord16 -> String

Polynomial SWord8

Methods

polynomial :: [Int] -> SWord8

pAdd :: SWord8 -> SWord8 -> SWord8

pMult :: (SWord8, SWord8, [Int]) -> SWord8

pDiv :: SWord8 -> SWord8 -> SWord8

pMod :: SWord8 -> SWord8 -> SWord8

pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)

showPoly :: SWord8 -> String

showPolynomial :: Bool -> SWord8 -> String

RegExpMatchable SString

Matching symbolic strings.

Methods

match :: SString -> RegExp -> SBool

RegExpMatchable SChar

Matching a character simply means the singleton string matches the regex.

Methods

match :: SChar -> RegExp -> SBool

Splittable SWord64 SWord32

Methods

split :: SWord64 -> (SWord32, SWord32)

(#) :: SWord32 -> SWord32 -> SWord64

extend :: SWord32 -> SWord64

Splittable SWord32 SWord16

Methods

split :: SWord32 -> (SWord16, SWord16)

(#) :: SWord16 -> SWord16 -> SWord32

extend :: SWord16 -> SWord32

Splittable SWord16 SWord8

Methods

split :: SWord16 -> (SWord8, SWord8)

(#) :: SWord8 -> SWord8 -> SWord16

extend :: SWord8 -> SWord16

Eq (SBV a)

Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do. Note that we do need this instance since we want Bits as a class for SBV that we implement, which necessiates the Eq class.

Methods

(==) :: SBV a -> SBV a -> Bool

(/=) :: SBV a -> SBV a -> Bool

Show (SBV a)

A Show instance is not particularly "desirable," when the value is symbolic, but we do need this instance as otherwise we cannot simply evaluate Haskell functions that return symbolic values and have their constant values printed easily!

Methods

showsPrec :: Int -> SBV a -> ShowS

show :: SBV a -> String

showList :: [SBV a] -> ShowS

Generic (SBV a)

Associated Types

type Rep (SBV a) :: * -> *

Methods

from :: SBV a -> Rep (SBV a) x

to :: Rep (SBV a) x -> SBV a

NFData (SBV a)

Methods

rnf :: SBV a -> ()

(Random a, SymWord a) => Random (SBV a)

Methods

randomR :: RandomGen g => (SBV a, SBV a) -> g -> (SBV a, g)

random :: RandomGen g => g -> (SBV a, g)

randomRs :: RandomGen g => (SBV a, SBV a) -> g -> [SBV a]

randoms :: RandomGen g => g -> [SBV a]

randomRIO :: (SBV a, SBV a) -> IO (SBV a)

randomIO :: IO (SBV a)

HasKind (SBV a)

Methods

kindOf :: SBV a -> Kind

hasSign :: SBV a -> Bool

intSizeOf :: SBV a -> Int

isBoolean :: SBV a -> Bool

isBounded :: SBV a -> Bool

isReal :: SBV a -> Bool

isFloat :: SBV a -> Bool

isDouble :: SBV a -> Bool

isInteger :: SBV a -> Bool

isUninterpreted :: SBV a -> Bool

isChar :: SBV a -> Bool

isString :: SBV a -> Bool

showType :: SBV a -> String

Outputtable (SBV a)

Methods

output :: SBV a -> Symbolic (SBV a)

(SymWord a, PrettyNum a) => PrettyNum (SBV a)

Methods

hexS :: SBV a -> String

binS :: SBV a -> String

hex :: SBV a -> String

bin :: SBV a -> String

SExecutable [SBV a]

Methods

sName_ :: [SBV a] -> Symbolic ()

sName :: [String] -> [SBV a] -> Symbolic ()

safe :: [SBV a] -> IO [SafeResult]

safeWith :: SMTConfig -> [SBV a] -> IO [SafeResult]

SExecutable (SBV a)

Methods

sName_ :: SBV a -> Symbolic ()

sName :: [String] -> SBV a -> Symbolic ()

safe :: SBV a -> IO [SafeResult]

safeWith :: SMTConfig -> SBV a -> IO [SafeResult]

HasKind a => Uninterpreted (SBV a)

Methods

uninterpret :: String -> SBV a

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

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

SymWord a => Mergeable (SBV a)

Methods

symbolicMerge :: Bool -> SBool -> SBV a -> SBV a -> SBV a

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

SymWord a => OrdSymbolic (SBV a)

Methods

(.<) :: SBV a -> SBV a -> SBool

(.<=) :: SBV a -> SBV a -> SBool

(.>) :: SBV a -> SBV a -> SBool

(.>=) :: SBV a -> SBV a -> SBool

smin :: SBV a -> SBV a -> SBV a

smax :: SBV a -> SBV a -> SBV a

inRange :: SBV a -> (SBV a, SBV a) -> SBool

EqSymbolic (SBV a)

Methods

(.==) :: SBV a -> SBV a -> SBool

(./=) :: SBV a -> SBV a -> SBool

distinct :: [SBV a] -> SBool

allEqual :: [SBV a] -> SBool

sElem :: SBV a -> [SBV a] -> SBool

(SymWord a, SymWord b, SExecutable p) => SExecutable ((SBV a, SBV b) -> p)

Methods

sName_ :: ((SBV a, SBV b) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [SafeResult]

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, SExecutable p) => SExecutable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)

Methods

sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic ()

sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Symbolic ()

safe :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [SafeResult]

(SymWord a, SExecutable p) => SExecutable (SBV a -> p)

Methods

sName_ :: (SBV a -> p) -> Symbolic ()

sName :: [String] -> (SBV a -> p) -> Symbolic ()

safe :: (SBV a -> p) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a -> p) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b) => SExecutable (SBV a, SBV b)

Methods

sName_ :: (SBV a, SBV b) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b) -> Symbolic ()

safe :: (SBV a, SBV b) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b) -> IO [SafeResult]

(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p)

Methods

forAll_ :: ((SBV a, SBV b) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b) -> p) -> Predicate

prove :: ((SBV a, SBV b) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> IO String

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p)

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> IO String

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

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> IO String

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

Methods

forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forAll :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

forSome :: [String] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> Predicate

prove :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult

proveWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO ThmResult

sat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult

satWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO SatResult

allSat :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO OptimizeResult

isVacuous :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isVacuousWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isTheorem :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isTheoremWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isSatisfiable :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) -> IO String

(SymWord a, Provable p) => Provable (SBV a -> p)

Methods

forAll_ :: (SBV a -> p) -> Predicate

forAll :: [String] -> (SBV a -> p) -> Predicate

forSome_ :: (SBV a -> p) -> Predicate

forSome :: [String] -> (SBV a -> p) -> Predicate

prove :: (SBV a -> p) -> IO ThmResult

proveWith :: SMTConfig -> (SBV a -> p) -> IO ThmResult

sat :: (SBV a -> p) -> IO SatResult

satWith :: SMTConfig -> (SBV a -> p) -> IO SatResult

allSat :: (SBV a -> p) -> IO AllSatResult

allSatWith :: SMTConfig -> (SBV a -> p) -> IO AllSatResult

optimize :: OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> (SBV a -> p) -> IO OptimizeResult

isVacuous :: (SBV a -> p) -> IO Bool

isVacuousWith :: SMTConfig -> (SBV a -> p) -> IO Bool

isTheorem :: (SBV a -> p) -> IO Bool

isTheoremWith :: SMTConfig -> (SBV a -> p) -> IO Bool

isSatisfiable :: (SBV a -> p) -> IO Bool

isSatisfiableWith :: SMTConfig -> (SBV a -> p) -> IO Bool

proveWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> (SBV a -> p) -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> (SBV a -> p) -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> (SBV a -> p) -> IO String

(SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a)

Methods

uninterpret :: String -> (SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV c, SBV b) -> SBV a) -> (SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV c, SBV b) -> SBV a) -> String -> (SBV c, SBV b) -> SBV a

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a)

Methods

uninterpret :: String -> (SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV d, SBV c, SBV b) -> SBV a) -> (SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

cgUninterpret :: String -> [String] -> ((SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

sbvUninterpret :: Maybe ([String], (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a) -> String -> (SBV h, SBV g, SBV f, SBV e, SBV d, SBV c, SBV b) -> SBV a

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

Methods

uninterpret :: String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV h -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV g -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV f -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

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

Methods

uninterpret :: String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV e -> SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV e -> SBV d -> SBV c -> SBV b -> SBV a

(SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV d -> SBV c -> SBV b -> SBV a)

Methods

uninterpret :: String -> SBV d -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV d -> SBV c -> SBV b -> SBV a) -> SBV d -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV d -> SBV c -> SBV b -> SBV a) -> String -> SBV d -> SBV c -> SBV b -> SBV a

(SymWord c, SymWord b, HasKind a) => Uninterpreted (SBV c -> SBV b -> SBV a)

Methods

uninterpret :: String -> SBV c -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV c -> SBV b -> SBV a) -> SBV c -> SBV b -> SBV a

sbvUninterpret :: Maybe ([String], SBV c -> SBV b -> SBV a) -> String -> SBV c -> SBV b -> SBV a

(SymWord b, HasKind a) => Uninterpreted (SBV b -> SBV a)

Methods

uninterpret :: String -> SBV b -> SBV a

cgUninterpret :: String -> [String] -> (SBV b -> SBV a) -> SBV b -> SBV a

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

SymWord e => Mergeable (STree i e)

Methods

symbolicMerge :: Bool -> SBool -> STree i e -> STree i e -> STree i e

select :: (SymWord b, Num b) => [STree i e] -> STree i e -> SBV b -> STree i e

(SymWord a, SymWord b, EqSymbolic z) => Equality ((SBV a, SBV b) -> z)

Methods

(===) :: ((SBV a, SBV b) -> z) -> ((SBV a, SBV b) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c) -> z)

Methods

(===) :: ((SBV a, SBV b, SBV c) -> z) -> ((SBV a, SBV b, SBV c) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d) -> z)

Methods

(===) :: ((SBV a, SBV b, SBV c, SBV d) -> z) -> ((SBV a, SBV b, SBV c, SBV d) -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality ((SBV a, SBV b, SBV c, SBV d, SBV e) -> z)

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

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

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

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

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

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

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

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

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

(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> z)

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

(SymWord a, SymWord b, SymWord c, SymWord d, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> SBV d -> z)

Methods

(===) :: (SBV a -> SBV b -> SBV c -> SBV d -> z) -> (SBV a -> SBV b -> SBV c -> SBV d -> z) -> IO ThmResult

(SymWord a, SymWord b, SymWord c, EqSymbolic z) => Equality (SBV a -> SBV b -> SBV c -> z)

Methods

(===) :: (SBV a -> SBV b -> SBV c -> z) -> (SBV a -> SBV b -> SBV c -> z) -> IO ThmResult

(SymWord a, SymWord b, EqSymbolic z) => Equality (SBV a -> SBV b -> z)

Methods

(===) :: (SBV a -> SBV b -> z) -> (SBV a -> SBV b -> z) -> IO ThmResult

(SymWord a, EqSymbolic z) => Equality (SBV a -> z)

Methods

(===) :: (SBV a -> z) -> (SBV a -> z) -> IO ThmResult

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c) => SExecutable (SBV a, SBV b, SBV c)

Methods

sName_ :: (SBV a, SBV b, SBV c) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d) => SExecutable (SBV a, SBV b, SBV c, SBV d)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> IO [SafeResult]

(NFData a, SymWord a, NFData b, SymWord b, NFData c, SymWord c, NFData d, SymWord d, NFData e, SymWord e, NFData f, SymWord f, NFData g, SymWord g) => SExecutable (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)

Methods

sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic ()

sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Symbolic ()

safe :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult]

safeWith :: SMTConfig -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> IO [SafeResult]

type Rep (SBV a)

type Rep (SBV a) = D1 * (MetaData "SBV" "Data.SBV.Core.Data" "sbv-7.8-BxR8ndNYkpZ1uweqho7QIs" True) (C1 * (MetaCons "SBV" PrefixI True) (S1 * (MetaSel (Just Symbol "unSBV") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * SVal)))

class HasKind a where

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.

Methods

kindOf :: a -> Kind

hasSign :: a -> Bool

intSizeOf :: a -> Int

isBoolean :: a -> Bool

isBounded :: a -> Bool

isReal :: a -> Bool

isFloat :: a -> Bool

isDouble :: a -> Bool

isInteger :: a -> Bool

isUninterpreted :: a -> Bool

isChar :: a -> Bool

isString :: a -> Bool

showType :: a -> String

kindOf :: (Read a, Data a) => a -> Kind

Instances

HasKind Bool

Methods

kindOf :: Bool -> Kind

hasSign :: Bool -> Bool

intSizeOf :: Bool -> Int

isBoolean :: Bool -> Bool

isBounded :: Bool -> Bool

isReal :: Bool -> Bool

isFloat :: Bool -> Bool

isDouble :: Bool -> Bool

isInteger :: Bool -> Bool

isUninterpreted :: Bool -> Bool

isChar :: Bool -> Bool

isString :: Bool -> Bool

showType :: Bool -> String

HasKind Char

Methods

kindOf :: Char -> Kind

hasSign :: Char -> Bool

intSizeOf :: Char -> Int

isBoolean :: Char -> Bool

isBounded :: Char -> Bool

isReal :: Char -> Bool

isFloat :: Char -> Bool

isDouble :: Char -> Bool

isInteger :: Char -> Bool

isUninterpreted :: Char -> Bool

isChar :: Char -> Bool

isString :: Char -> Bool

showType :: Char -> String

HasKind Double

Methods

kindOf :: Double -> Kind

hasSign :: Double -> Bool

intSizeOf :: Double -> Int

isBoolean :: Double -> Bool

isBounded :: Double -> Bool

isReal :: Double -> Bool

isFloat :: Double -> Bool

isDouble :: Double -> Bool

isInteger :: Double -> Bool

isUninterpreted :: Double -> Bool

isChar :: Double -> Bool

isString :: Double -> Bool

showType :: Double -> String

HasKind Float

Methods

kindOf :: Float -> Kind

hasSign :: Float -> Bool

intSizeOf :: Float -> Int

isBoolean :: Float -> Bool

isBounded :: Float -> Bool

isReal :: Float -> Bool

isFloat :: Float -> Bool

isDouble :: Float -> Bool

isInteger :: Float -> Bool

isUninterpreted :: Float -> Bool

isChar :: Float -> Bool

isString :: Float -> Bool

showType :: Float -> String

HasKind Int8

Methods

kindOf :: Int8 -> Kind

hasSign :: Int8 -> Bool

intSizeOf :: Int8 -> Int

isBoolean :: Int8 -> Bool

isBounded :: Int8 -> Bool

isReal :: Int8 -> Bool

isFloat :: Int8 -> Bool

isDouble :: Int8 -> Bool

isInteger :: Int8 -> Bool

isUninterpreted :: Int8 -> Bool

isChar :: Int8 -> Bool

isString :: Int8 -> Bool

showType :: Int8 -> String

HasKind Int16

Methods

kindOf :: Int16 -> Kind

hasSign :: Int16 -> Bool

intSizeOf :: Int16 -> Int

isBoolean :: Int16 -> Bool

isBounded :: Int16 -> Bool

isReal :: Int16 -> Bool

isFloat :: Int16 -> Bool

isDouble :: Int16 -> Bool

isInteger :: Int16 -> Bool

isUninterpreted :: Int16 -> Bool

isChar :: Int16 -> Bool

isString :: Int16 -> Bool

showType :: Int16 -> String

HasKind Int32

Methods

kindOf :: Int32 -> Kind

hasSign :: Int32 -> Bool

intSizeOf :: Int32 -> Int

isBoolean :: Int32 -> Bool

isBounded :: Int32 -> Bool

isReal :: Int32 -> Bool

isFloat :: Int32 -> Bool

isDouble :: Int32 -> Bool

isInteger :: Int32 -> Bool

isUninterpreted :: Int32 -> Bool

isChar :: Int32 -> Bool

isString :: Int32 -> Bool

showType :: Int32 -> String

HasKind Int64

Methods

kindOf :: Int64 -> Kind

hasSign :: Int64 -> Bool

intSizeOf :: Int64 -> Int

isBoolean :: Int64 -> Bool

isBounded :: Int64 -> Bool

isReal :: Int64 -> Bool

isFloat :: Int64 -> Bool

isDouble :: Int64 -> Bool

isInteger :: Int64 -> Bool

isUninterpreted :: Int64 -> Bool

isChar :: Int64 -> Bool

isString :: Int64 -> Bool

showType :: Int64 -> String

HasKind Integer

Methods

kindOf :: Integer -> Kind

hasSign :: Integer -> Bool

intSizeOf :: Integer -> Int

isBoolean :: Integer -> Bool

isBounded :: Integer -> Bool

isReal :: Integer -> Bool

isFloat :: Integer -> Bool

isDouble :: Integer -> Bool

isInteger :: Integer -> Bool

isUninterpreted :: Integer -> Bool

isChar :: Integer -> Bool

isString :: Integer -> Bool

showType :: Integer -> String

HasKind Word8

Methods

kindOf :: Word8 -> Kind

hasSign :: Word8 -> Bool

intSizeOf :: Word8 -> Int

isBoolean :: Word8 -> Bool

isBounded :: Word8 -> Bool

isReal :: Word8 -> Bool

isFloat :: Word8 -> Bool

isDouble :: Word8 -> Bool

isInteger :: Word8 -> Bool

isUninterpreted :: Word8 -> Bool

isChar :: Word8 -> Bool

isString :: Word8 -> Bool

showType :: Word8 -> String

HasKind Word16

Methods

kindOf :: Word16 -> Kind

hasSign :: Word16 -> Bool

intSizeOf :: Word16 -> Int

isBoolean :: Word16 -> Bool

isBounded :: Word16 -> Bool

isReal :: Word16 -> Bool

isFloat :: Word16 -> Bool

isDouble :: Word16 -> Bool

isInteger :: Word16 -> Bool

isUninterpreted :: Word16 -> Bool

isChar :: Word16 -> Bool

isString :: Word16 -> Bool

showType :: Word16 -> String

HasKind Word32

Methods

kindOf :: Word32 -> Kind

hasSign :: Word32 -> Bool

intSizeOf :: Word32 -> Int

isBoolean :: Word32 -> Bool

isBounded :: Word32 -> Bool

isReal :: Word32 -> Bool

isFloat :: Word32 -> Bool

isDouble :: Word32 -> Bool

isInteger :: Word32 -> Bool

isUninterpreted :: Word32 -> Bool

isChar :: Word32 -> Bool

isString :: Word32 -> Bool

showType :: Word32 -> String

HasKind Word64

Methods

kindOf :: Word64 -> Kind

hasSign :: Word64 -> Bool

intSizeOf :: Word64 -> Int

isBoolean :: Word64 -> Bool

isBounded :: Word64 -> Bool

isReal :: Word64 -> Bool

isFloat :: Word64 -> Bool

isDouble :: Word64 -> Bool

isInteger :: Word64 -> Bool

isUninterpreted :: Word64 -> Bool

isChar :: Word64 -> Bool

isString :: Word64 -> Bool

showType :: Word64 -> String

HasKind String

Methods

kindOf :: String -> Kind

hasSign :: String -> Bool

intSizeOf :: String -> Int

isBoolean :: String -> Bool

isBounded :: String -> Bool

isReal :: String -> Bool

isFloat :: String -> Bool

isDouble :: String -> Bool

isInteger :: String -> Bool

isUninterpreted :: String -> Bool

isChar :: String -> Bool

isString :: String -> Bool

showType :: String -> String

HasKind AlgReal

Methods

kindOf :: AlgReal -> Kind

hasSign :: AlgReal -> Bool

intSizeOf :: AlgReal -> Int

isBoolean :: AlgReal -> Bool

isBounded :: AlgReal -> Bool

isReal :: AlgReal -> Bool

isFloat :: AlgReal -> Bool

isDouble :: AlgReal -> Bool

isInteger :: AlgReal -> Bool

isUninterpreted :: AlgReal -> Bool

isChar :: AlgReal -> Bool

isString :: AlgReal -> Bool

showType :: AlgReal -> String

HasKind Kind

Methods

kindOf :: Kind -> Kind

hasSign :: Kind -> Bool

intSizeOf :: Kind -> Int

isBoolean :: Kind -> Bool

isBounded :: Kind -> Bool

isReal :: Kind -> Bool

isFloat :: Kind -> Bool

isDouble :: Kind -> Bool

isInteger :: Kind -> Bool

isUninterpreted :: Kind -> Bool

isChar :: Kind -> Bool

isString :: Kind -> Bool

showType :: Kind -> String

HasKind ExtCW

Kind instance for Extended CW

Methods

kindOf :: ExtCW -> Kind

hasSign :: ExtCW -> Bool

intSizeOf :: ExtCW -> Int

isBoolean :: ExtCW -> Bool

isBounded :: ExtCW -> Bool

isReal :: ExtCW -> Bool

isFloat :: ExtCW -> Bool

isDouble :: ExtCW -> Bool

isInteger :: ExtCW -> Bool

isUninterpreted :: ExtCW -> Bool

isChar :: ExtCW -> Bool

isString :: ExtCW -> Bool

showType :: ExtCW -> String

HasKind GeneralizedCW

Kind instance for generalized CW

Methods

kindOf :: GeneralizedCW -> Kind

hasSign :: GeneralizedCW -> Bool

intSizeOf :: GeneralizedCW -> Int

isBoolean :: GeneralizedCW -> Bool

isBounded :: GeneralizedCW -> Bool

isReal :: GeneralizedCW -> Bool

isFloat :: GeneralizedCW -> Bool

isDouble :: GeneralizedCW -> Bool

isInteger :: GeneralizedCW -> Bool

isUninterpreted :: GeneralizedCW -> Bool

isChar :: GeneralizedCW -> Bool

isString :: GeneralizedCW -> Bool

showType :: GeneralizedCW -> String

HasKind CW

Kind instance for CW

Methods

kindOf :: CW -> Kind

hasSign :: CW -> Bool

intSizeOf :: CW -> Int

isBoolean :: CW -> Bool

isBounded :: CW -> Bool

isReal :: CW -> Bool

isFloat :: CW -> Bool

isDouble :: CW -> Bool

isInteger :: CW -> Bool

isUninterpreted :: CW -> Bool

isChar :: CW -> Bool

isString :: CW -> Bool

showType :: CW -> String

HasKind RoundingMode

RoundingMode kind

Methods

kindOf :: RoundingMode -> Kind

hasSign :: RoundingMode -> Bool

intSizeOf :: RoundingMode -> Int

isBoolean :: RoundingMode -> Bool

isBounded :: RoundingMode -> Bool

isReal :: RoundingMode -> Bool

isFloat :: RoundingMode -> Bool

isDouble :: RoundingMode -> Bool

isInteger :: RoundingMode -> Bool

isUninterpreted :: RoundingMode -> Bool

isChar :: RoundingMode -> Bool

isString :: RoundingMode -> Bool

showType :: RoundingMode -> String

HasKind SVal

Methods

kindOf :: SVal -> Kind

hasSign :: SVal -> Bool

intSizeOf :: SVal -> Int

isBoolean :: SVal -> Bool

isBounded :: SVal -> Bool

isReal :: SVal -> Bool

isFloat :: SVal -> Bool

isDouble :: SVal -> Bool

isInteger :: SVal -> Bool

isUninterpreted :: SVal -> Bool

isChar :: SVal -> Bool

isString :: SVal -> Bool

showType :: SVal -> String

HasKind SW

Methods

kindOf :: SW -> Kind

hasSign :: SW -> Bool

intSizeOf :: SW -> Int

isBoolean :: SW -> Bool

isBounded :: SW -> Bool

isReal :: SW -> Bool

isFloat :: SW -> Bool

isDouble :: SW -> Bool

isInteger :: SW -> Bool

isUninterpreted :: SW -> Bool

isChar :: SW -> Bool

isString :: SW -> Bool

showType :: SW -> String

HasKind E

Methods

kindOf :: E -> Kind

hasSign :: E -> Bool

intSizeOf :: E -> Int

isBoolean :: E -> Bool

isBounded :: E -> Bool

isReal :: E -> Bool

isFloat :: E -> Bool

isDouble :: E -> Bool

isInteger :: E -> Bool

isUninterpreted :: E -> Bool

isChar :: E -> Bool

isString :: E -> Bool

showType :: E -> String

HasKind Word4

HasKind instance; simply returning the underlying kind for the type

Methods

kindOf :: Word4 -> Kind

hasSign :: Word4 -> Bool

intSizeOf :: Word4 -> Int

isBoolean :: Word4 -> Bool

isBounded :: Word4 -> Bool

isReal :: Word4 -> Bool

isFloat :: Word4 -> Bool

isDouble :: Word4 -> Bool

isInteger :: Word4 -> Bool

isUninterpreted :: Word4 -> Bool

isChar :: Word4 -> Bool

isString :: Word4 -> Bool

showType :: Word4 -> String

HasKind Color

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isInteger :: Color -> Bool

isUninterpreted :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

showType :: Color -> String

HasKind Nationality

Methods

kindOf :: Nationality -> Kind

hasSign :: Nationality -> Bool

intSizeOf :: Nationality -> Int

isBoolean :: Nationality -> Bool

isBounded :: Nationality -> Bool

isReal :: Nationality -> Bool

isFloat :: Nationality -> Bool

isDouble :: Nationality -> Bool

isInteger :: Nationality -> Bool

isUninterpreted :: Nationality -> Bool

isChar :: Nationality -> Bool

isString :: Nationality -> Bool

showType :: Nationality -> String

HasKind Beverage

Methods

kindOf :: Beverage -> Kind

hasSign :: Beverage -> Bool

intSizeOf :: Beverage -> Int

isBoolean :: Beverage -> Bool

isBounded :: Beverage -> Bool

isReal :: Beverage -> Bool

isFloat :: Beverage -> Bool

isDouble :: Beverage -> Bool

isInteger :: Beverage -> Bool

isUninterpreted :: Beverage -> Bool

isChar :: Beverage -> Bool

isString :: Beverage -> Bool

showType :: Beverage -> String

HasKind Pet

Methods

kindOf :: Pet -> Kind

hasSign :: Pet -> Bool

intSizeOf :: Pet -> Int

isBoolean :: Pet -> Bool

isBounded :: Pet -> Bool

isReal :: Pet -> Bool

isFloat :: Pet -> Bool

isDouble :: Pet -> Bool

isInteger :: Pet -> Bool

isUninterpreted :: Pet -> Bool

isChar :: Pet -> Bool

isString :: Pet -> Bool

showType :: Pet -> String

HasKind Sport

Methods

kindOf :: Sport -> Kind

hasSign :: Sport -> Bool

intSizeOf :: Sport -> Int

isBoolean :: Sport -> Bool

isBounded :: Sport -> Bool

isReal :: Sport -> Bool

isFloat :: Sport -> Bool

isDouble :: Sport -> Bool

isInteger :: Sport -> Bool

isUninterpreted :: Sport -> Bool

isChar :: Sport -> Bool

isString :: Sport -> Bool

showType :: Sport -> String

HasKind Color

Methods

kindOf :: Color -> Kind

hasSign :: Color -> Bool

intSizeOf :: Color -> Int

isBoolean :: Color -> Bool

isBounded :: Color -> Bool

isReal :: Color -> Bool

isFloat :: Color -> Bool

isDouble :: Color -> Bool

isInteger :: Color -> Bool

isUninterpreted :: Color -> Bool

isChar :: Color -> Bool

isString :: Color -> Bool

showType :: Color -> String

HasKind U2Member

Methods

kindOf :: U2Member -> Kind

hasSign :: U2Member -> Bool

intSizeOf :: U2Member -> Int

isBoolean :: U2Member -> Bool

isBounded :: U2Member -> Bool

isReal :: U2Member -> Bool

isFloat :: U2Member -> Bool

isDouble :: U2Member -> Bool

isInteger :: U2Member -> Bool

isUninterpreted :: U2Member -> Bool

isChar :: U2Member -> Bool

isString :: U2Member -> Bool

showType :: U2Member -> String

HasKind Location

Methods

kindOf :: Location -> Kind

hasSign :: Location -> Bool

intSizeOf :: Location -> Int

isBoolean :: Location -> Bool

isBounded :: Location -> Bool

isReal :: Location -> Bool

isFloat :: Location -> Bool

isDouble :: Location -> Bool

isInteger :: Location -> Bool

isUninterpreted :: Location -> Bool

isChar :: Location -> Bool

isString :: Location -> Bool

showType :: Location -> String

HasKind Day

Methods

kindOf :: Day -> Kind

hasSign :: Day -> Bool

intSizeOf :: Day -> Int

isBoolean :: Day -> Bool

isBounded :: Day -> Bool

isReal :: Day -> Bool

isFloat :: Day -> Bool

isDouble :: Day -> Bool

isInteger :: Day -> Bool

isUninterpreted :: Day -> Bool

isChar :: Day -> Bool

isString :: Day -> Bool

showType :: Day -> String

HasKind BinOp

Methods

kindOf :: BinOp -> Kind

hasSign :: BinOp -> Bool

intSizeOf :: BinOp -> Int

isBoolean :: BinOp -> Bool

isBounded :: BinOp -> Bool

isReal :: BinOp -> Bool

isFloat :: BinOp -> Bool

isDouble :: BinOp -> Bool

isInteger :: BinOp -> Bool

isUninterpreted :: BinOp -> Bool

isChar :: BinOp -> Bool

isString :: BinOp -> Bool

showType :: BinOp -> String

HasKind UnOp

Methods

kindOf :: UnOp -> Kind

hasSign :: UnOp -> Bool

intSizeOf :: UnOp -> Int

isBoolean :: UnOp -> Bool

isBounded :: UnOp -> Bool

isReal :: UnOp -> Bool

isFloat :: UnOp -> Bool

isDouble :: UnOp -> Bool

isInteger :: UnOp -> Bool

isUninterpreted :: UnOp -> Bool

isChar :: UnOp -> Bool

isString :: UnOp -> Bool

showType :: UnOp -> String

HasKind B

Methods

kindOf :: B -> Kind

hasSign :: B -> Bool

intSizeOf :: B -> Int

isBoolean :: B -> Bool

isBounded :: B -> Bool

isReal :: B -> Bool

isFloat :: B -> Bool

isDouble :: B -> Bool

isInteger :: B -> Bool

isUninterpreted :: B -> Bool

isChar :: B -> Bool

isString :: B -> Bool

showType :: B -> String

HasKind Q

Methods

kindOf :: Q -> Kind

hasSign :: Q -> Bool

intSizeOf :: Q -> Int

isBoolean :: Q -> Bool

isBounded :: Q -> Bool

isReal :: Q -> Bool

isFloat :: Q -> Bool

isDouble :: Q -> Bool

isInteger :: Q -> Bool

isUninterpreted :: Q -> Bool

isChar :: Q -> Bool

isString :: Q -> Bool

showType :: Q -> String

HasKind L

Similarly, HasKinds default implementation is sufficient.

Methods

kindOf :: L -> Kind

hasSign :: L -> Bool

intSizeOf :: L -> Int

isBoolean :: L -> Bool

isBounded :: L -> Bool

isReal :: L -> Bool

isFloat :: L -> Bool

isDouble :: L -> Bool

isInteger :: L -> Bool

isUninterpreted :: L -> Bool

isChar :: L -> Bool

isString :: L -> Bool

showType :: L -> String

HasKind (SBV a)

Methods

kindOf :: SBV a -> Kind

hasSign :: SBV a -> Bool

intSizeOf :: SBV a -> Int

isBoolean :: SBV a -> Bool

isBounded :: SBV a -> Bool

isReal :: SBV a -> Bool

isFloat :: SBV a -> Bool

isDouble :: SBV a -> Bool

isInteger :: SBV a -> Bool

isUninterpreted :: SBV a -> Bool

isChar :: SBV a -> Bool

isString :: SBV a -> Bool

showType :: SBV a -> String

data Kind

Kind of symbolic value

Constructors

KBool

KBounded !Bool !Int

KUnbounded

KReal

KUserSort String (Either String [String])

KFloat

KDouble

KChar

KString

Instances

Eq Kind

We want to equate user-sorts only by name

Methods

(==) :: Kind -> Kind -> Bool

(/=) :: Kind -> Kind -> Bool

Ord Kind

We want to order user-sorts only by name

Methods

compare :: Kind -> Kind -> Ordering

(<) :: Kind -> Kind -> Bool

(<=) :: Kind -> Kind -> Bool

(>) :: Kind -> Kind -> Bool

(>=) :: Kind -> Kind -> Bool

max :: Kind -> Kind -> Kind

min :: Kind -> Kind -> Kind

Show Kind

Methods

showsPrec :: Int -> Kind -> ShowS

show :: Kind -> String

showList :: [Kind] -> ShowS

HasKind Kind

Methods

kindOf :: Kind -> Kind

hasSign :: Kind -> Bool

intSizeOf :: Kind -> Int

isBoolean :: Kind -> Bool

isBounded :: Kind -> Bool

isReal :: Kind -> Bool

isFloat :: Kind -> Bool

isDouble :: Kind -> Bool

isInteger :: Kind -> Bool

isUninterpreted :: Kind -> Bool

isChar :: Kind -> Bool

isString :: Kind -> Bool

showType :: Kind -> String

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

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

Methods

forall :: String -> Symbolic (SBV a)

Create a user named input (universal)

forall_ :: Symbolic (SBV a)

Create an automatically named input

mkForallVars :: Int -> Symbolic [SBV a]

Get a bunch of new words

exists :: String -> Symbolic (SBV a)

Create an existential variable

exists_ :: Symbolic (SBV a)

Create an automatically named existential variable

mkExistVars :: Int -> Symbolic [SBV a]

Create a bunch of existentials

free :: String -> Symbolic (SBV a)

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

free_ :: Symbolic (SBV a)

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

mkFreeVars :: Int -> Symbolic [SBV a]

Create a bunch of free vars

symbolic :: String -> Symbolic (SBV a)

Similar to free; Just a more convenient name

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

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

literal :: a -> SBV a

Turn a literal constant to symbolic

unliteral :: SBV a -> Maybe a

Extract a literal, if the value is concrete

fromCW :: CW -> a

Extract a literal, from a CW representation

isConcrete :: SBV a -> Bool

Is the symbolic word concrete?

isSymbolic :: SBV a -> Bool

Is the symbolic word really symbolic?

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

Does it concretely satisfy the given predicate?

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

One stop allocator

literal :: Show a => a -> SBV a

Turn a literal constant to symbolic

fromCW :: Read a => CW -> a

Extract a literal, from a CW representation

mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)

One stop allocator

Instances

SymWord RoundingMode

RoundingMode can be used symbolically

Methods

forall :: String -> Symbolic (SBV RoundingMode)

forall_ :: Symbolic (SBV RoundingMode)

mkForallVars :: Int -> Symbolic [SBV RoundingMode]

exists :: String -> Symbolic (SBV RoundingMode)

exists_ :: Symbolic (SBV RoundingMode)

mkExistVars :: Int -> Symbolic [SBV RoundingMode]

free :: String -> Symbolic (SBV RoundingMode)

free_ :: Symbolic (SBV RoundingMode)

mkFreeVars :: Int -> Symbolic [SBV RoundingMode]

symbolic :: String -> Symbolic (SBV RoundingMode)

symbolics :: [String] -> Symbolic [SBV RoundingMode]

literal :: RoundingMode -> SBV RoundingMode

unliteral :: SBV RoundingMode -> Maybe RoundingMode

fromCW :: CW -> RoundingMode

isConcrete :: SBV RoundingMode -> Bool

isSymbolic :: SBV RoundingMode -> Bool

isConcretely :: SBV RoundingMode -> (RoundingMode -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV RoundingMode)

SymWord E

Methods

forall :: String -> Symbolic (SBV E)

forall_ :: Symbolic (SBV E)

mkForallVars :: Int -> Symbolic [SBV E]

exists :: String -> Symbolic (SBV E)

exists_ :: Symbolic (SBV E)

mkExistVars :: Int -> Symbolic [SBV E]

free :: String -> Symbolic (SBV E)

free_ :: Symbolic (SBV E)

mkFreeVars :: Int -> Symbolic [SBV E]

symbolic :: String -> Symbolic (SBV E)

symbolics :: [String] -> Symbolic [SBV E]

literal :: E -> SBV E

unliteral :: SBV E -> Maybe E

fromCW :: CW -> E

isConcrete :: SBV E -> Bool

isSymbolic :: SBV E -> Bool

isConcretely :: SBV E -> (E -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV E)

SymWord Word4

SymWord instance, allowing this type to be used in proofs/sat etc.

Methods

forall :: String -> Symbolic (SBV Word4)

forall_ :: Symbolic (SBV Word4)

mkForallVars :: Int -> Symbolic [SBV Word4]

exists :: String -> Symbolic (SBV Word4)

exists_ :: Symbolic (SBV Word4)

mkExistVars :: Int -> Symbolic [SBV Word4]

free :: String -> Symbolic (SBV Word4)

free_ :: Symbolic (SBV Word4)

mkFreeVars :: Int -> Symbolic [SBV Word4]

symbolic :: String -> Symbolic (SBV Word4)

symbolics :: [String] -> Symbolic [SBV Word4]

literal :: Word4 -> SBV Word4

unliteral :: SBV Word4 -> Maybe Word4

fromCW :: CW -> Word4

isConcrete :: SBV Word4 -> Bool

isSymbolic :: SBV Word4 -> Bool

isConcretely :: SBV Word4 -> (Word4 -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Word4)

SymWord Color

Methods

forall :: String -> Symbolic (SBV Color)

forall_ :: Symbolic (SBV Color)

mkForallVars :: Int -> Symbolic [SBV Color]

exists :: String -> Symbolic (SBV Color)

exists_ :: Symbolic (SBV Color)

mkExistVars :: Int -> Symbolic [SBV Color]

free :: String -> Symbolic (SBV Color)

free_ :: Symbolic (SBV Color)

mkFreeVars :: Int -> Symbolic [SBV Color]

symbolic :: String -> Symbolic (SBV Color)

symbolics :: [String] -> Symbolic [SBV Color]

literal :: Color -> SBV Color

unliteral :: SBV Color -> Maybe Color

fromCW :: CW -> Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

isConcretely :: SBV Color -> (Color -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color)

SymWord Nationality

Methods

forall :: String -> Symbolic (SBV Nationality)

forall_ :: Symbolic (SBV Nationality)

mkForallVars :: Int -> Symbolic [SBV Nationality]

exists :: String -> Symbolic (SBV Nationality)

exists_ :: Symbolic (SBV Nationality)

mkExistVars :: Int -> Symbolic [SBV Nationality]

free :: String -> Symbolic (SBV Nationality)

free_ :: Symbolic (SBV Nationality)

mkFreeVars :: Int -> Symbolic [SBV Nationality]

symbolic :: String -> Symbolic (SBV Nationality)

symbolics :: [String] -> Symbolic [SBV Nationality]

literal :: Nationality -> SBV Nationality

unliteral :: SBV Nationality -> Maybe Nationality

fromCW :: CW -> Nationality

isConcrete :: SBV Nationality -> Bool

isSymbolic :: SBV Nationality -> Bool

isConcretely :: SBV Nationality -> (Nationality -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Nationality)

SymWord Beverage

Methods

forall :: String -> Symbolic (SBV Beverage)

forall_ :: Symbolic (SBV Beverage)

mkForallVars :: Int -> Symbolic [SBV Beverage]

exists :: String -> Symbolic (SBV Beverage)

exists_ :: Symbolic (SBV Beverage)

mkExistVars :: Int -> Symbolic [SBV Beverage]

free :: String -> Symbolic (SBV Beverage)

free_ :: Symbolic (SBV Beverage)

mkFreeVars :: Int -> Symbolic [SBV Beverage]

symbolic :: String -> Symbolic (SBV Beverage)

symbolics :: [String] -> Symbolic [SBV Beverage]

literal :: Beverage -> SBV Beverage

unliteral :: SBV Beverage -> Maybe Beverage

fromCW :: CW -> Beverage

isConcrete :: SBV Beverage -> Bool

isSymbolic :: SBV Beverage -> Bool

isConcretely :: SBV Beverage -> (Beverage -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Beverage)

SymWord Pet

Methods

forall :: String -> Symbolic (SBV Pet)

forall_ :: Symbolic (SBV Pet)

mkForallVars :: Int -> Symbolic [SBV Pet]

exists :: String -> Symbolic (SBV Pet)

exists_ :: Symbolic (SBV Pet)

mkExistVars :: Int -> Symbolic [SBV Pet]

free :: String -> Symbolic (SBV Pet)

free_ :: Symbolic (SBV Pet)

mkFreeVars :: Int -> Symbolic [SBV Pet]

symbolic :: String -> Symbolic (SBV Pet)

symbolics :: [String] -> Symbolic [SBV Pet]

literal :: Pet -> SBV Pet

unliteral :: SBV Pet -> Maybe Pet

fromCW :: CW -> Pet

isConcrete :: SBV Pet -> Bool

isSymbolic :: SBV Pet -> Bool

isConcretely :: SBV Pet -> (Pet -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Pet)

SymWord Sport

Methods

forall :: String -> Symbolic (SBV Sport)

forall_ :: Symbolic (SBV Sport)

mkForallVars :: Int -> Symbolic [SBV Sport]

exists :: String -> Symbolic (SBV Sport)

exists_ :: Symbolic (SBV Sport)

mkExistVars :: Int -> Symbolic [SBV Sport]

free :: String -> Symbolic (SBV Sport)

free_ :: Symbolic (SBV Sport)

mkFreeVars :: Int -> Symbolic [SBV Sport]

symbolic :: String -> Symbolic (SBV Sport)

symbolics :: [String] -> Symbolic [SBV Sport]

literal :: Sport -> SBV Sport

unliteral :: SBV Sport -> Maybe Sport

fromCW :: CW -> Sport

isConcrete :: SBV Sport -> Bool

isSymbolic :: SBV Sport -> Bool

isConcretely :: SBV Sport -> (Sport -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Sport)

SymWord Color

Methods

forall :: String -> Symbolic (SBV Color)

forall_ :: Symbolic (SBV Color)

mkForallVars :: Int -> Symbolic [SBV Color]

exists :: String -> Symbolic (SBV Color)

exists_ :: Symbolic (SBV Color)

mkExistVars :: Int -> Symbolic [SBV Color]

free :: String -> Symbolic (SBV Color)

free_ :: Symbolic (SBV Color)

mkFreeVars :: Int -> Symbolic [SBV Color]

symbolic :: String -> Symbolic (SBV Color)

symbolics :: [String] -> Symbolic [SBV Color]

literal :: Color -> SBV Color

unliteral :: SBV Color -> Maybe Color

fromCW :: CW -> Color

isConcrete :: SBV Color -> Bool

isSymbolic :: SBV Color -> Bool

isConcretely :: SBV Color -> (Color -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Color)

SymWord U2Member

Methods

forall :: String -> Symbolic (SBV U2Member)

forall_ :: Symbolic (SBV U2Member)

mkForallVars :: Int -> Symbolic [SBV U2Member]

exists :: String -> Symbolic (SBV U2Member)

exists_ :: Symbolic (SBV U2Member)

mkExistVars :: Int -> Symbolic [SBV U2Member]

free :: String -> Symbolic (SBV U2Member)

free_ :: Symbolic (SBV U2Member)

mkFreeVars :: Int -> Symbolic [SBV U2Member]

symbolic :: String -> Symbolic (SBV U2Member)

symbolics :: [String] -> Symbolic [SBV U2Member]

literal :: U2Member -> SBV U2Member

unliteral :: SBV U2Member -> Maybe U2Member

fromCW :: CW -> U2Member

isConcrete :: SBV U2Member -> Bool

isSymbolic :: SBV U2Member -> Bool

isConcretely :: SBV U2Member -> (U2Member -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV U2Member)

SymWord Location

Methods

forall :: String -> Symbolic (SBV Location)

forall_ :: Symbolic (SBV Location)

mkForallVars :: Int -> Symbolic [SBV Location]

exists :: String -> Symbolic (SBV Location)

exists_ :: Symbolic (SBV Location)

mkExistVars :: Int -> Symbolic [SBV Location]

free :: String -> Symbolic (SBV Location)

free_ :: Symbolic (SBV Location)

mkFreeVars :: Int -> Symbolic [SBV Location]

symbolic :: String -> Symbolic (SBV Location)

symbolics :: [String] -> Symbolic [SBV Location]

literal :: Location -> SBV Location

unliteral :: SBV Location -> Maybe Location

fromCW :: CW -> Location

isConcrete :: SBV Location -> Bool

isSymbolic :: SBV Location -> Bool

isConcretely :: SBV Location -> (Location -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Location)

SymWord Day

Methods

forall :: String -> Symbolic (SBV Day)

forall_ :: Symbolic (SBV Day)

mkForallVars :: Int -> Symbolic [SBV Day]

exists :: String -> Symbolic (SBV Day)

exists_ :: Symbolic (SBV Day)

mkExistVars :: Int -> Symbolic [SBV Day]

free :: String -> Symbolic (SBV Day)

free_ :: Symbolic (SBV Day)

mkFreeVars :: Int -> Symbolic [SBV Day]

symbolic :: String -> Symbolic (SBV Day)

symbolics :: [String] -> Symbolic [SBV Day]

literal :: Day -> SBV Day

unliteral :: SBV Day -> Maybe Day

fromCW :: CW -> Day

isConcrete :: SBV Day -> Bool

isSymbolic :: SBV Day -> Bool

isConcretely :: SBV Day -> (Day -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Day)

SymWord BinOp

Methods

forall :: String -> Symbolic (SBV BinOp)

forall_ :: Symbolic (SBV BinOp)

mkForallVars :: Int -> Symbolic [SBV BinOp]

exists :: String -> Symbolic (SBV BinOp)

exists_ :: Symbolic (SBV BinOp)

mkExistVars :: Int -> Symbolic [SBV BinOp]

free :: String -> Symbolic (SBV BinOp)

free_ :: Symbolic (SBV BinOp)

mkFreeVars :: Int -> Symbolic [SBV BinOp]

symbolic :: String -> Symbolic (SBV BinOp)

symbolics :: [String] -> Symbolic [SBV BinOp]

literal :: BinOp -> SBV BinOp

unliteral :: SBV BinOp -> Maybe BinOp

fromCW :: CW -> BinOp

isConcrete :: SBV BinOp -> Bool

isSymbolic :: SBV BinOp -> Bool

isConcretely :: SBV BinOp -> (BinOp -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV BinOp)

SymWord UnOp

Methods

forall :: String -> Symbolic (SBV UnOp)

forall_ :: Symbolic (SBV UnOp)

mkForallVars :: Int -> Symbolic [SBV UnOp]

exists :: String -> Symbolic (SBV UnOp)

exists_ :: Symbolic (SBV UnOp)

mkExistVars :: Int -> Symbolic [SBV UnOp]

free :: String -> Symbolic (SBV UnOp)

free_ :: Symbolic (SBV UnOp)

mkFreeVars :: Int -> Symbolic [SBV UnOp]

symbolic :: String -> Symbolic (SBV UnOp)

symbolics :: [String] -> Symbolic [SBV UnOp]

literal :: UnOp -> SBV UnOp

unliteral :: SBV UnOp -> Maybe UnOp

fromCW :: CW -> UnOp

isConcrete :: SBV UnOp -> Bool

isSymbolic :: SBV UnOp -> Bool

isConcretely :: SBV UnOp -> (UnOp -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV UnOp)

SymWord B

Methods

forall :: String -> Symbolic (SBV B)

forall_ :: Symbolic (SBV B)

mkForallVars :: Int -> Symbolic [SBV B]

exists :: String -> Symbolic (SBV B)

exists_ :: Symbolic (SBV B)

mkExistVars :: Int -> Symbolic [SBV B]

free :: String -> Symbolic (SBV B)

free_ :: Symbolic (SBV B)

mkFreeVars :: Int -> Symbolic [SBV B]

symbolic :: String -> Symbolic (SBV B)

symbolics :: [String] -> Symbolic [SBV B]

literal :: B -> SBV B

unliteral :: SBV B -> Maybe B

fromCW :: CW -> B

isConcrete :: SBV B -> Bool

isSymbolic :: SBV B -> Bool

isConcretely :: SBV B -> (B -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV B)

SymWord Q

Methods

forall :: String -> Symbolic (SBV Q)

forall_ :: Symbolic (SBV Q)

mkForallVars :: Int -> Symbolic [SBV Q]

exists :: String -> Symbolic (SBV Q)

exists_ :: Symbolic (SBV Q)

mkExistVars :: Int -> Symbolic [SBV Q]

free :: String -> Symbolic (SBV Q)

free_ :: Symbolic (SBV Q)

mkFreeVars :: Int -> Symbolic [SBV Q]

symbolic :: String -> Symbolic (SBV Q)

symbolics :: [String] -> Symbolic [SBV Q]

literal :: Q -> SBV Q

unliteral :: SBV Q -> Maybe Q

fromCW :: CW -> Q

isConcrete :: SBV Q -> Bool

isSymbolic :: SBV Q -> Bool

isConcretely :: SBV Q -> (Q -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV Q)

SymWord L

Declare instances to make L a usable uninterpreted sort. First we need the SymWord instance, with the default definition sufficing.

Methods

forall :: String -> Symbolic (SBV L)

forall_ :: Symbolic (SBV L)

mkForallVars :: Int -> Symbolic [SBV L]

exists :: String -> Symbolic (SBV L)

exists_ :: Symbolic (SBV L)

mkExistVars :: Int -> Symbolic [SBV L]

free :: String -> Symbolic (SBV L)

free_ :: Symbolic (SBV L)

mkFreeVars :: Int -> Symbolic [SBV L]

symbolic :: String -> Symbolic (SBV L)

symbolics :: [String] -> Symbolic [SBV L]

literal :: L -> SBV L

unliteral :: SBV L -> Maybe L

fromCW :: CW -> L

isConcrete :: SBV L -> Bool

isSymbolic :: SBV L -> Bool

isConcretely :: SBV L -> (L -> Bool) -> Bool

mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV L)

data Symbolic a

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

Instances

Monad Symbolic

Methods

(>>=) :: Symbolic a -> (a -> Symbolic b) -> Symbolic b

(>>) :: Symbolic a -> Symbolic b -> Symbolic b

return :: a -> Symbolic a

fail :: String -> Symbolic a

Functor Symbolic

Methods

fmap :: (a -> b) -> Symbolic a -> Symbolic b

(<$) :: a -> Symbolic b -> Symbolic a

Applicative Symbolic

Methods

pure :: a -> Symbolic a

(<*>) :: Symbolic (a -> b) -> Symbolic a -> Symbolic b

liftA2 :: (a -> b -> c) -> Symbolic a -> Symbolic b -> Symbolic c

(*>) :: Symbolic a -> Symbolic b -> Symbolic b

(<*) :: Symbolic a -> Symbolic b -> Symbolic a

MonadIO Symbolic

Methods

liftIO :: IO a -> Symbolic a

Provable Predicate

Methods

forAll_ :: Predicate -> Predicate

forAll :: [String] -> Predicate -> Predicate

forSome_ :: Predicate -> Predicate

forSome :: [String] -> Predicate -> Predicate

prove :: Predicate -> IO ThmResult

proveWith :: SMTConfig -> Predicate -> IO ThmResult

sat :: Predicate -> IO SatResult

satWith :: SMTConfig -> Predicate -> IO SatResult

allSat :: Predicate -> IO AllSatResult

allSatWith :: SMTConfig -> Predicate -> IO AllSatResult

optimize :: OptimizeStyle -> Predicate -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> Predicate -> IO OptimizeResult

isVacuous :: Predicate -> IO Bool

isVacuousWith :: SMTConfig -> Predicate -> IO Bool

isTheorem :: Predicate -> IO Bool

isTheoremWith :: SMTConfig -> Predicate -> IO Bool

isSatisfiable :: Predicate -> IO Bool

isSatisfiableWith :: SMTConfig -> Predicate -> IO Bool

proveWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> Predicate -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> Predicate -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> Predicate -> IO String

MonadReader State Symbolic

Methods

ask :: Symbolic State

local :: (State -> State) -> Symbolic a -> Symbolic a

reader :: (State -> a) -> Symbolic a

NFData a => SExecutable (Symbolic a)

Methods

sName_ :: Symbolic a -> Symbolic ()

sName :: [String] -> Symbolic a -> Symbolic ()

safe :: Symbolic a -> IO [SafeResult]

safeWith :: SMTConfig -> Symbolic a -> IO [SafeResult]

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

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.

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

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

runSMT :: Symbolic a -> IO a

Run an arbitrary symbolic computation, equivalent to runSMTWith defaultSMTCfg

runSMTWith :: SMTConfig -> Symbolic a -> IO a

Runs an arbitrary symbolic computation, exposed to the user in SAT mode

Module exports

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

module Data.Bits

module Data.Word

module Data.Int

module Data.Ratio

Orphan instances

Provable Goal

Methods

forAll_ :: Goal -> Predicate

forAll :: [String] -> Goal -> Predicate

forSome_ :: Goal -> Predicate

forSome :: [String] -> Goal -> Predicate

prove :: Goal -> IO ThmResult

proveWith :: SMTConfig -> Goal -> IO ThmResult

sat :: Goal -> IO SatResult

satWith :: SMTConfig -> Goal -> IO SatResult

allSat :: Goal -> IO AllSatResult

allSatWith :: SMTConfig -> Goal -> IO AllSatResult

optimize :: OptimizeStyle -> Goal -> IO OptimizeResult

optimizeWith :: SMTConfig -> OptimizeStyle -> Goal -> IO OptimizeResult

isVacuous :: Goal -> IO Bool

isVacuousWith :: SMTConfig -> Goal -> IO Bool

isTheorem :: Goal -> IO Bool

isTheoremWith :: SMTConfig -> Goal -> IO Bool

isSatisfiable :: Goal -> IO Bool

isSatisfiableWith :: SMTConfig -> Goal -> IO Bool

proveWithAll :: [SMTConfig] -> Goal -> IO [(Solver, NominalDiffTime, ThmResult)]

proveWithAny :: [SMTConfig] -> Goal -> IO (Solver, NominalDiffTime, ThmResult)

satWithAll :: [SMTConfig] -> Goal -> IO [(Solver, NominalDiffTime, SatResult)]

satWithAny :: [SMTConfig] -> Goal -> IO (Solver, NominalDiffTime, SatResult)

generateSMTBenchmark :: Bool -> Goal -> IO String