Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)

`TheoryBVRewriter::RewriteITEBv()` is currently always returning the
status `REWRITE_DONE`. This can result in a situation where a rewritten
node can be rewritten again (which breaks the contract of our rewriter).
The unit test in this commit illustrates the issue. The commit fixes the
issue by returning `REWRITE_AGAIN` or `REWRITE_AGAIN_FULL` if a node
changed. `REWRITE_AGAIN_FULL` is needed if the resulting node may have a
child that is not a subterm of the original expression.

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 8f9e6614c4d357176ae2483d59767ba6a6c00c17..0f7629c5f4e8c4cd8e2bf496962120fd1caa32e1 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -173,12 +173,19 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
                             RewriteRule<BvIteConstCond>,
                             RewriteRule<BvIteEqualChildren>,
                             RewriteRule<BvIteConstChildren>,
-                            RewriteRule<BvIteEqualCond>,
-                            RewriteRule<BvIteMergeThenIf>,
+                            RewriteRule<BvIteEqualCond>>::apply(node);
+  if (resultNode != node)
+  {
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
+
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<BvIteMergeThenIf>,
                             RewriteRule<BvIteMergeElseIf>,
                             RewriteRule<BvIteMergeThenElse>,
                             RewriteRule<BvIteMergeElseElse>>::apply(node);
-  return RewriteResponse(REWRITE_DONE, resultNode);
+  return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN_FULL,
+                         resultNode);
 }
 
 RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 3d29c4de181e77e1e70c49888c07cb6c3d20b9b0..963466b09cc3881e76ee490f5c802bff4046ea7c 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -2,6 +2,7 @@ cvc4_add_unit_test_black(theory_black theory)
 cvc4_add_unit_test_white(evaluator_white theory)
 cvc4_add_unit_test_white(logic_info_white theory)
 cvc4_add_unit_test_white(theory_arith_white theory)
+cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
 cvc4_add_unit_test_white(theory_bv_white theory)
 cvc4_add_unit_test_white(theory_engine_white theory)
 cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)

diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
new file mode 100644 (file)
index 0000000..1f4cc0c
--- /dev/null
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -0,0 +1,94 @@
+/*********************                                                        */
+/*! \file theory_bv_rewriter_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Unit tests for the bit-vector rewriter
+ **
+ ** Unit tests for the bit-vector rewriter.
+ **/
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
+#include "util/bitvector.h"
+
+#include <cxxtest/TestSuite.h>
+#include <iostream>
+#include <memory>
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+
+class TheoryBvRewriterWhite : public CxxTest::TestSuite
+{
+ public:
+  TheoryBvRewriterWhite() {}
+
+  void setUp() override
+  {
+    Options opts;
+    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+    d_em = new ExprManager(opts);
+    d_smt = new SmtEngine(d_em);
+    d_scope = new SmtScope(d_smt);
+
+    d_nm = NodeManager::currentNM();
+  }
+
+  void tearDown() override
+  {
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  Node boolToBv(Node b)
+  {
+    return d_nm->mkNode(ITE,
+                        b,
+                        d_nm->mkConst(BitVector(1, 1u)),
+                        d_nm->mkConst(BitVector(1, 0u)));
+  }
+
+  void testRewriteToFixpoint()
+  {
+    TypeNode boolType = d_nm->booleanType();
+    TypeNode bvType = d_nm->mkBitVectorType(1);
+
+    Node zero = d_nm->mkConst(BitVector(1, 0u));
+    Node b1 = d_nm->mkVar("b1", boolType);
+    Node b2 = d_nm->mkVar("b2", boolType);
+    Node b3 = d_nm->mkVar("b3", boolType);
+    Node bv = d_nm->mkVar("bv", bvType);
+
+    Node n = d_nm->mkNode(
+        BITVECTOR_ITE,
+        boolToBv(b1),
+        d_nm->mkNode(BITVECTOR_ITE,
+                     boolToBv(b2),
+                     d_nm->mkNode(BITVECTOR_ITE, boolToBv(b3), zero, bv),
+                     bv),
+        bv);
+    Node nr = Rewriter::rewrite(n);
+    TS_ASSERT_EQUALS(nr, Rewriter::rewrite(nr));
+  }
+
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  SmtScope* d_scope;
+
+  NodeManager* d_nm;
+};