From 312e94e4233244654f11218ef38cabb1c51c6f7d Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 8 Feb 2018 08:10:36 -0800
Subject: [PATCH] Simplify and cleanup bv::utils::mkConjunction. (#1571)

---
 src/theory/bv/theory_bv_utils.cpp | 79 ++++---------------------------
 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.  */
-- 
2.30.2