diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-20 04:08:56 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-20 02:08:56 +0000 |
commit | a95980ecd80b971086c328c3e1bb731852890a07 (patch) | |
tree | 8b9be61587f4c29e24c9f15edb9f31f955c4aef9 /src/parser/parser.cpp | |
parent | 8bb85b0f1664f6d03bcbf3997533140204c29251 (diff) |
Add more getters for api::Term (#6496)
This PR adds more getter functions for api::Term to retrieve values from constant terms (and terms that the average API use might consider constant).
It also introduces std::wstring as regular representation for string constants instead of std::vector<uint32> for the SMT-LIB parser and the String class.
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 43 |
1 files changed, 26 insertions, 17 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f3a0d5c83..d57ec0c9a 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -741,7 +741,7 @@ void Parser::reset() {} SymbolManager* Parser::getSymbolManager() { return d_symman; } -std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) +std::wstring Parser::processAdHocStringEsc(const std::string& s) { std::wstring ws; { @@ -763,7 +763,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) } } - std::vector<unsigned> str; + std::wstring res; unsigned i = 0; while (i < ws.size()) { @@ -771,7 +771,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) if (ws[i] != '\\') { // don't worry about printable here - str.push_back(static_cast<unsigned>(ws[i])); + res.push_back(ws[i]); ++i; continue; } @@ -789,49 +789,49 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) { case 'n': { - str.push_back(static_cast<unsigned>('\n')); + res.push_back('\n'); i++; } break; case 't': { - str.push_back(static_cast<unsigned>('\t')); + res.push_back('\t'); i++; } break; case 'v': { - str.push_back(static_cast<unsigned>('\v')); + res.push_back('\v'); i++; } break; case 'b': { - str.push_back(static_cast<unsigned>('\b')); + res.push_back('\b'); i++; } break; case 'r': { - str.push_back(static_cast<unsigned>('\r')); + res.push_back('\r'); i++; } break; case 'f': { - str.push_back(static_cast<unsigned>('\f')); + res.push_back('\f'); i++; } break; case 'a': { - str.push_back(static_cast<unsigned>('\a')); + res.push_back('\a'); i++; } break; case '\\': { - str.push_back(static_cast<unsigned>('\\')); + res.push_back('\\'); i++; } break; @@ -846,7 +846,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) shex << ws[i + 1] << ws[i + 2]; unsigned val; shex >> std::hex >> val; - str.push_back(val); + res.push_back(val); i += 3; isValid = true; } @@ -875,25 +875,25 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) && ws[i + 2] < '8') { num = num * 8 + static_cast<unsigned>(ws[i + 2]) - 48; - str.push_back(num); + res.push_back(num); i += 3; } else { - str.push_back(num); + res.push_back(num); i += 2; } } else { - str.push_back(num); + res.push_back(num); i++; } } } } } - return str; + return res; } api::Term Parser::mkStringConstant(const std::string& s) @@ -903,9 +903,18 @@ api::Term Parser::mkStringConstant(const std::string& s) return d_solver->mkString(s, true); } // otherwise, we must process ad-hoc escape sequences - std::vector<unsigned> str = processAdHocStringEsc(s); + std::wstring str = processAdHocStringEsc(s); return d_solver->mkString(str); } +api::Term Parser::mkCharConstant(const std::string& s) +{ + Assert(s.find_first_not_of("0123456789abcdefABCDEF", 0) == std::string::npos + && s.size() <= 5 && s.size() > 0) + << "Unexpected string for hexadecimal character " << s; + wchar_t val = static_cast<wchar_t>(std::stoul(s, 0, 16)); + return d_solver->mkString(std::wstring(1, val)); +} + } // namespace parser } // namespace cvc5 |