diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/checks.h | 4 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 1458 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 132 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 6 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxd | 4 | ||||
| -rw-r--r-- | src/api/python/genkinds.py.in | 4 |
6 files changed, 804 insertions, 804 deletions
diff --git a/src/api/checks.h b/src/api/checks.h index d5408d312..4686c0694 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -528,7 +528,7 @@ namespace api { this == bv.d_solver, "bound variable", bound_vars, i) \ << "a term associated with this solver object"; \ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - bv.d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, \ + bv.d_node->getKind() == CVC5::Kind::BOUND_VARIABLE, \ "bound variable", \ bound_vars, \ i) \ @@ -560,7 +560,7 @@ namespace api { this == bv.d_solver, "bound variable", bound_vars, i) \ << "a term associated with this solver object"; \ CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( \ - bv.d_node->getKind() == CVC4::Kind::BOUND_VARIABLE, \ + bv.d_node->getKind() == CVC5::Kind::BOUND_VARIABLE, \ "bound variable", \ bound_vars, \ i) \ diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e8b190003..66ddff9d4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -64,7 +64,7 @@ #include "util/stats_histogram.h" #include "util/utility.h" -namespace CVC4 { +namespace CVC5 { namespace api { /* -------------------------------------------------------------------------- */ @@ -87,570 +87,570 @@ struct Statistics /* -------------------------------------------------------------------------- */ /* 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}, +const static std::unordered_map<Kind, CVC5::Kind, KindHashFunction> s_kinds{ + {INTERNAL_KIND, CVC5::Kind::UNDEFINED_KIND}, + {UNDEFINED_KIND, CVC5::Kind::UNDEFINED_KIND}, + {NULL_EXPR, CVC5::Kind::NULL_EXPR}, /* Builtin ------------------------------------------------------------- */ - {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT}, - {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE}, - {EQUAL, CVC4::Kind::EQUAL}, - {DISTINCT, CVC4::Kind::DISTINCT}, - {CONSTANT, CVC4::Kind::VARIABLE}, - {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, - {SEXPR, CVC4::Kind::SEXPR}, - {LAMBDA, CVC4::Kind::LAMBDA}, - {WITNESS, CVC4::Kind::WITNESS}, + {UNINTERPRETED_CONSTANT, CVC5::Kind::UNINTERPRETED_CONSTANT}, + {ABSTRACT_VALUE, CVC5::Kind::ABSTRACT_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, 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}, - {MATCH, CVC4::Kind::MATCH}, - {MATCH_CASE, CVC4::Kind::MATCH_CASE}, - {MATCH_BIND_CASE, CVC4::Kind::MATCH_BIND_CASE}, + {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}, + {MATCH, CVC5::Kind::MATCH}, + {MATCH_CASE, CVC5::Kind::MATCH_CASE}, + {MATCH_BIND_CASE, CVC5::Kind::MATCH_BIND_CASE}, /* UF ------------------------------------------------------------------ */ - {APPLY_UF, CVC4::Kind::APPLY_UF}, - {CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT}, - {CARDINALITY_VALUE, CVC4::Kind::CARDINALITY_VALUE}, - {HO_APPLY, CVC4::Kind::HO_APPLY}, + {APPLY_UF, CVC5::Kind::APPLY_UF}, + {CARDINALITY_CONSTRAINT, CVC5::Kind::CARDINALITY_CONSTRAINT}, + {CARDINALITY_VALUE, CVC5::Kind::CARDINALITY_VALUE}, + {HO_APPLY, CVC5::Kind::HO_APPLY}, /* Arithmetic ---------------------------------------------------------- */ - {PLUS, CVC4::Kind::PLUS}, - {MULT, CVC4::Kind::MULT}, - {IAND, CVC4::Kind::IAND}, - {MINUS, CVC4::Kind::MINUS}, - {UMINUS, CVC4::Kind::UMINUS}, - {DIVISION, CVC4::Kind::DIVISION}, - {INTS_DIVISION, CVC4::Kind::INTS_DIVISION}, - {INTS_MODULUS, CVC4::Kind::INTS_MODULUS}, - {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}, - {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}, + {PLUS, CVC5::Kind::PLUS}, + {MULT, CVC5::Kind::MULT}, + {IAND, CVC5::Kind::IAND}, + {MINUS, CVC5::Kind::MINUS}, + {UMINUS, CVC5::Kind::UMINUS}, + {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, 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_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, 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, CVC4::Kind::INT_TO_BITVECTOR}, - {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT}, + {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_PLUS, CVC5::Kind::BITVECTOR_PLUS}, + {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, 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}, + {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_PLUS, CVC5::Kind::FLOATINGPOINT_PLUS}, + {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_ISN, CVC5::Kind::FLOATINGPOINT_ISN}, + {FLOATINGPOINT_ISSN, CVC5::Kind::FLOATINGPOINT_ISSN}, + {FLOATINGPOINT_ISZ, CVC5::Kind::FLOATINGPOINT_ISZ}, + {FLOATINGPOINT_ISINF, CVC5::Kind::FLOATINGPOINT_ISINF}, + {FLOATINGPOINT_ISNAN, CVC5::Kind::FLOATINGPOINT_ISNAN}, + {FLOATINGPOINT_ISNEG, CVC5::Kind::FLOATINGPOINT_ISNEG}, + {FLOATINGPOINT_ISPOS, CVC5::Kind::FLOATINGPOINT_ISPOS}, {FLOATINGPOINT_TO_FP_FLOATINGPOINT, - CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL}, + CVC5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, + {FLOATINGPOINT_TO_FP_REAL, CVC5::Kind::FLOATINGPOINT_TO_FP_REAL}, {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, + CVC5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, - {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC}, - {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV}, - {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV}, - {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL}, + CVC5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, + {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, CVC4::Kind::SELECT}, - {STORE, CVC4::Kind::STORE}, - {CONST_ARRAY, CVC4::Kind::STORE_ALL}, - {EQ_RANGE, CVC4::Kind::EQ_RANGE}, + {SELECT, CVC5::Kind::SELECT}, + {STORE, CVC5::Kind::STORE}, + {CONST_ARRAY, CVC5::Kind::STORE_ALL}, + {EQ_RANGE, CVC5::Kind::EQ_RANGE}, /* Datatypes ----------------------------------------------------------- */ - {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR}, - {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR}, - {APPLY_TESTER, CVC4::Kind::APPLY_TESTER}, - {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE}, - {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE}, - {DT_SIZE, CVC4::Kind::DT_SIZE}, - {TUPLE_PROJECT, CVC4::Kind::TUPLE_PROJECT}, + {APPLY_SELECTOR, CVC5::Kind::APPLY_SELECTOR}, + {APPLY_CONSTRUCTOR, CVC5::Kind::APPLY_CONSTRUCTOR}, + {APPLY_TESTER, CVC5::Kind::APPLY_TESTER}, + {TUPLE_UPDATE, CVC5::Kind::TUPLE_UPDATE}, + {RECORD_UPDATE, CVC5::Kind::RECORD_UPDATE}, + {DT_SIZE, CVC5::Kind::DT_SIZE}, + {TUPLE_PROJECT, CVC5::Kind::TUPLE_PROJECT}, /* 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}, + {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 ---------------------------------------------------------------- */ - {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}, - {COMPREHENSION, CVC4::Kind::COMPREHENSION}, - {CHOOSE, CVC4::Kind::CHOOSE}, - {IS_SINGLETON, CVC4::Kind::IS_SINGLETON}, + {EMPTYSET, CVC5::Kind::EMPTYSET}, + {UNION, CVC5::Kind::UNION}, + {INTERSECTION, CVC5::Kind::INTERSECTION}, + {SETMINUS, CVC5::Kind::SETMINUS}, + {SUBSET, CVC5::Kind::SUBSET}, + {MEMBER, CVC5::Kind::MEMBER}, + {SINGLETON, CVC5::Kind::SINGLETON}, + {INSERT, CVC5::Kind::INSERT}, + {CARD, CVC5::Kind::CARD}, + {COMPLEMENT, CVC5::Kind::COMPLEMENT}, + {UNIVERSE_SET, CVC5::Kind::UNIVERSE_SET}, + {JOIN, CVC5::Kind::JOIN}, + {PRODUCT, CVC5::Kind::PRODUCT}, + {TRANSPOSE, CVC5::Kind::TRANSPOSE}, + {TCLOSURE, CVC5::Kind::TCLOSURE}, + {JOIN_IMAGE, CVC5::Kind::JOIN_IMAGE}, + {IDEN, CVC5::Kind::IDEN}, + {COMPREHENSION, CVC5::Kind::COMPREHENSION}, + {CHOOSE, CVC5::Kind::CHOOSE}, + {IS_SINGLETON, CVC5::Kind::IS_SINGLETON}, /* Bags ---------------------------------------------------------------- */ - {UNION_MAX, CVC4::Kind::UNION_MAX}, - {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT}, - {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN}, - {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT}, - {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE}, - {SUBBAG, CVC4::Kind::SUBBAG}, - {BAG_COUNT, CVC4::Kind::BAG_COUNT}, - {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL}, - {MK_BAG, CVC4::Kind::MK_BAG}, - {EMPTYBAG, CVC4::Kind::EMPTYBAG}, - {BAG_CARD, CVC4::Kind::BAG_CARD}, - {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE}, - {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON}, - {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET}, - {BAG_TO_SET, CVC4::Kind::BAG_TO_SET}, + {UNION_MAX, CVC5::Kind::UNION_MAX}, + {UNION_DISJOINT, CVC5::Kind::UNION_DISJOINT}, + {INTERSECTION_MIN, CVC5::Kind::INTERSECTION_MIN}, + {DIFFERENCE_SUBTRACT, CVC5::Kind::DIFFERENCE_SUBTRACT}, + {DIFFERENCE_REMOVE, CVC5::Kind::DIFFERENCE_REMOVE}, + {SUBBAG, CVC5::Kind::SUBBAG}, + {BAG_COUNT, CVC5::Kind::BAG_COUNT}, + {DUPLICATE_REMOVAL, CVC5::Kind::DUPLICATE_REMOVAL}, + {MK_BAG, CVC5::Kind::MK_BAG}, + {EMPTYBAG, CVC5::Kind::EMPTYBAG}, + {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}, /* 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_UPDATE, CVC4::Kind::STRING_UPDATE}, - {STRING_CHARAT, CVC4::Kind::STRING_CHARAT}, - {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN}, - {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF}, - {STRING_REPLACE, CVC4::Kind::STRING_STRREPL}, - {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL}, - {STRING_REPLACE_RE, CVC4::Kind::STRING_REPLACE_RE}, - {STRING_REPLACE_RE_ALL, CVC4::Kind::STRING_REPLACE_RE_ALL}, - {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER}, - {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER}, - {STRING_REV, CVC4::Kind::STRING_REV}, - {STRING_FROM_CODE, CVC4::Kind::STRING_FROM_CODE}, - {STRING_TO_CODE, CVC4::Kind::STRING_TO_CODE}, - {STRING_LT, CVC4::Kind::STRING_LT}, - {STRING_LEQ, CVC4::Kind::STRING_LEQ}, - {STRING_PREFIX, CVC4::Kind::STRING_PREFIX}, - {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX}, - {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT}, - {STRING_FROM_INT, CVC4::Kind::STRING_ITOS}, - {STRING_TO_INT, 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_DIFF, CVC4::Kind::REGEXP_DIFF}, - {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_REPEAT, CVC4::Kind::REGEXP_REPEAT}, - {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP}, - {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY}, - {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA}, - {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT}, + {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_STRCTN}, + {STRING_INDEXOF, CVC5::Kind::STRING_STRIDOF}, + {STRING_REPLACE, CVC5::Kind::STRING_STRREPL}, + {STRING_REPLACE_ALL, CVC5::Kind::STRING_STRREPLALL}, + {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_EMPTY, CVC5::Kind::REGEXP_EMPTY}, + {REGEXP_SIGMA, CVC5::Kind::REGEXP_SIGMA}, + {REGEXP_COMPLEMENT, CVC5::Kind::REGEXP_COMPLEMENT}, // maps to the same kind as the string versions - {SEQ_CONCAT, CVC4::Kind::STRING_CONCAT}, - {SEQ_LENGTH, CVC4::Kind::STRING_LENGTH}, - {SEQ_EXTRACT, CVC4::Kind::STRING_SUBSTR}, - {SEQ_UPDATE, CVC4::Kind::STRING_UPDATE}, - {SEQ_AT, CVC4::Kind::STRING_CHARAT}, - {SEQ_CONTAINS, CVC4::Kind::STRING_STRCTN}, - {SEQ_INDEXOF, CVC4::Kind::STRING_STRIDOF}, - {SEQ_REPLACE, CVC4::Kind::STRING_STRREPL}, - {SEQ_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL}, - {SEQ_REV, CVC4::Kind::STRING_REV}, - {SEQ_PREFIX, CVC4::Kind::STRING_PREFIX}, - {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX}, - {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE}, - {SEQ_UNIT, CVC4::Kind::SEQ_UNIT}, - {SEQ_NTH, CVC4::Kind::SEQ_NTH}, + {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_STRCTN}, + {SEQ_INDEXOF, CVC5::Kind::STRING_STRIDOF}, + {SEQ_REPLACE, CVC5::Kind::STRING_STRREPL}, + {SEQ_REPLACE_ALL, CVC5::Kind::STRING_STRREPLALL}, + {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, CVC4::Kind::FORALL}, - {EXISTS, CVC4::Kind::EXISTS}, - {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST}, - {INST_PATTERN, CVC4::Kind::INST_PATTERN}, - {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN}, - {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE}, - {INST_PATTERN_LIST, CVC4::Kind::INST_PATTERN_LIST}, - {LAST_KIND, CVC4::Kind::LAST_KIND}, + {FORALL, CVC5::Kind::FORALL}, + {EXISTS, CVC5::Kind::EXISTS}, + {BOUND_VAR_LIST, CVC5::Kind::BOUND_VAR_LIST}, + {INST_PATTERN, CVC5::Kind::INST_PATTERN}, + {INST_NO_PATTERN, CVC5::Kind::INST_NO_PATTERN}, + {INST_ATTRIBUTE, CVC5::Kind::INST_ATTRIBUTE}, + {INST_PATTERN_LIST, CVC5::Kind::INST_PATTERN_LIST}, + {LAST_KIND, CVC5::Kind::LAST_KIND}, }; /* Mapping from internal kind to external (API) kind. */ -const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> +const static std::unordered_map<CVC5::Kind, Kind, CVC5::kind::KindHashFunction> s_kinds_internal{ - {CVC4::Kind::UNDEFINED_KIND, UNDEFINED_KIND}, - {CVC4::Kind::NULL_EXPR, NULL_EXPR}, + {CVC5::Kind::UNDEFINED_KIND, UNDEFINED_KIND}, + {CVC5::Kind::NULL_EXPR, NULL_EXPR}, /* Builtin --------------------------------------------------------- */ - {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT}, - {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE}, - {CVC4::Kind::EQUAL, EQUAL}, - {CVC4::Kind::DISTINCT, DISTINCT}, - {CVC4::Kind::VARIABLE, CONSTANT}, - {CVC4::Kind::BOUND_VARIABLE, VARIABLE}, - {CVC4::Kind::SEXPR, SEXPR}, - {CVC4::Kind::LAMBDA, LAMBDA}, - {CVC4::Kind::WITNESS, WITNESS}, + {CVC5::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT}, + {CVC5::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE}, + {CVC5::Kind::EQUAL, EQUAL}, + {CVC5::Kind::DISTINCT, DISTINCT}, + {CVC5::Kind::VARIABLE, CONSTANT}, + {CVC5::Kind::BOUND_VARIABLE, VARIABLE}, + {CVC5::Kind::SEXPR, SEXPR}, + {CVC5::Kind::LAMBDA, LAMBDA}, + {CVC5::Kind::WITNESS, WITNESS}, /* 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}, - {CVC4::Kind::MATCH, MATCH}, - {CVC4::Kind::MATCH_CASE, MATCH_CASE}, - {CVC4::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE}, + {CVC5::Kind::CONST_BOOLEAN, CONST_BOOLEAN}, + {CVC5::Kind::NOT, NOT}, + {CVC5::Kind::AND, AND}, + {CVC5::Kind::IMPLIES, IMPLIES}, + {CVC5::Kind::OR, OR}, + {CVC5::Kind::XOR, XOR}, + {CVC5::Kind::ITE, ITE}, + {CVC5::Kind::MATCH, MATCH}, + {CVC5::Kind::MATCH_CASE, MATCH_CASE}, + {CVC5::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE}, /* UF -------------------------------------------------------------- */ - {CVC4::Kind::APPLY_UF, APPLY_UF}, - {CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT}, - {CVC4::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE}, - {CVC4::Kind::HO_APPLY, HO_APPLY}, + {CVC5::Kind::APPLY_UF, APPLY_UF}, + {CVC5::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT}, + {CVC5::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE}, + {CVC5::Kind::HO_APPLY, HO_APPLY}, /* Arithmetic ------------------------------------------------------ */ - {CVC4::Kind::PLUS, PLUS}, - {CVC4::Kind::MULT, MULT}, - {CVC4::Kind::IAND, IAND}, - {CVC4::Kind::MINUS, MINUS}, - {CVC4::Kind::UMINUS, UMINUS}, - {CVC4::Kind::DIVISION, DIVISION}, - {CVC4::Kind::DIVISION_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::INTS_DIVISION, INTS_DIVISION}, - {CVC4::Kind::INTS_DIVISION_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::INTS_MODULUS, INTS_MODULUS}, - {CVC4::Kind::INTS_MODULUS_TOTAL, INTERNAL_KIND}, - {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}, - {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}, + {CVC5::Kind::PLUS, PLUS}, + {CVC5::Kind::MULT, MULT}, + {CVC5::Kind::IAND, IAND}, + {CVC5::Kind::MINUS, MINUS}, + {CVC5::Kind::UMINUS, UMINUS}, + {CVC5::Kind::DIVISION, DIVISION}, + {CVC5::Kind::DIVISION_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::INTS_DIVISION, INTS_DIVISION}, + {CVC5::Kind::INTS_DIVISION_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::INTS_MODULUS, INTS_MODULUS}, + {CVC5::Kind::INTS_MODULUS_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::ABS, ABS}, + {CVC5::Kind::DIVISIBLE, DIVISIBLE}, + {CVC5::Kind::POW, POW}, + {CVC5::Kind::EXPONENTIAL, EXPONENTIAL}, + {CVC5::Kind::SINE, SINE}, + {CVC5::Kind::COSINE, COSINE}, + {CVC5::Kind::TANGENT, TANGENT}, + {CVC5::Kind::COSECANT, COSECANT}, + {CVC5::Kind::SECANT, SECANT}, + {CVC5::Kind::COTANGENT, COTANGENT}, + {CVC5::Kind::ARCSINE, ARCSINE}, + {CVC5::Kind::ARCCOSINE, ARCCOSINE}, + {CVC5::Kind::ARCTANGENT, ARCTANGENT}, + {CVC5::Kind::ARCCOSECANT, ARCCOSECANT}, + {CVC5::Kind::ARCSECANT, ARCSECANT}, + {CVC5::Kind::ARCCOTANGENT, ARCCOTANGENT}, + {CVC5::Kind::SQRT, SQRT}, + {CVC5::Kind::DIVISIBLE_OP, DIVISIBLE}, + {CVC5::Kind::CONST_RATIONAL, CONST_RATIONAL}, + {CVC5::Kind::LT, LT}, + {CVC5::Kind::LEQ, LEQ}, + {CVC5::Kind::GT, GT}, + {CVC5::Kind::GEQ, GEQ}, + {CVC5::Kind::IS_INTEGER, IS_INTEGER}, + {CVC5::Kind::TO_INTEGER, TO_INTEGER}, + {CVC5::Kind::TO_REAL, TO_REAL}, + {CVC5::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_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}, - {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT}, - {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND}, - {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND}, - {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT}, - {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT}, - {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}, - {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR}, - {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT}, + {CVC5::Kind::CONST_BITVECTOR, CONST_BITVECTOR}, + {CVC5::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT}, + {CVC5::Kind::BITVECTOR_AND, BITVECTOR_AND}, + {CVC5::Kind::BITVECTOR_OR, BITVECTOR_OR}, + {CVC5::Kind::BITVECTOR_XOR, BITVECTOR_XOR}, + {CVC5::Kind::BITVECTOR_NOT, BITVECTOR_NOT}, + {CVC5::Kind::BITVECTOR_NAND, BITVECTOR_NAND}, + {CVC5::Kind::BITVECTOR_NOR, BITVECTOR_NOR}, + {CVC5::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR}, + {CVC5::Kind::BITVECTOR_COMP, BITVECTOR_COMP}, + {CVC5::Kind::BITVECTOR_MULT, BITVECTOR_MULT}, + {CVC5::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS}, + {CVC5::Kind::BITVECTOR_SUB, BITVECTOR_SUB}, + {CVC5::Kind::BITVECTOR_NEG, BITVECTOR_NEG}, + {CVC5::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV}, + {CVC5::Kind::BITVECTOR_UREM, BITVECTOR_UREM}, + {CVC5::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV}, + {CVC5::Kind::BITVECTOR_SREM, BITVECTOR_SREM}, + {CVC5::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD}, + {CVC5::Kind::BITVECTOR_SHL, BITVECTOR_SHL}, + {CVC5::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR}, + {CVC5::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR}, + {CVC5::Kind::BITVECTOR_ULT, BITVECTOR_ULT}, + {CVC5::Kind::BITVECTOR_ULE, BITVECTOR_ULE}, + {CVC5::Kind::BITVECTOR_UGT, BITVECTOR_UGT}, + {CVC5::Kind::BITVECTOR_UGE, BITVECTOR_UGE}, + {CVC5::Kind::BITVECTOR_SLT, BITVECTOR_SLT}, + {CVC5::Kind::BITVECTOR_SLE, BITVECTOR_SLE}, + {CVC5::Kind::BITVECTOR_SGT, BITVECTOR_SGT}, + {CVC5::Kind::BITVECTOR_SGE, BITVECTOR_SGE}, + {CVC5::Kind::BITVECTOR_ULTBV, BITVECTOR_ULTBV}, + {CVC5::Kind::BITVECTOR_SLTBV, BITVECTOR_SLTBV}, + {CVC5::Kind::BITVECTOR_ITE, BITVECTOR_ITE}, + {CVC5::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR}, + {CVC5::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND}, + {CVC5::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT}, + {CVC5::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT}, + {CVC5::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND}, + {CVC5::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND}, + {CVC5::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT}, + {CVC5::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT}, + {CVC5::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT}, + {CVC5::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT}, + {CVC5::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND}, + {CVC5::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND}, + {CVC5::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT}, + {CVC5::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT}, + {CVC5::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR}, + {CVC5::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR}, + {CVC5::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, + {CVC5::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT}, + {CVC5::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE}, + {CVC5::Kind::FLOATINGPOINT_FP, FLOATINGPOINT_FP}, + {CVC5::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ}, + {CVC5::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS}, + {CVC5::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG}, + {CVC5::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS}, + {CVC5::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB}, + {CVC5::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT}, + {CVC5::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV}, + {CVC5::Kind::FLOATINGPOINT_FMA, FLOATINGPOINT_FMA}, + {CVC5::Kind::FLOATINGPOINT_SQRT, FLOATINGPOINT_SQRT}, + {CVC5::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM}, + {CVC5::Kind::FLOATINGPOINT_RTI, FLOATINGPOINT_RTI}, + {CVC5::Kind::FLOATINGPOINT_MIN, FLOATINGPOINT_MIN}, + {CVC5::Kind::FLOATINGPOINT_MAX, FLOATINGPOINT_MAX}, + {CVC5::Kind::FLOATINGPOINT_LEQ, FLOATINGPOINT_LEQ}, + {CVC5::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT}, + {CVC5::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ}, + {CVC5::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT}, + {CVC5::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN}, + {CVC5::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN}, + {CVC5::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ}, + {CVC5::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF}, + {CVC5::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN}, + {CVC5::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG}, + {CVC5::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS}, + {CVC5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + {CVC5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, + {CVC5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, + {CVC5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, + {CVC5::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL}, + {CVC5::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL}, + {CVC5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + {CVC5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, + {CVC5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + {CVC5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP, + {CVC5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP, FLOATINGPOINT_TO_FP_GENERIC}, - {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, INTERNAL_KIND}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL}, - {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC}, + {CVC5::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV}, + {CVC5::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV}, + {CVC5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND}, + {CVC5::Kind::FLOATINGPOINT_TO_UBV_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV}, + {CVC5::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV}, + {CVC5::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, INTERNAL_KIND}, + {CVC5::Kind::FLOATINGPOINT_TO_SBV_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL}, + {CVC5::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND}, /* Arrays ---------------------------------------------------------- */ - {CVC4::Kind::SELECT, SELECT}, - {CVC4::Kind::STORE, STORE}, - {CVC4::Kind::STORE_ALL, CONST_ARRAY}, + {CVC5::Kind::SELECT, SELECT}, + {CVC5::Kind::STORE, STORE}, + {CVC5::Kind::STORE_ALL, CONST_ARRAY}, /* Datatypes ------------------------------------------------------- */ - {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, - {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, - {CVC4::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, - {CVC4::Kind::APPLY_TESTER, APPLY_TESTER}, - {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE}, - {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE}, - {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, - {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE}, - {CVC4::Kind::DT_SIZE, DT_SIZE}, - {CVC4::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, + {CVC5::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, + {CVC5::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, + {CVC5::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND}, + {CVC5::Kind::APPLY_TESTER, APPLY_TESTER}, + {CVC5::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE}, + {CVC5::Kind::TUPLE_UPDATE, TUPLE_UPDATE}, + {CVC5::Kind::RECORD_UPDATE_OP, RECORD_UPDATE}, + {CVC5::Kind::RECORD_UPDATE, RECORD_UPDATE}, + {CVC5::Kind::DT_SIZE, DT_SIZE}, + {CVC5::Kind::TUPLE_PROJECT, TUPLE_PROJECT}, /* 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}, + {CVC5::Kind::SEP_NIL, SEP_NIL}, + {CVC5::Kind::SEP_EMP, SEP_EMP}, + {CVC5::Kind::SEP_PTO, SEP_PTO}, + {CVC5::Kind::SEP_STAR, SEP_STAR}, + {CVC5::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}, - {CVC4::Kind::COMPREHENSION, COMPREHENSION}, - {CVC4::Kind::CHOOSE, CHOOSE}, - {CVC4::Kind::IS_SINGLETON, IS_SINGLETON}, + {CVC5::Kind::EMPTYSET, EMPTYSET}, + {CVC5::Kind::UNION, UNION}, + {CVC5::Kind::INTERSECTION, INTERSECTION}, + {CVC5::Kind::SETMINUS, SETMINUS}, + {CVC5::Kind::SUBSET, SUBSET}, + {CVC5::Kind::MEMBER, MEMBER}, + {CVC5::Kind::SINGLETON, SINGLETON}, + {CVC5::Kind::INSERT, INSERT}, + {CVC5::Kind::CARD, CARD}, + {CVC5::Kind::COMPLEMENT, COMPLEMENT}, + {CVC5::Kind::UNIVERSE_SET, UNIVERSE_SET}, + {CVC5::Kind::JOIN, JOIN}, + {CVC5::Kind::PRODUCT, PRODUCT}, + {CVC5::Kind::TRANSPOSE, TRANSPOSE}, + {CVC5::Kind::TCLOSURE, TCLOSURE}, + {CVC5::Kind::JOIN_IMAGE, JOIN_IMAGE}, + {CVC5::Kind::IDEN, IDEN}, + {CVC5::Kind::COMPREHENSION, COMPREHENSION}, + {CVC5::Kind::CHOOSE, CHOOSE}, + {CVC5::Kind::IS_SINGLETON, IS_SINGLETON}, /* Bags ------------------------------------------------------------ */ - {CVC4::Kind::UNION_MAX, UNION_MAX}, - {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT}, - {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, - {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, - {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, - {CVC4::Kind::SUBBAG, SUBBAG}, - {CVC4::Kind::BAG_COUNT, BAG_COUNT}, - {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL}, - {CVC4::Kind::MK_BAG, MK_BAG}, - {CVC4::Kind::EMPTYBAG, EMPTYBAG}, - {CVC4::Kind::BAG_CARD, BAG_CARD}, - {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE}, - {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, - {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET}, - {CVC4::Kind::BAG_TO_SET, BAG_TO_SET}, + {CVC5::Kind::UNION_MAX, UNION_MAX}, + {CVC5::Kind::UNION_DISJOINT, UNION_DISJOINT}, + {CVC5::Kind::INTERSECTION_MIN, INTERSECTION_MIN}, + {CVC5::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT}, + {CVC5::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE}, + {CVC5::Kind::SUBBAG, SUBBAG}, + {CVC5::Kind::BAG_COUNT, BAG_COUNT}, + {CVC5::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL}, + {CVC5::Kind::MK_BAG, MK_BAG}, + {CVC5::Kind::EMPTYBAG, EMPTYBAG}, + {CVC5::Kind::BAG_CARD, BAG_CARD}, + {CVC5::Kind::BAG_CHOOSE, BAG_CHOOSE}, + {CVC5::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON}, + {CVC5::Kind::BAG_FROM_SET, BAG_FROM_SET}, + {CVC5::Kind::BAG_TO_SET, BAG_TO_SET}, /* 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_UPDATE, STRING_UPDATE}, - {CVC4::Kind::STRING_CHARAT, STRING_CHARAT}, - {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS}, - {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF}, - {CVC4::Kind::STRING_STRREPL, STRING_REPLACE}, - {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL}, - {CVC4::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE}, - {CVC4::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL}, - {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER}, - {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER}, - {CVC4::Kind::STRING_REV, STRING_REV}, - {CVC4::Kind::STRING_FROM_CODE, STRING_FROM_CODE}, - {CVC4::Kind::STRING_TO_CODE, STRING_TO_CODE}, - {CVC4::Kind::STRING_LT, STRING_LT}, - {CVC4::Kind::STRING_LEQ, STRING_LEQ}, - {CVC4::Kind::STRING_PREFIX, STRING_PREFIX}, - {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX}, - {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT}, - {CVC4::Kind::STRING_ITOS, STRING_FROM_INT}, - {CVC4::Kind::STRING_STOI, STRING_TO_INT}, - {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_DIFF, REGEXP_DIFF}, - {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_REPEAT, REGEXP_REPEAT}, - {CVC4::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, - {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP}, - {CVC4::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, - {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, - {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, - {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, - {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, - {CVC4::Kind::SEQ_UNIT, SEQ_UNIT}, - {CVC4::Kind::SEQ_NTH, SEQ_NTH}, + {CVC5::Kind::STRING_CONCAT, STRING_CONCAT}, + {CVC5::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, + {CVC5::Kind::STRING_LENGTH, STRING_LENGTH}, + {CVC5::Kind::STRING_SUBSTR, STRING_SUBSTR}, + {CVC5::Kind::STRING_UPDATE, STRING_UPDATE}, + {CVC5::Kind::STRING_CHARAT, STRING_CHARAT}, + {CVC5::Kind::STRING_STRCTN, STRING_CONTAINS}, + {CVC5::Kind::STRING_STRIDOF, STRING_INDEXOF}, + {CVC5::Kind::STRING_STRREPL, STRING_REPLACE}, + {CVC5::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL}, + {CVC5::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE}, + {CVC5::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL}, + {CVC5::Kind::STRING_TOLOWER, STRING_TOLOWER}, + {CVC5::Kind::STRING_TOUPPER, STRING_TOUPPER}, + {CVC5::Kind::STRING_REV, STRING_REV}, + {CVC5::Kind::STRING_FROM_CODE, STRING_FROM_CODE}, + {CVC5::Kind::STRING_TO_CODE, STRING_TO_CODE}, + {CVC5::Kind::STRING_LT, STRING_LT}, + {CVC5::Kind::STRING_LEQ, STRING_LEQ}, + {CVC5::Kind::STRING_PREFIX, STRING_PREFIX}, + {CVC5::Kind::STRING_SUFFIX, STRING_SUFFIX}, + {CVC5::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT}, + {CVC5::Kind::STRING_ITOS, STRING_FROM_INT}, + {CVC5::Kind::STRING_STOI, STRING_TO_INT}, + {CVC5::Kind::CONST_STRING, CONST_STRING}, + {CVC5::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP}, + {CVC5::Kind::REGEXP_CONCAT, REGEXP_CONCAT}, + {CVC5::Kind::REGEXP_UNION, REGEXP_UNION}, + {CVC5::Kind::REGEXP_INTER, REGEXP_INTER}, + {CVC5::Kind::REGEXP_DIFF, REGEXP_DIFF}, + {CVC5::Kind::REGEXP_STAR, REGEXP_STAR}, + {CVC5::Kind::REGEXP_PLUS, REGEXP_PLUS}, + {CVC5::Kind::REGEXP_OPT, REGEXP_OPT}, + {CVC5::Kind::REGEXP_RANGE, REGEXP_RANGE}, + {CVC5::Kind::REGEXP_REPEAT, REGEXP_REPEAT}, + {CVC5::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT}, + {CVC5::Kind::REGEXP_LOOP, REGEXP_LOOP}, + {CVC5::Kind::REGEXP_LOOP_OP, REGEXP_LOOP}, + {CVC5::Kind::REGEXP_EMPTY, REGEXP_EMPTY}, + {CVC5::Kind::REGEXP_SIGMA, REGEXP_SIGMA}, + {CVC5::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT}, + {CVC5::Kind::CONST_SEQUENCE, CONST_SEQUENCE}, + {CVC5::Kind::SEQ_UNIT, SEQ_UNIT}, + {CVC5::Kind::SEQ_NTH, SEQ_NTH}, /* Quantifiers ----------------------------------------------------- */ - {CVC4::Kind::FORALL, FORALL}, - {CVC4::Kind::EXISTS, EXISTS}, - {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, - {CVC4::Kind::INST_PATTERN, INST_PATTERN}, - {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, - {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE}, - {CVC4::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST}, + {CVC5::Kind::FORALL, FORALL}, + {CVC5::Kind::EXISTS, EXISTS}, + {CVC5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, + {CVC5::Kind::INST_PATTERN, INST_PATTERN}, + {CVC5::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, + {CVC5::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE}, + {CVC5::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST}, /* ----------------------------------------------------------------- */ - {CVC4::Kind::LAST_KIND, LAST_KIND}, + {CVC5::Kind::LAST_KIND, LAST_KIND}, }; /* Set of kinds for indexed operators */ @@ -677,8 +677,8 @@ const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds( namespace { -/** Convert a CVC4::Kind (internal) to a CVC4::api::Kind (external). */ -CVC4::api::Kind intToExtKind(CVC4::Kind k) +/** Convert a CVC5::Kind (internal) to a CVC5::api::Kind (external). */ +CVC5::api::Kind intToExtKind(CVC5::Kind k) { auto it = api::s_kinds_internal.find(k); if (it == api::s_kinds_internal.end()) @@ -688,13 +688,13 @@ CVC4::api::Kind intToExtKind(CVC4::Kind k) return it->second; } -/** Convert a CVC4::api::Kind (external) to a CVC4::Kind (internal). */ -CVC4::Kind extToIntKind(CVC4::api::Kind k) +/** Convert a CVC5::api::Kind (external) to a CVC5::Kind (internal). */ +CVC5::Kind extToIntKind(CVC5::api::Kind k) { auto it = api::s_kinds.find(k); if (it == api::s_kinds.end()) { - return CVC4::Kind::UNDEFINED_KIND; + return CVC5::Kind::UNDEFINED_KIND; } return it->second; } @@ -709,17 +709,17 @@ bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; } * as datatype constructors/selectors/testers as terms * but interally they are not */ -bool isApplyKind(CVC4::Kind k) +bool isApplyKind(CVC5::Kind k) { - return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR - || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER); + return (k == CVC5::Kind::APPLY_UF || k == CVC5::Kind::APPLY_CONSTRUCTOR + || k == CVC5::Kind::APPLY_SELECTOR || k == CVC5::Kind::APPLY_TESTER); } #ifdef CVC4_ASSERTIONS /** Return true if given kind is a defined internal kind. */ -bool isDefinedIntKind(CVC4::Kind k) +bool isDefinedIntKind(CVC5::Kind k) { - return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND; + return k != CVC5::Kind::UNDEFINED_KIND && k != CVC5::Kind::LAST_KIND; } #endif @@ -728,7 +728,7 @@ uint32_t minArity(Kind k) { Assert(isDefinedKind(k)); Assert(isDefinedIntKind(extToIntKind(k))); - uint32_t min = CVC4::kind::metakind::getMinArityForKind(extToIntKind(k)); + uint32_t min = CVC5::kind::metakind::getMinArityForKind(extToIntKind(k)); // At the API level, we treat functions/constructors/selectors/testers as // normal terms instead of making them part of the operator @@ -744,7 +744,7 @@ uint32_t maxArity(Kind k) { Assert(isDefinedKind(k)); Assert(isDefinedIntKind(extToIntKind(k))); - uint32_t max = CVC4::kind::metakind::getMaxArityForKind(extToIntKind(k)); + uint32_t max = CVC5::kind::metakind::getMaxArityForKind(extToIntKind(k)); // At the API level, we treat functions/constructors/selectors/testers as // normal terms instead of making them part of the operator @@ -762,7 +762,7 @@ uint32_t maxArity(Kind k) std::string kindToString(Kind k) { return k == INTERNAL_KIND ? "INTERNAL_KIND" - : CVC4::kind::kindToString(extToIntKind(k)); + : CVC5::kind::kindToString(extToIntKind(k)); } std::ostream& operator<<(std::ostream& out, Kind k) @@ -834,11 +834,11 @@ class CVC4ApiRecoverableExceptionStream { \ throw CVC4ApiRecoverableException(e.getMessage()); \ } \ - catch (const CVC4::RecoverableModalException& e) \ + catch (const CVC5::RecoverableModalException& e) \ { \ throw CVC4ApiRecoverableException(e.getMessage()); \ } \ - catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ + catch (const CVC5::Exception& e) { throw CVC4ApiException(e.getMessage()); } \ catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); } } // namespace @@ -847,49 +847,49 @@ class CVC4ApiRecoverableExceptionStream /* Result */ /* -------------------------------------------------------------------------- */ -Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {} +Result::Result(const CVC5::Result& r) : d_result(new CVC5::Result(r)) {} -Result::Result() : d_result(new CVC4::Result()) {} +Result::Result() : d_result(new CVC5::Result()) {} bool Result::isNull() const { - return d_result->getType() == CVC4::Result::TYPE_NONE; + return d_result->getType() == CVC5::Result::TYPE_NONE; } bool Result::isSat(void) const { - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::SAT; + return d_result->getType() == CVC5::Result::TYPE_SAT + && d_result->isSat() == CVC5::Result::SAT; } bool Result::isUnsat(void) const { - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::UNSAT; + return d_result->getType() == CVC5::Result::TYPE_SAT + && d_result->isSat() == CVC5::Result::UNSAT; } bool Result::isSatUnknown(void) const { - return d_result->getType() == CVC4::Result::TYPE_SAT - && d_result->isSat() == CVC4::Result::SAT_UNKNOWN; + return d_result->getType() == CVC5::Result::TYPE_SAT + && d_result->isSat() == CVC5::Result::SAT_UNKNOWN; } bool Result::isEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == CVC4::Result::ENTAILED; + return d_result->getType() == CVC5::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC5::Result::ENTAILED; } bool Result::isNotEntailed(void) const { - return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED; + return d_result->getType() == CVC5::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC5::Result::NOT_ENTAILED; } bool Result::isEntailmentUnknown(void) const { - return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT - && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN; + return d_result->getType() == CVC5::Result::TYPE_ENTAILMENT + && d_result->isEntailed() == CVC5::Result::ENTAILMENT_UNKNOWN; } bool Result::operator==(const Result& r) const @@ -904,18 +904,18 @@ bool Result::operator!=(const Result& r) const Result::UnknownExplanation Result::getUnknownExplanation(void) const { - CVC4::Result::UnknownExplanation expl = d_result->whyUnknown(); + CVC5::Result::UnknownExplanation expl = d_result->whyUnknown(); switch (expl) { - case CVC4::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK; - case CVC4::Result::INCOMPLETE: return INCOMPLETE; - case CVC4::Result::TIMEOUT: return TIMEOUT; - case CVC4::Result::RESOURCEOUT: return RESOURCEOUT; - case CVC4::Result::MEMOUT: return MEMOUT; - case CVC4::Result::INTERRUPTED: return INTERRUPTED; - case CVC4::Result::NO_STATUS: return NO_STATUS; - case CVC4::Result::UNSUPPORTED: return UNSUPPORTED; - case CVC4::Result::OTHER: return OTHER; + case CVC5::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK; + case CVC5::Result::INCOMPLETE: return INCOMPLETE; + case CVC5::Result::TIMEOUT: return TIMEOUT; + case CVC5::Result::RESOURCEOUT: return RESOURCEOUT; + case CVC5::Result::MEMOUT: return MEMOUT; + case CVC5::Result::INTERRUPTED: return INTERRUPTED; + case CVC5::Result::NO_STATUS: return NO_STATUS; + case CVC5::Result::UNSUPPORTED: return UNSUPPORTED; + case CVC5::Result::OTHER: return OTHER; default: return UNKNOWN_REASON; } return UNKNOWN_REASON; @@ -952,12 +952,12 @@ std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e) /* Sort */ /* -------------------------------------------------------------------------- */ -Sort::Sort(const Solver* slv, const CVC4::TypeNode& t) - : d_solver(slv), d_type(new CVC4::TypeNode(t)) +Sort::Sort(const Solver* slv, const CVC5::TypeNode& t) + : d_solver(slv), d_type(new CVC5::TypeNode(t)) { } -Sort::Sort() : d_solver(nullptr), d_type(new CVC4::TypeNode()) {} +Sort::Sort() : d_solver(nullptr), d_type(new CVC5::TypeNode()) {} Sort::~Sort() { @@ -1332,7 +1332,7 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const CVC4_API_CHECK(isParametricDatatype() || isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; //////// all checks before this line - std::vector<CVC4::TypeNode> tparams = sortVectorToTypeNodes(params); + std::vector<CVC5::TypeNode> tparams = sortVectorToTypeNodes(params); if (d_type->isDatatype()) { return Sort(d_solver, d_type->instantiateParametricDatatype(tparams)); @@ -1368,7 +1368,7 @@ Sort Sort::substitute(const std::vector<Sort>& sorts, CVC4_API_CHECK_SORTS(replacements); //////// all checks before this line - std::vector<CVC4::TypeNode> tSorts = sortVectorToTypeNodes(sorts), + std::vector<CVC5::TypeNode> tSorts = sortVectorToTypeNodes(sorts), tReplacements = sortVectorToTypeNodes(replacements); return Sort(d_solver, @@ -1394,7 +1394,7 @@ std::string Sort::toString() const CVC4_API_TRY_CATCH_END; } -const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; } +const CVC5::TypeNode& Sort::getTypeNode(void) const { return *d_type; } /* Constructor sort ------------------------------------------------------- */ @@ -1757,15 +1757,15 @@ bool Sort::isNullHelper() const { return d_type->isNull(); } /* Op */ /* -------------------------------------------------------------------------- */ -Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {} +Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC5::Node()) {} Op::Op(const Solver* slv, const Kind k) - : d_solver(slv), d_kind(k), d_node(new CVC4::Node()) + : d_solver(slv), d_kind(k), d_node(new CVC5::Node()) { } -Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n) - : d_solver(slv), d_kind(k), d_node(new CVC4::Node(n)) +Op::Op(const Solver* slv, const Kind k, const CVC5::Node& n) + : d_solver(slv), d_kind(k), d_node(new CVC5::Node(n)) { } @@ -1914,53 +1914,53 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const // using if/else instead of case statement because want local variables if (k == BITVECTOR_EXTRACT) { - CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>(); + CVC5::BitVectorExtract ext = d_node->getConst<BitVectorExtract>(); indices = std::make_pair(ext.d_high, ext.d_low); } else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) { - CVC4::FloatingPointToFPIEEEBitVector ext = + CVC5::FloatingPointToFPIEEEBitVector ext = d_node->getConst<FloatingPointToFPIEEEBitVector>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) { - CVC4::FloatingPointToFPFloatingPoint ext = + CVC5::FloatingPointToFPFloatingPoint ext = d_node->getConst<FloatingPointToFPFloatingPoint>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_REAL) { - CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); + CVC5::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) { - CVC4::FloatingPointToFPSignedBitVector ext = + CVC5::FloatingPointToFPSignedBitVector ext = d_node->getConst<FloatingPointToFPSignedBitVector>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) { - CVC4::FloatingPointToFPUnsignedBitVector ext = + CVC5::FloatingPointToFPUnsignedBitVector ext = d_node->getConst<FloatingPointToFPUnsignedBitVector>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == FLOATINGPOINT_TO_FP_GENERIC) { - CVC4::FloatingPointToFPGeneric ext = + CVC5::FloatingPointToFPGeneric ext = d_node->getConst<FloatingPointToFPGeneric>(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } else if (k == REGEXP_LOOP) { - CVC4::RegExpLoop ext = d_node->getConst<RegExpLoop>(); + CVC5::RegExpLoop ext = d_node->getConst<RegExpLoop>(); indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc); } else @@ -2031,13 +2031,13 @@ bool Op::isIndexedHelper() const { return !d_node->isNull(); } /* Term */ /* -------------------------------------------------------------------------- */ -Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {} +Term::Term() : d_solver(nullptr), d_node(new CVC5::Node()) {} -Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv) +Term::Term(const Solver* slv, const CVC5::Node& n) : d_solver(slv) { // Ensure that we create the node in the correct node manager. NodeManagerScope scope(d_solver->getNodeManager()); - d_node.reset(new CVC4::Node(n)); + d_node.reset(new CVC5::Node(n)); } Term::~Term() @@ -2251,7 +2251,7 @@ Op Term::getOp() const { // it's an indexed operator // so we should return the indexed op - CVC4::Node op = d_node->getOperator(); + CVC5::Node op = d_node->getOperator(); return Op(d_solver, intToExtKind(d_node->getKind()), op); } // Notice this is the only case where getKindHelper is used, since the @@ -2276,7 +2276,7 @@ Term Term::getConstArrayBase() const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; // CONST_ARRAY kind maps to STORE_ALL internal kind - CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL) + CVC4_API_CHECK(d_node->getKind() == CVC5::Kind::STORE_ALL) << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()"; //////// all checks before this line return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue()); @@ -2288,7 +2288,7 @@ std::vector<Term> Term::getConstSequenceElements() const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE) + CVC4_API_CHECK(d_node->getKind() == CVC5::Kind::CONST_SEQUENCE) << "Expecting a CONST_SEQUENCE Term when calling " "getConstSequenceElements()"; //////// all checks before this line @@ -2414,7 +2414,7 @@ Term::const_iterator::const_iterator() } Term::const_iterator::const_iterator(const Solver* slv, - const std::shared_ptr<CVC4::Node>& n, + const std::shared_ptr<CVC5::Node>& n, uint32_t p) : d_solver(slv), d_origNode(n), d_pos(p) { @@ -2515,14 +2515,14 @@ Term::const_iterator Term::end() const return Term::const_iterator(d_solver, d_node, endpos); } -const CVC4::Node& Term::getNode(void) const { return *d_node; } +const CVC5::Node& Term::getNode(void) const { return *d_node; } namespace detail { -const Rational& getRational(const CVC4::Node& node) +const Rational& getRational(const CVC5::Node& node) { return node.getConst<Rational>(); } -Integer getInteger(const CVC4::Node& node) +Integer getInteger(const CVC5::Node& node) { return node.getConst<Rational>().getNumerator(); } @@ -2545,7 +2545,7 @@ bool checkReal64Bounds(const Rational& r) bool isInteger(const Node& node) { - return node.getKind() == CVC4::Kind::CONST_RATIONAL + return node.getKind() == CVC5::Kind::CONST_RATIONAL && node.getConst<Rational>().isIntegral(); } bool isInt32(const Node& node) @@ -2658,7 +2658,7 @@ bool Term::isString() const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; //////// all checks before this line - return d_node->getKind() == CVC4::Kind::CONST_STRING; + return d_node->getKind() == CVC5::Kind::CONST_STRING; //////// CVC4_API_TRY_CATCH_END; } @@ -2667,10 +2667,10 @@ std::wstring Term::getString() const { CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK_NOT_NULL; - CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_STRING) + CVC4_API_CHECK(d_node->getKind() == CVC5::Kind::CONST_STRING) << "Term should be a String when calling getString()"; //////// all checks before this line - return d_node->getConst<CVC4::String>().toWString(); + return d_node->getConst<CVC5::String>().toWString(); //////// CVC4_API_TRY_CATCH_END; } @@ -2754,18 +2754,18 @@ Kind Term::getKindHelper() const { switch (d_node->getKind()) { - case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; - case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; - case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT; - case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE; - case CVC4::Kind::STRING_CHARAT: return SEQ_AT; - case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS; - case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF; - case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE; - case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL; - case CVC4::Kind::STRING_REV: return SEQ_REV; - case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX; - case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX; + case CVC5::Kind::STRING_CONCAT: return SEQ_CONCAT; + case CVC5::Kind::STRING_LENGTH: return SEQ_LENGTH; + case CVC5::Kind::STRING_SUBSTR: return SEQ_EXTRACT; + case CVC5::Kind::STRING_UPDATE: return SEQ_UPDATE; + case CVC5::Kind::STRING_CHARAT: return SEQ_AT; + case CVC5::Kind::STRING_STRCTN: return SEQ_CONTAINS; + case CVC5::Kind::STRING_STRIDOF: return SEQ_INDEXOF; + case CVC5::Kind::STRING_STRREPL: return SEQ_REPLACE; + case CVC5::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL; + case CVC5::Kind::STRING_REV: return SEQ_REV; + case CVC5::Kind::STRING_PREFIX: return SEQ_PREFIX; + case CVC5::Kind::STRING_SUFFIX: return SEQ_SUFFIX; default: // fall through to conversion below break; @@ -2802,7 +2802,7 @@ DatatypeConstructorDecl::DatatypeConstructorDecl() DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv, const std::string& name) - : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name)) + : d_solver(slv), d_ctor(new CVC5::DTypeConstructor(name)) { } DatatypeConstructorDecl::~DatatypeConstructorDecl() @@ -2884,7 +2884,7 @@ DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {} DatatypeDecl::DatatypeDecl(const Solver* slv, const std::string& name, bool isCoDatatype) - : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype)) + : d_solver(slv), d_dtype(new CVC5::DType(name, isCoDatatype)) { } @@ -2893,7 +2893,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, const Sort& param, bool isCoDatatype) : d_solver(slv), - d_dtype(new CVC4::DType( + d_dtype(new CVC5::DType( name, std::vector<TypeNode>{*param.d_type}, isCoDatatype)) { } @@ -2905,8 +2905,8 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, : d_solver(slv) { std::vector<TypeNode> tparams = Sort::sortVectorToTypeNodes(params); - d_dtype = std::shared_ptr<CVC4::DType>( - new CVC4::DType(name, tparams, isCoDatatype)); + d_dtype = std::shared_ptr<CVC5::DType>( + new CVC5::DType(name, tparams, isCoDatatype)); } bool DatatypeDecl::isNullHelper() const { return !d_dtype; } @@ -2991,15 +2991,15 @@ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) return out; } -CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } +CVC5::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; } /* DatatypeSelector --------------------------------------------------------- */ DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {} DatatypeSelector::DatatypeSelector(const Solver* slv, - const CVC4::DTypeSelector& stor) - : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor)) + const CVC5::DTypeSelector& stor) + : d_solver(slv), d_stor(new CVC5::DTypeSelector(stor)) { CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector"; } @@ -3079,8 +3079,8 @@ DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr) } DatatypeConstructor::DatatypeConstructor(const Solver* slv, - const CVC4::DTypeConstructor& ctor) - : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor)) + const CVC5::DTypeConstructor& ctor) + : d_solver(slv), d_ctor(new CVC5::DTypeConstructor(ctor)) { CVC4_API_CHECK(d_ctor->isResolved()) << "Expected resolved datatype constructor"; @@ -3214,14 +3214,14 @@ DatatypeConstructor::const_iterator DatatypeConstructor::end() const } DatatypeConstructor::const_iterator::const_iterator( - const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin) + const Solver* slv, const CVC5::DTypeConstructor& ctor, bool begin) { d_solver = slv; d_int_stors = &ctor.getArgs(); - const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels = + const std::vector<std::shared_ptr<CVC5::DTypeSelector>>& sels = ctor.getArgs(); - for (const std::shared_ptr<CVC4::DTypeSelector>& s : sels) + for (const std::shared_ptr<CVC5::DTypeSelector>& s : sels) { /* Can not use emplace_back here since constructor is private. */ d_stors.push_back(DatatypeSelector(d_solver, *s.get())); @@ -3341,8 +3341,8 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) /* Datatype ----------------------------------------------------------------- */ -Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype) - : d_solver(slv), d_dtype(new CVC4::DType(dtype)) +Datatype::Datatype(const Solver* slv, const CVC5::DType& dtype) + : d_solver(slv), d_dtype(new CVC5::DType(dtype)) { CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype"; } @@ -3549,7 +3549,7 @@ DatatypeConstructor Datatype::getConstructorForName( } Datatype::const_iterator::const_iterator(const Solver* slv, - const CVC4::DType& dtype, + const CVC5::DType& dtype, bool begin) : d_solver(slv), d_int_ctors(&dtype.getConstructors()) { @@ -3816,7 +3816,7 @@ Sort Grammar::resolve() bvl = Term( d_solver, d_solver->getNodeManager()->mkNode( - CVC4::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars))); + CVC5::kind::BOUND_VAR_LIST, Term::termVectorToNodes(d_sygusVars))); } std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size()); @@ -3829,7 +3829,7 @@ Sort Grammar::resolve() Sort(d_solver, d_solver->getNodeManager()->mkSort(ntsymbol.toString())); } - std::vector<CVC4::DType> datatypes; + std::vector<CVC5::DType> datatypes; std::set<TypeNode> unresTypes; datatypes.reserve(d_ntSyms.size()); @@ -3903,12 +3903,12 @@ void Grammar::addSygusConstructorTerm( { Term lbvl = Term(d_solver, - d_solver->getNodeManager()->mkNode(CVC4::kind::BOUND_VAR_LIST, + d_solver->getNodeManager()->mkNode(CVC5::kind::BOUND_VAR_LIST, Term::termVectorToNodes(args))); // its operator is a lambda op = Term(d_solver, d_solver->getNodeManager()->mkNode( - CVC4::kind::LAMBDA, *lbvl.d_node, *op.d_node)); + CVC5::kind::LAMBDA, *lbvl.d_node, *op.d_node)); } std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs); dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst); @@ -4027,27 +4027,27 @@ std::ostream& operator<<(std::ostream& out, const Grammar& grammar) /* -------------------------------------------------------------------------- */ const static std:: - unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction> + unordered_map<RoundingMode, CVC5::RoundingMode, RoundingModeHashFunction> s_rmodes{ {ROUND_NEAREST_TIES_TO_EVEN, - CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, - {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE}, - {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_NEGATIVE}, - {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO}, + CVC5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, + {ROUND_TOWARD_POSITIVE, CVC5::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_NEGATIVE, CVC5::RoundingMode::ROUND_TOWARD_NEGATIVE}, + {ROUND_TOWARD_ZERO, CVC5::RoundingMode::ROUND_TOWARD_ZERO}, {ROUND_NEAREST_TIES_TO_AWAY, - CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, + CVC5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, }; -const static std::unordered_map<CVC4::RoundingMode, +const static std::unordered_map<CVC5::RoundingMode, RoundingMode, - CVC4::RoundingModeHashFunction> + CVC5::RoundingModeHashFunction> s_rmodes_internal{ - {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, + {CVC5::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, ROUND_NEAREST_TIES_TO_EVEN}, - {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, - {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE}, - {CVC4::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, - {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, + {CVC5::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, + {CVC5::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE}, + {CVC5::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, + {CVC5::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, ROUND_NEAREST_TIES_TO_AWAY}, }; @@ -4093,7 +4093,7 @@ void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const { #ifdef CVC4_STATISTICS_ON const TypeNode tn = sort.getTypeNode(); - TypeConstant tc = tn.getKind() == CVC4::kind::TYPE_CONSTANT + TypeConstant tc = tn.getKind() == CVC5::kind::TYPE_CONSTANT ? tn.getConst<TypeConstant>() : LAST_TYPE; if (is_var) @@ -4124,10 +4124,10 @@ Term Solver::mkRealFromStrHelper(const std::string& s) const //////// all checks before this line try { - CVC4::Rational r = s.find('/') != std::string::npos - ? CVC4::Rational(s) - : CVC4::Rational::fromDecimal(s); - return mkValHelper<CVC4::Rational>(r); + CVC5::Rational r = s.find('/') != std::string::npos + ? CVC5::Rational(s) + : CVC5::Rational::fromDecimal(s); + return mkValHelper<CVC5::Rational>(r); } catch (const std::invalid_argument& e) { @@ -4144,7 +4144,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const { CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0"; //////// all checks before this line - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + return mkValHelper<CVC5::BitVector>(CVC5::BitVector(size, val)); } Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const @@ -4153,7 +4153,7 @@ Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base) << "base 2, 10, or 16"; //////// all checks before this line - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base)); + return mkValHelper<CVC5::BitVector>(CVC5::BitVector(s, base)); } Term Solver::mkBVFromStrHelper(uint32_t size, @@ -4180,7 +4180,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size, << size << " too small to hold value " << s << ")"; } - return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val)); + return mkValHelper<CVC5::BitVector>(CVC5::BitVector(size, val)); } Term Solver::mkCharFromStrHelper(const std::string& s) const @@ -4195,7 +4195,7 @@ Term Solver::mkCharFromStrHelper(const std::string& s) const //////// all checks before this line std::vector<unsigned> cpts; cpts.push_back(val); - return mkValHelper<CVC4::String>(CVC4::String(cpts)); + return mkValHelper<CVC5::String>(CVC5::String(cpts)); } Term Solver::getValueHelper(const Term& term) const @@ -4230,14 +4230,14 @@ Term Solver::mkTermFromKind(Kind kind) const Node res; if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA) { - CVC4::Kind k = extToIntKind(kind); + CVC5::Kind k = extToIntKind(kind); Assert(isDefinedIntKind(k)); res = d_nodeMgr->mkNode(k, std::vector<Node>()); } else { Assert(kind == PI); - res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI); + res = d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC5::kind::PI); } (void)res.getType(true); /* kick off type checking */ increment_term_stats(kind); @@ -4250,7 +4250,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const //////// all checks before this line std::vector<Node> echildren = Term::termVectorToNodes(children); - CVC4::Kind k = extToIntKind(kind); + CVC5::Kind k = extToIntKind(kind); Node res; if (echildren.size() > 2) { @@ -4340,7 +4340,7 @@ Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const return mkTermHelper(op.d_kind, children); } - const CVC4::Kind int_kind = extToIntKind(op.d_kind); + const CVC5::Kind int_kind = extToIntKind(op.d_kind); std::vector<Node> echildren = Term::termVectorToNodes(children); NodeBuilder<> nb(int_kind); @@ -4360,14 +4360,14 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal( // double checks //////// all checks before this line - std::vector<CVC4::DType> datatypes; + std::vector<CVC5::DType> datatypes; for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) { datatypes.push_back(dtypedecls[i].getDatatype()); } std::set<TypeNode> utypes = Sort::sortSetToTypeNodes(unresolvedSorts); - std::vector<CVC4::TypeNode> dtypes = + std::vector<CVC5::TypeNode> dtypes = getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes); std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes); return retTypes; @@ -4439,7 +4439,7 @@ Term Solver::ensureTermSort(const Term& term, const Sort& sort) const res = Term(this, d_nodeMgr->mkNode(extToIntKind(DIVISION), *res.d_node, - d_nodeMgr->mkConst(CVC4::Rational(1)))); + d_nodeMgr->mkConst(CVC5::Rational(1)))); } Assert(res.getSort() == sort); return res; @@ -4507,7 +4507,7 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const { CVC4_API_KIND_CHECK(kind); Assert(isDefinedIntKind(extToIntKind(kind))); - const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind)); + const CVC5::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind)); CVC4_API_KIND_CHECK_EXPECTED( mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR, kind) @@ -4870,7 +4870,7 @@ Term Solver::mkPi() const CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC4::kind::PI); + d_nodeMgr->mkNullaryOperator(d_nodeMgr->realType(), CVC5::kind::PI); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// @@ -4896,7 +4896,7 @@ Term Solver::mkInteger(int64_t val) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term integer = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Term integer = mkValHelper<CVC5::Rational>(CVC5::Rational(val)); Assert(integer.getSort() == getIntegerSort()); return integer; //////// @@ -4924,7 +4924,7 @@ Term Solver::mkReal(int64_t val) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(val)); + Term rational = mkValHelper<CVC5::Rational>(CVC5::Rational(val)); return ensureRealSort(rational); //////// CVC4_API_TRY_CATCH_END; @@ -4935,7 +4935,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - Term rational = mkValHelper<CVC4::Rational>(CVC4::Rational(num, den)); + Term rational = mkValHelper<CVC5::Rational>(CVC5::Rational(num, den)); return ensureRealSort(rational); //////// CVC4_API_TRY_CATCH_END; @@ -4947,7 +4947,7 @@ Term Solver::mkRegexpEmpty() const CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Node>()); + d_nodeMgr->mkNode(CVC5::kind::REGEXP_EMPTY, std::vector<CVC5::Node>()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// @@ -4960,7 +4960,7 @@ Term Solver::mkRegexpSigma() const CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line Node res = - d_nodeMgr->mkNode(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Node>()); + d_nodeMgr->mkNode(CVC5::kind::REGEXP_SIGMA, std::vector<CVC5::Node>()); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// @@ -4976,7 +4976,7 @@ Term Solver::mkEmptySet(const Sort& sort) const CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort) << "set sort associated with this solver object"; //////// all checks before this line - return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*sort.d_type)); + return mkValHelper<CVC5::EmptySet>(CVC5::EmptySet(*sort.d_type)); //////// CVC4_API_TRY_CATCH_END; } @@ -4990,7 +4990,7 @@ Term Solver::mkEmptyBag(const Sort& sort) const CVC4_API_ARG_CHECK_EXPECTED(sort.isNull() || this == sort.d_solver, sort) << "bag sort associated with this solver object"; //////// all checks before this line - return mkValHelper<CVC4::EmptyBag>(CVC4::EmptyBag(*sort.d_type)); + return mkValHelper<CVC5::EmptyBag>(CVC5::EmptyBag(*sort.d_type)); //////// CVC4_API_TRY_CATCH_END; } @@ -5002,7 +5002,7 @@ Term Solver::mkSepNil(const Sort& sort) const CVC4_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line Node res = - getNodeManager()->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL); + getNodeManager()->mkNullaryOperator(*sort.d_type, CVC5::kind::SEP_NIL); (void)res.getType(true); /* kick off type checking */ return Term(this, res); //////// @@ -5014,7 +5014,7 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences)); + return mkValHelper<CVC5::String>(CVC5::String(s, useEscSequences)); //////// CVC4_API_TRY_CATCH_END; } @@ -5024,7 +5024,7 @@ Term Solver::mkString(const unsigned char c) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c))); + return mkValHelper<CVC5::String>(CVC5::String(std::string(1, c))); //////// CVC4_API_TRY_CATCH_END; } @@ -5034,7 +5034,7 @@ Term Solver::mkString(const std::vector<uint32_t>& s) const NodeManagerScope scope(getNodeManager()); CVC4_API_TRY_CATCH_BEGIN; //////// all checks before this line - return mkValHelper<CVC4::String>(CVC4::String(s)); + return mkValHelper<CVC5::String>(CVC5::String(s)); //////// CVC4_API_TRY_CATCH_END; } @@ -5070,7 +5070,7 @@ Term Solver::mkUniverseSet(const Sort& sort) const //////// all checks before this line Node res = getNodeManager()->mkNullaryOperator(*sort.d_type, - CVC4::kind::UNIVERSE_SET); + CVC5::kind::UNIVERSE_SET); // TODO(#2771): Reenable? // (void)res->getType(true); /* kick off type checking */ return Term(this, res); @@ -5128,8 +5128,8 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const // this is safe because the constant array stores its type n = n[0]; } - Term res = mkValHelper<CVC4::ArrayStoreAll>( - CVC4::ArrayStoreAll(*sort.d_type, n)); + Term res = + mkValHelper<CVC5::ArrayStoreAll>(CVC5::ArrayStoreAll(*sort.d_type, n)); return res; //////// CVC4_API_TRY_CATCH_END; @@ -5142,7 +5142,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), false)); //////// CVC4_API_TRY_CATCH_END; @@ -5155,7 +5155,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC5::FloatingPoint>( FloatingPoint::makeInf(FloatingPointSize(exp, sig), true)); //////// CVC4_API_TRY_CATCH_END; @@ -5168,7 +5168,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC5::FloatingPoint>( FloatingPoint::makeNaN(FloatingPointSize(exp, sig))); //////// CVC4_API_TRY_CATCH_END; @@ -5181,7 +5181,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), false)); //////// CVC4_API_TRY_CATCH_END; @@ -5194,7 +5194,7 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( + return mkValHelper<CVC5::FloatingPoint>( FloatingPoint::makeZero(FloatingPointSize(exp, sig), true)); //////// CVC4_API_TRY_CATCH_END; @@ -5207,7 +5207,7 @@ Term Solver::mkRoundingMode(RoundingMode rm) const CVC4_API_CHECK(Configuration::isBuiltWithSymFPU()) << "Expected CVC4 to be compiled with SymFPU support"; //////// all checks before this line - return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm)); + return mkValHelper<CVC5::RoundingMode>(s_rmodes.at(rm)); //////// CVC4_API_TRY_CATCH_END; } @@ -5218,8 +5218,8 @@ Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_SORT(sort); //////// all checks before this line - return mkValHelper<CVC4::UninterpretedConstant>( - CVC4::UninterpretedConstant(*sort.d_type, index)); + return mkValHelper<CVC5::UninterpretedConstant>( + CVC5::UninterpretedConstant(*sort.d_type, index)); //////// CVC4_API_TRY_CATCH_END; } @@ -5230,11 +5230,11 @@ Term Solver::mkAbstractValue(const std::string& index) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string"; - CVC4::Integer idx(index, 10); + CVC5::Integer idx(index, 10); CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index) << "a string representing an integer > 0"; //////// all checks before this line - return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(idx))); + return Term(this, getNodeManager()->mkConst(CVC5::AbstractValue(idx))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away //////// @@ -5248,7 +5248,7 @@ Term Solver::mkAbstractValue(uint64_t index) const CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0"; //////// all checks before this line return Term(this, - getNodeManager()->mkConst(CVC4::AbstractValue(Integer(index)))); + getNodeManager()->mkConst(CVC5::AbstractValue(Integer(index)))); // do not call getType(), for abstract values, type can not be computed // until it is substituted away //////// @@ -5271,8 +5271,8 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const val.getSort().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; //////// all checks before this line - return mkValHelper<CVC4::FloatingPoint>( - CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>())); + return mkValHelper<CVC5::FloatingPoint>( + CVC5::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>())); //////// CVC4_API_TRY_CATCH_END; } @@ -5461,7 +5461,7 @@ Term Solver::mkTerm(const Op& op) const return mkTermFromKind(op.d_kind); } - const CVC4::Kind int_kind = extToIntKind(op.d_kind); + const CVC5::Kind int_kind = extToIntKind(op.d_kind); Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node)); (void)res.d_node->getType(true); /* kick off type checking */ @@ -5534,7 +5534,7 @@ Term Solver::mkTuple(const std::vector<Sort>& sorts, CVC4_API_SOLVER_CHECK_SORTS(sorts); CVC4_API_SOLVER_CHECK_TERMS(terms); //////// all checks before this line - std::vector<CVC4::Node> args; + std::vector<CVC5::Node> args; for (size_t i = 0, size = sorts.size(); i < size; i++) { args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node); @@ -5580,7 +5580,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const { res = Op(this, kind, - *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_node); + *mkValHelper<CVC5::RecordUpdate>(CVC5::RecordUpdate(arg)).d_node); } else { @@ -5591,7 +5591,7 @@ Op Solver::mkOp(Kind kind, const std::string& arg) const << "a string representing an integer, real or rational value."; res = Op(this, kind, - *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg))) + *mkValHelper<CVC5::Divisible>(CVC5::Divisible(CVC5::Integer(arg))) .d_node); } return res; @@ -5610,76 +5610,76 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const case DIVISIBLE: res = Op(this, kind, - *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_node); + *mkValHelper<CVC5::Divisible>(CVC5::Divisible(arg)).d_node); break; case BITVECTOR_REPEAT: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg)) + *mkValHelper<CVC5::BitVectorRepeat>(CVC5::BitVectorRepeat(arg)) .d_node); break; case BITVECTOR_ZERO_EXTEND: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorZeroExtend>( - CVC4::BitVectorZeroExtend(arg)) + *mkValHelper<CVC5::BitVectorZeroExtend>( + CVC5::BitVectorZeroExtend(arg)) .d_node); break; case BITVECTOR_SIGN_EXTEND: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorSignExtend>( - CVC4::BitVectorSignExtend(arg)) + *mkValHelper<CVC5::BitVectorSignExtend>( + CVC5::BitVectorSignExtend(arg)) .d_node); break; case BITVECTOR_ROTATE_LEFT: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorRotateLeft>( - CVC4::BitVectorRotateLeft(arg)) + *mkValHelper<CVC5::BitVectorRotateLeft>( + CVC5::BitVectorRotateLeft(arg)) .d_node); break; case BITVECTOR_ROTATE_RIGHT: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorRotateRight>( - CVC4::BitVectorRotateRight(arg)) + *mkValHelper<CVC5::BitVectorRotateRight>( + CVC5::BitVectorRotateRight(arg)) .d_node); break; case INT_TO_BITVECTOR: res = Op( this, kind, - *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)).d_node); + *mkValHelper<CVC5::IntToBitVector>(CVC5::IntToBitVector(arg)).d_node); break; case IAND: res = - Op(this, kind, *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_node); + Op(this, kind, *mkValHelper<CVC5::IntAnd>(CVC5::IntAnd(arg)).d_node); break; case FLOATINGPOINT_TO_UBV: res = Op( this, kind, - *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg)) + *mkValHelper<CVC5::FloatingPointToUBV>(CVC5::FloatingPointToUBV(arg)) .d_node); break; case FLOATINGPOINT_TO_SBV: res = Op( this, kind, - *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) + *mkValHelper<CVC5::FloatingPointToSBV>(CVC5::FloatingPointToSBV(arg)) .d_node); break; case TUPLE_UPDATE: res = Op(this, kind, - *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_node); + *mkValHelper<CVC5::TupleUpdate>(CVC5::TupleUpdate(arg)).d_node); break; case REGEXP_REPEAT: res = Op(this, kind, - *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)).d_node); + *mkValHelper<CVC5::RegExpRepeat>(CVC5::RegExpRepeat(arg)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -5703,57 +5703,57 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const case BITVECTOR_EXTRACT: res = Op(this, kind, - *mkValHelper<CVC4::BitVectorExtract>( - CVC4::BitVectorExtract(arg1, arg2)) + *mkValHelper<CVC5::BitVectorExtract>( + CVC5::BitVectorExtract(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>( - CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPIEEEBitVector>( + CVC5::FloatingPointToFPIEEEBitVector(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_FLOATINGPOINT: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>( - CVC4::FloatingPointToFPFloatingPoint(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPFloatingPoint>( + CVC5::FloatingPointToFPFloatingPoint(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_REAL: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPReal>( - CVC4::FloatingPointToFPReal(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPReal>( + CVC5::FloatingPointToFPReal(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>( - CVC4::FloatingPointToFPSignedBitVector(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPSignedBitVector>( + CVC5::FloatingPointToFPSignedBitVector(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>( - CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPUnsignedBitVector>( + CVC5::FloatingPointToFPUnsignedBitVector(arg1, arg2)) .d_node); break; case FLOATINGPOINT_TO_FP_GENERIC: res = Op(this, kind, - *mkValHelper<CVC4::FloatingPointToFPGeneric>( - CVC4::FloatingPointToFPGeneric(arg1, arg2)) + *mkValHelper<CVC5::FloatingPointToFPGeneric>( + CVC5::FloatingPointToFPGeneric(arg1, arg2)) .d_node); break; case REGEXP_LOOP: res = Op( this, kind, - *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)).d_node); + *mkValHelper<CVC5::RegExpLoop>(CVC5::RegExpLoop(arg1, arg2)).d_node); break; default: CVC4_API_KIND_CHECK_EXPECTED(false, kind) @@ -5778,7 +5778,7 @@ Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const { res = Op(this, kind, - *mkValHelper<CVC4::TupleProjectOp>(CVC4::TupleProjectOp(args)) + *mkValHelper<CVC5::TupleProjectOp>(CVC5::TupleProjectOp(args)) .d_node); } break; @@ -5819,7 +5819,7 @@ Result Solver::checkEntailed(const Term& term) const "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM(term); //////// all checks before this line - CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node); + CVC5::Result r = d_smtEngine->checkEntailed(*term.d_node); return Result(r); //////// CVC4_API_TRY_CATCH_END; @@ -5869,7 +5869,7 @@ Result Solver::checkSat(void) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line - CVC4::Result r = d_smtEngine->checkSat(); + CVC5::Result r = d_smtEngine->checkSat(); return Result(r); //////// CVC4_API_TRY_CATCH_END; @@ -5888,7 +5888,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); //////// all checks before this line - CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node); + CVC5::Result r = d_smtEngine->checkSat(*assumption.d_node); return Result(r); //////// CVC4_API_TRY_CATCH_END; @@ -5912,7 +5912,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC4_API_SOLVER_CHECK_TERM(term); } std::vector<Node> eassumptions = Term::termVectorToNodes(assumptions); - CVC4::Result r = d_smtEngine->checkSat(eassumptions); + CVC5::Result r = d_smtEngine->checkSat(eassumptions); return Result(r); //////// CVC4_API_TRY_CATCH_END; @@ -6641,7 +6641,7 @@ void Solver::setLogic(const std::string& logic) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_CHECK(!d_smtEngine->isFullyInited()) << "Invalid call to 'setLogic', solver is already fully initialized"; - CVC4::LogicInfo logic_info(logic); + CVC5::LogicInfo logic_info(logic); //////// all checks before this line d_smtEngine->setLogic(logic_info); //////// @@ -6824,12 +6824,12 @@ Term Solver::getSynthSolution(Term term) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(term); - std::map<CVC4::Node, CVC4::Node> map; + std::map<CVC5::Node, CVC5::Node> map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; - std::map<CVC4::Node, CVC4::Node>::const_iterator it = map.find(*term.d_node); + std::map<CVC5::Node, CVC5::Node>::const_iterator it = map.find(*term.d_node); CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term"; //////// all checks before this line @@ -6845,7 +6845,7 @@ std::vector<Term> Solver::getSynthSolutions( CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector"; CVC4_API_SOLVER_CHECK_TERMS(terms); - std::map<CVC4::Node, CVC4::Node> map; + std::map<CVC5::Node, CVC5::Node> map; CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map)) << "The solver is not in a state immediately preceded by a " "successful call to checkSynth"; @@ -6856,7 +6856,7 @@ std::vector<Term> Solver::getSynthSolutions( for (size_t i = 0, n = terms.size(); i < n; ++i) { - std::map<CVC4::Node, CVC4::Node>::const_iterator it = + std::map<CVC5::Node, CVC5::Node>::const_iterator it = map.find(*terms[i].d_node); CVC4_API_CHECK(it != map.cend()) @@ -6893,4 +6893,4 @@ Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); } } // namespace api -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5a8f62983..8e5ddf28d 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -30,7 +30,7 @@ #include <unordered_set> #include <vector> -namespace CVC4 { +namespace CVC5 { template <bool ref_count> class NodeTemplate; @@ -201,14 +201,14 @@ class CVC4_EXPORT Result * @param r the internal result that is to be wrapped by this result * @return the Result */ - Result(const CVC4::Result& r); + Result(const CVC5::Result& r); /** * The interal result wrapped by this result. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::Result is * not ref counted. */ - std::shared_ptr<CVC4::Result> d_result; + std::shared_ptr<CVC5::Result> d_result; }; /** @@ -239,16 +239,16 @@ class Datatype; */ class CVC4_EXPORT Sort { - friend class CVC4::DatatypeDeclarationCommand; - friend class CVC4::DeclareFunctionCommand; - friend class CVC4::DeclareHeapCommand; - friend class CVC4::DeclareSortCommand; - friend class CVC4::DeclareSygusVarCommand; - friend class CVC4::DefineSortCommand; - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::GetModelCommand; - friend class CVC4::SynthFunCommand; + friend class CVC5::DatatypeDeclarationCommand; + friend class CVC5::DeclareFunctionCommand; + friend class CVC5::DeclareHeapCommand; + friend class CVC5::DeclareSortCommand; + friend class CVC5::DeclareSygusVarCommand; + friend class CVC5::DefineSortCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::GetModelCommand; + friend class CVC5::SynthFunCommand; friend class DatatypeConstructor; friend class DatatypeConstructorDecl; friend class DatatypeSelector; @@ -700,7 +700,7 @@ class CVC4_EXPORT Sort private: /** @return the internal wrapped TypeNode of this sort. */ - const CVC4::TypeNode& getTypeNode(void) const; + const CVC5::TypeNode& getTypeNode(void) const; /** Helper to convert a set of Sorts to internal TypeNodes. */ std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts); @@ -717,7 +717,7 @@ class CVC4_EXPORT Sort * @param t the internal type that is to be wrapped by this sort * @return the Sort */ - Sort(const Solver* slv, const CVC4::TypeNode& t); + Sort(const Solver* slv, const CVC5::TypeNode& t); /** * Helper for isNull checks. This prevents calling an API function with @@ -733,10 +733,10 @@ class CVC4_EXPORT Sort /** * The interal type wrapped by this sort. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Type is already ref counted, so this + * to memory allocation (CVC5::Type is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::TypeNode> d_type; + std::shared_ptr<CVC5::TypeNode> d_type; }; /** @@ -847,7 +847,7 @@ class CVC4_EXPORT Op * @param n the internal node that is to be wrapped by this term * @return the Term */ - Op(const Solver* slv, const Kind k, const CVC4::Node& n); + Op(const Solver* slv, const Kind k, const CVC5::Node& n); /** * Helper for isNull checks. This prevents calling an API function with @@ -874,10 +874,10 @@ class CVC4_EXPORT Op /** * The internal node wrapped by this operator. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Node is already ref counted, so this + * to memory allocation (CVC5::Node is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::Node> d_node; + std::shared_ptr<CVC5::Node> d_node; }; /* -------------------------------------------------------------------------- */ @@ -889,25 +889,25 @@ class CVC4_EXPORT Op */ class CVC4_EXPORT Term { - friend class CVC4::AssertCommand; - friend class CVC4::BlockModelValuesCommand; - friend class CVC4::CheckSatCommand; - friend class CVC4::CheckSatAssumingCommand; - friend class CVC4::DeclareSygusVarCommand; - friend class CVC4::DefineFunctionCommand; - friend class CVC4::DefineFunctionRecCommand; - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::GetModelCommand; - friend class CVC4::GetQuantifierEliminationCommand; - friend class CVC4::GetUnsatCoreCommand; - friend class CVC4::GetValueCommand; - friend class CVC4::SetUserAttributeCommand; - friend class CVC4::SimplifyCommand; - friend class CVC4::SygusConstraintCommand; - friend class CVC4::SygusInvConstraintCommand; - friend class CVC4::SynthFunCommand; - friend class CVC4::QueryCommand; + friend class CVC5::AssertCommand; + friend class CVC5::BlockModelValuesCommand; + friend class CVC5::CheckSatCommand; + friend class CVC5::CheckSatAssumingCommand; + friend class CVC5::DeclareSygusVarCommand; + friend class CVC5::DefineFunctionCommand; + friend class CVC5::DefineFunctionRecCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::GetModelCommand; + friend class CVC5::GetQuantifierEliminationCommand; + friend class CVC5::GetUnsatCoreCommand; + friend class CVC5::GetValueCommand; + friend class CVC5::SetUserAttributeCommand; + friend class CVC5::SimplifyCommand; + friend class CVC5::SygusConstraintCommand; + friend class CVC5::SygusInvConstraintCommand; + friend class CVC5::SynthFunCommand; + friend class CVC5::QueryCommand; friend class Datatype; friend class DatatypeConstructor; friend class DatatypeSelector; @@ -1116,7 +1116,7 @@ class CVC4_EXPORT Term * @param p the position of the iterator (e.g. which child it's on) */ const_iterator(const Solver* slv, - const std::shared_ptr<CVC4::Node>& e, + const std::shared_ptr<CVC5::Node>& e, uint32_t p); /** @@ -1169,7 +1169,7 @@ class CVC4_EXPORT Term */ const Solver* d_solver; /** The original node to be iterated over. */ - std::shared_ptr<CVC4::Node> d_origNode; + std::shared_ptr<CVC5::Node> d_origNode; /** Keeps track of the iteration position. */ uint32_t d_pos; }; @@ -1259,10 +1259,10 @@ class CVC4_EXPORT Term * @param n the internal node that is to be wrapped by this term * @return the Term */ - Term(const Solver* slv, const CVC4::Node& n); + Term(const Solver* slv, const CVC5::Node& n); /** @return the internal wrapped Node of this term. */ - const CVC4::Node& getNode(void) const; + const CVC5::Node& getNode(void) const; /** * Helper for isNull checks. This prevents calling an API function with @@ -1285,10 +1285,10 @@ class CVC4_EXPORT Term /** * The internal node wrapped by this term. * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due - * to memory allocation (CVC4::Node is already ref counted, so this + * to memory allocation (CVC5::Node is already ref counted, so this * could be a unique_ptr instead). */ - std::shared_ptr<CVC4::Node> d_node; + std::shared_ptr<CVC5::Node> d_node; }; /** @@ -1445,9 +1445,9 @@ class CVC4_EXPORT DatatypeConstructorDecl * The internal (intermediate) datatype constructor wrapped by this * datatype constructor declaration. * Note: This is a shared_ptr rather than a unique_ptr since - * CVC4::DTypeConstructor is not ref counted. + * CVC5::DTypeConstructor is not ref counted. */ - std::shared_ptr<CVC4::DTypeConstructor> d_ctor; + std::shared_ptr<CVC5::DTypeConstructor> d_ctor; }; class Solver; @@ -1534,7 +1534,7 @@ class CVC4_EXPORT DatatypeDecl bool isCoDatatype = false); /** @return the internal wrapped Dtype of this datatype declaration. */ - CVC4::DType& getDatatype(void) const; + CVC5::DType& getDatatype(void) const; /** * Helper for isNull checks. This prevents calling an API function with @@ -1550,10 +1550,10 @@ class CVC4_EXPORT DatatypeDecl /** * The internal (intermediate) datatype wrapped by this datatype * declaration. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DType> d_dtype; + std::shared_ptr<CVC5::DType> d_dtype; }; /** @@ -1604,7 +1604,7 @@ class CVC4_EXPORT DatatypeSelector * @param stor the internal datatype selector to be wrapped * @return the DatatypeSelector */ - DatatypeSelector(const Solver* slv, const CVC4::DTypeSelector& stor); + DatatypeSelector(const Solver* slv, const CVC5::DTypeSelector& stor); /** * Helper for isNull checks. This prevents calling an API function with @@ -1619,10 +1619,10 @@ class CVC4_EXPORT DatatypeSelector /** * The internal datatype selector wrapped by this datatype selector. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DTypeSelector> d_stor; + std::shared_ptr<CVC5::DTypeSelector> d_stor; }; /** @@ -1785,7 +1785,7 @@ class CVC4_EXPORT DatatypeConstructor * @param true if this is a begin() iterator */ const_iterator(const Solver* slv, - const CVC4::DTypeConstructor& ctor, + const CVC5::DTypeConstructor& ctor, bool begin); /** @@ -1823,7 +1823,7 @@ class CVC4_EXPORT DatatypeConstructor * @param ctor the internal datatype constructor to be wrapped * @return the DatatypeConstructor */ - DatatypeConstructor(const Solver* slv, const CVC4::DTypeConstructor& ctor); + DatatypeConstructor(const Solver* slv, const CVC5::DTypeConstructor& ctor); /** * Return selector for name. @@ -1845,10 +1845,10 @@ class CVC4_EXPORT DatatypeConstructor /** * The internal datatype constructor wrapped by this datatype constructor. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DTypeConstructor> d_ctor; + std::shared_ptr<CVC5::DTypeConstructor> d_ctor; }; /* @@ -2007,7 +2007,7 @@ class CVC4_EXPORT Datatype * @param dtype the internal datatype to iterate over * @param true if this is a begin() iterator */ - const_iterator(const Solver* slv, const CVC4::DType& dtype, bool begin); + const_iterator(const Solver* slv, const CVC5::DType& dtype, bool begin); /** * The associated solver object. @@ -2044,7 +2044,7 @@ class CVC4_EXPORT Datatype * @param dtype the internal datatype to be wrapped * @return the Datatype */ - Datatype(const Solver* slv, const CVC4::DType& dtype); + Datatype(const Solver* slv, const CVC5::DType& dtype); /** * Return constructor for name. @@ -2066,10 +2066,10 @@ class CVC4_EXPORT Datatype /** * The internal datatype wrapped by this datatype. - * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is + * Note: This is a shared_ptr rather than a unique_ptr since CVC5::DType is * not ref counted. */ - std::shared_ptr<CVC4::DType> d_dtype; + std::shared_ptr<CVC5::DType> d_dtype; }; /** @@ -2135,9 +2135,9 @@ std::ostream& operator<<(std::ostream& out, */ class CVC4_EXPORT Grammar { - friend class CVC4::GetAbductCommand; - friend class CVC4::GetInterpolCommand; - friend class CVC4::SynthFunCommand; + friend class CVC5::GetAbductCommand; + friend class CVC5::GetInterpolCommand; + friend class CVC5::SynthFunCommand; friend class Solver; public: @@ -3704,5 +3704,5 @@ class CVC4_EXPORT Solver }; } // namespace api -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index c98667da7..ef2f6af74 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -21,7 +21,7 @@ #include <ostream> -namespace CVC4 { +namespace CVC5 { namespace api { /* -------------------------------------------------------------------------- */ @@ -33,7 +33,7 @@ namespace api { * * Note that the underlying type of Kind must be signed (to enable range * checks for validity). The size of this type depends on the size of - * CVC4::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h). + * CVC5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h). */ enum CVC4_EXPORT Kind : int32_t { @@ -2868,6 +2868,6 @@ struct CVC4_EXPORT KindHashFunction }; } // namespace api -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 19e7eb092..9d69e2a15 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -19,7 +19,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4": pass -cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": +cdef extern from "api/cvc4cpp.h" namespace "CVC5::api": cdef cppclass Datatype: Datatype() except + DatatypeConstructor operator[](size_t idx) except + @@ -353,7 +353,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": size_t operator()(const Term & t) except + -cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode": +cdef extern from "api/cvc4cpp.h" namespace "CVC5::api::RoundingMode": cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, cdef RoundingMode ROUND_TOWARD_POSITIVE, cdef RoundingMode ROUND_TOWARD_NEGATIVE, diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in index 0f8ba4b45..46bf2b45e 100644 --- a/src/api/python/genkinds.py.in +++ b/src/api/python/genkinds.py.in @@ -40,13 +40,13 @@ PYCOMMENT = '#' CDEF_KIND = " cdef Kind " KINDS_PXD_TOP = \ -r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": +r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC5::api": cdef cppclass Kind: pass # Kind declarations: See cvc4cppkind.h for additional information -cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": +cdef extern from "api/cvc4cppkind.h" namespace "CVC5::api::Kind": """ KINDS_PXI_TOP = \ |