Preliminary support for types in parser

8 files changed, 625 insertions, 317 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index fe906cbe0..3ecde0169 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -fvisibility=hidden
+AM_CXXFLAGS = -Wall -fvisibility=hidden -Wno-deprecated
 
 SUBDIRS = smt cvc
 
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 34691dc33..5a9af8d4a 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -21,11 +21,13 @@
  */
 
 #include <iostream>
+#include <limits.h>
 
 #include "antlr_parser.h"
 #include "util/output.h"
 #include "util/Assert.h"
 #include "expr/command.h"
+#include "expr/type.h"
 
 using namespace std;
 using namespace CVC4;
@@ -46,9 +48,58 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
   antlr::LLkParser(lexer, k) {
 }
 
-Expr AntlrParser::getVariable(std::string var_name) {
-  Expr e = d_varSymbolTable.getObject(var_name);
-  return e;
+Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
+  Assert( isDeclared(name,type) );
+  switch( type ) {
+  case SYM_VARIABLE: // Predicates and functions share var namespace
+  // case SYM_PREDICATE:
+  case SYM_FUNCTION:
+    return d_varSymbolTable.getObject(name);
+  default:
+    Unhandled("Unhandled symbol type!");
+  }
+}
+
+Expr AntlrParser::getVariable(std::string name) {
+  return getSymbol(name,SYM_VARIABLE);
+}
+
+Expr AntlrParser::getFunction(std::string name) {
+  return getSymbol(name,SYM_FUNCTION);
+}
+
+// Expr AntlrParser::getPredicate(std::string name) {
+//   return getSymbol(name,SYM_PREDICATE);
+// }
+
+const Type* 
+AntlrParser::getType(std::string var_name, 
+                     SymbolType type) {
+  Assert( isDeclared(var_name, type) );
+  const Type* t = d_varTypeTable.getObject(var_name);
+  return t;
+}
+
+const Type* AntlrParser::getSort(std::string name) {
+  Assert( isDeclared(name,SYM_SORT) );
+  const Type* t = d_sortTable.getObject(name);
+  return t;
+}
+
+/* Returns true if name is bound to a boolean variable. */
+bool AntlrParser::isBoolean(std::string name) {
+  return isDeclared(name,SYM_VARIABLE) && getType(name)->isBoolean();
+}
+
+/* Returns true if name is bound to a function. */
+bool AntlrParser::isFunction(std::string name) {
+  return isDeclared(name,SYM_FUNCTION) && getType(name)->isFunction();
+}
+
+/* Returns true if name is either a boolean variable OR a function
+   returning boolean. */
+bool AntlrParser::isPredicate(std::string name) {
+  return isDeclared(name,SYM_FUNCTION) && getType(name)->isPredicate();
 }
 
 Expr AntlrParser::getTrueExpr() const {
@@ -60,7 +111,9 @@ Expr AntlrParser::getFalseExpr() const {
 }
 
 Expr AntlrParser::mkExpr(Kind kind, const Expr& child) {
-  return d_exprManager->mkExpr(kind, child);
+  Expr result = d_exprManager->mkExpr(kind, child);
+  Debug("parser") << "mkExpr() => " << result << std::endl;
+  return result;
 }
 
 Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) {
@@ -82,50 +135,173 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector<Expr>& children) {
   return result;
 }
 
-void AntlrParser::newFunction(std::string name, 
-                               const std::vector< std::string>& sorts) {
-  // FIXME: Need to actually create a function type
-  d_varSymbolTable.bindName(name, d_exprManager->mkVar());
+const FunctionType* 
+AntlrParser::functionType(const Type* domainType, 
+                          const Type* rangeType) {
+  return d_exprManager->mkFunctionType(domainType,rangeType);
 }
 
-void AntlrParser::newFunctions(const std::vector<std::string>& names, 
-                               const std::vector< std::string>& sorts) {
-  for(unsigned i = 0; i < names.size(); ++i) {
-    newFunction(names[i], sorts);
+const FunctionType* 
+AntlrParser::functionType(const std::vector<const Type*>& argTypes, 
+                          const Type* rangeType) {
+  Assert( argTypes.size() > 0 );
+  return d_exprManager->mkFunctionType(argTypes,rangeType);
+}
+
+const FunctionType* 
+AntlrParser::functionType(const std::vector<const Type*>& sorts) {
+  Assert( sorts.size() > 1 );
+  std::vector<const Type*> argTypes(sorts);
+  const Type* rangeType = argTypes.back();
+  argTypes.pop_back();
+  return functionType(argTypes,rangeType);
+}
+
+Expr AntlrParser::newFunction(std::string name, 
+                              const std::vector<const Type*>& sorts) {
+  Assert( sorts.size() > 0 );
+  if( sorts.size() == 1 ) {
+    return mkVar(name, sorts[0]);
+  } else {
+    return mkVar(name, functionType(sorts));
   }
 }
 
-void AntlrParser::newPredicate(std::string name,
-                               const std::vector<std::string>& sorts) {
-  Debug("parser") << "newPredicate(" << name << ")" << std::endl;
+const std::vector<Expr>
+AntlrParser::newFunctions(const std::vector<std::string>& names, 
+                          const std::vector<const Type*>& sorts) {
+  const FunctionType* t = functionType(sorts);
+  return mkVars(names, t);
+}
+
+const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
   if(sorts.size() == 0) {
-    d_varSymbolTable.bindName(name, d_exprManager->mkVar());
+    return d_exprManager->booleanType();
   } else {
-    Unhandled("Non unary predicate not supported yet!");
+    return d_exprManager->mkFunctionType(sorts,d_exprManager->booleanType());
+  }
+}
+
+Expr
+AntlrParser::newPredicate(std::string name,
+                          const std::vector<const Type*>& sorts) {
+  const Type* t = predicateType(sorts);
+  return mkVar(name, t);
+}
+
+const std::vector<Expr>
+AntlrParser::newPredicates(const std::vector<std::string>& names,
+                                const std::vector<const Type*>& sorts) {
+  const Type* t = predicateType(sorts);
+  return mkVars(names, t);
+}
+
+Expr 
+AntlrParser::mkVar(const std::string name, const Type* type) {
+  Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
+  Assert( !isDeclared(name) ) ;
+  Expr expr = d_exprManager->mkVar(type);
+  d_varSymbolTable.bindName(name, expr);
+  d_varTypeTable.bindName(name,type);
+  Assert( isDeclared(name) ) ;
+  return expr;
+}
+
+const std::vector<Expr> 
+AntlrParser::mkVars(const std::vector<std::string> names, 
+                    const Type* type) {
+  std::vector<Expr> vars;
+  for(unsigned i = 0; i < names.size(); ++i) {
+    vars.push_back(mkVar(names[i], type));
   }
+  return vars;
 }
 
-void AntlrParser::newPredicates(const std::vector<std::string>& names,
-                                const std::vector<std::string>& sorts) {
+
+const Type* 
+AntlrParser::newSort(std::string name) {
+  Debug("parser") << "newSort(" << name << ")" << std::endl;
+  Assert( !isDeclared(name,SYM_SORT) ) ;
+  const Type* type = d_exprManager->mkSort(name);
+  d_sortTable.bindName(name,type);
+  Assert( isDeclared(name,SYM_SORT) ) ;
+  return type;
+}
+
+const std::vector<const Type*>
+AntlrParser::newSorts(const std::vector<std::string>& names) {
+  std::vector<const Type*> types;
   for(unsigned i = 0; i < names.size(); ++i) {
-    newPredicate(names[i], sorts);
+    types.push_back(newSort(names[i]));
   }
+  return types;
 }
 
-bool AntlrParser::isSort(std::string name) {
-  return d_sortTable.isBound(name);
+const BooleanType* AntlrParser::booleanType() {
+  return d_exprManager->booleanType(); 
 }
 
-void AntlrParser::newSort(std::string name) {
-  Assert( !isSort(name) ) ;
-  // Trivial binding
-  d_sortTable.bindName(name,name);
-  Assert( isSort(name) ) ;
+const KindType* AntlrParser::kindType() {
+  return d_exprManager->kindType(); 
 }
 
-void AntlrParser::newSorts(const std::vector<std::string>& names) {
-  for(unsigned i = 0; i < names.size(); ++i) {
-    newSort(names[i]);
+unsigned int AntlrParser::minArity(Kind kind) {
+  switch(kind) {
+  case FALSE:
+  case SKOLEM:
+  case TRUE:
+  case VARIABLE:
+    return 0;
+
+  case NOT:
+    return 1;
+
+  case AND:
+  case APPLY:
+  case EQUAL: 
+  case IFF:
+  case IMPLIES:
+  case PLUS:
+  case OR:
+  case XOR:
+    return 2;
+
+  case ITE:
+    return 3;
+
+  default:
+    Unhandled("kind in minArity");
+  }
+}
+
+unsigned int AntlrParser::maxArity(Kind kind) {
+  switch(kind) {
+  case FALSE:
+  case SKOLEM:
+  case TRUE:
+  case VARIABLE:
+    return 0;
+
+  case NOT:
+    return 1;
+
+  case EQUAL: 
+  case IFF:
+  case IMPLIES:
+  case XOR:
+    return 2;
+
+  case ITE:
+    return 3;
+
+  case AND:
+  case APPLY:
+  case PLUS:
+  case OR:
+    return UINT_MAX;
+
+  default:
+    Unhandled("kind in minArity");
   }
 }
 
@@ -135,8 +311,12 @@ void AntlrParser::setExpressionManager(ExprManager* em) {
 
 bool AntlrParser::isDeclared(string name, SymbolType type) {
   switch(type) {
-  case SYM_VARIABLE:
+  case SYM_VARIABLE: // Predicates and functions share var namespace
+  // case SYM_PREDICATE:
+  case SYM_FUNCTION:
     return d_varSymbolTable.isBound(name);
+  case SYM_SORT:
+    return d_sortTable.isBound(name);
   default:
     Unhandled("Unhandled symbol type!");
   }
@@ -149,25 +329,14 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
                                  LT(1).get()->getColumn());
 }
 
-bool AntlrParser::checkDeclaration(string varName, DeclarationCheck check) {
-  switch(check) {
-  case CHECK_DECLARED:
-    return isDeclared(varName, SYM_VARIABLE);
-  case CHECK_UNDECLARED:
-    return !isDeclared(varName, SYM_VARIABLE);
-  case CHECK_NONE:
-    return true;
-  default:
-    Unhandled("Unknown check type!");
-  }
-}
-
-bool AntlrParser::checkSort(std::string name, DeclarationCheck check) {
+bool AntlrParser::checkDeclaration(string varName, 
+                                   DeclarationCheck check,
+                                   SymbolType type) {
   switch(check) {
   case CHECK_DECLARED:
-    return isSort(name);
+    return isDeclared(varName, type);
   case CHECK_UNDECLARED:
-    return !isSort(name);
+    return !isDeclared(varName, type);
   case CHECK_NONE:
     return true;
   default:
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 5a7291be6..3cfe4fc5d 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -31,6 +31,8 @@
 namespace CVC4 {
 
 class Command;
+class Type;
+class FunctionType;
 
 namespace parser {
 
@@ -110,23 +112,13 @@ protected:
    * @return the variable expression
    */
   Expr getVariable(std::string var_name);
+  Expr getFunction(std::string var_name);
+  /* Expr getPredicate(std::string var_name); */
 
   /**
-   * Return true if the the declaration policy we want to enforce is true.
-   * @param varName the symbol to check
-   * @oaram check the kind of check to perform
-   * @return true if the check holds
+   * Returns a sort, given a name
    */
-  bool checkDeclaration(std::string varName, DeclarationCheck check);
-
-  /**
-   * Return true if the the declaration policy we want to enforce is true
-   * on the given sort name.
-   * @param name the sort symbol to check
-   * @oaram check the kind of check to perform
-   * @return true if the check holds
-   */
-  bool checkSort(std::string name, DeclarationCheck check);
+  const Type* getSort(std::string sort_name);
 
   /**
    * Types of symbols.
@@ -135,9 +127,11 @@ protected:
     /** Variables */
     SYM_VARIABLE,
     /** Predicates */
-    SYM_PREDICATE,
+    /* SYM_PREDICATE, */
     /** Functions */
-    SYM_FUNCTION
+    SYM_FUNCTION,
+    /** Sorts */
+    SYM_SORT
   };
 
   /**
@@ -147,10 +141,19 @@ protected:
   bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
 
   /**
-   * Checks if the sort has been declared.
-   * @param the sort name
+   * Return true if the the declaration policy we want to enforce is true.
+   * @param varName the symbol to check
+   * @oaram check the kind of check to perform
+   * @return true if the check holds
    */
-  bool isSort(std::string name);
+  bool checkDeclaration(std::string varName, 
+                        DeclarationCheck check,
+                        SymbolType type = SYM_VARIABLE);
+
+
+  /** Returns the type for the variable with the given name. */
+  const Type* getType(std::string var_name,
+                      SymbolType type = SYM_VARIABLE);
 
   /**
    * Returns the true expression.
@@ -199,14 +202,32 @@ protected:
    */
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
+  /* Create a new CVC4 variable expression . */
+  Expr mkVar(const std::string name, const Type* type);
+
+  const std::vector<Expr> 
+  mkVars(const std::vector<std::string> names, 
+         const Type* type);
+
+
+  /** Returns a function type over the given domain and range types. */
+  const FunctionType* functionType(const Type* domain, const Type* range);
+  /** Returns a function type over the given types. argTypes must have
+      at least 1 element. */
+  const FunctionType* functionType(const std::vector<const Type*>& argTypes,
+                             const Type* rangeType);
+  /** Returns a function type over the given types. types must have
+      at least 2 elements (i.e., a domain and range). */
+  const FunctionType* functionType(const std::vector<const Type*>& types);
+
   /**
    * Creates a new function over the given sorts. The function
    * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1].
    * @param name the name of the function
    * @param sorts the sorts
    */
-  void newFunction(std::string name, 
-                   const std::vector<std::string>& sorts);
+  Expr newFunction(std::string name, 
+                   const std::vector<const Type*>& sorts);
 
   /**
    * Creates new functions over the given sorts. Each function has
@@ -214,40 +235,75 @@ protected:
    * @param name the name of the function
    * @param sorts the sorts
    */
-  void newFunctions(const std::vector<std::string>& names, 
-                    const std::vector<std::string>& sorts);
+  const std::vector<Expr> 
+  newFunctions(const std::vector<std::string>& names, 
+               const std::vector<const Type*>& sorts);
+
+  /** Returns a predicate type over the given sorts. sorts must be 
+      non-empty. If sorts has size 1, then the type is just BOOLEAN. */
+  const Type* predicateType(const std::vector<const Type*>& sorts);
 
   /**
-   * Creates a new predicate over the given sorts. The predicate has
-   * arity sorts.size().
+   * Creates a new predicate (a function with range boolean) over the 
+   * given sorts. The predicate has sorts.size().
    * @param name the name of the predicate
    * @param sorts the sorts
    */
-  void newPredicate(std::string name, const std::vector<std::string>& sorts);
+  Expr newPredicate(std::string name, const std::vector<const Type*>& sorts);
 
   /**
-   * Creates new predicates over the given sorts. Each predicate
-   * will have arity sorts.size().
+   * Creates new predicates (a function with range boolean) over the 
+   * given sorts. Each predicate will have arity sorts.size().
    * @param p_names the names of the predicates
    */
-  void newPredicates(const std::vector<std::string>& names, const std::vector<
-      std::string>& sorts);
+  const std::vector<Expr>
+  newPredicates(const std::vector<std::string>& names,
+                const std::vector<const Type*>& sorts);
 
   /**
    * Creates a new sort with the given name.
    */
-  void newSort(std::string name);
+  const Type* newSort(std::string name);
 
   /**
    * Creates a new sorts with the given names.
    */
-  void newSorts(const std::vector<std::string>& names);
+  const std::vector<const Type*>
+  newSorts(const std::vector<std::string>& names);
+
+  bool isBoolean(std::string name);
+  bool isFunction(std::string name);
+  bool isPredicate(std::string name);
+
+  const BooleanType* booleanType();
+  const KindType* kindType();
+
+  unsigned int minArity(Kind kind);
+  unsigned int maxArity(Kind kind);
 
   /**
    * Returns the precedence rank of the kind.
    */
   static unsigned getPrecedence(Kind kind);
 
+  inline std::string toString(DeclarationCheck check) {
+    switch(check) {
+    case CHECK_NONE: return "CHECK_NONE";
+    case CHECK_DECLARED:  return "CHECK_DECLARED";
+    case CHECK_UNDECLARED: return "CHECK_UNDECLARED";
+    default: Unreachable();
+    }
+  }
+
+  inline std::string toString(SymbolType type) {
+    switch(type) {
+    case SYM_VARIABLE: return "SYM_VARIABLE";
+    case SYM_FUNCTION: return "SYM_FUNCTION";
+    case SYM_SORT: return "SYM_SORT";
+    default: Unreachable();
+    }
+  }
+
 private:
 
   /** The expression manager */
@@ -256,10 +312,20 @@ private:
   /** The symbol table lookup */
   SymbolTable<Expr> d_varSymbolTable;
 
+  /** A temporary hack: keep all the variable types in their own special
+      table. These should actually be Expr attributes. */
+  SymbolTable<const Type*> d_varTypeTable;
+
   /** The sort table */
-  SymbolTable<std::string> d_sortTable;
+  SymbolTable<const Type*> d_sortTable;
+
+  Expr getSymbol(std::string var_name, SymbolType type);
+
 };
 
+
+
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g
index afcc7597d..b5bf90015 100644
--- a/src/parser/cvc/cvc_lexer.g
+++ b/src/parser/cvc/cvc_lexer.g
@@ -39,6 +39,7 @@ options {
 tokens {
   // Types
   BOOLEAN       = "BOOLEAN";
+  TYPE          = "TYPE";
   // Boolean oparators
   AND           = "AND";
   IF            = "IF";
@@ -67,6 +68,8 @@ tokens {
 COMMA   : ',';
 IMPLIES : "=>";
 IFF     : "<=>";
+RIGHT_ARROW : "->";
+EQUAL   : "=";
 
 /**
  * Matches any letter ('a'-'z' and 'A'-'Z').
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 662888050..30df2d439 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -16,6 +16,8 @@
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
 #include "expr/command.h"
+#include "expr/type.h"
+#include "util/output.h"
 }
 
 header "post_include_cpp" {
@@ -68,29 +70,72 @@ parseExpr returns [CVC4::Expr expr]
 command returns [CVC4::Command* cmd = 0]
 {
   Expr f;
-  vector<string> ids;
+  Debug("parser") << "command: " << LT(1)->getText() << endl;
 }
   : ASSERT   f = formula  SEMICOLON { cmd = new AssertCommand(f);   }
   | QUERY    f = formula  SEMICOLON { cmd = new QueryCommand(f);    }
   | CHECKSAT f = formula  SEMICOLON { cmd = new CheckSatCommand(f); }
   | CHECKSAT              SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); }
-  | identifierList[ids, CHECK_UNDECLARED] COLON type {
-      // FIXME: switch on type (may not be predicates)
-      vector<string> sorts;
-      newPredicates(ids,sorts);
-      cmd = new DeclarationCommand(ids);
-    }
-    SEMICOLON
+  | cmd = declaration
   | EOF
   ;
 
 /**
- * Mathches a list of identifiers separated by a comma and puts them in the
+ * Match a declaration
+ */
+
+declaration returns [CVC4::DeclarationCommand* cmd]
+{
+  vector<string> ids;
+  const Type* t;
+  Debug("parser") << "declaration: " << LT(1)->getText() << endl;
+} 
+  : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON
+    { cmd = new DeclarationCommand(ids,t); }
+  ;
+
+/** Match the right-hand side of a declaration. Returns the type. */
+declType[std::vector<std::string>& idList] returns [const CVC4::Type* t]
+{
+  Debug("parser") << "declType: " << LT(1)->getText() << endl;
+}
+  : /* A sort declaration (e.g., "T : TYPE") */
+    TYPE { newSorts(idList); t = kindType(); }
+  | /* A variable declaration */
+    t = type { mkVars(idList,t); }
+  ;
+
+/**
+ * Match the type in a declaration and do the declaration binding.
+ * TODO: Actually parse sorts into Type objects.
+ */
+type returns  [const CVC4::Type* t]
+{
+  const Type *t1, *t2;
+  Debug("parser") << "type: " << LT(1)->getText() << endl;
+}
+  : /* Simple type */
+    t = baseType
+  | /* Single-parameter function type */
+    t1 = baseType RIGHT_ARROW t2 = baseType
+    { t = functionType(t1,t2); }
+  | /* Multi-parameter function type */
+    LPAREN t1 = baseType 
+    { std::vector<const Type*> argTypes;
+      argTypes.push_back(t1); }
+    (COMMA t1 = baseType { argTypes.push_back(t1); } )+ 
+    RPAREN RIGHT_ARROW t2 = baseType
+    { t = functionType(argTypes,t2); }
+  ;
+
+/**
+ * Matches a list of identifiers separated by a comma and puts them in the
  * given list.
  * @param idList the list to fill with identifiers.
  * @param check what kinds of check to perform on the symbols
  */
-identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_NONE]
+identifierList[std::vector<std::string>& idList, 
+               DeclarationCheck check = CHECK_NONE]
 {
   string id;
 }
@@ -102,10 +147,12 @@ identifierList[std::vector<std::string>& idList, DeclarationCheck check = CHECK_
 /**
  * Matches an identifier and returns a string.
  */
-identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
+identifier[DeclarationCheck check = CHECK_NONE,
+           SymbolType type = SYM_VARIABLE] 
+returns [std::string id]
   : x:IDENTIFIER
     { id = x->getText(); }
-    { checkDeclaration(id, check) }?
+    { checkDeclaration(id, check, type) }?
     exception catch [antlr::SemanticException& ex] {
       switch (check) {
         case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
@@ -119,8 +166,25 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
  * Matches a type.
  * TODO: parse more types
  */
-type
-  : BOOLEAN
+baseType returns [const CVC4::Type* t]
+{
+  std::string id;
+  Debug("parser") << "base type: " << LT(1)->getText() << endl;
+}
+  : BOOLEAN { t = booleanType(); }
+  | t = typeSymbol
+  ;
+
+/**
+ * Matches a type identifier
+ */
+typeSymbol returns [const CVC4::Type* t]
+{
+  std::string id;
+  Debug("parser") << "type symbol: " << LT(1)->getText() << endl;
+}
+  : id = identifier[CHECK_DECLARED,SYM_SORT]
+    { t = getSort(id); }
   ;
 
 /**
@@ -128,159 +192,197 @@ type
  * @return the expression representing the formula
  */
 formula returns [CVC4::Expr formula]
-  :  formula = boolFormula
+{
+  Debug("parser") << "formula: " << LT(1)->getText() << endl;
+}
+  :  formula = iffFormula
   ;
 
 /**
- * Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of
- * operands (primaryBoolFormulas) and operators (Kinds) and then calls the
- * createPrecedenceExpr method to build the expression using the precedence
- * and associativity of the operators.
- * @return the expression representing the formula
+ * Matches a comma-separated list of formulas
  */
-boolFormula returns [CVC4::Expr formula]
-  : formula = boolAndFormula
+formulaList[std::vector<CVC4::Expr>& formulas]
+{
+  Expr f;
+}
+  : f = formula { formulas.push_back(f); }
+    ( COMMA f = formula
+      { formulas.push_back(f); }
+    )*
   ;
 
 /**
- * Matches a Boolean AND formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IFF formula (right-associative)
  */
-boolAndFormula returns [CVC4::Expr andFormula]
+iffFormula returns [CVC4::Expr f]
 {
   Expr e;
-  vector<Expr> exprs;
+  Debug("parser") << "<=> formula: " << LT(1)->getText() << endl;
 }
-  : e = boolXorFormula { exprs.push_back(e); }
-      ( AND e = boolXorFormula { exprs.push_back(e); } )*
-    {
-      andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
-    }
+  : f = impliesFormula
+    ( IFF e = iffFormula
+        { f = mkExpr(CVC4::IFF, f, e); }
+    )?
   ;
 
 /**
- * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IMPLIES formula (right-associative)
  */
-boolXorFormula returns [CVC4::Expr xorFormula]
+impliesFormula returns [CVC4::Expr f]
 {
   Expr e;
-  vector<Expr> exprs;
+  Debug("parser") << "=> Formula: " << LT(1)->getText() << endl;
 }
-  : e = boolOrFormula { exprs.push_back(e); }
-      ( XOR e = boolOrFormula { exprs.push_back(e); } )*
-    {
-      xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
-    }
+  : f = orFormula 
+    ( IMPLIES e = impliesFormula
+        { f = mkExpr(CVC4::IFF, f, e); }
+    )?
   ;
 
 /**
- * Matches a Boolean OR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean OR formula (left-associative)
  */
-boolOrFormula returns [CVC4::Expr orFormula]
+orFormula returns [CVC4::Expr f]
 {
   Expr e;
   vector<Expr> exprs;
+  Debug("parser") << "OR Formula: " << LT(1)->getText() << endl;
 }
-  : e = boolImpliesFormula { exprs.push_back(e); }
-      ( OR e = boolImpliesFormula { exprs.push_back(e); } )*
+  : e = xorFormula { exprs.push_back(e); }
+      ( OR e = xorFormula { exprs.push_back(e); } )*
     {
-      orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+      f = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
     }
   ;
 
 /**
- * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
+ * Matches a Boolean XOR formula (left-associative)
  */
-boolImpliesFormula returns [CVC4::Expr impliesFormula]
+xorFormula returns [CVC4::Expr f]
 {
-  vector<Expr> exprs;
   Expr e;
+  Debug("parser") << "XOR formula: " << LT(1)->getText() << endl;
 }
-  : e = boolIffFormula { exprs.push_back(e); }
-    ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
+  : f = andFormula
+    ( XOR e = andFormula 
+      { f = mkExpr(CVC4::XOR,f, e); }
     )*
-    {
-      impliesFormula = exprs.back();
-      for (int i = exprs.size() - 2; i >= 0; -- i) {
-        impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
-      }
-    }
   ;
 
 /**
- * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
+ * Matches a Boolean AND formula (left-associative)
  */
-boolIffFormula returns [CVC4::Expr iffFormula]
+andFormula returns [CVC4::Expr f]
 {
   Expr e;
+  vector<Expr> exprs;
+  Debug("parser") << "AND Formula: " << LT(1)->getText() << endl;
 }
-  : iffFormula = primaryBoolFormula
-    ( IFF e = primaryBoolFormula
-        { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
-    )*
+  : e = notFormula { exprs.push_back(e); }
+    ( AND e = notFormula { exprs.push_back(e); } )*
+    {
+      f = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+    }
   ;
 
 /**
- * Parses a primary Boolean formula. A primary Boolean formula is either a
- * Boolean atom (variables and predicates) a negation of a primary Boolean
- * formula or a formula enclosed in parenthesis.
+ * Parses a NOT formula.
  * @return the expression representing the formula
  */
-primaryBoolFormula returns [CVC4::Expr formula]
-  : formula = boolAtom
-  | formula = iteFormula
-  | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); }
-  | LPAREN formula = boolFormula RPAREN
+notFormula returns [CVC4::Expr f]
+{
+  Debug("parser") << "NOT formula: " << LT(1)->getText() << endl;
+}
+  : /* negation */
+    NOT f = notFormula 
+    { f = mkExpr(CVC4::NOT, f); }
+  | /* a boolean atom */
+    f = predFormula
   ;
 
+predFormula returns [CVC4::Expr f]
+{
+  Debug("parser") << "predicate formula: " << LT(1)->getText() << endl;
+}
+  : { Expr e; }
+    f = term 
+    (EQUAL e = term
+      { f = mkExpr(CVC4::EQUAL, f, e); }
+    )?
+  ; // TODO: lt, gt, etc.
+
 /**
- * Parses an ITE boolean formula.
+ * Parses a term.
  */
-iteFormula returns [CVC4::Expr formula] 
+term returns [CVC4::Expr t]
 {
-  Expr iteCondition, iteThen, iteElse;
+  std::string name;
+  Debug("parser") << "term: " << LT(1)->getText() << endl;
 }
-  : IF iteCondition = boolFormula 
-    THEN iteThen = boolFormula
-    iteElse = iteElseFormula
-    ENDIF     
-    { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }  
+  : /* function application */
+    { isFunction(LT(1)->getText()) }? 
+    name = functionSymbol[CHECK_DECLARED]
+    {
+      std::vector<CVC4::Expr> args;
+      args.push_back( getFunction(name) ); 
+    }
+    LPAREN formulaList[args] RPAREN
+    // TODO: check arity
+    { t = mkExpr(CVC4::APPLY, args); }
+
+  | /* if-then-else */
+    t = iteTerm
+
+  | /* parenthesized sub-formula */
+    LPAREN t = formula RPAREN
+
+    /* constants */
+  | TRUE  { t = getTrueExpr(); }
+  | FALSE { t = getFalseExpr(); }
+
+  | /* variable */
+    name = identifier[CHECK_DECLARED]
+    { t = getVariable(name); }
   ;
 
 /**
- * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
+ * Parses an ITE term.
  */
-iteElseFormula returns [CVC4::Expr formula]
+iteTerm returns [CVC4::Expr t] 
 {
   Expr iteCondition, iteThen, iteElse;
+  Debug("parser") << "ite: " << LT(1)->getText() << endl;
 }
-  : ELSE formula = boolFormula
-  | ELSEIF iteCondition = boolFormula
-    THEN iteThen = boolFormula
-    iteElse = iteElseFormula
-    { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }
+  : IF iteCondition = formula 
+    THEN iteThen = formula
+    iteElse = iteElseTerm
+    ENDIF     
+    { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }  
   ;
 
 /**
- * Parses the Boolean atoms (variables and predicates).
- * @return the expression representing the atom.
+ * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ...
  */
-boolAtom returns [CVC4::Expr atom]
+iteElseTerm returns [CVC4::Expr t]
 {
-  string p;
+  Expr iteCondition, iteThen, iteElse;
+  Debug("parser") << "else: " << LT(1)->getText() << endl;
 }
-  : p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); }
-      exception catch [antlr::SemanticException ex] {
-        rethrow(ex, "Undeclared variable " + p);
-      }
-  | TRUE  { atom = getTrueExpr(); }
-  | FALSE { atom = getFalseExpr(); }
+  : ELSE t = formula
+  | ELSEIF iteCondition = formula
+    THEN iteThen = formula
+    iteElse = iteElseTerm
+    { t = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); }
   ;
 
 /**
- * Parses a predicate symbol (an identifier).
+ * Parses a function symbol (an identifier).
  * @param what kind of check to perform on the id
  * @return the predicate symol
  */
-predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
-  : pSymbol = identifier[check]
+functionSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string symbol]
+{
+  Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
+
+}  : symbol = identifier[check,SYM_FUNCTION]
   ;
diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g
index d71edfbc3..695b7b787 100644
--- a/src/parser/smt/smt_lexer.g
+++ b/src/parser/smt/smt_lexer.g
@@ -37,11 +37,11 @@ tokens {
   // Base SMT-LIB tokens
   DISTINCT      = "distinct";
   ITE           = "ite";
+  IF_THEN_ELSE  = "if_then_else";
   TRUE          = "true";
   FALSE         = "false";
   NOT           = "not";
   IMPLIES       = "implies";
-  IF_THEN_ELSE  = "if_then_else";
   AND           = "and";
   OR            = "or";
   XOR           = "xor";
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 47e275171..28101532b 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -19,6 +19,8 @@ header "post_include_hpp" {
 }
 
 header "post_include_cpp" {
+#include "expr/type.h"
+#include "util/output.h"
 #include <vector>
 
 using namespace std;
@@ -109,93 +111,63 @@ benchAttribute returns [Command* smt_command = 0]
   ;
 
 /**
- * Matches an identifier and returns a string.
- * @param check what kinds of check to do on the symbol
- * @return the id string
- */
-identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
-  : x:IDENTIFIER
-    { id = x->getText(); }
-    { checkDeclaration(id, check) }?
-    exception catch [antlr::SemanticException& ex] {
-      switch (check) {
-        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
-        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
-        default: throw ex;
-      }
-    }
-  ;
-
-/**
  * Matches an annotated formula.
  * @return the expression representing the formula
  */
 annotatedFormula returns [CVC4::Expr formula]
 {
+  Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
   Kind kind;
-  vector<Expr> children;
+  vector<Expr> args; 
 }
-  :  formula = annotatedAtom 
-  |  LPAREN kind = boolConnective annotatedFormulas[children] RPAREN 
-    { formula = mkExpr(kind, children);  }    
-    /* TODO: let, flet, quantifiers */
-  ;
+  : /* a built-in operator application */
+    LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
+    { args.size() >= minArity(kind) 
+      && args.size() <= maxArity(kind) }?
+    { formula = mkExpr(kind,args); }
+      exception catch [antlr::SemanticException& ex] {
+        stringstream ss;
+        ss << "Expected ";
+        if( args.size() < minArity(kind) ) {
+          ss << "at least " << minArity(kind) << " ";
+        } else {
+          ss << "at most " << maxArity(kind) << " ";
+        }
+        ss << "arguments for operator '" << kind << "'. ";
+        ss << "Found: " << args.size();
+        rethrow(ex, ss.str());
+      }
 
-/**
- * Matches a sequence of annotaed formulas and puts them into the formulas
- * vector.
- * @param formulas the vector to fill with formulas
- */   
-annotatedFormulas[std::vector<Expr>& formulas]
-{
-  Expr f;
-}
-  : ( f = annotatedFormula { formulas.push_back(f); } )+
-  ;
+  | /* A non-built-in function application */
+    { isFunction(LT(2)->getText()) }? 
+    { Expr f; }
+    LPAREN f = functionSymbol
+    { args.push_back(f); }
+    annotatedFormulas[args] RPAREN
+    // TODO: check arity
+    { formula = mkExpr(CVC4::APPLY,args); }
 
-/**
- * Matches an annotated proposition atom, which is either a propositional atom 
- * or built of other atoms using a predicate symbol.  
- * @return expression representing the atom
- */
-annotatedAtom returns [CVC4::Expr atom] 
-{ 
-  Kind kind;
-  string predName;
-  Expr pred;
-  vector<Expr> children;
-}
-  : atom = propositionalAtom  
-  | LPAREN kind = arithPredicate annotatedTerms[children] RPAREN
-    { atom = mkExpr(kind,children); }
-  | LPAREN pred = predicateSymbol
-    { children.push_back(pred); }
-    annotatedTerms[children] RPAREN
-    { atom = mkExpr(CVC4::APPLY,children); }
-  ;
+  | /* An ite expression */
+    LPAREN (ITE | IF_THEN_ELSE) 
+    { Expr test, trueExpr, falseExpr; }
+    test = annotatedFormula 
+    trueExpr = annotatedFormula
+    falseExpr = annotatedFormula
+    RPAREN
+    { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); }
 
-/** 
- * Matches an annotated term.
- * @return the expression representing the term 
- */
-annotatedTerm returns [CVC4::Expr term] 
-{ 
-  Kind kind;
-  Expr f, t1, t2;
-  vector<Expr> children;
-}
-  : term = baseTerm
-  | LPAREN f = functionSymbol
-    { children.push_back(f); }
-    annotatedTerms[children] RPAREN 
-    { term = mkExpr(CVC4::APPLY, children);  }
-  // | LPAREN kind = arithFunction annotatedTerms[children] RPAREN
-  //   { term = mkExpr(kind,children); }
-  | LPAREN ITE 
-    f = annotatedFormula 
-    t1 = annotatedTerm 
-    t2 = annotatedTerm RPAREN
-    { term = mkExpr(CVC4::ITE, f, t1, t2); }
+  | /* a parenthesized sub-formula */
+    LPAREN formula = annotatedFormula RPAREN
+
+  | /* a variable */
+    { std::string name; }
+    name = identifier[CHECK_DECLARED]
+    { formula = getVariable(name); }
+
+    /* constants */
+  | TRUE          { formula = getTrueExpr(); }
+  | FALSE         { formula = getFalseExpr(); }
+    /* TODO: let, flet, quantifiers, arithmetic constants */
   ;
 
 /**
@@ -203,50 +175,29 @@ annotatedTerm returns [CVC4::Expr term]
  * vector.
  * @param formulas the vector to fill with formulas
  */   
-annotatedTerms[std::vector<Expr>& terms]
-{
-  Expr t;
-}
-  : ( t = annotatedFormula { terms.push_back(t); } )+
-  ;
-
-baseTerm returns [CVC4::Expr term]
+annotatedFormulas[std::vector<Expr>& formulas]
 {
-  string name;
+  Expr f;
 }
-  : name = identifier[CHECK_DECLARED] { term = getVariable(name); }
-    /* TODO: constants */
+  : ( f = annotatedFormula { formulas.push_back(f); } )+
   ;
 
 /**
 * Matches on of the unary Boolean connectives.
 * @return the kind of the Bollean connective
 */
-boolConnective returns [CVC4::Kind kind]
+builtinOp returns [CVC4::Kind kind]
+{
+  Debug("parser") << "builtin: " << LT(1)->getText() << endl;
+}
   : NOT      { kind = CVC4::NOT;     }
   | IMPLIES  { kind = CVC4::IMPLIES; }
   | AND      { kind = CVC4::AND;     }
   | OR       { kind = CVC4::OR;      }
   | XOR      { kind = CVC4::XOR;     }
   | IFF      { kind = CVC4::IFF;     }
-  ;
-
-/**
- * Matches a propositional atom and returns the expression of the atom.
- * @return atom the expression of the atom
- */
-propositionalAtom returns [CVC4::Expr atom]
-{
-  std::string p;
-}
-   : atom = predicateSymbol
-   | TRUE          { atom = getTrueExpr(); }
-   | FALSE         { atom = getFalseExpr(); }
-   ;
-
-arithPredicate returns [CVC4::Kind kind]
-  : EQUAL { kind = CVC4::EQUAL; }
-    /* TODO: lt, gt */
+  | EQUAL    { kind = CVC4::EQUAL;   }
+    /* TODO: lt, gt, plus, minus, etc. */
   ;
 
 /**
@@ -258,22 +209,11 @@ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p]
   ;
 
 /**
- * Matches an previously declared predicate symbol (returning an Expr)
- */
-predicateSymbol returns [CVC4::Expr pred]
-{ 
-  string name;
-}
-  : name = predicateName[CHECK_DECLARED]
-    { pred = getVariable(name); }
-  ;
-
-/**
  * Matches a (possibly undeclared) function identifier (returning the string)
  * @param check what kind of check to do with the symbol
  */
 functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name]
-  :  name = identifier[check]
+  :  name = identifier[check,SYM_FUNCTION]
   ;
 
 /**
@@ -284,7 +224,7 @@ functionSymbol returns [CVC4::Expr fun]
   string name;
 }
   : name = functionName[CHECK_DECLARED]
-    { fun = getVariable(name); }
+    { fun = getFunction(name); }
   ;
   
 /**
@@ -299,19 +239,26 @@ attribute
  * @param check the check to perform on the name
  */
 sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] 
-  : name = identifier[CHECK_NONE] 
-    /* We pass CHECK_NONE to identifier, because identifier checks
-       in the variable namespace, not the sorts namespace. */
-    { checkSort(name,check) }?
+  : name = identifier[check,SYM_SORT] 
+  ;
+
+sortSymbol returns [const CVC4::Type* t]
+{ 
+  std::string name;
+}
+  : name = sortName { t = getSort(name); }
   ;
 
 functionDeclaration
 {
   string name;
-  vector<string> sorts;
+  const Type* t;
+  std::vector<const Type*> sorts;
 }
-  : LPAREN name = functionName[CHECK_UNDECLARED]
-        sortNames[sorts, CHECK_DECLARED] RPAREN
+  : LPAREN name = functionName[CHECK_UNDECLARED] 
+      t = sortSymbol // require at least one sort
+    { sorts.push_back(t); }
+      sortList[sorts] RPAREN
     { newFunction(name, sorts); } 
   ;
               
@@ -321,10 +268,9 @@ functionDeclaration
 predicateDeclaration
 {
   string p_name;
-  vector<string> p_sorts;
+  std::vector<const Type*> p_sorts;
 }
-  : LPAREN p_name = predicateName[CHECK_UNDECLARED] 
-        sortNames[p_sorts, CHECK_DECLARED] RPAREN
+  : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN
     { newPredicate(p_name, p_sorts); } 
   ;
 
@@ -339,12 +285,11 @@ sortDeclaration
 /**
  * Matches a sequence of sort symbols and fills them into the given vector.
  */
-sortNames[std::vector<std::string>& sorts,DeclarationCheck check = CHECK_NONE]
+sortList[std::vector<const Type*>& sorts]
 {
-  std::string name;
+  const Type* t;
 }
-  : ( name = sortName[check] 
-      { sorts.push_back(name); })* 
+  : ( t = sortSymbol { sorts.push_back(t); })* 
   ;
 
 /**
@@ -363,3 +308,28 @@ annotation
   : attribute (USER_VALUE)?
   ;
 
+/**
+ * Matches an identifier and returns a string.
+ * @param check what kinds of check to do on the symbol
+ * @return the id string
+ */
+identifier[DeclarationCheck check = CHECK_NONE, 
+           SymbolType type = SYM_VARIABLE] 
+returns [std::string id]
+{
+  Debug("parser") << "identifier: " << LT(1)->getText() 
+                  << " check? " << toString(check)
+                  << " type? " << toString(type) << endl;
+}
+  : x:IDENTIFIER
+    { id = x->getText(); }
+    { checkDeclaration(id, check,type) }?
+    exception catch [antlr::SemanticException& ex] {
+      switch (check) {
+        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
+        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+        default: throw ex;
+      }
+    }
+  ;
+
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index e4aec930e..d790a1c84 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -78,14 +78,12 @@ public:
 
   /**
    * Returns the last binding expression of the name.
+   * Requires the name to have a binding in the table.
    */
   ObjectType getObject(const std::string name) throw () {
-    ObjectType result;
     table_iterator find = d_nameBindings.find(name);
-    if(find != d_nameBindings.end()) {
-      result = find->second.top();
-    }
-    return result;
+    Assert(find != d_nameBindings.end());
+    return find->second.top();
   }
 
   /**