Simplify how defined functions are tracked during parsing (#3177)

2 files changed, 3 insertions, 94 deletions

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index dd75170b5..c14143ef1 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -344,21 +344,18 @@ class SymbolTable::Implementation {
   Implementation()
       : d_context(),
         d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
-        d_typeMap(new (true) TypeMap(&d_context)),
-        d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {
+        d_typeMap(new (true) TypeMap(&d_context))
+  {
     d_overload_trie = new OverloadedTypeTrie(&d_context);
   }
 
   ~Implementation() {
     d_exprMap->deleteSelf();
     d_typeMap->deleteSelf();
-    d_functions->deleteSelf();
     delete d_overload_trie;
   }
 
   bool bind(const string& name, Expr obj, bool levelZero, bool doOverload);
-  bool bindDefinedFunction(const string& name, Expr obj, bool levelZero,
-                           bool doOverload);
   void bindType(const string& name, Type t, bool levelZero = false);
   void bindType(const string& name, const vector<Type>& params, Type t,
                 bool levelZero = false);
@@ -396,9 +393,6 @@ class SymbolTable::Implementation {
   using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>;
   TypeMap* d_typeMap;
 
-  /** A set of defined functions. */
-  CDHashSet<Expr, ExprHashFunction>* d_functions;
-
   //------------------------ operator overloading
   // the null expression
   Expr d_nullExpr;
@@ -430,40 +424,10 @@ bool SymbolTable::Implementation::bind(const string& name, Expr obj,
   return true;
 }
 
-bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
-                                                      Expr obj, bool levelZero,
-                                                      bool doOverload) {
-  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
-  ExprManagerScope ems(obj);
-  if (doOverload) {
-    if (!bindWithOverloading(name, obj)) {
-      return false;
-    }
-  }
-  if (levelZero) {
-    d_exprMap->insertAtContextLevelZero(name, obj);
-    d_functions->insertAtContextLevelZero(obj);
-  } else {
-    d_exprMap->insert(name, obj);
-    d_functions->insert(obj);
-  }
-  return true;
-}
-
 bool SymbolTable::Implementation::isBound(const string& name) const {
   return d_exprMap->find(name) != d_exprMap->end();
 }
 
-bool SymbolTable::Implementation::isBoundDefinedFunction(
-    const string& name) const {
-  CDHashMap<string, Expr>::const_iterator found = d_exprMap->find(name);
-  return found != d_exprMap->end() && d_functions->contains((*found).second);
-}
-
-bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const {
-  return d_functions->contains(func);
-}
-
 Expr SymbolTable::Implementation::lookup(const string& name) const {
   Assert(isBound(name));
   Expr expr = (*d_exprMap->find(name)).second;
@@ -646,15 +610,6 @@ bool SymbolTable::bind(const string& name,
   return d_implementation->bind(name, obj, levelZero, doOverload);
 }
 
-bool SymbolTable::bindDefinedFunction(const string& name,
-                                      Expr obj,
-                                      bool levelZero,
-                                      bool doOverload)
-{
-  return d_implementation->bindDefinedFunction(name, obj, levelZero,
-                                               doOverload);
-}
-
 void SymbolTable::bindType(const string& name, Type t, bool levelZero)
 {
   d_implementation->bindType(name, t, levelZero);
@@ -672,16 +627,6 @@ bool SymbolTable::isBound(const string& name) const
 {
   return d_implementation->isBound(name);
 }
-
-bool SymbolTable::isBoundDefinedFunction(const string& name) const
-{
-  return d_implementation->isBoundDefinedFunction(name);
-}
-
-bool SymbolTable::isBoundDefinedFunction(Expr func) const
-{
-  return d_implementation->isBoundDefinedFunction(func);
-}
 bool SymbolTable::isBoundType(const string& name) const
 {
   return d_implementation->isBoundType(name);
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 07f557059..868106a19 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -70,36 +70,6 @@ class CVC4_PUBLIC SymbolTable {
             bool doOverload = false);
 
   /**
-   * Bind a function body to a name in the current scope.
-   *
-   * When doOverload is false:
-   * if <code>name</code> is already bound to an expression in the current
-   * level, then the binding is replaced. If <code>name</code> is bound
-   * in a previous level, then the binding is "covered" by this one
-   * until the current scope is popped.
-   * If levelZero is true the name shouldn't be already bound.
-   *
-   * When doOverload is true:
-   * if <code>name</code> is already bound to an expression in the current
-   * level, then we mark the previous bound expression and obj as overloaded
-   * functions.
-   *
-   * Same as bind() but registers this as a function (so that
-   * isBoundDefinedFunction() returns true).
-   *
-   * @param name an identifier
-   * @param obj the expression to bind to <code>name</code>
-   * @param levelZero set if the binding must be done at level 0
-   * @param doOverload set if the binding can overload the function name.
-   *
-   * Returns false if the binding was invalid.
-   */
-  bool bindDefinedFunction(const std::string& name,
-                           Expr obj,
-                           bool levelZero = false,
-                           bool doOverload = false);
-
-  /**
    * Bind a type to a name in the current scope.  If <code>name</code>
    * is already bound to a type in the current level, then the binding
    * is replaced. If <code>name</code> is bound in a previous level,
@@ -131,8 +101,7 @@ class CVC4_PUBLIC SymbolTable {
                 bool levelZero = false);
 
   /**
-   * Check whether a name is bound to an expression with either bind()
-   * or bindDefinedFunction().
+   * Check whether a name is bound to an expression with bind().
    *
    * @param name the identifier to check.
    * @returns true iff name is bound in the current scope.
@@ -140,11 +109,6 @@ class CVC4_PUBLIC SymbolTable {
   bool isBound(const std::string& name) const;
 
   /**
-   * Check whether a name was bound to a function with bindDefinedFunction().
-   */
-  bool isBoundDefinedFunction(const std::string& name) const;
-
-  /**
    * Check whether an Expr was bound to a function (i.e., was the
    * second arg to bindDefinedFunction()).
    */