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

1 files changed, 1 insertions, 21 deletions

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