mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 07:03:23 +00:00
Code Activity

resolved conflicts

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-12 18:29:46 +00:00
commit f399fe5e1d
50 changed files with 323 additions and 294 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/api/java/Solver.java
View file

@ -57,8 +57,8 @@ public class Solver extends Z3Object
/**
* The current number of backtracking points (scopes).
* @see pop
* @see push
* @see #pop
* @see #push
**/
public int getNumScopes()
{
@ -68,7 +68,7 @@ public class Solver extends Z3Object
/**
* Creates a backtracking point.
* @see pop
* @see #pop
**/
public void push()
{
@ -89,7 +89,7 @@ public class Solver extends Z3Object
* Remarks: Note that
* an exception is thrown if {@code n} is not smaller than
* {@code NumScopes}
* @see push
* @see #push
**/
public void pop(int n)
{
@ -139,12 +139,14 @@ public class Solver extends Z3Object
{
getContext().checkContextMatch(constraints);
getContext().checkContextMatch(ps);
if (constraints.length != ps.length)
if (constraints.length != ps.length) {
throw new Z3Exception("Argument size mismatch");
}
for (int i = 0; i < constraints.length; i++)
for (int i = 0; i < constraints.length; i++) {
Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
constraints[i].getNativeObject(), ps[i].getNativeObject());
constraints[i].getNativeObject(), ps[i].getNativeObject());
}
}
/**
@ -194,20 +196,21 @@ public class Solver extends Z3Object
/**
* Checks whether the assertions in the solver are consistent or not.
* Remarks:
* @see getModel
* @see getUnsatCore
* @see getProof
* @see #getModel
* @see #getUnsatCore
* @see #getProof
**/
public Status check(Expr... assumptions)
{
Z3_lbool r;
if (assumptions == null)
if (assumptions == null) {
r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
getNativeObject()));
else
getNativeObject()));
} else {
r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
.nCtx(), getNativeObject(), (int) assumptions.length, AST
.arrayToNative(assumptions)));
.nCtx(), getNativeObject(), assumptions.length, AST
.arrayToNative(assumptions)));
}
switch (r)
{
case Z3_L_TRUE:
@ -222,9 +225,9 @@ public class Solver extends Z3Object
/**
* Checks whether the assertions in the solver are consistent or not.
* Remarks:
* @see getModel
* @see getUnsatCore
* @see getProof
* @see #getModel
* @see #getUnsatCore
* @see #getProof
**/
public Status check()
{
@ -243,10 +246,11 @@ public class Solver extends Z3Object
public Model getModel()
{
long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
if (x == 0)
if (x == 0) {
return null;
else
} else {
return new Model(getContext(), x);
}
}
/**
@ -261,10 +265,11 @@ public class Solver extends Z3Object
public Expr getProof()
{
long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
if (x == 0)
if (x == 0) {
return null;
else
} else {
return Expr.create(getContext(), x);
}
}
/**
@ -315,6 +320,7 @@ public class Solver extends Z3Object
/**
* A string representation of the solver.
**/
@Override
public String toString()
{
try
@ -332,12 +338,14 @@ public class Solver extends Z3Object
super(ctx, obj);
}
@Override
void incRef(long o)
{
getContext().getSolverDRQ().incAndClear(getContext(), o);
super.incRef(o);
}
@Override
void decRef(long o)
{
getContext().getSolverDRQ().add(o);