From 78cd7af7b3897d630ad375f72d43b4c67df6d557 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 5 Mar 2018 11:26:53 -0800
Subject: [PATCH] Add uniform way to serialize containers of Expr to stream.
 (#1638)

---
 src/expr/expr_template.cpp | 36 +++++++++++++++++++++++++
 src/expr/expr_template.h   | 54 ++++++++++++++++++++++++++++++++++++++
 src/expr/node.h            | 27 ++++---------------
 src/util/utility.h         | 13 +++++++++
 4 files changed, 108 insertions(+), 22 deletions(-)

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f4dd294a7..6bcd15027 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -54,6 +54,42 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
   }
 }
 
+std::ostream& operator<<(std::ostream& out, const std::vector<Expr>& container)
+{
+  container_to_stream(out, container);
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const std::set<Expr>& container)
+{
+  container_to_stream(out, container);
+  return out;
+}
+
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_set<Expr, ExprHashFunction>& container)
+{
+  container_to_stream(out, container);
+  return out;
+}
+
+template <typename V>
+std::ostream& operator<<(std::ostream& out, const std::map<Expr, V>& container)
+{
+  container_to_stream(out, container);
+  return out;
+}
+
+template <typename V>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_map<Expr, V, ExprHashFunction>& container)
+{
+  container_to_stream(out, container);
+  return out;
+}
+
 TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
     : Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
 {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index cc9949c30..f406981a8 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -30,7 +30,10 @@ ${includes}
 #include <iosfwd>
 #include <iterator>
 #include <string>
+#include <map>
+#include <set>
 #include <unordered_map>
+#include <unordered_set>
 
 #include "base/exception.h"
 #include "options/language.h"
@@ -141,6 +144,57 @@ std::ostream& operator<<(std::ostream& out,
  */
 std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
 
+/**
+ * Serialize a vector of expressions to given stream.
+ *
+ * @param out the output stream to use
+ * @param container the vector of expressions to output to the stream
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const std::vector<Expr>& container);
+
+/**
+ * Serialize a set of expressions to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the set of expressions to output to the stream
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const std::set<Expr>& container);
+
+/**
+ * Serialize an unordered_set of expressions to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the unordered_set of expressions to output to the stream
+ * @return the stream
+ */
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_set<Expr, ExprHashFunction>& container);
+
+/**
+ * Serialize a map of expressions to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the map of expressions to output to the stream
+ * @return the stream
+ */
+template <typename V>
+std::ostream& operator<<(std::ostream& out, const std::map<Expr, V>& container);
+
+/**
+ * Serialize an unordered_map of expressions to the given stream.
+ *
+ * @param out the output stream to use
+ * @param container the unordered_map of expressions to output to the stream
+ * @return the stream
+ */
+template <typename V>
+std::ostream& operator<<(
+    std::ostream& out,
+    const std::unordered_map<Expr, V, ExprHashFunction>& container);
+
 // for hash_maps, hash_sets..
 struct ExprHashFunction {
   size_t operator()(CVC4::Expr e) const;
diff --git a/src/expr/node.h b/src/expr/node.h
index 84278ff8a..e1b979570 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -923,23 +923,6 @@ 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 << "]";
-}
-
-}
-
 /**
  * Serialize a vector of nodes to given stream.
  *
@@ -951,7 +934,7 @@ template <bool RC>
 std::ostream& operator<<(std::ostream& out,
                          const std::vector<NodeTemplate<RC>>& container)
 {
-  nodeContainerToOut(out, container);
+  container_to_stream(out, container);
   return out;
 }
 
@@ -966,7 +949,7 @@ template <bool RC>
 std::ostream& operator<<(std::ostream& out,
                          const std::set<NodeTemplate<RC>>& container)
 {
-  nodeContainerToOut(out, container);
+  container_to_stream(out, container);
   return out;
 }
 
@@ -982,7 +965,7 @@ std::ostream& operator<<(
     std::ostream& out,
     const std::unordered_set<NodeTemplate<RC>, hash_function>& container)
 {
-  nodeContainerToOut(out, container);
+  container_to_stream(out, container);
   return out;
 }
 
@@ -998,7 +981,7 @@ std::ostream& operator<<(
     std::ostream& out,
     const std::map<NodeTemplate<RC>, V>& container)
 {
-  nodeContainerToOut(out, container);
+  container_to_stream(out, container);
   return out;
 }
 
@@ -1014,7 +997,7 @@ std::ostream& operator<<(
     std::ostream& out,
     const std::unordered_map<NodeTemplate<RC>, V, HF>& container)
 {
-  nodeContainerToOut(out, container);
+  container_to_stream(out, container);
   return out;
 }
 
diff --git a/src/util/utility.h b/src/util/utility.h
index adfd2bc64..78a1e94f7 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -67,6 +67,19 @@ inline InputIterator find_if_unique(InputIterator first, InputIterator last, Pre
   return (match2 == last) ? match : last;
 }
 
+template <typename T>
+void container_to_stream(std::ostream& out, const T& container)
+{
+  out << "[";
+  bool is_first = true;
+  for (const auto& item : container)
+  {
+    out << (!is_first ? ", " : "") << item;
+    is_first = false;
+  }
+  out << "]";
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UTILITY_H */
-- 
2.30.2