mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 04:28:17 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-06-29 16:53:46 -07:00
parent c2f9d35d59 37c9a31296
commit fd95a9e061
4 changed files with 67 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/api/java/Context.java
View file

@ -4017,21 +4017,21 @@ public class Context implements AutoCloseable {
@Override
public void close()
{
m_AST_DRQ.clear(this);
m_ASTMap_DRQ.clear(this);
m_ASTVector_DRQ.clear(this);
m_ApplyResult_DRQ.clear(this);
m_FuncEntry_DRQ.clear(this);
m_FuncInterp_DRQ.clear(this);
m_Goal_DRQ.clear(this);
m_Model_DRQ.clear(this);
m_Params_DRQ.clear(this);
m_Probe_DRQ.clear(this);
m_Solver_DRQ.clear(this);
m_Optimize_DRQ.clear(this);
m_Statistics_DRQ.clear(this);
m_Tactic_DRQ.clear(this);
m_Fixedpoint_DRQ.clear(this);
m_AST_DRQ.forceClear(this);
m_ASTMap_DRQ.forceClear(this);
m_ASTVector_DRQ.forceClear(this);
m_ApplyResult_DRQ.forceClear(this);
m_FuncEntry_DRQ.forceClear(this);
m_FuncInterp_DRQ.forceClear(this);
m_Goal_DRQ.forceClear(this);
m_Model_DRQ.forceClear(this);
m_Params_DRQ.forceClear(this);
m_Probe_DRQ.forceClear(this);
m_Solver_DRQ.forceClear(this);
m_Optimize_DRQ.forceClear(this);
m_Statistics_DRQ.forceClear(this);
m_Tactic_DRQ.forceClear(this);
m_Fixedpoint_DRQ.forceClear(this);
m_boolSort = null;
m_intSort = null;

33
src/api/java/Fixedpoint.java
View file

@ -87,12 +87,11 @@ public class Fixedpoint extends Z3Object
/**
* Add rule into the fixedpoint solver.
*
*
* @param name Nullable rule name.
* @throws Z3Exception
**/
public void addRule(BoolExpr rule, Symbol name)
{
public void addRule(BoolExpr rule, Symbol name) {
getContext().checkContextMatch(rule);
Native.fixedpointAddRule(getContext().nCtx(), getNativeObject(),
rule.getNativeObject(), AST.getNativeObject(name));
@ -103,11 +102,10 @@ public class Fixedpoint extends Z3Object
*
* @throws Z3Exception
**/
public void addFact(FuncDecl pred, int ... args)
{
public void addFact(FuncDecl pred, int ... args) {
getContext().checkContextMatch(pred);
Native.fixedpointAddFact(getContext().nCtx(), getNativeObject(),
pred.getNativeObject(), (int) args.length, args);
pred.getNativeObject(), args.length, args);
}
/**
@ -119,9 +117,7 @@ public class Fixedpoint extends Z3Object
*
* @throws Z3Exception
**/
public Status query(BoolExpr query)
{
public Status query(BoolExpr query) {
getContext().checkContextMatch(query);
Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQuery(getContext().nCtx(),
getNativeObject(), query.getNativeObject()));
@ -144,9 +140,7 @@ public class Fixedpoint extends Z3Object
*
* @throws Z3Exception
**/
public Status query(FuncDecl[] relations)
{
public Status query(FuncDecl[] relations) {
getContext().checkContextMatch(relations);
Z3_lbool r = Z3_lbool.fromInt(Native.fixedpointQueryRelations(getContext()
.nCtx(), getNativeObject(), AST.arrayLength(relations), AST
@ -166,8 +160,7 @@ public class Fixedpoint extends Z3Object
* Creates a backtracking point.
* @see #pop
**/
public void push()
{
public void push() {
Native.fixedpointPush(getContext().nCtx(), getNativeObject());
}
@ -178,19 +171,17 @@ public class Fixedpoint extends Z3Object
*
* @see #push
**/
public void pop()
{
public void pop() {
Native.fixedpointPop(getContext().nCtx(), getNativeObject());
}
/**
* Update named rule into in the fixedpoint solver.
*
*
* @param name Nullable rule name.
* @throws Z3Exception
**/
public void updateRule(BoolExpr rule, Symbol name)
{
public void updateRule(BoolExpr rule, Symbol name) {
getContext().checkContextMatch(rule);
Native.fixedpointUpdateRule(getContext().nCtx(), getNativeObject(),
rule.getNativeObject(), AST.getNativeObject(name));

13
src/api/java/IDecRefQueue.java
View file

@ -59,6 +59,9 @@ public abstract class IDecRefQueue<T extends Z3Object> {
clear(ctx);
}
/**
* Clean all references currently in {@code referenceQueue}.
*/
protected void clear(Context ctx)
{
Reference<? extends T> ref;
@ -67,4 +70,14 @@ public abstract class IDecRefQueue<T extends Z3Object> {
decRef(ctx, z3ast);
}
}
/**
* Clean all references stored in {@code referenceMap},
* <b>regardless</b> of whether they are in {@code referenceMap} or not.
*/
public void forceClear(Context ctx) {
for (long ref : referenceMap.values()) {
decRef(ctx, ref);
}
}
}

38
src/api/java/Quantifier.java
View file

@ -145,20 +145,28 @@ public class Quantifier extends BoolExpr
.nCtx(), getNativeObject()));
}
/**
* Create a quantified expression.
*
* @param patterns Nullable patterns
* @param noPatterns Nullable noPatterns
* @param quantifierID Nullable quantifierID
* @param skolemID Nullable skolemID
*/
public static Quantifier of(
Context ctx, boolean isForall, Sort[] sorts, Symbol[] names,
Expr body, int weight, Pattern[] patterns, Expr[] noPatterns,
Symbol quantifierID, Symbol skolemID
) {
Symbol quantifierID, Symbol skolemID) {
ctx.checkContextMatch(patterns);
ctx.checkContextMatch(noPatterns);
ctx.checkContextMatch(sorts);
ctx.checkContextMatch(names);
ctx.checkContextMatch(body);
if (sorts.length != names.length)
if (sorts.length != names.length) {
throw new Z3Exception(
"Number of sorts does not match number of names");
}
long nativeObj;
if (noPatterns == null && quantifierID == null && skolemID == null) {
@ -180,18 +188,26 @@ public class Quantifier extends BoolExpr
}
/**
* @param ctx Context to create the quantifier on.
* @param isForall Quantifier type.
* @param bound Bound variables.
* @param body Body of the quantifier.
* @param weight Weight.
* @param patterns Nullable array of patterns.
* @param noPatterns Nullable array of noPatterns.
* @param quantifierID Nullable quantifier identifier.
* @param skolemID Nullable skolem identifier.
*/
public static Quantifier of(Context ctx, boolean isForall, Expr[] bound, Expr body,
int weight, Pattern[] patterns, Expr[] noPatterns,
Symbol quantifierID, Symbol skolemID)
{
Symbol quantifierID, Symbol skolemID) {
ctx.checkContextMatch(noPatterns);
ctx.checkContextMatch(patterns);
// ctx.CheckContextMatch(bound);
ctx.checkContextMatch(body);
long nativeObj;
if (noPatterns == null && quantifierID == null && skolemID == null)
{
if (noPatterns == null && quantifierID == null && skolemID == null) {
nativeObj = Native.mkQuantifierConst(ctx.nCtx(),
isForall, weight, AST.arrayLength(bound),
AST.arrayToNative(bound), AST.arrayLength(patterns),
@ -214,11 +230,11 @@ public class Quantifier extends BoolExpr
}
@Override
void checkNativeObject(long obj)
{
void checkNativeObject(long obj) {
if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
.toInt())
.toInt()) {
throw new Z3Exception("Underlying object is not a quantifier");
}
super.checkNativeObject(obj);
}
}