From: Morgan Deters Date: Wed, 19 Jun 2013 15:09:49 +0000 (-0400) Subject: Give a more useful parse error message for "undeclared variable -1". X-Git-Tag: cvc5-1.0.0~7287^2~95 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=010ad47b7b3e1909f31525fc45be2c27c1b72e45;p=cvc5.git Give a more useful parse error message for "undeclared variable -1". Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus. --- diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index fa2a1e744..a7834a5aa 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -374,7 +374,8 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) { void Parser::checkDeclaration(const std::string& varName, DeclarationCheck check, - SymbolType type) + SymbolType type, + std::string notes) throw(ParserException) { if(!d_checksEnabled) { return; @@ -384,14 +385,16 @@ void Parser::checkDeclaration(const std::string& varName, case CHECK_DECLARED: if( !isDeclared(varName, type) ) { parseError("Symbol " + varName + " not declared as a " + - (type == SYM_VARIABLE ? "variable" : "type")); + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); } break; case CHECK_UNDECLARED: if( isDeclared(varName, type) ) { parseError("Symbol " + varName + " previously declared as a " + - (type == SYM_VARIABLE ? "variable" : "type")); + (type == SYM_VARIABLE ? "variable" : "type") + + (notes.size() == 0 ? notes : "\n" + notes)); } break; diff --git a/src/parser/parser.h b/src/parser/parser.h index b4e79b427..883f1f12b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -312,7 +312,8 @@ public: * @throws ParserException if checks are enabled and the check fails */ void checkDeclaration(const std::string& name, DeclarationCheck check, - SymbolType type = SYM_VARIABLE) throw(ParserException); + SymbolType type = SYM_VARIABLE, + std::string notes = "") throw(ParserException); /** * Reserve a symbol at the assertion level. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c50a0972b..3f1d3b087 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -97,6 +97,30 @@ public: return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1)))); } + /** + * Smt2 parser provides its own checkDeclaration, which does the + * same as the base, but with some more helpful errors. + */ + void checkDeclaration(const std::string& name, DeclarationCheck check, + SymbolType type = SYM_VARIABLE, + std::string notes = "") throw(ParserException) { + // 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; + } + + 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()); + } + private: void addArithmeticOperators();