From dfc80d3b697125a2d4b3694786ef9507245c52a6 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Sun, 12 Jun 2016 14:14:11 +0200
Subject: [PATCH 01/10] Do not needlessly catch exceptions in Java bindings
A lot of existing code in Java bindings catches exceptions just to
silence them later.
This is:
a) Unnecessary: it is OK for a function to throw a RuntimeException
without declaring it.
b) Highly unidiomatic and not recommended by Java experts (see Effective
Java and others)
c) Confusing as has the potential to hide the existing bugs and have
them resurface at the most inconvenient/unexpected moment.
---
src/api/java/AST.java | 11 ++---------
src/api/java/ASTMap.java | 8 +-------
src/api/java/ASTVector.java | 11 ++---------
src/api/java/ApplyResult.java | 11 ++---------
src/api/java/BitVecNum.java | 8 +-------
src/api/java/FPNum.java | 8 +-------
src/api/java/FiniteDomainNum.java | 8 +-------
src/api/java/Fixedpoint.java | 8 +-------
src/api/java/FuncDecl.java | 8 +-------
src/api/java/Goal.java | 11 ++---------
src/api/java/IntNum.java | 11 ++---------
src/api/java/Model.java | 11 ++---------
src/api/java/ParamDescrs.java | 11 ++---------
src/api/java/Params.java | 8 +-------
src/api/java/Pattern.java | 8 +-------
src/api/java/RatNum.java | 11 ++---------
src/api/java/Solver.java | 10 ++--------
src/api/java/Sort.java | 12 +++---------
src/api/java/Statistics.java | 21 +++++----------------
19 files changed, 34 insertions(+), 161 deletions(-)
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index e84dc8c81..f43aa85d2 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());
}
/**
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index 7bc485bf5..a6201d8a0 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -104,13 +104,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)
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index ab99e2aee..da1ab0f12 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -88,15 +88,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)
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index 84c63e966..f598c9504 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -64,15 +64,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)
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/FPNum.java b/src/api/java/FPNum.java
index 69a44c559..9aeb41759 100644
--- a/src/api/java/FPNum.java
+++ b/src/api/java/FPNum.java
@@ -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..2ff10a1f3 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();
- }
}
/**
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/Goal.java b/src/api/java/Goal.java
index 46b04f6bf..e60971179 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -211,15 +211,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());
}
/**
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/Model.java b/src/api/java/Model.java
index 0695d7cf1..1bf77d246 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -283,15 +283,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)
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 8f8c6df0b..f265fb19e 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -82,15 +82,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)
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index 25d009b12..4be36c23d 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -115,13 +115,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)
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/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..431811b8d 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -323,14 +323,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)
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index e30e0b8b3..30a43e7dd 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());
}
/**
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 5af0cf863..1e842a892 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -84,15 +84,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 +112,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());
}
/**
From 495ef0f055f300089ec57f7aa71c2cc48d0fd402 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Sun, 12 Jun 2016 14:18:13 +0200
Subject: [PATCH 02/10] Java bindings with no finalizers
Replacing finalizers with PhantomReferences, required quite a lot of
changes to the codebase.
---
src/api/java/AST.java | 25 +--
src/api/java/ASTDecRefQueue.java | 25 +--
src/api/java/ASTMap.java | 11 +-
src/api/java/ASTVector.java | 11 +-
src/api/java/ApplyResult.java | 14 +-
src/api/java/ApplyResultDecRefQueue.java | 25 +--
src/api/java/AstMapDecRefQueue.java | 25 +--
src/api/java/AstVectorDecRefQueue.java | 25 +--
src/api/java/BoolExpr.java | 10 +-
src/api/java/Constructor.java | 44 ++---
src/api/java/ConstructorList.java | 25 +--
src/api/java/Context.java | 176 +++++++++----------
src/api/java/EnumSort.java | 12 +-
src/api/java/Expr.java | 25 +--
src/api/java/FPNum.java | 6 +-
src/api/java/Fixedpoint.java | 13 +-
src/api/java/FixedpointDecRefQueue.java | 21 +--
src/api/java/FuncInterp.java | 86 +++------
src/api/java/FuncInterpDecRefQueue.java | 25 +--
src/api/java/FuncInterpEntryDecRefQueue.java | 25 +--
src/api/java/Goal.java | 25 +--
src/api/java/GoalDecRefQueue.java | 23 +--
src/api/java/IDecRefQueue.java | 59 ++++---
src/api/java/IDisposable.java | 25 ---
src/api/java/InterpolationContext.java | 21 ++-
src/api/java/ListSort.java | 15 +-
src/api/java/Model.java | 14 +-
src/api/java/ModelDecRefQueue.java | 25 +--
src/api/java/Optimize.java | 15 +-
src/api/java/OptimizeDecRefQueue.java | 26 +--
src/api/java/ParamDescrs.java | 14 +-
src/api/java/ParamDescrsDecRefQueue.java | 25 +--
src/api/java/Params.java | 14 +-
src/api/java/ParamsDecRefQueue.java | 25 +--
src/api/java/Probe.java | 11 +-
src/api/java/ProbeDecRefQueue.java | 22 +--
src/api/java/Quantifier.java | 73 ++++----
src/api/java/Solver.java | 20 +--
src/api/java/SolverDecRefQueue.java | 25 +--
src/api/java/Sort.java | 1 +
src/api/java/Statistics.java | 14 +-
src/api/java/StatisticsDecRefQueue.java | 25 +--
src/api/java/StringSymbol.java | 4 +-
src/api/java/Symbol.java | 25 ++-
src/api/java/Tactic.java | 11 +-
src/api/java/TacticDecRefQueue.java | 25 +--
src/api/java/TupleSort.java | 8 +-
src/api/java/Z3Object.java | 88 ++--------
48 files changed, 368 insertions(+), 939 deletions(-)
delete mode 100644 src/api/java/IDisposable.java
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<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);
- }
-
- @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<AST>
{
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<ApplyResult>
{
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<ASTMap>
{
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<ASTVector>
{
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<String, String> settings)
+ public static Context mkContext(Map<String, String> settings)
{
- super();
- synchronized (creation_lock) {
+ 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.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<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);
@@ -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<Fixedpoint>
{
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<FuncInterp>
{
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<FuncInterp.Entry>
{
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<Goal>
{
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<T extends Z3Object>
{
- protected final Object m_lock = new Object();
- protected LinkedList<Long> m_queue = new LinkedList<Long>();
- protected int m_move_limit;
+ private final int m_move_limit;
+
+ // TODO: problem: ReferenceQueue has no API to return length.
+ private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
+ private int queueSize = 0;
+ private final Map<PhantomReference<T>, 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<T> 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<? 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/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 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<Model>
{
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<Optimize> {
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<ParamDescrs>
{
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<Params>
{
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<Probe>
{
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<Solver>
{
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<Statistics>
{
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<Tactic> {
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;
}
From 5657399d554f0c67715855840d2cee09e20c5ed1 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Sun, 12 Jun 2016 20:39:54 +0200
Subject: [PATCH 03/10] Bugfix for incorrect order of operations.
---
src/api/java/Z3Object.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index 6fd12bfba..f982bba1c 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -29,8 +29,8 @@ public abstract class Z3Object {
Z3Object(Context ctx, long obj) {
m_ctx = ctx;
checkNativeObject(obj);
- incRef(obj);
m_n_obj = obj;
+ incRef(obj);
}
/**
From 2a347f04bf79a6e223899cfba6690123d388b9f3 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Sun, 12 Jun 2016 21:00:51 +0200
Subject: [PATCH 04/10] Java API: FuncInterp.Entry should be an inner static
class
...as it does not use any fields of the outer FuncInterp object.
---
src/api/java/FuncInterp.java | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index c84979aa1..52f09c5a4 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -28,8 +28,8 @@ 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.
*
From 22ffd65d1e2a02583128a9a19a547d8b340e2547 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Sun, 12 Jun 2016 21:01:58 +0200
Subject: [PATCH 05/10] Java API: split incRef into incRef and
addToReferenceQueue
One method should do one thing only, it's easy to mix things up
otherwise.
---
src/api/java/AST.java | 9 ++++---
src/api/java/ASTMap.java | 12 +++++----
src/api/java/ASTVector.java | 12 +++++----
src/api/java/ApplyResult.java | 11 ++++++---
src/api/java/Constructor.java | 7 ++++--
src/api/java/ConstructorList.java | 7 +++++-
src/api/java/Fixedpoint.java | 8 ++++--
src/api/java/FixedpointDecRefQueue.java | 4 +--
src/api/java/FuncInterp.java | 33 +++++++++++++++----------
src/api/java/Goal.java | 11 ++++++---
src/api/java/Model.java | 11 ++++++---
src/api/java/Optimize.java | 8 ++++--
src/api/java/ParamDescrs.java | 11 ++++++---
src/api/java/Params.java | 12 ++++++---
src/api/java/Probe.java | 15 +++++------
src/api/java/Solver.java | 17 +++++++------
src/api/java/Statistics.java | 11 ++++++---
src/api/java/Symbol.java | 11 ++++++---
src/api/java/Tactic.java | 12 +++++----
src/api/java/Z3Object.java | 15 +++++++----
20 files changed, 150 insertions(+), 87 deletions(-)
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 4b5b37d46..e1cde837f 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -192,9 +192,12 @@ public class AST extends Z3Object implements Comparable<AST>
}
@Override
- void incRef(long o)
- {
- Native.incRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.incRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getASTDRQ().storeReference(getContext(), this);
}
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index b4ae7102a..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
@@ -118,9 +117,12 @@ class ASTMap extends Z3Object
}
@Override
- void incRef(long o)
- {
- Native.astMapIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.astMapIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getASTMapDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 7c5ca1067..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
**/
@@ -103,9 +102,12 @@ public class ASTVector extends Z3Object
}
@Override
- void incRef(long o)
- {
- Native.astVectorIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getASTVectorDRQ().storeReference(getContext(), this);
}
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index 8b3c1daf6..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.
**/
@@ -74,8 +73,12 @@ public class ApplyResult extends Z3Object
}
@Override
- void incRef(long o) {
- Native.applyResultIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getApplyResultDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Constructor.java b/src/api/java/Constructor.java
index 28558b15a..87ab86c3f 100644
--- a/src/api/java/Constructor.java
+++ b/src/api/java/Constructor.java
@@ -85,9 +85,12 @@ public class Constructor extends Z3Object {
}
@Override
- void incRef(long o) {
-
+ void incRef() {
// Datatype constructors are not reference counted.
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getConstructorDRQ().storeReference(getContext(), this);
}
diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java
index 3f1835082..c79e08d9e 100644
--- a/src/api/java/ConstructorList.java
+++ b/src/api/java/ConstructorList.java
@@ -28,7 +28,12 @@ public class ConstructorList extends Z3Object {
}
@Override
- void incRef(long o) {
+ void incRef() {
+ // Constructor lists are not reference counted.
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getConstructorListDRQ().storeReference(getContext(), this);
}
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 5a7958364..876345f1e 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -349,8 +349,12 @@ public class Fixedpoint extends Z3Object
}
@Override
- void incRef(long o) {
- Native.fixedpointIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.fixedpointIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getFixedpointDRQ().storeReference(getContext(), this);
}
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index d5ae79a2b..3cba67ced 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -17,8 +17,7 @@ Notes:
package com.microsoft.z3;
-class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint>
-{
+class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
public FixedpointDecRefQueue()
{
super();
@@ -29,7 +28,6 @@ class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint>
super(move_limit);
}
-
@Override
protected void decRef(Context ctx, long obj)
{
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index 52f09c5a4..b5873d98e 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -22,8 +22,8 @@ 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.
@@ -32,10 +32,10 @@ public class FuncInterp 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();
@@ -81,14 +81,17 @@ public class FuncInterp extends Z3Object
return res + getValue() + "]";
}
- Entry(Context ctx, long obj)
- {
+ Entry(Context ctx, long obj) {
super(ctx, obj);
}
@Override
- void incRef(long o) {
- Native.funcEntryIncRef(getContext().nCtx(), o);;
+ void incRef() {
+ Native.funcEntryIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getFuncEntryDRQ().storeReference(getContext(), this);
}
}
@@ -176,8 +179,12 @@ public class FuncInterp extends Z3Object
}
@Override
- void incRef(long o) {
- Native.funcInterpIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.funcInterpIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getFuncInterpDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index a6d41ccd2..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
@@ -242,8 +241,12 @@ public class Goal extends Z3Object
}
@Override
- void incRef(long o) {
- Native.goalIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.goalIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getGoalDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index fc6c6046b..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.
@@ -293,8 +292,12 @@ public class Model extends Z3Object
}
@Override
- void incRef(long o) {
- Native.modelIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.modelIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getModelDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index a5705a388..ea100d1ca 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -266,8 +266,12 @@ public class Optimize extends Z3Object
}
@Override
- void incRef(long o) {
- Native.optimizeIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.optimizeIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getOptimizeDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index f90e4dd99..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.
**/
@@ -92,8 +91,12 @@ public class ParamDescrs extends Z3Object
}
@Override
- void incRef(long o) {
- Native.paramDescrsIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getParamDescrsDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index e3b143371..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.
**/
@@ -123,9 +122,14 @@ public class Params extends Z3Object
super(ctx, Native.mkParams(ctx.nCtx()));
}
+
@Override
- void incRef(long o) {
- Native.paramsIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.paramsIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getParamsDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index 6983613c1..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,15 +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)
- {
- Native.probeIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.probeIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getProbeDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 5d538b2f3..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.
**/
@@ -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)
{
@@ -333,8 +332,12 @@ public class Solver extends Z3Object
}
@Override
- void incRef(long o) {
- Native.solverIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.solverIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getSolverDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index d2ba2bbd3..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}
@@ -191,8 +190,12 @@ public class Statistics extends Z3Object
}
@Override
- void incRef(long o) {
- Native.statsIncRef(getContext().nCtx(), o);
+ void incRef() {
getContext().getStatisticsDRQ().storeReference(getContext(), this);
}
+
+ @Override
+ void addToReferenceQueue() {
+ Native.statsIncRef(getContext().nCtx(), getNativeObject());
+ }
}
diff --git a/src/api/java/Symbol.java b/src/api/java/Symbol.java
index 21925b099..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)
**/
@@ -81,7 +80,13 @@ public class Symbol extends Z3Object
}
@Override
- void incRef(long o) {
+ void incRef() {
+ // Symbol does not require tracking.
+ }
+
+ @Override
+ void addToReferenceQueue() {
+
// Symbol does not require tracking.
}
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index f7e030f04..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.
**/
@@ -93,9 +92,12 @@ public class Tactic extends Z3Object
}
@Override
- void incRef(long o)
- {
- Native.tacticIncRef(getContext().nCtx(), o);
+ void incRef() {
+ Native.tacticIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
getContext().getTacticDRQ().storeReference(getContext(), this);
}
}
diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java
index f982bba1c..7c5f606d9 100644
--- a/src/api/java/Z3Object.java
+++ b/src/api/java/Z3Object.java
@@ -30,15 +30,20 @@ public abstract class Z3Object {
m_ctx = ctx;
checkNativeObject(obj);
m_n_obj = obj;
- incRef(obj);
+ incRef();
+ addToReferenceQueue();
}
/**
- * Increment reference count on {@code o}.
- *
- * @param o Z3 object.
+ * Add to ReferenceQueue for tracking reachability on the object and
+ * decreasing the reference count when the object is no longer reachable.
*/
- abstract void incRef(long o);
+ abstract void addToReferenceQueue();
+
+ /**
+ * Increment reference count on {@code this}.
+ */
+ abstract void incRef();
/**
* This function is provided for overriding, and a child class
From 27aa37946e56a4d9722de416791a2e40dc5d2054 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Mon, 13 Jun 2016 12:09:34 +0200
Subject: [PATCH 06/10] Do not lock on context creation and deletion.
---
src/api/java/Context.java | 24 +++++++-----------------
1 file changed, 7 insertions(+), 17 deletions(-)
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 41fb027fe..e66920441 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -31,12 +31,7 @@ public class Context implements AutoCloseable {
static final Object creation_lock = new Object();
public static Context mkContext() {
- long m_ctx;
- synchronized (creation_lock) {
- m_ctx = Native.mkContextRc(0);
- // TODO: then adding settings will not be under the lock.
- }
- return new Context(m_ctx);
+ return new Context(Native.mkContextRc(0));
}
@@ -59,14 +54,11 @@ public class Context implements AutoCloseable {
**/
public static Context mkContext(Map<String, String> settings)
{
- 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.mkContextRc(cfg);
- Native.delConfig(cfg);
- }
+ long cfg = Native.mkConfig();
+ for (Map.Entry<String, String> kv : settings.entrySet())
+ Native.setParamValue(cfg, kv.getKey(), kv.getValue());
+ long m_ctx = Native.mkContextRc(cfg);
+ Native.delConfig(cfg);
return new Context(m_ctx);
}
@@ -4047,8 +4039,6 @@ public class Context implements AutoCloseable {
m_realSort = null;
m_stringSort = null;
- synchronized (creation_lock) {
- Native.delContext(m_ctx);
- }
+ Native.delContext(m_ctx);
}
}
From 26d6c99aac2ecf1304f695c75540f47715e0ce6d Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Mon, 13 Jun 2016 12:11:03 +0200
Subject: [PATCH 07/10] Typo in Javadoc.
---
src/api/java/IDecRefQueue.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index b0a93b552..f3cea7249 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -46,7 +46,7 @@ public abstract class IDecRefQueue<T extends Z3Object>
/**
* 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.
+ * This function should always be called on the {@code ctx} thread.
*
* @param ctx Z3 context.
* @param obj Pointer to a Z3 object.
From a914822346179531cf36c79809e5f01842267c84 Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Mon, 13 Jun 2016 12:18:31 +0200
Subject: [PATCH 08/10] JavaAPI: DecRefQueue -- do not use move_limit for now.
---
src/api/java/ASTDecRefQueue.java | 5 ---
src/api/java/ApplyResultDecRefQueue.java | 5 ---
src/api/java/AstMapDecRefQueue.java | 10 ++----
src/api/java/AstVectorDecRefQueue.java | 10 ++----
src/api/java/ConstructorDecRefQueue.java | 12 +++++++
src/api/java/ConstructorListDecRefQueue.java | 12 +++++++
src/api/java/Context.java | 34 ++++++++++----------
src/api/java/FixedpointDecRefQueue.java | 5 ---
src/api/java/FuncInterpDecRefQueue.java | 5 ---
src/api/java/FuncInterpEntryDecRefQueue.java | 10 ++----
src/api/java/GoalDecRefQueue.java | 10 ++----
src/api/java/IDecRefQueue.java | 23 ++++---------
src/api/java/ModelDecRefQueue.java | 10 ++----
src/api/java/OptimizeDecRefQueue.java | 5 ---
src/api/java/ParamDescrsDecRefQueue.java | 9 ++----
src/api/java/ParamsDecRefQueue.java | 10 ++----
src/api/java/ProbeDecRefQueue.java | 5 ---
src/api/java/SolverDecRefQueue.java | 10 ++----
src/api/java/StatisticsDecRefQueue.java | 10 ++----
src/api/java/TacticDecRefQueue.java | 5 ---
20 files changed, 65 insertions(+), 140 deletions(-)
create mode 100644 src/api/java/ConstructorDecRefQueue.java
create mode 100644 src/api/java/ConstructorListDecRefQueue.java
diff --git a/src/api/java/ASTDecRefQueue.java b/src/api/java/ASTDecRefQueue.java
index d462e16d5..b0a6fa217 100644
--- a/src/api/java/ASTDecRefQueue.java
+++ b/src/api/java/ASTDecRefQueue.java
@@ -24,11 +24,6 @@ class ASTDecRefQueue extends IDecRefQueue<AST>
super();
}
- public ASTDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.decRef(ctx.nCtx(), obj);
diff --git a/src/api/java/ApplyResultDecRefQueue.java b/src/api/java/ApplyResultDecRefQueue.java
index d28ff755e..e1a660781 100644
--- a/src/api/java/ApplyResultDecRefQueue.java
+++ b/src/api/java/ApplyResultDecRefQueue.java
@@ -24,11 +24,6 @@ class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
super();
}
- public ApplyResultDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
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 234b7eec4..6c96970b7 100644
--- a/src/api/java/AstMapDecRefQueue.java
+++ b/src/api/java/AstMapDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class ASTMapDecRefQueue extends IDecRefQueue<ASTMap>
-{
+class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
public ASTMapDecRefQueue()
{
super();
}
- public ASTMapDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
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 3a486ee06..e7ce3e33e 100644
--- a/src/api/java/AstVectorDecRefQueue.java
+++ b/src/api/java/AstVectorDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector>
-{
+class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
public ASTVectorDecRefQueue()
{
super();
}
- public ASTVectorDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.astVectorDecRef(ctx.nCtx(), obj);
}
-};
+}
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/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 e66920441..1e2b5d4fa 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3905,24 +3905,24 @@ public class Context implements AutoCloseable {
}
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 ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue(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(10);
+ new ConstructorListDecRefQueue();
public IDecRefQueue<Constructor> getConstructorDRQ() {
return m_Constructor_DRQ;
diff --git a/src/api/java/FixedpointDecRefQueue.java b/src/api/java/FixedpointDecRefQueue.java
index 3cba67ced..69ed82092 100644
--- a/src/api/java/FixedpointDecRefQueue.java
+++ b/src/api/java/FixedpointDecRefQueue.java
@@ -23,11 +23,6 @@ class FixedpointDecRefQueue extends IDecRefQueue<Fixedpoint> {
super();
}
- public FixedpointDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj)
{
diff --git a/src/api/java/FuncInterpDecRefQueue.java b/src/api/java/FuncInterpDecRefQueue.java
index 136c07b6a..d8715bd0e 100644
--- a/src/api/java/FuncInterpDecRefQueue.java
+++ b/src/api/java/FuncInterpDecRefQueue.java
@@ -24,11 +24,6 @@ class FuncInterpDecRefQueue extends IDecRefQueue<FuncInterp>
super();
}
- public FuncInterpDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
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 8f6741ba0..a4d8a0690 100644
--- a/src/api/java/FuncInterpEntryDecRefQueue.java
+++ b/src/api/java/FuncInterpEntryDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry>
-{
+class FuncInterpEntryDecRefQueue extends IDecRefQueue<FuncInterp.Entry> {
public FuncInterpEntryDecRefQueue()
{
super();
}
- public FuncInterpEntryDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.funcEntryDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/GoalDecRefQueue.java b/src/api/java/GoalDecRefQueue.java
index 724ec003f..90bad1fb1 100644
--- a/src/api/java/GoalDecRefQueue.java
+++ b/src/api/java/GoalDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class GoalDecRefQueue extends IDecRefQueue<Goal>
-{
+class GoalDecRefQueue extends IDecRefQueue<Goal> {
public GoalDecRefQueue()
{
super();
}
- public GoalDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.goalDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index f3cea7249..5a80adf5f 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -23,25 +23,16 @@ import java.lang.ref.ReferenceQueue;
import java.util.IdentityHashMap;
import java.util.Map;
-public abstract class IDecRefQueue<T extends Z3Object>
-{
- private final int m_move_limit;
-
- // TODO: problem: ReferenceQueue has no API to return length.
+/**
+ *
+ * @param <T>
+ */
+public abstract class IDecRefQueue<T extends Z3Object> {
private final ReferenceQueue<T> referenceQueue = new ReferenceQueue<>();
- private int queueSize = 0;
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;
- }
+ protected IDecRefQueue() {}
/**
* An implementation of this method should decrement the reference on a
@@ -56,8 +47,6 @@ public abstract class IDecRefQueue<T extends Z3Object>
public void storeReference(Context ctx, T obj) {
PhantomReference<T> ref = new PhantomReference<>(obj, referenceQueue);
referenceMap.put(ref, obj.getNativeObject());
-
- // TODO: use move_limit, somehow get the size of referenceQueue.
clear(ctx);
}
diff --git a/src/api/java/ModelDecRefQueue.java b/src/api/java/ModelDecRefQueue.java
index 6b141078e..f1b7c3fdd 100644
--- a/src/api/java/ModelDecRefQueue.java
+++ b/src/api/java/ModelDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class ModelDecRefQueue extends IDecRefQueue<Model>
-{
+class ModelDecRefQueue extends IDecRefQueue<Model> {
public ModelDecRefQueue()
{
super();
}
- public ModelDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.modelDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/OptimizeDecRefQueue.java b/src/api/java/OptimizeDecRefQueue.java
index a06165f3e..0acf20068 100644
--- a/src/api/java/OptimizeDecRefQueue.java
+++ b/src/api/java/OptimizeDecRefQueue.java
@@ -23,11 +23,6 @@ class OptimizeDecRefQueue extends IDecRefQueue<Optimize> {
super();
}
- public OptimizeDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.optimizeDecRef(ctx.nCtx(), obj);
diff --git a/src/api/java/ParamDescrsDecRefQueue.java b/src/api/java/ParamDescrsDecRefQueue.java
index ab7f4ddd6..ee3257db9 100644
--- a/src/api/java/ParamDescrsDecRefQueue.java
+++ b/src/api/java/ParamDescrsDecRefQueue.java
@@ -17,20 +17,15 @@ Notes:
package com.microsoft.z3;
-class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs>
-{
+class ParamDescrsDecRefQueue extends IDecRefQueue<ParamDescrs> {
public ParamDescrsDecRefQueue()
{
super();
}
- public ParamDescrsDecRefQueue(int move_limit) {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj)
{
Native.paramDescrsDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/ParamsDecRefQueue.java b/src/api/java/ParamsDecRefQueue.java
index b5281ecbc..349713f67 100644
--- a/src/api/java/ParamsDecRefQueue.java
+++ b/src/api/java/ParamsDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class ParamsDecRefQueue extends IDecRefQueue<Params>
-{
+class ParamsDecRefQueue extends IDecRefQueue<Params> {
public ParamsDecRefQueue()
{
super();
}
- public ParamsDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.paramsDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/ProbeDecRefQueue.java b/src/api/java/ProbeDecRefQueue.java
index 3f78c6288..b25446c0c 100644
--- a/src/api/java/ProbeDecRefQueue.java
+++ b/src/api/java/ProbeDecRefQueue.java
@@ -24,11 +24,6 @@ class ProbeDecRefQueue extends IDecRefQueue<Probe>
super();
}
- public ProbeDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj)
{
diff --git a/src/api/java/SolverDecRefQueue.java b/src/api/java/SolverDecRefQueue.java
index 106892fec..efa15d939 100644
--- a/src/api/java/SolverDecRefQueue.java
+++ b/src/api/java/SolverDecRefQueue.java
@@ -17,17 +17,11 @@ Notes:
package com.microsoft.z3;
-class SolverDecRefQueue extends IDecRefQueue<Solver>
-{
+class SolverDecRefQueue extends IDecRefQueue<Solver> {
public SolverDecRefQueue() { super(); }
- public SolverDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj) {
Native.solverDecRef(ctx.nCtx(), obj);
}
-};
+}
diff --git a/src/api/java/StatisticsDecRefQueue.java b/src/api/java/StatisticsDecRefQueue.java
index fecf52267..ed698e4ca 100644
--- a/src/api/java/StatisticsDecRefQueue.java
+++ b/src/api/java/StatisticsDecRefQueue.java
@@ -17,20 +17,14 @@ Notes:
package com.microsoft.z3;
-class StatisticsDecRefQueue extends IDecRefQueue<Statistics>
-{
+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);
}
-};
+}
diff --git a/src/api/java/TacticDecRefQueue.java b/src/api/java/TacticDecRefQueue.java
index 079904175..8f151f25c 100644
--- a/src/api/java/TacticDecRefQueue.java
+++ b/src/api/java/TacticDecRefQueue.java
@@ -23,11 +23,6 @@ class TacticDecRefQueue extends IDecRefQueue<Tactic> {
super();
}
- public TacticDecRefQueue(int move_limit)
- {
- super(move_limit);
- }
-
@Override
protected void decRef(Context ctx, long obj)
{
From b65d83aacfea8adacebe7d2919c55bdedb475a8c Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Mon, 13 Jun 2016 12:22:32 +0200
Subject: [PATCH 09/10] Java API: explain the phantom references mechanics in
Javadoc.
---
src/api/java/IDecRefQueue.java | 11 ++++++++++-
1 file changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index 5a80adf5f..2deb9c0f9 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -24,8 +24,17 @@ import java.util.IdentityHashMap;
import java.util.Map;
/**
+ * A queue to handle management of native memory.
*
- * @param <T>
+ * <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<>();
From b086aac45ff1069159f35bd5243ca6d479963ebc Mon Sep 17 00:00:00 2001
From: George Karpenkov <george@metaworld.me>
Date: Thu, 16 Jun 2016 18:21:55 +0200
Subject: [PATCH 10/10] Use constructors instead of static methods for
Context.java.
---
src/api/java/Context.java | 24 +++++++++---------------
1 file changed, 9 insertions(+), 15 deletions(-)
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 1e2b5d4fa..39d35d9d3 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -30,8 +30,9 @@ public class Context implements AutoCloseable {
private final long m_ctx;
static final Object creation_lock = new Object();
- public static Context mkContext() {
- return new Context(Native.mkContextRc(0));
+ public Context () {
+ m_ctx = Native.mkContextRc(0);
+ init();
}
@@ -52,24 +53,17 @@ public class Context implements AutoCloseable {
* 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 static Context mkContext(Map<String, String> settings)
- {
+ public Context(Map<String, String> settings) {
long cfg = Native.mkConfig();
- for (Map.Entry<String, String> kv : settings.entrySet())
+ for (Map.Entry<String, String> kv : settings.entrySet()) {
Native.setParamValue(cfg, kv.getKey(), kv.getValue());
- long m_ctx = Native.mkContextRc(cfg);
+ }
+ m_ctx = Native.mkContextRc(cfg);
Native.delConfig(cfg);
- return new Context(m_ctx);
+ init();
}
- /**
- * Constructor.
- **/
- protected Context(long m_ctx)
- {
- this.m_ctx = m_ctx;
-
- // Code which used to be in "initContext".
+ private void init() {
setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT);
Native.setInternalErrorHandler(m_ctx);
}