diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-10 13:28:58 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-10 21:28:58 +0000 |
| commit | c81140e9ab5db8bc95eb15145641be9d909d0618 (patch) | |
| tree | 991c424872f4b23a06b81dab9db7b8bf8aa30a7b /test | |
| parent | bd52deb7434b1b08a122db4513972644c11fc4aa (diff) | |
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).
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/expr/node_black.cpp | 8 | ||||
| -rw-r--r-- | test/unit/expr/node_manager_black.cpp | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp index 0d481ea4f..6c9c0a932 100644 --- a/test/unit/expr/node_black.cpp +++ b/test/unit/expr/node_black.cpp @@ -445,16 +445,16 @@ TEST_F(TestNodeBlackNode, getNumChildren) #ifdef CVC4_ASSERTIONS ASSERT_DEATH(testNaryExpForSize(AND, 0), "getNumChildren\\(\\) >= " - "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); ASSERT_DEATH(testNaryExpForSize(AND, 1), "getNumChildren\\(\\) >= " - "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); ASSERT_DEATH(testNaryExpForSize(NOT, 0), "getNumChildren\\(\\) >= " - "kind::metakind::getLowerBoundForKind\\(getKind\\(\\)\\)"); + "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); ASSERT_DEATH(testNaryExpForSize(NOT, 2), "getNumChildren\\(\\) <= " - "kind::metakind::getUpperBoundForKind\\(getKind\\(\\)\\)"); + "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)"); #endif /* CVC4_ASSERTIONS */ } diff --git a/test/unit/expr/node_manager_black.cpp b/test/unit/expr/node_manager_black.cpp index 2d8570fa5..a2ede3ed0 100644 --- a/test/unit/expr/node_manager_black.cpp +++ b/test/unit/expr/node_manager_black.cpp @@ -314,7 +314,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) { #ifdef CVC4_ASSERTIONS std::vector<Node> vars; - const unsigned int max = metakind::getUpperBoundForKind(AND); + const uint32_t max = metakind::getMaxArityForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); Node skolem_i = d_nodeManager->mkSkolem("i", boolType); Node skolem_j = d_nodeManager->mkSkolem("j", boolType); |