diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-01 20:06:10 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-01 20:06:10 +0000 |
commit | f4918a518a69090ed0ba2547fb21cd8f418c648b (patch) | |
tree | 51dc3b180d20ef8358eba3f1ca4d66d17ba446c2 /src/expr | |
parent | ed25d7b7527691442ab48d02353e20c87ab8e2da (diff) |
Changing min/maxArity to use metakind info.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 62 |
1 files changed, 2 insertions, 60 deletions
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 { |