Use template for bv::utils::mkAnd. (#1569)

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index da3822aa68d17b523d7b99b94b4d315e9dbc31b6..7df575ece2d55d88c4a05d3d80b740fbe3dbd7b9 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -370,62 +370,6 @@ Node mkAnd(TNode node1, TNode node2)
   return NodeManager::currentNM()->mkNode(kind::AND, node1, node2);
 }
 
-Node mkAnd(const std::vector<TNode>& conjunctions)
-{
-  std::set<TNode> all;
-  all.insert(conjunctions.begin(), conjunctions.end());
-
-  if (all.size() == 0)
-  {
-    return mkTrue();
-  }
-
-  if (all.size() == 1)
-  {
-    // All the same, or just one
-    return conjunctions[0];
-  }
-
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end)
-  {
-    conjunction << *it;
-    ++it;
-  }
-
-  return conjunction;
-}
-
-Node mkAnd(const std::vector<Node>& conjunctions)
-{
-  std::set<TNode> all;
-  all.insert(conjunctions.begin(), conjunctions.end());
-
-  if (all.size() == 0)
-  {
-    return mkTrue();
-  }
-
-  if (all.size() == 1)
-  {
-    // All the same, or just one
-    return conjunctions[0];
-  }
-
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end)
-  {
-    conjunction << *it;
-    ++it;
-  }
-
-  return conjunction;
-}
-
 Node mkOr(TNode node1, TNode node2)
 {
   return NodeManager::currentNM()->mkNode(kind::OR, node1, node2);

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 6115a7e96a690103385c0fe8610f9d46b7be2769..6e6cdcabe78793c5e8fef8c16ee8a137d2aab3f3 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -127,8 +127,21 @@ Node mkSortedNode(Kind kind, std::vector<Node>& children);
 Node mkNot(Node child);
 /* Create node of kind AND. */
 Node mkAnd(TNode node1, TNode node2);
-Node mkAnd(const std::vector<TNode>& conjunctions);
-Node mkAnd(const std::vector<Node>& conjunctions);
+/* Create n-ary node of kind AND. */
+template<bool ref_count>
+Node mkAnd(const std::vector<NodeTemplate<ref_count>>& conjunctions)
+{
+  std::set<TNode> all(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 0) { return mkTrue(); }
+
+  /* All the same, or just one  */
+  if (all.size() == 1) { return conjunctions[0]; }
+
+  NodeBuilder<> conjunction(kind::AND);
+  for (const Node& n : all) { conjunction << n; }
+  return conjunction;
+}
 /* Create node of kind OR. */
 Node mkOr(TNode node1, TNode node2);
 Node mkOr(const std::vector<Node>& nodes);