Data.SBV.Internals

Running symbolic programs manually

data Result

data SBVRunMode

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

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 FPOp

type NamedSymVar

getTableIndex

data SBVPgm

data Symbolic a

class SExecutable a

runSymbolic

runSymbolic'

data State

getPathCondition

extendPathCondition

inProofMode

data SBVRunMode

data Kind

class Outputtable a

data Result

data Logic

data SMTLibLogic

addConstraint

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

getSBranchRunConfig

declNewSArray

declNewSFunArray

Operations useful for instantiating SBV type classes

genLiteral

genFromCW

genMkSymVar

checkAndConvert

genParse

showModel

data SMTModel

liftQRem

liftDMod

Polynomial operations that operate on bit-vectors

ites

mdp

addPoly

Compilation to C

compileToC'

compileToCLib'

Code generation primitives

class CgTarget a

data CgConfig

defaultCgConfig

data CgVal

data CgState

initCgState

data SBVCodeGen a

liftSymbolic

cgSBVToSW

cgPerformRTCs

cgIntegerSize

data CgSRealType

cgSRealType

cgGenerateDriver

cgGenerateMakefile

cgSetDriverValues

cgIgnoreSAssert

cgAddPrototype

cgAddDecl

cgAddLDFlags

svCgInput

svCgInputArr

svCgOutput

svCgOutputArr

svCgReturn

svCgReturnArr

cgInput

cgInputArr

cgOutput

cgOutputArr

cgReturn

cgReturnArr

data CgPgmBundle

data CgPgmKind

isCgDriver

isCgMakefile

codeGen

renderCgPgmBundle

render'

Various math utilities around floats

fpRound0

fpRatio0

fpMaxH

fpMinH

fp2fp

fpRemH

fpRoundToIntegralH

fpIsEqualObjectH

fpIsNormalizedH