Merge pull request #364 from ftsrg/reachgsat

Handle RatExprs in MDDs

Author: mondokm

build.gradle.kts

@@ -29,7 +29,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.14.0"
+    version = "6.14.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/expressionnode/LitExprConverter.java

@@ -34,6 +34,8 @@
 import hu.bme.mit.theta.core.type.fptype.FpType;
 import hu.bme.mit.theta.core.type.inttype.IntLitExpr;
 import hu.bme.mit.theta.core.type.inttype.IntType;
+import hu.bme.mit.theta.core.type.rattype.RatLitExpr;
+import hu.bme.mit.theta.core.type.rattype.RatType;
 import hu.bme.mit.theta.core.utils.BvUtils;
 import java.math.BigInteger;
 
@@ -54,7 +56,9 @@ public static int toInt(LitExpr<?> litExpr) {
             var ret = BvUtils.neutralBvLitExprToBigInteger(bvLitExpr).intValue();
             return ret;
         }
-        if (litExpr instanceof ArrayLitExpr<?, ?> || litExpr instanceof FpLitExpr) {
+        if (litExpr instanceof ArrayLitExpr<?, ?>
+                || litExpr instanceof FpLitExpr
+                || litExpr instanceof RatLitExpr) {
             if (objToInt.get(litExpr) != null) {
                 return objToInt.get(litExpr);
             }
@@ -82,7 +86,7 @@ public static LitExpr<?> toLitExpr(int integer, Type type) {
             return BvUtils.bigIntegerToNeutralBvLitExpr(
                     BigInteger.valueOf(integer), ((BvType) type).getSize());
         }
-        if (type instanceof ArrayType<?, ?> || type instanceof FpType) {
+        if (type instanceof ArrayType<?, ?> || type instanceof FpType || type instanceof RatType) {
             return (LitExpr<?>) objToInt.inverse().get(integer);
         }
         if (type instanceof EnumType) {

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java

@@ -24,6 +24,7 @@
 import hu.bme.mit.theta.common.DispatchTable2;
 import hu.bme.mit.theta.common.Tuple2;
 import hu.bme.mit.theta.common.Utils;
+import hu.bme.mit.theta.common.container.Containers;
 import hu.bme.mit.theta.core.model.Valuation;
 import hu.bme.mit.theta.core.type.Expr;
 import hu.bme.mit.theta.core.type.LitExpr;
@@ -415,7 +416,7 @@ private Expr<BoolType> simplifyXor(final XorExpr expr, final Valuation val) {
     }
 
     private Expr<BoolType> simplifyAnd(final AndExpr expr, final Valuation val) {
-        final Set<Expr<BoolType>> ops = new HashSet<>();
+        final Set<Expr<BoolType>> ops = Containers.createSet();
 
         if (expr.getOps().isEmpty()) {
             return True();
@@ -445,7 +446,7 @@ private Expr<BoolType> simplifyAnd(final AndExpr expr, final Valuation val) {
     }
 
     private Expr<BoolType> simplifyOr(final OrExpr expr, final Valuation val) {
-        final Set<Expr<BoolType>> ops = new HashSet<>();
+        final Set<Expr<BoolType>> ops = Containers.createSet();
 
         if (expr.getOps().isEmpty()) {
             return True();