Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/expr/metakind.cpp	Lines:	567	743	76.3 %
Date:	2021-05-22	Branches:	358	788	45.4 %

/******************************************************************************
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2010-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * This header file was automatically generated by:
 *
 *     ../../../src/expr/mkmetakind /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/expr/metakind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-05-22/src/theory/quantifiers/kinds
 *
 * for the cvc5 project.
 */

/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Andres Noetzli, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "expr/metakind.h"

#include <iostream>

namespace cvc5 {
namespace kind {

/**
 * Get the metakind for a particular kind.
 */
MetaKind metaKindOf(Kind k)
{
  static const MetaKind metaKinds[] = {
      metakind::INVALID, /* UNDEFINED_KIND */
      metakind::INVALID, /* NULL_EXPR */
      // clang-format off

    /* from builtin */
    metakind::VARIABLE, /* SORT_TAG */
    metakind::PARAMETERIZED, /* SORT_TYPE */
    metakind::CONSTANT, /* UNINTERPRETED_CONSTANT */
    metakind::CONSTANT, /* ABSTRACT_VALUE */
    metakind::CONSTANT, /* BUILTIN */
    metakind::OPERATOR, /* EQUAL */
    metakind::OPERATOR, /* DISTINCT */
    metakind::VARIABLE, /* VARIABLE */
    metakind::VARIABLE, /* BOUND_VARIABLE */
    metakind::VARIABLE, /* SKOLEM */
    metakind::OPERATOR, /* SEXPR */
    metakind::OPERATOR, /* LAMBDA */
    metakind::OPERATOR, /* WITNESS */
    metakind::CONSTANT, /* TYPE_CONSTANT */
    metakind::OPERATOR, /* FUNCTION_TYPE */

    /* from booleans */
    metakind::CONSTANT, /* CONST_BOOLEAN */
    metakind::OPERATOR, /* NOT */
    metakind::OPERATOR, /* AND */
    metakind::OPERATOR, /* IMPLIES */
    metakind::OPERATOR, /* OR */
    metakind::OPERATOR, /* XOR */
    metakind::OPERATOR, /* ITE */

    /* from uf */
    metakind::PARAMETERIZED, /* APPLY_UF */
    metakind::VARIABLE, /* BOOLEAN_TERM_VARIABLE */
    metakind::OPERATOR, /* CARDINALITY_CONSTRAINT */
    metakind::OPERATOR, /* COMBINED_CARDINALITY_CONSTRAINT */
    metakind::PARAMETERIZED, /* PARTIAL_APPLY_UF */
    metakind::OPERATOR, /* CARDINALITY_VALUE */
    metakind::OPERATOR, /* HO_APPLY */

    /* from arith */
    metakind::OPERATOR, /* PLUS */
    metakind::OPERATOR, /* MULT */
    metakind::OPERATOR, /* NONLINEAR_MULT */
    metakind::OPERATOR, /* MINUS */
    metakind::OPERATOR, /* UMINUS */
    metakind::OPERATOR, /* DIVISION */
    metakind::OPERATOR, /* DIVISION_TOTAL */
    metakind::OPERATOR, /* INTS_DIVISION */
    metakind::OPERATOR, /* INTS_DIVISION_TOTAL */
    metakind::OPERATOR, /* INTS_MODULUS */
    metakind::OPERATOR, /* INTS_MODULUS_TOTAL */
    metakind::OPERATOR, /* ABS */
    metakind::PARAMETERIZED, /* DIVISIBLE */
    metakind::OPERATOR, /* POW */
    metakind::OPERATOR, /* EXPONENTIAL */
    metakind::OPERATOR, /* SINE */
    metakind::OPERATOR, /* COSINE */
    metakind::OPERATOR, /* TANGENT */
    metakind::OPERATOR, /* COSECANT */
    metakind::OPERATOR, /* SECANT */
    metakind::OPERATOR, /* COTANGENT */
    metakind::OPERATOR, /* ARCSINE */
    metakind::OPERATOR, /* ARCCOSINE */
    metakind::OPERATOR, /* ARCTANGENT */
    metakind::OPERATOR, /* ARCCOSECANT */
    metakind::OPERATOR, /* ARCSECANT */
    metakind::OPERATOR, /* ARCCOTANGENT */
    metakind::OPERATOR, /* SQRT */
    metakind::CONSTANT, /* DIVISIBLE_OP */
    metakind::CONSTANT, /* CONST_RATIONAL */
    metakind::OPERATOR, /* LT */
    metakind::OPERATOR, /* LEQ */
    metakind::OPERATOR, /* GT */
    metakind::OPERATOR, /* GEQ */
    metakind::CONSTANT, /* INDEXED_ROOT_PREDICATE_OP */
    metakind::PARAMETERIZED, /* INDEXED_ROOT_PREDICATE */
    metakind::OPERATOR, /* IS_INTEGER */
    metakind::OPERATOR, /* TO_INTEGER */
    metakind::OPERATOR, /* TO_REAL */
    metakind::OPERATOR, /* CAST_TO_REAL */
    metakind::NULLARY_OPERATOR, /* PI */
    metakind::CONSTANT, /* IAND_OP */
    metakind::PARAMETERIZED, /* IAND */

    /* from bv */
    metakind::CONSTANT, /* BITVECTOR_TYPE */
    metakind::CONSTANT, /* CONST_BITVECTOR */
    metakind::OPERATOR, /* BITVECTOR_BB_TERM */
    metakind::OPERATOR, /* BITVECTOR_CONCAT */
    metakind::OPERATOR, /* BITVECTOR_AND */
    metakind::OPERATOR, /* BITVECTOR_COMP */
    metakind::OPERATOR, /* BITVECTOR_OR */
    metakind::OPERATOR, /* BITVECTOR_XOR */
    metakind::OPERATOR, /* BITVECTOR_NOT */
    metakind::OPERATOR, /* BITVECTOR_NAND */
    metakind::OPERATOR, /* BITVECTOR_NOR */
    metakind::OPERATOR, /* BITVECTOR_XNOR */
    metakind::OPERATOR, /* BITVECTOR_MULT */
    metakind::OPERATOR, /* BITVECTOR_NEG */
    metakind::OPERATOR, /* BITVECTOR_ADD */
    metakind::OPERATOR, /* BITVECTOR_SUB */
    metakind::OPERATOR, /* BITVECTOR_UDIV */
    metakind::OPERATOR, /* BITVECTOR_UREM */
    metakind::OPERATOR, /* BITVECTOR_SDIV */
    metakind::OPERATOR, /* BITVECTOR_SMOD */
    metakind::OPERATOR, /* BITVECTOR_SREM */
    metakind::OPERATOR, /* BITVECTOR_ASHR */
    metakind::OPERATOR, /* BITVECTOR_LSHR */
    metakind::OPERATOR, /* BITVECTOR_SHL */
    metakind::OPERATOR, /* BITVECTOR_ULE */
    metakind::OPERATOR, /* BITVECTOR_ULT */
    metakind::OPERATOR, /* BITVECTOR_UGE */
    metakind::OPERATOR, /* BITVECTOR_UGT */
    metakind::OPERATOR, /* BITVECTOR_SLE */
    metakind::OPERATOR, /* BITVECTOR_SLT */
    metakind::OPERATOR, /* BITVECTOR_SGE */
    metakind::OPERATOR, /* BITVECTOR_SGT */
    metakind::OPERATOR, /* BITVECTOR_ULTBV */
    metakind::OPERATOR, /* BITVECTOR_SLTBV */
    metakind::OPERATOR, /* BITVECTOR_REDAND */
    metakind::OPERATOR, /* BITVECTOR_REDOR */
    metakind::OPERATOR, /* BITVECTOR_ITE */
    metakind::OPERATOR, /* BITVECTOR_TO_NAT */
    metakind::OPERATOR, /* BITVECTOR_ACKERMANNIZE_UDIV */
    metakind::OPERATOR, /* BITVECTOR_ACKERMANNIZE_UREM */
    metakind::OPERATOR, /* BITVECTOR_EAGER_ATOM */
    metakind::CONSTANT, /* BITVECTOR_BITOF_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_BITOF */
    metakind::CONSTANT, /* BITVECTOR_EXTRACT_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_EXTRACT */
    metakind::CONSTANT, /* BITVECTOR_REPEAT_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_REPEAT */
    metakind::CONSTANT, /* BITVECTOR_ROTATE_LEFT_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_ROTATE_LEFT */
    metakind::CONSTANT, /* BITVECTOR_ROTATE_RIGHT_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_ROTATE_RIGHT */
    metakind::CONSTANT, /* BITVECTOR_SIGN_EXTEND_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_SIGN_EXTEND */
    metakind::CONSTANT, /* BITVECTOR_ZERO_EXTEND_OP */
    metakind::PARAMETERIZED, /* BITVECTOR_ZERO_EXTEND */
    metakind::CONSTANT, /* INT_TO_BITVECTOR_OP */
    metakind::PARAMETERIZED, /* INT_TO_BITVECTOR */

    /* from fp */
    metakind::CONSTANT, /* CONST_FLOATINGPOINT */
    metakind::CONSTANT, /* CONST_ROUNDINGMODE */
    metakind::CONSTANT, /* FLOATINGPOINT_TYPE */
    metakind::OPERATOR, /* FLOATINGPOINT_FP */
    metakind::OPERATOR, /* FLOATINGPOINT_EQ */
    metakind::OPERATOR, /* FLOATINGPOINT_ABS */
    metakind::OPERATOR, /* FLOATINGPOINT_NEG */
    metakind::OPERATOR, /* FLOATINGPOINT_PLUS */
    metakind::OPERATOR, /* FLOATINGPOINT_SUB */
    metakind::OPERATOR, /* FLOATINGPOINT_MULT */
    metakind::OPERATOR, /* FLOATINGPOINT_DIV */
    metakind::OPERATOR, /* FLOATINGPOINT_FMA */
    metakind::OPERATOR, /* FLOATINGPOINT_SQRT */
    metakind::OPERATOR, /* FLOATINGPOINT_REM */
    metakind::OPERATOR, /* FLOATINGPOINT_RTI */
    metakind::OPERATOR, /* FLOATINGPOINT_MIN */
    metakind::OPERATOR, /* FLOATINGPOINT_MAX */
    metakind::OPERATOR, /* FLOATINGPOINT_MIN_TOTAL */
    metakind::OPERATOR, /* FLOATINGPOINT_MAX_TOTAL */
    metakind::OPERATOR, /* FLOATINGPOINT_LEQ */
    metakind::OPERATOR, /* FLOATINGPOINT_LT */
    metakind::OPERATOR, /* FLOATINGPOINT_GEQ */
    metakind::OPERATOR, /* FLOATINGPOINT_GT */
    metakind::OPERATOR, /* FLOATINGPOINT_ISN */
    metakind::OPERATOR, /* FLOATINGPOINT_ISSN */
    metakind::OPERATOR, /* FLOATINGPOINT_ISZ */
    metakind::OPERATOR, /* FLOATINGPOINT_ISINF */
    metakind::OPERATOR, /* FLOATINGPOINT_ISNAN */
    metakind::OPERATOR, /* FLOATINGPOINT_ISNEG */
    metakind::OPERATOR, /* FLOATINGPOINT_ISPOS */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_REAL_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_REAL */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_FP_GENERIC */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_UBV_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_UBV */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_UBV_TOTAL */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_SBV_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_SBV */
    metakind::CONSTANT, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
    metakind::PARAMETERIZED, /* FLOATINGPOINT_TO_SBV_TOTAL */
    metakind::OPERATOR, /* FLOATINGPOINT_TO_REAL */
    metakind::OPERATOR, /* FLOATINGPOINT_TO_REAL_TOTAL */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_NAN */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_INF */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_ZERO */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_SIGN */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_EXPONENT */
    metakind::OPERATOR, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
    metakind::OPERATOR, /* ROUNDINGMODE_BITBLAST */

    /* from arrays */
    metakind::OPERATOR, /* ARRAY_TYPE */
    metakind::OPERATOR, /* SELECT */
    metakind::OPERATOR, /* STORE */
    metakind::OPERATOR, /* EQ_RANGE */
    metakind::CONSTANT, /* STORE_ALL */
    metakind::OPERATOR, /* ARR_TABLE_FUN */
    metakind::OPERATOR, /* ARRAY_LAMBDA */
    metakind::OPERATOR, /* PARTIAL_SELECT_0 */
    metakind::OPERATOR, /* PARTIAL_SELECT_1 */

    /* from datatypes */
    metakind::OPERATOR, /* CONSTRUCTOR_TYPE */
    metakind::OPERATOR, /* SELECTOR_TYPE */
    metakind::OPERATOR, /* TESTER_TYPE */
    metakind::OPERATOR, /* UPDATER_TYPE */
    metakind::PARAMETERIZED, /* APPLY_CONSTRUCTOR */
    metakind::PARAMETERIZED, /* APPLY_SELECTOR */
    metakind::PARAMETERIZED, /* APPLY_SELECTOR_TOTAL */
    metakind::PARAMETERIZED, /* APPLY_TESTER */
    metakind::PARAMETERIZED, /* APPLY_UPDATER */
    metakind::CONSTANT, /* DATATYPE_TYPE */
    metakind::OPERATOR, /* PARAMETRIC_DATATYPE */
    metakind::PARAMETERIZED, /* APPLY_TYPE_ASCRIPTION */
    metakind::CONSTANT, /* ASCRIPTION_TYPE */
    metakind::OPERATOR, /* DT_SIZE */
    metakind::OPERATOR, /* DT_HEIGHT_BOUND */
    metakind::OPERATOR, /* DT_SIZE_BOUND */
    metakind::OPERATOR, /* DT_SYGUS_BOUND */
    metakind::OPERATOR, /* DT_SYGUS_EVAL */
    metakind::OPERATOR, /* MATCH */
    metakind::OPERATOR, /* MATCH_CASE */
    metakind::OPERATOR, /* MATCH_BIND_CASE */
    metakind::CONSTANT, /* TUPLE_PROJECT_OP */
    metakind::PARAMETERIZED, /* TUPLE_PROJECT */

    /* from sep */
    metakind::NULLARY_OPERATOR, /* SEP_NIL */
    metakind::OPERATOR, /* SEP_EMP */
    metakind::OPERATOR, /* SEP_PTO */
    metakind::OPERATOR, /* SEP_STAR */
    metakind::OPERATOR, /* SEP_WAND */
    metakind::OPERATOR, /* SEP_LABEL */

    /* from sets */
    metakind::CONSTANT, /* EMPTYSET */
    metakind::OPERATOR, /* SET_TYPE */
    metakind::OPERATOR, /* UNION */
    metakind::OPERATOR, /* INTERSECTION */
    metakind::OPERATOR, /* SETMINUS */
    metakind::OPERATOR, /* SUBSET */
    metakind::OPERATOR, /* MEMBER */
    metakind::CONSTANT, /* SINGLETON_OP */
    metakind::PARAMETERIZED, /* SINGLETON */
    metakind::OPERATOR, /* INSERT */
    metakind::OPERATOR, /* CARD */
    metakind::OPERATOR, /* COMPLEMENT */
    metakind::NULLARY_OPERATOR, /* UNIVERSE_SET */
    metakind::OPERATOR, /* COMPREHENSION */
    metakind::OPERATOR, /* CHOOSE */
    metakind::OPERATOR, /* IS_SINGLETON */
    metakind::OPERATOR, /* JOIN */
    metakind::OPERATOR, /* PRODUCT */
    metakind::OPERATOR, /* TRANSPOSE */
    metakind::OPERATOR, /* TCLOSURE */
    metakind::OPERATOR, /* JOIN_IMAGE */
    metakind::OPERATOR, /* IDEN */

    /* from bags */
    metakind::CONSTANT, /* EMPTYBAG */
    metakind::OPERATOR, /* BAG_TYPE */
    metakind::OPERATOR, /* UNION_MAX */
    metakind::OPERATOR, /* UNION_DISJOINT */
    metakind::OPERATOR, /* INTERSECTION_MIN */
    metakind::OPERATOR, /* DIFFERENCE_SUBTRACT */
    metakind::OPERATOR, /* DIFFERENCE_REMOVE */
    metakind::OPERATOR, /* SUBBAG */
    metakind::OPERATOR, /* BAG_COUNT */
    metakind::OPERATOR, /* DUPLICATE_REMOVAL */
    metakind::CONSTANT, /* MK_BAG_OP */
    metakind::PARAMETERIZED, /* MK_BAG */
    metakind::OPERATOR, /* BAG_IS_SINGLETON */
    metakind::OPERATOR, /* BAG_CARD */
    metakind::OPERATOR, /* BAG_FROM_SET */
    metakind::OPERATOR, /* BAG_TO_SET */
    metakind::OPERATOR, /* BAG_CHOOSE */

    /* from strings */
    metakind::OPERATOR, /* STRING_CONCAT */
    metakind::OPERATOR, /* STRING_IN_REGEXP */
    metakind::OPERATOR, /* STRING_LENGTH */
    metakind::OPERATOR, /* STRING_SUBSTR */
    metakind::OPERATOR, /* STRING_UPDATE */
    metakind::OPERATOR, /* STRING_CHARAT */
    metakind::OPERATOR, /* STRING_STRCTN */
    metakind::OPERATOR, /* STRING_LT */
    metakind::OPERATOR, /* STRING_LEQ */
    metakind::OPERATOR, /* STRING_STRIDOF */
    metakind::OPERATOR, /* STRING_STRREPL */
    metakind::OPERATOR, /* STRING_STRREPLALL */
    metakind::OPERATOR, /* STRING_REPLACE_RE */
    metakind::OPERATOR, /* STRING_REPLACE_RE_ALL */
    metakind::OPERATOR, /* STRING_PREFIX */
    metakind::OPERATOR, /* STRING_SUFFIX */
    metakind::OPERATOR, /* STRING_IS_DIGIT */
    metakind::OPERATOR, /* STRING_ITOS */
    metakind::OPERATOR, /* STRING_STOI */
    metakind::OPERATOR, /* STRING_TO_CODE */
    metakind::OPERATOR, /* STRING_FROM_CODE */
    metakind::OPERATOR, /* STRING_TOLOWER */
    metakind::OPERATOR, /* STRING_TOUPPER */
    metakind::OPERATOR, /* STRING_REV */
    metakind::CONSTANT, /* CONST_STRING */
    metakind::OPERATOR, /* SEQUENCE_TYPE */
    metakind::CONSTANT, /* CONST_SEQUENCE */
    metakind::OPERATOR, /* SEQ_UNIT */
    metakind::OPERATOR, /* SEQ_NTH */
    metakind::OPERATOR, /* SEQ_NTH_TOTAL */
    metakind::OPERATOR, /* STRING_TO_REGEXP */
    metakind::OPERATOR, /* REGEXP_CONCAT */
    metakind::OPERATOR, /* REGEXP_UNION */
    metakind::OPERATOR, /* REGEXP_INTER */
    metakind::OPERATOR, /* REGEXP_DIFF */
    metakind::OPERATOR, /* REGEXP_STAR */
    metakind::OPERATOR, /* REGEXP_PLUS */
    metakind::OPERATOR, /* REGEXP_OPT */
    metakind::OPERATOR, /* REGEXP_RANGE */
    metakind::OPERATOR, /* REGEXP_COMPLEMENT */
    metakind::OPERATOR, /* REGEXP_EMPTY */
    metakind::OPERATOR, /* REGEXP_SIGMA */
    metakind::CONSTANT, /* REGEXP_REPEAT_OP */
    metakind::PARAMETERIZED, /* REGEXP_REPEAT */
    metakind::CONSTANT, /* REGEXP_LOOP_OP */
    metakind::PARAMETERIZED, /* REGEXP_LOOP */
    metakind::OPERATOR, /* REGEXP_RV */

    /* from quantifiers */
    metakind::OPERATOR, /* FORALL */
    metakind::OPERATOR, /* EXISTS */
    metakind::VARIABLE, /* INST_CONSTANT */
    metakind::OPERATOR, /* BOUND_VAR_LIST */
    metakind::OPERATOR, /* INST_PATTERN */
    metakind::OPERATOR, /* INST_NO_PATTERN */
    metakind::OPERATOR, /* INST_ATTRIBUTE */
    metakind::OPERATOR, /* INST_POOL */
    metakind::OPERATOR, /* INST_ADD_TO_POOL */
    metakind::OPERATOR, /* SKOLEM_ADD_TO_POOL */
    metakind::OPERATOR, /* INST_PATTERN_LIST */
  // clang-format on
      metakind::INVALID  /* LAST_KIND */
  };                     /* metaKinds[] */

  Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);

  // We've asserted that k >= NULL_EXPR (which is 0), but we still
  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
  // emits warnings for non-assertion builds, since the check isn't done.
  return metaKinds[k + 1];
} /* metaKindOf(k) */

}  // namespace kind

namespace expr {

// clang-format off

// The reinterpret_cast of d_children to "::cvc5::UninterpretedConstant const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::UninterpretedConstant const& NodeValue::getConst< ::cvc5::UninterpretedConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::UNINTERPRETED_CONSTANT, *this,
                 "Improper kind for getConst<::cvc5::UninterpretedConstant>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::UninterpretedConstant const* >(d_children)
    : *reinterpret_cast< ::cvc5::UninterpretedConstant const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::AbstractValue const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::AbstractValue const& NodeValue::getConst< ::cvc5::AbstractValue >() const {
  AssertArgument(getKind() == ::cvc5::kind::ABSTRACT_VALUE, *this,
                 "Improper kind for getConst<::cvc5::AbstractValue>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::AbstractValue const* >(d_children)
    : *reinterpret_cast< ::cvc5::AbstractValue const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::Kind const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::Kind const& NodeValue::getConst< ::cvc5::Kind >() const {
  AssertArgument(getKind() == ::cvc5::kind::BUILTIN, *this,
                 "Improper kind for getConst<::cvc5::Kind>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::Kind const* >(d_children)
    : *reinterpret_cast< ::cvc5::Kind const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::TypeConstant const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::TypeConstant const& NodeValue::getConst< ::cvc5::TypeConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::TYPE_CONSTANT, *this,
                 "Improper kind for getConst<::cvc5::TypeConstant>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::TypeConstant const* >(d_children)
    : *reinterpret_cast< ::cvc5::TypeConstant const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "bool const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
bool const& NodeValue::getConst< bool >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_BOOLEAN, *this,
                 "Improper kind for getConst<bool>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< bool const* >(d_children)
    : *reinterpret_cast< bool const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::Divisible const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::Divisible const& NodeValue::getConst< ::cvc5::Divisible >() const {
  AssertArgument(getKind() == ::cvc5::kind::DIVISIBLE_OP, *this,
                 "Improper kind for getConst<::cvc5::Divisible>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::Divisible const* >(d_children)
    : *reinterpret_cast< ::cvc5::Divisible const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::Rational const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::Rational const& NodeValue::getConst< ::cvc5::Rational >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_RATIONAL, *this,
                 "Improper kind for getConst<::cvc5::Rational>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::Rational const* >(d_children)
    : *reinterpret_cast< ::cvc5::Rational const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::IndexedRootPredicate const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::IndexedRootPredicate const& NodeValue::getConst< ::cvc5::IndexedRootPredicate >() const {
  AssertArgument(getKind() == ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP, *this,
                 "Improper kind for getConst<::cvc5::IndexedRootPredicate>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::IndexedRootPredicate const* >(d_children)
    : *reinterpret_cast< ::cvc5::IndexedRootPredicate const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::IntAnd const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::IntAnd const& NodeValue::getConst< ::cvc5::IntAnd >() const {
  AssertArgument(getKind() == ::cvc5::kind::IAND_OP, *this,
                 "Improper kind for getConst<::cvc5::IntAnd>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::IntAnd const* >(d_children)
    : *reinterpret_cast< ::cvc5::IntAnd const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorSize const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorSize const& NodeValue::getConst< ::cvc5::BitVectorSize >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_TYPE, *this,
                 "Improper kind for getConst<::cvc5::BitVectorSize>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorSize const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorSize const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVector const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVector const& NodeValue::getConst< ::cvc5::BitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_BITVECTOR, *this,
                 "Improper kind for getConst<::cvc5::BitVector>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVector const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVector const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorBitOf const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorBitOf const& NodeValue::getConst< ::cvc5::BitVectorBitOf >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_BITOF_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorBitOf>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorBitOf const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorBitOf const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorExtract const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorExtract const& NodeValue::getConst< ::cvc5::BitVectorExtract >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_EXTRACT_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorExtract>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorExtract const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorExtract const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorRepeat const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorRepeat const& NodeValue::getConst< ::cvc5::BitVectorRepeat >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_REPEAT_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorRepeat>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorRepeat const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorRepeat const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorRotateLeft const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorRotateLeft const& NodeValue::getConst< ::cvc5::BitVectorRotateLeft >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorRotateLeft>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorRotateLeft const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorRotateLeft const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorRotateRight const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorRotateRight const& NodeValue::getConst< ::cvc5::BitVectorRotateRight >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorRotateRight>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorRotateRight const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorRotateRight const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorSignExtend const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorSignExtend const& NodeValue::getConst< ::cvc5::BitVectorSignExtend >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorSignExtend>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorSignExtend const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorSignExtend const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::BitVectorZeroExtend const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::BitVectorZeroExtend const& NodeValue::getConst< ::cvc5::BitVectorZeroExtend >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP, *this,
                 "Improper kind for getConst<::cvc5::BitVectorZeroExtend>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::BitVectorZeroExtend const* >(d_children)
    : *reinterpret_cast< ::cvc5::BitVectorZeroExtend const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::IntToBitVector const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::IntToBitVector const& NodeValue::getConst< ::cvc5::IntToBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::INT_TO_BITVECTOR_OP, *this,
                 "Improper kind for getConst<::cvc5::IntToBitVector>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::IntToBitVector const* >(d_children)
    : *reinterpret_cast< ::cvc5::IntToBitVector const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPoint const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPoint const& NodeValue::getConst< ::cvc5::FloatingPoint >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_FLOATINGPOINT, *this,
                 "Improper kind for getConst<::cvc5::FloatingPoint>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPoint const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPoint const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::RoundingMode const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::RoundingMode const& NodeValue::getConst< ::cvc5::RoundingMode >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_ROUNDINGMODE, *this,
                 "Improper kind for getConst<::cvc5::RoundingMode>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::RoundingMode const* >(d_children)
    : *reinterpret_cast< ::cvc5::RoundingMode const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointSize const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointSize const& NodeValue::getConst< ::cvc5::FloatingPointSize >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TYPE, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointSize>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointSize const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointSize const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPIEEEBitVector const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPIEEEBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPIEEEBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPIEEEBitVector>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPIEEEBitVector const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPIEEEBitVector const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPFloatingPoint const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPFloatingPoint const& NodeValue::getConst< ::cvc5::FloatingPointToFPFloatingPoint >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPFloatingPoint>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPFloatingPoint const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPFloatingPoint const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPReal const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPReal const& NodeValue::getConst< ::cvc5::FloatingPointToFPReal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPReal>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPReal const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPReal const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPSignedBitVector const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPSignedBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPSignedBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPSignedBitVector>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPSignedBitVector const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPSignedBitVector const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPUnsignedBitVector const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< ::cvc5::FloatingPointToFPUnsignedBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPUnsignedBitVector>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPUnsignedBitVector const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPUnsignedBitVector const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToFPGeneric const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToFPGeneric const& NodeValue::getConst< ::cvc5::FloatingPointToFPGeneric >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToFPGeneric>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToFPGeneric const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToFPGeneric const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToUBV const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToUBV const& NodeValue::getConst< ::cvc5::FloatingPointToUBV >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToUBV>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToUBV const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToUBV const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToUBVTotal const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToUBVTotal const& NodeValue::getConst< ::cvc5::FloatingPointToUBVTotal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToUBVTotal>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToUBVTotal const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToUBVTotal const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToSBV const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToSBV const& NodeValue::getConst< ::cvc5::FloatingPointToSBV >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToSBV>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToSBV const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToSBV const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::FloatingPointToSBVTotal const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::FloatingPointToSBVTotal const& NodeValue::getConst< ::cvc5::FloatingPointToSBVTotal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, *this,
                 "Improper kind for getConst<::cvc5::FloatingPointToSBVTotal>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::FloatingPointToSBVTotal const* >(d_children)
    : *reinterpret_cast< ::cvc5::FloatingPointToSBVTotal const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::ArrayStoreAll const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::ArrayStoreAll const& NodeValue::getConst< ::cvc5::ArrayStoreAll >() const {
  AssertArgument(getKind() == ::cvc5::kind::STORE_ALL, *this,
                 "Improper kind for getConst<::cvc5::ArrayStoreAll>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::ArrayStoreAll const* >(d_children)
    : *reinterpret_cast< ::cvc5::ArrayStoreAll const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::DatatypeIndexConstant const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::DatatypeIndexConstant const& NodeValue::getConst< ::cvc5::DatatypeIndexConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::DATATYPE_TYPE, *this,
                 "Improper kind for getConst<::cvc5::DatatypeIndexConstant>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::DatatypeIndexConstant const* >(d_children)
    : *reinterpret_cast< ::cvc5::DatatypeIndexConstant const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::AscriptionType const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::AscriptionType const& NodeValue::getConst< ::cvc5::AscriptionType >() const {
  AssertArgument(getKind() == ::cvc5::kind::ASCRIPTION_TYPE, *this,
                 "Improper kind for getConst<::cvc5::AscriptionType>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::AscriptionType const* >(d_children)
    : *reinterpret_cast< ::cvc5::AscriptionType const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::TupleProjectOp const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::TupleProjectOp const& NodeValue::getConst< ::cvc5::TupleProjectOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::TUPLE_PROJECT_OP, *this,
                 "Improper kind for getConst<::cvc5::TupleProjectOp>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::TupleProjectOp const* >(d_children)
    : *reinterpret_cast< ::cvc5::TupleProjectOp const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::EmptySet const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::EmptySet const& NodeValue::getConst< ::cvc5::EmptySet >() const {
  AssertArgument(getKind() == ::cvc5::kind::EMPTYSET, *this,
                 "Improper kind for getConst<::cvc5::EmptySet>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::EmptySet const* >(d_children)
    : *reinterpret_cast< ::cvc5::EmptySet const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::SingletonOp const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::SingletonOp const& NodeValue::getConst< ::cvc5::SingletonOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::SINGLETON_OP, *this,
                 "Improper kind for getConst<::cvc5::SingletonOp>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::SingletonOp const* >(d_children)
    : *reinterpret_cast< ::cvc5::SingletonOp const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::EmptyBag const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::EmptyBag const& NodeValue::getConst< ::cvc5::EmptyBag >() const {
  AssertArgument(getKind() == ::cvc5::kind::EMPTYBAG, *this,
                 "Improper kind for getConst<::cvc5::EmptyBag>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::EmptyBag const* >(d_children)
    : *reinterpret_cast< ::cvc5::EmptyBag const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::MakeBagOp const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::MakeBagOp const& NodeValue::getConst< ::cvc5::MakeBagOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::MK_BAG_OP, *this,
                 "Improper kind for getConst<::cvc5::MakeBagOp>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::MakeBagOp const* >(d_children)
    : *reinterpret_cast< ::cvc5::MakeBagOp const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::String const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::String const& NodeValue::getConst< ::cvc5::String >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_STRING, *this,
                 "Improper kind for getConst<::cvc5::String>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::String const* >(d_children)
    : *reinterpret_cast< ::cvc5::String const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::Sequence const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::Sequence const& NodeValue::getConst< ::cvc5::Sequence >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_SEQUENCE, *this,
                 "Improper kind for getConst<::cvc5::Sequence>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::Sequence const* >(d_children)
    : *reinterpret_cast< ::cvc5::Sequence const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::RegExpRepeat const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::RegExpRepeat const& NodeValue::getConst< ::cvc5::RegExpRepeat >() const {
  AssertArgument(getKind() == ::cvc5::kind::REGEXP_REPEAT_OP, *this,
                 "Improper kind for getConst<::cvc5::RegExpRepeat>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::RegExpRepeat const* >(d_children)
    : *reinterpret_cast< ::cvc5::RegExpRepeat const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// The reinterpret_cast of d_children to "::cvc5::RegExpLoop const*"
// flags a "strict aliasing" warning; it's okay, because we never access
// the embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

template <>
::cvc5::RegExpLoop const& NodeValue::getConst< ::cvc5::RegExpLoop >() const {
  AssertArgument(getKind() == ::cvc5::kind::REGEXP_LOOP_OP, *this,
                 "Improper kind for getConst<::cvc5::RegExpLoop>()");
  // To support non-inlined CONSTANT-kinded NodeValues (those that are
  // "constructed" when initially checking them against the NodeManager
  // pool), we must check d_nchildren here.
  return d_nchildren == 0
    ? *reinterpret_cast< ::cvc5::RegExpLoop const* >(d_children)
    : *reinterpret_cast< ::cvc5::RegExpLoop const* >(d_children[0]);
}

// re-enable the warning
#pragma GCC diagnostic warning "-Wstrict-aliasing"


// clang-format on

}  // namespace expr

namespace kind {
namespace metakind {

size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv)
{
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);

  switch (nv->d_kind)
  {
// clang-format off

  case kind::UNINTERPRETED_CONSTANT:
    return ::cvc5::UninterpretedConstantHashFunction()(nv->getConst< ::cvc5::UninterpretedConstant >());

  case kind::ABSTRACT_VALUE:
    return ::cvc5::AbstractValueHashFunction()(nv->getConst< ::cvc5::AbstractValue >());

  case kind::BUILTIN:
    return ::cvc5::kind::KindHashFunction()(nv->getConst< ::cvc5::Kind >());

  case kind::TYPE_CONSTANT:
    return ::cvc5::TypeConstantHashFunction()(nv->getConst< ::cvc5::TypeConstant >());

  case kind::CONST_BOOLEAN:
    return ::cvc5::BoolHashFunction()(nv->getConst< bool >());

  case kind::DIVISIBLE_OP:
    return ::cvc5::DivisibleHashFunction()(nv->getConst< ::cvc5::Divisible >());

  case kind::CONST_RATIONAL:
    return ::cvc5::RationalHashFunction()(nv->getConst< ::cvc5::Rational >());

  case kind::INDEXED_ROOT_PREDICATE_OP:
    return ::cvc5::IndexedRootPredicateHashFunction()(nv->getConst< ::cvc5::IndexedRootPredicate >());

  case kind::IAND_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::IntAnd >()(nv->getConst< ::cvc5::IntAnd >());

  case kind::BITVECTOR_TYPE:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >()(nv->getConst< ::cvc5::BitVectorSize >());

  case kind::CONST_BITVECTOR:
    return ::cvc5::BitVectorHashFunction()(nv->getConst< ::cvc5::BitVector >());

  case kind::BITVECTOR_BITOF_OP:
    return ::cvc5::BitVectorBitOfHashFunction()(nv->getConst< ::cvc5::BitVectorBitOf >());

  case kind::BITVECTOR_EXTRACT_OP:
    return ::cvc5::BitVectorExtractHashFunction()(nv->getConst< ::cvc5::BitVectorExtract >());

  case kind::BITVECTOR_REPEAT_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >()(nv->getConst< ::cvc5::BitVectorRepeat >());

  case kind::BITVECTOR_ROTATE_LEFT_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >()(nv->getConst< ::cvc5::BitVectorRotateLeft >());

  case kind::BITVECTOR_ROTATE_RIGHT_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >()(nv->getConst< ::cvc5::BitVectorRotateRight >());

  case kind::BITVECTOR_SIGN_EXTEND_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >()(nv->getConst< ::cvc5::BitVectorSignExtend >());

  case kind::BITVECTOR_ZERO_EXTEND_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >()(nv->getConst< ::cvc5::BitVectorZeroExtend >());

  case kind::INT_TO_BITVECTOR_OP:
    return ::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >()(nv->getConst< ::cvc5::IntToBitVector >());

  case kind::CONST_FLOATINGPOINT:
    return ::cvc5::FloatingPointHashFunction()(nv->getConst< ::cvc5::FloatingPoint >());

  case kind::CONST_ROUNDINGMODE:
    return ::cvc5::RoundingModeHashFunction()(nv->getConst< ::cvc5::RoundingMode >());

  case kind::FLOATINGPOINT_TYPE:
    return ::cvc5::FloatingPointSizeHashFunction()(nv->getConst< ::cvc5::FloatingPointSize >());

  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x1>()(nv->getConst< ::cvc5::FloatingPointToFPIEEEBitVector >());

  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x2>()(nv->getConst< ::cvc5::FloatingPointToFPFloatingPoint >());

  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x4>()(nv->getConst< ::cvc5::FloatingPointToFPReal >());

  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x8>()(nv->getConst< ::cvc5::FloatingPointToFPSignedBitVector >());

  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x10>()(nv->getConst< ::cvc5::FloatingPointToFPUnsignedBitVector >());

  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
    return ::cvc5::FloatingPointConvertSortHashFunction<0x11>()(nv->getConst< ::cvc5::FloatingPointToFPGeneric >());

  case kind::FLOATINGPOINT_TO_UBV_OP:
    return ::cvc5::FloatingPointToBVHashFunction<0x1>()(nv->getConst< ::cvc5::FloatingPointToUBV >());

  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
    return ::cvc5::FloatingPointToBVHashFunction<0x4>()(nv->getConst< ::cvc5::FloatingPointToUBVTotal >());

  case kind::FLOATINGPOINT_TO_SBV_OP:
    return ::cvc5::FloatingPointToBVHashFunction<0x2>()(nv->getConst< ::cvc5::FloatingPointToSBV >());

  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
    return ::cvc5::FloatingPointToBVHashFunction<0x8>()(nv->getConst< ::cvc5::FloatingPointToSBVTotal >());

  case kind::STORE_ALL:
    return ::cvc5::ArrayStoreAllHashFunction()(nv->getConst< ::cvc5::ArrayStoreAll >());

  case kind::DATATYPE_TYPE:
    return ::cvc5::DatatypeIndexConstantHashFunction()(nv->getConst< ::cvc5::DatatypeIndexConstant >());

  case kind::ASCRIPTION_TYPE:
    return ::cvc5::AscriptionTypeHashFunction()(nv->getConst< ::cvc5::AscriptionType >());

  case kind::TUPLE_PROJECT_OP:
    return ::cvc5::TupleProjectOpHashFunction()(nv->getConst< ::cvc5::TupleProjectOp >());

  case kind::EMPTYSET:
    return ::cvc5::EmptySetHashFunction()(nv->getConst< ::cvc5::EmptySet >());

  case kind::SINGLETON_OP:
    return ::cvc5::SingletonOpHashFunction()(nv->getConst< ::cvc5::SingletonOp >());

  case kind::EMPTYBAG:
    return ::cvc5::EmptyBagHashFunction()(nv->getConst< ::cvc5::EmptyBag >());

  case kind::MK_BAG_OP:
    return ::cvc5::MakeBagOpHashFunction()(nv->getConst< ::cvc5::MakeBagOp >());

  case kind::CONST_STRING:
    return ::cvc5::strings::StringHashFunction()(nv->getConst< ::cvc5::String >());

  case kind::CONST_SEQUENCE:
    return ::cvc5::SequenceHashFunction()(nv->getConst< ::cvc5::Sequence >());

  case kind::REGEXP_REPEAT_OP:
    return ::cvc5::RegExpRepeatHashFunction()(nv->getConst< ::cvc5::RegExpRepeat >());

  case kind::REGEXP_LOOP_OP:
    return ::cvc5::RegExpLoopHashFunction()(nv->getConst< ::cvc5::RegExpLoop >());

// clang-format on
default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
  }
}

template <bool pool>
bool NodeValueCompare::compare(const ::cvc5::expr::NodeValue* nv1,
                               const ::cvc5::expr::NodeValue* nv2)
{
  if(nv1->d_kind != nv2->d_kind) {
    return false;
  }

  if (nv1->getMetaKind() == kind::metakind::CONSTANT)
  {
    switch (nv1->d_kind)
    {
// clang-format off

    case kind::UNINTERPRETED_CONSTANT:
      return NodeValueConstCompare< kind::UNINTERPRETED_CONSTANT, pool >::compare(nv1, nv2);

    case kind::ABSTRACT_VALUE:
      return NodeValueConstCompare< kind::ABSTRACT_VALUE, pool >::compare(nv1, nv2);

    case kind::BUILTIN:
      return NodeValueConstCompare< kind::BUILTIN, pool >::compare(nv1, nv2);

    case kind::TYPE_CONSTANT:
      return NodeValueConstCompare< kind::TYPE_CONSTANT, pool >::compare(nv1, nv2);

    case kind::CONST_BOOLEAN:
      return NodeValueConstCompare< kind::CONST_BOOLEAN, pool >::compare(nv1, nv2);

    case kind::DIVISIBLE_OP:
      return NodeValueConstCompare< kind::DIVISIBLE_OP, pool >::compare(nv1, nv2);

    case kind::CONST_RATIONAL:
      return NodeValueConstCompare< kind::CONST_RATIONAL, pool >::compare(nv1, nv2);

    case kind::INDEXED_ROOT_PREDICATE_OP:
      return NodeValueConstCompare< kind::INDEXED_ROOT_PREDICATE_OP, pool >::compare(nv1, nv2);

    case kind::IAND_OP:
      return NodeValueConstCompare< kind::IAND_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_TYPE:
      return NodeValueConstCompare< kind::BITVECTOR_TYPE, pool >::compare(nv1, nv2);

    case kind::CONST_BITVECTOR:
      return NodeValueConstCompare< kind::CONST_BITVECTOR, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_BITOF_OP:
      return NodeValueConstCompare< kind::BITVECTOR_BITOF_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_EXTRACT_OP:
      return NodeValueConstCompare< kind::BITVECTOR_EXTRACT_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_REPEAT_OP:
      return NodeValueConstCompare< kind::BITVECTOR_REPEAT_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_ROTATE_LEFT_OP:
      return NodeValueConstCompare< kind::BITVECTOR_ROTATE_LEFT_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_ROTATE_RIGHT_OP:
      return NodeValueConstCompare< kind::BITVECTOR_ROTATE_RIGHT_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_SIGN_EXTEND_OP:
      return NodeValueConstCompare< kind::BITVECTOR_SIGN_EXTEND_OP, pool >::compare(nv1, nv2);

    case kind::BITVECTOR_ZERO_EXTEND_OP:
      return NodeValueConstCompare< kind::BITVECTOR_ZERO_EXTEND_OP, pool >::compare(nv1, nv2);

    case kind::INT_TO_BITVECTOR_OP:
      return NodeValueConstCompare< kind::INT_TO_BITVECTOR_OP, pool >::compare(nv1, nv2);

    case kind::CONST_FLOATINGPOINT:
      return NodeValueConstCompare< kind::CONST_FLOATINGPOINT, pool >::compare(nv1, nv2);

    case kind::CONST_ROUNDINGMODE:
      return NodeValueConstCompare< kind::CONST_ROUNDINGMODE, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TYPE:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TYPE, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_REAL_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_REAL_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_FP_GENERIC_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_UBV_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_UBV_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_SBV_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_SBV_OP, pool >::compare(nv1, nv2);

    case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
      return NodeValueConstCompare< kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, pool >::compare(nv1, nv2);

    case kind::STORE_ALL:
      return NodeValueConstCompare< kind::STORE_ALL, pool >::compare(nv1, nv2);

    case kind::DATATYPE_TYPE:
      return NodeValueConstCompare< kind::DATATYPE_TYPE, pool >::compare(nv1, nv2);

    case kind::ASCRIPTION_TYPE:
      return NodeValueConstCompare< kind::ASCRIPTION_TYPE, pool >::compare(nv1, nv2);

    case kind::TUPLE_PROJECT_OP:
      return NodeValueConstCompare< kind::TUPLE_PROJECT_OP, pool >::compare(nv1, nv2);

    case kind::EMPTYSET:
      return NodeValueConstCompare< kind::EMPTYSET, pool >::compare(nv1, nv2);

    case kind::SINGLETON_OP:
      return NodeValueConstCompare< kind::SINGLETON_OP, pool >::compare(nv1, nv2);

    case kind::EMPTYBAG:
      return NodeValueConstCompare< kind::EMPTYBAG, pool >::compare(nv1, nv2);

    case kind::MK_BAG_OP:
      return NodeValueConstCompare< kind::MK_BAG_OP, pool >::compare(nv1, nv2);

    case kind::CONST_STRING:
      return NodeValueConstCompare< kind::CONST_STRING, pool >::compare(nv1, nv2);

    case kind::CONST_SEQUENCE:
      return NodeValueConstCompare< kind::CONST_SEQUENCE, pool >::compare(nv1, nv2);

    case kind::REGEXP_REPEAT_OP:
      return NodeValueConstCompare< kind::REGEXP_REPEAT_OP, pool >::compare(nv1, nv2);

    case kind::REGEXP_LOOP_OP:
      return NodeValueConstCompare< kind::REGEXP_LOOP_OP, pool >::compare(nv1, nv2);

// clang-format on
default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv1->d_kind);
    }
  }

  if(nv1->d_nchildren != nv2->d_nchildren) {
    return false;
  }

  ::cvc5::expr::NodeValue::const_nv_iterator i = nv1->nv_begin();
  ::cvc5::expr::NodeValue::const_nv_iterator j = nv2->nv_begin();
  ::cvc5::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end();

  while(i != i_end) {
    if((*i) != (*j)) {
      return false;
    }
    ++i;
    ++j;
  }

  return true;
}

template bool NodeValueCompare::compare<true>(
    const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2);
template bool NodeValueCompare::compare<false>(
    const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2);

void NodeValueConstPrinter::toStream(std::ostream& out,
                                     const ::cvc5::expr::NodeValue* nv)
{
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);

  switch (nv->d_kind)
  {
// clang-format off

  case kind::UNINTERPRETED_CONSTANT:
    out << nv->getConst< ::cvc5::UninterpretedConstant >();
    break;

  case kind::ABSTRACT_VALUE:
    out << nv->getConst< ::cvc5::AbstractValue >();
    break;

  case kind::BUILTIN:
    out << nv->getConst< ::cvc5::Kind >();
    break;

  case kind::TYPE_CONSTANT:
    out << nv->getConst< ::cvc5::TypeConstant >();
    break;

  case kind::CONST_BOOLEAN:
    out << nv->getConst< bool >();
    break;

  case kind::DIVISIBLE_OP:
    out << nv->getConst< ::cvc5::Divisible >();
    break;

  case kind::CONST_RATIONAL:
    out << nv->getConst< ::cvc5::Rational >();
    break;

  case kind::INDEXED_ROOT_PREDICATE_OP:
    out << nv->getConst< ::cvc5::IndexedRootPredicate >();
    break;

  case kind::IAND_OP:
    out << nv->getConst< ::cvc5::IntAnd >();
    break;

  case kind::BITVECTOR_TYPE:
    out << nv->getConst< ::cvc5::BitVectorSize >();
    break;

  case kind::CONST_BITVECTOR:
    out << nv->getConst< ::cvc5::BitVector >();
    break;

  case kind::BITVECTOR_BITOF_OP:
    out << nv->getConst< ::cvc5::BitVectorBitOf >();
    break;

  case kind::BITVECTOR_EXTRACT_OP:
    out << nv->getConst< ::cvc5::BitVectorExtract >();
    break;

  case kind::BITVECTOR_REPEAT_OP:
    out << nv->getConst< ::cvc5::BitVectorRepeat >();
    break;

  case kind::BITVECTOR_ROTATE_LEFT_OP:
    out << nv->getConst< ::cvc5::BitVectorRotateLeft >();
    break;

  case kind::BITVECTOR_ROTATE_RIGHT_OP:
    out << nv->getConst< ::cvc5::BitVectorRotateRight >();
    break;

  case kind::BITVECTOR_SIGN_EXTEND_OP:
    out << nv->getConst< ::cvc5::BitVectorSignExtend >();
    break;

  case kind::BITVECTOR_ZERO_EXTEND_OP:
    out << nv->getConst< ::cvc5::BitVectorZeroExtend >();
    break;

  case kind::INT_TO_BITVECTOR_OP:
    out << nv->getConst< ::cvc5::IntToBitVector >();
    break;

  case kind::CONST_FLOATINGPOINT:
    out << nv->getConst< ::cvc5::FloatingPoint >();
    break;

  case kind::CONST_ROUNDINGMODE:
    out << nv->getConst< ::cvc5::RoundingMode >();
    break;

  case kind::FLOATINGPOINT_TYPE:
    out << nv->getConst< ::cvc5::FloatingPointSize >();
    break;

  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPIEEEBitVector >();
    break;

  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPFloatingPoint >();
    break;

  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPReal >();
    break;

  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPSignedBitVector >();
    break;

  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPUnsignedBitVector >();
    break;

  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
    out << nv->getConst< ::cvc5::FloatingPointToFPGeneric >();
    break;

  case kind::FLOATINGPOINT_TO_UBV_OP:
    out << nv->getConst< ::cvc5::FloatingPointToUBV >();
    break;

  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
    out << nv->getConst< ::cvc5::FloatingPointToUBVTotal >();
    break;

  case kind::FLOATINGPOINT_TO_SBV_OP:
    out << nv->getConst< ::cvc5::FloatingPointToSBV >();
    break;

  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
    out << nv->getConst< ::cvc5::FloatingPointToSBVTotal >();
    break;

  case kind::STORE_ALL:
    out << nv->getConst< ::cvc5::ArrayStoreAll >();
    break;

  case kind::DATATYPE_TYPE:
    out << nv->getConst< ::cvc5::DatatypeIndexConstant >();
    break;

  case kind::ASCRIPTION_TYPE:
    out << nv->getConst< ::cvc5::AscriptionType >();
    break;

  case kind::TUPLE_PROJECT_OP:
    out << nv->getConst< ::cvc5::TupleProjectOp >();
    break;

  case kind::EMPTYSET:
    out << nv->getConst< ::cvc5::EmptySet >();
    break;

  case kind::SINGLETON_OP:
    out << nv->getConst< ::cvc5::SingletonOp >();
    break;

  case kind::EMPTYBAG:
    out << nv->getConst< ::cvc5::EmptyBag >();
    break;

  case kind::MK_BAG_OP:
    out << nv->getConst< ::cvc5::MakeBagOp >();
    break;

  case kind::CONST_STRING:
    out << nv->getConst< ::cvc5::String >();
    break;

  case kind::CONST_SEQUENCE:
    out << nv->getConst< ::cvc5::Sequence >();
    break;

  case kind::REGEXP_REPEAT_OP:
    out << nv->getConst< ::cvc5::RegExpRepeat >();
    break;

  case kind::REGEXP_LOOP_OP:
    out << nv->getConst< ::cvc5::RegExpLoop >();
    break;

// clang-format on
default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
  }
}

void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
  toStream(out, n.d_nv);
}

// The reinterpret_cast of d_children to various constant payload types
// in deleteNodeValueConstant(), below, can flag a "strict aliasing"
// warning; it should actually be okay, because we never access the
// embedded constant as a NodeValue* child, and never access an embedded
// NodeValue* child as a constant.
#pragma GCC diagnostic ignored "-Wstrict-aliasing"

/**
 * Cleanup to be performed when a NodeValue zombie is collected, and
 * it has CONSTANT metakind.  This calls the destructor for the underlying
 * C++ type representing the constant value.  See
 * NodeManager::reclaimZombies() for more information.
 *
 * This doesn't support "non-inlined" NodeValues, which shouldn't need this
 * kind of cleanup.
 */
void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv)
{
  Assert(nv->getMetaKind() == kind::metakind::CONSTANT);

  switch (nv->d_kind)
  {
// clang-format off

  case kind::UNINTERPRETED_CONSTANT:
    std::allocator< ::cvc5::UninterpretedConstant >().destroy(reinterpret_cast< ::cvc5::UninterpretedConstant* >(nv->d_children));
    break;

  case kind::ABSTRACT_VALUE:
    std::allocator< ::cvc5::AbstractValue >().destroy(reinterpret_cast< ::cvc5::AbstractValue* >(nv->d_children));
    break;

  case kind::BUILTIN:
    std::allocator< ::cvc5::Kind >().destroy(reinterpret_cast< ::cvc5::Kind* >(nv->d_children));
    break;

  case kind::TYPE_CONSTANT:
    std::allocator< ::cvc5::TypeConstant >().destroy(reinterpret_cast< ::cvc5::TypeConstant* >(nv->d_children));
    break;

  case kind::CONST_BOOLEAN:
    std::allocator< bool >().destroy(reinterpret_cast< bool* >(nv->d_children));
    break;

  case kind::DIVISIBLE_OP:
    std::allocator< ::cvc5::Divisible >().destroy(reinterpret_cast< ::cvc5::Divisible* >(nv->d_children));
    break;

  case kind::CONST_RATIONAL:
    std::allocator< ::cvc5::Rational >().destroy(reinterpret_cast< ::cvc5::Rational* >(nv->d_children));
    break;

  case kind::INDEXED_ROOT_PREDICATE_OP:
    std::allocator< ::cvc5::IndexedRootPredicate >().destroy(reinterpret_cast< ::cvc5::IndexedRootPredicate* >(nv->d_children));
    break;

  case kind::IAND_OP:
    std::allocator< ::cvc5::IntAnd >().destroy(reinterpret_cast< ::cvc5::IntAnd* >(nv->d_children));
    break;

  case kind::BITVECTOR_TYPE:
    std::allocator< ::cvc5::BitVectorSize >().destroy(reinterpret_cast< ::cvc5::BitVectorSize* >(nv->d_children));
    break;

  case kind::CONST_BITVECTOR:
    std::allocator< ::cvc5::BitVector >().destroy(reinterpret_cast< ::cvc5::BitVector* >(nv->d_children));
    break;

  case kind::BITVECTOR_BITOF_OP:
    std::allocator< ::cvc5::BitVectorBitOf >().destroy(reinterpret_cast< ::cvc5::BitVectorBitOf* >(nv->d_children));
    break;

  case kind::BITVECTOR_EXTRACT_OP:
    std::allocator< ::cvc5::BitVectorExtract >().destroy(reinterpret_cast< ::cvc5::BitVectorExtract* >(nv->d_children));
    break;

  case kind::BITVECTOR_REPEAT_OP:
    std::allocator< ::cvc5::BitVectorRepeat >().destroy(reinterpret_cast< ::cvc5::BitVectorRepeat* >(nv->d_children));
    break;

  case kind::BITVECTOR_ROTATE_LEFT_OP:
    std::allocator< ::cvc5::BitVectorRotateLeft >().destroy(reinterpret_cast< ::cvc5::BitVectorRotateLeft* >(nv->d_children));
    break;

  case kind::BITVECTOR_ROTATE_RIGHT_OP:
    std::allocator< ::cvc5::BitVectorRotateRight >().destroy(reinterpret_cast< ::cvc5::BitVectorRotateRight* >(nv->d_children));
    break;

  case kind::BITVECTOR_SIGN_EXTEND_OP:
    std::allocator< ::cvc5::BitVectorSignExtend >().destroy(reinterpret_cast< ::cvc5::BitVectorSignExtend* >(nv->d_children));
    break;

  case kind::BITVECTOR_ZERO_EXTEND_OP:
    std::allocator< ::cvc5::BitVectorZeroExtend >().destroy(reinterpret_cast< ::cvc5::BitVectorZeroExtend* >(nv->d_children));
    break;

  case kind::INT_TO_BITVECTOR_OP:
    std::allocator< ::cvc5::IntToBitVector >().destroy(reinterpret_cast< ::cvc5::IntToBitVector* >(nv->d_children));
    break;

  case kind::CONST_FLOATINGPOINT:
    std::allocator< ::cvc5::FloatingPoint >().destroy(reinterpret_cast< ::cvc5::FloatingPoint* >(nv->d_children));
    break;

  case kind::CONST_ROUNDINGMODE:
    std::allocator< ::cvc5::RoundingMode >().destroy(reinterpret_cast< ::cvc5::RoundingMode* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TYPE:
    std::allocator< ::cvc5::FloatingPointSize >().destroy(reinterpret_cast< ::cvc5::FloatingPointSize* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
    std::allocator< ::cvc5::FloatingPointToFPIEEEBitVector >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPIEEEBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
    std::allocator< ::cvc5::FloatingPointToFPFloatingPoint >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPFloatingPoint* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
    std::allocator< ::cvc5::FloatingPointToFPReal >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPReal* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
    std::allocator< ::cvc5::FloatingPointToFPSignedBitVector >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPSignedBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
    std::allocator< ::cvc5::FloatingPointToFPUnsignedBitVector >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPUnsignedBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
    std::allocator< ::cvc5::FloatingPointToFPGeneric >().destroy(reinterpret_cast< ::cvc5::FloatingPointToFPGeneric* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_UBV_OP:
    std::allocator< ::cvc5::FloatingPointToUBV >().destroy(reinterpret_cast< ::cvc5::FloatingPointToUBV* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
    std::allocator< ::cvc5::FloatingPointToUBVTotal >().destroy(reinterpret_cast< ::cvc5::FloatingPointToUBVTotal* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_SBV_OP:
    std::allocator< ::cvc5::FloatingPointToSBV >().destroy(reinterpret_cast< ::cvc5::FloatingPointToSBV* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
    std::allocator< ::cvc5::FloatingPointToSBVTotal >().destroy(reinterpret_cast< ::cvc5::FloatingPointToSBVTotal* >(nv->d_children));
    break;

  case kind::STORE_ALL:
    std::allocator< ::cvc5::ArrayStoreAll >().destroy(reinterpret_cast< ::cvc5::ArrayStoreAll* >(nv->d_children));
    break;

  case kind::DATATYPE_TYPE:
    std::allocator< ::cvc5::DatatypeIndexConstant >().destroy(reinterpret_cast< ::cvc5::DatatypeIndexConstant* >(nv->d_children));
    break;

  case kind::ASCRIPTION_TYPE:
    std::allocator< ::cvc5::AscriptionType >().destroy(reinterpret_cast< ::cvc5::AscriptionType* >(nv->d_children));
    break;

  case kind::TUPLE_PROJECT_OP:
    std::allocator< ::cvc5::TupleProjectOp >().destroy(reinterpret_cast< ::cvc5::TupleProjectOp* >(nv->d_children));
    break;

  case kind::EMPTYSET:
    std::allocator< ::cvc5::EmptySet >().destroy(reinterpret_cast< ::cvc5::EmptySet* >(nv->d_children));
    break;

  case kind::SINGLETON_OP:
    std::allocator< ::cvc5::SingletonOp >().destroy(reinterpret_cast< ::cvc5::SingletonOp* >(nv->d_children));
    break;

  case kind::EMPTYBAG:
    std::allocator< ::cvc5::EmptyBag >().destroy(reinterpret_cast< ::cvc5::EmptyBag* >(nv->d_children));
    break;

  case kind::MK_BAG_OP:
    std::allocator< ::cvc5::MakeBagOp >().destroy(reinterpret_cast< ::cvc5::MakeBagOp* >(nv->d_children));
    break;

  case kind::CONST_STRING:
    std::allocator< ::cvc5::String >().destroy(reinterpret_cast< ::cvc5::String* >(nv->d_children));
    break;

  case kind::CONST_SEQUENCE:
    std::allocator< ::cvc5::Sequence >().destroy(reinterpret_cast< ::cvc5::Sequence* >(nv->d_children));
    break;

  case kind::REGEXP_REPEAT_OP:
    std::allocator< ::cvc5::RegExpRepeat >().destroy(reinterpret_cast< ::cvc5::RegExpRepeat* >(nv->d_children));
    break;

  case kind::REGEXP_LOOP_OP:
    std::allocator< ::cvc5::RegExpLoop >().destroy(reinterpret_cast< ::cvc5::RegExpLoop* >(nv->d_children));
    break;

// clang-format on
default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
  }
}

// re-enable the strict-aliasing warning
# pragma GCC diagnostic warning "-Wstrict-aliasing"

uint32_t getMinArityForKind(::cvc5::Kind k)
{
  static const unsigned lbs[] = {
    0, /* NULL_EXPR */
// clang-format off

    0, /* SORT_TAG */
    0, /* SORT_TYPE */
    0, /* UNINTERPRETED_CONSTANT */
    0, /* ABSTRACT_VALUE */
    0, /* BUILTIN */
    2, /* EQUAL */
    2, /* DISTINCT */
    0, /* VARIABLE */
    0, /* BOUND_VARIABLE */
    0, /* SKOLEM */
    0, /* SEXPR */
    2, /* LAMBDA */
    2, /* WITNESS */
    0, /* TYPE_CONSTANT */
    2, /* FUNCTION_TYPE */
    0, /* CONST_BOOLEAN */
    1, /* NOT */
    2, /* AND */
    2, /* IMPLIES */
    2, /* OR */
    2, /* XOR */
    3, /* ITE */
    1, /* APPLY_UF */
    0, /* BOOLEAN_TERM_VARIABLE */
    2, /* CARDINALITY_CONSTRAINT */
    1, /* COMBINED_CARDINALITY_CONSTRAINT */
    1, /* PARTIAL_APPLY_UF */
    1, /* CARDINALITY_VALUE */
    2, /* HO_APPLY */
    2, /* PLUS */
    2, /* MULT */
    2, /* NONLINEAR_MULT */
    2, /* MINUS */
    1, /* UMINUS */
    2, /* DIVISION */
    2, /* DIVISION_TOTAL */
    2, /* INTS_DIVISION */
    2, /* INTS_DIVISION_TOTAL */
    2, /* INTS_MODULUS */
    2, /* INTS_MODULUS_TOTAL */
    1, /* ABS */
    1, /* DIVISIBLE */
    2, /* POW */
    1, /* EXPONENTIAL */
    1, /* SINE */
    1, /* COSINE */
    1, /* TANGENT */
    1, /* COSECANT */
    1, /* SECANT */
    1, /* COTANGENT */
    1, /* ARCSINE */
    1, /* ARCCOSINE */
    1, /* ARCTANGENT */
    1, /* ARCCOSECANT */
    1, /* ARCSECANT */
    1, /* ARCCOTANGENT */
    1, /* SQRT */
    0, /* DIVISIBLE_OP */
    0, /* CONST_RATIONAL */
    2, /* LT */
    2, /* LEQ */
    2, /* GT */
    2, /* GEQ */
    0, /* INDEXED_ROOT_PREDICATE_OP */
    2, /* INDEXED_ROOT_PREDICATE */
    1, /* IS_INTEGER */
    1, /* TO_INTEGER */
    1, /* TO_REAL */
    1, /* CAST_TO_REAL */
    0, /* PI */
    0, /* IAND_OP */
    2, /* IAND */
    0, /* BITVECTOR_TYPE */
    0, /* CONST_BITVECTOR */
    1, /* BITVECTOR_BB_TERM */
    2, /* BITVECTOR_CONCAT */
    2, /* BITVECTOR_AND */
    2, /* BITVECTOR_COMP */
    2, /* BITVECTOR_OR */
    2, /* BITVECTOR_XOR */
    1, /* BITVECTOR_NOT */
    2, /* BITVECTOR_NAND */
    2, /* BITVECTOR_NOR */
    2, /* BITVECTOR_XNOR */
    2, /* BITVECTOR_MULT */
    1, /* BITVECTOR_NEG */
    2, /* BITVECTOR_ADD */
    2, /* BITVECTOR_SUB */
    2, /* BITVECTOR_UDIV */
    2, /* BITVECTOR_UREM */
    2, /* BITVECTOR_SDIV */
    2, /* BITVECTOR_SMOD */
    2, /* BITVECTOR_SREM */
    2, /* BITVECTOR_ASHR */
    2, /* BITVECTOR_LSHR */
    2, /* BITVECTOR_SHL */
    2, /* BITVECTOR_ULE */
    2, /* BITVECTOR_ULT */
    2, /* BITVECTOR_UGE */
    2, /* BITVECTOR_UGT */
    2, /* BITVECTOR_SLE */
    2, /* BITVECTOR_SLT */
    2, /* BITVECTOR_SGE */
    2, /* BITVECTOR_SGT */
    2, /* BITVECTOR_ULTBV */
    2, /* BITVECTOR_SLTBV */
    1, /* BITVECTOR_REDAND */
    1, /* BITVECTOR_REDOR */
    3, /* BITVECTOR_ITE */
    1, /* BITVECTOR_TO_NAT */
    1, /* BITVECTOR_ACKERMANNIZE_UDIV */
    1, /* BITVECTOR_ACKERMANNIZE_UREM */
    1, /* BITVECTOR_EAGER_ATOM */
    0, /* BITVECTOR_BITOF_OP */
    1, /* BITVECTOR_BITOF */
    0, /* BITVECTOR_EXTRACT_OP */
    1, /* BITVECTOR_EXTRACT */
    0, /* BITVECTOR_REPEAT_OP */
    1, /* BITVECTOR_REPEAT */
    0, /* BITVECTOR_ROTATE_LEFT_OP */
    1, /* BITVECTOR_ROTATE_LEFT */
    0, /* BITVECTOR_ROTATE_RIGHT_OP */
    1, /* BITVECTOR_ROTATE_RIGHT */
    0, /* BITVECTOR_SIGN_EXTEND_OP */
    1, /* BITVECTOR_SIGN_EXTEND */
    0, /* BITVECTOR_ZERO_EXTEND_OP */
    1, /* BITVECTOR_ZERO_EXTEND */
    0, /* INT_TO_BITVECTOR_OP */
    1, /* INT_TO_BITVECTOR */
    0, /* CONST_FLOATINGPOINT */
    0, /* CONST_ROUNDINGMODE */
    0, /* FLOATINGPOINT_TYPE */
    3, /* FLOATINGPOINT_FP */
    2, /* FLOATINGPOINT_EQ */
    1, /* FLOATINGPOINT_ABS */
    1, /* FLOATINGPOINT_NEG */
    3, /* FLOATINGPOINT_PLUS */
    3, /* FLOATINGPOINT_SUB */
    3, /* FLOATINGPOINT_MULT */
    3, /* FLOATINGPOINT_DIV */
    4, /* FLOATINGPOINT_FMA */
    2, /* FLOATINGPOINT_SQRT */
    2, /* FLOATINGPOINT_REM */
    2, /* FLOATINGPOINT_RTI */
    2, /* FLOATINGPOINT_MIN */
    2, /* FLOATINGPOINT_MAX */
    3, /* FLOATINGPOINT_MIN_TOTAL */
    3, /* FLOATINGPOINT_MAX_TOTAL */
    2, /* FLOATINGPOINT_LEQ */
    2, /* FLOATINGPOINT_LT */
    2, /* FLOATINGPOINT_GEQ */
    2, /* FLOATINGPOINT_GT */
    1, /* FLOATINGPOINT_ISN */
    1, /* FLOATINGPOINT_ISSN */
    1, /* FLOATINGPOINT_ISZ */
    1, /* FLOATINGPOINT_ISINF */
    1, /* FLOATINGPOINT_ISNAN */
    1, /* FLOATINGPOINT_ISNEG */
    1, /* FLOATINGPOINT_ISPOS */
    0, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
    1, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
    2, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
    0, /* FLOATINGPOINT_TO_FP_REAL_OP */
    2, /* FLOATINGPOINT_TO_FP_REAL */
    0, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
    2, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
    2, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
    1, /* FLOATINGPOINT_TO_FP_GENERIC */
    0, /* FLOATINGPOINT_TO_UBV_OP */
    2, /* FLOATINGPOINT_TO_UBV */
    0, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
    3, /* FLOATINGPOINT_TO_UBV_TOTAL */
    0, /* FLOATINGPOINT_TO_SBV_OP */
    2, /* FLOATINGPOINT_TO_SBV */
    0, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
    3, /* FLOATINGPOINT_TO_SBV_TOTAL */
    1, /* FLOATINGPOINT_TO_REAL */
    2, /* FLOATINGPOINT_TO_REAL_TOTAL */
    1, /* FLOATINGPOINT_COMPONENT_NAN */
    1, /* FLOATINGPOINT_COMPONENT_INF */
    1, /* FLOATINGPOINT_COMPONENT_ZERO */
    1, /* FLOATINGPOINT_COMPONENT_SIGN */
    1, /* FLOATINGPOINT_COMPONENT_EXPONENT */
    1, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
    1, /* ROUNDINGMODE_BITBLAST */
    2, /* ARRAY_TYPE */
    2, /* SELECT */
    3, /* STORE */
    4, /* EQ_RANGE */
    0, /* STORE_ALL */
    4, /* ARR_TABLE_FUN */
    1, /* ARRAY_LAMBDA */
    0, /* PARTIAL_SELECT_0 */
    0, /* PARTIAL_SELECT_1 */
    1, /* CONSTRUCTOR_TYPE */
    2, /* SELECTOR_TYPE */
    1, /* TESTER_TYPE */
    2, /* UPDATER_TYPE */
    0, /* APPLY_CONSTRUCTOR */
    1, /* APPLY_SELECTOR */
    1, /* APPLY_SELECTOR_TOTAL */
    1, /* APPLY_TESTER */
    2, /* APPLY_UPDATER */
    0, /* DATATYPE_TYPE */
    1, /* PARAMETRIC_DATATYPE */
    1, /* APPLY_TYPE_ASCRIPTION */
    0, /* ASCRIPTION_TYPE */
    1, /* DT_SIZE */
    2, /* DT_HEIGHT_BOUND */
    2, /* DT_SIZE_BOUND */
    2, /* DT_SYGUS_BOUND */
    1, /* DT_SYGUS_EVAL */
    2, /* MATCH */
    2, /* MATCH_CASE */
    3, /* MATCH_BIND_CASE */
    0, /* TUPLE_PROJECT_OP */
    1, /* TUPLE_PROJECT */
    0, /* SEP_NIL */
    2, /* SEP_EMP */
    2, /* SEP_PTO */
    2, /* SEP_STAR */
    2, /* SEP_WAND */
    2, /* SEP_LABEL */
    0, /* EMPTYSET */
    1, /* SET_TYPE */
    2, /* UNION */
    2, /* INTERSECTION */
    2, /* SETMINUS */
    2, /* SUBSET */
    2, /* MEMBER */
    0, /* SINGLETON_OP */
    1, /* SINGLETON */
    2, /* INSERT */
    1, /* CARD */
    1, /* COMPLEMENT */
    0, /* UNIVERSE_SET */
    3, /* COMPREHENSION */
    1, /* CHOOSE */
    1, /* IS_SINGLETON */
    2, /* JOIN */
    2, /* PRODUCT */
    1, /* TRANSPOSE */
    1, /* TCLOSURE */
    2, /* JOIN_IMAGE */
    1, /* IDEN */
    0, /* EMPTYBAG */
    1, /* BAG_TYPE */
    2, /* UNION_MAX */
    2, /* UNION_DISJOINT */
    2, /* INTERSECTION_MIN */
    2, /* DIFFERENCE_SUBTRACT */
    2, /* DIFFERENCE_REMOVE */
    2, /* SUBBAG */
    2, /* BAG_COUNT */
    1, /* DUPLICATE_REMOVAL */
    0, /* MK_BAG_OP */
    2, /* MK_BAG */
    1, /* BAG_IS_SINGLETON */
    1, /* BAG_CARD */
    1, /* BAG_FROM_SET */
    1, /* BAG_TO_SET */
    1, /* BAG_CHOOSE */
    2, /* STRING_CONCAT */
    2, /* STRING_IN_REGEXP */
    1, /* STRING_LENGTH */
    3, /* STRING_SUBSTR */
    3, /* STRING_UPDATE */
    2, /* STRING_CHARAT */
    2, /* STRING_STRCTN */
    2, /* STRING_LT */
    2, /* STRING_LEQ */
    3, /* STRING_STRIDOF */
    3, /* STRING_STRREPL */
    3, /* STRING_STRREPLALL */
    3, /* STRING_REPLACE_RE */
    3, /* STRING_REPLACE_RE_ALL */
    2, /* STRING_PREFIX */
    2, /* STRING_SUFFIX */
    1, /* STRING_IS_DIGIT */
    1, /* STRING_ITOS */
    1, /* STRING_STOI */
    1, /* STRING_TO_CODE */
    1, /* STRING_FROM_CODE */
    1, /* STRING_TOLOWER */
    1, /* STRING_TOUPPER */
    1, /* STRING_REV */
    0, /* CONST_STRING */
    1, /* SEQUENCE_TYPE */
    0, /* CONST_SEQUENCE */
    1, /* SEQ_UNIT */
    2, /* SEQ_NTH */
    2, /* SEQ_NTH_TOTAL */
    1, /* STRING_TO_REGEXP */
    2, /* REGEXP_CONCAT */
    2, /* REGEXP_UNION */
    2, /* REGEXP_INTER */
    2, /* REGEXP_DIFF */
    1, /* REGEXP_STAR */
    1, /* REGEXP_PLUS */
    1, /* REGEXP_OPT */
    2, /* REGEXP_RANGE */
    1, /* REGEXP_COMPLEMENT */
    0, /* REGEXP_EMPTY */
    0, /* REGEXP_SIGMA */
    0, /* REGEXP_REPEAT_OP */
    1, /* REGEXP_REPEAT */
    0, /* REGEXP_LOOP_OP */
    1, /* REGEXP_LOOP */
    1, /* REGEXP_RV */
    2, /* FORALL */
    2, /* EXISTS */
    0, /* INST_CONSTANT */
    1, /* BOUND_VAR_LIST */
    1, /* INST_PATTERN */
    1, /* INST_NO_PATTERN */
    1, /* INST_ATTRIBUTE */
    1, /* INST_POOL */
    2, /* INST_ADD_TO_POOL */
    2, /* SKOLEM_ADD_TO_POOL */
    1, /* INST_PATTERN_LIST */
// clang-format on

    0 /* LAST_KIND */
  };

  return lbs[k];
}

uint32_t getMaxArityForKind(::cvc5::Kind k)
{
  static const unsigned ubs[] = {
    0, /* NULL_EXPR */
// clang-format off

    0, /* SORT_TAG */
    expr::NodeValue::MAX_CHILDREN, /* SORT_TYPE */
    0, /* UNINTERPRETED_CONSTANT */
    0, /* ABSTRACT_VALUE */
    0, /* BUILTIN */
    2, /* EQUAL */
    expr::NodeValue::MAX_CHILDREN, /* DISTINCT */
    0, /* VARIABLE */
    0, /* BOUND_VARIABLE */
    0, /* SKOLEM */
    expr::NodeValue::MAX_CHILDREN, /* SEXPR */
    2, /* LAMBDA */
    2, /* WITNESS */
    0, /* TYPE_CONSTANT */
    expr::NodeValue::MAX_CHILDREN, /* FUNCTION_TYPE */
    0, /* CONST_BOOLEAN */
    1, /* NOT */
    expr::NodeValue::MAX_CHILDREN, /* AND */
    2, /* IMPLIES */
    expr::NodeValue::MAX_CHILDREN, /* OR */
    2, /* XOR */
    3, /* ITE */
    expr::NodeValue::MAX_CHILDREN, /* APPLY_UF */
    0, /* BOOLEAN_TERM_VARIABLE */
    2, /* CARDINALITY_CONSTRAINT */
    1, /* COMBINED_CARDINALITY_CONSTRAINT */
    expr::NodeValue::MAX_CHILDREN, /* PARTIAL_APPLY_UF */
    1, /* CARDINALITY_VALUE */
    2, /* HO_APPLY */
    expr::NodeValue::MAX_CHILDREN, /* PLUS */
    expr::NodeValue::MAX_CHILDREN, /* MULT */
    expr::NodeValue::MAX_CHILDREN, /* NONLINEAR_MULT */
    2, /* MINUS */
    1, /* UMINUS */
    2, /* DIVISION */
    2, /* DIVISION_TOTAL */
    2, /* INTS_DIVISION */
    2, /* INTS_DIVISION_TOTAL */
    2, /* INTS_MODULUS */
    2, /* INTS_MODULUS_TOTAL */
    1, /* ABS */
    1, /* DIVISIBLE */
    2, /* POW */
    1, /* EXPONENTIAL */
    1, /* SINE */
    1, /* COSINE */
    1, /* TANGENT */
    1, /* COSECANT */
    1, /* SECANT */
    1, /* COTANGENT */
    1, /* ARCSINE */
    1, /* ARCCOSINE */
    1, /* ARCTANGENT */
    1, /* ARCCOSECANT */
    1, /* ARCSECANT */
    1, /* ARCCOTANGENT */
    1, /* SQRT */
    0, /* DIVISIBLE_OP */
    0, /* CONST_RATIONAL */
    2, /* LT */
    2, /* LEQ */
    2, /* GT */
    2, /* GEQ */
    0, /* INDEXED_ROOT_PREDICATE_OP */
    2, /* INDEXED_ROOT_PREDICATE */
    1, /* IS_INTEGER */
    1, /* TO_INTEGER */
    1, /* TO_REAL */
    1, /* CAST_TO_REAL */
    0, /* PI */
    0, /* IAND_OP */
    2, /* IAND */
    0, /* BITVECTOR_TYPE */
    0, /* CONST_BITVECTOR */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_BB_TERM */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_CONCAT */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_AND */
    2, /* BITVECTOR_COMP */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_OR */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_XOR */
    1, /* BITVECTOR_NOT */
    2, /* BITVECTOR_NAND */
    2, /* BITVECTOR_NOR */
    2, /* BITVECTOR_XNOR */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_MULT */
    1, /* BITVECTOR_NEG */
    expr::NodeValue::MAX_CHILDREN, /* BITVECTOR_ADD */
    2, /* BITVECTOR_SUB */
    2, /* BITVECTOR_UDIV */
    2, /* BITVECTOR_UREM */
    2, /* BITVECTOR_SDIV */
    2, /* BITVECTOR_SMOD */
    2, /* BITVECTOR_SREM */
    2, /* BITVECTOR_ASHR */
    2, /* BITVECTOR_LSHR */
    2, /* BITVECTOR_SHL */
    2, /* BITVECTOR_ULE */
    2, /* BITVECTOR_ULT */
    2, /* BITVECTOR_UGE */
    2, /* BITVECTOR_UGT */
    2, /* BITVECTOR_SLE */
    2, /* BITVECTOR_SLT */
    2, /* BITVECTOR_SGE */
    2, /* BITVECTOR_SGT */
    2, /* BITVECTOR_ULTBV */
    2, /* BITVECTOR_SLTBV */
    1, /* BITVECTOR_REDAND */
    1, /* BITVECTOR_REDOR */
    3, /* BITVECTOR_ITE */
    1, /* BITVECTOR_TO_NAT */
    1, /* BITVECTOR_ACKERMANNIZE_UDIV */
    1, /* BITVECTOR_ACKERMANNIZE_UREM */
    1, /* BITVECTOR_EAGER_ATOM */
    0, /* BITVECTOR_BITOF_OP */
    1, /* BITVECTOR_BITOF */
    0, /* BITVECTOR_EXTRACT_OP */
    1, /* BITVECTOR_EXTRACT */
    0, /* BITVECTOR_REPEAT_OP */
    1, /* BITVECTOR_REPEAT */
    0, /* BITVECTOR_ROTATE_LEFT_OP */
    1, /* BITVECTOR_ROTATE_LEFT */
    0, /* BITVECTOR_ROTATE_RIGHT_OP */
    1, /* BITVECTOR_ROTATE_RIGHT */
    0, /* BITVECTOR_SIGN_EXTEND_OP */
    1, /* BITVECTOR_SIGN_EXTEND */
    0, /* BITVECTOR_ZERO_EXTEND_OP */
    1, /* BITVECTOR_ZERO_EXTEND */
    0, /* INT_TO_BITVECTOR_OP */
    1, /* INT_TO_BITVECTOR */
    0, /* CONST_FLOATINGPOINT */
    0, /* CONST_ROUNDINGMODE */
    0, /* FLOATINGPOINT_TYPE */
    3, /* FLOATINGPOINT_FP */
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_EQ */
    1, /* FLOATINGPOINT_ABS */
    1, /* FLOATINGPOINT_NEG */
    3, /* FLOATINGPOINT_PLUS */
    3, /* FLOATINGPOINT_SUB */
    3, /* FLOATINGPOINT_MULT */
    3, /* FLOATINGPOINT_DIV */
    4, /* FLOATINGPOINT_FMA */
    2, /* FLOATINGPOINT_SQRT */
    2, /* FLOATINGPOINT_REM */
    2, /* FLOATINGPOINT_RTI */
    2, /* FLOATINGPOINT_MIN */
    2, /* FLOATINGPOINT_MAX */
    3, /* FLOATINGPOINT_MIN_TOTAL */
    3, /* FLOATINGPOINT_MAX_TOTAL */
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_LEQ */
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_LT */
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_GEQ */
    expr::NodeValue::MAX_CHILDREN, /* FLOATINGPOINT_GT */
    1, /* FLOATINGPOINT_ISN */
    1, /* FLOATINGPOINT_ISSN */
    1, /* FLOATINGPOINT_ISZ */
    1, /* FLOATINGPOINT_ISINF */
    1, /* FLOATINGPOINT_ISNAN */
    1, /* FLOATINGPOINT_ISNEG */
    1, /* FLOATINGPOINT_ISPOS */
    0, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP */
    1, /* FLOATINGPOINT_TO_FP_IEEE_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP */
    2, /* FLOATINGPOINT_TO_FP_FLOATINGPOINT */
    0, /* FLOATINGPOINT_TO_FP_REAL_OP */
    2, /* FLOATINGPOINT_TO_FP_REAL */
    0, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP */
    2, /* FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP */
    2, /* FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR */
    0, /* FLOATINGPOINT_TO_FP_GENERIC_OP */
    2, /* FLOATINGPOINT_TO_FP_GENERIC */
    0, /* FLOATINGPOINT_TO_UBV_OP */
    2, /* FLOATINGPOINT_TO_UBV */
    0, /* FLOATINGPOINT_TO_UBV_TOTAL_OP */
    3, /* FLOATINGPOINT_TO_UBV_TOTAL */
    0, /* FLOATINGPOINT_TO_SBV_OP */
    2, /* FLOATINGPOINT_TO_SBV */
    0, /* FLOATINGPOINT_TO_SBV_TOTAL_OP */
    3, /* FLOATINGPOINT_TO_SBV_TOTAL */
    1, /* FLOATINGPOINT_TO_REAL */
    2, /* FLOATINGPOINT_TO_REAL_TOTAL */
    1, /* FLOATINGPOINT_COMPONENT_NAN */
    1, /* FLOATINGPOINT_COMPONENT_INF */
    1, /* FLOATINGPOINT_COMPONENT_ZERO */
    1, /* FLOATINGPOINT_COMPONENT_SIGN */
    1, /* FLOATINGPOINT_COMPONENT_EXPONENT */
    1, /* FLOATINGPOINT_COMPONENT_SIGNIFICAND */
    1, /* ROUNDINGMODE_BITBLAST */
    2, /* ARRAY_TYPE */
    2, /* SELECT */
    3, /* STORE */
    4, /* EQ_RANGE */
    0, /* STORE_ALL */
    4, /* ARR_TABLE_FUN */
    1, /* ARRAY_LAMBDA */
    2, /* PARTIAL_SELECT_0 */
    2, /* PARTIAL_SELECT_1 */
    expr::NodeValue::MAX_CHILDREN, /* CONSTRUCTOR_TYPE */
    2, /* SELECTOR_TYPE */
    1, /* TESTER_TYPE */
    2, /* UPDATER_TYPE */
    expr::NodeValue::MAX_CHILDREN, /* APPLY_CONSTRUCTOR */
    1, /* APPLY_SELECTOR */
    1, /* APPLY_SELECTOR_TOTAL */
    1, /* APPLY_TESTER */
    2, /* APPLY_UPDATER */
    0, /* DATATYPE_TYPE */
    expr::NodeValue::MAX_CHILDREN, /* PARAMETRIC_DATATYPE */
    1, /* APPLY_TYPE_ASCRIPTION */
    0, /* ASCRIPTION_TYPE */
    1, /* DT_SIZE */
    2, /* DT_HEIGHT_BOUND */
    2, /* DT_SIZE_BOUND */
    2, /* DT_SYGUS_BOUND */
    expr::NodeValue::MAX_CHILDREN, /* DT_SYGUS_EVAL */
    expr::NodeValue::MAX_CHILDREN, /* MATCH */
    2, /* MATCH_CASE */
    3, /* MATCH_BIND_CASE */
    0, /* TUPLE_PROJECT_OP */
    1, /* TUPLE_PROJECT */
    0, /* SEP_NIL */
    2, /* SEP_EMP */
    2, /* SEP_PTO */
    expr::NodeValue::MAX_CHILDREN, /* SEP_STAR */
    2, /* SEP_WAND */
    2, /* SEP_LABEL */
    0, /* EMPTYSET */
    1, /* SET_TYPE */
    2, /* UNION */
    2, /* INTERSECTION */
    2, /* SETMINUS */
    2, /* SUBSET */
    2, /* MEMBER */
    0, /* SINGLETON_OP */
    1, /* SINGLETON */
    expr::NodeValue::MAX_CHILDREN, /* INSERT */
    1, /* CARD */
    1, /* COMPLEMENT */
    0, /* UNIVERSE_SET */
    3, /* COMPREHENSION */
    1, /* CHOOSE */
    1, /* IS_SINGLETON */
    2, /* JOIN */
    2, /* PRODUCT */
    1, /* TRANSPOSE */
    1, /* TCLOSURE */
    2, /* JOIN_IMAGE */
    1, /* IDEN */
    0, /* EMPTYBAG */
    1, /* BAG_TYPE */
    2, /* UNION_MAX */
    2, /* UNION_DISJOINT */
    2, /* INTERSECTION_MIN */
    2, /* DIFFERENCE_SUBTRACT */
    2, /* DIFFERENCE_REMOVE */
    2, /* SUBBAG */
    2, /* BAG_COUNT */
    1, /* DUPLICATE_REMOVAL */
    0, /* MK_BAG_OP */
    2, /* MK_BAG */
    1, /* BAG_IS_SINGLETON */
    1, /* BAG_CARD */
    1, /* BAG_FROM_SET */
    1, /* BAG_TO_SET */
    1, /* BAG_CHOOSE */
    expr::NodeValue::MAX_CHILDREN, /* STRING_CONCAT */
    2, /* STRING_IN_REGEXP */
    1, /* STRING_LENGTH */
    3, /* STRING_SUBSTR */
    3, /* STRING_UPDATE */
    2, /* STRING_CHARAT */
    2, /* STRING_STRCTN */
    2, /* STRING_LT */
    2, /* STRING_LEQ */
    3, /* STRING_STRIDOF */
    3, /* STRING_STRREPL */
    3, /* STRING_STRREPLALL */
    3, /* STRING_REPLACE_RE */
    3, /* STRING_REPLACE_RE_ALL */
    2, /* STRING_PREFIX */
    2, /* STRING_SUFFIX */
    1, /* STRING_IS_DIGIT */
    1, /* STRING_ITOS */
    1, /* STRING_STOI */
    1, /* STRING_TO_CODE */
    1, /* STRING_FROM_CODE */
    1, /* STRING_TOLOWER */
    1, /* STRING_TOUPPER */
    1, /* STRING_REV */
    0, /* CONST_STRING */
    1, /* SEQUENCE_TYPE */
    0, /* CONST_SEQUENCE */
    1, /* SEQ_UNIT */
    2, /* SEQ_NTH */
    2, /* SEQ_NTH_TOTAL */
    1, /* STRING_TO_REGEXP */
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_CONCAT */
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_UNION */
    expr::NodeValue::MAX_CHILDREN, /* REGEXP_INTER */
    2, /* REGEXP_DIFF */
    1, /* REGEXP_STAR */
    1, /* REGEXP_PLUS */
    1, /* REGEXP_OPT */
    2, /* REGEXP_RANGE */
    1, /* REGEXP_COMPLEMENT */
    0, /* REGEXP_EMPTY */
    0, /* REGEXP_SIGMA */
    0, /* REGEXP_REPEAT_OP */
    1, /* REGEXP_REPEAT */
    0, /* REGEXP_LOOP_OP */
    1, /* REGEXP_LOOP */
    1, /* REGEXP_RV */
    3, /* FORALL */
    3, /* EXISTS */
    0, /* INST_CONSTANT */
    expr::NodeValue::MAX_CHILDREN, /* BOUND_VAR_LIST */
    expr::NodeValue::MAX_CHILDREN, /* INST_PATTERN */
    1, /* INST_NO_PATTERN */
    1, /* INST_ATTRIBUTE */
    expr::NodeValue::MAX_CHILDREN, /* INST_POOL */
    2, /* INST_ADD_TO_POOL */
    2, /* SKOLEM_ADD_TO_POOL */
    expr::NodeValue::MAX_CHILDREN, /* INST_PATTERN_LIST */
// clang-format on

    0, /* LAST_KIND */
  };

  return ubs[k];
}
}  // namespace metakind

/**
 * Map a kind of the operator to the kind of the enclosing expression. For
 * example, since the kind of functions is just VARIABLE, it should map
 * VARIABLE to APPLY_UF.
 */
Kind operatorToKind(::cvc5::expr::NodeValue* nv)
{
  if(nv->getKind() == kind::BUILTIN) {
    return nv->getConst<Kind>();
  } else if(nv->getKind() == kind::LAMBDA) {
    return kind::APPLY_UF;
  }

  switch (Kind k CVC5_UNUSED = nv->getKind())
  {
// clang-format off


    /* from builtin */
    case kind::SORT_TAG: return kind::SORT_TYPE;

    /* from booleans */

    /* from uf */
    case kind::VARIABLE: return kind::APPLY_UF;
    case kind::APPLY_UF: return kind::PARTIAL_APPLY_UF;

    /* from arith */
    case kind::DIVISIBLE_OP: return kind::DIVISIBLE;
    case kind::INDEXED_ROOT_PREDICATE_OP: return kind::INDEXED_ROOT_PREDICATE;
    case kind::IAND_OP: return kind::IAND;

    /* from bv */
    case kind::BITVECTOR_BITOF_OP: return kind::BITVECTOR_BITOF;
    case kind::BITVECTOR_EXTRACT_OP: return kind::BITVECTOR_EXTRACT;
    case kind::BITVECTOR_REPEAT_OP: return kind::BITVECTOR_REPEAT;
    case kind::BITVECTOR_ROTATE_LEFT_OP: return kind::BITVECTOR_ROTATE_LEFT;
    case kind::BITVECTOR_ROTATE_RIGHT_OP: return kind::BITVECTOR_ROTATE_RIGHT;
    case kind::BITVECTOR_SIGN_EXTEND_OP: return kind::BITVECTOR_SIGN_EXTEND;
    case kind::BITVECTOR_ZERO_EXTEND_OP: return kind::BITVECTOR_ZERO_EXTEND;
    case kind::INT_TO_BITVECTOR_OP: return kind::INT_TO_BITVECTOR;

    /* from fp */
    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR;
    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: return kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT;
    case kind::FLOATINGPOINT_TO_FP_REAL_OP: return kind::FLOATINGPOINT_TO_FP_REAL;
    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR;
    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: return kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR;
    case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: return kind::FLOATINGPOINT_TO_FP_GENERIC;
    case kind::FLOATINGPOINT_TO_UBV_OP: return kind::FLOATINGPOINT_TO_UBV;
    case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP: return kind::FLOATINGPOINT_TO_UBV_TOTAL;
    case kind::FLOATINGPOINT_TO_SBV_OP: return kind::FLOATINGPOINT_TO_SBV;
    case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP: return kind::FLOATINGPOINT_TO_SBV_TOTAL;

    /* from arrays */

    /* from datatypes */
    case kind::APPLY_TYPE_ASCRIPTION: return kind::APPLY_CONSTRUCTOR;
    case kind::SELECTOR_TYPE: return kind::APPLY_SELECTOR;
    case kind::TESTER_TYPE: return kind::APPLY_TESTER;
    case kind::UPDATER_TYPE: return kind::APPLY_UPDATER;
    case kind::ASCRIPTION_TYPE: return kind::APPLY_TYPE_ASCRIPTION;
    case kind::TUPLE_PROJECT_OP: return kind::TUPLE_PROJECT;

    /* from sep */

    /* from sets */
    case kind::SINGLETON_OP: return kind::SINGLETON;

    /* from bags */
    case kind::MK_BAG_OP: return kind::MK_BAG;

    /* from strings */
    case kind::REGEXP_REPEAT_OP: return kind::REGEXP_REPEAT;
    case kind::REGEXP_LOOP_OP: return kind::REGEXP_LOOP;

    /* from quantifiers */
// clang-format on

    default: return kind::UNDEFINED_KIND; /* LAST_KIND */
  };
}

}  // namespace kind
}  // namespace cvc5

Generated by: GCOVR (Version 3.2)