Data.SBV.Internals

Running symbolic programs manually

data Result

data SBVRunMode

data IStage

Solver capabilities

data SolverCapabilities

Internal structures useful for low-level programming

type SBool

type SWord8

type SWord16

type SWord32

type SWord64

type SInt8

type SInt16

type SInt32

type SInt64

type SInteger

type SReal

type SFloat

type SDouble

nan

infinity

sNaN

sInfinity

data RoundingMode

type SRoundingMode

sRoundNearestTiesToEven

sRoundNearestTiesToAway

sRoundTowardPositive

sRoundTowardNegative

sRoundTowardZero

sRNE

sRNA

sRTP

sRTN

sRTZ

class SymWord a

data CW

data CWVal

data AlgReal

data ExtCW

data GeneralizedCW

isRegularCW

cwSameType

cwToBool

mkConstCW

liftCW2

mapCW

mapCW2

data SW

trueSW

falseSW

trueCW

falseCW

normCW

data SVal

data SBV a

data NodeId

mkSymSBV

data ArrayContext

type ArrayInfo

class SymArray array

data SFunArray a b

mkSFunArray

data SArray a b

sbvToSW

sbvToSymSW

forceSWArg

data SBVExpr

newExpr

cache

data Cached a

uncache

uncacheAI

class HasKind a

data Op

data PBOp

data FPOp

type NamedSymVar

getTableIndex

data SBVPgm

data Symbolic a

runSymbolic

data State

getPathCondition

extendPathCondition

inSMTMode

data SBVRunMode

data Kind

class Outputtable a

data Result

class SolverContext m

internalVariable

internalConstraint

isCodeGenMode

data SBVType

newUninterpreted

addAxiom

data Quantifier

needsExistentials

data SMTLibPgm

data SMTLibVersion

smtLibVersionExtension

smtLibReservedNames

data SolverCapabilities

extractSymbolicSimulationState

data SMTScript

data Solver

data SMTSolver

data SMTResult

data SMTModel

data SMTConfig

declNewSArray

declNewSFunArray

data OptimizeStyle

data Penalty

data Objective a

data QueryState

data Query a

data SMTProblem

Operations useful for instantiating SBV type classes

genLiteral

genFromCW

data CW

genMkSymVar

checkAndConvert

genParse

showModel

data SMTModel

liftQRem

liftDMod

Compilation to C, extras

compileToC'

compileToCLib'

Code generation primitives

The codegen monad

data SBVCodeGen a

Specifying inputs, SBV variants

cgInput

cgInputArr

cgOutput

cgOutputArr

cgReturn

cgReturnArr

Specifying inputs, SVal variants

svCgInput

svCgInputArr

svCgOutput

svCgOutputArr

svCgReturn

svCgReturnArr

Settings

cgPerformRTCs

cgSetDriverValues

cgAddPrototype

cgAddDecl

cgAddLDFlags

cgIgnoreSAssert

cgIntegerSize

cgSRealType

data CgSRealType

Infrastructure

class CgTarget a

data CgConfig

data CgState

data CgPgmBundle

data CgPgmKind

data CgVal

defaultCgConfig

initCgState

isCgDriver

isCgMakefile

Generating collateral

cgGenerateDriver

cgGenerateMakefile

codeGen

renderCgPgmBundle

Various math utilities around floats

fpRound0

fpRatio0

fpMaxH

fpMinH

fp2fp

fpRemH

fpRoundToIntegralH

fpIsEqualObjectH

fpIsNormalizedH

Pretty number printing

class PrettyNum a

readBin

shex

shexI

sbin

sbinI

showCFloat

showCDouble

showHFloat

showHDouble

showSMTFloat

showSMTDouble

smtRoundingMode

cwToSMTLib

mkSkolemZero

Timing computations

data Timing

showTDiff

Coordinating with the solver

sendStringToSolver

sendRequestToSolver

retrieveResponseFromSolver