diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/smt2_quote_string.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
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 <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 */ |