Fix printing of models of uninterpreted sorts (#3597)

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 223bd9af917e705d9bdc841a09cfe0f1a5498eb9..806569b08e30bcc345919aa61b8413aef13d3e92 100644 (file)
--- 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 << ")";
     }

diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index 626767f5f7e71d11712d345a314ccbc2cc24b600..8d1d4b987c7ea15d7f5058dc7e54335d5faf64ba 100644 (file)
--- 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 <sstream>
 #include <string>
 
 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 823bbb0bdda21ed09ac8e3430db02676fc332f32..9e3e04f0606bcb18c6619e274b03c476c34ab1de 100644 (file)
--- 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 (file)
index 0000000..efe68e9
--- /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)