Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
 Symbolic types
 Arrays of symbolic values
 Creating symbolic values
 Symbolic Equality and Comparisons
 Conditionals: Mergeable values
 Symbolic integral numbers
 Division and Modulus
 Bitvector operations
 IEEEfloating point numbers
 Enumerations
 Uninterpreted sorts, axioms, constants, and functions
 Properties, proofs, and satisfiability
 Constraints
 Checking safety
 Quickchecking
 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.
>>>
prove $ \x > x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.
>>>
prove $ \x > x `shiftL` 2 .== 2 * (x :: SWord8)
Falsifiable. Counterexample: s0 = 64 :: Word8
The function prove
has the following type:
prove
::Provable
a => a >IO
ThmResult
The class Provable
comes with instances for nary 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 bitsize.SInt
n
: Generalized symbolic ints of arbitrary bitsize.SInteger
: Unbounded signed integers.SReal
: Algebraicreal numbers.SFloat
: IEEE754 singleprecision floating point values.SDouble
: IEEE754 doubleprecision floating point values.SRational
: Rationals. (Ratio of two symbolic integers.)SFloatingPoint
: Generalized IEEE754 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 8tuples, can be nested)SEither
: Symbolic sumsSMaybe
: 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 SMTLib axioms.
 Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
 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)  quickchecked
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 thirdparty SMT solvers via the standard SMTLib interface: http://smtlib.cs.uiowa.edu/
The SBV library is designed to work with any SMTLib compliant SMTsolver. Currently, we support the following SMTSolvers outofthe 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: http://fmv.jku.at/boolector/ and its successor Bitwuzla from Stanford university: https://github.com/bitwuzla/bitwuzla
 MathSAT from Fondazione Bruno Kessler and DISIUniversity 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
 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
 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 Uninterpreted a where
 uninterpret :: String > a
 cgUninterpret :: String > [String] > a > a
 sbvUninterpret :: Maybe ([String], a) > String > a
 sym :: String > a
 addAxiom :: SolverContext m => String > [String] > m ()
 type Predicate = Symbolic SBool
 type Goal = Symbolic ()
 type Provable = MProvable IO
 forAll_ :: Provable a => a > Symbolic SBool
 forAll :: Provable a => [String] > a > Symbolic SBool
 forSome_ :: Provable a => a > Symbolic SBool
 forSome :: Provable a => [String] > a > Symbolic SBool
 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 :: Provable a => a > IO SatResult
 satWith :: Provable a => SMTConfig > a > IO SatResult
 dsat :: Provable a => a > IO SatResult
 dsatWith :: Provable a => SMTConfig > a > IO SatResult
 allSat :: Provable a => a > IO AllSatResult
 allSatWith :: Provable a => SMTConfig > a > IO AllSatResult
 optimize :: Provable a => OptimizeStyle > a > IO OptimizeResult
 optimizeWith :: Provable a => SMTConfig > OptimizeStyle > a > IO OptimizeResult
 isVacuous :: Provable a => a > IO Bool
 isVacuousWith :: Provable a => SMTConfig > a > IO Bool
 isTheorem :: Provable a => a > IO Bool
 isTheoremWith :: Provable a => SMTConfig > a > IO Bool
 isSatisfiable :: Provable a => a > IO Bool
 isSatisfiableWith :: Provable a => SMTConfig > a > IO Bool
 proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, ThmResult)]
 proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, ThmResult)
 satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, SatResult)]
 proveConcurrentWithAny :: Provable a => SMTConfig > [Query b] > a > IO (Solver, NominalDiffTime, ThmResult)
 proveConcurrentWithAll :: Provable a => SMTConfig > [Query b] > a > IO [(Solver, NominalDiffTime, ThmResult)]
 satConcurrentWithAny :: Provable a => SMTConfig > [Query b] > a > IO (Solver, NominalDiffTime, SatResult)
 satConcurrentWithAll :: Provable a => SMTConfig > [Query b] > a > IO [(Solver, NominalDiffTime, SatResult)]
 satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, SatResult)
 generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool > a > m String
 solve :: [SBool] > Symbolic SBool
 constrain :: SolverContext m => SBool > m ()
 softConstrain :: SolverContext m => SBool > m ()
 namedConstraint :: SolverContext m => String > SBool > m ()
 constrainWithAttribute :: SolverContext m => [(String, String)] > SBool > 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 ()
 sName :: SExecutable IO a => [String] > 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, ([([CV], CV)], CV))
 getModelUIFunValue :: String > a > Maybe (SBVType, ([([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
 satTrackUFs :: Bool
 isNonModelVar :: String > Bool
 validateModel :: Bool
 optimizeValidateConstraints :: Bool
 transcript :: Maybe FilePath
 smtLibVersion :: SMTLibVersion
 dsatPrecision :: Maybe Double
 solver :: SMTSolver
 extraArgs :: [String]
 allowQuantifiedQueries :: Bool
 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
 forall :: SymVal a => String > Symbolic (SBV a)
 forall_ :: SymVal a => Symbolic (SBV a)
 mkForallVars :: SymVal a => Int > Symbolic [SBV a]
 exists :: SymVal a => String > Symbolic (SBV a)
 exists_ :: SymVal a => Symbolic (SBV a)
 mkExistVars :: SymVal a => Int > Symbolic [SBV 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, ifthenelse
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 SMTsolvers, 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 typedAPI.
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
Bitvectors
Unsigned bitvectors
data WordN (n :: Nat) Source #
An unsigned bitvector carrying its size info
Instances
Signed bitvectors
A signed bitvector carrying its size info
Instances
Converting between fixedsize and arbitrary bitvectors
type family BVIsNonZero (arg :: Nat) :: Constraint where ... Source #
Type family to create the appropriate nonzero constraint
BVIsNonZero 0 = TypeError BVZeroWidth  
BVIsNonZero _ = () 
type family FromSized (t :: Type) :: Type where ... Source #
Capture the correspondence between sized and fixedsized 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 fixedsized 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 bitvector 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 SMTLib.
Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixedsize
bitvectors. 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
, andbvTake
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 IEEE754 standard; and correspond to Haskell's
Float
and Double
types. For SMT support with floatingpoint numbers, see the paper
by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smtfpa.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 machinedependent 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 brainfloat 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 singlevariable 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/theoriesReals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve nonlinear equations involving realvariables. (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 rootsofpolynomials are represented implicitly by their defining equation
AlgRational Bool Rational  bool says it's exact (i.e., SMTsolver 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
Eq a => Eq (RealPoint a) Source #  
Ord a => Ord (RealPoint a) Source #  
Defined in Data.SBV.Core.AlgReals  
Show a => Show (RealPoint a) Source #  
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/theoriesUnicodeStrings.shtml and here: http://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 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/theoriesUnicodeStrings.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 fixedlength list of characters.
Symbolic lists
Support for symbolic lists (initial version contributed by Joel Burget) adds support for sequence support, described here: http://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.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 fixedlength 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 8tuples 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 ifthenelse 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 > Maybe (SBV b) > 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 SMTarrays: http://smtlib.cs.uiowa.edu/theoriesArraysEx.shtml
 Maps directly to SMTlib 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 codegeneration (i.e., compilation to C)
 Cannot quickcheck theorems using
SArray
values
Instances
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
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.
(.==) :: 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.
>>>
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)]
Q.E.D.
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 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 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 (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 (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 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 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 (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 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 ifthenelse, 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
OrdSymbolic a => OrdSymbolic [a] Source #  
OrdSymbolic a => OrdSymbolic (Maybe a) Source #  
Defined in Data.SBV.Core.Model  
(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 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 bitprecise 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 ifthenelse call with a symbolic test. SBV
provides all basic types as instances of this class, so users only need
to declare instances for custom datatypes of their programs as needed.
A Mergeable
instance may be automatically derived for a custom datatype
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 datatype. See
Status
for an example and an
illustration of what the instance would look like if written by hand.
The function select
is a totalindexing function out of a list of choices
with a default value, simulating array/list indexing. It's an nway 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 thenandelse 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 #
Ifthenelse. 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 typesignatures that work for all
symbolic numbers, such as SWord8
, SInt8
etc. For instance, we can write a generic
listminimum 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 Source #  
Defined in Data.SBV.Core.Model  
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 Integer Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word8 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  
(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 bitvectors.
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:
xsQuotRem
0 = (0, x) xsDivMod
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
Bitvector 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 integralsymbolic 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 typesignatures 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 shiftamount 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 rotateleft, 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
.
>>>
prove $ \x y > (x `sBarrelRotateLeft` y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)
Q.E.D.
sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a > SBV b > SBV a Source #
An implementation of rotateright, using a barrel shifter like design. See comments
for sBarrelRotateLeft
for details.
>>>
prove $ \x y > (x `sBarrelRotateRight` y) `sBarrelRotateLeft` (y :: SWord32) .== (x :: SWord64)
Q.E.D.
sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a > SBV b > SBV a Source #
Arithmetic shiftright 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 signbit, 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 bitvector operations
class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where Source #
Finite bitlength 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 #
Bigendian blasting of a word into its bits.
blastLE :: SBV a > [SBool] Source #
Littleendian blasting of a word into its bits.
fromBitsBE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
fromBitsLE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
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 carryout from the addition. Only for unsigned quantities.
fullMultiplier :: SBV a > SBV a > (SBV a, SBV a) Source #
Full multiplier, returns both high and loworder bits. Only for unsigned quantities.
sCountLeadingZeros :: SBV a > SWord8 Source #
Count leading zeros in a word, bigendian interpretation.
sCountTrailingZeros :: SBV a > SWord8 Source #
Count trailing zeros in a word, bigendian interpretation.
Instances
Splitting, joining, and extending bitvectors
:: 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)  Input bit vector of size 
> SBV (bv ((i  j) + 1))  Output is of size 
Extract a portion of bits to form a smaller bitvector.
>>>
prove $ \x > bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
Q.E.D.
:: (KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m, BVIsNonZero m, SymVal (bv m))  
=> SBV (bv n)  First input, of size 
> SBV (bv m)  Second input, of size 
> SBV (bv (n + m))  Concatenation, of size 
Join two bitvectors.
>>>
prove $ \x y > x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71))
Q.E.D.
:: 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)  Input, of size 
> SBV (bv m)  Output, of size 
Zero extend a bitvector.
>>>
prove $ \x > bvExtract (Proxy @20) (Proxy @12) (zeroExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.
:: 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)  Input, of size 
> SBV (bv m)  Output, of size 
Sign extend a bitvector.
>>>
prove $ \x > sNot (msb x) .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== 0
Q.E.D.>>>
prove $ \x > msb x .=> bvExtract (Proxy @20) (Proxy @12) (signExtend (x :: SInt 12) :: SInt 21) .== complement 0
Q.E.D.
:: 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)  Input, of size 
> SBV (bv m)  Output, of size 
Drop bits from the top of a bitvector.
>>>
prove $ \x > bvDrop (Proxy @0) (x :: SWord 43) .== x
Q.E.D.>>>
prove $ \x > bvDrop (Proxy @20) (x :: SWord 21) .== ite (lsb x) 1 0
Q.E.D.
:: forall i n bv proxy. (KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n)  
=> proxy i 

> SBV (bv n)  Input, of size 
> SBV (bv i)  Output, of size 
Take bits from the top of a bitvector.
>>>
prove $ \x > bvTake (Proxy @13) (x :: SWord 13) .== x
Q.E.D.>>>
prove $ \x > bvTake (Proxy @1) (x :: SWord 13) .== ite (msb x) 1 0
Q.E.D.>>>
prove $ \x > bvTake (Proxy @4) x # bvDrop (Proxy @4) x .== (x :: SWord 23)
Q.E.D.
class ByteConverter a where Source #
A helper class to convert sized bitvectors to/from bytes.
toBytes :: a > [SWord 8] Source #
Convert to a sequence of bytes
>>>
prove $ \a b c d > toBytes ((fromBytes [a, b, c, d]) :: SWord 32) .== [a, b, c, d]
Q.E.D.
fromBytes :: [SWord 8] > a Source #
Convert from a sequence of bytes
>>>
prove $ \r > fromBytes (toBytes r) .== (r :: SWord 64)
Q.E.D.
Instances
ByteConverter (SWord 8) Source # 

ByteConverter (SWord 16) Source # 

ByteConverter (SWord 32) Source # 

ByteConverter (SWord 64) Source # 

ByteConverter (SWord 128) Source # 

ByteConverter (SWord 256) Source # 

ByteConverter (SWord 512) Source # 
