diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-07 12:34:59 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-07 12:34:59 -0800 |
commit | b661071c238ea32e72ee6bddbff65f38328dd345 (patch) | |
tree | 01493bc735e9ed77d5f530e8205728a6adbd6b2b | |
parent | a5c952d63bca9f94d3886db4d9c09d08d7a23033 (diff) |
Use template for bv::utils::mkOr. (#1570)
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 28 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 16 |
2 files changed, 15 insertions, 29 deletions
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index 7df575ece..9b66574f6 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -375,34 +375,6 @@ Node mkOr(TNode node1, TNode node2) return NodeManager::currentNM()->mkNode(kind::OR, node1, node2); } -Node mkOr(const std::vector<Node>& nodes) -{ - std::set<TNode> all; - all.insert(nodes.begin(), nodes.end()); - - if (all.size() == 0) - { - return mkTrue(); - } - - if (all.size() == 1) - { - // All the same, or just one - return nodes[0]; - } - - NodeBuilder<> disjunction(kind::OR); - std::set<TNode>::const_iterator it = all.begin(); - std::set<TNode>::const_iterator it_end = all.end(); - while (it != it_end) - { - disjunction << *it; - ++it; - } - - return disjunction; -} - Node mkXor(TNode node1, TNode node2) { return NodeManager::currentNM()->mkNode(kind::XOR, node1, node2); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 6e6cdcabe..f6784621f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -144,7 +144,21 @@ Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions) } /* Create node of kind OR. */ Node mkOr(TNode node1, TNode node2); -Node mkOr(const std::vector<Node>& nodes); +/* Create n-ary node of kind OR. */ +template<bool ref_count> +Node mkOr(const std::vector<NodeTemplate<ref_count>>& nodes) +{ + std::set<TNode> all(nodes.begin(), nodes.end()); + + if (all.size() == 0) { return mkTrue(); } + + /* All the same, or just one */ + if (all.size() == 1) { return nodes[0]; } + + NodeBuilder<> disjunction(kind::OR); + for (const Node& n : all) { disjunction << n; } + return disjunction; +} /* Create node of kind XOR. */ Node mkXor(TNode node1, TNode node2); |