diff options
Diffstat (limited to 'src/printer/smt2/smt2_printer.cpp')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 53 |
1 files changed, 46 insertions, 7 deletions
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) || |