From 28ea853b689ce762b6450023added88e6b4b5400 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 10 Jan 2020 10:49:53 -0800 Subject: Fix printing of models of uninterpreted sorts (#3597) --- src/printer/smt2/smt2_printer.cpp | 36 ++++++++------------------- src/util/smt2_quote_string.cpp | 13 +++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress0/printer/empty_sort.smt2 | 9 +++++++ 4 files changed, 29 insertions(+), 30 deletions(-) create mode 100644 test/regress/regress0/printer/empty_sort.smt2 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().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(); 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 << ")"; } diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index 626767f5f..8d1d4b987 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -16,6 +16,7 @@ #include "util/smt2_quote_string.h" +#include #include namespace CVC4 { @@ -24,10 +25,13 @@ namespace CVC4 { * SMT-LIB 2 quoting for symbols */ std::string quoteSymbol(const std::string& s){ - if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) { - // simple unquoted symbol - return s; - } else { + // this is the set of SMT-LIBv2 permitted characters in "simple" (non-quoted) + // symbols + if (s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz" + "0123456789~!@$%^&*_-+=<>.?/") + != std::string::npos + || s.empty() || (s[0] >= '0' && s[0] <= '9')) + { std::string tmp(s); // must quote the symbol, but it cannot contain | or \, we turn those into _ size_t p; @@ -36,6 +40,7 @@ std::string quoteSymbol(const std::string& s){ } return "|" + tmp + "|"; } + return s; } }/* CVC4 namespace */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 823bbb0bd..9e3e04f06 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -621,6 +621,7 @@ set(regress_0_tests regress0/print_lambda.cvc regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 + regress0/printer/empty_sort.smt2 regress0/printer/empty_symbol_name.smt2 regress0/printer/let_shadowing.smt2 regress0/printer/symbol_starting_w_digit.smt2 diff --git a/test/regress/regress0/printer/empty_sort.smt2 b/test/regress/regress0/printer/empty_sort.smt2 new file mode 100644 index 000000000..efe68e920 --- /dev/null +++ b/test/regress/regress0/printer/empty_sort.smt2 @@ -0,0 +1,9 @@ +; EXPECT: (declare-fun gt () us_image) +; EXPECT: (declare-fun gt () ||) +; SCRUBBER: sed -e '/declare-fun/!d; s/declare-fun [^[:space:]]*/declare-fun gt/g' +(set-option :produce-models true) +(set-logic QF_UF) +(declare-sort us_image 0) +(declare-sort || 0) +(check-sat) +(get-model) -- cgit v1.2.3