Dagification of output expressions.

By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.

If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.

9 files changed, 172 insertions, 23 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 78d04f000..ae24f4984 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -43,6 +43,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
   c.toStream(out,
              Node::setdepth::getDepth(out),
              Node::printtypes::getPrintTypes(out),
+             Node::dag::getDag(out),
              Node::setlanguage::getLanguage(out));
   return out;
 }
@@ -101,9 +102,9 @@ std::string Command::toString() const throw() {
   return ss.str();
 }
 
-void Command::toStream(std::ostream& out, int toDepth, bool types,
+void Command::toStream(std::ostream& out, int toDepth, bool types, size_t dag,
                        OutputLanguage language) const throw() {
-  Printer::getPrinter(language)->toStream(out, this, toDepth, types);
+  Printer::getPrinter(language)->toStream(out, this, toDepth, types, dag);
 }
 
 void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 19d1f16e7..98046c242 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -205,7 +205,7 @@ public:
   virtual void invoke(SmtEngine* smtEngine) throw() = 0;
   virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
-  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+  virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                         OutputLanguage language = language::output::LANG_AST) const throw();
 
   std::string toString() const throw();
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 6ed7f2d25..9b6c55703 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -9,6 +9,7 @@
 
 %ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth);
 %ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
 %ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
 
 %rename(assign) CVC4::Expr::operator=(const Expr&);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index d0f5fde9e..c70fed889 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -45,6 +45,7 @@ namespace expr {
 
 const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
 const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
+const int ExprDag::s_iosIndex = std::ios_base::xalloc();
 const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
@@ -416,10 +417,10 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
-void Expr::toStream(std::ostream& out, int depth, bool types,
+void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag,
                     OutputLanguage language) const {
   ExprManagerScope ems(*this);
-  d_node->toStream(out, depth, types, language);
+  d_node->toStream(out, depth, types, dag, language);
 }
 
 Node Expr::getNode() const throw() {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 7a6c0179d..6cd476a5f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -79,6 +79,7 @@ namespace smt {
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
+  class CVC4_PUBLIC ExprDag;
   class CVC4_PUBLIC ExprSetLanguage;
 
   NodeTemplate<true> exportInternal(NodeTemplate<false> n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
@@ -400,7 +401,7 @@ public:
    * debugging expressions)
    * @param language the language in which to output
    */
-  void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                 OutputLanguage language = language::output::LANG_AST) const;
 
   /**
@@ -493,6 +494,11 @@ public:
   typedef expr::ExprPrintTypes printtypes;
 
   /**
+   * IOStream manipulator to print expressions as a DAG (or not).
+   */
+  typedef expr::ExprDag dag;
+
+  /**
    * IOStream manipulator to set the output language for Exprs.
    */
   typedef expr::ExprSetLanguage setlanguage;
@@ -722,13 +728,13 @@ public:
  */
 class CVC4_PUBLIC ExprPrintTypes {
   /**
-   * The allocated index in ios_base for our depth setting.
+   * The allocated index in ios_base for our setting.
    */
   static const int s_iosIndex;
 
   /**
-   * The default depth to print, for ostreams that haven't yet had a
-   * setdepth() applied to them.
+   * The default printtypes setting, for ostreams that haven't yet had a
+   * printtypes() applied to them.
    */
   static const int s_defaultPrintTypes = false;
 
@@ -782,6 +788,85 @@ public:
 };/* class ExprPrintTypes */
 
 /**
+ * IOStream manipulator to print expressions as a dag (or not).
+ */
+class CVC4_PUBLIC ExprDag {
+  /**
+   * The allocated index in ios_base for our setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default setting, for ostreams that haven't yet had a
+   * dag() applied to them.
+   */
+  static const size_t s_defaultDag = 1;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  size_t d_dag;
+
+public:
+  /**
+   * Construct a ExprDag with the given setting (dagification on or off).
+   */
+  explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
+
+  /**
+   * Construct a ExprDag with the given setting (letify only common
+   * subexpressions that appear more than 'dag' times).  dag==0 means
+   * don't dagify.
+   */
+  ExprDag(size_t dag) : d_dag(dag) {}
+
+  inline void applyDag(std::ostream& out) {
+    // (offset by one to detect whether default has been set yet)
+    out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
+  }
+
+  static inline size_t getDag(std::ostream& out) {
+    long& l = out.iword(s_iosIndex);
+    if(l == 0) {
+      // set the default dag setting on this ostream
+      // (offset by one to detect whether default has been set yet)
+      l = s_defaultDag + 1;
+    }
+    return static_cast<size_t>(l - 1);
+  }
+
+  static inline void setDag(std::ostream& out, size_t dag) {
+    // (offset by one to detect whether default has been set yet)
+    out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
+  }
+
+  /**
+   * Set the dag state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    size_t d_oldDag;
+
+  public:
+
+    inline Scope(std::ostream& out, size_t dag) :
+      d_out(out),
+      d_oldDag(ExprDag::getDag(out)) {
+      ExprDag::setDag(out, dag);
+    }
+
+    inline ~Scope() {
+      ExprDag::setDag(d_out, d_oldDag);
+    }
+
+  };/* class ExprDag::Scope */
+
+};/* class ExprDag */
+
+/**
  * IOStream manipulator to set the output language for Exprs.
  */
 class CVC4_PUBLIC ExprSetLanguage {
@@ -857,13 +942,13 @@ public:
 
 ${getConst_instantiations}
 
-#line 861 "${template}"
+#line 938 "${template}"
 
 namespace expr {
 
 /**
- * Sets the default print-types setting when pretty-printing an Expr
- * to an ostream.  Use like this:
+ * Sets the default depth when pretty-printing a Expr to an ostream.
+ * Use like this:
  *
  *   // let out be an ostream, e an Expr
  *   out << Expr::setdepth(n) << e << endl;
@@ -876,11 +961,11 @@ inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
 }
 
 /**
- * Sets the default depth when pretty-printing a Expr to an ostream.
- * Use like this:
+ * Sets the default print-types setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
  *
  *   // let out be an ostream, e an Expr
- *   out << Expr::setprinttypes(true) << e << endl;
+ *   out << Expr::printtypes(true) << e << endl;
  *
  * The setting stays permanently (until set again) with the stream.
  */
@@ -890,6 +975,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
 }
 
 /**
+ * Sets the default dag setting when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::dag(true) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
+  d.applyDag(out);
+  return out;
+}
+
+/**
  * Sets the output language when pretty-printing a Expr to an ostream.
  * Use like this:
  *
diff --git a/src/expr/node.h b/src/expr/node.h
index 3532116bc..a61944433 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -803,10 +803,10 @@ public:
    * (might break language compliance, but good for debugging expressions)
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                        OutputLanguage language = language::output::LANG_AST) const {
     assertTNodeNotExpired();
-    d_nv->toStream(out, toDepth, types, language);
+    d_nv->toStream(out, toDepth, types, dag, language);
   }
 
   /**
@@ -837,6 +837,11 @@ public:
   typedef expr::ExprPrintTypes printtypes;
 
   /**
+   * IOStream manipulator to print expressions as DAGs (or not).
+   */
+  typedef expr::ExprDag dag;
+
+  /**
    * IOStream manipulator to set the output language for Exprs.
    */
   typedef expr::ExprSetLanguage setlanguage;
@@ -885,6 +890,7 @@ inline std::ostream& operator<<(std::ostream& out, TNode n) {
   n.toStream(out,
              Node::setdepth::getDepth(out),
              Node::printtypes::getPrintTypes(out),
+             Node::dag::getDag(out),
              Node::setlanguage::getLanguage(out));
   return out;
 }
@@ -1468,6 +1474,16 @@ bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) con
  */
 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
   Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(true)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) {
+  Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(false)
             << Node::setlanguage(language::output::LANG_AST)
             << n << std::endl;
   Warning().flush();
@@ -1479,6 +1495,16 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n)
 
 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
   Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(true)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) {
+  Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(false)
             << Node::setlanguage(language::output::LANG_AST)
             << n << std::endl;
   Warning().flush();
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 970d2e0fc..dbf706c45 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -45,14 +45,14 @@ string NodeValue::toString() const {
   return ss.str();
 }
 
-void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
+void NodeValue::toStream(std::ostream& out, int toDepth, bool types, size_t dag,
                          OutputLanguage language) const {
   // Ensure that this node value is live for the length of this call.
   // It really breaks things badly if we don't have a nonzero ref
   // count, even just for printing.
   RefCountGuard guard(this);
 
-  Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types);
+  Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types, dag);
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index e5ecfbc48..657fabeb5 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -267,7 +267,7 @@ public:
   }
 
   std::string toString() const;
-  void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                 OutputLanguage = language::output::LANG_AST) const;
 
   static inline unsigned kindToDKind(Kind k) {
@@ -487,6 +487,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
   nv.toStream(out,
               Node::setdepth::getDepth(out),
               Node::printtypes::getPrintTypes(out),
+              Node::dag::getDag(out),
               Node::setlanguage::getLanguage(out));
   return out;
 }
@@ -501,11 +502,20 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
  */
 static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) {
   Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(true)
+            << Node::setlanguage(language::output::LANG_AST)
+            << *nv << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) {
+  Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(false)
             << Node::setlanguage(language::output::LANG_AST)
             << *nv << std::endl;
   Warning().flush();
 }
-
 static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) {
   nv->printAst(Warning(), 0);
   Warning().flush();
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 482da2814..bfbedde88 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -389,9 +389,9 @@ public:
    * (might break language compliance, but good for debugging expressions)
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                        OutputLanguage language = language::output::LANG_AST) const {
-    d_nv->toStream(out, toDepth, types, language);
+    d_nv->toStream(out, toDepth, types, dag, language);
   }
 
   /**
@@ -636,6 +636,7 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
   n.toStream(out,
              Node::setdepth::getDepth(out),
              Node::printtypes::getPrintTypes(out),
+             Node::dag::getDag(out),
              Node::setlanguage::getLanguage(out));
   return out;
 }
@@ -980,6 +981,16 @@ inline const SubrangeBounds& TypeNode::getSubrangeBounds() const {
  */
 static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) {
   Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(true)
+            << Node::setlanguage(language::output::LANG_AST)
+            << n << std::endl;
+  Warning().flush();
+}
+static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) {
+  Warning() << Node::setdepth(-1)
+            << Node::printtypes(false)
+            << Node::dag(false)
             << Node::setlanguage(language::output::LANG_AST)
             << n << std::endl;
   Warning().flush();