diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-10 10:49:53 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-10 12:49:53 -0600 |
commit | 28ea853b689ce762b6450023added88e6b4b5400 (patch) | |
tree | 697341e3d32608d2db5df28214904d9177c151d3 /src/printer | |
parent | 3848242e33130ba507cbfcd5d8296cdeaa3dfa35 (diff) |
Fix printing of models of uninterpreted sorts (#3597)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 36 |
1 files changed, 10 insertions, 26 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 223bd9af9..806569b08 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -91,21 +91,6 @@ void Smt2Printer::toStream( } } -static std::string maybeQuoteSymbol(const std::string& s) { - // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) symbols - if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz" - "0123456789~!@$%^&*_-+=<>.?/") - != string::npos - || s.empty() || (s[0] >= '0' && s[0] <= '9')) - { - // need to quote it - stringstream ss; - ss << '|' << s << '|'; - return ss.str(); - } - return s; -} - static bool stringifyRegexp(Node n, stringstream& ss) { if(n.getKind() == kind::STRING_TO_REGEXP) { ss << n[0].getConst<String>().toString(true); @@ -268,7 +253,7 @@ void Smt2Printer::toStream(std::ostream& out, } else { - out << maybeQuoteSymbol(dt.getName()); + out << CVC4::quoteSymbol(dt.getName()); } break; } @@ -277,7 +262,7 @@ void Smt2Printer::toStream(std::ostream& out, const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>(); std::stringstream ss; ss << '@' << uc; - out << maybeQuoteSymbol(ss.str()); + out << CVC4::quoteSymbol(ss.str()); break; } @@ -381,7 +366,7 @@ void Smt2Printer::toStream(std::ostream& out, out << '('; } if(n.getAttribute(expr::VarNameAttr(), name)) { - out << maybeQuoteSymbol(name); + out << CVC4::quoteSymbol(name); } if(n.getNumChildren() != 0) { for(unsigned i = 0; i < n.getNumChildren(); ++i) { @@ -446,7 +431,7 @@ void Smt2Printer::toStream(std::ostream& out, string s; if (n.getAttribute(expr::VarNameAttr(), s)) { - out << maybeQuoteSymbol(s); + out << CVC4::quoteSymbol(s); } else { @@ -1328,9 +1313,8 @@ void Smt2Printer::toStream(std::ostream& out, static std::string quoteSymbol(TNode n) { - // #warning "check the old implementation. It seems off." std::stringstream ss; - ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); + ss << n; return CVC4::quoteSymbol(ss.str()); } @@ -1361,7 +1345,7 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const std::string name; if (smt->getExpressionName(*i,name)) { // Named assertions always get printed - out << maybeQuoteSymbol(name) << endl; + out << CVC4::quoteSymbol(name) << endl; } else if (options::dumpUnsatCoresFull()) { // Unnamed assertions only get printed if the option is set out << *i << endl; @@ -1802,7 +1786,7 @@ static void toStreamRational(std::ostream& out, static void toStream(std::ostream& out, const DeclareTypeCommand* c) { - out << "(declare-sort " << maybeQuoteSymbol(c->getSymbol()) << " " + out << "(declare-sort " << CVC4::quoteSymbol(c->getSymbol()) << " " << c->getArity() << ")"; } @@ -1917,7 +1901,7 @@ static void toStream(std::ostream& out, const Datatype & d) { for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); ctor != ctor_end; ++ctor){ if( ctor!=d.begin() ) out << " "; - out << "(" << maybeQuoteSymbol(ctor->getName()); + out << "(" << CVC4::quoteSymbol(ctor->getName()); for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); arg != arg_end; ++arg){ @@ -1955,7 +1939,7 @@ static void toStream(std::ostream& out, ++i) { const Datatype& d = i->getDatatype(); - out << "(" << maybeQuoteSymbol(d.getName()); + out << "(" << CVC4::quoteSymbol(d.getName()); out << " " << d.getNumParameters() << ")"; } out << ") ("; @@ -2039,7 +2023,7 @@ static void toStream(std::ostream& out, ++i) { const Datatype& d = i->getDatatype(); - out << "(" << maybeQuoteSymbol(d.getName()) << " "; + out << "(" << CVC4::quoteSymbol(d.getName()) << " "; toStream(out, d); out << ")"; } |