3 files changed, 32 insertions, 32 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index bbeee4f7f..1a85f45c3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1057,7 +1057,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
   std::string id;
   std::vector<Type> types;
   std::vector< std::pair<std::string, Type> > typeIds;
-  DeclarationScope* declScope;
+  //SymbolTable* symtab;
   Parser* parser;
   lhs = false;
 }
@@ -1097,11 +1097,11 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
      * declared in the outer context.  What follows isn't quite right,
      * though, since type aliases and function definitions should be
      * retained in the set of current declarations. */
-    { /*declScope = PARSER_STATE->getDeclarationScope();
-      PARSER_STATE->useDeclarationsFrom(new DeclarationScope());*/ }
+    { /*symtab = PARSER_STATE->getSymbolTable();
+      PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ }
     formula[f] ( COMMA formula[f2] )? RPAREN
-    { /*DeclarationScope* old = PARSER_STATE->getDeclarationScope();
-      PARSER_STATE->useDeclarationsFrom(declScope);
+    { /*SymbolTable* old = PARSER_STATE->getSymbolTable();
+      PARSER_STATE->useDeclarationsFrom(symtab);
       delete old;*/
       t = f2.isNull() ?
         EXPR_MANAGER->mkPredicateSubtype(f) :
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 44148a7f1..29db640c7 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -43,8 +43,8 @@ namespace parser {
 Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   d_exprManager(exprManager),
   d_input(input),
-  d_declScopeAllocated(),
-  d_declScope(&d_declScopeAllocated),
+  d_symtabAllocated(),
+  d_symtab(&d_symtabAllocated),
   d_anonymousFunctionCount(0),
   d_done(false),
   d_checksEnabled(true),
@@ -60,7 +60,7 @@ Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
-    return d_declScope->lookup(name);
+    return d_symtab->lookup(name);
 
   default:
     Unhandled(type);
@@ -87,7 +87,7 @@ Type Parser::getType(const std::string& var_name,
 Type Parser::getSort(const std::string& name) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope->lookupType(name);
+  Type t = d_symtab->lookupType(name);
   return t;
 }
 
@@ -95,14 +95,14 @@ Type Parser::getSort(const std::string& name,
                      const std::vector<Type>& params) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(name, SYM_SORT) );
-  Type t = d_declScope->lookupType(name, params);
+  Type t = d_symtab->lookupType(name, params);
   return t;
 }
 
 size_t Parser::getArity(const std::string& sort_name){
   checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
   Assert( isDeclared(sort_name, SYM_SORT) );
-  return d_declScope->lookupArity(sort_name);
+  return d_symtab->lookupArity(sort_name);
 }
 
 /* Returns true if name is bound to a boolean variable. */
@@ -125,14 +125,14 @@ bool Parser::isFunctionLike(const std::string& name) {
 bool Parser::isDefinedFunction(const std::string& name) {
   // more permissive in type than isFunction(), because defined
   // functions can be zero-ary and declared functions cannot.
-  return d_declScope->isBoundDefinedFunction(name);
+  return d_symtab->isBoundDefinedFunction(name);
 }
 
 /* Returns true if the Expr is a defined function. */
 bool Parser::isDefinedFunction(Expr func) {
   // more permissive in type than isFunction(), because defined
   // functions can be zero-ary and declared functions cannot.
-  return d_declScope->isBoundDefinedFunction(func);
+  return d_symtab->isBoundDefinedFunction(func);
 }
 
 /* Returns true if name is bound to a function returning boolean. */
@@ -179,20 +179,20 @@ Parser::mkVars(const std::vector<std::string> names,
 void
 Parser::defineVar(const std::string& name, const Expr& val,
                        bool levelZero) {
-  d_declScope->bind(name, val, levelZero);
+  d_symtab->bind(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineFunction(const std::string& name, const Expr& val,
                        bool levelZero) {
-  d_declScope->bindDefinedFunction(name, val, levelZero);
+  d_symtab->bindDefinedFunction(name, val, levelZero);
   Assert( isDeclared(name) );
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  d_declScope->bindType(name, type);
+  d_symtab->bindType(name, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -200,7 +200,7 @@ void
 Parser::defineType(const std::string& name,
                    const std::vector<Type>& params,
                    const Type& type) {
-  d_declScope->bindType(name, params, type);
+  d_symtab->bindType(name, params, type);
   Assert( isDeclared(name, SYM_SORT) );
 }
 
@@ -369,9 +369,9 @@ DatatypeType Parser::mkTupleType(const std::vector<Type>& types) {
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_declScope->isBound(name);
+    return d_symtab->isBound(name);
   case SYM_SORT:
-    return d_declScope->isBoundType(name);
+    return d_symtab->isBoundType(name);
   default:
     Unhandled(type);
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 635dd6b6c..f3210ae29 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -28,7 +28,7 @@
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "expr/expr.h"
-#include "expr/declaration_scope.h"
+#include "expr/symbol_table.h"
 #include "expr/kind.h"
 #include "expr/expr_stream.h"
 
@@ -117,15 +117,15 @@ class CVC4_PUBLIC Parser {
    * The declaration scope that is "owned" by this parser.  May or
    * may not be the current declaration scope in use.
    */
-  DeclarationScope d_declScopeAllocated;
+  SymbolTable d_symtabAllocated;
 
   /**
    * This current symbol table used by this parser.  Initially points
-   * to d_declScopeAllocated, but can be changed (making this parser
+   * to d_symtabAllocated, but can be changed (making this parser
    * delegate its definitions and lookups to another parser).
    * See useDeclarationsFrom().
    */
-  DeclarationScope* d_declScope;
+  SymbolTable* d_symtab;
 
   /** How many anonymous functions we've created. */
   size_t d_anonymousFunctionCount;
@@ -493,8 +493,8 @@ public:
     }
   }
 
-  inline void pushScope() { d_declScope->pushScope(); }
-  inline void popScope() { d_declScope->popScope(); }
+  inline void pushScope() { d_symtab->pushScope(); }
+  inline void popScope() { d_symtab->popScope(); }
 
   /**
    * Set the current symbol table used by this parser.
@@ -523,25 +523,25 @@ public:
    */
   inline void useDeclarationsFrom(Parser* parser) {
     if(parser == NULL) {
-      d_declScope = &d_declScopeAllocated;
+      d_symtab = &d_symtabAllocated;
     } else {
-      d_declScope = parser->d_declScope;
+      d_symtab = parser->d_symtab;
     }
   }
 
-  inline void useDeclarationsFrom(DeclarationScope* scope) {
-    d_declScope = scope;
+  inline void useDeclarationsFrom(SymbolTable* symtab) {
+    d_symtab = symtab;
   }
 
-  inline DeclarationScope* getDeclarationScope() const {
-    return d_declScope;
+  inline SymbolTable* getSymbolTable() const {
+    return d_symtab;
   }
 
   /**
    * Gets the current declaration level.
    */
   inline size_t getDeclarationLevel() const throw() {
-    return d_declScope->getLevel();
+    return d_symtab->getLevel();
   }
 
   /**