From b38ffa21717d220e98581854e2af1ee9d13ce5b7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Jan 2020 14:22:32 -0600 Subject: [PATCH] Fix unary minus parse check (#3594) --- src/parser/smt2/smt2.h | 27 +++++++++++---------------- 1 file 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) -- 2.30.2