From: Aina Niemetz Date: Fri, 21 Feb 2020 22:20:15 +0000 (-0800) Subject: New C++ API: Remove TOTAL kinds. (#3794) X-Git-Tag: cvc5-1.0.0~3621 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=641f14f02de0fb4f6a852fe53eb50b69f34101ee;p=cvc5.git New C++ API: Remove TOTAL kinds. (#3794) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7f8fc8097..b16e5afc5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -98,11 +98,8 @@ const static std::unordered_map s_kinds{ {MINUS, CVC4::Kind::MINUS}, {UMINUS, CVC4::Kind::UMINUS}, {DIVISION, CVC4::Kind::DIVISION}, - {DIVISION_TOTAL, CVC4::Kind::DIVISION_TOTAL}, {INTS_DIVISION, CVC4::Kind::INTS_DIVISION}, - {INTS_DIVISION_TOTAL, CVC4::Kind::INTS_DIVISION_TOTAL}, {INTS_MODULUS, CVC4::Kind::INTS_MODULUS}, - {INTS_MODULUS_TOTAL, CVC4::Kind::INTS_MODULUS_TOTAL}, {ABS, CVC4::Kind::ABS}, {DIVISIBLE, CVC4::Kind::DIVISIBLE}, {POW, CVC4::Kind::POW}, @@ -149,8 +146,6 @@ const static std::unordered_map s_kinds{ {BITVECTOR_SDIV, CVC4::Kind::BITVECTOR_SDIV}, {BITVECTOR_SREM, CVC4::Kind::BITVECTOR_SREM}, {BITVECTOR_SMOD, CVC4::Kind::BITVECTOR_SMOD}, - {BITVECTOR_UDIV_TOTAL, CVC4::Kind::BITVECTOR_UDIV_TOTAL}, - {BITVECTOR_UREM_TOTAL, CVC4::Kind::BITVECTOR_UREM_TOTAL}, {BITVECTOR_SHL, CVC4::Kind::BITVECTOR_SHL}, {BITVECTOR_LSHR, CVC4::Kind::BITVECTOR_LSHR}, {BITVECTOR_ASHR, CVC4::Kind::BITVECTOR_ASHR}, @@ -212,11 +207,8 @@ const static std::unordered_map s_kinds{ 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_UBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL}, {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV}, - {FLOATINGPOINT_TO_SBV_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL}, {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL}, - {FLOATINGPOINT_TO_REAL_TOTAL, CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL}, /* Arrays -------------------------------------------------------------- */ {SELECT, CVC4::Kind::SELECT}, {STORE, CVC4::Kind::STORE}, @@ -224,7 +216,6 @@ const static std::unordered_map s_kinds{ /* Datatypes ----------------------------------------------------------- */ {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR}, {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR}, - {APPLY_SELECTOR_TOTAL, CVC4::Kind::APPLY_SELECTOR_TOTAL}, {APPLY_TESTER, CVC4::Kind::APPLY_TESTER}, {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE}, {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE}, @@ -334,11 +325,11 @@ const static std::unordered_map {CVC4::Kind::MINUS, MINUS}, {CVC4::Kind::UMINUS, UMINUS}, {CVC4::Kind::DIVISION, DIVISION}, - {CVC4::Kind::DIVISION_TOTAL, DIVISION_TOTAL}, + {CVC4::Kind::DIVISION_TOTAL, INTERNAL_KIND}, {CVC4::Kind::INTS_DIVISION, INTS_DIVISION}, - {CVC4::Kind::INTS_DIVISION_TOTAL, INTS_DIVISION_TOTAL}, + {CVC4::Kind::INTS_DIVISION_TOTAL, INTERNAL_KIND}, {CVC4::Kind::INTS_MODULUS, INTS_MODULUS}, - {CVC4::Kind::INTS_MODULUS_TOTAL, INTS_MODULUS_TOTAL}, + {CVC4::Kind::INTS_MODULUS_TOTAL, INTERNAL_KIND}, {CVC4::Kind::ABS, ABS}, {CVC4::Kind::DIVISIBLE, DIVISIBLE}, {CVC4::Kind::POW, POW}, @@ -386,8 +377,8 @@ const static std::unordered_map {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV}, {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM}, {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD}, - {CVC4::Kind::BITVECTOR_UDIV_TOTAL, BITVECTOR_UDIV_TOTAL}, - {CVC4::Kind::BITVECTOR_UREM_TOTAL, BITVECTOR_UREM_TOTAL}, + {CVC4::Kind::BITVECTOR_UDIV_TOTAL, INTERNAL_KIND}, + {CVC4::Kind::BITVECTOR_UREM_TOTAL, INTERNAL_KIND}, {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL}, {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR}, {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR}, @@ -470,14 +461,14 @@ const static std::unordered_map {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, FLOATINGPOINT_TO_UBV_TOTAL}, - {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_UBV_TOTAL}, + {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, FLOATINGPOINT_TO_SBV_TOTAL}, - {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, FLOATINGPOINT_TO_SBV_TOTAL}, + {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, FLOATINGPOINT_TO_REAL_TOTAL}, + {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND}, /* Arrays ---------------------------------------------------------- */ {CVC4::Kind::SELECT, SELECT}, {CVC4::Kind::STORE, STORE}, @@ -485,7 +476,7 @@ const static std::unordered_map /* Datatypes ------------------------------------------------------- */ {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR}, {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR}, - {CVC4::Kind::APPLY_SELECTOR_TOTAL, APPLY_SELECTOR_TOTAL}, + {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}, @@ -573,9 +564,7 @@ const static std::unordered_set s_indexed_kinds( BITVECTOR_ROTATE_RIGHT, INT_TO_BITVECTOR, FLOATINGPOINT_TO_UBV, - FLOATINGPOINT_TO_UBV_TOTAL, FLOATINGPOINT_TO_SBV, - FLOATINGPOINT_TO_SBV_TOTAL, TUPLE_UPDATE, BITVECTOR_EXTRACT, FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, @@ -1172,15 +1161,9 @@ uint32_t Op::getIndices() const case FLOATINGPOINT_TO_UBV: i = d_expr->getConst().bvs.size; break; - case FLOATINGPOINT_TO_UBV_TOTAL: - i = d_expr->getConst().bvs.size; - break; case FLOATINGPOINT_TO_SBV: i = d_expr->getConst().bvs.size; break; - case FLOATINGPOINT_TO_SBV_TOTAL: - i = d_expr->getConst().bvs.size; - break; case TUPLE_UPDATE: i = d_expr->getConst().getIndex(); break; default: CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" @@ -3262,24 +3245,12 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const *mkValHelper(CVC4::FloatingPointToUBV(arg)) .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_TOTAL: - res = Op(kind, - *mkValHelper( - CVC4::FloatingPointToUBVTotal(arg)) - .d_expr.get()); - break; case FLOATINGPOINT_TO_SBV: res = Op( kind, *mkValHelper(CVC4::FloatingPointToSBV(arg)) .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_TOTAL: - res = Op(kind, - *mkValHelper( - CVC4::FloatingPointToSBVTotal(arg)) - .d_expr.get()); - break; case TUPLE_UPDATE: res = Op( kind, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index dcb05be17..27c28cec6 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -317,15 +317,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ DIVISION, - /** - * Real division with interpreted division by 0 - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer, Real - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector& children) - */ - DIVISION_TOTAL, /** * Integer division, division by 0 undefined. * Parameters: 2 @@ -335,15 +326,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ INTS_DIVISION, - /** - * Integer division with interpreted division by 0. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector& children) - */ - INTS_DIVISION_TOTAL, /** * Integer modulus, division by 0 undefined. * Parameters: 2 @@ -353,15 +335,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ INTS_MODULUS, - /** - * Integer modulus with interpreted division by 0. - * Parameters: 2 - * -[1]..[2]: Terms of sort Integer - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector& children) - */ - INTS_MODULUS_TOTAL, /** * Absolute value. * Parameters: 1 @@ -777,26 +750,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ BITVECTOR_SMOD, - /** - * Unsigned division of two bit-vectors, truncating towards 0 - * (defined to be the all-ones bit pattern, if divisor is 0). - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector& children) - */ - BITVECTOR_UDIV_TOTAL, - /** - * Unsigned remainder from truncating division of two bit-vectors - * (defined to be equal to the dividend, if divisor is 0). - * Parameters: 2 - * -[1]..[2]: Terms of bit-vector sort (sorts must match) - * Create with: - * mkTerm(Kind kind, Term child1, Term child2) - * mkTerm(Kind kind, const std::vector& children) - */ - BITVECTOR_UREM_TOTAL, /** * Bit-vector shift left. * The two bit-vector parameters must have same width. @@ -1242,12 +1195,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ FLOATINGPOINT_MAX, -#if 0 - /* floating-point minimum (defined for all inputs) */ - FLOATINGPOINT_MIN_TOTAL, - /* floating-point maximum (defined for all inputs) */ - FLOATINGPOINT_MAX_TOTAL, -#endif /** * Floating-point less than or equal. * Parameters: 2 @@ -1457,23 +1404,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_UBV, - /** - * Operator for to_ubv_total. - * Parameters: 1 - * -[1]: Size of the bit-vector to convert to - * Create with: - * mkOp(Kind kind, uint32_t param) - * - * Conversion from a floating-point value to an unsigned bit vector - * (defined for all inputs). - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_UBV_TOTAL - * -[2]: Term of sort FloatingPoint - * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector& children) - */ - FLOATINGPOINT_TO_UBV_TOTAL, /** * Operator for to_sbv. * Parameters: 1 @@ -1490,23 +1420,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Op op, const std::vector& children) */ FLOATINGPOINT_TO_SBV, - /** - * Operator for to_sbv_total. - * Parameters: 1 - * -[1]: Size of the bit-vector to convert to - * Create with: - * mkOp(Kind kind, uint32_t param) - * - * Conversion from a floating-point value to a signed bit vector - * (defined for all inputs). - * Parameters: 2 - * -[1]: Op of kind FLOATINGPOINT_TO_FP_TO_SBV_TOTAL - * -[2]: Term of sort FloatingPoint - * Create with: - * mkTerm(Op op, Term child) - * mkTerm(Op op, const std::vector& children) - */ - FLOATINGPOINT_TO_SBV_TOTAL, /** * Floating-point to real. * Parameters: 1 @@ -1515,14 +1428,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Term child) */ FLOATINGPOINT_TO_REAL, - /** - * Floating-point to real (defined for all inputs). - * Parameters: 1 - * -[1]: Term of sort FloatingPoint - * Create with: - * mkTerm(Kind kind, Term child) - */ - FLOATINGPOINT_TO_REAL_TOTAL, /* Arrays ---------------------------------------------------------------- */ @@ -1596,15 +1501,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, Op op, Term child) */ APPLY_SELECTOR, - /** - * Datatype selector application. - * Parameters: 1 - * -[1]: Selector (operator) - * -[2]: Datatype term (defined rigidly if mis-applied) - * Create with: - * mkTerm(Kind kind, Op op, Term child) - */ - APPLY_SELECTOR_TOTAL, /** * Datatype tester application. * Parameters: 2 diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h index 6fb7e839c..4a66d76aa 100644 --- a/test/unit/api/op_black.h +++ b/test/unit/api/op_black.h @@ -126,23 +126,11 @@ void OpBlack::testGetIndicesUint() floatingpoint_to_ubv_ot.getIndices(); TS_ASSERT(floatingpoint_to_ubv_idx == 11); - Op floatingpoint_to_ubv_total_ot = - d_solver.mkOp(FLOATINGPOINT_TO_UBV_TOTAL, 12); - uint32_t floatingpoint_to_ubv_total_idx = - floatingpoint_to_ubv_total_ot.getIndices(); - TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); - Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); uint32_t floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices(); TS_ASSERT(floatingpoint_to_sbv_idx == 13); - Op floatingpoint_to_sbv_total_ot = - d_solver.mkOp(FLOATINGPOINT_TO_SBV_TOTAL, 14); - uint32_t floatingpoint_to_sbv_total_idx = - floatingpoint_to_sbv_total_ot.getIndices(); - TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); - Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); uint32_t tuple_update_idx = tuple_update_ot.getIndices(); TS_ASSERT(tuple_update_idx == 5);