Merge pull request #110 from ftsrg/rattoint

RatToIntExpr: rational to int type conversion expression
ftsrg · Apr 12, 2021 · 6d92707 · 6d92707
2 parents d1144bc + 5ad60b7
commit 6d92707
Show file tree

Hide file tree

Showing 10 changed files with 143 additions and 2 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "2.12.0"
+    version = "2.12.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatExprs.java
@@ -156,4 +156,7 @@ public static RatMulExpr Mul(final Expr<RatType> op1, final Expr<RatType> op2, f
 		return RatMulExpr.of(ImmutableList.of(op1, op2, op3, op4, op5));
 	}
 
+    public static RatToIntExpr ToInt(Expr<RatType> op) {
+		return RatToIntExpr.of(op);
+    }
 }
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatLitExpr.java
@@ -19,6 +19,7 @@
 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 hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 
 import java.math.BigInteger;
 
@@ -186,4 +187,7 @@ public int compareTo(final RatLitExpr that) {
 		return this.getNum().multiply(that.getDenom()).compareTo(this.getDenom().multiply(that.getNum()));
 	}
 
+    public IntLitExpr toInt() {
+		return IntLitExpr.of(num.divide(denom));
+    }
 }
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatToIntExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatToIntExpr.java
@@ -0,0 +1,88 @@
+/*
+ *  Copyright 2017 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.core.type.rattype;
+
+import hu.bme.mit.theta.core.model.Valuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.UnaryExpr;
+import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
+import hu.bme.mit.theta.core.type.inttype.IntType;
+
+import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
+import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
+import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
+
+public final class RatToIntExpr extends UnaryExpr<RatType, IntType> {
+
+	private static final int HASH_SEED = 4828;
+	private static final String OPERATOR_LABEL = "to_int";
+
+	private RatToIntExpr(final Expr<RatType> op) {
+		super(op);
+	}
+
+	public static RatToIntExpr of(final Expr<RatType> op) {
+		return new RatToIntExpr(op);
+	}
+
+	public static RatToIntExpr create(final Expr<?> op) {
+		final Expr<RatType> newOp = cast(op, Rat());
+		return RatToIntExpr.of(newOp);
+	}
+
+	@Override
+	public IntType getType() {
+		return Int();
+	}
+
+	@Override
+	public IntLitExpr eval(final Valuation val) {
+		final RatLitExpr opVal = (RatLitExpr) getOp().eval(val);
+		return opVal.toInt();
+	}
+
+	@Override
+	public RatToIntExpr with(final Expr<RatType> op) {
+		if (op == getOp()) {
+			return this;
+		} else {
+			return RatToIntExpr.of(op);
+		}
+	}
+
+	@Override
+	public boolean equals(final Object obj) {
+		if (this == obj) {
+			return true;
+		} else if (obj instanceof RatToIntExpr) {
+			final RatToIntExpr that = (RatToIntExpr) obj;
+			return this.getOp().equals(that.getOp());
+		} else {
+			return false;
+		}
+	}
+
+	@Override
+	protected int getHashSeed() {
+		return HASH_SEED;
+	}
+
+	@Override
+	public String getOperatorLabel() {
+		return OPERATOR_LABEL;
+	}
+
+}
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/rattype/RatType.java
@@ -22,7 +22,7 @@
 import hu.bme.mit.theta.core.type.abstracttype.Ordered;
 
 public final class RatType
-		implements Additive<RatType>, Multiplicative<RatType>, Equational<RatType>, Ordered<RatType> {
+		implements Additive<RatType>, Multiplicative<RatType>, Equational<RatType>, Ordered<RatType>{
 
 	private static final RatType INSTANCE = new RatType();
 	private static final int HASH_SEED = 385863;

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java
@@ -114,6 +114,7 @@
 import hu.bme.mit.theta.core.type.rattype.RatNeqExpr;
 import hu.bme.mit.theta.core.type.rattype.RatPosExpr;
 import hu.bme.mit.theta.core.type.rattype.RatSubExpr;
+import hu.bme.mit.theta.core.type.rattype.RatToIntExpr;
 import hu.bme.mit.theta.core.type.rattype.RatType;
 
 public final class ExprSimplifier {
@@ -160,6 +161,8 @@ public final class ExprSimplifier {
 
 			.addCase(RatLtExpr.class, ExprSimplifier::simplifyRatLt)
 
+			.addCase(RatToIntExpr.class, ExprSimplifier::simplifyRatToInt)
+
 			// Integer
 
 			.addCase(IntToRatExpr.class, ExprSimplifier::simplifyIntToRat)
@@ -760,6 +763,17 @@ private static Expr<BoolType> simplifyRatLt(final RatLtExpr expr, final Valuatio
 		return expr.with(leftOp, rightOp);
 	}
 
+	private static Expr<IntType> simplifyRatToInt(final RatToIntExpr expr, final Valuation val) {
+		final Expr<RatType> op = simplify(expr.getOp(), val);
+
+		if (op instanceof RatLitExpr) {
+			final RatLitExpr litOp = (RatLitExpr) op;
+			return litOp.toInt();
+		}
+
+		return expr.with(op);
+	}
+
 	/*
 	 * Integers
 	 */

diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java
@@ -53,6 +53,7 @@
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Neq;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub;
+import static hu.bme.mit.theta.core.type.rattype.RatExprs.ToInt;
 import static org.junit.Assert.assertEquals;
 
 import hu.bme.mit.theta.common.Tuple2;
@@ -255,6 +256,16 @@ public void testRem() {
 		assertEquals(Int(0), evaluate(Rem(Int(3), Int(3))));
 	}
 
+	@Test
+	public void testRatToInt() {
+		assertEquals(Int(1), evaluate(ToInt(Rat(4, 3))));
+		assertEquals(Int(1), evaluate(ToInt(Rat(3, 3))));
+		assertEquals(Int(0), evaluate(ToInt(Rat(2, 3))));
+		assertEquals(Int(-1), evaluate(ToInt(Rat(-4, 3))));
+		assertEquals(Int(-1), evaluate(ToInt(Rat(4, -3))));
+		assertEquals(Int(1), evaluate(ToInt(Rat(-4, -3))));
+	}
+
 	// rattype
 
 	@Test

diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/utils/ExprSimplifierTest.java
@@ -73,6 +73,7 @@
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Neq;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat;
 import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub;
+import static hu.bme.mit.theta.core.type.rattype.RatExprs.ToInt;
 import static hu.bme.mit.theta.core.utils.ExprUtils.simplify;
 import static org.junit.Assert.assertEquals;
 import static org.junit.Assert.assertTrue;
@@ -353,6 +354,16 @@ public void testIntLt() {
 		assertEquals(False(), simplify(Lt(a, a)));
 	}
 
+	@Test
+	public void testRatToInt() {
+		assertEquals(Int(1), simplify(ToInt(Rat(4, 3))));
+		assertEquals(Int(1), simplify(ToInt(Rat(3, 3))));
+		assertEquals(Int(0), simplify(ToInt(Rat(2, 3))));
+		assertEquals(Int(-1), simplify(ToInt(Rat(-4, 3))));
+		assertEquals(Int(-1), simplify(ToInt(Rat(4, -3))));
+		assertEquals(Int(1), simplify(ToInt(Rat(-4, -3))));
+	}
+
 	// Bitvectors
 
 	@Test

diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java
@@ -112,6 +112,7 @@
 import hu.bme.mit.theta.core.type.rattype.RatNeqExpr;
 import hu.bme.mit.theta.core.type.rattype.RatPosExpr;
 import hu.bme.mit.theta.core.type.rattype.RatSubExpr;
+import hu.bme.mit.theta.core.type.rattype.RatToIntExpr;
 import hu.bme.mit.theta.core.utils.BvUtils;
 
 import java.util.List;
@@ -194,6 +195,8 @@ public Z3ExprTransformer(final Z3TransformationManager transformer, final Contex
 
 				.addCase(RatLtExpr.class, this::transformRatLt)
 
+				.addCase(RatToIntExpr.class, this::transformRatToInt)
+
 				// Integers
 
 				.addCase(IntLitExpr.class, this::transformIntLit)
@@ -522,6 +525,11 @@ private com.microsoft.z3.Expr transformRatLt(final RatLtExpr expr) {
 		return context.mkLt(leftOpTerm, rightOpTerm);
 	}
 
+	private com.microsoft.z3.Expr transformRatToInt(final RatToIntExpr expr) {
+		final com.microsoft.z3.RealExpr opTerm = (com.microsoft.z3.RealExpr) toTerm(expr.getOp());
+		return context.mkReal2Int(opTerm);
+	}
+
 	/*
 	 * Integers
 	 */

diff --git a/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java b/subprojects/common/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3TermTransformer.java
@@ -77,6 +77,7 @@
 import hu.bme.mit.theta.core.type.inttype.IntToRatExpr;
 import hu.bme.mit.theta.core.type.inttype.IntModExpr;
 import hu.bme.mit.theta.core.type.rattype.RatDivExpr;
+import hu.bme.mit.theta.core.type.rattype.RatToIntExpr;
 import hu.bme.mit.theta.core.utils.BvUtils;
 import hu.bme.mit.theta.core.utils.TypeUtils;
 import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array;
@@ -111,6 +112,7 @@ public Z3TermTransformer(final Z3SymbolTable symbolTable) {
 		environment.put("select", exprBinaryOperator(ArrayReadExpr::create));
 		environment.put("store", exprTernaryOperator(ArrayWriteExpr::create));
 		environment.put("to_real", exprUnaryOperator(IntToRatExpr::create));
+		environment.put("to_int", exprUnaryOperator(RatToIntExpr::create));
 		environment.put("mod", exprBinaryOperator(IntModExpr::create));
 	}