Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
	library_versions

1 files changed, 40 insertions, 9 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0761b4cda..4f943a0b5 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -126,6 +126,23 @@ class CVC4_PUBLIC Parser {
    */
   SymbolTable* d_symtab;
 
+  /**
+   * The level of the assertions in the declaration scope.  Things declared
+   * after this level are bindings from e.g. a let, a quantifier, or a
+   * lambda.
+   */
+  size_t d_assertionLevel;
+
+  /**
+   * Maintains a list of reserved symbols at the assertion level that might
+   * not occur in our symbol table.  This is necessary to e.g. support the
+   * proper behavior of the :named annotation in SMT-LIBv2 when used under
+   * a let or a quantifier, since inside a let/quant body the declaration
+   * scope is that of the let/quant body, but the defined name should be
+   * reserved at the assertion level.
+   */
+  std::set<std::string> d_reservedSymbols;
+
   /** How many anonymous functions we've created. */
   size_t d_anonymousFunctionCount;
 
@@ -288,6 +305,11 @@ public:
                         SymbolType type = SYM_VARIABLE) throw(ParserException);
 
   /**
+   * Reserve a symbol at the assertion level.
+   */
+  void reserveSymbolAtAssertionLevel(const std::string& name);
+
+  /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
    * @throws ParserException if checks are enabled and name is not
@@ -487,9 +509,25 @@ public:
     }
   }
 
+  /**
+   * Gets the current declaration level.
+   */
   inline size_t scopeLevel() const { return d_symtab->getLevel(); }
-  inline void pushScope() { d_symtab->pushScope(); }
-  inline void popScope() { d_symtab->popScope(); }
+
+  inline void pushScope(bool bindingLevel = false) {
+    d_symtab->pushScope();
+    if(!bindingLevel) {
+      d_assertionLevel = scopeLevel();
+    }
+  }
+
+  inline void popScope() {
+    d_symtab->popScope();
+    if(scopeLevel() < d_assertionLevel) {
+      d_assertionLevel = scopeLevel();
+      d_reservedSymbols.clear();
+    }
+  }
 
   /**
    * Set the current symbol table used by this parser.
@@ -533,13 +571,6 @@ public:
   }
 
   /**
-   * Gets the current declaration level.
-   */
-  inline size_t getDeclarationLevel() const throw() {
-    return d_symtab->getLevel();
-  }
-
-  /**
    * An expression stream interface for a parser.  This stream simply
    * pulls expressions from the given Parser object.
    *