diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-19 11:09:49 -0400 |
commit | 010ad47b7b3e1909f31525fc45be2c27c1b72e45 (patch) | |
tree | b18bf9b0724c6418dc57bf0d15a9db351f6f252e /src/parser/smt2/smt2.h | |
parent | c5177b11ad8cc5287fa7a8e65f78d5f6cfe23ead (diff) |
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.
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 24 |
1 files changed, 24 insertions, 0 deletions
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(); |