From a816b4895ce3eca95784ee85fafaa6aabcda5d27 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Wed, 6 Jan 2016 11:16:30 +0100 Subject: [PATCH] Logic simplifications There is no point in writing "boolean ? true : false" instead of "boolean" --- src/api/java/BitVecNum.java | 6 ++++-- src/api/java/Context.java | 9 +++------ src/api/java/Goal.java | 4 ++-- src/api/java/IntNum.java | 4 ++-- src/api/java/Model.java | 6 +++--- src/api/java/Params.java | 2 +- src/api/java/Quantifier.java | 12 ++++++------ 7 files changed, 21 insertions(+), 22 deletions(-) diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index cd5e789b9..5a62f8087 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -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; } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 29f353f07..f1baa92f2 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1537,8 +1537,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))); } /** @@ -1580,8 +1579,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))); } /** @@ -1621,8 +1619,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))); } /** diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java index 41d4e27ac..46b04f6bf 100644 --- a/src/api/java/Goal.java +++ b/src/api/java/Goal.java @@ -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) diff --git a/src/api/java/IntNum.java b/src/api/java/IntNum.java index 4078b3db3..71d878311 100644 --- a/src/api/java/IntNum.java +++ b/src/api/java/IntNum.java @@ -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; } diff --git a/src/api/java/Model.java b/src/api/java/Model.java index 16613af68..795a08fe8 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -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); diff --git a/src/api/java/Params.java b/src/api/java/Params.java index 8eef253b0..25d009b12 100644 --- a/src/api/java/Params.java +++ b/src/api/java/Params.java @@ -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)); } /** diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index 08df1c1f5..1b425d3e4 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -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