Fix node arity issue in reduction of int2bv (#3777)

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index a35176a9359fd53e4db8b0d6653683c2b2e16e46..03f55c0595e46fa9f4a604daa891947ee5cb3856 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -615,7 +615,6 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
 int TheoryBV::getReduction(int effort, Node n, Node& nr)
 {
   Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
-  NodeManager* const nm = NodeManager::currentNM();
   if (n.getKind() == kind::BITVECTOR_TO_NAT)
   {
     nr = utils::eliminateBv2Nat(n);
@@ -623,25 +622,7 @@ int TheoryBV::getReduction(int effort, Node n, Node& nr)
   }
   else if (n.getKind() == kind::INT_TO_BITVECTOR)
   {
-    // taken from rewrite code
-    const unsigned size = n.getOperator().getConst<IntToBitVector>().size;
-    const Node bvzero = utils::mkZero(1);
-    const Node bvone = utils::mkOne(1);
-    std::vector<Node> v;
-    Integer i = 2;
-    while (v.size() < size)
-    {
-      Node cond = nm->mkNode(
-          kind::GEQ,
-          nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))),
-          nm->mkConst(Rational(i, 2)));
-      cond = Rewriter::rewrite(cond);
-      v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
-      i *= 2;
-    }
-    NodeBuilder<> result(kind::BITVECTOR_CONCAT);
-    result.append(v.rbegin(), v.rend());
-    nr = Node(result);
+    nr = utils::eliminateBv2Nat(n);
     return -1;
   }
   return 0;

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 c9f814be640a3623bd34b5b9226cb5807e51f5d3..aef20ee0a40be62668b9d7fd26ce4cf42c155089 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -292,23 +292,7 @@ inline Node RewriteRule<IntToBVEliminate>::apply(TNode node)
   //if( node[0].isConst() ){
     //TODO? direct computation instead of term construction+rewriting
   //}
-
-  const unsigned size = node.getOperator().getConst<IntToBitVector>().size;
-  NodeManager* const nm = NodeManager::currentNM();
-  const Node bvzero = utils::mkZero(1);
-  const Node bvone = utils::mkOne(1);
-
-  std::vector<Node> v;
-  Integer i = 2;
-  while(v.size() < size) {
-    Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
-    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
-    i *= 2;
-  }
-
-  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
-  result.append(v.rbegin(), v.rend());
-  return Node(result);
+  return utils::eliminateInt2Bv(node);
 }
 
 template <>

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 2094e804fd41663170138ffbdca274a7f6cc302b..44510c26b49042b3a5da1169b7e3e7930849c41f 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -481,6 +481,33 @@ Node eliminateBv2Nat(TNode node)
   return children.size() == 1 ? children[0] : nm->mkNode(kind::PLUS, children);
 }
 
+Node eliminateInt2Bv(TNode node)
+{
+  const uint32_t size = node.getOperator().getConst<IntToBitVector>().size;
+  NodeManager* const nm = NodeManager::currentNM();
+  const Node bvzero = utils::mkZero(1);
+  const Node bvone = utils::mkOne(1);
+
+  std::vector<Node> v;
+  Integer i = 2;
+  while (v.size() < size)
+  {
+    Node cond = nm->mkNode(
+        kind::GEQ,
+        nm->mkNode(kind::INTS_MODULUS_TOTAL, node[0], nm->mkConst(Rational(i))),
+        nm->mkConst(Rational(i, 2)));
+    v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
+    i *= 2;
+  }
+  if (v.size() == 1)
+  {
+    return v[0];
+  }
+  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  result.append(v.rbegin(), v.rend());
+  return Node(result);
+}
+
 }/* 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 30454be4ac9329cf400dce9b1c632a880bb61cc0..4303926f1b2c7c86361b953fe5553959082980af 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -215,6 +215,15 @@ void intersect(const std::vector<uint32_t>& v1,
  * where n is the bitwidth of x.
  */
 Node eliminateBv2Nat(TNode node);
+/**
+ * Returns the rewritten form of node, which is a term of the form int2bv(x).
+ * The return value of this method is the concatenation term:
+ *   (bvconcat ite( (>= (mod x (^ 2 n)) (^ 2 (n-1))) (_ bv1 1) (_ bv1 0))
+ *             ...
+ *             ite( (>= (mod x (^ 2 1)) (^ 2 0)) (_ bv1 1) (_ bv1 0)))
+ * where n is the bit-width of x.
+ */
+Node eliminateInt2Bv(TNode node);
 }
 }
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6acc6f7c82f9cdf48011d63d14fde6f83f439fed..00faecedd0ac376138ca37c8273a6e46dd5d49d6 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1200,6 +1200,7 @@ set(regress_1_tests
   regress1/bv/fuzz34.smtv1.smt2
   regress1/bv/fuzz38.smtv1.smt2
   regress1/bv/issue3654.smt2
+  regress1/bv/issue3776.smt2
   regress1/bv/test-bv-abstraction.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2

diff --git a/test/regress/regress1/bv/issue3776.smt2 b/test/regress/regress1/bv/issue3776.smt2
new file mode 100644 (file)
index 0000000..215f3e2
--- /dev/null
+++ b/test/regress/regress1/bv/issue3776.smt2
@@ -0,0 +1,6 @@
+; COMMAND_LINE: --rewrite-divk
+; EXPECT: sat
+(set-logic QF_BVLIA)
+(declare-fun t () Int)
+(assert (= t (bv2nat ((_ int2bv 1) t))))
+(check-sat)