Adding test for whether a kind is n-ary (#4718)

2 files changed, 10 insertions, 0 deletions

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