diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-17 22:07:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-17 22:07:59 +0000 |
commit | 4923b53ad705acc04348da693f03f83f8d9853db (patch) | |
tree | b557cb22ce1f21bcbcca9d6ebdcbf205e5537b58 /src/printer | |
parent | 2b83291d229c957e2becf7397d186040959602df (diff) |
SMT-LIBv2 compliance updates:
* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
(there were some minor differences from the spec)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 27 | ||||
-rw-r--r-- | src/printer/printer.cpp | 40 | ||||
-rw-r--r-- | src/printer/printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 1 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 32 |
6 files changed, 60 insertions, 48 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e4a25e008..664ea58fc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -709,6 +709,10 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, }/* CvcPrinter::toStream(Command*) */ +static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { + Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr); +} + template <class T> static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); @@ -725,29 +729,6 @@ 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(size_t i = 0; i < s.size(); ++i) { - if(s[i] == '"') { - s.replace(i, 1, "\\\""); - ++i; - } else if(s[i] == '\\') { - s.replace(i, 1, "\\\\"); - ++i; - } - } - out << "\"" << s << "\""; - } else { - out << sexpr; - } -} - static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5229400b5..0881b814b 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -25,6 +25,10 @@ #include "printer/cvc/cvc_printer.h" #include "printer/ast/ast_printer.h" +#include <string> + +using namespace std; + namespace CVC4 { Printer* Printer::d_printers[language::output::LANG_MAX]; @@ -87,4 +91,40 @@ void Printer::toStream(std::ostream& out, const Result& r) const throw() { } }/* Printer::toStream() */ +void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << sexpr.getRationalValue(); + } else if(sexpr.isKeyword()) { + out << sexpr.getValue(); + } 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 << '('; + const vector<SExpr>& kids = sexpr.getChildren(); + bool first = true; + for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) { + if(first) { + first = false; + } else { + out << ' '; + } + out << *i; + } + out << ')'; + } +}/* Printer::toStream() */ + }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 8d1931a83..e3b1d6f40 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -22,6 +22,7 @@ #define __CVC4__PRINTER__PRINTER_H #include "util/language.h" +#include "util/sexpr.h" #include "expr/node.h" #include "expr/command.h" @@ -62,6 +63,9 @@ public: /** Write a CommandStatus out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; + /** Write an SExpr out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const SExpr& sexpr) const throw(); + /** * Write a Result out to a stream with this Printer. * diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index f74a1e07d..fa46523a4 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -47,6 +47,10 @@ void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw s->toStream(out, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() { + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); +}/* SmtPrinter::toStream() */ + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 612dfd19e..6e1c607bf 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -34,6 +34,7 @@ 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(); + void toStream(std::ostream& out, const SExpr& sexpr) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 640f4209c..a3b22ac24 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -27,6 +27,7 @@ #include "printer/dagification_visitor.h" #include "util/node_visitor.h" #include "theory/substitutions.h" +#include "util/language.h" using namespace std; @@ -503,27 +504,8 @@ 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; - } +static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { + Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); } template <class T> @@ -679,23 +661,23 @@ 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() << " "; + out << "(set-info :" << c->getFlag() << " "; toStream(out, c->getSExpr()); out << ")"; } static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { - out << "(get-info " << c->getFlag() << ")"; + out << "(get-info :" << c->getFlag() << ")"; } static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { - out << "(set-option " << c->getFlag() << " "; + out << "(set-option :" << c->getFlag() << " "; toStream(out, c->getSExpr()); out << ")"; } static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { - out << "(get-option " << c->getFlag() << ")"; + out << "(get-option :" << c->getFlag() << ")"; } static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { |