diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-04-06 22:06:52 +0000 |
commit | 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 (patch) | |
tree | ea510f4987dadcdbbb361684445419e4939cdf00 /src/printer | |
parent | 6a5fb6d945b109921cb9b6117f4ede0b6d110c08 (diff) |
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 40 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 31 |
3 files changed, 64 insertions, 9 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 04690f500..a3d15f822 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -173,6 +173,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo toStream(out, n[1], depth, types, true); out << " ELSE "; toStream(out, n[2], depth, types, true); + out << " ENDIF"; return; break; case kind::TUPLE_TYPE: @@ -237,18 +238,18 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo if (n.getNumChildren() > 2) { out << '('; } - for (unsigned i = 0; i < n.getNumChildren(); ++ i) { - if (i > 0) { + for (unsigned i = 1; i < n.getNumChildren(); ++i) { + if (i > 1) { out << ", "; } - toStream(out, n[i], depth, types, false); + toStream(out, n[i - 1], depth, types, false); } if (n.getNumChildren() > 2) { out << ')'; } } out << " -> "; - toStream(out, n[n.getNumChildren()-1], depth, types, false); + toStream(out, n[n.getNumChildren() - 1], depth, types, false); return; break; @@ -630,6 +631,29 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ +static void toStream(std::ostream& out, const SExpr& sexpr) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << sexpr.getRationalValue(); + } else if(sexpr.isString()) { + string s = sexpr.getValue(); + // escape backslash and quote + for(string::iterator i = s.begin(); i != s.end(); ++i) { + if(*i == '"') { + s.replace(i, i + 1, "\\\""); + ++i; + } else if(*i == '\\') { + s.replace(i, i + 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + out << sexpr; + } +} + static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } @@ -756,7 +780,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "% (set-info " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { @@ -764,7 +790,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { } static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { - out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "% (set-option " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index 2ac514988..e6490de63 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -45,7 +45,7 @@ void SmtPrinter::toStream(std::ostream& out, const Command* c, void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { s->toStream(out, language::output::LANG_SMTLIB_V2); -} +}/* SmtPrinter::toStream() */ }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 691e96ed7..218654a19 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -427,6 +427,29 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, }/* Smt2Printer::toStream(Command*) */ +static void toStream(std::ostream& out, const SExpr& sexpr) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << sexpr.getRationalValue(); + } else if(sexpr.isString()) { + string s = sexpr.getValue(); + // escape backslash and quote + for(size_t i = 0; i < s.length(); ++i) { + if(s[i] == '"') { + s.replace(i, 1, "\\\""); + ++i; + } else if(s[i] == '\\') { + s.replace(i, 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + out << sexpr; + } +} + template <class T> static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); @@ -576,7 +599,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "(set-info " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { @@ -584,7 +609,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { } static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { - out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "(set-option " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { |