Refactor handling of global declarations (#5577)

This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.

This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.

This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.

This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.

15 files changed, 63 insertions, 192 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index ef85dd1a9..46e88af8f 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -20,7 +20,6 @@
 #include <limits.h>
 
 #include "base/output.h"
-#include "expr/type.h"
 #include "parser/antlr_line_buffered_input.h"
 #include "parser/bounded_token_buffer.h"
 #include "parser/bounded_token_factory.h"
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index f174ed470..8831bfb7a 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -565,13 +565,9 @@ namespace CVC4 {
 #include <vector>
 
 #include "base/output.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 
-
 #define REPEAT_COMMAND(k, CommandCtor)                      \
   ({                                                        \
     unsigned __k = (k);                                     \
@@ -742,13 +738,15 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     { UNSUPPORTED("POPTO_SCOPE command"); }
 
   | RESET_TOK
-    { cmd->reset(new ResetCommand());
+    {
+      cmd->reset(new ResetCommand());
+      // reset the state of the parser, which is independent of the symbol
+      // manager
       PARSER_STATE->reset();
     }
 
   | RESET_TOK ASSERTIONS_TOK
     { cmd->reset(new ResetAssertionsCommand());
-      PARSER_STATE->reset();
     }
 
     // Datatypes can be mututally-recursive if they're in the same
@@ -889,7 +887,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
       idCommaFlag=true;
       })?
     {
-      func = PARSER_STATE->bindVar(id, t, ExprManager::VAR_FLAG_NONE, true);
+      func = PARSER_STATE->bindVar(id, t, false, true);
       ids.push_back(id);
       types.push_back(t);
       funcs.push_back(func);
@@ -1117,8 +1115,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
           } else {
             Debug("parser") << "  " << *i << " not declared" << std::endl;
             if(topLevel) {
-              api::Term func =
-                  PARSER_STATE->bindVar(*i, t, ExprManager::VAR_FLAG_GLOBAL);
+              api::Term func = PARSER_STATE->bindVar(*i, t);
               Command* decl = new DeclareFunctionCommand(*i, func, t);
               seq->addCommand(decl);
             } else {
@@ -1151,10 +1148,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
             ++i) {
           Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
-          api::Term func = PARSER_STATE->mkVar(
-              *i,
-              t,
-              ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
+          api::Term func = SOLVER->mkConst(t, *i);
           PARSER_STATE->defineVar(*i, fterm);
           Command* decl = new DefineFunctionCommand(*i, func, formals, f, true);
           seq->addCommand(decl);
@@ -2307,11 +2301,11 @@ datatypeDef[std::vector<CVC4::api::DatatypeDecl>& datatypes]
      * below. */
   : identifier[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
     ( LBRACKET identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
+        t = PARSER_STATE->mkSort(id2);
         params.push_back( t );
       }
       ( COMMA identifier[id2,CHECK_UNDECLARED,SYM_SORT] {
-        t = PARSER_STATE->mkSort(id2, ExprManager::SORT_FLAG_PLACEHOLDER);
+        t = PARSER_STATE->mkSort(id2);
         params.push_back( t ); }
       )* RBRACKET
     )?
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 5e3510a4b..393e80e02 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -18,7 +18,6 @@
 
 #include <antlr3.h>
 
-#include "expr/expr_manager.h"
 #include "parser/antlr_input.h"
 #include "parser/parser_exception.h"
 #include "parser/cvc/CvcLexer.h"
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 603da0e31..038fc1ef5 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -20,7 +20,6 @@
 #include "parser/input.h"
 
 #include "base/output.h"
-#include "expr/type.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
 
diff --git a/src/parser/input.h b/src/parser/input.h
index 19fd4db72..c05384740 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -25,16 +25,12 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "options/language.h"
 #include "parser/parser_exception.h"
 
 namespace CVC4 {
 
 class Command;
-class Type;
-class FunctionType;
 
 namespace parser {
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1ca2e1c01..ab0571e53 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -25,9 +25,7 @@
 
 #include "api/cvc4cpp.h"
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/kind.h"
-#include "expr/type.h"
 #include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser_exception.h"
@@ -199,16 +197,13 @@ bool Parser::isPredicate(const std::string& name) {
 
 api::Term Parser::bindVar(const std::string& name,
                           const api::Sort& type,
-                          uint32_t flags,
+                          bool levelZero,
                           bool doOverload)
 {
-  if (d_symman->getGlobalDeclarations())
-  {
-    flags |= ExprManager::VAR_FLAG_GLOBAL;
-  }
+  bool globalDecls = d_symman->getGlobalDeclarations();
   Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
-  api::Term expr = mkVar(name, type, flags);
-  defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
+  api::Term expr = d_solver->mkConst(type, name);
+  defineVar(name, expr, globalDecls || levelZero, doOverload);
   return expr;
 }
 
@@ -217,7 +212,7 @@ api::Term Parser::bindBoundVar(const std::string& name, const api::Sort& type)
   Debug("parser") << "bindBoundVar(" << name << ", " << type << ")"
                   << std::endl;
   api::Term expr = d_solver->mkVar(type, name);
-  defineVar(name, expr, false);
+  defineVar(name, expr);
   return expr;
 }
 
@@ -232,33 +227,14 @@ std::vector<api::Term> Parser::bindBoundVars(
   return vars;
 }
 
-api::Term Parser::mkAnonymousFunction(const std::string& prefix,
-                                      const api::Sort& type,
-                                      uint32_t flags)
-{
-  bool globalDecls = d_symman->getGlobalDeclarations();
-  if (globalDecls)
-  {
-    flags |= ExprManager::VAR_FLAG_GLOBAL;
-  }
-  stringstream name;
-  name << prefix << "_anon_" << ++d_anonymousFunctionCount;
-  return mkVar(name.str(), type, flags);
-}
-
 std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
                                         const api::Sort& type,
-                                        uint32_t flags,
+                                        bool levelZero,
                                         bool doOverload)
 {
-  bool globalDecls = d_symman->getGlobalDeclarations();
-  if (globalDecls)
-  {
-    flags |= ExprManager::VAR_FLAG_GLOBAL;
-  }
   std::vector<api::Term> vars;
   for (unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(bindVar(names[i], type, flags, doOverload));
+    vars.push_back(bindVar(names[i], type, levelZero, doOverload));
   }
   return vars;
 }
@@ -330,34 +306,29 @@ void Parser::defineParameterizedType(const std::string& name,
   defineType(name, params, type);
 }
 
-api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
+api::Sort Parser::mkSort(const std::string& name)
 {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  api::Sort type = d_solver->mkUninterpretedSort(name);
   bool globalDecls = d_symman->getGlobalDeclarations();
-  defineType(
-      name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+  api::Sort type = d_solver->mkUninterpretedSort(name);
+  defineType(name, type, globalDecls);
   return type;
 }
 
-api::Sort Parser::mkSortConstructor(const std::string& name,
-                                    size_t arity,
-                                    uint32_t flags)
+api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity)
 {
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  api::Sort type = d_solver->mkSortConstructorSort(name, arity);
   bool globalDecls = d_symman->getGlobalDeclarations();
-  defineType(name,
-             vector<api::Sort>(arity),
-             type,
-             globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+  api::Sort type = d_solver->mkSortConstructorSort(name, arity);
+  defineType(name, vector<api::Sort>(arity), type, globalDecls);
   return type;
 }
 
 api::Sort Parser::mkUnresolvedType(const std::string& name)
 {
-  api::Sort unresolved = mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER);
+  api::Sort unresolved = d_solver->mkUninterpretedSort(name);
+  defineType(name, unresolved);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -365,8 +336,8 @@ api::Sort Parser::mkUnresolvedType(const std::string& name)
 api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name,
                                               size_t arity)
 {
-  api::Sort unresolved =
-      mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER);
+  api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity);
+  defineType(name, vector<api::Sort>(arity), unresolved);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
@@ -633,20 +604,9 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   return t;
 }
 
-//!!!!!!!!!!! temporary
-api::Term Parser::mkVar(const std::string& name,
-                        const api::Sort& type,
-                        uint32_t flags)
-{
-  return d_solver->mkConst(type, name);
-}
-//!!!!!!!!!!! temporary
-
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch (type) {
-    case SYM_VARIABLE:
-      return d_reservedSymbols.find(name) != d_reservedSymbols.end() ||
-             d_symtab->isBound(name);
+    case SYM_VARIABLE: return d_symtab->isBound(name);
     case SYM_SORT:
       return d_symtab->isBoundType(name);
   }
@@ -654,11 +614,6 @@ 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,
@@ -769,23 +724,14 @@ size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
 void Parser::pushScope(bool isUserContext)
 {
   d_symman->pushScope(isUserContext);
-  if (isUserContext)
-  {
-    d_assertionLevel = scopeLevel();
-  }
 }
 
 void Parser::popScope()
 {
   d_symman->popScope();
-  if (scopeLevel() < d_assertionLevel)
-  {
-    d_assertionLevel = scopeLevel();
-    d_reservedSymbols.clear();
-  }
 }
 
-void Parser::reset() { d_symman->reset(); }
+void Parser::reset() {}
 
 SymbolManager* Parser::getSymbolManager() { return d_symman; }
 
@@ -928,11 +874,11 @@ api::Term Parser::mkStringConstant(const std::string& s)
 {
   if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
   {
-    return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
+    return d_solver->mkString(s, true);
   }
   // otherwise, we must process ad-hoc escape sequences
   std::vector<unsigned> str = processAdHocStringEsc(s);
-  return api::Term(d_solver, d_solver->mkString(str).getExpr());
+  return d_solver->mkString(str);
 }
 
 } /* CVC4::parser namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 686a0d147..31c421e2c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -127,16 +127,6 @@ private:
   */
  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;
 
@@ -395,11 +385,6 @@ public:
                         std::string notes = "");
 
   /**
-   * Reserve a symbol at the assertion level.
-   */
-  void reserveSymbolAtAssertionLevel(const std::string& name);
-
-  /**
    * Checks whether the given expression is function-like, i.e.
    * it expects arguments. This is checked by looking at the type 
    * of fun. Examples of function types are function, constructor,
@@ -410,33 +395,35 @@ public:
    */
   void checkFunctionLike(api::Term fun);
 
-  /** Create a new CVC4 variable expression of the given type. 
+  /** Create a new CVC4 variable expression of the given type.
    *
-   * flags specify information about the variable, e.g. whether it is global or defined
-   *   (see enum in expr_manager_template.h).
+   * It is inserted at context level zero in the symbol table if levelZero is
+   * true, or if we are using global declarations.
    *
    * If a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *  else if doOverload is false, the existing expression is shadowed by the
+   * new expression.
    */
   api::Term bindVar(const std::string& name,
                     const api::Sort& type,
-                    uint32_t flags = ExprManager::VAR_FLAG_NONE,
+                    bool levelZero = false,
                     bool doOverload = false);
 
   /**
    * Create a set of new CVC4 variable expressions of the given type.
    *
-   * flags specify information about the variable, e.g. whether it is global or defined
-   *   (see enum in expr_manager_template.h).
+   * It is inserted at context level zero in the symbol table if levelZero is
+   * true, or if we are using global declarations.
    *
    * For each name, if a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *  else if doOverload is false, the existing expression is shadowed by the
+   * new expression.
    */
   std::vector<api::Term> bindVars(const std::vector<std::string> names,
                                   const api::Sort& type,
-                                  uint32_t flags = ExprManager::VAR_FLAG_NONE,
+                                  bool levelZero = false,
                                   bool doOverload = false);
 
   /**
@@ -455,9 +442,6 @@ public:
   /**
    * Create a set of new CVC4 bound variable expressions of the given type.
    *
-   * flags specify information about the variable, e.g. whether it is global or defined
-   *   (see enum in expr_manager_template.h).
-   *
    * For each name, if a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
    *  else if doOverload is false, the existing expression is shadowed by the new expression.
@@ -465,18 +449,6 @@ public:
   std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
                                        const api::Sort& type);
 
-  /**
-   * Create a new CVC4 function expression of the given type,
-   * appending a unique index to its name.  (That's the ONLY
-   * difference between mkAnonymousFunction() and mkVar()).
-   *
-   * flags specify information about the variable, e.g. whether it is global or defined
-   *   (see enum in expr_manager_template.h).
-   */
-  api::Term mkAnonymousFunction(const std::string& prefix,
-                                const api::Sort& type,
-                                uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
   /** Create a new variable definition (e.g., from a let binding). 
    * levelZero is set if the binding must be done at level 0.
    * If a symbol with name already exists,
@@ -526,15 +498,12 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  api::Sort mkSort(const std::string& name,
-                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  api::Sort mkSort(const std::string& name);
 
   /**
    * Creates a new sort constructor with the given name and arity.
    */
-  api::Sort mkSortConstructor(const std::string& name,
-                              size_t arity,
-                              uint32_t flags = ExprManager::SORT_FLAG_NONE);
+  api::Sort mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Creates a new "unresolved type," used only during parsing.
@@ -667,15 +636,6 @@ public:
    */
   api::Term applyTypeAscription(api::Term t, api::Sort s);
 
-  //!!!!!!!!!!! temporary
-  /**
-   * Make var, with flags required by the ExprManager, see ExprManager::mkVar.
-   */
-  api::Term mkVar(const std::string& name,
-                  const api::Sort& type,
-                  uint32_t flags);
-  //!!!!!!!!!!! temporary
-
   /**
    * Add an operator to the current legal set.
    *
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index b9d0cb415..e68ecfe71 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -23,7 +23,6 @@
 
 #include "api/cvc4cpp.h"
 #include "cvc/cvc.h"
-#include "expr/expr_manager.h"
 #include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6eb3d8061..11ccb4935 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -103,9 +103,6 @@ namespace CVC4 {
 
 #include "api/cvc4cpp.h"
 #include "base/output.h"
-#include "expr/expr.h"
-#include "expr/kind.h"
-#include "expr/type.h"
 #include "options/set_language.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -294,7 +291,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       else
       {
         api::Term func =
-            PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+            PARSER_STATE->bindVar(name, t, false, true);
         cmd->reset(new DeclareFunctionCommand(name, func, t));
       }
     }
@@ -333,8 +330,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       // must not be extended with the name itself; no recursion
       // permitted)
       // we allow overloading for function definitions
-      api::Term func = PARSER_STATE->bindVar(name, t,
-                                      ExprManager::VAR_FLAG_DEFINED, true);
+      api::Term func = PARSER_STATE->bindVar(name, t, false, true);
       cmd->reset(new DefineFunctionCommand(
           name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
     }
@@ -775,7 +771,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
     sortSymbol[t,CHECK_DECLARED]
     { // allow overloading here
       api::Term c =
-          PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+          PARSER_STATE->bindVar(name, t, false, true);
       cmd->reset(new DeclareFunctionCommand(name, c, t)); }
 
     /* get model */
@@ -792,14 +788,16 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
     /* reset: reset everything, returning solver to initial state.
      * Logic and options must be set again. */
   | RESET_TOK
-    { cmd->reset(new ResetCommand());
+    {
+      cmd->reset(new ResetCommand());
+      // reset the state of the parser, which is independent of the symbol
+      // manager
       PARSER_STATE->reset();
     }
     /* reset-assertions: reset assertions, assertion stack, declarations,
      * etc., but the logic and options remain as they were. */
   | RESET_ASSERTIONS_TOK
     { cmd->reset(new ResetAssertionsCommand());
-      PARSER_STATE->resetAssertions();
     }
   | DEFINE_FUN_REC_TOK
     { PARSER_STATE->checkThatLogicIsSet(); }
@@ -943,7 +941,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         }
         // allow overloading
         api::Term func =
-            PARSER_STATE->bindVar(name, tt, ExprManager::VAR_FLAG_NONE, true);
+            PARSER_STATE->bindVar(name, tt, false, true);
         seq->addCommand(new DeclareFunctionCommand(name, func, tt));
         sorts.clear();
       }
@@ -963,7 +961,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         }
         // allow overloading
         api::Term func =
-            PARSER_STATE->bindVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+            PARSER_STATE->bindVar(name, t, false, true);
         seq->addCommand(new DeclareFunctionCommand(name, func, t));
         sorts.clear();
       }
@@ -977,8 +975,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       { PARSER_STATE->checkUserSymbol(name); }
       term[e,e2]
       {
-        api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
-                                        ExprManager::VAR_FLAG_DEFINED);
+        api::Term func = PARSER_STATE->bindVar(name, e.getSort());
         cmd->reset(new DefineFunctionCommand(
             name, func, e, SYM_MAN->getGlobalDeclarations()));
       }
@@ -1008,8 +1005,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
           }
           tt = SOLVER->mkFunctionSort(sorts, tt);
         }
-        api::Term func = PARSER_STATE->bindVar(name, tt,
-                                        ExprManager::VAR_FLAG_DEFINED);
+        api::Term func = PARSER_STATE->bindVar(name, tt);
         cmd->reset(new DefineFunctionCommand(
             name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
       }
@@ -1030,8 +1026,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
       // permitted)
-      api::Term func = PARSER_STATE->bindVar(name, t,
-                                      ExprManager::VAR_FLAG_DEFINED);
+      api::Term func = PARSER_STATE->bindVar(name, t);
       cmd->reset(new DefineFunctionCommand(
           name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
     }
@@ -1101,7 +1096,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
   LPAREN_TOK /* parametric sorts */
   ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
     {
-      sorts.push_back(PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER));
+      sorts.push_back(PARSER_STATE->mkSort(name));
     }
   )*
   RPAREN_TOK
@@ -1197,7 +1192,7 @@ datatypesDef[bool isCo,
     ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK
       ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
         {
-          params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); }
+          params.push_back( PARSER_STATE->mkSort(name)); }
       )*
       RPAREN_TOK {
         // if the arity was fixed by prelude and is not equal to the number of parameters
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 17f5661b4..2474c89c2 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -18,7 +18,7 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "expr/type.h"
+#include "expr/expr.h"
 #include "options/options.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
@@ -41,10 +41,9 @@ Smt2::Smt2(api::Solver* solver,
       d_logicSet(false),
       d_seenSetLogic(false)
 {
-  pushScope(true);
 }
 
-Smt2::~Smt2() { popScope(); }
+Smt2::~Smt2() {}
 
 void Smt2::addArithmeticOperators() {
   addOperator(api::PLUS, "+");
@@ -445,7 +444,7 @@ api::Term Smt2::bindDefineFunRec(
   api::Sort ft = mkFlatFunctionType(sorts, t, flattenVars);
 
   // allow overloading
-  return bindVar(fname, ft, ExprManager::VAR_FLAG_NONE, true);
+  return bindVar(fname, ft, false, true);
 }
 
 void Smt2::pushDefineFunRecScope(
@@ -473,16 +472,6 @@ void Smt2::reset() {
   d_logic = LogicInfo();
   operatorKindMap.clear();
   d_lastNamedTerm = std::pair<api::Term, std::string>();
-  this->Parser::reset();
-  pushScope(true);
-}
-
-void Smt2::resetAssertions() {
-  // Remove all declarations except the ones at level 0.
-  while (this->scopeLevel() > 0) {
-    this->popScope();
-  }
-  pushScope(true);
 }
 
 std::unique_ptr<Command> Smt2::invConstraint(
@@ -1083,6 +1072,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   else if (p.d_kind == api::APPLY_SELECTOR && !p.d_expr.isNull())
   {
     // tuple selector case
+    std::string indexString = p.d_expr.toString();
     Integer x = p.d_expr.getExpr().getConst<Rational>().getNumerator();
     if (!x.fitsUnsignedInt())
     {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 654ff9fbf..ed329675d 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -192,8 +192,6 @@ class Smt2 : public Parser
 
   void reset() override;
 
-  void resetAssertions();
-
   /**
    * Creates a command that adds an invariant constraint.
    *
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 99907b51a..01eaf7096 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -18,7 +18,6 @@
 
 #include <antlr3.h>
 
-#include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
index e1365f603..729dad4ec 100644
--- a/src/parser/smt2/sygus_input.cpp
+++ b/src/parser/smt2/sygus_input.cpp
@@ -18,7 +18,6 @@
 
 #include <antlr3.h>
 
-#include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index f80b9c3c8..23bbd443d 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -21,7 +21,6 @@
 #include <set>
 
 #include "api/cvc4cpp.h"
-#include "expr/type.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "smt/command.h"
@@ -247,7 +246,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p)
   {
     api::Sort t =
         p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
-    expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
+    expr = bindVar(p.d_name, t, true);  // must define at level zero
     preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
   }
   return expr;
@@ -291,7 +290,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       api::Sort t =
           p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
       t = d_solver->mkFunctionSort(sorts, t);
-      v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
+      v = bindVar(p.d_name, t, true);  // must define at level zero
       preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
     }
     // args might be rationals, in which case we need to create
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 5634510ff..12c1a148a 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -19,7 +19,6 @@
 
 #include <antlr3.h>
 
-#include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"