Merge pull request #69 from ftsrg/bigint

Replace int as underlying type in IntLitExpr and RatLitExpr
ftsrg · Aug 27, 2020 · e39f3ad · e39f3ad
2 parents ea7be30 + 91db1b9
commit e39f3ad
Show file tree

Hide file tree

Showing 24 changed files with 235 additions and 177 deletions.
diff --git 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
@@ -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<VarDe
 			final RatLitExpr sx = (RatLitExpr) valuation.eval(x).get();
 			final RatLitExpr fx = sx.frac();
 
-			if (fx.getNum() == 0) {
-				dbm.and(Eq(x, sx.getNum()));
+			if (fx.getNum().compareTo(BigInteger.ZERO) == 0) {
+				dbm.and(Eq(x, sx.getNum().intValue()));
 			} else {
-				dbm.and(Lt(x, sx.ceil()));
-				dbm.and(Gt(x, sx.floor()));
+				dbm.and(Lt(x, sx.ceil().intValue()));
+				dbm.and(Gt(x, sx.floor().intValue()));
 			}
 
 			for (final VarDecl<RatType> y : constrainedVars) {
@@ -88,9 +89,9 @@ public static ZoneState region(final Valuation valuation, final Collection<VarDe
 
 				final int compareResult = fx.compareTo(fy);
 				if (compareResult == 0) {
-					dbm.and(Eq(x, y, sx.floor() - sy.floor()));
+					dbm.and(Eq(x, y, sx.floor().intValue() - sy.floor().intValue()));
 				} else if (compareResult < 0) {
-					dbm.and(Lt(x, y, sx.floor() - sy.floor()));
+					dbm.and(Lt(x, y, sx.floor().intValue() - sy.floor().intValue()));
 				}
 			}
 		}

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
@@ -634,14 +634,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/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<?, BoolType> 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
@@ -102,7 +102,7 @@ public <DeclType extends Type> ClockOp visit(final AssignStmt<DeclType> 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,16 +123,16 @@ public <DeclType extends Type> ClockOp visit(final AssignStmt<DeclType> 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);
 							}
 						}
 					} 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
@@ -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
@@ -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
@@ -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
@@ -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<IntType> 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
@@ -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
@@ -34,17 +34,17 @@ public final class IntLitExpr extends NullaryExpr<IntType> implements LitExpr<In
 	private static final int HASH_SEED = 4111;
 	private volatile int hashCode = 0;
 
-	private final int value;
+	private final BigInteger value;
 
-	private IntLitExpr(final int value) {
+	private IntLitExpr(final BigInteger value) {
 		this.value = value;
 	}
 
-	public static IntLitExpr of(final int value) {
+	public static IntLitExpr of(final BigInteger value) {
 		return new IntLitExpr(value);
 	}
 
-	public int getValue() {
+	public BigInteger getValue() {
 		return value;
 	}
 
@@ -63,7 +63,7 @@ public RatLitExpr toRat() {
 	}
 
 	public BvLitExpr toBv(int size, boolean isSigned) {
-		BigInteger res = BigInteger.valueOf(value);
+		BigInteger res = value;
 		BigInteger fittedRes = BvUtils.fitBigIntegerIntoDomain(res, size, isSigned);
 
 		if(res.equals(fittedRes)) {
@@ -74,23 +74,23 @@ public BvLitExpr toBv(int size, boolean isSigned) {
 	}
 
 	public IntLitExpr add(final IntLitExpr that) {
-		return IntLitExpr.of(this.value + that.value);
+		return IntLitExpr.of(this.value.add(that.value));
 	}
 
 	public IntLitExpr sub(final IntLitExpr that) {
-		return IntLitExpr.of(this.value - that.value);
+		return IntLitExpr.of(this.value.subtract(that.value));
 	}
 
 	public IntLitExpr neg() {
-		return IntLitExpr.of(-this.value);
+		return IntLitExpr.of(this.value.negate());
 	}
 
 	public IntLitExpr pos() {
 		return IntLitExpr.of(this.value);
 	}
 
 	public IntLitExpr div(final IntLitExpr that) {
-		return IntLitExpr.of(this.value / that.value);
+		return IntLitExpr.of(this.value.divide(that.value));
 	}
 
 	public IntLitExpr mod(final IntLitExpr that) {
@@ -99,11 +99,11 @@ public IntLitExpr mod(final IntLitExpr that) {
 		// 5 mod -3 = 2
 		// -5 mod 3 = 1
 		// -5 mod -3 = 1
-		int result = this.value % that.value;
-		if (result < 0) {
-			result += Math.abs(that.value);
+		var result = this.value.mod(that.value.abs());
+		if (result.compareTo(BigInteger.ZERO) < 0) {
+			result = result.add(that.value.abs());
 		}
-		assert result >= 0;
+		assert result.compareTo(BigInteger.ZERO) >= 0;
 		return IntLitExpr.of(result);
 	}
 
@@ -113,57 +113,57 @@ 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
 	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,20 +175,20 @@ 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;
 		}
 	}
 
 	@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
@@ -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<IntType> op : getOps()) {
 			final IntLitExpr opVal = (IntLitExpr) op.eval(val);
-			prod *= opVal.getValue();
+			prod = prod.multiply(opVal.getValue());
 		}
 		return Int(prod);
 	}