diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 18:14:18 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-20 17:00:56 -0400 |
commit | 0e6d0a7bced1083db25a286b5ddfd79fba344639 (patch) | |
tree | a5d75edb81df8f6ce0c904b5cb20870faa6d3bc0 /src/parser/parser.h | |
parent | aef543d74c4fb23a86ad2986d67e7fc7f11d1feb (diff) |
Detect multiply-defined :named annotations and issue an error.
Thanks to David Cok for pointing out this issue.
Conflicts:
library_versions
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 49 |
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. * |