diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-02-21 14:20:15 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-21 14:20:15 -0800 |
commit | 641f14f02de0fb4f6a852fe53eb50b69f34101ee (patch) | |
tree | 8b03b6bb0b2dcc22becadb494e4ab7ab04384fb1 /src/api | |
parent | 18eb247c3f14761dc0e1981d4faf11833f069b9d (diff) |
New C++ API: Remove TOTAL kinds. (#3794)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 51 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 104 |
2 files changed, 11 insertions, 144 deletions
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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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, Kind, CVC4::kind::KindHashFunction> {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<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> /* 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<Kind, KindHashFunction> 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<FloatingPointToUBV>().bvs.size; break; - case FLOATINGPOINT_TO_UBV_TOTAL: - i = d_expr->getConst<FloatingPointToUBVTotal>().bvs.size; - break; case FLOATINGPOINT_TO_SBV: i = d_expr->getConst<FloatingPointToSBV>().bvs.size; break; - case FLOATINGPOINT_TO_SBV_TOTAL: - i = d_expr->getConst<FloatingPointToSBVTotal>().bvs.size; - break; case TUPLE_UPDATE: i = d_expr->getConst<TupleUpdate>().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>(CVC4::FloatingPointToUBV(arg)) .d_expr.get()); break; - case FLOATINGPOINT_TO_UBV_TOTAL: - res = Op(kind, - *mkValHelper<CVC4::FloatingPointToUBVTotal>( - CVC4::FloatingPointToUBVTotal(arg)) - .d_expr.get()); - break; case FLOATINGPOINT_TO_SBV: res = Op( kind, *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg)) .d_expr.get()); break; - case FLOATINGPOINT_TO_SBV_TOTAL: - res = Op(kind, - *mkValHelper<CVC4::FloatingPointToSBVTotal>( - 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 @@ -318,15 +318,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& children) - */ - DIVISION_TOTAL, - /** * Integer division, division by 0 undefined. * Parameters: 2 * -[1]..[2]: Terms of sort Integer @@ -336,15 +327,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& children) - */ - INTS_DIVISION_TOTAL, - /** * Integer modulus, division by 0 undefined. * Parameters: 2 * -[1]..[2]: Terms of sort Integer @@ -354,15 +336,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& children) - */ - INTS_MODULUS_TOTAL, - /** * Absolute value. * Parameters: 1 * -[1]: Term of sort Integer @@ -778,26 +751,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& 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<Term>& children) - */ - BITVECTOR_UREM_TOTAL, - /** * Bit-vector shift left. * The two bit-vector parameters must have same width. * Parameters: 2 @@ -1242,12 +1195,6 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& 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 @@ -1458,23 +1405,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& children) - */ - FLOATINGPOINT_TO_UBV_TOTAL, - /** * Operator for to_sbv. * Parameters: 1 * -[1]: Size of the bit-vector to convert to @@ -1491,23 +1421,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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<Term>& children) - */ - FLOATINGPOINT_TO_SBV_TOTAL, - /** * Floating-point to real. * Parameters: 1 * -[1]: Term of sort FloatingPoint @@ -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 ---------------------------------------------------------------- */ @@ -1597,15 +1502,6 @@ enum CVC4_PUBLIC Kind : int32_t */ 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 * -[1]: Tester term |