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

1 files changed, 14 insertions, 43 deletions

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));