[feat] Propagate equalities into a SelectExpr

[feat] Split condition before to adding it to replacements
UnitTestBot · Jun 12, 2023 · d9e61ed · d9e61ed
1 parent 1388aa6
commit d9e61ed
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 7 deletions.
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
@@ -149,17 +149,22 @@ class ExprReplaceVisitor2 : public ExprVisitor {
                           : Action::changeTo(visit(sexpr.falseExpr));
     }
 
+    std::vector<ref<Expr>> splittedCond;
+    Expr::splitAnds(cond, splittedCond);
+
     ExprHashMap<ref<Expr>> localReplacements;
-    if (const EqExpr *ee = dyn_cast<EqExpr>(cond)) {
-      if (isa<ConstantExpr>(ee->left)) {
-        localReplacements.insert(std::make_pair(ee->right, ee->left));
+    for (auto scond : splittedCond) {
+      if (const EqExpr *ee = dyn_cast<EqExpr>(scond)) {
+        if (isa<ConstantExpr>(ee->left)) {
+          localReplacements.insert(std::make_pair(ee->right, ee->left));
+        } else {
+          localReplacements.insert(
+              std::make_pair(scond, ConstantExpr::alloc(1, Expr::Bool)));
+        }
       } else {
         localReplacements.insert(
-            std::make_pair(cond, ConstantExpr::alloc(1, Expr::Bool)));
+            std::make_pair(scond, ConstantExpr::alloc(1, Expr::Bool)));
       }
-    } else {
-      localReplacements.insert(
-          std::make_pair(cond, ConstantExpr::alloc(1, Expr::Bool)));
     }
 
     replacements.push_back(localReplacements);

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
@@ -2119,6 +2119,16 @@ static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
       return EqExpr::create(al->left, ar->left);
     }
     return EqExpr::alloc(l, r);
+  } else if (isa<SelectExpr>(l) || isa<SelectExpr>(r)) {
+    if (SelectExpr *se = dyn_cast<SelectExpr>(l)) {
+      return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, r),
+                                EqExpr::create(se->falseExpr, r));
+    }
+    if (SelectExpr *se = dyn_cast<SelectExpr>(r)) {
+      return SelectExpr::create(se->cond, EqExpr::create(se->trueExpr, l),
+                                EqExpr::create(se->falseExpr, l));
+    }
+    return EqExpr::alloc(l, r);
   } else {
     return EqExpr::alloc(l, r);
   }