From 010ad47b7b3e1909f31525fc45be2c27c1b72e45 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Jun 2013 11:09:49 -0400
Subject: [PATCH] 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.
---
 src/parser/parser.cpp  |  9 ++++++---
 src/parser/parser.h    |  3 ++-
 src/parser/smt2/smt2.h | 24 ++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 4 deletions(-)

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();
-- 
2.30.2