Public Member Functions | |
Context () throws Z3Exception | |
Context (Map< String, String > settings) throws Z3Exception | |
IntSymbol | mkSymbol (int i) throws Z3Exception |
StringSymbol | mkSymbol (String name) throws Z3Exception |
BoolSort | getBoolSort () throws Z3Exception |
IntSort | getIntSort () throws Z3Exception |
RealSort | getRealSort () throws Z3Exception |
BoolSort | mkBoolSort () throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (Symbol s) throws Z3Exception |
UninterpretedSort | mkUninterpretedSort (String str) throws Z3Exception |
IntSort | mkIntSort () throws Z3Exception |
RealSort | mkRealSort () throws Z3Exception |
BitVecSort | mkBitVecSort (int size) throws Z3Exception |
ArraySort | mkArraySort (Sort domain, Sort range) throws Z3Exception |
TupleSort | mkTupleSort (Symbol name, Symbol[] fieldNames, Sort[] fieldSorts) throws Z3Exception |
EnumSort | mkEnumSort (Symbol name, Symbol...enumNames) throws Z3Exception |
EnumSort | mkEnumSort (String name, String...enumNames) throws Z3Exception |
ListSort | mkListSort (Symbol name, Sort elemSort) throws Z3Exception |
ListSort | mkListSort (String name, Sort elemSort) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (Symbol name, long size) throws Z3Exception |
FiniteDomainSort | mkFiniteDomainSort (String name, long size) throws Z3Exception |
Constructor | mkConstructor (Symbol name, Symbol recognizer, Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
Constructor | mkConstructor (String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) throws Z3Exception |
DatatypeSort | mkDatatypeSort (Symbol name, Constructor[] constructors) throws Z3Exception |
DatatypeSort | mkDatatypeSort (String name, Constructor[] constructors) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (Symbol[] names, Constructor[][] c) throws Z3Exception |
DatatypeSort[] | mkDatatypeSorts (String[] names, Constructor[][] c) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (Symbol name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkFuncDecl (String name, Sort domain, Sort range) throws Z3Exception |
FuncDecl | mkFreshFuncDecl (String prefix, Sort[] domain, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (Symbol name, Sort range) throws Z3Exception |
FuncDecl | mkConstDecl (String name, Sort range) throws Z3Exception |
FuncDecl | mkFreshConstDecl (String prefix, Sort range) throws Z3Exception |
Expr | mkBound (int index, Sort ty) throws Z3Exception |
Pattern | mkPattern (Expr...terms) throws Z3Exception |
Expr | mkConst (Symbol name, Sort range) throws Z3Exception |
Expr | mkConst (String name, Sort range) throws Z3Exception |
Expr | mkFreshConst (String prefix, Sort range) throws Z3Exception |
Expr | mkConst (FuncDecl f) throws Z3Exception |
BoolExpr | mkBoolConst (Symbol name) throws Z3Exception |
BoolExpr | mkBoolConst (String name) throws Z3Exception |
IntExpr | mkIntConst (Symbol name) throws Z3Exception |
IntExpr | mkIntConst (String name) throws Z3Exception |
RealExpr | mkRealConst (Symbol name) throws Z3Exception |
RealExpr | mkRealConst (String name) throws Z3Exception |
BitVecExpr | mkBVConst (Symbol name, int size) throws Z3Exception |
BitVecExpr | mkBVConst (String name, int size) throws Z3Exception |
Expr | mkApp (FuncDecl f, Expr...args) throws Z3Exception |
BoolExpr | mkTrue () throws Z3Exception |
BoolExpr | mkFalse () throws Z3Exception |
BoolExpr | mkBool (boolean value) throws Z3Exception |
BoolExpr | mkEq (Expr x, Expr y) throws Z3Exception |
BoolExpr | mkDistinct (Expr...args) throws Z3Exception |
BoolExpr | mkNot (BoolExpr a) throws Z3Exception |
Expr | mkITE (BoolExpr t1, Expr t2, Expr t3) throws Z3Exception |
BoolExpr | mkIff (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkImplies (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkXor (BoolExpr t1, BoolExpr t2) throws Z3Exception |
BoolExpr | mkAnd (BoolExpr...t) throws Z3Exception |
BoolExpr | mkOr (BoolExpr...t) throws Z3Exception |
ArithExpr | mkAdd (ArithExpr...t) throws Z3Exception |
ArithExpr | mkMul (ArithExpr...t) throws Z3Exception |
ArithExpr | mkSub (ArithExpr...t) throws Z3Exception |
ArithExpr | mkUnaryMinus (ArithExpr t) throws Z3Exception |
ArithExpr | mkDiv (ArithExpr t1, ArithExpr t2) throws Z3Exception |
IntExpr | mkMod (IntExpr t1, IntExpr t2) throws Z3Exception |
IntExpr | mkRem (IntExpr t1, IntExpr t2) throws Z3Exception |
ArithExpr | mkPower (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkLe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGt (ArithExpr t1, ArithExpr t2) throws Z3Exception |
BoolExpr | mkGe (ArithExpr t1, ArithExpr t2) throws Z3Exception |
RealExpr | mkInt2Real (IntExpr t) throws Z3Exception |
IntExpr | mkReal2Int (RealExpr t) throws Z3Exception |
BoolExpr | mkIsInteger (RealExpr t) throws Z3Exception |
BitVecExpr | mkBVNot (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedAND (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRedOR (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNAND (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVXNOR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVNeg (BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVAdd (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSub (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVMul (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVUDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSDiv (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVURem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSRem (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVSMod (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVULE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSLE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGE (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVUGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSGT (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkConcat (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkExtract (int high, int low, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkSignExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkZeroExt (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkRepeat (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVSHL (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVLSHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVASHR (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateRight (int i, BitVecExpr t) throws Z3Exception |
BitVecExpr | mkBVRotateLeft (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkBVRotateRight (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BitVecExpr | mkInt2BV (int n, IntExpr t) throws Z3Exception |
IntExpr | mkBV2Int (BitVecExpr t, boolean signed) throws Z3Exception |
BoolExpr | mkBVAddNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVAddNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVSubNoUnderflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVSDivNoOverflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
BoolExpr | mkBVNegNoOverflow (BitVecExpr t) throws Z3Exception |
BoolExpr | mkBVMulNoOverflow (BitVecExpr t1, BitVecExpr t2, boolean isSigned) throws Z3Exception |
BoolExpr | mkBVMulNoUnderflow (BitVecExpr t1, BitVecExpr t2) throws Z3Exception |
ArrayExpr | mkArrayConst (Symbol name, Sort domain, Sort range) throws Z3Exception |
ArrayExpr | mkArrayConst (String name, Sort domain, Sort range) throws Z3Exception |
Expr | mkSelect (ArrayExpr a, Expr i) throws Z3Exception |
ArrayExpr | mkStore (ArrayExpr a, Expr i, Expr v) throws Z3Exception |
ArrayExpr | mkConstArray (Sort domain, Expr v) throws Z3Exception |
ArrayExpr | mkMap (FuncDecl f, ArrayExpr...args) throws Z3Exception |
Expr | mkTermArray (ArrayExpr array) throws Z3Exception |
SetSort | mkSetSort (Sort ty) throws Z3Exception |
Expr | mkEmptySet (Sort domain) throws Z3Exception |
Expr | mkFullSet (Sort domain) throws Z3Exception |
Expr | mkSetAdd (Expr set, Expr element) throws Z3Exception |
Expr | mkSetDel (Expr set, Expr element) throws Z3Exception |
Expr | mkSetUnion (Expr...args) throws Z3Exception |
Expr | mkSetIntersection (Expr...args) throws Z3Exception |
Expr | mkSetDifference (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkSetComplement (Expr arg) throws Z3Exception |
Expr | mkSetMembership (Expr elem, Expr set) throws Z3Exception |
Expr | mkSetSubset (Expr arg1, Expr arg2) throws Z3Exception |
Expr | mkNumeral (String v, Sort ty) throws Z3Exception |
Expr | mkNumeral (int v, Sort ty) throws Z3Exception |
Expr | mkNumeral (long v, Sort ty) throws Z3Exception |
RatNum | mkReal (int num, int den) throws Z3Exception |
RatNum | mkReal (String v) throws Z3Exception |
RatNum | mkReal (int v) throws Z3Exception |
RatNum | mkReal (long v) throws Z3Exception |
IntNum | mkInt (String v) throws Z3Exception |
IntNum | mkInt (int v) throws Z3Exception |
IntNum | mkInt (long v) throws Z3Exception |
BitVecNum | mkBV (String v, int size) throws Z3Exception |
BitVecNum | mkBV (int v, int size) throws Z3Exception |
BitVecNum | mkBV (long v, int size) throws Z3Exception |
Quantifier | mkForall (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkForall (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkExists (Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
Quantifier | mkQuantifier (boolean universal, Expr[] boundConstants, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) throws Z3Exception |
void | setPrintMode (Z3_ast_print_mode value) throws Z3Exception |
String | benchmarkToSMTString (String name, String logic, String status, String attributes, BoolExpr[] assumptions, BoolExpr formula) throws Z3Exception |
void | parseSMTLIBString (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
void | parseSMTLIBFile (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
int | getNumSMTLIBFormulas () throws Z3Exception |
BoolExpr[] | getSMTLIBFormulas () throws Z3Exception |
int | getNumSMTLIBAssumptions () throws Z3Exception |
BoolExpr[] | getSMTLIBAssumptions () throws Z3Exception |
int | getNumSMTLIBDecls () throws Z3Exception |
FuncDecl[] | getSMTLIBDecls () throws Z3Exception |
int | getNumSMTLIBSorts () throws Z3Exception |
Sort[] | getSMTLIBSorts () throws Z3Exception |
BoolExpr | parseSMTLIB2String (String str, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
BoolExpr | parseSMTLIB2File (String fileName, Symbol[] sortNames, Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) throws Z3Exception |
Goal | mkGoal (boolean models, boolean unsatCores, boolean proofs) throws Z3Exception |
Params | mkParams () throws Z3Exception |
int | getNumTactics () throws Z3Exception |
String[] | getTacticNames () throws Z3Exception |
String | getTacticDescription (String name) throws Z3Exception |
Tactic | mkTactic (String name) throws Z3Exception |
Tactic | andThen (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | then (Tactic t1, Tactic t2, Tactic...ts) throws Z3Exception |
Tactic | orElse (Tactic t1, Tactic t2) throws Z3Exception |
Tactic | tryFor (Tactic t, int ms) throws Z3Exception |
Tactic | when (Probe p, Tactic t) throws Z3Exception |
Tactic | cond (Probe p, Tactic t1, Tactic t2) throws Z3Exception |
Tactic | repeat (Tactic t, int max) throws Z3Exception |
Tactic | skip () throws Z3Exception |
Tactic | fail () throws Z3Exception |
Tactic | failIf (Probe p) throws Z3Exception |
Tactic | failIfNotDecided () throws Z3Exception |
Tactic | usingParams (Tactic t, Params p) throws Z3Exception |
Tactic | with (Tactic t, Params p) throws Z3Exception |
Tactic | parOr (Tactic...t) throws Z3Exception |
Tactic | parAndThen (Tactic t1, Tactic t2) throws Z3Exception |
void | interrupt () throws Z3Exception |
int | getNumProbes () throws Z3Exception |
String[] | getProbeNames () throws Z3Exception |
String | getProbeDescription (String name) throws Z3Exception |
Probe | mkProbe (String name) throws Z3Exception |
Probe | constProbe (double val) throws Z3Exception |
Probe | lt (Probe p1, Probe p2) throws Z3Exception |
Probe | gt (Probe p1, Probe p2) throws Z3Exception |
Probe | le (Probe p1, Probe p2) throws Z3Exception |
Probe | ge (Probe p1, Probe p2) throws Z3Exception |
Probe | eq (Probe p1, Probe p2) throws Z3Exception |
Probe | and (Probe p1, Probe p2) throws Z3Exception |
Probe | or (Probe p1, Probe p2) throws Z3Exception |
Probe | not (Probe p) throws Z3Exception |
Solver | mkSolver () throws Z3Exception |
Solver | mkSolver (Symbol logic) throws Z3Exception |
Solver | mkSolver (String logic) throws Z3Exception |
Solver | mkSimpleSolver () throws Z3Exception |
Solver | mkSolver (Tactic t) throws Z3Exception |
Fixedpoint | mkFixedpoint () throws Z3Exception |
AST | wrapAST (long nativeObject) throws Z3Exception |
long | unwrapAST (AST a) |
String | SimplifyHelp () throws Z3Exception |
ParamDescrs | getSimplifyParameterDescriptions () throws Z3Exception |
void | updateParamValue (String id, String value) throws Z3Exception |
void | dispose () |
Static Public Member Functions | |
static void | ToggleWarningMessages (boolean enabled) throws Z3Exception |
Protected Member Functions | |
void | finalize () |
Protected Attributes | |
long | m_refCount = 0 |
Package Functions | |
Symbol[] | MkSymbols (String[] names) throws Z3Exception |
long | nCtx () |
void | initContext () throws Z3Exception |
void | checkContextMatch (Z3Object other) throws Z3Exception |
void | checkContextMatch (Z3Object[] arr) throws Z3Exception |
ASTDecRefQueue | ast_DRQ () |
ASTMapDecRefQueue | astmap_DRQ () |
ASTVectorDecRefQueue | astvector_DRQ () |
ApplyResultDecRefQueue | applyResult_DRQ () |
FuncInterpEntryDecRefQueue | funcEntry_DRQ () |
FuncInterpDecRefQueue | funcInterp_DRQ () |
GoalDecRefQueue | goal_DRQ () |
ModelDecRefQueue | model_DRQ () |
ParamsDecRefQueue | params_DRQ () |
ParamDescrsDecRefQueue | paramDescrs_DRQ () |
ProbeDecRefQueue | probe_DRQ () |
SolverDecRefQueue | solver_DRQ () |
StatisticsDecRefQueue | statistics_DRQ () |
TacticDecRefQueue | tactic_DRQ () |
FixedpointDecRefQueue | fixedpoint_DRQ () |
Package Attributes | |
long | m_ctx = 0 |
The main interaction with Z3 happens via the Context.
Definition at line 27 of file Context.java.
Context | ( | ) | throws Z3Exception [inline] |
Definition at line 32 of file Context.java.
{ super(); m_ctx = Native.mkContextRc(0); initContext(); }
Context | ( | Map< String, String > | settings | ) | throws Z3Exception [inline] |
The following parameters can be set:
Definition at line 57 of file Context.java.
{ super(); long cfg = Native.mkConfig(); for (Map.Entry<String, String> kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); initContext(); }
Probe and | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value p1 and p2 evaluate to "true".
Definition at line 2758 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeAnd(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
Tactic andThen | ( | Tactic | t1, |
Tactic | t2, | ||
Tactic... | ts | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 .
Definition at line 2440 of file Context.java.
Referenced by Context.then().
{ checkContextMatch(t1); checkContextMatch(t2); checkContextMatch(ts); long last = 0; if (ts != null && ts.length > 0) { last = ts[ts.length - 1].getNativeObject(); for (int i = ts.length - 2; i >= 0; i--) last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(), last); } if (last != 0) { last = Native.tacticAndThen(nCtx(), t2.getNativeObject(), last); return new Tactic(this, Native.tacticAndThen(nCtx(), t1.getNativeObject(), last)); } else return new Tactic(this, Native.tacticAndThen(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
ApplyResultDecRefQueue applyResult_DRQ | ( | ) | [inline, package] |
Definition at line 2982 of file Context.java.
Referenced by ApplyResult.decRef(), and ApplyResult.incRef().
{
return m_ApplyResult_DRQ;
}
ASTDecRefQueue ast_DRQ | ( | ) | [inline, package] |
Definition at line 2967 of file Context.java.
Referenced by AST.decRef(), and AST.incRef().
{
return m_AST_DRQ;
}
ASTMapDecRefQueue astmap_DRQ | ( | ) | [inline, package] |
Definition at line 2972 of file Context.java.
Referenced by ASTMap.decRef(), and ASTMap.incRef().
{
return m_ASTMap_DRQ;
}
ASTVectorDecRefQueue astvector_DRQ | ( | ) | [inline, package] |
Definition at line 2977 of file Context.java.
Referenced by ASTVector.decRef(), and ASTVector.incRef().
{
return m_ASTVector_DRQ;
}
String benchmarkToSMTString | ( | String | name, |
String | logic, | ||
String | status, | ||
String | attributes, | ||
BoolExpr[] | assumptions, | ||
BoolExpr | formula | ||
) | throws Z3Exception [inline] |
Convert a benchmark into an SMT-LIB formatted string.
name | Name of the benchmark. The argument is optional. |
logic | The benchmark logic. |
status | The status string (sat, unsat, or unknown) |
attributes | Other attributes, such as source, difficulty or category. |
assumptions | Auxiliary assumptions. |
formula | Formula to be checked for consistency in conjunction with assumptions. |
Definition at line 2177 of file Context.java.
{ return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, attributes, (int) assumptions.length, AST.arrayToNative(assumptions), formula.getNativeObject()); }
void checkContextMatch | ( | Z3Object | other | ) | throws Z3Exception [inline, package] |
Definition at line 2938 of file Context.java.
Referenced by Fixedpoint.add(), Goal.add(), Solver.add(), Fixedpoint.addFact(), Fixedpoint.addRule(), Context.and(), Context.andThen(), Probe.apply(), Tactic.apply(), FuncDecl.apply(), Solver.assertAndTrack(), Context.checkContextMatch(), InterpolationContext.ComputeInterpolant(), Context.cond(), Context.eq(), Context.failIf(), Context.ge(), Model.getConstInterp(), Model.getFuncInterp(), InterpolationContext.GetInterpolant(), Context.gt(), Context.le(), Context.lt(), Context.mkAdd(), Context.mkAnd(), Context.mkApp(), Context.mkArraySort(), Context.mkBV2Int(), Context.mkBVAdd(), Context.mkBVAddNoOverflow(), Context.mkBVAddNoUnderflow(), Context.mkBVAND(), Context.mkBVASHR(), Context.mkBVLSHR(), Context.mkBVMul(), Context.mkBVMulNoOverflow(), Context.mkBVMulNoUnderflow(), Context.mkBVNAND(), Context.mkBVNeg(), Context.mkBVNegNoOverflow(), Context.mkBVNOR(), Context.mkBVNot(), Context.mkBVOR(), Context.mkBVRedAND(), Context.mkBVRedOR(), Context.mkBVRotateLeft(), Context.mkBVRotateRight(), Context.mkBVSDiv(), Context.mkBVSDivNoOverflow(), Context.mkBVSGE(), Context.mkBVSGT(), Context.mkBVSHL(), Context.mkBVSLE(), Context.mkBVSLT(), Context.mkBVSMod(), Context.mkBVSRem(), Context.mkBVSub(), Context.mkBVSubNoOverflow(), Context.mkBVSubNoUnderflow(), Context.mkBVUDiv(), Context.mkBVUGE(), Context.mkBVUGT(), Context.mkBVULE(), Context.mkBVULT(), Context.mkBVURem(), Context.mkBVXNOR(), Context.mkBVXOR(), Context.mkConcat(), Context.mkConst(), Context.mkConstArray(), Context.mkConstDecl(), Context.mkDatatypeSort(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkDiv(), Context.mkEmptySet(), Context.mkEnumSort(), Context.mkEq(), Context.mkExtract(), Context.mkFiniteDomainSort(), Context.mkFreshConst(), Context.mkFreshConstDecl(), Context.mkFreshFuncDecl(), Context.mkFullSet(), Context.mkFuncDecl(), Context.mkGe(), Context.mkGt(), Context.mkIff(), Context.mkImplies(), Context.mkInt2BV(), Context.mkInt2Real(), InterpolationContext.MkInterpolant(), Context.mkIsInteger(), Context.mkITE(), Context.mkLe(), Context.mkListSort(), Context.mkLt(), Context.mkMap(), Context.mkMod(), Context.mkMul(), Context.mkNot(), Context.mkNumeral(), Context.mkOr(), Context.mkPower(), Context.mkReal2Int(), Context.mkRem(), Context.mkRepeat(), Context.mkSelect(), Context.mkSetAdd(), Context.mkSetComplement(), Context.mkSetDel(), Context.mkSetDifference(), Context.mkSetIntersection(), Context.mkSetMembership(), Context.mkSetSort(), Context.mkSetSubset(), Context.mkSetUnion(), Context.mkSignExt(), Context.mkStore(), Context.mkSub(), Context.mkTermArray(), Context.mkTupleSort(), Context.mkUnaryMinus(), Context.mkUninterpretedSort(), Context.mkXor(), Context.mkZeroExt(), Context.not(), Context.or(), Context.orElse(), Context.parAndThen(), Context.parOr(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.registerRelation(), Context.repeat(), Solver.setParameters(), Fixedpoint.setParameters(), Expr.substitute(), Expr.substituteVars(), Context.tryFor(), Expr.update(), Fixedpoint.updateRule(), Context.usingParams(), and Context.when().
{ if (this != other.getContext()) throw new Z3Exception("Context mismatch"); }
void checkContextMatch | ( | Z3Object[] | arr | ) | throws Z3Exception [inline, package] |
Definition at line 2944 of file Context.java.
{ if (arr != null) for (Z3Object a : arr) checkContextMatch(a); }
Create a tactic that applies t1 to a given goal if the probe p evaluates to true and t2 otherwise.
Definition at line 2523 of file Context.java.
{ checkContextMatch(p); checkContextMatch(t1); checkContextMatch(t2); return new Tactic(this, Native.tacticCond(nCtx(), p.getNativeObject(), t1.getNativeObject(), t2.getNativeObject())); }
Probe constProbe | ( | double | val | ) | throws Z3Exception [inline] |
Create a probe that always evaluates to val .
Definition at line 2681 of file Context.java.
{ return new Probe(this, Native.probeConst(nCtx(), val)); }
void dispose | ( | ) | [inline] |
Disposes of the context.
Reimplemented from IDisposable.
Definition at line 3070 of file Context.java.
Referenced by Context.finalize().
{ m_AST_DRQ.clear(this); m_ASTMap_DRQ.clear(this); m_ASTVector_DRQ.clear(this); m_ApplyResult_DRQ.clear(this); m_FuncEntry_DRQ.clear(this); m_FuncInterp_DRQ.clear(this); m_Goal_DRQ.clear(this); m_Model_DRQ.clear(this); m_Params_DRQ.clear(this); m_Probe_DRQ.clear(this); m_Solver_DRQ.clear(this); m_Statistics_DRQ.clear(this); m_Tactic_DRQ.clear(this); m_Fixedpoint_DRQ.clear(this); m_boolSort = null; m_intSort = null; m_realSort = null; }
Probe eq | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2
Definition at line 2746 of file Context.java.
Referenced by SortRef.cast(), and BoolSortRef.cast().
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeEq(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
Tactic fail | ( | ) | throws Z3Exception [inline] |
Create a tactic always fails.
Definition at line 2558 of file Context.java.
{ return new Tactic(this, Native.tacticFail(nCtx())); }
Tactic failIf | ( | Probe | p | ) | throws Z3Exception [inline] |
Create a tactic that fails if the probe p evaluates to false.
Definition at line 2568 of file Context.java.
{ checkContextMatch(p); return new Tactic(this, Native.tacticFailIf(nCtx(), p.getNativeObject())); }
Tactic failIfNotDecided | ( | ) | throws Z3Exception [inline] |
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
Definition at line 2580 of file Context.java.
{ return new Tactic(this, Native.tacticFailIfNotDecided(nCtx())); }
void finalize | ( | ) | [inline, protected] |
Finalizer.
Definition at line 3047 of file Context.java.
{ dispose(); if (m_refCount == 0) { try { Native.delContext(m_ctx); } catch (Z3Exception e) { // OK. } m_ctx = 0; } /* else CMW: re-queue the finalizer? */ }
FixedpointDecRefQueue fixedpoint_DRQ | ( | ) | [inline, package] |
Definition at line 3037 of file Context.java.
Referenced by Fixedpoint.decRef(), and Fixedpoint.incRef().
{
return m_Fixedpoint_DRQ;
}
FuncInterpEntryDecRefQueue funcEntry_DRQ | ( | ) | [inline, package] |
Definition at line 2987 of file Context.java.
Referenced by FuncInterp.Entry.decRef(), and FuncInterp.Entry.incRef().
{
return m_FuncEntry_DRQ;
}
FuncInterpDecRefQueue funcInterp_DRQ | ( | ) | [inline, package] |
Definition at line 2992 of file Context.java.
Referenced by FuncInterp.decRef(), and FuncInterp.incRef().
{
return m_FuncInterp_DRQ;
}
Probe ge | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value returned by p1 is greater than or equal the value returned by p2
Definition at line 2733 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeGe(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
BoolSort getBoolSort | ( | ) | throws Z3Exception [inline] |
Retrieves the Boolean sort of the context.
Definition at line 106 of file Context.java.
Referenced by Context.mkBoolConst().
{ if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort; }
IntSort getIntSort | ( | ) | throws Z3Exception [inline] |
Retrieves the Integer sort of the context.
Definition at line 116 of file Context.java.
Referenced by Context.mkInt(), and Context.mkIntConst().
{ if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort; }
int getNumProbes | ( | ) | throws Z3Exception [inline] |
The number of supported Probes.
Definition at line 2643 of file Context.java.
Referenced by Context.getProbeNames().
{ return Native.getNumProbes(nCtx()); }
int getNumSMTLIBAssumptions | ( | ) | throws Z3Exception [inline] |
The number of SMTLIB assumptions parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2259 of file Context.java.
Referenced by Context.getSMTLIBAssumptions().
{ return Native.getSmtlibNumAssumptions(nCtx()); }
int getNumSMTLIBDecls | ( | ) | throws Z3Exception [inline] |
The number of SMTLIB declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2283 of file Context.java.
Referenced by Context.getSMTLIBDecls().
{ return Native.getSmtlibNumDecls(nCtx()); }
int getNumSMTLIBFormulas | ( | ) | throws Z3Exception [inline] |
The number of SMTLIB formulas parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2235 of file Context.java.
Referenced by Context.getSMTLIBFormulas().
{ return Native.getSmtlibNumFormulas(nCtx()); }
int getNumSMTLIBSorts | ( | ) | throws Z3Exception [inline] |
The number of SMTLIB sorts parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2306 of file Context.java.
Referenced by Context.getSMTLIBSorts().
{ return Native.getSmtlibNumSorts(nCtx()); }
int getNumTactics | ( | ) | throws Z3Exception [inline] |
The number of supported tactics.
Definition at line 2399 of file Context.java.
Referenced by Context.getTacticNames().
{ return Native.getNumTactics(nCtx()); }
String getProbeDescription | ( | String | name | ) | throws Z3Exception [inline] |
Returns a string containing a description of the probe with the given name.
Definition at line 2665 of file Context.java.
{ return Native.probeGetDescr(nCtx(), name); }
String [] getProbeNames | ( | ) | throws Z3Exception [inline] |
The names of all supported Probes.
Definition at line 2651 of file Context.java.
{ int n = getNumProbes(); String[] res = new String[n]; for (int i = 0; i < n; i++) res[i] = Native.getProbeName(nCtx(), i); return res; }
RealSort getRealSort | ( | ) | throws Z3Exception [inline] |
Retrieves the Real sort of the context.
Definition at line 126 of file Context.java.
Referenced by Context.mkReal(), and Context.mkRealConst().
{ if (m_realSort == null) m_realSort = new RealSort(this); return m_realSort; }
ParamDescrs getSimplifyParameterDescriptions | ( | ) | throws Z3Exception [inline] |
Retrieves parameter descriptions for simplifier.
Definition at line 2897 of file Context.java.
{ return new ParamDescrs(this, Native.simplifyGetParamDescrs(nCtx())); }
BoolExpr [] getSMTLIBAssumptions | ( | ) | throws Z3Exception [inline] |
The assumptions parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2268 of file Context.java.
{ int n = getNumSMTLIBAssumptions(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = (BoolExpr) Expr.create(this, Native.getSmtlibAssumption(nCtx(), i)); return res; }
FuncDecl [] getSMTLIBDecls | ( | ) | throws Z3Exception [inline] |
The declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2292 of file Context.java.
{ int n = getNumSMTLIBDecls(); FuncDecl[] res = new FuncDecl[n]; for (int i = 0; i < n; i++) res[i] = new FuncDecl(this, Native.getSmtlibDecl(nCtx(), i)); return res; }
BoolExpr [] getSMTLIBFormulas | ( | ) | throws Z3Exception [inline] |
The formulas parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2244 of file Context.java.
{ int n = getNumSMTLIBFormulas(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = (BoolExpr) Expr.create(this, Native.getSmtlibFormula(nCtx(), i)); return res; }
Sort [] getSMTLIBSorts | ( | ) | throws Z3Exception [inline] |
The declarations parsed by the last call to ParseSMTLIBString
or ParseSMTLIBFile
.
Definition at line 2315 of file Context.java.
{ int n = getNumSMTLIBSorts(); Sort[] res = new Sort[n]; for (int i = 0; i < n; i++) res[i] = Sort.create(this, Native.getSmtlibSort(nCtx(), i)); return res; }
String getTacticDescription | ( | String | name | ) | throws Z3Exception [inline] |
Returns a string containing a description of the tactic with the given name.
Definition at line 2421 of file Context.java.
{ return Native.tacticGetDescr(nCtx(), name); }
String [] getTacticNames | ( | ) | throws Z3Exception [inline] |
The names of all supported tactics.
Definition at line 2407 of file Context.java.
{ int n = getNumTactics(); String[] res = new String[n]; for (int i = 0; i < n; i++) res[i] = Native.getTacticName(nCtx(), i); return res; }
GoalDecRefQueue goal_DRQ | ( | ) | [inline, package] |
Definition at line 2997 of file Context.java.
Referenced by Goal.decRef(), and Goal.incRef().
{
return m_Goal_DRQ;
}
Probe gt | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2
Definition at line 2705 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeGt(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
void initContext | ( | ) | throws Z3Exception [inline, package] |
Definition at line 2932 of file Context.java.
Referenced by Context.Context(), and InterpolationContext.InterpolationContext().
{ setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); Native.setInternalErrorHandler(nCtx()); }
void interrupt | ( | ) | throws Z3Exception [inline] |
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.
Definition at line 2635 of file Context.java.
{ Native.interrupt(nCtx()); }
Probe le | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value returned by p1 is less than or equal the value returned by p2
Definition at line 2719 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeLe(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
Probe lt | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2
Definition at line 2691 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeLt(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
ArithExpr mkAdd | ( | ArithExpr... | t | ) | throws Z3Exception [inline] |
Create an expression representing t[0] + t[1] + ...
.
Definition at line 763 of file Context.java.
{ checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t))); }
BoolExpr mkAnd | ( | BoolExpr... | t | ) | throws Z3Exception [inline] |
Create an expression representing t[0] and t[1] and ...
.
Definition at line 741 of file Context.java.
{ checkContextMatch(t); return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, AST.arrayToNative(t))); }
Expr mkApp | ( | FuncDecl | f, |
Expr... | args | ||
) | throws Z3Exception [inline] |
Create a new function application.
Definition at line 624 of file Context.java.
Referenced by EnumSort.getConsts(), ListSort.getNil(), and Context.mkConst().
{ checkContextMatch(f); checkContextMatch(args); return Expr.create(this, f, args); }
ArrayExpr mkArrayConst | ( | Symbol | name, |
Sort | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Create an array constant.
Definition at line 1633 of file Context.java.
{ return (ArrayExpr) mkConst(name, mkArraySort(domain, range)); }
ArrayExpr mkArrayConst | ( | String | name, |
Sort | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Create an array constant.
Definition at line 1643 of file Context.java.
{ return (ArrayExpr) mkConst(mkSymbol(name), mkArraySort(domain, range)); }
ArraySort mkArraySort | ( | Sort | domain, |
Sort | range | ||
) | throws Z3Exception [inline] |
Create a new array sort.
Definition at line 191 of file Context.java.
Referenced by Context.mkArrayConst().
{ checkContextMatch(domain); checkContextMatch(range); return new ArraySort(this, domain, range); }
BitVecSort mkBitVecSort | ( | int | size | ) | throws Z3Exception [inline] |
Create a new bit-vector sort.
Definition at line 182 of file Context.java.
Referenced by Context.mkBV(), and Context.mkBVConst().
{ return new BitVecSort(this, Native.mkBvSort(nCtx(), size)); }
BoolExpr mkBool | ( | boolean | value | ) | throws Z3Exception [inline] |
Creates a Boolean value.
Definition at line 650 of file Context.java.
BoolExpr mkBoolConst | ( | Symbol | name | ) | throws Z3Exception [inline] |
Create a Boolean constant.
Definition at line 552 of file Context.java.
{ return (BoolExpr) mkConst(name, getBoolSort()); }
BoolExpr mkBoolConst | ( | String | name | ) | throws Z3Exception [inline] |
Create a Boolean constant.
Definition at line 561 of file Context.java.
{ return (BoolExpr) mkConst(mkSymbol(name), getBoolSort()); }
BoolSort mkBoolSort | ( | ) | throws Z3Exception [inline] |
Create a new Boolean sort.
Definition at line 136 of file Context.java.
Referenced by Expr.isBool().
{ return new BoolSort(this); }
Expr mkBound | ( | int | index, |
Sort | ty | ||
) | throws Z3Exception [inline] |
Creates a new bound variable.
index | The de-Bruijn index of the variable |
ty | The sort of the variable |
Definition at line 482 of file Context.java.
{ return Expr.create(this, Native.mkBound(nCtx(), index, ty.getNativeObject())); }
BitVecNum mkBV | ( | String | v, |
int | size | ||
) | throws Z3Exception [inline] |
Create a bit-vector numeral.
v | A string representing the value in decimal notation. |
size | the size of the bit-vector |
Definition at line 2025 of file Context.java.
{ return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); }
BitVecNum mkBV | ( | int | v, |
int | size | ||
) | throws Z3Exception [inline] |
Create a bit-vector numeral.
v | value of the numeral. |
size | the size of the bit-vector |
Definition at line 2035 of file Context.java.
{ return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); }
BitVecNum mkBV | ( | long | v, |
int | size | ||
) | throws Z3Exception [inline] |
Create a bit-vector numeral.
v | value of the numeral. |
*
size | the size of the bit-vector |
Definition at line 2045 of file Context.java.
{ return (BitVecNum) mkNumeral(v, mkBitVecSort(size)); }
IntExpr mkBV2Int | ( | BitVecExpr | t, |
boolean | signed | ||
) | throws Z3Exception [inline] |
Create an integer from the bit-vector argument t . If is_signed
is false, then the bit-vector t1
is treated as unsigned. So the result is non-negative and in the range [0..2^N-1]
, where N are the number of bits in t . If is_signed
is true, t1
is treated as a signed bit-vector.
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of bit-vector sort.
Definition at line 1509 of file Context.java.
{ checkContextMatch(t); return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(), (signed) ? true : false)); }
BitVecExpr mkBVAdd | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement addition. The arguments must have the same bit-vector sort.
Definition at line 1071 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvadd(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVAddNoOverflow | ( | BitVecExpr | t1, |
BitVecExpr | t2, | ||
boolean | isSigned | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise addition does not overflow. The arguments must be of bit-vector sort.
Definition at line 1521 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true : false)); }
BoolExpr mkBVAddNoUnderflow | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise addition does not underflow. The arguments must be of bit-vector sort.
Definition at line 1536 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvaddNoUnderflow(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVAND | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise conjunction. The arguments must have a bit-vector sort.
Definition at line 982 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvand(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVASHR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Arithmetic shift right It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1416 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvashr(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVConst | ( | Symbol | name, |
int | size | ||
) | throws Z3Exception [inline] |
Creates a bit-vector constant.
Definition at line 606 of file Context.java.
{ return (BitVecExpr) mkConst(name, mkBitVecSort(size)); }
BitVecExpr mkBVConst | ( | String | name, |
int | size | ||
) | throws Z3Exception [inline] |
Creates a bit-vector constant.
Definition at line 615 of file Context.java.
{ return (BitVecExpr) mkConst(name, mkBitVecSort(size)); }
BitVecExpr mkBVLSHR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Logical shift right It is equivalent to unsigned division by 2^x
where x
is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1396 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvlshr(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVMul | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement multiplication. The arguments must have the same bit-vector sort.
Definition at line 1097 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvmul(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVMulNoOverflow | ( | BitVecExpr | t1, |
BitVecExpr | t2, | ||
boolean | isSigned | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise multiplication does not overflow. The arguments must be of bit-vector sort.
Definition at line 1605 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true : false)); }
BoolExpr mkBVMulNoUnderflow | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise multiplication does not underflow. The arguments must be of bit-vector sort.
Definition at line 1620 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvmulNoUnderflow(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVNAND | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise NAND. The arguments must have a bit-vector sort.
Definition at line 1021 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvnand(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVNeg | ( | BitVecExpr | t | ) | throws Z3Exception [inline] |
Standard two's complement unary minus. The arguments must have a bit-vector sort.
Definition at line 1060 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkBvneg(nCtx(), t.getNativeObject())); }
BoolExpr mkBVNegNoOverflow | ( | BitVecExpr | t | ) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise negation does not overflow. The arguments must be of bit-vector sort.
Definition at line 1593 of file Context.java.
{ checkContextMatch(t); return new BoolExpr(this, Native.mkBvnegNoOverflow(nCtx(), t.getNativeObject())); }
BitVecExpr mkBVNOR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise NOR. The arguments must have a bit-vector sort.
Definition at line 1034 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvnor(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVNot | ( | BitVecExpr | t | ) | throws Z3Exception [inline] |
Bitwise negation. The argument must have a bit-vector sort.
Definition at line 947 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkBvnot(nCtx(), t.getNativeObject())); }
BitVecExpr mkBVOR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise disjunction. The arguments must have a bit-vector sort.
Definition at line 995 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvor(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVRedAND | ( | BitVecExpr | t | ) | throws Z3Exception [inline] |
Take conjunction of bits in a vector, return vector of length 1. The argument must have a bit-vector sort.
Definition at line 958 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredand(nCtx(), t.getNativeObject())); }
BitVecExpr mkBVRedOR | ( | BitVecExpr | t | ) | throws Z3Exception [inline] |
Take disjunction of bits in a vector, return vector of length 1. The argument must have a bit-vector sort.
Definition at line 970 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkBvredor(nCtx(), t.getNativeObject())); }
BitVecExpr mkBVRotateLeft | ( | int | i, |
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Rotate Left. Rotate bits of t
to the left i
times. The argument t must have a bit-vector sort.
Definition at line 1429 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateLeft(nCtx(), i, t.getNativeObject())); }
BitVecExpr mkBVRotateLeft | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Rotate Left. Rotate bits of t1 to the left t2 times. The arguments must have the same bit-vector sort.
Definition at line 1454 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkExtRotateLeft(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVRotateRight | ( | int | i, |
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Rotate Right. Rotate bits of t
to the right i
times. The argument t must have a bit-vector sort.
Definition at line 1441 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkRotateRight(nCtx(), i, t.getNativeObject())); }
BitVecExpr mkBVRotateRight | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Rotate Right. Rotate bits of t1 to the rightt2 times. The arguments must have the same bit-vector sort.
Definition at line 1469 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkExtRotateRight(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVSDiv | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Signed division. It is defined in the following way:
floor
of t1/t2
if t2
is different from zero, and t1*t2 >= 0
.ceiling
of t1/t2
if t2
is different from zero, and t1*t2 < 0
.If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1133 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsdiv(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSDivNoOverflow | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise signed division does not overflow. The arguments must be of bit-vector sort.
Definition at line 1579 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsdivNoOverflow(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSGE | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement signed greater than or equal to. The arguments must have the same bit-vector sort.
Definition at line 1258 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsge(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSGT | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement signed greater-than. The arguments must have the same bit-vector sort.
Definition at line 1284 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsgt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVSHL | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Shift left. It is equivalent to multiplication by 2^x
where x
is the value of t2 .
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1377 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvshl(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSLE | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement signed less-than or equal to. The arguments must have the same bit-vector sort.
Definition at line 1232 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsle(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSLT | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement signed less-than The arguments must have the same bit-vector sort.
Definition at line 1206 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvslt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVSMod | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement signed remainder (sign follows divisor). If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1180 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsmod(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVSRem | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Signed remainder. It is defined as t1 - (t1 /s t2) * t2
, where /s
represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1
.
If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1166 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsrem(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVSub | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Two's complement subtraction. The arguments must have the same bit-vector sort.
Definition at line 1084 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvsub(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSubNoOverflow | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise subtraction does not overflow. The arguments must be of bit-vector sort.
Definition at line 1550 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsubNoOverflow(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVSubNoUnderflow | ( | BitVecExpr | t1, |
BitVecExpr | t2, | ||
boolean | isSigned | ||
) | throws Z3Exception [inline] |
Create a predicate that checks that the bit-wise subtraction does not underflow. The arguments must be of bit-vector sort.
Definition at line 1564 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1 .getNativeObject(), t2.getNativeObject(), (isSigned) ? true : false)); }
BitVecExpr mkBVUDiv | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned division. It is defined as the floor of t1/t2
if t2
is different from zero. If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1112 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvudiv(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVUGE | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned greater than or equal to. The arguments must have the same bit-vector sort.
Definition at line 1245 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvuge(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVUGT | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned greater-than. The arguments must have the same bit-vector sort.
Definition at line 1271 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvugt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVULE | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned less-than or equal to. The arguments must have the same bit-vector sort.
Definition at line 1219 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvule(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkBVULT | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned less-than The arguments must have the same bit-vector sort.
Definition at line 1193 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkBvult(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVURem | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Unsigned remainder. It is defined as t1 - (t1 /u t2) * t2
, where /u
represents unsigned division. If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1148 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvurem(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVXNOR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise XNOR. The arguments must have a bit-vector sort.
Definition at line 1047 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvxnor(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkBVXOR | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bitwise XOR. The arguments must have a bit-vector sort.
Definition at line 1008 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkBvxor(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkConcat | ( | BitVecExpr | t1, |
BitVecExpr | t2 | ||
) | throws Z3Exception [inline] |
Bit-vector concatenation. The arguments must have a bit-vector sort.
n1+n2
, where n1
(n2
) is the size of t1
(t2
). Definition at line 1302 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BitVecExpr(this, Native.mkConcat(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
Expr mkConst | ( | Symbol | name, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new Constant of sort range and named name .
Definition at line 505 of file Context.java.
Referenced by Context.mkArrayConst(), Context.mkBoolConst(), Context.mkBVConst(), Context.mkConst(), Context.mkIntConst(), and Context.mkRealConst().
{ checkContextMatch(name); checkContextMatch(range); return Expr.create( this, Native.mkConst(nCtx(), name.getNativeObject(), range.getNativeObject())); }
Expr mkConst | ( | String | name, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new Constant of sort range and named name .
Definition at line 521 of file Context.java.
Expr mkConst | ( | FuncDecl | f | ) | throws Z3Exception [inline] |
Creates a fresh constant from the FuncDecl f .
f | A decl of a 0-arity function |
Definition at line 543 of file Context.java.
{ return mkApp(f, (Expr[]) null); }
ArrayExpr mkConstArray | ( | Sort | domain, |
Expr | v | ||
) | throws Z3Exception [inline] |
Create a constant array. The resulting term is an array, such that a select
on an arbitrary index produces the value v
.
Definition at line 1699 of file Context.java.
{ checkContextMatch(domain); checkContextMatch(v); return new ArrayExpr(this, Native.mkConstArray(nCtx(), domain.getNativeObject(), v.getNativeObject())); }
FuncDecl mkConstDecl | ( | Symbol | name, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new constant function declaration.
Definition at line 447 of file Context.java.
{ checkContextMatch(name); checkContextMatch(range); return new FuncDecl(this, name, null, range); }
FuncDecl mkConstDecl | ( | String | name, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new constant function declaration.
Definition at line 458 of file Context.java.
{ checkContextMatch(range); return new FuncDecl(this, mkSymbol(name), null, range); }
Constructor mkConstructor | ( | Symbol | name, |
Symbol | recognizer, | ||
Symbol[] | fieldNames, | ||
Sort[] | sorts, | ||
int[] | sortRefs | ||
) | throws Z3Exception [inline] |
Create a datatype constructor.
name | constructor name |
recognizer | name of recognizer function. |
fieldNames | names of the constructor fields. |
sorts | field sorts, 0 if the field sort refers to a recursive sort. |
sortRefs | reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. |
Definition at line 287 of file Context.java.
{ return new Constructor(this, name, recognizer, fieldNames, sorts, sortRefs); }
Constructor mkConstructor | ( | String | name, |
String | recognizer, | ||
String[] | fieldNames, | ||
Sort[] | sorts, | ||
int[] | sortRefs | ||
) | throws Z3Exception [inline] |
Create a datatype constructor.
name | |
recognizer | |
fieldNames | |
sorts | |
sortRefs |
Definition at line 303 of file Context.java.
DatatypeSort mkDatatypeSort | ( | Symbol | name, |
Constructor[] | constructors | ||
) | throws Z3Exception [inline] |
Create a new datatype sort.
Definition at line 315 of file Context.java.
{ checkContextMatch(name); checkContextMatch(constructors); return new DatatypeSort(this, name, constructors); }
DatatypeSort mkDatatypeSort | ( | String | name, |
Constructor[] | constructors | ||
) | throws Z3Exception [inline] |
Create a new datatype sort.
Definition at line 327 of file Context.java.
{ checkContextMatch(constructors); return new DatatypeSort(this, mkSymbol(name), constructors); }
DatatypeSort [] mkDatatypeSorts | ( | Symbol[] | names, |
Constructor | c[][] | ||
) | throws Z3Exception [inline] |
Create mutually recursive datatypes.
names | names of datatype sorts |
c | list of constructors, one list per sort. |
Definition at line 340 of file Context.java.
Referenced by Context.mkDatatypeSorts().
{ checkContextMatch(names); int n = (int) names.length; ConstructorList[] cla = new ConstructorList[n]; long[] n_constr = new long[n]; for (int i = 0; i < n; i++) { Constructor[] constructor = c[i]; checkContextMatch(constructor); cla[i] = new ConstructorList(this, constructor); n_constr[i] = cla[i].getNativeObject(); } long[] n_res = new long[n]; Native.mkDatatypes(nCtx(), n, Symbol.arrayToNative(names), n_res, n_constr); DatatypeSort[] res = new DatatypeSort[n]; for (int i = 0; i < n; i++) res[i] = new DatatypeSort(this, n_res[i]); return res; }
DatatypeSort [] mkDatatypeSorts | ( | String[] | names, |
Constructor | c[][] | ||
) | throws Z3Exception [inline] |
Create mutually recursive data-types.
names | |
c |
Definition at line 371 of file Context.java.
{ return mkDatatypeSorts(MkSymbols(names), c); }
BoolExpr mkDistinct | ( | Expr... | args | ) | throws Z3Exception [inline] |
Creates a distinct
term.
Definition at line 669 of file Context.java.
{ checkContextMatch(args); return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length, AST.arrayToNative(args))); }
ArithExpr mkDiv | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 / t2
.
Definition at line 807 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return (ArithExpr) Expr.create(this, Native.mkDiv(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
Expr mkEmptySet | ( | Sort | domain | ) | throws Z3Exception [inline] |
Create an empty set.
Definition at line 1753 of file Context.java.
{ checkContextMatch(domain); return Expr.create(this, Native.mkEmptySet(nCtx(), domain.getNativeObject())); }
EnumSort mkEnumSort | ( | Symbol | name, |
Symbol... | enumNames | ||
) | throws Z3Exception [inline] |
Create a new enumeration sort.
Definition at line 216 of file Context.java.
{ checkContextMatch(name); checkContextMatch(enumNames); return new EnumSort(this, name, enumNames); }
EnumSort mkEnumSort | ( | String | name, |
String... | enumNames | ||
) | throws Z3Exception [inline] |
Create a new enumeration sort.
Definition at line 228 of file Context.java.
BoolExpr mkEq | ( | Expr | x, |
Expr | y | ||
) | throws Z3Exception [inline] |
Creates the equality x = y .
Definition at line 658 of file Context.java.
{ checkContextMatch(x); checkContextMatch(y); return new BoolExpr(this, Native.mkEq(nCtx(), x.getNativeObject(), y.getNativeObject())); }
Quantifier mkExists | ( | Sort[] | sorts, |
Symbol[] | names, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create an existential Quantifier.
Definition at line 2095 of file Context.java.
Referenced by Context.mkQuantifier().
{ return new Quantifier(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); }
Quantifier mkExists | ( | Expr[] | boundConstants, |
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create an existential Quantifier.
Definition at line 2107 of file Context.java.
{ return new Quantifier(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); }
BitVecExpr mkExtract | ( | int | high, |
int | low, | ||
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Bit-vector extraction. Extract the bits high down to low from a bitvector of size m
to yield a new bitvector of size n
, where n = high - low + 1
. The argument t must have a bit-vector sort.
Definition at line 1318 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkExtract(nCtx(), high, low, t.getNativeObject())); }
BoolExpr mkFalse | ( | ) | throws Z3Exception [inline] |
FiniteDomainSort mkFiniteDomainSort | ( | Symbol | name, |
long | size | ||
) | throws Z3Exception [inline] |
Create a new finite domain sort.
Definition at line 258 of file Context.java.
{ checkContextMatch(name); return new FiniteDomainSort(this, name, size); }
FiniteDomainSort mkFiniteDomainSort | ( | String | name, |
long | size | ||
) | throws Z3Exception [inline] |
Create a new finite domain sort.
Definition at line 269 of file Context.java.
{ return new FiniteDomainSort(this, mkSymbol(name), size); }
Fixedpoint mkFixedpoint | ( | ) | throws Z3Exception [inline] |
Create a Fixedpoint context.
Definition at line 2849 of file Context.java.
{ return new Fixedpoint(this); }
Quantifier mkForall | ( | Sort[] | sorts, |
Symbol[] | names, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create a universal Quantifier. Creates a forall formula, where weight is the weight, patterns is an array of patterns, sorts is an array with the sorts of the bound variables, names is an array with the 'names' of the bound variables, and body is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.
sorts | the sorts of the bound variables. |
names | names of the bound variables |
body | the body of the quantifier. |
weight | quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. |
patterns | array containing the patterns created using MkPattern . |
noPatterns | array containing the anti-patterns created using MkPattern . |
quantifierID | optional symbol to track quantifier. |
skolemID | optional symbol to track skolem constants. |
Definition at line 2070 of file Context.java.
Referenced by Context.mkQuantifier().
{ return new Quantifier(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); }
Quantifier mkForall | ( | Expr[] | boundConstants, |
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create a universal Quantifier.
Definition at line 2082 of file Context.java.
{ return new Quantifier(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); }
Expr mkFreshConst | ( | String | prefix, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a fresh Constant of sort range and a name prefixed with prefix .
Definition at line 531 of file Context.java.
{ checkContextMatch(range); return Expr.create(this, Native.mkFreshConst(nCtx(), prefix, range.getNativeObject())); }
FuncDecl mkFreshConstDecl | ( | String | prefix, |
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a fresh constant function declaration with a name prefixed with prefix .
Definition at line 470 of file Context.java.
{ checkContextMatch(range); return new FuncDecl(this, prefix, null, range); }
FuncDecl mkFreshFuncDecl | ( | String | prefix, |
Sort[] | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a fresh function declaration with a name prefixed with prefix .
Definition at line 435 of file Context.java.
{ checkContextMatch(domain); checkContextMatch(range); return new FuncDecl(this, prefix, domain, range); }
Expr mkFullSet | ( | Sort | domain | ) | throws Z3Exception [inline] |
Create the full set.
Definition at line 1764 of file Context.java.
{ checkContextMatch(domain); return Expr.create(this, Native.mkFullSet(nCtx(), domain.getNativeObject())); }
FuncDecl mkFuncDecl | ( | Symbol | name, |
Sort[] | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new function declaration.
Definition at line 381 of file Context.java.
{ checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); return new FuncDecl(this, name, domain, range); }
FuncDecl mkFuncDecl | ( | Symbol | name, |
Sort | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new function declaration.
Definition at line 394 of file Context.java.
{ checkContextMatch(name); checkContextMatch(domain); checkContextMatch(range); Sort[] q = new Sort[] { domain }; return new FuncDecl(this, name, q, range); }
FuncDecl mkFuncDecl | ( | String | name, |
Sort[] | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new function declaration.
Definition at line 408 of file Context.java.
{ checkContextMatch(domain); checkContextMatch(range); return new FuncDecl(this, mkSymbol(name), domain, range); }
FuncDecl mkFuncDecl | ( | String | name, |
Sort | domain, | ||
Sort | range | ||
) | throws Z3Exception [inline] |
Creates a new function declaration.
Definition at line 420 of file Context.java.
{ checkContextMatch(domain); checkContextMatch(range); Sort[] q = new Sort[] { domain }; return new FuncDecl(this, mkSymbol(name), q, range); }
BoolExpr mkGe | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 >= t2
Definition at line 895 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkGe(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
Goal mkGoal | ( | boolean | models, |
boolean | unsatCores, | ||
boolean | proofs | ||
) | throws Z3Exception [inline] |
Creates a new Goal. Note that the Context must have been created with proof generation support if proofs is set to true here.
models | Indicates whether model generation should be enabled. |
unsatCores | Indicates whether unsat core generation should be enabled. |
proofs | Indicates whether proof generation should be enabled. |
Definition at line 2380 of file Context.java.
{ return new Goal(this, models, unsatCores, proofs); }
BoolExpr mkGt | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 > t2
Definition at line 883 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkGt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkIff | ( | BoolExpr | t1, |
BoolExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 iff t2
.
Definition at line 705 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkIff(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BoolExpr mkImplies | ( | BoolExpr | t1, |
BoolExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 -> t2
.
Definition at line 717 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkImplies(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
IntNum mkInt | ( | String | v | ) | throws Z3Exception [inline] |
Create an integer numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1989 of file Context.java.
{ return new IntNum(this, Native.mkNumeral(nCtx(), v, getIntSort() .getNativeObject())); }
IntNum mkInt | ( | int | v | ) | throws Z3Exception [inline] |
Create an integer numeral.
v | value of the numeral. |
Definition at line 2001 of file Context.java.
{ return new IntNum(this, Native.mkInt(nCtx(), v, getIntSort() .getNativeObject())); }
IntNum mkInt | ( | long | v | ) | throws Z3Exception [inline] |
Create an integer numeral.
v | value of the numeral. |
Definition at line 2013 of file Context.java.
{ return new IntNum(this, Native.mkInt64(nCtx(), v, getIntSort() .getNativeObject())); }
BitVecExpr mkInt2BV | ( | int | n, |
IntExpr | t | ||
) | throws Z3Exception [inline] |
Create an n bit bit-vector from the integer argument t . NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of integer sort.
Definition at line 1487 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkInt2bv(nCtx(), n, t.getNativeObject())); }
RealExpr mkInt2Real | ( | IntExpr | t | ) | throws Z3Exception [inline] |
Coerce an integer to a real. There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
You can take the floor of a real by creating an auxiliary integer Term k
and and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1
. The argument must be of integer sort.
Definition at line 913 of file Context.java.
{ checkContextMatch(t); return new RealExpr(this, Native.mkInt2real(nCtx(), t.getNativeObject())); }
IntExpr mkIntConst | ( | Symbol | name | ) | throws Z3Exception [inline] |
Creates an integer constant.
Definition at line 570 of file Context.java.
{ return (IntExpr) mkConst(name, getIntSort()); }
IntExpr mkIntConst | ( | String | name | ) | throws Z3Exception [inline] |
Creates an integer constant.
Definition at line 579 of file Context.java.
{ return (IntExpr) mkConst(name, getIntSort()); }
IntSort mkIntSort | ( | ) | throws Z3Exception [inline] |
Create a new integer sort.
Definition at line 164 of file Context.java.
{ return new IntSort(this); }
BoolExpr mkIsInteger | ( | RealExpr | t | ) | throws Z3Exception [inline] |
Creates an expression that checks whether a real number is an integer.
Definition at line 936 of file Context.java.
{ checkContextMatch(t); return new BoolExpr(this, Native.mkIsInt(nCtx(), t.getNativeObject())); }
Create an expression representing an if-then-else: ite(t1, t2, t3)
.
t1 | An expression with Boolean sort |
t2 | An expression |
t3 | An expression with the same sort as t2 |
Definition at line 692 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); checkContextMatch(t3); return Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(), t2.getNativeObject(), t3.getNativeObject())); }
BoolExpr mkLe | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 <= t2
Definition at line 871 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkLe(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
ListSort mkListSort | ( | Symbol | name, |
Sort | elemSort | ||
) | throws Z3Exception [inline] |
Create a new list sort.
Definition at line 237 of file Context.java.
{ checkContextMatch(name); checkContextMatch(elemSort); return new ListSort(this, name, elemSort); }
ListSort mkListSort | ( | String | name, |
Sort | elemSort | ||
) | throws Z3Exception [inline] |
Create a new list sort.
Definition at line 248 of file Context.java.
{ checkContextMatch(elemSort); return new ListSort(this, mkSymbol(name), elemSort); }
BoolExpr mkLt | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 < t2
Definition at line 859 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkLt(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
ArrayExpr mkMap | ( | FuncDecl | f, |
ArrayExpr... | args | ||
) | throws Z3Exception [inline] |
Maps f on the argument arrays. Eeach element of args
must be of an array sort [domain_i -> range_i]
. The function declaration f
must have type range_1 .. range_n -> range
. v
must have sort range. The sort of the result is [domain_i -> range]
.
Definition at line 1717 of file Context.java.
{ checkContextMatch(f); checkContextMatch(args); return (ArrayExpr) Expr.create(this, Native.mkMap(nCtx(), f.getNativeObject(), AST.arrayLength(args), AST.arrayToNative(args))); }
IntExpr mkMod | ( | IntExpr | t1, |
IntExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 mod t2
. The arguments must have int type.
Definition at line 820 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new IntExpr(this, Native.mkMod(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
ArithExpr mkMul | ( | ArithExpr... | t | ) | throws Z3Exception [inline] |
Create an expression representing t[0] * t[1] * ...
.
Definition at line 774 of file Context.java.
{ checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t))); }
BoolExpr mkNot | ( | BoolExpr | a | ) | throws Z3Exception [inline] |
Mk an expression representing not(a)
.
Definition at line 679 of file Context.java.
{ checkContextMatch(a); return new BoolExpr(this, Native.mkNot(nCtx(), a.getNativeObject())); }
Expr mkNumeral | ( | String | v, |
Sort | ty | ||
) | throws Z3Exception [inline] |
Create a Term of a given sort.
v | A string representing the Term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]* . |
ty | The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. |
Definition at line 1890 of file Context.java.
Referenced by Context.mkBV().
{ checkContextMatch(ty); return Expr.create(this, Native.mkNumeral(nCtx(), v, ty.getNativeObject())); }
Expr mkNumeral | ( | int | v, |
Sort | ty | ||
) | throws Z3Exception [inline] |
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1908 of file Context.java.
{ checkContextMatch(ty); return Expr.create(this, Native.mkInt(nCtx(), v, ty.getNativeObject())); }
Expr mkNumeral | ( | long | v, |
Sort | ty | ||
) | throws Z3Exception [inline] |
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1925 of file Context.java.
{ checkContextMatch(ty); return Expr.create(this, Native.mkInt64(nCtx(), v, ty.getNativeObject())); }
BoolExpr mkOr | ( | BoolExpr... | t | ) | throws Z3Exception [inline] |
Create an expression representing t[0] or t[1] or ...
.
Definition at line 752 of file Context.java.
{ checkContextMatch(t); return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, AST.arrayToNative(t))); }
Params mkParams | ( | ) | throws Z3Exception [inline] |
Creates a new ParameterSet.
Definition at line 2390 of file Context.java.
{ return new Params(this); }
Pattern mkPattern | ( | Expr... | terms | ) | throws Z3Exception [inline] |
Create a quantifier pattern.
Definition at line 491 of file Context.java.
{ if (terms.length == 0) throw new Z3Exception("Cannot create a pattern from zero terms"); long[] termsNative = AST.arrayToNative(terms); return new Pattern(this, Native.mkPattern(nCtx(), (int) terms.length, termsNative)); }
ArithExpr mkPower | ( | ArithExpr | t1, |
ArithExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 ^ t2
.
Definition at line 845 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return (ArithExpr) Expr.create( this, Native.mkPower(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
Probe mkProbe | ( | String | name | ) | throws Z3Exception [inline] |
Creates a new Probe.
Definition at line 2673 of file Context.java.
{ return new Probe(this, name); }
Quantifier mkQuantifier | ( | boolean | universal, |
Sort[] | sorts, | ||
Symbol[] | names, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create a Quantifier.
Definition at line 2119 of file Context.java.
Quantifier mkQuantifier | ( | boolean | universal, |
Expr[] | boundConstants, | ||
Expr | body, | ||
int | weight, | ||
Pattern[] | patterns, | ||
Expr[] | noPatterns, | ||
Symbol | quantifierID, | ||
Symbol | skolemID | ||
) | throws Z3Exception [inline] |
Create a Quantifier.
Definition at line 2136 of file Context.java.
RatNum mkReal | ( | int | num, |
int | den | ||
) | throws Z3Exception [inline] |
Create a real from a fraction.
num | numerator of rational. |
den | denominator of rational. |
Definition at line 1940 of file Context.java.
{ if (den == 0) throw new Z3Exception("Denominator is zero"); return new RatNum(this, Native.mkReal(nCtx(), num, den)); }
RatNum mkReal | ( | String | v | ) | throws Z3Exception [inline] |
Create a real numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1954 of file Context.java.
{ return new RatNum(this, Native.mkNumeral(nCtx(), v, getRealSort() .getNativeObject())); }
RatNum mkReal | ( | int | v | ) | throws Z3Exception [inline] |
Create a real numeral.
v | value of the numeral. |
Definition at line 1966 of file Context.java.
{ return new RatNum(this, Native.mkInt(nCtx(), v, getRealSort() .getNativeObject())); }
RatNum mkReal | ( | long | v | ) | throws Z3Exception [inline] |
Create a real numeral.
v | value of the numeral. |
Definition at line 1978 of file Context.java.
{ return new RatNum(this, Native.mkInt64(nCtx(), v, getRealSort() .getNativeObject())); }
IntExpr mkReal2Int | ( | RealExpr | t | ) | throws Z3Exception [inline] |
Coerce a real to an integer. The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.
Definition at line 926 of file Context.java.
{ checkContextMatch(t); return new IntExpr(this, Native.mkReal2int(nCtx(), t.getNativeObject())); }
RealExpr mkRealConst | ( | Symbol | name | ) | throws Z3Exception [inline] |
Creates a real constant.
Definition at line 588 of file Context.java.
{ return (RealExpr) mkConst(name, getRealSort()); }
RealExpr mkRealConst | ( | String | name | ) | throws Z3Exception [inline] |
Creates a real constant.
Definition at line 597 of file Context.java.
{ return (RealExpr) mkConst(name, getRealSort()); }
RealSort mkRealSort | ( | ) | throws Z3Exception [inline] |
IntExpr mkRem | ( | IntExpr | t1, |
IntExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 rem t2
. The arguments must have int type.
Definition at line 833 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new IntExpr(this, Native.mkRem(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkRepeat | ( | int | i, |
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Bit-vector repetition. The argument t must have a bit-vector sort.
Definition at line 1359 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkRepeat(nCtx(), i, t.getNativeObject())); }
Expr mkSelect | ( | ArrayExpr | a, |
Expr | i | ||
) | throws Z3Exception [inline] |
Array read. The argument a
is the array and i
is the index of the array that gets read.
The node a
must have an array sort [domain -> range]
, and i
must have the sort domain
. The sort of the result is range
.
Definition at line 1659 of file Context.java.
{ checkContextMatch(a); checkContextMatch(i); return Expr.create( this, Native.mkSelect(nCtx(), a.getNativeObject(), i.getNativeObject())); }
Expr mkSetAdd | ( | Expr | set, |
Expr | element | ||
) | throws Z3Exception [inline] |
Add an element to the set.
Definition at line 1775 of file Context.java.
{ checkContextMatch(set); checkContextMatch(element); return Expr.create( this, Native.mkSetAdd(nCtx(), set.getNativeObject(), element.getNativeObject())); }
Expr mkSetComplement | ( | Expr | arg | ) | throws Z3Exception [inline] |
Take the complement of a set.
Definition at line 1843 of file Context.java.
{ checkContextMatch(arg); return Expr.create(this, Native.mkSetComplement(nCtx(), arg.getNativeObject())); }
Expr mkSetDel | ( | Expr | set, |
Expr | element | ||
) | throws Z3Exception [inline] |
Remove an element from a set.
Definition at line 1789 of file Context.java.
{ checkContextMatch(set); checkContextMatch(element); return Expr.create( this, Native.mkSetDel(nCtx(), set.getNativeObject(), element.getNativeObject())); }
Expr mkSetDifference | ( | Expr | arg1, |
Expr | arg2 | ||
) | throws Z3Exception [inline] |
Take the difference between two sets.
Definition at line 1829 of file Context.java.
{ checkContextMatch(arg1); checkContextMatch(arg2); return Expr.create( this, Native.mkSetDifference(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); }
Expr mkSetIntersection | ( | Expr... | args | ) | throws Z3Exception [inline] |
Take the intersection of a list of sets.
Definition at line 1816 of file Context.java.
{ checkContextMatch(args); return Expr.create( this, Native.mkSetIntersect(nCtx(), (int) args.length, AST.arrayToNative(args))); }
Expr mkSetMembership | ( | Expr | elem, |
Expr | set | ||
) | throws Z3Exception [inline] |
Check for set membership.
Definition at line 1854 of file Context.java.
{ checkContextMatch(elem); checkContextMatch(set); return Expr.create( this, Native.mkSetMember(nCtx(), elem.getNativeObject(), set.getNativeObject())); }
SetSort mkSetSort | ( | Sort | ty | ) | throws Z3Exception [inline] |
Create a set type.
Definition at line 1743 of file Context.java.
{ checkContextMatch(ty); return new SetSort(this, ty); }
Expr mkSetSubset | ( | Expr | arg1, |
Expr | arg2 | ||
) | throws Z3Exception [inline] |
Check for subsetness of sets.
Definition at line 1868 of file Context.java.
{ checkContextMatch(arg1); checkContextMatch(arg2); return Expr.create( this, Native.mkSetSubset(nCtx(), arg1.getNativeObject(), arg2.getNativeObject())); }
Expr mkSetUnion | ( | Expr... | args | ) | throws Z3Exception [inline] |
Take the union of a list of sets.
Definition at line 1803 of file Context.java.
{ checkContextMatch(args); return Expr.create( this, Native.mkSetUnion(nCtx(), (int) args.length, AST.arrayToNative(args))); }
BitVecExpr mkSignExt | ( | int | i, |
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Bit-vector sign extension. Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i
, where m
is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1333 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkSignExt(nCtx(), i, t.getNativeObject())); }
Solver mkSimpleSolver | ( | ) | throws Z3Exception [inline] |
Creates a new (incremental) solver.
Definition at line 2828 of file Context.java.
{ return new Solver(this, Native.mkSimpleSolver(nCtx())); }
Solver mkSolver | ( | ) | throws Z3Exception [inline] |
Creates a new (incremental) solver. This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2795 of file Context.java.
Referenced by Tactic.getSolver(), and Context.mkSolver().
{ return mkSolver((Symbol) null); }
Solver mkSolver | ( | Symbol | logic | ) | throws Z3Exception [inline] |
Creates a new (incremental) solver. This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2806 of file Context.java.
Solver mkSolver | ( | String | logic | ) | throws Z3Exception [inline] |
Creates a new (incremental) solver.
Definition at line 2819 of file Context.java.
Solver mkSolver | ( | Tactic | t | ) | throws Z3Exception [inline] |
Creates a solver that is implemented using the given tactic. The solver supports the commands Push
and Pop
, but it will always solve each check from scratch.
Definition at line 2839 of file Context.java.
{ return new Solver(this, Native.mkSolverFromTactic(nCtx(), t.getNativeObject())); }
Array update. The node a
must have an array sort [domain -> range]
, i
must have sort domain
, v
must have sort range. The sort of the result is [domain -> range]
. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to a
(with respect to select
) on all indices except for i
, where it maps to v
(and the select
of a
with respect to i
may be a different value).
Definition at line 1683 of file Context.java.
{ checkContextMatch(a); checkContextMatch(i); checkContextMatch(v); return new ArrayExpr(this, Native.mkStore(nCtx(), a.getNativeObject(), i.getNativeObject(), v.getNativeObject())); }
ArithExpr mkSub | ( | ArithExpr... | t | ) | throws Z3Exception [inline] |
Create an expression representing t[0] - t[1] - ...
.
Definition at line 785 of file Context.java.
{ checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t))); }
IntSymbol mkSymbol | ( | int | i | ) | throws Z3Exception [inline] |
Creates a new symbol using an integer. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.
Definition at line 73 of file Context.java.
Referenced by Params.add(), Context.mkArrayConst(), Context.mkBoolConst(), Context.mkConst(), Context.mkConstDecl(), Context.mkConstructor(), Context.mkDatatypeSort(), Context.mkEnumSort(), Context.mkFiniteDomainSort(), Context.mkFuncDecl(), Context.mkListSort(), Context.mkSolver(), Context.MkSymbols(), and Context.mkUninterpretedSort().
{ return new IntSymbol(this, i); }
StringSymbol mkSymbol | ( | String | name | ) | throws Z3Exception [inline] |
Create a symbol using a string.
Definition at line 81 of file Context.java.
{ return new StringSymbol(this, name); }
Symbol [] MkSymbols | ( | String[] | names | ) | throws Z3Exception [inline, package] |
Create an array of symbols.
Definition at line 89 of file Context.java.
Referenced by Context.mkConstructor(), Context.mkDatatypeSorts(), and Context.mkEnumSort().
{ if (names == null) return null; Symbol[] result = new Symbol[names.length]; for (int i = 0; i < names.length; ++i) result[i] = mkSymbol(names[i]); return result; }
Tactic mkTactic | ( | String | name | ) | throws Z3Exception [inline] |
Creates a new Tactic.
Definition at line 2430 of file Context.java.
Referenced by Goal.simplify().
{ return new Tactic(this, name); }
Expr mkTermArray | ( | ArrayExpr | array | ) | throws Z3Exception [inline] |
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Definition at line 1732 of file Context.java.
{ checkContextMatch(array); return Expr.create(this, Native.mkArrayDefault(nCtx(), array.getNativeObject())); }
BoolExpr mkTrue | ( | ) | throws Z3Exception [inline] |
TupleSort mkTupleSort | ( | Symbol | name, |
Symbol[] | fieldNames, | ||
Sort[] | fieldSorts | ||
) | throws Z3Exception [inline] |
Create a new tuple sort.
Definition at line 202 of file Context.java.
{ checkContextMatch(name); checkContextMatch(fieldNames); checkContextMatch(fieldSorts); return new TupleSort(this, name, (int) fieldNames.length, fieldNames, fieldSorts); }
ArithExpr mkUnaryMinus | ( | ArithExpr | t | ) | throws Z3Exception [inline] |
Create an expression representing -t
.
Definition at line 796 of file Context.java.
{ checkContextMatch(t); return (ArithExpr) Expr.create(this, Native.mkUnaryMinus(nCtx(), t.getNativeObject())); }
UninterpretedSort mkUninterpretedSort | ( | Symbol | s | ) | throws Z3Exception [inline] |
Create a new uninterpreted sort.
Definition at line 145 of file Context.java.
Referenced by Context.mkUninterpretedSort().
{ checkContextMatch(s); return new UninterpretedSort(this, s); }
UninterpretedSort mkUninterpretedSort | ( | String | str | ) | throws Z3Exception [inline] |
Create a new uninterpreted sort.
Definition at line 155 of file Context.java.
{ return mkUninterpretedSort(mkSymbol(str)); }
BoolExpr mkXor | ( | BoolExpr | t1, |
BoolExpr | t2 | ||
) | throws Z3Exception [inline] |
Create an expression representing t1 xor t2
.
Definition at line 729 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new BoolExpr(this, Native.mkXor(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
BitVecExpr mkZeroExt | ( | int | i, |
BitVecExpr | t | ||
) | throws Z3Exception [inline] |
Bit-vector zero extension. Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i
, where m
is the size of the given bit-vector. The argument t must have a bit-vector sort.
Definition at line 1347 of file Context.java.
{ checkContextMatch(t); return new BitVecExpr(this, Native.mkZeroExt(nCtx(), i, t.getNativeObject())); }
ModelDecRefQueue model_DRQ | ( | ) | [inline, package] |
Definition at line 3002 of file Context.java.
Referenced by Model.decRef(), and Model.incRef().
{
return m_Model_DRQ;
}
long nCtx | ( | ) | [inline, package] |
Definition at line 2927 of file Context.java.
Referenced by Context.and(), Context.andThen(), Context.benchmarkToSMTString(), InterpolationContext.CheckInterpolant(), InterpolationContext.ComputeInterpolant(), Context.cond(), Context.constProbe(), ASTVectorDecRefQueue.decRef(), ASTDecRefQueue.decRef(), FixedpointDecRefQueue.decRef(), FuncInterpDecRefQueue.decRef(), FuncInterpEntryDecRefQueue.decRef(), GoalDecRefQueue.decRef(), ModelDecRefQueue.decRef(), ParamDescrsDecRefQueue.decRef(), ParamsDecRefQueue.decRef(), ProbeDecRefQueue.decRef(), SolverDecRefQueue.decRef(), StatisticsDecRefQueue.decRef(), TacticDecRefQueue.decRef(), ASTMapDecRefQueue.decRef(), ApplyResultDecRefQueue.decRef(), Context.eq(), Context.fail(), Context.failIf(), Context.failIfNotDecided(), Context.ge(), InterpolationContext.GetInterpolant(), Context.getNumProbes(), Context.getNumSMTLIBAssumptions(), Context.getNumSMTLIBDecls(), Context.getNumSMTLIBFormulas(), Context.getNumSMTLIBSorts(), Context.getNumTactics(), Context.getProbeDescription(), Context.getProbeNames(), Context.getSimplifyParameterDescriptions(), Context.getSMTLIBAssumptions(), Context.getSMTLIBDecls(), Context.getSMTLIBFormulas(), Context.getSMTLIBSorts(), Context.getTacticDescription(), Context.getTacticNames(), Context.gt(), ApplyResultDecRefQueue.incRef(), FixedpointDecRefQueue.incRef(), FuncInterpDecRefQueue.incRef(), FuncInterpEntryDecRefQueue.incRef(), GoalDecRefQueue.incRef(), ASTMapDecRefQueue.incRef(), ModelDecRefQueue.incRef(), ParamDescrsDecRefQueue.incRef(), ParamsDecRefQueue.incRef(), ProbeDecRefQueue.incRef(), SolverDecRefQueue.incRef(), StatisticsDecRefQueue.incRef(), TacticDecRefQueue.incRef(), ASTDecRefQueue.incRef(), ASTVectorDecRefQueue.incRef(), Context.initContext(), InterpolationContext.InterpolationProfile(), Context.interrupt(), Context.le(), Context.lt(), Context.mkAdd(), Context.mkAnd(), Context.mkBitVecSort(), Context.mkBound(), Context.mkBV2Int(), Context.mkBVAdd(), Context.mkBVAddNoOverflow(), Context.mkBVAddNoUnderflow(), Context.mkBVAND(), Context.mkBVASHR(), Context.mkBVLSHR(), Context.mkBVMul(), Context.mkBVMulNoOverflow(), Context.mkBVMulNoUnderflow(), Context.mkBVNAND(), Context.mkBVNeg(), Context.mkBVNegNoOverflow(), Context.mkBVNOR(), Context.mkBVNot(), Context.mkBVOR(), Context.mkBVRedAND(), Context.mkBVRedOR(), Context.mkBVRotateLeft(), Context.mkBVRotateRight(), Context.mkBVSDiv(), Context.mkBVSDivNoOverflow(), Context.mkBVSGE(), Context.mkBVSGT(), Context.mkBVSHL(), Context.mkBVSLE(), Context.mkBVSLT(), Context.mkBVSMod(), Context.mkBVSRem(), Context.mkBVSub(), Context.mkBVSubNoOverflow(), Context.mkBVSubNoUnderflow(), Context.mkBVUDiv(), Context.mkBVUGE(), Context.mkBVUGT(), Context.mkBVULE(), Context.mkBVULT(), Context.mkBVURem(), Context.mkBVXNOR(), Context.mkBVXOR(), Context.mkConcat(), Context.mkConst(), Context.mkConstArray(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkDiv(), Context.mkEmptySet(), Context.mkEq(), Context.mkExtract(), Context.mkFalse(), Context.mkFreshConst(), Context.mkFullSet(), Context.mkGe(), Context.mkGt(), Context.mkIff(), Context.mkImplies(), Context.mkInt(), Context.mkInt2BV(), Context.mkInt2Real(), InterpolationContext.MkInterpolant(), Context.mkIsInteger(), Context.mkITE(), Context.mkLe(), Context.mkLt(), Context.mkMap(), Context.mkMod(), Context.mkMul(), Context.mkNot(), Context.mkNumeral(), Context.mkOr(), Context.mkPattern(), Context.mkPower(), Context.mkReal(), Context.mkReal2Int(), Context.mkRem(), Context.mkRepeat(), Context.mkSelect(), Context.mkSetAdd(), Context.mkSetComplement(), Context.mkSetDel(), Context.mkSetDifference(), Context.mkSetIntersection(), Context.mkSetMembership(), Context.mkSetSubset(), Context.mkSetUnion(), Context.mkSignExt(), Context.mkSimpleSolver(), Context.mkSolver(), Context.mkStore(), Context.mkSub(), Context.mkTermArray(), Context.mkTrue(), Context.mkUnaryMinus(), Context.mkXor(), Context.mkZeroExt(), Context.not(), Context.or(), Context.orElse(), Context.parAndThen(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Context.parseSMTLIBFile(), Context.parseSMTLIBString(), InterpolationContext.ReadInterpolationProblem(), Context.repeat(), Context.setPrintMode(), Context.SimplifyHelp(), Context.skip(), Context.tryFor(), Context.updateParamValue(), Context.usingParams(), Context.when(), and InterpolationContext.WriteInterpolationProblem().
{ return m_ctx; }
Probe not | ( | Probe | p | ) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value p does not evaluate to "true".
Definition at line 2782 of file Context.java.
{ checkContextMatch(p); return new Probe(this, Native.probeNot(nCtx(), p.getNativeObject())); }
Probe or | ( | Probe | p1, |
Probe | p2 | ||
) | throws Z3Exception [inline] |
Create a probe that evaluates to "true" when the value p1 or p2 evaluate to "true".
Definition at line 2770 of file Context.java.
{ checkContextMatch(p1); checkContextMatch(p2); return new Probe(this, Native.probeOr(nCtx(), p1.getNativeObject(), p2.getNativeObject())); }
Tactic orElse | ( | Tactic | t1, |
Tactic | t2 | ||
) | throws Z3Exception [inline] |
Create a tactic that first applies t1 to a Goal and if it fails then returns the result of t2 applied to the Goal.
Definition at line 2480 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new Tactic(this, Native.tacticOrElse(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
ParamDescrsDecRefQueue paramDescrs_DRQ | ( | ) | [inline, package] |
Definition at line 3012 of file Context.java.
Referenced by ParamDescrs.decRef(), and ParamDescrs.incRef().
{
return m_ParamDescrs_DRQ;
}
ParamsDecRefQueue params_DRQ | ( | ) | [inline, package] |
Definition at line 3007 of file Context.java.
Referenced by Params.decRef(), and Params.incRef().
{
return m_Params_DRQ;
}
Tactic parAndThen | ( | Tactic | t1, |
Tactic | t2 | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1 . The subgoals are processed in parallel.
Definition at line 2622 of file Context.java.
{ checkContextMatch(t1); checkContextMatch(t2); return new Tactic(this, Native.tacticParAndThen(nCtx(), t1.getNativeObject(), t2.getNativeObject())); }
Tactic parOr | ( | Tactic... | t | ) | throws Z3Exception [inline] |
Create a tactic that applies the given tactics in parallel.
Definition at line 2610 of file Context.java.
{ checkContextMatch(t); return new Tactic(this, Native.tacticParOr(nCtx(), Tactic.arrayLength(t), Tactic.arrayToNative(t))); }
BoolExpr parseSMTLIB2File | ( | String | fileName, |
Symbol[] | sortNames, | ||
Sort[] | sorts, | ||
Symbol[] | declNames, | ||
FuncDecl[] | decls | ||
) | throws Z3Exception [inline] |
Parse the given file using the SMT-LIB2 parser.
Definition at line 2353 of file Context.java.
{ int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(), fileName, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls))); }
BoolExpr parseSMTLIB2String | ( | String | str, |
Symbol[] | sortNames, | ||
Sort[] | sorts, | ||
Symbol[] | declNames, | ||
FuncDecl[] | decls | ||
) | throws Z3Exception [inline] |
Parse the given string using the SMT-LIB2 parser.
Definition at line 2332 of file Context.java.
{ int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(), str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls))); }
void parseSMTLIBFile | ( | String | fileName, |
Symbol[] | sortNames, | ||
Sort[] | sorts, | ||
Symbol[] | declNames, | ||
FuncDecl[] | decls | ||
) | throws Z3Exception [inline] |
Parse the given file using the SMT-LIB parser.
Definition at line 2215 of file Context.java.
{ int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); Native.parseSmtlibFile(nCtx(), fileName, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls)); }
void parseSMTLIBString | ( | String | str, |
Symbol[] | sortNames, | ||
Sort[] | sorts, | ||
Symbol[] | declNames, | ||
FuncDecl[] | decls | ||
) | throws Z3Exception [inline] |
Parse the given string using the SMT-LIB parser. The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays sortNames and declNames don't need to match the names of the sorts and declarations in the arrays sorts and decls . This is a useful feature since we can use arbitrary names to reference sorts and declarations.
Definition at line 2196 of file Context.java.
{ int csn = Symbol.arrayLength(sortNames); int cs = Sort.arrayLength(sorts); int cdn = Symbol.arrayLength(declNames); int cd = AST.arrayLength(decls); if (csn != cs || cdn != cd) throw new Z3Exception("Argument size mismatch"); Native.parseSmtlibString(nCtx(), str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts), AST.arrayLength(decls), Symbol.arrayToNative(declNames), AST.arrayToNative(decls)); }
ProbeDecRefQueue probe_DRQ | ( | ) | [inline, package] |
Definition at line 3017 of file Context.java.
Referenced by Probe.decRef(), and Probe.incRef().
{
return m_Probe_DRQ;
}
Tactic repeat | ( | Tactic | t, |
int | max | ||
) | throws Z3Exception [inline] |
Create a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
Definition at line 2538 of file Context.java.
{ checkContextMatch(t); return new Tactic(this, Native.tacticRepeat(nCtx(), t.getNativeObject(), max)); }
void setPrintMode | ( | Z3_ast_print_mode | value | ) | throws Z3Exception [inline] |
Selects the format used for pretty-printing expressions. The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
Definition at line 2160 of file Context.java.
Referenced by Context.initContext().
{ Native.setAstPrintMode(nCtx(), value.toInt()); }
String SimplifyHelp | ( | ) | throws Z3Exception [inline] |
Return a string describing all available parameters to Expr.Simplify
.
Definition at line 2888 of file Context.java.
{ return Native.simplifyGetHelp(nCtx()); }
Tactic skip | ( | ) | throws Z3Exception [inline] |
Create a tactic that just returns the given goal.
Definition at line 2549 of file Context.java.
{ return new Tactic(this, Native.tacticSkip(nCtx())); }
SolverDecRefQueue solver_DRQ | ( | ) | [inline, package] |
Definition at line 3022 of file Context.java.
Referenced by Solver.decRef(), and Solver.incRef().
{
return m_Solver_DRQ;
}
StatisticsDecRefQueue statistics_DRQ | ( | ) | [inline, package] |
Definition at line 3027 of file Context.java.
Referenced by Statistics.decRef(), and Statistics.incRef().
{
return m_Statistics_DRQ;
}
TacticDecRefQueue tactic_DRQ | ( | ) | [inline, package] |
Definition at line 3032 of file Context.java.
Referenced by Tactic.decRef(), and Tactic.incRef().
{
return m_Tactic_DRQ;
}
Tactic then | ( | Tactic | t1, |
Tactic | t2, | ||
Tactic... | ts | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t1 to a Goal and then t2 to every subgoal produced by t1 . Shorthand for AndThen
.
Definition at line 2470 of file Context.java.
{ return andThen(t1, t2, ts); }
static void ToggleWarningMessages | ( | boolean | enabled | ) | throws Z3Exception [inline, static] |
Enable/disable printing of warning messages to the console. Note that this function is static and effects the behaviour of all contexts globally.
Definition at line 2907 of file Context.java.
{ Native.toggleWarningMessages((enabled) ? true : false); }
Tactic tryFor | ( | Tactic | t, |
int | ms | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t to a goal for ms milliseconds. If t does not terminate within ms milliseconds, then it fails.
Definition at line 2495 of file Context.java.
{ checkContextMatch(t); return new Tactic(this, Native.tacticTryFor(nCtx(), t.getNativeObject(), ms)); }
Unwraps an AST. This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,
).
a | The AST to unwrap. |
Definition at line 2879 of file Context.java.
{
return a.getNativeObject();
}
void updateParamValue | ( | String | id, |
String | value | ||
) | throws Z3Exception [inline] |
Update a mutable configuration parameter. The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -ini?
Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.
Definition at line 2920 of file Context.java.
{ Native.updateParamValue(nCtx(), id, value); }
Tactic usingParams | ( | Tactic | t, |
Params | p | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t using the given set of parameters p .
Definition at line 2589 of file Context.java.
Referenced by Context.with().
{ checkContextMatch(t); checkContextMatch(p); return new Tactic(this, Native.tacticUsingParams(nCtx(), t.getNativeObject(), p.getNativeObject())); }
Tactic when | ( | Probe | p, |
Tactic | t | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t to a given goal if the probe p evaluates to true. If p evaluates to false, then the new tactic behaves like the skip
tactic.
Definition at line 2509 of file Context.java.
{ checkContextMatch(t); checkContextMatch(p); return new Tactic(this, Native.tacticWhen(nCtx(), p.getNativeObject(), t.getNativeObject())); }
Tactic with | ( | Tactic | t, |
Params | p | ||
) | throws Z3Exception [inline] |
Create a tactic that applies t using the given set of parameters p . Alias for UsingParams
Definition at line 2602 of file Context.java.
{ return usingParams(t, p); }
AST wrapAST | ( | long | nativeObject | ) | throws Z3Exception [inline] |
Wraps an AST. This function is used for transitions between native and managed objects. Note that nativeObject must be a native object obtained from Z3 (e.g., through
) and that it must have a correct reference count (see e.g., .
nativeObject | The native pointer to wrap. |
Definition at line 2864 of file Context.java.
{ return AST.create(this, nativeObject); }
long m_ctx = 0 [package] |
Definition at line 2925 of file Context.java.
Referenced by Context.Context(), Context.finalize(), InterpolationContext.InterpolationContext(), and Context.nCtx().
long m_refCount = 0 [protected] |
Definition at line 3042 of file Context.java.
Referenced by Z3Object.dispose(), Context.finalize(), and Z3Object.Z3Object().