sbv-5.9: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Brian Huffman
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Dynamic

Contents

- Programming with symbolic values
  - Symbolic types
    - Abstract symbolic value type
    - Arrays of symbolic values
  - Creating a symbolic variable
  - Operations on symbolic values
    - Boolean literals
    - Integer literals
    - Float literals
  - Algrebraic reals (only from rationals)
    - Symbolic equality
    - Constructing concrete lists
    - Symbolic ordering
    - Arithmetic operations
    - Logical operations
    - Splitting, joining, and extending
    - Sign-casting
    - Indexed lookups
    - Word-level operations
  - Conditionals: Mergeable values
- Uninterpreted sorts, constants, and functions
- Properties, proofs, and satisfiability
  - Proving properties
  - Checking satisfiability
  - Checking safety
- Proving properties using multiple solvers
- Quick-check
- Model extraction
  - Inspecting proof results
  - Programmable model extraction
- SMT Interface: Configurations and solvers
- Symbolic computations
- Getting SMT-Lib output (for offline analysis)
- Code generation from symbolic programs
  - Setting code-generation options
  - Designating inputs
  - Designating outputs
  - Designating return values
  - Code generation with uninterpreted functions
  - Code generation with `SInteger` and `SReal` types
  - Compilation to C

Description

Dynamically typed low-level API to the SBV library, for users who want to generate symbolic values at run-time. Note that with this API it is possible to create terms that are not type correct; use at your own risk!

Synopsis

- data SVal
- class HasKind a where
  - kindOf :: a -> Kind
  - hasSign :: a -> Bool
  - intSizeOf :: a -> Int
  - isBoolean :: a -> Bool
  - isBounded :: a -> Bool
  - isReal :: a -> Bool
  - isFloat :: a -> Bool
  - isDouble :: a -> Bool
  - isInteger :: a -> Bool
  - isUninterpreted :: a -> Bool
  - showType :: a -> String
- data Kind
  - = KBool
  - | KBounded Bool Int
  - | KUnbounded
  - | KReal
  - | KUserSort String (Either String [String])
  - | KFloat
  - | KDouble
- data CW = CW {
  - _cwKind :: !Kind
  - cwVal :: !CWVal
  }
- data CWVal
  - = CWAlgReal AlgReal
  - | CWInteger Integer
  - | CWFloat Float
  - | CWDouble Double
  - | CWUserSort (Maybe Int, String)
- cwToBool :: CW -> Bool
- data SArr
- readSArr :: SArr -> SVal -> SVal
- resetSArr :: SArr -> SVal -> SArr
- writeSArr :: SArr -> SVal -> SVal -> SArr
- mergeSArr :: SVal -> SArr -> SArr -> SArr
- newSArr :: (Kind, Kind) -> (Int -> String) -> Maybe SVal -> Symbolic SArr
- eqSArr :: SArr -> SArr -> SVal
- data Symbolic a
- data Quantifier
  - = ALL
  - | EX
- svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic SVal
- svTrue :: SVal
- svFalse :: SVal
- svBool :: Bool -> SVal
- svAsBool :: SVal -> Maybe Bool
- svInteger :: Kind -> Integer -> SVal
- svAsInteger :: SVal -> Maybe Integer
- svFloat :: Float -> SVal
- svDouble :: Double -> SVal
- svReal :: Rational -> SVal
- svNumerator :: SVal -> Maybe Integer
- svDenominator :: SVal -> Maybe Integer
- svEqual :: SVal -> SVal -> SVal
- svNotEqual :: SVal -> SVal -> SVal
- svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
- svLessThan :: SVal -> SVal -> SVal
- svGreaterThan :: SVal -> SVal -> SVal
- svLessEq :: SVal -> SVal -> SVal
- svGreaterEq :: SVal -> SVal -> SVal
- svPlus :: SVal -> SVal -> SVal
- svTimes :: SVal -> SVal -> SVal
- svMinus :: SVal -> SVal -> SVal
- svUNeg :: SVal -> SVal
- svAbs :: SVal -> SVal
- svDivide :: SVal -> SVal -> SVal
- svQuot :: SVal -> SVal -> SVal
- svRem :: SVal -> SVal -> SVal
- svExp :: SVal -> SVal -> SVal
- svAnd :: SVal -> SVal -> SVal
- svOr :: SVal -> SVal -> SVal
- svXOr :: SVal -> SVal -> SVal
- svNot :: SVal -> SVal
- svShl :: SVal -> Int -> SVal
- svShr :: SVal -> Int -> SVal
- svRol :: SVal -> Int -> SVal
- svRor :: SVal -> Int -> SVal
- svExtract :: Int -> Int -> SVal -> SVal
- svJoin :: SVal -> SVal -> SVal
- svSign :: SVal -> SVal
- svUnsign :: SVal -> SVal
- svSelect :: [SVal] -> SVal -> SVal -> SVal
- svToWord1 :: SVal -> SVal
- svFromWord1 :: SVal -> SVal
- svTestBit :: SVal -> Int -> SVal
- svShiftLeft :: SVal -> SVal -> SVal
- svShiftRight :: SVal -> SVal -> SVal
- svRotateLeft :: SVal -> SVal -> SVal
- svRotateRight :: SVal -> SVal -> SVal
- svIte :: SVal -> SVal -> SVal -> SVal
- svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
- svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
- svIsSatisfiableInCurrentPath :: SVal -> Symbolic Bool
- svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
- proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
- satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
- allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
- safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
- proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, ThmResult)]
- proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, ThmResult)
- satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, SatResult)]
- satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, SatResult)
- svQuickCheck :: Symbolic SVal -> IO Bool
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- newtype AllSatResult = AllSatResult (Bool, [SMTResult])
- data SMTResult
  - = Unsatisfiable SMTConfig
  - | Satisfiable SMTConfig SMTModel
  - | Unknown SMTConfig SMTModel
  - | ProofError SMTConfig [String]
  - | TimeOut SMTConfig
- genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
- getModel :: SMTResult -> Either String (Bool, [CW])
- getModelDictionary :: SMTResult -> Map String CW
- data SMTConfig = SMTConfig {
  - verbose :: Bool
  - timing :: Bool
  - sBranchTimeOut :: Maybe Int
  - timeOut :: Maybe Int
  - printBase :: Int
  - printRealPrec :: Int
  - solverTweaks :: [String]
  - satCmd :: String
  - isNonModelVar :: String -> Bool
  - smtFile :: Maybe FilePath
  - smtLibVersion :: SMTLibVersion
  - solver :: SMTSolver
  - roundingMode :: RoundingMode
  - useLogic :: Maybe Logic
  }
- data SMTLibVersion = SMTLib2
- data SMTLibLogic
  - = AUFLIA
  - | AUFLIRA
  - | AUFNIRA
  - | LRA
  - | QF_ABV
  - | QF_AUFBV
  - | QF_AUFLIA
  - | QF_AX
  - | QF_BV
  - | QF_IDL
  - | QF_LIA
  - | QF_LRA
  - | QF_NIA
  - | QF_NRA
  - | QF_RDL
  - | QF_UF
  - | QF_UFBV
  - | QF_UFIDL
  - | QF_UFLIA
  - | QF_UFLRA
  - | QF_UFNRA
  - | UFLRA
  - | UFNIA
  - | QF_FPBV
  - | QF_FP
- data Logic
  - = PredefinedLogic SMTLibLogic
  - | CustomLogic String
- data OptimizeOpts
  - = Iterative Bool
  - | Quantified
- data Solver
  - = Z3
  - | Yices
  - | Boolector
  - | CVC4
  - | MathSAT
  - | ABC
- data SMTSolver = SMTSolver {
  - name :: Solver
  - executable :: String
  - options :: [String]
  - engine :: SMTEngine
  - capabilities :: SolverCapabilities
  }
- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- sbvCurrentSolver :: SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- outputSVal :: SVal -> Symbolic ()
- compileToSMTLib :: SMTLibVersion -> Bool -> Symbolic SVal -> IO String
- generateSMTBenchmarks :: Bool -> FilePath -> Symbolic SVal -> IO ()
- data SBVCodeGen a
- cgPerformRTCs :: Bool -> SBVCodeGen ()
- cgSetDriverValues :: [Integer] -> SBVCodeGen ()
- cgGenerateDriver :: Bool -> SBVCodeGen ()
- cgGenerateMakefile :: Bool -> SBVCodeGen ()
- svCgInput :: Kind -> String -> SBVCodeGen SVal
- svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
- svCgOutput :: String -> SVal -> SBVCodeGen ()
- svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
- svCgReturn :: SVal -> SBVCodeGen ()
- svCgReturnArr :: [SVal] -> SBVCodeGen ()
- cgAddPrototype :: [String] -> SBVCodeGen ()
- cgAddDecl :: [String] -> SBVCodeGen ()
- cgAddLDFlags :: [String] -> SBVCodeGen ()
- cgIgnoreSAssert :: Bool -> SBVCodeGen ()
- cgIntegerSize :: Int -> SBVCodeGen ()
- cgSRealType :: CgSRealType -> SBVCodeGen ()
- data CgSRealType
  - = CgFloat
  - | CgDouble
  - | CgLongDouble
- compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
- compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()

# Programming with symbolic values

## Symbolic types

### Abstract symbolic value type

data SVal Source

The Symbolic value. Either a constant (`Left`) or a symbolic value (`Right Cached`). Note that caching is essential for making sure sharing is preserved.

Instances

Eq SVal Source | Equality constraint on SBV values. Not desirable since we can't really compare two symbolic values, but will do.
Show SVal Source | Show instance for `SVal`. Not particularly "desirable", but will do if needed NB. We do not show the type info on constant KBool values, since there's no implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)
NFData SVal Source |
HasKind SVal Source |

class HasKind a where Source

A class for capturing values that have a sign and a size (finite or infinite) minimal complete definition: kindOf. This class can be automatically derived for data-types that have a `Data` instance; this is useful for creating uninterpreted sorts.

Minimal complete definition

Nothing

Methods

kindOf :: a -> Kind Source

hasSign :: a -> Bool Source

intSizeOf :: a -> Int Source

isBoolean :: a -> Bool Source

isBounded :: a -> Bool Source

isReal :: a -> Bool Source

isFloat :: a -> Bool Source

isDouble :: a -> Bool Source

isInteger :: a -> Bool Source

isUninterpreted :: a -> Bool Source

showType :: a -> String Source

Instances

HasKind Bool Source |
HasKind Double Source |
HasKind Float Source |
HasKind Int8 Source |
HasKind Int16 Source |
HasKind Int32 Source |
HasKind Int64 Source |
HasKind Integer Source |
HasKind Word8 Source |
HasKind Word16 Source |
HasKind Word32 Source |
HasKind Word64 Source |
HasKind AlgReal Source |
HasKind Kind Source |
HasKind CW Source | `Kind` instance for CW
HasKind RoundingMode Source | `RoundingMode` kind
HasKind SVal Source |
HasKind E Source |
HasKind Word4 Source | HasKind instance; simply returning the underlying kind for the type
HasKind Sport Source |
HasKind Pet Source |
HasKind Beverage Source |
HasKind Nationality Source |
HasKind Color Source |
HasKind Location Source |
HasKind U2Member Source |
HasKind B Source |
HasKind Q Source |
HasKind L Source | Similarly, `HasKind`s default implementation is sufficient.
HasKind a => HasKind (SBV a) Source |

data Kind Source

Kind of symbolic value

Constructors

KBool |
KBounded Bool Int |
KUnbounded |
KReal |
KUserSort String (Either String [String]) |
KFloat |
KDouble |

Instances

Eq Kind Source | We want to equate user-sorts only by name
Ord Kind Source | We want to order user-sorts only by name
Show Kind Source |
HasKind Kind Source |

data CW Source

`CW` represents a concrete word of a fixed size: Endianness is mostly irrelevant (see the `FromBits` class). For signed words, the most significant digit is considered to be the sign.

Constructors

CW |

Fields

_cwKind :: !Kind
cwVal :: !CWVal

Instances

Eq CW Source |
Ord CW Source |
Show CW Source | Show instance for `CW`.
HasKind CW Source | `Kind` instance for CW
PrettyNum CW Source |
SatModel CW Source | `CW` as extracted from a model; trivial definition
SDivisible CW Source |

data CWVal Source

A constant value

Constructors

CWAlgReal AlgReal | algebraic real
CWInteger Integer | bit-vector/unbounded integer
CWFloat Float | float
CWDouble Double | double
CWUserSort (Maybe Int, String) | value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations

Instances

Eq CWVal Source | Eq instance for CWVal. Note that we cannot simply derive Eq/Ord, since CWAlgReal doesn't have proper instances for these when values are infinitely precise reals. However, we do need a structural eq/ord for Map indexes; so define custom ones here:
Ord CWVal Source | Ord instance for CWVal. Same comments as the `Eq` instance why this cannot be derived.

cwToBool :: CW -> Bool Source

Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)

### Arrays of symbolic values

data SArr Source

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

- 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 `SArr` values
- Typically slower as it heavily relies on SMT-solving for the array theory

readSArr :: SArr -> SVal -> SVal Source

Read the array element at `a`

resetSArr :: SArr -> SVal -> SArr Source

Reset all the elements of the array to the value `b`

writeSArr :: SArr -> SVal -> SVal -> SArr Source

Update the element at `a` to be `b`

mergeSArr :: SVal -> SArr -> SArr -> SArr 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

newSArr :: (Kind, Kind) -> (Int -> String) -> Maybe SVal -> Symbolic SArr Source

Create a named new array, with an optional initial value

eqSArr :: SArr -> SArr -> SVal Source

Compare two arrays for equality

## Creating a symbolic variable

data Symbolic a Source

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.

Instances

Monad Symbolic Source |
Functor Symbolic Source |
Applicative Symbolic Source |
MonadIO Symbolic Source |
Provable Predicate Source |
NFData a => SExecutable (Symbolic a) Source |

data Quantifier Source

Quantifiers: forall or exists. Note that we allow arbitrary nestings.

Constructors

ALL |
EX |

Instances

Eq Quantifier Source |
NFData Quantifier Source |

svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> Symbolic SVal Source

Create a symbolic value, based on the quantifier we have. If an explicit quantifier is given, we just use that. If not, then we pick existential for SAT calls and universal for everything else. `randomCW` is used for generating random values for this variable when used for `quickCheck` purposes.

## Operations on symbolic values

### Boolean literals

svTrue :: SVal Source

Boolean True.

svFalse :: SVal Source

Boolean False.

svBool :: Bool -> SVal Source

Convert from a Boolean.

svAsBool :: SVal -> Maybe Bool Source

Extract a bool, by properly interpreting the integer stored.

### Integer literals

svInteger :: Kind -> Integer -> SVal Source

Convert from an Integer.

svAsInteger :: SVal -> Maybe Integer Source

Extract an integer from a concrete value.

### Float literals

svFloat :: Float -> SVal Source

Convert from a Float

svDouble :: Double -> SVal Source

Convert from a Float

## Algrebraic reals (only from rationals)

svReal :: Rational -> SVal Source

Convert from a Rational

svNumerator :: SVal -> Maybe Integer Source

Grab the numerator of an SReal, if available

svDenominator :: SVal -> Maybe Integer Source

Grab the denominator of an SReal, if available

### Symbolic equality

svEqual :: SVal -> SVal -> SVal Source

Equality.

svNotEqual :: SVal -> SVal -> SVal Source

Inequality.

### Constructing concrete lists

svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal] Source

Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus the lifting to Integers preserves the bounds; and then going back is just fine. So, things like `[1, 5 .. 200] :: [SInt8]` work just fine (end evaluate to empty list), since we see `[1, 5 .. -56]` in the `Integer` domain. Also note the explicit check for `s /= f` below to make sure we don't stutter and produce an infinite list.

### Symbolic ordering

svLessThan :: SVal -> SVal -> SVal Source

Less than.

svGreaterThan :: SVal -> SVal -> SVal Source

Greater than.

svLessEq :: SVal -> SVal -> SVal Source

Less than or equal to.

svGreaterEq :: SVal -> SVal -> SVal Source

Greater than or equal to.

### Arithmetic operations

svPlus :: SVal -> SVal -> SVal Source

Addition.

svTimes :: SVal -> SVal -> SVal Source

Multiplication.

svMinus :: SVal -> SVal -> SVal Source

Subtraction.

svUNeg :: SVal -> SVal Source

Unary minus.

svAbs :: SVal -> SVal Source

Absolute value.

svDivide :: SVal -> SVal -> SVal Source

Division.

svQuot :: SVal -> SVal -> SVal Source

Quotient: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "div" operator (Euclidean division, which always has a non-negative remainder). For unsigned bitvectors, it is "bvudiv"; and for signed bitvectors it is "bvsdiv", which rounds toward zero. All operations have unspecified semantics in case `y = 0`.

svRem :: SVal -> SVal -> SVal Source

Remainder: Overloaded operation whose meaning depends on the kind at which it is used: For unbounded integers, it corresponds to the SMT-Lib "mod" operator (always non-negative). For unsigned bitvectors, it is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds toward zero (sign of remainder matches that of `x`). All operations have unspecified semantics in case `y = 0`.

svExp :: SVal -> SVal -> SVal Source

Exponentiation.

### Logical operations

svAnd :: SVal -> SVal -> SVal Source

Bitwise and.

svOr :: SVal -> SVal -> SVal Source

Bitwise or.

svXOr :: SVal -> SVal -> SVal Source

Bitwise xor.

svNot :: SVal -> SVal Source

Bitwise complement.

svShl :: SVal -> Int -> SVal Source

Shift left by a constant amount. Translates to the "bvshl" operation in SMT-Lib.

svShr :: SVal -> Int -> SVal Source

Shift right by a constant amount. Translates to either "bvlshr" (logical shift right) or "bvashr" (arithmetic shift right) in SMT-Lib, depending on whether `x` is a signed bitvector.

svRol :: SVal -> Int -> SVal Source

Rotate-left, by a constant

svRor :: SVal -> Int -> SVal Source

Rotate-right, by a constant

### Splitting, joining, and extending

svExtract :: Int -> Int -> SVal -> SVal Source

Extract bit-sequences.

svJoin :: SVal -> SVal -> SVal Source

Join two words, by concataneting

### Sign-casting

svSign :: SVal -> SVal Source

Convert a symbolic bitvector from unsigned to signed.

svUnsign :: SVal -> SVal Source

Convert a symbolic bitvector from signed to unsigned.

### Indexed lookups

svSelect :: [SVal] -> SVal -> SVal -> SVal Source

Total indexing operation. `svSelect xs default index` is intuitively the same as `xs !! index`, except it evaluates to `default` if `index` overflows. Translates to SMT-Lib tables.

### Word-level operations

svToWord1 :: SVal -> SVal Source

Convert an SVal from kind Bool to an unsigned bitvector of size 1.

svFromWord1 :: SVal -> SVal Source

Convert an SVal from a bitvector of size 1 (signed or unsigned) to kind Bool.

svTestBit :: SVal -> Int -> SVal Source

Test the value of a bit. Note that we do an extract here as opposed to masking and checking against zero, as we found extraction to be much faster with large bit-vectors.

svShiftLeft :: SVal -> SVal -> SVal Source

Generalization of `svShl`, where the shift-amount is symbolic. The first argument should be a bounded quantity.

svShiftRight :: SVal -> SVal -> SVal Source

Generalization of `svShr`, where the shift-amount is symbolic. The first argument should be a bounded quantity.

NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical.

svRotateLeft :: SVal -> SVal -> SVal Source

Generalization of `svRol`, where the rotation amount is symbolic. The first argument should be a bounded quantity.

svRotateRight :: SVal -> SVal -> SVal Source

Generalization of `svRor`, where the rotation amount is symbolic. The first argument should be a bounded quantity.

## Conditionals: Mergeable values

svIte :: SVal -> SVal -> SVal -> SVal Source

If-then-else. This one will force branches.

svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal Source

Lazy If-then-else. This one will delay forcing the branches unless it's really necessary.

svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal Source

Merge two symbolic values, at kind `k`, possibly `force`'ing the branches to make sure they do not evaluate to the same result.

svIsSatisfiableInCurrentPath :: SVal -> Symbolic Bool Source

Reduce a condition (i.e., try to concretize it) under the given path

# Uninterpreted sorts, constants, and functions

svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal 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.

# Properties, proofs, and satisfiability

## Proving properties

proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult Source

Proves the predicate using the given SMT-solver

## Checking satisfiability

satWith :: SMTConfig -> Symbolic SVal -> IO SatResult Source

Find a satisfying assignment using the given SMT-solver

allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult Source

Find all satisfying assignments using the given SMT-solver

## Checking safety

safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult] Source

Check safety using the given SMT-solver

# Proving properties using multiple solvers

proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, ThmResult)] Source

Prove a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, ThmResult) Source

Prove a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, SatResult)] Source

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The results will be returned in the order produced.

satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, SatResult) Source

Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only the result of the first one to finish will be returned, remaining threads will be killed.

# Quick-check

svQuickCheck :: Symbolic SVal -> IO Bool Source

Dynamic variant of quick-check

# Model extraction

## Inspecting proof results

newtype ThmResult Source

A `prove` call results in a `ThmResult`

Constructors

ThmResult SMTResult |

Instances

Show ThmResult Source | User friendly way of printing theorem results
Modelable ThmResult Source | `ThmResult` as a generic model provider

newtype SatResult Source

A `sat` call results in a `SatResult` The reason for having a separate `SatResult` is to have a more meaningful `Show` instance.

Constructors

SatResult SMTResult |

Instances

Show SatResult Source | User friendly way of printing satisfiablity results
Modelable SatResult Source | `SatResult` as a generic model provider

newtype SafeResult Source

A `safe` call results in a `SafeResult`

Constructors

SafeResult (Maybe String, String, SMTResult) |

Instances

Show SafeResult Source | User friendly way of printing safety results

newtype AllSatResult Source

An `allSat` call results in a `AllSatResult`. The boolean says whether we should warn the user about prefix-existentials.

Constructors

AllSatResult (Bool, [SMTResult]) |

Instances

Show AllSatResult Source | The Show instance of AllSatResults. Note that we have to be careful in being lazy enough as the typical use case is to pull results out as they become available.

data SMTResult Source

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 | Unsatisfiable
Satisfiable SMTConfig SMTModel | Satisfiable with model
Unknown SMTConfig SMTModel | Prover returned unknown, with a potential (possibly bogus) model
ProofError SMTConfig [String] | Prover errored out
TimeOut SMTConfig | Computation timed out (see the `timeout` combinator)

Instances

NFData SMTResult Source |
Modelable SMTResult Source | `SMTResult` as a generic model provider

## Programmable model extraction

genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW]) Source

Parse a signed/sized value from a sequence of CWs

getModel :: SMTResult -> Either String (Bool, [CW]) Source

Extract a model, the result is a tuple where the first argument (if True) indicates whether the model was "probable". (i.e., if the solver returned unknown.)

getModelDictionary :: SMTResult -> 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`.

# SMT Interface: Configurations and solvers

data SMTConfig Source

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

verbose :: Bool

  Debug mode

timing :: Bool

  Print timing information on how long different phases took (construction, solving, etc.)

sBranchTimeOut :: Maybe Int

  How much time to give to the solver for each call of `sBranch` check. (In seconds. Default: No limit.)

timeOut :: Maybe Int

  How much time to give to the solver. (In seconds. Default: No limit.)

printBase :: Int

  Print integral literals in this base (2, 10, and 16 are supported.)

printRealPrec :: Int

  Print algebraic real values with this precision. (SReal, default: 16)

solverTweaks :: [String]

  Additional lines of script to give to the solver (user specified)

satCmd :: String

  Usually "(check-sat)". However, users might tweak it based on solver characteristics.

isNonModelVar :: String -> Bool

  When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)

smtFile :: Maybe FilePath

  If Just, the generated SMT script will be put in this file (for debugging purposes mostly)

smtLibVersion :: SMTLibVersion

  What version of SMT-lib we use for the tool

solver :: SMTSolver

  The actual SMT solver.

roundingMode :: RoundingMode

  Rounding mode to use for floating-point conversions

useLogic :: Maybe Logic

  If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string.

Instances

Show SMTConfig Source |

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 |

Instances

Bounded SMTLibVersion Source |
Enum SMTLibVersion Source |
Eq SMTLibVersion Source |
Show SMTLibVersion Source |
NFData SMTLibVersion Source |

data SMTLibLogic Source

SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the user can override this choice using the `useLogic` parameter to the configuration. This is especially handy if one is experimenting with custom logics that might be supported on new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for the official list.

Constructors

AUFLIA | Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values
AUFLIRA | Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value
AUFNIRA | Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value
LRA | Linear formulas in linear real arithmetic
QF_ABV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays
QF_AUFBV | Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols
QF_AUFLIA | Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols
QF_AX | Quantifier-free formulas over the theory of arrays with extensionality
QF_BV | Quantifier-free formulas over the theory of fixed-size bitvectors
QF_IDL | Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant
QF_LIA | Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables
QF_LRA | Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.
QF_NIA | Quantifier-free integer arithmetic.
QF_NRA | Quantifier-free real arithmetic.
QF_RDL | Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant.
QF_UF | Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.
QF_UFBV | Unquantified formulas over bitvectors with uninterpreted sort function and symbols.
QF_UFIDL | Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols.
QF_UFLIA | Unquantified linear integer arithmetic with uninterpreted sort and function symbols.
QF_UFLRA | Unquantified linear real arithmetic with uninterpreted sort and function symbols.
QF_UFNRA | Unquantified non-linear real arithmetic with uninterpreted sort and function symbols.
UFLRA | Linear real arithmetic with uninterpreted sort and function symbols.
UFNIA | Non-linear integer arithmetic with uninterpreted sort and function symbols.
QF_FPBV | Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors
QF_FP | Quantifier-free formulas over the theory of floating point numbers

Instances

Show SMTLibLogic Source |

data Logic Source

Chosen logic for the solver

Constructors

PredefinedLogic SMTLibLogic | Use one of the logics as defined by the standard
CustomLogic String | Use this name for the logic

Instances

Show Logic Source |

data OptimizeOpts Source

Optimizer configuration. Note that iterative and quantified approaches are in general not interchangeable. For instance, iterative solutions will loop infinitely when there is no optimal value, but quantified solutions can handle such problems. Of course, quantified problems are harder for SMT solvers, naturally.

Constructors

Iterative Bool | Iteratively search. if True, it will be reporting progress
Quantified | Use quantifiers

data Solver Source

Solvers that SBV is aware of

Constructors

Z3 |
Yices |
Boolector |
CVC4 |
MathSAT |
ABC |

Instances

Bounded Solver Source |
Enum Solver Source |
Show Solver Source |

data SMTSolver Source

An SMT solver

Constructors

SMTSolver |

Fields

name :: Solver

  The solver in use

executable :: String

  The path to its executable

options :: [String]

  Options to provide to the solver

engine :: SMTEngine

  The solver engine, responsible for interpreting solver output

capabilities :: SolverCapabilities

  Various capabilities of the solver

Instances

Show SMTSolver Source |

boolector :: SMTConfig Source

Default configuration for the Boolector SMT solver

cvc4 :: SMTConfig Source

Default configuration for the CVC4 SMT Solver.

yices :: SMTConfig Source

Default configuration for the Yices SMT Solver.

z3 :: SMTConfig Source

Default configuration for the Z3 SMT solver

mathSAT :: SMTConfig Source

Default configuration for the MathSAT SMT solver

abc :: SMTConfig Source

Default configuration for the ABC synthesis and verification tool.

defaultSolverConfig :: Solver -> SMTConfig Source

The default configs corresponding to supported SMT solvers

sbvCurrentSolver :: SMTConfig Source

The currently active solver, obtained by importing Data.SBV. To have other solvers current, import one of the bridge modules Data.SBV.Bridge.ABC, Data.SBV.Bridge.Boolector, Data.SBV.Bridge.CVC4, Data.SBV.Bridge.Yices, or Data.SBV.Bridge.Z3 directly.

defaultSMTCfg :: SMTConfig Source

The default solver used by SBV. This is currently set to z3.

sbvCheckSolverInstallation :: SMTConfig -> IO Bool Source

Check whether the given solver is installed and is ready to go. This call does a simple call to the solver to ensure all is well.

sbvAvailableSolvers :: IO [SMTConfig] Source

Return the known available solver configs, installed on your machine.

# Symbolic computations

outputSVal :: SVal -> Symbolic () Source

Mark an interim result as an output. Useful when constructing Symbolic programs that return multiple values, or when the result is programmatically computed.

# Getting SMT-Lib output (for offline analysis)

compileToSMTLib Source

Arguments

:: SMTLibVersion | If True, output SMT-Lib2, otherwise SMT-Lib1
-> Bool | If True, translate directly, otherwise negate the goal. (Use True for SAT queries, False for PROVE queries.)
-> Symbolic SVal |
-> IO String |

Compiles to SMT-Lib and returns the resulting program as a string. Useful for saving the result to a file for off-line analysis, for instance if you have an SMT solver that's not natively supported out-of-the box by the SBV library. It takes two arguments:

- version: The SMTLib-version to produce. Note that we currently only support SMTLib2.
- isSat : If `True`, will translate it as a SAT query, i.e., in the positive. If `False`, will translate as a PROVE query, i.e., it will negate the result. (In this case, the check-sat call to the SMT solver will produce UNSAT if the input is a theorem, as usual.)

generateSMTBenchmarks :: Bool -> FilePath -> Symbolic SVal -> IO () Source

Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with suffix ".smt2". The `Bool` argument controls whether this is a SAT instance, i.e., translate the query directly, or a PROVE instance, i.e., translate the negated query. (See the second boolean argument to `compileToSMTLib` for details.)

# Code generation from symbolic programs

data SBVCodeGen a Source

The code-generation monad. Allows for precise layout of input values reference parameters (for returning composite values in languages such as C), and return values.

Instances

Monad SBVCodeGen Source |
Functor SBVCodeGen Source |
Applicative SBVCodeGen Source |
MonadIO SBVCodeGen Source |

## Setting code-generation options

cgPerformRTCs :: Bool -> SBVCodeGen () Source

Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large value etc. on/off. Default: `False`.

cgSetDriverValues :: [Integer] -> SBVCodeGen () Source

Sets driver program run time values, useful for generating programs with fixed drivers for testing. Default: None, i.e., use random values.

cgGenerateDriver :: Bool -> SBVCodeGen () Source

Should we generate a driver program? Default: `True`. When a library is generated, it will have a driver if any of the contituent functions has a driver. (See `compileToCLib`.)

cgGenerateMakefile :: Bool -> SBVCodeGen () Source

Should we generate a Makefile? Default: `True`.

## Designating inputs

svCgInput :: Kind -> String -> SBVCodeGen SVal Source

Creates an atomic input in the generated code.

svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal] Source

Creates an array input in the generated code.

## Designating outputs

svCgOutput :: String -> SVal -> SBVCodeGen () Source

Creates an atomic output in the generated code.

svCgOutputArr :: String -> [SVal] -> SBVCodeGen () Source

Creates an array output in the generated code.

## Designating return values

svCgReturn :: SVal -> SBVCodeGen () Source

Creates a returned (unnamed) value in the generated code.

svCgReturnArr :: [SVal] -> SBVCodeGen () Source

Creates a returned (unnamed) array value in the generated code.

## Code generation with uninterpreted functions

cgAddPrototype :: [String] -> SBVCodeGen () Source

Adds the given lines to the header file generated, useful for generating programs with uninterpreted functions.

cgAddDecl :: [String] -> SBVCodeGen () Source

Adds the given lines to the program file generated, useful for generating programs with uninterpreted functions.

cgAddLDFlags :: [String] -> SBVCodeGen () Source

Adds the given words to the compiler options in the generated Makefile, useful for linking extra stuff in.

cgIgnoreSAssert :: Bool -> SBVCodeGen () Source

Ignore assertions (those generated by `sAssert` calls) in the generated C code

## Code generation with `SInteger` and `SReal` types

cgIntegerSize :: Int -> SBVCodeGen () Source

Sets number of bits to be used for representing the `SInteger` type in the generated C code. The argument must be one of `8`, `16`, `32`, or `64`. Note that this is essentially unsafe as the semantics of unbounded Haskell integers becomes reduced to the corresponding bit size, as typical in most C implementations.

cgSRealType :: CgSRealType -> SBVCodeGen () Source

Sets the C type to be used for representing the `SReal` type in the generated C code. The setting can be one of C's `"float"`, `"double"`, or `"long double"`, types, depending on the precision needed. Note that this is essentially unsafe as the semantics of infinite precision SReal values becomes reduced to the corresponding floating point type in C, and hence it is subject to rounding errors.

data CgSRealType Source

Possible mappings for the `SReal` type when translated to C. Used in conjunction with the function `cgSRealType`. Note that the particular characteristics of the mapped types depend on the platform and the compiler used for compiling the generated C program. See http://en.wikipedia.org/wiki/C_data_types for details.

Constructors

CgFloat

    float

CgDouble

    double

CgLongDouble

    long double

Instances

Eq CgSRealType Source |
Show CgSRealType Source | `Show` instance for `cgSRealType` displays values as they would be used in a C program

## Compilation to C

compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO () Source

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the C function to generate.
- The final argument is the function to be compiled.

Compilation will also generate a `Makefile`, a header file, and a driver (test) program, etc.

compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO () Source

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

- The first argument is the directory name under which the files will be saved. To save files in the current directory pass ``Just` "."`. Use `Nothing` for printing to stdout.
- The second argument is the name of the archive to generate.
- The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of `compileToC`, except in a list.