From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 20 Mar 2013 17:09:18 +0000 (-0400)
Subject: Properly |quote| symbols in SMT-LIBv2 output.
X-Git-Tag: cvc5-1.0.0~7383
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c661d41f7594ee3c761b173c1e709ce428ce89d;p=cvc5.git

Properly |quote| symbols in SMT-LIBv2 output.
---

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8541ca6ae..ef4fd5fea 100644
--- 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 cc385327e..3a13d8dba 100644
--- 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
index 000000000..26050d931
--- /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: )