Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

- Symbolic types
- Arrays of symbolic values
- Creating symbolic values
- Symbolic Equality and Comparisons
- Conditionals: Mergeable values
- Symbolic integral numbers
- Division and Modulus
- Bit-vector operations
- IEEE-floating point numbers
- Enumerations
- Uninterpreted sorts, constants, and functions
- Stopping unrolling: Defined functions
- Special relations
- Properties, proofs, and satisfiability
- Constraints and Quantifiers
- Checking safety
- Quick-checking
- Optimization
- Model extraction
- SMT Interface
- Abstract SBV type
- Module exports

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

`>>>`

Q.E.D.`prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)`

`>>>`

Falsifiable. Counter-example: s0 = 64 :: Word8`prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)`

And similarly, `sat`

finds a satisfying instance. The types involved are:

`prove`

::`Provable`

a => a ->`IO`

`ThmResult`

`sat`

::`Satisfiable`

a => a ->`IO`

`SatResult`

The classes `Provable`

and `Satisfiable`

come 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).`SWord`

`n`

: Generalized symbolic words of arbitrary bit-size.`SInt`

`n`

: Generalized symbolic ints of arbitrary bit-size.`SInteger`

: Unbounded signed integers.`SReal`

: Algebraic-real numbers.`SFloat`

: IEEE-754 single-precision floating point values.`SDouble`

: IEEE-754 double-precision floating point values.`SRational`

: Rationals. (Ratio of two symbolic integers.)`SFloatingPoint`

: Generalized IEEE-754 floating point values, with user specified exponent and mantissa widths.`SChar`

,`SString`

,`RegExp`

: Characters, strings and regular expressions.`SList`

: Symbolic lists (which can be nested)`STuple`

,`STuple2`

,`STuple3`

, ..,`STuple8`

: Symbolic tuples (upto 8-tuples, can be nested)`SEither`

: Symbolic sums`SMaybe`

: Symbolic optional values.`SSet`

: Symbolic sets.`SArray`

: 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.
- Ability to define SMTLib functions, generated directly from Haskell versions, including support for recursive and mutually recursive functions.
- Express quantified formulas (both universals and existentials, including alternating quantifiers), covering first-order logic.
- Model validation: SBV can validate models returned by solvers, which allows
for protection against bugs in SMT solvers and SBV itself. (See the
`validateModel`

parameter.)

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, and CVC5 from Stanford University and the University of Iowa. https://cvc4.github.io/ and https://cvc5.github.io
- Boolector from Johannes Kepler University: https://boolector.github.io and its successor Bitwuzla from Stanford university: https://bitwuzla.github.io
- MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
- Yices from SRI: http://yices.csl.sri.com/
- DReal from CMU: http://dreal.github.io/
- 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.

## Synopsis

- type SBool = SBV Bool
- sTrue :: SBool
- sFalse :: SBool
- sNot :: 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
- oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a
- sAnd :: [SBool] -> SBool
- sOr :: [SBool] -> SBool
- sAny :: (a -> SBool) -> [a] -> SBool
- sAll :: (a -> SBool) -> [a] -> SBool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SWord (n :: Nat) = SBV (WordN n)
- data WordN (n :: Nat)
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInt (n :: Nat) = SBV (IntN n)
- data IntN (n :: Nat)
- type family BVIsNonZero (arg :: Nat) :: Constraint where ...
- type family FromSized (t :: Type) :: Type where ...
- type family ToSized (t :: Type) :: Type where ...
- fromSized :: FromSizedBV a => a -> FromSized a
- toSized :: ToSizedBV a => a -> ToSized a
- type SInteger = SBV Integer
- type family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where ...
- type SFloat = SBV Float
- type SDouble = SBV Double
- type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb)
- data FloatingPoint (eb :: Nat) (sb :: Nat)
- type SFPHalf = SBV FPHalf
- type FPHalf = FloatingPoint 5 11
- type SFPBFloat = SBV FPBFloat
- type FPBFloat = FloatingPoint 8 8
- type SFPSingle = SBV FPSingle
- type FPSingle = FloatingPoint 8 24
- type SFPDouble = SBV FPDouble
- type FPDouble = FloatingPoint 11 53
- type SFPQuad = SBV FPQuad
- type FPQuad = FloatingPoint 15 113
- type SRational = SBV Rational
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSInteger :: SReal -> SInteger
- algRealToRational :: AlgReal -> RationalCV
- data RealPoint a
- = OpenPoint a
- | ClosedPoint a

- realPoint :: RealPoint a -> a
- data RationalCV
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- class SymTuple a
- type STuple a b = SBV (a, b)
- type STuple2 a b = SBV (a, b)
- type STuple3 a b c = SBV (a, b, c)
- type STuple4 a b c d = SBV (a, b, c, d)
- type STuple5 a b c d e = SBV (a, b, c, d, e)
- type STuple6 a b c d e f = SBV (a, b, c, d, e, f)
- type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)
- type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)
- type SMaybe a = SBV (Maybe a)
- type SEither a b = SBV (Either a b)
- data RCSet a
- = RegularSet (Set a)
- | ComplementSet (Set a)

- type SSet a = SBV (RCSet a)
- class SymArray array where
- newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
- newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
- data SArray a b
- lambdaAsArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b
- sBool :: String -> Symbolic SBool
- sBool_ :: Symbolic SBool
- sWord8 :: String -> Symbolic SWord8
- sWord8_ :: Symbolic SWord8
- sWord16 :: String -> Symbolic SWord16
- sWord16_ :: Symbolic SWord16
- sWord32 :: String -> Symbolic SWord32
- sWord32_ :: Symbolic SWord32
- sWord64 :: String -> Symbolic SWord64
- sWord64_ :: Symbolic SWord64
- sWord :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SWord n)
- sWord_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SWord n)
- sInt8 :: String -> Symbolic SInt8
- sInt8_ :: Symbolic SInt8
- sInt16 :: String -> Symbolic SInt16
- sInt16_ :: Symbolic SInt16
- sInt32 :: String -> Symbolic SInt32
- sInt32_ :: Symbolic SInt32
- sInt64 :: String -> Symbolic SInt64
- sInt64_ :: Symbolic SInt64
- sInt :: (KnownNat n, BVIsNonZero n) => String -> Symbolic (SInt n)
- sInt_ :: (KnownNat n, BVIsNonZero n) => Symbolic (SInt n)
- sInteger :: String -> Symbolic SInteger
- sInteger_ :: Symbolic SInteger
- sReal :: String -> Symbolic SReal
- sReal_ :: Symbolic SReal
- sRational :: String -> Symbolic SRational
- sRational_ :: Symbolic SRational
- sFloat :: String -> Symbolic SFloat
- sFloat_ :: Symbolic SFloat
- sDouble :: String -> Symbolic SDouble
- sDouble_ :: Symbolic SDouble
- sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb)
- sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb)
- sFPHalf :: String -> Symbolic SFPHalf
- sFPHalf_ :: Symbolic SFPHalf
- sFPBFloat :: String -> Symbolic SFPBFloat
- sFPBFloat_ :: Symbolic SFPBFloat
- sFPSingle :: String -> Symbolic SFPSingle
- sFPSingle_ :: Symbolic SFPSingle
- sFPDouble :: String -> Symbolic SFPDouble
- sFPDouble_ :: Symbolic SFPDouble
- sFPQuad :: String -> Symbolic SFPQuad
- sFPQuad_ :: Symbolic SFPQuad
- sChar :: String -> Symbolic SChar
- sChar_ :: Symbolic SChar
- sString :: String -> Symbolic SString
- sString_ :: Symbolic SString
- sList :: SymVal a => String -> Symbolic (SList a)
- sList_ :: SymVal a => Symbolic (SList a)
- sTuple :: (SymTuple tup, SymVal tup) => String -> Symbolic (SBV tup)
- sTuple_ :: (SymTuple tup, SymVal tup) => Symbolic (SBV tup)
- sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b)
- sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b)
- sMaybe :: SymVal a => String -> Symbolic (SMaybe a)
- sMaybe_ :: SymVal a => Symbolic (SMaybe a)
- sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a)
- sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a)
- sBools :: [String] -> Symbolic [SBool]
- sWord8s :: [String] -> Symbolic [SWord8]
- sWord16s :: [String] -> Symbolic [SWord16]
- sWord32s :: [String] -> Symbolic [SWord32]
- sWord64s :: [String] -> Symbolic [SWord64]
- sWords :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SWord n]
- sInt8s :: [String] -> Symbolic [SInt8]
- sInt16s :: [String] -> Symbolic [SInt16]
- sInt32s :: [String] -> Symbolic [SInt32]
- sInt64s :: [String] -> Symbolic [SInt64]
- sInts :: (KnownNat n, BVIsNonZero n) => [String] -> Symbolic [SInt n]
- sIntegers :: [String] -> Symbolic [SInteger]
- sReals :: [String] -> Symbolic [SReal]
- sRationals :: [String] -> Symbolic [SRational]
- sFloats :: [String] -> Symbolic [SFloat]
- sDoubles :: [String] -> Symbolic [SDouble]
- sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb]
- sFPHalfs :: [String] -> Symbolic [SFPHalf]
- sFPBFloats :: [String] -> Symbolic [SFPBFloat]
- sFPSingles :: [String] -> Symbolic [SFPSingle]
- sFPDoubles :: [String] -> Symbolic [SFPDouble]
- sFPQuads :: [String] -> Symbolic [SFPQuad]
- sChars :: [String] -> Symbolic [SChar]
- sStrings :: [String] -> Symbolic [SString]
- sLists :: SymVal a => [String] -> Symbolic [SList a]
- sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup]
- sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b]
- sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a]
- sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class Equality a where
- class Mergeable a where
- ite :: Mergeable a => SBool -> a -> a -> a
- iteLazy :: Mergeable a => SBool -> a -> a -> a
- class (SymVal a, Num a, Bits a, Integral a) => SIntegral a
- class SDivisible a where
- sEDivMod :: SInteger -> SInteger -> (SInteger, SInteger)
- sEDiv :: SInteger -> SInteger -> SInteger
- sEMod :: SInteger -> SInteger -> SInteger
- sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
- sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a
- class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where
- sFiniteBitSize :: SBV a -> Int
- lsb :: SBV a -> SBool
- msb :: SBV a -> SBool
- blastBE :: SBV a -> [SBool]
- blastLE :: SBV a -> [SBool]
- fromBitsBE :: [SBool] -> SBV a
- fromBitsLE :: [SBool] -> SBV a
- sTestBit :: SBV a -> Int -> SBool
- sExtractBits :: SBV a -> [Int] -> [SBool]
- sPopCount :: SBV a -> SWord8
- setBitTo :: SBV a -> Int -> SBool -> SBV a
- fullAdder :: SBV a -> SBV a -> (SBool, SBV a)
- fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)
- sCountLeadingZeros :: SBV a -> SWord8
- sCountTrailingZeros :: SBV a -> SWord8

- bvExtract :: forall i j n bv proxy. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j, (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) => proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
- (#) :: (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m)) => SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
- zeroExtend :: forall n m bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)), BVIsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- signExtend :: forall n m bv. (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n), SIntegral (bv (m - n)), BVIsNonZero (m - n)) => SBV (bv n) -> SBV (bv m)
- bvDrop :: forall i n m bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n, ((i + m) - n) <= 0, BVIsNonZero (n - i)) => proxy i -> SBV (bv n) -> SBV (bv m)
- bvTake :: forall i n bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) => proxy i -> SBV (bv n) -> SBV (bv i)
- class ByteConverter a where
- (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
- class (SymVal a, RealFloat a) => IEEEFloating a where
- fpAbs :: SBV a -> SBV a
- fpNeg :: SBV a -> SBV a
- fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
- fpSqrt :: SRoundingMode -> SBV a -> SBV a
- fpRem :: SBV a -> SBV a -> SBV a
- fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a
- fpMin :: SBV a -> SBV a -> SBV a
- fpMax :: SBV a -> SBV a -> SBV a
- fpIsEqualObject :: SBV a -> SBV a -> SBool
- fpIsNormal :: SBV a -> SBool
- fpIsSubnormal :: SBV a -> SBool
- fpIsZero :: SBV a -> SBool
- fpIsInfinite :: SBV a -> SBool
- fpIsNaN :: SBV a -> SBool
- fpIsNegative :: SBV a -> SBool
- fpIsPositive :: SBV a -> SBool
- fpIsNegativeZero :: SBV a -> SBool
- fpIsPositiveZero :: SBV a -> SBool
- fpIsPoint :: SBV a -> SBool

- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymVal a) => SBV a
- sInfinity :: (Floating a, SymVal a) => SBV a
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class SymVal a => IEEEFloatConvertible a where
- fromSFloat :: SRoundingMode -> SFloat -> SBV a
- toSFloat :: SRoundingMode -> SBV a -> SFloat
- fromSDouble :: SRoundingMode -> SDouble -> SBV a
- toSDouble :: SRoundingMode -> SBV a -> SDouble
- fromSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SFloatingPoint eb sb -> SBV a
- toSFloatingPoint :: ValidFloat eb sb => SRoundingMode -> SBV a -> SFloatingPoint eb sb

- sFloatAsSWord32 :: SFloat -> SWord32
- sWord32AsSFloat :: SWord32 -> SFloat
- sDoubleAsSWord64 :: SDouble -> SWord64
- sWord64AsSDouble :: SWord64 -> SDouble
- sFloatingPointAsSWord :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> SWord (eb + sb)
- sWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
- blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
- blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
- blastSFloatingPoint :: forall eb sb. (ValidFloat eb sb, KnownNat (eb + sb), BVIsNonZero (eb + sb)) => SFloatingPoint eb sb -> (SBool, [SBool], [SBool])
- crack :: SBV a -> String
- mkSymbolicEnumeration :: Name -> Q [Dec]
- mkUninterpretedSort :: Name -> Q [Dec]
- class SMTDefinable a where
- smtFunction :: Lambda Symbolic a => String -> a -> a
- uninterpret :: String -> a
- cgUninterpret :: String -> [String] -> a -> a
- sbvDefineValue :: String -> UIKind a -> a
- sym :: String -> a

- type Relation a = (SBV a, SBV a) -> SBool
- isPartialOrder :: SymVal a => String -> Relation a -> SBool
- isLinearOrder :: SymVal a => String -> Relation a -> SBool
- isTreeOrder :: SymVal a => String -> Relation a -> SBool
- isPiecewiseLinearOrder :: SymVal a => String -> Relation a -> SBool
- mkTransitiveClosure :: forall a. SymVal a => String -> Relation a -> Relation a
- type Predicate = Symbolic SBool
- type ConstraintSet = Symbolic ()
- type Provable = ProvableM IO
- type Satisfiable = SatisfiableM IO
- prove :: Provable a => a -> IO ThmResult
- proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
- dprove :: Provable a => a -> IO ThmResult
- dproveWith :: Provable a => SMTConfig -> a -> IO ThmResult
- sat :: Satisfiable a => a -> IO SatResult
- satWith :: Satisfiable a => SMTConfig -> a -> IO SatResult
- dsat :: Satisfiable a => a -> IO SatResult
- dsatWith :: Satisfiable a => SMTConfig -> a -> IO SatResult
- allSat :: Satisfiable a => a -> IO AllSatResult
- allSatWith :: Satisfiable a => SMTConfig -> a -> IO AllSatResult
- optimize :: Satisfiable a => OptimizeStyle -> a -> IO OptimizeResult
- optimizeWith :: Satisfiable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
- isVacuousProof :: Provable a => a -> IO Bool
- isVacuousProofWith :: Provable a => SMTConfig -> a -> IO Bool
- isTheorem :: Provable a => a -> IO Bool
- isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool
- isSatisfiable :: Satisfiable a => a -> IO Bool
- isSatisfiableWith :: Satisfiable a => SMTConfig -> a -> IO Bool
- proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
- proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
- proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
- satWithAny :: Satisfiable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
- satWithAll :: Satisfiable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
- satConcurrentWithAny :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
- satConcurrentWithAll :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
- generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String
- generateSMTBenchmarkProof :: ProvableM m a => a -> m String
- solve :: [SBool] -> Symbolic SBool
- constrain :: (SolverContext m, QuantifiedBool a) => a -> m ()
- softConstrain :: (SolverContext m, QuantifiedBool a) => a -> m ()
- class QuantifiedBool a
- quantifiedBool :: QuantifiedBool a => a -> SBool
- newtype Forall (nm :: Symbol) a = Forall (SBV a)
- newtype Exists (nm :: Symbol) a = Exists (SBV a)
- newtype ExistsUnique (nm :: Symbol) a = ExistsUnique (SBV a)
- newtype ForallN (n :: Nat) (nm :: Symbol) a = ForallN [SBV a]
- newtype ExistsN (n :: Nat) (nm :: Symbol) a = ExistsN [SBV a]
- class QNot a where
- class Skolemize a where
- skolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => a -> SkolemsTo a
- taggedSkolemize :: (Constraint Symbolic (SkolemsTo a), Skolemize a) => String -> a -> SkolemsTo a

- namedConstraint :: (SolverContext m, QuantifiedBool a) => String -> a -> m ()
- constrainWithAttribute :: (SolverContext m, QuantifiedBool a) => [(String, String)] -> a -> m ()
- pbAtMost :: [SBool] -> Int -> SBool
- pbAtLeast :: [SBool] -> Int -> SBool
- pbExactly :: [SBool] -> Int -> SBool
- pbLe :: [(Int, SBool)] -> Int -> SBool
- pbGe :: [(Int, SBool)] -> Int -> SBool
- pbEq :: [(Int, SBool)] -> Int -> SBool
- pbMutexed :: [SBool] -> SBool
- pbStronglyMutexed :: [SBool] -> SBool
- sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a
- isSafe :: SafeResult -> Bool
- class ExtractIO m => SExecutable m a
- sName :: SExecutable IO a => a -> Symbolic ()
- safe :: SExecutable IO a => a -> IO [SafeResult]
- safeWith :: SExecutable IO a => SMTConfig -> a -> IO [SafeResult]
- sbvQuickCheck :: Symbolic SBool -> IO Bool
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)

- data Objective a
- class Metric a where
- type MetricSpace a :: Type
- toMetricSpace :: SBV a -> SBV (MetricSpace a)
- fromMetricSpace :: SBV (MetricSpace a) -> SBV a
- msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
- msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()

- minimize :: Metric a => String -> SBV a -> Symbolic ()
- maximize :: Metric a => String -> SBV a -> Symbolic ()
- assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
- data Penalty
- data ExtCV
- data GeneralizedCV
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- data AllSatResult = AllSatResult {}
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- data SMTResult
- data SMTReasonUnknown
- observe :: SymVal a => String -> SBV a -> SBV a
- observeIf :: SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
- sObserve :: SymVal a => String -> SBV a -> Symbolic ()
- class SatModel a where
- class Modelable a where
- modelExists :: a -> Bool
- getModelAssignment :: SatModel b => a -> Either String (Bool, b)
- getModelDictionary :: a -> Map String CV
- getModelValue :: SymVal b => String -> a -> Maybe b
- getModelUninterpretedValue :: String -> a -> Maybe String
- extractModel :: SatModel b => a -> Maybe b
- getModelObjectives :: a -> Map String GeneralizedCV
- getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
- getModelUIFuns :: a -> Map String (SBVType, Either String ([([CV], CV)], CV))
- getModelUIFunValue :: String -> a -> Maybe (SBVType, Either String ([([CV], CV)], CV))

- displayModels :: SatModel a => ([(Bool, a)] -> [(Bool, a)]) -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
- extractModels :: SatModel a => AllSatResult -> [a]
- getModelDictionaries :: AllSatResult -> [Map String CV]
- getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b]
- getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- crackNum :: Bool
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- allSatTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- dsatPrecision :: Maybe Double
- solver :: SMTSolver
- extraArgs :: [String]
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath

- data Timing
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: String -> String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities

- boolector :: SMTConfig
- bitwuzla :: SMTConfig
- cvc4 :: SMTConfig
- cvc5 :: SMTConfig
- yices :: SMTConfig
- dReal :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- defaultDeltaSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- getAvailableSolvers :: IO [SMTConfig]
- setLogic :: SolverContext m => Logic -> m ()
- data Logic
- setOption :: SolverContext m => SMTOption -> m ()
- setInfo :: SolverContext m => String -> [String] -> m ()
- setTimeOut :: SolverContext m => Integer -> m ()
- data SBVException = SBVException {
- sbvExceptionDescription :: String
- sbvExceptionSent :: Maybe String
- sbvExceptionExpected :: Maybe String
- sbvExceptionReceived :: Maybe String
- sbvExceptionStdOut :: Maybe String
- sbvExceptionStdErr :: Maybe String
- sbvExceptionExitCode :: Maybe ExitCode
- sbvExceptionConfig :: SMTConfig
- sbvExceptionReason :: Maybe [String]
- sbvExceptionHint :: Maybe [String]

- data SBV a
- class HasKind a where
- kindOf :: a -> Kind
- hasSign :: a -> Bool
- intSizeOf :: a -> Int
- isBoolean :: a -> Bool
- isBounded :: a -> Bool
- isReal :: a -> Bool
- isFloat :: a -> Bool
- isDouble :: a -> Bool
- isRational :: a -> Bool
- isFP :: a -> Bool
- isUnbounded :: a -> Bool
- isUserSort :: a -> Bool
- isChar :: a -> Bool
- isString :: a -> Bool
- isList :: a -> Bool
- isSet :: a -> Bool
- isTuple :: a -> Bool
- isMaybe :: a -> Bool
- isEither :: a -> Bool
- showType :: a -> String

- data Kind
- class (HasKind a, Typeable a) => SymVal a
- free :: SymVal a => String -> Symbolic (SBV a)
- free_ :: SymVal a => Symbolic (SBV a)
- mkFreeVars :: SymVal a => Int -> Symbolic [SBV a]
- symbolic :: SymVal a => String -> Symbolic (SBV a)
- symbolics :: SymVal a => [String] -> Symbolic [SBV a]
- literal :: SymVal a => a -> SBV a
- unliteral :: SymVal a => SBV a -> Maybe a
- fromCV :: SymVal a => CV -> a
- isConcrete :: SymVal a => SBV a -> Bool
- isSymbolic :: SymVal a => SBV a -> Bool
- isConcretely :: SymVal a => SBV a -> (a -> Bool) -> Bool
- mkSymVal :: SymVal a => VarContext -> Maybe String -> Symbolic (SBV a)
- class MonadIO m => MonadSymbolic m where
- symbolicEnv :: m State

- type Symbolic = SymbolicT IO
- data SymbolicT m a
- label :: SymVal a => String -> SBV a -> SBV a
- output :: Outputtable a => a -> Symbolic a
- runSMT :: Symbolic a -> IO a
- runSMTWith :: SMTConfig -> Symbolic a -> IO a
- module Data.Bits
- module Data.Word
- module Data.Int
- module Data.Ratio

# 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 `Bool`

s. Clearly we would like these values to be
symbolic (i.e., `SBool`

), thus stopping us from using some native Haskell constructs.
When symbolic versions of operators are needed, they are typically obtained by prepending a dot,
for instance `==`

becomes `.==`

. Care has been taken to make the transition painless. In
particular, any Haskell program you build out of symbolic components is fully concretely
executable within Haskell, without the need for any custom interpreters. (They are truly
Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated
feel of the system, one of the original design goals for SBV.

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

### Boolean values and functions

oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a Source #

Returns 1 if the boolean is `sTrue`

, otherwise 0.

### Logical aggregations

## Bit-vectors

### Unsigned bit-vectors

data WordN (n :: Nat) Source #

An unsigned bit-vector carrying its size info

#### Instances

### Signed bit-vectors

A signed bit-vector carrying its size info

#### Instances

### Converting between fixed-size and arbitrary bitvectors

type family BVIsNonZero (arg :: Nat) :: Constraint where ... Source #

Type family to create the appropriate non-zero constraint

BVIsNonZero 0 = TypeError BVZeroWidth | |

BVIsNonZero _ = () |

type family FromSized (t :: Type) :: Type where ... Source #

Capture the correspondence between sized and fixed-sized BVs

FromSized (WordN 8) = Word8 | |

FromSized (WordN 16) = Word16 | |

FromSized (WordN 32) = Word32 | |

FromSized (WordN 64) = Word64 | |

FromSized (IntN 8) = Int8 | |

FromSized (IntN 16) = Int16 | |

FromSized (IntN 32) = Int32 | |

FromSized (IntN 64) = Int64 | |

FromSized (SWord 8) = SWord8 | |

FromSized (SWord 16) = SWord16 | |

FromSized (SWord 32) = SWord32 | |

FromSized (SWord 64) = SWord64 | |

FromSized (SInt 8) = SInt8 | |

FromSized (SInt 16) = SInt16 | |

FromSized (SInt 32) = SInt32 | |

FromSized (SInt 64) = SInt64 |

type family ToSized (t :: Type) :: Type where ... Source #

Capture the correspondence between fixed-sized and sized BVs

ToSized Word8 = WordN 8 | |

ToSized Word16 = WordN 16 | |

ToSized Word32 = WordN 32 | |

ToSized Word64 = WordN 64 | |

ToSized Int8 = IntN 8 | |

ToSized Int16 = IntN 16 | |

ToSized Int32 = IntN 32 | |

ToSized Int64 = IntN 64 | |

ToSized SWord8 = SWord 8 | |

ToSized SWord16 = SWord 16 | |

ToSized SWord32 = SWord 32 | |

ToSized SWord64 = SWord 64 | |

ToSized SInt8 = SInt 8 | |

ToSized SInt16 = SInt 16 | |

ToSized SInt32 = SInt 32 | |

ToSized SInt64 = SInt 64 |

## 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:
`bvExtract`

,`#`

,`zeroExtend`

,`signExtend`

,`bvDrop`

, and`bvTake`

Usual arithmetic (`+`

, `-`

, `*`

, `sQuotRem`

, `sQuot`

, `sRem`

, `sDivMod`

, `sDiv`

, `sMod`

) and logical operations (`.<`

, `.<=`

, `.>`

, `.>=`

, `.==`

, `./=`

) operations are
supported for `SInteger`

fully, both in programming and verification modes.

## 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 family ValidFloat (eb :: Nat) (sb :: Nat) :: Constraint where ... Source #

A valid float has restrictions on eb/sb values. NB. In the below encoding, I found that CPP is very finicky about substitution of the machine-dependent macros. If you try to put the conditionals in the same line, it fails to substitute for some reason. Hence the awkward spacing. Filed this as a bug report for CPPHS at https://github.com/malcolmwallace/cpphs/issues/25.

ValidFloat (eb :: Nat) (sb :: Nat) = (KnownNat eb, KnownNat sb, If ((((eb `CmpNat` 2) == 'EQ) || ((eb `CmpNat` 2) == 'GT)) && ((((eb `CmpNat` 61) == 'EQ) || ((eb `CmpNat` 61) == 'LT)) && ((((sb `CmpNat` 2) == 'EQ) || ((sb `CmpNat` 2) == 'GT)) && (((sb `CmpNat` 4611686018427387902) == 'EQ) || ((sb `CmpNat` 4611686018427387902) == 'LT))))) (() :: Constraint) (TypeError (InvalidFloat eb sb))) |

type SFloatingPoint (eb :: Nat) (sb :: Nat) = SBV (FloatingPoint eb sb) Source #

A symbolic arbitrary precision floating point value

data FloatingPoint (eb :: Nat) (sb :: Nat) Source #

A floating point value, indexed by its exponent and significand sizes.

An IEEE SP is `FloatingPoint 8 24`

DP is `FloatingPoint 11 53`

etc.

#### Instances

type FPHalf = FloatingPoint 5 11 Source #

Abbreviation for IEEE half precision float, bit width 16 = 5 + 11.

type FPBFloat = FloatingPoint 8 8 Source #

Abbreviation for brain-float precision float, bit width 16 = 8 + 8.

type FPSingle = FloatingPoint 8 24 Source #

Abbreviation for IEEE single precision float, bit width 32 = 8 + 24.

type FPDouble = FloatingPoint 11 53 Source #

Abbreviation for IEEE double precision float, bit width 64 = 11 + 53.

type FPQuad = FloatingPoint 15 113 Source #

Abbreviation for IEEE quadruble precision float, bit width 128 = 15 + 113.

## Rationals

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

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

AlgRational Bool Rational | bool says it's exact (i.e., SMT-solver did not return it with ? at the end.) |

AlgPolyRoot (Integer, AlgRealPoly) (Maybe String) | which root of this polynomial and an approximate decimal representation with given precision, if available |

AlgInterval (RealPoint Rational) (RealPoint Rational) | interval, with low and high bounds |

#### Instances

sRealToSInteger :: SReal -> SInteger Source #

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`

.

Is the endpoint included in the interval?

OpenPoint a | open: i.e., doesn't include the point |

ClosedPoint a | closed: i.e., includes the point |

#### Instances

Show a => Show (RealPoint a) Source # | |

Eq a => Eq (RealPoint a) Source # | |

Ord a => Ord (RealPoint a) Source # | |

Defined in Data.SBV.Core.AlgReals |

data RationalCV Source #

Conversion from internal rationals to Haskell values

RatIrreducible AlgReal | Root of a polynomial, cannot be reduced |

RatExact Rational | An exact rational |

RatApprox Rational | An approximated value |

RatInterval (RealPoint Rational) (RealPoint Rational) | Interval. Can be open/closed on both ends. |

#### Instances

Show RationalCV Source # | |

Defined in Data.SBV.Core.AlgReals showsPrec :: Int -> RationalCV -> ShowS # show :: RationalCV -> String # showList :: [RationalCV] -> ShowS # |

## Characters, Strings and Regular Expressions

Support for characters, strings, and regular expressions (initial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml

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

type SChar = SBV Char Source #

A symbolic character. Note that this is the full unicode character set. see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml for details.

type SString = SBV String Source #

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 but finite length,
and internally processed as one unit as opposed to a fixed-length list of characters.

## Symbolic lists

Support for symbolic lists (initial version contributed by Joel Burget) adds support for sequence support.

See Data.SBV.List for related functions.

type SList a = SBV [a] Source #

A symbolic list of items. Note that a symbolic list is *not* a list of symbolic items,
that is, it is not the case that `SList a = [a]`

, unlike what one might expect following
haskell lists/sequences. An `SList`

is a symbolic value of its own, of possibly arbitrary but finite
length, and internally processed as one unit as opposed to a fixed-length list of items.
Note that lists can be nested, i.e., we do allow lists of lists of ... items.

## Tuples

Tuples can be used as symbolic values. This is useful in combination with lists, for example `SBV [(Integer, String)]`

is a valid type. These types can be arbitrarily nested, eg `SBV [(Integer, [(Char, (Integer, String))])]`

. Instances of upto 8-tuples are provided.

Identify tuple like things. Note that there are no methods, just instances to control type inference

#### Instances

SymTuple () Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c, d) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c, d, e) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c, d, e, f) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c, d, e, f, g) Source # | |

Defined in Data.SBV.Core.Model | |

SymTuple (a, b, c, d, e, f, g, h) Source # | |

Defined in Data.SBV.Core.Model |

## Sum types

## Sets

A `RCSet`

is either a regular set or a set given by its complement from the corresponding universal set.

RegularSet (Set a) | |

ComplementSet (Set a) |

#### Instances

# Arrays of symbolic values

class SymArray array where Source #

Arrays of symbolic values
An `array a b`

is an array indexed by the type

, with elements of type `SBV`

a

.`SBV`

b

If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.

The reason for this class is rather historic. In the past, SBV provided two different kinds of
arrays: an `SArray`

abstraction that mapped directly to SMTLib arrays (which is still available
today), and a functional notion of arrays that used internal caching, called `SFunArray`

. The latter
has been removed as the code turned out to be rather tricky and hard to maintain; so we only
have one instance of this class. But end users can add their own instances, if needed.

NB. `sListArray`

insists on a concrete initializer, because not having one would break
referential transparency. See https://github.com/LeventErkok/sbv/issues/553 for details.

sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b Source #

Create a literal array

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

Read the array element at `a`

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

Update the element at `a`

to be `b`

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

Merge two given arrays on the symbolic condition
Intuitively: `mergeArrays cond a b = if cond then a else b`

.
Merging pushes the if-then-else choice down on to elements

#### Instances

SymArray SArray Source # | |

Defined in Data.SBV.Core.Data newArray_ :: (MonadSymbolic m, HasKind a, HasKind b) => Maybe (SBV b) -> m (SArray a b) Source # newArray :: (MonadSymbolic m, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (SArray a b) Source # sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> SArray a b Source # readArray :: SArray a b -> SBV a -> SBV b Source # writeArray :: SymVal b => SArray a b -> SBV a -> SBV b -> SArray a b Source # mergeArrays :: SymVal b => SBV Bool -> SArray a b -> SArray a b -> SArray a b Source # newArrayInState :: (HasKind a, HasKind b) => Maybe String -> Either (Maybe (SBV b)) String -> State -> IO (SArray a b) Source # |

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

Create a new anonymous array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see `newArray_`

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

Create a named new array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see `newArray`

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

- Maps directly to SMT-lib arrays
- Reading from an uninitialized value is OK. If the default value is given in
`newArray`

, it will be the result. Otherwise, the read yields an uninterpreted constant. - Can check for equality of these arrays
- Cannot be used in code-generation (i.e., compilation to C)
- Cannot quick-check theorems using
`SArray`

values

#### Instances

lambdaAsArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b Source #

Using a lambda as an array

# 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. We provide both the named and anonymous
versions, latter with the underscore suffix.

sRational_ :: Symbolic SRational Source #

Declare an unnamed `SRational`

.

NB. For a version which generalizes over the underlying monad, see `sRational_`

sFloatingPoint :: ValidFloat eb sb => String -> Symbolic (SFloatingPoint eb sb) Source #

Declare a named 'SFloatingPoint eb sb'

NB. For a version which generalizes over the underlying monad, see `sFloatingPoint`

sFloatingPoint_ :: ValidFloat eb sb => Symbolic (SFloatingPoint eb sb) Source #

Declare an unnamed `SFloatingPoint`

`eb`

`sb`

NB. For a version which generalizes over the underlying monad, see `sFloatingPoint_`

sFPSingle_ :: Symbolic SFPSingle Source #

Declare an unnamed `SFPSingle`

NB. For a version which generalizes over the underlying monad, see `sFPSingle_`

sFPDouble_ :: Symbolic SFPDouble Source #

Declare an unnamed `SFPDouble`

NB. For a version which generalizes over the underlying monad, see `sFPDouble_`

sTuple :: (SymTuple tup, SymVal tup) => String -> Symbolic (SBV tup) Source #

Declare a named tuple.

NB. For a version which generalizes over the underlying monad, see `sTuple`

sTuple_ :: (SymTuple tup, SymVal tup) => Symbolic (SBV tup) Source #

Declare an unnamed tuple.

NB. For a version which generalizes over the underlying monad, see `sTuple_`

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

sRationals :: [String] -> Symbolic [SRational] Source #

Declare a list of `SRational`

values.

NB. For a version which generalizes over the underlying monad, see `sRationals`

sFloatingPoints :: ValidFloat eb sb => [String] -> Symbolic [SFloatingPoint eb sb] Source #

Declare a list of `SFloatingPoint`

`eb`

`sb`

's

NB. For a version which generalizes over the underlying monad, see `sFloatingPoints`

sFPBFloats :: [String] -> Symbolic [SFPBFloat] Source #

Declare a list of `SFPQuad`

s

NB. For a version which generalizes over the underlying monad, see `sFPBFloats`

sFPSingles :: [String] -> Symbolic [SFPSingle] Source #

Declare a list of `SFPSingle`

s

NB. For a version which generalizes over the underlying monad, see `sFPSingles`

sFPDoubles :: [String] -> Symbolic [SFPDouble] Source #

Declare a list of `SFPDouble`

s

NB. For a version which generalizes over the underlying monad, see `sFPDoubles`

sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup] Source #

Declare a list of tuples.

NB. For a version which generalizes over the underlying monad, see `sTuples`

# Symbolic Equality and Comparisons

Symbolic equality provides the notion of what it means to be equal, similar to Haskell's `Eq`

class, except allowing comparison of
symbolic values. The methods are `.==`

and `./=`

, returning `SBool`

results. We also provide a notion of strong equality (`.===`

and `./==`

),
which is useful for floating-point value comparisons as it deals more uniformly with `NaN`

and positive/negative zeros. Additionally, we
provide `distinct`

that can be used to assert all elements of a list are different from each other, and `distinctExcept`

which is similar
to `distinct`

but allows for certain values to be considered different. These latter two functions are useful in modeling a variety of
puzzles and cardinality constraints:

`>>>`

Q.E.D.`prove $ \a -> distinctExcept [a, a] [0::SInteger] .<=> a .== 0`

`>>>`

Q.E.D.`prove $ \a b -> distinctExcept [a, b] [0::SWord8] .<=> (a .== b .=> a .== 0)`

`>>>`

Q.E.D.`prove $ \a b c d -> distinctExcept [a, b, c, d] [] .== distinct [a, b, c, (d::SInteger)]`

class EqSymbolic a where Source #

Symbolic Equality. Note that we can't use Haskell's `Eq`

class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.

Minimal complete definition: None, if the type is instance of `Generic`

. Otherwise `(.==)`

.

Nothing

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

Symbolic equality.

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

Symbolic inequality.

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

Strong equality. On floats (`SFloat`

/`SDouble`

), strong equality is object equality; that
is `NaN == NaN`

holds, but `+0 == -0`

doesn't. On other types, (.===) is simply (.==).
Note that (.==) is the *right* notion of equality for floats per IEEE754 specs, since by
definition `+0 == -0`

and `NaN`

equals no other value including itself. But occasionally
we want to be stronger and state `NaN`

equals `NaN`

and `+0`

and `-0`

are different from
each other. In a context where your type is concrete, simply use `fpIsEqualObject`

. But in
a polymorphic context, use the strong equality instead.

NB. If you do not care about or work with floats, simply use (.==) and (./=).

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

Negation of strong equality. Equaivalent to negation of (.===) on all types.

distinct :: [a] -> SBool Source #

Returns (symbolic) `sTrue`

if all the elements of the given list are different.

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

Returns (symbolic) `sTrue`

if all the elements of the given list are different. The second
list contains exceptions, i.e., if an element belongs to that set, it will be considered
distinct regardless of repetition.

allEqual :: [a] -> SBool Source #

Returns (symbolic) `sTrue`

if all the elements of the given list are the same.

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

Symbolic membership test.

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

Symbolic negated membership test.

#### Instances

EqSymbolic RegExp Source # | Regular expressions can be compared for equality. Note that we diverge here from the equality in the concrete sense; i.e., the Eq instance does not match the symbolic case. This is a bit unfortunate, but unavoidable with the current design of how we "distinguish" operators. Hopefully shouldn't be a big deal, though one should be careful. |

Defined in Data.SBV.Core.Model (.==) :: RegExp -> RegExp -> SBool Source # (./=) :: RegExp -> RegExp -> SBool Source # (.===) :: RegExp -> RegExp -> SBool Source # (./==) :: RegExp -> RegExp -> SBool Source # distinct :: [RegExp] -> SBool Source # distinctExcept :: [RegExp] -> [RegExp] -> SBool Source # allEqual :: [RegExp] -> SBool Source # | |

EqSymbolic Bool Source # | |

Defined in Data.SBV.Core.Model (.==) :: Bool -> Bool -> SBool Source # (./=) :: Bool -> Bool -> SBool Source # (.===) :: Bool -> Bool -> SBool Source # (./==) :: Bool -> Bool -> SBool Source # distinct :: [Bool] -> SBool Source # distinctExcept :: [Bool] -> [Bool] -> SBool Source # allEqual :: [Bool] -> SBool Source # | |

EqSymbolic (SBV a) Source # | |

Defined in Data.SBV.Core.Model (.==) :: SBV a -> SBV a -> SBool Source # (./=) :: SBV a -> SBV a -> SBool Source # (.===) :: SBV a -> SBV a -> SBool Source # (./==) :: SBV a -> SBV a -> SBool Source # distinct :: [SBV a] -> SBool Source # distinctExcept :: [SBV a] -> [SBV a] -> SBool Source # allEqual :: [SBV a] -> SBool Source # | |

EqSymbolic a => EqSymbolic (S a) Source # | Symbolic equality for |

Defined in Documentation.SBV.Examples.ProofTools.BMC (.==) :: S a -> S a -> SBool Source # (./=) :: S a -> S a -> SBool Source # (.===) :: S a -> S a -> SBool Source # (./==) :: S a -> S a -> SBool Source # distinct :: [S a] -> SBool Source # distinctExcept :: [S a] -> [S a] -> SBool Source # allEqual :: [S a] -> SBool Source # | |

EqSymbolic a => EqSymbolic (Maybe a) Source # | |

Defined in Data.SBV.Core.Model (.==) :: Maybe a -> Maybe a -> SBool Source # (./=) :: Maybe a -> Maybe a -> SBool Source # (.===) :: Maybe a -> Maybe a -> SBool Source # (./==) :: Maybe a -> Maybe a -> SBool Source # distinct :: [Maybe a] -> SBool Source # distinctExcept :: [Maybe a] -> [Maybe a] -> SBool Source # allEqual :: [Maybe a] -> SBool Source # | |

EqSymbolic a => EqSymbolic [a] Source # | |

Defined in Data.SBV.Core.Model (.==) :: [a] -> [a] -> SBool Source # (./=) :: [a] -> [a] -> SBool Source # (.===) :: [a] -> [a] -> SBool Source # (./==) :: [a] -> [a] -> SBool Source # distinct :: [[a]] -> SBool Source # distinctExcept :: [[a]] -> [[a]] -> SBool Source # allEqual :: [[a]] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # | |

Defined in Data.SBV.Core.Model (.==) :: Either a b -> Either a b -> SBool Source # (./=) :: Either a b -> Either a b -> SBool Source # (.===) :: Either a b -> Either a b -> SBool Source # (./==) :: Either a b -> Either a b -> SBool Source # distinct :: [Either a b] -> SBool Source # distinctExcept :: [Either a b] -> [Either a b] -> SBool Source # allEqual :: [Either a b] -> SBool Source # | |

EqSymbolic (SArray a b) Source # | |

Defined in Data.SBV.Core.Model (.==) :: SArray a b -> SArray a b -> SBool Source # (./=) :: SArray a b -> SArray a b -> SBool Source # (.===) :: SArray a b -> SArray a b -> SBool Source # (./==) :: SArray a b -> SArray a b -> SBool Source # distinct :: [SArray a b] -> SBool Source # distinctExcept :: [SArray a b] -> [SArray a b] -> SBool Source # allEqual :: [SArray a b] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b) -> (a, b) -> SBool Source # (./=) :: (a, b) -> (a, b) -> SBool Source # (.===) :: (a, b) -> (a, b) -> SBool Source # (./==) :: (a, b) -> (a, b) -> SBool Source # distinct :: [(a, b)] -> SBool Source # distinctExcept :: [(a, b)] -> [(a, b)] -> SBool Source # allEqual :: [(a, b)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c) -> (a, b, c) -> SBool Source # (./=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.===) :: (a, b, c) -> (a, b, c) -> SBool Source # (./==) :: (a, b, c) -> (a, b, c) -> SBool Source # distinct :: [(a, b, c)] -> SBool Source # distinctExcept :: [(a, b, c)] -> [(a, b, c)] -> SBool Source # allEqual :: [(a, b, c)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.===) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # distinct :: [(a, b, c, d)] -> SBool Source # distinctExcept :: [(a, b, c, d)] -> [(a, b, c, d)] -> SBool Source # allEqual :: [(a, b, c, d)] -> SBool Source # sElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # sNotElem :: (a, b, c, d) -> [(a, b, c, d)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.===) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # distinct :: [(a, b, c, d, e)] -> SBool Source # distinctExcept :: [(a, b, c, d, e)] -> [(a, b, c, d, e)] -> SBool Source # allEqual :: [(a, b, c, d, e)] -> SBool Source # sElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # sNotElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # | |

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

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.===) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # distinct :: [(a, b, c, d, e, f)] -> SBool Source # distinctExcept :: [(a, b, c, d, e, f)] -> [(a, b, c, d, e, f)] -> SBool Source # allEqual :: [(a, b, c, d, e, f)] -> SBool Source # sElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # sNotElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # | |

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

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.===) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # distinct :: [(a, b, c, d, e, f, g)] -> SBool Source # distinctExcept :: [(a, b, c, d, e, f, g)] -> [(a, b, c, d, e, f, g)] -> SBool Source # allEqual :: [(a, b, c, d, e, f, g)] -> SBool Source # sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source # sNotElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source # |

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

Symbolic Comparisons. Similar to `Eq`

, we cannot implement Haskell's `Ord`

class
since there is no way to return an `Ordering`

value from a symbolic comparison.
Furthermore, `OrdSymbolic`

requires `Mergeable`

to implement if-then-else, for the
benefit of implementing symbolic versions of `max`

and `min`

functions.

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

Symbolic less than.

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

Symbolic less than or equal to.

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

Symbolic greater than.

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

Symbolic greater than or equal to.

Symbolic minimum.

Symbolic maximum.

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

Is the value within the allowed *inclusive* range?

#### Instances

(Ord a, SymVal a) => OrdSymbolic (SBV a) Source # | If comparison is over something SMTLib can handle, just translate it. Otherwise desugar. |

Defined in Data.SBV.Core.Model | |

OrdSymbolic a => OrdSymbolic (Maybe a) Source # | |

Defined in Data.SBV.Core.Model | |

OrdSymbolic a => OrdSymbolic [a] Source # | |

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # | |

Defined in Data.SBV.Core.Model (.<) :: Either a b -> Either a b -> SBool Source # (.<=) :: Either a b -> Either a b -> SBool Source # (.>) :: Either a b -> Either a b -> SBool Source # (.>=) :: Either a b -> Either a b -> SBool Source # smin :: Either a b -> Either a b -> Either a b Source # smax :: Either a b -> Either a b -> Either a b Source # inRange :: Either a b -> (Either a b, Either a b) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c) -> (a, b, c) -> SBool Source # (.<=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>=) :: (a, b, c) -> (a, b, c) -> SBool Source # smin :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # smax :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # inRange :: (a, b, c) -> ((a, b, c), (a, b, c)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # inRange :: (a, b, c, d) -> ((a, b, c, d), (a, b, c, d)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # inRange :: (a, b, c, d, e) -> ((a, b, c, d, e), (a, b, c, d, e)) -> SBool Source # | |

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

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # smin :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # smax :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # inRange :: (a, b, c, d, e, f) -> ((a, b, c, d, e, f), (a, b, c, d, e, f)) -> SBool Source # | |

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

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool Source # |

class Equality a where Source #

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

#### Instances

# Conditionals: Mergeable values

class Mergeable a where Source #

Symbolic conditionals are modeled by the `Mergeable`

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

A `Mergeable`

instance may be automatically derived for a custom data-type
with a single constructor where the type of each field is an instance of
`Mergeable`

, such as a record of symbolic values. Users only need to add
`Generic`

and `Mergeable`

to the `deriving`

clause for the data-type. See
`Status`

for an example and an
illustration of what the instance would look like if written by hand.

The function `select`

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

function.

Minimal complete definition: None, if the type is instance of `Generic`

. Otherwise
`symbolicMerge`

. Note that most types subject to merging are likely to be
trivial instances of `Generic`

.

Nothing

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

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

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

Total indexing operation. `select xs default index`

is intuitively
the same as `xs !! index`

, except it evaluates to `default`

if `index`

underflows/overflows.

#### Instances

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

If-then-else. This is by definition `symbolicMerge`

with both
branches forced. This is typically the desired behavior, but also
see `iteLazy`

should you need more laziness.

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

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

# Symbolic integral numbers

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

Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic type-signatures that work for all
symbolic numbers, such as `SWord8`

, `SInt8`

etc. For instance, we can write a generic
list-minimum function as follows:

mm :: SIntegral a => [SBV a] -> SBV a mm = foldr1 (a b -> ite (a .<= b) a b)

It is similar to the standard `Integral`

class, except ranging over symbolic instances.

#### Instances

SIntegral Int16 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int32 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int64 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int8 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word16 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word32 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word64 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word8 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Integer Source # | |

Defined in Data.SBV.Core.Model | |

(KnownNat n, BVIsNonZero n) => SIntegral (IntN n) Source # | |

Defined in Data.SBV.Core.Sized | |

(KnownNat n, BVIsNonZero n) => SIntegral (WordN n) Source # | |

Defined in Data.SBV.Core.Sized |

# Division and Modulus

class SDivisible a where Source #

The `SDivisible`

class captures the essence of division.
Unfortunately we cannot use Haskell's `Integral`

class since the `Real`

and `Enum`

superclasses are not implementable for symbolic bit-vectors.
However, `quotRem`

and `divMod`

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.

### C code generation of division operations

In the case of division or modulo of a minimal signed value (e.g. `-128`

for
`SInt8`

) by `-1`

, SMTLIB and Haskell agree on what the result should be.
Unfortunately the result in C code depends on CPU architecture and compiler
settings, as this is undefined behaviour in C. **SBV does not guarantee**
what will happen in generated C code in this corner case.

#### Instances

### Euclidian division and modulus

Euclidian division and modulus for integers differ from regular division modulus when
the divisor is negative. It satisfies the following desirable property: For any `m`

, `n`

, we have:

Given`m`

,`n`

, s.t., n /= 0 Let (q, r) = m`sEDivMod`

n Then: m = n * q + r and 0 <= r <= |n| - 1

That is, the modulus is always positive. There's no standard Haskell function that performs this operation. The main reason to prefer this function is that SMT solvers can deal with them better. Compare:

`>>>`

(-2 :: SInteger,-1 :: SInteger)`sDivMod @SInteger 3 (-2)`

`>>>`

(-1 :: SInteger,1 :: SInteger)`sEDivMod 3 (-2)`

`>>>`

Q.E.D.`prove $ \x y -> y .> 0 .=> x `sDivMod` y .== x `sEDivMod` y`

# Bit-vector operations

## Conversions

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

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.

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

Generalization of `shiftR`

, when the shift-amount is symbolic. Since Haskell's
`shiftR`

only takes an `Int`

as the shift amount, it cannot be used when we have
a symbolic amount to shift with.

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.

sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #

An implementation of rotate-left, using a barrel shifter like design. Only works when both
arguments are finite bitvectors, and furthermore when the second argument is unsigned.
The first condition is enforced by the type, but the second is dynamically checked.
We provide this implementation as an alternative to `sRotateLeft`

since SMTLib logic
does not support variable argument rotates (as opposed to shifts), and thus this
implementation can produce better code for verification compared to `sRotateLeft`

.

`>>>`

Q.E.D.`prove $ \x y -> (x `sBarrelRotateLeft` y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)`

sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #

An implementation of rotate-right, using a barrel shifter like design. See comments
for `sBarrelRotateLeft`

for details.

`>>>`

Q.E.D.`prove $ \x y -> (x `sBarrelRotateRight` y) `sBarrelRotateLeft` (y :: SWord32) .== (x :: SWord64)`

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

Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent
to `sShiftRight`

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

## Finite bit-vector operations

class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where Source #

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`

.

sFiniteBitSize :: SBV a -> Int Source #

Bit size.

lsb :: SBV a -> SBool Source #

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

msb :: SBV a -> SBool Source #

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

blastBE :: SBV a -> [SBool] Source #

Big-endian blasting of a word into its bits.

blastLE :: SBV a -> [SBool] Source #

Little-endian blasting of a word into its bits.

fromBitsBE :: [SBool] -> SBV a Source #

Reconstruct from given bits, given in little-endian.

fromBitsLE :: [SBool] -> SBV a Source #

Reconstruct from given bits, given in little-endian.

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

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

Variant of `sTestBit`

, where we want to extract multiple bit positions.

sPopCount :: SBV a -> SWord8 Source #

Variant of `popCount`

, returning a symbolic value.

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

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

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

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

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

sCountLeadingZeros :: SBV a -> SWord8 Source #

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

sCountTrailingZeros :: SBV a -> SWord8 Source #

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