Data.SBV.Dynamic

Programming with symbolic values

Symbolic types

Abstract symbolic value type

data SVal

class HasKind a

data Kind

data CW

data CWVal

cwToBool

Arrays of symbolic values

data SArr

readSArr

resetSArr

writeSArr

mergeSArr

newSArr

eqSArr

Creating a symbolic variable

data Symbolic a

data Quantifier

svMkSymVar

Operations on symbolic values

Boolean literals

svTrue

svFalse

svBool

svAsBool

Integer literals

svInteger

svAsInteger

Float literals

svFloat

svDouble

Algrebraic reals (only from rationals)

svReal

svNumerator

svDenominator

Symbolic equality

svEqual

svNotEqual

Constructing concrete lists

svEnumFromThenTo

Symbolic ordering

svLessThan

svGreaterThan

svLessEq

svGreaterEq

Arithmetic operations

svPlus

svTimes

svMinus

svUNeg

svAbs

svDivide

svQuot

svRem

svExp

svAddConstant

svIncrement

svDecrement

Logical operations

svAnd

svOr

svXOr

svNot

svShl

svShr

svRol

svRor

Splitting, joining, and extending

svExtract

svJoin

Sign-casting

svSign

svUnsign

Indexed lookups

svSelect

Word-level operations

svToWord1

svFromWord1

svTestBit

svSetBit

svShiftLeft

svShiftRight

svRotateLeft

svRotateRight

svWordFromBE

svWordFromLE

svBlastLE

svBlastBE

Conditionals: Mergeable values

svIte

svLazyIte

svSymbolicMerge

svIsSatisfiableInCurrentPath

Uninterpreted sorts, constants, and functions

svUninterpreted

Properties, proofs, and satisfiability

Proving properties

proveWith

Checking satisfiability

satWith

allSatWith

Checking safety

safeWith

Proving properties using multiple solvers

proveWithAll

proveWithAny

satWithAll

satWithAny

Quick-check

svQuickCheck

Model extraction

Inspecting proof results

data ThmResult

data SatResult

data SafeResult

data AllSatResult

data SMTResult

Programmable model extraction

genParse

getModel

getModelDictionary

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

outputSVal

Getting SMT-Lib output (for offline analysis)

compileToSMTLib

generateSMTBenchmarks

Code generation from symbolic programs

data SBVCodeGen a

Setting code-generation options

cgPerformRTCs

cgSetDriverValues

cgGenerateDriver

cgGenerateMakefile

Designating inputs

svCgInput

svCgInputArr

Designating outputs

svCgOutput

svCgOutputArr

Designating return values

svCgReturn

svCgReturnArr

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