diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-10 17:18:11 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-11 01:18:11 +0000 |
commit | 0a021463ccdf674b5d5d9aee70908fe4fef300b9 (patch) | |
tree | 09f494f518eabf3574bc1fcd254e54f32227c0bb | |
parent | a5ede7e253513ac0103c2521d7ac0c0452062b43 (diff) |
Refactor Node::getOperator() to fix compiler warning. (#6110)
-rw-r--r-- | src/expr/node.h | 30 | ||||
-rw-r--r-- | test/unit/expr/node_black.cpp | 4 |
2 files changed, 10 insertions, 24 deletions
diff --git a/src/expr/node.h b/src/expr/node.h index c73850e59..7e6324822 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1255,37 +1255,23 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { * Otherwise, it will be a node with kind BUILTIN. */ template <bool ref_count> -NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { +NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const +{ Assert(NodeManager::currentNM() != NULL) << "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); - switch(kind::MetaKind mk = getMetaKind()) { - case kind::metakind::INVALID: - IllegalArgument(*this, "getOperator() called on Node with INVALID-kinded kind"); - - case kind::metakind::VARIABLE: - IllegalArgument(*this, "getOperator() called on Node with VARIABLE-kinded kind"); - - case kind::metakind::OPERATOR: { + kind::MetaKind mk = getMetaKind(); + if (mk == kind::metakind::OPERATOR) + { /* Returns a BUILTIN node. */ return NodeManager::currentNM()->operatorOf(getKind()); } - - case kind::metakind::PARAMETERIZED: - /* The operator is the first child. */ - return Node(d_nv->d_children[0]); - - case kind::metakind::CONSTANT: - IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind"); - - case kind::metakind::NULLARY_OPERATOR: - IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind"); - - default: Unhandled() << mk; - } + Assert(mk == kind::metakind::PARAMETERIZED); + /* The operator is the first child. */ + return Node(d_nv->d_children[0]); } /** diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp index 6c9c0a932..b536fb932 100644 --- a/test/unit/expr/node_black.cpp +++ b/test/unit/expr/node_black.cpp @@ -422,8 +422,8 @@ TEST_F(TestNodeBlackNode, getOperator) ASSERT_EQ(f, fa.getOperator()); #ifdef CVC4_ASSERTIONS - ASSERT_THROW(f.getOperator(), IllegalArgumentException); - ASSERT_THROW(a.getOperator(), IllegalArgumentException); + ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED"); + ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED"); #endif } |