Finishing parser cleanup. Code is now review-ready.

8 files changed, 186 insertions, 203 deletions

diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 0b0139118..4eda9805a 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -20,15 +20,17 @@
  *      Author: dejan
  */
 
-#include "expr/node.h"
+#include "context/context.h"
 #include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/node_manager.h"
 #include "expr/expr_manager.h"
-#include "context/context.h"
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/type.h"
 
 using namespace std;
 using namespace CVC4::context;
+using namespace CVC4::kind;
 
 namespace CVC4 {
 
@@ -115,10 +117,25 @@ FunctionType* ExprManager::mkFunctionType(Type* domain,
 /** Make a function type with input types from argTypes. */
 FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
                                           Type* range) {
+  Assert( argTypes.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkFunctionType(argTypes, range);
 }
 
+FunctionType*
+ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
+  Assert( sorts.size() >= 2 );
+  NodeManagerScope nms(d_nodeManager);
+  return d_nodeManager->mkFunctionType(sorts);
+}
+
+FunctionType*
+ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
+  Assert( sorts.size() >= 1 );
+  NodeManagerScope nms(d_nodeManager);
+  return d_nodeManager->mkPredicateType(sorts);
+}
+
 Type* ExprManager::mkSort(const std::string& name) {
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkSort(name);
@@ -134,6 +151,69 @@ Expr ExprManager::mkVar(Type* type) {
   return Expr(this, new Node(d_nodeManager->mkVar(type)));
 }
 
+unsigned int ExprManager::minArity(Kind kind) {
+  switch(kind) {
+  case FALSE:
+  case SKOLEM:
+  case TRUE:
+  case VARIABLE:
+    return 0;
+
+  case AND:
+  case NOT:
+  case OR:
+    return 1;
+
+  case APPLY_UF:
+  case DISTINCT:
+  case EQUAL:
+  case IFF:
+  case IMPLIES:
+  case PLUS:
+  case XOR:
+    return 2;
+
+  case ITE:
+    return 3;
+
+  default:
+    Unhandled(kind);
+  }
+}
+
+unsigned int ExprManager::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_UF:
+  case DISTINCT:
+  case PLUS:
+  case OR:
+    return UINT_MAX;
+
+  default:
+    Unhandled(kind);
+  }
+}
+
+
 NodeManager* ExprManager::getNodeManager() const {
   return d_nodeManager;
 }
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 3c73e1ced..f2009ad80 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -99,11 +99,26 @@ public:
     mkFunctionType(Type* domain,
                    Type* range);
 
-  /** Make a function type with input types from argTypes. */
+  /** Make a function type with input types from argTypes. <code>argTypes</code>
+   * must have at least one element. */
   FunctionType*
     mkFunctionType(const std::vector<Type*>& argTypes,
                    Type* range);
 
+  /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
+   * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
+   * least 2 elements.
+   */
+  FunctionType*
+    mkFunctionType(const std::vector<Type*>& sorts);
+
+  /** Make a predicate type with input types from <code>sorts</code>. The result with
+   * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
+   * least one element.
+   */
+  FunctionType*
+    mkPredicateType(const std::vector<Type*>& sorts);
+
   /** Make a new sort with the given name. */
   Type* mkSort(const std::string& name);
 
@@ -111,6 +126,12 @@ public:
   Expr mkVar(Type* type, const std::string& name);
   Expr mkVar(Type* type);
 
+  /** Returns the minimum arity of the given kind. */
+  static unsigned int minArity(Kind kind);
+
+  /** Returns the maximum arity of the given kind. */
+  static unsigned int maxArity(Kind kind);
+
 private:
   /** The context */
   context::Context* d_ctxt;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c51c7fb77..f2718a06c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -293,10 +293,25 @@ public:
   /** Make a function type from domain to range. */
   inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
 
-  /** Make a function type with input types from argTypes. */
+  /** Make a function type with input types from argTypes. <code>argTypes</code>
+   * must have at least one element. */
   inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
                                       Type* range) const;
 
+  /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
+   * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
+   * least 2 elements.
+   */
+  inline FunctionType*
+    mkFunctionType(const std::vector<Type*>& sorts);
+
+  /** Make a predicate type with input types from <code>sorts</code>. The result with
+   * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
+   * least one element.
+   */
+  inline FunctionType*
+    mkPredicateType(const std::vector<Type*>& sorts);
+
   /** Make a new sort with the given name. */
   inline Type* mkSort(const std::string& name) const;
 
@@ -437,6 +452,20 @@ NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
   return new FunctionType(argTypes, range);
 }
 
+inline FunctionType*
+NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
+  Assert( sorts.size() >= 2 );
+  std::vector<Type*> argTypes(sorts);
+  Type* rangeType = argTypes.back();
+  argTypes.pop_back();
+  return mkFunctionType(argTypes,rangeType);
+}
+
+inline FunctionType*
+NodeManager::mkPredicateType(const std::vector<Type*>& sorts) {
+  Assert( sorts.size() >= 1 );
+  return mkFunctionType(sorts,booleanType());
+}
 inline Type* NodeManager::mkSort(const std::string& name) const {
   return new SortType(name);
 }
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index f32da2eac..4cb4d577b 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -133,7 +133,9 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
   Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* A sort declaration (e.g., "T : TYPE") */
-    TYPE_TOK { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); }
+    TYPE_TOK 
+    { ANTLR_INPUT->newSorts(idList); 
+      t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
     type[t] { ANTLR_INPUT->mkVars(idList,t); }
   ;
@@ -144,21 +146,21 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
  */
 type[CVC4::Type*& t]
 @init {
+  Type* t2;
   std::vector<Type*> typeList;
   Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
   : /* Simple type */
     baseType[t]
   | /* Single-parameter function type */
-    baseType[t] { typeList.push_back(t); }
-    ARROW_TOK baseType[t] 
-    { t = ANTLR_INPUT->functionType(typeList,t); }
+    baseType[t] ARROW_TOK baseType[t2] 
+    { t = EXPR_MANAGER->mkFunctionType(t,t2); }
   | /* Multi-parameter function type */
     LPAREN baseType[t]
     { typeList.push_back(t); }
     (COMMA baseType[t] { typeList.push_back(t); } )+
     RPAREN ARROW_TOK baseType[t]
-    { t = ANTLR_INPUT->functionType(typeList,t); }
+    { t = EXPR_MANAGER->mkFunctionType(typeList,t); }
   ;
 
 /**
@@ -198,7 +200,7 @@ baseType[CVC4::Type*& t]
   std::string id;
   Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
 }
-  : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); }
+  : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); }
   | typeSymbol[t]
   ;
 
@@ -415,9 +417,9 @@ functionSymbol[CVC4::Expr& f]
   Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
   std::string name;
 }
-  : identifier[name,CHECK_DECLARED,SYM_FUNCTION]
+  : identifier[name,CHECK_DECLARED,SYM_VARIABLE]
     { ANTLR_INPUT->checkFunction(name);
-      f = ANTLR_INPUT->getFunction(name); }
+      f = ANTLR_INPUT->getVariable(name); }
   ;
 
 
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 06faf5106..01de4ea4f 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -163,7 +163,6 @@ Expr Input::getSymbol(const std::string& name, SymbolType type) {
   switch( type ) {
 
   case SYM_VARIABLE: // Functions share var namespace
-  case SYM_FUNCTION:
     return d_varSymbolTable.getObject(name);
 
   default:
@@ -176,10 +175,6 @@ Expr Input::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Expr Input::getFunction(const std::string& name) {
-  return getSymbol(name, SYM_FUNCTION);
-}
-
 Type*
 Input::getType(const std::string& var_name,
                      SymbolType type) {
@@ -201,46 +196,12 @@ bool Input::isBoolean(const std::string& name) {
 
 /* Returns true if name is bound to a function. */
 bool Input::isFunction(const std::string& name) {
-  return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction();
+  return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction();
 }
 
 /* Returns true if name is bound to a function returning boolean. */
 bool Input::isPredicate(const std::string& name) {
-  return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate();
-}
-
-Type*
-Input::functionType(Type* domainType,
-                          Type* rangeType) {
-  return d_exprManager->mkFunctionType(domainType,rangeType);
-}
-
-Type*
-Input::functionType(const std::vector<Type*>& argTypes,
-                          Type* rangeType) {
-  Assert( argTypes.size() > 0 );
-  return d_exprManager->mkFunctionType(argTypes,rangeType);
-}
-
-Type*
-Input::functionType(const std::vector<Type*>& sorts) {
-  Assert( sorts.size() > 0 );
-  if( sorts.size() == 1 ) {
-    return sorts[0];
-  } else {
-    std::vector<Type*> argTypes(sorts);
-    Type* rangeType = argTypes.back();
-    argTypes.pop_back();
-    return functionType(argTypes,rangeType);
-  }
-}
-
-Type* Input::predicateType(const std::vector<Type*>& sorts) {
-  if(sorts.size() == 0) {
-    return d_exprManager->booleanType();
-  } else {
-    return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType());
-  }
+  return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate();
 }
 
 Expr 
@@ -303,80 +264,9 @@ Input::newSorts(const std::vector<std::string>& names) {
   return types;
 }
 
-BooleanType* Input::booleanType() {
-  return d_exprManager->booleanType();
-}
-
-KindType* Input::kindType() {
-  return d_exprManager->kindType();
-}
-
-unsigned int Input::minArity(Kind kind) {
-  switch(kind) {
-  case FALSE:
-  case SKOLEM:
-  case TRUE:
-  case VARIABLE:
-    return 0;
-
-  case AND:
-  case NOT:
-  case OR:
-    return 1;
-
-  case APPLY_UF:
-  case DISTINCT:
-  case EQUAL:
-  case IFF:
-  case IMPLIES:
-  case PLUS:
-  case XOR:
-    return 2;
-
-  case ITE:
-    return 3;
-
-  default:
-    Unhandled(kind);
-  }
-}
-
-unsigned int Input::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_UF:
-  case DISTINCT:
-  case PLUS:
-  case OR:
-    return UINT_MAX;
-
-  default:
-    Unhandled(kind);
-  }
-}
-
 bool Input::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
-  case SYM_VARIABLE: // Functions share var namespace
-  case SYM_FUNCTION:
+  case SYM_VARIABLE:
     return d_varSymbolTable.isBound(name);
   case SYM_SORT:
     return d_sortTable.isBound(name);
@@ -427,8 +317,8 @@ void Input::checkArity(Kind kind, unsigned int numArgs)
     return;
   }
 
-  unsigned int min = minArity(kind);
-  unsigned int max = maxArity(kind);
+  unsigned int min = d_exprManager->minArity(kind);
+  unsigned int max = d_exprManager->maxArity(kind);
 
   if( numArgs < min || numArgs > max ) {
     stringstream ss;
diff --git a/src/parser/input.h b/src/parser/input.h
index 42a94ab41..90cdc4e8d 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -66,8 +66,6 @@ inline std::string toString(DeclarationCheck check) {
 enum SymbolType {
   /** Variables */
   SYM_VARIABLE,
-  /** Functions */
-  SYM_FUNCTION,
   /** Sorts */
   SYM_SORT
 };
@@ -77,7 +75,6 @@ enum SymbolType {
 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();
   }
@@ -207,13 +204,6 @@ public:
     Expr getVariable(const std::string& var_name);
 
     /**
-     * Returns a function, given a name and a type.
-     * @param name the name of the function
-     * @return the function expression
-     */
-    Expr getFunction(const std::string& name);
-
-    /**
      * Returns a sort, given a name
      */
     Type* getSort(const std::string& sort_name);
@@ -278,30 +268,6 @@ public:
     /** Remove a variable definition (e.g., from a let binding). */
     void undefineVar(const std::string& name);
 
-    /** Returns a function type over the given domain and range types. */
-    Type* functionType(Type* domain, Type* range);
-
-    /** Returns a function type over the given types. argTypes must be
-        non-empty. */
-    Type* functionType(const std::vector<Type*>& argTypes,
-                             Type* rangeType);
-
-    /**
-     * Returns a function type over the given types. If types has only
-     * one element, then the type is just types[0].
-     *
-     * @param types a non-empty list of input and output types.
-     */
-    Type* functionType(const std::vector<Type*>& types);
-
-    /**
-     * Returns a predicate type over the given sorts. If sorts is empty,
-     * then the type is just BOOLEAN.
-
-     * @param sorts a list of input types
-     */
-    Type* predicateType(const std::vector<Type*>& sorts);
-
     /**
      * Creates a new sort with the given name.
      */
@@ -322,18 +288,6 @@ public:
     /** Is the symbol bound to a predicate? */
     bool isPredicate(const std::string& name);
 
-    /** Returns the boolean type. */
-    BooleanType* booleanType();
-
-    /** Returns the kind type (i.e., the type of types). */
-    KindType* kindType();
-
-    /** Returns the minimum arity of the given kind. */
-    static unsigned int minArity(Kind kind);
-
-    /** Returns the maximum arity of the given kind. */
-    static unsigned int maxArity(Kind kind);
-
     /** Throws a <code>ParserException</code> with the given error message.
      * Implementations should fill in the <code>ParserException</code> with
      * line number information, etc. */
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 56bedce81..d03cbf47e 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -255,7 +255,7 @@ predicateName[std::string& name, CVC4::parser::DeclarationCheck check]
  * @param check what kind of check to do with the symbol
  */
 functionName[std::string& name, CVC4::parser::DeclarationCheck check]
-  :  identifier[name,check,SYM_FUNCTION] 
+  :  identifier[name,check,SYM_VARIABLE] 
   ;
 
 /**
@@ -267,7 +267,7 @@ functionSymbol[CVC4::Expr& fun]
 }
   : functionName[name,CHECK_DECLARED]
     { ANTLR_INPUT->checkFunction(name);
-      fun = ANTLR_INPUT->getFunction(name); }
+      fun = ANTLR_INPUT->getVariable(name); }
   ;
   
 /**
@@ -277,8 +277,6 @@ attribute
   :  ATTR_IDENTIFIER
   ;
 
-
-
 functionDeclaration
 @declarations {
   std::string name;
@@ -288,7 +286,11 @@ functionDeclaration
       t = sortSymbol // require at least one sort
     { sorts.push_back(t); }
       sortList[sorts] RPAREN_TOK
-    { t = ANTLR_INPUT->functionType(sorts);
+    { if( sorts.size() == 1 ) {
+        Assert( t == sorts[0] ); 
+      } else {
+        t = EXPR_MANAGER->mkFunctionType(sorts);
+      }
       ANTLR_INPUT->mkVar(name, t); } 
   ;
               
@@ -301,7 +303,12 @@ predicateDeclaration
   std::vector<Type*> p_sorts;
 }
   : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
-    { Type *t = ANTLR_INPUT->predicateType(p_sorts);
+    { Type *t;
+      if( p_sorts.empty() ) {
+        t = EXPR_MANAGER->booleanType();
+      } else { 
+        t = EXPR_MANAGER->mkPredicateType(p_sorts);
+      }
       ANTLR_INPUT->mkVar(name, t); } 
   ;
 
@@ -395,7 +402,7 @@ fun_identifier[std::string& id,
     { id = AntlrInput::tokenText($FUN_IDENTIFIER);
       Debug("parser") << "fun_identifier: " << id
                       << " check? " << toString(check) << std::endl;
-      ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
+      ANTLR_INPUT->checkDeclaration(id, check); }
   ;
 
 
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index b7c58ba99..6e2adb356 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -27,27 +27,6 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace std;
 
-/* Set up declaration context for expr inputs */
-
-void setupContext(Input* input) {
-  /* a, b, c: BOOLEAN */
-  input->mkVar("a",(Type*)input->booleanType());
-  input->mkVar("b",(Type*)input->booleanType());
-  input->mkVar("c",(Type*)input->booleanType());
-  /* t, u, v: TYPE */
-  Type *t = input->newSort("t");
-  Type *u = input->newSort("u");
-  Type *v = input->newSort("v");
-  /* f : t->u; g: u->v; h: v->t; */
-  input->mkVar("f", input->functionType(t,u));
-  input->mkVar("g", input->functionType(u,v));
-  input->mkVar("h", input->functionType(v,t));
-  /* x:t; y:u; z:v; */
-  input->mkVar("x",t);
-  input->mkVar("y",u);
-  input->mkVar("z",v);
-}
-
 
 /************************** CVC test inputs ********************************/
 
@@ -162,6 +141,27 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
 class ParserBlack : public CxxTest::TestSuite {
   ExprManager *d_exprManager;
 
+  /* Set up declaration context for expr inputs */
+
+  void setupContext(Input* input) {
+    /* a, b, c: BOOLEAN */
+    input->mkVar("a",(Type*)d_exprManager->booleanType());
+    input->mkVar("b",(Type*)d_exprManager->booleanType());
+    input->mkVar("c",(Type*)d_exprManager->booleanType());
+    /* t, u, v: TYPE */
+    Type *t = input->newSort("t");
+    Type *u = input->newSort("u");
+    Type *v = input->newSort("v");
+    /* f : t->u; g: u->v; h: v->t; */
+    input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u));
+    input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v));
+    input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t));
+    /* x:t; y:u; z:v; */
+    input->mkVar("x",t);
+    input->mkVar("y",u);
+    input->mkVar("z",v);
+  }
+
   void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) {
     for(int i = 0; i < numInputs; ++i) {
       try {