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

3 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index ee0c172af..c201c9ffc 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -184,9 +184,10 @@ Node ExtendedRewriter::extendedRewrite(Node n)
         // we may have subsumed children down to one
         ret = children[0];
       }
-      else if (isAssoc && children.size() > kind::metakind::getUpperBoundForKind(k))
+      else if (isAssoc
+               && children.size() > kind::metakind::getMaxArityForKind(k))
       {
-        Assert(kind::metakind::getUpperBoundForKind(k) >= 2);
+        Assert(kind::metakind::getMaxArityForKind(k) >= 2);
         // kind may require binary construction
         ret = children[0];
         for (unsigned i = 1, nchild = children.size(); i < nchild; i++)
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 7e36edcd4..3cbac95a2 100644
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -1182,7 +1182,7 @@ Node EqProof::addToProof(
   // use (= t1 t2) as a premise and rely on a symmetry step to justify it.
   unsigned arity = d_node[0].getNumChildren();
   Kind k = d_node[0].getKind();
-  bool isNary = ExprManager::isNAryKind(k);
+  bool isNary = NodeManager::isNAryKind(k);
 
   // N-ary operators are fun. The following proof is a valid EqProof
   //
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 59dc3943d..3eb0ed629 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1029,7 +1029,7 @@ void EqualityEngine::buildEqConclusion(EqualityNodeId id1,
   if ((d_isInternal[id1] || d_isInternal[id2])
       && (k1 != k2 || k1 == kind::APPLY_UF || k1 == kind::APPLY_CONSTRUCTOR
           || k1 == kind::APPLY_SELECTOR || k1 == kind::APPLY_TESTER
-          || !ExprManager::isNAryKind(k1)))
+          || !NodeManager::isNAryKind(k1)))
   {
     return;
   }