From 903570f7620aa989f6c717e8103c238069fc8d39 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 13 Feb 2018 15:02:28 -0800
Subject: [PATCH] Moved (unrecursified) bv::utils::collectVars. (#1602)

---
 src/theory/bv/bv_subtheory_algebraic.cpp | 36 +++++++++++++++++++++++-
 src/theory/bv/theory_bv_utils.cpp        | 18 ------------
 src/theory/bv/theory_bv_utils.h          |  5 +---
 3 files changed, 36 insertions(+), 23 deletions(-)

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index ef5844e1f..888c95692 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -23,6 +23,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
+#include <unordered_set>
 
 using namespace CVC4::context;
 using namespace CVC4::prop;
@@ -33,6 +34,38 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+/* ------------------------------------------------------------------------- */
+
+namespace {
+
+/* Collect all variables under a given a node.  */
+void collectVariables(TNode node, utils::NodeSet& vars)
+{
+  std::vector<TNode> stack;
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+
+  stack.push_back(node);
+  while (!stack.empty())
+  {
+    Node n = stack.back();
+    stack.pop_back();
+
+    if (vars.find(n) != vars.end()) continue;
+    if (visited.find(n) != visited.end()) continue;
+    visited.insert(n);
+
+    if (Theory::isLeafOf(n, THEORY_BV) && n.getKind() != kind::CONST_BITVECTOR)
+    {
+      vars.insert(n);
+      continue;
+    }
+    stack.insert(stack.end(), n.begin(), n.end());
+  }
+}
+
+};
+
+/* ------------------------------------------------------------------------- */
 
 bool hasExpensiveBVOperators(TNode fact);
 Node mergeExplanations(const std::vector<Node>& expls);
@@ -677,6 +710,7 @@ void AlgebraicSolver::assertFact(TNode fact) {
 EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_UNKNOWN;
 }
+
 bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
 {
   Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
@@ -705,7 +739,7 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
     Debug("bitvector-model") << "   " << current << " => " << subst << "\n";
     values[i] = subst;
-    utils::collectVariables(subst, leaf_vars);
+    collectVariables(subst, leaf_vars);
   }
 
   Debug("bitvector-model") << "Model:\n";
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index eaa9f463b..ef56a30cc 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -496,24 +496,6 @@ void intersect(const std::vector<uint32_t>& v1,
 
 /* ------------------------------------------------------------------------- */
 
-void collectVariables(TNode node, NodeSet& vars)
-{
-  if (vars.find(node) != vars.end()) return;
-
-  if (Theory::isLeafOf(node, THEORY_BV)
-      && node.getKind() != kind::CONST_BITVECTOR)
-  {
-    vars.insert(node);
-    return;
-  }
-  for (unsigned i = 0; i < node.getNumChildren(); ++i)
-  {
-    collectVariables(node[i], vars);
-  }
-}
-
-/* ------------------------------------------------------------------------- */
-
 }/* CVC4::theory::bv::utils namespace */
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 1e27d75c0..e1a37cf76 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Dejan Jovanovic, Morgan Deters
+ **   Aina Niemetz, Dejan Jovanovic, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -194,9 +194,6 @@ void intersect(const std::vector<uint32_t>& v1,
                const std::vector<uint32_t>& v2,
                std::vector<uint32_t>& intersection);
 
-/* Collect all variables under a given a node.  */
-void collectVariables(TNode node, NodeSet& vars);
-
 }
 }
 }
-- 
2.30.2