simple-smt-0.8: A simple way to interact with an SMT solver process.

Index

absSimpleSMT
ackCommandSimpleSMT
addSimpleSMT
addManySimpleSMT
andSimpleSMT
andManySimpleSMT
assertSimpleSMT
AtomSimpleSMT
BitsSimpleSMT
BoolSimpleSMT
boolSimpleSMT
bvAddSimpleSMT
bvAndSimpleSMT
bvAShrSimpleSMT
bvBinSimpleSMT
bvHexSimpleSMT
bvLShrSimpleSMT
bvMulSimpleSMT
bvNegSimpleSMT
bvNotSimpleSMT
bvOrSimpleSMT
bvSDivSimpleSMT
bvShlSimpleSMT
bvSLeqSimpleSMT
bvSLtSimpleSMT
bvSRemSimpleSMT
bvSubSimpleSMT
bvUDivSimpleSMT
bvULeqSimpleSMT
bvULtSimpleSMT
bvURemSimpleSMT
bvXOrSimpleSMT
checkSimpleSMT
commandSimpleSMT
concatSimpleSMT
constSimpleSMT
declareSimpleSMT
declareDatatypeSimpleSMT
declareFunSimpleSMT
defineSimpleSMT
defineFunSimpleSMT
distinctSimpleSMT
divSimpleSMT
divisibleSimpleSMT
eqSimpleSMT
extractSimpleSMT
famSimpleSMT
funSimpleSMT
geqSimpleSMT
getConstSimpleSMT
getConstsSimpleSMT
getExprSimpleSMT
getExprsSimpleSMT
gtSimpleSMT
impliesSimpleSMT
inNewScopeSimpleSMT
IntSimpleSMT
intSimpleSMT
iteSimpleSMT
leqSimpleSMT
ListSimpleSMT
loadFileSimpleSMT
Logger 
1 (Type/Class)SimpleSMT
2 (Data Constructor)SimpleSMT
logIndentedSimpleSMT
logLevelSimpleSMT
logMessageSimpleSMT
logMessageAtSimpleSMT
logSetLevelSimpleSMT
logTabSimpleSMT
logUntabSimpleSMT
ltSimpleSMT
modSimpleSMT
mulSimpleSMT
negSimpleSMT
newLoggerSimpleSMT
newSolverSimpleSMT
notSimpleSMT
orSimpleSMT
orManySimpleSMT
OtherSimpleSMT
popSimpleSMT
popManySimpleSMT
pushSimpleSMT
pushManySimpleSMT
readSExprSimpleSMT
RealSimpleSMT
realSimpleSMT
realDivSimpleSMT
ResultSimpleSMT
SatSimpleSMT
selectSimpleSMT
setLogicSimpleSMT
setLogicMaybeSimpleSMT
setOptionSimpleSMT
setOptionMaybeSimpleSMT
SExprSimpleSMT
showsSExprSimpleSMT
signExtendSimpleSMT
simpleCommandSimpleSMT
simpleCommandMaybeSimpleSMT
Solver 
1 (Type/Class)SimpleSMT
2 (Data Constructor)SimpleSMT
stopSimpleSMT
storeSimpleSMT
subSimpleSMT
tArraySimpleSMT
tBitsSimpleSMT
tBoolSimpleSMT
tIntSimpleSMT
tRealSimpleSMT
UnknownSimpleSMT
UnsatSimpleSMT
ValueSimpleSMT
valueSimpleSMT
withLogLevelSimpleSMT
xorSimpleSMT
zeroExtendSimpleSMT