diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-07 14:22:32 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-07 14:22:32 -0600 |
commit | b38ffa21717d220e98581854e2af1ee9d13ce5b7 (patch) | |
tree | ba873bed85e7a392f27dd3b250ec0447b37fa0bc | |
parent | 53dc40ec71344d6cc8df9f009cbbba4dbefccb64 (diff) |
Fix unary minus parse check (#3594)
-rw-r--r-- | src/parser/smt2/smt2.h | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index efdb0c70f..4f0935916 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -450,26 +450,21 @@ class Smt2 : public Parser { // if the symbol is something like "-1", we'll give the user a helpful // syntax hint. (-1 is a valid identifier in SMT-LIB, NOT unary minus.) - if( check != CHECK_DECLARED || - name[0] != '-' || - name.find_first_not_of("0123456789", 1) != std::string::npos ) { - this->Parser::checkDeclaration(name, check, type, notes); - return; - }else{ - //it is allowable in sygus - if (sygus_v1() && name[0] == '-') + if (name.length() > 1 && name[0] == '-' + && name.find_first_not_of("0123456789", 1) == std::string::npos) + { + if (sygus_v1()) { - //do not check anything + // "-1" is allowed in SyGuS version 1.0 return; } + std::stringstream ss; + ss << notes << "You may have intended to apply unary minus: `(- " + << name.substr(1) << ")'\n"; + this->Parser::checkDeclaration(name, check, type, ss.str()); + return; } - - std::stringstream ss; - ss << notes - << "You may have intended to apply unary minus: `(- " - << name.substr(1) - << ")'\n"; - this->Parser::checkDeclaration(name, check, type, ss.str()); + this->Parser::checkDeclaration(name, check, type, notes); } void checkOperator(Kind kind, unsigned numArgs) |