diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-08 08:10:36 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-08 10:10:36 -0600 |
commit | 312e94e4233244654f11218ef38cabb1c51c6f7d (patch) | |
tree | 5b7f11a5e155f4f640a326e7716ee9fa123a8653 | |
parent | aa62cb849687985e499fe28ff18b62938b657e92 (diff) |
Simplify and cleanup bv::utils::mkConjunction. (#1571)
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 79 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 3 |
2 files changed, 10 insertions, 72 deletions
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 9b66574f6..9e05ef516 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -480,82 +480,21 @@ Node mkUmulo(TNode t1, TNode t2) /* ------------------------------------------------------------------------- */ -Node mkConjunction(const std::set<TNode> nodes) -{ - std::set<TNode> expandedNodes; - - std::set<TNode>::const_iterator it = nodes.begin(); - std::set<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) - { - TNode current = *it; - if (current != mkTrue()) - { - Assert(current.getKind() == kind::EQUAL - || (current.getKind() == kind::NOT - && current[0].getKind() == kind::EQUAL)); - expandedNodes.insert(current); - } - ++it; - } - - Assert(expandedNodes.size() > 0); - if (expandedNodes.size() == 1) - { - return *expandedNodes.begin(); - } - - NodeBuilder<> conjunction(kind::AND); - - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) - { - conjunction << *it; - ++it; - } - - return conjunction; -} - Node mkConjunction(const std::vector<TNode>& nodes) { - std::vector<TNode> expandedNodes; - - std::vector<TNode>::const_iterator it = nodes.begin(); - std::vector<TNode>::const_iterator it_end = nodes.end(); - while (it != it_end) + NodeBuilder<> conjunction(kind::AND); + Node btrue = mkTrue(); + for (const Node& n : nodes) { - TNode current = *it; - - if (current != mkTrue()) + if (n != btrue) { - Assert(isBVPredicate(current)); - expandedNodes.push_back(current); + Assert(isBVPredicate(n)); + conjunction << n; } - ++it; - } - - if (expandedNodes.size() == 0) - { - return mkTrue(); - } - - if (expandedNodes.size() == 1) - { - return *expandedNodes.begin(); - } - - NodeBuilder<> conjunction(kind::AND); - - it = expandedNodes.begin(); - it_end = expandedNodes.end(); - while (it != it_end) - { - conjunction << *it; - ++it; } - + unsigned nchildren = conjunction.getNumChildren(); + if (nchildren == 0) { return btrue; } + if (nchildren == 1) { return conjunction[0]; } return conjunction; } diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index f6784621f..6f1300632 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -190,8 +190,7 @@ Node mkDec(TNode t); * http://ieeexplore.ieee.org/document/987767 */ Node mkUmulo(TNode t1, TNode t2); -/* Create conjunction over a set of (dis)equalities. */ -Node mkConjunction(const std::set<TNode> nodes); +/* Create conjunction. */ Node mkConjunction(const std::vector<TNode>& nodes); /* Get a set of all operands of nested and nodes. */ |