New C++ API: Remove TOTAL kinds. (#3794)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 7f8fc80970adb3921d4aacfa75851784822b193c..b16e5afc59644653e17cc2569b60047a55b62415 100644 (file)
--- 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 dcb05be17e07b63d6497c65387941dde4264bfdd..27c28cec6deec4fba8baa336758932713d5d7bab 100644 (file)
--- 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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<Term>& children)
-   */
-  INTS_MODULUS_TOTAL,
   /**
    * Absolute value.
    * Parameters: 1
@@ -777,26 +750,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& 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<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.
@@ -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
@@ -1457,23 +1404,6 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Op op, const std::vector<Term>& 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<Term>& 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<Term>& 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<Term>& 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 6fb7e839cba897bb4ae66725617e4fbb77efbbcf..4a66d76aa5a322fcb9e4fd033b5d5142d30dc9aa 100644 (file)
--- 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<uint32_t>();
   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<uint32_t>();
-  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<uint32_t>();
   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<uint32_t>();
-  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<uint32_t>();
   TS_ASSERT(tuple_update_idx == 5);