mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'cheshire-codesmells'
This commit is contained in:
commit
da502a79dc
|
@ -28,23 +28,16 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
* Object comparison.
|
||||
*
|
||||
* @param o another AST
|
||||
**/
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
AST casted = null;
|
||||
if (o == this) return true;
|
||||
if (!(o instanceof AST)) return false;
|
||||
AST casted = (AST) o;
|
||||
|
||||
try
|
||||
{
|
||||
casted = AST.class.cast(o);
|
||||
} catch (ClassCastException e)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
return (this == casted) ||
|
||||
(this != null) &&
|
||||
(casted != null) &&
|
||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||
return
|
||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||
(Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
||||
}
|
||||
|
||||
|
@ -56,17 +49,13 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
* positive if after else zero.
|
||||
* @throws Z3Exception on error
|
||||
**/
|
||||
@Override
|
||||
public int compareTo(AST other)
|
||||
{
|
||||
if (other == null)
|
||||
if (other == null) {
|
||||
return 1;
|
||||
|
||||
if (getId() < other.getId())
|
||||
return -1;
|
||||
else if (getId() > other.getId())
|
||||
return +1;
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
return Integer.compare(getId(), other.getId());
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -74,14 +63,10 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
*
|
||||
* @return A hash code
|
||||
**/
|
||||
@Override
|
||||
public int hashCode()
|
||||
{
|
||||
int r = 0;
|
||||
try {
|
||||
Native.getAstHash(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
catch (Z3Exception ex) {}
|
||||
return r;
|
||||
return Native.getAstHash(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -103,11 +88,12 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
public AST translate(Context ctx)
|
||||
{
|
||||
|
||||
if (getContext() == ctx)
|
||||
if (getContext() == ctx) {
|
||||
return this;
|
||||
else
|
||||
} else {
|
||||
return new AST(ctx, Native.translate(getContext().nCtx(),
|
||||
getNativeObject(), ctx.nCtx()));
|
||||
getNativeObject(), ctx.nCtx()));
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -188,6 +174,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
/**
|
||||
* A string representation of the AST.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -217,6 +204,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
// Console.WriteLine("AST IncRef()");
|
||||
|
@ -226,6 +214,7 @@ public class AST extends Z3Object implements Comparable<AST>
|
|||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
// Console.WriteLine("AST DecRef()");
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -101,6 +101,7 @@ class ASTMap extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the map.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -122,12 +123,14 @@ class ASTMap extends Z3Object
|
|||
super(ctx, Native.mkAstMap(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getASTMapDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getASTMapDRQ().add(o);
|
||||
|
|
|
@ -87,6 +87,7 @@ public class ASTVector extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the vector.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -108,12 +109,14 @@ public class ASTVector extends Z3Object
|
|||
super(ctx, Native.mkAstVector(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getASTVectorDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getASTVectorDRQ().add(o);
|
||||
|
|
|
@ -63,6 +63,7 @@ public class ApplyResult extends Z3Object
|
|||
/**
|
||||
* A string representation of the ApplyResult.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -79,12 +80,14 @@ public class ApplyResult extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getApplyResultDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getApplyResultDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ApplyResultDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTMapDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ASTVectorDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -32,8 +32,9 @@ public class BitVecNum extends BitVecExpr
|
|||
public int getInt()
|
||||
{
|
||||
Native.IntPtr res = new Native.IntPtr();
|
||||
if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
|
||||
throw new Z3Exception("Numeral is not an int");
|
||||
}
|
||||
return res.value;
|
||||
}
|
||||
|
||||
|
@ -45,8 +46,9 @@ public class BitVecNum extends BitVecExpr
|
|||
public long getLong()
|
||||
{
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
|
||||
throw new Z3Exception("Numeral is not a long");
|
||||
}
|
||||
return res.value;
|
||||
}
|
||||
|
||||
|
@ -61,6 +63,7 @@ public class BitVecNum extends BitVecExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -87,11 +87,7 @@ public class Constructor extends Z3Object
|
|||
{
|
||||
try {
|
||||
Native.delConstructor(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
catch (Throwable t) {
|
||||
throw t;
|
||||
}
|
||||
finally {
|
||||
} finally {
|
||||
super.finalize();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -31,11 +31,7 @@ public class ConstructorList extends Z3Object
|
|||
{
|
||||
try {
|
||||
Native.delConstructorList(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
catch (Throwable t) {
|
||||
throw t;
|
||||
}
|
||||
finally {
|
||||
} finally {
|
||||
super.finalize();
|
||||
}
|
||||
}
|
||||
|
@ -50,7 +46,7 @@ public class ConstructorList extends Z3Object
|
|||
super(ctx);
|
||||
|
||||
setNativeObject(Native.mkConstructorList(getContext().nCtx(),
|
||||
(int) constructors.length,
|
||||
constructors.length,
|
||||
Constructor.arrayToNative(constructors)));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -110,8 +110,9 @@ public class Context extends IDisposable
|
|||
**/
|
||||
public BoolSort getBoolSort()
|
||||
{
|
||||
if (m_boolSort == null)
|
||||
if (m_boolSort == null) {
|
||||
m_boolSort = new BoolSort(this);
|
||||
}
|
||||
return m_boolSort;
|
||||
}
|
||||
|
||||
|
@ -120,8 +121,9 @@ public class Context extends IDisposable
|
|||
**/
|
||||
public IntSort getIntSort()
|
||||
{
|
||||
if (m_intSort == null)
|
||||
if (m_intSort == null) {
|
||||
m_intSort = new IntSort(this);
|
||||
}
|
||||
return m_intSort;
|
||||
}
|
||||
|
||||
|
@ -130,8 +132,9 @@ public class Context extends IDisposable
|
|||
**/
|
||||
public RealSort getRealSort()
|
||||
{
|
||||
if (m_realSort == null)
|
||||
if (m_realSort == null) {
|
||||
m_realSort = new RealSort(this);
|
||||
}
|
||||
return m_realSort;
|
||||
}
|
||||
|
||||
|
@ -148,8 +151,9 @@ public class Context extends IDisposable
|
|||
**/
|
||||
public SeqSort getStringSort()
|
||||
{
|
||||
if (m_stringSort == null)
|
||||
if (m_stringSort == null) {
|
||||
m_stringSort = mkStringSort();
|
||||
}
|
||||
return m_stringSort;
|
||||
}
|
||||
|
||||
|
@ -322,13 +326,6 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Create a datatype constructor.
|
||||
* @param name
|
||||
* @param recognizer
|
||||
* @param fieldNames
|
||||
* @param sorts
|
||||
* @param sortRefs
|
||||
*
|
||||
* @return
|
||||
**/
|
||||
public Constructor mkConstructor(String name, String recognizer,
|
||||
String[] fieldNames, Sort[] sorts, int[] sortRefs)
|
||||
|
@ -369,7 +366,7 @@ public class Context extends IDisposable
|
|||
|
||||
{
|
||||
checkContextMatch(names);
|
||||
int n = (int) names.length;
|
||||
int n = names.length;
|
||||
ConstructorList[] cla = new ConstructorList[n];
|
||||
long[] n_constr = new long[n];
|
||||
for (int i = 0; i < n; i++)
|
||||
|
@ -391,10 +388,6 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Create mutually recursive data-types.
|
||||
* @param names
|
||||
* @param c
|
||||
*
|
||||
* @return
|
||||
**/
|
||||
public DatatypeSort[] mkDatatypeSorts(String[] names, Constructor[][] c)
|
||||
|
||||
|
@ -406,7 +399,7 @@ public class Context extends IDisposable
|
|||
* Update a datatype field at expression t with value v.
|
||||
* The function performs a record update at t. The field
|
||||
* that is passed in as argument is updated with value v,
|
||||
* the remainig fields of t are unchanged.
|
||||
* the remaining fields of t are unchanged.
|
||||
**/
|
||||
public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
|
||||
throws Z3Exception
|
||||
|
@ -502,8 +495,8 @@ public class Context extends IDisposable
|
|||
/**
|
||||
* Creates a fresh constant function declaration with a name prefixed with
|
||||
* {@code prefix"}.
|
||||
* @see mkFuncDecl(String,Sort,Sort)
|
||||
* @see mkFuncDecl(String,Sort[],Sort)
|
||||
* @see #mkFuncDecl(String,Sort,Sort)
|
||||
* @see #mkFuncDecl(String,Sort[],Sort)
|
||||
**/
|
||||
public FuncDecl mkFreshConstDecl(String prefix, Sort range)
|
||||
|
||||
|
@ -1519,7 +1512,7 @@ public class Context extends IDisposable
|
|||
{
|
||||
checkContextMatch(t);
|
||||
return new IntExpr(this, Native.mkBv2int(nCtx(), t.getNativeObject(),
|
||||
(signed) ? true : false));
|
||||
(signed)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1533,8 +1526,7 @@ public class Context extends IDisposable
|
|||
checkContextMatch(t1);
|
||||
checkContextMatch(t2);
|
||||
return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true
|
||||
: false));
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1576,8 +1568,7 @@ public class Context extends IDisposable
|
|||
checkContextMatch(t1);
|
||||
checkContextMatch(t2);
|
||||
return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true
|
||||
: false));
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1617,8 +1608,7 @@ public class Context extends IDisposable
|
|||
checkContextMatch(t1);
|
||||
checkContextMatch(t2);
|
||||
return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true
|
||||
: false));
|
||||
.getNativeObject(), t2.getNativeObject(), (isSigned)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1662,8 +1652,8 @@ public class Context extends IDisposable
|
|||
* {@code [domain -> range]}, and {@code i} must have the sort
|
||||
* {@code domain}. The sort of the result is {@code range}.
|
||||
*
|
||||
* @see mkArraySort
|
||||
* @see mkStore
|
||||
* @see #mkArraySort
|
||||
* @see #mkStore
|
||||
|
||||
**/
|
||||
public Expr mkSelect(ArrayExpr a, Expr i)
|
||||
|
@ -1688,8 +1678,8 @@ public class Context extends IDisposable
|
|||
* {@code select}) on all indices except for {@code i}, where it
|
||||
* maps to {@code v} (and the {@code select} of {@code a}
|
||||
* with respect to {@code i} may be a different value).
|
||||
* @see mkArraySort
|
||||
* @see mkSelect
|
||||
* @see #mkArraySort
|
||||
* @see #mkSelect
|
||||
|
||||
**/
|
||||
public ArrayExpr mkStore(ArrayExpr a, Expr i, Expr v)
|
||||
|
@ -1706,8 +1696,8 @@ public class Context extends IDisposable
|
|||
* Remarks: The resulting term is an array, such
|
||||
* that a {@code select} on an arbitrary index produces the value
|
||||
* {@code v}.
|
||||
* @see mkArraySort
|
||||
* @see mkSelect
|
||||
* @see #mkArraySort
|
||||
* @see #mkSelect
|
||||
*
|
||||
**/
|
||||
public ArrayExpr mkConstArray(Sort domain, Expr v)
|
||||
|
@ -1720,15 +1710,15 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Maps f on the argument arrays.
|
||||
* Remarks: Eeach element of
|
||||
* Remarks: Each element of
|
||||
* {@code args} must be of an array sort
|
||||
* {@code [domain_i -> range_i]}. The function declaration
|
||||
* {@code f} must have type {@code range_1 .. range_n -> range}.
|
||||
* {@code v} must have sort range. The sort of the result is
|
||||
* {@code [domain_i -> range]}.
|
||||
* @see mkArraySort
|
||||
* @see mkSelect
|
||||
* @see mkStore
|
||||
* @see #mkArraySort
|
||||
* @see #mkSelect
|
||||
* @see #mkStore
|
||||
|
||||
**/
|
||||
public ArrayExpr mkMap(FuncDecl f, ArrayExpr... args)
|
||||
|
@ -2121,12 +2111,13 @@ public class Context extends IDisposable
|
|||
*
|
||||
* @return A Term with value {@code num}/{@code den}
|
||||
* and sort Real
|
||||
* @see mkNumeral(String,Sort)
|
||||
* @see #mkNumeral(String,Sort)
|
||||
**/
|
||||
public RatNum mkReal(int num, int den)
|
||||
{
|
||||
if (den == 0)
|
||||
if (den == 0) {
|
||||
throw new Z3Exception("Denominator is zero");
|
||||
}
|
||||
|
||||
return new RatNum(this, Native.mkReal(nCtx(), num, den));
|
||||
}
|
||||
|
@ -2256,7 +2247,7 @@ public class Context extends IDisposable
|
|||
* 'names' of the bound variables, and {@code body} is the body
|
||||
* of the quantifier. Quantifiers are associated with weights indicating the
|
||||
* importance of using the quantifier during instantiation.
|
||||
* Note that the bound variables are de-Bruijn indices created using {@link mkBound}.
|
||||
* Note that the bound variables are de-Bruijn indices created using {@link #mkBound}.
|
||||
* Z3 applies the convention that the last element in {@code names} and
|
||||
* {@code sorts} refers to the variable with index 0, the second to last element
|
||||
* of {@code names} and {@code sorts} refers to the variable
|
||||
|
@ -2286,7 +2277,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Creates an existential quantifier using de-Brujin indexed variables.
|
||||
* @see mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
* @see #mkForall(Sort[],Symbol[],Expr,int,Pattern[],Expr[],Symbol,Symbol)
|
||||
**/
|
||||
public Quantifier mkExists(Sort[] sorts, Symbol[] names, Expr body,
|
||||
int weight, Pattern[] patterns, Expr[] noPatterns,
|
||||
|
@ -2383,7 +2374,7 @@ public class Context extends IDisposable
|
|||
{
|
||||
|
||||
return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
|
||||
attributes, (int) assumptions.length,
|
||||
attributes, assumptions.length,
|
||||
AST.arrayToNative(assumptions), formula.getNativeObject());
|
||||
}
|
||||
|
||||
|
@ -2413,7 +2404,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Parse the given file using the SMT-LIB parser.
|
||||
* @see parseSMTLIBString
|
||||
* @see #parseSMTLIBString
|
||||
**/
|
||||
public void parseSMTLIBFile(String fileName, Symbol[] sortNames,
|
||||
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
|
||||
|
@ -2527,7 +2518,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Parse the given string using the SMT-LIB2 parser.
|
||||
* @see parseSMTLIBString
|
||||
* @see #parseSMTLIBString
|
||||
*
|
||||
* @return A conjunction of assertions in the scope (up to push/pop) at the
|
||||
* end of the string.
|
||||
|
@ -2541,8 +2532,9 @@ public class Context extends IDisposable
|
|||
int cs = Sort.arrayLength(sorts);
|
||||
int cdn = Symbol.arrayLength(declNames);
|
||||
int cd = AST.arrayLength(decls);
|
||||
if (csn != cs || cdn != cd)
|
||||
if (csn != cs || cdn != cd) {
|
||||
throw new Z3Exception("Argument size mismatch");
|
||||
}
|
||||
return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
|
||||
str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
|
||||
AST.arrayToNative(sorts), AST.arrayLength(decls),
|
||||
|
@ -2551,13 +2543,12 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Parse the given file using the SMT-LIB2 parser.
|
||||
* @see parseSMTLIB2String
|
||||
* @see #parseSMTLIB2String
|
||||
**/
|
||||
public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
|
||||
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
|
||||
|
||||
{
|
||||
|
||||
int csn = Symbol.arrayLength(sortNames);
|
||||
int cs = Sort.arrayLength(sorts);
|
||||
int cdn = Symbol.arrayLength(declNames);
|
||||
|
@ -2648,9 +2639,10 @@ public class Context extends IDisposable
|
|||
if (ts != null && ts.length > 0)
|
||||
{
|
||||
last = ts[ts.length - 1].getNativeObject();
|
||||
for (int i = ts.length - 2; i >= 0; i--)
|
||||
for (int i = ts.length - 2; i >= 0; i--) {
|
||||
last = Native.tacticAndThen(nCtx(), ts[i].getNativeObject(),
|
||||
last);
|
||||
last);
|
||||
}
|
||||
}
|
||||
if (last != 0)
|
||||
{
|
||||
|
@ -2664,7 +2656,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Create a tactic that applies {@code t1} to a Goal and then
|
||||
* {@code t2"/> to every subgoal produced by <paramref name="t1}.
|
||||
* {@code t2} to every subgoal produced by {@code t1}
|
||||
*
|
||||
* Remarks: Shorthand for {@code AndThen}.
|
||||
**/
|
||||
|
@ -2999,7 +2991,7 @@ public class Context extends IDisposable
|
|||
|
||||
/**
|
||||
* Creates a new (incremental) solver.
|
||||
* @see mkSolver(Symbol)
|
||||
* @see #mkSolver(Symbol)
|
||||
**/
|
||||
public Solver mkSolver(String logic)
|
||||
{
|
||||
|
@ -3839,7 +3831,7 @@ public class Context extends IDisposable
|
|||
* that is returned must be handled externally and through native calls (see
|
||||
* e.g.,
|
||||
* @see Native#incRef
|
||||
* @see wrapAST
|
||||
* @see #wrapAST
|
||||
* @param a The AST to unwrap.
|
||||
**/
|
||||
public long unwrapAST(AST a)
|
||||
|
@ -3878,7 +3870,7 @@ public class Context extends IDisposable
|
|||
}
|
||||
|
||||
protected long m_ctx = 0;
|
||||
protected static Object creation_lock = new Object();
|
||||
protected static final Object creation_lock = new Object();
|
||||
|
||||
long nCtx()
|
||||
{
|
||||
|
@ -4049,7 +4041,7 @@ public class Context extends IDisposable
|
|||
m_Params_DRQ.clear(this);
|
||||
m_Probe_DRQ.clear(this);
|
||||
m_Solver_DRQ.clear(this);
|
||||
m_Optimize_DRQ.clear(this);
|
||||
m_Optimize_DRQ.clear(this);
|
||||
m_Statistics_DRQ.clear(this);
|
||||
m_Tactic_DRQ.clear(this);
|
||||
m_Fixedpoint_DRQ.clear(this);
|
||||
|
|
|
@ -101,7 +101,7 @@ public class DatatypeSort extends Sort
|
|||
|
||||
{
|
||||
super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
|
||||
(int) constructors.length, arrayToNative(constructors)));
|
||||
constructors.length, arrayToNative(constructors)));
|
||||
|
||||
}
|
||||
};
|
||||
|
|
|
@ -98,7 +98,7 @@ public class EnumSort extends Sort
|
|||
long[] n_constdecls = new long[n];
|
||||
long[] n_testers = new long[n];
|
||||
setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
|
||||
name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
|
||||
name.getNativeObject(), n, Symbol.arrayToNative(enumNames),
|
||||
n_constdecls, n_testers));
|
||||
}
|
||||
};
|
||||
|
|
|
@ -33,7 +33,6 @@ public class Expr extends AST
|
|||
* Returns a simplified version of the expression
|
||||
* @return Expr
|
||||
* @throws Z3Exception on error
|
||||
* @return an Expr
|
||||
**/
|
||||
public Expr simplify()
|
||||
{
|
||||
|
@ -48,19 +47,20 @@ public class Expr extends AST
|
|||
* @see Context#SimplifyHelp
|
||||
* @return an Expr
|
||||
* @throws Z3Exception on error
|
||||
* @return an Expr
|
||||
**/
|
||||
public Expr simplify(Params p)
|
||||
{
|
||||
|
||||
if (p == null)
|
||||
if (p == null) {
|
||||
return Expr.create(getContext(),
|
||||
Native.simplify(getContext().nCtx(), getNativeObject()));
|
||||
else
|
||||
Native.simplify(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
else {
|
||||
return Expr.create(
|
||||
getContext(),
|
||||
Native.simplifyEx(getContext().nCtx(), getNativeObject(),
|
||||
p.getNativeObject()));
|
||||
getContext(),
|
||||
Native.simplifyEx(getContext().nCtx(), getNativeObject(),
|
||||
p.getNativeObject()));
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -106,9 +106,10 @@ public class Expr extends AST
|
|||
{
|
||||
int n = getNumArgs();
|
||||
Expr[] res = new Expr[n];
|
||||
for (int i = 0; i < n; i++)
|
||||
for (int i = 0; i < n; i++) {
|
||||
res[i] = Expr.create(getContext(),
|
||||
Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
|
||||
Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
|
@ -122,10 +123,11 @@ public class Expr extends AST
|
|||
public void update(Expr[] args)
|
||||
{
|
||||
getContext().checkContextMatch(args);
|
||||
if (isApp() && args.length != getNumArgs())
|
||||
if (isApp() && args.length != getNumArgs()) {
|
||||
throw new Z3Exception("Number of arguments does not match");
|
||||
}
|
||||
setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
|
||||
(int) args.length, Expr.arrayToNative(args)));
|
||||
args.length, Expr.arrayToNative(args)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -144,10 +146,11 @@ public class Expr extends AST
|
|||
{
|
||||
getContext().checkContextMatch(from);
|
||||
getContext().checkContextMatch(to);
|
||||
if (from.length != to.length)
|
||||
if (from.length != to.length) {
|
||||
throw new Z3Exception("Argument sizes do not match");
|
||||
}
|
||||
return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
|
||||
getNativeObject(), (int) from.length, Expr.arrayToNative(from),
|
||||
getNativeObject(), from.length, Expr.arrayToNative(from),
|
||||
Expr.arrayToNative(to)));
|
||||
}
|
||||
|
||||
|
@ -160,7 +163,6 @@ public class Expr extends AST
|
|||
**/
|
||||
public Expr substitute(Expr from, Expr to)
|
||||
{
|
||||
|
||||
return substitute(new Expr[] { from }, new Expr[] { to });
|
||||
}
|
||||
|
||||
|
@ -179,7 +181,7 @@ public class Expr extends AST
|
|||
|
||||
getContext().checkContextMatch(to);
|
||||
return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
|
||||
getNativeObject(), (int) to.length, Expr.arrayToNative(to)));
|
||||
getNativeObject(), to.length, Expr.arrayToNative(to)));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -189,23 +191,23 @@ public class Expr extends AST
|
|||
*
|
||||
* @return A copy of the term which is associated with {@code ctx}
|
||||
* @throws Z3Exception on error
|
||||
* @return an Expr
|
||||
**/
|
||||
public Expr translate(Context ctx)
|
||||
{
|
||||
|
||||
if (getContext() == ctx)
|
||||
if (getContext() == ctx) {
|
||||
return this;
|
||||
else
|
||||
} else {
|
||||
return Expr.create(
|
||||
ctx,
|
||||
Native.translate(getContext().nCtx(), getNativeObject(),
|
||||
ctx.nCtx()));
|
||||
ctx,
|
||||
Native.translate(getContext().nCtx(), getNativeObject(),
|
||||
ctx.nCtx()));
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns a string representation of the expression.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return super.toString();
|
||||
|
@ -224,9 +226,8 @@ public class Expr extends AST
|
|||
/**
|
||||
* Indicates whether the term is well-sorted.
|
||||
*
|
||||
* @return True if the term is well-sorted, false otherwise.
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
* @return True if the term is well-sorted, false otherwise.
|
||||
**/
|
||||
public boolean isWellSorted()
|
||||
{
|
||||
|
@ -2038,7 +2039,7 @@ public class Expr extends AST
|
|||
* identity, but in the context of a register machine allows for terms of
|
||||
* kind {@code isRelationUnion} to perform destructive updates to
|
||||
* the first argument.
|
||||
* @see isRelationUnion
|
||||
* @see #isRelationUnion
|
||||
* @throws Z3Exception on error
|
||||
* @return a boolean
|
||||
**/
|
||||
|
@ -2117,12 +2118,14 @@ public class Expr extends AST
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
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())
|
||||
Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST.toInt()) {
|
||||
throw new Z3Exception("Underlying object is not a term");
|
||||
}
|
||||
super.checkNativeObject(obj);
|
||||
}
|
||||
|
||||
|
@ -2186,10 +2189,10 @@ public class Expr extends AST
|
|||
return new FPRMExpr(ctx, obj);
|
||||
case Z3_FINITE_DOMAIN_SORT:
|
||||
return new FiniteDomainExpr(ctx, obj);
|
||||
case Z3_SEQ_SORT:
|
||||
return new SeqExpr(ctx, obj);
|
||||
case Z3_RE_SORT:
|
||||
return new ReExpr(ctx, obj);
|
||||
case Z3_SEQ_SORT:
|
||||
return new SeqExpr(ctx, obj);
|
||||
case Z3_RE_SORT:
|
||||
return new ReExpr(ctx, obj);
|
||||
default: ;
|
||||
}
|
||||
|
||||
|
|
|
@ -36,8 +36,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
|
|||
public int getInt()
|
||||
{
|
||||
Native.IntPtr res = new Native.IntPtr();
|
||||
if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res)) {
|
||||
throw new Z3Exception("Numeral is not an int");
|
||||
}
|
||||
return res.value;
|
||||
}
|
||||
|
||||
|
@ -47,8 +48,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
|
|||
public long getInt64()
|
||||
{
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res)) {
|
||||
throw new Z3Exception("Numeral is not an int64");
|
||||
}
|
||||
return res.value;
|
||||
}
|
||||
|
||||
|
@ -63,6 +65,7 @@ public class FiniteDomainNum extends FiniteDomainExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -164,7 +164,7 @@ public class Fixedpoint extends Z3Object
|
|||
|
||||
/**
|
||||
* Creates a backtracking point.
|
||||
* @see pop
|
||||
* @see #pop
|
||||
**/
|
||||
public void push()
|
||||
{
|
||||
|
@ -176,7 +176,7 @@ public class Fixedpoint extends Z3Object
|
|||
* Remarks: Note that an exception is thrown if {@code pop}
|
||||
* is called without a corresponding {@code push}
|
||||
*
|
||||
* @see push
|
||||
* @see #push
|
||||
**/
|
||||
public void pop()
|
||||
{
|
||||
|
@ -252,6 +252,7 @@ public class Fixedpoint extends Z3Object
|
|||
/**
|
||||
* Retrieve internal string representation of fixedpoint object.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -353,12 +354,14 @@ public class Fixedpoint extends Z3Object
|
|||
super(ctx, Native.mkFixedpoint(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getFixedpointDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getFixedpointDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FixedpointDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,35 +29,22 @@ public class FuncDecl extends AST
|
|||
/**
|
||||
* Object comparison.
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
FuncDecl casted = null;
|
||||
if (o == this) return true;
|
||||
if (!(o instanceof FuncDecl)) return false;
|
||||
FuncDecl other = (FuncDecl) o;
|
||||
|
||||
try {
|
||||
casted = FuncDecl.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return
|
||||
(this == casted) ||
|
||||
(this != null) &&
|
||||
(casted != null) &&
|
||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||
(Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
||||
return
|
||||
(getContext().nCtx() == other.getContext().nCtx()) &&
|
||||
(Native.isEqFuncDecl(
|
||||
getContext().nCtx(),
|
||||
getNativeObject(),
|
||||
other.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* A hash code.
|
||||
**/
|
||||
public int hashCode()
|
||||
{
|
||||
return super.hashCode();
|
||||
}
|
||||
|
||||
/**
|
||||
* A string representations of the function declaration.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -72,6 +59,7 @@ public class FuncDecl extends AST
|
|||
/**
|
||||
* Returns a unique identifier for the function declaration.
|
||||
**/
|
||||
@Override
|
||||
public int getId()
|
||||
{
|
||||
return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
|
||||
|
@ -87,7 +75,7 @@ public class FuncDecl extends AST
|
|||
|
||||
/**
|
||||
* The size of the domain of the function declaration
|
||||
* @see getArity
|
||||
* @see #getArity
|
||||
**/
|
||||
public int getDomainSize()
|
||||
{
|
||||
|
@ -370,9 +358,6 @@ public class FuncDecl extends AST
|
|||
|
||||
/**
|
||||
* Create expression that applies function to arguments.
|
||||
* @param args
|
||||
*
|
||||
* @return
|
||||
**/
|
||||
public Expr apply(Expr ... args)
|
||||
{
|
||||
|
|
|
@ -70,6 +70,7 @@ public class FuncInterp extends Z3Object
|
|||
/**
|
||||
* A string representation of the function entry.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -82,7 +83,7 @@ public class FuncInterp extends Z3Object
|
|||
return res + getValue() + "]";
|
||||
} catch (Z3Exception e)
|
||||
{
|
||||
return new String("Z3Exception: " + e.getMessage());
|
||||
return "Z3Exception: " + e.getMessage();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -91,18 +92,20 @@ public class FuncInterp extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@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);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
/**
|
||||
* The number of entries in the function interpretation.
|
||||
|
@ -183,7 +186,7 @@ public class FuncInterp extends Z3Object
|
|||
return res;
|
||||
} catch (Z3Exception e)
|
||||
{
|
||||
return new String("Z3Exception: " + e.getMessage());
|
||||
return "Z3Exception: " + e.getMessage();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -192,12 +195,14 @@ public class FuncInterp extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getFuncInterpDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FuncInterpDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,6 +29,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class FuncInterpEntryDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -57,17 +57,18 @@ public final class Global
|
|||
public static String getParameter(String id)
|
||||
{
|
||||
Native.StringPtr res = new Native.StringPtr();
|
||||
if (!Native.globalParamGet(id, res))
|
||||
if (!Native.globalParamGet(id, res)) {
|
||||
return null;
|
||||
else
|
||||
} else {
|
||||
return res.value;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Restore the value of all global (and module) parameters.
|
||||
* Remarks:
|
||||
* This command will not affect already created objects (such as tactics and solvers)
|
||||
* @see setParameter
|
||||
* @see #setParameter
|
||||
**/
|
||||
public static void resetParameters()
|
||||
{
|
||||
|
@ -83,7 +84,7 @@ public final class Global
|
|||
public static void ToggleWarningMessages(boolean enabled)
|
||||
|
||||
{
|
||||
Native.toggleWarningMessages((enabled) ? true : false);
|
||||
Native.toggleWarningMessages((enabled));
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
@ -246,8 +246,8 @@ public class Goal extends Z3Object
|
|||
Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
|
||||
|
||||
{
|
||||
super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
|
||||
(unsatCores) ? true : false, (proofs) ? true : false));
|
||||
super(ctx, Native.mkGoal(ctx.nCtx(), (models),
|
||||
(unsatCores), (proofs)));
|
||||
}
|
||||
|
||||
void incRef(long o)
|
||||
|
|
|
@ -29,6 +29,7 @@ class GoalDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class GoalDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -21,7 +21,7 @@ import java.util.LinkedList;
|
|||
|
||||
public abstract class IDecRefQueue
|
||||
{
|
||||
protected Object m_lock = new Object();
|
||||
protected final Object m_lock = new Object();
|
||||
protected LinkedList<Long> m_queue = new LinkedList<Long>();
|
||||
protected int m_move_limit;
|
||||
|
||||
|
|
|
@ -19,9 +19,7 @@ Notes:
|
|||
|
||||
package com.microsoft.z3;
|
||||
|
||||
public class IDisposable
|
||||
public abstract class IDisposable
|
||||
{
|
||||
public void dispose()
|
||||
{
|
||||
}
|
||||
public abstract void dispose();
|
||||
}
|
||||
|
|
|
@ -36,7 +36,7 @@ public class IntNum extends IntExpr
|
|||
public int getInt()
|
||||
{
|
||||
Native.IntPtr res = new Native.IntPtr();
|
||||
if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res))
|
||||
throw new Z3Exception("Numeral is not an int");
|
||||
return res.value;
|
||||
}
|
||||
|
@ -47,7 +47,7 @@ public class IntNum extends IntExpr
|
|||
public long getInt64()
|
||||
{
|
||||
Native.LongPtr res = new Native.LongPtr();
|
||||
if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
|
||||
if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res))
|
||||
throw new Z3Exception("Numeral is not an int64");
|
||||
return res.value;
|
||||
}
|
||||
|
|
|
@ -46,6 +46,7 @@ public class IntSymbol extends Symbol
|
|||
super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
|
||||
|
|
|
@ -92,7 +92,7 @@ public class Model extends Z3Object
|
|||
return null;
|
||||
else
|
||||
{
|
||||
if (Native.isAsArray(getContext().nCtx(), n) ^ true)
|
||||
if (!Native.isAsArray(getContext().nCtx(), n))
|
||||
throw new Z3Exception(
|
||||
"Argument was not an array constant");
|
||||
long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
|
||||
|
@ -212,8 +212,8 @@ public class Model extends Z3Object
|
|||
public Expr eval(Expr t, boolean completion)
|
||||
{
|
||||
Native.LongPtr v = new Native.LongPtr();
|
||||
if (Native.modelEval(getContext().nCtx(), getNativeObject(),
|
||||
t.getNativeObject(), (completion) ? true : false, v) ^ true)
|
||||
if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
|
||||
t.getNativeObject(), (completion), v))
|
||||
throw new ModelEvaluationFailedException();
|
||||
else
|
||||
return Expr.create(getContext(), v.value);
|
||||
|
@ -244,8 +244,8 @@ public class Model extends Z3Object
|
|||
* in a formula. The interpretation for a sort is a finite set of distinct
|
||||
* values. We say this finite set is the "universe" of the sort.
|
||||
*
|
||||
* @see getNumSorts
|
||||
* @see getSortUniverse
|
||||
* @see #getNumSorts
|
||||
* @see #getSortUniverse
|
||||
*
|
||||
* @throws Z3Exception
|
||||
**/
|
||||
|
@ -282,6 +282,7 @@ public class Model extends Z3Object
|
|||
*
|
||||
* @return A string representation of the model.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -298,12 +299,14 @@ public class Model extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getModelDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getModelDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ModelDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ModelDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -32,7 +32,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public String getHelp()
|
||||
{
|
||||
return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
|
||||
return Native.optimizeGetHelp(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -42,7 +42,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public void setParameters(Params value)
|
||||
{
|
||||
Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
|
||||
Native.optimizeSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -50,7 +50,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public ParamDescrs getParameterDescriptions()
|
||||
{
|
||||
return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
|
||||
return new ParamDescrs(getContext(), Native.optimizeGetParamDescrs(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -112,8 +112,9 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Print a string representation of the handle.
|
||||
**/
|
||||
public String toString()
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return getValue().toString();
|
||||
}
|
||||
|
@ -128,9 +129,9 @@ public class Optimize extends Z3Object
|
|||
|
||||
public Handle AssertSoft(BoolExpr constraint, int weight, String group)
|
||||
{
|
||||
getContext().checkContextMatch(constraint);
|
||||
Symbol s = getContext().mkSymbol(group);
|
||||
return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
|
||||
getContext().checkContextMatch(constraint);
|
||||
Symbol s = getContext().mkSymbol(group);
|
||||
return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
|
@ -142,15 +143,15 @@ public class Optimize extends Z3Object
|
|||
|
||||
public Status Check()
|
||||
{
|
||||
Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
|
||||
switch (r) {
|
||||
case Z3_L_TRUE:
|
||||
return Status.SATISFIABLE;
|
||||
case Z3_L_FALSE:
|
||||
return Status.UNSATISFIABLE;
|
||||
default:
|
||||
return Status.UNKNOWN;
|
||||
}
|
||||
Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
|
||||
switch (r) {
|
||||
case Z3_L_TRUE:
|
||||
return Status.SATISFIABLE;
|
||||
case Z3_L_FALSE:
|
||||
return Status.UNSATISFIABLE;
|
||||
default:
|
||||
return Status.UNKNOWN;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -158,7 +159,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public void Push()
|
||||
{
|
||||
Native.optimizePush(getContext().nCtx(), getNativeObject());
|
||||
Native.optimizePush(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
|
@ -170,7 +171,7 @@ public class Optimize extends Z3Object
|
|||
|
||||
public void Pop()
|
||||
{
|
||||
Native.optimizePop(getContext().nCtx(), getNativeObject());
|
||||
Native.optimizePop(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
|
||||
|
@ -182,11 +183,12 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public Model getModel()
|
||||
{
|
||||
long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
|
||||
if (x == 0)
|
||||
return null;
|
||||
else
|
||||
return new Model(getContext(), x);
|
||||
long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
|
||||
if (x == 0) {
|
||||
return null;
|
||||
} else {
|
||||
return new Model(getContext(), x);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -196,7 +198,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public Handle MkMaximize(ArithExpr e)
|
||||
{
|
||||
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -205,7 +207,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public Handle MkMinimize(ArithExpr e)
|
||||
{
|
||||
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -213,7 +215,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
private ArithExpr GetLower(int index)
|
||||
{
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
|
||||
}
|
||||
|
||||
|
||||
|
@ -222,7 +224,7 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
private ArithExpr GetUpper(int index)
|
||||
{
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
|
||||
return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -237,10 +239,11 @@ public class Optimize extends Z3Object
|
|||
|
||||
/**
|
||||
* Print the context to a String (SMT-LIB parseable benchmark).
|
||||
**/
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
|
||||
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -248,27 +251,28 @@ public class Optimize extends Z3Object
|
|||
**/
|
||||
public Statistics getStatistics()
|
||||
{
|
||||
return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
|
||||
return new Statistics(getContext(), Native.optimizeGetStatistics(getContext().nCtx(), getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
Optimize(Context ctx, long obj) throws Z3Exception
|
||||
{
|
||||
super(ctx, obj);
|
||||
super(ctx, obj);
|
||||
}
|
||||
|
||||
Optimize(Context ctx) throws Z3Exception
|
||||
{
|
||||
super(ctx, Native.mkOptimize(ctx.nCtx()));
|
||||
super(ctx, Native.mkOptimize(ctx.nCtx()));
|
||||
}
|
||||
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getOptimizeDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getOptimizeDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class OptimizeDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -72,6 +72,7 @@ public class ParamDescrs extends Z3Object
|
|||
/**
|
||||
* Retrieves a string representation of the ParamDescrs.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -88,12 +89,14 @@ public class ParamDescrs extends Z3Object
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getParamDescrsDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ParamDescrsDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -29,7 +29,7 @@ public class Params extends Z3Object
|
|||
public void add(Symbol name, boolean value)
|
||||
{
|
||||
Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
|
||||
name.getNativeObject(), (value) ? true : false);
|
||||
name.getNativeObject(), (value));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -112,6 +112,7 @@ public class Params extends Z3Object
|
|||
/**
|
||||
* A string representation of the parameter set.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -128,12 +129,14 @@ public class Params extends Z3Object
|
|||
super(ctx, Native.mkParams(ctx.nCtx()));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getParamsDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getParamsDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ParamsDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ParamsDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -50,6 +50,7 @@ public class Pattern extends AST
|
|||
/**
|
||||
* A string representation of the pattern.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -51,12 +51,14 @@ public class Probe extends Z3Object
|
|||
super(ctx, Native.mkProbe(ctx.nCtx(), name));
|
||||
}
|
||||
|
||||
@Override
|
||||
void incRef(long o)
|
||||
{
|
||||
getContext().getProbeDRQ().incAndClear(getContext(), o);
|
||||
super.incRef(o);
|
||||
}
|
||||
|
||||
@Override
|
||||
void decRef(long o)
|
||||
{
|
||||
getContext().getProbeDRQ().add(o);
|
||||
|
|
|
@ -29,6 +29,7 @@ class ProbeDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -40,6 +41,7 @@ class ProbeDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -163,15 +163,14 @@ public class Quantifier extends BoolExpr
|
|||
|
||||
if (noPatterns == null && quantifierID == null && skolemID == null)
|
||||
{
|
||||
setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true
|
||||
: false, weight, AST.arrayLength(patterns), AST
|
||||
setNativeObject(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) ? true : false, weight, AST.getNativeObject(quantifierID),
|
||||
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),
|
||||
|
@ -195,13 +194,13 @@ public class Quantifier extends BoolExpr
|
|||
if (noPatterns == null && quantifierID == null && skolemID == null)
|
||||
{
|
||||
setNativeObject(Native.mkQuantifierConst(ctx.nCtx(),
|
||||
(isForall) ? true : false, weight, AST.arrayLength(bound),
|
||||
isForall, weight, AST.arrayLength(bound),
|
||||
AST.arrayToNative(bound), AST.arrayLength(patterns),
|
||||
AST.arrayToNative(patterns), body.getNativeObject()));
|
||||
} else
|
||||
{
|
||||
setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
|
||||
(isForall) ? true : false, weight,
|
||||
isForall, weight,
|
||||
AST.getNativeObject(quantifierID),
|
||||
AST.getNativeObject(skolemID), AST.arrayLength(bound),
|
||||
AST.arrayToNative(bound), AST.arrayLength(patterns),
|
||||
|
@ -215,6 +214,7 @@ public class Quantifier extends BoolExpr
|
|||
super(ctx, obj);
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST
|
||||
|
|
|
@ -74,6 +74,7 @@ public class RatNum extends RealExpr
|
|||
/**
|
||||
* Returns a string representation of the numeral.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -26,6 +26,7 @@ class SolverDecRefQueue extends IDecRefQueue
|
|||
super(move_limit);
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void incRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
@ -37,6 +38,7 @@ class SolverDecRefQueue extends IDecRefQueue
|
|||
}
|
||||
}
|
||||
|
||||
@Override
|
||||
protected void decRef(Context ctx, long obj)
|
||||
{
|
||||
try
|
||||
|
|
|
@ -27,25 +27,20 @@ public class Sort extends AST
|
|||
{
|
||||
/**
|
||||
* Equality operator for objects of type Sort.
|
||||
* @param o
|
||||
* @return
|
||||
**/
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
Sort casted = null;
|
||||
if (o == this) return true;
|
||||
if (!(o instanceof Sort)) return false;
|
||||
Sort other = (Sort) o;
|
||||
|
||||
try {
|
||||
casted = Sort.class.cast(o);
|
||||
} catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return
|
||||
(this == casted) ||
|
||||
(this != null) &&
|
||||
(casted != null) &&
|
||||
(getContext().nCtx() == casted.getContext().nCtx()) &&
|
||||
(Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
|
||||
return (getContext().nCtx() == other.getContext().nCtx()) &&
|
||||
(Native.isEqSort(
|
||||
getContext().nCtx(),
|
||||
getNativeObject(),
|
||||
other.getNativeObject()
|
||||
));
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -141,10 +136,10 @@ public class Sort extends AST
|
|||
return new FPSort(ctx, obj);
|
||||
case Z3_ROUNDING_MODE_SORT:
|
||||
return new FPRMSort(ctx, obj);
|
||||
case Z3_SEQ_SORT:
|
||||
return new SeqSort(ctx, obj);
|
||||
case Z3_RE_SORT:
|
||||
return new ReSort(ctx, obj);
|
||||
case Z3_SEQ_SORT:
|
||||
return new SeqSort(ctx, obj);
|
||||
case Z3_RE_SORT:
|
||||
return new ReSort(ctx, obj);
|
||||
default:
|
||||
throw new Z3Exception("Unknown sort kind");
|
||||
}
|
||||
|
|
|
@ -72,12 +72,13 @@ public class Statistics extends Z3Object
|
|||
**/
|
||||
public String getValueString()
|
||||
{
|
||||
if (isUInt())
|
||||
if (isUInt()) {
|
||||
return Integer.toString(m_int);
|
||||
else if (isDouble())
|
||||
} else if (isDouble()) {
|
||||
return Double.toString(m_double);
|
||||
else
|
||||
} else {
|
||||
throw new Z3Exception("Unknown statistical entry type");
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -90,7 +91,7 @@ public class Statistics extends Z3Object
|
|||
return Key + ": " + getValueString();
|
||||
} catch (Z3Exception e)
|
||||
{
|
||||
return new String("Z3Exception: " + e.getMessage());
|
||||
return "Z3Exception: " + e.getMessage();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -150,14 +151,15 @@ public class Statistics extends Z3Object
|
|||
{
|
||||
Entry e;
|
||||
String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
|
||||
if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i))
|
||||
if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) {
|
||||
e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
|
||||
getNativeObject(), i));
|
||||
else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i))
|
||||
getNativeObject(), i));
|
||||
} else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
|
||||
e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
|
||||
getNativeObject(), i));
|
||||
else
|
||||
getNativeObject(), i));
|
||||
} else {
|
||||
throw new Z3Exception("Unknown data entry value");
|
||||
}
|
||||
res[i] = e;
|
||||
}
|
||||
return res;
|
||||
|
@ -186,9 +188,11 @@ public class Statistics extends Z3Object
|
|||
{
|
||||
int n = size();
|
||||
Entry[] es = getEntries();
|
||||
for (int i = 0; i < n; i++)
|
||||
if (es[i].Key == key)
|
||||
for (int i = 0; i < n; i++) {
|
||||
if (es[i].Key.equals(key)) {
|
||||
return es[i];
|
||||
}
|
||||
}
|
||||
return null;
|
||||
}
|
||||
|
||||
|
|
|
@ -38,7 +38,7 @@ public enum Status
|
|||
this.intValue = v;
|
||||
}
|
||||
|
||||
public static final Status fromInt(int v)
|
||||
public static Status fromInt(int v)
|
||||
{
|
||||
for (Status k : values())
|
||||
if (k.intValue == v)
|
||||
|
|
|
@ -44,6 +44,7 @@ public class StringSymbol extends Symbol
|
|||
super(ctx, Native.mkStringSymbol(ctx.nCtx(), s));
|
||||
}
|
||||
|
||||
@Override
|
||||
void checkNativeObject(long obj)
|
||||
{
|
||||
if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL
|
||||
|
|
|
@ -49,22 +49,19 @@ public class Symbol extends Z3Object
|
|||
return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
|
||||
}
|
||||
|
||||
@Override
|
||||
public boolean equals(Object o)
|
||||
{
|
||||
Symbol casted = null;
|
||||
try {
|
||||
casted = Symbol.class.cast(o);
|
||||
}
|
||||
catch (ClassCastException e) {
|
||||
return false;
|
||||
}
|
||||
|
||||
return this.getNativeObject() == casted.getNativeObject();
|
||||
if (o == this) return true;
|
||||
if (!(o instanceof Symbol)) return false;
|
||||
Symbol other = (Symbol) o;
|
||||
return this.getNativeObject() == other.getNativeObject();
|
||||
}
|
||||
|
||||
/**
|
||||
* A string representation of the symbol.
|
||||
**/
|
||||
@Override
|
||||
public String toString()
|
||||
{
|
||||
try
|
||||
|
@ -74,11 +71,10 @@ public class Symbol extends Z3Object
|
|||
else if (isStringSymbol())
|
||||
return ((StringSymbol) this).getString();
|
||||
else
|
||||
return new String(
|
||||
"Z3Exception: Unknown symbol kind encountered.");
|
||||
return "Z3Exception: Unknown symbol kind encountered.";
|
||||
} catch (Z3Exception ex)
|
||||
{
|
||||
return new String("Z3Exception: " + ex.getMessage());
|
||||
return "Z3Exception: " + ex.getMessage();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -31,11 +31,7 @@ public class Z3Object extends IDisposable
|
|||
{
|
||||
try {
|
||||
dispose();
|
||||
}
|
||||
catch (Throwable t) {
|
||||
throw t;
|
||||
}
|
||||
finally {
|
||||
} finally {
|
||||
super.finalize();
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue