From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 16 Mar 2022 03:48:34 +0000 (-0700)
Subject: api: Print the correct string for external kinds. (#8320)
X-Git-Tag: cvc5-1.0.0~241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=708aee85110e74620641532bf1708e0b8cfa29cc;p=cvc5.git

api: Print the correct string for external kinds. (#8320)

We currently print the string representation of the internal kind.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index dda7aacc7..bef2b9ac9 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -104,286 +104,299 @@ struct APIStatistics
 /* Kind                                                                       */
 /* -------------------------------------------------------------------------- */
 
+#define KIND_ENUM(external_name, internal_name)                  \
+  {                                                              \
+    external_name, std::make_pair(internal_name, #external_name) \
+  }
+
 /* Mapping from external (API) kind to internal kind. */
-const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
-    {INTERNAL_KIND, cvc5::Kind::UNDEFINED_KIND},
-    {UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND},
-    {NULL_EXPR, cvc5::Kind::NULL_EXPR},
-    /* Builtin ------------------------------------------------------------- */
-    {UNINTERPRETED_SORT_VALUE, cvc5::Kind::UNINTERPRETED_SORT_VALUE},
-    {EQUAL, cvc5::Kind::EQUAL},
-    {DISTINCT, cvc5::Kind::DISTINCT},
-    {CONSTANT, cvc5::Kind::VARIABLE},
-    {VARIABLE, cvc5::Kind::BOUND_VARIABLE},
-    {SEXPR, cvc5::Kind::SEXPR},
-    {LAMBDA, cvc5::Kind::LAMBDA},
-    {WITNESS, cvc5::Kind::WITNESS},
-    /* Boolean ------------------------------------------------------------- */
-    {CONST_BOOLEAN, cvc5::Kind::CONST_BOOLEAN},
-    {NOT, cvc5::Kind::NOT},
-    {AND, cvc5::Kind::AND},
-    {IMPLIES, cvc5::Kind::IMPLIES},
-    {OR, cvc5::Kind::OR},
-    {XOR, cvc5::Kind::XOR},
-    {ITE, cvc5::Kind::ITE},
-    /* UF ------------------------------------------------------------------ */
-    {APPLY_UF, cvc5::Kind::APPLY_UF},
-    {CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT},
-    {HO_APPLY, cvc5::Kind::HO_APPLY},
-    /* Arithmetic ---------------------------------------------------------- */
-    {ADD, cvc5::Kind::ADD},
-    {MULT, cvc5::Kind::MULT},
-    {IAND, cvc5::Kind::IAND},
-    {POW2, cvc5::Kind::POW2},
-    {SUB, cvc5::Kind::SUB},
-    {NEG, cvc5::Kind::NEG},
-    {DIVISION, cvc5::Kind::DIVISION},
-    {INTS_DIVISION, cvc5::Kind::INTS_DIVISION},
-    {INTS_MODULUS, cvc5::Kind::INTS_MODULUS},
-    {ABS, cvc5::Kind::ABS},
-    {DIVISIBLE, cvc5::Kind::DIVISIBLE},
-    {POW, cvc5::Kind::POW},
-    {EXPONENTIAL, cvc5::Kind::EXPONENTIAL},
-    {SINE, cvc5::Kind::SINE},
-    {COSINE, cvc5::Kind::COSINE},
-    {TANGENT, cvc5::Kind::TANGENT},
-    {COSECANT, cvc5::Kind::COSECANT},
-    {SECANT, cvc5::Kind::SECANT},
-    {COTANGENT, cvc5::Kind::COTANGENT},
-    {ARCSINE, cvc5::Kind::ARCSINE},
-    {ARCCOSINE, cvc5::Kind::ARCCOSINE},
-    {ARCTANGENT, cvc5::Kind::ARCTANGENT},
-    {ARCCOSECANT, cvc5::Kind::ARCCOSECANT},
-    {ARCSECANT, cvc5::Kind::ARCSECANT},
-    {ARCCOTANGENT, cvc5::Kind::ARCCOTANGENT},
-    {SQRT, cvc5::Kind::SQRT},
-    {CONST_RATIONAL, cvc5::Kind::CONST_RATIONAL},
-    {LT, cvc5::Kind::LT},
-    {LEQ, cvc5::Kind::LEQ},
-    {GT, cvc5::Kind::GT},
-    {GEQ, cvc5::Kind::GEQ},
-    {IS_INTEGER, cvc5::Kind::IS_INTEGER},
-    {TO_INTEGER, cvc5::Kind::TO_INTEGER},
-    {TO_REAL, cvc5::Kind::TO_REAL},
-    {PI, cvc5::Kind::PI},
-    /* BV ------------------------------------------------------------------ */
-    {CONST_BITVECTOR, cvc5::Kind::CONST_BITVECTOR},
-    {BITVECTOR_CONCAT, cvc5::Kind::BITVECTOR_CONCAT},
-    {BITVECTOR_AND, cvc5::Kind::BITVECTOR_AND},
-    {BITVECTOR_OR, cvc5::Kind::BITVECTOR_OR},
-    {BITVECTOR_XOR, cvc5::Kind::BITVECTOR_XOR},
-    {BITVECTOR_NOT, cvc5::Kind::BITVECTOR_NOT},
-    {BITVECTOR_NAND, cvc5::Kind::BITVECTOR_NAND},
-    {BITVECTOR_NOR, cvc5::Kind::BITVECTOR_NOR},
-    {BITVECTOR_XNOR, cvc5::Kind::BITVECTOR_XNOR},
-    {BITVECTOR_COMP, cvc5::Kind::BITVECTOR_COMP},
-    {BITVECTOR_MULT, cvc5::Kind::BITVECTOR_MULT},
-    {BITVECTOR_ADD, cvc5::Kind::BITVECTOR_ADD},
-    {BITVECTOR_SUB, cvc5::Kind::BITVECTOR_SUB},
-    {BITVECTOR_NEG, cvc5::Kind::BITVECTOR_NEG},
-    {BITVECTOR_UDIV, cvc5::Kind::BITVECTOR_UDIV},
-    {BITVECTOR_UREM, cvc5::Kind::BITVECTOR_UREM},
-    {BITVECTOR_SDIV, cvc5::Kind::BITVECTOR_SDIV},
-    {BITVECTOR_SREM, cvc5::Kind::BITVECTOR_SREM},
-    {BITVECTOR_SMOD, cvc5::Kind::BITVECTOR_SMOD},
-    {BITVECTOR_SHL, cvc5::Kind::BITVECTOR_SHL},
-    {BITVECTOR_LSHR, cvc5::Kind::BITVECTOR_LSHR},
-    {BITVECTOR_ASHR, cvc5::Kind::BITVECTOR_ASHR},
-    {BITVECTOR_ULT, cvc5::Kind::BITVECTOR_ULT},
-    {BITVECTOR_ULE, cvc5::Kind::BITVECTOR_ULE},
-    {BITVECTOR_UGT, cvc5::Kind::BITVECTOR_UGT},
-    {BITVECTOR_UGE, cvc5::Kind::BITVECTOR_UGE},
-    {BITVECTOR_SLT, cvc5::Kind::BITVECTOR_SLT},
-    {BITVECTOR_SLE, cvc5::Kind::BITVECTOR_SLE},
-    {BITVECTOR_SGT, cvc5::Kind::BITVECTOR_SGT},
-    {BITVECTOR_SGE, cvc5::Kind::BITVECTOR_SGE},
-    {BITVECTOR_ULTBV, cvc5::Kind::BITVECTOR_ULTBV},
-    {BITVECTOR_SLTBV, cvc5::Kind::BITVECTOR_SLTBV},
-    {BITVECTOR_ITE, cvc5::Kind::BITVECTOR_ITE},
-    {BITVECTOR_REDOR, cvc5::Kind::BITVECTOR_REDOR},
-    {BITVECTOR_REDAND, cvc5::Kind::BITVECTOR_REDAND},
-    {BITVECTOR_EXTRACT, cvc5::Kind::BITVECTOR_EXTRACT},
-    {BITVECTOR_REPEAT, cvc5::Kind::BITVECTOR_REPEAT},
-    {BITVECTOR_ZERO_EXTEND, cvc5::Kind::BITVECTOR_ZERO_EXTEND},
-    {BITVECTOR_SIGN_EXTEND, cvc5::Kind::BITVECTOR_SIGN_EXTEND},
-    {BITVECTOR_ROTATE_LEFT, cvc5::Kind::BITVECTOR_ROTATE_LEFT},
-    {BITVECTOR_ROTATE_RIGHT, cvc5::Kind::BITVECTOR_ROTATE_RIGHT},
-    {INT_TO_BITVECTOR, cvc5::Kind::INT_TO_BITVECTOR},
-    {BITVECTOR_TO_NAT, cvc5::Kind::BITVECTOR_TO_NAT},
-    /* FP ------------------------------------------------------------------ */
-    {CONST_FLOATINGPOINT, cvc5::Kind::CONST_FLOATINGPOINT},
-    {CONST_ROUNDINGMODE, cvc5::Kind::CONST_ROUNDINGMODE},
-    {FLOATINGPOINT_FP, cvc5::Kind::FLOATINGPOINT_FP},
-    {FLOATINGPOINT_EQ, cvc5::Kind::FLOATINGPOINT_EQ},
-    {FLOATINGPOINT_ABS, cvc5::Kind::FLOATINGPOINT_ABS},
-    {FLOATINGPOINT_NEG, cvc5::Kind::FLOATINGPOINT_NEG},
-    {FLOATINGPOINT_ADD, cvc5::Kind::FLOATINGPOINT_ADD},
-    {FLOATINGPOINT_SUB, cvc5::Kind::FLOATINGPOINT_SUB},
-    {FLOATINGPOINT_MULT, cvc5::Kind::FLOATINGPOINT_MULT},
-    {FLOATINGPOINT_DIV, cvc5::Kind::FLOATINGPOINT_DIV},
-    {FLOATINGPOINT_FMA, cvc5::Kind::FLOATINGPOINT_FMA},
-    {FLOATINGPOINT_SQRT, cvc5::Kind::FLOATINGPOINT_SQRT},
-    {FLOATINGPOINT_REM, cvc5::Kind::FLOATINGPOINT_REM},
-    {FLOATINGPOINT_RTI, cvc5::Kind::FLOATINGPOINT_RTI},
-    {FLOATINGPOINT_MIN, cvc5::Kind::FLOATINGPOINT_MIN},
-    {FLOATINGPOINT_MAX, cvc5::Kind::FLOATINGPOINT_MAX},
-    {FLOATINGPOINT_LEQ, cvc5::Kind::FLOATINGPOINT_LEQ},
-    {FLOATINGPOINT_LT, cvc5::Kind::FLOATINGPOINT_LT},
-    {FLOATINGPOINT_GEQ, cvc5::Kind::FLOATINGPOINT_GEQ},
-    {FLOATINGPOINT_GT, cvc5::Kind::FLOATINGPOINT_GT},
-    {FLOATINGPOINT_IS_NORMAL, cvc5::Kind::FLOATINGPOINT_IS_NORMAL},
-    {FLOATINGPOINT_IS_SUBNORMAL, cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL},
-    {FLOATINGPOINT_IS_ZERO, cvc5::Kind::FLOATINGPOINT_IS_ZERO},
-    {FLOATINGPOINT_IS_INF, cvc5::Kind::FLOATINGPOINT_IS_INF},
-    {FLOATINGPOINT_IS_NAN, cvc5::Kind::FLOATINGPOINT_IS_NAN},
-    {FLOATINGPOINT_IS_NEG, cvc5::Kind::FLOATINGPOINT_IS_NEG},
-    {FLOATINGPOINT_IS_POS, cvc5::Kind::FLOATINGPOINT_IS_POS},
-    {FLOATINGPOINT_TO_FP_FROM_FP, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP},
-    {FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
-     cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV},
-    {FLOATINGPOINT_TO_FP_FROM_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL},
-    {FLOATINGPOINT_TO_FP_FROM_SBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV},
-    {FLOATINGPOINT_TO_FP_FROM_UBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV},
-    {FLOATINGPOINT_TO_FP_GENERIC, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC},
-    {FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV},
-    {FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV},
-    {FLOATINGPOINT_TO_REAL, cvc5::Kind::FLOATINGPOINT_TO_REAL},
-    /* Arrays -------------------------------------------------------------- */
-    {SELECT, cvc5::Kind::SELECT},
-    {STORE, cvc5::Kind::STORE},
-    {CONST_ARRAY, cvc5::Kind::STORE_ALL},
-    {EQ_RANGE, cvc5::Kind::EQ_RANGE},
-    /* Datatypes ----------------------------------------------------------- */
-    {APPLY_SELECTOR, cvc5::Kind::APPLY_SELECTOR},
-    {APPLY_CONSTRUCTOR, cvc5::Kind::APPLY_CONSTRUCTOR},
-    {APPLY_TESTER, cvc5::Kind::APPLY_TESTER},
-    {APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER},
-    {DT_SIZE, cvc5::Kind::DT_SIZE},
-    {MATCH, cvc5::Kind::MATCH},
-    {MATCH_CASE, cvc5::Kind::MATCH_CASE},
-    {MATCH_BIND_CASE, cvc5::Kind::MATCH_BIND_CASE},
-    {TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT},
-    /* Separation Logic ---------------------------------------------------- */
-    {SEP_NIL, cvc5::Kind::SEP_NIL},
-    {SEP_EMP, cvc5::Kind::SEP_EMP},
-    {SEP_PTO, cvc5::Kind::SEP_PTO},
-    {SEP_STAR, cvc5::Kind::SEP_STAR},
-    {SEP_WAND, cvc5::Kind::SEP_WAND},
-    /* Sets ---------------------------------------------------------------- */
-    {SET_EMPTY, cvc5::Kind::SET_EMPTY},
-    {SET_UNION, cvc5::Kind::SET_UNION},
-    {SET_INTER, cvc5::Kind::SET_INTER},
-    {SET_MINUS, cvc5::Kind::SET_MINUS},
-    {SET_SUBSET, cvc5::Kind::SET_SUBSET},
-    {SET_MEMBER, cvc5::Kind::SET_MEMBER},
-    {SET_SINGLETON, cvc5::Kind::SET_SINGLETON},
-    {SET_INSERT, cvc5::Kind::SET_INSERT},
-    {SET_CARD, cvc5::Kind::SET_CARD},
-    {SET_COMPLEMENT, cvc5::Kind::SET_COMPLEMENT},
-    {SET_UNIVERSE, cvc5::Kind::SET_UNIVERSE},
-    {SET_COMPREHENSION, cvc5::Kind::SET_COMPREHENSION},
-    {SET_CHOOSE, cvc5::Kind::SET_CHOOSE},
-    {SET_IS_SINGLETON, cvc5::Kind::SET_IS_SINGLETON},
-    {SET_MAP, cvc5::Kind::SET_MAP},
-    /* Relations ----------------------------------------------------------- */
-    {RELATION_JOIN, cvc5::Kind::RELATION_JOIN},
-    {RELATION_PRODUCT, cvc5::Kind::RELATION_PRODUCT},
-    {RELATION_TRANSPOSE, cvc5::Kind::RELATION_TRANSPOSE},
-    {RELATION_TCLOSURE, cvc5::Kind::RELATION_TCLOSURE},
-    {RELATION_JOIN_IMAGE, cvc5::Kind::RELATION_JOIN_IMAGE},
-    {RELATION_IDEN, cvc5::Kind::RELATION_IDEN},
-    /* Bags ---------------------------------------------------------------- */
-    {BAG_UNION_MAX, cvc5::Kind::BAG_UNION_MAX},
-    {BAG_UNION_DISJOINT, cvc5::Kind::BAG_UNION_DISJOINT},
-    {BAG_INTER_MIN, cvc5::Kind::BAG_INTER_MIN},
-    {BAG_DIFFERENCE_SUBTRACT, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT},
-    {BAG_DIFFERENCE_REMOVE, cvc5::Kind::BAG_DIFFERENCE_REMOVE},
-    {BAG_SUBBAG, cvc5::Kind::BAG_SUBBAG},
-    {BAG_COUNT, cvc5::Kind::BAG_COUNT},
-    {BAG_MEMBER, cvc5::Kind::BAG_MEMBER},
-    {BAG_DUPLICATE_REMOVAL, cvc5::Kind::BAG_DUPLICATE_REMOVAL},
-    {BAG_MAKE, cvc5::Kind::BAG_MAKE},
-    {BAG_EMPTY, cvc5::Kind::BAG_EMPTY},
-    {BAG_CARD, cvc5::Kind::BAG_CARD},
-    {BAG_CHOOSE, cvc5::Kind::BAG_CHOOSE},
-    {BAG_IS_SINGLETON, cvc5::Kind::BAG_IS_SINGLETON},
-    {BAG_FROM_SET, cvc5::Kind::BAG_FROM_SET},
-    {BAG_TO_SET, cvc5::Kind::BAG_TO_SET},
-    {BAG_MAP, cvc5::Kind::BAG_MAP},
-    {BAG_FILTER, cvc5::Kind::BAG_FILTER},
-    {BAG_FOLD, cvc5::Kind::BAG_FOLD},
-    {TABLE_PRODUCT, cvc5::Kind::TABLE_PRODUCT},
-    /* Strings ------------------------------------------------------------- */
-    {STRING_CONCAT, cvc5::Kind::STRING_CONCAT},
-    {STRING_IN_REGEXP, cvc5::Kind::STRING_IN_REGEXP},
-    {STRING_LENGTH, cvc5::Kind::STRING_LENGTH},
-    {STRING_SUBSTR, cvc5::Kind::STRING_SUBSTR},
-    {STRING_UPDATE, cvc5::Kind::STRING_UPDATE},
-    {STRING_CHARAT, cvc5::Kind::STRING_CHARAT},
-    {STRING_CONTAINS, cvc5::Kind::STRING_CONTAINS},
-    {STRING_INDEXOF, cvc5::Kind::STRING_INDEXOF},
-    {STRING_INDEXOF_RE, cvc5::Kind::STRING_INDEXOF_RE},
-    {STRING_REPLACE, cvc5::Kind::STRING_REPLACE},
-    {STRING_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL},
-    {STRING_REPLACE_RE, cvc5::Kind::STRING_REPLACE_RE},
-    {STRING_REPLACE_RE_ALL, cvc5::Kind::STRING_REPLACE_RE_ALL},
-    {STRING_TOLOWER, cvc5::Kind::STRING_TOLOWER},
-    {STRING_TOUPPER, cvc5::Kind::STRING_TOUPPER},
-    {STRING_REV, cvc5::Kind::STRING_REV},
-    {STRING_FROM_CODE, cvc5::Kind::STRING_FROM_CODE},
-    {STRING_TO_CODE, cvc5::Kind::STRING_TO_CODE},
-    {STRING_LT, cvc5::Kind::STRING_LT},
-    {STRING_LEQ, cvc5::Kind::STRING_LEQ},
-    {STRING_PREFIX, cvc5::Kind::STRING_PREFIX},
-    {STRING_SUFFIX, cvc5::Kind::STRING_SUFFIX},
-    {STRING_IS_DIGIT, cvc5::Kind::STRING_IS_DIGIT},
-    {STRING_FROM_INT, cvc5::Kind::STRING_ITOS},
-    {STRING_TO_INT, cvc5::Kind::STRING_STOI},
-    {CONST_STRING, cvc5::Kind::CONST_STRING},
-    {STRING_TO_REGEXP, cvc5::Kind::STRING_TO_REGEXP},
-    {REGEXP_CONCAT, cvc5::Kind::REGEXP_CONCAT},
-    {REGEXP_UNION, cvc5::Kind::REGEXP_UNION},
-    {REGEXP_INTER, cvc5::Kind::REGEXP_INTER},
-    {REGEXP_DIFF, cvc5::Kind::REGEXP_DIFF},
-    {REGEXP_STAR, cvc5::Kind::REGEXP_STAR},
-    {REGEXP_PLUS, cvc5::Kind::REGEXP_PLUS},
-    {REGEXP_OPT, cvc5::Kind::REGEXP_OPT},
-    {REGEXP_RANGE, cvc5::Kind::REGEXP_RANGE},
-    {REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT},
-    {REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP},
-    {REGEXP_NONE, cvc5::Kind::REGEXP_NONE},
-    {REGEXP_ALL, cvc5::Kind::REGEXP_ALL},
-    {REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR},
-    {REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT},
-    // maps to the same kind as the string versions
-    {SEQ_CONCAT, cvc5::Kind::STRING_CONCAT},
-    {SEQ_LENGTH, cvc5::Kind::STRING_LENGTH},
-    {SEQ_EXTRACT, cvc5::Kind::STRING_SUBSTR},
-    {SEQ_UPDATE, cvc5::Kind::STRING_UPDATE},
-    {SEQ_AT, cvc5::Kind::STRING_CHARAT},
-    {SEQ_CONTAINS, cvc5::Kind::STRING_CONTAINS},
-    {SEQ_INDEXOF, cvc5::Kind::STRING_INDEXOF},
-    {SEQ_REPLACE, cvc5::Kind::STRING_REPLACE},
-    {SEQ_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL},
-    {SEQ_REV, cvc5::Kind::STRING_REV},
-    {SEQ_PREFIX, cvc5::Kind::STRING_PREFIX},
-    {SEQ_SUFFIX, cvc5::Kind::STRING_SUFFIX},
-    {CONST_SEQUENCE, cvc5::Kind::CONST_SEQUENCE},
-    {SEQ_UNIT, cvc5::Kind::SEQ_UNIT},
-    {SEQ_NTH, cvc5::Kind::SEQ_NTH},
-    /* Quantifiers --------------------------------------------------------- */
-    {FORALL, cvc5::Kind::FORALL},
-    {EXISTS, cvc5::Kind::EXISTS},
-    {VARIABLE_LIST, cvc5::Kind::BOUND_VAR_LIST},
-    {INST_PATTERN, cvc5::Kind::INST_PATTERN},
-    {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN},
-    {INST_POOL, cvc5::Kind::INST_POOL},
-    {INST_ADD_TO_POOL, cvc5::Kind::INST_ADD_TO_POOL},
-    {SKOLEM_ADD_TO_POOL, cvc5::Kind::SKOLEM_ADD_TO_POOL},
-    {INST_ATTRIBUTE, cvc5::Kind::INST_ATTRIBUTE},
-    {INST_PATTERN_LIST, cvc5::Kind::INST_PATTERN_LIST},
-    {LAST_KIND, cvc5::Kind::LAST_KIND},
-};
+const static std::unordered_map<Kind, std::pair<cvc5::Kind, std::string>>
+    s_kinds{
+        KIND_ENUM(INTERNAL_KIND, cvc5::Kind::UNDEFINED_KIND),
+        KIND_ENUM(UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND),
+        KIND_ENUM(NULL_EXPR, cvc5::Kind::NULL_EXPR),
+        /* Builtin ---------------------------------------------------------- */
+        KIND_ENUM(UNINTERPRETED_SORT_VALUE,
+                  cvc5::Kind::UNINTERPRETED_SORT_VALUE),
+        KIND_ENUM(EQUAL, cvc5::Kind::EQUAL),
+        KIND_ENUM(DISTINCT, cvc5::Kind::DISTINCT),
+        KIND_ENUM(CONSTANT, cvc5::Kind::VARIABLE),
+        KIND_ENUM(VARIABLE, cvc5::Kind::BOUND_VARIABLE),
+        KIND_ENUM(SEXPR, cvc5::Kind::SEXPR),
+        KIND_ENUM(LAMBDA, cvc5::Kind::LAMBDA),
+        KIND_ENUM(WITNESS, cvc5::Kind::WITNESS),
+        /* Boolean ---------------------------------------------------------- */
+        KIND_ENUM(CONST_BOOLEAN, cvc5::Kind::CONST_BOOLEAN),
+        KIND_ENUM(NOT, cvc5::Kind::NOT),
+        KIND_ENUM(AND, cvc5::Kind::AND),
+        KIND_ENUM(IMPLIES, cvc5::Kind::IMPLIES),
+        KIND_ENUM(OR, cvc5::Kind::OR),
+        KIND_ENUM(XOR, cvc5::Kind::XOR),
+        KIND_ENUM(ITE, cvc5::Kind::ITE),
+        /* UF --------------------------------------------------------------- */
+        KIND_ENUM(APPLY_UF, cvc5::Kind::APPLY_UF),
+        KIND_ENUM(CARDINALITY_CONSTRAINT, cvc5::Kind::CARDINALITY_CONSTRAINT),
+        KIND_ENUM(HO_APPLY, cvc5::Kind::HO_APPLY),
+        /* Arithmetic ------------------------------------------------------- */
+        KIND_ENUM(ADD, cvc5::Kind::ADD),
+        KIND_ENUM(MULT, cvc5::Kind::MULT),
+        KIND_ENUM(IAND, cvc5::Kind::IAND),
+        KIND_ENUM(POW2, cvc5::Kind::POW2),
+        KIND_ENUM(SUB, cvc5::Kind::SUB),
+        KIND_ENUM(NEG, cvc5::Kind::NEG),
+        KIND_ENUM(DIVISION, cvc5::Kind::DIVISION),
+        KIND_ENUM(INTS_DIVISION, cvc5::Kind::INTS_DIVISION),
+        KIND_ENUM(INTS_MODULUS, cvc5::Kind::INTS_MODULUS),
+        KIND_ENUM(ABS, cvc5::Kind::ABS),
+        KIND_ENUM(DIVISIBLE, cvc5::Kind::DIVISIBLE),
+        KIND_ENUM(POW, cvc5::Kind::POW),
+        KIND_ENUM(EXPONENTIAL, cvc5::Kind::EXPONENTIAL),
+        KIND_ENUM(SINE, cvc5::Kind::SINE),
+        KIND_ENUM(COSINE, cvc5::Kind::COSINE),
+        KIND_ENUM(TANGENT, cvc5::Kind::TANGENT),
+        KIND_ENUM(COSECANT, cvc5::Kind::COSECANT),
+        KIND_ENUM(SECANT, cvc5::Kind::SECANT),
+        KIND_ENUM(COTANGENT, cvc5::Kind::COTANGENT),
+        KIND_ENUM(ARCSINE, cvc5::Kind::ARCSINE),
+        KIND_ENUM(ARCCOSINE, cvc5::Kind::ARCCOSINE),
+        KIND_ENUM(ARCTANGENT, cvc5::Kind::ARCTANGENT),
+        KIND_ENUM(ARCCOSECANT, cvc5::Kind::ARCCOSECANT),
+        KIND_ENUM(ARCSECANT, cvc5::Kind::ARCSECANT),
+        KIND_ENUM(ARCCOTANGENT, cvc5::Kind::ARCCOTANGENT),
+        KIND_ENUM(SQRT, cvc5::Kind::SQRT),
+        KIND_ENUM(CONST_RATIONAL, cvc5::Kind::CONST_RATIONAL),
+        KIND_ENUM(LT, cvc5::Kind::LT),
+        KIND_ENUM(LEQ, cvc5::Kind::LEQ),
+        KIND_ENUM(GT, cvc5::Kind::GT),
+        KIND_ENUM(GEQ, cvc5::Kind::GEQ),
+        KIND_ENUM(IS_INTEGER, cvc5::Kind::IS_INTEGER),
+        KIND_ENUM(TO_INTEGER, cvc5::Kind::TO_INTEGER),
+        KIND_ENUM(TO_REAL, cvc5::Kind::TO_REAL),
+        KIND_ENUM(PI, cvc5::Kind::PI),
+        /* BV --------------------------------------------------------------- */
+        KIND_ENUM(CONST_BITVECTOR, cvc5::Kind::CONST_BITVECTOR),
+        KIND_ENUM(BITVECTOR_CONCAT, cvc5::Kind::BITVECTOR_CONCAT),
+        KIND_ENUM(BITVECTOR_AND, cvc5::Kind::BITVECTOR_AND),
+        KIND_ENUM(BITVECTOR_OR, cvc5::Kind::BITVECTOR_OR),
+        KIND_ENUM(BITVECTOR_XOR, cvc5::Kind::BITVECTOR_XOR),
+        KIND_ENUM(BITVECTOR_NOT, cvc5::Kind::BITVECTOR_NOT),
+        KIND_ENUM(BITVECTOR_NAND, cvc5::Kind::BITVECTOR_NAND),
+        KIND_ENUM(BITVECTOR_NOR, cvc5::Kind::BITVECTOR_NOR),
+        KIND_ENUM(BITVECTOR_XNOR, cvc5::Kind::BITVECTOR_XNOR),
+        KIND_ENUM(BITVECTOR_COMP, cvc5::Kind::BITVECTOR_COMP),
+        KIND_ENUM(BITVECTOR_MULT, cvc5::Kind::BITVECTOR_MULT),
+        KIND_ENUM(BITVECTOR_ADD, cvc5::Kind::BITVECTOR_ADD),
+        KIND_ENUM(BITVECTOR_SUB, cvc5::Kind::BITVECTOR_SUB),
+        KIND_ENUM(BITVECTOR_NEG, cvc5::Kind::BITVECTOR_NEG),
+        KIND_ENUM(BITVECTOR_UDIV, cvc5::Kind::BITVECTOR_UDIV),
+        KIND_ENUM(BITVECTOR_UREM, cvc5::Kind::BITVECTOR_UREM),
+        KIND_ENUM(BITVECTOR_SDIV, cvc5::Kind::BITVECTOR_SDIV),
+        KIND_ENUM(BITVECTOR_SREM, cvc5::Kind::BITVECTOR_SREM),
+        KIND_ENUM(BITVECTOR_SMOD, cvc5::Kind::BITVECTOR_SMOD),
+        KIND_ENUM(BITVECTOR_SHL, cvc5::Kind::BITVECTOR_SHL),
+        KIND_ENUM(BITVECTOR_LSHR, cvc5::Kind::BITVECTOR_LSHR),
+        KIND_ENUM(BITVECTOR_ASHR, cvc5::Kind::BITVECTOR_ASHR),
+        KIND_ENUM(BITVECTOR_ULT, cvc5::Kind::BITVECTOR_ULT),
+        KIND_ENUM(BITVECTOR_ULE, cvc5::Kind::BITVECTOR_ULE),
+        KIND_ENUM(BITVECTOR_UGT, cvc5::Kind::BITVECTOR_UGT),
+        KIND_ENUM(BITVECTOR_UGE, cvc5::Kind::BITVECTOR_UGE),
+        KIND_ENUM(BITVECTOR_SLT, cvc5::Kind::BITVECTOR_SLT),
+        KIND_ENUM(BITVECTOR_SLE, cvc5::Kind::BITVECTOR_SLE),
+        KIND_ENUM(BITVECTOR_SGT, cvc5::Kind::BITVECTOR_SGT),
+        KIND_ENUM(BITVECTOR_SGE, cvc5::Kind::BITVECTOR_SGE),
+        KIND_ENUM(BITVECTOR_ULTBV, cvc5::Kind::BITVECTOR_ULTBV),
+        KIND_ENUM(BITVECTOR_SLTBV, cvc5::Kind::BITVECTOR_SLTBV),
+        KIND_ENUM(BITVECTOR_ITE, cvc5::Kind::BITVECTOR_ITE),
+        KIND_ENUM(BITVECTOR_REDOR, cvc5::Kind::BITVECTOR_REDOR),
+        KIND_ENUM(BITVECTOR_REDAND, cvc5::Kind::BITVECTOR_REDAND),
+        KIND_ENUM(BITVECTOR_EXTRACT, cvc5::Kind::BITVECTOR_EXTRACT),
+        KIND_ENUM(BITVECTOR_REPEAT, cvc5::Kind::BITVECTOR_REPEAT),
+        KIND_ENUM(BITVECTOR_ZERO_EXTEND, cvc5::Kind::BITVECTOR_ZERO_EXTEND),
+        KIND_ENUM(BITVECTOR_SIGN_EXTEND, cvc5::Kind::BITVECTOR_SIGN_EXTEND),
+        KIND_ENUM(BITVECTOR_ROTATE_LEFT, cvc5::Kind::BITVECTOR_ROTATE_LEFT),
+        KIND_ENUM(BITVECTOR_ROTATE_RIGHT, cvc5::Kind::BITVECTOR_ROTATE_RIGHT),
+        KIND_ENUM(INT_TO_BITVECTOR, cvc5::Kind::INT_TO_BITVECTOR),
+        KIND_ENUM(BITVECTOR_TO_NAT, cvc5::Kind::BITVECTOR_TO_NAT),
+        /* FP --------------------------------------------------------------- */
+        KIND_ENUM(CONST_FLOATINGPOINT, cvc5::Kind::CONST_FLOATINGPOINT),
+        KIND_ENUM(CONST_ROUNDINGMODE, cvc5::Kind::CONST_ROUNDINGMODE),
+        KIND_ENUM(FLOATINGPOINT_FP, cvc5::Kind::FLOATINGPOINT_FP),
+        KIND_ENUM(FLOATINGPOINT_EQ, cvc5::Kind::FLOATINGPOINT_EQ),
+        KIND_ENUM(FLOATINGPOINT_ABS, cvc5::Kind::FLOATINGPOINT_ABS),
+        KIND_ENUM(FLOATINGPOINT_NEG, cvc5::Kind::FLOATINGPOINT_NEG),
+        KIND_ENUM(FLOATINGPOINT_ADD, cvc5::Kind::FLOATINGPOINT_ADD),
+        KIND_ENUM(FLOATINGPOINT_SUB, cvc5::Kind::FLOATINGPOINT_SUB),
+        KIND_ENUM(FLOATINGPOINT_MULT, cvc5::Kind::FLOATINGPOINT_MULT),
+        KIND_ENUM(FLOATINGPOINT_DIV, cvc5::Kind::FLOATINGPOINT_DIV),
+        KIND_ENUM(FLOATINGPOINT_FMA, cvc5::Kind::FLOATINGPOINT_FMA),
+        KIND_ENUM(FLOATINGPOINT_SQRT, cvc5::Kind::FLOATINGPOINT_SQRT),
+        KIND_ENUM(FLOATINGPOINT_REM, cvc5::Kind::FLOATINGPOINT_REM),
+        KIND_ENUM(FLOATINGPOINT_RTI, cvc5::Kind::FLOATINGPOINT_RTI),
+        KIND_ENUM(FLOATINGPOINT_MIN, cvc5::Kind::FLOATINGPOINT_MIN),
+        KIND_ENUM(FLOATINGPOINT_MAX, cvc5::Kind::FLOATINGPOINT_MAX),
+        KIND_ENUM(FLOATINGPOINT_LEQ, cvc5::Kind::FLOATINGPOINT_LEQ),
+        KIND_ENUM(FLOATINGPOINT_LT, cvc5::Kind::FLOATINGPOINT_LT),
+        KIND_ENUM(FLOATINGPOINT_GEQ, cvc5::Kind::FLOATINGPOINT_GEQ),
+        KIND_ENUM(FLOATINGPOINT_GT, cvc5::Kind::FLOATINGPOINT_GT),
+        KIND_ENUM(FLOATINGPOINT_IS_NORMAL, cvc5::Kind::FLOATINGPOINT_IS_NORMAL),
+        KIND_ENUM(FLOATINGPOINT_IS_SUBNORMAL,
+                  cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL),
+        KIND_ENUM(FLOATINGPOINT_IS_ZERO, cvc5::Kind::FLOATINGPOINT_IS_ZERO),
+        KIND_ENUM(FLOATINGPOINT_IS_INF, cvc5::Kind::FLOATINGPOINT_IS_INF),
+        KIND_ENUM(FLOATINGPOINT_IS_NAN, cvc5::Kind::FLOATINGPOINT_IS_NAN),
+        KIND_ENUM(FLOATINGPOINT_IS_NEG, cvc5::Kind::FLOATINGPOINT_IS_NEG),
+        KIND_ENUM(FLOATINGPOINT_IS_POS, cvc5::Kind::FLOATINGPOINT_IS_POS),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_FP,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_REAL,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_SBV,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_UBV,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV),
+        KIND_ENUM(FLOATINGPOINT_TO_FP_GENERIC,
+                  cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC),
+        KIND_ENUM(FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV),
+        KIND_ENUM(FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV),
+        KIND_ENUM(FLOATINGPOINT_TO_REAL, cvc5::Kind::FLOATINGPOINT_TO_REAL),
+        /* Arrays ----------------------------------------------------------- */
+        KIND_ENUM(SELECT, cvc5::Kind::SELECT),
+        KIND_ENUM(STORE, cvc5::Kind::STORE),
+        KIND_ENUM(CONST_ARRAY, cvc5::Kind::STORE_ALL),
+        KIND_ENUM(EQ_RANGE, cvc5::Kind::EQ_RANGE),
+        /* Datatypes -------------------------------------------------------- */
+        KIND_ENUM(APPLY_SELECTOR, cvc5::Kind::APPLY_SELECTOR),
+        KIND_ENUM(APPLY_CONSTRUCTOR, cvc5::Kind::APPLY_CONSTRUCTOR),
+        KIND_ENUM(APPLY_TESTER, cvc5::Kind::APPLY_TESTER),
+        KIND_ENUM(APPLY_UPDATER, cvc5::Kind::APPLY_UPDATER),
+        KIND_ENUM(DT_SIZE, cvc5::Kind::DT_SIZE),
+        KIND_ENUM(MATCH, cvc5::Kind::MATCH),
+        KIND_ENUM(MATCH_CASE, cvc5::Kind::MATCH_CASE),
+        KIND_ENUM(MATCH_BIND_CASE, cvc5::Kind::MATCH_BIND_CASE),
+        KIND_ENUM(TUPLE_PROJECT, cvc5::Kind::TUPLE_PROJECT),
+        /* Separation Logic ------------------------------------------------- */
+        KIND_ENUM(SEP_NIL, cvc5::Kind::SEP_NIL),
+        KIND_ENUM(SEP_EMP, cvc5::Kind::SEP_EMP),
+        KIND_ENUM(SEP_PTO, cvc5::Kind::SEP_PTO),
+        KIND_ENUM(SEP_STAR, cvc5::Kind::SEP_STAR),
+        KIND_ENUM(SEP_WAND, cvc5::Kind::SEP_WAND),
+        /* Sets ------------------------------------------------------------- */
+        KIND_ENUM(SET_EMPTY, cvc5::Kind::SET_EMPTY),
+        KIND_ENUM(SET_UNION, cvc5::Kind::SET_UNION),
+        KIND_ENUM(SET_INTER, cvc5::Kind::SET_INTER),
+        KIND_ENUM(SET_MINUS, cvc5::Kind::SET_MINUS),
+        KIND_ENUM(SET_SUBSET, cvc5::Kind::SET_SUBSET),
+        KIND_ENUM(SET_MEMBER, cvc5::Kind::SET_MEMBER),
+        KIND_ENUM(SET_SINGLETON, cvc5::Kind::SET_SINGLETON),
+        KIND_ENUM(SET_INSERT, cvc5::Kind::SET_INSERT),
+        KIND_ENUM(SET_CARD, cvc5::Kind::SET_CARD),
+        KIND_ENUM(SET_COMPLEMENT, cvc5::Kind::SET_COMPLEMENT),
+        KIND_ENUM(SET_UNIVERSE, cvc5::Kind::SET_UNIVERSE),
+        KIND_ENUM(SET_COMPREHENSION, cvc5::Kind::SET_COMPREHENSION),
+        KIND_ENUM(SET_CHOOSE, cvc5::Kind::SET_CHOOSE),
+        KIND_ENUM(SET_IS_SINGLETON, cvc5::Kind::SET_IS_SINGLETON),
+        KIND_ENUM(SET_MAP, cvc5::Kind::SET_MAP),
+        /* Relations -------------------------------------------------------- */
+        KIND_ENUM(RELATION_JOIN, cvc5::Kind::RELATION_JOIN),
+        KIND_ENUM(RELATION_PRODUCT, cvc5::Kind::RELATION_PRODUCT),
+        KIND_ENUM(RELATION_TRANSPOSE, cvc5::Kind::RELATION_TRANSPOSE),
+        KIND_ENUM(RELATION_TCLOSURE, cvc5::Kind::RELATION_TCLOSURE),
+        KIND_ENUM(RELATION_JOIN_IMAGE, cvc5::Kind::RELATION_JOIN_IMAGE),
+        KIND_ENUM(RELATION_IDEN, cvc5::Kind::RELATION_IDEN),
+        /* Bags ------------------------------------------------------------- */
+        KIND_ENUM(BAG_UNION_MAX, cvc5::Kind::BAG_UNION_MAX),
+        KIND_ENUM(BAG_UNION_DISJOINT, cvc5::Kind::BAG_UNION_DISJOINT),
+        KIND_ENUM(BAG_INTER_MIN, cvc5::Kind::BAG_INTER_MIN),
+        KIND_ENUM(BAG_DIFFERENCE_SUBTRACT, cvc5::Kind::BAG_DIFFERENCE_SUBTRACT),
+        KIND_ENUM(BAG_DIFFERENCE_REMOVE, cvc5::Kind::BAG_DIFFERENCE_REMOVE),
+        KIND_ENUM(BAG_SUBBAG, cvc5::Kind::BAG_SUBBAG),
+        KIND_ENUM(BAG_COUNT, cvc5::Kind::BAG_COUNT),
+        KIND_ENUM(BAG_MEMBER, cvc5::Kind::BAG_MEMBER),
+        KIND_ENUM(BAG_DUPLICATE_REMOVAL, cvc5::Kind::BAG_DUPLICATE_REMOVAL),
+        KIND_ENUM(BAG_MAKE, cvc5::Kind::BAG_MAKE),
+        KIND_ENUM(BAG_EMPTY, cvc5::Kind::BAG_EMPTY),
+        KIND_ENUM(BAG_CARD, cvc5::Kind::BAG_CARD),
+        KIND_ENUM(BAG_CHOOSE, cvc5::Kind::BAG_CHOOSE),
+        KIND_ENUM(BAG_IS_SINGLETON, cvc5::Kind::BAG_IS_SINGLETON),
+        KIND_ENUM(BAG_FROM_SET, cvc5::Kind::BAG_FROM_SET),
+        KIND_ENUM(BAG_TO_SET, cvc5::Kind::BAG_TO_SET),
+        KIND_ENUM(BAG_MAP, cvc5::Kind::BAG_MAP),
+        KIND_ENUM(BAG_FILTER, cvc5::Kind::BAG_FILTER),
+        KIND_ENUM(BAG_FOLD, cvc5::Kind::BAG_FOLD),
+        KIND_ENUM(TABLE_PRODUCT, cvc5::Kind::TABLE_PRODUCT),
+        /* Strings ---------------------------------------------------------- */
+        KIND_ENUM(STRING_CONCAT, cvc5::Kind::STRING_CONCAT),
+        KIND_ENUM(STRING_IN_REGEXP, cvc5::Kind::STRING_IN_REGEXP),
+        KIND_ENUM(STRING_LENGTH, cvc5::Kind::STRING_LENGTH),
+        KIND_ENUM(STRING_SUBSTR, cvc5::Kind::STRING_SUBSTR),
+        KIND_ENUM(STRING_UPDATE, cvc5::Kind::STRING_UPDATE),
+        KIND_ENUM(STRING_CHARAT, cvc5::Kind::STRING_CHARAT),
+        KIND_ENUM(STRING_CONTAINS, cvc5::Kind::STRING_CONTAINS),
+        KIND_ENUM(STRING_INDEXOF, cvc5::Kind::STRING_INDEXOF),
+        KIND_ENUM(STRING_INDEXOF_RE, cvc5::Kind::STRING_INDEXOF_RE),
+        KIND_ENUM(STRING_REPLACE, cvc5::Kind::STRING_REPLACE),
+        KIND_ENUM(STRING_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL),
+        KIND_ENUM(STRING_REPLACE_RE, cvc5::Kind::STRING_REPLACE_RE),
+        KIND_ENUM(STRING_REPLACE_RE_ALL, cvc5::Kind::STRING_REPLACE_RE_ALL),
+        KIND_ENUM(STRING_TOLOWER, cvc5::Kind::STRING_TOLOWER),
+        KIND_ENUM(STRING_TOUPPER, cvc5::Kind::STRING_TOUPPER),
+        KIND_ENUM(STRING_REV, cvc5::Kind::STRING_REV),
+        KIND_ENUM(STRING_FROM_CODE, cvc5::Kind::STRING_FROM_CODE),
+        KIND_ENUM(STRING_TO_CODE, cvc5::Kind::STRING_TO_CODE),
+        KIND_ENUM(STRING_LT, cvc5::Kind::STRING_LT),
+        KIND_ENUM(STRING_LEQ, cvc5::Kind::STRING_LEQ),
+        KIND_ENUM(STRING_PREFIX, cvc5::Kind::STRING_PREFIX),
+        KIND_ENUM(STRING_SUFFIX, cvc5::Kind::STRING_SUFFIX),
+        KIND_ENUM(STRING_IS_DIGIT, cvc5::Kind::STRING_IS_DIGIT),
+        KIND_ENUM(STRING_FROM_INT, cvc5::Kind::STRING_ITOS),
+        KIND_ENUM(STRING_TO_INT, cvc5::Kind::STRING_STOI),
+        KIND_ENUM(CONST_STRING, cvc5::Kind::CONST_STRING),
+        KIND_ENUM(STRING_TO_REGEXP, cvc5::Kind::STRING_TO_REGEXP),
+        KIND_ENUM(REGEXP_CONCAT, cvc5::Kind::REGEXP_CONCAT),
+        KIND_ENUM(REGEXP_UNION, cvc5::Kind::REGEXP_UNION),
+        KIND_ENUM(REGEXP_INTER, cvc5::Kind::REGEXP_INTER),
+        KIND_ENUM(REGEXP_DIFF, cvc5::Kind::REGEXP_DIFF),
+        KIND_ENUM(REGEXP_STAR, cvc5::Kind::REGEXP_STAR),
+        KIND_ENUM(REGEXP_PLUS, cvc5::Kind::REGEXP_PLUS),
+        KIND_ENUM(REGEXP_OPT, cvc5::Kind::REGEXP_OPT),
+        KIND_ENUM(REGEXP_RANGE, cvc5::Kind::REGEXP_RANGE),
+        KIND_ENUM(REGEXP_REPEAT, cvc5::Kind::REGEXP_REPEAT),
+        KIND_ENUM(REGEXP_LOOP, cvc5::Kind::REGEXP_LOOP),
+        KIND_ENUM(REGEXP_NONE, cvc5::Kind::REGEXP_NONE),
+        KIND_ENUM(REGEXP_ALL, cvc5::Kind::REGEXP_ALL),
+        KIND_ENUM(REGEXP_ALLCHAR, cvc5::Kind::REGEXP_ALLCHAR),
+        KIND_ENUM(REGEXP_COMPLEMENT, cvc5::Kind::REGEXP_COMPLEMENT),
+        // maps to the same kind as the string versions
+        KIND_ENUM(SEQ_CONCAT, cvc5::Kind::STRING_CONCAT),
+        KIND_ENUM(SEQ_LENGTH, cvc5::Kind::STRING_LENGTH),
+        KIND_ENUM(SEQ_EXTRACT, cvc5::Kind::STRING_SUBSTR),
+        KIND_ENUM(SEQ_UPDATE, cvc5::Kind::STRING_UPDATE),
+        KIND_ENUM(SEQ_AT, cvc5::Kind::STRING_CHARAT),
+        KIND_ENUM(SEQ_CONTAINS, cvc5::Kind::STRING_CONTAINS),
+        KIND_ENUM(SEQ_INDEXOF, cvc5::Kind::STRING_INDEXOF),
+        KIND_ENUM(SEQ_REPLACE, cvc5::Kind::STRING_REPLACE),
+        KIND_ENUM(SEQ_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL),
+        KIND_ENUM(SEQ_REV, cvc5::Kind::STRING_REV),
+        KIND_ENUM(SEQ_PREFIX, cvc5::Kind::STRING_PREFIX),
+        KIND_ENUM(SEQ_SUFFIX, cvc5::Kind::STRING_SUFFIX),
+        KIND_ENUM(CONST_SEQUENCE, cvc5::Kind::CONST_SEQUENCE),
+        KIND_ENUM(SEQ_UNIT, cvc5::Kind::SEQ_UNIT),
+        KIND_ENUM(SEQ_NTH, cvc5::Kind::SEQ_NTH),
+        /* Quantifiers ------------------------------------------------------ */
+        KIND_ENUM(FORALL, cvc5::Kind::FORALL),
+        KIND_ENUM(EXISTS, cvc5::Kind::EXISTS),
+        KIND_ENUM(VARIABLE_LIST, cvc5::Kind::BOUND_VAR_LIST),
+        KIND_ENUM(INST_PATTERN, cvc5::Kind::INST_PATTERN),
+        KIND_ENUM(INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN),
+        KIND_ENUM(INST_POOL, cvc5::Kind::INST_POOL),
+        KIND_ENUM(INST_ADD_TO_POOL, cvc5::Kind::INST_ADD_TO_POOL),
+        KIND_ENUM(SKOLEM_ADD_TO_POOL, cvc5::Kind::SKOLEM_ADD_TO_POOL),
+        KIND_ENUM(INST_ATTRIBUTE, cvc5::Kind::INST_ATTRIBUTE),
+        KIND_ENUM(INST_PATTERN_LIST, cvc5::Kind::INST_PATTERN_LIST),
+        KIND_ENUM(LAST_KIND, cvc5::Kind::LAST_KIND),
+    };
 
 /* Mapping from internal kind to external (API) kind. */
 const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
@@ -731,7 +744,7 @@ cvc5::Kind extToIntKind(cvc5::api::Kind k)
   {
     return cvc5::Kind::UNDEFINED_KIND;
   }
-  return it->second;
+  return it->second.first;
 }
 
 /** Return true if given kind is a defined external kind. */
@@ -797,24 +810,17 @@ uint32_t maxArity(Kind k)
 
 std::string kindToString(Kind k)
 {
-  return k == INTERNAL_KIND ? "INTERNAL_KIND"
-                            : cvc5::kind::kindToString(extToIntKind(k));
-}
-
-const char* toString(Kind k)
-{
-  return k == INTERNAL_KIND ? "INTERNAL_KIND"
-                            : cvc5::kind::toString(extToIntKind(k));
+  auto it = s_kinds.find(k);
+  if (it == s_kinds.end())
+  {
+    return "UNDEFINED_KIND";
+  }
+  return it->second.second;
 }
 
 std::ostream& operator<<(std::ostream& out, Kind k)
 {
-  switch (k)
-  {
-    case INTERNAL_KIND: out << "INTERNAL_KIND"; break;
-    default: out << extToIntKind(k);
-  }
-  return out;
+  return out << kindToString(k);
 }
 
 /* -------------------------------------------------------------------------- */