From: Andres Noetzli Date: Mon, 21 Mar 2022 23:27:40 +0000 (-0700) Subject: Remove `Op::getIndices()` (#8355) X-Git-Tag: cvc5-1.0.0~217 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0bfa39a9846284eed5bbf9a3caf72e3b817a192;p=cvc5.git Remove `Op::getIndices()` (#8355) This commit removes `Op::getIndices()`. As discussed offline, the semantics of that method were confusing and the use cases are covered by `Op::getNumIndices()` and `Op::operator[]()` (which mirror `Term::getNumChildren()` and `Term::operator[]()`). Future changes are going to update the Python and Java bindings to support `Op::operator[]()`. --- diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py index 3c93e407e..d653522b0 100644 --- a/examples/api/python/extract.py +++ b/examples/api/python/extract.py @@ -38,9 +38,6 @@ if __name__ == "__main__": ext_0_0 = slv.mkOp(Kind.BVExtract, 0, 0) x_0_0 = slv.mkTerm(ext_0_0, x) - # test getting indices - assert ext_30_0.getIndices() == (30, 0) - eq = slv.mkTerm(Kind.Equal, x_31_1, x_30_0) print("Asserting:", eq) slv.assertFormula(eq) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1b48b600d..37cdd5619 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -2063,163 +2063,6 @@ Term Op::getIndexHelper(size_t index) const CVC5_API_TRY_CATCH_END; } -template <> -std::string Op::getIndices() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(!d_node->isNull()) - << "Expecting a non-null internal expression. This Op is not indexed."; - Kind k = intToExtKind(d_node->getKind()); - CVC5_API_CHECK(k == DIVISIBLE) << "Can't get string index from" - << " kind " << kindToString(k); - //////// all checks before this line - return d_node->getConst().k.toString(); - //////// - CVC5_API_TRY_CATCH_END; -} - -template <> -uint32_t Op::getIndices() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(!d_node->isNull()) - << "Expecting a non-null internal expression. This Op is not indexed."; - //////// all checks before this line - - uint32_t i = 0; - Kind k = intToExtKind(d_node->getKind()); - switch (k) - { - case BITVECTOR_REPEAT: - i = d_node->getConst().d_repeatAmount; - break; - case BITVECTOR_ZERO_EXTEND: - i = d_node->getConst().d_zeroExtendAmount; - break; - case BITVECTOR_SIGN_EXTEND: - i = d_node->getConst().d_signExtendAmount; - break; - case BITVECTOR_ROTATE_LEFT: - i = d_node->getConst().d_rotateLeftAmount; - break; - case BITVECTOR_ROTATE_RIGHT: - i = d_node->getConst().d_rotateRightAmount; - break; - case INT_TO_BITVECTOR: i = d_node->getConst().d_size; break; - case IAND: i = d_node->getConst().d_size; break; - case FLOATINGPOINT_TO_UBV: - i = d_node->getConst().d_bv_size.d_size; - break; - case FLOATINGPOINT_TO_SBV: - i = d_node->getConst().d_bv_size.d_size; - break; - case REGEXP_REPEAT: - i = d_node->getConst().d_repeatAmount; - break; - default: - CVC5_API_CHECK(false) << "Can't get uint32_t index from" - << " kind " << kindToString(k); - } - return i; - //////// - CVC5_API_TRY_CATCH_END; -} - -template <> -std::pair Op::getIndices() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(!d_node->isNull()) - << "Expecting a non-null internal expression. This Op is not indexed."; - //////// all checks before this line - - std::pair indices; - Kind k = intToExtKind(d_node->getKind()); - - // using if/else instead of case statement because want local variables - if (k == BITVECTOR_EXTRACT) - { - cvc5::BitVectorExtract ext = d_node->getConst(); - indices = std::make_pair(ext.d_high, ext.d_low); - } - else if (k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV) - { - cvc5::FloatingPointToFPIEEEBitVector ext = - d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == FLOATINGPOINT_TO_FP_FROM_FP) - { - cvc5::FloatingPointToFPFloatingPoint ext = - d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == FLOATINGPOINT_TO_FP_FROM_REAL) - { - cvc5::FloatingPointToFPReal ext = d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == FLOATINGPOINT_TO_FP_FROM_SBV) - { - cvc5::FloatingPointToFPSignedBitVector ext = - d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == FLOATINGPOINT_TO_FP_FROM_UBV) - { - cvc5::FloatingPointToFPUnsignedBitVector ext = - d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == FLOATINGPOINT_TO_FP_GENERIC) - { - cvc5::FloatingPointToFPGeneric ext = - d_node->getConst(); - indices = std::make_pair(ext.getSize().exponentWidth(), - ext.getSize().significandWidth()); - } - else if (k == REGEXP_LOOP) - { - cvc5::RegExpLoop ext = d_node->getConst(); - indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc); - } - else - { - CVC5_API_CHECK(false) << "Can't get pair indices from" - << " kind " << kindToString(k); - } - return indices; - //////// - CVC5_API_TRY_CATCH_END; -} - -template <> -std::vector Op::getIndices() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(!d_node->isNull()) - << "Expecting a non-null internal expression. This Op is not indexed."; - size_t size = getNumIndicesHelper(); - std::vector terms(getNumIndices()); - for (size_t i = 0; i < size; i++) - { - terms[i] = getIndexHelper(i); - } - //////// all checks before this line - return terms; - //////// - CVC5_API_TRY_CATCH_END; -} - std::string Op::toString() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 7ea90c774..d0419bf1e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -879,22 +879,8 @@ class CVC5_EXPORT Op * @param i the position of the index to return * @return the index at position i */ - Term operator[](size_t i) const; - /** - * Get the indices used to create this Op. - * Supports the following template arguments: - * - string - * - Kind - * - uint32_t - * - pair - * Check the Op Kind with getKind() to determine which argument to use. - * @return the indices used to create this Op - */ - template - T getIndices() const; - /** * @return a string representation of this operator */ diff --git a/src/api/java/io/github/cvc5/api/Op.java b/src/api/java/io/github/cvc5/api/Op.java index 096fd559d..1263465e0 100644 --- a/src/api/java/io/github/cvc5/api/Op.java +++ b/src/api/java/io/github/cvc5/api/Op.java @@ -99,32 +99,6 @@ public class Op extends AbstractPointer private native int getNumIndices(long pointer); - /** - * Get the indices used to create this Op. - * Check the Op Kind with getKind() to determine which argument to use. - * - * @return the indices used to create this Op - */ - public int[] getIntegerIndices() - { - return getIntegerIndices(pointer); - } - - private native int[] getIntegerIndices(long pointer); - - /** - * Get the indices used to create this Op. - * Check the Op Kind with getKind() to determine which argument to use. - * - * @return the indices used to create this Op - */ - public String[] getStringIndices() - { - return getStringIndices(pointer); - } - - private native String[] getStringIndices(long pointer); - /** * @return a string representation of this operator */ diff --git a/src/api/java/jni/op.cpp b/src/api/java/jni/op.cpp index f34444001..83072e88c 100644 --- a/src/api/java/jni/op.cpp +++ b/src/api/java/jni/op.cpp @@ -109,79 +109,6 @@ JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Op_getNumIndices(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Op - * Method: getIntegerIndices - * Signature: (J)[I - */ -JNIEXPORT jintArray JNICALL Java_io_github_cvc5_api_Op_getIntegerIndices( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Op* current = reinterpret_cast(pointer); - size_t size = current->getNumIndices(); - std::vector indices(size); - if (size == 1) - { - uint32_t index = current->getIndices(); - indices[0] = index; - } - - if (size == 2) - { - std::pair pair = - current->getIndices>(); - indices[0] = pair.first; - indices[1] = pair.second; - } - - if (size > 2) - { - std::string message = "Unhandled case when number of indices > 2."; - throw CVC5ApiException(message); - } - - jintArray ret = env->NewIntArray((jsize)size); - env->SetIntArrayRegion(ret, 0, size, indices.data()); - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - -/* - * Class: io_github_cvc5_api_Op - * Method: getStringIndices - * Signature: (J)[Ljava/lang/String; - */ -JNIEXPORT jobjectArray JNICALL -Java_io_github_cvc5_api_Op_getStringIndices(JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Op* current = reinterpret_cast(pointer); - size_t size = current->getNumIndices(); - std::vector indices(size); - if (size == 1) - { - std::string cIndex = current->getIndices(); - jstring jIndex = env->NewStringUTF(cIndex.c_str()); - indices[0] = jIndex; - } - - if (size > 1) // currently only one string is implemented in cvc5.cpp - { - std::string message = "Unhandled case when number of indices > 1."; - throw CVC5ApiException(message); - } - - // construct a java array of String - jclass stringClass = env->FindClass("Ljava/lang/String;"); - jobjectArray ret = env->NewObjectArray((jsize)size, stringClass, nullptr); - for (size_t i = 0; i < size; i++) - { - env->SetObjectArrayElement(ret, i, indices[i]); - } - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} /* * Class: io_github_cvc5_api_Op diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 71ec13081..0251790e7 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -129,7 +129,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isNull() except + bint isIndexed() except + size_t getNumIndices() except + - T getIndices[T]() except + string toString() except + cdef cppclass OpHashFunction: diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index c8d552ea3..e861473cc 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -499,31 +499,6 @@ cdef class Op: """ return self.cop.getNumIndices() - def getIndices(self): - """ - :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() `). - """ - indices = None - try: - indices = self.cop.getIndices[string]().decode() - except: - pass - - try: - indices = self.cop.getIndices[uint32_t]() - except: - pass - - try: - indices = self.cop.getIndices[pair[uint32_t, uint32_t]]() - except: - pass - - if indices is None: - raise RuntimeError("Unable to retrieve indices from {}".format(self)) - - return indices - cdef class Grammar: """ A Sygus Grammar. diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index 81501763c..8792b5df1 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -140,136 +140,6 @@ TEST_F(TestApiBlackOp, subscriptOperator) ASSERT_EQ(4, regexp_loop[0].getUInt32Value()); } -TEST_F(TestApiBlackOp, getIndicesString) -{ - Op x; - ASSERT_THROW(x.getIndices(), CVC5ApiException); - - Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); - ASSERT_TRUE(divisible_ot.isIndexed()); - std::string divisible_idx = divisible_ot.getIndices(); - ASSERT_EQ(divisible_idx, "4"); -} - -TEST_F(TestApiBlackOp, getIndicesUint) -{ - Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); - ASSERT_TRUE(bitvector_repeat_ot.isIndexed()); - uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices(); - ASSERT_EQ(bitvector_repeat_idx, 5); - ASSERT_THROW( - (bitvector_repeat_ot.getIndices>()), - CVC5ApiException); - - Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); - uint32_t bitvector_zero_extend_idx = - bitvector_zero_extend_ot.getIndices(); - ASSERT_EQ(bitvector_zero_extend_idx, 6); - - Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); - uint32_t bitvector_sign_extend_idx = - bitvector_sign_extend_ot.getIndices(); - ASSERT_EQ(bitvector_sign_extend_idx, 7); - - Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); - uint32_t bitvector_rotate_left_idx = - bitvector_rotate_left_ot.getIndices(); - ASSERT_EQ(bitvector_rotate_left_idx, 8); - - Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); - uint32_t bitvector_rotate_right_idx = - bitvector_rotate_right_ot.getIndices(); - ASSERT_EQ(bitvector_rotate_right_idx, 9); - - Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10); - uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices(); - ASSERT_EQ(int_to_bitvector_idx, 10); - - Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); - uint32_t floatingpoint_to_ubv_idx = - floatingpoint_to_ubv_ot.getIndices(); - ASSERT_EQ(floatingpoint_to_ubv_idx, 11); - - Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); - uint32_t floatingpoint_to_sbv_idx = - floatingpoint_to_sbv_ot.getIndices(); - ASSERT_EQ(floatingpoint_to_sbv_idx, 13); -} - -TEST_F(TestApiBlackOp, getIndicesPairUint) -{ - Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); - ASSERT_TRUE(bitvector_extract_ot.isIndexed()); - std::pair bitvector_extract_indices = - bitvector_extract_ot.getIndices>(); - ASSERT_TRUE( - (bitvector_extract_indices == std::pair{4, 0})); - - Op floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25); - std::pair floatingpoint_to_fp_ieee_bitvector_indices = - floatingpoint_to_fp_ieee_bitvector_ot - .getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_ieee_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25); - std::pair floatingpoint_to_fp_floatingpoint_indices = - floatingpoint_to_fp_floatingpoint_ot - .getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_floatingpoint_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_real_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25); - std::pair floatingpoint_to_fp_real_indices = - floatingpoint_to_fp_real_ot.getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_real_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_signed_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25); - std::pair floatingpoint_to_fp_signed_bitvector_indices = - floatingpoint_to_fp_signed_bitvector_ot - .getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_signed_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25); - std::pair floatingpoint_to_fp_unsigned_bitvector_indices = - floatingpoint_to_fp_unsigned_bitvector_ot - .getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_unsigned_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_generic_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); - std::pair floatingpoint_to_fp_generic_indices = - floatingpoint_to_fp_generic_ot - .getIndices>(); - ASSERT_TRUE((floatingpoint_to_fp_generic_indices - == std::pair{4, 25})); - ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices(), - CVC5ApiException); -} - -TEST_F(TestApiBlackOp, getIndicesVector) -{ - std::vector indices = {0, 3, 2, 0, 1, 2}; - Op tuple_project_op = d_solver.mkOp(TUPLE_PROJECT, indices); - - ASSERT_TRUE(tuple_project_op.isIndexed()); - std::vector tuple_project_extract_indices = - tuple_project_op.getIndices>(); - ASSERT_THROW(tuple_project_op.getIndices(), CVC5ApiException); - for (size_t i = 0; i < indices.size(); i++) - { - ASSERT_EQ(indices[i], tuple_project_extract_indices[i].getUInt32Value()); - ASSERT_EQ(indices[i], tuple_project_op[i].getUInt32Value()); - } -} TEST_F(TestApiBlackOp, opScopingToString) { diff --git a/test/unit/api/cpp/op_white.cpp b/test/unit/api/cpp/op_white.cpp index 3483d409d..d8e7d6d19 100644 --- a/test/unit/api/cpp/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp @@ -29,7 +29,7 @@ TEST_F(TestApiWhiteOp, opFromKind) { Op plus(&d_solver, ADD); ASSERT_FALSE(plus.isIndexed()); - ASSERT_THROW(plus.getIndices(), CVC5ApiException); + ASSERT_EQ(0, plus.getNumIndices()); ASSERT_EQ(plus, d_solver.mkOp(ADD)); } } // namespace test diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 393f658c5..17a7aee9a 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -58,96 +58,6 @@ class OpTest assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT)); } - @Test void getIndicesString() throws CVC5ApiException - { - Op x = d_solver.getNullOp(); - assertThrows(CVC5ApiException.class, () -> x.getStringIndices()); - - Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); - assertTrue(divisible_ot.isIndexed()); - String divisible_idx = divisible_ot.getStringIndices()[0]; - assertEquals(divisible_idx, "4"); - } - - @Test void getIndicesUint() throws CVC5ApiException - { - Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); - assertTrue(bitvector_repeat_ot.isIndexed()); - int bitvector_repeat_idx = bitvector_repeat_ot.getIntegerIndices()[0]; - assertEquals(bitvector_repeat_idx, 5); - - // unlike bitvector_repeat_ot.getIndices>() in - // c++, this does not throw in Java - // assertThrows(CVC5ApiException.class, - // () -> bitvector_repeat_ot.getIntegerIndices()); - - Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); - int bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIntegerIndices()[0]; - assertEquals(bitvector_zero_extend_idx, 6); - - Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); - int bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIntegerIndices()[0]; - assertEquals(bitvector_sign_extend_idx, 7); - - Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); - int bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIntegerIndices()[0]; - assertEquals(bitvector_rotate_left_idx, 8); - - Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); - int bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIntegerIndices()[0]; - assertEquals(bitvector_rotate_right_idx, 9); - - Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10); - int int_to_bitvector_idx = int_to_bitvector_ot.getIntegerIndices()[0]; - assertEquals(int_to_bitvector_idx, 10); - - Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); - int floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIntegerIndices()[0]; - assertEquals(floatingpoint_to_ubv_idx, 11); - - Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); - int floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIntegerIndices()[0]; - assertEquals(floatingpoint_to_sbv_idx, 13); - } - - @Test void getIndicesPairUint() throws CVC5ApiException - { - Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); - assertTrue(bitvector_extract_ot.isIndexed()); - int[] bitvector_extract_indices = bitvector_extract_ot.getIntegerIndices(); - assertArrayEquals(bitvector_extract_indices, new int[] {4, 0}); - - Op floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25); - int[] floatingpoint_to_fp_ieee_bitvector_indices = - floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25}); - - Op floatingpoint_to_fp_floatingpoint_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25); - int[] floatingpoint_to_fp_floatingpoint_indices = - floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25}); - - Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25); - int[] floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25}); - - Op floatingpoint_to_fp_signed_bitvector_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25); - int[] floatingpoint_to_fp_signed_bitvector_indices = - floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25}); - - Op floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25); - int[] floatingpoint_to_fp_unsigned_bitvector_indices = - floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25}); - - Op floatingpoint_to_fp_generic_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); - int[] floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIntegerIndices(); - assertArrayEquals(floatingpoint_to_fp_generic_indices, new int[] {4, 25}); - assertThrows(CVC5ApiException.class, () -> floatingpoint_to_fp_generic_ot.getStringIndices()); - } @Test void opScopingToString() throws CVC5ApiException {