| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV
Contents
- Symbolic types
- Arrays of symbolic values
- Creating symbolic values
- Symbolic Equality and Comparisons
- Conditionals: Mergeable values
- Symbolic integral numbers
- Division and Modulus
- Bit-vector operations
- IEEE-floating point numbers
- Enumerations
- Uninterpreted sorts, constants, and functions
- Properties, proofs, and satisfiability
- Constraints
- Checking safety
- Quick-checking
- Optimization
- Model extraction
- SMT Interface
- Abstract SBV type
- Module exports
- Orphan instances
Description
(The sbv library is hosted at http://github.com/LeventErkok/sbv. Comments, bug reports, and patches are always welcome.)
SBV: SMT Based Verification
Express properties about Haskell programs and automatically prove them using SMT solvers.
>>>prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)Q.E.D.
>>>prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)Falsifiable. Counter-example: s0 = 32 :: Word8
The function prove has the following type:
prove::Provablea => a ->IOThmResult
The class Provable comes with instances for n-ary predicates, for arbitrary n.
The predicates are just regular Haskell functions over symbolic types listed below.
Functions for checking satisfiability (sat and allSat) are also
provided.
The sbv library introduces the following symbolic types:
SBool: Symbolic Booleans (bits).SWord8,SWord16,SWord32,SWord64: Symbolic Words (unsigned).SInt8,SInt16,SInt32,SInt64: Symbolic Ints (signed).SInteger: Unbounded signed integers.SReal: Algebraic-real numbersSFloat: IEEE-754 single-precision floating point valuesSDouble: IEEE-754 double-precision floating point valuesSString,RegExp: Strings and regular expressionsSArray,SFunArray: Flat arrays of symbolic values.- Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
- Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
- Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
The user can construct ordinary Haskell programs using these types, which behave
very similar to their concrete counterparts. In particular these types belong to the
standard classes Num, Bits, custom versions of Eq (EqSymbolic)
and Ord (OrdSymbolic), along with several other custom classes for simplifying
programming with symbolic values. The framework takes full advantage of Haskell's type
inference to avoid many common mistakes.
Furthermore, predicates (i.e., functions that return SBool) built out of
these types can also be:
- proven correct via an external SMT solver (the
provefunction) - checked for satisfiability (the
sat,allSatfunctions) - used in synthesis (the
satfunction with existentials) - quick-checked
If a predicate is not valid, prove will return a counterexample: An
assignment to inputs such that the predicate fails. The sat function will
return a satisfying assignment, if there is one. The allSat function returns
all satisfying assignments.
The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: http://smtlib.cs.uiowa.edu/
The SBV library is designed to work with any SMT-Lib compliant SMT-solver. Currently, we support the following SMT-Solvers out-of-the box:
- ABC from University of Berkeley: http://www.eecs.berkeley.edu/~alanmi/abc/
- CVC4 from New York University and University of Iowa: http://cvc4.cs.nyu.edu/
- Boolector from Johannes Kepler University: http://fmv.jku.at/boolector/
- MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: http://mathsat.fbk.eu/
- Yices from SRI: http://yices.csl.sri.com/
- Z3 from Microsoft: http://github.com/Z3Prover/z3/wiki
SBV requires recent versions of these solvers; please see the file
SMTSolverVersions.md in the source distribution for specifics.
SBV also allows calling these solvers in parallel, either getting results from multiple solvers
or returning the fastest one. (See proveWithAll, proveWithAny, etc.)
Support for other compliant solvers can be added relatively easily, please get in touch if there is a solver you'd like to see included.
- type SBool = SBV Bool
- oneIf :: (Num a, SymWord a) => SBool -> SBV a
- class Boolean b where
- bAnd :: Boolean b => [b] -> b
- bOr :: Boolean b => [b] -> b
- bAny :: Boolean b => (a -> b) -> [a] -> b
- bAll :: Boolean b => (a -> b) -> [a] -> b
- 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 SString = SBV String
- type SChar = SBV Char
- (.++) :: SString -> SString -> SString
- (.!!) :: SString -> SInteger -> SChar
- class SymArray array where
- data SArray a b
- data SFunArray a b
- mkSFunArray :: (SBV a -> SBV b) -> 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
- 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]
- 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 (SymWord a, Num a, Bits a, Integral a) => SIntegral a
- class SDivisible a where
- sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord 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 (SymWord a, Num a, Bits a) => SFiniteBits a where
- class Splittable a b | b -> a where
- (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
- class (SymWord a, RealFloat a) => IEEEFloating a where
- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymWord a) => SBV a
- sInfinity :: (Floating a, SymWord 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
- 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
- addAxiom :: String -> [String] -> Symbolic ()
- type Predicate = Symbolic SBool
- type Goal = Symbolic ()
- class Provable a where
- solve :: [SBool] -> Symbolic SBool
- constrain :: SolverContext m => SBool -> m ()
- namedConstraint :: SolverContext m => 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 :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a
- isSafe :: SafeResult -> Bool
- class SExecutable a where
- sbvQuickCheck :: Symbolic SBool -> IO Bool
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)
- data Objective a
- class Metric a where
- assertSoft :: String -> SBool -> Penalty -> Symbolic ()
- data Penalty
- data ExtCW
- data GeneralizedCW
- 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
- observe :: SymWord a => String -> SBV a -> Symbolic ()
- class SatModel a where
- class Modelable a where
- displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
- extractModels :: SatModel a => AllSatResult -> [a]
- getModelDictionaries :: AllSatResult -> [Map String CW]
- getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
- getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: 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
- 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 ()
- setOption :: SolverContext m => SMTOption -> m ()
- setInfo :: SolverContext m => String -> [String] -> m ()
- setTimeOut :: SolverContext m => Integer -> m ()
- data SMTException = SMTException {
- smtExceptionDescription :: String
- smtExceptionSent :: String
- smtExceptionExpected :: String
- smtExceptionReceived :: String
- smtExceptionStdOut :: String
- smtExceptionStdErr :: Maybe String
- smtExceptionExitCode :: Maybe ExitCode
- smtExceptionConfig :: SMTConfig
- smtExceptionReason :: Maybe [String]
- smtExceptionHint :: Maybe [String]
- data SBV a
- class HasKind a where
- data Kind
- class (HasKind a, Ord a) => SymWord a where
- data Symbolic a
- label :: SymWord a => String -> SBV a -> SBV a
- output :: Outputtable a => a -> Symbolic a
- runSMT :: Symbolic a -> IO a
- runSMTWith :: SMTConfig -> Symbolic a -> IO a
- module Data.Bits
- module Data.Word
- module Data.Int
- module Data.Ratio
Documentation
The SBV library is really two things:
- A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
- A framework for proving properties of such programs using SMT solvers.
The programming goal of SBV is to provide a seamless experience, i.e., let people program
in the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the Num and Bits classes simplify coding), it makes life harder
in others. For instance, if-then-else only takes Bool as a test in Haskell, and
comparisons (> etc.) only return Bools. Clearly we would like these values to be
symbolic (i.e., SBool), thus stopping us from using some native Haskell constructs.
When symbolic versions of operators are needed, they are typically obtained by prepending a dot,
for instance == becomes .==. Care has been taken to make the transition painless. In
particular, any Haskell program you build out of symbolic components is fully concretely
executable within Haskell, without the need for any custom interpreters. (They are truly
Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated
feel of the system, one of the original design goals for SBV.
Incremental query mode: SBV provides a wide variety of ways to utilize SMT-solvers, without requiring the user to deal with the solvers themselves. While this mode is convenient, advanced users might need access to the underlying solver at a lower level. For such use cases, SBV allows users to have an interactive session: The user can issue commands to the solver, inspect the values/results, and formulate new constraints. This advanced feature is available through the Data.SBV.Control module, where most SMTLib features are made available via a typed-API.
Symbolic types
Booleans
oneIf :: (Num a, SymWord a) => SBool -> SBV a Source #
Returns 1 if the boolean is true, otherwise 0.
The Boolean class
class Boolean b where Source #
The Boolean class: a generalization of Haskell's Bool type
Haskell Bool and SBV's SBool are instances of this class, unifying the treatment of boolean values.
Minimal complete definition: true, bnot, &&&
However, it's advisable to define false, and ||| as well (typically), for clarity.
Methods
logical true
logical false
complement
(&&&) :: b -> b -> b infixr 3 Source #
and
(|||) :: b -> b -> b infixr 2 Source #
or
(~&) :: b -> b -> b infixr 3 Source #
nand
(~|) :: b -> b -> b infixr 2 Source #
nor
(<+>) :: b -> b -> b infixl 6 Source #
xor
(==>) :: b -> b -> b infixr 1 Source #
implies
(<=>) :: b -> b -> b infixr 1 Source #
equivalence
fromBool :: Bool -> b Source #
cast from Bool
Logical operations
Bit-vectors
Unsigned bit-vectors
Signed bit-vectors
Unbounded integers
The SBV library supports unbounded signed integers with the type SInteger, which are not subject to
overflow/underflow as it is the case with the bounded types, such as SWord8, SInt16, etc. However,
some bit-vector based operations are not supported for the SInteger type while in the verification mode. That
is, you can use these operations on SInteger values during normal programming/simulation.
but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib.
Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size
bit-vectors. The operations that are restricted to bounded word/int sizes are:
- Rotations and shifts:
rotateL,rotateR,shiftL,shiftR - Bitwise logical ops:
.&.,.|.,xor,complement - Extraction and concatenation:
split,#, andextend(see theSplittableclass)
Usual arithmetic (+, -, *, sQuotRem, sQuot, sRem, sDivMod, sDiv, sMod) and logical operations (.<, .<=, .>, .>=, .==, ./=) operations are
supported for SInteger fully, both in programming and verification modes.
Floating point numbers
Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's
Float and Double types. For SMT support with floating-point numbers, see the paper
by Rummer and Wahl: http://www.philipp.ruemmer.org/publications/smt-fpa.pdf.
Algebraic reals
Algebraic reals are roots of single-variable polynomials with rational coefficients. (See
http://en.wikipedia.org/wiki/Algebraic_number.) Note that algebraic reals are infinite
precision numbers, but they do not cover all real numbers. (In particular, they cannot
represent transcendentals.) Some irrational numbers are algebraic (such as sqrt 2), while
others are not (such as pi and e).
SBV can deal with real numbers just fine, since the theory of reals is decidable. (See http://smtlib.cs.uiowa.edu/theories-Reals.shtml.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.)
Algebraic reals. Note that the representation is left abstract. We represent rational results explicitly, while the roots-of-polynomials are represented implicitly by their defining equation
Instances
| Eq AlgReal Source # | |
| Fractional AlgReal Source # | NB: Following the other types we have, we require `a/0` to be `0` for all a. |
| Num AlgReal Source # | |
| Ord AlgReal Source # | |
| Real AlgReal Source # | |
| Show AlgReal Source # | |
| Arbitrary AlgReal Source # | |
| Random AlgReal Source # | |
| HasKind AlgReal Source # | |
| SatModel AlgReal Source # |
|
| SMTValue AlgReal Source # | |
| Metric SReal Source # | |
| IEEEFloatConvertable AlgReal Source # | |
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.
Strings and Regular Expressions
Support for strings (intial version contributed by Joel Burget) adds support for QF_S logic, described here: https://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.
See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for further related functions.
type 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 length,
and internally processed as one unit as opposed to a fixed-length list of characters.
type SChar = SBV Char Source #
A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
is currently an 8-bit unsigned value, corresponding to the ISO-8859-1 (Latin-1) character
set: http://en.wikipedia.org/wiki/ISO/IEC_8859-1. A Haskell Char, on the other hand, is based
on unicode. Therefore, there isn't a 1-1 correspondence between a Haskell character and an SBV
character for the time being. This limitation is due to the SMT-solvers only supporting this
particular subset. However, there is a pending proposal to add support for unicode, and SBV
will track these changes to have full unicode support as solvers become available. For
details, see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml
(.++) :: SString -> SString -> SString infixr 5 Source #
Short cut for concat.
>>>sat $ \x y z -> length x .== 5 &&& length y .== 1 &&& x .++ y .++ z .== "Hello world!"Satisfiable. Model: s0 = "Hello" :: String s1 = " " :: String s2 = "world!" :: String
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 SBV aSBV b
While it's certainly possible for user to create instances of SymArray, the
SArray and SFunArray instances already provided should cover most use cases
in practice. (There are some differences between these models, however, see the corresponding
declaration.)
Minimal complete definition: All methods are required, no defaults.
Minimal complete definition
Methods
newArray_ :: (HasKind a, HasKind b) => Symbolic (array a b) Source #
Create a new anonymous array
newArray :: (HasKind a, HasKind b) => String -> Symbolic (array a b) Source #
Create a named new array
readArray :: array a b -> SBV a -> SBV b Source #
Read the array element at a
writeArray :: SymWord b => array a b -> SBV a -> SBV b -> array a b Source #
Update the element at a to be b
mergeArrays :: SymWord b => SBV Bool -> array a b -> array a b -> array a b Source #
Merge two given arrays on the symbolic condition
Intuitively: mergeArrays cond a b = if cond then a else b.
Merging pushes the if-then-else choice down on to elements
Arrays implemented in terms of SMT-arrays: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
- Maps directly to SMT-lib arrays
- Reading from an unintialized value is OK and yields an unspecified result
- Can check for equality of these arrays
- Cannot quick-check theorems using
SArrayvalues - Typically slower as it heavily relies on SMT-solving for the array theory
Arrays implemented internally as functions
- Internally handled by the library and not mapped to SMT-Lib
- Reading an uninitialized value is considered an error (will throw exception)
- Cannot check for equality (internally represented as functions)
- Can quick-check
- Typically faster as it gets compiled away during translation
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b Source #
Lift a function to an array. Useful for creating arrays in a pure context. (Otherwise use newArray.)
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.
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.
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.
Minimal complete definition
Methods
(.==) :: a -> a -> SBool infix 4 Source #
Symbolic equality.
(./=) :: a -> a -> SBool infix 4 Source #
Symbolic inequality.
distinct :: [a] -> SBool Source #
Returns (symbolic) true if all the elements of the given list are different.
allEqual :: [a] -> SBool Source #
Returns (symbolic) true 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 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 # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source # | |
| (EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source # | |
class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #
Symbolic Comparisons. Similar to Eq, we cannot implement Haskell's Ord class
since there is no way to return an Ordering value from a symbolic comparison.
Furthermore, OrdSymbolic requires Mergeable to implement if-then-else, for the
benefit of implementing symbolic versions of max and min functions.
Minimal complete definition
Methods
(.<) :: 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 # | |
| SymWord a => OrdSymbolic (SBV a) Source # | |
| (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # | |
| (OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source # | |
| (OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source # | |
class Equality a where Source #
Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.
Minimal complete definition
Instances
Conditionals: Mergeable values
class Mergeable a where Source #
Symbolic conditionals are modeled by the Mergeable class, describing
how to merge the results of an if-then-else call with a symbolic test. SBV
provides all basic types as instances of this class, so users only need
to declare instances for custom data-types of their programs as needed.
A Mergeable instance may be automatically derived for a custom data-type
with a single constructor where the type of each field is an instance of
Mergeable, such as a record of symbolic values. Users only need to add
Generic and Mergeable to the deriving clause for the data-type. See
Status for an example and an
illustration of what the instance would look like if written by hand.
The function select is a total-indexing function out of a list of choices
with a default value, simulating array/list indexing. It's an n-way generalization
of the ite function.
Minimal complete definition: None, if the type is instance of Generic. Otherwise
symbolicMerge. Note that most types subject to merging are likely to be
trivial instances of Generic.
Methods
symbolicMerge :: Bool -> SBool -> a -> a -> a Source #
Merge two values based on the condition. The first argument states whether we force the then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a Source #
Total indexing operation. select xs default index is intuitively
the same as xs !! index, except it evaluates to default if index
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 then-and-else branches before the merging, at the word level. This is an efficiency concern; one that we'd rather not make but unfortunately necessary for getting symbolic simulation working efficiently.
Instances
ite :: Mergeable a => SBool -> a -> a -> a Source #
If-then-else. This is by definition symbolicMerge with both
branches forced. This is typically the desired behavior, but also
see iteLazy should you need more laziness.
iteLazy :: Mergeable a => SBool -> a -> a -> a Source #
A Lazy version of ite, which does not force its arguments. This might cause issues for symbolic simulation with large thunks around, so use with care.
Symbolic integral numbers
class (SymWord a, Num a, Bits a, Integral a) => SIntegral a Source #
Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic type-signatures that work for all
symbolic numbers, such as SWord8, SInt8 etc. For instance, we can write a generic
list-minimum function as follows:
mm :: SIntegral a => [SBV a] -> SBV a mm = foldr1 (a b -> ite (a .<= b) a b)
It is similar to the standard Integral class, except ranging over symbolic instances.
Instances
Division and Modulus
class SDivisible a where Source #
The SDivisible class captures the essence of division.
Unfortunately we cannot use Haskell's Integral class since the Real
and Enum superclasses are not implementable for symbolic bit-vectors.
However, quotRem and divMod both make perfect sense, and the SDivisible class captures
this operation. One issue is how division by 0 behaves. The verification
technology requires total functions, and there are several design choices
here. We follow Isabelle/HOL approach of assigning the value 0 for division
by 0. Therefore, we impose the following pair of laws:
xsQuotRem0 = (0, x) xsDivMod0 = (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 # | |
| SDivisible Word32 Source # | |
| SDivisible Word64 Source # | |
| SDivisible CW Source # | |
| SDivisible SInteger Source # | |
| SDivisible SInt64 Source # | |
| SDivisible SInt32 Source # | |
| SDivisible SInt16 Source # | |
| SDivisible SInt8 Source # | |
| SDivisible SWord64 Source # | |
| SDivisible SWord32 Source # | |
| SDivisible SWord16 Source # | |
| SDivisible SWord8 Source # | |
| SDivisible SWord4 Source # | SDvisible instance, using default methods |
| SDivisible Word4 Source # | SDvisible instance, using 0-extension |
Bit-vector operations
Conversions
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b Source #
Conversion between integral-symbolic values, akin to Haskell's fromIntegral
Shifts and rotates
Symbolic words (both signed and unsigned) are an instance of Haskell's Bits class, so regular
bitwise operations are automatically available for them. Shifts and rotates, however, require
specialized type-signatures since Haskell insists on an Int second argument for them.
sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a Source #
Generalization of shiftR, when the shift-amount is symbolic. Since Haskell's
shiftR only takes an Int as the shift amount, it cannot be used when we have
a symbolic amount to shift with.
NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,
following the usual Haskell convention. See sSignedShiftArithRight for a variant
that explicitly uses the msb as the sign bit, even for unsigned underlying types.
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 shift-right with a symbolic unsigned shift amount. This is equivalent
to sShiftRight when the argument is signed. However, if the argument is unsigned,
then it explicitly treats its msb as a sign-bit, and uses it as the bit that
gets shifted in. Useful when using the underlying unsigned bit representation to implement
custom signed operations. Note that there is no direct Haskell analogue of this function.
Finite bit-vector operations
class (SymWord a, Num a, Bits a) => SFiniteBits a where Source #
Finite bit-length symbolic values. Essentially the same as SIntegral, but further leaves out Integer. Loosely
based on Haskell's FiniteBits class, but with more methods defined and structured differently to fit into the
symbolic world view. Minimal complete definition: sFiniteBitSize.
Minimal complete definition
Methods
sFiniteBitSize :: SBV a -> Int Source #
Bit size.
lsb :: SBV a -> SBool Source #
Least significant bit of a word, always stored at index 0.
msb :: SBV a -> SBool Source #
Most significant bit of a word, always stored at the last position.
blastBE :: SBV a -> [SBool] Source #
Big-endian blasting of a word into its bits.
blastLE :: SBV a -> [SBool] Source #
Little-endian blasting of a word into its bits.
fromBitsBE :: [SBool] -> SBV a Source #
Reconstruct from given bits, given in little-endian.
fromBitsLE :: [SBool] -> SBV a Source #
Reconstruct from given bits, given in little-endian.
sTestBit :: SBV a -> Int -> SBool Source #
sExtractBits :: SBV a -> [Int] -> [SBool] Source #
Variant of sTestBit, where we want to extract multiple bit positions.
sPopCount :: SBV a -> SWord8 Source #
Variant of popCount, returning a symbolic value.
setBitTo :: SBV a -> Int -> SBool -> SBV a Source #
fullAdder :: SBV a -> SBV a -> (SBool, SBV a) Source #
Full adder, returns carry-out from the addition. Only for unsigned quantities.
fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a) Source #
Full multipler, returns both high and low-order bits. Only for unsigned quantities.
sCountLeadingZeros :: SBV a -> SWord8 Source #
Count leading zeros in a word, big-endian interpretation.
sCountTrailingZeros :: SBV a -> SWord8 Source #
Count trailing zeros in a word, big-endian interpretation.
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 bit-size word than b, typically double.
The extend operation captures embedding of a b value into an a
without changing its semantic value.
Minimal complete definition: All, no defaults.
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.
IEEE-floating point numbers
class (SymWord a, RealFloat a) => IEEEFloating a where Source #
A class of floating-point (IEEE754) operations, some of which behave differently based on rounding modes. Note that unless the rounding mode is concretely RoundNearestTiesToEven, we will not concretely evaluate these, but rather pass down to the SMT solver.
Methods
fpAbs :: SBV a -> SBV a 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 floating-point, 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 #
Fused-multiply-add three floating point values, using the given rounding mode. fpFMA x y z = x*y+z but with only
one rounding done for the whole operation; not two. Note that we will never concretely evaluate this function since
Haskell lacks an FMA implementation.
fpSqrt :: SRoundingMode -> SBV a -> SBV a Source #
Compute the square-root 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 floating-point number a normal value. (i.e., not denormalized.)
fpIsSubnormal :: SBV a -> SBool Source #
Is the floating-point number a subnormal value. (Also known as denormal.)
fpIsZero :: SBV a -> SBool Source #
Is the floating-point number 0? (Note that both +0 and -0 will satisfy this predicate.)
fpIsInfinite :: SBV a -> SBool Source #
Is the floating-point number infinity? (Note that both +oo and -oo will satisfy this predicate.)
fpIsNaN :: SBV a -> SBool Source #
Is the floating-point number a NaN value?
fpIsNegative :: SBV a -> SBool Source #
Is the floating-point number negative? Note that -0 satisfies this predicate but +0 does not.
fpIsPositive :: SBV a -> SBool Source #
Is the floating-point 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 floating-point number a regular floating point, i.e., not NaN, nor +oo, nor -oo. Normals or denormals are allowed.
Instances
| IEEEFloating Double Source # | SDouble instance |
| IEEEFloating Float Source # | SFloat instance |
data RoundingMode Source #
Rounding mode to be used for the IEEE floating-point operations.
Note that Haskell's default is RoundNearestTiesToEven. If you use
a different rounding mode, then the counter-examples you get may not
match what you observe in Haskell.
Constructors
| RoundNearestTiesToEven | Round to nearest representable floating point value. If precisely at half-way, pick the even number. (In this context, even means the lowest-order bit is zero.) |
| RoundNearestTiesToAway | Round to nearest representable floating point value. If precisely at half-way, pick the number further away from 0. (That is, for positive values, pick the greater; for negative values, pick the smaller.) |
| RoundTowardPositive | Round towards positive infinity. (Also known as rounding-up or ceiling.) |
| RoundTowardNegative | Round towards negative infinity. (Also known as rounding-down or floor.) |
| RoundTowardZero | Round towards zero. (Also known as truncation.) |
Instances
| Bounded RoundingMode Source # | |
| Enum RoundingMode Source # | |
| Eq RoundingMode Source # | |
| Data RoundingMode Source # | |
| Ord RoundingMode Source # | |
| Read RoundingMode Source # | |
| Show RoundingMode Source # | |
| HasKind RoundingMode Source # |
|
| SymWord RoundingMode Source # |
|
| SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices) |
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 RoundNearestPositive
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.
Minimal complete definition
Methods
fromSFloat :: SRoundingMode -> SFloat -> SBV a Source #
toSFloat :: SRoundingMode -> SBV a -> SFloat Source #
fromSDouble :: SRoundingMode -> SDouble -> SBV a Source #
Instances
Bit-pattern conversions
sFloatAsSWord32 :: SFloat -> SWord32 Source #
Convert an SFloat to an SWord32, preserving the bit-correspondence. Note that since the
representation for NaNs are not unique, this function will return a symbolic value when given a
concrete NaN.
Implementation note: Since there's no corresponding function in SMTLib for conversion to bit-representation due to partiality, we use a translation trick by allocating a new word variable, converting it to float, and requiring it to be equivalent to the input. In code-generation mode, we simply map it to a simple conversion.
sWord32AsSFloat :: SWord32 -> SFloat Source #
Reinterpret the bits in a 32-bit word as a single-precision floating point number
sDoubleAsSWord64 :: SDouble -> SWord64 Source #
Convert an SDouble to an SWord64, preserving the bit-correspondence. Note that since the
representation for NaNs are not unique, this function will return a symbolic value when given a
concrete NaN.
See the implementation note for sFloatAsSWord32, as it applies here as well.
sWord64AsSDouble :: SWord64 -> SDouble Source #
Reinterpret the bits in a 32-bit word as a single-precision floating point number
blastSFloat :: SFloat -> (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a single-precision float. The output will have 8 bits in the second argument for exponent, and 23 in the third for the mantissa.
blastSDouble :: SDouble -> (SBool, [SBool], [SBool]) Source #
Extract the sign/exponent/mantissa of a single-precision float. The output will have 11 bits in the second argument for exponent, and 52 in the third for the mantissa.
Enumerations
If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then SBV will actually translate that as just such a data-type to SMT-Lib, and will use the constructors as the inhabitants of the said sort. A simple example is:
data X = A | B | C
mkSymbolicEnumeration ''X
Note the magic incantation mkSymbolicEnumeration ''X. For this to work, you need to have the following
options turned on:
LANGUAGE TemplateHaskell LANGUAGE StandaloneDeriving LANGUAGE DeriveDataTypeable LANGUAGE DeriveAnyClass
Now, the user can define
type SX = SBV X
and treat SX as a regular symbolic type ranging over the values A, B, and C. Such values can be compared for equality, and with the usual
other comparison operators, such as .==, ./=, .>, .>=, <, and <=.
Note that in this latter case the type is no longer uninterpreted, but is properly represented as a simple enumeration of the said elements. A simple query would look like:
allSat $ x -> x .== (x :: SX)
which would list all three elements of this domain as satisfying solutions.
Solution #1:
s0 = A :: X
Solution #2:
s0 = B :: X
Solution #3:
s0 = C :: X
Found 3 different solutions.
Note that the result is properly typed as X elements; these are not mere strings. So, in a getModelAssignment scenario, the user can recover actual
elements of the domain and program further with those values as usual.
See Documentation.SBV.Examples.Misc.Enumerate for an extended example on how to use symbolic enumerations.
Uninterpreted sorts, constants, and functions
Users can introduce new uninterpreted sorts simply by defining a data-type in Haskell and registering it as such. The following example demonstrates:
data B = B () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind, SatModel)
(Note that you'll also need to use the language pragmas DeriveDataTypeable, DeriveAnyClass, and import Data.Generics for the above to work.)
This is all it takes to introduce B as an uninterpreted sort in SBV, which makes the type SBV B automagically become available as the type
of symbolic values that ranges over B values. Note that the () argument is important to distinguish it from enumerations, which will be
translated to proper SMT data-types.
Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by
the Uninterpreted class.
class Uninterpreted a where 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 uninterpreted-functions as a general means of black-box'ing operations that are irrelevant for the purposes of the proof; i.e., when the proofs can be performed without any knowledge about the function itself.
Minimal complete definition: sbvUninterpret. However, most instances in
practice are already provided by SBV, so end-users should not need to define their
own instances.
Minimal complete definition
Methods
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 code-generation. For execution and verification the value is used as is. For code-generation, the alternate definition is used. This is useful when we want to take advantage of native libraries on the target languages.
sbvUninterpret :: Maybe ([String], a) -> String -> a Source #
Most generalized form of uninterpretation, this function should not be needed by end-user-code, but is rather useful for the library development.
Instances
addAxiom :: String -> [String] -> Symbolic () Source #
Add a user specified axiom to the generated SMT-Lib file. The first argument is a mere string, use for commenting purposes. The second argument is intended to hold the multiple-lines of the axiom text as expressed in SMT-Lib notation. Note that we perform no checks on the axiom itself, to see whether it's actually well-formed or is sensical by any means. A separate formalization of SMT-Lib would be very useful here.
Properties, proofs, and satisfiability
The SBV library provides a "push-button" verification system via automated SMT solving. The design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers. To that end, we use the SMT-Lib standard (http://smtlib.cs.uiowa.edu/) to communicate with arbitrary SMT solvers.
A note on reasoning in the presence of quantifers
Note that SBV allows reasoning with quantifiers: Inputs can be existentially or universally quantified. Predicates can be built with arbitrary nesting of such quantifiers as well. However, SBV always assumes that the input is in prenex-normal form: https://en.wikipedia.org/wiki/Prenex_normal_form. That is, all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately, the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers. SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested quantification, you will manually have to first convert to prenex-normal form (which produces an equisatisfiable but not necessarily equivalent formula), and code that explicitly in SBV. See https://github.com/LeventErkok/sbv/issues/256 for a detailed discussion of this issue.
Using multiple solvers
On a multi-core machine, it might be desirable to try a given property using multiple SMT solvers, using parallel threads. Even with machines with single-cores, threading can be helpful if you want to try out multiple-solvers but do not know which one would work the best for the problem at hand ahead of time.
SBV allows proving/satisfiability-checking with multiple backends at the same time. Each function comes in two variants, one that returns the results from all solvers, the other that returns the fastest one.
The All variants, (i.e., proveWithAll, satWithAll) run all solvers and
return all the results. SBV internally makes sure that the result is lazily generated; so,
the order of solvers given does not matter. In other words, the order of results will follow
the order of the solvers as they finish, not as given by the user. These variants are useful when you
want to make sure multiple-solvers agree (or disagree!) on a given problem.
The Any variants, (i.e., proveWithAny, satWithAny) will run all the solvers
in parallel, and return the results of the first one finishing. The other threads will then be killed. These variants
are useful when you do not care if the solvers produce the same result, but rather want to get the
solution as quickly as possible, taking advantage of modern many-core machines.
Note that the function sbvAvailableSolvers will return all the installed solvers, which can be
used as the first argument to all these functions, if you simply want to try all available solvers on a machine.
type Predicate = Symbolic SBool Source #
A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The Symbolic
monad captures the underlying representation, and can/should be ignored by the users of the library,
unless you are building further utilities on top of SBV itself. Instead, simply use the Predicate
type when necessary.
type Goal = Symbolic () Source #
A goal is a symbolic program that returns no values. The idea is that the constraints/min-max goals will serve as appropriate directives for sat/prove calls.
class Provable a where Source #
A type a is provable if we can turn it into a predicate.
Note that a predicate can be made from a curried function of arbitrary arity, where
each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So
predicates can be constructed from almost arbitrary Haskell functions that have arbitrary
shapes. (See the instance declarations below.)
Methods
forAll_ :: a -> Predicate Source #
Turns a value into a universally quantified predicate, internally naming the inputs.
In this case the sbv library will use names of the form s1, s2, etc. to name these variables
Example:
forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y
is a predicate with two arguments, captured using an ordinary Haskell function. Internally,
x will be named s0 and y will be named s1.
forAll :: [String] -> a -> Predicate Source #
Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:
forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y
This is the same as above, except the variables will be named x and y respectively,
simplifying the counter-examples when they are printed.
forSome_ :: a -> Predicate Source #
Turns a value into an existentially quantified predicate. (Indeed, exists would have been
a better choice here for the name, but alas it's already taken.)
forSome :: [String] -> a -> Predicate Source #
Version of forSome that allows user defined names.
prove :: a -> IO ThmResult Source #
Prove a predicate, using the default solver.
proveWith :: SMTConfig -> a -> IO ThmResult Source #
Prove the predicate using the given SMT-solver.
sat :: a -> IO SatResult Source #
Find a satisfying assignment for a predicate, using the default solver.
satWith :: SMTConfig -> a -> IO SatResult Source #
Find a satisfying assignment using the given SMT-solver.
allSat :: a -> IO AllSatResult Source #
Find all satisfying assignments, using the default solver. See allSatWith for details.
allSatWith :: SMTConfig -> a -> IO AllSatResult Source #
Return all satisfying assignments for a predicate, equivalent to allSatWith defaultSMTCfgSInteger) or a very large number of them, you
might have to wait for a long time. To avoid such cases, use the allSatMaxModelCount parameter
in the configuration.
NB. Uninterpreted constant/function values and counter-examples for array values are ignored for
the purposes of allSat
optimize :: OptimizeStyle -> a -> IO OptimizeResult Source #
Optimize a given collection of Objectives
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult Source #
Optimizes the objectives using the given SMT-solver.
isVacuous :: a -> IO Bool Source #
Check if the constraints given are consistent, using the default solver.
isVacuousWith :: SMTConfig -> a -> IO Bool Source #
Determine if the constraints are vacuous using the given SMT-solver.
isTheorem :: a -> IO Bool Source #
Checks theoremhood using the default solver.
isTheoremWith :: SMTConfig -> a -> IO Bool Source #
Check whether a given property is a theorem.
isSatisfiable :: a -> IO Bool Source #
Checks satisfiability using the default solver.
isSatisfiableWith :: SMTConfig -> a -> IO Bool Source #
Check whether a given property is satisfiable.
proveWithAll :: [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 :: [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 :: [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 :: [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 :: Bool -> a -> IO String Source #
Create an SMT-Lib2 benchmark. The Bool argument controls whether this is a SAT instance, i.e.,
translate the query directly, or a PROVE instance, i.e., translate the negated query.
Instances
| Provable SBool Source # | |
| Provable Predicate Source # | |
| (SymWord a, SymWord b, Provable p) => Provable ((SBV a, SBV b) -> p) Source # | |
| (SymWord a, SymWord b, SymWord c, Provable p) => Provable ((SBV a, SBV b, SBV c) -> p) Source # | |
| (SymWord a, SymWord b, SymWord c, SymWord d, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d) -> p) Source # | |
| (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) Source # | |
| (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) Source # | |
| (SymWord a, SymWord b, SymWord c, SymWord d, SymWord e, SymWord f, SymWord g, Provable p) => Provable ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) Source # | |
| (HasKind a, HasKind b, Provable p) => Provable (SFunArray a b -> p) Source # | |
| (HasKind a, HasKind b, Provable p) => Provable (SArray a b -> p) Source # | |
| (SymWord a, Provable p) => Provable (SBV a -> p) Source # | |
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]
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
provecall: 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
quickCheckcall: 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
genTestcall: Similar toquickCheckandprove: If a constraint does not hold, the input value is ignored and is not included in the test set.
A good use case (in fact the motivating use case) for constrain is attaching a
constraint to a forall or exists variable at the time of its creation.
Also, the conjunctive semantics for sat and the implicative
semantics for prove simplify programming by choosing the correct interpretation
automatically. However, one should be aware of the semantic difference. For instance, in
the presence of constraints, formulas that are provable are not necessarily
satisfiable. To wit, consider:
do x <-exists"x"constrain$ x .< x return $ x .< (x ::SWord8)
This predicate is unsatisfiable since no element of SWord8 is less than itself. But
it's (vacuously) true, since it excludes the entire domain of values, thus making the proof
trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given
constraints are not vacuous, the functions isVacuous (and isVacuousWith) can be used.
Also note that this semantics imply that test case generation (genTest) and quick-check
can take arbitrarily long in the presence of constraints, if the random input values generated
rarely satisfy the constraints. (As an extreme case, consider constrain false
constrain :: SolverContext m => SBool -> m () Source #
Add a constraint, any satisfying instance must satisfy this condition
Constraint Vacuity
When adding constraints, one has to be careful about
making sure they are not inconsistent. The function isVacuous can be use for this purpose.
Here is an example. Consider the following predicate:
>>>let pred = do { x <- free "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }
This predicate asserts that all 8-bit values are larger than 5, subject to the constraint that the
values considered satisfy x .< x, i.e., they are less than themselves. Since there are no values that
satisfy this constraint, the proof will pass vacuously:
>>>prove predQ.E.D.
We can use isVacuous to make sure to see that the pass was vacuous:
>>>isVacuous predTrue
While the above example is trivial, things can get complicated if there are multiple constraints with non-straightforward relations; so if constraints are used one should make sure to check the predicate is not vacuously true. Here's an example that is not vacuous:
>>>let pred' = do { x <- free "x"; constrain $ x .> 6; return $ x .>= (5 :: SWord8) }
This time the proof passes as expected:
>>>prove pred'Q.E.D.
And the proof is not vacuous:
>>>isVacuous pred'False
Named constraints
Constraints can be given names:
namedConstraint "a is at least 5" $ a .>= 5namedConstraint :: SolverContext m => String -> SBool -> m () Source #
Add a named constraint. The name is used in unsat-core extraction.
Unsat cores
Named constraints are useful when used in conjunction with getUnsatCore function
where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable.
This feature is enabled by the following option:
setOption $ ProduceUnsatCores True
See Documentation.SBV.Examples.Misc.UnsatCore for an example use case.
Cardinality constraints
A pseudo-boolean function (http://en.wikipedia.org/wiki/Pseudo-Boolean_function) is a
function from booleans to reals, basically treating True as 1 and False as 0. They
are typically expressed in polynomial form. Such functions can be used to express cardinality
constraints, where we want to count how many things satisfy a certain condition.
One can code such constraints using regular SBV programming: Simply walk over the booleans and the corresponding coefficients, and assert the required relation. For instance:
[b0, b1, b2, b3] `pbAtMost` 2
is precisely equivalent to:
sum (map (\b -> ite b 1 0) [b0, b1, b2, b3]) .<= 2
and they both express that at most two of b0, b1, b2, and b3 can be true.
However, the equivalent forms give rise to long formulas and the cardinality constraint
can get lost in the translation. The idea here is that if you use these functions instead, SBV will
produce better translations to SMTLib for more efficient solving of cardinality constraints, assuming
the backend solver supports them. Currently, only Z3 supports pseudo-booleans directly. For all other solvers,
SBV will translate these to equivalent terms that do not require special functions.
Checking safety
The sAssert function allows users to introduce invariants to make sure
certain properties hold at all times. This is another mechanism to provide further documentation/contract info
into SBV code. The functions safe and safeWith can be used to statically discharge these proof assumptions.
If a violation is found, SBV will print a model showing which inputs lead to the invariant being violated.
Here's a simple example. Let's assume we have a function that does subtraction, and requires its first argument to be larger than the second:
>>>let sub x y = sAssert Nothing "sub: x >= y must hold!" (x .>= y) (x - y)
Clearly, this function is not safe, as there's nothing that stops us from passing it a larger second argument.
We can use safe to statically see if such a violation is possible before we use this function elsewhere.
>>>safe (sub :: SInt8 -> SInt8 -> SInt8)[sub: x >= y must hold!: Violated. Model: s0 = 30 :: Int8 s1 = 32 :: Int8]
What happens if we make sure to arrange for this invariant? Consider this version:
>>>let safeSub x y = ite (x .>= y) (sub x y) 0
Clearly, safeSub must be safe. And indeed, SBV can prove that:
>>>safe (safeSub :: SInt8 -> SInt8 -> SInt8)[sub: x >= y must hold!: No violations detected]
Note how we used sub and safeSub polymorphically. We only need to monomorphise our types when a proof
attempt is done, as we did in the safe calls.
If required, the user can pass a CallStack through the first argument to sAssert, which will be used
by SBV to print a diagnostic info to pinpoint the failure.
Also see Documentation.SBV.Examples.Misc.NoDiv0 for the classic div-by-zero example.
sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a Source #
Symbolic assert. Check that the given boolean condition is always true in the given path. The optional first argument can be used to provide call-stack info via GHC's location facilities.
isSafe :: SafeResult -> Bool Source #
Check if a safe-call was safe or not, turning a SafeResult to a Bool.
class SExecutable a where Source #
Symbolically executable program fragments. This class is mainly used for safe calls, and is sufficently populated internally to cover most use
cases. Users can extend it as they wish to allow safe checks for SBV programs that return/take types that are user-defined.
Methods
sName_ :: a -> Symbolic () Source #
sName :: [String] -> a -> Symbolic () Source #
safe :: a -> IO [SafeResult] Source #
Check safety using the default solver.
safeWith :: SMTConfig -> a -> IO [SafeResult] Source #
Check if any of the sAssert calls can be violated.
Instances
Quick-checking
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 SReals. That is, it can find models satisfying all the constraints while minimizing
or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend,
and a good review of these features is given
in this paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.
Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are:
Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals).
For instance, a call of the form
minimize "name-of-goal" $ x + 2*yminimizes the arithmetic goal x+2*y, where x and y can be signed/unsigned bit-vectors, reals,
or integers.
A simple example
Here's an optimization example in action:
>>>optimize Lexicographic $ \x y -> minimize "goal" (x+2*(y::SInteger))Optimal in an extension field: goal = -oo :: Integer
We will describe the role of the constructor Lexicographic shortly.
Of course, this becomes more useful when the result is not in an extension field:
>>>:{optimize Lexicographic $ do x <- sInteger "x" y <- sInteger "y" constrain $ x .> 0 constrain $ x .< 6 constrain $ y .> 2 constrain $ y .< 12 minimize "goal" $ x + 2 * y :} Optimal model: x = 1 :: Integer y = 3 :: Integer goal = 7 :: Integer
As usual, the programmatic API can be used to extract the values of objectives and model-values (getModelObjectives,
getModelAssignment, etc.) to access these values and program with them further.
The following examples illustrate the use of basic optimization routines:
- Documentation.SBV.Examples.Optimization.LinearOpt: Simple linear-optimization example.
- Documentation.SBV.Examples.Optimization.Production: Scheduling machines in a shop
- Documentation.SBV.Examples.Optimization.VM: Scheduling virtual-machines in a data-center
Multiple optimization goals
Multiple goals can be specified, using the same syntax. In this case, the user gets to pick what style of
optimization to perform, by passing the relevant OptimizeStyle as the first argument to optimize.
- [
Lexicographic]. The solver will optimize the goals in the given order, optimizing the latter ones under the model that optimizes the previous ones. - [
Independent]. The solver will optimize the goals independently of each other. In this case the user will be presented a model for each goal given. - [
Pareto]. Finally, the user can query for pareto-fronts. A pareto front is an model such that no goal can be made "better" without making some other goal "worse."
The optional number argument to Pareto specifies the maximum number of pareto-fronts the user is asking
to get. If Nothing, SBV will query for all pareto-fronts. Note that pareto-fronts can be infinite
in number, so if Nothing is used, there is a potential for infinitely waiting for the SBV-solver interaction
to finish. (If you suspect this might be the case, run in verbose mode to see the interaction and
put a limiting factor appropriately.)
data OptimizeStyle 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.
Constructors
| Lexicographic | Objectives are optimized in the order given, earlier objectives have higher priority. This is the default. |
| Independent | Each objective is optimized independently. |
| Pareto (Maybe Int) | Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. |
Instances
Objectives
Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.
Class of metrics we can optimize for. Currently, bounded signed/unsigned bit-vectors, unbounded integers, and algebraic reals can be optimized. (But not, say, SFloat, SDouble, or SBool.) Minimal complete definition: minimize/maximize.
A good reference on these features is given in the following paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.
Soft assumptions
Related to optimization, SBV implements soft-asserts via assertSoft calls. A soft assertion
is a hint to the SMT solver that we would like a particular condition to hold if **possible*.
That is, if there is a solution satisfying it, then we would like it to hold, but it can be violated
if there is no way to satisfy it. Each soft-assertion can be associated with a numeric penalty for
not satisfying it, hence turning it into an optimization problem.
Note that assertSoft works well with optimization goals ('minimize'/'maximize' etc.),
and are most useful when we are optimizing a metric and thus some of the constraints
can be relaxed with a penalty to obtain a good solution. Again
see https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf
for a good overview of the features in Z3 that SBV is providing the bridge for.
A soft assertion can be specified in one of the following three main ways:
assertSoft "bounded_x" (x .< 5) DefaultPenalty
assertSoft "bounded_x" (x .< 5) (Penalty 2.3 Nothing)
assertSoft "bounded_x" (x .< 5) (Penalty 4.7 (Just "group-1"))In the first form, we are saying that the constraint x .< 5 must be satisfied, if possible,
but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.
In the second case, we are associating a penalty value of 2.3.
Finally in the third case, we are also associating this constraint with a group. The group name is only needed if we have classes of soft-constraints that should be considered together.
assertSoft :: String -> SBool -> Penalty -> Symbolic () Source #
Introduce a soft assertion, with an optional penalty
Penalty for a soft-assertion. The default penalty is 1, with all soft-assertions belonging
to the same objective goal. A positive weight and an optional group can be provided by using
the Penalty constructor.
Constructors
| DefaultPenalty | Default: Penalty of |
| 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 CW value will be in the corresponding extension field.
A simple expression type over extendent values, covering infinity, epsilon and intervals.
data GeneralizedCW Source #
A generalized CW allows for expressions involving infinite and epsilon values/intervals Used in optimization problems.
Constructors
| ExtendedCW ExtCW | |
| RegularCW CW |
Instances
| Show GeneralizedCW Source # | Show instance for Generalized |
| HasKind GeneralizedCW Source # |
|
Model extraction
The default Show instances for prover calls provide all the counter-example information in a
human-readable form and should be sufficient for most casual uses of sbv. However, tools built
on top of sbv will inevitably need to look into the constructed models more deeply, programmatically
extracting their results and performing actions based on them. The API provided in this section
aims at simplifying this task.
Inspecting proof results
ThmResult, SatResult, and AllSatResult are simple newtype wrappers over SMTResult. Their
main purpose is so that we can provide custom Show instances to print results accordingly.
A prove call results in a ThmResult
newtype AllSatResult Source #
An allSat call results in a AllSatResult. The first boolean says whether we
hit the max-model limit as we searched. The second boolean says whether
there were prefix-existentials.
Constructors
| AllSatResult (Bool, Bool, [SMTResult]) |
Instances
newtype SafeResult Source #
A safe call results in a SafeResult
Constructors
| SafeResult (Maybe String, String, SMTResult) |
Instances
data OptimizeResult Source #
An optimize call results in a OptimizeResult. In the ParetoResult case, the boolean is True
if we reached pareto-query limit and so there might be more unqueried results remaining. If False,
it means that we have all the pareto fronts returned. See the Pareto OptimizeStyle for details.
Constructors
| LexicographicResult SMTResult | |
| ParetoResult (Bool, [SMTResult]) | |
| IndependentResult [(String, SMTResult)] |
Instances
The result of an SMT solver call. Each constructor is tagged with
the SMTConfig that created it so that further tools can inspect it
and build layers of results, if needed. For ordinary uses of the library,
this type should not be needed, instead use the accessor functions on
it. (Custom Show instances and model extractors.)
Constructors
| Unsatisfiable SMTConfig (Maybe [String]) | Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter. |
| Satisfiable SMTConfig SMTModel | Satisfiable with model |
| SatExtField SMTConfig SMTModel | Prover returned a model, but in an extension field containing Infinite/epsilon |
| Unknown SMTConfig String | Prover returned unknown, with the given reason |
| ProofError SMTConfig [String] | Prover errored out |
Observing expressions
The observe command can be used to trace values of arbitrary expressions during a sat, prove, or perhaps more
importantly, in a quickCheck call. This is useful for, for instance, recording expected/obtained expressions as a symbolic program is executing.
>>>:{prove $ do a1 <- free "i1" a2 <- free "i2" let spec, res :: SWord8 spec = a1 + a2 res = ite (a1 .== 12 &&& a2 .== 22) -- insert a malicious bug! 1 (a1 + a2) observe "Expected" spec observe "Result" res return $ spec .== res :} Falsifiable. Counter-example: i1 = 12 :: Word8 i2 = 22 :: Word8 Expected = 34 :: Word8 Result = 1 :: Word8
observe :: SymWord a => String -> SBV a -> Symbolic () Source #
Observe the value of an expression. Such values are useful in model construction, as they are printed part of a satisfying model, or a counter-example. The same works for quick-check as well. Useful when we want to see intermediate values, or expected/obtained pairs in a particular run.
Programmable model extraction
While default Show instances are sufficient for most use cases, it is sometimes desirable (especially
for library construction) that the SMT-models are reinterpreted in terms of domain types. Programmable
extraction allows getting arbitrarily typed models out of SMT models.
class SatModel a where 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 CW's (constant-words)
coming from the solver, and the type a is interpreted based on these constants. Many typical
instances are already provided, so new instances can be declared with relative ease.
Minimum complete definition: parseCWs
Methods
parseCWs :: [CW] -> Maybe (a, [CW]) Source #
Given a sequence of constant-words, extract one instance of the type a, returning
the remaining elements untouched. If the next element is not what's expected for this
type you should return Nothing
cvtModel :: (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW]) 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.
parseCWs :: Read a => [CW] -> Maybe (a, [CW]) Source #
Given a sequence of constant-words, extract one instance of the type a, returning
the remaining elements untouched. If the next element is not what's expected for this
type you should return Nothing
Instances
| SatModel Bool 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 CW Source # |
|
| SatModel RoundingMode Source # | A rounding mode, extracted from a model. (Default definition suffices) |
| SatModel E Source # | Make |
| SatModel Word4 Source # | SatModel instance, merely uses the generic parsing method. |
| SatModel Color Source # | Make |
| SatModel Nationality Source # | Make |
| SatModel Beverage Source # | Make |
| SatModel Pet Source # | Make |
| SatModel Sport Source # | Make |
| SatModel U2Member Source # | Make |
| SatModel Location Source # | Make |
| SatModel Day Source # | Make |
| SatModel BinOp Source # | Make |
| SatModel UnOp Source # | Make |
| SatModel a => SatModel [a] Source # | A list of values as extracted from a model. When reading a list, we go as long as we can (maximal-munch). Note that this never fails, as we can always return the empty list! |
| (SatModel a, SatModel b) => SatModel (a, b) Source # | Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) Source # | 3-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) Source # | 4-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) Source # | 5-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) Source # | 6-Tuples extracted from a model |
| (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) Source # | 7-Tuples extracted from a model |
class Modelable a where Source #
Various SMT results that we can extract models out of.
Minimal complete definition
modelExists, getModelAssignment, getModelDictionary, getModelObjectives
Methods
modelExists :: a -> Bool Source #
Is there a model?
getModelAssignment :: SatModel b => a -> Either String (Bool, b) Source #
Extract assignments of a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)
getModelDictionary :: a -> Map String CW Source #
Extract a model dictionary. Extract a dictionary mapping the variables to
their respective values as returned by the SMT solver. Also see getModelDictionaries.
getModelValue :: SymWord b => String -> a -> Maybe b Source #
Extract a model value for a given element. Also see getModelValues.
getModelUninterpretedValue :: String -> a -> Maybe String Source #
Extract a representative name for the model value of an uninterpreted kind.
This is supposed to correspond to the value as computed internally by the
SMT solver; and is unportable from solver to solver. Also see getModelUninterpretedValues.
extractModel :: SatModel b => a -> Maybe b Source #
A simpler variant of getModelAssignment to get a model out without the fuss.
getModelObjectives :: a -> Map String GeneralizedCW Source #
Extract model objective values, for all optimization goals.
getModelObjectiveValue :: String -> a -> Maybe GeneralizedCW Source #
Extract the value of an objective
displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int Source #
Given an allSat call, we typically want to iterate over it and print the results in sequence. The
displayModels function automates this task by calling disp on each result, consecutively. The first
Int argument to disp 'is the current model number. The second argument is a tuple, where the first
element indicates whether the model is alleged (i.e., if the solver is not sure, returing Unknown)
extractModels :: SatModel a => AllSatResult -> [a] Source #
Return all the models from an allSat call, similar to extractModel but
is suitable for the case of multiple results.
getModelDictionaries :: AllSatResult -> [Map String CW] Source #
Get dictionaries from an all-sat call. Similar to getModelDictionary.
getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b] Source #
Extract value of a variable from an all-sat call. Similar to getModelValue.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] Source #
Extract value of an uninterpreted variable from an all-sat call. Similar to getModelUninterpretedValue.
SMT Interface
Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc. which are instantiations of this type for those solvers, with
reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as z3{verbose=True}.)
Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after
the decimal point. The default value is 16, but it can be set to any positive integer.
When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value
exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
of the real value is not finite, i.e., if it is not rational.
The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
Constructors
| SMTConfig | |
Fields
| |
Specify how to save timing information, if at all.
Constructors
| NoTiming | |
| PrintTiming | |
| SaveTiming (IORef NominalDiffTime) |
data SMTLibVersion Source #
Representation of SMTLib Program versions. As of June 2015, we're dropping support for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case SMTLib3 comes along and we want to support 2 and 3 simultaneously.
Constructors
| SMTLib2 |
Solvers that SBV is aware of
An SMT solver
Constructors
| SMTSolver | |
Fields
| |
Controlling verbosity
SBV provides various levels of verbosity to aid in debugging, by using the SMTConfig fields:
- [
verbose] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise and is good for quick debugging. The output is not supposed to be machine-readable. - [
redirectVerbose] Send the verbose output to a file. Note that you still have to set `verbose=True` for redirection to take effect. Otherwise, the output is the same as what you would see inverbose. - [
transcript] Produce a file that is valid SMTLib2 format, containing everything sent and received. In particular, one can directly feed this file to the SMT-solver outside of the SBV since it is machine-readable. This is good for offline analysis situations, where you want to have a full account of what happened. For instance, it will print time-stamps at every interaction point, so you can see how long each command took.
Solvers
Configurations
defaultSolverConfig :: Solver -> SMTConfig Source #
The default configs corresponding to supported SMT solvers
defaultSMTCfg :: SMTConfig Source #
The default solver used by SBV. This is currently set to z3.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool Source #
Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.
sbvAvailableSolvers :: IO [SMTConfig] Source #
Return the known available solver configs, installed on your machine.
setLogic :: SolverContext m => Logic -> m () Source #
Set the logic.
setOption :: SolverContext m => SMTOption -> m () Source #
Set an option.
setInfo :: SolverContext m => String -> [String] -> m () Source #
Set info. Example: setInfo ":status" ["unsat"].
setTimeOut :: SolverContext m => Integer -> m () Source #
Set a solver time-out value, in milli-seconds. This function
essentially translates to the SMTLib call (set-info :timeout val),
and your backend solver may or may not support it! The amount given
is in milliseconds. Also see the function timeOut for finer level
control of time-outs, directly from SBV.
Solver exceptions
data SMTException Source #
An SMT exception generated by the back-end solver and is thrown from SBV. If the solver
ever responds with a non-success value for a command, SBV will throw an SMTException,
it so the user can process it as required. The provided Show instance will render the failure
nicely. Note that if you ever catch this exception, the solver is no longer alive: You should either
throw the exception up, or do other proper clean-up before continuing.
Constructors
Instances
| Show SMTException Source # | A fairly nice rendering of the exception, for display purposes. |
| Exception SMTException Source # | SMTExceptions are throwable. A simple "show" will render this exception nicely though of course you can inspect the individual fields as necessary. |
Abstract SBV type
The Symbolic value. The parameter a is phantom, but is
extremely important in keeping the user interface strongly typed.
Instances
class HasKind a where Source #
A class for capturing values that have a sign and a size (finite or infinite)
minimal complete definition: kindOf, unless you can take advantage of the default
signature: This class can be automatically derived for data-types that have
a Data instance; this is useful for creating uninterpreted sorts. So, in
reality, end users should almost never need to define any methods.
Methods
intSizeOf :: a -> Int Source #
isBoolean :: a -> Bool Source #
isBounded :: a -> Bool Source #
isDouble :: a -> Bool Source #
isInteger :: a -> Bool Source #
isUninterpreted :: a -> Bool Source #
isString :: a -> Bool Source #
Instances
Kind of symbolic value
class (HasKind a, Ord a) => SymWord a where Source #
A SymWord is a potential symbolic bitvector that can be created instances of
to be fed to a symbolic program. Note that these methods are typically not needed
in casual uses with prove, sat, allSat etc, as default instances automatically
provide the necessary bits.
Methods
forall :: String -> Symbolic (SBV a) Source #
Create a user named input (universal)
forall_ :: Symbolic (SBV a) Source #
Create an automatically named input
mkForallVars :: Int -> Symbolic [SBV a] Source #
Get a bunch of new words
exists :: String -> Symbolic (SBV a) Source #
Create an existential variable
exists_ :: Symbolic (SBV a) Source #
Create an automatically named existential variable
mkExistVars :: Int -> Symbolic [SBV a] Source #
Create a bunch of existentials
free :: String -> Symbolic (SBV a) Source #
Create a free variable, universal in a proof, existential in sat
free_ :: Symbolic (SBV a) Source #
Create an unnamed free variable, universal in proof, existential in sat
mkFreeVars :: Int -> Symbolic [SBV a] Source #
Create a bunch of free vars
symbolic :: String -> Symbolic (SBV a) Source #
Similar to free; Just a more convenient name
symbolics :: [String] -> Symbolic [SBV a] Source #
Similar to mkFreeVars; but automatically gives names based on the strings
literal :: a -> SBV a Source #
Turn a literal constant to symbolic
unliteral :: SBV a -> Maybe a Source #
Extract a literal, if the value is concrete
Extract a literal, from a CW representation
isConcrete :: SBV a -> Bool Source #
Is the symbolic word concrete?
isSymbolic :: SBV a -> Bool Source #
Is the symbolic word really symbolic?
isConcretely :: SBV a -> (a -> Bool) -> Bool Source #
Does it concretely satisfy the given predicate?
mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #
One stop allocator
literal :: Show a => a -> SBV a Source #
Turn a literal constant to symbolic
fromCW :: Read a => CW -> a Source #
Extract a literal, from a CW representation
mkSymWord :: (Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a) Source #
One stop allocator
Instances
| SymWord RoundingMode Source # |
|
| SymWord E Source # | |
| SymWord Word4 Source # | SymWord instance, allowing this type to be used in proofs/sat etc. |
| SymWord Color Source # | |
| SymWord Nationality Source # | |
| SymWord Beverage Source # | |
| SymWord Pet Source # | |
| SymWord Sport Source # | |
| SymWord U2Member Source # | |
| SymWord Location Source # | |
| SymWord Day Source # | |
| SymWord BinOp Source # | |
| SymWord UnOp Source # | |
| SymWord B Source # | |
| SymWord Q Source # | |
| SymWord L Source # | Declare instances to make |
A Symbolic computation. Represented by a reader monad carrying the state of the computation, layered on top of IO for creating unique references to hold onto intermediate results.
label :: SymWord a => String -> SBV a -> SBV a Source #
label: Label the result of an expression. This is essentially a no-op, but useful as it generates a comment in the generated C/SMT-Lib code. Note that if the argument is a constant, then the label is dropped completely, per the usual constant folding strategy.
output :: Outputtable a => a -> Symbolic a Source #
Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.
runSMT :: Symbolic a -> IO a Source #
Run an arbitrary symbolic computation, equivalent to runSMTWith defaultSMTCfg
runSMTWith :: SMTConfig -> Symbolic a -> IO a Source #
Runs an arbitrary symbolic computation, exposed to the user in SAT mode
Module exports
The SBV library exports the following modules wholesale, as user programs will have to import these modules to make any sensible use of the SBV functionality.
module Data.Bits
module Data.Word
module Data.Int
module Data.Ratio