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")) } 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 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 a72c6dfbfb..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 @@ -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) { @@ -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); } @@ -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 a5778abad7..218978570b 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 @@ -71,6 +71,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; @@ -645,14 +646,14 @@ 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); } @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/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 898a8a55da..84d3ee6c5e 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 @@ -254,7 +254,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 4d89f649a7..3412a67ed0 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() { @@ -29,6 +31,14 @@ public static IntType Int() { } public static IntLitExpr Int(final int 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) { return IntLitExpr.of(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 85f31c4985..56ac69747c 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,17 @@ public final class IntLitExpr extends NullaryExpr implements LitExpr= 0; + assert result.compareTo(BigInteger.ZERO) >= 0; return IntLitExpr.of(result); } @@ -113,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 @@ -163,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; @@ -175,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; } @@ -183,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/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 982dc05bfe..3501208984 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() { @@ -29,6 +31,38 @@ public static RatType Rat() { } public static RatLitExpr Rat(final int num, final int denom) { + return RatLitExpr.of(BigInteger.valueOf(num), BigInteger.valueOf(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(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) { return RatLitExpr.of(num, 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 876cc21c73..3aa1034e77 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,40 +15,40 @@ */ 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); } @@ -62,42 +62,42 @@ 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 pos() { @@ -105,47 +105,47 @@ public RatLitExpr pos() { } 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() { - return sub(of(floor(), 1)); + return sub(of(floor(), BigInteger.ONE)); } @Override @@ -153,8 +153,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; @@ -166,7 +166,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; } @@ -183,7 +183,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 af337f2685..a0716deeb3 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; @@ -508,15 +509,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(); } } @@ -585,17 +586,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); } } @@ -773,24 +774,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); } @@ -810,7 +811,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); } } @@ -848,26 +849,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/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 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..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,25 +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.util.List; - -import java.util.ArrayList; - public class ExprSimplifierTest { private final ConstDecl cx = Const("x", Bool()); @@ -269,6 +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("4294967294"), simplify(Add(Int(Integer.MAX_VALUE), Int(Integer.MAX_VALUE)))); } @Test 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 c40ac5f95f..8e688160a1 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 @@ -422,7 +422,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) { @@ -501,7 +503,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 b6345e17da..dbe42760de 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 @@ -179,14 +179,14 @@ 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); } 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); } 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..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 @@ -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,14 +520,14 @@ 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); } @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/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); } 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; }