diff --git a/src/api/java/AST.java b/src/api/java/AST.java index f43aa85d2..4b5b37d46 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -187,34 +187,15 @@ public class AST extends Z3Object implements Comparable return Native.astToString(getContext().nCtx(), getNativeObject()); } - AST(Context ctx) - { - super(ctx); - } - - AST(Context ctx, long obj) - { + AST(Context ctx, long obj) { super(ctx, obj); } @Override void incRef(long o) { - // Console.WriteLine("AST IncRef()"); - if (getContext() == null || o == 0) - return; - getContext().getASTDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - // Console.WriteLine("AST DecRef()"); - if (getContext() == null || o == 0) - return; - getContext().getASTDRQ().add(o); - super.decRef(o); + Native.incRef(getContext().nCtx(), o); + getContext().getASTDRQ().storeReference(getContext(), this); } static AST create(Context ctx, long obj) diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java index 32f6a5d0e..d462e16d5 100644 --- a/src/api/java/ASTDecRefQueue.java +++ b/src/api/java/ASTDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTDecRefQueue extends IDecRefQueue +class ASTDecRefQueue extends IDecRefQueue { public ASTDecRefQueue() { @@ -30,26 +30,7 @@ class ASTDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.incRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.decRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.decRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java index a6201d8a0..b4ae7102a 100644 --- a/src/api/java/ASTMap.java +++ b/src/api/java/ASTMap.java @@ -120,14 +120,7 @@ class ASTMap extends Z3Object @Override void incRef(long o) { - getContext().getASTMapDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getASTMapDRQ().add(o); - super.decRef(o); + Native.astMapIncRef(getContext().nCtx(), o); + getContext().getASTMapDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java index da1ab0f12..7c5ca1067 100644 --- a/src/api/java/ASTVector.java +++ b/src/api/java/ASTVector.java @@ -105,17 +105,10 @@ public class ASTVector extends Z3Object @Override void incRef(long o) { - getContext().getASTVectorDRQ().incAndClear(getContext(), o); - super.incRef(o); + Native.astVectorIncRef(getContext().nCtx(), o); + getContext().getASTVectorDRQ().storeReference(getContext(), this); } - @Override - void decRef(long o) - { - getContext().getASTVectorDRQ().add(o); - super.decRef(o); - } - /** * Translates the AST vector into an AST[] * */ diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java index f598c9504..8b3c1daf6 100644 --- a/src/api/java/ApplyResult.java +++ b/src/api/java/ApplyResult.java @@ -74,16 +74,8 @@ public class ApplyResult extends Z3Object } @Override - void incRef(long o) - { - getContext().getApplyResultDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getApplyResultDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.applyResultIncRef(getContext().nCtx(), o); + getContext().getApplyResultDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java index 63f315ecd..d28ff755e 100644 --- a/src/api/java/ApplyResultDecRefQueue.java +++ b/src/api/java/ApplyResultDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ApplyResultDecRefQueue extends IDecRefQueue +class ApplyResultDecRefQueue extends IDecRefQueue { public ApplyResultDecRefQueue() { @@ -30,26 +30,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.applyResultIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.applyResultDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.applyResultDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/AstMapDecRefQueue.java b/src/api/java/AstMapDecRefQueue.java index 1598f75e7..234b7eec4 100644 --- a/src/api/java/AstMapDecRefQueue.java +++ b/src/api/java/AstMapDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTMapDecRefQueue extends IDecRefQueue +class ASTMapDecRefQueue extends IDecRefQueue { public ASTMapDecRefQueue() { @@ -30,26 +30,7 @@ class ASTMapDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.astMapIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.astMapDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.astMapDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java index a63d808d3..3a486ee06 100644 --- a/src/api/java/AstVectorDecRefQueue.java +++ b/src/api/java/AstVectorDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ASTVectorDecRefQueue extends IDecRefQueue +class ASTVectorDecRefQueue extends IDecRefQueue { public ASTVectorDecRefQueue() { @@ -30,26 +30,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.astVectorIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.astVectorDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.astVectorDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/BoolExpr.java b/src/api/java/BoolExpr.java index 02eabd2b5..dc75b2e7c 100644 --- a/src/api/java/BoolExpr.java +++ b/src/api/java/BoolExpr.java @@ -20,15 +20,7 @@ package com.microsoft.z3; /** * Boolean expressions **/ -public class BoolExpr extends Expr -{ - /** - * Constructor for BoolExpr - **/ - protected BoolExpr(Context ctx) - { - super(ctx); - } +public class BoolExpr extends Expr { /** * Constructor for BoolExpr diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java index a6c2856d4..28558b15a 100644 --- a/src/api/java/Constructor.java +++ b/src/api/java/Constructor.java @@ -20,8 +20,14 @@ package com.microsoft.z3; /** * Constructors are used for datatype sorts. **/ -public class Constructor extends Z3Object -{ +public class Constructor extends Z3Object { + private final int n; + + Constructor(Context ctx, int n, long nativeObj) { + super(ctx, nativeObj); + this.n = n; + } + /** * The number of fields of the constructor. * @throws Z3Exception @@ -78,29 +84,16 @@ public class Constructor extends Z3Object return t; } - /** - * Destructor. - * @throws Throwable - * @throws Z3Exception on error - **/ - protected void finalize() throws Throwable - { - try { - Native.delConstructor(getContext().nCtx(), getNativeObject()); - } finally { - super.finalize(); - } + @Override + void incRef(long o) { + + // Datatype constructors are not reference counted. + getContext().getConstructorDRQ().storeReference(getContext(), this); } - private int n = 0; - - Constructor(Context ctx, Symbol name, Symbol recognizer, - Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) - - { - super(ctx); - - n = AST.arrayLength(fieldNames); + static Constructor of(Context ctx, Symbol name, Symbol recognizer, + Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { + int n = AST.arrayLength(fieldNames); if (n != AST.arrayLength(sorts)) throw new Z3Exception( @@ -112,9 +105,10 @@ public class Constructor extends Z3Object if (sortRefs == null) sortRefs = new int[n]; - setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), + long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(), recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames), - Sort.arrayToNative(sorts), sortRefs)); + Sort.arrayToNative(sorts), sortRefs); + return new Constructor(ctx, n, nativeObj); } } diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index fe3fae1ac..3f1835082 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -20,32 +20,21 @@ package com.microsoft.z3; /** * Lists of constructors **/ -public class ConstructorList extends Z3Object -{ - /** - * Destructor. - * @throws Throwable - * @throws Z3Exception on error - **/ - protected void finalize() throws Throwable - { - try { - Native.delConstructorList(getContext().nCtx(), getNativeObject()); - } finally { - super.finalize(); - } - } +public class ConstructorList extends Z3Object { ConstructorList(Context ctx, long obj) { super(ctx, obj); } + @Override + void incRef(long o) { + getContext().getConstructorListDRQ().storeReference(getContext(), this); + } + ConstructorList(Context ctx, Constructor[] constructors) { - super(ctx); - - setNativeObject(Native.mkConstructorList(getContext().nCtx(), + super(ctx, Native.mkConstructorList(ctx.nCtx(), constructors.length, Constructor.arrayToNative(constructors))); } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 9fa17fcd4..41fb027fe 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -17,34 +17,35 @@ Notes: package com.microsoft.z3; -import java.util.Map; -import java.util.concurrent.atomic.AtomicInteger; +import static com.microsoft.z3.Constructor.of; import com.microsoft.z3.enumerations.Z3_ast_print_mode; +import java.util.Map; + /** * The main interaction with Z3 happens via the Context. **/ -public class Context extends IDisposable -{ - /** - * Constructor. - **/ - public Context() - { - super(); - synchronized (creation_lock) { +public class Context implements AutoCloseable { + private final long m_ctx; + static final Object creation_lock = new Object(); + + public static Context mkContext() { + long m_ctx; + synchronized (creation_lock) { m_ctx = Native.mkContextRc(0); - initContext(); + // TODO: then adding settings will not be under the lock. } + return new Context(m_ctx); } + /** * Constructor. * Remarks: - * The following parameters can be set: + * The following parameters can be set: * - proof (Boolean) Enable proof generation - * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting + * - debug_ref_count (Boolean) Enable debug support for Z3_ast reference counting * - trace (Boolean) Tracing support for VCC * - trace_file_name (String) Trace out file for VCC traces * - timeout (unsigned) default timeout (in milliseconds) used for solvers @@ -53,20 +54,32 @@ public class Context extends IDisposable * - model model generation for solvers, this parameter can be overwritten when creating a solver * - model_validate validate models produced by solvers * - unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver - * Note that in previous versions of Z3, this constructor was also used to set global and + * Note that in previous versions of Z3, this constructor was also used to set global and * module parameters. For this purpose we should now use {@code Global.setParameter} **/ - public Context(Map settings) + public static Context mkContext(Map settings) { - super(); - synchronized (creation_lock) { + long m_ctx; + synchronized (creation_lock) { long cfg = Native.mkConfig(); for (Map.Entry kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); - initContext(); } + return new Context(m_ctx); + } + + /** + * Constructor. + **/ + protected Context(long m_ctx) + { + this.m_ctx = m_ctx; + + // Code which used to be in "initContext". + setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); + Native.setInternalErrorHandler(m_ctx); } /** @@ -242,7 +255,7 @@ public class Context extends IDisposable checkContextMatch(name); checkContextMatch(fieldNames); checkContextMatch(fieldSorts); - return new TupleSort(this, name, (int) fieldNames.length, fieldNames, + return new TupleSort(this, name, fieldNames.length, fieldNames, fieldSorts); } @@ -319,8 +332,7 @@ public class Context extends IDisposable Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) { - - return new Constructor(this, name, recognizer, fieldNames, sorts, + return of(this, name, recognizer, fieldNames, sorts, sortRefs); } @@ -329,10 +341,8 @@ public class Context extends IDisposable **/ public Constructor mkConstructor(String name, String recognizer, String[] fieldNames, Sort[] sorts, int[] sortRefs) - { - - return new Constructor(this, mkSymbol(name), mkSymbol(recognizer), + return of(this, mkSymbol(name), mkSymbol(recognizer), mkSymbols(fieldNames), sorts, sortRefs); } @@ -525,7 +535,7 @@ public class Context extends IDisposable 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, + return new Pattern(this, Native.mkPattern(nCtx(), terms.length, termsNative)); } @@ -688,7 +698,7 @@ public class Context extends IDisposable public BoolExpr mkDistinct(Expr... args) { checkContextMatch(args); - return new BoolExpr(this, Native.mkDistinct(nCtx(), (int) args.length, + return new BoolExpr(this, Native.mkDistinct(nCtx(), args.length, AST.arrayToNative(args))); } @@ -756,7 +766,7 @@ public class Context extends IDisposable public BoolExpr mkAnd(BoolExpr... t) { checkContextMatch(t); - return new BoolExpr(this, Native.mkAnd(nCtx(), (int) t.length, + return new BoolExpr(this, Native.mkAnd(nCtx(), t.length, AST.arrayToNative(t))); } @@ -766,7 +776,7 @@ public class Context extends IDisposable public BoolExpr mkOr(BoolExpr... t) { checkContextMatch(t); - return new BoolExpr(this, Native.mkOr(nCtx(), (int) t.length, + return new BoolExpr(this, Native.mkOr(nCtx(), t.length, AST.arrayToNative(t))); } @@ -777,7 +787,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkAdd(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkAdd(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -787,7 +797,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkMul(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkMul(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -797,7 +807,7 @@ public class Context extends IDisposable { checkContextMatch(t); return (ArithExpr) Expr.create(this, - Native.mkSub(nCtx(), (int) t.length, AST.arrayToNative(t))); + Native.mkSub(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -1814,7 +1824,7 @@ public class Context extends IDisposable { checkContextMatch(args); return (ArrayExpr)Expr.create(this, - Native.mkSetUnion(nCtx(), (int) args.length, + Native.mkSetUnion(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1825,7 +1835,7 @@ public class Context extends IDisposable { checkContextMatch(args); return (ArrayExpr)Expr.create(this, - Native.mkSetIntersect(nCtx(), (int) args.length, + Native.mkSetIntersect(nCtx(), args.length, AST.arrayToNative(args))); } @@ -1912,7 +1922,7 @@ public class Context extends IDisposable public SeqExpr MkConcat(SeqExpr... t) { checkContextMatch(t); - return new SeqExpr(this, Native.mkSeqConcat(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new SeqExpr(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t))); } @@ -2040,7 +2050,7 @@ public class Context extends IDisposable public ReExpr MkConcat(ReExpr... t) { checkContextMatch(t); - return new ReExpr(this, Native.mkReConcat(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new ReExpr(this, Native.mkReConcat(nCtx(), t.length, AST.arrayToNative(t))); } /** @@ -2049,7 +2059,7 @@ public class Context extends IDisposable public ReExpr MkUnion(ReExpr... t) { checkContextMatch(t); - return new ReExpr(this, Native.mkReUnion(nCtx(), (int)t.length, AST.arrayToNative(t))); + return new ReExpr(this, Native.mkReUnion(nCtx(), t.length, AST.arrayToNative(t))); } @@ -2258,7 +2268,7 @@ public class Context extends IDisposable Symbol quantifierID, Symbol skolemID) { - return new Quantifier(this, true, sorts, names, body, weight, patterns, + return Quantifier.of(this, true, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2271,7 +2281,7 @@ public class Context extends IDisposable Symbol skolemID) { - return new Quantifier(this, true, boundConstants, body, weight, + return Quantifier.of(this, true, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2284,7 +2294,7 @@ public class Context extends IDisposable Symbol quantifierID, Symbol skolemID) { - return new Quantifier(this, false, sorts, names, body, weight, + return Quantifier.of(this, false, sorts, names, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -2297,7 +2307,7 @@ public class Context extends IDisposable Symbol skolemID) { - return new Quantifier(this, false, boundConstants, body, weight, + return Quantifier.of(this, false, boundConstants, body, weight, patterns, noPatterns, quantifierID, skolemID); } @@ -3814,7 +3824,7 @@ public class Context extends IDisposable * must be a native object obtained from Z3 (e.g., through * {@code UnwrapAST}) and that it must have a correct reference count. * @see Native#incRef - * @see unwrapAST + * @see #unwrapAST * @param nativeObject The native pointer to wrap. **/ public AST wrapAST(long nativeObject) @@ -3869,19 +3879,12 @@ public class Context extends IDisposable Native.updateParamValue(nCtx(), id, value); } - protected long m_ctx = 0; - protected static final Object creation_lock = new Object(); long nCtx() { return m_ctx; } - void initContext() - { - setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); - Native.setInternalErrorHandler(nCtx()); - } void checkContextMatch(Z3Object other) { @@ -3925,110 +3928,103 @@ public class Context extends IDisposable private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10); private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10); private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue(10); + private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(10); + private ConstructorListDecRefQueue m_ConstructorList_DRQ = + new ConstructorListDecRefQueue(10); - public IDecRefQueue getASTDRQ() + public IDecRefQueue getConstructorDRQ() { + return m_Constructor_DRQ; + } + + public IDecRefQueue getConstructorListDRQ() { + return m_ConstructorList_DRQ; + } + + public IDecRefQueue getASTDRQ() { return m_AST_DRQ; } - public IDecRefQueue getASTMapDRQ() + public IDecRefQueue getASTMapDRQ() { return m_ASTMap_DRQ; } - public IDecRefQueue getASTVectorDRQ() + public IDecRefQueue getASTVectorDRQ() { return m_ASTVector_DRQ; } - public IDecRefQueue getApplyResultDRQ() + public IDecRefQueue getApplyResultDRQ() { return m_ApplyResult_DRQ; } - public IDecRefQueue getFuncEntryDRQ() + public IDecRefQueue getFuncEntryDRQ() { return m_FuncEntry_DRQ; } - public IDecRefQueue getFuncInterpDRQ() + public IDecRefQueue getFuncInterpDRQ() { return m_FuncInterp_DRQ; } - public IDecRefQueue getGoalDRQ() + public IDecRefQueue getGoalDRQ() { return m_Goal_DRQ; } - public IDecRefQueue getModelDRQ() + public IDecRefQueue getModelDRQ() { return m_Model_DRQ; } - public IDecRefQueue getParamsDRQ() + public IDecRefQueue getParamsDRQ() { return m_Params_DRQ; } - public IDecRefQueue getParamDescrsDRQ() + public IDecRefQueue getParamDescrsDRQ() { return m_ParamDescrs_DRQ; } - public IDecRefQueue getProbeDRQ() + public IDecRefQueue getProbeDRQ() { return m_Probe_DRQ; } - public IDecRefQueue getSolverDRQ() + public IDecRefQueue getSolverDRQ() { return m_Solver_DRQ; } - public IDecRefQueue getStatisticsDRQ() + public IDecRefQueue getStatisticsDRQ() { return m_Statistics_DRQ; } - public IDecRefQueue getTacticDRQ() + public IDecRefQueue getTacticDRQ() { return m_Tactic_DRQ; } - public IDecRefQueue getFixedpointDRQ() + public IDecRefQueue getFixedpointDRQ() { return m_Fixedpoint_DRQ; } - public IDecRefQueue getOptimizeDRQ() + public IDecRefQueue getOptimizeDRQ() { return m_Optimize_DRQ; } - protected AtomicInteger m_refCount = new AtomicInteger(0); - - /** - * Finalizer. - * @throws Throwable - **/ - protected void finalize() throws Throwable - { - try { - dispose(); - } - catch (Throwable t) { - throw t; - } - finally { - super.finalize(); - } - } - /** * Disposes of the context. **/ - public void dispose() + @Override + public void close() { m_AST_DRQ.clear(this); m_ASTMap_DRQ.clear(this); @@ -4052,15 +4048,7 @@ public class Context extends IDisposable m_stringSort = null; synchronized (creation_lock) { - if (m_refCount.get() == 0 && m_ctx != 0) { - try { - Native.delContext(m_ctx); - } catch (Z3Exception e) { - // OK? - System.out.println("Context deletion failed; memory leak possible."); - } - m_ctx = 0; - } + Native.delContext(m_ctx); } } } diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index bb60eef56..ce2f8d578 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -92,13 +92,9 @@ public class EnumSort extends Sort EnumSort(Context ctx, Symbol name, Symbol[] enumNames) { - super(ctx, 0); - - int n = enumNames.length; - long[] n_constdecls = new long[n]; - long[] n_testers = new long[n]; - setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), - name.getNativeObject(), n, Symbol.arrayToNative(enumNames), - n_constdecls, n_testers)); + super(ctx, Native.mkEnumerationSort(ctx.nCtx(), + name.getNativeObject(), enumNames.length, + Symbol.arrayToNative(enumNames), + new long[enumNames.length], new long[enumNames.length])); } }; diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index b24d3ac62..ea3fd2147 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -120,13 +120,13 @@ public class Expr extends AST * @param args arguments * @throws Z3Exception on error **/ - public void update(Expr[] args) + public Expr update(Expr[] args) { getContext().checkContextMatch(args); if (isApp() && args.length != getNumArgs()) { throw new Z3Exception("Number of arguments does not match"); } - setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(), + return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(), args.length, Expr.arrayToNative(args))); } @@ -2091,36 +2091,23 @@ public class Expr extends AST **/ public int getIndex() { - if (!isVar()) + if (!isVar()) { throw new Z3Exception("Term is not a bound variable."); + } return Native.getIndexValue(getContext().nCtx(), getNativeObject()); } - /** - * Constructor for Expr - **/ - protected Expr(Context ctx) - { - super(ctx); - { - } - } - /** * Constructor for Expr * @throws Z3Exception on error **/ - protected Expr(Context ctx, long obj) - { + protected Expr(Context ctx, long obj) { super(ctx, obj); - { - } } @Override - void checkNativeObject(long obj) - { + void checkNativeObject(long obj) { if (!Native.isApp(getContext().nCtx(), obj) && Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_VAR_AST.toInt() && Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) { diff --git a/src/api/java/FPNum.java b/src/api/java/FPNum.java index 9aeb41759..402d25ebe 100644 --- a/src/api/java/FPNum.java +++ b/src/api/java/FPNum.java @@ -28,7 +28,7 @@ public class FPNum extends FPExpr */ public boolean getSign() { Native.IntPtr res = new Native.IntPtr(); - if (Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Sign is not a Boolean value"); return res.value != 0; } @@ -53,7 +53,7 @@ public class FPNum extends FPExpr public long getSignificandUInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralSignificandUint64(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Significand is not a 64 bit unsigned integer"); return res.value; } @@ -72,7 +72,7 @@ public class FPNum extends FPExpr */ public long getExponentInt64() { Native.LongPtr res = new Native.LongPtr(); - if (Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res) ^ true) + if (!Native.fpaGetNumeralExponentInt64(getContext().nCtx(), getNativeObject(), res)) throw new Z3Exception("Exponent is not a 64 bit integer"); return res.value; } diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java index 2ff10a1f3..5a7958364 100644 --- a/src/api/java/Fixedpoint.java +++ b/src/api/java/Fixedpoint.java @@ -349,16 +349,11 @@ public class Fixedpoint extends Z3Object } @Override - void incRef(long o) - { - getContext().getFixedpointDRQ().incAndClear(getContext(), o); - super.incRef(o); + void incRef(long o) { + Native.fixedpointIncRef(getContext().nCtx(), o); + getContext().getFixedpointDRQ().storeReference(getContext(), this); } @Override - void decRef(long o) - { - getContext().getFixedpointDRQ().add(o); - super.decRef(o); - } + void checkNativeObject(long obj) { } } diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java index e65538a30..d5ae79a2b 100644 --- a/src/api/java/FixedpointDecRefQueue.java +++ b/src/api/java/FixedpointDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FixedpointDecRefQueue extends IDecRefQueue +class FixedpointDecRefQueue extends IDecRefQueue { public FixedpointDecRefQueue() { @@ -29,27 +29,10 @@ class FixedpointDecRefQueue extends IDecRefQueue super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.fixedpointIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } @Override protected void decRef(Context ctx, long obj) { - try - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.fixedpointDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java index 72f6bb25d..c84979aa1 100644 --- a/src/api/java/FuncInterp.java +++ b/src/api/java/FuncInterp.java @@ -73,18 +73,12 @@ public class FuncInterp extends Z3Object @Override public String toString() { - try - { - int n = getNumArgs(); - String res = "["; - Expr[] args = getArgs(); - for (int i = 0; i < n; i++) - res += args[i] + ", "; - return res + getValue() + "]"; - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); - } + int n = getNumArgs(); + String res = "["; + Expr[] args = getArgs(); + for (int i = 0; i < n; i++) + res += args[i] + ", "; + return res + getValue() + "]"; } Entry(Context ctx, long obj) @@ -93,17 +87,9 @@ public class FuncInterp extends Z3Object } @Override - void incRef(long o) - { - getContext().getFuncEntryDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getFuncEntryDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.funcEntryIncRef(getContext().nCtx(), o);; + getContext().getFuncEntryDRQ().storeReference(getContext(), this); } } @@ -161,33 +147,27 @@ public class FuncInterp extends Z3Object **/ public String toString() { - try + String res = ""; + res += "["; + for (Entry e : getEntries()) { - String res = ""; - res += "["; - for (Entry e : getEntries()) + int n = e.getNumArgs(); + if (n > 1) + res += "["; + Expr[] args = e.getArgs(); + for (int i = 0; i < n; i++) { - int n = e.getNumArgs(); - if (n > 1) - res += "["; - Expr[] args = e.getArgs(); - for (int i = 0; i < n; i++) - { - if (i != 0) - res += ", "; - res += args[i]; - } - if (n > 1) - res += "]"; - res += " -> " + e.getValue() + ", "; + if (i != 0) + res += ", "; + res += args[i]; } - res += "else -> " + getElse(); - res += "]"; - return res; - } catch (Z3Exception e) - { - return "Z3Exception: " + e.getMessage(); + if (n > 1) + res += "]"; + res += " -> " + e.getValue() + ", "; } + res += "else -> " + getElse(); + res += "]"; + return res; } FuncInterp(Context ctx, long obj) @@ -196,16 +176,8 @@ public class FuncInterp extends Z3Object } @Override - void incRef(long o) - { - getContext().getFuncInterpDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getFuncInterpDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.funcInterpIncRef(getContext().nCtx(), o); + getContext().getFuncInterpDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java index c888e9e3d..136c07b6a 100644 --- a/src/api/java/FuncInterpDecRefQueue.java +++ b/src/api/java/FuncInterpDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FuncInterpDecRefQueue extends IDecRefQueue +class FuncInterpDecRefQueue extends IDecRefQueue { public FuncInterpDecRefQueue() { @@ -30,26 +30,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.funcInterpIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.funcInterpDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.funcInterpDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/FuncInterpEntryDecRefQueue.java b/src/api/java/FuncInterpEntryDecRefQueue.java index 7dfdaa27d..8f6741ba0 100644 --- a/src/api/java/FuncInterpEntryDecRefQueue.java +++ b/src/api/java/FuncInterpEntryDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class FuncInterpEntryDecRefQueue extends IDecRefQueue +class FuncInterpEntryDecRefQueue extends IDecRefQueue { public FuncInterpEntryDecRefQueue() { @@ -30,26 +30,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.funcEntryIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.funcEntryDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.funcEntryDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index e60971179..a6d41ccd2 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -222,11 +222,11 @@ public class Goal extends Z3Object **/ public BoolExpr AsBoolExpr() { int n = size(); - if (n == 0) + if (n == 0) { return getContext().mkTrue(); - else if (n == 1) + } else if (n == 1) { return getFormulas()[0]; - else { + } else { return getContext().mkAnd(getFormulas()); } } @@ -236,23 +236,14 @@ public class Goal extends Z3Object super(ctx, obj); } - Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) - - { + Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) { super(ctx, Native.mkGoal(ctx.nCtx(), (models), (unsatCores), (proofs))); } - void incRef(long o) - { - getContext().getGoalDRQ().incAndClear(getContext(), o); - super.incRef(o); + @Override + void incRef(long o) { + Native.goalIncRef(getContext().nCtx(), o); + getContext().getGoalDRQ().storeReference(getContext(), this); } - - void decRef(long o) - { - getContext().getGoalDRQ().add(o); - super.decRef(o); - } - } diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java index be921241b..724ec003f 100644 --- a/src/api/java/GoalDecRefQueue.java +++ b/src/api/java/GoalDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class GoalDecRefQueue extends IDecRefQueue +class GoalDecRefQueue extends IDecRefQueue { public GoalDecRefQueue() { @@ -30,26 +30,7 @@ class GoalDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.goalIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { + protected void decRef(Context ctx, long obj) { Native.goalDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } } }; diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java index 1a99a3d92..b0a93b552 100644 --- a/src/api/java/IDecRefQueue.java +++ b/src/api/java/IDecRefQueue.java @@ -17,13 +17,21 @@ Notes: package com.microsoft.z3; -import java.util.LinkedList; +import java.lang.ref.PhantomReference; +import java.lang.ref.Reference; +import java.lang.ref.ReferenceQueue; +import java.util.IdentityHashMap; +import java.util.Map; -public abstract class IDecRefQueue +public abstract class IDecRefQueue { - protected final Object m_lock = new Object(); - protected LinkedList m_queue = new LinkedList(); - protected int m_move_limit; + private final int m_move_limit; + + // TODO: problem: ReferenceQueue has no API to return length. + private final ReferenceQueue referenceQueue = new ReferenceQueue<>(); + private int queueSize = 0; + private final Map, Long> referenceMap = + new IdentityHashMap<>(); protected IDecRefQueue() { @@ -34,38 +42,31 @@ public abstract class IDecRefQueue { m_move_limit = move_limit; } - - public void setLimit(int l) { m_move_limit = l; } - - protected abstract void incRef(Context ctx, long obj); + /** + * An implementation of this method should decrement the reference on a + * given native object. + * This function should be always called on the {@code ctx} thread. + * + * @param ctx Z3 context. + * @param obj Pointer to a Z3 object. + */ protected abstract void decRef(Context ctx, long obj); - protected void incAndClear(Context ctx, long o) - { - incRef(ctx, o); - if (m_queue.size() >= m_move_limit) - clear(ctx); - } + public void storeReference(Context ctx, T obj) { + PhantomReference ref = new PhantomReference<>(obj, referenceQueue); + referenceMap.put(ref, obj.getNativeObject()); - protected void add(long o) - { - if (o == 0) - return; - - synchronized (m_lock) - { - m_queue.add(o); - } + // TODO: use move_limit, somehow get the size of referenceQueue. + clear(ctx); } protected void clear(Context ctx) { - synchronized (m_lock) - { - for (Long o : m_queue) - decRef(ctx, o); - m_queue.clear(); + Reference ref; + while ((ref = referenceQueue.poll()) != null) { + long z3ast = referenceMap.remove(ref); + decRef(ctx, z3ast); } } } diff --git a/src/api/java/IDisposable.java b/src/api/java/IDisposable.java deleted file mode 100644 index dae8a7262..000000000 --- a/src/api/java/IDisposable.java +++ /dev/null @@ -1,25 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - IDisposable.java - -Abstract: - - Compatability interface (C# -> Java) - -Author: - - Christoph Wintersteiger (cwinter) 2012-03-16 - -Notes: - ---*/ - -package com.microsoft.z3; - -public abstract class IDisposable -{ - public abstract void dispose(); -} diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 47a128643..99a63821f 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -17,11 +17,10 @@ Notes: package com.microsoft.z3; -import java.util.Map; -import java.lang.String; - import com.microsoft.z3.enumerations.Z3_lbool; +import java.util.Map; + /** * The InterpolationContext is suitable for generation of interpolants. * @@ -33,13 +32,13 @@ public class InterpolationContext extends Context /** * Constructor. **/ - public InterpolationContext() + public static InterpolationContext mkContext() { - super(); + long m_ctx; synchronized(creation_lock) { m_ctx = Native.mkInterpolationContext(0); - initContext(); } + return new InterpolationContext(m_ctx); } /** @@ -49,17 +48,21 @@ public class InterpolationContext extends Context * Remarks: * @see Context#Context **/ - public InterpolationContext(Map settings) + public static InterpolationContext mkContext(Map settings) { - super(); + long m_ctx; synchronized(creation_lock) { long cfg = Native.mkConfig(); for (Map.Entry kv : settings.entrySet()) Native.setParamValue(cfg, kv.getKey(), kv.getValue()); m_ctx = Native.mkInterpolationContext(cfg); Native.delConfig(cfg); - initContext(); } + return new InterpolationContext(m_ctx); + } + + private InterpolationContext(long m_ctx) { + super(m_ctx); } /** diff --git a/src/api/java/ListSort.java b/src/api/java/ListSort.java index 705e93579..0ff2c36cf 100644 --- a/src/api/java/ListSort.java +++ b/src/api/java/ListSort.java @@ -17,6 +17,8 @@ Notes: package com.microsoft.z3; +import com.microsoft.z3.Native.LongPtr; + /** * List sorts. **/ @@ -88,14 +90,9 @@ public class ListSort extends Sort ListSort(Context ctx, Symbol name, Sort elemSort) { - super(ctx, 0); - - Native.LongPtr inil = new Native.LongPtr(), iisnil = new Native.LongPtr(); - Native.LongPtr icons = new Native.LongPtr(), iiscons = new Native.LongPtr(); - Native.LongPtr ihead = new Native.LongPtr(), itail = new Native.LongPtr(); - - setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(), - elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead, - itail)); + super(ctx, Native.mkListSort(ctx.nCtx(), name.getNativeObject(), + elemSort.getNativeObject(), + new LongPtr(), new Native.LongPtr(), new LongPtr(), + new LongPtr(), new LongPtr(), new LongPtr())); } }; diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 1bf77d246..fc6c6046b 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -293,16 +293,8 @@ public class Model extends Z3Object } @Override - void incRef(long o) - { - getContext().getModelDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getModelDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.modelIncRef(getContext().nCtx(), o); + getContext().getModelDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java index b97add310..6b141078e 100644 --- a/src/api/java/ModelDecRefQueue.java +++ b/src/api/java/ModelDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ModelDecRefQueue extends IDecRefQueue +class ModelDecRefQueue extends IDecRefQueue { public ModelDecRefQueue() { @@ -30,26 +30,7 @@ class ModelDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.modelIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.modelDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.modelDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index 5dfe8fcf4..a5705a388 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -266,17 +266,8 @@ public class Optimize extends Z3Object } @Override - void incRef(long o) - { - getContext().getOptimizeDRQ().incAndClear(getContext(), o); - super.incRef(o); + void incRef(long o) { + Native.optimizeIncRef(getContext().nCtx(), o); + getContext().getOptimizeDRQ().storeReference(getContext(), this); } - - @Override - void decRef(long o) - { - getContext().getOptimizeDRQ().add(o); - super.decRef(o); - } - } diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java index 795a8a399..a06165f3e 100644 --- a/src/api/java/OptimizeDecRefQueue.java +++ b/src/api/java/OptimizeDecRefQueue.java @@ -17,8 +17,7 @@ Notes: package com.microsoft.z3; -class OptimizeDecRefQueue extends IDecRefQueue -{ +class OptimizeDecRefQueue extends IDecRefQueue { public OptimizeDecRefQueue() { super(); @@ -30,26 +29,7 @@ class OptimizeDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.fixedpointIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.fixedpointDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.optimizeDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java index f265fb19e..f90e4dd99 100644 --- a/src/api/java/ParamDescrs.java +++ b/src/api/java/ParamDescrs.java @@ -92,16 +92,8 @@ public class ParamDescrs extends Z3Object } @Override - void incRef(long o) - { - getContext().getParamDescrsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getParamDescrsDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.paramDescrsIncRef(getContext().nCtx(), o); + getContext().getParamDescrsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java index e3515bff6..ab7f4ddd6 100644 --- a/src/api/java/ParamDescrsDecRefQueue.java +++ b/src/api/java/ParamDescrsDecRefQueue.java @@ -17,39 +17,20 @@ Notes: package com.microsoft.z3; -class ParamDescrsDecRefQueue extends IDecRefQueue +class ParamDescrsDecRefQueue extends IDecRefQueue { public ParamDescrsDecRefQueue() { super(); } - public ParamDescrsDecRefQueue(int move_limit) - { + public ParamDescrsDecRefQueue(int move_limit) { super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.paramDescrsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - @Override protected void decRef(Context ctx, long obj) { - try - { - Native.paramDescrsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.paramDescrsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 4be36c23d..e3b143371 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -124,16 +124,8 @@ public class Params extends Z3Object } @Override - void incRef(long o) - { - getContext().getParamsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getParamsDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.paramsIncRef(getContext().nCtx(), o); + getContext().getParamsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java index f989f8015..b5281ecbc 100644 --- a/src/api/java/ParamsDecRefQueue.java +++ b/src/api/java/ParamsDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ParamsDecRefQueue extends IDecRefQueue +class ParamsDecRefQueue extends IDecRefQueue { public ParamsDecRefQueue() { @@ -30,26 +30,7 @@ class ParamsDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.paramsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.paramsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.paramsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java index bcaa76ce6..6983613c1 100644 --- a/src/api/java/Probe.java +++ b/src/api/java/Probe.java @@ -54,14 +54,7 @@ public class Probe extends Z3Object @Override void incRef(long o) { - getContext().getProbeDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getProbeDRQ().add(o); - super.decRef(o); + Native.probeIncRef(getContext().nCtx(), o); + getContext().getProbeDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java index 368bd5bba..3f78c6288 100644 --- a/src/api/java/ProbeDecRefQueue.java +++ b/src/api/java/ProbeDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class ProbeDecRefQueue extends IDecRefQueue +class ProbeDecRefQueue extends IDecRefQueue { public ProbeDecRefQueue() { @@ -29,27 +29,9 @@ class ProbeDecRefQueue extends IDecRefQueue super(move_limit); } - @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.probeIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - @Override protected void decRef(Context ctx, long obj) { - try - { - Native.probeDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.probeDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 1b425d3e4..a78277839 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -145,68 +145,67 @@ public class Quantifier extends BoolExpr .nCtx(), getNativeObject())); } - Quantifier(Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, + public static Quantifier of( + Context ctx, boolean isForall, Sort[] sorts, Symbol[] names, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, - Symbol quantifierID, Symbol skolemID) - { - super(ctx, 0); - - getContext().checkContextMatch(patterns); - getContext().checkContextMatch(noPatterns); - getContext().checkContextMatch(sorts); - getContext().checkContextMatch(names); - getContext().checkContextMatch(body); + Symbol quantifierID, Symbol skolemID + ) { + ctx.checkContextMatch(patterns); + ctx.checkContextMatch(noPatterns); + ctx.checkContextMatch(sorts); + ctx.checkContextMatch(names); + ctx.checkContextMatch(body); if (sorts.length != names.length) throw new Z3Exception( "Number of sorts does not match number of names"); - if (noPatterns == null && quantifierID == null && skolemID == null) - { - setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST + long nativeObj; + if (noPatterns == null && quantifierID == null && skolemID == null) { + nativeObj = Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST .arrayToNative(patterns), AST.arrayLength(sorts), AST .arrayToNative(sorts), Symbol.arrayToNative(names), body - .getNativeObject())); - } else - { - setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), - (isForall), weight, AST.getNativeObject(quantifierID), - AST.getNativeObject(skolemID), - AST.arrayLength(patterns), AST.arrayToNative(patterns), - AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), - AST.arrayLength(sorts), AST.arrayToNative(sorts), - Symbol.arrayToNative(names), - body.getNativeObject())); + .getNativeObject()); + } else { + nativeObj = Native.mkQuantifierEx(ctx.nCtx(), + (isForall), weight, AST.getNativeObject(quantifierID), + AST.getNativeObject(skolemID), + AST.arrayLength(patterns), AST.arrayToNative(patterns), + AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), + AST.arrayLength(sorts), AST.arrayToNative(sorts), + Symbol.arrayToNative(names), + body.getNativeObject()); } + return new Quantifier(ctx, nativeObj); } - Quantifier(Context ctx, boolean isForall, Expr[] bound, Expr body, + + public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body, int weight, Pattern[] patterns, Expr[] noPatterns, Symbol quantifierID, Symbol skolemID) { - super(ctx, 0); - - getContext().checkContextMatch(noPatterns); - getContext().checkContextMatch(patterns); - // Context().CheckContextMatch(bound); - getContext().checkContextMatch(body); + ctx.checkContextMatch(noPatterns); + ctx.checkContextMatch(patterns); + // ctx.CheckContextMatch(bound); + ctx.checkContextMatch(body); + long nativeObj; if (noPatterns == null && quantifierID == null && skolemID == null) { - setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), + nativeObj = Native.mkQuantifierConst(ctx.nCtx(), isForall, weight, AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), - AST.arrayToNative(patterns), body.getNativeObject())); - } else - { - setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), + AST.arrayToNative(patterns), body.getNativeObject()); + } else { + nativeObj = Native.mkQuantifierConstEx(ctx.nCtx(), isForall, weight, AST.getNativeObject(quantifierID), AST.getNativeObject(skolemID), AST.arrayLength(bound), AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(noPatterns), - AST.arrayToNative(noPatterns), body.getNativeObject())); + AST.arrayToNative(noPatterns), body.getNativeObject()); } + return new Quantifier(ctx, nativeObj); } Quantifier(Context ctx, long obj) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 431811b8d..5d538b2f3 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -127,13 +127,13 @@ public class Solver extends Z3Object * using the Boolean constants in ps. * * Remarks: - * This API is an alternative to {@link check} with assumptions for + * This API is an alternative to {@link #check()} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using {@link assertAndTrack} + * of the Boolean variables provided using {@code #assertAndTrack} * and the Boolean literals - * provided using {@link check} with assumptions. + * provided using {@link #check()} with assumptions. **/ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { @@ -333,16 +333,8 @@ public class Solver extends Z3Object } @Override - void incRef(long o) - { - getContext().getSolverDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - @Override - void decRef(long o) - { - getContext().getSolverDRQ().add(o); - super.decRef(o); + void incRef(long o) { + Native.solverIncRef(getContext().nCtx(), o); + getContext().getSolverDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java index f4d5fb139..106892fec 100644 --- a/src/api/java/SolverDecRefQueue.java +++ b/src/api/java/SolverDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class SolverDecRefQueue extends IDecRefQueue +class SolverDecRefQueue extends IDecRefQueue { public SolverDecRefQueue() { super(); } @@ -27,26 +27,7 @@ class SolverDecRefQueue extends IDecRefQueue } @Override - protected void incRef(Context ctx, long obj) - { - try - { - Native.solverIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - @Override - protected void decRef(Context ctx, long obj) - { - try - { - Native.solverDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + protected void decRef(Context ctx, long obj) { + Native.solverDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 30a43e7dd..0763a69a3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -95,6 +95,7 @@ public class Sort extends AST super(ctx, obj); } + @Override void checkNativeObject(long obj) { if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_SORT_AST diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java index 1e842a892..d2ba2bbd3 100644 --- a/src/api/java/Statistics.java +++ b/src/api/java/Statistics.java @@ -190,15 +190,9 @@ public class Statistics extends Z3Object super(ctx, obj); } - void incRef(long o) - { - getContext().getStatisticsDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - void decRef(long o) - { - getContext().getStatisticsDRQ().add(o); - super.decRef(o); + @Override + void incRef(long o) { + Native.statsIncRef(getContext().nCtx(), o); + getContext().getStatisticsDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java index 89c66a746..fecf52267 100644 --- a/src/api/java/StatisticsDecRefQueue.java +++ b/src/api/java/StatisticsDecRefQueue.java @@ -17,7 +17,7 @@ Notes: package com.microsoft.z3; -class StatisticsDecRefQueue extends IDecRefQueue +class StatisticsDecRefQueue extends IDecRefQueue { public StatisticsDecRefQueue() { @@ -29,25 +29,8 @@ class StatisticsDecRefQueue extends IDecRefQueue super(move_limit); } - protected void incRef(Context ctx, long obj) - { - try - { - Native.statsIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - - protected void decRef(Context ctx, long obj) - { - try - { - Native.statsDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + @Override + protected void decRef(Context ctx, long obj) { + Native.statsDecRef(ctx.nCtx(), obj); } }; diff --git a/src/api/java/StringSymbol.java b/src/api/java/StringSymbol.java index 8470e1cd4..576737ea7 100644 --- a/src/api/java/StringSymbol.java +++ b/src/api/java/StringSymbol.java @@ -48,9 +48,9 @@ public class StringSymbol extends Symbol void checkNativeObject(long obj) { if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL - .toInt()) + .toInt()) { throw new Z3Exception("Symbol is not of String kind"); - + } super.checkNativeObject(obj); } } diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java index beeaebb69..21925b099 100644 --- a/src/api/java/Symbol.java +++ b/src/api/java/Symbol.java @@ -62,19 +62,13 @@ public class Symbol extends Z3Object * A string representation of the symbol. **/ @Override - public String toString() - { - try - { - if (isIntSymbol()) - return Integer.toString(((IntSymbol) this).getInt()); - else if (isStringSymbol()) - return ((StringSymbol) this).getString(); - else - return "Z3Exception: Unknown symbol kind encountered."; - } catch (Z3Exception ex) - { - return "Z3Exception: " + ex.getMessage(); + public String toString() { + if (isIntSymbol()) { + return Integer.toString(((IntSymbol) this).getInt()); + } else if (isStringSymbol()) { + return ((StringSymbol) this).getString(); + } else { + return "Z3Exception: Unknown symbol kind encountered."; } } @@ -86,6 +80,11 @@ public class Symbol extends Z3Object super(ctx, obj); } + @Override + void incRef(long o) { + // Symbol does not require tracking. + } + static Symbol create(Context ctx, long obj) { switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj))) diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java index 786f8a6ec..f7e030f04 100644 --- a/src/api/java/Tactic.java +++ b/src/api/java/Tactic.java @@ -92,15 +92,10 @@ public class Tactic extends Z3Object super(ctx, Native.mkTactic(ctx.nCtx(), name)); } + @Override void incRef(long o) { - getContext().getTacticDRQ().incAndClear(getContext(), o); - super.incRef(o); - } - - void decRef(long o) - { - getContext().getTacticDRQ().add(o); - super.decRef(o); + Native.tacticIncRef(getContext().nCtx(), o); + getContext().getTacticDRQ().storeReference(getContext(), this); } } diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java index 026760e46..079904175 100644 --- a/src/api/java/TacticDecRefQueue.java +++ b/src/api/java/TacticDecRefQueue.java @@ -17,8 +17,7 @@ Notes: package com.microsoft.z3; -class TacticDecRefQueue extends IDecRefQueue -{ +class TacticDecRefQueue extends IDecRefQueue { public TacticDecRefQueue() { super(); @@ -29,25 +28,9 @@ class TacticDecRefQueue extends IDecRefQueue super(move_limit); } - protected void incRef(Context ctx, long obj) - { - try - { - Native.tacticIncRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } - } - + @Override protected void decRef(Context ctx, long obj) { - try - { - Native.tacticDecRef(ctx.nCtx(), obj); - } catch (Z3Exception e) - { - // OK. - } + Native.tacticDecRef(ctx.nCtx(), obj); } -}; +} diff --git a/src/api/java/TupleSort.java b/src/api/java/TupleSort.java index 1594b874d..ede20d260 100644 --- a/src/api/java/TupleSort.java +++ b/src/api/java/TupleSort.java @@ -59,11 +59,9 @@ public class TupleSort extends Sort TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames, Sort[] fieldSorts) { - super(ctx, 0); - - Native.LongPtr t = new Native.LongPtr(); - setNativeObject(Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(), + super(ctx, Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(), numFields, Symbol.arrayToNative(fieldNames), - AST.arrayToNative(fieldSorts), t, new long[numFields])); + AST.arrayToNative(fieldSorts), new Native.LongPtr(), + new long[numFields])); } }; diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index dc1feecbf..6fd12bfba 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -21,88 +21,38 @@ package com.microsoft.z3; * Internal base class for interfacing with native Z3 objects. Should not be * used externally. **/ -public class Z3Object extends IDisposable -{ - /** - * Finalizer. - * @throws Throwable - **/ - protected void finalize() throws Throwable - { - try { - dispose(); - } finally { - super.finalize(); - } - } +public abstract class Z3Object { - /** - * Disposes of the underlying native Z3 object. - **/ - public void dispose() - { - if (m_n_obj != 0) - { - decRef(m_n_obj); - m_n_obj = 0; - } + private final Context m_ctx; + private final long m_n_obj; - if (m_ctx != null) - { - if (m_ctx.m_refCount.decrementAndGet() == 0) - m_ctx.dispose(); - m_ctx = null; - } - } - - private Context m_ctx = null; - private long m_n_obj = 0; - - Z3Object(Context ctx) - { - ctx.m_refCount.incrementAndGet(); - m_ctx = ctx; - } - - Z3Object(Context ctx, long obj) - { - ctx.m_refCount.incrementAndGet(); + Z3Object(Context ctx, long obj) { m_ctx = ctx; + checkNativeObject(obj); incRef(obj); m_n_obj = obj; } - void incRef(long o) - { - } + /** + * Increment reference count on {@code o}. + * + * @param o Z3 object. + */ + abstract void incRef(long o); - void decRef(long o) - { - } - - void checkNativeObject(long obj) - { - } + /** + * This function is provided for overriding, and a child class + * can insert consistency checks on {@code obj}. + * + * @param obj Z3 native object. + */ + void checkNativeObject(long obj) {} long getNativeObject() { return m_n_obj; } - void setNativeObject(long value) - { - if (value != 0) - { - checkNativeObject(value); - incRef(value); - } - if (m_n_obj != 0) - { - decRef(m_n_obj); - } - m_n_obj = value; - } - static long getNativeObject(Z3Object s) { if (s == null) @@ -121,7 +71,7 @@ public class Z3Object extends IDisposable 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(); + an[i] = (a[i] == null) ? 0 : a[i].getNativeObject(); return an; }