Use template for bv::utils::mkOr. (#1570)

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 7df575ece2d55d88c4a05d3d80b740fbe3dbd7b9..9b66574f6e90ef25c445a6d86099a5772c8b6e0f 100644 (file)
--- 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 6e6cdcabe78793c5e8fef8c16ee8a137d2aab3f3..f6784621f86293caf9ce5f413be77d317d667ea8 100644 (file)
--- 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);