Public Member Functions | |
void | dispose () throws Z3Exception |
Protected Member Functions | |
void | finalize () throws Z3Exception |
Package Functions | |
Z3Object (Context ctx) | |
Z3Object (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
void | checkNativeObject (long obj) throws Z3Exception |
long | getNativeObject () |
void | setNativeObject (long value) throws Z3Exception |
Context | getContext () |
Static Package Functions | |
static long | getNativeObject (Z3Object s) |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition at line 24 of file Z3Object.java.
Definition at line 55 of file Z3Object.java.
{ ctx.m_refCount++; m_ctx = ctx; }
Z3Object | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 61 of file Z3Object.java.
{ ctx.m_refCount++; m_ctx = ctx; incRef(obj); m_n_obj = obj; }
static int arrayLength | ( | Z3Object[] | a | ) | [inline, static, package] |
Definition at line 122 of file Z3Object.java.
Referenced by Constructor.Constructor(), Expr.create(), FuncDecl.FuncDecl(), Context.mkMap(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Context.parseSMTLIBFile(), Context.parseSMTLIBString(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), and Fixedpoint.toString().
{
return (a == null) ? 0 : a.length;
}
static long [] arrayToNative | ( | Z3Object[] | a | ) | [inline, static, package] |
Definition at line 112 of file Z3Object.java.
Referenced by Context.benchmarkToSMTString(), Solver.check(), InterpolationContext.CheckInterpolant(), Constructor.Constructor(), ConstructorList.ConstructorList(), Expr.create(), DatatypeSort.DatatypeSort(), EnumSort.EnumSort(), FuncDecl.FuncDecl(), Context.mkAdd(), Context.mkAnd(), Context.mkDatatypeSorts(), Context.mkDistinct(), Context.mkMap(), Context.mkMul(), Context.mkOr(), Context.mkPattern(), Context.mkSetIntersection(), Context.mkSetUnion(), Context.mkSub(), Context.parOr(), Context.parseSMTLIB2File(), Context.parseSMTLIB2String(), Context.parseSMTLIBFile(), Context.parseSMTLIBString(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.setPredicateRepresentation(), Expr.substitute(), Expr.substituteVars(), Fixedpoint.toString(), TupleSort.TupleSort(), Expr.update(), and InterpolationContext.WriteInterpolationProblem().
{ if (a == null) return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) an[i] = (a[i] == null) ? 0 : a[i].getNativeObject(); return an; }
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented in Expr, FuncDecl, Quantifier, Sort, IntSymbol, and StringSymbol.
Definition at line 77 of file Z3Object.java.
Referenced by Z3Object.setNativeObject().
{ }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented in Fixedpoint, Solver, Model, Goal, AST, Statistics, FuncInterp, Params, ASTMap, ASTVector, Tactic, FuncInterp.Entry, ParamDescrs, ApplyResult, and Probe.
Definition at line 73 of file Z3Object.java.
Referenced by Z3Object.dispose(), and Z3Object.setNativeObject().
{ }
void dispose | ( | ) | throws Z3Exception [inline] |
Disposes of the underlying native Z3 object.
Reimplemented from IDisposable.
Definition at line 37 of file Z3Object.java.
Referenced by Z3Object.finalize().
{ if (m_n_obj != 0) { decRef(m_n_obj); m_n_obj = 0; } if (m_ctx != null) { m_ctx.m_refCount--; m_ctx = null; } }
void finalize | ( | ) | throws Z3Exception [inline, protected] |
Finalizer.
Reimplemented in Constructor, and ConstructorList.
Definition at line 29 of file Z3Object.java.
{ dispose(); }
Context getContext | ( | ) | [inline, package] |
Definition at line 107 of file Z3Object.java.
Referenced by Params.add(), Fixedpoint.add(), Goal.add(), Solver.add(), Fixedpoint.addCover(), Fixedpoint.addFact(), Fixedpoint.addRule(), Probe.apply(), Tactic.apply(), FuncDecl.apply(), Solver.assertAndTrack(), Solver.check(), StringSymbol.checkNativeObject(), IntSymbol.checkNativeObject(), Sort.checkNativeObject(), Quantifier.checkNativeObject(), FuncDecl.checkNativeObject(), Expr.checkNativeObject(), Constructor.ConstructorDecl(), ConstructorList.ConstructorList(), ASTMap.contains(), ApplyResult.convertModel(), Probe.decRef(), ApplyResult.decRef(), ParamDescrs.decRef(), FuncInterp.Entry.decRef(), Tactic.decRef(), ASTVector.decRef(), ASTMap.decRef(), Params.decRef(), FuncInterp.decRef(), Statistics.decRef(), AST.decRef(), Goal.decRef(), Model.decRef(), Solver.decRef(), Fixedpoint.decRef(), ASTMap.erase(), Model.eval(), ConstructorList.finalize(), Constructor.finalize(), ASTMap.find(), ASTVector.get(), Constructor.getAccessorDecls(), DatatypeSort.getAccessors(), Fixedpoint.getAnswer(), FuncInterp.Entry.getArgs(), Expr.getArgs(), RelationSort.getArity(), FuncDecl.getArity(), FuncInterp.getArity(), Solver.getAssertions(), Fixedpoint.getAssertions(), AST.getASTKind(), Quantifier.getBody(), Expr.getBoolValue(), Quantifier.getBoundVariableNames(), Quantifier.getBoundVariableSorts(), RelationSort.getColumnSorts(), ListSort.getConsDecl(), EnumSort.getConstDecls(), Model.getConstDecls(), Model.getConstInterp(), DatatypeSort.getConstructors(), EnumSort.getConsts(), Fixedpoint.getCoverDelta(), FuncDecl.getDeclKind(), Model.getDecls(), RatNum.getDenominator(), Goal.getDepth(), ArraySort.getDomain(), FuncDecl.getDomain(), FuncDecl.getDomainSize(), FuncInterp.getElse(), FuncInterp.getEntries(), Statistics.getEntries(), TupleSort.getFieldDecls(), Goal.getFormulas(), Expr.getFuncDecl(), Model.getFuncDecls(), Model.getFuncInterp(), ListSort.getHeadDecl(), Solver.getHelp(), Fixedpoint.getHelp(), Tactic.getHelp(), Sort.getId(), FuncDecl.getId(), AST.getId(), Expr.getIndex(), IntSymbol.getInt(), BitVecNum.getInt(), IntNum.getInt(), IntNum.getInt64(), ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), ASTMap.getKeys(), Statistics.getKeys(), Symbol.getKind(), ParamDescrs.getKind(), BitVecNum.getLong(), Solver.getModel(), Sort.getName(), FuncDecl.getName(), ParamDescrs.getNames(), ListSort.getNil(), ListSort.getNilDecl(), Quantifier.getNoPatterns(), FuncInterp.Entry.getNumArgs(), Expr.getNumArgs(), Solver.getNumAssertions(), Quantifier.getNumBound(), DatatypeSort.getNumConstructors(), Model.getNumConsts(), FuncInterp.getNumEntries(), RatNum.getNumerator(), Goal.getNumExprs(), TupleSort.getNumFields(), Model.getNumFuncs(), Fixedpoint.getNumLevels(), Quantifier.getNumNoPatterns(), FuncDecl.getNumParameters(), Quantifier.getNumPatterns(), Solver.getNumScopes(), Model.getNumSorts(), ApplyResult.getNumSubgoals(), Pattern.getNumTerms(), Tactic.getParameterDescriptions(), Solver.getParameterDescriptions(), Fixedpoint.getParameterDescriptions(), FuncDecl.getParameters(), Quantifier.getPatterns(), Goal.getPrecision(), Solver.getProof(), ArraySort.getRange(), FuncDecl.getRange(), Fixedpoint.getReasonUnknown(), Solver.getReasonUnknown(), DatatypeSort.getRecognizers(), Fixedpoint.getRules(), AST.getSExpr(), BitVecSort.getSize(), FiniteDomainSort.getSize(), Tactic.getSolver(), Expr.getSort(), Sort.getSortKind(), Model.getSorts(), Model.getSortUniverse(), Solver.getStatistics(), StringSymbol.getString(), ApplyResult.getSubgoals(), ListSort.getTailDecl(), Pattern.getTerms(), Constructor.getTesterDecl(), EnumSort.getTesterDecls(), Solver.getUnsatCore(), FuncInterp.Entry.getValue(), Quantifier.getWeight(), AST.hashCode(), Goal.inconsistent(), Probe.incRef(), ApplyResult.incRef(), FuncInterp.Entry.incRef(), ParamDescrs.incRef(), Tactic.incRef(), ASTVector.incRef(), ASTMap.incRef(), Params.incRef(), FuncInterp.incRef(), Statistics.incRef(), AST.incRef(), Goal.incRef(), Model.incRef(), Solver.incRef(), Fixedpoint.incRef(), ASTMap.insert(), Expr.isAlgebraicNumber(), Expr.isArray(), Expr.isBool(), Expr.isBV(), Goal.isDecidedSat(), Goal.isDecidedUnsat(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isNumeral(), Expr.isReal(), Expr.isRelation(), Quantifier.isUniversal(), Expr.isWellSorted(), TupleSort.mkDecl(), Solver.pop(), Fixedpoint.pop(), ASTVector.push(), Solver.push(), Fixedpoint.push(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.registerRelation(), ASTMap.reset(), Solver.reset(), Goal.reset(), ASTVector.resize(), ASTVector.set(), Solver.setParameters(), Fixedpoint.setParameters(), Fixedpoint.setPredicateRepresentation(), Expr.simplify(), Goal.simplify(), ASTVector.size(), ParamDescrs.size(), ASTMap.size(), Goal.size(), Statistics.size(), Expr.substitute(), Expr.substituteVars(), AlgebraicNum.toDecimal(), RatNum.toDecimalString(), AlgebraicNum.toLower(), Pattern.toString(), BitVecNum.toString(), ApplyResult.toString(), IntNum.toString(), FuncDecl.toString(), ParamDescrs.toString(), RatNum.toString(), Sort.toString(), ASTVector.toString(), ASTMap.toString(), Params.toString(), Statistics.toString(), AST.toString(), Goal.toString(), Fixedpoint.toString(), Model.toString(), Solver.toString(), AlgebraicNum.toUpper(), ASTVector.translate(), AST.translate(), Expr.translate(), Goal.translate(), Expr.update(), Fixedpoint.updateRule(), and ParamDescrs.validate().
{
return m_ctx;
}
long getNativeObject | ( | ) | [inline, package] |
Definition at line 81 of file Z3Object.java.
Referenced by Params.add(), Fixedpoint.add(), Goal.add(), Solver.add(), Fixedpoint.addCover(), Fixedpoint.addFact(), Fixedpoint.addRule(), Context.andThen(), Probe.apply(), Tactic.apply(), Z3Object.arrayToNative(), Solver.assertAndTrack(), Solver.check(), Constructor.ConstructorDecl(), ASTMap.contains(), ApplyResult.convertModel(), AST.equals(), Sort.equals(), ASTMap.erase(), Model.eval(), ConstructorList.finalize(), Constructor.finalize(), ASTMap.find(), ASTVector.get(), Constructor.getAccessorDecls(), DatatypeSort.getAccessors(), Fixedpoint.getAnswer(), FuncInterp.Entry.getArgs(), Expr.getArgs(), RelationSort.getArity(), FuncDecl.getArity(), FuncInterp.getArity(), Solver.getAssertions(), Fixedpoint.getAssertions(), AST.getASTKind(), Quantifier.getBody(), Expr.getBoolValue(), Quantifier.getBoundVariableNames(), Quantifier.getBoundVariableSorts(), RelationSort.getColumnSorts(), ListSort.getConsDecl(), EnumSort.getConstDecls(), Model.getConstDecls(), Model.getConstInterp(), DatatypeSort.getConstructors(), Fixedpoint.getCoverDelta(), FuncDecl.getDeclKind(), Model.getDecls(), RatNum.getDenominator(), Goal.getDepth(), ArraySort.getDomain(), FuncDecl.getDomain(), FuncDecl.getDomainSize(), FuncInterp.getElse(), FuncInterp.getEntries(), Statistics.getEntries(), TupleSort.getFieldDecls(), Goal.getFormulas(), Expr.getFuncDecl(), Model.getFuncDecls(), Model.getFuncInterp(), ListSort.getHeadDecl(), Solver.getHelp(), Fixedpoint.getHelp(), Tactic.getHelp(), Sort.getId(), FuncDecl.getId(), AST.getId(), Expr.getIndex(), IntSymbol.getInt(), BitVecNum.getInt(), IntNum.getInt(), IntNum.getInt64(), InterpolationContext.GetInterpolant(), ListSort.getIsConsDecl(), ListSort.getIsNilDecl(), ASTMap.getKeys(), Statistics.getKeys(), Symbol.getKind(), ParamDescrs.getKind(), BitVecNum.getLong(), Solver.getModel(), Sort.getName(), FuncDecl.getName(), ParamDescrs.getNames(), Z3Object.getNativeObject(), ListSort.getNilDecl(), Quantifier.getNoPatterns(), FuncInterp.Entry.getNumArgs(), Expr.getNumArgs(), Solver.getNumAssertions(), Quantifier.getNumBound(), DatatypeSort.getNumConstructors(), Model.getNumConsts(), FuncInterp.getNumEntries(), RatNum.getNumerator(), Goal.getNumExprs(), TupleSort.getNumFields(), Model.getNumFuncs(), Fixedpoint.getNumLevels(), Quantifier.getNumNoPatterns(), FuncDecl.getNumParameters(), Quantifier.getNumPatterns(), Solver.getNumScopes(), Model.getNumSorts(), ApplyResult.getNumSubgoals(), Pattern.getNumTerms(), Tactic.getParameterDescriptions(), Solver.getParameterDescriptions(), Fixedpoint.getParameterDescriptions(), FuncDecl.getParameters(), Quantifier.getPatterns(), Goal.getPrecision(), Solver.getProof(), ArraySort.getRange(), FuncDecl.getRange(), Fixedpoint.getReasonUnknown(), Solver.getReasonUnknown(), DatatypeSort.getRecognizers(), Fixedpoint.getRules(), AST.getSExpr(), BitVecSort.getSize(), FiniteDomainSort.getSize(), Expr.getSort(), Sort.getSortKind(), Model.getSorts(), Model.getSortUniverse(), Solver.getStatistics(), StringSymbol.getString(), ApplyResult.getSubgoals(), ListSort.getTailDecl(), Pattern.getTerms(), Constructor.getTesterDecl(), EnumSort.getTesterDecls(), Solver.getUnsatCore(), FuncInterp.Entry.getValue(), Quantifier.getWeight(), AST.hashCode(), Goal.inconsistent(), ASTMap.insert(), Expr.isAlgebraicNumber(), Expr.isArray(), Expr.isBool(), Expr.isBV(), Goal.isDecidedSat(), Goal.isDecidedUnsat(), Expr.isFiniteDomain(), Expr.isInt(), Expr.isNumeral(), Expr.isReal(), Expr.isRelation(), Quantifier.isUniversal(), Expr.isWellSorted(), TupleSort.mkDecl(), Context.mkMap(), Context.mkSetMembership(), Solver.pop(), Fixedpoint.pop(), ASTVector.push(), Solver.push(), Fixedpoint.push(), Quantifier.Quantifier(), Fixedpoint.query(), Fixedpoint.registerRelation(), ASTMap.reset(), Solver.reset(), Goal.reset(), ASTVector.resize(), ASTVector.set(), Solver.setParameters(), Fixedpoint.setParameters(), Fixedpoint.setPredicateRepresentation(), Expr.simplify(), ASTVector.size(), ParamDescrs.size(), ASTMap.size(), Goal.size(), Statistics.size(), Expr.substitute(), Expr.substituteVars(), AlgebraicNum.toDecimal(), RatNum.toDecimalString(), AlgebraicNum.toLower(), Pattern.toString(), BitVecNum.toString(), IntNum.toString(), ApplyResult.toString(), FuncDecl.toString(), ParamDescrs.toString(), RatNum.toString(), Sort.toString(), ASTVector.toString(), ASTMap.toString(), Params.toString(), Statistics.toString(), AST.toString(), Goal.toString(), Fixedpoint.toString(), Model.toString(), Solver.toString(), AlgebraicNum.toUpper(), ASTVector.translate(), AST.translate(), Expr.translate(), Goal.translate(), Context.unwrapAST(), Expr.update(), Fixedpoint.updateRule(), and ParamDescrs.validate().
{
return m_n_obj;
}
static long getNativeObject | ( | Z3Object | s | ) | [inline, static, package] |
Definition at line 100 of file Z3Object.java.
{ if (s == null) return 0; return s.getNativeObject(); }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented in Fixedpoint, Solver, Model, Goal, AST, Statistics, FuncInterp, Params, ASTMap, ASTVector, Tactic, FuncInterp.Entry, ParamDescrs, ApplyResult, and Probe.
Definition at line 69 of file Z3Object.java.
Referenced by Z3Object.setNativeObject(), and Z3Object.Z3Object().
{ }
void setNativeObject | ( | long | value | ) | throws Z3Exception [inline, package] |
Definition at line 86 of file Z3Object.java.
Referenced by Constructor.Constructor(), ConstructorList.ConstructorList(), EnumSort.EnumSort(), ListSort.ListSort(), Quantifier.Quantifier(), TupleSort.TupleSort(), and Expr.update().
{ if (value != 0) { checkNativeObject(value); incRef(value); } if (m_n_obj != 0) { decRef(m_n_obj); } m_n_obj = value; }