From 9aab4da2460b62273ac937ad96b7b6695b904e0d Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Sat, 11 Jul 2020 01:55:31 -0300 Subject: [PATCH] Adding test for whether a kind is n-ary (#4718) --- src/expr/expr_manager_template.cpp | 5 +++++ src/expr/expr_manager_template.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 7bec489a3..445ca9ee7 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1029,6 +1029,11 @@ unsigned ExprManager::maxArity(Kind kind) { return metakind::getUpperBoundForKind(kind); } +bool ExprManager::isNAryKind(Kind fun) +{ + return ExprManager::maxArity(fun) == expr::NodeValue::MAX_CHILDREN; +} + NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index db5d22fa8..3f180e951 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -574,6 +574,11 @@ class CVC4_PUBLIC ExprManager { /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + /** Whether a kind is n-ary. The test is based on n-ary kinds having their + * maximal arity as the maximal possible number of children of a node. + **/ + static bool isNAryKind(Kind fun); + /** * Return the datatype at the given index owned by this class. Type nodes are * associated with datatypes through the DatatypeIndexConstant class. The -- 2.30.2