Op overload parser (#1162)

* Update parser for operator overloading.

* Improvements

* Updates

* Add assert

7 files changed, 348 insertions, 156 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d0324cc45..eef7ca54d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1047,7 +1047,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t,
             i != i_end;
             ++i) {
           if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) {
-            Type oldType = PARSER_STATE->getType(*i);
+            Type oldType = PARSER_STATE->getVariable(*i).getType();
             Debug("parser") << "  " << *i << " was declared previously "
                             << "with type " << oldType << std::endl;
             if(oldType != t) {
@@ -1745,22 +1745,10 @@ postfixTerm[CVC4::Expr& f]
       formula[f] { args.push_back(f); }
       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
       // TODO: check arity
-      { Type t = args.front().getType();
-        Debug("parser") << "type is " << t << std::endl;
+      { Kind k = PARSER_STATE->getKindForFunction(args.front());
         Debug("parser") << "expr is " << args.front() << std::endl;
-        if(PARSER_STATE->isDefinedFunction(args.front())) {
-          f = MK_EXPR(CVC4::kind::APPLY, args);
-        } else if(t.isFunction()) {
-          f = MK_EXPR(CVC4::kind::APPLY_UF, args);
-        } else if(t.isConstructor()) {
-          f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
-        } else if(t.isSelector()) {
-          f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
-        } else if(t.isTester()) {
-          f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
-        } else {
-          PARSER_STATE->parseError("internal error: unhandled function application kind");
-        }
+        Debug("parser") << "kind is " << k << std::endl;
+        f = MK_EXPR(k, args);
       }
 
       /* record / tuple select */
@@ -2137,9 +2125,9 @@ simpleTerm[CVC4::Expr& f]
     /* variable / zero-ary constructor application */
   | identifier[name,CHECK_DECLARED,SYM_VARIABLE]
     /* ascriptions will be required for parameterized zero-ary constructors */
-    { f = PARSER_STATE->getVariable(name); }
-    { // datatypes: zero-ary constructors
-      Type t2 = PARSER_STATE->getType(name);
+    { f = PARSER_STATE->getVariable(name);
+      // datatypes: zero-ary constructors
+      Type t2 = f.getType();
       if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) {
         // don't require parentheses, immediately turn it into an apply
         f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 63492caa8..c8b4ac966 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -23,6 +23,7 @@
 #include <iostream>
 #include <iterator>
 #include <sstream>
+#include <unordered_set>
 
 #include "base/output.h"
 #include "expr/expr.h"
@@ -92,11 +93,61 @@ Expr Parser::getFunction(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Type Parser::getType(const std::string& var_name, SymbolType type) {
-  checkDeclaration(var_name, CHECK_DECLARED, type);
-  assert(isDeclared(var_name, type));
-  Type t = getSymbol(var_name, type).getType();
-  return t;
+Expr Parser::getExpressionForName(const std::string& name) {
+  Type t;
+  return getExpressionForNameAndType(name, t);
+}
+
+Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
+  assert( isDeclared(name) );
+  // first check if the variable is declared and not overloaded
+  Expr expr = getVariable(name);
+  if(expr.isNull()) {
+    // the variable is overloaded, try with type if the type exists
+    if(!t.isNull()) {
+      // if we decide later to support annotations for function types, this will update to 
+      // separate t into ( argument types, return type )
+      expr = getOverloadedConstantForType(name, t);
+      if(expr.isNull()) {
+        parseError("Cannot get overloaded constant for type ascription.");
+      }
+    }else{
+      parseError("Overloaded constants must be type cast.");
+    }
+  }
+  // now, post-process the expression
+  assert( !expr.isNull() );
+  if(isDefinedFunction(expr)) {
+    // defined functions/constants are wrapped in an APPLY so that they are
+    // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions
+    expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr);
+  }else{
+    Type te = expr.getType();
+    if(te.isConstructor() && ConstructorType(te).getArity() == 0) {
+      // nullary constructors have APPLY_CONSTRUCTOR kind with no children
+      expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+    }
+  }
+  return expr;
+}
+
+Kind Parser::getKindForFunction(Expr fun) {
+  if(isDefinedFunction(fun)) {
+    return APPLY;
+  }
+  Type t = fun.getType();
+  if(t.isConstructor()) {
+    return APPLY_CONSTRUCTOR;
+  } else if(t.isSelector()) {
+    return APPLY_SELECTOR;
+  } else if(t.isTester()) {
+    return APPLY_TESTER;
+  } else if(t.isFunction()) {
+    return APPLY_UF;
+  }else{
+    parseError("internal error: unhandled function application kind");
+    return UNDEFINED_KIND;
+  }
 }
 
 Type Parser::getSort(const std::string& name) {
@@ -121,16 +172,15 @@ size_t Parser::getArity(const std::string& sort_name) {
 
 /* Returns true if name is bound to a boolean variable. */
 bool Parser::isBoolean(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
+  Expr expr = getVariable(name);
+  return !expr.isNull() && expr.getType().isBoolean();
 }
 
-/* Returns true if name is bound to a function-like thing (function,
- * constructor, tester, or selector). */
-bool Parser::isFunctionLike(const std::string& name) {
-  if (!isDeclared(name, SYM_VARIABLE)) {
+bool Parser::isFunctionLike(Expr fun) {
+  if(fun.isNull()) {
     return false;
   }
-  Type type = getType(name);
+  Type type = fun.getType();
   return type.isFunction() || type.isConstructor() || type.isTester() ||
          type.isSelector();
 }
@@ -151,16 +201,17 @@ bool Parser::isDefinedFunction(Expr func) {
 
 /* Returns true if name is bound to a function returning boolean. */
 bool Parser::isPredicate(const std::string& name) {
-  return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
+  Expr expr = getVariable(name);
+  return !expr.isNull() && expr.getType().isPredicate();
 }
 
-Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+Expr Parser::mkVar(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 = d_exprManager->mkVar(name, type, flags);
-  defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
+  defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
   return expr;
 }
 
@@ -172,13 +223,13 @@ Expr Parser::mkBoundVar(const std::string& name, const Type& type) {
 }
 
 Expr Parser::mkFunction(const std::string& name, const Type& type,
-                        uint32_t flags) {
+                        uint32_t flags, bool doOverload) {
   if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkVar(name, type, flags);
-  defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
+  defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
   return expr;
 }
 
@@ -193,13 +244,13 @@ Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
 }
 
 std::vector<Expr> Parser::mkVars(const std::vector<std::string> names,
-                                 const Type& type, uint32_t flags) {
+                                 const Type& type, uint32_t flags, bool doOverload) {
   if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   std::vector<Expr> vars;
   for (unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type, flags));
+    vars.push_back(mkVar(names[i], type, flags, doOverload));
   }
   return vars;
 }
@@ -214,15 +265,23 @@ std::vector<Expr> Parser::mkBoundVars(const std::vector<std::string> names,
 }
 
 void Parser::defineVar(const std::string& name, const Expr& val,
-                       bool levelZero) {
+                       bool levelZero, bool doOverload) {
   Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
-  d_symtab->bind(name, val, levelZero);
+  if (!d_symtab->bind(name, val, levelZero, doOverload)) {
+    std::stringstream ss;
+    ss << "Failed to bind " << name << " to symbol of type " << val.getType();
+    parseError(ss.str()); 
+  }
   assert(isDeclared(name));
 }
 
 void Parser::defineFunction(const std::string& name, const Expr& val,
-                            bool levelZero) {
-  d_symtab->bindDefinedFunction(name, val, levelZero);
+                            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));
 }
 
@@ -305,7 +364,7 @@ bool Parser::isUnresolvedType(const std::string& name) {
 }
 
 std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
-    std::vector<Datatype>& datatypes) {
+    std::vector<Datatype>& datatypes, bool doOverload) {
   try {
     std::vector<DatatypeType> types =
         d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
@@ -326,6 +385,8 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
       } else {
         defineType(name, t);
       }
+      std::unordered_set< std::string > consNames;
+      std::unordered_set< std::string > selNames;
       for (Datatype::const_iterator j = dt.begin(), j_end = dt.end();
            j != j_end; ++j) {
         const DatatypeConstructor& ctor = *j;
@@ -333,27 +394,37 @@ std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
         Expr constructor = ctor.getConstructor();
         Debug("parser-idt") << "+ define " << constructor << std::endl;
         string constructorName = ctor.getName();
-        if (isDeclared(constructorName, SYM_VARIABLE)) {
-          throw ParserException(constructorName + " already declared");
+        if(consNames.find(constructorName)==consNames.end()) {
+          if(!doOverload) {
+            checkDeclaration(constructorName, CHECK_UNDECLARED);
+          }
+          defineVar(constructorName, constructor, false, doOverload);
+          consNames.insert(constructorName);
+        }else{
+          throw ParserException(constructorName + " already declared in this datatype");
         }
-        defineVar(constructorName, constructor);
         Expr tester = ctor.getTester();
         Debug("parser-idt") << "+ define " << tester << std::endl;
         string testerName = ctor.getTesterName();
-        if (isDeclared(testerName, SYM_VARIABLE)) {
-          throw ParserException(testerName + " already declared");
+        if(!doOverload) {
+          checkDeclaration(testerName, CHECK_UNDECLARED);
         }
-        defineVar(testerName, tester);
+        defineVar(testerName, tester, false, doOverload);
         for (DatatypeConstructor::const_iterator k = ctor.begin(),
                                                  k_end = ctor.end();
              k != k_end; ++k) {
           Expr selector = (*k).getSelector();
           Debug("parser-idt") << "+++ define " << selector << std::endl;
           string selectorName = (*k).getName();
-          if (isDeclared(selectorName, SYM_VARIABLE)) {
-            throw ParserException(selectorName + " already declared");
+          if(selNames.find(selectorName)==selNames.end()) {
+            if(!doOverload) {
+              checkDeclaration(selectorName, CHECK_UNDECLARED);
+            }
+            defineVar(selectorName, selector, false, doOverload);
+            selNames.insert(selectorName);
+          }else{
+            throw ParserException(selectorName + " already declared in this datatype");
           }
-          defineVar(selectorName, selector);
         }
       }
     }
@@ -426,9 +497,13 @@ void Parser::checkDeclaration(const std::string& varName,
   }
 }
 
-void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
-  if (d_checksEnabled && !isFunctionLike(name)) {
-    parseError("Expecting function-like symbol, found '" + name + "'");
+void Parser::checkFunctionLike(Expr fun) throw(ParserException) {
+  if (d_checksEnabled && !isFunctionLike(fun)) {
+    stringstream ss;
+    ss << "Expecting function-like symbol, found '";
+    ss << fun;
+    ss << "'";
+    parseError(ss.str());
   }
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 5e867afa3..eb0588ab0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -134,7 +134,7 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
  */
 class CVC4_PUBLIC Parser {
   friend class ParserBuilder;
-
+private:
   /** The expression manager */
   ExprManager *d_exprManager;
   /** The resource manager associated with this expr manager */
@@ -235,7 +235,9 @@ class CVC4_PUBLIC Parser {
    */
   std::list<Command*> d_commandQueue;
 
-  /** Lookup a symbol in the given namespace. */
+  /** Lookup a symbol in the given namespace (as specified by the type). 
+   * Only returns a symbol if it is not overloaded, returns null otherwise.
+   */
   Expr getSymbol(const std::string& var_name, SymbolType type);
 
 protected:
@@ -318,22 +320,53 @@ public:
   bool logicIsForced() const { return d_logicIsForced; }
 
   /**
-   * Returns a variable, given a name.
+   * Gets the variable currently bound to name.
    *
    * @param name the name of the variable
    * @return the variable expression
+   * Only returns a variable if its name is not overloaded, returns null otherwise.
    */
   Expr getVariable(const std::string& name);
 
   /**
-   * Returns a function, given a name.
+   * Gets the function currently bound to name.
    *
    * @param name the name of the variable
    * @return the variable expression
+   * Only returns a function if its name is not overloaded, returns null otherwise.
    */
   Expr getFunction(const std::string& name);
 
   /**
+   * Returns the expression that name should be interpreted as, based on the current binding.
+   *
+   * The symbol name should be declared.
+   * This creates the expression that the string "name" should be interpreted as.
+   * Typically this corresponds to a variable, but it may also correspond to
+   * a nullary constructor or a defined function.
+   * Only returns an expression if its name is not overloaded, returns null otherwise.
+   */
+  virtual Expr getExpressionForName(const std::string& name);
+  
+  /**
+   * Returns the expression that name should be interpreted as, based on the current binding.
+   *
+   * This is the same as above but where the name has been type cast to t. 
+   */
+  virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
+  
+  /**
+   * Returns the kind that should be used for applications of expression fun, where
+   * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. 
+   * Returns a parse error if fun does not have function-like type.
+   * 
+   * For example, this function returns
+   *   APPLY_UF if fun has function type, 
+   *   APPLY_CONSTRUCTOR if fun has constructor type.
+   */
+  Kind getKindForFunction(Expr fun);
+  
+  /**
    * Returns a sort, given a name.
    * @param sort_name the name to look up
    */
@@ -377,12 +410,15 @@ public:
   void reserveSymbolAtAssertionLevel(const std::string& name);
 
   /**
-   * 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
+   * Checks whether the given expression is function-like, i.e.
+   * it expects arguments. This is checked by looking at the type 
+   * of fun. Examples of function types are function, constructor,
+   * selector, tester.
+   * @param fun the expression to check
+   * @throws ParserException if checks are enabled and fun is not
+   * a function
    */
-  void checkFunctionLike(const std::string& name) throw(ParserException);
+  void checkFunctionLike(Expr fun) throw(ParserException);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</code> arguments.
@@ -405,52 +441,82 @@ public:
    */
   void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
 
-  /**
-   * Returns the type for the variable with the given name.
+  /** Create a new CVC4 variable expression of the given type. 
    *
-   * @param var_name the symbol to lookup
-   * @param type the (namespace) type of the symbol
+   * flags specify information about the variable, e.g. whether it is global or defined
+   *   (see enum in expr_manager_template.h).
+   *
+   * 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.
    */
-  Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
-
-  /** Create a new CVC4 variable expression of the given type. */
   Expr mkVar(const std::string& name, const Type& type,
-             uint32_t flags = ExprManager::VAR_FLAG_NONE);
+             uint32_t flags = ExprManager::VAR_FLAG_NONE, 
+             bool doOverload = false);
 
   /**
    * Create a set of new CVC4 variable expressions of the given type.
+   *
+   * flags specify information about the variable, e.g. whether it is global or defined
+   *   (see enum in expr_manager_template.h).
+   *
+   * For each name, 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.
    */
   std::vector<Expr>
     mkVars(const std::vector<std::string> names, const Type& type,
-           uint32_t flags = ExprManager::VAR_FLAG_NONE);
+           uint32_t flags = ExprManager::VAR_FLAG_NONE, 
+           bool doOverload = false);
 
   /** Create a new CVC4 bound variable expression of the given type. */
   Expr mkBoundVar(const std::string& name, const Type& type);
 
   /**
    * Create a set of new CVC4 bound variable expressions of the given type.
+   *
+   * flags specify information about the variable, e.g. whether it is global or defined
+   *   (see enum in expr_manager_template.h).
+   *
+   * For each name, 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.
    */
   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);
+                  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()).
+   *
+   * flags specify information about the variable, e.g. whether it is global or defined
+   *   (see enum in expr_manager_template.h).
    */
   Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
                            uint32_t flags = ExprManager::VAR_FLAG_NONE);
 
-  /** Create a new variable definition (e.g., from a let binding). */
+  /** Create a new variable definition (e.g., from a let binding). 
+   * 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 defineVar(const std::string& name, const Expr& val,
-                 bool levelZero = false);
+                 bool levelZero = false, bool doOverload = false);
 
-  /** Create a new function definition (e.g., from a define-fun). */
+  /** 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 levelZero = false, bool doOverload = false);
 
   /** Create a new type definition. */
   void defineType(const std::string& name, const Type& type);
@@ -500,9 +566,12 @@ public:
 
   /**
    * Create sorts of mutually-recursive datatypes.
+   * For each symbol defined by the datatype, 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.
    */
   std::vector<DatatypeType>
-  mkMutualDatatypeTypes(std::vector<Datatype>& datatypes);
+  mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false);
 
   /**
    * Add an operator to the current legal set.
@@ -522,8 +591,10 @@ public:
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
 
-  /** Is the symbol bound to a function (or function-like thing)? */
-  bool isFunctionLike(const std::string& name);
+  /** Is fun a function (or function-like thing)? 
+  * Currently this means its type is either a function, constructor, tester, or selector.
+  */
+  bool isFunctionLike(Expr fun);
 
   /** Is the symbol bound to a defined function? */
   bool isDefinedFunction(const std::string& name);
@@ -663,6 +734,30 @@ public:
     ~ExprStream() { delete d_parser; }
     Expr nextExpr() { return d_parser->nextExpression(); }
   };/* class Parser::ExprStream */
+  
+  //------------------------ operator overloading
+  /** is this function overloaded? */
+  bool isOverloadedFunction(Expr fun) {
+    return d_symtab->isOverloadedFunction(fun);
+  }
+  
+  /** Get overloaded constant for type.
+   * If possible, it returns a defined symbol with name
+   * that has type t. Otherwise returns null expression.
+  */
+  Expr getOverloadedConstantForType(const std::string& name, Type t) {
+    return d_symtab->getOverloadedConstantForType(name, t);
+  }
+  
+  /**
+   * If possible, returns a defined function for a name
+   * and a vector of expected argument types. Otherwise returns
+   * null expression.
+   */
+  Expr getOverloadedFunctionForTypes(const std::string& name, std::vector< Type >& argTypes) {
+    return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
+  }
+  //------------------------ end operator overloading
 };/* class Parser */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 93169504d..479ef35c5 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -483,8 +483,8 @@ functionSymbol[CVC4::Expr& fun]
 	std::string name;
 }
   : functionName[name,CHECK_DECLARED]
-    { PARSER_STATE->checkFunctionLike(name);
-      fun = PARSER_STATE->getVariable(name); }
+    { fun = PARSER_STATE->getVariable(name);
+      PARSER_STATE->checkFunctionLike(fun); }
   ;
 
 /**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2aa85fbe3..3deffe703 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -339,7 +339,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     }
   | /* function declaration */
     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    symbol[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK sortList[sorts] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
@@ -351,7 +351,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         }
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
-      Expr func = PARSER_STATE->mkVar(name, t);
+      // we allow overloading for function declarations
+      Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
       cmd->reset(new DeclareFunctionCommand(name, func, t));
     }
   | /* function definition */
@@ -386,8 +387,9 @@ command [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)
+      // we allow overloading for function definitions
       Expr func = PARSER_STATE->mkFunction(name, t,
-                                           ExprManager::VAR_FLAG_DEFINED);
+                                           ExprManager::VAR_FLAG_DEFINED, true);
       cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
     }
   | /* value query */
@@ -622,7 +624,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
       }else{
         synth_fun_type = range;
       }
-      synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type);
+      // allow overloading for synth fun
+      synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true);
       PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
@@ -1145,10 +1148,11 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
 
     /* declare-const */
   | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    symbol[name,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
-    { Expr c = PARSER_STATE->mkVar(name, t);
+    { // allow overloading here
+      Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
       cmd->reset(new DeclareFunctionCommand(name, c, t)); }
 
     /* get model */
@@ -1178,7 +1182,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
     { PARSER_STATE->checkThatLogicIsSet();
       seq.reset(new CVC4::CommandSequence());
     }
-    symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
+    symbol[fname,CHECK_NONE,SYM_VARIABLE]
     { PARSER_STATE->checkUserSymbol(fname); }
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     sortSymbol[t,CHECK_DECLARED]
@@ -1192,7 +1196,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
         }
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
-      Expr func = PARSER_STATE->mkVar(fname, t);
+      // allow overloading
+      Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
       seq->addCommand(new DeclareFunctionCommand(fname, func, t));
       if( sortedVarNames.empty() ){
         func_app = func;
@@ -1249,7 +1254,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
           }
         }
         sortedVarNames.clear();
-        Expr func = PARSER_STATE->mkVar(fname, t);
+        // allow overloading
+        Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
         seq->addCommand(new DeclareFunctionCommand(fname, func, t));
         funcs.push_back( func );
       }
@@ -1391,7 +1397,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         } else {
           t = sorts[0];
         }
-        Expr func = PARSER_STATE->mkVar(name, t);
+        // allow overloading
+        Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
         seq->addCommand(new DeclareFunctionCommand(name, func, t));
         sorts.clear();
       }
@@ -1412,7 +1419,8 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
-        Expr func = PARSER_STATE->mkVar(name, t);
+        // allow overloading
+        Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
         seq->addCommand(new DeclareFunctionCommand(name, func, t));
         sorts.clear();
       }
@@ -1513,7 +1521,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
-    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)));
+    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
   }
   ;
   
@@ -1529,7 +1537,7 @@ datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
  }
  ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
  RPAREN_TOK
- { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); }
+ { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); }
  ;
   
 datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
@@ -1591,7 +1599,7 @@ datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
     )+
   RPAREN_TOK
   { PARSER_STATE->popScope();
-    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); 
+    cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); 
   }
   ;
 
@@ -1788,6 +1796,22 @@ symbolicExpr[CVC4::SExpr& sexpr]
  */
 term[CVC4::Expr& expr, CVC4::Expr& expr2]
 @init {
+  std::string name;
+}
+: termNonVariable[expr, expr2]
+    /* a variable */
+  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+    { expr = PARSER_STATE->getExpressionForName(name); 
+      assert( !expr.isNull() );
+    }
+  ;
+
+/**
+ * Matches a term.
+ * @return the expression representing the formula
+ */
+termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
+@init {
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind = kind::NULL_EXPR;
   Expr op;
@@ -1804,6 +1828,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   Type type;
   std::string s;
   bool isBuiltinOperator = false;
+  bool isOverloadedFunction = false;
+  bool readVariable = false;
   int match_vindex = -1;
   std::vector<Type> match_ptypes;
 }
@@ -1852,17 +1878,29 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
+  | LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) 
+    sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
     {
+      if(readVariable) {
+        Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl;
+        // get the variable expression for the type
+        f = PARSER_STATE->getExpressionForNameAndType(name, type); 
+        assert( !f.isNull() );
+      }
       if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
-        std::vector<CVC4::Expr> v;
-        Expr e = f.getOperator();
-        const DatatypeConstructor& dtc =
-            Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-        v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
-                             MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
-        v.insert(v.end(), f.begin(), f.end());
-        expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+        // could be a parametric type constructor or just an overloaded constructor
+        if(((DatatypeType)type).isParametric()) {
+          std::vector<CVC4::Expr> v;
+          Expr e = f.getOperator();
+          const DatatypeConstructor& dtc =
+              Datatype::datatypeOf(e)[Datatype::indexOf(e)];
+          v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION,
+                               MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
+          v.insert(v.end(), f.begin(), f.end());
+          expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+        }else{
+          expr = f;
+        }
       } else if(f.getKind() == CVC4::kind::EMPTYSET) {
         Debug("parser") << "Empty set encountered: " << f << " "
                           << f2 << " " << type <<  std::endl;
@@ -1877,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
+        }else{
+          expr = f;
         }
       }
     }
@@ -1925,32 +1965,20 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else {
         /* A non-built-in function application */
         PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
-        //hack to allow constants with parentheses (disabled for now)
-        //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(name) ){
-        //  op = PARSER_STATE->getVariable(name);
-        //}else{
-        PARSER_STATE->checkFunctionLike(name);
-        const bool isDefinedFunction =
-          PARSER_STATE->isDefinedFunction(name);
-        if(isDefinedFunction) {
-          expr = PARSER_STATE->getFunction(name);
-          kind = CVC4::kind::APPLY;
-        } else {
-          expr = PARSER_STATE->getVariable(name);
-          Type t = expr.getType();
-          if(t.isConstructor()) {
-            kind = CVC4::kind::APPLY_CONSTRUCTOR;
-          } else if(t.isSelector()) {
-            kind = CVC4::kind::APPLY_SELECTOR;
-          } else if(t.isTester()) {
-            kind = CVC4::kind::APPLY_TESTER;
-          } else {
-            kind = CVC4::kind::APPLY_UF;
-          }
+        expr = PARSER_STATE->getVariable(name);
+        if(!expr.isNull()) {
+          //hack to allow constants with parentheses (disabled for now)
+          //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(expr) ){
+          //  op = PARSER_STATE->getVariable(name);
+          //}else{
+          PARSER_STATE->checkFunctionLike(expr);
+          kind = PARSER_STATE->getKindForFunction(expr);
+          args.push_back(expr);
+        }else{
+          isOverloadedFunction = true;
         }
-        args.push_back(expr);
       }
-        }
+    }
     //(termList[args,expr])? RPAREN_TOK
     termList[args,expr] RPAREN_TOK
     { Debug("parser") << "args has size " << args.size() << std::endl
@@ -1958,6 +1986,20 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
         Debug("parser") << "++ " << *i << std::endl;
       }
+      if(isOverloadedFunction) {
+        std::vector< Type > argTypes;
+        for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
+          argTypes.push_back( (*i).getType() );
+        }
+        expr = PARSER_STATE->getOverloadedFunctionForTypes(name, argTypes);
+        if(!expr.isNull()) {
+          PARSER_STATE->checkFunctionLike(expr);
+          kind = PARSER_STATE->getKindForFunction(expr);
+          args.insert(args.begin(),expr);
+        }else{
+          PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
+        }
+      }
       if(isBuiltinOperator) {
         PARSER_STATE->checkOperator(kind, args.size());
       }
@@ -2169,30 +2211,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       // ConstructorType(expr.getType()).getArity()==0;
       expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
     }
-    /* a variable */
-  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { if( PARSER_STATE->sygus() && name[0]=='-' && 
-          name.find_first_not_of("0123456789", 1) == std::string::npos ){
-        //allow unary minus in sygus
-        expr = MK_CONST(Rational(name));
-      }else{
-        const bool isDefinedFunction =
-          PARSER_STATE->isDefinedFunction(name);
-        if(PARSER_STATE->isAbstractValue(name)) {
-          expr = PARSER_STATE->mkAbstractValue(name);
-        } else if(isDefinedFunction) {
-          expr = MK_EXPR(CVC4::kind::APPLY,
-                        PARSER_STATE->getFunction(name));
-        } else {
-          expr = PARSER_STATE->getVariable(name);
-          Type t = PARSER_STATE->getType(name);
-          if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
-            // don't require parentheses, immediately turn it into an apply
-            expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
-          }
-        }
-      }
-    }
 
     /* attributed expressions */
   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
@@ -2966,11 +2984,10 @@ constructorDef[CVC4::Datatype& type]
   std::string id;
   CVC4::DatatypeConstructor* ctor = NULL;
 }
-  : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE]
+  : symbol[id,CHECK_NONE,SYM_VARIABLE]
     { // make the tester
       std::string testerId("is-");
       testerId.append(id);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
       ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
@@ -2986,7 +3003,7 @@ selector[CVC4::DatatypeConstructor& ctor]
   std::string id;
   Type t, t2;
 }
-  : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
+  : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
     { ctor.addArg(id, t);
       Debug("parser-idt") << "selector: " << id.c_str()
                           << " of type " << t << std::endl;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index aeabdbac2..acfd886ce 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -337,6 +337,18 @@ bool Smt2::logicIsSet() {
   return d_logicSet;
 }
 
+Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
+  if(sygus() && name[0]=='-' && 
+    name.find_first_not_of("0123456789", 1) == std::string::npos) {
+    //allow unary minus in sygus
+    return getExprManager()->mkConst(Rational(name));
+  }else if(isAbstractValue(name)) {
+    return mkAbstractValue(name);
+  }else{
+    return Parser::getExpressionForNameAndType(name, t);
+  }
+}
+
 void Smt2::reset() {
   d_logicSet = false;
   d_logic = LogicInfo();
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index e470c8111..46f1c631b 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -87,6 +87,11 @@ public:
   bool isTheoryEnabled(Theory theory) const;
 
   bool logicIsSet();
+  
+  /**
+   * Returns the expression that name should be interpreted as. 
+   */
+  virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
 
   void reset();