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

sIntegerToSReal

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