From 5ca5dd42d95ce08a4ea456212fffcd2672e31fc1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 19 Mar 2014 13:58:59 -0400 Subject: [PATCH] Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting. --- src/printer/smt2/smt2_printer.cpp | 19 +++++++++++++++++++ src/printer/smt2/smt2_printer.h | 1 + 2 files changed, 20 insertions(+) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 849d5c0a5..6485670b5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -697,6 +697,25 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() { Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr); } +void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() { + if(sexpr.isKeyword()) { + std::string s = sexpr.getValue(); + if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@%^&*_-+=<>.?/") == std::string::npos) { + // simple unquoted symbol + out << s; + } else { + // must quote the symbol, but it cannot contain | or \, we turn those into _ + size_t p; + while((p = s.find_first_of("\\|")) != std::string::npos) { + s = s.replace(p, 1, "_"); + } + out << "|" << s << "|"; + } + } else { + this->Printer::toStream(out, sexpr); + } +} + template static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index c70bb78c3..c3f8deb9c 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -45,6 +45,7 @@ public: 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 Result& r) const throw(); + void toStream(std::ostream& out, const SExpr& sexpr) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ -- 2.30.2