Add uniform way to serialize containers of Expr to stream. (#1638)

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f4dd294a7adaa01f43cb989d146313a2026bdf8c..6bcd1502767b8a4d857253c85bce81d91510db5f 100644 (file)
--- 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 cc9949c30b89d446c18d08b9e6c94ba4c5c2109a..f406981a83c3693ae988e69876c1bda35b8f96c8 100644 (file)
--- 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 84278ff8a208e06451a4f88ffc41934f45de462e..e1b9795705d2dd78779b7c5bcd2809ffcb964acb 100644 (file)
--- 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 adfd2bc641d71337bb1647ad2a8147882b7cf397..78a1e94f7f0f1bbeedff3932ca7f6ec739cb218f 100644 (file)
--- 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 */