diff options
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 40 |
1 files changed, 34 insertions, 6 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() { |