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

8 files changed, 37 insertions, 182 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()).
    */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 6de746ad7..7191ee064 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1153,7 +1153,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t,
           Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
           Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
-          PARSER_STATE->defineFunction(*i, f);
+          PARSER_STATE->defineVar(*i, f);
           Command* decl = new DefineFunctionCommand(*i, func, f);
           seq->addCommand(decl);
         }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c8e09b8e0..8217e32c6 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -138,19 +138,25 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
 }
 
 Kind Parser::getKindForFunction(Expr fun) {
-  if(isDefinedFunction(fun)) {
+  Type t = fun.getType();
+  if (t.isFunction())
+  {
     return APPLY_UF;
   }
-  Type t = fun.getType();
-  if(t.isConstructor()) {
+  else if (t.isConstructor())
+  {
     return APPLY_CONSTRUCTOR;
-  } else if(t.isSelector()) {
+  }
+  else if (t.isSelector())
+  {
     return APPLY_SELECTOR;
-  } else if(t.isTester()) {
+  }
+  else if (t.isTester())
+  {
     return APPLY_TESTER;
-  } else if(t.isFunction()) {
-    return APPLY_UF;
-  }else{
+  }
+  else
+  {
     parseError("internal error: unhandled function application kind");
     return UNDEFINED_KIND;
   }
@@ -191,20 +197,6 @@ bool Parser::isFunctionLike(Expr fun) {
          type.isSelector();
 }
 
-/* Returns true if name is bound to a defined function. */
-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_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_symtab->isBoundDefinedFunction(func);
-}
-
 /* Returns true if name is bound to a function returning boolean. */
 bool Parser::isPredicate(const std::string& name) {
   Expr expr = getVariable(name);
@@ -228,17 +220,6 @@ Expr Parser::mkBoundVar(const std::string& name, const Type& type) {
   return expr;
 }
 
-Expr Parser::mkFunction(const std::string& name, const Type& type,
-                        uint32_t flags, bool doOverload) {
-  if (d_globalDeclarations) {
-    flags |= ExprManager::VAR_FLAG_GLOBAL;
-  }
-  Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
-  Expr expr = getExprManager()->mkVar(name, type, flags);
-  defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
-  return expr;
-}
-
 Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
                                  uint32_t flags) {
   if (d_globalDeclarations) {
@@ -282,16 +263,6 @@ void Parser::defineVar(const std::string& name, const Expr& val,
   assert(isDeclared(name));
 }
 
-void Parser::defineFunction(const std::string& name, const Expr& val,
-                            bool levelZero, bool doOverload) {
-  if (!d_symtab->bindDefinedFunction(name, val, levelZero, doOverload)) {
-    std::stringstream ss;
-    ss << "Failed to bind defined function " << name << " to symbol of type " << val.getType();
-    parseError(ss.str()); 
-  }
-  assert(isDeclared(name));
-}
-
 void Parser::defineType(const std::string& name, const Type& type) {
   d_symtab->bindType(name, type);
   assert(isDeclared(name, SYM_SORT));
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8f9cc425a..9319181db 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -497,15 +497,10 @@ public:
    */
   std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
 
-  /** Create a new CVC4 function expression of the given type. */
-  Expr mkFunction(const std::string& name, const Type& type,
-                  uint32_t flags = ExprManager::VAR_FLAG_NONE, 
-                  bool doOverload=false);
-
   /**
    * 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 mkFunction()).
+   * 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).
@@ -522,15 +517,6 @@ public:
   void defineVar(const std::string& name, const Expr& val,
                  bool levelZero = false, bool doOverload = false);
 
-  /** Create a new function definition (e.g., from a define-fun). 
-   * levelZero is set if the binding must be done at level 0.
-   * 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.
-   */
-  void defineFunction(const std::string& name, const Expr& val,
-                      bool levelZero = false, bool doOverload = false);
-
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
@@ -677,12 +663,6 @@ public:
   */
   bool isFunctionLike(Expr fun);
 
-  /** Is the symbol bound to a defined function? */
-  bool isDefinedFunction(const std::string& name);
-
-  /** Is the Expr a defined function? */
-  bool isDefinedFunction(Expr func);
-
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2a736402e..c672d8ff5 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -400,8 +400,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       // must not be extended with the name itself; no recursion
       // permitted)
       // we allow overloading for function definitions
-      Expr func = PARSER_STATE->mkFunction(name, t,
-                                           ExprManager::VAR_FLAG_DEFINED, true);
+      Expr func = PARSER_STATE->mkVar(name, t,
+                                      ExprManager::VAR_FLAG_DEFINED, true);
       cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
     }
   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
@@ -745,7 +745,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
     }
     ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
         if( !terms.empty() ){
-          if( !PARSER_STATE->isDefinedFunction(name) ){
+          if (!PARSER_STATE->isDeclared(name))
+          {
             std::stringstream ss;
             ss << "Function " << name << " in inv-constraint is not defined.";
             PARSER_STATE->parseError(ss.str());
@@ -988,11 +989,10 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
           // fail, but we need an operator to continue here..
           Debug("parser-sygus")
               << "Sygus grammar " << fun << " : op (declare="
-              << PARSER_STATE->isDeclared(name) << ", define="
-              << PARSER_STATE->isDefinedFunction(name) << ") : " << name
+              << PARSER_STATE->isDeclared(name) << ") : " << name
               << std::endl;
-          if(!PARSER_STATE->isDeclared(name) &&
-             !PARSER_STATE->isDefinedFunction(name) ){
+          if (!PARSER_STATE->isDeclared(name))
+          {
             PARSER_STATE->parseError("Functions in sygus grammars must be "
                                      "defined.");
           }
@@ -1459,8 +1459,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
       { PARSER_STATE->checkUserSymbol(name); }
       term[e,e2]
-      { Expr func = PARSER_STATE->mkFunction(name, e.getType(),
-                                             ExprManager::VAR_FLAG_DEFINED);
+      { Expr func = PARSER_STATE->mkVar(name, e.getType(),
+                                        ExprManager::VAR_FLAG_DEFINED);
         cmd->reset(new DefineFunctionCommand(name, func, e));
       }
     | LPAREN_TOK
@@ -1492,8 +1492,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
-        Expr func = PARSER_STATE->mkFunction(name, t,
-                                             ExprManager::VAR_FLAG_DEFINED);
+        Expr func = PARSER_STATE->mkVar(name, t,
+                                        ExprManager::VAR_FLAG_DEFINED);
         cmd->reset(new DefineFunctionCommand(name, func, terms, e));
       }
     )
@@ -1515,8 +1515,8 @@ 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)
-      Expr func = PARSER_STATE->mkFunction(name, t,
-                                           ExprManager::VAR_FLAG_DEFINED);
+      Expr func = PARSER_STATE->mkVar(name, t,
+                                      ExprManager::VAR_FLAG_DEFINED);
       cmd->reset(new DefineFunctionCommand(name, func, terms, e));
     }
 
@@ -2863,7 +2863,7 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
       // check that sexpr is a fresh function symbol, and reserve it
       PARSER_STATE->reserveSymbolAtAssertionLevel(name);
       // define it
-      Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+      Expr func = PARSER_STATE->mkVar(name, expr.getType());
       // remember the last term to have been given a :named attribute
       PARSER_STATE->setLastNamedTerm(expr, name);
       // bind name to expr with define-fun
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 039f573f9..be0306a9e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1171,7 +1171,7 @@ void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
   Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
   std::stringstream ss;
   ss << datatypes[index].getName() << "_let";
-  Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+  Expr let_func = mkVar(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
   d_sygus_defined_funs.push_back( let_func );
   preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
 
@@ -1338,7 +1338,7 @@ void Smt2::mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
           // the given name.
           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
         }
-        else if (isDefinedFunction(ops[i]))
+        else if (ops[i].getKind() == kind::VARIABLE)
         {
           Debug("parser-sygus") << "--> Defined function " << ops[i]
                                 << std::endl;
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 599b3bbe1..54fba4d1b 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -841,7 +841,7 @@ thfAtomTyping[CVC4::Command*& cmd]
           CVC4::Expr freshExpr;
           if (type.isFunction())
           {
-            freshExpr = PARSER_STATE->mkFunction(name, type);
+            freshExpr = PARSER_STATE->mkVar(name, type);
           }
           else
           {
@@ -1077,12 +1077,7 @@ tffTypedAtom[CVC4::Command*& cmd]
           }
         } else {
           // as yet, it's undeclared
-          CVC4::Expr expr;
-          if(type.isFunction()) {
-            expr = PARSER_STATE->mkFunction(name, type);
-          } else {
-            expr = PARSER_STATE->mkVar(name, type);
-          }
+          CVC4::Expr expr = PARSER_STATE->mkVar(name, type);
           cmd = new DeclareFunctionCommand(name, expr, type);
         }
       }