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

Floating point numbers

type SFloat

type SDouble

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

class HasKind a

data Kind

Arrays of symbolic values

class SymArray array

data SArray a b

data SFunArray a b

mkSFunArray

Operations on symbolic values

Word level

sTestBit

sExtractBits

sPopCount

sShiftLeft

sShiftRight

sRotateLeft

sRotateRight

sSignedShiftArithRight

sFromIntegral

setBitTo

oneIf

lsb

msb

label

Addition and Multiplication with high-bits

fullAdder

fullMultiplier

Exponentiation

(.^)

Blasting/Unblasting

blastBE

blastLE

class FromBits a

Splitting, joining, and extending

class Splittable a b

Conditionals: Mergeable values

class Mergeable a

ite

iteLazy

Symbolic integral numbers

class SIntegral a

Division

class SDivisible a

The Boolean class

class Boolean b

Generalizations of boolean operations

bAnd

bOr

bAny

bAll

Uninterpreted sorts, constants, and functions

class Uninterpreted a

addAxiom

Symbolic Equality and Comparisons

class EqSymbolic a

class OrdSymbolic a

class Equality a

Constraints

constrain

namedConstraint

Cardinality constraints

pbAtMost

pbAtLeast

pbExactly

pbLe

pbGe

pbEq

pbMutexed

pbStronglyMutexed

Enumerations

mkSymbolicEnumeration

Properties, proofs, satisfiability, and safety

type Predicate

type Goal

class Provable a

Checking safety

sAssert

isSafe

class SExecutable a

Satisfying a sequence of boolean conditions

solve

Quick-checking

sbvQuickCheck

Running a symbolic computation

runSMT

runSMTWith

Optimization

data OptimizeStyle

data Penalty

data Objective a

minimize

maximize

assertSoft

data ExtCW

data GeneralizedCW

Model extraction

Inspecting proof results

data ThmResult

data SatResult

data AllSatResult

data SafeResult

data OptimizeResult

data SMTResult

IEEE-floating point numbers

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

Programmable model extraction

class SatModel a

class Modelable a

displayModels

extractModels

getModelDictionaries

getModelValues

getModelUninterpretedValues

SMT Interface: Configurations and solvers

data SMTConfig

data Timing

data SMTLibVersion

data Solver

data SMTSolver

boolector

cvc4

yices

z3

mathSAT

abc

defaultSolverConfig

defaultSMTCfg

sbvCheckSolverInstallation

sbvAvailableSolvers

setLogic

setOption

setInfo

setTimeOut

Symbolic computations

data Symbolic a

output

class SymWord a

Module exports