From 0c661d41f7594ee3c761b173c1e709ce428ce89d Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 20 Mar 2013 13:09:18 -0400
Subject: Properly |quote| symbols in SMT-LIBv2 output.

---
 src/printer/smt2/smt2_printer.cpp | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'src/printer/smt2')

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;
     }
   }
-- 
cgit v1.2.3