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.

11 files changed, 320 insertions, 32 deletions

diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am
index ca3cbacf1..3f0eba12d 100644
--- a/src/printer/Makefile.am
+++ b/src/printer/Makefile.am
@@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 noinst_LTLIBRARIES = libprinter.la
 
 libprinter_la_SOURCES = \
+	dagification_visitor.h \
 	printer.h \
 	printer.cpp \
 	ast/ast_printer.h \
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index b941957c4..5a7b2e834 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -21,6 +21,8 @@
 #include "util/language.h" // for LANG_AST
 #include "expr/node_manager.h" // for VarNameAttr
 #include "expr/command.h"
+#include "printer/dagification_visitor.h"
+#include "util/node_visitor.h"
 
 #include <iostream>
 #include <vector>
@@ -34,6 +36,40 @@ namespace printer {
 namespace ast {
 
 void AstPrinter::toStream(std::ostream& out, TNode n,
+                          int toDepth, bool types, size_t dag) const throw() {
+  if(dag != 0) {
+    DagificationVisitor dv(dag);
+    NodeVisitor<DagificationVisitor> visitor;
+    visitor.run(dv, n);
+    const theory::SubstitutionMap& lets = dv.getLets();
+    if(!lets.empty()) {
+      out << "(LET ";
+      bool first = true;
+      for(theory::SubstitutionMap::const_iterator i = lets.begin();
+          i != lets.end();
+          ++i) {
+        if(! first) {
+          out << ", ";
+        } else {
+          first = false;
+        }
+        toStream(out, (*i).second, toDepth, types, false);
+        out << " := ";
+        toStream(out, (*i).first, toDepth, types, false);
+      }
+      out << " IN ";
+    }
+    Node body = dv.getDagifiedBody();
+    toStream(out, body, toDepth, types);
+    if(!lets.empty()) {
+      out << ')';
+    }
+  } else {
+    toStream(out, n, toDepth, types);
+  }
+}
+
+void AstPrinter::toStream(std::ostream& out, TNode n,
                           int toDepth, bool types) const throw() {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
@@ -57,7 +93,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, language::output::LANG_AST);
+      n.getType().toStream(out, -1, false, 0, language::output::LANG_AST);
     }
 
     return;
@@ -73,8 +109,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       out << ' ';
       if(toDepth != 0) {
-        n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                                 types, language::output::LANG_AST);
+        toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
       } else {
         out << "(...)";
       }
@@ -87,8 +122,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
         out << ' ';
       }
       if(toDepth != 0) {
-        (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                      types, language::output::LANG_AST);
+        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types);
       } else {
         out << "(...)";
       }
@@ -101,9 +135,10 @@ template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void AstPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types) const throw() {
+                          int toDepth, bool types, size_t dag) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
+  expr::ExprDag::Scope dagScope(out, dag);
 
   if(tryToStream<EmptyCommand>(out, c) ||
      tryToStream<AssertCommand>(out, c) ||
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 2cae4c672..4dfb2c0d5 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -30,9 +30,10 @@ namespace printer {
 namespace ast {
 
 class AstPrinter : public CVC4::Printer {
-public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+public:
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class AstPrinter */
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index f779a1bdc..cc95d72b0 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -36,8 +36,37 @@ namespace CVC4 {
 namespace printer {
 namespace cvc {
 
-void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, bool bracket) const throw()
-{
+void CvcPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw() {
+  if(dag != 0) {
+    DagificationVisitor dv(dag);
+    NodeVisitor<DagificationVisitor> visitor;
+    visitor.run(dv, n);
+    const theory::SubstitutionMap& lets = dv.getLets();
+    if(!lets.empty()) {
+      out << "LET ";
+      bool first = true;
+      for(theory::SubstitutionMap::const_iterator i = lets.begin();
+          i != lets.end();
+          ++i) {
+        if(! first) {
+          out << ", ";
+        } else {
+          first = false;
+        }
+        toStream(out, (*i).second, toDepth, types, false);
+        out << " = ";
+        toStream(out, (*i).first, toDepth, types, false);
+      }
+      out << " IN ";
+    }
+    Node body = dv.getDagifiedBody();
+    toStream(out, body, toDepth, types, false);
+  } else {
+    toStream(out, n, toDepth, types, false);
+  }
+}
+
+void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, bool bracket) const throw() {
   if (depth == 0) {
     out << "(...)";
   } else {
@@ -568,9 +597,10 @@ template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void CvcPrinter::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types) const throw() {
+                           int toDepth, bool types, size_t dag) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
+  expr::ExprDag::Scope dagScope(out, dag);
 
   if(tryToStream<AssertCommand>(out, c) ||
      tryToStream<PushCommand>(out, c) ||
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 3db3f2c66..7fb611a79 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -24,6 +24,9 @@
 #include <iostream>
 
 #include "printer/printer.h"
+#include "printer/dagification_visitor.h"
+#include "theory/substitutions.h"
+#include "util/node_visitor.h"
 
 namespace CVC4 {
 namespace printer {
@@ -32,10 +35,8 @@ namespace cvc {
 class CvcPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw() {
-    toStream(out, n, toDepth, types, false);
-  }
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class CvcPrinter */
 
diff --git a/src/printer/dagification_visitor.h b/src/printer/dagification_visitor.h
new file mode 100644
index 000000000..8e17f6027
--- /dev/null
+++ b/src/printer/dagification_visitor.h
@@ -0,0 +1,180 @@
+/*********************                                                        */
+/*! \file dagification_visitor.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011, 2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__DAGIFICATION_VISITOR_H
+#define __CVC4__PRINTER__DAGIFICATION_VISITOR_H
+
+#include "context/context.h"
+#include "theory/substitutions.h"
+#include "expr/node.h"
+#include "util/hash.h"
+
+#include <vector>
+#include <string>
+#include <sstream>
+
+namespace CVC4 {
+namespace printer {
+
+class DagificationVisitor {
+
+  unsigned d_threshold;
+  std::string d_letVarPrefix;
+  std::hash_map<TNode, unsigned, TNodeHashFunction> d_nodeCount;
+  TNode d_top;
+  context::Context* d_context;
+  theory::SubstitutionMap* d_substitutions;
+  unsigned d_letVar;
+  bool d_done;
+  std::hash_map<TNode, TNode, TNodeHashFunction> d_uniqueParent;
+  std::vector<TNode> d_substNodes;
+
+public:
+
+  typedef void return_type;
+
+  DagificationVisitor(unsigned threshold, std::string letVarPrefix = "_let_") :
+    d_threshold(threshold),
+    d_letVarPrefix(letVarPrefix),
+    d_nodeCount(),
+    d_top(),
+    d_context(new context::Context()),
+    d_substitutions(new theory::SubstitutionMap(d_context)),
+    d_letVar(0),
+    d_done(false),
+    d_uniqueParent(),
+    d_substNodes() {
+
+    // 0 doesn't make sense
+    CheckArgument(threshold > 0, threshold);
+  }
+
+  ~DagificationVisitor() {
+    delete d_substitutions;
+    delete d_context;
+  }
+
+  /**
+   * Returns true if current has already been dagified.
+   */
+  bool alreadyVisited(TNode current, TNode parent) {
+    // don't visit variables, constants, or those exprs that we've
+    // already seen more than the threshold: if we've increased
+    // the count beyond the threshold already, we've done the same
+    // for all subexpressions, so it isn't useful to traverse and
+    // increment again (they'll be dagified anyway).
+    return current.getMetaKind() == kind::metakind::VARIABLE ||
+           current.getMetaKind() == kind::metakind::CONSTANT ||
+           ( ( current.getKind() == kind::NOT ||
+               current.getKind() == kind::UMINUS ) &&
+             ( current[0].getMetaKind() == kind::metakind::VARIABLE ||
+               current[0].getMetaKind() == kind::metakind::CONSTANT ) ) ||
+           current.getKind() == kind::SORT_TYPE ||
+           d_nodeCount[current] > d_threshold;
+  }
+
+  /**
+   * Dagify the "current" expression.
+   */
+  void visit(TNode current, TNode parent) {
+    if(d_uniqueParent.find(current) != d_uniqueParent.end()) {
+      TNode& uniqueParent = d_uniqueParent[current];
+
+      if(!uniqueParent.isNull() && uniqueParent != parent) {
+        // there is not a unique parent for this expr
+        uniqueParent = TNode::null();
+      }
+
+      unsigned count = ++d_nodeCount[current];
+
+      if(count > d_threshold) {
+        d_substNodes.push_back(current);
+      }
+    } else {
+      Assert(d_nodeCount[current] == 0);
+      d_nodeCount[current] = 1;
+      d_uniqueParent[current] = parent;
+    }
+  }
+
+  /**
+   * Marks the node as the starting literal.
+   */
+  void start(TNode node) {
+    Assert(!d_done, "DagificationVisitor cannot be re-used");
+    d_top = node;
+  }
+
+  /**
+   * Called when we're done with all visitation.
+   */
+  void done(TNode node) {
+    Assert(!d_done);
+
+    d_done = true;
+
+    // letify subexprs before parents (cascading LETs)
+    std::sort(d_substNodes.begin(), d_substNodes.end());
+
+    for(std::vector<TNode>::iterator i = d_substNodes.begin();
+        i != d_substNodes.end();
+        ++i) {
+      Assert(d_nodeCount[*i] > d_threshold);
+      TNode parent = d_uniqueParent[*i];
+      if(!parent.isNull() && d_nodeCount[parent] > d_threshold) {
+        // no need to letify this expr, because it only occurs in
+        // a single super-expression, and that one will be letified
+        continue;
+      }
+
+      std::stringstream ss;
+      ss << d_letVarPrefix << d_letVar++;
+      Node letvar = NodeManager::currentNM()->mkVar(ss.str(), (*i).getType());
+
+      Node n = d_substitutions->apply(*i);
+      // the three last arguments to addSubstitution are:
+      // invalidateCache -- the rhs of our substitution is a letvar,
+      //   we're not going to use it on lhs so no cache problem
+      // backSub - no need for SubstitutionMap to do internal substitution,
+      //   we did our own above
+      // forwardSub - ditto
+      Assert(! d_substitutions->hasSubstitution(n));
+      d_substitutions->addSubstitution(n, letvar);
+    }
+  }
+
+  /**
+   * Get the let substitutions.
+   */
+  const theory::SubstitutionMap& getLets() {
+    Assert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+    return *d_substitutions;
+  }
+
+  /**
+   * Return the let-substituted expression.
+   */
+  Node getDagifiedBody() {
+    Assert(d_done, "DagificationVisitor must be used as a visitor before getting the dagified version out!");
+    return d_substitutions->apply(d_top);
+  }
+
+};/* class DagificationVisitor */
+
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__DAGIFICATION_VISITOR_H */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 04b435060..8d1931a83 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -53,11 +53,11 @@ public:
 
   /** Write a Node out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, TNode n,
-                        int toDepth, bool types) const throw() = 0;
+                        int toDepth, bool types, size_t dag) const throw() = 0;
 
   /** Write a Command out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Command* c,
-                        int toDepth, bool types) const throw() = 0;
+                        int toDepth, bool types, size_t dag) const throw() = 0;
 
   /** Write a CommandStatus out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index e6490de63..f74a1e07d 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -34,13 +34,13 @@ namespace printer {
 namespace smt {
 
 void SmtPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const throw() {
-  n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
+                          int toDepth, bool types, size_t dag) const throw() {
+  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
 void SmtPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types) const throw() {
-  c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
+                          int toDepth, bool types, size_t dag) const throw() {
+  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
 void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 370e0908c..612dfd19e 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -31,8 +31,8 @@ namespace smt {
 
 class SmtPrinter : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class SmtPrinter */
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a1ee99d8f..d3ec376ae 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -24,6 +24,8 @@
 #include <typeinfo>
 
 #include "util/boolean_simplification.h"
+#include "printer/dagification_visitor.h"
+#include "util/node_visitor.h"
 
 using namespace std;
 
@@ -36,6 +38,42 @@ static string smtKindString(Kind k) throw();
 static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
 
 void Smt2Printer::toStream(std::ostream& out, TNode n,
+                           int toDepth, bool types, size_t dag) const throw() {
+  if(dag != 0) {
+    DagificationVisitor dv(dag);
+    NodeVisitor<DagificationVisitor> visitor;
+    visitor.run(dv, n);
+    const theory::SubstitutionMap& lets = dv.getLets();
+    if(!lets.empty()) {
+      out << "(let (";
+      bool first = true;
+      for(theory::SubstitutionMap::const_iterator i = lets.begin();
+          i != lets.end();
+          ++i) {
+        if(!first) {
+          out << ' ';
+        } else {
+          first = false;
+        }
+        out << '(';
+        toStream(out, (*i).second, toDepth, types);
+        out << ' ';
+        toStream(out, (*i).first, toDepth, types);
+        out << ')';
+      }
+      out << ") ";
+    }
+    Node body = dv.getDagifiedBody();
+    toStream(out, body, toDepth, types);
+    if(!lets.empty()) {
+      out << ')';
+    }
+  } else {
+    toStream(out, n, toDepth, types);
+  }
+}
+
+void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types) const throw() {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
@@ -59,7 +97,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, language::output::LANG_SMTLIB_V2);
+      n.getType().toStream(out, -1, false, 0, language::output::LANG_SMTLIB_V2);
     }
 
     return;
@@ -251,8 +289,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
      stillNeedToPrintParams) {
     if(toDepth != 0) {
-      n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                               types, language::output::LANG_SMTLIB_V2);
+      toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types);
     } else {
       out << "(...)";
     }
@@ -264,8 +301,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
         iend = n.end();
       i != iend; ) {
     if(toDepth != 0) {
-      (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                    types, language::output::LANG_SMTLIB_V2);
+      toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types);
     } else {
       out << "(...)";
     }
@@ -273,7 +309,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       out << ' ';
     }
   }
-  if(n.getNumChildren() != 0) out << ')';
+  if(n.getNumChildren() != 0) {
+    out << ')';
+  }
 }/* Smt2Printer::toStream(TNode) */
 
 static string smtKindString(Kind k) throw() {
@@ -395,9 +433,10 @@ template <class T>
 static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void Smt2Printer::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types) const throw() {
+                           int toDepth, bool types, size_t dag) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
+  expr::ExprDag::Scope dagScope(out, dag);
 
   if(tryToStream<AssertCommand>(out, c) ||
      tryToStream<PushCommand>(out, c) ||
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index a48104e45..fd65a1efa 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -30,9 +30,10 @@ namespace printer {
 namespace smt2 {
 
 class Smt2Printer : public CVC4::Printer {
-public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+public:
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class Smt2Printer */