Data.SBV

Programming with symbolic values

Symbolic types

Symbolic bit

type SBool

Unsigned symbolic bit-vectors

type SWord8

type SWord16

type SWord32

type SWord64

Signed symbolic bit-vectors

type SInt8

type SInt16

type SInt32

type SInt64

Signed unbounded integers

type SInteger

IEEE-floating point numbers

type SFloat

type SDouble

class IEEEFloating a

class IEEEFloatConvertable a

data RoundingMode

type SRoundingMode

nan

infinity

sNaN

sInfinity

Rounding modes

sRoundNearestTiesToEven

sRoundNearestTiesToAway

sRoundTowardPositive

sRoundTowardNegative

sRoundTowardZero

sRNE

sRNA

sRTP

sRTN

sRTZ

Bit-pattern conversions

sFloatAsSWord32

sWord32AsSFloat

sDoubleAsSWord64

sWord64AsSDouble

blastSFloat

blastSDouble

Signed algebraic reals

type SReal

data AlgReal

sRealToSInteger

Creating a symbolic variable

sBool

sWord8

sWord16

sWord32

sWord64

sInt8

sInt16

sInt32

sInt64

sInteger

sReal

sFloat

sDouble

Creating a list of symbolic variables

sBools

sWord8s

sWord16s

sWord32s

sWord64s

sInt8s

sInt16s

sInt32s

sInt64s

sIntegers

sReals

sFloats

sDoubles

Abstract SBV type

data SBV a

Arrays of symbolic values

class SymArray array

data SArray a b

data SFunArray a b

mkSFunArray

Full binary trees

type STree i e

readSTree

writeSTree

mkSTree

Operations on symbolic values

Word level

sTestBit

sExtractBits

sPopCount

sShiftLeft

sShiftRight

sRotateLeft

sRotateRight

sSignedShiftArithRight

sFromIntegral

setBitTo

oneIf

lsb

msb

label

Predicates

allEqual

allDifferent

inRange

sElem

Addition and Multiplication with high-bits

fullAdder

fullMultiplier

Exponentiation

(.^)

Blasting/Unblasting

blastBE

blastLE

class FromBits a

Splitting, joining, and extending

class Splittable a b

Polynomial arithmetic and CRCs

class Polynomial a

crcBV

crc

Conditionals: Mergeable values

class Mergeable a

ite

iteLazy

Symbolic equality

class EqSymbolic a

Symbolic ordering

class OrdSymbolic a

Symbolic integral numbers

class SIntegral a

Division

class SDivisible a

The Boolean class

class Boolean b

Generalizations of boolean operations

bAnd

bOr

bAny

bAll

Pretty-printing and reading numbers in Hex & Binary

class PrettyNum a

readBin

Checking satisfiability in path conditions

isSatisfiableInCurrentPath

Uninterpreted sorts, constants, and functions

class Uninterpreted a

addAxiom

Enumerations

Properties, proofs, satisfiability, and safety

Predicates

type Predicate

class Provable a

class Equality a

Proving properties

prove

proveWith

isTheorem

isTheoremWith

Checking satisfiability

sat

satWith

isSatisfiable

isSatisfiableWith

Checking safety

sAssert

safe

safeWith

isSafe

class SExecutable a

Finding all satisfying assignments

allSat

allSatWith

Satisfying a sequence of boolean conditions

solve

Adding constraints

constrain

pConstrain

Checking constraint vacuity

isVacuous

isVacuousWith

Quick-checking

sbvQuickCheck

Proving properties using multiple solvers

proveWithAll

proveWithAny

satWithAll

satWithAny

Optimization

minimize

maximize

optimize

minimizeWith

maximizeWith

optimizeWith

Computing expected values

expectedValue

expectedValueWith

Model extraction

Inspecting proof results

data ThmResult

data SatResult

data SafeResult

data AllSatResult

data SMTResult

Programmable model extraction

class SatModel a

class Modelable a

displayModels

extractModels

getModelDictionaries

getModelValues

getModelUninterpretedValues

SMT Interface: Configurations and solvers

data SMTConfig

data SMTLibVersion

data SMTLibLogic

data Logic

data OptimizeOpts

data Solver

data SMTSolver

boolector

cvc4

yices

z3

mathSAT

abc

defaultSolverConfig

sbvCurrentSolver

defaultSMTCfg

sbvCheckSolverInstallation

sbvAvailableSolvers

Symbolic computations

data Symbolic a

output

class SymWord a

Getting SMT-Lib output (for offline analysis)

compileToSMTLib

generateSMTBenchmarks

Test case generation

genTest

getTestValues

data TestVectors

data TestStyle

renderTest

data CW

class HasKind a

data Kind

cwToBool

Code generation from symbolic programs

data SBVCodeGen a

Setting code-generation options

cgPerformRTCs

cgSetDriverValues

cgGenerateDriver

cgGenerateMakefile

Designating inputs

cgInput

cgInputArr

Designating outputs

cgOutput

cgOutputArr

Designating return values

cgReturn

cgReturnArr

Code generation with uninterpreted functions

cgAddPrototype

cgAddDecl

cgAddLDFlags

cgIgnoreSAssert

Code generation with SInteger and SReal types

cgIntegerSize

cgSRealType

data CgSRealType

Compilation to C

compileToC

compileToCLib

Module exports