From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 11 Mar 2021 01:18:11 +0000 (-0800)
Subject: Refactor Node::getOperator() to fix compiler warning. (#6110)
X-Git-Tag: cvc5-1.0.0~2105
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a021463ccdf674b5d5d9aee70908fe4fef300b9;p=cvc5.git

Refactor Node::getOperator() to fix compiler warning. (#6110)
---

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
 }