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

Logic simplifications

Browse source 
There is no point in writing "boolean ? true : false" instead of
"boolean"
This commit is contained in:
George Karpenkov 2016-01-06 11:16:30 +01:00
parent 52fdf73178
commit a816b4895c
7 changed files with 21 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -32,8 +32,9 @@ public class BitVecNum extends BitVecExpr
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;
} }
@ -45,8 +46,9 @@ public class BitVecNum extends BitVecExpr
public long getLong() public long getLong()
{ {
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 a long"); throw new Z3Exception("Numeral is not a long");
}
return res.value; return res.value;
} }

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

@ -1537,8 +1537,7 @@ public class Context extends IDisposable
checkContextMatch(t1); checkContextMatch(t1);
checkContextMatch(t2); checkContextMatch(t2);
return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1 return new BoolExpr(this, Native.mkBvaddNoOverflow(nCtx(), t1
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true .getNativeObject(), t2.getNativeObject(), (isSigned)));
: false));
} }
/** /**
@ -1580,8 +1579,7 @@ public class Context extends IDisposable
checkContextMatch(t1); checkContextMatch(t1);
checkContextMatch(t2); checkContextMatch(t2);
return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1 return new BoolExpr(this, Native.mkBvsubNoUnderflow(nCtx(), t1
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true .getNativeObject(), t2.getNativeObject(), (isSigned)));
: false));
} }
/** /**
@ -1621,8 +1619,7 @@ public class Context extends IDisposable
checkContextMatch(t1); checkContextMatch(t1);
checkContextMatch(t2); checkContextMatch(t2);
return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1 return new BoolExpr(this, Native.mkBvmulNoOverflow(nCtx(), t1
.getNativeObject(), t2.getNativeObject(), (isSigned) ? true .getNativeObject(), t2.getNativeObject(), (isSigned)));
: false));
} }
/** /**

4
src/api/java/Goal.java
View file

@ -246,8 +246,8 @@ public class Goal extends Z3Object
Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
{ {
super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false, super(ctx, Native.mkGoal(ctx.nCtx(), (models),
(unsatCores) ? true : false, (proofs) ? true : false)); (unsatCores), (proofs)));
} }
void incRef(long o) void incRef(long o)

4
src/api/java/IntNum.java
View file

@ -36,7 +36,7 @@ public class IntNum extends IntExpr
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,7 +47,7 @@ public class IntNum extends IntExpr
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;
} }

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

@ -92,7 +92,7 @@ public class Model extends Z3Object
return null; return null;
else else
{ {
if (Native.isAsArray(getContext().nCtx(), n) ^ true) if (!Native.isAsArray(getContext().nCtx(), n))
throw new Z3Exception( throw new Z3Exception(
"Argument was not an array constant"); "Argument was not an array constant");
long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
@ -212,8 +212,8 @@ public class Model extends Z3Object
public Expr eval(Expr t, boolean completion) public Expr eval(Expr t, boolean completion)
{ {
Native.LongPtr v = new Native.LongPtr(); Native.LongPtr v = new Native.LongPtr();
if (Native.modelEval(getContext().nCtx(), getNativeObject(), if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
t.getNativeObject(), (completion) ? true : false, v) ^ true) t.getNativeObject(), (completion), v))
throw new ModelEvaluationFailedException(); throw new ModelEvaluationFailedException();
else else
return Expr.create(getContext(), v.value); return Expr.create(getContext(), v.value);

2
src/api/java/Params.java
View file

@ -29,7 +29,7 @@ public class Params extends Z3Object
public void add(Symbol name, boolean value) public void add(Symbol name, boolean value)
{ {
Native.paramsSetBool(getContext().nCtx(), getNativeObject(), Native.paramsSetBool(getContext().nCtx(), getNativeObject(),
name.getNativeObject(), (value) ? true : false); name.getNativeObject(), (value));
} }
/** /**

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

@ -163,15 +163,14 @@ public class Quantifier extends BoolExpr
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall) ? true setNativeObject(Native.mkQuantifier(ctx.nCtx(), (isForall), weight, AST.arrayLength(patterns), AST
: false, weight, AST.arrayLength(patterns), AST
.arrayToNative(patterns), AST.arrayLength(sorts), AST .arrayToNative(patterns), AST.arrayLength(sorts), AST
.arrayToNative(sorts), Symbol.arrayToNative(names), body .arrayToNative(sorts), Symbol.arrayToNative(names), body
.getNativeObject())); .getNativeObject()));
} else } else
{ {
setNativeObject(Native.mkQuantifierEx(ctx.nCtx(), setNativeObject(Native.mkQuantifierEx(ctx.nCtx(),
(isForall) ? true : false, weight, AST.getNativeObject(quantifierID), (isForall), weight, AST.getNativeObject(quantifierID),
AST.getNativeObject(skolemID), AST.getNativeObject(skolemID),
AST.arrayLength(patterns), AST.arrayToNative(patterns), AST.arrayLength(patterns), AST.arrayToNative(patterns),
AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns), AST.arrayLength(noPatterns), AST.arrayToNative(noPatterns),
@ -195,13 +194,13 @@ public class Quantifier extends BoolExpr
if (noPatterns == null && quantifierID == null && skolemID == null) if (noPatterns == null && quantifierID == null && skolemID == null)
{ {
setNativeObject(Native.mkQuantifierConst(ctx.nCtx(), 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(bound), AST.arrayLength(patterns),
AST.arrayToNative(patterns), body.getNativeObject())); AST.arrayToNative(patterns), body.getNativeObject()));
} else } else
{ {
setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(), setNativeObject(Native.mkQuantifierConstEx(ctx.nCtx(),
(isForall) ? true : false, weight, isForall, weight,
AST.getNativeObject(quantifierID), AST.getNativeObject(quantifierID),
AST.getNativeObject(skolemID), AST.arrayLength(bound), AST.getNativeObject(skolemID), AST.arrayLength(bound),
AST.arrayToNative(bound), AST.arrayLength(patterns), AST.arrayToNative(bound), AST.arrayLength(patterns),
@ -215,6 +214,7 @@ public class Quantifier extends BoolExpr
super(ctx, obj); super(ctx, obj);
} }
@Override
void checkNativeObject(long obj) void checkNativeObject(long obj)
{ {
if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_QUANTIFIER_AST