New C++ API: Implementation of Kind maps. (#2130)

1 files changed, 532 insertions, 1 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index bc6201597..968102f5d 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -16,6 +16,7 @@
 
 #include "api/cvc4cpp.h"
 
+#include "expr/kind.h"
 #include "expr/type.h"
 #include "util/result.h"
 
@@ -92,6 +93,537 @@ std::ostream& operator<<(std::ostream& out, const Result& r)
 }
 
 /* -------------------------------------------------------------------------- */
+/* Kind                                                                       */
+/* -------------------------------------------------------------------------- */
+
+/* Mapping from external (API) kind to internal kind. */
+const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
+    {INTERNAL_KIND, CVC4::Kind::UNDEFINED_KIND},
+    {UNDEFINED_KIND, CVC4::Kind::UNDEFINED_KIND},
+    {NULL_EXPR, CVC4::Kind::NULL_EXPR},
+    /* Builtin ------------------------------------------------------------- */
+    {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT},
+    {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE},
+    {FUNCTION, CVC4::Kind::FUNCTION},
+    {APPLY, CVC4::Kind::APPLY},
+    {EQUAL, CVC4::Kind::EQUAL},
+    {DISTINCT, CVC4::Kind::DISTINCT},
+    {VARIABLE, CVC4::Kind::VARIABLE},
+    {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+    {LAMBDA, CVC4::Kind::LAMBDA},
+    {CHOICE, CVC4::Kind::CHOICE},
+    {CHAIN, CVC4::Kind::CHAIN},
+    {CHAIN_OP, CVC4::Kind::CHAIN_OP},
+    /* Boolean ------------------------------------------------------------- */
+    {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
+    {NOT, CVC4::Kind::NOT},
+    {AND, CVC4::Kind::AND},
+    {IMPLIES, CVC4::Kind::IMPLIES},
+    {OR, CVC4::Kind::OR},
+    {XOR, CVC4::Kind::XOR},
+    {ITE, CVC4::Kind::ITE},
+    /* UF ------------------------------------------------------------------ */
+    {APPLY_UF, CVC4::Kind::APPLY_UF},
+    {CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT},
+    {HO_APPLY, CVC4::Kind::HO_APPLY},
+    /* Arithmetic ---------------------------------------------------------- */
+    {PLUS, CVC4::Kind::PLUS},
+    {MULT, CVC4::Kind::MULT},
+    {MINUS, CVC4::Kind::MINUS},
+    {UMINUS, CVC4::Kind::UMINUS},
+    {DIVISION, CVC4::Kind::DIVISION},
+    {DIVISION_TOTAL, CVC4::Kind::DIVISION_TOTAL},
+    {INTS_DIVISION, CVC4::Kind::INTS_DIVISION},
+    {INTS_DIVISION_TOTAL, CVC4::Kind::INTS_DIVISION_TOTAL},
+    {INTS_MODULUS, CVC4::Kind::INTS_MODULUS},
+    {INTS_MODULUS_TOTAL, CVC4::Kind::INTS_MODULUS_TOTAL},
+    {ABS, CVC4::Kind::ABS},
+    {DIVISIBLE, CVC4::Kind::DIVISIBLE},
+    {POW, CVC4::Kind::POW},
+    {EXPONENTIAL, CVC4::Kind::EXPONENTIAL},
+    {SINE, CVC4::Kind::SINE},
+    {COSINE, CVC4::Kind::COSINE},
+    {TANGENT, CVC4::Kind::TANGENT},
+    {COSECANT, CVC4::Kind::COSECANT},
+    {SECANT, CVC4::Kind::SECANT},
+    {COTANGENT, CVC4::Kind::COTANGENT},
+    {ARCSINE, CVC4::Kind::ARCSINE},
+    {ARCCOSINE, CVC4::Kind::ARCCOSINE},
+    {ARCTANGENT, CVC4::Kind::ARCTANGENT},
+    {ARCCOSECANT, CVC4::Kind::ARCCOSECANT},
+    {ARCSECANT, CVC4::Kind::ARCSECANT},
+    {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
+    {SQRT, CVC4::Kind::SQRT},
+    {DIVISIBLE_OP, CVC4::Kind::DIVISIBLE_OP},
+    {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
+    {LT, CVC4::Kind::LT},
+    {LEQ, CVC4::Kind::LEQ},
+    {GT, CVC4::Kind::GT},
+    {GEQ, CVC4::Kind::GEQ},
+    {IS_INTEGER, CVC4::Kind::IS_INTEGER},
+    {TO_INTEGER, CVC4::Kind::TO_INTEGER},
+    {TO_REAL, CVC4::Kind::TO_REAL},
+    {PI, CVC4::Kind::PI},
+    /* BV ------------------------------------------------------------------ */
+    {CONST_BITVECTOR, CVC4::Kind::CONST_BITVECTOR},
+    {BITVECTOR_CONCAT, CVC4::Kind::BITVECTOR_CONCAT},
+    {BITVECTOR_AND, CVC4::Kind::BITVECTOR_AND},
+    {BITVECTOR_OR, CVC4::Kind::BITVECTOR_OR},
+    {BITVECTOR_XOR, CVC4::Kind::BITVECTOR_XOR},
+    {BITVECTOR_NOT, CVC4::Kind::BITVECTOR_NOT},
+    {BITVECTOR_NAND, CVC4::Kind::BITVECTOR_NAND},
+    {BITVECTOR_NOR, CVC4::Kind::BITVECTOR_NOR},
+    {BITVECTOR_XNOR, CVC4::Kind::BITVECTOR_XNOR},
+    {BITVECTOR_COMP, CVC4::Kind::BITVECTOR_COMP},
+    {BITVECTOR_MULT, CVC4::Kind::BITVECTOR_MULT},
+    {BITVECTOR_PLUS, CVC4::Kind::BITVECTOR_PLUS},
+    {BITVECTOR_SUB, CVC4::Kind::BITVECTOR_SUB},
+    {BITVECTOR_NEG, CVC4::Kind::BITVECTOR_NEG},
+    {BITVECTOR_UDIV, CVC4::Kind::BITVECTOR_UDIV},
+    {BITVECTOR_UREM, CVC4::Kind::BITVECTOR_UREM},
+    {BITVECTOR_SDIV, CVC4::Kind::BITVECTOR_SDIV},
+    {BITVECTOR_SREM, CVC4::Kind::BITVECTOR_SREM},
+    {BITVECTOR_SMOD, CVC4::Kind::BITVECTOR_SMOD},
+    {BITVECTOR_UDIV_TOTAL, CVC4::Kind::BITVECTOR_UDIV_TOTAL},
+    {BITVECTOR_UREM_TOTAL, CVC4::Kind::BITVECTOR_UREM_TOTAL},
+    {BITVECTOR_SHL, CVC4::Kind::BITVECTOR_SHL},
+    {BITVECTOR_LSHR, CVC4::Kind::BITVECTOR_LSHR},
+    {BITVECTOR_ASHR, CVC4::Kind::BITVECTOR_ASHR},
+    {BITVECTOR_ULT, CVC4::Kind::BITVECTOR_ULT},
+    {BITVECTOR_ULE, CVC4::Kind::BITVECTOR_ULE},
+    {BITVECTOR_UGT, CVC4::Kind::BITVECTOR_UGT},
+    {BITVECTOR_UGE, CVC4::Kind::BITVECTOR_UGE},
+    {BITVECTOR_SLT, CVC4::Kind::BITVECTOR_SLT},
+    {BITVECTOR_SLE, CVC4::Kind::BITVECTOR_SLE},
+    {BITVECTOR_SGT, CVC4::Kind::BITVECTOR_SGT},
+    {BITVECTOR_SGE, CVC4::Kind::BITVECTOR_SGE},
+    {BITVECTOR_ULTBV, CVC4::Kind::BITVECTOR_ULTBV},
+    {BITVECTOR_SLTBV, CVC4::Kind::BITVECTOR_SLTBV},
+    {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
+    {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
+    {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
+    {BITVECTOR_EXTRACT_OP, CVC4::Kind::BITVECTOR_EXTRACT_OP},
+    {BITVECTOR_REPEAT_OP, CVC4::Kind::BITVECTOR_REPEAT_OP},
+    {BITVECTOR_ZERO_EXTEND_OP, CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP},
+    {BITVECTOR_SIGN_EXTEND_OP, CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP},
+    {BITVECTOR_ROTATE_LEFT_OP, CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP},
+    {BITVECTOR_ROTATE_RIGHT_OP, CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP},
+    {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
+    {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
+    {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
+    {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
+    {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
+    {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
+    {INT_TO_BITVECTOR_OP, CVC4::Kind::INT_TO_BITVECTOR_OP},
+    {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
+    {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
+    /* FP ------------------------------------------------------------------ */
+    {CONST_FLOATINGPOINT, CVC4::Kind::CONST_FLOATINGPOINT},
+    {CONST_ROUNDINGMODE, CVC4::Kind::CONST_ROUNDINGMODE},
+    {FLOATINGPOINT_FP, CVC4::Kind::FLOATINGPOINT_FP},
+    {FLOATINGPOINT_EQ, CVC4::Kind::FLOATINGPOINT_EQ},
+    {FLOATINGPOINT_ABS, CVC4::Kind::FLOATINGPOINT_ABS},
+    {FLOATINGPOINT_NEG, CVC4::Kind::FLOATINGPOINT_NEG},
+    {FLOATINGPOINT_PLUS, CVC4::Kind::FLOATINGPOINT_PLUS},
+    {FLOATINGPOINT_SUB, CVC4::Kind::FLOATINGPOINT_SUB},
+    {FLOATINGPOINT_MULT, CVC4::Kind::FLOATINGPOINT_MULT},
+    {FLOATINGPOINT_DIV, CVC4::Kind::FLOATINGPOINT_DIV},
+    {FLOATINGPOINT_FMA, CVC4::Kind::FLOATINGPOINT_FMA},
+    {FLOATINGPOINT_SQRT, CVC4::Kind::FLOATINGPOINT_SQRT},
+    {FLOATINGPOINT_REM, CVC4::Kind::FLOATINGPOINT_REM},
+    {FLOATINGPOINT_RTI, CVC4::Kind::FLOATINGPOINT_RTI},
+    {FLOATINGPOINT_MIN, CVC4::Kind::FLOATINGPOINT_MIN},
+    {FLOATINGPOINT_MAX, CVC4::Kind::FLOATINGPOINT_MAX},
+    {FLOATINGPOINT_LEQ, CVC4::Kind::FLOATINGPOINT_LEQ},
+    {FLOATINGPOINT_LT, CVC4::Kind::FLOATINGPOINT_LT},
+    {FLOATINGPOINT_GEQ, CVC4::Kind::FLOATINGPOINT_GEQ},
+    {FLOATINGPOINT_GT, CVC4::Kind::FLOATINGPOINT_GT},
+    {FLOATINGPOINT_ISN, CVC4::Kind::FLOATINGPOINT_ISN},
+    {FLOATINGPOINT_ISSN, CVC4::Kind::FLOATINGPOINT_ISSN},
+    {FLOATINGPOINT_ISZ, CVC4::Kind::FLOATINGPOINT_ISZ},
+    {FLOATINGPOINT_ISINF, CVC4::Kind::FLOATINGPOINT_ISINF},
+    {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
+    {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
+    {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
+    {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
+    {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
+    {FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
+    {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
+    {FLOATINGPOINT_TO_FP_REAL_OP, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP},
+    {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
+    {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
+    {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
+    {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
+    {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
+    {FLOATINGPOINT_TO_FP_GENERIC_OP,
+     CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP},
+    {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
+    {FLOATINGPOINT_TO_UBV_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_OP},
+    {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
+    {FLOATINGPOINT_TO_UBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP},
+    {FLOATINGPOINT_TO_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL},
+    {FLOATINGPOINT_TO_SBV_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_OP},
+    {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
+    {FLOATINGPOINT_TO_SBV_TOTAL_OP, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP},
+    {FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL},
+    {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
+    {FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL},
+    /* Arrays -------------------------------------------------------------- */
+    {SELECT, CVC4::Kind::SELECT},
+    {STORE, CVC4::Kind::STORE},
+    {STORE_ALL, CVC4::Kind::STORE_ALL},
+    /* Datatypes ----------------------------------------------------------- */
+    {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
+    {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
+    {APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL},
+    {APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
+    {TUPLE_UPDATE_OP, CVC4::Kind::TUPLE_UPDATE_OP},
+    {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
+    {RECORD_UPDATE_OP, CVC4::Kind::RECORD_UPDATE_OP},
+    {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
+    /* Separation Logic ---------------------------------------------------- */
+    {SEP_NIL, CVC4::Kind::SEP_NIL},
+    {SEP_EMP, CVC4::Kind::SEP_EMP},
+    {SEP_PTO, CVC4::Kind::SEP_PTO},
+    {SEP_STAR, CVC4::Kind::SEP_STAR},
+    {SEP_WAND, CVC4::Kind::SEP_WAND},
+    /* Sets ---------------------------------------------------------------- */
+    {EMPTYSET, CVC4::Kind::EMPTYSET},
+    {UNION, CVC4::Kind::UNION},
+    {INTERSECTION, CVC4::Kind::INTERSECTION},
+    {SETMINUS, CVC4::Kind::SETMINUS},
+    {SUBSET, CVC4::Kind::SUBSET},
+    {MEMBER, CVC4::Kind::MEMBER},
+    {SINGLETON, CVC4::Kind::SINGLETON},
+    {INSERT, CVC4::Kind::INSERT},
+    {CARD, CVC4::Kind::CARD},
+    {COMPLEMENT, CVC4::Kind::COMPLEMENT},
+    {UNIVERSE_SET, CVC4::Kind::UNIVERSE_SET},
+    {JOIN, CVC4::Kind::JOIN},
+    {PRODUCT, CVC4::Kind::PRODUCT},
+    {TRANSPOSE, CVC4::Kind::TRANSPOSE},
+    {TCLOSURE, CVC4::Kind::TCLOSURE},
+    {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE},
+    {IDEN, CVC4::Kind::IDEN},
+    /* Strings ------------------------------------------------------------- */
+    {STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
+    {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
+    {STRING_LENGTH, CVC4::Kind::STRING_LENGTH},
+    {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR},
+    {STRING_CHARAT, CVC4::Kind::STRING_CHARAT},
+    {STRING_STRCTN, CVC4::Kind::STRING_STRCTN},
+    {STRING_STRIDOF, CVC4::Kind::STRING_STRIDOF},
+    {STRING_STRREPL, CVC4::Kind::STRING_STRREPL},
+    {STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
+    {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
+    {STRING_ITOS, CVC4::Kind::STRING_ITOS},
+    {STRING_STOI, CVC4::Kind::STRING_STOI},
+    {CONST_STRING, CVC4::Kind::CONST_STRING},
+    {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP},
+    {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT},
+    {REGEXP_UNION, CVC4::Kind::REGEXP_UNION},
+    {REGEXP_INTER, CVC4::Kind::REGEXP_INTER},
+    {REGEXP_STAR, CVC4::Kind::REGEXP_STAR},
+    {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
+    {REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
+    {REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
+    {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
+    {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
+    {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
+    /* Quantifiers --------------------------------------------------------- */
+    {FORALL, CVC4::Kind::FORALL},
+    {EXISTS, CVC4::Kind::EXISTS},
+    {LAST_KIND, CVC4::Kind::LAST_KIND},
+};
+
+/* Mapping from internal kind to external (API) kind. */
+const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
+    s_kinds_internal{
+        {CVC4::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
+        {CVC4::Kind::NULL_EXPR, NULL_EXPR},
+        /* Builtin --------------------------------------------------------- */
+        {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
+        {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
+        {CVC4::Kind::FUNCTION, FUNCTION},
+        {CVC4::Kind::APPLY, APPLY},
+        {CVC4::Kind::EQUAL, EQUAL},
+        {CVC4::Kind::DISTINCT, DISTINCT},
+        {CVC4::Kind::VARIABLE, VARIABLE},
+        {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+        {CVC4::Kind::LAMBDA, LAMBDA},
+        {CVC4::Kind::CHOICE, CHOICE},
+        {CVC4::Kind::CHAIN, CHAIN},
+        {CVC4::Kind::CHAIN_OP, CHAIN_OP},
+        /* Boolean --------------------------------------------------------- */
+        {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
+        {CVC4::Kind::NOT, NOT},
+        {CVC4::Kind::AND, AND},
+        {CVC4::Kind::IMPLIES, IMPLIES},
+        {CVC4::Kind::OR, OR},
+        {CVC4::Kind::XOR, XOR},
+        {CVC4::Kind::ITE, ITE},
+        /* UF -------------------------------------------------------------- */
+        {CVC4::Kind::APPLY_UF, APPLY_UF},
+        {CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
+        {CVC4::Kind::HO_APPLY, HO_APPLY},
+        /* Arithmetic ------------------------------------------------------ */
+        {CVC4::Kind::PLUS, PLUS},
+        {CVC4::Kind::MULT, MULT},
+        {CVC4::Kind::MINUS, MINUS},
+        {CVC4::Kind::UMINUS, UMINUS},
+        {CVC4::Kind::DIVISION, DIVISION},
+        {CVC4::Kind::DIVISION_TOTAL, DIVISION_TOTAL},
+        {CVC4::Kind::INTS_DIVISION, INTS_DIVISION},
+        {CVC4::Kind::INTS_DIVISION_TOTAL, INTS_DIVISION_TOTAL},
+        {CVC4::Kind::INTS_MODULUS, INTS_MODULUS},
+        {CVC4::Kind::INTS_MODULUS_TOTAL, INTS_MODULUS_TOTAL},
+        {CVC4::Kind::ABS, ABS},
+        {CVC4::Kind::DIVISIBLE, DIVISIBLE},
+        {CVC4::Kind::POW, POW},
+        {CVC4::Kind::EXPONENTIAL, EXPONENTIAL},
+        {CVC4::Kind::SINE, SINE},
+        {CVC4::Kind::COSINE, COSINE},
+        {CVC4::Kind::TANGENT, TANGENT},
+        {CVC4::Kind::COSECANT, COSECANT},
+        {CVC4::Kind::SECANT, SECANT},
+        {CVC4::Kind::COTANGENT, COTANGENT},
+        {CVC4::Kind::ARCSINE, ARCSINE},
+        {CVC4::Kind::ARCCOSINE, ARCCOSINE},
+        {CVC4::Kind::ARCTANGENT, ARCTANGENT},
+        {CVC4::Kind::ARCCOSECANT, ARCCOSECANT},
+        {CVC4::Kind::ARCSECANT, ARCSECANT},
+        {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
+        {CVC4::Kind::SQRT, SQRT},
+        {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE_OP},
+        {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
+        {CVC4::Kind::LT, LT},
+        {CVC4::Kind::LEQ, LEQ},
+        {CVC4::Kind::GT, GT},
+        {CVC4::Kind::GEQ, GEQ},
+        {CVC4::Kind::IS_INTEGER, IS_INTEGER},
+        {CVC4::Kind::TO_INTEGER, TO_INTEGER},
+        {CVC4::Kind::TO_REAL, TO_REAL},
+        {CVC4::Kind::PI, PI},
+        /* BV -------------------------------------------------------------- */
+        {CVC4::Kind::CONST_BITVECTOR, CONST_BITVECTOR},
+        {CVC4::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT},
+        {CVC4::Kind::BITVECTOR_AND, BITVECTOR_AND},
+        {CVC4::Kind::BITVECTOR_OR, BITVECTOR_OR},
+        {CVC4::Kind::BITVECTOR_XOR, BITVECTOR_XOR},
+        {CVC4::Kind::BITVECTOR_NOT, BITVECTOR_NOT},
+        {CVC4::Kind::BITVECTOR_NAND, BITVECTOR_NAND},
+        {CVC4::Kind::BITVECTOR_NOR, BITVECTOR_NOR},
+        {CVC4::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR},
+        {CVC4::Kind::BITVECTOR_COMP, BITVECTOR_COMP},
+        {CVC4::Kind::BITVECTOR_MULT, BITVECTOR_MULT},
+        {CVC4::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS},
+        {CVC4::Kind::BITVECTOR_SUB, BITVECTOR_SUB},
+        {CVC4::Kind::BITVECTOR_NEG, BITVECTOR_NEG},
+        {CVC4::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV},
+        {CVC4::Kind::BITVECTOR_UREM, BITVECTOR_UREM},
+        {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV},
+        {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM},
+        {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD},
+        {CVC4::Kind::BITVECTOR_UDIV_TOTAL, BITVECTOR_UDIV_TOTAL},
+        {CVC4::Kind::BITVECTOR_UREM_TOTAL, BITVECTOR_UREM_TOTAL},
+        {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL},
+        {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR},
+        {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR},
+        {CVC4::Kind::BITVECTOR_ULT, BITVECTOR_ULT},
+        {CVC4::Kind::BITVECTOR_ULE, BITVECTOR_ULE},
+        {CVC4::Kind::BITVECTOR_UGT, BITVECTOR_UGT},
+        {CVC4::Kind::BITVECTOR_UGE, BITVECTOR_UGE},
+        {CVC4::Kind::BITVECTOR_SLT, BITVECTOR_SLT},
+        {CVC4::Kind::BITVECTOR_SLE, BITVECTOR_SLE},
+        {CVC4::Kind::BITVECTOR_SGT, BITVECTOR_SGT},
+        {CVC4::Kind::BITVECTOR_SGE, BITVECTOR_SGE},
+        {CVC4::Kind::BITVECTOR_ULTBV, BITVECTOR_ULTBV},
+        {CVC4::Kind::BITVECTOR_SLTBV, BITVECTOR_SLTBV},
+        {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
+        {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
+        {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
+        {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT_OP},
+        {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT_OP},
+        {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND_OP},
+        {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND_OP},
+        {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT_OP},
+        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT_OP},
+        {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
+        {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
+        {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
+        {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
+        {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
+        {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
+        {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR_OP},
+        {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
+        {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
+        /* FP -------------------------------------------------------------- */
+        {CVC4::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT},
+        {CVC4::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE},
+        {CVC4::Kind::FLOATINGPOINT_FP, FLOATINGPOINT_FP},
+        {CVC4::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ},
+        {CVC4::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS},
+        {CVC4::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG},
+        {CVC4::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS},
+        {CVC4::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB},
+        {CVC4::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT},
+        {CVC4::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV},
+        {CVC4::Kind::FLOATINGPOINT_FMA, FLOATINGPOINT_FMA},
+        {CVC4::Kind::FLOATINGPOINT_SQRT, FLOATINGPOINT_SQRT},
+        {CVC4::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM},
+        {CVC4::Kind::FLOATINGPOINT_RTI, FLOATINGPOINT_RTI},
+        {CVC4::Kind::FLOATINGPOINT_MIN, FLOATINGPOINT_MIN},
+        {CVC4::Kind::FLOATINGPOINT_MAX, FLOATINGPOINT_MAX},
+        {CVC4::Kind::FLOATINGPOINT_LEQ, FLOATINGPOINT_LEQ},
+        {CVC4::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
+        {CVC4::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ},
+        {CVC4::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT},
+        {CVC4::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN},
+        {CVC4::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN},
+        {CVC4::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ},
+        {CVC4::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF},
+        {CVC4::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN},
+        {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
+        {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+         FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
+         FLOATINGPOINT_TO_FP_GENERIC_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP,
+         FLOATINGPOINT_TO_UBV_TOTAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP,
+         FLOATINGPOINT_TO_SBV_TOTAL_OP},
+        {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL},
+        {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
+        {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, FLOATINGPOINT_TO_REAL_TOTAL},
+        /* Arrays ---------------------------------------------------------- */
+        {CVC4::Kind::SELECT, SELECT},
+        {CVC4::Kind::STORE, STORE},
+        {CVC4::Kind::STORE_ALL, STORE_ALL},
+        /* Datatypes ------------------------------------------------------- */
+        {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
+        {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
+        {CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL},
+        {CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
+        {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE_OP},
+        {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
+        {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE_OP},
+        {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
+        /* Separation Logic ------------------------------------------------ */
+        {CVC4::Kind::SEP_NIL, SEP_NIL},
+        {CVC4::Kind::SEP_EMP, SEP_EMP},
+        {CVC4::Kind::SEP_PTO, SEP_PTO},
+        {CVC4::Kind::SEP_STAR, SEP_STAR},
+        {CVC4::Kind::SEP_WAND, SEP_WAND},
+        /* Sets ------------------------------------------------------------ */
+        {CVC4::Kind::EMPTYSET, EMPTYSET},
+        {CVC4::Kind::UNION, UNION},
+        {CVC4::Kind::INTERSECTION, INTERSECTION},
+        {CVC4::Kind::SETMINUS, SETMINUS},
+        {CVC4::Kind::SUBSET, SUBSET},
+        {CVC4::Kind::MEMBER, MEMBER},
+        {CVC4::Kind::SINGLETON, SINGLETON},
+        {CVC4::Kind::INSERT, INSERT},
+        {CVC4::Kind::CARD, CARD},
+        {CVC4::Kind::COMPLEMENT, COMPLEMENT},
+        {CVC4::Kind::UNIVERSE_SET, UNIVERSE_SET},
+        {CVC4::Kind::JOIN, JOIN},
+        {CVC4::Kind::PRODUCT, PRODUCT},
+        {CVC4::Kind::TRANSPOSE, TRANSPOSE},
+        {CVC4::Kind::TCLOSURE, TCLOSURE},
+        {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE},
+        {CVC4::Kind::IDEN, IDEN},
+        /* Strings --------------------------------------------------------- */
+        {CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
+        {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
+        {CVC4::Kind::STRING_LENGTH, STRING_LENGTH},
+        {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR},
+        {CVC4::Kind::STRING_CHARAT, STRING_CHARAT},
+        {CVC4::Kind::STRING_STRCTN, STRING_STRCTN},
+        {CVC4::Kind::STRING_STRIDOF, STRING_STRIDOF},
+        {CVC4::Kind::STRING_STRREPL, STRING_STRREPL},
+        {CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
+        {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
+        {CVC4::Kind::STRING_ITOS, STRING_ITOS},
+        {CVC4::Kind::STRING_STOI, STRING_STOI},
+        {CVC4::Kind::CONST_STRING, CONST_STRING},
+        {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP},
+        {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT},
+        {CVC4::Kind::REGEXP_UNION, REGEXP_UNION},
+        {CVC4::Kind::REGEXP_INTER, REGEXP_INTER},
+        {CVC4::Kind::REGEXP_STAR, REGEXP_STAR},
+        {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
+        {CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
+        {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
+        {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
+        {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
+        {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
+        /* Quantifiers ----------------------------------------------------- */
+        {CVC4::Kind::FORALL, FORALL},
+        {CVC4::Kind::EXISTS, EXISTS},
+        /* ----------------------------------------------------------------- */
+        {CVC4::Kind::LAST_KIND, LAST_KIND},
+    };
+
+namespace {
+  Kind intToExtKind(CVC4::Kind k)
+  {
+    auto it = s_kinds_internal.find(k);
+    if (it == s_kinds_internal.end()) { return INTERNAL_KIND; }
+    return it->second;
+  }
+
+  CVC4::Kind extToIntKind(Kind k)
+  {
+    auto it = s_kinds.find(k);
+    if (it == s_kinds.end()) { return CVC4::Kind::UNDEFINED_KIND; }
+    return it->second;
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, Kind k)
+{
+  switch (k)
+  {
+    case INTERNAL_KIND: out << "INTERNAL_KIND"; break;
+    default: out << extToIntKind(k);
+  }
+  return out;
+}
+
+size_t KindHashFunction::operator()(Kind k) const { return k; }
+
+/* -------------------------------------------------------------------------- */
 /* Sort                                                                       */
 /* -------------------------------------------------------------------------- */
 
@@ -267,6 +799,5 @@ size_t SortHashFunction::operator()(const Sort& s) const {
   return TypeHashFunction()(*s.d_type);
 }
 
-
 }  // namespace api
 }  // namespace CVC4