From 1137be19eb0db13066d1376e40ad9744e9841eaf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 21:47:15 +0200 Subject: [PATCH 01/13] Change underlying type of IntLitExpr to BigInteger in core --- .../bme/mit/theta/core/clock/op/ClockOps.java | 4 +- .../core/dsl/impl/ExprCreatorVisitor.java | 3 +- .../theta/core/parser/CoreInterpreter.java | 3 +- .../mit/theta/core/type/bvtype/BvLitExpr.java | 2 +- .../theta/core/type/inttype/IntAddExpr.java | 5 +- .../mit/theta/core/type/inttype/IntExprs.java | 7 ++ .../theta/core/type/inttype/IntLitExpr.java | 78 ++++++++++--------- .../theta/core/type/inttype/IntMulExpr.java | 5 +- .../mit/theta/core/utils/ExprSimplifier.java | 23 +++--- .../theta/core/utils/ExprSimplifierTest.java | 2 + 10 files changed, 75 insertions(+), 57 deletions(-) diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java index a72c6dfbfb..56a85fb3b9 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java @@ -102,7 +102,7 @@ public ClockOp visit(final AssignStmt stmt, fi if (expr instanceof IntLitExpr) { final IntLitExpr intLit = (IntLitExpr) expr; - final int value = Math.toIntExact(intLit.getValue()); + final int value = Math.toIntExact(intLit.getValue().longValue()); return Reset(varDecl, value); } else if (expr instanceof RefExpr) { @@ -132,7 +132,7 @@ public ClockOp visit(final AssignStmt stmt, fi } else if (ops[1].equals(varRef)) { if (ops[0] instanceof IntLitExpr) { final IntLitExpr intLit = (IntLitExpr) ops[0]; - final int offset = Math.toIntExact(intLit.getValue()); + final int offset = Math.toIntExact(intLit.getValue().longValue()); return Shift(varDecl, offset); } } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java index 6ffef43623..ecffce7327 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java @@ -51,6 +51,7 @@ import static hu.bme.mit.theta.core.utils.TypeUtils.castBv; import static java.util.stream.Collectors.toList; +import java.math.BigInteger; import java.util.Collection; import java.util.Collections; import java.util.List; @@ -589,7 +590,7 @@ public FalseExpr visitFalseExpr(final FalseExprContext ctx) { @Override public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { - final int value = Integer.parseInt(ctx.value.getText()); + final var value = new BigInteger(ctx.value.getText()); return Int(value); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/parser/CoreInterpreter.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/parser/CoreInterpreter.java index 81a4f7ddbe..95df444f5e 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/parser/CoreInterpreter.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/parser/CoreInterpreter.java @@ -24,6 +24,7 @@ import static hu.bme.mit.theta.core.type.anytype.Exprs.Ref; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import java.math.BigInteger; import java.util.List; import java.util.function.BiFunction; import java.util.function.BinaryOperator; @@ -181,7 +182,7 @@ public Expr expr(final SExpr sexpr) { } else if (object instanceof Decl) { return Ref((Decl) object); } else if (object instanceof Integer) { - return Int((Integer) object); + return Int(BigInteger.valueOf((Integer) object)); } else { throw new UnsupportedOperationException(); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java index e8aa328228..59eddf8c5f 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvLitExpr.java @@ -248,7 +248,7 @@ public BoolLitExpr geq(final BvLitExpr that) { } public IntLitExpr toInt() { - return Int(BvUtils.bvLitExprToBigInteger(this).intValue()); + return Int(BvUtils.bvLitExprToBigInteger(this)); } @Override diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntAddExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntAddExpr.java index 1d19ccd4bf..5be645e42e 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntAddExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntAddExpr.java @@ -19,6 +19,7 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; +import java.math.BigInteger; import java.util.List; import hu.bme.mit.theta.core.model.Valuation; @@ -49,10 +50,10 @@ public IntType getType() { @Override public IntLitExpr eval(final Valuation val) { - int sum = 0; + var sum = BigInteger.ZERO; for (final Expr op : getOps()) { final IntLitExpr opVal = (IntLitExpr) op.eval(val); - sum += opVal.getValue(); + sum = sum.add(opVal.getValue()); } return Int(sum); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java index f0f028b11f..0af2281387 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java @@ -19,6 +19,8 @@ import hu.bme.mit.theta.core.type.Expr; +import java.math.BigInteger; + public final class IntExprs { private IntExprs() { @@ -28,10 +30,15 @@ public static IntType Int() { return IntType.getInstance(); } + @Deprecated public static IntLitExpr Int(final int value) { return IntLitExpr.of(value); } + public static IntLitExpr Int(final BigInteger value) { + return IntLitExpr.of(value); + } + public static IntToRatExpr ToRat(final Expr op) { return IntToRatExpr.of(op); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java index 1a219e1f0c..2ef70e48c9 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java @@ -34,17 +34,21 @@ public final class IntLitExpr extends NullaryExpr implements LitExpr= 0; + assert result.compareTo(BigInteger.ZERO) >= 0; return IntLitExpr.of(result); } @@ -109,49 +113,49 @@ public IntLitExpr rem(final IntLitExpr that) { // 5 rem -3 = -2 // -5 rem 3 = 1 // -5 rem -3 = -1 - final int thisAbs = Math.abs(this.value); - final int thatAbs = Math.abs(that.value); - if (this.value < 0 && that.value < 0) { - int result = thisAbs % thatAbs; - if (result != 0) { - result -= thatAbs; + final var thisAbs = this.value.abs(); + final var thatAbs = that.value.abs(); + if (this.value.compareTo(BigInteger.ZERO) < 0 && that.value.compareTo(BigInteger.ZERO) < 0) { + var result = thisAbs.mod(thatAbs); + if (result.compareTo(BigInteger.ZERO) != 0) { + result = result.subtract(thatAbs); } return new IntLitExpr(result); - } else if (this.value >= 0 && that.value < 0) { - return new IntLitExpr(-(thisAbs % thatAbs)); - } else if (this.value < 0 && that.value >= 0) { - int result = thisAbs % thatAbs; - if (result != 0) { - result = thatAbs - result; + } else if (this.value.compareTo(BigInteger.ZERO) >= 0 && that.value.compareTo(BigInteger.ZERO) < 0) { + return new IntLitExpr(thisAbs.mod(thatAbs).negate()); + } else if (this.value.compareTo(BigInteger.ZERO) < 0 && that.value.compareTo(BigInteger.ZERO) >= 0) { + var result = thisAbs.mod(thatAbs); + if (result.compareTo(BigInteger.ZERO) != 0) { + result = thatAbs.subtract(result); } return IntLitExpr.of(result); } else { - return IntLitExpr.of(this.value % that.value); + return IntLitExpr.of(this.value.mod(that.value)); } } public BoolLitExpr eq(final IntLitExpr that) { - return Bool(this.value == that.value); + return Bool(this.value.compareTo(that.value) == 0); } public BoolLitExpr neq(final IntLitExpr that) { - return Bool(this.value != that.value); + return Bool(this.value.compareTo(that.value) != 0); } public BoolLitExpr lt(final IntLitExpr that) { - return Bool(this.value < that.value); + return Bool(this.value.compareTo(that.value) < 0); } public BoolLitExpr leq(final IntLitExpr that) { - return Bool(this.value <= that.value); + return Bool(this.value.compareTo(that.value) <= 0); } public BoolLitExpr gt(final IntLitExpr that) { - return Bool(this.value > that.value); + return Bool(this.value.compareTo(that.value) > 0); } public BoolLitExpr geq(final IntLitExpr that) { - return Bool(this.value >= that.value); + return Bool(this.value.compareTo(that.value) >= 0); } @Override @@ -159,7 +163,7 @@ public int hashCode() { int result = hashCode; if (result == 0) { result = HASH_SEED; - result = 31 * result + value; + result = 31 * result + value.hashCode(); hashCode = result; } return result; @@ -171,7 +175,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof IntLitExpr) { final IntLitExpr that = (IntLitExpr) obj; - return this.getValue() == that.getValue(); + return this.getValue().compareTo(that.getValue()) == 0; } else { return false; } @@ -179,12 +183,12 @@ public boolean equals(final Object obj) { @Override public String toString() { - return Long.toString(getValue()); + return getValue().toString(); } @Override public int compareTo(final IntLitExpr that) { - return Long.compare(this.getValue(), that.getValue()); + return this.getValue().compareTo(that.getValue()); } } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntMulExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntMulExpr.java index 66f8a417b7..0c81fb0d43 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntMulExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntMulExpr.java @@ -19,6 +19,7 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; +import java.math.BigInteger; import java.util.List; import hu.bme.mit.theta.core.model.Valuation; @@ -49,10 +50,10 @@ public IntType getType() { @Override public IntLitExpr eval(final Valuation val) { - int prod = 1; + var prod = BigInteger.ONE; for (final Expr op : getOps()) { final IntLitExpr opVal = (IntLitExpr) op.eval(val); - prod *= opVal.getValue(); + prod = prod.multiply(opVal.getValue()); } return Int(prod); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 266260acea..1753c0bd4b 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -23,6 +23,7 @@ import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import java.math.BigInteger; import java.util.ArrayList; import java.util.Iterator; import java.util.List; @@ -721,24 +722,24 @@ private static Expr simplifyIntAdd(final IntAddExpr expr, final Valuati ops.add(opVisited); } } - int value = 0; + var value = BigInteger.ZERO; for (final Iterator> iterator = ops.iterator(); iterator.hasNext(); ) { final Expr op = iterator.next(); if (op instanceof IntLitExpr) { final IntLitExpr litOp = (IntLitExpr) op; - value = value + litOp.getValue(); + value = value.add(litOp.getValue()); iterator.remove(); } } - if (value != 0) { + if (value.compareTo(BigInteger.ZERO) != 0) { final Expr sum = Int(value); ops.add(sum); } if (ops.isEmpty()) { - return Int(0); + return Int(BigInteger.ZERO); } else if (ops.size() == 1) { return Utils.singleElementOf(ops); } @@ -758,7 +759,7 @@ private static Expr simplifyIntSub(final IntSubExpr expr, final Valuati if (leftOp instanceof RefExpr && rightOp instanceof RefExpr) { if (leftOp.equals(rightOp)) { - return Int(0); + return Int(BigInteger.ZERO); } } @@ -792,26 +793,26 @@ private static Expr simplifyIntMul(final IntMulExpr expr, final Valuati } } - int value = 1; + var value = BigInteger.ONE; for (final Iterator> iterator = ops.iterator(); iterator.hasNext(); ) { final Expr op = iterator.next(); if (op instanceof IntLitExpr) { final IntLitExpr litOp = (IntLitExpr) op; - value = value * litOp.getValue(); + value = value.multiply(litOp.getValue()); iterator.remove(); - if (value == 0) { - return Int(0); + if (value.compareTo(BigInteger.ZERO) == 0) { + return Int(BigInteger.ZERO); } } } - if (value != 1) { + if (value.compareTo(BigInteger.ONE) != 0) { final Expr prod = Int(value); ops.add(0, prod); } if (ops.isEmpty()) { - return Int(1); + return Int(BigInteger.ONE); } else if (ops.size() == 1) { return Utils.singleElementOf(ops); } diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index ef4b9b3718..52a210ccfa 100644 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -74,6 +74,7 @@ import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.type.rattype.RatType; +import java.math.BigInteger; import java.util.List; import java.util.ArrayList; @@ -269,6 +270,7 @@ public void testIntAdd() { assertEquals(Add(a, Int(4)), simplify(Add(Int(1), Add(a, Int(3))))); assertEquals(a, simplify(Add(Int(-3), a, Int(3)))); assertEquals(Add(a, b, a, b, c), simplify(Add(a, Add(b, Add(a, Add(b, c)))))); + assertEquals(Int(new BigInteger("4294967294")), simplify(Add(Int(Integer.MAX_VALUE), Int(Integer.MAX_VALUE)))); } @Test From 3bd8e9b794c0d67813dc300630e4cdc849289d2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:03:19 +0200 Subject: [PATCH 02/13] Change underlying type of IntLitExpr to BigInteger in solver --- .../main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java | 2 +- .../main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index f74c4fa79c..5ec6b0e19a 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -450,7 +450,7 @@ private com.microsoft.z3.Expr transformRatLt(final RatLtExpr expr) { */ private com.microsoft.z3.Expr transformIntLit(final IntLitExpr expr) { - return context.mkInt(expr.getValue()); + return context.mkInt(expr.getValue().toString()); } private com.microsoft.z3.Expr transformIntAdd(final IntAddExpr expr) { diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java index 57e5e42ccf..ee2a9fdf53 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java @@ -178,7 +178,7 @@ private Expr transform(final com.microsoft.z3.Expr term, final Model model, private Expr transformIntLit(final com.microsoft.z3.Expr term) { final com.microsoft.z3.IntNum intNum = (com.microsoft.z3.IntNum) term; - final int value = intNum.getInt(); + final var value = intNum.getBigInteger(); return Int(value); } From 08c49d40f4647acee6fd38355d476fa3e663a1a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:18:52 +0200 Subject: [PATCH 03/13] Change underlying type of IntLitExpr to BigInteger in xta --- .../src/main/java/hu/bme/mit/theta/xta/dsl/XtaType.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaType.java b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaType.java index 273c8d05c8..1424e6fb35 100644 --- a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaType.java +++ b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaType.java @@ -121,8 +121,8 @@ public Type visitRangeType(final RangeTypeContext ctx) { final IntLitExpr lowerLitExpr = (IntLitExpr) ExprUtils.simplify(lowerExpr); final IntLitExpr upperLitExpr = (IntLitExpr) ExprUtils.simplify(upperExpr); - final int lower = lowerLitExpr.getValue(); - final int upper = upperLitExpr.getValue(); + final int lower = lowerLitExpr.getValue().intValue(); + final int upper = upperLitExpr.getValue().intValue(); final Type result = RangeType.Range(lower, upper); return result; @@ -156,7 +156,7 @@ public Type visitIdIndex(final IdIndexContext ctx) { final Object value = env.compute(variableSymbol, v -> v.instantiate("", env).asConstant().getExpr()); final IntLitExpr elemCount = (IntLitExpr) value; - final Type result = RangeType.Range(0, elemCount.getValue() - 1); + final Type result = RangeType.Range(0, elemCount.getValue().intValue() - 1); return result; } else if (symbol instanceof XtaTypeSymbol) { @@ -174,7 +174,7 @@ public Type visitExpressionIndex(final ExpressionIndexContext ctx) { final XtaExpression expression = new XtaExpression(scope, ctx.fExpression); final Expr expr = expression.instantiate(env); final IntLitExpr elemCount = (IntLitExpr) expr; - final Type result = RangeType.Range(0, elemCount.getValue() - 1); + final Type result = RangeType.Range(0, elemCount.getValue().intValue() - 1); return result; } From 0be52670a351508d49351f3b8381a3cd13623ff1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:19:13 +0200 Subject: [PATCH 04/13] Change underlying type of IntLitExpr to BigInteger in grammars --- .../src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java | 2 +- .../main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java | 1 - .../java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java | 3 ++- .../src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java | 3 ++- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index 1238c93c65..51ca2d693e 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -626,7 +626,7 @@ public FalseExpr visitFalseExpr(final FalseExprContext ctx) { @Override public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { - final int value = Integer.parseInt(ctx.value.getText()); + final var value = new BigInteger(ctx.value.getText()); return Int(value); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java index 0af2281387..ac6b8b5d96 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java @@ -30,7 +30,6 @@ public static IntType Int() { return IntType.getInstance(); } - @Deprecated public static IntLitExpr Int(final int value) { return IntLitExpr.of(value); } diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java index c651c18cc1..5f96203fce 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java +++ b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java @@ -41,6 +41,7 @@ import static hu.bme.mit.theta.sts.dsl.StsDslHelper.createParamList; import static java.util.stream.Collectors.toList; +import java.math.BigInteger; import java.util.Collection; import java.util.List; import java.util.Optional; @@ -519,7 +520,7 @@ public FalseExpr visitFalseExpr(final FalseExprContext ctx) { @Override public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { - final int value = Integer.parseInt(ctx.value.getText()); + final var value = new BigInteger(ctx.value.getText()); return Int(value); } diff --git a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java index 464bed9b89..e35de6f1db 100644 --- a/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java +++ b/subprojects/xta/src/main/java/hu/bme/mit/theta/xta/dsl/XtaExpression.java @@ -41,6 +41,7 @@ import hu.bme.mit.theta.xta.dsl.gen.XtaDslParser.*; import hu.bme.mit.theta.xta.utils.LabelExpr; +import java.math.BigInteger; import java.util.Collection; import java.util.List; import java.util.stream.Stream; @@ -97,7 +98,7 @@ public Expr visitParenthesisExpression(final ParenthesisExpressionContext ctx @Override public Expr visitNatExpression(final NatExpressionContext ctx) { - final int value = Integer.parseInt(ctx.fValue.getText()); + final var value = new BigInteger(ctx.fValue.getText()); return Int(value); } From d10a962efc765021564ef267f907818fa2a7ee19 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:44:10 +0200 Subject: [PATCH 05/13] Change underlying type of RatLitExpr to BigInteger in core --- .../theta/core/clock/constr/ClockConstrs.java | 4 +- .../bme/mit/theta/core/clock/op/ClockOps.java | 4 +- .../core/dsl/impl/ExprCreatorVisitor.java | 4 +- .../theta/core/type/inttype/IntLitExpr.java | 2 +- .../theta/core/type/rattype/RatAddExpr.java | 17 +-- .../mit/theta/core/type/rattype/RatExprs.java | 15 +++ .../theta/core/type/rattype/RatLitExpr.java | 104 ++++++++++-------- .../theta/core/type/rattype/RatMulExpr.java | 9 +- .../mit/theta/core/utils/ExprSimplifier.java | 18 +-- .../mit/theta/core/expr/RatLitExprTest.java | 9 +- 10 files changed, 108 insertions(+), 78 deletions(-) diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java index 0fb60c0df9..a72225f5af 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/constr/ClockConstrs.java @@ -291,8 +291,8 @@ private static int extractConstrRhs(final BinaryExpr expr) { if (rightOp instanceof RatLitExpr) { final RatLitExpr ratLit = (RatLitExpr) rightOp; - if (ratLit.getDenom() == 1) { - final int num = ratLit.getNum(); + if (ratLit.getDenom().intValue() == 1) { + final int num = ratLit.getNum().intValue(); return num; } } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java index 56a85fb3b9..39962ca929 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/clock/op/ClockOps.java @@ -123,8 +123,8 @@ public ClockOp visit(final AssignStmt stmt, fi if (ops[0].equals(varRef)) { if (ops[1] instanceof RatLitExpr) { final RatLitExpr ratLit = (RatLitExpr) ops[1]; - final int num = ratLit.getNum(); - final int denom = ratLit.getDenom(); + final int num = ratLit.getNum().intValue(); + final int denom = ratLit.getDenom().intValue(); if (denom == 1) { return Shift(varDecl, num); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java index ecffce7327..753a4a4a83 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/impl/ExprCreatorVisitor.java @@ -596,8 +596,8 @@ public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { @Override public RatLitExpr visitRatLitExpr(final RatLitExprContext ctx) { - final int num = Integer.parseInt(ctx.num.getText()); - final int denom = Integer.parseInt(ctx.denom.getText()); + final var num = new BigInteger(ctx.num.getText()); + final var denom = new BigInteger(ctx.denom.getText()); return Rat(num, denom); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java index 2ef70e48c9..611fae83da 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java @@ -63,7 +63,7 @@ public IntLitExpr eval(final Valuation val) { } public RatLitExpr toRat() { - return Rat(this.value.intValue(), 1); + return Rat(this.value, 1); } public BvLitExpr toBv(int size, boolean isSigned) { diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatAddExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatAddExpr.java index 2373050de9..7c458a9908 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatAddExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatAddExpr.java @@ -19,6 +19,7 @@ import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; +import java.math.BigInteger; import java.util.List; import hu.bme.mit.theta.core.model.Valuation; @@ -49,16 +50,16 @@ public RatType getType() { @Override public RatLitExpr eval(final Valuation val) { - int sumNum = 0; - int sumDenom = 1; + var sumNum = BigInteger.ZERO; + var sumDenom = BigInteger.ONE; for (final Expr op : getOps()) { final RatLitExpr opLit = (RatLitExpr) op.eval(val); - final int leftNum = sumNum; - final int leftDenom = sumDenom; - final int rightNum = opLit.getNum(); - final int rightDenom = opLit.getDenom(); - sumNum = leftNum * rightDenom + leftDenom * rightNum; - sumDenom = leftDenom * rightDenom; + final var leftNum = sumNum; + final var leftDenom = sumDenom; + final var rightNum = opLit.getNum(); + final var rightDenom = opLit.getDenom(); + sumNum = leftNum.multiply(rightDenom).add(leftDenom.multiply(rightNum)); + sumDenom = leftDenom.multiply(rightDenom); } return Rat(sumNum, sumDenom); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java index 8bad2720f0..dc7f70e251 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java @@ -19,6 +19,8 @@ import hu.bme.mit.theta.core.type.Expr; +import java.math.BigInteger; + public final class RatExprs { private RatExprs() { @@ -28,10 +30,23 @@ public static RatType Rat() { return RatType.getInstance(); } + @Deprecated public static RatLitExpr Rat(final int num, final int denom) { return RatLitExpr.of(num, denom); } + public static RatLitExpr Rat(final BigInteger num, final int denom) { + return RatLitExpr.of(num, denom); + } + + public static RatLitExpr Rat(final int num, final BigInteger denom) { + return RatLitExpr.of(num, denom); + } + + public static RatLitExpr Rat(final BigInteger num, final BigInteger denom) { + return RatLitExpr.of(num, denom); + } + public static RatAddExpr Add(final Iterable> ops) { return RatAddExpr.of(ops); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java index 45dac9419b..bc6c4c39d1 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java @@ -15,43 +15,55 @@ */ package hu.bme.mit.theta.core.type.rattype; -import static com.google.common.base.Preconditions.checkArgument; -import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; -import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; - -import com.google.common.math.IntMath; - import hu.bme.mit.theta.core.model.Valuation; import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.NullaryExpr; import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; +import java.math.BigInteger; + +import static com.google.common.base.Preconditions.checkArgument; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; + public final class RatLitExpr extends NullaryExpr implements LitExpr, Comparable { private static final int HASH_SEED = 149; - private final int num; - private final int denom; + private final BigInteger num; + private final BigInteger denom; private volatile int hashCode = 0; - private RatLitExpr(final int num, final int denom) { - checkArgument(denom != 0); + private RatLitExpr(final BigInteger num, final BigInteger denom) { + checkArgument(denom.compareTo(BigInteger.ZERO) != 0); - final int gcd = IntMath.gcd(Math.abs(num), Math.abs(denom)); - if (denom >= 0) { - this.num = num / gcd; - this.denom = denom / gcd; + final var gcd = num.abs().gcd(denom.abs()); + if (denom.compareTo(BigInteger.ZERO) >= 0) { + this.num = num.divide(gcd); + this.denom = denom.divide(gcd); } else { - this.num = -num / gcd; - this.denom = -denom / gcd; + this.num = num.divide(gcd).negate(); + this.denom = denom.divide(gcd).negate(); } } - public static RatLitExpr of(final int num, final int denom) { + public static RatLitExpr of(final BigInteger num, final BigInteger denom) { return new RatLitExpr(num, denom); } + public static RatLitExpr of(final BigInteger num, final int denom) { + return new RatLitExpr(num, BigInteger.valueOf(denom)); + } + + public static RatLitExpr of(final int num, final BigInteger denom) { + return new RatLitExpr(BigInteger.valueOf(num), denom); + } + + public static RatLitExpr of(final int num, final int denom) { + return new RatLitExpr(BigInteger.valueOf(num), BigInteger.valueOf(denom)); + } + @Override public RatType getType() { return Rat(); @@ -62,82 +74,82 @@ public LitExpr eval(final Valuation val) { return this; } - public int getNum() { + public BigInteger getNum() { return num; } - public int getDenom() { + public BigInteger getDenom() { return denom; } public int sign() { - return (num < 0) ? -1 : (num == 0) ? 0 : 1; + return num.signum(); } - public int floor() { - if (num >= 0 || num % denom == 0) { - return num / denom; + public BigInteger floor() { + if (num.compareTo(BigInteger.ZERO) >= 0 || num.mod(denom).compareTo(BigInteger.ZERO) == 0) { + return num.divide(denom); } else { - return num / denom - 1; + return num.divide(denom).subtract(BigInteger.ONE); } } - public int ceil() { - if (num <= 0 || num % denom == 0) { - return num / denom; + public BigInteger ceil() { + if (num.compareTo(BigInteger.ZERO) <= 0 || num.mod(denom).compareTo(BigInteger.ZERO) == 0) { + return num.divide(denom); } else { - return num / denom + 1; + return num.divide(denom).add(BigInteger.ONE); } } public RatLitExpr add(final RatLitExpr that) { - return RatLitExpr.of(this.getNum() * that.getDenom() + this.getDenom() * that.getNum(), - this.getDenom() * that.getDenom()); + return RatLitExpr.of(this.getNum().multiply(that.getDenom()).add(this.getDenom().multiply(that.getNum())), + this.getDenom().multiply(that.getDenom())); } public RatLitExpr sub(final RatLitExpr that) { - return RatLitExpr.of(this.getNum() * that.getDenom() - this.getDenom() * that.getNum(), - this.getDenom() * that.getDenom()); + return RatLitExpr.of(this.getNum().multiply(that.getDenom()).subtract(this.getDenom().multiply(that.getNum())), + this.getDenom().multiply(that.getDenom())); } public RatLitExpr neg() { - return RatLitExpr.of(-this.getNum(), this.getDenom()); + return RatLitExpr.of(this.getNum().negate(), this.getDenom()); } public RatLitExpr mul(final RatLitExpr that) { - return RatLitExpr.of(this.getNum() * that.getNum(), this.getDenom() * that.getDenom()); + return RatLitExpr.of(this.getNum().multiply(that.getNum()), this.getDenom().multiply(that.getDenom())); } public RatLitExpr div(final RatLitExpr that) { - return RatLitExpr.of(this.getNum() * that.getDenom(), this.getDenom() * that.getNum()); + return RatLitExpr.of(this.getNum().multiply(that.getDenom()), this.getDenom().multiply(that.getNum())); } public BoolLitExpr eq(final RatLitExpr that) { - return Bool(this.getNum() == that.getNum() && this.getDenom() == that.getDenom()); + return Bool(this.getNum().compareTo(that.getNum()) == 0 && this.getDenom().compareTo(that.getDenom()) == 0); } public BoolLitExpr neq(final RatLitExpr that) { - return Bool(this.getNum() != that.getNum() || this.getDenom() != that.getDenom()); + return Bool(this.getNum().compareTo(that.getNum()) != 0 || this.getDenom().compareTo(that.getDenom()) != 0); } public BoolLitExpr lt(final RatLitExpr that) { - return Bool(this.getNum() * that.getDenom() < this.getDenom() * that.getNum()); + return Bool(this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum())) < 0); } public BoolLitExpr leq(final RatLitExpr that) { - return Bool(this.getNum() * that.getDenom() <= this.getDenom() * that.getNum()); + return Bool(this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum())) <= 0); } public BoolLitExpr gt(final RatLitExpr that) { - return Bool(this.getNum() * that.getDenom() > this.getDenom() * that.getNum()); + return Bool(this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum())) > 0); } public BoolLitExpr geq(final RatLitExpr that) { - return Bool(this.getNum() * that.getDenom() >= this.getDenom() * that.getNum()); + return Bool(this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum())) >= 0); } public RatLitExpr abs() { - return RatLitExpr.of(Math.abs(num), denom); + return RatLitExpr.of(num.abs(), denom); } public RatLitExpr frac() { @@ -149,8 +161,8 @@ public int hashCode() { int result = hashCode; if (result == 0) { result = HASH_SEED; - result = 31 * result + num; - result = 31 * result + denom; + result = 31 * result + num.hashCode(); + result = 31 * result + denom.hashCode(); hashCode = result; } return hashCode; @@ -162,7 +174,7 @@ public boolean equals(final Object obj) { return true; } else if (obj instanceof RatLitExpr) { final RatLitExpr that = (RatLitExpr) obj; - return (this.getNum() == that.getNum() && this.getDenom() == that.getDenom()); + return (this.getNum().compareTo(that.getNum()) == 0 && this.getDenom().compareTo(that.getDenom()) == 0); } else { return false; } @@ -179,7 +191,7 @@ public String toString() { @Override public int compareTo(final RatLitExpr that) { - return Integer.compare(this.getNum() * that.getDenom(), this.getDenom() * that.getNum()); + return this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum())); } } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatMulExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatMulExpr.java index 3daab0381c..0cce611977 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatMulExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatMulExpr.java @@ -19,6 +19,7 @@ import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; +import java.math.BigInteger; import java.util.List; import hu.bme.mit.theta.core.model.Valuation; @@ -49,12 +50,12 @@ public RatType getType() { @Override public RatLitExpr eval(final Valuation val) { - int prodNum = 1; - int prodDenom = 1; + var prodNum = BigInteger.ONE; + var prodDenom = BigInteger.ONE; for (final Expr op : getOps()) { final RatLitExpr opLit = (RatLitExpr) op.eval(val); - prodNum *= opLit.getNum(); - prodDenom *= opLit.getDenom(); + prodNum = prodNum.multiply(opLit.getNum()); + prodDenom = prodDenom.multiply(opLit.getDenom()); } return Rat(prodNum, prodDenom); } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java index 1753c0bd4b..ab849100c2 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java @@ -461,15 +461,15 @@ private static Expr simplifyRatAdd(final RatAddExpr expr, final Valuati ops.add(opVisited); } } - int num = 0; - int denom = 1; + var num = BigInteger.ZERO; + var denom = BigInteger.ONE; for (final Iterator> iterator = ops.iterator(); iterator.hasNext(); ) { final Expr op = iterator.next(); if (op instanceof RatLitExpr) { final RatLitExpr litOp = (RatLitExpr) op; - num = num * litOp.getDenom() + denom * litOp.getNum(); - denom *= litOp.getDenom(); + num = num.multiply(litOp.getDenom()).add(denom.multiply(litOp.getNum())); + denom = denom.multiply(litOp.getDenom()); iterator.remove(); } } @@ -534,17 +534,17 @@ private static Expr simplifyRatMul(final RatMulExpr expr, final Valuati ops.add(opVisited); } } - int num = 1; - int denom = 1; + var num = BigInteger.ONE; + var denom = BigInteger.ONE; for (final Iterator> iterator = ops.iterator(); iterator.hasNext(); ) { final Expr op = iterator.next(); if (op instanceof RatLitExpr) { final RatLitExpr litOp = (RatLitExpr) op; - num *= litOp.getNum(); - denom *= litOp.getDenom(); + num = num.multiply(litOp.getNum()); + denom = denom.multiply(litOp.getDenom()); iterator.remove(); - if (num == 0) { + if (num.compareTo(BigInteger.ZERO) == 0) { return Rat(0, 1); } } diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/expr/RatLitExprTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/expr/RatLitExprTest.java index e4a2b1d1f9..741f6f6af3 100644 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/expr/RatLitExprTest.java +++ b/subprojects/core/src/test/java/hu/bme/mit/theta/core/expr/RatLitExprTest.java @@ -18,6 +18,7 @@ import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; import static org.junit.Assert.assertEquals; +import java.math.BigInteger; import java.util.Arrays; import java.util.Collection; @@ -89,17 +90,17 @@ public static Collection data() { @Test public void testFloor() { // Act - final long actualFloor = number.floor(); + final var actualFloor = number.floor(); // Assert - assertEquals(expectedfloor, actualFloor); + assertEquals(BigInteger.valueOf(expectedfloor), actualFloor); } @Test public void testCeil() { // Act - final long actualCeil = number.ceil(); + final var actualCeil = number.ceil(); // Assert - assertEquals(expectedCeil, actualCeil); + assertEquals(BigInteger.valueOf(expectedCeil), actualCeil); } @Test From 1a70c5d6f17c9c49c2eb3047efac6d482046bf0a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:46:01 +0200 Subject: [PATCH 06/13] Change underlying type of RatLitExpr to BigInteger in analysis --- .../hu/bme/mit/theta/analysis/zone/ZoneState.java | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java index 6be5d737ed..910306f5de 100644 --- a/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java +++ b/subprojects/analysis/src/main/java/hu/bme/mit/theta/analysis/zone/ZoneState.java @@ -22,6 +22,7 @@ import static hu.bme.mit.theta.core.type.booltype.SmartBoolExprs.And; import static java.util.stream.Collectors.toList; +import java.math.BigInteger; import java.util.Collection; import java.util.Collections; import java.util.Map; @@ -71,11 +72,11 @@ public static ZoneState region(final Valuation valuation, final Collection y : constrainedVars) { @@ -88,9 +89,9 @@ public static ZoneState region(final Valuation valuation, final Collection Date: Wed, 26 Aug 2020 22:53:28 +0200 Subject: [PATCH 07/13] Change underlying type of RatLitExpr to BigInteger in solver --- .../java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java | 4 +++- .../java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java | 5 +++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index 5ec6b0e19a..f13d514d43 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -375,7 +375,9 @@ private com.microsoft.z3.FuncDecl transformParamDecl(final ParamDecl paramDec */ private com.microsoft.z3.Expr transformRatLit(final RatLitExpr expr) { - return context.mkReal(Math.toIntExact(expr.getNum()), Math.toIntExact(expr.getDenom())); + var num = context.mkReal(expr.getNum().toString()); + var denom = context.mkReal(expr.getDenom().toString()); + return context.mkDiv(num, denom); } private com.microsoft.z3.Expr transformRatAdd(final RatAddExpr expr) { diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java index ee2a9fdf53..2510f40b13 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java @@ -43,6 +43,7 @@ import com.microsoft.z3.FuncDecl; import com.microsoft.z3.Model; +import com.microsoft.z3.Native; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; @@ -184,8 +185,8 @@ private Expr transformIntLit(final com.microsoft.z3.Expr term) { private Expr transformRatLit(final com.microsoft.z3.Expr term) { final com.microsoft.z3.RatNum ratNum = (com.microsoft.z3.RatNum) term; - final int num = ratNum.getNumerator().getInt(); - final int denom = ratNum.getDenominator().getInt(); + final var num = ratNum.getNumerator().getBigInteger(); + final var denom = ratNum.getDenominator().getBigInteger(); return Rat(num, denom); } From 8699afd6530de4adb02f8dc9cfed737ec60ec3a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:54:34 +0200 Subject: [PATCH 08/13] Change underlying type of RatLitExpr to BigInteger in cfa --- .../src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index 51ca2d693e..aef054649c 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -632,8 +632,8 @@ public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { @Override public RatLitExpr visitRatLitExpr(final RatLitExprContext ctx) { - final int num = Integer.parseInt(ctx.num.getText()); - final int denom = Integer.parseInt(ctx.denom.getText()); + final var num = new BigInteger(ctx.num.getText()); + final var denom = new BigInteger(ctx.denom.getText()); return Rat(num, denom); } From 99ab77892b0c2571a0be7f246b492fc2bbc8175c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:55:39 +0200 Subject: [PATCH 09/13] Change underlying type of RatLitExpr to BigInteger in sts --- .../java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java index 5f96203fce..f6ab330069 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java +++ b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java @@ -526,8 +526,8 @@ public IntLitExpr visitIntLitExpr(final IntLitExprContext ctx) { @Override public RatLitExpr visitRatLitExpr(final RatLitExprContext ctx) { - final int num = Integer.parseInt(ctx.num.getText()); - final int denom = Integer.parseInt(ctx.denom.getText()); + final var num = new BigInteger(ctx.num.getText()); + final var denom = new BigInteger(ctx.denom.getText()); return Rat(num, denom); } From 0db51e6c4b3baa1132e2e768019103911a6b6981 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Wed, 26 Aug 2020 22:58:33 +0200 Subject: [PATCH 10/13] Cleanup code --- .../main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java | 1 - 1 file changed, 1 deletion(-) diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java index dc7f70e251..c212636d45 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java @@ -30,7 +30,6 @@ public static RatType Rat() { return RatType.getInstance(); } - @Deprecated public static RatLitExpr Rat(final int num, final int denom) { return RatLitExpr.of(num, denom); } From ad2a16c27ca4d2dd7c3d5c1720ec45c0ca3050b7 Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Thu, 27 Aug 2020 09:49:42 +0200 Subject: [PATCH 11/13] Remove unused import --- .../main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java | 1 - 1 file changed, 1 deletion(-) diff --git a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java index 2510f40b13..316131c63a 100644 --- a/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java +++ b/subprojects/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java @@ -43,7 +43,6 @@ import com.microsoft.z3.FuncDecl; import com.microsoft.z3.Model; -import com.microsoft.z3.Native; import hu.bme.mit.theta.common.TernaryOperator; import hu.bme.mit.theta.common.TriFunction; import hu.bme.mit.theta.common.Tuple2; From b05cd37010adeb3146726dba64df21bafde75a10 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mih=C3=A1ly=20Dobos-Kov=C3=A1cs?= Date: Thu, 27 Aug 2020 10:15:00 +0200 Subject: [PATCH 12/13] Add overloads to Int and Rat that take a String as parameter. --- .../mit/theta/core/type/inttype/IntExprs.java | 6 ++- .../theta/core/type/inttype/IntLitExpr.java | 4 -- .../mit/theta/core/type/rattype/RatExprs.java | 28 ++++++++++-- .../theta/core/type/rattype/RatLitExpr.java | 14 +----- .../theta/core/utils/ExprSimplifierTest.java | 43 +++++++++---------- 5 files changed, 51 insertions(+), 44 deletions(-) diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java index ac6b8b5d96..2fb6a15277 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntExprs.java @@ -31,7 +31,11 @@ public static IntType Int() { } public static IntLitExpr Int(final int value) { - return IntLitExpr.of(value); + return IntLitExpr.of(BigInteger.valueOf(value)); + } + + public static IntLitExpr Int(final String value) { + return IntLitExpr.of(new BigInteger(value)); } public static IntLitExpr Int(final BigInteger value) { diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java index 611fae83da..ad72f35023 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java @@ -44,10 +44,6 @@ public static IntLitExpr of(final BigInteger value) { return new IntLitExpr(value); } - public static IntLitExpr of(final int value) { - return new IntLitExpr(BigInteger.valueOf(value)); - } - public BigInteger getValue() { return value; } diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java index c212636d45..5b4f3a9ac8 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java @@ -31,15 +31,35 @@ public static RatType Rat() { } public static RatLitExpr Rat(final int num, final int denom) { - return RatLitExpr.of(num, denom); + return RatLitExpr.of(BigInteger.valueOf(num), BigInteger.valueOf(denom)); } - public static RatLitExpr Rat(final BigInteger num, final int denom) { - return RatLitExpr.of(num, denom); + public static RatLitExpr Rat(final int num, final String denom) { + return RatLitExpr.of(BigInteger.valueOf(num), new BigInteger(denom)); } public static RatLitExpr Rat(final int num, final BigInteger denom) { - return RatLitExpr.of(num, denom); + return RatLitExpr.of(BigInteger.valueOf(num), denom); + } + + public static RatLitExpr Rat(final String num, final int denom) { + return RatLitExpr.of(new BigInteger(num), BigInteger.valueOf(denom)); + } + + public static RatLitExpr Rat(final String num, final String denom) { + return RatLitExpr.of(new BigInteger(num), new BigInteger(denom)); + } + + public static RatLitExpr Rat(final String num, final BigInteger denom) { + return RatLitExpr.of(new BigInteger(num), denom); + } + + public static RatLitExpr Rat(final BigInteger num, final int denom) { + return RatLitExpr.of(num, BigInteger.valueOf(denom)); + } + + public static RatLitExpr Rat(final BigInteger num, final String denom) { + return RatLitExpr.of(num, new BigInteger(denom)); } public static RatLitExpr Rat(final BigInteger num, final BigInteger denom) { diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java index bc6c4c39d1..aec86427b6 100644 --- a/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java @@ -52,18 +52,6 @@ public static RatLitExpr of(final BigInteger num, final BigInteger denom) { return new RatLitExpr(num, denom); } - public static RatLitExpr of(final BigInteger num, final int denom) { - return new RatLitExpr(num, BigInteger.valueOf(denom)); - } - - public static RatLitExpr of(final int num, final BigInteger denom) { - return new RatLitExpr(BigInteger.valueOf(num), denom); - } - - public static RatLitExpr of(final int num, final int denom) { - return new RatLitExpr(BigInteger.valueOf(num), BigInteger.valueOf(denom)); - } - @Override public RatType getType() { return Rat(); @@ -153,7 +141,7 @@ public RatLitExpr abs() { } public RatLitExpr frac() { - return sub(of(floor(), 1)); + return sub(of(floor(), BigInteger.ONE)); } @Override diff --git a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java index 52a210ccfa..81f6496a72 100644 --- a/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java +++ b/subprojects/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java @@ -15,9 +15,28 @@ */ package hu.bme.mit.theta.core.utils; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvExprs; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.inttype.IntExprs; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.type.rattype.RatType; +import org.junit.Test; + +import java.util.ArrayList; +import java.util.List; + import static hu.bme.mit.theta.core.decl.Decls.Const; import static hu.bme.mit.theta.core.type.anytype.Exprs.Ite; -import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.*; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; @@ -59,26 +78,6 @@ import static org.junit.Assert.assertEquals; import static org.junit.Assert.assertTrue; -import hu.bme.mit.theta.core.type.bvtype.BvExprs; -import hu.bme.mit.theta.core.type.bvtype.BvType; -import hu.bme.mit.theta.core.type.inttype.IntExprs; -import hu.bme.mit.theta.common.Tuple2; -import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; -import org.junit.Test; - -import hu.bme.mit.theta.core.decl.ConstDecl; -import hu.bme.mit.theta.core.model.ImmutableValuation; -import hu.bme.mit.theta.core.model.Valuation; -import hu.bme.mit.theta.core.type.Expr; -import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.inttype.IntType; -import hu.bme.mit.theta.core.type.rattype.RatType; - -import java.math.BigInteger; -import java.util.List; - -import java.util.ArrayList; - public class ExprSimplifierTest { private final ConstDecl cx = Const("x", Bool()); @@ -270,7 +269,7 @@ public void testIntAdd() { assertEquals(Add(a, Int(4)), simplify(Add(Int(1), Add(a, Int(3))))); assertEquals(a, simplify(Add(Int(-3), a, Int(3)))); assertEquals(Add(a, b, a, b, c), simplify(Add(a, Add(b, Add(a, Add(b, c)))))); - assertEquals(Int(new BigInteger("4294967294")), simplify(Add(Int(Integer.MAX_VALUE), Int(Integer.MAX_VALUE)))); + assertEquals(Int("4294967294"), simplify(Add(Int(Integer.MAX_VALUE), Int(Integer.MAX_VALUE)))); } @Test From 91db1b9d296e093c21b039eeb5ae1ed0fc6a2155 Mon Sep 17 00:00:00 2001 From: Akos Hajdu Date: Thu, 27 Aug 2020 17:22:46 +0200 Subject: [PATCH 13/13] Bump version --- build.gradle.kts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index 28c7603c36..c35d700247 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -10,7 +10,7 @@ buildscript { allprojects { group = "hu.bme.mit.inf.theta" - version = "1.6.5" + version = "1.7.0" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) }