FpEq simplification fixed

ftsrg · Nov 14, 2023 · 9ed1975 · 9ed1975
1 parent b05edbe
commit 9ed1975
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 8 deletions.
diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java
@@ -251,9 +251,7 @@ public int hashCode() {
 
     @Override
     public boolean equals(final Object obj) {
-        if (this == obj) {
-            return true;
-        } else if (obj != null && this.getClass() == obj.getClass() && getType().equals(((FpLitExpr) obj).getType())) {
+        if (obj != null && this.getClass() == obj.getClass() && getType().equals(((FpLitExpr) obj).getType())) {
             return eq((FpLitExpr) obj).equals(BoolExprs.True());
         } else {
             return false;

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
@@ -145,7 +145,7 @@
 import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv;
 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.SimplifierLevel.*;
+import static hu.bme.mit.theta.core.utils.SimplifierLevel.LITERAL_ONLY;
 
 public final class ExprSimplifier {
 
@@ -2004,10 +2004,6 @@ private Expr<BoolType> simplifyFpEq(final FpEqExpr expr, final Valuation val) {
 
         if (leftOp instanceof FpLitExpr && rightOp instanceof FpLitExpr) {
             return Bool(leftOp.equals(rightOp));
-        } else if (leftOp instanceof RefExpr && rightOp instanceof RefExpr) {
-            if (level != LITERAL_ONLY && leftOp.equals(rightOp)) {
-                return True();
-            }
         }
 
         return expr.with(leftOp, rightOp);

diff --git a/...ion/grammar/preprocess/BitwiseOption.java → ...on/grammar/preprocess/MainArithmetic.java b/...ion/grammar/preprocess/BitwiseOption.java → ...on/grammar/preprocess/MainArithmetic.java