From 55725be5569e27755538f2032cbe7bcb9353f310 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 3 Jul 2018 08:59:35 -0700 Subject: [PATCH] New C++ API: Implementation of Kind maps. (#2130) --- src/api/cvc4cpp.cpp | 533 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 532 insertions(+), 1 deletion(-) 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" @@ -91,6 +92,537 @@ std::ostream& operator<<(std::ostream& out, const Result& r) return out; } +/* -------------------------------------------------------------------------- */ +/* Kind */ +/* -------------------------------------------------------------------------- */ + +/* Mapping from external (API) kind to internal kind. */ +const static std::unordered_map 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 + 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 -- 2.30.2