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

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7bec489a35a10f6d03fd7886ac38be942e3eb8ba..445ca9ee77b209feede981c60bda8ad68b6c9c11 100644 (file)
--- 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 db5d22fa890358723bdd19117522aeddd7a39705..3f180e95164eebbe1227191faa8f6d37f54b20d6 100644 (file)
--- 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