Data.SBV.Internals

Running symbolic programs manually

data Result

data SBVRunMode

runSymbolic

runSymbolic'

Other internal structures useful for low-level programming

data SBV a

slet

data CW

data Kind

data CWVal

data AlgReal

data Quantifier

mkConstCW

genVar

genVar_

liftQRem

liftDMod

symbolicMergeWithKind

cache

sbvToSW

newExpr

normCW

data SBVExpr

data Op

mkSymSBVWithRandom

Operations useful for instantiating SBV type classes

genLiteral

genFromCW

genMkSymVar

checkAndConvert

genParse

Compilation to C

compileToC'

compileToCLib'

data CgPgmBundle

data CgPgmKind