smtLib-1.1: A library for working with the SMTLIB format.

Index

.<. | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
.>. | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
=/= |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Core
=== |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Core
==> | SMTLib2.Core
And | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
and | SMTLib2.Core
Annot |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
annot | SMTLib2.Compat1
App |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
app | SMTLib2
assume | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Attr |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
3 (Data Constructor) | SMTLib2
attrName |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2
AttrVal | SMTLib2
attrVal |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2
Bind |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
Binder |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
binder | SMTLib2.Compat1
bindSort | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
bindType | SMTLib2
bindVar |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2
bit0 | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
bit1 | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
bv |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvadd |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvand |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvashr |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvcomp |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvlshr |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvmul |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvnand |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvneg |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvnor |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvnot |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvor |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsdiv |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsge |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsgt |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvshl |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsle |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvslt |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsmod |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsrem |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvsub |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvudiv |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvuge |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvugt |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvule |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvult | SMTLib2.BitVector
bvurem |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvxnor |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
bvxor |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
CmdAnnot | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdAssert | SMTLib2
CmdAssumption | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdCheckSat | SMTLib2
CmdComment | SMTLib2
CmdDeclareConst | SMTLib2
CmdDeclareFun | SMTLib2
CmdDeclareType | SMTLib2
CmdDefineFun | SMTLib2
CmdDefineType | SMTLib2
CmdExit | SMTLib2
CmdExtraFuns | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdExtraPreds | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdExtraSorts | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdFormula | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdGetAssertions | SMTLib2
CmdGetInfo | SMTLib2
CmdGetOption | SMTLib2
CmdGetProof | SMTLib2
CmdGetUnsatCore | SMTLib2
CmdGetValue | SMTLib2
CmdLogic | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdNotes | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
CmdPop | SMTLib2
CmdPush | SMTLib2
CmdSetInfo | SMTLib2
CmdSetLogic | SMTLib2
CmdSetOption | SMTLib2
CmdStatus | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Command |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
command | SMTLib2.Compat1
concat |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
Conn |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
constDef | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
defExpr | SMTLib2
Defn |
1 (Type/Class) | SMTLib2
2 (Data Constructor) | SMTLib2
defVar | SMTLib2
err | SMTLib2.Compat1
Exists |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
Expr | SMTLib2
extract |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
Fail | SMTLib2.Compat1
false | SMTLib2.Core
FAnnot | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
FFalse | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
FLet | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Forall |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
Formula | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
formula | SMTLib2.Compat1
FPred | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
FTrue | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
funAnnots | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
funArgs | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
FunDecl |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
funDef | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
funName | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
funRes | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
FVar | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
goal | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
I |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
Ident |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
ident | SMTLib2.Compat1
Iff | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
IfThenElse | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Implies | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
InfoAllStatistics | SMTLib2
InfoAttr | SMTLib2
InfoAuthors | SMTLib2
InfoErrorBehavior | SMTLib2
InfoFlag | SMTLib2
InfoName | SMTLib2
InfoReasonUnknown | SMTLib2
InfoStatus | SMTLib2
InfoVersion | SMTLib2
isBitVec | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
ITE | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
ite | SMTLib2.Core
Let |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
Lit |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
LitBV | SMTLib2
Literal |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
literal | SMTLib2.Compat1
LitFrac |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
LitNum |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
LitStr |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
logic | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
N |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib2
nAbs | SMTLib2.Int
nAdd | SMTLib2.Int
Name |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
name | SMTLib2.Compat1
nDiv | SMTLib2.Int
nGeq | SMTLib2.Int
nGt | SMTLib2.Int
nLeq | SMTLib2.Int
nLt | SMTLib2.Int
nMod | SMTLib2.Int
nMul | SMTLib2.Int
nNeg | SMTLib2.Int
Not | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
not | SMTLib2.Core
nSub | SMTLib2.Int
num | SMTLib2.Int
OK | SMTLib2.Compat1
OptAttr | SMTLib2
OptDiagnosticOutputChannel | SMTLib2
OptExpandDefinitions | SMTLib2
OptInteractiveMode | SMTLib2
Option | SMTLib2
OptPrintSuccess | SMTLib2
OptProduceAssignments | SMTLib2
OptProduceModels | SMTLib2
OptProduceProofs | SMTLib2
OptProduceUnsatCores | SMTLib2
OptRandomSeed | SMTLib2
OptRegularOutputChannel | SMTLib2
OptVerbosity | SMTLib2
Or | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
or | SMTLib2.Core
PP |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib2
pp |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2
predAnnots | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
predArgs | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
PredDecl |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
predName | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Quant |
1 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
3 (Data Constructor) | SMTLib2
4 (Type/Class) | SMTLib2
quant | SMTLib2.Compat1
repeat |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
rotate_left |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
rotate_right |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
Sat | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
scrCommands | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Script |
1 (Type/Class) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Data Constructor) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
3 (Type/Class) | SMTLib2
4 (Data Constructor) | SMTLib2
script | SMTLib2.Compat1
scrName | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
select |
1 (Function) | SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Array
sign_extend |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
Sort | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
sort | SMTLib2.Compat1
Status | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
store |
1 (Function) | SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Array
TAnnot | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
TApp | SMTLib2
tArray |
1 (Function) | SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Array
tBitVec |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector
tBool | SMTLib2.Core
Term | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
term | SMTLib2.Compat1
tInt |
1 (Function) | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.Int
toEither | SMTLib2.Compat1
toMaybe | SMTLib2.Compat1
Trans | SMTLib2.Compat1
true | SMTLib2.Core
TVar | SMTLib2
Type | SMTLib2
Unknown | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Unsat | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Var | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
Xor | SMTLib1, SMTLib1.QF_BV, SMTLib1.QF_AUFBV
xor | SMTLib2.Core
zero_extend |
1 (Function) | SMTLib1.QF_BV, SMTLib1.QF_AUFBV
2 (Function) | SMTLib2.BitVector