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

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

### Numeric conversions

svFromIntegral

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