Safe Haskell  None 

Language  Haskell2010 
 Symbolic types
 Arrays of symbolic values
 Creating symbolic values
 Symbolic Equality and Comparisons
 Conditionals: Mergeable values
 Symbolic integral numbers
 Division and Modulus
 Bitvector operations
 IEEEfloating point numbers
 Enumerations
 Uninterpreted sorts, constants, and functions
 Properties, proofs, and satisfiability
 Constraints
 Checking safety
 Quickchecking
 Optimization
 Model extraction
 SMT Interface
 Abstract SBV type
 Module exports
Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental
(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)
SBV: SMT Based Verification
Express properties about Haskell programs and automatically prove them using SMT solvers.
>>>
prove $ \x > x `shiftL` 2 .== 4 * (x :: SWord8)
Q.E.D.
>>>
prove $ \x > x `shiftL` 2 .== 2 * (x :: SWord8)
Falsifiable. Counterexample: s0 = 64 :: Word8
The function prove
has the following type:
prove
::Provable
a => a >IO
ThmResult
The class Provable
comes with instances for nary predicates, for arbitrary n.
The predicates are just regular Haskell functions over symbolic types listed below.
Functions for checking satisfiability (sat
and allSat
) are also
provided.
The sbv library introduces the following symbolic types:
SBool
: Symbolic Booleans (bits).SWord8
,SWord16
,SWord32
,SWord64
: Symbolic Words (unsigned).SInt8
,SInt16
,SInt32
,SInt64
: Symbolic Ints (signed).SInteger
: Unbounded signed integers.SReal
: Algebraicreal numbersSFloat
: IEEE754 singleprecision floating point valuesSDouble
: IEEE754 doubleprecision floating point valuesSChar
,SString
,RegExp
: Characters, strings and regular expressionsSList
: Symbolic lists (which can be nested)SArray
,SFunArray
: Flat arrays of symbolic values. Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
 Uninterpreted constants and functions over symbolic values, with user defined 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.
The sbv library uses thirdparty SMT solvers via the standard SMTLib interface: http://smtlib.cs.uiowa.edu/
The SBV library is designed to work with any SMTLib compliant SMTsolver. Currently, we support the following SMTSolvers outofthe box:
 ABC from University of Berkeley: http://www.eecs.berkeley.edu/~alanmi/abc/
 CVC4 from Stanford: http://cvc4.cs.stanford.edu/web/
 Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
 MathSAT from Fondazione Bruno Kessler and DISIUniversity of Trento: http://mathsat.fbk.eu/
 Yices from SRI: http://yices.csl.sri.com/
 Z3 from Microsoft: http://github.com/Z3Prover/z3/wiki
SBV requires recent versions of these solvers; please see the file
SMTSolverVersions.md
in the source distribution for specifics.
SBV also allows calling these solvers in parallel, either getting results from multiple solvers
or returning the fastest one. (See proveWithAll
, proveWithAny
, etc.)
Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.
Synopsis
 type SBool = SBV Bool
 sTrue :: SBool
 sFalse :: SBool
 sNot :: SBool > SBool
 (.&&) :: SBool > SBool > SBool
 (.) :: SBool > SBool > SBool
 (.<+>) :: SBool > SBool > SBool
 (.~&) :: SBool > SBool > SBool
 (.~) :: SBool > SBool > SBool
 (.=>) :: SBool > SBool > SBool
 (.<=>) :: SBool > SBool > SBool
 fromBool :: Bool > SBool
 oneIf :: (Num a, SymVal a) => SBool > SBV a
 sAnd :: [SBool] > SBool
 sOr :: [SBool] > SBool
 sAny :: (a > SBool) > [a] > SBool
 sAll :: (a > SBool) > [a] > SBool
 type SWord8 = SBV Word8
 type SWord16 = SBV Word16
 type SWord32 = SBV Word32
 type SWord64 = SBV Word64
 type 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
 type SReal = SBV AlgReal
 data AlgReal
 sRealToSInteger :: SReal > SInteger
 type SChar = SBV Char
 type SString = SBV String
 type SList a = SBV [a]
 type STuple2 a b = SBV (a, b)
 type STuple3 a b c = SBV (a, b, c)
 type STuple4 a b c d = SBV (a, b, c, d)
 type STuple5 a b c d e = SBV (a, b, c, d, e)
 type STuple6 a b c d e f = SBV (a, b, c, d, e, f)
 type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)
 type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)
 class SymArray array where
 newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) > Symbolic (array a b)
 newArray :: (SymArray array, HasKind a, HasKind b) => String > Maybe (SBV b) > Symbolic (array a b)
 data SArray a b
 data SFunArray a b
 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
 sChar :: String > Symbolic SChar
 sString :: String > Symbolic SString
 sList :: SymVal a => String > Symbolic (SList a)
 sTuple :: SymVal tup => String > Symbolic (SBV tup)
 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]
 sChars :: [String] > Symbolic [SChar]
 sStrings :: [String] > Symbolic [SString]
 sLists :: SymVal a => [String] > Symbolic [SList a]
 sTuples :: SymVal tup => [String] > Symbolic [SBV tup]
 class EqSymbolic a where
 class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
 class Equality a where
 class Mergeable a where
 ite :: Mergeable a => SBool > a > a > a
 iteLazy :: Mergeable a => SBool > a > a > a
 class (SymVal a, Num a, Bits a, Integral a) => SIntegral a
 class SDivisible a where
 sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a > SBV b
 sShiftLeft :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sShiftRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a
 sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a > SBV b > SBV a
 sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a > SBV b > SBV a
 sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a > SBV b > SBV a
 class (SymVal a, Num a, Bits a) => SFiniteBits a where
 sFiniteBitSize :: SBV a > Int
 lsb :: SBV a > SBool
 msb :: SBV a > SBool
 blastBE :: SBV a > [SBool]
 blastLE :: SBV a > [SBool]
 fromBitsBE :: [SBool] > SBV a
 fromBitsLE :: [SBool] > SBV a
 sTestBit :: SBV a > Int > SBool
 sExtractBits :: SBV a > [Int] > [SBool]
 sPopCount :: SBV a > SWord8
 setBitTo :: SBV a > Int > SBool > SBV a
 fullAdder :: SBV a > SBV a > (SBool, SBV a)
 fullMultiplier :: SBV a > SBV a > (SBV a, SBV a)
 sCountLeadingZeros :: SBV a > SWord8
 sCountTrailingZeros :: SBV a > SWord8
 class Splittable a b  b > a where
 (.^) :: (Mergeable b, Num b, SIntegral e) => b > SBV e > b
 class (SymVal a, RealFloat a) => IEEEFloating a where
 fpAbs :: SBV a > SBV a
 fpNeg :: SBV a > SBV a
 fpAdd :: SRoundingMode > SBV a > SBV a > SBV a
 fpSub :: SRoundingMode > SBV a > SBV a > SBV a
 fpMul :: SRoundingMode > SBV a > SBV a > SBV a
 fpDiv :: SRoundingMode > SBV a > SBV a > SBV a
 fpFMA :: SRoundingMode > SBV a > SBV a > SBV a > SBV a
 fpSqrt :: SRoundingMode > SBV a > SBV a
 fpRem :: SBV a > SBV a > SBV a
 fpRoundToIntegral :: SRoundingMode > SBV a > SBV a
 fpMin :: SBV a > SBV a > SBV a
 fpMax :: SBV a > SBV a > SBV a
 fpIsEqualObject :: SBV a > SBV a > SBool
 fpIsNormal :: SBV a > SBool
 fpIsSubnormal :: SBV a > SBool
 fpIsZero :: SBV a > SBool
 fpIsInfinite :: SBV a > SBool
 fpIsNaN :: SBV a > SBool
 fpIsNegative :: SBV a > SBool
 fpIsPositive :: SBV a > SBool
 fpIsNegativeZero :: SBV a > SBool
 fpIsPositiveZero :: SBV a > SBool
 fpIsPoint :: SBV a > SBool
 data RoundingMode
 type SRoundingMode = SBV RoundingMode
 nan :: Floating a => a
 infinity :: Floating a => a
 sNaN :: (Floating a, SymVal a) => SBV a
 sInfinity :: (Floating a, SymVal a) => SBV a
 sRoundNearestTiesToEven :: SRoundingMode
 sRoundNearestTiesToAway :: SRoundingMode
 sRoundTowardPositive :: SRoundingMode
 sRoundTowardNegative :: SRoundingMode
 sRoundTowardZero :: SRoundingMode
 sRNE :: SRoundingMode
 sRNA :: SRoundingMode
 sRTP :: SRoundingMode
 sRTN :: SRoundingMode
 sRTZ :: SRoundingMode
 class IEEEFloatConvertable a where
 fromSFloat :: SRoundingMode > SFloat > SBV a
 toSFloat :: SRoundingMode > SBV a > SFloat
 fromSDouble :: SRoundingMode > SDouble > SBV a
 toSDouble :: SRoundingMode > SBV a > SDouble
 sFloatAsSWord32 :: SFloat > SWord32
 sWord32AsSFloat :: SWord32 > SFloat
 sDoubleAsSWord64 :: SDouble > SWord64
 sWord64AsSDouble :: SWord64 > SDouble
 blastSFloat :: SFloat > (SBool, [SBool], [SBool])
 blastSDouble :: SDouble > (SBool, [SBool], [SBool])
 mkSymbolicEnumeration :: Name > Q [Dec]
 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
 type Goal = Symbolic ()
 type Provable = MProvable IO
 forAll_ :: Provable a => a > Symbolic SBool
 forAll :: Provable a => [String] > a > Symbolic SBool
 forSome_ :: Provable a => a > Symbolic SBool
 forSome :: Provable a => [String] > a > Symbolic SBool
 prove :: Provable a => a > IO ThmResult
 proveWith :: Provable a => SMTConfig > a > IO ThmResult
 sat :: Provable a => a > IO SatResult
 satWith :: Provable a => SMTConfig > a > IO SatResult
 allSat :: Provable a => a > IO AllSatResult
 allSatWith :: Provable a => SMTConfig > a > IO AllSatResult
 optimize :: Provable a => OptimizeStyle > a > IO OptimizeResult
 optimizeWith :: Provable a => SMTConfig > OptimizeStyle > a > IO OptimizeResult
 isVacuous :: Provable a => a > IO Bool
 isVacuousWith :: Provable a => SMTConfig > a > IO Bool
 isTheorem :: Provable a => a > IO Bool
 isTheoremWith :: Provable a => SMTConfig > a > IO Bool
 isSatisfiable :: Provable a => a > IO Bool
 isSatisfiableWith :: Provable a => SMTConfig > a > IO Bool
 proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, ThmResult)]
 proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, ThmResult)
 satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, SatResult)]
 satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, SatResult)
 generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool > a > m String
 solve :: [SBool] > Symbolic SBool
 constrain :: SolverContext m => SBool > m ()
 softConstrain :: SolverContext m => SBool > m ()
 namedConstraint :: SolverContext m => String > SBool > m ()
 constrainWithAttribute :: SolverContext m => [(String, String)] > SBool > m ()
 pbAtMost :: [SBool] > Int > SBool
 pbAtLeast :: [SBool] > Int > SBool
 pbExactly :: [SBool] > Int > SBool
 pbLe :: [(Int, SBool)] > Int > SBool
 pbGe :: [(Int, SBool)] > Int > SBool
 pbEq :: [(Int, SBool)] > Int > SBool
 pbMutexed :: [SBool] > SBool
 pbStronglyMutexed :: [SBool] > SBool
 sAssert :: HasKind a => Maybe CallStack > String > SBool > SBV a > SBV a
 isSafe :: SafeResult > Bool
 class ExtractIO m => SExecutable m a
 sName_ :: SExecutable IO a => a > Symbolic ()
 sName :: SExecutable IO a => [String] > a > Symbolic ()
 safe :: SExecutable IO a => a > IO [SafeResult]
 safeWith :: SExecutable IO a => SMTConfig > a > IO [SafeResult]
 sbvQuickCheck :: Symbolic SBool > IO Bool
 data OptimizeStyle
 = Lexicographic
  Independent
  Pareto (Maybe Int)
 data Objective a
 class Metric a
 minimize :: Metric a => String > a > Symbolic ()
 maximize :: Metric a => String > a > Symbolic ()
 assertWithPenalty :: String > SBool > Penalty > Symbolic ()
 data Penalty
 data ExtCV
 data GeneralizedCV
 newtype ThmResult = ThmResult SMTResult
 newtype SatResult = SatResult SMTResult
 newtype AllSatResult = AllSatResult (Bool, Bool, [SMTResult])
 newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
 data OptimizeResult
 data SMTResult
 data SMTReasonUnknown
 observe :: SymVal a => String > SBV a > SBV a
 observeIf :: SymVal a => (a > Bool) > String > SBV a > SBV a
 class SatModel a where
 class Modelable a where
 modelExists :: a > Bool
 getModelAssignment :: SatModel b => a > Either String (Bool, b)
 getModelDictionary :: a > Map String CV
 getModelValue :: SymVal b => String > a > Maybe b
 getModelUninterpretedValue :: String > a > Maybe String
 extractModel :: SatModel b => a > Maybe b
 getModelObjectives :: a > Map String GeneralizedCV
 getModelObjectiveValue :: String > a > Maybe GeneralizedCV
 displayModels :: SatModel a => (Int > (Bool, a) > IO ()) > AllSatResult > IO Int
 extractModels :: SatModel a => AllSatResult > [a]
 getModelDictionaries :: AllSatResult > [Map String CV]
 getModelValues :: SymVal b => String > AllSatResult > [Maybe b]
 getModelUninterpretedValues :: String > AllSatResult > [Maybe String]
 data SMTConfig = SMTConfig {
 verbose :: Bool
 timing :: Timing
 printBase :: Int
 printRealPrec :: Int
 satCmd :: String
 allSatMaxModelCount :: Maybe Int
 isNonModelVar :: String > Bool
 transcript :: Maybe FilePath
 smtLibVersion :: SMTLibVersion
 solver :: SMTSolver
 roundingMode :: RoundingMode
 solverSetOptions :: [SMTOption]
 ignoreExitCode :: Bool
 redirectVerbose :: Maybe FilePath
 data Timing
 data SMTLibVersion = SMTLib2
 data Solver
 data SMTSolver = SMTSolver {
 name :: Solver
 executable :: String
 preprocess :: String > String
 options :: SMTConfig > [String]
 engine :: SMTEngine
 capabilities :: SolverCapabilities
 boolector :: SMTConfig
 cvc4 :: SMTConfig
 yices :: SMTConfig
 z3 :: SMTConfig
 mathSAT :: SMTConfig
 abc :: SMTConfig
 defaultSolverConfig :: Solver > SMTConfig
 defaultSMTCfg :: SMTConfig
 sbvCheckSolverInstallation :: SMTConfig > IO Bool
 sbvAvailableSolvers :: IO [SMTConfig]
 setLogic :: SolverContext m => Logic > m ()
 data Logic
 setOption :: SolverContext m => SMTOption > m ()
 setInfo :: SolverContext m => String > [String] > m ()
 setTimeOut :: SolverContext m => Integer > m ()
 data SBVException = SBVException {
 sbvExceptionDescription :: String
 sbvExceptionSent :: Maybe String
 sbvExceptionExpected :: Maybe String
 sbvExceptionReceived :: Maybe String
 sbvExceptionStdOut :: Maybe String
 sbvExceptionStdErr :: Maybe String
 sbvExceptionExitCode :: Maybe ExitCode
 sbvExceptionConfig :: SMTConfig
 sbvExceptionReason :: Maybe [String]
 sbvExceptionHint :: Maybe [String]
 data SBV a
 class HasKind a where
 kindOf :: a > Kind
 hasSign :: a > Bool
 intSizeOf :: a > Int
 isBoolean :: a > Bool
 isBounded :: a > Bool
 isReal :: a > Bool
 isFloat :: a > Bool
 isDouble :: a > Bool
 isInteger :: a > Bool
 isUninterpreted :: a > Bool
 isChar :: a > Bool
 isString :: a > Bool
 isList :: a > Bool
 isTuple :: a > Bool
 showType :: a > String
 data Kind
 class (HasKind a, Ord a, Typeable a) => SymVal a
 forall :: SymVal a => String > Symbolic (SBV a)
 forall_ :: SymVal a => Symbolic (SBV a)
 mkForallVars :: SymVal a => Int > Symbolic [SBV a]
 exists :: SymVal a => String > Symbolic (SBV a)
 exists_ :: SymVal a => Symbolic (SBV a)
 mkExistVars :: SymVal a => Int > Symbolic [SBV a]
 free :: SymVal a => String > Symbolic (SBV a)
 free_ :: SymVal a => Symbolic (SBV a)
 mkFreeVars :: SymVal a => Int > Symbolic [SBV a]
 symbolic :: SymVal a => String > Symbolic (SBV a)
 symbolics :: SymVal a => [String] > Symbolic [SBV a]
 literal :: SymVal a => a > SBV a
 unliteral :: SymVal a => SBV a > Maybe a
 fromCV :: SymVal a => CV > a
 isConcrete :: SymVal a => SBV a > Bool
 isSymbolic :: SymVal a => SBV a > Bool
 isConcretely :: SymVal a => SBV a > (a > Bool) > Bool
 mkSymVal :: SymVal a => Maybe Quantifier > Maybe String > Symbolic (SBV a)
 class MonadIO m => MonadSymbolic m where
 symbolicEnv :: m State
 type Symbolic = SymbolicT IO
 data SymbolicT m a
 label :: SymVal a => String > SBV a > SBV a
 output :: Outputtable a => a > Symbolic a
 runSMT :: Symbolic a > IO a
 runSMTWith :: SMTConfig > Symbolic a > IO a
 module Data.Bits
 module Data.Word
 module Data.Int
 module Data.Ratio
Documentation
The SBV library is really two things:
 A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
 A framework for proving properties of such programs using SMT solvers.
The programming goal of SBV is to provide a seamless experience, i.e., let people program
in the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the Num
and Bits
classes simplify coding), it makes life harder
in others. For instance, ifthenelse
only takes Bool
as a test in Haskell, and
comparisons (>
etc.) only return Bool
s. Clearly we would like these values to be
symbolic (i.e., SBool
), thus stopping us from using some native Haskell constructs.
When symbolic versions of operators are needed, they are typically obtained by prepending a dot,
for instance ==
becomes .==
. Care has been taken to make the transition painless. In
particular, any Haskell program you build out of symbolic components is fully concretely
executable within Haskell, without the need for any custom interpreters. (They are truly
Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated
feel of the system, one of the original design goals for SBV.
Incremental query mode: SBV provides a wide variety of ways to utilize SMTsolvers, without requiring the user to deal with the solvers themselves. While this mode is convenient, advanced users might need access to the underlying solver at a lower level. For such use cases, SBV allows users to have an interactive session: The user can issue commands to the solver, inspect the values/results, and formulate new constraints. This advanced feature is available through the Data.SBV.Control module, where most SMTLib features are made available via a typedAPI.
Symbolic types
Booleans
Boolean values and functions
oneIf :: (Num a, SymVal a) => SBool > SBV a Source #
Returns 1 if the boolean is sTrue
, otherwise 0.
Logical aggregations
Bitvectors
Unsigned bitvectors
Signed bitvectors
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.
Floating point numbers
Floating point numbers are defined by the IEEE754 standard; and correspond to Haskell's
Float
and Double
types. For SMT support with floatingpoint numbers, see the paper
by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smtfpa.pdf.
Algebraic reals
Algebraic reals are roots of singlevariable polynomials with rational coefficients. (See
http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite
precision numbers, but they do not cover all real numbers. (In particular, they cannot
represent transcendentals.) Some irrational numbers are algebraic (such as sqrt 2
), while
others are not (such as pi and e).
SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://smtlib.cs.uiowa.edu/theoriesReals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve nonlinear equations involving realvariables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)
Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the rootsofpolynomials are represented implicitly by their defining equation
Instances
sRealToSInteger :: SReal > SInteger Source #
Convert an SReal to an SInteger. That is, it computes the
largest integer n
that satisfies sIntegerToSReal n <= r
essentially giving us the floor
.
For instance, 1.3
will be 1
, but 1.3
will be 2
.
Characters, Strings and Regular Expressions
Support for characters, strings, and regular expressions (intial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theoriesUnicodeStrings.shtml and here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.
See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for related functions.
type SChar = SBV Char Source #
A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
is currently an 8bit unsigned value, corresponding to the ISO88591 (Latin1) character
set: http://en.wikipedia.org/wiki/ISO/IEC_88591. A Haskell Char
, on the other hand, is based
on unicode. Therefore, there isn't a 11 correspondence between a Haskell character and an SBV
character for the time being. This limitation is due to the SMTsolvers only supporting this
particular subset. However, there is a pending proposal to add support for unicode, and SBV
will track these changes to have full unicode support as solvers become available. For
details, see: http://smtlib.cs.uiowa.edu/theoriesUnicodeStrings.shtml
type SString = SBV String Source #
A symbolic string. Note that a symbolic string is not a list of symbolic characters,
that is, it is not the case that SString = [SChar]
, unlike what one might expect following
Haskell strings. An SString
is a symbolic value of its own, of possibly arbitrary but finite length,
and internally processed as one unit as opposed to a fixedlength list of characters.
Symbolic lists
Support for symbolic lists (intial version contributed by Joel Burget) adds support for sequence support, described here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.
See Data.SBV.List for related functions.
type SList a = SBV [a] Source #
A symbolic list of items. Note that a symbolic list is not a list of symbolic items,
that is, it is not the case that SList a = [a]
, unlike what one might expect following
haskell lists/sequences. An SList
is a symbolic value of its own, of possibly arbitrary but finite
length, and internally processed as one unit as opposed to a fixedlength list of items.
Note that lists can be nested, i.e., we do allow lists of lists of ... items.
Tuples
Tuples can be used as symbolic values. This is useful in combination with lists, for example SBV [(Integer, String)]
is a valid type. These types can be arbitrarily nested, eg SBV [(Integer, [(Char, (Integer, String))])]
. Instances of upto 8tuples are provided.
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
.SBV
b
If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.
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. Note that there are a few differences between these two models in
terms of use models:
SArray
produces SMTLib arrays, and requires a solver that understands the array theory.SFunArray
is internally handled, and thus can be used with any solver. (Note that all solvers exceptabc
support arrays, so this isn't a big decision factor.) For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
 Only
SArray
supports checking equality of arrays. (That is, checking if an entire array is equivalent to another.)SFunArray
s cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible.  Only
SFunArray
supports compilation to C. Programs usingSArray
will not be accepted by the Ccode generator.  You cannot use quickcheck on programs that contain these arrays. (Neither
SArray
norSFunArray
.)  With
SArray
, SBV transfers all arrayprocessing to the SMTsolver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. WithSFunArray
, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.
As a rule of thumb, try SArray
first. These should generate compact code. However, if
the backend solver has hard time solving the generated problems, switch to
SFunArray
. If you still have issues, please report so we can see what the problem might be!
readArray :: array a b > SBV a > SBV b Source #
Read the array element at a
writeArray :: SymVal b => array a b > SBV a > SBV b > array a b Source #
Update the element at a
to be b
mergeArrays :: SymVal b => SBV Bool > array a b > array a b > array a b Source #
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b
.
Merging pushes the ifthenelse choice down on to elements
Instances
newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) > Symbolic (array a b) Source #
Create a new anonymous array, possibly with a default initial value.
NB. For a version which generalizes over the underlying monad, see newArray_
newArray :: (SymArray array, HasKind a, HasKind b) => String > Maybe (SBV b) > Symbolic (array a b) Source #
Create a named new array, possibly with a default initial value.
NB. For a version which generalizes over the underlying monad, see newArray
Arrays implemented in terms of SMTarrays: http://smtlib.cs.uiowa.edu/theoriesArraysEx.shtml
 Maps directly to SMTlib arrays
 Reading from an unintialized value is OK. If the default value is given in
newArray
, it will be the result. Otherwise, the read yields an uninterpreted constant.  Can check for equality of these arrays
 Cannot be used in codegeneration (i.e., compilation to C)
 Cannot quickcheck theorems using
SArray
values  Typically slower as it heavily relies on SMTsolving for the array theory
Instances
Arrays implemented internally, without translating to SMTLib functions:
 Internally handled by the library and not mapped to SMTLib, hence can be used with solvers that don't support arrays. (Such as abc.)
 Reading from an unintialized value is OK. If the default value is given in
newArray
, it will be the result. Otherwise, the read yields an uninterpreted constant.  Cannot check for equality of arrays.
 Can be used in codegeneration (i.e., compilation to C).
 Can not quickcheck theorems using
SFunArray
values  Typically faster as it gets compiled away during translation.
Instances
Creating symbolic values
Single value
These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms
for free
(specialized at the given type), but they might be easier to use.
sTuple :: SymVal tup => String > Symbolic (SBV tup) Source #
Declare a tuple.
NB. For a version which generalizes over the underlying monad, see sTuple
List of values
These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms
for mapM
free
(specialized at the given type), but they might be easier to use.
sTuples :: SymVal tup => [String] > Symbolic [SBV tup] Source #
Declare a list of tuples.
NB. For a version which generalizes over the underlying monad, see sTuples
Symbolic Equality and Comparisons
class EqSymbolic a where Source #
Symbolic Equality. Note that we can't use Haskell's Eq
class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.
(.==) :: a > a > SBool infix 4 Source #
Symbolic equality.
(./=) :: a > a > SBool infix 4 Source #
Symbolic inequality.
distinct :: [a] > SBool Source #
Returns (symbolic) sTrue
if all the elements of the given list are different.
allEqual :: [a] > SBool Source #
Returns (symbolic) sTrue
if all the elements of the given list are the same.
sElem :: a > [a] > SBool Source #
Symbolic membership test.
Instances
EqSymbolic Bool Source #  
EqSymbolic a => EqSymbolic [a] Source #  
EqSymbolic a => EqSymbolic (Maybe a) Source #  
EqSymbolic (SBV a) Source #  
EqSymbolic a => EqSymbolic (S a) Source #  Symbolic equality for 
(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source #  
(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source #  
EqSymbolic (SArray a b) Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source #  
Defined in Data.SBV.Core.Model  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (./=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # distinct :: [(a, b, c, d, e, f)] > SBool Source # allEqual :: [(a, b, c, d, e, f)] > SBool Source # sElem :: (a, b, c, d, e, f) > [(a, b, c, d, e, f)] > SBool Source #  
(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source #  
Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (./=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # distinct :: [(a, b, c, d, e, f, g)] > SBool Source # allEqual :: [(a, b, c, d, e, f, g)] > SBool Source # sElem :: (a, b, c, d, e, f, g) > [(a, b, c, d, e, f, g)] > SBool Source # 
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #
Symbolic Comparisons. Similar to Eq
, we cannot implement Haskell's Ord
class
since there is no way to return an Ordering
value from a symbolic comparison.
Furthermore, OrdSymbolic
requires Mergeable
to implement ifthenelse, for the
benefit of implementing symbolic versions of max
and min
functions.
(.<) :: a > a > SBool infix 4 Source #
Symbolic less than.
(.<=) :: a > a > SBool infix 4 Source #
Symbolic less than or equal to.
(.>) :: a > a > SBool infix 4 Source #
Symbolic greater than.
(.>=) :: a > a > SBool infix 4 Source #
Symbolic greater than or equal to.
Symbolic minimum.
Symbolic maximum.
inRange :: a > (a, a) > SBool Source #
Is the value withing the allowed inclusive range?
Instances
OrdSymbolic a => OrdSymbolic [a] Source #  
OrdSymbolic a => OrdSymbolic (Maybe a) Source #  
Defined in Data.SBV.Core.Model  
SymVal a => OrdSymbolic (SBV a) Source #  
Defined in Data.SBV.Core.Model  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source #  
Defined in Data.SBV.Core.Model (.<) :: Either a b > Either a b > SBool Source # (.<=) :: Either a b > Either a b > SBool Source # (.>) :: Either a b > Either a b > SBool Source # (.>=) :: Either a b > Either a b > SBool Source # smin :: Either a b > Either a b > Either a b Source # smax :: Either a b > Either a b > Either a b Source # inRange :: Either a b > (Either a b, Either a b) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c) > (a, b, c) > SBool Source # (.<=) :: (a, b, c) > (a, b, c) > SBool Source # (.>) :: (a, b, c) > (a, b, c) > SBool Source # (.>=) :: (a, b, c) > (a, b, c) > SBool Source # smin :: (a, b, c) > (a, b, c) > (a, b, c) Source # smax :: (a, b, c) > (a, b, c) > (a, b, c) Source # inRange :: (a, b, c) > ((a, b, c), (a, b, c)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.<=) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.>) :: (a, b, c, d) > (a, b, c, d) > SBool Source # (.>=) :: (a, b, c, d) > (a, b, c, d) > SBool Source # smin :: (a, b, c, d) > (a, b, c, d) > (a, b, c, d) Source # smax :: (a, b, c, d) > (a, b, c, d) > (a, b, c, d) Source # inRange :: (a, b, c, d) > ((a, b, c, d), (a, b, c, d)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.<=) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.>) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # (.>=) :: (a, b, c, d, e) > (a, b, c, d, e) > SBool Source # smin :: (a, b, c, d, e) > (a, b, c, d, e) > (a, b, c, d, e) Source # smax :: (a, b, c, d, e) > (a, b, c, d, e) > (a, b, c, d, e) Source # inRange :: (a, b, c, d, e) > ((a, b, c, d, e), (a, b, c, d, e)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.<=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.>) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # (.>=) :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > SBool Source # smin :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > (a, b, c, d, e, f) Source # smax :: (a, b, c, d, e, f) > (a, b, c, d, e, f) > (a, b, c, d, e, f) Source # inRange :: (a, b, c, d, e, f) > ((a, b, c, d, e, f), (a, b, c, d, e, f)) > SBool Source #  
(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source #  
Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.<=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.>) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # (.>=) :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > SBool Source # smin :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) Source # smax :: (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) > (a, b, c, d, e, f, g) Source # inRange :: (a, b, c, d, e, f, g) > ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) > SBool Source # 
class Equality a where Source #
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bitprecise proofs.
Instances
Conditionals: Mergeable values
class Mergeable a where Source #
Symbolic conditionals are modeled by the Mergeable
class, describing
how to merge the results of an ifthenelse call with a symbolic test. SBV
provides all basic types as instances of this class, so users only need
to declare instances for custom datatypes of their programs as needed.
A Mergeable
instance may be automatically derived for a custom datatype
with a single constructor where the type of each field is an instance of
Mergeable
, such as a record of symbolic values. Users only need to add
Generic
and Mergeable
to the deriving
clause for the datatype. See
Status
for an example and an
illustration of what the instance would look like if written by hand.
The function select
is a totalindexing function out of a list of choices
with a default value, simulating array/list indexing. It's an nway generalization
of the ite
function.
Minimal complete definition: None, if the type is instance of Generic
. Otherwise
symbolicMerge
. Note that most types subject to merging are likely to be
trivial instances of Generic
.
Nothing
symbolicMerge :: Bool > SBool > a > a > a Source #
Merge two values based on the condition. The first argument states whether we force the thenandelse branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
select :: (SymVal b, Num b) => [a] > a > SBV b > a Source #
Total indexing operation. select xs default index
is intuitively
the same as xs !! index
, except it evaluates to default
if index
underflows/overflows.
symbolicMerge :: (Generic a, GMergeable (Rep a)) => Bool > SBool > a > a > a Source #
Merge two values based on the condition. The first argument states whether we force the 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.
Instances
ite :: Mergeable a => SBool > a > a > a Source #
Ifthenelse. This is by definition symbolicMerge
with both
branches forced. This is typically the desired behavior, but also
see iteLazy
should you need more laziness.
iteLazy :: Mergeable a => SBool > a > a > a Source #
A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.
Symbolic integral numbers
class (SymVal a, Num a, Bits a, Integral a) => SIntegral a Source #
Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic typesignatures that work for all
symbolic numbers, such as SWord8
, SInt8
etc. For instance, we can write a generic
listminimum function as follows:
mm :: SIntegral a => [SBV a] > SBV a mm = foldr1 (a b > ite (a .<= b) a b)
It is similar to the standard Integral
class, except ranging over symbolic instances.
Instances
SIntegral Int8 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int16 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int32 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Int64 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Integer Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word8 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word16 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word32 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word64 Source #  
Defined in Data.SBV.Core.Model  
SIntegral Word4 Source #  SIntegral instance, using default methods 
Defined in Documentation.SBV.Examples.Misc.Word4 
Division and Modulus
class SDivisible a where Source #
The SDivisible
class captures the essence of division.
Unfortunately we cannot use Haskell's Integral
class since the Real
and Enum
superclasses are not implementable for symbolic bitvectors.
However, quotRem
and divMod
both make perfect sense, and the SDivisible
class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following pair of laws:
xsQuotRem
0 = (0, x) xsDivMod
0 = (0, x)
Note that our instances implement this law even when x
is 0
itself.
NB. quot
truncates toward zero, while div
truncates toward negative infinity.
Instances
SDivisible Int8 Source #  
SDivisible Int16 Source #  
SDivisible Int32 Source #  
SDivisible Int64 Source #  
SDivisible Integer Source #  
SDivisible Word8 Source #  
SDivisible Word16 Source #  
Defined in Data.SBV.Core.Model  
SDivisible Word32 Source #  
Defined in Data.SBV.Core.Model  
SDivisible Word64 Source #  
Defined in Data.SBV.Core.Model  
SDivisible CV Source #  
SDivisible SInteger Source #  
Defined in Data.SBV.Core.Model  
SDivisible SInt64 Source #  
Defined in Data.SBV.Core.Model  
SDivisible SInt32 Source #  
Defined in Data.SBV.Core.Model  
SDivisible SInt16 Source #  
Defined in Data.SBV.Core.Model  
SDivisible SInt8 Source #  
SDivisible SWord64 Source #  
SDivisible SWord32 Source #  
SDivisible SWord16 Source #  
SDivisible SWord8 Source #  
Defined in Data.SBV.Core.Model  
SDivisible SWord4 Source #  SDvisible instance, using default methods 
Defined in Documentation.SBV.Examples.Misc.Word4  
SDivisible Word4 Source #  SDvisible instance, using 0extension 
Defined in Documentation.SBV.Examples.Misc.Word4 
Bitvector operations
Conversions
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a > SBV b Source #
Conversion between integralsymbolic values, akin to Haskell's fromIntegral
Shifts and rotates
Symbolic words (both signed and unsigned) are an instance of Haskell's Bits
class, so regular
bitwise operations are automatically available for them. Shifts and rotates, however, require
specialized typesignatures since Haskell insists on an Int
second argument for them.
sShiftRight :: (SIntegral a, SIntegral b) => SBV a > SBV b > SBV a Source #
Generalization of shiftR
, when the shiftamount is symbolic. Since Haskell's
shiftR
only takes an Int
as the shift amount, it cannot be used when we have
a symbolic amount to shift with.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
following the usual Haskell convention. See sSignedShiftArithRight
for a variant
that explicitly uses the msb as the sign bit, even for unsigned underlying types.
sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a > SBV b > SBV a Source #
sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a > SBV b > SBV a Source #
sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a > SBV b > SBV a Source #
Arithmetic shiftright with a symbolic unsigned shift amount. This is equivalent
to sShiftRight
when the argument is signed. However, if the argument is unsigned,
then it explicitly treats its msb as a signbit, and uses it as the bit that
gets shifted in. Useful when using the underlying unsigned bit representation to implement
custom signed operations. Note that there is no direct Haskell analogue of this function.
Finite bitvector operations
class (SymVal a, Num a, Bits a) => SFiniteBits a where Source #
Finite bitlength symbolic values. Essentially the same as SIntegral
, but further leaves out Integer
. Loosely
based on Haskell's FiniteBits
class, but with more methods defined and structured differently to fit into the
symbolic world view. Minimal complete definition: sFiniteBitSize
.
sFiniteBitSize :: SBV a > Int Source #
Bit size.
lsb :: SBV a > SBool Source #
Least significant bit of a word, always stored at index 0.
msb :: SBV a > SBool Source #
Most significant bit of a word, always stored at the last position.
blastBE :: SBV a > [SBool] Source #
Bigendian blasting of a word into its bits.
blastLE :: SBV a > [SBool] Source #
Littleendian blasting of a word into its bits.
fromBitsBE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
fromBitsLE :: [SBool] > SBV a Source #
Reconstruct from given bits, given in littleendian.
sTestBit :: SBV a > Int > SBool Source #
sExtractBits :: SBV a > [Int] > [SBool] Source #
Variant of sTestBit
, where we want to extract multiple bit positions.
sPopCount :: SBV a > SWord8 Source #
Variant of popCount
, returning a symbolic value.
setBitTo :: SBV a > Int > SBool > SBV a Source #
fullAdder :: SBV a > SBV a > (SBool, SBV a) Source #
Full adder, returns carryout from the addition. Only for unsigned quantities.
fullMultiplier :: SBV a > SBV a > (SBV a, SBV a) Source #
Full multipler, returns both high and loworder bits. Only for unsigned quantities.
sCountLeadingZeros :: SBV a > SWord8 Source #
Count leading zeros in a word, bigendian interpretation.
sCountTrailingZeros :: SBV a > SWord8 Source #
Count trailing zeros in a word, bigendian interpretation.
Instances
Splitting, joining, and extending
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.
Instances
Splittable Word8 Word4 Source #  Joiningsplitting tofrom Word8 
Splittable Word16 Word8 Source #  
Splittable Word32 Word16 Source #  
Splittable Word64 Word32 Source #  
Splittable SWord64 SWord32 Source #  
Splittable SWord32 SWord16 Source #  
Splittable SWord16 SWord8 Source #  
Exponentiation
(.^) :: (Mergeable b, Num b, SIntegral e) => b > SBV e > b Source #
Symbolic exponentiation using bit blasting and repeated squaring.
N.B. The exponent must be unsigned/bounded if symbolic. Signed exponents will be rejected.
IEEEfloating point numbers
class (SymVal a, RealFloat a) => IEEEFloating a where Source #
A class of floatingpoint (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.
Nothing
fpAbs :: SBV a > SBV a Source #
Compute the floating point absolute value.
fpNeg :: SBV a > SBV a Source #
Compute the unary negation. Note that 0  x
is not equivalent to x
for floatingpoint, since 0
and 0
are different.
fpAdd :: SRoundingMode > SBV a > SBV a > SBV a Source #
Add two floating point values, using the given rounding mode
fpSub :: SRoundingMode > SBV a > SBV a > SBV a Source #
Subtract two floating point values, using the given rounding mode
fpMul :: SRoundingMode > SBV a > SBV a > SBV a Source #
Multiply two floating point values, using the given rounding mode
fpDiv :: SRoundingMode > SBV a > SBV a > SBV a Source #
Divide two floating point values, using the given rounding mode
fpFMA :: SRoundingMode > SBV a > SBV a > SBV a > SBV a Source #
Fusedmultiplyadd three floating point values, using the given rounding mode. fpFMA x y z = x*y+z
but with only
one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
Haskell lacks an FMA implementation.
fpSqrt :: SRoundingMode > SBV a > SBV a Source #
Compute the squareroot of a float, using the given rounding mode
fpRem :: SBV a > SBV a > SBV a Source #
Compute the remainder: x  y * n
, where n
is the truncated integer nearest to x/y. The rounding mode
is implicitly assumed to be RoundNearestTiesToEven
.
fpRoundToIntegral :: SRoundingMode > SBV a > SBV a Source #
Round to the nearest integral value, using the given rounding mode.
fpMin :: SBV a > SBV a > SBV a Source #
Compute the minimum of two floats, respects infinity
and NaN
values
fpMax :: SBV a > SBV a > SBV a Source #
Compute the maximum of two floats, respects infinity
and NaN
values
fpIsEqualObject :: SBV a > SBV a > SBool Source #
Are the two given floats exactly the same. That is, NaN
will compare equal to itself, +0
will not compare
equal to 0
etc. This is the object level equality, as opposed to the semantic equality. (For the latter, just use .==
.)
fpIsNormal :: SBV a > SBool Source #
Is the floatingpoint number a normal value. (i.e., not denormalized.)
fpIsSubnormal :: SBV a > SBool Source #
Is the floatingpoint number a subnormal value. (Also known as denormal.)
fpIsZero :: SBV a > SBool Source #
Is the floatingpoint number 0? (Note that both +0 and 0 will satisfy this predicate.)
fpIsInfinite :: SBV a > SBool Source #
Is the floatingpoint number infinity? (Note that both +oo and oo will satisfy this predicate.)
fpIsNaN :: SBV a > SBool Source #
Is the floatingpoint number a NaN value?
fpIsNegative :: SBV a > SBool Source #
Is the floatingpoint number negative? Note that 0 satisfies this predicate but +0 does not.
fpIsPositive :: SBV a > SBool Source #
Is the floatingpoint number positive? Note that +0 satisfies this predicate but 0 does not.
fpIsNegativeZero :: SBV a > SBool Source #
Is the floating point number 0?
fpIsPositiveZero :: SBV a > SBool Source #
Is the floating point number +0?
fpIsPoint :: SBV a > SBool Source #
Is the floatingpoint number a regular floating point, i.e., not NaN, nor +oo, nor oo. Normals or denormals are allowed.
Instances
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.) 
Instances
type SRoundingMode = SBV RoundingMode Source #
The symbolic variant of RoundingMode
Rounding modes
sRoundNearestTiesToEven :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToAway :: SRoundingMode Source #
Symbolic variant of RoundNearestTiesToAway
sRoundTowardPositive :: SRoundingMode Source #
Symbolic variant of RoundTowardPositive
sRoundTowardNegative :: SRoundingMode Source #
Symbolic variant of RoundTowardNegative
sRoundTowardZero :: SRoundingMode Source #
Symbolic variant of RoundTowardZero
sRNE :: SRoundingMode Source #
Alias for sRoundNearestTiesToEven
sRNA :: SRoundingMode Source #
Alias for sRoundNearestTiesToAway
sRTP :: SRoundingMode Source #
Alias for sRoundTowardPositive
sRTN :: SRoundingMode Source #
Alias for sRoundTowardNegative
sRTZ :: SRoundingMode Source #
Alias for sRoundTowardZero
Conversion to/from floats
class IEEEFloatConvertable a where Source #
Capture convertability from/to FloatingPoint representations
NB. fromSFloat
and fromSDouble
are underspecified when given
when given a NaN
, +oo
, or oo
value that cannot be represented
in the target domain. For these inputs, we define the result to be +0, arbitrarily.
fromSFloat :: SRoundingMode > SFloat > SBV a Source #
toSFloat :: SRoundingMode > SBV a > SFloat Source #
fromSDouble :: SRoundingMode > SDouble > SBV a Source #
Instances
Bitpattern conversions
sFloatAsSWord32 :: SFloat > SWord32 Source #
Convert an SFloat
to an SWord32
, preserving the bitcorrespondence. Note that since the
representation for NaN
s are not unique, this function will return a symbolic value when given a
concrete NaN
.
Implementation note: Since there's no corresponding function in SMTLib for conversion to bitrepresentation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In codegeneration mode, we simply map it to a simple conversion.
sWord32AsSFloat :: SWord32 > SFloat Source #
Reinterpret the bits in a 32bit word as a singleprecision floating point number
sDoubleAsSWord64 :: SDouble > SWord64 Source #
Convert an SDouble
to an SWord64
, preserving the bitcorrespondence. Note that since the
representation for NaN
s are not unique, this function will return a symbolic value when given a
concrete NaN
.
See the implementation note for sFloatAsSWord32
, as it applies here as well.
sWord64AsSDouble :: SWord64 > SDouble Source #
Reinterpret the bits in a 32bit word as a singleprecision floating point number
blastSFloat :: SFloat > (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a singleprecision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
blastSDouble :: SDouble > (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a singleprecision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
Enumerations
If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually translate that as just such a datatype to SMTLib, and will use the constructors as the inhabitants of the said sort. A simple example is:
data X = A  B  C mkSymbolicEnumeration ''X
Note the magic incantation mkSymbolicEnumeration ''X
. For this to work, you need to have the following
options turned on:
LANGUAGE TemplateHaskell LANGUAGE StandaloneDeriving LANGUAGE DeriveDataTypeable LANGUAGE DeriveAnyClass
Now, the user can define
type SX = SBV X
and treat SX
as a regular symbolic type ranging over the values A
, B
, and C
. Such values can be compared for equality, and with the usual
other comparison operators, such as .==
, ./=
, .>
, .>=
, <
, and <=
.
Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple query would look like:
allSat $ x > x .== (x :: SX)
which would list all three elements of this domain as satisfying solutions.
Solution #1: s0 = A :: X Solution #2: s0 = B :: X Solution #3: s0 = C :: X Found 3 different solutions.
Note that the result is properly typed as X
elements; these are not mere strings. So, in a getModelAssignment
scenario, the user can recover actual
elements of the domain and program further with those values as usual.
See Documentation.SBV.Examples.Misc.Enumerate for an extended example on how to use symbolic enumerations.
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, Show, Read, Data, SymVal, HasKind, SatModel)
(Note that you'll also need to use the language pragmas DeriveDataTypeable
, DeriveAnyClass
, and import Data.Generics
for the above to work.)
This is all it takes to introduce B
as an uninterpreted sort in SBV, which makes the type SBV B
automagically become available as the type
of symbolic values that ranges over B
values. Note that the ()
argument is important to distinguish it from enumerations, which will be
translated to proper SMT datatypes.
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.
Instances
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.
NB. For a version which generalizes over the underlying monad, see addAxiom
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://smtlib.cs.uiowa.edu/) to communicate with arbitrary SMT solvers.
A note on reasoning in the presence of quantifers
Note that SBV allows reasoning with quantifiers: Inputs can be existentially or universally quantified. Predicates can be built with arbitrary nesting of such quantifiers as well. However, SBV always assumes that the input is in prenexnormal form: http://en.wikipedia.org/wiki/Prenex_normal_form. That is, all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately, the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers. SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested quantification, you will manually have to first convert to prenexnormal form (which produces an equisatisfiable but not necessarily equivalent formula), and code that explicitly in SBV. See http://github.com/LeventErkok/sbv/issues/256 for a detailed discussion of this issue.
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.
SBV allows 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
) 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
) 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.
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.
type Goal = Symbolic () Source #
A goal is a symbolic program that returns no values. The idea is that the constraints/minmax goals will serve as appropriate directives for sat/prove calls.
forAll_ :: Provable a => a > Symbolic SBool 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
.
NB. For a version which generalizes over the underlying monad, see forAll_
forAll :: Provable a => [String] > a > Symbolic SBool 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.
NB. For a version which generalizes over the underlying monad, see forAll
prove :: Provable a => a > IO ThmResult Source #
Prove a predicate, using the default solver.
NB. For a version which generalizes over the underlying monad, see prove
proveWith :: Provable a => SMTConfig > a > IO ThmResult Source #
Prove the predicate using the given SMTsolver.
NB. For a version which generalizes over the underlying monad, see proveWith
sat :: Provable a => a > IO SatResult Source #
Find a satisfying assignment for a predicate, using the default solver.
NB. For a version which generalizes over the underlying monad, see sat
satWith :: Provable a => SMTConfig > a > IO SatResult Source #
Find a satisfying assignment using the given SMTsolver.
NB. For a version which generalizes over the underlying monad, see satWith
allSat :: Provable a => a > IO AllSatResult Source #
Find all satisfying assignments, using the default solver.
Equivalent to
. See allSatWith
defaultSMTCfg
allSatWith
for details.
NB. For a version which generalizes over the underlying monad, see allSat
allSatWith :: Provable a => SMTConfig > a > IO AllSatResult Source #
Return all satisfying assignments for a predicate.
Note that this call will block until all satisfying assignments are found. If you have a problem
with infinitely many satisfying models (consider SInteger
) or a very large number of them, you
might have to wait for a long time. To avoid such cases, use the allSatMaxModelCount
parameter in the configuration.
NB. Uninterpreted constant/function values and counterexamples for array values are ignored for
the purposes of allSat
. That is, only the satisfying assignments modulo uninterpreted functions and
array inputs will be returned. This is due to the limitation of not having a robust means of getting a
function counterexample back from the SMT solver.
Find all satisfying assignments using the given SMTsolver
NB. For a version which generalizes over the underlying monad, see allSatWith
optimize :: Provable a => OptimizeStyle > a > IO OptimizeResult Source #
optimizeWith :: Provable a => SMTConfig > OptimizeStyle > a > IO OptimizeResult Source #
Optimizes the objectives using the given SMTsolver.
NB. For a version which generalizes over the underlying monad, see optimizeWith
isVacuous :: Provable a => a > IO Bool Source #
Check if the constraints given are consistent, using the default solver.
NB. For a version which generalizes over the underlying monad, see isVacuous
isVacuousWith :: Provable a => SMTConfig > a > IO Bool Source #
Determine if the constraints are vacuous using the given SMTsolver.
NB. For a version which generalizes over the underlying monad, see isVacuousWith
isTheorem :: Provable a => a > IO Bool Source #
Checks theoremhood using the default solver.
NB. For a version which generalizes over the underlying monad, see isTheorem
isTheoremWith :: Provable a => SMTConfig > a > IO Bool Source #
Check whether a given property is a theorem.
NB. For a version which generalizes over the underlying monad, see isTheoremWith
isSatisfiable :: Provable a => a > IO Bool Source #
Checks satisfiability using the default solver.
NB. For a version which generalizes over the underlying monad, see isSatisfiable
isSatisfiableWith :: Provable a => SMTConfig > a > IO Bool Source #
Check whether a given property is satisfiable.
NB. For a version which generalizes over the underlying monad, see isSatisfiableWith
proveWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, ThmResult)] Source #
Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
proveWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, ThmResult) Source #
Prove a property with multiple solvers, running them in separate threads. Only
the result of the first one to finish will be returned, remaining threads will be killed.
Note that we send a ThreadKilled
to the losing processes, but we do *not* actually wait for them
to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
that some processes take their time to terminate. So, this solution favors quick turnaround.
satWithAll :: Provable a => [SMTConfig] > a > IO [(Solver, NominalDiffTime, SatResult)] Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.
satWithAny :: Provable a => [SMTConfig] > a > IO (Solver, NominalDiffTime, SatResult) Source #
Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only
the result of the first one to finish will be returned, remaining threads will be killed.
Note that we send a ThreadKilled
to the losing processes, but we do *not* actually wait for them
to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
that some processes take their time to terminate. So, this solution favors quick turnaround.
generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool > a > m String Source #
Create an SMTLib2 benchmark. The Bool
argument controls whether this is a SAT instance, i.e.,
translate the query directly, or a PROVE instance, i.e., translate the negated query.
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:
sat $ do [x, y, z] < sIntegers ["x", "y", "z"] solve [x .> 5, y + z .< x]
NB. For a version which generalizes over the underlying monad, see solve
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
sFalse
constrain :: SolverContext m => SBool > m () Source #
Add a constraint, any satisfying instance must satisfy this condition
softConstrain :: SolverContext m => SBool > m () Source #
Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot
Constraint Vacuity
When adding constraints, one has to be careful about
making sure they are not inconsistent. The function isVacuous
can be use for this purpose.
Here is an example. Consider the following predicate:
>>>
let pred = do { x < free "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }
This predicate asserts that all 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 < free "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }
This time the proof passes as expected:
>>>
prove pred'
Q.E.D.
And the proof is not vacuous:
>>>
isVacuous pred'
False
Named constraints and attributes
Constraints can be given names:
namedConstraint
"a is at least 5" $ a .>= 5
Similarly, arbitrary term attributes can also be associated:
constrainWithAttribute
[(":solverspecificattribute", "value")] $ a .>= 5
Note that a namedConstraint
is equivalent to a constrainWithAttribute
call, setting the `":named"' attribute.
namedConstraint :: SolverContext m => String > SBool > m () Source #
Add a named constraint. The name is used in unsatcore extraction.
constrainWithAttribute :: SolverContext m => [(String, String)] > SBool > m () Source #
Add a constraint, with arbitrary attributes. Used in interpolant generation.
Unsat cores
Named constraints are useful when used in conjunction with getUnsatCore
function
where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable.
See getUnsatCore
for details and Documentation.SBV.Examples.Queries.UnsatCore for an example use case.
Cardinality constraints
A pseudoboolean function (http://en.wikipedia.org/wiki/PseudoBoolean_function) is a
function from booleans to reals, basically treating True
as 1
and False
as 0
. They
are typically expressed in polynomial form. Such functions can be used to express cardinality
constraints, where we want to count how many things satisfy a certain condition.
One can code such constraints using regular SBV programming: Simply walk over the booleans and the corresponding coefficients, and assert the required relation. For instance:
[b0, b1, b2, b3] `pbAtMost` 2
is precisely equivalent to:
sum (map (\b > ite b 1 0) [b0, b1, b2, b3]) .<= 2
and they both express that at most two of b0
, b1
, b2
, and b3
can be sTrue
.
However, the equivalent forms give rise to long formulas and the cardinality constraint
can get lost in the translation. The idea here is that if you use these functions instead, SBV will
produce better translations to SMTLib for more efficient solving of cardinality constraints, assuming
the backend solver supports them. Currently, only Z3 supports pseudobooleans directly. For all other solvers,
SBV will translate these to equivalent terms that do not require special functions.
Checking safety
The sAssert
function allows users to introduce invariants to make sure
certain properties hold at all times. This is another mechanism to provide further documentation/contract info
into SBV code. The functions safe
and safeWith
can be used to statically discharge these proof assumptions.
If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.
Here's a simple example. Let's assume we have a function that does subtraction, and requires its first argument to be larger than the second:
>>>
let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x  y)
Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument.
We can use safe
to statically see if such a violation is possible before we use this function elsewhere.
>>>
safe (sub :: SInt8 > SInt8 > SInt8)
[sub: x >= y must hold!: Violated. Model: s0 = 0 :: Int8 s1 = 1 :: Int8]
What happens if we make sure to arrange for this invariant? Consider this version:
>>>
let safeSub x y = ite (x .>= y) (sub x y) 0
Clearly, safeSub
must be safe. And indeed, SBV can prove that:
>>>
safe (safeSub :: SInt8 > SInt8 > SInt8)
[sub: x >= y must hold!: No violations detected]
Note how we used sub
and safeSub
polymorphically. We only need to monomorphise our types when a proof
attempt is done, as we did in the safe
calls.
If required, the user can pass a CallStack
through the first argument to sAssert
, which will be used
by SBV to print a diagnostic info to pinpoint the failure.
Also see Documentation.SBV.Examples.Misc.NoDiv0 for the classic divbyzero example.
sAssert :: HasKind a => Maybe CallStack > String > SBool > SBV a > SBV a Source #
Symbolic assert. Check that the given boolean condition is always sTrue
in the given path. The
optional first argument can be used to provide callstack info via GHC's location facilities.
isSafe :: SafeResult > Bool Source #
Check if a safecall was safe or not, turning a SafeResult
to a Bool.
class ExtractIO m => SExecutable m a 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.
Instances
sName_ :: SExecutable IO a => a > Symbolic () Source #
NB. For a version which generalizes over the underlying monad, see sName_
sName :: SExecutable IO a => [String] > a > Symbolic () Source #
NB. For a version which generalizes over the underlying monad, see sName
safe :: SExecutable IO a => a > IO [SafeResult] Source #
Check safety using the default solver.
NB. For a version which generalizes over the underlying monad, see safe
safeWith :: SExecutable IO a => SMTConfig > a > IO [SafeResult] Source #
Quickchecking
sbvQuickCheck :: Symbolic SBool > IO Bool Source #
Quick check an SBV property. Note that a regular quickCheck
call will work just as
well. Use this variant if you want to receive the boolean result.
Optimization
SBV can optimize metric functions, i.e., those that generate both bounded SIntN
, SWordN
, and unbounded SInteger
types, along with those produce SReal
s. That is, it can find models satisfying all the constraints while minimizing
or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend,
and a good review of these features is given
in this paper: http://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/nbjornerscss2014.pdf.
Goals can be lexicographically (default), independently, or paretofront optimized. The relevant functions are:
Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals).
For instance, a call of the form
minimize
"nameofgoal" $ x + 2*y
minimizes the arithmetic goal x+2*y
, where x
and y
can be signed/unsigned bitvectors, reals,
or integers.
A simple example
Here's an optimization example in action:
>>>
optimize Lexicographic $ \x y > minimize "goal" (x+2*(y::SInteger))
Optimal in an extension field: goal = oo :: Integer
We will describe the role of the constructor Lexicographic
shortly.
Of course, this becomes more useful when the result is not in an extension field:
>>>
:{
optimize Lexicographic $ do x < sInteger "x" y < sInteger "y" constrain $ x .> 0 constrain $ x .< 6 constrain $ y .> 2 constrain $ y .< 12 minimize "goal" $ x + 2 * y :} Optimal model: x = 1 :: Integer y = 3 :: Integer goal = 7 :: Integer
As usual, the programmatic API can be used to extract the values of objectives and modelvalues (getModelObjectives
,
getModelAssignment
, etc.) to access these values and program with them further.
The following examples illustrate the use of basic optimization routines:
 Documentation.SBV.Examples.Optimization.LinearOpt: Simple linearoptimization example.
 Documentation.SBV.Examples.Optimization.Production: Scheduling machines in a shop
 Documentation.SBV.Examples.Optimization.VM: Scheduling virtualmachines in a datacenter
Multiple optimization goals
Multiple goals can be specified, using the same syntax. In this case, the user gets to pick what style of
optimization to perform, by passing the relevant OptimizeStyle
as the first argument to optimize
.
 [
Lexicographic
]. The solver will optimize the goals in the given order, optimizing the latter ones under the model that optimizes the previous ones.  [
Independent
]. The solver will optimize the goals independently of each other. In this case the user will be presented a model for each goal given.  [
Pareto
]. Finally, the user can query for paretofronts. A pareto front is an model such that no goal can be made "better" without making some other goal "worse."
Pareto fronts only make sense when the objectives are bounded. If there are unbounded objective values, then the
backend solver can loop infinitely. (This is what z3 does currently.) If you are not sure the objectives are
bounded, you should first use Independent
mode to ensure the objectives are bounded, and then switch to
paretomode to extract them further.
The optional number argument to Pareto
specifies the maximum number of paretofronts the user is asking
to get. If Nothing
, SBV will query for all paretofronts. Note that paretofronts can be really large,
so if Nothing
is used, there is a potential for waiting indefinitely for the SBVsolver interaction to finish. (If
you suspect this might be the case, run in verbose
mode to see the interaction and put a limiting factor
appropriately.)
data OptimizeStyle Source #
Style of optimization. Note that in the pareto case the user is allowed
to specify a max number of fronts to query the solver for, since there might
potentially be an infinite number of them and there is no way to know exactly
how many ahead of time. If Nothing
is given, SBV will possibly loop forever
if the number is really infinite.
Lexicographic  Objectives are optimized in the order given, earlier objectives have higher priority. 
Independent  Each objective is optimized independently. 
Pareto (Maybe Int)  Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. 
Instances
Eq OptimizeStyle Source #  
Defined in Data.SBV.Core.Symbolic (==) :: OptimizeStyle > OptimizeStyle > Bool # (/=) :: OptimizeStyle > OptimizeStyle > Bool #  
Show OptimizeStyle Source #  
Defined in Data.SBV.Core.Symbolic showsPrec :: Int > OptimizeStyle > ShowS # show :: OptimizeStyle > String # showList :: [OptimizeStyle] > ShowS #  
NFData OptimizeStyle Source #  
Defined in Data.SBV.Core.Symbolic rnf :: OptimizeStyle > () # 
Objectives
Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.
Minimize String a  Minimize this metric 
Maximize String a  Maximize this metric 
AssertWithPenalty String a Penalty  A soft assertion, with an associated penalty 
Class of metrics we can optimize for. Currently, bounded signed/unsigned bitvectors, unbounded integers, and algebraic reals can be optimized. (But not, say, SFloat, SDouble, or SBool.) Minimal complete definition: minimize/maximize.
A good reference on these features is given in the following paper: http://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/nbjornerscss2014.pdf.
Instances
Metric SReal Source #  
Defined in Data.SBV.Core.Model  
Metric SInteger Source #  
Defined in Data.SBV.Core.Model  
Metric SInt64 Source #  
Defined in Data.SBV.Core.Model  
Metric SInt32 Source #  
Defined in Data.SBV.Core.Model  
Metric SInt16 Source #  
Defined in Data.SBV.Core.Model  
Metric SInt8 Source #  
Defined in Data.SBV.Core.Model  
Metric SWord64 Source #  
Defined in Data.SBV.Core.Model  
Metric SWord32 Source #  
Defined in Data.SBV.Core.Model  
Metric SWord16 Source #  
Defined in Data.SBV.Core.Model  
Metric SWord8 Source #  
Defined in Data.SBV.Core.Model 
minimize :: Metric a => String > a > Symbolic () Source #
Minimize a named metric
NB. For a version which generalizes over the underlying monad, see minimize
maximize :: Metric a => String > a > Symbolic () Source #
Maximize a named metric
NB. For a version which generalizes over the underlying monad, see maximize
Soft assertions
Related to optimization, SBV implements softasserts via assertWithPenalty
calls. A soft assertion
is a hint to the SMT solver that we would like a particular condition to hold if **possible*.
That is, if there is a solution satisfying it, then we would like it to hold, but it can be violated
if there is no way to satisfy it. Each softassertion can be associated with a numeric penalty for
not satisfying it, hence turning it into an optimization problem.
Note that assertWithPenalty
works well with optimization goals ('minimize'/'maximize' etc.),
and are most useful when we are optimizing a metric and thus some of the constraints
can be relaxed with a penalty to obtain a good solution. Again
see http://www.microsoft.com/enus/research/wpcontent/uploads/2016/02/nbjornerscss2014.pdf
for a good overview of the features in Z3 that SBV is providing the bridge for.
A soft assertion can be specified in one of the following three main ways:
assertWithPenalty
"bounded_x" (x .< 5)DefaultPenalty
assertWithPenalty
"bounded_x" (x .< 5) (Penalty
2.3 Nothing)assertWithPenalty
"bounded_x" (x .< 5) (Penalty
4.7 (Just "group1"))
In the first form, we are saying that the constraint x .< 5
must be satisfied, if possible,
but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.
In the second case, we are associating a penalty value of 2.3
.
Finally in the third case, we are also associating this constraint with a group. The group name is only needed if we have classes of softconstraints that should be considered together.
assertWithPenalty :: String > SBool > Penalty > Symbolic () Source #
Introduce a soft assertion, with an optional penalty
NB. For a version which generalizes over the underlying monad, see assertWithPenalty
Penalty for a softassertion. The default penalty is 1
, with all softassertions belonging
to the same objective goal. A positive weight and an optional group can be provided by using
the Penalty
constructor.
DefaultPenalty  Default: Penalty of 
Penalty Rational (Maybe String)  Penalty with a weight and an optional group 
Field extensions
If an optimization results in an infinity/epsilon value, the returned CV
value will be in the corresponding extension field.
A simple expression type over extendent values, covering infinity, epsilon and intervals.
Infinite Kind  
Epsilon Kind  
Interval ExtCV ExtCV  
BoundedCV CV  
AddExtCV ExtCV ExtCV  
MulExtCV ExtCV ExtCV 
Instances
Show ExtCV Source #  Show instance, shows with the kind 
HasKind ExtCV Source #  Kind instance for Extended CV 
Defined in Data.SBV.Core.Concrete kindOf :: ExtCV > Kind Source # hasSign :: ExtCV > Bool Source # intSizeOf :: ExtCV > Int Source # isBoolean :: ExtCV > Bool Source # isBounded :: ExtCV > Bool Source # isReal :: ExtCV > Bool Source # isFloat :: ExtCV > Bool Source # isDouble :: ExtCV > Bool Source # isInteger :: ExtCV > Bool Source # isUninterpreted :: ExtCV > Bool Source # isChar :: ExtCV > Bool Source # isString :: ExtCV > Bool Source # isList :: ExtCV > Bool Source # 
data GeneralizedCV Source #
A generalized CV allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
Instances
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.
Instances
Show ThmResult Source #  
NFData ThmResult Source #  
Defined in Data.SBV.SMT.SMT  
Modelable ThmResult Source # 

Defined in Data.SBV.SMT.SMT modelExists :: ThmResult > Bool Source # getModelAssignment :: SatModel b => ThmResult > Either String (Bool, b) Source # getModelDictionary :: ThmResult > Map String CV Source # getModelValue :: SymVal b => String > ThmResult > Maybe b Source # getModelUninterpretedValue :: String > ThmResult > Maybe String Source # extractModel :: SatModel b => ThmResult > Maybe b Source # getModelObjectives :: ThmResult > Map String GeneralizedCV Source # getModelObjectiveValue :: String > ThmResult > Maybe GeneralizedCV Source # 
A sat
call results in a SatResult
The reason for having a separate SatResult
is to have a more meaningful Show
instance.
Instances
Show SatResult Source #  
NFData SatResult Source #  
Defined in Data.SBV.SMT.SMT  
Modelable SatResult Source # 

Defined in Data.SBV.SMT.SMT modelExists :: SatResult > Bool Source # getModelAssignment :: SatModel b => SatResult > Either String (Bool, b) Source # getModelDictionary :: SatResult > Map String CV Source # getModelValue :: SymVal b => String > SatResult > Maybe b Source # getModelUninterpretedValue :: String > SatResult > Maybe String Source # extractModel :: SatModel b => SatResult > Maybe b Source # getModelObjectives :: SatResult > Map String GeneralizedCV Source # getModelObjectiveValue :: String > SatResult > Maybe GeneralizedCV Source # 
newtype AllSatResult Source #
An allSat
call results in a AllSatResult
. The first boolean says whether we
hit the maxmodel limit as we searched. The second boolean says whether
there were prefixexistentials.
AllSatResult (Bool, Bool, [SMTResult]) 
Instances
Show AllSatResult Source #  
Defined in Data.SBV.SMT.SMT showsPrec :: Int > AllSatResult > ShowS # show :: AllSatResult > String # showList :: [AllSatResult] > ShowS # 
newtype SafeResult Source #
A safe
call results in a SafeResult
Instances
Show SafeResult Source #  
Defined in Data.SBV.SMT.SMT showsPrec :: Int > SafeResult > ShowS # show :: SafeResult > String # showList :: [SafeResult] > ShowS # 
data OptimizeResult Source #
An optimize
call results in a OptimizeResult
. In the ParetoResult
case, the boolean is True
if we reached paretoquery limit and so there might be more unqueried results remaining. If False
,
it means that we have all the pareto fronts returned. See the Pareto
OptimizeStyle
for details.
LexicographicResult SMTResult  
ParetoResult (Bool, [SMTResult])  
IndependentResult [(String, SMTResult)] 
Instances
Show OptimizeResult Source #  
Defined in Data.SBV.SMT.SMT showsPrec :: Int > OptimizeResult > ShowS # show :: OptimizeResult > String # showList :: [OptimizeResult] > ShowS # 
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 (Maybe [String])  Unsatisfiable. If unsatcores are enabled, they will be returned in the second parameter. 
Satisfiable SMTConfig SMTModel  Satisfiable with model 
SatExtField SMTConfig SMTModel  Prover returned a model, but in an extension field containing Infinite/epsilon 
Unknown SMTConfig SMTReasonUnknown  Prover returned unknown, with the given reason 
ProofError SMTConfig [String]  Prover errored out 
Instances
NFData SMTResult Source #  
Defined in Data.SBV.Core.Symbolic  
Modelable SMTResult Source # 

Defined in Data.SBV.SMT.SMT modelExists :: SMTResult > Bool Source # getModelAssignment :: SatModel b => SMTResult > Either String (Bool, b) Source # getModelDictionary :: SMTResult > Map String CV Source # getModelValue :: SymVal b => String > SMTResult > Maybe b Source # getModelUninterpretedValue :: String > SMTResult > Maybe String Source # extractModel :: SatModel b => SMTResult > Maybe b Source # getModelObjectives :: SMTResult > Map String GeneralizedCV Source # getModelObjectiveValue :: String > SMTResult > Maybe GeneralizedCV Source # 
data SMTReasonUnknown Source #
Reason for reporting unknown.
Instances
Observing expressions
The observe
command can be used to trace values of arbitrary expressions during a sat
, prove
, or perhaps more
importantly, in a quickCheck
call. This is useful for, for instance, recording expected/obtained expressions as a symbolic program is executing.
>>>
:{
prove $ do a1 < free "i1" a2 < free "i2" let spec, res :: SWord8 spec = a1 + a2 res = ite (a1 .== 12 .&& a2 .== 22)  insert a malicious bug! 1 (a1 + a2) return $ observe "Expected" spec .== observe "Result" res :} Falsifiable. Counterexample: Expected = 34 :: Word8 Result = 1 :: Word8 i1 = 12 :: Word8 i2 = 22 :: Word8
The observeIf
variant allows the user to specify a boolean condition when the value is interesting to observe. Useful when
you have lots of "debugging" points, but not all are of interest.
observe :: SymVal a => String > SBV a > SBV a Source #
Observe the value of an expression, uncoditionally. See observeIf
for a generalized version.
observeIf :: SymVal a => (a > Bool) > String > SBV a > SBV a Source #
Observe the value of an expression, if the given condition holds. Such values are useful in model construction, as they are printed part of a satisfying model, or a
counterexample. The same works for quickcheck as well. Useful when we want to see intermediate values, or expected/obtained
pairs in a particular run. Note that an observed expression is always symbolic, i.e., it won't be constant folded. Compare this to label
which is used for putting a label in the generated SMTLibC code.
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.
class SatModel a where Source #
Instances of SatModel
can be automatically extracted from models returned by the
solvers. The idea is that the sbv infrastructure provides a stream of CV's (constant values)
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: parseCVs
Nothing
parseCVs :: [CV] > Maybe (a, [CV]) 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, [CV]) > Maybe (b, [CV]) 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.
parseCVs :: Read a => [CV] > Maybe (a, [CV]) 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
Instances
SatModel Bool Source # 

SatModel Double Source # 

SatModel Float Source # 

SatModel Int8 Source # 

SatModel Int16 Source # 

SatModel Int32 Source # 

SatModel Int64 Source # 

SatModel Integer Source # 

SatModel Word8 Source # 

SatModel Word16 Source # 

SatModel Word32 Source # 

SatModel Word64 Source # 

SatModel () Source #  Base case for 
SatModel AlgReal Source # 

SatModel CV Source # 

SatModel RoundingMode Source #  A rounding mode, extracted from a model. (Default definition suffices) 
Defined in Data.SBV.SMT.SMT  
SatModel State Source #  Make 
SatModel E Source #  Make 
SatModel Word4 Source #  SatModel instance, merely uses the generic parsing method. 