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 RoundingFloat a

data RoundingMode

type SRoundingMode

nan

infinity

sNaN

sInfinity

fusedMA

Rounding modes

sRoundNearestTiesToEven

sRoundNearestTiesToAway

sRoundTowardPositive

sRoundTowardNegative

sRoundTowardZero

FP classifiers

isNormalFP

isSubnormalFP

isZeroFP

isInfiniteFP

isNaNFP

isNegativeFP

isPositiveFP

isNegativeZeroFP

isPositiveZeroFP

isPointFP

Conversion to and from Word32, Word64

sWord32ToSFloat

sWord64ToSDouble

sFloatToSWord32

sDoubleToSWord64

Blasting floats to sign, exponent, mantissa bits

blastSFloat

blastSDouble

Signed algebraic reals

type SReal

data AlgReal

sIntegerToSReal

fpToSReal

sRealToSFloat

sRealToSDouble

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

sbvTestBit

sbvPopCount

sbvShiftLeft

sbvShiftRight

sbvRotateLeft

sbvRotateRight

sbvSignedShiftArithRight

setBitTo

oneIf

lsb

msb

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

Sign-casting

class SignCast a b

Polynomial arithmetic and CRCs

class Polynomial a

crcBV

crc

Conditionals: Mergeable values

class Mergeable a

ite

iteLazy

sBranch

Conditional symbolic simulation

sAssert

sAssertCont

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

Uninterpreted sorts, constants, and functions

class Uninterpreted a

addAxiom

Enumerations

Properties, proofs, and satisfiability

Predicates

type Predicate

class Provable a

class Equality a

Proving properties

prove

proveWith

isTheorem

isTheoremWith

Checking satisfiability

sat

satWith

isSatisfiable

isSatisfiableWith

Finding all satisfying assignments

allSat

allSatWith

Satisfying a sequence of boolean conditions

solve

Adding constraints

constrain

pConstrain

Checking constraint vacuity

isVacuous

isVacuousWith

Checking safety

safe

safeWith

class SExecutable a

Proving properties using multiple solvers

proveWithAll

proveWithAny

satWithAll

satWithAny

allSatWithAll

allSatWithAny

Optimization

minimize

maximize

optimize

minimizeWith

maximizeWith

optimizeWith

Computing expected values

expectedValue

expectedValueWith

Model extraction

Inspecting proof results

data ThmResult

data SatResult

data AllSatResult

data SMTResult

data SafeResult

Programmable model extraction

class SatModel a

class Modelable a

displayModels

extractModels

getModelDictionaries

getModelValues

getModelUninterpretedValues

SMT Interface: Configurations and solvers

data SMTConfig

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

Code generation with SInteger and SReal types

cgIntegerSize

cgSRealType

data CgSRealType

Compilation to C

compileToC

compileToCLib

Module exports