diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-10 10:49:53 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-10 12:49:53 -0600 |
commit | 28ea853b689ce762b6450023added88e6b4b5400 (patch) | |
tree | 697341e3d32608d2db5df28214904d9177c151d3 /src/util | |
parent | 3848242e33130ba507cbfcd5d8296cdeaa3dfa35 (diff) |
Fix printing of models of uninterpreted sorts (#3597)
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 */ |