|
BoolExpr | MkInterpolant (BoolExpr a) |
|
BoolExpr [] | GetInterpolant (Expr pf, Expr pat, Params p) |
|
ComputeInterpolantResult | ComputeInterpolant (Expr pat, Params p) |
|
String | InterpolationProfile () |
|
CheckInterpolantResult | CheckInterpolant (Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory) |
|
ReadInterpolationProblemResult | ReadInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) |
|
void | WriteInterpolationProblem (String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory) |
|
| Context () |
|
| Context (Map< String, String > settings) |
|
IntSymbol | mkSymbol (int i) |
|
StringSymbol | mkSymbol (String name) |
|
BoolSort | getBoolSort () |
|
IntSort | getIntSort () |
|
RealSort | getRealSort () |
|
BoolSort | mkBoolSort () |
|
SeqSort | getStringSort () |
|
UninterpretedSort | mkUninterpretedSort (Symbol s) |
|
UninterpretedSort | mkUninterpretedSort (String str) |
|
IntSort | mkIntSort () |
|
RealSort | mkRealSort () |
|
BitVecSort | mkBitVecSort (int size) |
|
ArraySort | mkArraySort (Sort domain, Sort range) |
|
SeqSort | mkStringSort () |
|
SeqSort | mkSeqSort (Sort s) |
|
ReSort | mkReSort (Sort s) |
|
TupleSort | mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) |
|
EnumSort | mkEnumSort (Symbol name, Symbol... enumNames) |
|
EnumSort | mkEnumSort (String name, String... enumNames) |
|
ListSort | mkListSort (Symbol name, Sort elemSort) |
|
ListSort | mkListSort (String name, Sort elemSort) |
|
FiniteDomainSort | mkFiniteDomainSort (Symbol name, long size) |
|
FiniteDomainSort | mkFiniteDomainSort (String name, long size) |
|
Constructor | mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) |
|
Constructor | mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) |
|
DatatypeSort | mkDatatypeSort (Symbol name, Constructor[] constructors) |
|
DatatypeSort | mkDatatypeSort (String name, Constructor[] constructors) |
|
DatatypeSort [] | mkDatatypeSorts (Symbol[] names, Constructor[][] c) |
|
DatatypeSort [] | mkDatatypeSorts (String[] names, Constructor[][] c) |
|
Expr | MkUpdateField (FuncDecl field, Expr t, Expr v) throws Z3Exception |
|
FuncDecl | mkFuncDecl (Symbol name, Sort[] domain, Sort range) |
|
FuncDecl | mkFuncDecl (Symbol name, Sort domain, Sort range) |
|
FuncDecl | mkFuncDecl (String name, Sort[] domain, Sort range) |
|
FuncDecl | mkFuncDecl (String name, Sort domain, Sort range) |
|
FuncDecl | mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) |
|
FuncDecl | mkConstDecl (Symbol name, Sort range) |
|
FuncDecl | mkConstDecl (String name, Sort range) |
|
FuncDecl | mkFreshConstDecl (String prefix, Sort range) |
|
Expr | mkBound (int index, Sort ty) |
|
Pattern | mkPattern (Expr... terms) |
|
Expr | mkConst (Symbol name, Sort range) |
|
Expr | mkConst (String name, Sort range) |
|
Expr | mkFreshConst (String prefix, Sort range) |
|
Expr | mkConst (FuncDecl f) |
|
BoolExpr | mkBoolConst (Symbol name) |
|
BoolExpr | mkBoolConst (String name) |
|
IntExpr | mkIntConst (Symbol name) |
|
IntExpr | mkIntConst (String name) |
|
RealExpr | mkRealConst (Symbol name) |
|
RealExpr | mkRealConst (String name) |
|
BitVecExpr | mkBVConst (Symbol name, int size) |
|
BitVecExpr | mkBVConst (String name, int size) |
|
Expr | mkApp (FuncDecl f, Expr... args) |
|
BoolExpr | mkTrue () |
|
BoolExpr | mkFalse () |
|
BoolExpr | mkBool (boolean value) |
|
BoolExpr | mkEq (Expr x, Expr y) |
|
BoolExpr | mkDistinct (Expr... args) |
|
BoolExpr | mkNot (BoolExpr a) |
|
Expr | mkITE (BoolExpr t1, Expr t2, Expr t3) |
|
BoolExpr | mkIff (BoolExpr t1, BoolExpr t2) |
|
BoolExpr | mkImplies (BoolExpr t1, BoolExpr t2) |
|
BoolExpr | mkXor (BoolExpr t1, BoolExpr t2) |
|
BoolExpr | mkAnd (BoolExpr... t) |
|
BoolExpr | mkOr (BoolExpr... t) |
|
ArithExpr | mkAdd (ArithExpr... t) |
|
ArithExpr | mkMul (ArithExpr... t) |
|
ArithExpr | mkSub (ArithExpr... t) |
|
ArithExpr | mkUnaryMinus (ArithExpr t) |
|
ArithExpr | mkDiv (ArithExpr t1, ArithExpr t2) |
|
IntExpr | mkMod (IntExpr t1, IntExpr t2) |
|
IntExpr | mkRem (IntExpr t1, IntExpr t2) |
|
ArithExpr | mkPower (ArithExpr t1, ArithExpr t2) |
|
BoolExpr | mkLt (ArithExpr t1, ArithExpr t2) |
|
BoolExpr | mkLe (ArithExpr t1, ArithExpr t2) |
|
BoolExpr | mkGt (ArithExpr t1, ArithExpr t2) |
|
BoolExpr | mkGe (ArithExpr t1, ArithExpr t2) |
|
RealExpr | mkInt2Real (IntExpr t) |
|
IntExpr | mkReal2Int (RealExpr t) |
|
BoolExpr | mkIsInteger (RealExpr t) |
|
BitVecExpr | mkBVNot (BitVecExpr t) |
|
BitVecExpr | mkBVRedAND (BitVecExpr t) |
|
BitVecExpr | mkBVRedOR (BitVecExpr t) |
|
BitVecExpr | mkBVAND (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVOR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVXOR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVNAND (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVNOR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVXNOR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVNeg (BitVecExpr t) |
|
BitVecExpr | mkBVAdd (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVSub (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVMul (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVUDiv (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVSDiv (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVURem (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVSRem (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVSMod (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVULT (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSLT (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVULE (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSLE (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVUGE (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSGE (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVUGT (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSGT (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkConcat (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkExtract (int high, int low, BitVecExpr t) |
|
BitVecExpr | mkSignExt (int i, BitVecExpr t) |
|
BitVecExpr | mkZeroExt (int i, BitVecExpr t) |
|
BitVecExpr | mkRepeat (int i, BitVecExpr t) |
|
BitVecExpr | mkBVSHL (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVLSHR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVASHR (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVRotateLeft (int i, BitVecExpr t) |
|
BitVecExpr | mkBVRotateRight (int i, BitVecExpr t) |
|
BitVecExpr | mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) |
|
BitVecExpr | mkInt2BV (int n, IntExpr t) |
|
IntExpr | mkBV2Int (BitVecExpr t, boolean signed) |
|
BoolExpr | mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) |
|
BoolExpr | mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) |
|
BoolExpr | mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) |
|
BoolExpr | mkBVNegNoOverflow (BitVecExpr t) |
|
BoolExpr | mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) |
|
BoolExpr | mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) |
|
ArrayExpr | mkArrayConst (Symbol name, Sort domain, Sort range) |
|
ArrayExpr | mkArrayConst (String name, Sort domain, Sort range) |
|
Expr | mkSelect (ArrayExpr a, Expr i) |
|
ArrayExpr | mkStore (ArrayExpr a, Expr i, Expr v) |
|
ArrayExpr | mkConstArray (Sort domain, Expr v) |
|
ArrayExpr | mkMap (FuncDecl f, ArrayExpr... args) |
|
Expr | mkTermArray (ArrayExpr array) |
|
Expr | mkArrayExt (ArrayExpr arg1, ArrayExpr arg2) |
|
SetSort | mkSetSort (Sort ty) |
|
ArrayExpr | mkEmptySet (Sort domain) |
|
ArrayExpr | mkFullSet (Sort domain) |
|
ArrayExpr | mkSetAdd (ArrayExpr set, Expr element) |
|
ArrayExpr | mkSetDel (ArrayExpr set, Expr element) |
|
ArrayExpr | mkSetUnion (ArrayExpr... args) |
|
ArrayExpr | mkSetIntersection (ArrayExpr... args) |
|
ArrayExpr | mkSetDifference (ArrayExpr arg1, ArrayExpr arg2) |
|
ArrayExpr | mkSetComplement (ArrayExpr arg) |
|
BoolExpr | mkSetMembership (Expr elem, ArrayExpr set) |
|
BoolExpr | mkSetSubset (ArrayExpr arg1, ArrayExpr arg2) |
|
SeqExpr | MkEmptySeq (Sort s) |
|
SeqExpr | MkUnit (Expr elem) |
|
SeqExpr | MkString (String s) |
|
SeqExpr | MkConcat (SeqExpr... t) |
|
IntExpr | MkLength (SeqExpr s) |
|
BoolExpr | MkPrefixOf (SeqExpr s1, SeqExpr s2) |
|
BoolExpr | MkSuffixOf (SeqExpr s1, SeqExpr s2) |
|
BoolExpr | MkContains (SeqExpr s1, SeqExpr s2) |
|
SeqExpr | MkAt (SeqExpr s, IntExpr index) |
|
SeqExpr | MkExtract (SeqExpr s, IntExpr offset, IntExpr length) |
|
IntExpr | MkIndexOf (SeqExpr s, SeqExpr substr, ArithExpr offset) |
|
SeqExpr | MkReplace (SeqExpr s, SeqExpr src, SeqExpr dst) |
|
ReExpr | MkToRe (SeqExpr s) |
|
BoolExpr | MkInRe (SeqExpr s, ReExpr re) |
|
ReExpr | MkStar (ReExpr re) |
|
ReExpr | MPlus (ReExpr re) |
|
ReExpr | MOption (ReExpr re) |
|
ReExpr | MkConcat (ReExpr... t) |
|
ReExpr | MkUnion (ReExpr... t) |
|
Expr | mkNumeral (String v, Sort ty) |
|
Expr | mkNumeral (int v, Sort ty) |
|
Expr | mkNumeral (long v, Sort ty) |
|
RatNum | mkReal (int num, int den) |
|
RatNum | mkReal (String v) |
|
RatNum | mkReal (int v) |
|
RatNum | mkReal (long v) |
|
IntNum | mkInt (String v) |
|
IntNum | mkInt (int v) |
|
IntNum | mkInt (long v) |
|
BitVecNum | mkBV (String v, int size) |
|
BitVecNum | mkBV (int v, int size) |
|
BitVecNum | mkBV (long v, int size) |
|
Quantifier | mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
Quantifier | mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
Quantifier | mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
Quantifier | mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
Quantifier | mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
Quantifier | mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) |
|
void | setPrintMode (Z3_ast_print_mode value) |
|
String | benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) |
|
void | parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) |
|
void | parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) |
|
int | getNumSMTLIBFormulas () |
|
BoolExpr [] | getSMTLIBFormulas () |
|
int | getNumSMTLIBAssumptions () |
|
BoolExpr [] | getSMTLIBAssumptions () |
|
int | getNumSMTLIBDecls () |
|
FuncDecl [] | getSMTLIBDecls () |
|
int | getNumSMTLIBSorts () |
|
Sort [] | getSMTLIBSorts () |
|
BoolExpr | parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) |
|
BoolExpr | parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) |
|
Goal | mkGoal (boolean models, boolean unsatCores, boolean proofs) |
|
Params | mkParams () |
|
int | getNumTactics () |
|
String [] | getTacticNames () |
|
String | getTacticDescription (String name) |
|
Tactic | mkTactic (String name) |
|
Tactic | andThen (Tactic t1, Tactic t2, Tactic... ts) |
|
Tactic | then (Tactic t1, Tactic t2, Tactic... ts) |
|
Tactic | orElse (Tactic t1, Tactic t2) |
|
Tactic | tryFor (Tactic t, int ms) |
|
Tactic | when (Probe p, Tactic t) |
|
Tactic | cond (Probe p, Tactic t1, Tactic t2) |
|
Tactic | repeat (Tactic t, int max) |
|
Tactic | skip () |
|
Tactic | fail () |
|
Tactic | failIf (Probe p) |
|
Tactic | failIfNotDecided () |
|
Tactic | usingParams (Tactic t, Params p) |
|
Tactic | with (Tactic t, Params p) |
|
Tactic | parOr (Tactic... t) |
|
Tactic | parAndThen (Tactic t1, Tactic t2) |
|
void | interrupt () |
|
int | getNumProbes () |
|
String [] | getProbeNames () |
|
String | getProbeDescription (String name) |
|
Probe | mkProbe (String name) |
|
Probe | constProbe (double val) |
|
Probe | lt (Probe p1, Probe p2) |
|
Probe | gt (Probe p1, Probe p2) |
|
Probe | le (Probe p1, Probe p2) |
|
Probe | ge (Probe p1, Probe p2) |
|
Probe | eq (Probe p1, Probe p2) |
|
Probe | and (Probe p1, Probe p2) |
|
Probe | or (Probe p1, Probe p2) |
|
Probe | not (Probe p) |
|
Solver | mkSolver () |
|
Solver | mkSolver (Symbol logic) |
|
Solver | mkSolver (String logic) |
|
Solver | mkSimpleSolver () |
|
Solver | mkSolver (Tactic t) |
|
Fixedpoint | mkFixedpoint () |
|
Optimize | mkOptimize () |
|
FPRMSort | mkFPRoundingModeSort () |
|
FPRMExpr | mkFPRoundNearestTiesToEven () |
|
FPRMNum | mkFPRNE () |
|
FPRMNum | mkFPRoundNearestTiesToAway () |
|
FPRMNum | mkFPRNA () |
|
FPRMNum | mkFPRoundTowardPositive () |
|
FPRMNum | mkFPRTP () |
|
FPRMNum | mkFPRoundTowardNegative () |
|
FPRMNum | mkFPRTN () |
|
FPRMNum | mkFPRoundTowardZero () |
|
FPRMNum | mkFPRTZ () |
|
FPSort | mkFPSort (int ebits, int sbits) |
|
FPSort | mkFPSortHalf () |
|
FPSort | mkFPSort16 () |
|
FPSort | mkFPSortSingle () |
|
FPSort | mkFPSort32 () |
|
FPSort | mkFPSortDouble () |
|
FPSort | mkFPSort64 () |
|
FPSort | mkFPSortQuadruple () |
|
FPSort | mkFPSort128 () |
|
FPNum | mkFPNaN (FPSort s) |
|
FPNum | mkFPInf (FPSort s, boolean negative) |
|
FPNum | mkFPZero (FPSort s, boolean negative) |
|
FPNum | mkFPNumeral (float v, FPSort s) |
|
FPNum | mkFPNumeral (double v, FPSort s) |
|
FPNum | mkFPNumeral (int v, FPSort s) |
|
FPNum | mkFPNumeral (boolean sgn, int exp, int sig, FPSort s) |
|
FPNum | mkFPNumeral (boolean sgn, long exp, long sig, FPSort s) |
|
FPNum | mkFP (float v, FPSort s) |
|
FPNum | mkFP (double v, FPSort s) |
|
FPNum | mkFP (int v, FPSort s) |
|
FPNum | mkFP (boolean sgn, int exp, int sig, FPSort s) |
|
FPNum | mkFP (boolean sgn, long exp, long sig, FPSort s) |
|
FPExpr | mkFPAbs (FPExpr t) |
|
FPExpr | mkFPNeg (FPExpr t) |
|
FPExpr | mkFPAdd (FPRMExpr rm, FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPSub (FPRMExpr rm, FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPMul (FPRMExpr rm, FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPDiv (FPRMExpr rm, FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPFMA (FPRMExpr rm, FPExpr t1, FPExpr t2, FPExpr t3) |
|
FPExpr | mkFPSqrt (FPRMExpr rm, FPExpr t) |
|
FPExpr | mkFPRem (FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPRoundToIntegral (FPRMExpr rm, FPExpr t) |
|
FPExpr | mkFPMin (FPExpr t1, FPExpr t2) |
|
FPExpr | mkFPMax (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPLEq (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPLt (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPGEq (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPGt (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPEq (FPExpr t1, FPExpr t2) |
|
BoolExpr | mkFPIsNormal (FPExpr t) |
|
BoolExpr | mkFPIsSubnormal (FPExpr t) |
|
BoolExpr | mkFPIsZero (FPExpr t) |
|
BoolExpr | mkFPIsInfinite (FPExpr t) |
|
BoolExpr | mkFPIsNaN (FPExpr t) |
|
BoolExpr | mkFPIsNegative (FPExpr t) |
|
BoolExpr | mkFPIsPositive (FPExpr t) |
|
FPExpr | mkFP (BitVecExpr sgn, BitVecExpr sig, BitVecExpr exp) |
|
FPExpr | mkFPToFP (BitVecExpr bv, FPSort s) |
|
FPExpr | mkFPToFP (FPRMExpr rm, FPExpr t, FPSort s) |
|
FPExpr | mkFPToFP (FPRMExpr rm, RealExpr t, FPSort s) |
|
FPExpr | mkFPToFP (FPRMExpr rm, BitVecExpr t, FPSort s, boolean signed) |
|
FPExpr | mkFPToFP (FPSort s, FPRMExpr rm, FPExpr t) |
|
BitVecExpr | mkFPToBV (FPRMExpr rm, FPExpr t, int sz, boolean signed) |
|
RealExpr | mkFPToReal (FPExpr t) |
|
BitVecExpr | mkFPToIEEEBV (FPExpr t) |
|
BitVecExpr | mkFPToFP (FPRMExpr rm, IntExpr exp, RealExpr sig, FPSort s) |
|
AST | wrapAST (long nativeObject) |
|
long | unwrapAST (AST a) |
|
String | SimplifyHelp () |
|
ParamDescrs | getSimplifyParameterDescriptions () |
|
void | updateParamValue (String id, String value) |
|
IDecRefQueue< Constructor > | getConstructorDRQ () |
|
IDecRefQueue< ConstructorList > | getConstructorListDRQ () |
|
IDecRefQueue< AST > | getASTDRQ () |
|
IDecRefQueue< ASTMap > | getASTMapDRQ () |
|
IDecRefQueue< ASTVector > | getASTVectorDRQ () |
|
IDecRefQueue< ApplyResult > | getApplyResultDRQ () |
|
IDecRefQueue< FuncInterp.Entry > | getFuncEntryDRQ () |
|
IDecRefQueue< FuncInterp > | getFuncInterpDRQ () |
|
IDecRefQueue< Goal > | getGoalDRQ () |
|
IDecRefQueue< Model > | getModelDRQ () |
|
IDecRefQueue< Params > | getParamsDRQ () |
|
IDecRefQueue< ParamDescrs > | getParamDescrsDRQ () |
|
IDecRefQueue< Probe > | getProbeDRQ () |
|
IDecRefQueue< Solver > | getSolverDRQ () |
|
IDecRefQueue< Statistics > | getStatisticsDRQ () |
|
IDecRefQueue< Tactic > | getTacticDRQ () |
|
IDecRefQueue< Fixedpoint > | getFixedpointDRQ () |
|
IDecRefQueue< Optimize > | getOptimizeDRQ () |
|
void | close () |
|