Changing min/maxArity to use metakind info.

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a2c90937b602efff367e85a1a5f2c99caff8123a..6a2640080f4867660290809e550b52dd05c8fa9f 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -195,69 +195,11 @@ Expr ExprManager::mkVar(Type* type) {
 }
 
 unsigned ExprManager::minArity(Kind kind) {
-  // FIXME: should be implemented this way, but parser depends on *parse*-level.
-  // See bug 75.
-  //return metakind::getLowerBoundForKind(kind);
-  switch(kind) {
-  case SKOLEM:
-  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 MULT:
-  case XOR:
-    return 2;
-
-  case ITE:
-    return 3;
-
-  default:
-    Unhandled(kind);
-  }
+  return metakind::getLowerBoundForKind(kind);
 }
 
 unsigned ExprManager::maxArity(Kind kind) {
-  // FIXME: should be implemented this way, but parser depends on *parse*-level.
-  // See bug 75.
-  //return metakind::getUpperBoundForKind(kind);
-  switch(kind) {
-  case SKOLEM:
-  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 MULT:
-  case OR:
-    return UINT_MAX;
-
-  default:
-    Unhandled(kind);
-  }
+  return metakind::getUpperBoundForKind(kind);
 }
 
 NodeManager* ExprManager::getNodeManager() const {

diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 9bcee54fd6f07530423fb87e81614a778e59130a..93b8560d010fb4b47c05ec9d890510bbbfe4f5fd 100644 (file)
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -158,12 +158,12 @@ annotatedFormula[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK 
-    { PARSER_STATE->checkArity(kind, args.size());
-      if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
+    { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
         /* Unary AND/OR can be replaced with the argument.
               It just so happens expr should already by the only argument. */
         Assert( expr == args[0] );
       } else {
+        PARSER_STATE->checkArity(kind, args.size());
         expr = MK_EXPR(kind, args);
       }
     }