Finishing parser cleanup. Code is now review-ready.

3 files changed, 136 insertions, 6 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);
 }