From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 1 Apr 2010 20:06:10 +0000 (+0000)
Subject: Changing min/maxArity to use metakind info.
X-Git-Tag: cvc5-1.0.0~9145
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4918a518a69090ed0ba2547fb21cd8f418c648b;p=cvc5.git

Changing min/maxArity to use metakind info.
---

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index a2c90937b..6a2640080 100644
--- 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 9bcee54fd..93b8560d0 100644
--- 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);
       }
     }