diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-09 00:35:38 +0000 |
commit | 700689a4e4ed42b5198816611eac5bcc1278284d (patch) | |
tree | 0d6029f9bc4f46a721930a27a47ac487771c452e /src/printer/ast | |
parent | a0411d4baad389ce88d4bd26edc8ed811625887c (diff) |
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.
Diffstat (limited to 'src/printer/ast')
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 47 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 5 |
2 files changed, 44 insertions, 8 deletions
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 */ |