Properly |quote| symbols in SMT-LIBv2 output.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8541ca6aef67ba09b68e4bf614f34b4e7b58eba8..ef4fd5fea544e992c0445363498d374da0c69d44 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -74,6 +74,17 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   }
 }
 
+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("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") != string::npos) {
+    // need to quote it
+    stringstream ss;
+    ss << '|' << s << '|';
+    return ss.str();
+  }
+  return s;
+}
+
 void Smt2Printer::toStream(std::ostream& out, TNode n,
                            int toDepth, bool types) const throw() {
   // null
@@ -86,7 +97,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if(n.isVar()) {
     string s;
     if(n.getAttribute(expr::VarNameAttr(), s)) {
-      out << s;
+      out << maybeQuoteSymbol(s);
     } else {
       if(n.getKind() == kind::VARIABLE) {
         out << "var_";
@@ -175,7 +186,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
 
     case kind::DATATYPE_TYPE:
-      out << n.getConst<Datatype>().getName();
+      out << maybeQuoteSymbol(n.getConst<Datatype>().getName());
       break;
 
     case kind::UNINTERPRETED_CONSTANT: {
@@ -196,7 +207,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   if(n.getKind() == kind::SORT_TYPE) {
     string name;
     if(n.getAttribute(expr::VarNameAttr(), name)) {
-      out << name;
+      out << maybeQuoteSymbol(name);
       return;
     }
   }

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index cc385327e7ef9b229c37d77e722af123332dc24c..3a13d8dba6c4e26522367bce92912689b532a949 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -113,6 +113,7 @@ TPTP_TESTS = \
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
+       smt2output.smt2 \
        bug32.cvc \
        bug49.smt \
        bug161.smt \

diff --git a/test/regress/regress0/smt2output.smt2 b/test/regress/regress0/smt2output.smt2
new file mode 100644 (file)
index 0000000..26050d9
--- /dev/null
+++ b/test/regress/regress0/smt2output.smt2
@@ -0,0 +1,15 @@
+; This test checks the correct output behavior of SMT-LIBv2 symbols
+; (sometimes they have to be |quoted| with pipes).
+;
+; COMMAND-LINE: -qm
+; EXIT: 10
+(declare-fun |toto| () Bool)
+(declare-fun |to to| () Bool)
+(assert (and toto |to to|))
+(check-sat)
+; EXPECT: sat
+(get-model)
+; EXPECT: (model
+; EXPECT: (define-fun toto () Bool true)
+; EXPECT: (define-fun |to to| () Bool true)
+; EXPECT: )