Data.SBV.Internals

Running symbolic programs manually

data Result

data SBVRunMode

data Symbolic a

runSymbolic

runSymbolic'

Other internal structures useful for low-level programming

data SBV a

slet

data CW

data Kind

class HasKind a

data CWVal

data AlgReal

data Quantifier

mkConstCW

genVar

genVar_

liftQRem

liftDMod

symbolicMergeWithKind

cache

sbvToSW

newExpr

normCW

data SBVExpr

data Op

data SBVType

newUninterpreted

forceSWArg

Operations useful for instantiating SBV type classes

genLiteral

genFromCW

genMkSymVar

checkAndConvert

genParse

showModel

data SMTModel

smtLibReservedNames

Polynomial operations that operate on bit-vectors

ites

mdp

addPoly

Compilation to C

compileToC'

compileToCLib'

data CgPgmBundle

data CgPgmKind

Various math utilities around floats

fpRound0

fpRatio0

fpMaxH

fpMinH

fp2fp

fpRemH

fpRoundToIntegralH

fpIsEqualObjectH

fpIsNormalizedH