Head

GCC Code Coverage Report
Directory:	.		Exec	Total	Coverage
File:	build-coverage/src/expr/metakind.cpp	Lines:	580	743	78.1 %
Date:	2021-09-05	Branches:	366	786	46.6 %

/******************************************************************************
 * 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-09-05/src/expr/metakind_template.cpp /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/builtin/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/booleans/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/uf/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/arith/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/bv/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/fp/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/arrays/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/datatypes/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/sep/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/sets/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/bags/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/src/theory/strings/kinds /barrett/scratch/cvc4-nightly/src/cvc5-2021-09-05/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>

// clang-format off

// #include "theory/builtin/::cvc5::theory::builtin::TheoryBuiltin"
#include "expr/uninterpreted_constant.h"
#include "util/abstract_value.h"
#include "expr/kind.h"
// #include "theory/booleans/::cvc5::theory::booleans::TheoryBool"
#include "util/bool.h"
// #include "theory/uf/::cvc5::theory::uf::TheoryUF"
// #include "theory/arith/::cvc5::theory::arith::TheoryArith"
#include "util/divisible.h"
#include "util/rational.h"
#include "util/indexed_root_predicate.h"
#include "util/iand.h"
// #include "theory/bv/::cvc5::theory::bv::TheoryBV"
#include "util/bitvector.h"
// #include "theory/fp/::cvc5::theory::fp::TheoryFp"
#include "util/floatingpoint.h"
#include "util/roundingmode.h"
// #include "theory/arrays/::cvc5::theory::arrays::TheoryArrays"
#include "expr/array_store_all.h"
// #include "theory/datatypes/::cvc5::theory::datatypes::TheoryDatatypes"
#include "expr/datatype_index.h"
#include "expr/ascription_type.h"
#include "theory/datatypes/tuple_project_op.h"
// #include "theory/sep/::cvc5::theory::sep::TheorySep"
// #include "theory/sets/::cvc5::theory::sets::TheorySets"
#include "expr/emptyset.h"
#include "theory/sets/singleton_op.h"
// #include "theory/bags/::cvc5::theory::bags::TheoryBags"
#include "expr/emptybag.h"
#include "theory/bags/make_bag_op.h"
// #include "theory/strings/::cvc5::theory::strings::TheoryStrings"
#include "util/string.h"
#include "expr/sequence.h"
#include "util/regexp.h"
// #include "theory/quantifiers/::cvc5::theory::quantifiers::TheoryQuantifiers"
// clang-format off

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, /* POW2 */
    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_ADD */
    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 */
    metakind::OPERATOR, /* BAG_MAP */

    /* 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_CONTAINS */
    metakind::OPERATOR, /* STRING_LT */
    metakind::OPERATOR, /* STRING_LEQ */
    metakind::OPERATOR, /* STRING_INDEXOF */
    metakind::OPERATOR, /* STRING_INDEXOF_RE */
    metakind::OPERATOR, /* STRING_REPLACE */
    metakind::OPERATOR, /* STRING_REPLACE_ALL */
    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 "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 <>
UninterpretedConstant const& NodeValue::getConst< UninterpretedConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::UNINTERPRETED_CONSTANT, *this,
                 "Improper kind for getConst<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< UninterpretedConstant const* >(d_children)
    : *reinterpret_cast< UninterpretedConstant const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
AbstractValue const& NodeValue::getConst< AbstractValue >() const {
  AssertArgument(getKind() == ::cvc5::kind::ABSTRACT_VALUE, *this,
                 "Improper kind for getConst<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< AbstractValue const* >(d_children)
    : *reinterpret_cast< AbstractValue const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
Kind const& NodeValue::getConst< Kind >() const {
  AssertArgument(getKind() == ::cvc5::kind::BUILTIN, *this,
                 "Improper kind for getConst<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< Kind const* >(d_children)
    : *reinterpret_cast< Kind const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
TypeConstant const& NodeValue::getConst< TypeConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::TYPE_CONSTANT, *this,
                 "Improper kind for getConst<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< TypeConstant const* >(d_children)
    : *reinterpret_cast< 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 "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 <>
Divisible const& NodeValue::getConst< Divisible >() const {
  AssertArgument(getKind() == ::cvc5::kind::DIVISIBLE_OP, *this,
                 "Improper kind for getConst<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< Divisible const* >(d_children)
    : *reinterpret_cast< Divisible const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
Rational const& NodeValue::getConst< Rational >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_RATIONAL, *this,
                 "Improper kind for getConst<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< Rational const* >(d_children)
    : *reinterpret_cast< Rational const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
IndexedRootPredicate const& NodeValue::getConst< IndexedRootPredicate >() const {
  AssertArgument(getKind() == ::cvc5::kind::INDEXED_ROOT_PREDICATE_OP, *this,
                 "Improper kind for getConst<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< IndexedRootPredicate const* >(d_children)
    : *reinterpret_cast< IndexedRootPredicate const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
IntAnd const& NodeValue::getConst< IntAnd >() const {
  AssertArgument(getKind() == ::cvc5::kind::IAND_OP, *this,
                 "Improper kind for getConst<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< IntAnd const* >(d_children)
    : *reinterpret_cast< IntAnd const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorSize const& NodeValue::getConst< BitVectorSize >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_TYPE, *this,
                 "Improper kind for getConst<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< BitVectorSize const* >(d_children)
    : *reinterpret_cast< BitVectorSize const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVector const& NodeValue::getConst< BitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_BITVECTOR, *this,
                 "Improper kind for getConst<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< BitVector const* >(d_children)
    : *reinterpret_cast< BitVector const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorBitOf const& NodeValue::getConst< BitVectorBitOf >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_BITOF_OP, *this,
                 "Improper kind for getConst<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< BitVectorBitOf const* >(d_children)
    : *reinterpret_cast< BitVectorBitOf const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorExtract const& NodeValue::getConst< BitVectorExtract >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_EXTRACT_OP, *this,
                 "Improper kind for getConst<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< BitVectorExtract const* >(d_children)
    : *reinterpret_cast< BitVectorExtract const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorRepeat const& NodeValue::getConst< BitVectorRepeat >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_REPEAT_OP, *this,
                 "Improper kind for getConst<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< BitVectorRepeat const* >(d_children)
    : *reinterpret_cast< BitVectorRepeat const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorRotateLeft const& NodeValue::getConst< BitVectorRotateLeft >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ROTATE_LEFT_OP, *this,
                 "Improper kind for getConst<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< BitVectorRotateLeft const* >(d_children)
    : *reinterpret_cast< BitVectorRotateLeft const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorRotateRight const& NodeValue::getConst< BitVectorRotateRight >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ROTATE_RIGHT_OP, *this,
                 "Improper kind for getConst<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< BitVectorRotateRight const* >(d_children)
    : *reinterpret_cast< BitVectorRotateRight const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorSignExtend const& NodeValue::getConst< BitVectorSignExtend >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_SIGN_EXTEND_OP, *this,
                 "Improper kind for getConst<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< BitVectorSignExtend const* >(d_children)
    : *reinterpret_cast< BitVectorSignExtend const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
BitVectorZeroExtend const& NodeValue::getConst< BitVectorZeroExtend >() const {
  AssertArgument(getKind() == ::cvc5::kind::BITVECTOR_ZERO_EXTEND_OP, *this,
                 "Improper kind for getConst<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< BitVectorZeroExtend const* >(d_children)
    : *reinterpret_cast< BitVectorZeroExtend const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
IntToBitVector const& NodeValue::getConst< IntToBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::INT_TO_BITVECTOR_OP, *this,
                 "Improper kind for getConst<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< IntToBitVector const* >(d_children)
    : *reinterpret_cast< IntToBitVector const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPoint const& NodeValue::getConst< FloatingPoint >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_FLOATINGPOINT, *this,
                 "Improper kind for getConst<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< FloatingPoint const* >(d_children)
    : *reinterpret_cast< FloatingPoint const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
RoundingMode const& NodeValue::getConst< RoundingMode >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_ROUNDINGMODE, *this,
                 "Improper kind for getConst<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< RoundingMode const* >(d_children)
    : *reinterpret_cast< RoundingMode const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointSize const& NodeValue::getConst< FloatingPointSize >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TYPE, *this,
                 "Improper kind for getConst<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< FloatingPointSize const* >(d_children)
    : *reinterpret_cast< FloatingPointSize const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPIEEEBitVector const& NodeValue::getConst< FloatingPointToFPIEEEBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPIEEEBitVector const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPIEEEBitVector const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPFloatingPoint const& NodeValue::getConst< FloatingPointToFPFloatingPoint >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPFloatingPoint const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPFloatingPoint const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPReal const& NodeValue::getConst< FloatingPointToFPReal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_REAL_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPReal const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPReal const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPSignedBitVector const& NodeValue::getConst< FloatingPointToFPSignedBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPSignedBitVector const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPSignedBitVector const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPUnsignedBitVector const& NodeValue::getConst< FloatingPointToFPUnsignedBitVector >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPUnsignedBitVector const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPUnsignedBitVector const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToFPGeneric const& NodeValue::getConst< FloatingPointToFPGeneric >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_FP_GENERIC_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToFPGeneric const* >(d_children)
    : *reinterpret_cast< FloatingPointToFPGeneric const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToUBV const& NodeValue::getConst< FloatingPointToUBV >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_UBV_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToUBV const* >(d_children)
    : *reinterpret_cast< FloatingPointToUBV const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToUBVTotal const& NodeValue::getConst< FloatingPointToUBVTotal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToUBVTotal const* >(d_children)
    : *reinterpret_cast< FloatingPointToUBVTotal const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToSBV const& NodeValue::getConst< FloatingPointToSBV >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_SBV_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToSBV const* >(d_children)
    : *reinterpret_cast< FloatingPointToSBV const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
FloatingPointToSBVTotal const& NodeValue::getConst< FloatingPointToSBVTotal >() const {
  AssertArgument(getKind() == ::cvc5::kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, *this,
                 "Improper kind for getConst<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< FloatingPointToSBVTotal const* >(d_children)
    : *reinterpret_cast< FloatingPointToSBVTotal const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
ArrayStoreAll const& NodeValue::getConst< ArrayStoreAll >() const {
  AssertArgument(getKind() == ::cvc5::kind::STORE_ALL, *this,
                 "Improper kind for getConst<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< ArrayStoreAll const* >(d_children)
    : *reinterpret_cast< ArrayStoreAll const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
DatatypeIndexConstant const& NodeValue::getConst< DatatypeIndexConstant >() const {
  AssertArgument(getKind() == ::cvc5::kind::DATATYPE_TYPE, *this,
                 "Improper kind for getConst<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< DatatypeIndexConstant const* >(d_children)
    : *reinterpret_cast< DatatypeIndexConstant const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
AscriptionType const& NodeValue::getConst< AscriptionType >() const {
  AssertArgument(getKind() == ::cvc5::kind::ASCRIPTION_TYPE, *this,
                 "Improper kind for getConst<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< AscriptionType const* >(d_children)
    : *reinterpret_cast< AscriptionType const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
TupleProjectOp const& NodeValue::getConst< TupleProjectOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::TUPLE_PROJECT_OP, *this,
                 "Improper kind for getConst<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< TupleProjectOp const* >(d_children)
    : *reinterpret_cast< TupleProjectOp const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
EmptySet const& NodeValue::getConst< EmptySet >() const {
  AssertArgument(getKind() == ::cvc5::kind::EMPTYSET, *this,
                 "Improper kind for getConst<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< EmptySet const* >(d_children)
    : *reinterpret_cast< EmptySet const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
SingletonOp const& NodeValue::getConst< SingletonOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::SINGLETON_OP, *this,
                 "Improper kind for getConst<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< SingletonOp const* >(d_children)
    : *reinterpret_cast< SingletonOp const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
EmptyBag const& NodeValue::getConst< EmptyBag >() const {
  AssertArgument(getKind() == ::cvc5::kind::EMPTYBAG, *this,
                 "Improper kind for getConst<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< EmptyBag const* >(d_children)
    : *reinterpret_cast< EmptyBag const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
MakeBagOp const& NodeValue::getConst< MakeBagOp >() const {
  AssertArgument(getKind() == ::cvc5::kind::MK_BAG_OP, *this,
                 "Improper kind for getConst<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< MakeBagOp const* >(d_children)
    : *reinterpret_cast< MakeBagOp const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
String const& NodeValue::getConst< String >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_STRING, *this,
                 "Improper kind for getConst<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< String const* >(d_children)
    : *reinterpret_cast< String const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
Sequence const& NodeValue::getConst< Sequence >() const {
  AssertArgument(getKind() == ::cvc5::kind::CONST_SEQUENCE, *this,
                 "Improper kind for getConst<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< Sequence const* >(d_children)
    : *reinterpret_cast< Sequence const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
RegExpRepeat const& NodeValue::getConst< RegExpRepeat >() const {
  AssertArgument(getKind() == ::cvc5::kind::REGEXP_REPEAT_OP, *this,
                 "Improper kind for getConst<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< RegExpRepeat const* >(d_children)
    : *reinterpret_cast< RegExpRepeat const* >(d_children[0]);
}

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


// The reinterpret_cast of d_children to "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 <>
RegExpLoop const& NodeValue::getConst< RegExpLoop >() const {
  AssertArgument(getKind() == ::cvc5::kind::REGEXP_LOOP_OP, *this,
                 "Improper kind for getConst<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< RegExpLoop const* >(d_children)
    : *reinterpret_cast< 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< UninterpretedConstant >());

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  case kind::REGEXP_LOOP_OP:
    return ::cvc5::RegExpLoopHashFunction()(nv->getConst< 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< UninterpretedConstant >();
    break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  case kind::REGEXP_LOOP_OP:
    out << nv->getConst< 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::destroy_at(reinterpret_cast< UninterpretedConstant* >(nv->d_children));
    break;

  case kind::ABSTRACT_VALUE:
    std::destroy_at(reinterpret_cast< AbstractValue* >(nv->d_children));
    break;

  case kind::BUILTIN:
    std::destroy_at(reinterpret_cast< Kind* >(nv->d_children));
    break;

  case kind::TYPE_CONSTANT:
    std::destroy_at(reinterpret_cast< TypeConstant* >(nv->d_children));
    break;

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

  case kind::DIVISIBLE_OP:
    std::destroy_at(reinterpret_cast< Divisible* >(nv->d_children));
    break;

  case kind::CONST_RATIONAL:
    std::destroy_at(reinterpret_cast< Rational* >(nv->d_children));
    break;

  case kind::INDEXED_ROOT_PREDICATE_OP:
    std::destroy_at(reinterpret_cast< IndexedRootPredicate* >(nv->d_children));
    break;

  case kind::IAND_OP:
    std::destroy_at(reinterpret_cast< IntAnd* >(nv->d_children));
    break;

  case kind::BITVECTOR_TYPE:
    std::destroy_at(reinterpret_cast< BitVectorSize* >(nv->d_children));
    break;

  case kind::CONST_BITVECTOR:
    std::destroy_at(reinterpret_cast< BitVector* >(nv->d_children));
    break;

  case kind::BITVECTOR_BITOF_OP:
    std::destroy_at(reinterpret_cast< BitVectorBitOf* >(nv->d_children));
    break;

  case kind::BITVECTOR_EXTRACT_OP:
    std::destroy_at(reinterpret_cast< BitVectorExtract* >(nv->d_children));
    break;

  case kind::BITVECTOR_REPEAT_OP:
    std::destroy_at(reinterpret_cast< BitVectorRepeat* >(nv->d_children));
    break;

  case kind::BITVECTOR_ROTATE_LEFT_OP:
    std::destroy_at(reinterpret_cast< BitVectorRotateLeft* >(nv->d_children));
    break;

  case kind::BITVECTOR_ROTATE_RIGHT_OP:
    std::destroy_at(reinterpret_cast< BitVectorRotateRight* >(nv->d_children));
    break;

  case kind::BITVECTOR_SIGN_EXTEND_OP:
    std::destroy_at(reinterpret_cast< BitVectorSignExtend* >(nv->d_children));
    break;

  case kind::BITVECTOR_ZERO_EXTEND_OP:
    std::destroy_at(reinterpret_cast< BitVectorZeroExtend* >(nv->d_children));
    break;

  case kind::INT_TO_BITVECTOR_OP:
    std::destroy_at(reinterpret_cast< IntToBitVector* >(nv->d_children));
    break;

  case kind::CONST_FLOATINGPOINT:
    std::destroy_at(reinterpret_cast< FloatingPoint* >(nv->d_children));
    break;

  case kind::CONST_ROUNDINGMODE:
    std::destroy_at(reinterpret_cast< RoundingMode* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TYPE:
    std::destroy_at(reinterpret_cast< FloatingPointSize* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPIEEEBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPFloatingPoint* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_REAL_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPReal* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPSignedBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPUnsignedBitVector* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_FP_GENERIC_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToFPGeneric* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_UBV_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToUBV* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_UBV_TOTAL_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToUBVTotal* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_SBV_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToSBV* >(nv->d_children));
    break;

  case kind::FLOATINGPOINT_TO_SBV_TOTAL_OP:
    std::destroy_at(reinterpret_cast< FloatingPointToSBVTotal* >(nv->d_children));
    break;

  case kind::STORE_ALL:
    std::destroy_at(reinterpret_cast< ArrayStoreAll* >(nv->d_children));
    break;

  case kind::DATATYPE_TYPE:
    std::destroy_at(reinterpret_cast< DatatypeIndexConstant* >(nv->d_children));
    break;

  case kind::ASCRIPTION_TYPE:
    std::destroy_at(reinterpret_cast< AscriptionType* >(nv->d_children));
    break;

  case kind::TUPLE_PROJECT_OP:
    std::destroy_at(reinterpret_cast< TupleProjectOp* >(nv->d_children));
    break;

  case kind::EMPTYSET:
    std::destroy_at(reinterpret_cast< EmptySet* >(nv->d_children));
    break;

  case kind::SINGLETON_OP:
    std::destroy_at(reinterpret_cast< SingletonOp* >(nv->d_children));
    break;

  case kind::EMPTYBAG:
    std::destroy_at(reinterpret_cast< EmptyBag* >(nv->d_children));
    break;

  case kind::MK_BAG_OP:
    std::destroy_at(reinterpret_cast< MakeBagOp* >(nv->d_children));
    break;

  case kind::CONST_STRING:
    std::destroy_at(reinterpret_cast< String* >(nv->d_children));
    break;

  case kind::CONST_SEQUENCE:
    std::destroy_at(reinterpret_cast< Sequence* >(nv->d_children));
    break;

  case kind::REGEXP_REPEAT_OP:
    std::destroy_at(reinterpret_cast< RegExpRepeat* >(nv->d_children));
    break;

  case kind::REGEXP_LOOP_OP:
    std::destroy_at(reinterpret_cast< 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, /* POW2 */
    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_ADD */
    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, /* BAG_MAP */
    2, /* STRING_CONCAT */
    2, /* STRING_IN_REGEXP */
    1, /* STRING_LENGTH */
    3, /* STRING_SUBSTR */
    3, /* STRING_UPDATE */
    2, /* STRING_CHARAT */
    2, /* STRING_CONTAINS */
    2, /* STRING_LT */
    2, /* STRING_LEQ */
    3, /* STRING_INDEXOF */
    3, /* STRING_INDEXOF_RE */
    3, /* STRING_REPLACE */
    3, /* STRING_REPLACE_ALL */
    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, /* POW2 */
    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_ADD */
    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 */
    2, /* BAG_MAP */
    expr::NodeValue::MAX_CHILDREN, /* STRING_CONCAT */
    2, /* STRING_IN_REGEXP */
    1, /* STRING_LENGTH */
    3, /* STRING_SUBSTR */
    3, /* STRING_UPDATE */
    2, /* STRING_CHARAT */
    2, /* STRING_CONTAINS */
    2, /* STRING_LT */
    2, /* STRING_LEQ */
    3, /* STRING_INDEXOF */
    3, /* STRING_INDEXOF_RE */
    3, /* STRING_REPLACE */
    3, /* STRING_REPLACE_ALL */
    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 */
    expr::NodeValue::MAX_CHILDREN, /* 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)