Fix BV ITE rewrite (#3004)

The rewrite `BvIteConstChildren` assumes that `BvIteEqualChildren` has
been applied before it runs. However, with nested ITEs, it was possible
to violate that assertion. Given `bvite(c1, bvite(c2, 0, 0), bvite(c3,
0, 0))`, `BvIteEqualChildren` would rewrite that term to `bvite(c2, 0,
0)`. The `LinearRewriteStrategy` then ran `BvIteConstChildren` on
`bvite(c2, 0, 0)` which complained about the equal children. This commit
implements a simple fix that splits the `LinearRewriteStrategy` into two
strategies to make sure that if `BvIteEqualChildren` rewrites a node, we
drop back to the `Rewriter`. This ensures that the rewrites on the
rewritten node are invoked in the correct order.

2 files changed, 29 insertions, 3 deletions

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 0f7629c5f..6b160ea67 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -171,9 +171,20 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
   Node resultNode =
       LinearRewriteStrategy<RewriteRule<EvalITEBv>,
                             RewriteRule<BvIteConstCond>,
-                            RewriteRule<BvIteEqualChildren>,
-                            RewriteRule<BvIteConstChildren>,
-                            RewriteRule<BvIteEqualCond>>::apply(node);
+                            RewriteRule<BvIteEqualChildren>>::apply(node);
+  // If the node has been rewritten, we return here because we need to make
+  // sure that `BvIteEqualChildren` has been applied until we reach a fixpoint
+  // before applying `BvIteConstChildren`. Otherwise, `BvIteConstChildren`
+  // potentially performs an unsound rewrite. Returning hands back the control
+  // to the `Rewriter` which will then call this method again, ensuring that
+  // the rewrites are applied in the correct order.
+  if (resultNode != node)
+  {
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
+
+  resultNode = LinearRewriteStrategy<RewriteRule<BvIteConstChildren>,
+                                     RewriteRule<BvIteEqualCond>>::apply(node);
   if (resultNode != node)
   {
     return RewriteResponse(REWRITE_AGAIN, resultNode);
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index 1f4cc0c2c..bf0ca73b3 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -85,6 +85,21 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
     TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr));
   }
 
+  void testRewriteBvIte()
+  {
+    TypeNode boolType = d_nm->booleanType();
+    TypeNode bvType = d_nm->mkBitVectorType(1);
+
+    Node zero = d_nm->mkConst(BitVector(1, 0u));
+    Node c1 = d_nm->mkVar("c1", bvType);
+    Node c2 = d_nm->mkVar("c2", bvType);
+
+    Node ite = d_nm->mkNode(BITVECTOR_ITE, c2, zero, zero);
+    Node n = d_nm->mkNode(BITVECTOR_ITE, c1, ite, ite);
+    Node nr = Rewriter::rewrite(n);
+    TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr));
+  }
+
  private:
   ExprManager* d_em;
   SmtEngine* d_smt;