Merge quantifiers2-trunk:

   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

1 files changed, 19 insertions, 0 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 0b150d25d..b0fda3354 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -892,6 +892,25 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) {
   return out;
 }
 
+/**
+ * Serializes a vector of node to the given stream.
+ *
+ * @param out the output stream to use
+ * @param ns 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;
+  }
+  return out;
+}
+
+
 }/* CVC4 namespace */
 
 #include <ext/hash_map>