Copyright  (c) Levent Erkok 

License  BSD3 
Maintainer  erkokl@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
 Programming with symbolic values
 Symbolic types
 Creating a symbolic variable
 Creating a list of symbolic variables
 Operations on symbolic values
 Polynomial arithmetic and CRCs
 Conditionals: Mergeable values
 Conditional symbolic simulation
 Symbolic equality
 Symbolic ordering
 Symbolic integral numbers
 Division
 The Boolean class
 Prettyprinting and reading numbers in Hex & Binary
 Uninterpreted sorts, constants, and functions
 Enumerations
 Properties, proofs, and satisfiability
 Checking safety
 Proving properties using multiple solvers
 Optimization
 Computing expected values
 Model extraction
 SMT Interface: Configurations and solvers
 Symbolic computations
 Getting SMTLib output (for offline analysis)
 Test case generation
 Code generation from symbolic programs
 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 $ forAll ["x"] $ \x > x `shiftL` 2 .== (x :: SWord8)
Falsifiable. Counterexample: x = 51 :: SWord8
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 signed and unsigned
bitvectors. Functions for checking satisfiability (sat
and allSat
) are also
provided.
In particular, the sbv library introduces the types:
SBool
: Symbolic Booleans (bits).SWord8
,SWord16
,SWord32
,SWord64
: Symbolic Words (unsigned).SInt8
,SInt16
,SInt32
,SInt64
: Symbolic Ints (signed).SInteger
: Unbounded signed integers.SReal
: Algebraicreal numbersSFloat
: IEEE754 singleprecision floating point valuesSDouble
: IEEE754 doubleprecision floating point valuesSArray
,SFunArray
: Flat arrays of symbolic values. Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
 Uninterpreted constants and functions over symbolic values, with user defined SMTLib axioms.
 Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
The user can construct ordinary Haskell programs using these types, which behave
very similar to their concrete counterparts. In particular these types belong to the
standard classes Num
, Bits
, custom versions of Eq
(EqSymbolic
)
and Ord
(OrdSymbolic
), along with several other custom classes for simplifying
programming with symbolic values. The framework takes full advantage of Haskell's type
inference to avoid many common mistakes.
Furthermore, predicates (i.e., functions that return SBool
) built out of
these types can also be:
 proven correct via an external SMT solver (the
prove
function)  checked for satisfiability (the
sat
,allSat
functions)  used in synthesis (the
sat
function with existentials)  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, lazily.
The sbv library uses thirdparty SMT solvers via the standard SMTLib interface: http://goedel.cs.uiowa.edu/smtlib/.
The SBV library is designed to work with any SMTLib compliant SMTsolver. Currently, we support the following SMTSolvers outofthe box:
 Z3 from Microsoft: http://research.microsoft.com/enus/um/redmond/projects/z3/
 Yices from SRI: http://yices.csl.sri.com/
 CVC4 from New York University and University of Iowa: http://cvc4.cs.nyu.edu/
 Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
 MathSAT from Fondazione Bruno Kessler and DISIUniversity of Trento: http://mathsat.fbk.eu/
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.
 type SBool = SBV Bool
 type SWord8 = SBV Word8
 type SWord16 = SBV Word16
 type SWord32 = SBV Word32
 type SWord64 = SBV Word64
 type SInt8 = SBV Int8
 type SInt16 = SBV Int16
 type SInt32 = SBV Int32
 type SInt64 = SBV Int64
 type SInteger = SBV Integer
 type SFloat = SBV Float
 type SDouble = SBV Double
 data RoundingMode
 nan :: Floating a => a
 infinity :: Floating a => a
 sNaN :: (Floating a, SymWord a) => SBV a
 sInfinity :: (Floating a, SymWord a) => SBV a
 fusedMA :: (SymWord a, Floating a) => SBV a > SBV a > SBV a > SBV a
 isSNaN :: (Floating a, SymWord a) => SBV a > SBool
 isFPPoint :: (Floating a, SymWord a) => SBV a > SBool
 type SReal = SBV AlgReal
 data AlgReal
 toSReal :: SInteger > SReal
 sBool :: String > Symbolic SBool
 sWord8 :: String > Symbolic SWord8
 sWord16 :: String > Symbolic SWord16
 sWord32 :: String > Symbolic SWord32
 sWord64 :: String > Symbolic SWord64
 sInt8 :: String > Symbolic SInt8
 sInt16 :: String > Symbolic SInt16
 sInt32 :: String > Symbolic SInt32
 sInt64 :: String > Symbolic SInt64
 sInteger :: String > Symbolic SInteger
 sReal :: String > Symbolic SReal
 sFloat :: String > Symbolic SFloat
 sDouble :: String > Symbolic SDouble
 sBools :: [String] > Symbolic [SBool]
 sWord8s :: [String] > Symbolic [SWord8]
 sWord16s :: [String] > Symbolic [SWord16]
 sWord32s :: [String] > Symbolic [SWord32]
 sWord64s :: [String] > Symbolic [SWord64]
 sInt8s :: [String] > Symbolic [SInt8]
 sInt16s :: [String] > Symbolic [SInt16]
 sInt32s :: [String] > Symbolic [SInt32]
 sInt64s :: [String] > Symbolic [SInt64]
 sIntegers :: [String] > Symbolic [SInteger]
 sReals :: [String] > Symbolic [SReal]
 sFloats :: [String] > Symbolic [SFloat]
 sDoubles :: [String] > Symbolic [SDouble]
 data SBV a
 class SymArray array where
 newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) > Symbolic (array a b)
 newArray :: (HasKind a, HasKind b) => String > Maybe (SBV b) > Symbolic (array a b)
 readArray :: array a b > SBV a > SBV b
 resetArray :: SymWord b => array a b > SBV b > array a b
 writeArray :: SymWord b => array a b > SBV a > SBV b > array a b
 mergeArrays :: SymWord b => SBV Bool > array a b > array a b > array a b
 data SArray a b
 data SFunArray a b
 mkSFunArray :: (SBV a > SBV b) > SFunArray a b
 type STree i e = STreeInternal (SBV i) (SBV e)
 readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e > SBV i > SBV e
 writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e > SBV i > SBV e > STree i e
 mkSTree :: forall i e. HasKind i => [SBV e] > STree i e
 sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a > Int > SBool
 sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a > SWord8
 sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sbvSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 setBitTo :: (Num a, Bits a, SymWord a) => SBV a > Int > SBool > SBV a
 oneIf :: (Num a, SymWord a) => SBool > SBV a
 lsb :: (Num a, Bits a, SymWord a) => SBV a > SBool
 msb :: (Num a, Bits a, SymWord a) => SBV a > SBool
 allEqual :: EqSymbolic a => [a] > SBool
 allDifferent :: EqSymbolic a => [a] > SBool
 inRange :: OrdSymbolic a => a > (a, a) > SBool
 sElem :: EqSymbolic a => a > [a] > SBool
 fullAdder :: SIntegral a => SBV a > SBV a > (SBool, SBV a)
 fullMultiplier :: SIntegral a => SBV a > SBV a > (SBV a, SBV a)
 blastBE :: (Num a, Bits a, SymWord a) => SBV a > [SBool]
 blastLE :: (Num a, Bits a, SymWord a) => SBV a > [SBool]
 class FromBits a where
 fromBitsLE, fromBitsBE :: [SBool] > a
 class Splittable a b  b > a where
 class SignCast a b  a > b, b > a where
 signCast :: a > b
 unsignCast :: b > a
 class (Num a, Bits a) => Polynomial a where
 crcBV :: Int > [SBool] > [SBool] > [SBool]
 crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int > SBV a > SBV b > SBV b
 class Mergeable a where
 ite :: Mergeable a => SBool > a > a > a
 iteLazy :: Mergeable a => SBool > a > a > a
 sBranch :: Mergeable a => SBool > a > a > a
 sAssert :: Mergeable a => String > SBool > a > a
 sAssertCont :: Mergeable a => String > (forall b. SMTConfig > Maybe (Map String CW) > b) > SBool > a > a
 class EqSymbolic a where
 class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
 class (SymWord a, Num a, Bits a) => SIntegral a
 class SDivisible a where
 class Boolean b where
 bAnd :: Boolean b => [b] > b
 bOr :: Boolean b => [b] > b
 bAny :: Boolean b => (a > b) > [a] > b
 bAll :: Boolean b => (a > b) > [a] > b
 class PrettyNum a where
 readBin :: Num a => String > a
 class Uninterpreted a where
 uninterpret :: String > a
 cgUninterpret :: String > [String] > a > a
 sbvUninterpret :: Maybe ([String], a) > String > a
 addAxiom :: String > [String] > Symbolic ()
 type Predicate = Symbolic SBool
 class Provable a where
 class Equality a where
 prove :: Provable a => a > IO ThmResult
 proveWith :: Provable a => SMTConfig > a > IO ThmResult
 isTheorem :: Provable a => Maybe Int > a > IO (Maybe Bool)
 isTheoremWith :: Provable a => SMTConfig > Maybe Int > a > IO (Maybe Bool)
 sat :: Provable a => a > IO SatResult
 satWith :: Provable a => SMTConfig > a > IO SatResult
 isSatisfiable :: Provable a => Maybe Int > a > IO (Maybe Bool)
 isSatisfiableWith :: Provable a => SMTConfig > Maybe Int > a > IO (Maybe Bool)
 allSat :: Provable a => a > IO AllSatResult
 allSatWith :: Provable a => SMTConfig > a > IO AllSatResult
 solve :: [SBool] > Symbolic SBool
 constrain :: SBool > Symbolic ()
 pConstrain :: Double > SBool > Symbolic ()
 isVacuous :: Provable a => a > IO Bool
 isVacuousWith :: Provable a => SMTConfig > a > IO Bool
 safe :: SExecutable a => a > IO SafeResult
 safeWith :: SExecutable a => SMTConfig > a > IO SafeResult
 class SExecutable a where
 proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, ThmResult)]
 proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, ThmResult)
 satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, SatResult)]
 satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, SatResult)
 allSatWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, AllSatResult)]
 allSatWithAny :: Provable a => [SMTConfig] > a > IO (Solver, AllSatResult)
 minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > (SBV c > SBV c > SBool) > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig > OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig > OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 optimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig > OptimizeOpts > (SBV c > SBV c > SBool) > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a])
 expectedValue :: Outputtable a => Symbolic a > IO [Double]
 expectedValueWith :: Outputtable a => Bool > Int > Maybe Int > Double > Symbolic a > IO [Double]
 newtype ThmResult = ThmResult SMTResult
 newtype SatResult = SatResult SMTResult
 newtype AllSatResult = AllSatResult (Bool, [SMTResult])
 data SMTResult
 = Unsatisfiable SMTConfig
  Satisfiable SMTConfig SMTModel
  Unknown SMTConfig SMTModel
  ProofError SMTConfig [String]
  TimeOut SMTConfig
 data SafeResult
 = SafeNeverFails
  SafeAlwaysFails String
  SafeFailsInModel String SMTConfig SMTModel
 class SatModel a where
 class Modelable a where
 modelExists :: a > Bool
 getModel :: SatModel b => a > Either String (Bool, b)
 getModelDictionary :: a > Map String CW
 getModelValue :: SymWord b => String > a > Maybe b
 getModelUninterpretedValue :: String > a > Maybe String
 extractModel :: SatModel b => a > Maybe b
 displayModels :: SatModel a => (Int > (Bool, a) > IO ()) > AllSatResult > IO Int
 extractModels :: SatModel a => AllSatResult > [a]
 getModelDictionaries :: AllSatResult > [Map String CW]
 getModelValues :: SymWord b => String > AllSatResult > [Maybe b]
 getModelUninterpretedValues :: String > AllSatResult > [Maybe String]
 data SMTConfig = SMTConfig {
 verbose :: Bool
 timing :: Bool
 sBranchTimeOut :: Maybe Int
 timeOut :: Maybe Int
 printBase :: Int
 printRealPrec :: Int
 solverTweaks :: [String]
 satCmd :: String
 smtFile :: Maybe FilePath
 useSMTLib2 :: Bool
 solver :: SMTSolver
 roundingMode :: RoundingMode
 useLogic :: Maybe Logic
 data SMTLibLogic
 data Logic
 data OptimizeOpts
 data Solver
 data SMTSolver = SMTSolver {
 name :: Solver
 executable :: String
 options :: [String]
 engine :: SMTEngine
 xformExitCode :: ExitCode > ExitCode
 capabilities :: SolverCapabilities
 boolector :: SMTConfig
 cvc4 :: SMTConfig
 yices :: SMTConfig
 z3 :: SMTConfig
 mathSAT :: SMTConfig
 defaultSolverConfig :: Solver > SMTConfig
 sbvCurrentSolver :: SMTConfig
 defaultSMTCfg :: SMTConfig
 sbvCheckSolverInstallation :: SMTConfig > IO Bool
 sbvAvailableSolvers :: IO [SMTConfig]
 data Symbolic a
 output :: Outputtable a => a > Symbolic a
 class (HasKind a, Ord a) => SymWord a where
 forall :: String > Symbolic (SBV a)
 forall_ :: Symbolic (SBV a)
 mkForallVars :: Int > Symbolic [SBV a]
 exists :: String > Symbolic (SBV a)
 exists_ :: Symbolic (SBV a)
 mkExistVars :: Int > Symbolic [SBV a]
 free :: String > Symbolic (SBV a)
 free_ :: Symbolic (SBV a)
 mkFreeVars :: Int > Symbolic [SBV a]
 symbolic :: String > Symbolic (SBV a)
 symbolics :: [String] > Symbolic [SBV a]
 literal :: a > SBV a
 unliteral :: SBV a > Maybe a
 fromCW :: CW > a
 isConcrete :: SBV a > Bool
 isSymbolic :: SBV a > Bool
 isConcretely :: SBV a > (a > Bool) > Bool
 mbMaxBound, mbMinBound :: Maybe a
 mkSymWord :: Maybe Quantifier > Maybe String > Symbolic (SBV a)
 compileToSMTLib :: Provable a => Bool > Bool > a > IO String
 generateSMTBenchmarks :: Provable a => Bool > FilePath > a > IO ()
 genTest :: Outputtable a => Int > Symbolic a > IO TestVectors
 getTestValues :: TestVectors > [([CW], [CW])]
 data TestVectors
 data TestStyle
 renderTest :: TestStyle > TestVectors > String
 data CW = CW {}
 class HasKind a where
 data Kind
 cwToBool :: CW > Bool
 data SBVCodeGen a
 cgPerformRTCs :: Bool > SBVCodeGen ()
 cgSetDriverValues :: [Integer] > SBVCodeGen ()
 cgGenerateDriver :: Bool > SBVCodeGen ()
 cgGenerateMakefile :: Bool > SBVCodeGen ()
 cgInput :: SymWord a => String > SBVCodeGen (SBV a)
 cgInputArr :: SymWord a => Int > String > SBVCodeGen [SBV a]
 cgOutput :: SymWord a => String > SBV a > SBVCodeGen ()
 cgOutputArr :: SymWord a => String > [SBV a] > SBVCodeGen ()
 cgReturn :: SymWord a => SBV a > SBVCodeGen ()
 cgReturnArr :: SymWord a => [SBV a] > SBVCodeGen ()
 cgAddPrototype :: [String] > SBVCodeGen ()
 cgAddDecl :: [String] > SBVCodeGen ()
 cgAddLDFlags :: [String] > SBVCodeGen ()
 cgIntegerSize :: Int > SBVCodeGen ()
 cgSRealType :: CgSRealType > SBVCodeGen ()
 data CgSRealType
 compileToC :: Maybe FilePath > String > SBVCodeGen () > IO ()
 compileToCLib :: Maybe FilePath > String > [(String, SBVCodeGen ())] > IO ()
 module Data.Bits
 module Data.Word
 module Data.Int
 module Data.Ratio
Programming with symbolic values
The SBV library is really two things:
 A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
 A framework for proving properties of such programs using SMT solvers.
The programming goal of SBV is to provide a seamless experience, i.e., let people program
in the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the Num
and Bits
classes simplify coding), it makes life harder
in others. For instance, 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.
Symbolic types
Symbolic bit
Unsigned symbolic bitvectors
Signed symbolic bitvectors
Signed unbounded integers
The SBV library supports unbounded signed integers with the type SInteger
, which are not subject to
overflow/underflow as it is the case with the bounded types, such as SWord8
, SInt16
, etc. However,
some 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:
split
, '#', andextend
(see theSplittable
class)
Usual arithmetic (+
, 
, *
, sQuotRem
, sQuot
, sRem
, sDivMod
, sDiv
, sMod
) and logical operations (.<
, .<=
, .>
, .>=
, .==
, ./=
) operations are
supported for SInteger
fully, both in programming and verification modes.
IEEEfloating 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.
data RoundingMode Source
Rounding mode to be used for the IEEE floatingpoint operations.
Note that Haskell's default is RoundNearestTiesToEven
. If you use
a different rounding mode, then the counterexamples you get may not
match what you observe in Haskell.
RoundNearestTiesToEven  Round to nearest representable floating point value. If precisely at halfway, pick the even number. (In this context, even means the lowestorder bit is zero.) 
RoundNearestTiesToAway  Round to nearest representable floating point value. If precisely at halfway, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.) 
RoundTowardPositive  Round towards positive infinity. (Also known as roundingup or ceiling.) 
RoundTowardNegative  Round towards negative infinity. (Also known as roundingdown or floor.) 
RoundTowardZero  Round towards zero. (Also known as truncation.) 
fusedMA :: (SymWord a, Floating a) => SBV a > SBV a > SBV a > SBV a Source
Fusedmultiply add. fusedMA a b c = a * b + c
, for double and floating point values.
Note that a fusedMA
call will *never* be concrete, even if all the arguments are constants; since
we cannot guarantee the precision requirements, which is the whole reason why fusedMA
exists in the
first place. (NB. fusedMA
only rounds once, even though it does two operations, and hence the extra
precision.)
isSNaN :: (Floating a, SymWord a) => SBV a > SBool Source
Note that the floating point value NaN does not compare equal to itself,
so we need a special recognizer for that. Haskell provides the isNaN predicate
with the RealFrac
class, which unfortunately is not currently implementable for
symbolic cases. (Requires trigonometric functions etc.) Thus, we provide this
recognizer separately. Note that the definition simply tests equality against
itself, which fails for NaN. Who said equality for floating point was reflexive?
isFPPoint :: (Floating a, SymWord a) => SBV a > SBool Source
We call a FP number FPPoint if it is neither NaN, nor +/ infinity.
Signed 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://goedel.cs.uiowa.edu/smtlib/theories/Reals.smt2.) 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
Creating a symbolic variable
These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms
for free
(specialized at the given type), but they might be easier to use.
Creating a list of symbolic variables
These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms
for mapM
free
(specialized at the given type), but they might be easier to use.
Abstract SBV type
The Symbolic value. Either a constant (Left
) or a symbolic
value (Right Cached
). Note that caching is essential for making
sure sharing is preserved. The parameter a
is phantom, but is
extremely important in keeping the user interface strongly typed.
Arrays of symbolic values
class SymArray array where Source
Flat arrays of symbolic values
An array a b
is an array indexed by the type
, with elements of type SBV
a
If an initial value is not provided in SBV
bnewArray_
and newArray
methods, then the elements
are left unspecified, i.e., the solver is free to choose any value. This is the right thing
to do if arrays are used as inputs to functions to be verified, typically.
While it's certainly possible for user to create instances of SymArray
, the
SArray
and SFunArray
instances already provided should cover most use cases
in practice. (There are some differences between these models, however, see the corresponding
declaration.)
Minimal complete definition: All methods are required, no defaults.
newArray_ :: (HasKind a, HasKind b) => Maybe (SBV b) > Symbolic (array a b) Source
Create a new array, with an optional initial value
newArray :: (HasKind a, HasKind b) => String > Maybe (SBV b) > Symbolic (array a b) Source
Create a named new array, with an optional initial value
readArray :: array a b > SBV a > SBV b Source
Read the array element at a
resetArray :: SymWord b => array a b > SBV b > array a b Source
Reset all the elements of the array to the value b
writeArray :: SymWord b => array a b > SBV a > SBV b > array a b Source
Update the element at a
to be b
mergeArrays :: SymWord b => SBV Bool > array a b > array a b > array a b Source
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b
.
Merging pushes the ifthenelse choice down on to elements
Arrays implemented in terms of SMTarrays: http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2
 Maps directly to SMTlib arrays
 Reading from an unintialized value is OK and yields an unspecified result
 Can check for equality of these arrays
 Cannot quickcheck theorems using
SArray
values  Typically slower as it heavily relies on SMTsolving for the array theory
Arrays implemented internally as functions
 Internally handled by the library and not mapped to SMTLib
 Reading an uninitialized value is considered an error (will throw exception)
 Cannot check for equality (internally represented as functions)
 Can quickcheck
 Typically faster as it gets compiled away during translation
mkSFunArray :: (SBV a > SBV b) > SFunArray a b Source
Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray
.)
Full binary trees
type STree i e = STreeInternal (SBV i) (SBV e) Source
A symbolic tree containing values of type e, indexed by
elements of type i. Note that these are fulltrees, and their
their shapes remain constant. There is no API provided that
can change the shape of the tree. These structures are useful
when dealing with datastructures that are indexed with symbolic
values where access time is important. STree
structures provide
logarithmic time reads and writes.
readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e > SBV i > SBV e Source
Reading a value. We bitblast the index and descend down the full tree according to bitvalues.
writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e > SBV i > SBV e > STree i e Source
Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.
mkSTree :: forall i e. HasKind i => [SBV e] > STree i e Source
Construct the fully balanced initial tree using the given values.
Operations on symbolic values
Word level
sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a > SWord8 Source
Replacement for popCount
. Since popCount
returns an Int
, we cannot implement
it for symbolic words. Here, we return an SWord8
, which can overflow when used on
quantities that have more than 255 bits. Currently, that's only the SInteger
type
that SBV supports, all other types are safe. Even with SInteger
, this will only
overflow if there are at least 256bits set in the number, and the smallest such
number is 2^2561, which is a pretty darn big number to worry about for practical
purposes. In any case, we do not support sbvPopCount
for unbounded symbolic integers,
as the only possible implementation wouldn't symbolically terminate. So the only overflow
issue is with reallyreally large concrete SInteger
values.
sbvShiftRight :: (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. The shift amount must be an unsigned quantity.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
following the usual Haskell convention. See sbvSignedShiftArithRight
for a variant
that explicitly uses the msb as the sign bit, even for unsigned underlying types.
sbvSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a Source
Arithmetic shiftright with a symbolic unsigned shift amount. This is equivalent
to sbvShiftRight
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.
lsb :: (Num a, Bits a, SymWord a) => SBV a > SBool Source
Least significant bit of a word, always stored at index 0.
msb :: (Num a, Bits a, SymWord a) => SBV a > SBool Source
Most significant bit of a word, always stored at the last position.
Predicates
allEqual :: EqSymbolic a => [a] > SBool Source
Returns (symbolic) true if all the elements of the given list are the same.
allDifferent :: EqSymbolic a => [a] > SBool Source
Returns (symbolic) true if all the elements of the given list are different.
inRange :: OrdSymbolic a => a > (a, a) > SBool Source
Returns (symbolic) true if the argument is in range
sElem :: EqSymbolic a => a > [a] > SBool Source
Symbolic membership test
Addition and Multiplication with highbits
fullAdder :: SIntegral a => SBV a > SBV a > (SBool, SBV a) Source
Full adder. Returns the carryout from the addition.
N.B. Only works for unsigned types. Signed arguments will be rejected.
fullMultiplier :: SIntegral a => SBV a > SBV a > (SBV a, SBV a) Source
Full multiplier: Returns both the highorder and the loworder bits in a tuple, thus fully accounting for the overflow.
N.B. Only works for unsigned types. Signed arguments will be rejected.
N.B. The higherorder bits are determined using a simple shiftadd multiplier, thus involving bitblasting. It'd be naive to expect SMT solvers to deal efficiently with properties involving this function, at least with the current state of the art.
Blasting/Unblasting
blastBE :: (Num a, Bits a, SymWord a) => SBV a > [SBool] Source
Bigendian blasting of a word into its bits. Also see the FromBits
class.
blastLE :: (Num a, Bits a, SymWord a) => SBV a > [SBool] Source
Littleendian blasting of a word into its bits. Also see the FromBits
class.
Unblasting a value from symbolicbits. The bits can be given littleendian or bigendian. For a signed number in littleendian, we assume the very last bit is the sign digit. This is a bit awkward, but it is more consistent with the "reverse" view of littlebigendian representations
Minimal complete definition: fromBitsLE
fromBitsLE, fromBitsBE :: [SBool] > a Source
Splitting, joining, and extending
class Splittable a b  b > a where Source
Splitting an a
into two b
's and joining back.
Intuitively, a
is a larger bitsize word than b
, typically double.
The extend
operation captures embedding of a b
value into an a
without changing its semantic value.
Minimal complete definition: All, no defaults.
Signcasting
class SignCast a b  a > b, b > a where Source
Sign casting a value into another. This essentially
means forgetting the sign bit and reinterpreting the bits
accordingly when converting a signed value to an unsigned
one. Similarly, when an unsigned quantity is converted to
a signed one, the most significant bit is interpreted
as the sign. We only define instances when the source
and target types are precisely the same size.
The idea is that signCast
and unsignCast
must form
an isomorphism pair between the types a
and b
, i.e., we
expect the following two properties to hold:
signCast . unsignCast = id unsingCast . signCast = id
Note that one naive way to implement both these operations
is simply to compute fromBitsLE . blastLE
, i.e., first
get all the bits of the word and then reconstruct in the target
type. While this is semantically correct, it generates a lot
of code (both during proofs via SMTLib, and when compiled to C).
The goal of this class is to avoid that cost, so these operations
can be compiled very efficiently, they will essentially become noop's.
Minimal complete definition: All, no defaults.
Polynomial arithmetic and CRCs
class (Num a, Bits a) => Polynomial a where Source
Implements polynomial addition, multiplication, division, and modulus operations
over GF(2^n). NB. Similar to sQuotRem
, division by 0
is interpreted as follows:
x pDivMod
0 = (0, x)
for all x
(including 0
)
Minimal complete definition: pMult
, pDivMod
, showPolynomial
polynomial :: [Int] > a Source
Given bitpositions to be set, create a polynomial For instance
polynomial [0, 1, 3] :: SWord8
will evaluate to 11
, since it sets the bits 0
, 1
, and 3
. Mathematicans would write this polynomial
as x^3 + x + 1
. And in fact, showPoly
will show it like that.
Add two polynomials in GF(2^n).
pMult :: (a, a, [Int]) > a Source
Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by the polynomial as specified by coefficients of the third argument. Note that the third argument is specifically left in this form as it is usally in GF(2^(n+1)), which is not available in our formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles, so this should not be a problem in practice.)
Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't fit into the resulting size.
Divide two polynomials in GF(2^n), see above note for division by 0.
Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0.
pDivMod :: a > a > (a, a) Source
Division and modulus packed together.
showPoly :: a > String Source
Display a polynomial like a mathematician would (over the monomial x
), with a type.
showPolynomial :: Bool > a > String Source
Display a polynomial like a mathematician would (over the monomial x
), the first argument
controls if the final type is shown as well.
crcBV :: Int > [SBool] > [SBool] > [SBool] Source
Compute CRCs over bitvectors. The call crcBV n m p
computes
the CRC of the message m
with respect to polynomial p
. The
inputs are assumed to be blasted bigendian. The number
n
specifies how many bits of CRC is needed. Note that n
is actually the degree of the polynomial p
, and thus it seems
redundant to pass it in. However, in a typical proof context,
the polynomial can be symbolic, so we cannot compute the degree
easily. While this can be workedaround by generating code that
accounts for all possible degrees, the resulting code would
be unnecessarily big and complicated, and much harder to reason
with. (Also note that a CRC is just the remainder from the
polynomial division, but this routine is much faster in practice.)
NB. The n
th bit of the polynomial p
must be set for the CRC
to be computed correctly. Note that the polynomial argument p
will
not even have this bit present most of the time, as it will typically
contain bits 0
through n1
as usual in the CRC literature. The higher
order n
th bit is simply assumed to be set, as it does not make
sense to use a polynomial of a lesser degree. This is usually not a problem
since CRC polynomials are designed and expressed this way.
NB. The literature on CRC's has many variants on how CRC's are computed. We follow the painless guide (http://www.ross.net/crc/download/crc_v3.txt) and compute the CRC as follows:
 Extend the message
m
by addingn
0 bits on the right Divide the polynomial thus obtained by the
p
 The remainder is the CRC value.
 Divide the polynomial thus obtained by the
There are many variants on final XOR's, reversed polynomials etc., so it is essential to double check you use the correct algorithm.
crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int > SBV a > SBV b > SBV b Source
Conditionals: Mergeable values
class Mergeable a where Source
Symbolic conditionals are modeled by the Mergeable
class, describing
how to merge the results of an 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.
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: symbolicMerge
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 :: (SymWord b, Num b) => [a] > a > SBV b > a Source
Total indexing operation. select xs default index
is intuitively
the same as xs !! index
, except it evaluates to default
if index
overflows
Mergeable ()  
Mergeable Mostek 

Mergeable Status  Mergeable instance for 
Mergeable a => Mergeable [a]  
Mergeable a => Mergeable (Maybe a)  
SymWord a => Mergeable (SBV a)  
Mergeable a => Mergeable (Move a)  Mergeable instance for 
Mergeable b => Mergeable (a > b)  
(Mergeable a, Mergeable b) => Mergeable (Either a b)  
(Mergeable a, Mergeable b) => Mergeable (a, b)  
(Ix a, Mergeable b) => Mergeable (Array a b)  
SymWord b => Mergeable (SFunArray a b)  
SymWord b => Mergeable (SArray a b)  
(SymWord e, Mergeable (SBV e)) => Mergeable (STree i e)  
(Mergeable a, Mergeable b, Mergeable c) => Mergeable (a, b, c)  
(Mergeable a, Mergeable b, Mergeable c, Mergeable d) => Mergeable (a, b, c, d)  
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e) => Mergeable (a, b, c, d, e)  
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f) => Mergeable (a, b, c, d, e, f)  
(Mergeable a, Mergeable b, Mergeable c, Mergeable d, Mergeable e, Mergeable f, Mergeable g) => Mergeable (a, b, c, d, e, f, g) 
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.
sBranch :: Mergeable a => SBool > a > a > a Source
Branch on a condition, much like ite
. The exception is that SBV will
check to make sure if the test condition is feasible by making an external
call to the SMT solver. Note that this can be expensive, thus we shall use
a timeout value (sBranchTimeOut
). There might be zero, one, or two such
external calls per sBranch
call:
 If condition is statically known to be True/False: 0 calls
 In this case, we simply constant fold..
 If condition is determined to be unsatisfiable : 1 call
 In this case, we know thenbranch is infeasible, so just take the elsebranch
 If condition is determined to be satisfable : 2 calls
 In this case, we know thenbranch is feasible, but we still have to check if the elsebranch is
In summary, sBranch
calls can be expensive, but they can help with the socalled symbolictermination
problem. See Data.SBV.Examples.Misc.SBranch for an example.
Conditional symbolic simulation
sAssert :: Mergeable a => String > SBool > a > a Source
Symbolic assert. Check that the given boolean condition is always true in the given path. Otherwise symbolic simulation will stop with a runtime error.
sAssertCont :: Mergeable a => String > (forall b. SMTConfig > Maybe (Map String CW) > b) > SBool > a > a Source
Symbolic assert with a programmable continuation. Check that the given boolean condition is always true in the given path.
Otherwise symbolic simulation will transfer the failing model to the given continuation. The
continuation takes the SMTConfig
, and a possible model: If it receives Nothing
, then it means that the condition
fails for all assignments to inputs. Otherwise, it'll receive Just
a dictionary that maps the
input variables to the appropriate CW
values that exhibit the failure. Note that the continuation
has no option but to display the result in some fashion and call error, due to its restricted type.
Symbolic equality
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: .==
EqSymbolic Bool  
EqSymbolic a => EqSymbolic [a]  
EqSymbolic a => EqSymbolic (Maybe a)  
EqSymbolic (SBV a)  
(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b)  
(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b)  
EqSymbolic (SArray a b)  
(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c)  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d)  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e)  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f)  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) 
Symbolic ordering
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.
Minimal complete definition: .<
OrdSymbolic a => OrdSymbolic [a]  
OrdSymbolic a => OrdSymbolic (Maybe a)  
SymWord a => OrdSymbolic (SBV a)  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b)  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b)  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c)  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d)  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e)  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f)  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) 
Symbolic integral numbers
class (SymWord a, Num a, Bits a) => SIntegral a Source
Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic 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.
Division
class SDivisible a where Source
The SDivisible
class captures the essence of division.
Unfortunately we cannot use Haskell's Integral
class since the Real
and Enum
superclasses are not implementable for symbolic bitvectors.
However, quotRem
and divMod
makes perfect sense, and the SDivisible
class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following law:
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.
The Boolean class
The Boolean
class: a generalization of Haskell's Bool
type
Haskell Bool
and SBV's SBool
are instances of this class, unifying the treatment of boolean values.
Minimal complete definition: true
, bnot
, &&&
However, it's advisable to define false
, and 
as well (typically), for clarity.
logical true
logical false
complement
(&&&) :: b > b > b infixr 3 Source
and
() :: b > b > b infixr 2 Source
or
(~&) :: b > b > b infixr 3 Source
nand
(~) :: b > b > b infixr 2 Source
nor
(<+>) :: b > b > b infixl 6 Source
xor
(==>) :: b > b > b infixr 1 Source
implies
(<=>) :: b > b > b infixr 1 Source
equivalence
cast from Bool
Generalizations of boolean operations
Prettyprinting and reading numbers in Hex & Binary
class PrettyNum a where Source
PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
Show a number in hexadecimal (starting with 0x
and type.)
Show a number in binary (starting with 0b
and type.)
Show a number in hex, without prefix, or types.
Show a number in bin, without prefix, or types.
readBin :: Num a => String > a Source
A more convenient interface for reading binary numbers, also supports negative numbers
Uninterpreted sorts, constants, and functions
Users can introduce new uninterpreted sorts simply by defining a datatype in Haskell and registering it as such. The following example demonstrates:
data B = B () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord B
instance HasKind B
instance SatModel B  required only if getModel
etc. is used.
(Note that you'll also need to use the language pragma DeriveDataTypeable
, and import Data.Generics
for the above to work.)
Once GHC implements derivable user classes (http://hackage.haskell.org/trac/ghc/ticket/5462), we will be able to simplify this to:
data B = B () deriving (Eq, Ord, Data, Typeable, Read, Show, SymWord, HasKind)
This is all it takes to introduce B
as an uninterpreted sort in SBV, which makes the type SBV B
automagically become available as the type
of symbolic values that ranges over B
values. Note that the ()
argument is important to distinguish it from enumerations.
Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by
the Uninterpreted
class.
class Uninterpreted a where Source
Uninterpreted constants and functions. An uninterpreted constant is a value that is indexed by its name. The only property the prover assumes about these values are that they are equivalent to themselves; i.e., (for functions) they return the same results when applied to same arguments. We support uninterpretedfunctions as a general means of blackbox'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Minimal complete definition: sbvUninterpret
. However, most instances in
practice are already provided by SBV, so endusers should not need to define their
own instances.
uninterpret :: String > a Source
Uninterpret a value, receiving an object that can be used instead. Use this version when you do not need to add an axiom about this value.
cgUninterpret :: String > [String] > a > a Source
Uninterpret a value, only for the purposes of codegeneration. For execution and verification the value is used as is. For codegeneration, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.
sbvUninterpret :: Maybe ([String], a) > String > a Source
Most generalized form of uninterpretation, this function should not be needed by endusercode, but is rather useful for the library development.
addAxiom :: String > [String] > Symbolic () Source
Add a user specified axiom to the generated SMTLib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiplelines of the axiom text as expressed in SMTLib notation. Note that we perform no checks on the axiom itself, to see whether it's actually wellformed or is sensical by any means. A separate formalization of SMTLib would be very useful here.
Enumerations
If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually translate that as just such a datatype to SMTLib, and will use the constructors as the inhabitants of the said sort. A simple example is:
data X = A  B  C deriving (Eq, Ord, Data, Typeable, Read, Show) instance SymWord X instance HasKind X instance SatModel X
Now, the user can define
type SX = SBV X
and treat SX
as a regular symbolic type ranging over the values A
, B
, and C
. Such values can be compared for equality, and with the usual
other comparison operators, such as .==
, ./=
, .>
, .>=
, <
, and <=
.
Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple query would look like:
allSat $ x > x .== (x :: SX)
which would list all three elements of this domain as satisfying solutions.
Solution #1: s0 = A :: X Solution #2: s0 = B :: X Solution #3: s0 = C :: X Found 3 different solutions.
Note that the result is properly typed as X
elements; these are not mere strings. So, in a getModel
scenario, the user can recover actual
elements of the domain and program further with those values as usual.
Properties, proofs, and satisfiability
The SBV library provides a "pushbutton" verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMTLib standard (http://goedel.cs.uiowa.edu/smtlib/) to communicate with arbitrary SMT solvers.
Predicates
type Predicate = Symbolic SBool Source
A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
purposes, it can be treated as an nary function from symbolicvalues to a boolean. The Symbolic
monad captures the underlying representation, and can/should be ignored by the users of the library,
unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate
type when necessary.
A type a
is provable if we can turn it into a predicate.
Note that a predicate can be made from a curried function of arbitrary arity, where
each element is either a symbolic type or upto a 7tuple of symbolictypes. So
predicates can be constructed from almost arbitrary Haskell functions that have arbitrary
shapes. (See the instance declarations below.)
forAll_ :: a > Predicate Source
Turns a value into a universally quantified predicate, internally naming the inputs.
In this case the sbv library will use names of the form s1, s2
, etc. to name these variables
Example:
forAll_ $ \(x::SWord8) y > x `shiftL` 2 .== y
is a predicate with two arguments, captured using an ordinary Haskell function. Internally,
x
will be named s0
and y
will be named s1
.
forAll :: [String] > a > Predicate Source
Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:
forAll ["x", "y"] $ \(x::SWord8) y > x `shiftL` 2 .== y
This is the same as above, except the variables will be named x
and y
respectively,
simplifying the counterexamples when they are printed.
forSome_ :: a > Predicate Source
Turns a value into an existentially quantified predicate. (Indeed, exists
would have been
a better choice here for the name, but alas it's already taken.)
forSome :: [String] > a > Predicate Source
Version of forSome
that allows user defined names
Provable SBool  
Provable Predicate  
(SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) > p)  
(SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) > p)  
(SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) > p)  
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) > p)  
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) > p)  
(SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) > p)  
(HasKind a, HasKind b, SymArray array, Provable p) => Provable (array a b > p)  
(SymWord a, Provable p) => Provable (SBV a > p) 
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bitprecise proofs.
Proving properties
prove :: Provable a => a > IO ThmResult Source
Prove a predicate, equivalent to proveWith
defaultSMTCfg
proveWith :: Provable a => SMTConfig > a > IO ThmResult Source
Proves the predicate using the given SMTsolver
isTheorem :: Provable a => Maybe Int > a > IO (Maybe Bool) Source
Checks theoremhood within the given optional time limit of i
seconds.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
isTheoremWith :: Provable a => SMTConfig > Maybe Int > a > IO (Maybe Bool) Source
Check whether a given property is a theorem, with an optional time out and the given solver.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
Checking satisfiability
sat :: Provable a => a > IO SatResult Source
Find a satisfying assignment for a predicate, equivalent to satWith
defaultSMTCfg
satWith :: Provable a => SMTConfig > a > IO SatResult Source
Find a satisfying assignment using the given SMTsolver
isSatisfiable :: Provable a => Maybe Int > a > IO (Maybe Bool) Source
Checks satisfiability within the given optional time limit of i
seconds.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
isSatisfiableWith :: Provable a => SMTConfig > Maybe Int > a > IO (Maybe Bool) Source
Check whether a given property is satisfiable, with an optional time out and the given solver.
Returns Nothing
if times out, or the result wrapped in a Just
otherwise.
Finding all satisfying assignments
allSat :: Provable a => a > IO AllSatResult Source
Return all satisfying assignments for a predicate, equivalent to
.
Satisfying assignments are constructed lazily, so they will be available as returned by the solver
and on demand.allSatWith
defaultSMTCfg
NB. Uninterpreted constant/function values and counterexamples for array values are ignored for
the purposes of
. That is, only the satisfying assignments modulo uninterpreted functions and
array inputs will be returned. This is due to the limitation of not having a robust means of getting a
function counterexample back from the SMT solver.allSat
allSatWith :: Provable a => SMTConfig > a > IO AllSatResult Source
Find all satisfying assignments using the given SMTsolver
Satisfying a sequence of boolean conditions
solve :: [SBool] > Symbolic SBool Source
Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:
do [x, y, z] < sIntegers ["x", "y", "z"] solve [x .> 5, y + z .< x]
Adding constraints
A constraint is a means for restricting the input domain of a formula. Here's a simple example:
do x <exists
"x" y <exists
"y"constrain
$ x .> yconstrain
$ x + y .>= 12constrain
$ y .>= 3 ...
The first constraint requires x
to be larger than y
. The scond one says that
sum of x
and y
must be at least 12
, and the final one says that y
to be at least 3
.
Constraints provide an easy way to assert additional properties on the input domain, right at the point of
the introduction of variables.
Note that the proper reading of a constraint depends on the context:
 In a
sat
(orallSat
) call: The constraint added is asserted conjunctively. That is, the resulting satisfying model (if any) will always satisfy all the constraints given.  In a
prove
call: In this case, the constraint acts as an implication. The property is proved under the assumption that the constraint holds. In other words, the constraint says that we only care about the input space that satisfies the constraint.  In a
quickCheck
call: The constraint acts as a filter forquickCheck
; if the constraint does not hold, then the input value is considered to be irrelevant and is skipped. Note that this is similar toprove
, but is stronger: We do not accept a test case to be valid just because the constraints fail on them, although semantically the implication does hold. We simply skip that test case as a bad test vector.  In a
genTest
call: Similar toquickCheck
andprove
: If a constraint does not hold, the input value is ignored and is not included in the test set.
A good use case (in fact the motivating use case) for constrain
is attaching a
constraint to a forall
or exists
variable at the time of its creation.
Also, the conjunctive semantics for sat
and the implicative
semantics for prove
simplify programming by choosing the correct interpretation
automatically. However, one should be aware of the semantic difference. For instance, in
the presence of constraints, formulas that are provable are not necessarily
satisfiable. To wit, consider:
do x <exists
"x"constrain
$ x .< x return $ x .< (x ::SWord8
)
This predicate is unsatisfiable since no element of SWord8
is less than itself. But
it's (vacuously) true, since it excludes the entire domain of values, thus making the proof
trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given
constraints are not vacuous, the functions isVacuous
(and isVacuousWith
) can be used.
Also note that this semantics imply that test case generation (genTest
) and quickcheck
can take arbitrarily long in the presence of constraints, if the random input values generated
rarely satisfy the constraints. (As an extreme case, consider
.)constrain
false
A probabilistic constraint (see pConstrain
) attaches a probability threshold for the
constraint to be considered. For instance:
pConstrain
0.8 c
will make sure that the condition c
is satisfied 80% of the time (and correspondingly, falsified 20%
of the time), in expectation. This variant is useful for genTest
and quickCheck
functions, where we
want to filter the test cases according to some probability distribution, to make sure that the testvectors
are drawn from interesting subsets of the input space. For instance, if we were to generate 100 test cases
with the above constraint, we'd expect about 80 of them to satisfy the condition c
, while about 20 of them
will fail it.
The following properties hold:
constrain
=pConstrain
1pConstrain
t c =pConstrain
(1t) (not c)
Note that while constrain
can be used freely, pConstrain
is only allowed in the contexts of
genTest
or quickCheck
. Calls to pConstrain
in a prove/sat call will be rejected as SBV does not
deal with probabilistic constraints when it comes to satisfiability and proofs.
Also, both constrain
and pConstrain
calls during codegeneration will also be rejected, for similar reasons.
constrain :: SBool > Symbolic () Source
Adding arbitrary constraints. When adding constraints, one has to be careful about
making sure they are not inconsistent. The function isVacuous
can be use for this purpose.
Here is an example. Consider the following predicate:
>>>
let pred = do { x < forall "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }
This predicate asserts that all 8bit values are larger than 5, subject to the constraint that the
values considered satisfy x .< x
, i.e., they are less than themselves. Since there are no values that
satisfy this constraint, the proof will pass vacuously:
>>>
prove pred
Q.E.D.
We can use isVacuous
to make sure to see that the pass was vacuous:
>>>
isVacuous pred
True
While the above example is trivial, things can get complicated if there are multiple constraints with nonstraightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:
>>>
let pred' = do { x < forall "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }
This time the proof passes as expected:
>>>
prove pred'
Q.E.D.
And the proof is not vacuous:
>>>
isVacuous pred'
False
pConstrain :: Double > SBool > Symbolic () Source
Adding a probabilistic constraint. The Double
argument is the probability
threshold. Probabilistic constraints are useful for genTest
and quickCheck
calls where we restrict our attention to interesting parts of the input domain.
Checking constraint vacuity
isVacuous :: Provable a => a > IO Bool Source
Check if the given constraints are satisfiable, equivalent to
.
See the function isVacuousWith
defaultSMTCfg
constrain
for an example use of isVacuous
.
isVacuousWith :: Provable a => SMTConfig > a > IO Bool Source
Determine if the constraints are vacuous using the given SMTsolver
Checking safety
The sAssert
and sAssertCont
functions allow users to introduce invariants throughout their code to make sure
certain properties hold at all times. This is another mechanism to provide further documentation/contract info
into SBV code. The functions safe
and safeWith
can then be used to statically discharge these proof assumptions.
If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.
Here's a simple example. Let's assume we have a function that does subtraction, and requires it's first argument to be larger than the second:
>>>
let sub x y = sAssert "sub: x >= y must hold!" (x .>= y) (x  y)
Clearly, this function is not safe, as there's nothing that ensures us to pass a larger second argument. If we try to prove a theorem regarding sub, we'll get an exception:
>>>
prove $ \x y > sub x y .>= (0 :: SInt16)
*** Exception: Assertion failure: "sub: x >= y must hold!" s0 = 32768 :: SInt16 s1 = 32767 :: SInt16
Of course, we can use, safe
to statically see if such a violation is possible before we attempt a proof:
>>>
safe (sub :: SInt8 > SInt8 > SInt8)
Assertion failure: "sub: x >= y must hold!" s0 = 128 :: SInt8 s1 = 127 :: SInt8
What happens if we make sure to arrange for this invariant? Consider this version:
>>>
let safeSub x y = ite (x .>= y) (sub x y) (sub y x)
Clearly, safeSub
must be safe. And indeed, SBV can prove that:
>>>
safe (safeSub :: SInt8 > SInt8 > SInt8)
No safety violations detected.
Note how we used sub
and safeSub
polymorphically. We only need to monomorphise our types when a proof
attempt is done, as we did in the safe
calls.
safe :: SExecutable a => a > IO SafeResult Source
Check if a given definition is safe; i.e., if all sAssert
conditions can be proven to hold.
safeWith :: SExecutable a => SMTConfig > a > IO SafeResult Source
Check if a given definition is safe using the given solver configuration; i.e., if all sAssert
conditions can be proven to hold.
class SExecutable a where Source
Symbolically executable program fragments. This class is mainly used for safe
calls, and is sufficently populated internally to cover most use
cases. Users can extend it as they wish to allow safe
checks for SBV programs that return/take types that are userdefined.
Proving properties using multiple solvers
On a multicore machine, it might be desirable to try a given property using multiple SMT solvers, using parallel threads. Even with machines with singlecores, threading can be helpful if you want to try out multiplesolvers but do not know which one would work the best for the problem at hand ahead of time.
The functions in this section allow proving/satisfiabilitychecking with multiple backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one.
The All
variants, (i.e., proveWithAll
, satWithAll
, allSatWithAll
) run all solvers and
return all the results. SBV internally makes sure that the result is lazily generated; so,
the order of solvers given does not matter. In other words, the order of results will follow
the order of the solvers as they finish, not as given by the user. These variants are useful when you
want to make sure multiplesolvers agree (or disagree!) on a given problem.
The Any
variants, (i.e., proveWithAny
, satWithAny
, allSatWithAny
) will run all the solvers
in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants
are useful when you do not care if the solvers produce the same result, but rather want to get the
solution as quickly as possible, taking advantage of modern manycore machines.
Note that the function sbvAvailableSolvers
will return all the installed solvers, which can be
used as the first argument to all these functions, if you simply want to try all available solvers on a machine.
proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, ThmResult)] Source
Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, ThmResult) Source
Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, SatResult)] Source
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, SatResult) Source
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
allSatWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, AllSatResult)] Source
Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
allSatWithAny :: Provable a => [SMTConfig] > a > IO (Solver, AllSatResult) Source
Find all satisfying assignments to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.
Optimization
Symbolic optimization. A call of the form:
minimize Quantified cost n valid
returns Just xs
, such that:
xs
has preciselyn
elementsvalid xs
holdscost xs
is minimal. That is, for all sequencesys
that satisfy the first two criteria above,cost xs .<= cost ys
holds.
If there is no such sequence, then minimize
will return Nothing
.
The function maximize
is similar, except the comparator is .>=
. So the value returned has the largest cost (or value, in that case).
The function optimize
allows the user to give a custom comparison function.
The OptimizeOpts
argument controls how the optimization is done. If Quantified
is used, then the SBV optimization engine satisfies the following predicate:
exists xs. forall ys. valid xs && (valid ys ``implies`` (cost xs ``cmp`` cost ys))
Note that this may cause efficiency problems as it involves alternating quantifiers.
If OptimizeOpts
is set to Iterative
True
, then SBV will programmatically
search for an optimal solution, by repeatedly calling the solver appropriately. (The boolean argument controls whether progress reports are given. Use
False
for quiet operation.) Note that the quantified and iterative versions are two different optimization approaches and may not necessarily yield the same
results. In particular, the quantified version can find solutions where there is no global optimum value, while the iterative version would simply loop forever
in such cases. On the other hand, the iterative version might be more suitable if the quantified version of the problem is too hard to deal with by the SMT solver.
minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a]) Source
Minimizes a cost function with respect to a constraint. Examples:
>>>
minimize Quantified sum 3 (bAll (.> (10 :: SInteger)))
Just [11,11,11]
maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a]) Source
Maximizes a cost function with respect to a constraint. Examples:
>>>
maximize Quantified sum 3 (bAll (.< (10 :: SInteger)))
Just [9,9,9]
optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts > (SBV c > SBV c > SBool) > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a]) Source
Variant of optimizeWith
using the default solver. See optimizeWith
for parameter descriptions.
minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig > OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a]) Source
Variant of minimize
allowing the use of a user specified solver. See optimizeWith
for parameter descriptions.
maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig > OptimizeOpts > ([SBV a] > SBV c) > Int > ([SBV a] > SBool) > IO (Maybe [a]) Source
Variant of maximize
allowing the use of a user specified solver. See optimizeWith
for parameter descriptions.
Computing expected values
expectedValue :: Outputtable a => Symbolic a > IO [Double] Source
Given a symbolic computation that produces a value, compute the
expected value that value would take if this computation is run
with its free variables drawn from uniform distributions of its
respective values, satisfying the given constraints specified by
constrain
and pConstrain
calls. This is equivalent to calling
expectedValueWith
the following parameters: verbose, warmup
round count of 10000
, no maximum iteration count, and with
convergence margin 0.0001
.
expectedValueWith :: Outputtable a => Bool > Int > Maybe Int > Double > Symbolic a > IO [Double] Source
Generalized version of expectedValue
, allowing the user to specify the
warmup count and the convergence factor. Maximum iteration count can also
be specified, at which point convergence won't be sought. The boolean controls verbosity.
Model extraction
The default Show
instances for prover calls provide all the counterexample information in a
humanreadable form and should be sufficient for most casual uses of sbv. However, tools built
on top of sbv will inevitably need to look into the constructed models more deeply, programmatically
extracting their results and performing actions based on them. The API provided in this section
aims at simplifying this task.
Inspecting proof results
ThmResult
, SatResult
, and AllSatResult
are simple newtype wrappers over SMTResult
. Their
main purpose is so that we can provide custom Show
instances to print results accordingly.
A prove
call results in a ThmResult
newtype AllSatResult Source
An allSat
call results in a AllSatResult
. The boolean says whether
we should warn the user about prefixexistentials.
AllSatResult (Bool, [SMTResult]) 
Show AllSatResult  The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available. 
The result of an SMT solver call. Each constructor is tagged with
the SMTConfig
that created it so that further tools can inspect it
and build layers of results, if needed. For ordinary uses of the library,
this type should not be needed, instead use the accessor functions on
it. (Custom Show instances and model extractors.)
Unsatisfiable SMTConfig  Unsatisfiable 
Satisfiable SMTConfig SMTModel  Satisfiable with model 
Unknown SMTConfig SMTModel  Prover returned unknown, with a potential (possibly bogus) model 
ProofError SMTConfig [String]  Prover errored out 
TimeOut SMTConfig  Computation timed out (see the 
data SafeResult Source
The result of an sAssert
call
Show SafeResult  The show instance for SafeResult. Note that this is for display purposes only, user programs are likely to pattern match on the output and proceed accordingly. 
Exception SafeResult  If a 
Typeable * SafeResult 
Programmable model extraction
While default Show
instances are sufficient for most use cases, it is sometimes desirable (especially
for library construction) that the SMTmodels are reinterpreted in terms of domain types. Programmable
extraction allows getting arbitrarily typed models out of SMT models.
Instances of SatModel
can be automatically extracted from models returned by the
solvers. The idea is that the sbv infrastructure provides a stream of CW'
s (constantwords)
coming from the solver, and the type a
is interpreted based on these constants. Many typical
instances are already provided, so new instances can be declared with relative ease.
Minimum complete definition: parseCWs
Nothing
parseCWs :: [CW] > Maybe (a, [CW]) Source
Given a sequence of constantwords, extract one instance of the type a
, returning
the remaining elements untouched. If the next element is not what's expected for this
type you should return Nothing
cvtModel :: (a > Maybe b) > Maybe (a, [CW]) > Maybe (b, [CW]) Source
Given a parsed model instance, transform it using f
, and return the result.
The default definition for this method should be sufficient in most use cases.
SatModel Bool 

SatModel Double 

SatModel Float 

SatModel Int8 

SatModel Int16 

SatModel Int32 

SatModel Int64 

SatModel Integer 

SatModel Word8 

SatModel Word16 

SatModel Word32 

SatModel Word64 

SatModel ()  Base case for 
SatModel AlgReal 

SatModel E  The 
SatModel Location  Make 
SatModel U2Member  Make 
SatModel a => SatModel [a]  A list of values as extracted from a model. When reading a list, we go as long as we can (maximalmunch). Note that this never fails, as we can always return the empty list! 
(SatModel a, SatModel b) => SatModel (a, b)  Tuples extracted from a model 
(SatModel a, SatModel b, SatModel c) => SatModel (a, b, c)  3Tuples extracted from a model 
(SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d)  4Tuples extracted from a model 
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e)  5Tuples extracted from a model 
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f)  6Tuples extracted from a model 
(SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g)  7Tuples extracted from a model 
class Modelable a where Source
Various SMT results that we can extract models out of.
modelExists :: a > Bool Source
Is there a model?
getModel :: SatModel b => a > Either String (Bool, b) Source
Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModelDictionary :: a > Map String CW Source
Extract a model dictionary. Extract a dictionary mapping the variables to
their respective values as returned by the SMT solver. Also see getModelDictionaries
.
getModelValue :: SymWord b => String > a > Maybe b Source
Extract a model value for a given element. Also see getModelValues
.
getModelUninterpretedValue :: String > a > Maybe String Source
Extract a representative name for the model value of an uninterpreted kind.
This is supposed to correspond to the value as computed internally by the
SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues
.
extractModel :: SatModel b => a > Maybe b Source
A simpler variant of getModel
to get a model out without the fuss.
displayModels :: SatModel a => (Int > (Bool, a) > IO ()) > AllSatResult > IO Int Source
Given an allSat
call, we typically want to iterate over it and print the results in sequence. The
displayModels
function automates this task by calling disp
on each result, consecutively. The first
Int
argument to disp
'is the current model number. The second argument is a tuple, where the first
element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)
extractModels :: SatModel a => AllSatResult > [a] Source
Return all the models from an allSat
call, similar to extractModel
but
is suitable for the case of multiple results.
getModelDictionaries :: AllSatResult > [Map String CW] Source
Get dictionaries from an allsat call. Similar to getModelDictionary
.
getModelValues :: SymWord b => String > AllSatResult > [Maybe b] Source
Extract value of a variable from an allsat call. Similar to getModelValue
.
getModelUninterpretedValues :: String > AllSatResult > [Maybe String] Source
Extract value of an uninterpreted variable from an allsat call. Similar to getModelUninterpretedValue
.
SMT Interface: Configurations and solvers
Solver configuration. See also z3
, yices
, cvc4
, boolector
, mathSAT
, etc. which are instantiations of this type for those solvers, with
reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}
.)
Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
precision value on the screen. The field printRealPrec
controls the printing precision, by specifying the number of digits after
the decimal point. The default value is 16, but it can be set to any positive integer.
When printing, SBV will add the suffix ...
at the and of a realvalue, if the given bound is not sufficient to represent the realvalue
exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
of the real value is not finite, i.e., if it is not rational.
SMTConfig  

data SMTLibLogic Source
SMTLib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the
user can override this choice using the useLogic
parameter to the configuration. This is especially handy if
one is experimenting with custom logics that might be supported on new solvers.
AUFLIA  Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values 
AUFLIRA  Linear formulas with free sort and function symbols over one and twodimentional arrays of integer index and real value 
AUFNIRA  Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value 
LRA  Linear formulas in linear real arithmetic 
UFLRA  Linear real arithmetic with uninterpreted sort and function symbols. 
UFNIA  Nonlinear integer arithmetic with uninterpreted sort and function symbols. 
QF_ABV  Quantifierfree formulas over the theory of bitvectors and bitvector arrays 
QF_AUFBV  Quantifierfree formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols 
QF_AUFLIA  Quantifierfree linear formulas over the theory of integer arrays extended with free sort and function symbols 
QF_AX  Quantifierfree formulas over the theory of arrays with extensionality 
QF_BV  Quantifierfree formulas over the theory of fixedsize bitvectors 
QF_IDL  Difference Logic over the integers. Boolean combinations of inequations of the form x  y < b where x and y are integer variables and b is an integer constant 
QF_LIA  Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables 
QF_LRA  Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. 
QF_NIA  Quantifierfree integer arithmetic. 
QF_NRA  Quantifierfree real arithmetic. 
QF_RDL  Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x  y < b where x and y are real variables and b is a rational constant. 
QF_UF  Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. 
QF_UFBV  Unquantified formulas over bitvectors with uninterpreted sort function and symbols. 
QF_UFIDL  Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. 
QF_UFLIA  Unquantified linear integer arithmetic with uninterpreted sort and function symbols. 
QF_UFLRA  Unquantified linear real arithmetic with uninterpreted sort and function symbols. 
QF_UFNRA  Unquantified nonlinear real arithmetic with uninterpreted sort and function symbols. 
QF_FPABV  Quantifierfree formulas over the theory of floating point numbers, arrays, and bitvectors 
QF_FPA  Quantifierfree formulas over the theory of floating point numbers 
Chosen logic for the solver
PredefinedLogic SMTLibLogic  Use one of the logics as defined by the standard 
CustomLogic String  Use this name for the logic 
data OptimizeOpts Source
Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.
Iterative Bool  Iteratively search. if True, it will be reporting progress 
Quantified  Use quantifiers 
Solvers that SBV is aware of
An SMT solver
SMTSolver  

defaultSolverConfig :: Solver > SMTConfig Source
The default configs corresponding to supported SMT solvers
sbvCurrentSolver :: SMTConfig Source
The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.
defaultSMTCfg :: SMTConfig Source
The default solver used by SBV. This is currently set to z3.
sbvCheckSolverInstallation :: SMTConfig > IO Bool Source
Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.
sbvAvailableSolvers :: IO [SMTConfig] Source
Return the known available solver configs, installed on your machine.
Symbolic computations
A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.
output :: Outputtable a => a > Symbolic a Source
Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.
class (HasKind a, Ord a) => SymWord a where Source
A SymWord
is a potential symbolic bitvector that can be created instances of
to be fed to a symbolic program. Note that these methods are typically not needed
in casual uses with prove
, sat
, allSat
etc, as default instances automatically
provide the necessary bits.
Nothing
forall :: String > Symbolic (SBV a) Source
Create a user named input (universal)
forall_ :: Symbolic (SBV a) Source
Create an automatically named input
mkForallVars :: Int > Symbolic [SBV a] Source
Get a bunch of new words
exists :: String > Symbolic (SBV a) Source
Create an existential variable
exists_ :: Symbolic (SBV a) Source
Create an automatically named existential variable
mkExistVars :: Int > Symbolic [SBV a] Source
Create a bunch of existentials
free :: String > Symbolic (SBV a) Source
Create a free variable, universal in a proof, existential in sat
free_ :: Symbolic (SBV a) Source
Create an unnamed free variable, universal in proof, existential in sat
mkFreeVars :: Int > Symbolic [SBV a] Source
Create a bunch of free vars
symbolic :: String > Symbolic (SBV a) Source
Similar to free; Just a more convenient name
symbolics :: [String] > Symbolic [SBV a] Source
Similar to mkFreeVars; but automatically gives names based on the strings
Turn a literal constant to symbolic
unliteral :: SBV a > Maybe a Source
Extract a literal, if the value is concrete
Extract a literal, from a CW representation
isConcrete :: SBV a > Bool Source
Is the symbolic word concrete?
isSymbolic :: SBV a > Bool Source
Is the symbolic word really symbolic?
isConcretely :: SBV a > (a > Bool) > Bool Source
Does it concretely satisfy the given predicate?
mbMaxBound, mbMinBound :: Maybe a Source
max/minbounds, if available. Note that we don't want to impose Bounded on our class as Integer is not Bounded but it is a SymWord
mkSymWord :: Maybe Quantifier > Maybe String > Symbolic (SBV a) Source
One stop allocator
SymWord Bool  
SymWord Double  
SymWord Float  
SymWord Int8  
SymWord Int16  
SymWord Int32  
SymWord Int64  
SymWord Integer  
SymWord Word8  
SymWord Word16  
SymWord Word32  
SymWord Word64  
SymWord AlgReal  
SymWord E  The 
SymWord Location  Make 
SymWord U2Member  Make 
SymWord B  Default instance declaration for 
SymWord Q  We need 
SymWord L  Declare instances to make 
Getting SMTLib output (for offline analysis)
:: Provable a  
=> Bool  If True, output SMTLib2, otherwise SMTLib1 
> Bool  If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.) 
> a  
> IO String 
Compiles to SMTLib and returns the resulting program as a string. Useful for saving the result to a file for offline analysis, for instance if you have an SMT solver that's not natively supported outofthe box by the SBV library. It takes two booleans:
 smtLib2: If
True
, will generate SMTLib2 output, otherwise SMTLib1 output
generateSMTBenchmarks :: Provable a => Bool > FilePath > a > IO () Source
Create both SMTLib1 and SMTLib2 benchmarks. The first argument is the basename of the file,
SMTLib1 version will be written with suffix ".smt1" and SMTLib2 version will be written with
suffix ".smt2". The Bool
argument controls whether this is a SAT instance, i.e., translate the query
directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to
compileToSMTLib
for details.)
Test case generation
genTest :: Outputtable a => Int > Symbolic a > IO TestVectors Source
Generate a set of concrete test values from a symbolic program. The output
can be rendered as test vectors in different languages as necessary. Use the
function output
call to indicate what fields should be in the test result.
(Also see constrain
and pConstrain
for filtering acceptable test values.)
getTestValues :: TestVectors > [([CW], [CW])] Source
Retrieve the test vectors for further processing. This function
is useful in cases where renderTest
is not sufficient and custom
output (or further preprocessing) is needed.
data TestVectors Source
Type of test vectors (abstract)
Test output style
Haskell String  As a Haskell value with given name 
C String  As a C array of structs with given name 
Forte String Bool ([Int], [Int])  As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted bigendian, otherwise littleendian The indices are the split points on bitvectors for input and output values 
renderTest :: TestStyle > TestVectors > String Source
Render the test as a Haskell value with the given name n
.
CW
represents a concrete word of a fixed size:
Endianness is mostly irrelevant (see the FromBits
class).
For signed words, the most significant digit is considered to be the sign.
A class for capturing values that have a sign and a size (finite or infinite)
minimal complete definition: kindOf. This class can be automatically derived
for datatypes that have a Data
instance; this is useful for creating uninterpreted
sorts.
Nothing
isUninterpreted :: a > Bool Source
HasKind Bool  
HasKind Double  
HasKind Float  
HasKind Int8  
HasKind Int16  
HasKind Int32  
HasKind Int64  
HasKind Integer  
HasKind Word8  
HasKind Word16  
HasKind Word32  
HasKind Word64  
HasKind AlgReal  
HasKind CW  
HasKind E  The 
HasKind Location  Make 
HasKind U2Member  Make 
HasKind B  Default instance declaration for 
HasKind Q 

HasKind L  Similarly, 
HasKind a => HasKind (SBV a) 
Kind of symbolic value
Code generation from symbolic programs
The SBV library can generate straightline executable code in C. (While other target languages are
certainly possible, currently only C is supported.) The generated code will perform no runtime memoryallocations,
(no calls to malloc
), so its memory usage can be predicted ahead of time. Also, the functions will execute precisely the
same instructions in all calls, so they have predictable timing properties as well. The generated code
has no loops or jumps, and is typically quite fast. While the generated code can be large due to complete unrolling,
these characteristics make them suitable for use in hard realtime systems, as well as in traditional computing.
data SBVCodeGen a Source
The codegeneration monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.
Setting codegeneration options
cgPerformRTCs :: Bool > SBVCodeGen () Source
Sets RTC (runtimechecks) for indexoutofbounds, shiftwithlarge value etc. on/off. Default: False
.
cgSetDriverValues :: [Integer] > SBVCodeGen () Source
Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.
cgGenerateDriver :: Bool > SBVCodeGen () Source
Should we generate a driver program? Default: True
. When a library is generated, it will have
a driver if any of the contituent functions has a driver. (See compileToCLib
.)
cgGenerateMakefile :: Bool > SBVCodeGen () Source
Should we generate a Makefile? Default: True
.
Designating inputs
cgInput :: SymWord a => String > SBVCodeGen (SBV a) Source
Creates an atomic input in the generated code.
cgInputArr :: SymWord a => Int > String > SBVCodeGen [SBV a] Source
Creates an array input in the generated code.
Designating outputs
cgOutput :: SymWord a => String > SBV a > SBVCodeGen () Source
Creates an atomic output in the generated code.
cgOutputArr :: SymWord a => String > [SBV a] > SBVCodeGen () Source
Creates an array output in the generated code.
Designating return values
cgReturn :: SymWord a => SBV a > SBVCodeGen () Source
Creates a returned (unnamed) value in the generated code.
cgReturnArr :: SymWord a => [SBV a] > SBVCodeGen () Source
Creates a returned (unnamed) array value in the generated code.
Code generation with uninterpreted functions
cgAddPrototype :: [String] > SBVCodeGen () Source
Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.
cgAddDecl :: [String] > SBVCodeGen () Source
Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.
cgAddLDFlags :: [String] > SBVCodeGen () Source
Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.
Code generation with SInteger
and SReal
types
The types SInteger
and SReal
are unbounded quantities that have no direct counterparts in the C language. Therefore,
it is not possible to generate standard C code for SBV programs using these types, unless custom libraries are available. To
overcome this, SBV allows the user to explicitly set what the corresponding types should be for these two cases, using
the functions below. Note that while these mappings will produce valid C code, the resulting code will be subject to
overflow/underflows for SInteger
, and rounding for SReal
, so there is an implicit loss of precision.
If the user does not specify these mappings, then SBV will refuse to compile programs that involve these types.
cgIntegerSize :: Int > SBVCodeGen () Source
Sets number of bits to be used for representing the SInteger
type in the generated C code.
The argument must be one of 8
, 16
, 32
, or 64
. Note that this is essentially unsafe as
the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as
typical in most C implementations.
cgSRealType :: CgSRealType > SBVCodeGen () Source
Sets the C type to be used for representing the SReal
type in the generated C code.
The setting can be one of C's "float"
, "double"
, or "long double"
, types, depending
on the precision needed. Note that this is essentially unsafe as the semantics of
infinite precision SReal values becomes reduced to the corresponding floating point type in
C, and hence it is subject to rounding errors.
data CgSRealType Source
Possible mappings for the SReal
type when translated to C. Used in conjunction
with the function cgSRealType
. Note that the particular characteristics of the
mapped types depend on the platform and the compiler used for compiling the generated
C program. See http://en.wikipedia.org/wiki/C_data_types for details.
CgFloat  float 
CgDouble  double 
CgLongDouble  long double 
Eq CgSRealType  
Show CgSRealType 

Compilation to C
compileToC :: Maybe FilePath > String > SBVCodeGen () > IO () Source
Given a symbolic computation, render it as an equivalent collection of files that make up a C program:
 The first argument is the directory name under which the files will be saved. To save
files in the current directory pass
. UseJust
"."Nothing
for printing to stdout.  The second argument is the name of the C function to generate.
 The final argument is the function to be compiled.
Compilation will also generate a Makefile
, a header file, and a driver (test) program, etc.
compileToCLib :: Maybe FilePath > String > [(String, SBVCodeGen ())] > IO () Source
Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.
 The first argument is the directory name under which the files will be saved. To save
files in the current directory pass
. UseJust
"."Nothing
for printing to stdout.  The second argument is the name of the archive to generate.
 The third argument is the list of functions to include, in the form of functionname/code pairs, similar
to the second and third arguments of
compileToC
, except in a list.
Module exports
The SBV library exports the following modules wholesale, as user programs will have to import these modules to make any sensible use of the SBV functionality.
module Data.Bits
module Data.Word
module Data.Int
module Data.Ratio