summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-10 17:18:11 -0800
committerGitHub <noreply@github.com>2021-03-11 01:18:11 +0000
commit0a021463ccdf674b5d5d9aee70908fe4fef300b9 (patch)
tree09f494f518eabf3574bc1fcd254e54f32227c0bb
parenta5ede7e253513ac0103c2521d7ac0c0452062b43 (diff)
Refactor Node::getOperator() to fix compiler warning. (#6110)
-rw-r--r--src/expr/node.h30
-rw-r--r--test/unit/expr/node_black.cpp4
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
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback