1 files changed, 40 insertions, 24 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0faf9bebf..1c492c843 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -186,26 +186,21 @@ public:
 
   bool strictModeEnabled() { return d_strictMode; }
 
-  /** Get the name of the input file. */
-/*
-  inline const std::string getFilename() {
-    return d_filename;
-  }
-*/
-
   /**
-   * Sets the logic for the current benchmark. Declares any logic symbols.
+   * Returns a variable, given a name.
    *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
+   * @param name the name of the variable
+   * @return the variable expression
    */
-//  void setLogic(const std::string& name);
+  Expr getVariable(const std::string& name);
 
   /**
-   * Returns a variable, given a name and a type.
+   * Returns a function, given a name.
+   *
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Expr getVariable(const std::string& var_name);
+  Expr getFunction(const std::string& name);
 
   /**
    * Returns a sort, given a name.
@@ -213,7 +208,7 @@ public:
   Type getSort(const std::string& sort_name);
 
   /**
-   * Returns a sort, given a name and args.
+   * Returns a (parameterized) sort, given a name and args.
    */
   Type getSort(const std::string& sort_name,
                const std::vector<Type>& params);
@@ -240,7 +235,8 @@ public:
   /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
-   * @throws ParserException if checks are enabled and name is not bound to a function
+   * @throws ParserException if checks are enabled and name is not
+   * bound to a function
    */
   void checkFunction(const std::string& name) throw (ParserException);
 
@@ -248,23 +244,26 @@ public:
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
-   * applied to <code>numArgs</code> arguments.
+   * @throws ParserException if checks are enabled and the operator
+   * <code>kind</code> cannot be applied to <code>numArgs</code>
+   * arguments.
    */
   void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
 
-  /** Check that <code>kind</code> is a legal operator in the current logic and
-   * that it can accept <code>numArgs</code> arguments.
+  /**
+   * Check that <code>kind</code> is a legal operator in the current
+   * logic and that it can accept <code>numArgs</code> arguments.
    *
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws ParserException if the parser mode is strict and the operator <code>kind</kind>
-   * has not been enabled
+   * @throws ParserException if the parser mode is strict and the
+   * operator <code>kind</kind> has not been enabled
    */
   void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
 
   /**
    * Returns the type for the variable with the given name.
+   *
    * @param var_name the symbol to lookup
    * @param type the (namespace) type of the symbol
    */
@@ -274,27 +273,41 @@ public:
   Expr mkVar(const std::string& name, const Type& type);
 
   /**
-   * Create a set of new CVC4 variable expressions of the given
-   * type.
+   * Create a set of new CVC4 variable expressions of the given type.
    */
   const std::vector<Expr>
   mkVars(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);
+
   /** Create a new variable definition (e.g., from a let binding). */
   void defineVar(const std::string& name, const Expr& val);
 
+  /** Create a new function definition (e.g., from a define-fun). */
+  void defineFunction(const std::string& name, const Expr& val);
+
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
 
+  /** Create a new (parameterized) type definition. */
+  void defineType(const std::string& name,
+                  const std::vector<Type>& params, const Type& type);
+
   /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */
   void defineParameterizedType(const std::string& name,
                                const std::vector<Type>& params,
                                const Type& type);
 
   /**
-   * Creates a new sort with the given name and arity.
+   * Creates a new sort with the given name.
+   */
+  Type mkSort(const std::string& name);
+
+  /**
+   * Creates a new sort constructor with the given name and arity.
    */
-  Type mkSort(const std::string& name, size_t arity = 0);
+  Type mkSortConstructor(const std::string& name, size_t arity);
 
   /**
    * Creates new sorts with the given names (all of arity 0).
@@ -314,6 +327,9 @@ public:
   /** Is the symbol bound to a function? */
   bool isFunction(const std::string& name);
 
+  /** Is the symbol bound to a defined function? */
+  bool isDefinedFunction(const std::string& name);
+
   /** Is the symbol bound to a predicate? */
   bool isPredicate(const std::string& name);