Skip to content

Commit

Permalink
Merge pull request #648 from cheshire/no_finalizers
Browse files Browse the repository at this point in the history
Replace finalizers with PhantomReferences in Java API
  • Loading branch information
Christoph M. Wintersteiger authored Jun 24, 2016
2 parents 1fb6721 + b086aac commit 3e96a79
Show file tree
Hide file tree
Showing 56 changed files with 525 additions and 1,242 deletions.
37 changes: 7 additions & 30 deletions src/api/java/AST.java
Original file line number Diff line number Diff line change
Expand Up @@ -175,15 +175,8 @@ public boolean isFuncDecl()
* 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());
}

/**
Expand All @@ -194,34 +187,18 @@ public String getSExpr()
return Native.astToString(getContext().nCtx(), getNativeObject());
}

AST(Context ctx)
{
super(ctx);
}

AST(Context ctx, long obj)
{
AST(Context ctx, long obj) {
super(ctx, obj);
}

@Override
void incRef(long o)
{
// Console.WriteLine("AST IncRef()");
if (getContext() == null || o == 0)
return;
getContext().getASTDRQ().incAndClear(getContext(), o);
super.incRef(o);
void incRef() {
Native.incRef(getContext().nCtx(), getNativeObject());
}

@Override
void decRef(long o)
{
// Console.WriteLine("AST DecRef()");
if (getContext() == null || o == 0)
return;
getContext().getASTDRQ().add(o);
super.decRef(o);
void addToReferenceQueue() {
getContext().getASTDRQ().storeReference(getContext(), this);
}

static AST create(Context ctx, long obj)
Expand Down
30 changes: 3 additions & 27 deletions src/api/java/ASTDecRefQueue.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,39 +17,15 @@

package com.microsoft.z3;

class ASTDecRefQueue extends IDecRefQueue
class ASTDecRefQueue extends IDecRefQueue<AST>
{
public ASTDecRefQueue()
{
super();
}

public ASTDecRefQueue(int move_limit)
{
super(move_limit);
}

@Override
protected void incRef(Context ctx, long obj)
{
try
{
Native.incRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}

@Override
protected void decRef(Context ctx, long obj)
{
try
{
Native.decRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
protected void decRef(Context ctx, long obj) {
Native.decRef(ctx.nCtx(), obj);
}
};
23 changes: 6 additions & 17 deletions src/api/java/ASTMap.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@
/**
* 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
Expand Down Expand Up @@ -104,13 +103,7 @@ public AST[] getKeys()
@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)
Expand All @@ -124,16 +117,12 @@ public String toString()
}

@Override
void incRef(long o)
{
getContext().getASTMapDRQ().incAndClear(getContext(), o);
super.incRef(o);
void incRef() {
Native.astMapIncRef(getContext().nCtx(), getNativeObject());
}

@Override
void decRef(long o)
{
getContext().getASTMapDRQ().add(o);
super.decRef(o);
void addToReferenceQueue() {
getContext().getASTMapDRQ().storeReference(getContext(), this);
}
}
28 changes: 8 additions & 20 deletions src/api/java/ASTVector.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,7 @@
/**
* Vectors of ASTs.
**/
public class ASTVector extends Z3Object
{
public class ASTVector extends Z3Object {
/**
* The size of the vector
**/
Expand Down Expand Up @@ -88,15 +87,8 @@ public ASTVector translate(Context ctx)
* 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)
Expand All @@ -110,19 +102,15 @@ public String toString()
}

@Override
void incRef(long o)
{
getContext().getASTVectorDRQ().incAndClear(getContext(), o);
super.incRef(o);
void incRef() {
Native.astVectorIncRef(getContext().nCtx(), getNativeObject());
}

@Override
void decRef(long o)
{
getContext().getASTVectorDRQ().add(o);
super.decRef(o);
void addToReferenceQueue() {
getContext().getASTVectorDRQ().storeReference(getContext(), this);
}

/**
* Translates the AST vector into an AST[]
* */
Expand Down
26 changes: 7 additions & 19 deletions src/api/java/ApplyResult.java
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@
* 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.
**/
Expand Down Expand Up @@ -64,15 +63,8 @@ public Model convertModel(int i, Model m)
* 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)
Expand All @@ -81,16 +73,12 @@ public String toString()
}

@Override
void incRef(long o)
{
getContext().getApplyResultDRQ().incAndClear(getContext(), o);
super.incRef(o);
void incRef() {
Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
}

@Override
void decRef(long o)
{
getContext().getApplyResultDRQ().add(o);
super.decRef(o);
void addToReferenceQueue() {
getContext().getApplyResultDRQ().storeReference(getContext(), this);
}
}
30 changes: 3 additions & 27 deletions src/api/java/ApplyResultDecRefQueue.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,39 +17,15 @@

package com.microsoft.z3;

class ApplyResultDecRefQueue extends IDecRefQueue
class ApplyResultDecRefQueue extends IDecRefQueue<ApplyResult>
{
public ApplyResultDecRefQueue()
{
super();
}

public ApplyResultDecRefQueue(int move_limit)
{
super(move_limit);
}

@Override
protected void incRef(Context ctx, long obj)
{
try
{
Native.applyResultIncRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}

@Override
protected void decRef(Context ctx, long obj)
{
try
{
Native.applyResultDecRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
protected void decRef(Context ctx, long obj) {
Native.applyResultDecRef(ctx.nCtx(), obj);
}
};
33 changes: 4 additions & 29 deletions src/api/java/AstMapDecRefQueue.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,39 +17,14 @@

package com.microsoft.z3;

class ASTMapDecRefQueue extends IDecRefQueue
{
class ASTMapDecRefQueue extends IDecRefQueue<ASTMap> {
public ASTMapDecRefQueue()
{
super();
}

public ASTMapDecRefQueue(int move_limit)
{
super(move_limit);
}

@Override
protected void incRef(Context ctx, long obj)
{
try
{
Native.astMapIncRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}

@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);
}
};
}
33 changes: 4 additions & 29 deletions src/api/java/AstVectorDecRefQueue.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,39 +17,14 @@

package com.microsoft.z3;

class ASTVectorDecRefQueue extends IDecRefQueue
{
class ASTVectorDecRefQueue extends IDecRefQueue<ASTVector> {
public ASTVectorDecRefQueue()
{
super();
}

public ASTVectorDecRefQueue(int move_limit)
{
super(move_limit);
}

@Override
protected void incRef(Context ctx, long obj)
{
try
{
Native.astVectorIncRef(ctx.nCtx(), obj);
} catch (Z3Exception e)
{
// OK.
}
}

@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);
}
};
}
8 changes: 1 addition & 7 deletions src/api/java/BitVecNum.java
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,7 @@ public BigInteger getBigInteger()
@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)
Expand Down
Loading

0 comments on commit 3e96a79

Please sign in to comment.