Merge branch 'master' into rm_cd_set_collectionrm_cd_set_collection

4 files changed, 124 insertions, 35 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 92f905c8b..84278ff8a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -2,9 +2,9 @@
 /*! \file node.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Tim King
+ **   Morgan Deters, Dejan Jovanovic, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -923,24 +923,100 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) {
   return out;
 }
 
+namespace {
+
+template <typename T>
+void nodeContainerToOut(std::ostream& out, const T& container)
+{
+  out << "[";
+  bool is_first = true;
+  for (const auto& item : container)
+  {
+    out << (!is_first ? ", " : "") << item;
+    is_first = false;
+  }
+  out << "]";
+}
+
+}
+
 /**
- * Serializes a vector of node to the given stream.
+ * Serialize a vector of nodes to given stream.
  *
  * @param out the output stream to use
- * @param ns the vector of nodes to output to the stream
+ * @param container the vector of nodes to output to the stream
  * @return the stream
  */
-template<bool ref_count>
-inline std::ostream& operator<<(std::ostream& out,
-                                const std::vector< NodeTemplate<ref_count> > & ns) {
-  for(typename std::vector< NodeTemplate<ref_count> >::const_iterator
-        i=ns.begin(), end=ns.end();
-      i != end; ++i){
-    out << *i;
-  }
+template <bool RC>
+std::ostream& operator<<(std::ostream& out,
+                         const std::vector<NodeTemplate<RC>>& container)
+{
+  nodeContainerToOut(out, container);
+  return out;
+}
+
+/**
+ * Serialize a set of nodes to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the set of nodes to output to the stream
+ * @return the stream
+ */
+template <bool RC>
+std::ostream& operator<<(std::ostream& out,
+                         const std::set<NodeTemplate<RC>>& container)
+{
+  nodeContainerToOut(out, container);
+  return out;
+}
+
+/**
+ * Serialize an unordered_set of nodes to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the unordered_set of nodes to output to the stream
+ * @return the stream
+ */
+template <bool RC, typename hash_function>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_set<NodeTemplate<RC>, hash_function>& container)
+{
+  nodeContainerToOut(out, container);
   return out;
 }
 
+/**
+ * Serialize a map of nodes to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the map of nodes to output to the stream
+ * @return the stream
+ */
+template <bool RC, typename V>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::map<NodeTemplate<RC>, V>& container)
+{
+  nodeContainerToOut(out, container);
+  return out;
+}
+
+/**
+ * Serialize an unordered_map of nodes to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the unordered_map of nodes to output to the stream
+ * @return the stream
+ */
+template <bool RC, typename V, typename HF>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_map<NodeTemplate<RC>, V, HF>& container)
+{
+  nodeContainerToOut(out, container);
+  return out;
+}
 
 }/* CVC4 namespace */
 
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);
-
 }
 }
 }