From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 9 Jun 2021 19:53:31 +0000 (-0700)
Subject: Reorder ITE rewrites (#6723)
X-Git-Tag: cvc5-1.0.0~1615
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=10e9d697e5ac14f921215b2847bd9bc9c035215e;p=cvc5.git

Reorder ITE rewrites (#6723)

Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
---

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index a5c63522d..8f6d9d3b7 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -345,16 +345,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
             << n << ": " << n[0].notNode() << std::endl;
         return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
       }
-      if (n[1] == tt || n[1] == ff)
-      {
-        // ITE C true y --> C v y
-        // ITE C false y --> ~C ^ y
-        Node resp =
-            n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]);
-        Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const "
-                          << n << ": " << resp << std::endl;
-        return RewriteResponse(REWRITE_AGAIN, resp);
-      }
     }
 
     if (n[0].getKind() == kind::NOT)
@@ -364,17 +354,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
           REWRITE_AGAIN, nodeManager->mkNode(kind::ITE, n[0][0], n[2], n[1]));
     }
 
-    if (n[2].isConst() && (n[2] == tt || n[2] == ff))
-    {
-      // ITE C x true --> ~C v x
-      // ITE C x false --> C ^ x
-      Node resp =
-          n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]);
-      Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const "
-                        << n << ": " << resp << std::endl;
-      return RewriteResponse(REWRITE_AGAIN, resp);
-    }
-
     int parityTmp;
     if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
       Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
@@ -424,6 +403,32 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
           << parityTmp << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);
     }
+
+    // Rewrites for ITEs with a constant branch. These rewrites are applied
+    // after the parity rewrites above because they may simplify ITEs such as
+    // `(ite c c true)` to `(ite c true true)`. As a result, we avoid
+    // introducing an unnecessary conjunction/disjunction here.
+    if (n[1].isConst() && (n[1] == tt || n[1] == ff))
+    {
+      // ITE C true y --> C v y
+      // ITE C false y --> ~C ^ y
+      Node resp =
+          n[1] == tt ? n[0].orNode(n[2]) : (n[0].negate()).andNode(n[2]);
+      Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[1] const "
+                        << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    }
+    else if (n[2].isConst() && (n[2] == tt || n[2] == ff))
+    {
+      // ITE C x true --> ~C v x
+      // ITE C x false --> C ^ x
+      Node resp =
+          n[2] == tt ? (n[0].negate()).orNode(n[1]) : n[0].andNode(n[1]);
+      Debug("bool-ite") << "TheoryBoolRewriter::preRewrite_ITE: n[2] const "
+                        << n << ": " << resp << std::endl;
+      return RewriteResponse(REWRITE_AGAIN, resp);
+    }
+
     break;
   }
   default:
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4ee8e513e..19c689b87 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -163,6 +163,7 @@ set(regress_0_tests
   regress0/auflia/fuzz05.smtv1.smt2
   regress0/auflia/x2.smtv1.smt2
   regress0/bool/issue1978.smt2
+  regress0/bool/issue6717-ite-rewrite.smt2
   regress0/boolean-prec.cvc
   regress0/boolean-terms-bug-array.smt2
   regress0/boolean-terms-kernel1.smt2
diff --git a/test/regress/regress0/bool/issue6717-ite-rewrite.smt2 b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2
new file mode 100644
index 000000000..3f78823df
--- /dev/null
+++ b/test/regress/regress0/bool/issue6717-ite-rewrite.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(declare-fun T () Bool)
+(declare-fun v () String)
+(assert (ite T T true))
+(assert (or T (and (str.prefixof v "") (exists ((x Int)) (= "t" (str.substr v 0 x))))))
+(set-info :status sat)
+(check-sat)