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.

1 files changed, 4 insertions, 4 deletions

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() {