Simplify and cleanup bv::utils::mkConjunction. (#1571)

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