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

diff --git a/src/expr/node.h b/src/expr/node.h
index c73850e59ba1d8940f6193d23be213855633730d..7e63248228f2dc05e0a646896afdd52e19cb87aa 100644 (file)
--- 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 6c9c0a932c7287f49bd915f7edc380ba32c447b4..b536fb932f49f647e5919d8035281a314f467034 100644 (file)
--- 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
 }