Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

- Symbolic types
- Arrays of symbolic values
- Creating symbolic values
- Symbolic Equality and Comparisons
- Conditionals: Mergeable values
- Symbolic integral numbers
- Division and Modulus
- 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

(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.

`>>>`

Q.E.D.`prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)`

`>>>`

Falsifiable. Counter-example: s0 = 32 :: Word8`prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)`

The function `prove`

has the following type:

`prove`

::`Provable`

a => a ->`IO`

`ThmResult`

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 numbers`SFloat`

: IEEE-754 single-precision floating point values`SDouble`

: IEEE-754 double-precision floating point values`SChar`

,`SString`

,`RegExp`

: Characters, strings and regular expressions`SList`

: Symbolic lists (which can be nested)`STuple`

,`STuple2`

,`STuple3`

, ..,`STuple8`

: Symbolic tuples (upto 8-tuples, can be nested)`SEither`

: Symbolic sums`SMaybe`

: Symbolic optional values`SSet`

: Symbolic sets`SArray`

,`SFunArray`

: Flat arrays of symbolic values.- Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs.
- Uninterpreted constants and functions over symbolic values, with user defined SMT-Lib axioms.
- Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
- Model validation: SBV can validate models returned by solvers, which allows
for protection against bugs in SMT solvers and SBV itself. (See the
`validateModel`

parameter.)

The user can construct ordinary Haskell programs using these types, which behave
very similar to their concrete counterparts. In particular these types belong to the
standard classes `Num`

, `Bits`

, custom versions of `Eq`

(`EqSymbolic`

)
and `Ord`

(`OrdSymbolic`

), along with several other custom classes for simplifying
programming with symbolic values. The framework takes full advantage of Haskell's type
inference to avoid many common mistakes.

Furthermore, predicates (i.e., functions that return `SBool`

) built out of
these types can also be:

- proven correct via an external SMT solver (the
`prove`

function) - checked for satisfiability (the
`sat`

,`allSat`

functions) - used in synthesis (the
`sat`

function with existentials) - 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 Stanford: http://cvc4.cs.stanford.edu/web/
- 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.

## Synopsis

- type SBool = SBV Bool
- sTrue :: SBool
- sFalse :: SBool
- sNot :: SBool -> SBool
- (.&&) :: SBool -> SBool -> SBool
- (.||) :: SBool -> SBool -> SBool
- (.<+>) :: SBool -> SBool -> SBool
- (.~&) :: SBool -> SBool -> SBool
- (.~|) :: SBool -> SBool -> SBool
- (.=>) :: SBool -> SBool -> SBool
- (.<=>) :: SBool -> SBool -> SBool
- fromBool :: Bool -> SBool
- oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a
- sAnd :: [SBool] -> SBool
- sOr :: [SBool] -> SBool
- sAny :: (a -> SBool) -> [a] -> SBool
- sAll :: (a -> SBool) -> [a] -> SBool
- type SWord8 = SBV Word8
- type SWord16 = SBV Word16
- type SWord32 = SBV Word32
- type SWord64 = SBV Word64
- type SInt8 = SBV Int8
- type SInt16 = SBV Int16
- type SInt32 = SBV Int32
- type SInt64 = SBV Int64
- type SInteger = SBV Integer
- type SFloat = SBV Float
- type SDouble = SBV Double
- type SReal = SBV AlgReal
- data AlgReal
- sRealToSInteger :: SReal -> SInteger
- type SChar = SBV Char
- type SString = SBV String
- type SList a = SBV [a]
- type STuple a b = SBV (a, b)
- type STuple2 a b = SBV (a, b)
- type STuple3 a b c = SBV (a, b, c)
- type STuple4 a b c d = SBV (a, b, c, d)
- type STuple5 a b c d e = SBV (a, b, c, d, e)
- type STuple6 a b c d e f = SBV (a, b, c, d, e, f)
- type STuple7 a b c d e f g = SBV (a, b, c, d, e, f, g)
- type STuple8 a b c d e f g h = SBV (a, b, c, d, e, f, g, h)
- type SMaybe a = SBV (Maybe a)
- type SEither a b = SBV (Either a b)
- data RCSet a
- = RegularSet (Set a)
- | ComplementSet (Set a)

- type SSet a = SBV (RCSet a)
- class SymArray array where
- newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)
- newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)
- data SArray a b
- data SFunArray a b
- sBool :: String -> Symbolic SBool
- sBool_ :: Symbolic SBool
- sWord8 :: String -> Symbolic SWord8
- sWord8_ :: Symbolic SWord8
- sWord16 :: String -> Symbolic SWord16
- sWord16_ :: Symbolic SWord16
- sWord32 :: String -> Symbolic SWord32
- sWord32_ :: Symbolic SWord32
- sWord64 :: String -> Symbolic SWord64
- sWord64_ :: Symbolic SWord64
- sInt8 :: String -> Symbolic SInt8
- sInt8_ :: Symbolic SInt8
- sInt16 :: String -> Symbolic SInt16
- sInt16_ :: Symbolic SInt16
- sInt32 :: String -> Symbolic SInt32
- sInt32_ :: Symbolic SInt32
- sInt64 :: String -> Symbolic SInt64
- sInt64_ :: Symbolic SInt64
- sInteger :: String -> Symbolic SInteger
- sInteger_ :: Symbolic SInteger
- sReal :: String -> Symbolic SReal
- sReal_ :: Symbolic SReal
- sFloat :: String -> Symbolic SFloat
- sFloat_ :: Symbolic SFloat
- sDouble :: String -> Symbolic SDouble
- sDouble_ :: Symbolic SDouble
- sChar :: String -> Symbolic SChar
- sChar_ :: Symbolic SChar
- sString :: String -> Symbolic SString
- sString_ :: Symbolic SString
- sList :: SymVal a => String -> Symbolic (SList a)
- sList_ :: SymVal a => Symbolic (SList a)
- sTuple :: SymVal tup => String -> Symbolic (SBV tup)
- sTuple_ :: SymVal tup => Symbolic (SBV tup)
- sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b)
- sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b)
- sMaybe :: SymVal a => String -> Symbolic (SMaybe a)
- sMaybe_ :: SymVal a => Symbolic (SMaybe a)
- sSet :: (Ord a, SymVal a) => String -> Symbolic (SSet a)
- sSet_ :: (Ord a, SymVal a) => Symbolic (SSet a)
- sBools :: [String] -> Symbolic [SBool]
- sWord8s :: [String] -> Symbolic [SWord8]
- sWord16s :: [String] -> Symbolic [SWord16]
- sWord32s :: [String] -> Symbolic [SWord32]
- sWord64s :: [String] -> Symbolic [SWord64]
- sInt8s :: [String] -> Symbolic [SInt8]
- sInt16s :: [String] -> Symbolic [SInt16]
- sInt32s :: [String] -> Symbolic [SInt32]
- sInt64s :: [String] -> Symbolic [SInt64]
- sIntegers :: [String] -> Symbolic [SInteger]
- sReals :: [String] -> Symbolic [SReal]
- sFloats :: [String] -> Symbolic [SFloat]
- sDoubles :: [String] -> Symbolic [SDouble]
- sChars :: [String] -> Symbolic [SChar]
- sStrings :: [String] -> Symbolic [SString]
- sLists :: SymVal a => [String] -> Symbolic [SList a]
- sTuples :: SymVal tup => [String] -> Symbolic [SBV tup]
- sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b]
- sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a]
- sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a]
- class EqSymbolic a where
- class (Mergeable a, EqSymbolic a) => OrdSymbolic a where
- class Equality a where
- class Mergeable a where
- ite :: Mergeable a => SBool -> a -> a -> a
- iteLazy :: Mergeable a => SBool -> a -> a -> a
- class (SymVal a, Num a, Bits a, Integral a) => SIntegral a
- class SDivisible a where
- sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b
- sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sRotateLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sRotateRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
- sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a
- sSignedShiftArithRight :: (SFiniteBits a, SIntegral b) => SBV a -> SBV b -> SBV a
- class (Ord a, SymVal a, Num a, Bits a) => SFiniteBits a where
- sFiniteBitSize :: SBV a -> Int
- lsb :: SBV a -> SBool
- msb :: SBV a -> SBool
- blastBE :: SBV a -> [SBool]
- blastLE :: SBV a -> [SBool]
- fromBitsBE :: [SBool] -> SBV a
- fromBitsLE :: [SBool] -> SBV a
- sTestBit :: SBV a -> Int -> SBool
- sExtractBits :: SBV a -> [Int] -> [SBool]
- sPopCount :: SBV a -> SWord8
- setBitTo :: SBV a -> Int -> SBool -> SBV a
- fullAdder :: SBV a -> SBV a -> (SBool, SBV a)
- fullMultiplier :: SBV a -> SBV a -> (SBV a, SBV a)
- sCountLeadingZeros :: SBV a -> SWord8
- sCountTrailingZeros :: SBV a -> SWord8

- class Splittable a b | b -> a where
- (.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
- class (SymVal a, RealFloat a) => IEEEFloating a where
- fpAbs :: SBV a -> SBV a
- fpNeg :: SBV a -> SBV a
- fpAdd :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpSub :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpMul :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpDiv :: SRoundingMode -> SBV a -> SBV a -> SBV a
- fpFMA :: SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
- fpSqrt :: SRoundingMode -> SBV a -> SBV a
- fpRem :: SBV a -> SBV a -> SBV a
- fpRoundToIntegral :: SRoundingMode -> SBV a -> SBV a
- fpMin :: SBV a -> SBV a -> SBV a
- fpMax :: SBV a -> SBV a -> SBV a
- fpIsEqualObject :: SBV a -> SBV a -> SBool
- fpIsNormal :: SBV a -> SBool
- fpIsSubnormal :: SBV a -> SBool
- fpIsZero :: SBV a -> SBool
- fpIsInfinite :: SBV a -> SBool
- fpIsNaN :: SBV a -> SBool
- fpIsNegative :: SBV a -> SBool
- fpIsPositive :: SBV a -> SBool
- fpIsNegativeZero :: SBV a -> SBool
- fpIsPositiveZero :: SBV a -> SBool
- fpIsPoint :: SBV a -> SBool

- data RoundingMode
- type SRoundingMode = SBV RoundingMode
- nan :: Floating a => a
- infinity :: Floating a => a
- sNaN :: (Floating a, SymVal a) => SBV a
- sInfinity :: (Floating a, SymVal a) => SBV a
- sRoundNearestTiesToEven :: SRoundingMode
- sRoundNearestTiesToAway :: SRoundingMode
- sRoundTowardPositive :: SRoundingMode
- sRoundTowardNegative :: SRoundingMode
- sRoundTowardZero :: SRoundingMode
- sRNE :: SRoundingMode
- sRNA :: SRoundingMode
- sRTP :: SRoundingMode
- sRTN :: SRoundingMode
- sRTZ :: SRoundingMode
- class SymVal a => IEEEFloatConvertible a where
- fromSFloat :: SRoundingMode -> SFloat -> SBV a
- toSFloat :: SRoundingMode -> SBV a -> SFloat
- fromSDouble :: SRoundingMode -> SDouble -> SBV a
- toSDouble :: SRoundingMode -> SBV a -> SDouble

- sFloatAsSWord32 :: SFloat -> SWord32
- sWord32AsSFloat :: SWord32 -> SFloat
- sDoubleAsSWord64 :: SDouble -> SWord64
- sWord64AsSDouble :: SWord64 -> SDouble
- blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
- blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
- mkSymbolicEnumeration :: Name -> Q [Dec]
- class Uninterpreted a where
- uninterpret :: String -> a
- cgUninterpret :: String -> [String] -> a -> a
- sbvUninterpret :: Maybe ([String], a) -> String -> a

- addAxiom :: String -> [String] -> Symbolic ()
- type Predicate = Symbolic SBool
- type Goal = Symbolic ()
- type Provable = MProvable IO
- forAll_ :: Provable a => a -> Symbolic SBool
- forAll :: Provable a => [String] -> a -> Symbolic SBool
- forSome_ :: Provable a => a -> Symbolic SBool
- forSome :: Provable a => [String] -> a -> Symbolic SBool
- prove :: Provable a => a -> IO ThmResult
- proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
- sat :: Provable a => a -> IO SatResult
- satWith :: Provable a => SMTConfig -> a -> IO SatResult
- allSat :: Provable a => a -> IO AllSatResult
- allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
- optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult
- optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
- isVacuous :: Provable a => a -> IO Bool
- isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
- isTheorem :: Provable a => a -> IO Bool
- isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool
- isSatisfiable :: Provable a => a -> IO Bool
- isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool
- proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
- proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
- satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
- satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
- generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String
- solve :: [SBool] -> Symbolic SBool
- constrain :: SolverContext m => SBool -> m ()
- softConstrain :: SolverContext m => SBool -> m ()
- namedConstraint :: SolverContext m => String -> SBool -> m ()
- constrainWithAttribute :: SolverContext m => [(String, String)] -> SBool -> m ()
- pbAtMost :: [SBool] -> Int -> SBool
- pbAtLeast :: [SBool] -> Int -> SBool
- pbExactly :: [SBool] -> Int -> SBool
- pbLe :: [(Int, SBool)] -> Int -> SBool
- pbGe :: [(Int, SBool)] -> Int -> SBool
- pbEq :: [(Int, SBool)] -> Int -> SBool
- pbMutexed :: [SBool] -> SBool
- pbStronglyMutexed :: [SBool] -> SBool
- sAssert :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a
- isSafe :: SafeResult -> Bool
- class ExtractIO m => SExecutable m a
- sName_ :: SExecutable IO a => a -> Symbolic ()
- sName :: SExecutable IO a => [String] -> a -> Symbolic ()
- safe :: SExecutable IO a => a -> IO [SafeResult]
- safeWith :: SExecutable IO a => SMTConfig -> a -> IO [SafeResult]
- sbvQuickCheck :: Symbolic SBool -> IO Bool
- data OptimizeStyle
- = Lexicographic
- | Independent
- | Pareto (Maybe Int)

- data Objective a
- class Metric a where
- type MetricSpace a :: *
- toMetricSpace :: SBV a -> SBV (MetricSpace a)
- fromMetricSpace :: SBV (MetricSpace a) -> SBV a
- msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()
- msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m ()

- minimize :: Metric a => String -> SBV a -> Symbolic ()
- maximize :: Metric a => String -> SBV a -> Symbolic ()
- assertWithPenalty :: String -> SBool -> Penalty -> Symbolic ()
- data Penalty
- data ExtCV
- data GeneralizedCV
- newtype ThmResult = ThmResult SMTResult
- newtype SatResult = SatResult SMTResult
- newtype AllSatResult = AllSatResult (Bool, Bool, Bool, [SMTResult])
- newtype SafeResult = SafeResult (Maybe String, String, SMTResult)
- data OptimizeResult
- data SMTResult
- data SMTReasonUnknown
- observe :: SymVal a => String -> SBV a -> SBV a
- observeIf :: SymVal a => (a -> Bool) -> String -> SBV a -> SBV a
- class SatModel a where
- class Modelable a where
- modelExists :: a -> Bool
- getModelAssignment :: SatModel b => a -> Either String (Bool, b)
- getModelDictionary :: a -> Map String CV
- getModelValue :: SymVal b => String -> a -> Maybe b
- getModelUninterpretedValue :: String -> a -> Maybe String
- extractModel :: SatModel b => a -> Maybe b
- getModelObjectives :: a -> Map String GeneralizedCV
- getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
- getModelUIFuns :: a -> Map String (SBVType, ([([CV], CV)], CV))
- getModelUIFunValue :: String -> a -> Maybe (SBVType, ([([CV], CV)], CV))

- displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
- extractModels :: SatModel a => AllSatResult -> [a]
- getModelDictionaries :: AllSatResult -> [Map String CV]
- getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b]
- getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- satTrackUFs :: Bool
- isNonModelVar :: String -> Bool
- validateModel :: Bool
- optimizeValidateConstraints :: Bool
- transcript :: Maybe FilePath
- smtLibVersion :: SMTLibVersion
- solver :: SMTSolver
- allowQuantifiedQueries :: Bool
- roundingMode :: RoundingMode
- solverSetOptions :: [SMTOption]
- ignoreExitCode :: Bool
- redirectVerbose :: Maybe FilePath

- data Timing
- data SMTLibVersion = SMTLib2
- data Solver
- data SMTSolver = SMTSolver {
- name :: Solver
- executable :: String
- preprocess :: String -> String
- options :: SMTConfig -> [String]
- engine :: SMTEngine
- capabilities :: SolverCapabilities

- boolector :: SMTConfig
- cvc4 :: SMTConfig
- yices :: SMTConfig
- z3 :: SMTConfig
- mathSAT :: SMTConfig
- abc :: SMTConfig
- defaultSolverConfig :: Solver -> SMTConfig
- defaultSMTCfg :: SMTConfig
- sbvCheckSolverInstallation :: SMTConfig -> IO Bool
- sbvAvailableSolvers :: IO [SMTConfig]
- setLogic :: SolverContext m => Logic -> m ()
- data Logic
- setOption :: SolverContext m => SMTOption -> m ()
- setInfo :: SolverContext m => String -> [String] -> m ()
- setTimeOut :: SolverContext m => Integer -> m ()
- data SBVException = SBVException {
- sbvExceptionDescription :: String
- sbvExceptionSent :: Maybe String
- sbvExceptionExpected :: Maybe String
- sbvExceptionReceived :: Maybe String
- sbvExceptionStdOut :: Maybe String
- sbvExceptionStdErr :: Maybe String
- sbvExceptionExitCode :: Maybe ExitCode
- sbvExceptionConfig :: SMTConfig
- sbvExceptionReason :: Maybe [String]
- sbvExceptionHint :: Maybe [String]

- data SBV a
- class HasKind a where
- kindOf :: a -> Kind
- hasSign :: a -> Bool
- intSizeOf :: a -> Int
- isBoolean :: a -> Bool
- isBounded :: a -> Bool
- isReal :: a -> Bool
- isFloat :: a -> Bool
- isDouble :: a -> Bool
- isUnbounded :: a -> Bool
- isUninterpreted :: a -> Bool
- isChar :: a -> Bool
- isString :: a -> Bool
- isList :: a -> Bool
- isSet :: a -> Bool
- isTuple :: a -> Bool
- isMaybe :: a -> Bool
- isEither :: a -> Bool
- showType :: a -> String

- data Kind
- class (HasKind a, Typeable a) => SymVal a
- forall :: SymVal a => String -> Symbolic (SBV a)
- forall_ :: SymVal a => Symbolic (SBV a)
- mkForallVars :: SymVal a => Int -> Symbolic [SBV a]
- exists :: SymVal a => String -> Symbolic (SBV a)
- exists_ :: SymVal a => Symbolic (SBV a)
- mkExistVars :: SymVal a => Int -> Symbolic [SBV a]
- free :: SymVal a => String -> Symbolic (SBV a)
- free_ :: SymVal a => Symbolic (SBV a)
- mkFreeVars :: SymVal a => Int -> Symbolic [SBV a]
- symbolic :: SymVal a => String -> Symbolic (SBV a)
- symbolics :: SymVal a => [String] -> Symbolic [SBV a]
- literal :: SymVal a => a -> SBV a
- unliteral :: SymVal a => SBV a -> Maybe a
- fromCV :: SymVal a => CV -> a
- isConcrete :: SymVal a => SBV a -> Bool
- isSymbolic :: SymVal a => SBV a -> Bool
- isConcretely :: SymVal a => SBV a -> (a -> Bool) -> Bool
- mkSymVal :: SymVal a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
- class MonadIO m => MonadSymbolic m where
- symbolicEnv :: m State

- type Symbolic = SymbolicT IO
- data SymbolicT m a
- label :: SymVal a => String -> SBV a -> SBV a
- output :: Outputtable a => a -> Symbolic a
- runSMT :: Symbolic a -> IO a
- runSMTWith :: SMTConfig -> Symbolic a -> IO a
- module Data.Bits
- module Data.Word
- module Data.Int
- module Data.Ratio

# Documentation

The SBV library is really two things:

- A framework for writing symbolic programs in Haskell, i.e., programs operating on symbolic values along with the usual concrete counterparts.
- A framework for proving properties of such programs using SMT solvers.

The programming goal of SBV is to provide a *seamless* experience, i.e., let people program
in the usual Haskell style without distractions of symbolic coding. While Haskell helps
in some aspects (the `Num`

and `Bits`

classes simplify coding), it makes life harder
in others. For instance, `if-then-else`

only takes `Bool`

as a test in Haskell, and
comparisons (`>`

etc.) only return `Bool`

s. Clearly we would like these values to be
symbolic (i.e., `SBool`

), thus stopping us from using some native Haskell constructs.
When symbolic versions of operators are needed, they are typically obtained by prepending a dot,
for instance `==`

becomes `.==`

. Care has been taken to make the transition painless. In
particular, any Haskell program you build out of symbolic components is fully concretely
executable within Haskell, without the need for any custom interpreters. (They are truly
Haskell programs, not AST's built out of pieces of syntax.) This provides for an integrated
feel of the system, one of the original design goals for SBV.

Incremental query mode: SBV provides a wide variety of ways to utilize 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

### Boolean values and functions

oneIf :: (Ord a, Num a, SymVal a) => SBool -> SBV a Source #

Returns 1 if the boolean is `sTrue`

, otherwise 0.

### Logical aggregations

## 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`

,`#`

, and`extend`

(see the`Splittable`

class)

Usual arithmetic (`+`

, `-`

, `*`

, `sQuotRem`

, `sQuot`

, `sRem`

, `sDivMod`

, `sDiv`

, `sMod`

) and logical operations (`.<`

, `.<=`

, `.>`

, `.>=`

, `.==`

, `./=`

) operations are
supported for `SInteger`

fully, both in programming and verification modes.

## Floating point numbers

Floating point numbers are defined by the 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

sRealToSInteger :: SReal -> SInteger Source #

Convert an SReal to an SInteger. That is, it computes the
largest integer `n`

that satisfies `sIntegerToSReal n <= r`

essentially giving us the `floor`

.

For instance, `1.3`

will be `1`

, but `-1.3`

will be `-2`

.

## Characters, Strings and Regular Expressions

Support for characters, strings, and regular expressions (intial version contributed by Joel Burget) adds support for QF_S logic, described here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml and here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.Char, Data.SBV.String, Data.SBV.RegExp for related functions.

type SChar = SBV Char Source #

A symbolic character. Note that, as far as SBV's symbolic strings are concerned, a character
is currently an 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

type SString = SBV String Source #

A symbolic string. Note that a symbolic string is *not* a list of symbolic characters,
that is, it is not the case that `SString = [SChar]`

, unlike what one might expect following
Haskell strings. An `SString`

is a symbolic value of its own, of possibly arbitrary but finite length,
and internally processed as one unit as opposed to a fixed-length list of characters.

## Symbolic lists

Support for symbolic lists (intial version contributed by Joel Burget) adds support for sequence support, described here: http://rise4fun.com/z3/tutorialcontent/sequences. Note that this logic is still not part of official SMTLib (as of March 2018), so it should be considered experimental.

See Data.SBV.List for related functions.

type SList a = SBV [a] Source #

A symbolic list of items. Note that a symbolic list is *not* a list of symbolic items,
that is, it is not the case that `SList a = [a]`

, unlike what one might expect following
haskell lists/sequences. An `SList`

is a symbolic value of its own, of possibly arbitrary but finite
length, and internally processed as one unit as opposed to a fixed-length list of items.
Note that lists can be nested, i.e., we do allow lists of lists of ... items.

## Tuples

Tuples can be used as symbolic values. This is useful in combination with lists, for example `SBV [(Integer, String)]`

is a valid type. These types can be arbitrarily nested, eg `SBV [(Integer, [(Char, (Integer, String))])]`

. Instances of upto 8-tuples are provided.

## Sum types

## Sets

A `RCSet`

is either a regular set or a set given by its complement from the corresponding universal set.

RegularSet (Set a) | |

ComplementSet (Set a) |

## Instances

# Arrays of symbolic values

class SymArray array where Source #

Flat arrays of symbolic values
An `array a b`

is an array indexed by the type

, with elements of type `SBV`

a

.`SBV`

b

If a default value is supplied, then all the array elements will be initialized to this value. Otherwise, they will be left unspecified, i.e., a read from an unwritten location will produce an uninterpreted constant.

While it's certainly possible for user to create instances of `SymArray`

, the
`SArray`

and `SFunArray`

instances already provided should cover most use cases
in practice. Note that there are a few differences between these two models in
terms of use models:

`SArray`

produces SMTLib arrays, and requires a solver that understands the array theory.`SFunArray`

is internally handled, and thus can be used with any solver. (Note that all solvers except`abc`

support arrays, so this isn't a big decision factor.)- For both arrays, if a default value is supplied, then reading from uninitialized cell will return that value. If the default is not given, then reading from uninitialized cells is still OK for both arrays, and will produce an uninterpreted constant in both cases.
- Only
`SArray`

supports checking equality of arrays. (That is, checking if an entire array is equivalent to another.)`SFunArray`

s cannot be checked for equality. In general, checking wholesale equality of arrays is a difficult decision problem and should be avoided if possible. - Only
`SFunArray`

supports compilation to C. Programs using`SArray`

will not be accepted by the C-code generator. - You cannot use quickcheck on programs that contain these arrays. (Neither
`SArray`

nor`SFunArray`

.) - With
`SArray`

, SBV transfers all array-processing to the SMT-solver. So, it can generate programs more quickly, but they might end up being too hard for the solver to handle. With`SFunArray`

, SBV only generates code for individual elements and the array itself never shows up in the resulting SMTLib program. This puts more onus on the SBV side and might have some performance impacts, but it might generate problems that are easier for the SMT solvers to handle.

As a rule of thumb, try `SArray`

first. These should generate compact code. However, if
the backend solver has hard time solving the generated problems, switch to
`SFunArray`

. If you still have issues, please report so we can see what the problem might be!

readArray :: array a b -> SBV a -> SBV b Source #

Read the array element at `a`

writeArray :: SymVal b => array a b -> SBV a -> SBV b -> array a b Source #

Update the element at `a`

to be `b`

mergeArrays :: SymVal b => SBV Bool -> array a b -> array a b -> array a b Source #

Merge two given arrays on the symbolic condition
Intuitively: `mergeArrays cond a b = if cond then a else b`

.
Merging pushes the if-then-else choice down on to elements

## Instances

newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b) Source #

Create a new anonymous array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see `newArray_`

newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b) Source #

Create a named new array, possibly with a default initial value.

NB. For a version which generalizes over the underlying monad, see `newArray`

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

- Maps directly to SMT-lib arrays
- Reading from an unintialized value is OK. If the default value is given in
`newArray`

, it will be the result. Otherwise, the read yields an uninterpreted constant. - Can check for equality of these arrays
- Cannot be used in code-generation (i.e., compilation to C)
- Cannot quick-check theorems using
`SArray`

values - Typically slower as it heavily relies on SMT-solving for the array theory

## Instances

Arrays implemented internally, without translating to SMT-Lib functions:

- Internally handled by the library and not mapped to SMT-Lib, hence can be used with solvers that don't support arrays. (Such as abc.)
- Reading from an unintialized value is OK. If the default value is given in
`newArray`

, it will be the result. Otherwise, the read yields an uninterpreted constant. - Cannot check for equality of arrays.
- Can be used in code-generation (i.e., compilation to C).
- Can not quick-check theorems using
`SFunArray`

values - Typically faster as it gets compiled away during translation.

## Instances

# Creating symbolic values

## Single value

These functions simplify declaring symbolic variables of various types. Strictly speaking, they are just synonyms
for `free`

(specialized at the given type), but they might be easier to use. We provide both the named and anonymous
versions, latter with the underscore suffix.

sTuple :: SymVal tup => String -> Symbolic (SBV tup) Source #

Declare a named tuple.

NB. For a version which generalizes over the underlying monad, see `sTuple`

sTuple_ :: SymVal tup => Symbolic (SBV tup) Source #

Declare an unnamed tuple.

NB. For a version which generalizes over the underlying monad, see `sTuple_`

## List of values

These functions simplify declaring a sequence symbolic variables of various types. Strictly speaking, they are just synonyms
for `mapM`

`free`

(specialized at the given type), but they might be easier to use.

sTuples :: SymVal tup => [String] -> Symbolic [SBV tup] Source #

Declare a list of tuples.

NB. For a version which generalizes over the underlying monad, see `sTuples`

# Symbolic Equality and Comparisons

class EqSymbolic a where Source #

Symbolic Equality. Note that we can't use Haskell's `Eq`

class since Haskell insists on returning Bool
Comparing symbolic values will necessarily return a symbolic value.

(.==) :: a -> a -> SBool infix 4 Source #

Symbolic equality.

(./=) :: a -> a -> SBool infix 4 Source #

Symbolic inequality.

(.===) :: a -> a -> SBool infix 4 Source #

Strong equality. On floats ('SFloat'/'SDouble'), strong equality is object equality; that
is `NaN == NaN`

holds, but `+0 == -0`

doesn't. On other types, (.===) is simply (.==).
Note that (.==) is the *right* notion of equality for floats per IEEE754 specs, since by
definition `+0 == -0`

and `NaN`

equals no other value including itself. But occasionally
we want to be stronger and state `NaN`

equals `NaN`

and `+0`

and `-0`

are different from
each other. In a context where your type is concrete, simply use `fpIsEqualObject`

. But in
a polymorphic context, use the strong equality instead.

NB. If you do not care about or work with floats, simply use (.==) and (./=).

(./==) :: a -> a -> SBool infix 4 Source #

Negation of strong equality. Equaivalent to negation of (.===) on all types.

distinct :: [a] -> SBool Source #

Returns (symbolic) `sTrue`

if all the elements of the given list are different.

allEqual :: [a] -> SBool Source #

Returns (symbolic) `sTrue`

if all the elements of the given list are the same.

sElem :: a -> [a] -> SBool Source #

Symbolic membership test.

## Instances

EqSymbolic Bool Source # | |

Defined in Data.SBV.Core.Model | |

EqSymbolic a => EqSymbolic [a] Source # | |

EqSymbolic a => EqSymbolic (Maybe a) Source # | |

EqSymbolic (SBV a) Source # | |

Defined in Data.SBV.Core.Model | |

EqSymbolic a => EqSymbolic (S a) Source # | Symbolic equality for |

Defined in Documentation.SBV.Examples.ProofTools.BMC | |

(EqSymbolic a, EqSymbolic b) => EqSymbolic (Either a b) Source # | |

Defined in Data.SBV.Core.Model | |

(EqSymbolic a, EqSymbolic b) => EqSymbolic (a, b) Source # | |

Defined in Data.SBV.Core.Model | |

EqSymbolic (SArray a b) Source # | |

Defined in Data.SBV.Core.Model | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c) => EqSymbolic (a, b, c) Source # | |

Defined in Data.SBV.Core.Model | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d) => EqSymbolic (a, b, c, d) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.===) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (./==) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # distinct :: [(a, b, c, d)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e) => EqSymbolic (a, b, c, d, e) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.===) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (./==) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # distinct :: [(a, b, c, d, e)] -> SBool Source # allEqual :: [(a, b, c, d, e)] -> SBool Source # sElem :: (a, b, c, d, e) -> [(a, b, c, d, e)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f) => EqSymbolic (a, b, c, d, e, f) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.===) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (./==) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # distinct :: [(a, b, c, d, e, f)] -> SBool Source # allEqual :: [(a, b, c, d, e, f)] -> SBool Source # sElem :: (a, b, c, d, e, f) -> [(a, b, c, d, e, f)] -> SBool Source # | |

(EqSymbolic a, EqSymbolic b, EqSymbolic c, EqSymbolic d, EqSymbolic e, EqSymbolic f, EqSymbolic g) => EqSymbolic (a, b, c, d, e, f, g) Source # | |

Defined in Data.SBV.Core.Model (.==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.===) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (./==) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # distinct :: [(a, b, c, d, e, f, g)] -> SBool Source # allEqual :: [(a, b, c, d, e, f, g)] -> SBool Source # sElem :: (a, b, c, d, e, f, g) -> [(a, b, c, d, e, f, g)] -> SBool Source # |

class (Mergeable a, EqSymbolic a) => OrdSymbolic a where Source #

Symbolic Comparisons. Similar to `Eq`

, we cannot implement Haskell's `Ord`

class
since there is no way to return an `Ordering`

value from a symbolic comparison.
Furthermore, `OrdSymbolic`

requires `Mergeable`

to implement if-then-else, for the
benefit of implementing symbolic versions of `max`

and `min`

functions.

(.<) :: a -> a -> SBool infix 4 Source #

Symbolic less than.

(.<=) :: a -> a -> SBool infix 4 Source #

Symbolic less than or equal to.

(.>) :: a -> a -> SBool infix 4 Source #

Symbolic greater than.

(.>=) :: a -> a -> SBool infix 4 Source #

Symbolic greater than or equal to.

Symbolic minimum.

Symbolic maximum.

inRange :: a -> (a, a) -> SBool Source #

Is the value withing the allowed *inclusive* range?

## Instances

OrdSymbolic a => OrdSymbolic [a] Source # | |

OrdSymbolic a => OrdSymbolic (Maybe a) Source # | |

Defined in Data.SBV.Core.Model | |

(Ord a, SymVal a) => OrdSymbolic (SBV a) Source # | |

Defined in Data.SBV.Core.Model | |

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (Either a b) Source # | |

Defined in Data.SBV.Core.Model (.<) :: Either a b -> Either a b -> SBool Source # (.<=) :: Either a b -> Either a b -> SBool Source # (.>) :: Either a b -> Either a b -> SBool Source # (.>=) :: Either a b -> Either a b -> SBool Source # smin :: Either a b -> Either a b -> Either a b Source # smax :: Either a b -> Either a b -> Either a b Source # inRange :: Either a b -> (Either a b, Either a b) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b) => OrdSymbolic (a, b) Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c) => OrdSymbolic (a, b, c) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c) -> (a, b, c) -> SBool Source # (.<=) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>) :: (a, b, c) -> (a, b, c) -> SBool Source # (.>=) :: (a, b, c) -> (a, b, c) -> SBool Source # smin :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # smax :: (a, b, c) -> (a, b, c) -> (a, b, c) Source # inRange :: (a, b, c) -> ((a, b, c), (a, b, c)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d) => OrdSymbolic (a, b, c, d) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.<=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # (.>=) :: (a, b, c, d) -> (a, b, c, d) -> SBool Source # smin :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # smax :: (a, b, c, d) -> (a, b, c, d) -> (a, b, c, d) Source # inRange :: (a, b, c, d) -> ((a, b, c, d), (a, b, c, d)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e) => OrdSymbolic (a, b, c, d, e) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.<=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # (.>=) :: (a, b, c, d, e) -> (a, b, c, d, e) -> SBool Source # smin :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # smax :: (a, b, c, d, e) -> (a, b, c, d, e) -> (a, b, c, d, e) Source # inRange :: (a, b, c, d, e) -> ((a, b, c, d, e), (a, b, c, d, e)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f) => OrdSymbolic (a, b, c, d, e, f) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.<=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # (.>=) :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> SBool Source # smin :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # smax :: (a, b, c, d, e, f) -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source # inRange :: (a, b, c, d, e, f) -> ((a, b, c, d, e, f), (a, b, c, d, e, f)) -> SBool Source # | |

(OrdSymbolic a, OrdSymbolic b, OrdSymbolic c, OrdSymbolic d, OrdSymbolic e, OrdSymbolic f, OrdSymbolic g) => OrdSymbolic (a, b, c, d, e, f, g) Source # | |

Defined in Data.SBV.Core.Model (.<) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.<=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # (.>=) :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> SBool Source # smin :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # smax :: (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source # inRange :: (a, b, c, d, e, f, g) -> ((a, b, c, d, e, f, g), (a, b, c, d, e, f, g)) -> SBool Source # |

class Equality a where Source #

Equality as a proof method. Allows for very concise construction of equivalence proofs, which is very typical in bit-precise proofs.

## Instances

# Conditionals: Mergeable values

class Mergeable a where Source #

Symbolic conditionals are modeled by the `Mergeable`

class, describing
how to merge the results of an 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`

.

Nothing

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 :: (Ord b, SymVal b, Num b) => [a] -> a -> SBV b -> a Source #

Total indexing operation. `select xs default index`

is intuitively
the same as `xs !! index`

, except it evaluates to `default`

if `index`

underflows/overflows.

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 (SymVal a, Num a, Bits a, Integral a) => SIntegral a Source #

Symbolic Numbers. This is a simple class that simply incorporates all number like
base types together, simplifying writing polymorphic 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

SIntegral Int8 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int16 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int32 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Int64 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Integer Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word8 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word16 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word32 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word64 Source # | |

Defined in Data.SBV.Core.Model | |

SIntegral Word4 Source # | SIntegral instance, using default methods |

Defined in Documentation.SBV.Examples.Misc.Word4 |

# Division and Modulus

class SDivisible a where Source #

The `SDivisible`

class captures the essence of division.
Unfortunately we cannot use Haskell's `Integral`

class since the `Real`

and `Enum`

superclasses are not implementable for symbolic 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:

x`sQuotRem`

0 = (0, x) x`sDivMod`

0 = (0, x)

Note that our instances implement this law even when `x`

is `0`

itself.

NB. `quot`

truncates toward zero, while `div`

truncates toward negative infinity.

## Instances

SDivisible Int8 Source # | |

SDivisible Int16 Source # | |

SDivisible Int32 Source # | |

SDivisible Int64 Source # | |

SDivisible Integer Source # | |

SDivisible Word8 Source # | |

SDivisible Word16 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible Word32 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible Word64 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible CV Source # | |

SDivisible SInteger Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible SInt64 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible SInt32 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible SInt16 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible SInt8 Source # | |

SDivisible SWord64 Source # | |

SDivisible SWord32 Source # | |

SDivisible SWord16 Source # | |

SDivisible SWord8 Source # | |

Defined in Data.SBV.Core.Model | |

SDivisible SWord4 Source # | SDvisible instance, using default methods |

Defined in Documentation.SBV.Examples.Misc.Word4 | |

SDivisible Word4 Source # | SDvisible instance, using 0-extension |

Defined in Documentation.SBV.Examples.Misc.Word4 |

# Bit-vector operations

## Conversions

sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b, SymVal b) => SBV a -> SBV b Source #

Conversion between 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.

sBarrelRotateLeft :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #

An implementation of rotate-left, using a barrel shifter like design. Only works when both
arguments are finite bitvectors, and furthermore when the second argument is unsigned.
The first condition is enforced by the type, but the second is dynamically checked.
We provide this implementation as an alternative to `sRotateLeft`

since SMTLib logic
does not support variable argument rotates (as opposed to shifts), and thus this
implementation can produce better code for verification compared to `sRotateLeft`

.

`>>>`

Q.E.D.`prove $ \x y -> (x `sBarrelRotateLeft` y) `sBarrelRotateRight` (y :: SWord32) .== (x :: SWord64)`

sBarrelRotateRight :: (SFiniteBits a, SFiniteBits b) => SBV a -> SBV b -> SBV a Source #

An implementation of rotate-right, using a barrel shifter like design. See comments
for `sBarrelRotateLeft`

for details.

`>>>`

Q.E.D.`prove $ \x y -> (x `sBarrelRotateRight` y) `sBarrelRotateLeft` (y :: SWord32) .== (x :: SWord64)`

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 (Ord a, SymVal 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`

.

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.

## Instances

## Splitting, joining, and extending

class Splittable a b | b -> a where Source #

Splitting an `a`

into two `b`

's and joining back.
Intuitively, `a`

is a larger bit-size word than `b`

, typically double.
The `extend`

operation captures embedding of a `b`

value into an `a`

without changing its semantic value.

## Instances

Splittable Word8 Word4 Source # | Joining |

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 (SymVal 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.

Nothing

fpAbs :: SBV a -> SBV a Source #

Compute the floating point absolute value.

fpNeg :: SBV a -> SBV a Source #

Compute the unary negation. Note that `0 - x`

is not equivalent to `-x`

for 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

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.

RoundNearestTiesToEven | Round to nearest representable floating point value.
If precisely at half-way, pick the even number.
(In this context, |

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

type SRoundingMode = SBV RoundingMode Source #

The symbolic variant of `RoundingMode`

## Rounding modes

sRoundNearestTiesToEven :: SRoundingMode Source #

Symbolic variant of `RoundNearestTiesToEven`

sRoundNearestTiesToAway :: SRoundingMode Source #

Symbolic variant of `RoundNearestTiesToAway`

sRoundTowardPositive :: SRoundingMode Source #

Symbolic variant of `RoundTowardPositive`

sRoundTowardNegative :: SRoundingMode Source #

Symbolic variant of `RoundTowardNegative`

sRoundTowardZero :: SRoundingMode Source #

Symbolic variant of `RoundTowardZero`

sRNE :: SRoundingMode Source #

Alias for `sRoundNearestTiesToEven`

sRNA :: SRoundingMode Source #

Alias for `sRoundNearestTiesToAway`

sRTP :: SRoundingMode Source #

Alias for `sRoundTowardPositive`

sRTN :: SRoundingMode Source #

Alias for `sRoundTowardNegative`

sRTZ :: SRoundingMode Source #

Alias for `sRoundTowardZero`

## Conversion to/from floats

class SymVal a => IEEEFloatConvertible a where Source #

Capture convertability from/to FloatingPoint representations.

Conversions to float: `toSFloat`

and `toSDouble`

simply return the
nearest representable float from the given type based on the rounding
mode provided.

Conversions from float: `fromSFloat`

and `fromSDouble`

functions do
the reverse conversion. However some care is needed when given values
that are not representable in the integral target domain. For instance,
converting an `SFloat`

to an `SInt8`

is problematic. The rules are as follows:

If the input value is a finite point and when rounded in the given rounding mode to an integral value lies within the target bounds, then that result is returned. (This is the regular interpretation of rounding in IEEE754.)

Otherwise (i.e., if the integral value in the float or double domain) doesn't
fit into the target type, then the result is unspecified. Note that if the input
is `+oo`

, `-oo`

, or `NaN`

, then the result is unspecified.

Due to the unspecified nature of conversions, SBV will never constant fold conversions from floats to integral values. That is, you will always get a symbolic value as output. (Conversions from floats to other floats will be constant folded. Conversions from integral values to floats will also be constant folded.)

Note that unspecified really means unspecified: In particular, SBV makes
no guarantees about matching the behavior between what you might get in
Haskell, via SMT-Lib, or the C-translation. If the input value is out-of-bounds
as defined above, or is `NaN`

or `oo`

or `-oo`

, then all bets are off. In particular
C and SMTLib are decidedly undefine this case, though that doesn't mean they do the
same thing! Same goes for Haskell, which seems to convert via Int64, but we do
not model that behavior in SBV as it doesn't seem to be intentional nor well documented.

You can check for `NaN`

, `oo`

and `-oo`

, using the predicates `fpIsNaN`

, `fpIsInfinite`

,
and `fpIsPositive`

, `fpIsNegative`

predicates, respectively; and do the proper conversion
based on your needs. (0 is a good choice, as are min/max bounds of the target type.)

Currently, SBV provides no predicates to check if a value would lie within range for a particular conversion task, as this depends on the rounding mode and the types involved and can be rather tricky to determine. (See http://github.com/LeventErkok/sbv/issues/456 for a discussion of the issues involved.) In a future release, we hope to be able to provide underflow and overflow predicates for these conversions as well.

Nothing

fromSFloat :: SRoundingMode -> SFloat -> SBV a Source #

Convert from an IEEE74 single precision float.

toSFloat :: SRoundingMode -> SBV a -> SFloat Source #

Convert to an IEEE-754 Single-precision float.

`>>>`

roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}`:{`

`>>>`

Q.E.D.`prove $ roundTrip @Int8`

`>>>`

Q.E.D.`prove $ roundTrip @Word8`

`>>>`

Q.E.D.`prove $ roundTrip @Int16`

`>>>`

Q.E.D.`prove $ roundTrip @Word16`

`>>>`

Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = -2130176960 :: Int32`prove $ roundTrip @Int32`

Note how we get a failure on `Int32`

. The counter-example value is not representable exactly as a single precision float:

`>>>`

(-2130177024) % 1`toRational (-2130176960 :: Float)`

Note how the numerator is different, it is off by 64. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.

toSFloat :: Integral a => SRoundingMode -> SBV a -> SFloat Source #

Convert to an IEEE-754 Single-precision float.

`>>>`

roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSFloat m (toSFloat m x) .== x :}`:{`

`>>>`

Q.E.D.`prove $ roundTrip @Int8`

`>>>`

Q.E.D.`prove $ roundTrip @Word8`

`>>>`

Q.E.D.`prove $ roundTrip @Int16`

`>>>`

Q.E.D.`prove $ roundTrip @Word16`

`>>>`

Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = -2130176960 :: Int32`prove $ roundTrip @Int32`

Note how we get a failure on `Int32`

. The counter-example value is not representable exactly as a single precision float:

`>>>`

(-2130177024) % 1`toRational (-2130176960 :: Float)`

Note how the numerator is different, it is off by 64. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.

fromSDouble :: SRoundingMode -> SDouble -> SBV a Source #

Convert from an IEEE74 double precision float.

toSDouble :: SRoundingMode -> SBV a -> SDouble Source #

Convert to an IEEE-754 Double-precision float.

`>>>`

roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}`:{`

`>>>`

Q.E.D.`prove $ roundTrip @Int8`

`>>>`

Q.E.D.`prove $ roundTrip @Word8`

`>>>`

Q.E.D.`prove $ roundTrip @Int16`

`>>>`

Q.E.D.`prove $ roundTrip @Word16`

`>>>`

Q.E.D.`prove $ roundTrip @Int32`

`>>>`

Q.E.D.`prove $ roundTrip @Word32`

`>>>`

Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 4611686018427387902 :: Int64`prove $ roundTrip @Int64`

Just like in the `SFloat`

case, once we reach 64-bits, we no longer can exactly represent the
integer value for all possible values:

`>>>`

4611686018427387904 % 1`toRational (4611686018427387902 ::Double)`

In this case the numerator is off by 2!

toSDouble :: Integral a => SRoundingMode -> SBV a -> SDouble Source #

Convert to an IEEE-754 Double-precision float.

`>>>`

roundTrip :: forall a. (Eq a, IEEEFloatConvertible a) => SRoundingMode -> SBV a -> SBool roundTrip m x = fromSDouble m (toSDouble m x) .== x :}`:{`

`>>>`

Q.E.D.`prove $ roundTrip @Int8`

`>>>`

Q.E.D.`prove $ roundTrip @Word8`

`>>>`

Q.E.D.`prove $ roundTrip @Int16`

`>>>`

Q.E.D.`prove $ roundTrip @Word16`

`>>>`

Q.E.D.`prove $ roundTrip @Int32`

`>>>`

Q.E.D.`prove $ roundTrip @Word32`

`>>>`

Falsifiable. Counter-example: s0 = RoundNearestTiesToEven :: RoundingMode s1 = 4611686018427387902 :: Int64`prove $ roundTrip @Int64`

Just like in the `SFloat`

case, once we reach 64-bits, we no longer can exactly represent the
integer value for all possible values:

`>>>`

4611686018427387904 % 1`toRational (4611686018427387902 ::Double)`

In this case the numerator is off by 2!

## Instances

## Bit-pattern conversions

sFloatAsSWord32 :: SFloat -> SWord32 Source #

Convert an `SFloat`

to an `SWord32`

, preserving the bit-correspondence. Note that since the
representation for `NaN`

s are not unique, this function will return a symbolic value when given a
concrete `NaN`

.

Implementation note: Since there's no corresponding function in SMTLib for conversion to 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 `NaN`

s are not unique, this function will return a symbolic value when given a
concrete `NaN`

.

See the implementation note for `sFloatAsSWord32`

, as it applies here as well.

sWord64AsSDouble :: SWord64 -> SDouble Source #

Reinterpret the bits in a 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, SymVal, HasKind, SatModel)

(Note that you'll also need to use the language pragmas `DeriveDataTypeable`

, `DeriveAnyClass`

, and import `Data.Generics`

for the above to work.)

This is all it takes to introduce `B`

as an uninterpreted sort in SBV, which makes the type `SBV B`

automagically become available as the type
of symbolic values that ranges over `B`

values. Note that the `()`

argument is important to distinguish it from enumerations, which will be
translated to proper SMT 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.

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.

NB. For a version which generalizes over the underlying monad, see `addAxiom`

# 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: http://en.wikipedia.org/wiki/Prenex_normal_form. That is,
all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately,
the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them
with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers.
SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested
quantification, you will manually have to first convert to prenex-normal form (which produces an equisatisfiable but not necessarily
equivalent formula), and code that explicitly in SBV. See http://github.com/LeventErkok/sbv/issues/256 for a detailed discussion
of this issue.

### Using multiple solvers

On a 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.

forAll_ :: Provable a => a -> Symbolic SBool Source #

Turns a value into a universally quantified predicate, internally naming the inputs.
In this case the sbv library will use names of the form `s1, s2`

, etc. to name these variables
Example:

forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y

is a predicate with two arguments, captured using an ordinary Haskell function. Internally,
`x`

will be named `s0`

and `y`

will be named `s1`

.

NB. For a version which generalizes over the underlying monad, see `forAll_`

forAll :: Provable a => [String] -> a -> Symbolic SBool Source #

Turns a value into a predicate, allowing users to provide names for the inputs. If the user does not provide enough number of names for the variables, the remaining ones will be internally generated. Note that the names are only used for printing models and has no other significance; in particular, we do not check that they are unique. Example:

forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y

This is the same as above, except the variables will be named `x`

and `y`

respectively,
simplifying the counter-examples when they are printed.

NB. For a version which generalizes over the underlying monad, see `forAll`

prove :: Provable a => a -> IO ThmResult Source #

Prove a predicate, using the default solver.

NB. For a version which generalizes over the underlying monad, see `prove`

proveWith :: Provable a => SMTConfig -> a -> IO ThmResult Source #

Prove the predicate using the given SMT-solver.

NB. For a version which generalizes over the underlying monad, see `proveWith`

sat :: Provable a => a -> IO SatResult Source #

Find a satisfying assignment for a predicate, using the default solver.

NB. For a version which generalizes over the underlying monad, see `sat`

satWith :: Provable a => SMTConfig -> a -> IO SatResult Source #

Find a satisfying assignment using the given SMT-solver.

NB. For a version which generalizes over the underlying monad, see `satWith`

allSat :: Provable a => a -> IO AllSatResult Source #

Find all satisfying assignments, using the default solver.
Equivalent to

. See `allSatWith`

`defaultSMTCfg`

`allSatWith`

for details.

NB. For a version which generalizes over the underlying monad, see `allSat`

allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult Source #

Return all satisfying assignments for a predicate.
Note that this call will block until all satisfying assignments are found. If you have a problem
with infinitely many satisfying models (consider `SInteger`

) or a very large number of them, you
might have to wait for a long time. To avoid such cases, use the `allSatMaxModelCount`

parameter in the configuration.

NB. Uninterpreted constant/function values and counter-examples for array values are ignored for
the purposes of `allSat`

. That is, only the satisfying assignments modulo uninterpreted functions and
array inputs will be returned. This is due to the limitation of not having a robust means of getting a
function counter-example back from the SMT solver.
Find all satisfying assignments using the given SMT-solver

NB. For a version which generalizes over the underlying monad, see `allSatWith`

optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult Source #

optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult Source #

Optimizes the objectives using the given SMT-solver.

NB. For a version which generalizes over the underlying monad, see `optimizeWith`

isVacuous :: Provable a => a -> IO Bool Source #

Check if the constraints given are consistent, using the default solver.

NB. For a version which generalizes over the underlying monad, see `isVacuous`

isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool Source #

Determine if the constraints are vacuous using the given SMT-solver.

NB. For a version which generalizes over the underlying monad, see `isVacuousWith`

isTheorem :: Provable a => a -> IO Bool Source #

Checks theoremhood using the default solver.

NB. For a version which generalizes over the underlying monad, see `isTheorem`

isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool Source #

Check whether a given property is a theorem.

NB. For a version which generalizes over the underlying monad, see `isTheoremWith`

isSatisfiable :: Provable a => a -> IO Bool Source #

Checks satisfiability using the default solver.

NB. For a version which generalizes over the underlying monad, see `isSatisfiable`

isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool Source #

Check whether a given property is satisfiable.

NB. For a version which generalizes over the underlying monad, see `isSatisfiableWith`

proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)] Source #

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

proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult) Source #

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

to the losing processes, but we do *not* actually wait for them
to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
that some processes take their time to terminate. So, this solution favors quick turnaround.

satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)] Source #

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

satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult) Source #

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

to the losing processes, but we do *not* actually wait for them
to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
that some processes take their time to terminate. So, this solution favors quick turnaround.

generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String Source #

Create an 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.

solve :: [SBool] -> Symbolic SBool Source #

Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing problems with constraints, like the following:

sat $ do [x, y, z] <- sIntegers ["x", "y", "z"] solve [x .> 5, y + z .< x]

NB. For a version which generalizes over the underlying monad, see `solve`

# Constraints

A constraint is a means for restricting the input domain of a formula. Here's a simple example:

do x <-`exists`

"x" y <-`exists`

"y"`constrain`

$ x .> y`constrain`

$ x + y .>= 12`constrain`

$ 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`

(or`allSat`

) call: The constraint added is asserted conjunctively. That is, the resulting satisfying model (if any) will always satisfy all the constraints given. - In a
`prove`

call: In this case, the constraint acts as an implication. The property is proved under the assumption that the constraint holds. In other words, the constraint says that we only care about the input space that satisfies the constraint. - In a
`quickCheck`

call: The constraint acts as a filter for`quickCheck`

; if the constraint does not hold, then the input value is considered to be irrelevant and is skipped. Note that this is similar to`prove`

, but is stronger: We do not accept a test case to be valid just because the constraints fail on them, although semantically the implication does hold. We simply skip that test case as a*bad*test vector. - In a
`genTest`

call: Similar to`quickCheck`

and`prove`

: 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`

`sFalse`

constrain :: SolverContext m => SBool -> m () Source #

Add a constraint, any satisfying instance must satisfy this condition.

softConstrain :: SolverContext m => SBool -> m () Source #

Add a soft constraint. The solver will try to satisfy this condition if possible, but won't if it cannot.

## Constraint Vacuity

When adding constraints, one has to be careful about
making sure they are not inconsistent. The function `isVacuous`

can be use for this purpose.
Here is an example. Consider the following predicate:

`>>>`

`let pred = do { x <- free "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }`

This predicate asserts that all 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:

`>>>`

Q.E.D.`prove pred`

We can use `isVacuous`

to make sure to see that the pass was vacuous:

`>>>`

True`isVacuous pred`

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:

`>>>`

Q.E.D.`prove pred'`

And the proof is not vacuous:

`>>>`

False`isVacuous pred'`

## Named constraints and attributes

Constraints can be given names:

` ``namedConstraint`

"a is at least 5" $ a .>= 5

Similarly, arbitrary term attributes can also be associated:

` ``constrainWithAttribute`

[(":solver-specific-attribute", "value")] $ a .>= 5

Note that a `namedConstraint`

is equivalent to a `constrainWithAttribute`

call, setting the `":named"' attribute.

namedConstraint :: SolverContext m => String -> SBool -> m () Source #

Add a named constraint. The name is used in unsat-core extraction.

constrainWithAttribute :: SolverContext m => [(String, String)] -> SBool -> m () Source #

Add a constraint, with arbitrary attributes. Used in interpolant generation.

## Unsat cores

Named constraints are useful when used in conjunction with `getUnsatCore`

function
where the backend solver can be queried to obtain an unsat core in case the constraints are unsatisfiable.
See `getUnsatCore`

for details and Documentation.SBV.Examples.Queries.UnsatCore for an example use case.

## Cardinality constraints

A 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 `sTrue`

.
However, the equivalent forms give rise to long formulas and the cardinality constraint
can get lost in the translation. The idea here is that if you use these functions instead, SBV will
produce better translations to SMTLib for more efficient solving of cardinality constraints, assuming
the backend solver supports them. Currently, only Z3 supports 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.

`>>>`

[sub: x >= y must hold!: Violated. Model: s0 = 30 :: Int8 s1 = 32 :: Int8]`safe (sub :: SInt8 -> SInt8 -> SInt8)`

What happens if we make sure to arrange for this invariant? Consider this version:

`>>>`

`let safeSub x y = ite (x .>= y) (sub x y) 0`

Clearly, `safeSub`

must be safe. And indeed, SBV can prove that:

`>>>`

[sub: x >= y must hold!: No violations detected]`safe (safeSub :: SInt8 -> SInt8 -> SInt8)`

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 :: HasKind a => Maybe CallStack -> String -> SBool -> SBV a -> SBV a Source #

Symbolic assert. Check that the given boolean condition is always `sTrue`

in the given path. The
optional first argument can be used to provide 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 ExtractIO m => SExecutable m a Source #

Symbolically executable program fragments. This class is mainly used for `safe`

calls, and is sufficently populated internally to cover most use
cases. Users can extend it as they wish to allow `safe`

checks for SBV programs that return/take types that are user-defined.

## Instances

sName_ :: SExecutable IO a => a -> Symbolic () Source #

NB. For a version which generalizes over the underlying monad, see `sName_`

sName :: SExecutable IO a => [String] -> a -> Symbolic () Source #

NB. For a version which generalizes over the underlying monad, see `sName`

safe :: SExecutable IO a => a -> IO [SafeResult] Source #

Check safety using the default solver.

NB. For a version which generalizes over the underlying monad, see `safe`

safeWith :: SExecutable IO a => SMTConfig -> a -> IO [SafeResult] Source #

# 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 `SReal`

s. That is, it can find models satisfying all the constraints while minimizing
or maximizing user given metrics. Currently, optimization requires the use of the z3 SMT solver as the backend,
and a good review of these features is given
in this paper: http://www.microsoft.com/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*y

minimizes 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:

`>>>`

Optimal in an extension field: goal = -oo :: Integer`optimize Lexicographic $ \x y -> minimize "goal" (x+2*(y::SInteger))`

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."

Pareto fronts only make sense when the objectives are bounded. If there are unbounded objective values, then the
backend solver can loop infinitely. (This is what z3 does currently.) If you are not sure the objectives are
bounded, you should first use `Independent`

mode to ensure the objectives are bounded, and then switch to
pareto-mode to extract them further.

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 really large,
so if `Nothing`

is used, there is a potential for waiting indefinitely 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.

Lexicographic | Objectives are optimized in the order given, earlier objectives have higher priority. |

Independent | Each objective is optimized independently. |

Pareto (Maybe Int) | Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse. |

## Instances

Eq OptimizeStyle Source # | |

Defined in Data.SBV.Core.Symbolic (==) :: OptimizeStyle -> OptimizeStyle -> Bool # (/=) :: OptimizeStyle -> OptimizeStyle -> Bool # | |

Show OptimizeStyle Source # | |

Defined in Data.SBV.Core.Symbolic showsPrec :: Int -> OptimizeStyle -> ShowS # show :: OptimizeStyle -> String # showList :: [OptimizeStyle] -> ShowS # | |

NFData OptimizeStyle Source # | |

Defined in Data.SBV.Core.Symbolic rnf :: OptimizeStyle -> () # |

## Objectives and Metrics

Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty for not satisfying it.

Minimize String a | Minimize this metric |

Maximize String a | Maximize this metric |

AssertWithPenalty String a Penalty | A soft assertion, with an associated penalty |

Class of metrics we can optimize for. Currently, booleans,
bounded signed/unsigned bit-vectors, unbounded integers,
algebraic reals and floats can be optimized. You can add
your instances, but bewared that the `MetricSpace`

should
map your type to something the backend solver understands, which
are limited to unsigned bit-vectors, reals, and unbounded integers
for z3.

A good reference on these features is given in the following paper: http://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf.

Minimal completion: None. However, if `MetricSpace`

is not identical to the type, you want
to define `toMetricSpace`

and possbly 'minimize'/'maximize' to add extra constraints as necessary.

Nothing

type MetricSpace a :: * Source #

The metric space we optimize the goal over. Usually the same as the type itself, but not always!
For instance, signed bit-vectors are optimized over their unsigned counterparts, floats are
optimized over their `Word32`

comparable counterparts, etc.

toMetricSpace :: SBV a -> SBV (MetricSpace a) Source #

Compute the metric value to optimize.

fromMetricSpace :: SBV (MetricSpace a) -> SBV a Source #

Compute the value itself from the metric corresponding to it.

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m () Source #

Minimizing a metric space

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV a -> m () Source #

Maximizing a metric space

toMetricSpace :: a ~ MetricSpace a => SBV a -> SBV (MetricSpace a) Source #

Compute the metric value to optimize.

fromMetricSpace :: a ~ MetricSpace a => SBV (MetricSpace a) -> SBV a Source #

Compute the value itself from the metric corresponding to it.