diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index e84dc8c81..e1cde837f 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -175,15 +175,8 @@ public class AST extends Z3Object implements Comparable<AST>
* A string representation of the AST.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.astToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.astToString(getContext().nCtx(), getNativeObject());
}
/**
@@ -194,34 +187,18 @@ public class AST extends Z3Object implements Comparable<AST>
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);
+ void incRef() {
+ Native.incRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- // Console.WriteLine("AST DecRef()");
- if (getContext() == null || o == 0)
- return;
- getContext().getASTDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ 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..b0a6fa217 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -17,39 +17,15 @@ Notes:
package com.microsoft.z3;
-class ASTDecRefQueue extends IDecRefQueue
+class ASTDecRefQueue extends IDecRefQueue<AST>
{
public ASTDecRefQueue()
{
super();
}
- public ASTDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@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 7bc485bf5..916811cec 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -20,8 +20,7 @@ package com.microsoft.z3;
/**
* Map from AST to AST
**/
-class ASTMap extends Z3Object
-{
+class ASTMap extends Z3Object {
/**
* Checks whether the map contains the key {@code k}.
* @param k An AST
@@ -104,13 +103,7 @@ class ASTMap extends Z3Object
@Override
public String toString()
{
- try
- {
- return Native.astMapToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.astMapToString(getContext().nCtx(), getNativeObject());
}
ASTMap(Context ctx, long obj)
@@ -124,16 +117,12 @@ class ASTMap extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getASTMapDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.astMapIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getASTMapDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getASTMapDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index ab99e2aee..4d9ab291a 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -20,8 +20,7 @@ package com.microsoft.z3;
/**
* Vectors of ASTs.
**/
-public class ASTVector extends Z3Object
-{
+public class ASTVector extends Z3Object {
/**
* The size of the vector
**/
@@ -88,15 +87,8 @@ public class ASTVector extends Z3Object
* Retrieves a string representation of the vector.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.astVectorToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.astVectorToString(getContext().nCtx(), getNativeObject());
}
ASTVector(Context ctx, long obj)
@@ -110,19 +102,15 @@ public class ASTVector extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getASTVectorDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getASTVectorDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getASTVectorDRQ().storeReference(getContext(), this);
}
-
+
/**
* Translates the AST vector into an AST[]
* */
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index 84c63e966..6fafbd888 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -21,8 +21,7 @@ package com.microsoft.z3;
* ApplyResult objects represent the result of an application of a tactic to a
* goal. It contains the subgoals that were produced.
**/
-public class ApplyResult extends Z3Object
-{
+public class ApplyResult extends Z3Object {
/**
* The number of Subgoals.
**/
@@ -64,15 +63,8 @@ public class ApplyResult extends Z3Object
* A string representation of the ApplyResult.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.applyResultToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.applyResultToString(getContext().nCtx(), getNativeObject());
}
ApplyResult(Context ctx, long obj)
@@ -81,16 +73,12 @@ public class ApplyResult extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getApplyResultDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getApplyResultDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getApplyResultDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index 63f315ecd..e1a660781 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -17,39 +17,15 @@ Notes:
package com.microsoft.z3;
-class ApplyResultDecRefQueue extends IDecRefQueue
+class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
{
public ApplyResultDecRefQueue()
{
super();
}
- public ApplyResultDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@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..6c96970b7 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class ASTMapDecRefQueue extends IDecRefQueue
-{
+class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
public ASTMapDecRefQueue()
{
super();
}
- public ASTMapDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.astMapIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.astMapDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.astMapDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/AstVectorDecRefQueue.java b/src/api/java/AstVectorDecRefQueue.java
index a63d808d3..e7ce3e33e 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class ASTVectorDecRefQueue extends IDecRefQueue
-{
+class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
public ASTVectorDecRefQueue()
{
super();
}
- public ASTVectorDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.astVectorIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.astVectorDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.astVectorDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java
index 5a62f8087..d6c176855 100644
--- a/src/api/java/BitVecNum.java
+++ b/src/api/java/BitVecNum.java
@@ -66,13 +66,7 @@ public class BitVecNum extends BitVecExpr
@Override
public String toString()
{
- try
- {
- return Native.getNumeralString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
BitVecNum(Context ctx, long 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..87ab86c3f 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,19 @@ 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() {
+ // Datatype constructors are not reference counted.
}
- private int n = 0;
+ @Override
+ void addToReferenceQueue() {
+ getContext().getConstructorDRQ().storeReference(getContext(), this);
+ }
- 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 +108,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/ConstructorDecRefQueue.java b/src/api/java/ConstructorDecRefQueue.java
new file mode 100644
index 000000000..5003dde5f
--- /dev/null
+++ b/src/api/java/ConstructorDecRefQueue.java
@@ -0,0 +1,12 @@
+package com.microsoft.z3;
+
+public class ConstructorDecRefQueue extends IDecRefQueue<Constructor> {
+ public ConstructorDecRefQueue() {
+ super();
+ }
+
+ @Override
+ protected void decRef(Context ctx, long obj) {
+ Native.delConstructor(ctx.nCtx(), obj);
+ }
+}
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index fe3fae1ac..c79e08d9e 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -20,32 +20,26 @@ 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() {
+ // Constructor lists are not reference counted.
+ }
+
+ @Override
+ void addToReferenceQueue() {
+ 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/ConstructorListDecRefQueue.java b/src/api/java/ConstructorListDecRefQueue.java
new file mode 100644
index 000000000..1a2460731
--- /dev/null
+++ b/src/api/java/ConstructorListDecRefQueue.java
@@ -0,0 +1,12 @@
+package com.microsoft.z3;
+
+public class ConstructorListDecRefQueue extends IDecRefQueue<ConstructorList> {
+ public ConstructorListDecRefQueue() {
+ super();
+ }
+
+ @Override
+ protected void decRef(Context ctx, long obj) {
+ Native.delConstructorList(ctx.nCtx(), obj);
+ }
+}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 9fa17fcd4..39d35d9d3 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -17,34 +17,31 @@ 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) {
- m_ctx = Native.mkContextRc(0);
- initContext();
- }
+public class Context implements AutoCloseable {
+ private final long m_ctx;
+ static final Object creation_lock = new Object();
+
+ public Context () {
+ m_ctx = Native.mkContextRc(0);
+ init();
}
+
/**
* 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 +50,22 @@ 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<String, String> settings)
- {
- super();
- synchronized (creation_lock) {
- 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();
+ public Context(Map<String, String> settings) {
+ 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);
+ init();
+ }
+
+ private void init() {
+ setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
+ Native.setInternalErrorHandler(m_ctx);
}
/**
@@ -242,7 +241,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 +318,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 +327,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 +521,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 +684,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 +752,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 +762,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 +773,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 +783,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 +793,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 +1810,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 +1821,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 +1908,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 +2036,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 +2045,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 +2254,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 +2267,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 +2280,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 +2293,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 +3810,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 +3865,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)
{
@@ -3910,125 +3899,118 @@ public class Context extends IDisposable
}
private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();
- private ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue(10);
- private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue(10);
- private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue(10);
- private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue(10);
- private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue(10);
- private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue(10);
- private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue(10);
- private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue(10);
- private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue(10);
- private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue(10);
- private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue(10);
- private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue(10);
- 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 ASTMapDecRefQueue m_ASTMap_DRQ = new ASTMapDecRefQueue();
+ private ASTVectorDecRefQueue m_ASTVector_DRQ = new ASTVectorDecRefQueue();
+ private ApplyResultDecRefQueue m_ApplyResult_DRQ = new ApplyResultDecRefQueue();
+ private FuncInterpEntryDecRefQueue m_FuncEntry_DRQ = new FuncInterpEntryDecRefQueue();
+ private FuncInterpDecRefQueue m_FuncInterp_DRQ = new FuncInterpDecRefQueue();
+ private GoalDecRefQueue m_Goal_DRQ = new GoalDecRefQueue();
+ private ModelDecRefQueue m_Model_DRQ = new ModelDecRefQueue();
+ private ParamsDecRefQueue m_Params_DRQ = new ParamsDecRefQueue();
+ private ParamDescrsDecRefQueue m_ParamDescrs_DRQ = new ParamDescrsDecRefQueue();
+ private ProbeDecRefQueue m_Probe_DRQ = new ProbeDecRefQueue();
+ private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
+ private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
+ private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
+ private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
+ private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
+ private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
+ private ConstructorListDecRefQueue m_ConstructorList_DRQ =
+ new ConstructorListDecRefQueue();
- public IDecRefQueue getASTDRQ()
+ public IDecRefQueue<Constructor> getConstructorDRQ() {
+ return m_Constructor_DRQ;
+ }
+
+ public IDecRefQueue<ConstructorList> getConstructorListDRQ() {
+ return m_ConstructorList_DRQ;
+ }
+
+ public IDecRefQueue<AST> getASTDRQ()
{
return m_AST_DRQ;
}
- public IDecRefQueue getASTMapDRQ()
+ public IDecRefQueue<ASTMap> getASTMapDRQ()
{
return m_ASTMap_DRQ;
}
- public IDecRefQueue getASTVectorDRQ()
+ public IDecRefQueue<ASTVector> getASTVectorDRQ()
{
return m_ASTVector_DRQ;
}
- public IDecRefQueue getApplyResultDRQ()
+ public IDecRefQueue<ApplyResult> getApplyResultDRQ()
{
return m_ApplyResult_DRQ;
}
- public IDecRefQueue getFuncEntryDRQ()
+ public IDecRefQueue<FuncInterp.Entry> getFuncEntryDRQ()
{
return m_FuncEntry_DRQ;
}
- public IDecRefQueue getFuncInterpDRQ()
+ public IDecRefQueue<FuncInterp> getFuncInterpDRQ()
{
return m_FuncInterp_DRQ;
}
- public IDecRefQueue getGoalDRQ()
+ public IDecRefQueue<Goal> getGoalDRQ()
{
return m_Goal_DRQ;
}
- public IDecRefQueue getModelDRQ()
+ public IDecRefQueue<Model> getModelDRQ()
{
return m_Model_DRQ;
}
- public IDecRefQueue getParamsDRQ()
+ public IDecRefQueue<Params> getParamsDRQ()
{
return m_Params_DRQ;
}
- public IDecRefQueue getParamDescrsDRQ()
+ public IDecRefQueue<ParamDescrs> getParamDescrsDRQ()
{
return m_ParamDescrs_DRQ;
}
- public IDecRefQueue getProbeDRQ()
+ public IDecRefQueue<Probe> getProbeDRQ()
{
return m_Probe_DRQ;
}
- public IDecRefQueue getSolverDRQ()
+ public IDecRefQueue<Solver> getSolverDRQ()
{
return m_Solver_DRQ;
}
- public IDecRefQueue getStatisticsDRQ()
+ public IDecRefQueue<Statistics> getStatisticsDRQ()
{
return m_Statistics_DRQ;
}
- public IDecRefQueue getTacticDRQ()
+ public IDecRefQueue<Tactic> getTacticDRQ()
{
return m_Tactic_DRQ;
}
- public IDecRefQueue getFixedpointDRQ()
+ public IDecRefQueue<Fixedpoint> getFixedpointDRQ()
{
return m_Fixedpoint_DRQ;
}
- public IDecRefQueue getOptimizeDRQ()
+ public IDecRefQueue<Optimize> 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);
@@ -4051,16 +4033,6 @@ public class Context extends IDisposable
m_realSort = null;
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 69a44c559..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;
}
@@ -87,13 +87,7 @@ public class FPNum extends FPExpr
*/
public String toString()
{
- try
- {
- return Native.getNumeralString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
}
diff --git a/src/api/java/FiniteDomainNum.java b/src/api/java/FiniteDomainNum.java
index e53ed22b2..68467e408 100644
--- a/src/api/java/FiniteDomainNum.java
+++ b/src/api/java/FiniteDomainNum.java
@@ -68,12 +68,6 @@ public class FiniteDomainNum extends FiniteDomainExpr
@Override
public String toString()
{
- try
- {
- return Native.getNumeralString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
}
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 14fb3a44a..876345f1e 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -255,14 +255,8 @@ public class Fixedpoint extends Z3Object
@Override
public String toString()
{
- try
- {
- return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
+ return Native.fixedpointToString(getContext().nCtx(), getNativeObject(),
0, null);
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
}
/**
@@ -355,16 +349,15 @@ public class Fixedpoint extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getFixedpointDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getFixedpointDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getFixedpointDRQ().storeReference(getContext(), this);
}
+
+ @Override
+ void checkNativeObject(long obj) { }
}
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index e65538a30..69ed82092 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -17,39 +17,15 @@ Notes:
package com.microsoft.z3;
-class FixedpointDecRefQueue extends IDecRefQueue
-{
+class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
public FixedpointDecRefQueue()
{
super();
}
- public FixedpointDecRefQueue(int move_limit)
- {
- 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/FuncDecl.java b/src/api/java/FuncDecl.java
index 301978c44..273e853c0 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -47,13 +47,7 @@ public class FuncDecl extends AST
@Override
public String toString()
{
- try
- {
- return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
}
/**
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index 72f6bb25d..b5873d98e 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -22,20 +22,20 @@ package com.microsoft.z3;
* Each entry in the finite map represents the value of a function given a set
* of arguments.
**/
-public class FuncInterp extends Z3Object
-{
+public class FuncInterp extends Z3Object {
+
/**
* An Entry object represents an element in the finite map used to encode a
* function interpretation.
**/
- public class Entry extends Z3Object
- {
+ public static class Entry extends Z3Object {
+
/**
* Return the (symbolic) value of this entry.
- *
+ *
* @throws Z3Exception
* @throws Z3Exception on error
- **/
+ **/
public Expr getValue()
{
return Expr.create(getContext(),
@@ -45,7 +45,7 @@ public class FuncInterp extends Z3Object
/**
* The number of arguments of the entry.
* @throws Z3Exception on error
- **/
+ **/
public int getNumArgs()
{
return Native.funcEntryGetNumArgs(getContext().nCtx(), getNativeObject());
@@ -53,10 +53,10 @@ public class FuncInterp extends Z3Object
/**
* The arguments of the function entry.
- *
+ *
* @throws Z3Exception
* @throws Z3Exception on error
- **/
+ **/
public Expr[] getArgs()
{
int n = getNumArgs();
@@ -73,37 +73,26 @@ 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)
- {
+ Entry(Context ctx, long obj) {
super(ctx, obj);
}
@Override
- void incRef(long o)
- {
- getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getFuncEntryDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getFuncEntryDRQ().storeReference(getContext(), this);
}
}
@@ -161,33 +150,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 +179,12 @@ public class FuncInterp extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getFuncInterpDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getFuncInterpDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index c888e9e3d..d8715bd0e 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -17,39 +17,15 @@ Notes:
package com.microsoft.z3;
-class FuncInterpDecRefQueue extends IDecRefQueue
+class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp>
{
public FuncInterpDecRefQueue()
{
super();
}
- public FuncInterpDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@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..a4d8a0690 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class FuncInterpEntryDecRefQueue extends IDecRefQueue
-{
+class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry> {
public FuncInterpEntryDecRefQueue()
{
super();
}
- public FuncInterpEntryDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.funcEntryIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.funcEntryDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.funcEntryDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index 46b04f6bf..25b1fe511 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -23,8 +23,7 @@ import com.microsoft.z3.enumerations.Z3_goal_prec;
* A goal (aka problem). A goal is essentially a set of formulas, that can be
* solved and/or transformed using tactics and solvers.
**/
-public class Goal extends Z3Object
-{
+public class Goal extends Z3Object {
/**
* The precision of the goal.
* Remarks: Goals can be transformed using over
@@ -211,15 +210,8 @@ public class Goal extends Z3Object
*
* @return A string representation of the Goal.
**/
- public String toString()
- {
- try
- {
- return Native.goalToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.goalToString(getContext().nCtx(), getNativeObject());
}
/**
@@ -229,11 +221,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());
}
}
@@ -243,23 +235,18 @@ 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() {
+ Native.goalIncRef(getContext().nCtx(), getNativeObject());
}
- void decRef(long o)
- {
- getContext().getGoalDRQ().add(o);
- super.decRef(o);
+ @Override
+ void addToReferenceQueue() {
+ getContext().getGoalDRQ().storeReference(getContext(), this);
}
-
}
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index be921241b..90bad1fb1 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class GoalDecRefQueue extends IDecRefQueue
-{
+class GoalDecRefQueue extends IDecRefQueue<Goal> {
public GoalDecRefQueue()
{
super();
}
- public GoalDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@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..2deb9c0f9 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -17,55 +17,54 @@ 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
-{
- protected final Object m_lock = new Object();
- protected LinkedList<Long> m_queue = new LinkedList<Long>();
- protected int m_move_limit;
+/**
+ * A queue to handle management of native memory.
+ *
+ * <p><b>Mechanics: </b>once an object is created, a metadata is stored for it in
+ * {@code referenceMap}, and a {@link PhantomReference} is created with a
+ * reference to {@code referenceQueue}.
+ * Once the object becomes strongly unreachable, the phantom reference gets
+ * added by JVM to the {@code referenceQueue}.
+ * After each object creation, we iterate through the available objects in
+ * {@code referenceQueue} and decrement references for them.
+ *
+ * @param <T> Type of object stored in queue.
+ */
+public abstract class IDecRefQueue<T extends Z3Object> {
+ private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
+ private final Map<PhantomReference<T>, Long> referenceMap =
+ new IdentityHashMap<>();
- protected IDecRefQueue()
- {
- m_move_limit = 1024;
- }
-
- protected IDecRefQueue(int move_limit)
- {
- m_move_limit = move_limit;
- }
-
- public void setLimit(int l) { m_move_limit = l; }
-
- protected abstract void incRef(Context ctx, long obj);
+ protected IDecRefQueue() {}
+ /**
+ * An implementation of this method should decrement the reference on a
+ * given native object.
+ * This function should always be 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);
- }
-
- protected void add(long o)
- {
- if (o == 0)
- return;
-
- synchronized (m_lock)
- {
- m_queue.add(o);
- }
+ public void storeReference(Context ctx, T obj) {
+ PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
+ referenceMap.put(ref, obj.getNativeObject());
+ clear(ctx);
}
protected void clear(Context ctx)
{
- synchronized (m_lock)
- {
- for (Long o : m_queue)
- decRef(ctx, o);
- m_queue.clear();
+ Reference<? extends T> 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/IntNum.java b/src/api/java/IntNum.java
index 71d878311..d3a5b456f 100644
--- a/src/api/java/IntNum.java
+++ b/src/api/java/IntNum.java
@@ -63,14 +63,7 @@ public class IntNum extends IntExpr
/**
* Returns a string representation of the numeral.
**/
- public String toString()
- {
- try
- {
- return Native.getNumeralString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
}
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<String, String> settings)
+ public static InterpolationContext mkContext(Map<String, String> settings)
{
- super();
+ long m_ctx;
synchronized(creation_lock) {
long cfg = Native.mkConfig();
for (Map.Entry<String, String> 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 0695d7cf1..60abb001d 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
/**
* A Model contains interpretations (assignments) of constants and functions.
**/
-public class Model extends Z3Object
-{
+public class Model extends Z3Object {
/**
* Retrieves the interpretation (the assignment) of {@code a} in
* the model.
@@ -283,15 +282,8 @@ public class Model extends Z3Object
* @return A string representation of the model.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.modelToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.modelToString(getContext().nCtx(), getNativeObject());
}
Model(Context ctx, long obj)
@@ -300,16 +292,12 @@ public class Model extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getModelDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.modelIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getModelDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getModelDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index b97add310..f1b7c3fdd 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class ModelDecRefQueue extends IDecRefQueue
-{
+class ModelDecRefQueue extends IDecRefQueue<Model> {
public ModelDecRefQueue()
{
super();
}
- public ModelDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.modelIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.modelDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.modelDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index 5dfe8fcf4..ea100d1ca 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -266,17 +266,12 @@ public class Optimize extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getOptimizeDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getOptimizeDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getOptimizeDRQ().storeReference(getContext(), this);
}
-
}
diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java
index 795a8a399..0acf20068 100644
--- a/src/api/java/OptimizeDecRefQueue.java
+++ b/src/api/java/OptimizeDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class OptimizeDecRefQueue extends IDecRefQueue
-{
+class OptimizeDecRefQueue extends IDecRefQueue<Optimize> {
public OptimizeDecRefQueue()
{
super();
}
- public OptimizeDecRefQueue(int move_limit)
- {
- 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.
- }
+ 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 8f8c6df0b..0008515e3 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_param_kind;
/**
* A ParamDescrs describes a set of parameters.
**/
-public class ParamDescrs extends Z3Object
-{
+public class ParamDescrs extends Z3Object {
/**
* validate a set of parameters.
**/
@@ -82,15 +81,8 @@ public class ParamDescrs extends Z3Object
* Retrieves a string representation of the ParamDescrs.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
}
ParamDescrs(Context ctx, long obj)
@@ -99,16 +91,12 @@ public class ParamDescrs extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getParamDescrsDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getParamDescrsDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index e3515bff6..ee3257db9 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -17,39 +17,15 @@ Notes:
package com.microsoft.z3;
-class ParamDescrsDecRefQueue extends IDecRefQueue
-{
+class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs> {
public ParamDescrsDecRefQueue()
{
super();
}
- 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 25d009b12..a76dd3cab 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -21,8 +21,7 @@ package com.microsoft.z3;
/**
* A ParameterSet represents a configuration in the form of Symbol/value pairs.
**/
-public class Params extends Z3Object
-{
+public class Params extends Z3Object {
/**
* Adds a parameter setting.
**/
@@ -115,13 +114,7 @@ public class Params extends Z3Object
@Override
public String toString()
{
- try
- {
- return Native.paramsToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.paramsToString(getContext().nCtx(), getNativeObject());
}
Params(Context ctx)
@@ -129,17 +122,14 @@ public class Params extends Z3Object
super(ctx, Native.mkParams(ctx.nCtx()));
}
+
@Override
- void incRef(long o)
- {
- getContext().getParamsDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.paramsIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getParamsDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getParamsDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index f989f8015..349713f67 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -17,39 +17,14 @@ Notes:
package com.microsoft.z3;
-class ParamsDecRefQueue extends IDecRefQueue
-{
+class ParamsDecRefQueue extends IDecRefQueue<Params> {
public ParamsDecRefQueue()
{
super();
}
- public ParamsDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.paramsIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.paramsDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.paramsDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/Pattern.java b/src/api/java/Pattern.java
index eb12b6448..852ffcd0f 100644
--- a/src/api/java/Pattern.java
+++ b/src/api/java/Pattern.java
@@ -53,13 +53,7 @@ public class Pattern extends AST
@Override
public String toString()
{
- try
- {
- return Native.patternToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.patternToString(getContext().nCtx(), getNativeObject());
}
Pattern(Context ctx, long obj)
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index bcaa76ce6..a36f3b64b 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -25,8 +25,7 @@ package com.microsoft.z3;
* also be obtained using the command {@code (help-tactic)} in the SMT 2.0
* front-end.
**/
-public class Probe extends Z3Object
-{
+public class Probe extends Z3Object {
/**
* Execute the probe over the goal.
*
@@ -46,22 +45,17 @@ public class Probe extends Z3Object
super(ctx, obj);
}
- Probe(Context ctx, String name)
- {
+ Probe(Context ctx, String name) {
super(ctx, Native.mkProbe(ctx.nCtx(), name));
}
@Override
- void incRef(long o)
- {
- getContext().getProbeDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.probeIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getProbeDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getProbeDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index 368bd5bba..b25446c0c 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -17,39 +17,16 @@ Notes:
package com.microsoft.z3;
-class ProbeDecRefQueue extends IDecRefQueue
+class ProbeDecRefQueue extends IDecRefQueue<Probe>
{
public ProbeDecRefQueue()
{
super();
}
- public ProbeDecRefQueue(int move_limit)
- {
- 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/RatNum.java b/src/api/java/RatNum.java
index f44823a2b..2bf1b28dd 100644
--- a/src/api/java/RatNum.java
+++ b/src/api/java/RatNum.java
@@ -75,15 +75,8 @@ public class RatNum extends RealExpr
* Returns a string representation of the numeral.
**/
@Override
- public String toString()
- {
- try
- {
- return Native.getNumeralString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ public String toString() {
+ return Native.getNumeralString(getContext().nCtx(), getNativeObject());
}
RatNum(Context ctx, long obj)
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index ea76637c8..a98fcbf94 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_lbool;
/**
* Solvers.
**/
-public class Solver extends Z3Object
-{
+public class Solver extends Z3Object {
/**
* A string that describes all available solver parameters.
**/
@@ -127,13 +126,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)
{
@@ -154,13 +153,13 @@ public class Solver extends Z3Object
* using the Boolean constant p.
*
* 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 {@link #assertAndTrack}
* and the Boolean literals
- * provided using {@link check} with assumptions.
+ * provided using {@link #check} with assumptions.
*/
public void assertAndTrack(BoolExpr constraint, BoolExpr p)
{
@@ -323,14 +322,8 @@ public class Solver extends Z3Object
@Override
public String toString()
{
- try
- {
- return Native
- .solverToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native
+ .solverToString(getContext().nCtx(), getNativeObject());
}
Solver(Context ctx, long obj)
@@ -339,16 +332,12 @@ public class Solver extends Z3Object
}
@Override
- void incRef(long o)
- {
- getContext().getSolverDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ void incRef() {
+ Native.solverIncRef(getContext().nCtx(), getNativeObject());
}
@Override
- void decRef(long o)
- {
- getContext().getSolverDRQ().add(o);
- super.decRef(o);
+ void addToReferenceQueue() {
+ getContext().getSolverDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index f4d5fb139..efa15d939 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -17,36 +17,11 @@ Notes:
package com.microsoft.z3;
-class SolverDecRefQueue extends IDecRefQueue
-{
+class SolverDecRefQueue extends IDecRefQueue<Solver> {
public SolverDecRefQueue() { super(); }
- public SolverDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
- protected void incRef(Context ctx, long obj)
- {
- try
- {
- Native.solverIncRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
+ protected void decRef(Context ctx, long obj) {
+ Native.solverDecRef(ctx.nCtx(), obj);
}
-
- @Override
- protected void decRef(Context ctx, long obj)
- {
- try
- {
- Native.solverDecRef(ctx.nCtx(), obj);
- } catch (Z3Exception e)
- {
- // OK.
- }
- }
-};
+}
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index e30e0b8b3..0763a69a3 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -82,15 +82,9 @@ public class Sort extends AST
/**
* A string representation of the sort.
**/
- public String toString()
- {
- try
- {
- return Native.sortToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ @Override
+ public String toString() {
+ return Native.sortToString(getContext().nCtx(), getNativeObject());
}
/**
@@ -101,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 5af0cf863..356cbeadb 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -20,8 +20,7 @@ package com.microsoft.z3;
/**
* Objects of this class track statistical information about solvers.
**/
-public class Statistics extends Z3Object
-{
+public class Statistics extends Z3Object {
/**
* Statistical data is organized into pairs of [Key, Entry], where every
* Entry is either a {@code DoubleEntry} or a {@code UIntEntry}
@@ -84,15 +83,9 @@ public class Statistics extends Z3Object
/**
* The string representation of the Entry.
**/
- public String toString()
- {
- try
- {
- return Key + ": " + getValueString();
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ @Override
+ public String toString() {
+ return Key + ": " + getValueString();
}
private boolean m_is_int = false;
@@ -118,15 +111,10 @@ public class Statistics extends Z3Object
/**
* A string representation of the statistical data.
**/
+ @Override
public String toString()
{
- try
- {
- return Native.statsToString(getContext().nCtx(), getNativeObject());
- } catch (Z3Exception e)
- {
- return "Z3Exception: " + e.getMessage();
- }
+ return Native.statsToString(getContext().nCtx(), getNativeObject());
}
/**
@@ -201,15 +189,13 @@ public class Statistics extends Z3Object
super(ctx, obj);
}
- void incRef(long o)
- {
- getContext().getStatisticsDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ @Override
+ void incRef() {
+ getContext().getStatisticsDRQ().storeReference(getContext(), this);
}
- void decRef(long o)
- {
- getContext().getStatisticsDRQ().add(o);
- super.decRef(o);
+ @Override
+ void addToReferenceQueue() {
+ Native.statsIncRef(getContext().nCtx(), getNativeObject());
}
}
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index 89c66a746..ed698e4ca 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/src/api/java/StatisticsDecRefQueue.java
@@ -17,37 +17,14 @@ Notes:
package com.microsoft.z3;
-class StatisticsDecRefQueue extends IDecRefQueue
-{
+class StatisticsDecRefQueue extends IDecRefQueue<Statistics> {
public StatisticsDecRefQueue()
{
super();
}
- public StatisticsDecRefQueue(int move_limit)
- {
- super(move_limit);
+ @Override
+ protected void decRef(Context ctx, long obj) {
+ Native.statsDecRef(ctx.nCtx(), obj);
}
-
- 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.
- }
- }
-};
+}
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..139894be1 100644
--- a/src/api/java/Symbol.java
+++ b/src/api/java/Symbol.java
@@ -22,8 +22,7 @@ import com.microsoft.z3.enumerations.Z3_symbol_kind;
/**
* Symbols are used to name several term and type constructors.
**/
-public class Symbol extends Z3Object
-{
+public class Symbol extends Z3Object {
/**
* The kind of the symbol (int or string)
**/
@@ -62,19 +61,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 +79,17 @@ public class Symbol extends Z3Object
super(ctx, obj);
}
+ @Override
+ void incRef() {
+ // Symbol does not require tracking.
+ }
+
+ @Override
+ void addToReferenceQueue() {
+
+ // 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..11d02ca73 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -24,8 +24,7 @@ package com.microsoft.z3;
* also be obtained using the command {@code (help-tactic)} in the SMT 2.0
* front-end.
**/
-public class Tactic extends Z3Object
-{
+public class Tactic extends Z3Object {
/**
* A string containing a description of parameters accepted by the tactic.
**/
@@ -92,15 +91,13 @@ public class Tactic extends Z3Object
super(ctx, Native.mkTactic(ctx.nCtx(), name));
}
- void incRef(long o)
- {
- getContext().getTacticDRQ().incAndClear(getContext(), o);
- super.incRef(o);
+ @Override
+ void incRef() {
+ Native.tacticIncRef(getContext().nCtx(), getNativeObject());
}
- void decRef(long o)
- {
- getContext().getTacticDRQ().add(o);
- super.decRef(o);
+ @Override
+ void addToReferenceQueue() {
+ getContext().getTacticDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 026760e46..8f151f25c 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/src/api/java/TacticDecRefQueue.java
@@ -17,37 +17,15 @@ Notes:
package com.microsoft.z3;
-class TacticDecRefQueue extends IDecRefQueue
-{
+class TacticDecRefQueue extends IDecRefQueue<Tactic> {
public TacticDecRefQueue()
{
super();
}
- public TacticDecRefQueue(int move_limit)
- {
- 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..7c5f606d9 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -21,88 +21,43 @@ 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();
+ Z3Object(Context ctx, long obj) {
m_ctx = ctx;
- }
-
- Z3Object(Context ctx, long obj)
- {
- ctx.m_refCount.incrementAndGet();
- m_ctx = ctx;
- incRef(obj);
+ checkNativeObject(obj);
m_n_obj = obj;
+ incRef();
+ addToReferenceQueue();
}
- void incRef(long o)
- {
- }
+ /**
+ * Add to ReferenceQueue for tracking reachability on the object and
+ * decreasing the reference count when the object is no longer reachable.
+ */
+ abstract void addToReferenceQueue();
- void decRef(long o)
- {
- }
+ /**
+ * Increment reference count on {@code this}.
+ */
+ abstract void incRef();
- 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 +76,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;
}