summaryrefslogtreecommitdiff
path: root/src/parser/parser.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r--src/parser/parser.cpp7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 198d1cc31..1c275add7 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -357,7 +357,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
bool Parser::isDeclared(const std::string& name, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
- return d_symtab->isBound(name);
+ return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
case SYM_SORT:
return d_symtab->isBoundType(name);
}
@@ -365,6 +365,11 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) {
return false;
}
+void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
+ checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE);
+ d_reservedSymbols.insert(varName);
+}
+
void Parser::checkDeclaration(const std::string& varName,
DeclarationCheck check,
SymbolType type)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback