z3-0.3.1: Bindings for the Z3 Theorem Prover

Index

%%Z3.Lang.Prelude, Z3.Lang
%*Z3.Lang.Prelude, Z3.Lang
&&*Z3.Lang.Prelude, Z3.Lang
+?Z3.Opts, Z3.Monad
//Z3.Lang.Prelude, Z3.Lang
/=*Z3.Lang.Prelude, Z3.Lang
<*Z3.Lang.Prelude, Z3.Lang
<=*Z3.Lang.Prelude, Z3.Lang
<=>Z3.Lang.Prelude, Z3.Lang
==*Z3.Lang.Prelude, Z3.Lang
==>Z3.Lang.Prelude, Z3.Lang
>*Z3.Lang.Prelude, Z3.Lang
>=*Z3.Lang.Prelude, Z3.Lang
and_Z3.Lang.Prelude, Z3.Lang
AppZ3.Base, Z3.Monad
Args 
1 (Type/Class)Z3.Lang.Prelude, Z3.Lang
2 (Data Constructor)Z3.Lang.Prelude, Z3.Lang
assertZ3.Lang.Prelude, Z3.Lang
assertCnstr 
1 (Function)Z3.Base
2 (Function)Z3.Monad
ASTZ3.Base, Z3.Monad
ASTPrintModeZ3.Base, Z3.Monad
astToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
AUFLIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
AUFLIRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
AUFNIRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
benchmarkToSMTLibString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
castZ3.Lang.Prelude, Z3.Lang
CastableZ3.Lang.Prelude, Z3.Lang
check 
1 (Function)Z3.Base
2 (Function)Z3.Monad, Z3.Lang.Prelude, Z3.Lang
checkModelZ3.Lang.Prelude, Z3.Lang
checkModelWithZ3.Lang.Prelude, Z3.Lang
checkModelWithResultZ3.Lang.Prelude, Z3.Lang
ConfigZ3.Base
ContextZ3.Base
contextToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
declareLg2Z3.Lang.Lg2
declarePow2Z3.Lang.Pow2
DecRefErrorZ3.Base
delConfigZ3.Base
delContextZ3.Base
delModel 
1 (Function)Z3.Base
2 (Function)Z3.Monad
distinctZ3.Lang.Prelude, Z3.Lang
dividesZ3.Lang.Prelude, Z3.Lang
errCodeZ3.Base
errMsgZ3.Base
eval 
1 (Function)Z3.Base
2 (Function)Z3.Monad
3 (Function)Z3.Lang.Prelude, Z3.Lang
evalArray 
1 (Function)Z3.Base
2 (Function)Z3.Monad
evalFunc 
1 (Function)Z3.Base
2 (Function)Z3.Monad
evalT 
1 (Function)Z3.Base
2 (Function)Z3.Monad
3 (Function)Z3.Lang.Prelude, Z3.Lang
evalZ3 
1 (Function)Z3.Monad
2 (Function)Z3.Lang.Prelude, Z3.Lang
evalZ3With 
1 (Function)Z3.Monad
2 (Function)Z3.Lang.Prelude, Z3.Lang
existsZ3.Lang.Prelude, Z3.Lang
ExprZ3.Lang.Prelude, Z3.Lang
exprToStringZ3.Lang.Prelude, Z3.Lang
falseZ3.Lang.Prelude, Z3.Lang
FileAccessErrorZ3.Base
forallZ3.Lang.Prelude, Z3.Lang
fun1Z3.Lang.Prelude, Z3.Lang
fun2Z3.Lang.Prelude, Z3.Lang
fun3Z3.Lang.Prelude, Z3.Lang
fun4Z3.Lang.Prelude, Z3.Lang
fun5Z3.Lang.Prelude, Z3.Lang
FuncDeclZ3.Base, Z3.Monad
funcDeclToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
FuncEntryZ3.Base, Z3.Monad
funcEntryGetArg 
1 (Function)Z3.Base
2 (Function)Z3.Monad
funcEntryGetNumArgs 
1 (Function)Z3.Base
2 (Function)Z3.Monad
funcEntryGetValue 
1 (Function)Z3.Base
2 (Function)Z3.Monad
FuncInterpZ3.Base, Z3.Monad
funcInterpGetArity 
1 (Function)Z3.Base
2 (Function)Z3.Monad
funcInterpGetElse 
1 (Function)Z3.Base
2 (Function)Z3.Monad
funcInterpGetEntry 
1 (Function)Z3.Base
2 (Function)Z3.Monad
funcInterpGetNumEntries 
1 (Function)Z3.Base
2 (Function)Z3.Monad
FuncModel 
1 (Type/Class)Z3.Base, Z3.Monad
2 (Data Constructor)Z3.Base, Z3.Monad
getAsArrayFuncDecl 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getBool 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getBvSortSize 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getContextZ3.Monad
getFuncInterp 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getInt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getModel 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getReal 
1 (Function)Z3.Base
2 (Function)Z3.Monad
getSolverZ3.Monad
getSortZ3.Base
iffZ3.Lang.Prelude, Z3.Lang
impliesZ3.Lang.Prelude, Z3.Lang
instanceWhenZ3.Lang.Prelude, Z3.Lang
InternalFatalZ3.Base
interpElseZ3.Base, Z3.Monad
interpMapZ3.Base, Z3.Monad
InvalidArgZ3.Base
InvalidPatternZ3.Base
InvalidUsageZ3.Base
IOBZ3.Base
isAsArray 
1 (Function)Z3.Base
2 (Function)Z3.Monad
IsIntZ3.Lang.Prelude, Z3.Lang
IsNumZ3.Lang.Prelude, Z3.Lang
IsRealZ3.Lang.Prelude, Z3.Lang
IsTyZ3.Lang.Prelude, Z3.Lang
iteZ3.Lang.Prelude, Z3.Lang
let_Z3.Lang.Prelude, Z3.Lang
literalZ3.Lang.Prelude, Z3.Lang
LogicZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
logicZ3.Lang.Prelude, Z3.Lang
LRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
max_Z3.Lang.Prelude, Z3.Lang
MemoutFailZ3.Base
min_Z3.Lang.Prelude, Z3.Lang
mkAdd 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkAnd 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkApp 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkArrayDefault 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkArraySort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBoolSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBound 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBv2int 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvadd 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvaddNoOverflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvaddNoUnderflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvand 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvashr 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvlshr 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvmul 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvmulNoOverflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvmulNoUnderflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvnand 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvneg 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvnegNoOverflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvnor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvnot 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvredand 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvredor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsdiv 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsdivNoOverflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsge 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsgt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvshl 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsle 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvslt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsmod 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsrem 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsub 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsubNoOverflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvsubNoUnderflow 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvudiv 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvuge 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvugt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvule 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvult 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvurem 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvxnor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkBvxor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkConcat 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkConfigZ3.Base
mkConst 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkConstArray 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkContextZ3.Base
mkDistinct 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkDiv 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkEq 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkExists 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkExtract 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkExtRotateLeft 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkExtRotateRight 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkFalse 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkForall 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkFuncDecl 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkGe 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkGt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkIff 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkImplies 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkInt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkInt2bv 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkInt2Real 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkIntSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkIntSymbol 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkIsInt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkIte 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkLe 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkLt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkMap 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkMod 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkMul 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkNot 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkNumeral 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkOr 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkParamsZ3.Base
mkPattern 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkReal 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkReal2Int 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkRealSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkRem 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkRepeat 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkRotateLeft 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkRotateRight 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkSelect 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkSignExt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkSimpleSolverZ3.Base
mkSolverZ3.Base
mkSolverForLogicZ3.Base
mkStore 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkStringSymbol 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkSub 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkTrue 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkTupleSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkUnaryMinus 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkUninterpretedSort 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkXor 
1 (Function)Z3.Base
2 (Function)Z3.Monad
mkZeroExt 
1 (Function)Z3.Base
2 (Function)Z3.Monad
Model 
1 (Type/Class)Z3.Base, Z3.Monad
2 (Type/Class)Z3.Lang.Prelude, Z3.Lang
modelToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
MonadZ3Z3.Monad
namedVarZ3.Lang.Prelude, Z3.Lang
NatZ3.Lang.Nat, Z3.Lang
NoParserZ3.Base
not_Z3.Lang.Prelude, Z3.Lang
optZ3.Opts, Z3.Monad
optionsZ3.Lang.Prelude, Z3.Lang
OptsZ3.Opts, Z3.Monad
OptValueZ3.Opts, Z3.Monad
or_Z3.Lang.Prelude, Z3.Lang
ParamsZ3.Base
paramsSetBoolZ3.Base
paramsSetDoubleZ3.Base
paramsSetSymbolZ3.Base
paramsSetUIntZ3.Base
paramsToStringZ3.Base
ParserErrorZ3.Base
PatZ3.Lang.Prelude, Z3.Lang
Pattern 
1 (Type/Class)Z3.Base, Z3.Monad
2 (Type/Class)Z3.Lang.Prelude, Z3.Lang
patternToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
pop 
1 (Function)Z3.Base
2 (Function)Z3.Monad, Z3.Lang.Prelude, Z3.Lang
push 
1 (Function)Z3.Base
2 (Function)Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_ABVZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_AUFBVZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_AUFLIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_AXZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_BVZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_IDLZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_LIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_LRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_NIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_NRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_RDLZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFBVZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFIDLZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFLIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFLRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
QF_UFNRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
ResultZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
SatZ3.Base, Z3.Monad
setASTPrintMode 
1 (Function)Z3.Base
2 (Function)Z3.Monad
setOptsZ3.Opts, Z3.Monad
setParamValueZ3.Base
showContext 
1 (Function)Z3.Base
2 (Function)Z3.Monad, Z3.Lang.Prelude, Z3.Lang
showModel 
1 (Function)Z3.Base
2 (Function)Z3.Monad
3 (Function)Z3.Lang.Prelude, Z3.Lang
softTimeoutZ3.Lang.Prelude, Z3.Lang
SolverZ3.Base
solverAssertAndTrackZ3.Base
solverAssertCnstrZ3.Base
solverCheckZ3.Base
solverCheckAndGetModelZ3.Base
solverGetReasonUnknownZ3.Base
solverPopZ3.Base
solverPushZ3.Base
solverResetZ3.Base
solverSetParamsZ3.Base
SortZ3.Base, Z3.Monad
SortErrorZ3.Base
sortToString 
1 (Function)Z3.Base
2 (Function)Z3.Monad
stdArgsZ3.Lang.Prelude, Z3.Lang
stdOptsZ3.Opts, Z3.Monad
SymbolZ3.Base, Z3.Monad
trueZ3.Lang.Prelude, Z3.Lang
UFLRAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
UFNIAZ3.Base, Z3.Monad, Z3.Lang.Prelude, Z3.Lang
UndefZ3.Base, Z3.Monad
UnsatZ3.Base, Z3.Monad
varZ3.Lang.Prelude, Z3.Lang
withConfigZ3.Base
withContextZ3.Base
withModelZ3.Monad
xorZ3.Lang.Prelude, Z3.Lang
Z3 
1 (Type/Class)Z3.Lang.Prelude, Z3.Lang
2 (Type/Class)Z3.Monad
Z3Error 
1 (Type/Class)Z3.Base
2 (Data Constructor)Z3.Base
Z3ErrorCodeZ3.Base
Z3ExceptionZ3.Base
Z3_PRINT_LOW_LEVELZ3.Base, Z3.Monad
Z3_PRINT_SMTLIB2_COMPLIANTZ3.Base, Z3.Monad
Z3_PRINT_SMTLIB_COMPLIANTZ3.Base, Z3.Monad
Z3_PRINT_SMTLIB_FULLZ3.Base, Z3.Monad
||*Z3.Lang.Prelude, Z3.Lang