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

Added braces

Browse source 
Lack of braces on multi-line statements is considered very scary in
Java.
This commit is contained in:
George Karpenkov 2016-01-06 11:14:53 +01:00
parent ccd88a63a5
commit c435bc379b
8 changed files with 84 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/api/java/AST.java
View file

@ -53,15 +53,10 @@ public class AST extends Z3Object implements Comparable<AST>
@Override @Override
public int compareTo(AST other) public int compareTo(AST other)
{ {
if (other == null) if (other == null) {
return 1; return 1;
}
if (getId() < other.getId()) return Integer.compare(getId(), other.getId());
return -1;
else if (getId() > other.getId())
return +1;
else
return 0;
} }
/** /**
@ -94,11 +89,12 @@ public class AST extends Z3Object implements Comparable<AST>
public AST translate(Context ctx) public AST translate(Context ctx)
{ {
if (getContext() == ctx) if (getContext() == ctx) {
return this; return this;
else } else {
return new AST(ctx, Native.translate(getContext().nCtx(), return new AST(ctx, Native.translate(getContext().nCtx(),
getNativeObject(), ctx.nCtx())); getNativeObject(), ctx.nCtx()));
}
} }
/** /**

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

@ -110,8 +110,9 @@ public class Context extends IDisposable
**/ **/
public BoolSort getBoolSort() public BoolSort getBoolSort()
{ {
if (m_boolSort == null) if (m_boolSort == null) {
m_boolSort = new BoolSort(this); m_boolSort = new BoolSort(this);
}
return m_boolSort; return m_boolSort;
} }
@ -120,8 +121,9 @@ public class Context extends IDisposable
**/ **/
public IntSort getIntSort() public IntSort getIntSort()
{ {
if (m_intSort == null) if (m_intSort == null) {
m_intSort = new IntSort(this); m_intSort = new IntSort(this);
}
return m_intSort; return m_intSort;
} }
@ -130,8 +132,9 @@ public class Context extends IDisposable
**/ **/
public RealSort getRealSort() public RealSort getRealSort()
{ {
if (m_realSort == null) if (m_realSort == null) {
m_realSort = new RealSort(this); m_realSort = new RealSort(this);
}
return m_realSort; return m_realSort;
} }
@ -148,8 +151,9 @@ public class Context extends IDisposable
**/ **/
public SeqSort getStringSort() public SeqSort getStringSort()
{ {
if (m_stringSort == null) if (m_stringSort == null) {
m_stringSort = mkStringSort(); m_stringSort = mkStringSort();
}
return m_stringSort; return m_stringSort;
} }

55
src/api/java/Expr.java
View file

@ -53,14 +53,16 @@ public class Expr extends AST
public Expr simplify(Params p) public Expr simplify(Params p)
{ {
if (p == null) if (p == null) {
return Expr.create(getContext(), return Expr.create(getContext(),
Native.simplify(getContext().nCtx(), getNativeObject())); Native.simplify(getContext().nCtx(), getNativeObject()));
else }
else {
return Expr.create( return Expr.create(
getContext(), getContext(),
Native.simplifyEx(getContext().nCtx(), getNativeObject(), Native.simplifyEx(getContext().nCtx(), getNativeObject(),
p.getNativeObject())); p.getNativeObject()));
}
} }
/** /**
@ -106,9 +108,10 @@ public class Expr extends AST
{ {
int n = getNumArgs(); int n = getNumArgs();
Expr[] res = new Expr[n]; Expr[] res = new Expr[n];
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++) {
res[i] = Expr.create(getContext(), res[i] = Expr.create(getContext(),
Native.getAppArg(getContext().nCtx(), getNativeObject(), i)); Native.getAppArg(getContext().nCtx(), getNativeObject(), i));
}
return res; return res;
} }
@ -122,10 +125,11 @@ public class Expr extends AST
public void update(Expr[] args) public void update(Expr[] args)
{ {
getContext().checkContextMatch(args); getContext().checkContextMatch(args);
if (isApp() && args.length != getNumArgs()) if (isApp() && args.length != getNumArgs()) {
throw new Z3Exception("Number of arguments does not match"); throw new Z3Exception("Number of arguments does not match");
}
setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(), setNativeObject(Native.updateTerm(getContext().nCtx(), getNativeObject(),
(int) args.length, Expr.arrayToNative(args))); args.length, Expr.arrayToNative(args)));
} }
/** /**
@ -144,10 +148,11 @@ public class Expr extends AST
{ {
getContext().checkContextMatch(from); getContext().checkContextMatch(from);
getContext().checkContextMatch(to); getContext().checkContextMatch(to);
if (from.length != to.length) if (from.length != to.length) {
throw new Z3Exception("Argument sizes do not match"); throw new Z3Exception("Argument sizes do not match");
}
return Expr.create(getContext(), Native.substitute(getContext().nCtx(), return Expr.create(getContext(), Native.substitute(getContext().nCtx(),
getNativeObject(), (int) from.length, Expr.arrayToNative(from), getNativeObject(), from.length, Expr.arrayToNative(from),
Expr.arrayToNative(to))); Expr.arrayToNative(to)));
} }
@ -160,7 +165,6 @@ public class Expr extends AST
**/ **/
public Expr substitute(Expr from, Expr to) public Expr substitute(Expr from, Expr to)
{ {
return substitute(new Expr[] { from }, new Expr[] { to }); return substitute(new Expr[] { from }, new Expr[] { to });
} }
@ -179,7 +183,7 @@ public class Expr extends AST
getContext().checkContextMatch(to); getContext().checkContextMatch(to);
return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(), return Expr.create(getContext(), Native.substituteVars(getContext().nCtx(),
getNativeObject(), (int) to.length, Expr.arrayToNative(to))); getNativeObject(), to.length, Expr.arrayToNative(to)));
} }
/** /**
@ -193,14 +197,14 @@ public class Expr extends AST
**/ **/
public Expr translate(Context ctx) public Expr translate(Context ctx)
{ {
if (getContext() == ctx) {
if (getContext() == ctx)
return this; return this;
else } else {
return Expr.create( return Expr.create(
ctx, ctx,
Native.translate(getContext().nCtx(), getNativeObject(), Native.translate(getContext().nCtx(), getNativeObject(),
ctx.nCtx())); ctx.nCtx()));
}
} }
/** /**
@ -2123,8 +2127,9 @@ public class Expr extends AST
{ {
if (!Native.isApp(getContext().nCtx(), 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_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"); throw new Z3Exception("Underlying object is not a term");
}
super.checkNativeObject(obj); super.checkNativeObject(obj);
} }
@ -2188,10 +2193,10 @@ public class Expr extends AST
return new FPRMExpr(ctx, obj); return new FPRMExpr(ctx, obj);
case Z3_FINITE_DOMAIN_SORT: case Z3_FINITE_DOMAIN_SORT:
return new FiniteDomainExpr(ctx, obj); return new FiniteDomainExpr(ctx, obj);
case Z3_SEQ_SORT: case Z3_SEQ_SORT:
return new SeqExpr(ctx, obj); return new SeqExpr(ctx, obj);
case Z3_RE_SORT: case Z3_RE_SORT:
return new ReExpr(ctx, obj); return new ReExpr(ctx, obj);
default: ; default: ;
} }

6
src/api/java/FiniteDomainNum.java
View file

@ -36,8 +36,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
public int getInt() public int getInt()
{ {
Native.IntPtr res = new Native.IntPtr(); 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"); throw new Z3Exception("Numeral is not an int");
}
return res.value; return res.value;
} }
@ -47,8 +48,9 @@ public class FiniteDomainNum extends FiniteDomainExpr
public long getInt64() public long getInt64()
{ {
Native.LongPtr res = new Native.LongPtr(); 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"); throw new Z3Exception("Numeral is not an int64");
}
return res.value; return res.value;
} }

5
src/api/java/Global.java
View file

@ -57,10 +57,11 @@ public final class Global
public static String getParameter(String id) public static String getParameter(String id)
{ {
Native.StringPtr res = new Native.StringPtr(); Native.StringPtr res = new Native.StringPtr();
if (!Native.globalParamGet(id, res)) if (!Native.globalParamGet(id, res)) {
return null; return null;
else } else {
return res.value; return res.value;
}
} }
/** /**

11
src/api/java/Optimize.java
View file

@ -183,11 +183,12 @@ public class Optimize extends Z3Object
**/ **/
public Model getModel() public Model getModel()
{ {
long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject()); long x = Native.optimizeGetModel(getContext().nCtx(), getNativeObject());
if (x == 0) if (x == 0) {
return null; return null;
else } else {
return new Model(getContext(), x); return new Model(getContext(), x);
}
} }
/** /**

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

@ -201,13 +201,14 @@ public class Solver extends Z3Object
public Status check(Expr... assumptions) public Status check(Expr... assumptions)
{ {
Z3_lbool r; Z3_lbool r;
if (assumptions == null) if (assumptions == null) {
r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(), r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
getNativeObject())); getNativeObject()));
else } else {
r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext() r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
.nCtx(), getNativeObject(), (int) assumptions.length, AST .nCtx(), getNativeObject(), assumptions.length, AST
.arrayToNative(assumptions))); .arrayToNative(assumptions)));
}
switch (r) switch (r)
{ {
case Z3_L_TRUE: case Z3_L_TRUE:
@ -243,10 +244,11 @@ public class Solver extends Z3Object
public Model getModel() public Model getModel()
{ {
long x = Native.solverGetModel(getContext().nCtx(), getNativeObject()); long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
if (x == 0) if (x == 0) {
return null; return null;
else } else {
return new Model(getContext(), x); return new Model(getContext(), x);
}
} }
/** /**
@ -261,10 +263,11 @@ public class Solver extends Z3Object
public Expr getProof() public Expr getProof()
{ {
long x = Native.solverGetProof(getContext().nCtx(), getNativeObject()); long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
if (x == 0) if (x == 0) {
return null; return null;
else } else {
return Expr.create(getContext(), x); return Expr.create(getContext(), x);
}
} }
/** /**

24
src/api/java/Statistics.java
View file

@ -72,12 +72,13 @@ public class Statistics extends Z3Object
**/ **/
public String getValueString() public String getValueString()
{ {
if (isUInt()) if (isUInt()) {
return Integer.toString(m_int); return Integer.toString(m_int);
else if (isDouble()) } else if (isDouble()) {
return Double.toString(m_double); return Double.toString(m_double);
else } else {
throw new Z3Exception("Unknown statistical entry type"); throw new Z3Exception("Unknown statistical entry type");
}
} }
/** /**
@ -150,14 +151,15 @@ public class Statistics extends Z3Object
{ {
Entry e; Entry e;
String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i); 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(), e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
getNativeObject(), i)); getNativeObject(), i));
else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(), e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
getNativeObject(), i)); getNativeObject(), i));
else } else {
throw new Z3Exception("Unknown data entry value"); throw new Z3Exception("Unknown data entry value");
}
res[i] = e; res[i] = e;
} }
return res; return res;
@ -186,9 +188,11 @@ public class Statistics extends Z3Object
{ {
int n = size(); int n = size();
Entry[] es = getEntries(); Entry[] es = getEntries();
for (int i = 0; i < n; i++) for (int i = 0; i < n; i++) {
if (es[i].Key == key) if (es[i].Key.equals(key)) {
return es[i]; return es[i];
}
}
return null; return null;
} }