diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/Makefile.am | 1 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.cpp | 47 | ||||
-rw-r--r-- | src/printer/ast/ast_printer.h | 5 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 36 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.h | 9 | ||||
-rw-r--r-- | src/printer/dagification_visitor.h | 180 | ||||
-rw-r--r-- | src/printer/printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 8 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 53 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 5 |
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 */ |