From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Sat, 11 Jul 2020 04:55:31 +0000 (-0300)
Subject: Adding test for whether a kind is n-ary (#4718)
X-Git-Tag: cvc5-1.0.0~3128
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9aab4da2460b62273ac937ad96b7b6695b904e0d;p=cvc5.git

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 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