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