From 9bb84e49df11dd669db1fff22cb69a08dfaa7bb4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jan 2020 13:31:44 -0600 Subject: [PATCH] Avoid PLUS with one child for bv2nat elimination (#3639) --- src/theory/bv/theory_bv.cpp | 16 +------------- ...ry_bv_rewrite_rules_operator_elimination.h | 15 +------------ src/theory/bv/theory_bv_utils.cpp | 22 +++++++++++++++++++ src/theory/bv/theory_bv_utils.h | 9 ++++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/bv/issue3621.smt2 | 5 +++++ 6 files changed, 39 insertions(+), 29 deletions(-) create mode 100644 test/regress/regress0/bv/issue3621.smt2 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::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& 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 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& v1, const std::vector& v2, std::vector& 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) -- 2.30.2