EnumEq simplification

RipplB · Feb 25, 2024 · eaf5b82 · eaf5b82
1 parent 2166105
commit eaf5b82
Showing 1 changed file with 30 additions and 0 deletions.
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
@@ -74,6 +74,9 @@
 import hu.bme.mit.theta.core.type.bvtype.BvURemExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvXorExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr;
+import hu.bme.mit.theta.core.type.enumtype.EnumEqExpr;
+import hu.bme.mit.theta.core.type.enumtype.EnumLitExpr;
+import hu.bme.mit.theta.core.type.enumtype.EnumType;
 import hu.bme.mit.theta.core.type.fptype.FpAbsExpr;
 import hu.bme.mit.theta.core.type.fptype.FpAddExpr;
 import hu.bme.mit.theta.core.type.fptype.FpAssignExpr;
@@ -240,6 +243,10 @@ public static ExprSimplifier create(final SimplifierLevel level) {
 
             .addCase(IntLtExpr.class, this::simplifyIntLt)
 
+            // Enum
+
+            .addCase(EnumEqExpr.class, this::simplifyEnumEqExpr)
+
             // Array
 
             .addCase(ArrayReadExpr.class, this::simplifyArrayRead)
@@ -1164,6 +1171,29 @@ private Expr<BoolType> simplifyIntLt(final IntLtExpr expr, final Valuation val)
         return expr.with(leftOp, rightOp);
     }
 
+    /*
+     * Enums
+     */
+
+    private Expr<BoolType> simplifyEnumEqExpr(final EnumEqExpr expr, final Valuation val) {
+        final Expr<EnumType> leftOp = simplify(expr.getLeftOp(), val);
+        final Expr<EnumType> rightOp = simplify(expr.getRightOp(), val);
+
+        if (leftOp instanceof EnumLitExpr && rightOp instanceof EnumLitExpr) {
+            final EnumLitExpr leftLit = (EnumLitExpr) leftOp;
+            final EnumLitExpr rightLit = (EnumLitExpr) rightOp;
+            return Bool(leftLit.equals(rightLit));
+        }
+
+        if (leftOp instanceof RefExpr && rightOp instanceof RefExpr) {
+            if (level != LITERAL_ONLY && leftOp.equals(rightOp)) {
+                return False();
+            }
+        }
+
+        return expr.with(leftOp, rightOp);
+    }
+
     /*
      * Bitvectors
      */