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/printer.cpp | |
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/printer.cpp')
-rw-r--r-- | src/printer/printer.cpp | 40 |
1 files changed, 40 insertions, 0 deletions
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 */ |