Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Protected Member Functions | Package Functions | Static Package Functions
Z3Object Class Reference
+ Inheritance diagram for Z3Object:

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)

Detailed Description

Internal base class for interfacing with native Z3 objects. Should not be used externally.

Definition at line 24 of file Z3Object.java.


Constructor & Destructor Documentation

Z3Object ( Context  ctx) [inline, package]

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;
    }

Member Function Documentation

static int arrayLength ( Z3Object[]  a) [inline, static, package]
static long [] arrayToNative ( Z3Object[]  a) [inline, static, package]
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]
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]
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;
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines