diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-08 17:23:32 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-08 17:23:32 -0500 |
| commit | 3162008b628174bd8bce70b336ce928e88ae07c6 (patch) | |
| tree | c1b6af2eff264ad72a0d8fbbe585822b02917cf4 /src/parser/smt1/Smt1.g | |
| parent | 4908c52200a80a848dc529cc312aa5418f6d3dee (diff) | |
Fix user-values in SMT-LIB v1.2
Diffstat (limited to 'src/parser/smt1/Smt1.g')
| -rw-r--r-- | src/parser/smt1/Smt1.g | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index 0f76baace..e3c36cf91 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -783,7 +783,15 @@ FLET_IDENTIFIER */ userValue[std::string& s] : USER_VALUE - { s = AntlrInput::tokenText($USER_VALUE); } + { s = AntlrInput::tokenText($USER_VALUE); + assert(*s.begin() == '{'); + assert(*s.rbegin() == '}'); + // trim whitespace + s.erase(s.begin(), s.begin() + 1); + s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace)))); + s.erase(s.end() - 1); + s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end()); + } ; PATTERN_ANNOTATION_BEGIN |