Move ExprManager::isNAryKind to NodeManager. (#6107)

This also renames metakind::getLowerBoundForKind and
metakind::getUpperBoundForKind for consistency.

Note that the NodeManager class needs to be reordered to comply to our
style guidelines. This PR does not reorder but introduces a public block
at the top (where the rest of the public interface of the class should
go eventually).

1 files changed, 8 insertions, 2 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5eb01ecbb..12fc99eaa 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -27,6 +27,7 @@
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
+#include "expr/metakind.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"
@@ -108,6 +109,11 @@ NodeManager::NodeManager(ExprManager* exprManager)
   init();
 }
 
+bool NodeManager::isNAryKind(Kind k)
+{
+  return kind::metakind::getMaxArityForKind(k) == expr::NodeValue::MAX_CHILDREN;
+}
+
 TypeNode NodeManager::booleanType()
 {
   return mkTypeConst<TypeConstant>(BOOLEAN_TYPE);
@@ -965,7 +971,7 @@ Node NodeManager::mkAssociative(Kind kind, const std::vector<Node>& children)
 {
   AlwaysAssert(kind::isAssociative(kind)) << "Illegal kind in mkAssociative";
 
-  const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+  const unsigned int max = kind::metakind::getMaxArityForKind(kind);
   size_t numChildren = children.size();
 
   /* If the number of children is within bounds, then there's nothing to do. */
@@ -973,7 +979,7 @@ Node NodeManager::mkAssociative(Kind kind, const std::vector<Node>& children)
   {
     return mkNode(kind, children);
   }
-  const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+  const unsigned int min = kind::metakind::getMinArityForKind(kind);
 
   std::vector<Node>::const_iterator it = children.begin();
   std::vector<Node>::const_iterator end = children.end();