Avoid PLUS with one child for bv2nat elimination (#3639)

6 files changed, 39 insertions, 29 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index afd99647b..48168d7d6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -618,21 +618,7 @@ int TheoryBV::getReduction(int effort, Node n, Node& nr)
   NodeManager* const nm = NodeManager::currentNM();
   if (n.getKind() == kind::BITVECTOR_TO_NAT)
   {
-    // taken from rewrite code
-    const unsigned size = utils::getSize(n[0]);
-    const Node z = nm->mkConst(Rational(0));
-    const Node bvone = utils::mkOne(1);
-    NodeBuilder<> result(kind::PLUS);
-    Integer i = 1;
-    for (unsigned bit = 0; bit < size; ++bit, i *= 2)
-    {
-      Node cond =
-          nm->mkNode(kind::EQUAL,
-                     nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]),
-                     bvone);
-      result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
-    }
-    nr = Node(result);
+    nr = utils::eliminateBv2Nat(n);
     return -1;
   }
   else if (n.getKind() == kind::INT_TO_BITVECTOR)
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 0ae082adc..c9f814be6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -275,20 +275,7 @@ inline Node RewriteRule<BVToNatEliminate>::apply(TNode node)
   //if( node[0].isConst() ){
     //TODO? direct computation instead of term construction+rewriting
   //}
-
-  const unsigned size = utils::getSize(node[0]);
-  NodeManager* const nm = NodeManager::currentNM();
-  const Node z = nm->mkConst(Rational(0));
-  const Node bvone = utils::mkOne(1);
-
-  NodeBuilder<> result(kind::PLUS);
-  Integer i = 1;
-  for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
-    Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]), bvone);
-    result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
-  }
-
-  return Node(result);
+  return utils::eliminateBv2Nat(node);
 }
 
 template <>
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 765541150..2094e804f 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -459,6 +459,28 @@ Node flattenAnd(std::vector<TNode>& queue)
 
 /* ------------------------------------------------------------------------- */
 
+Node eliminateBv2Nat(TNode node)
+{
+  const unsigned size = utils::getSize(node[0]);
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node z = nm->mkConst(Rational(0));
+  const Node bvone = utils::mkOne(1);
+
+  Integer i = 1;
+  std::vector<Node> children;
+  for (unsigned bit = 0; bit < size; ++bit, i *= 2)
+  {
+    Node cond =
+        nm->mkNode(kind::EQUAL,
+                   nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), node[0]),
+                   bvone);
+    children.push_back(
+        nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z));
+  }
+  // avoid plus with one child
+  return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
+}
+
 }/* CVC4::theory::bv::utils namespace */
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 23eaab3f8..30454be4a 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -206,6 +206,15 @@ void intersect(const std::vector<uint32_t>& v1,
                const std::vector<uint32_t>& v2,
                std::vector<uint32_t>& intersection);
 
+/**
+ * Returns the rewritten form of node, which is a term of the form bv2nat(x).
+ * The return value of this method is the integer sum:
+ *   (+ ite( (= ((_ extract (n-1) (n-1)) x) 1) (^ 2 (n-1)) 0)
+ *      ...
+ *      ite( (= ((_ extract 0 0) x) 1) (^ 2 0) 0))
+ * where n is the bitwidth of x.
+ */
+Node eliminateBv2Nat(TNode node);
 }
 }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 518e3a889..176eb0bf8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -333,6 +333,7 @@ set(regress_0_tests
   regress0/bv/fuzz40.delta01.smtv1.smt2
   regress0/bv/fuzz40.smtv1.smt2
   regress0/bv/fuzz41.smtv1.smt2
+  regress0/bv/issue3621.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
diff --git a/test/regress/regress0/bv/issue3621.smt2 b/test/regress/regress0/bv/issue3621.smt2
new file mode 100644
index 000000000..d2121e828
--- /dev/null
+++ b/test/regress/regress0/bv/issue3621.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BVLIA)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 1))
+(assert (< (bv2nat a) 1))
+(check-sat)