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)
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<Divisible>().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<BitVectorRepeat>().d_repeatAmount;
- break;
- case BITVECTOR_ZERO_EXTEND:
- i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
- break;
- case BITVECTOR_SIGN_EXTEND:
- i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount;
- break;
- case BITVECTOR_ROTATE_LEFT:
- i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
- break;
- case BITVECTOR_ROTATE_RIGHT:
- i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount;
- break;
- case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
- case IAND: i = d_node->getConst<IntAnd>().d_size; break;
- case FLOATINGPOINT_TO_UBV:
- i = d_node->getConst<FloatingPointToUBV>().d_bv_size.d_size;
- break;
- case FLOATINGPOINT_TO_SBV:
- i = d_node->getConst<FloatingPointToSBV>().d_bv_size.d_size;
- break;
- case REGEXP_REPEAT:
- i = d_node->getConst<RegExpRepeat>().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<uint32_t, 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
-
- std::pair<uint32_t, uint32_t> 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<BitVectorExtract>();
- 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<FloatingPointToFPIEEEBitVector>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == FLOATINGPOINT_TO_FP_FROM_FP)
- {
- cvc5::FloatingPointToFPFloatingPoint ext =
- d_node->getConst<FloatingPointToFPFloatingPoint>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == FLOATINGPOINT_TO_FP_FROM_REAL)
- {
- cvc5::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == FLOATINGPOINT_TO_FP_FROM_SBV)
- {
- cvc5::FloatingPointToFPSignedBitVector ext =
- d_node->getConst<FloatingPointToFPSignedBitVector>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == FLOATINGPOINT_TO_FP_FROM_UBV)
- {
- cvc5::FloatingPointToFPUnsignedBitVector ext =
- d_node->getConst<FloatingPointToFPUnsignedBitVector>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == FLOATINGPOINT_TO_FP_GENERIC)
- {
- cvc5::FloatingPointToFPGeneric ext =
- d_node->getConst<FloatingPointToFPGeneric>();
- indices = std::make_pair(ext.getSize().exponentWidth(),
- ext.getSize().significandWidth());
- }
- else if (k == REGEXP_LOOP)
- {
- cvc5::RegExpLoop ext = d_node->getConst<RegExpLoop>();
- indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc);
- }
- else
- {
- CVC5_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
- << " kind " << kindToString(k);
- }
- return indices;
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-template <>
-std::vector<api::Term> 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<Term> 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;
* @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<uint32_t, uint32_t>
- * Check the Op Kind with getKind() to determine which argument to use.
- * @return the indices used to create this Op
- */
- template <typename T>
- T getIndices() const;
-
/**
* @return a string representation of this operator
*/
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
*/
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<Op*>(pointer);
- size_t size = current->getNumIndices();
- std::vector<jint> indices(size);
- if (size == 1)
- {
- uint32_t index = current->getIndices<uint32_t>();
- indices[0] = index;
- }
-
- if (size == 2)
- {
- std::pair<uint32_t, uint32_t> pair =
- current->getIndices<std::pair<uint32_t, uint32_t>>();
- 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<Op*>(pointer);
- size_t size = current->getNumIndices();
- std::vector<jstring> indices(size);
- if (size == 1)
- {
- std::string cIndex = current->getIndices<std::string>();
- 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
bint isNull() except +
bint isIndexed() except +
size_t getNumIndices() except +
- T getIndices[T]() except +
string toString() except +
cdef cppclass OpHashFunction:
"""
return self.cop.getNumIndices()
- def getIndices(self):
- """
- :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::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.
ASSERT_EQ(4, regexp_loop[0].getUInt32Value());
}
-TEST_F(TestApiBlackOp, getIndicesString)
-{
- Op x;
- ASSERT_THROW(x.getIndices<std::string>(), CVC5ApiException);
-
- Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
- ASSERT_TRUE(divisible_ot.isIndexed());
- std::string divisible_idx = divisible_ot.getIndices<std::string>();
- 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<uint32_t>();
- ASSERT_EQ(bitvector_repeat_idx, 5);
- ASSERT_THROW(
- (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
- CVC5ApiException);
-
- Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
- uint32_t bitvector_zero_extend_idx =
- bitvector_zero_extend_ot.getIndices<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t>();
- 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<uint32_t, uint32_t> bitvector_extract_indices =
- bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE(
- (bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
-
- Op floatingpoint_to_fp_ieee_bitvector_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
- floatingpoint_to_fp_ieee_bitvector_ot
- .getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_ieee_bitvector_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
-
- Op floatingpoint_to_fp_floatingpoint_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
- floatingpoint_to_fp_floatingpoint_ot
- .getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_floatingpoint_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
-
- Op floatingpoint_to_fp_real_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
- floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_real_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
-
- Op floatingpoint_to_fp_signed_bitvector_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
- floatingpoint_to_fp_signed_bitvector_ot
- .getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_signed_bitvector_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
-
- Op floatingpoint_to_fp_unsigned_bitvector_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
- floatingpoint_to_fp_unsigned_bitvector_ot
- .getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_unsigned_bitvector_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
-
- Op floatingpoint_to_fp_generic_ot =
- d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
- std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
- floatingpoint_to_fp_generic_ot
- .getIndices<std::pair<uint32_t, uint32_t>>();
- ASSERT_TRUE((floatingpoint_to_fp_generic_indices
- == std::pair<uint32_t, uint32_t>{4, 25}));
- ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
- CVC5ApiException);
-}
-
-TEST_F(TestApiBlackOp, getIndicesVector)
-{
- std::vector<uint32_t> 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<Term> tuple_project_extract_indices =
- tuple_project_op.getIndices<std::vector<Term>>();
- ASSERT_THROW(tuple_project_op.getIndices<std::string>(), 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)
{
{
Op plus(&d_solver, ADD);
ASSERT_FALSE(plus.isIndexed());
- ASSERT_THROW(plus.getIndices<uint32_t>(), CVC5ApiException);
+ ASSERT_EQ(0, plus.getNumIndices());
ASSERT_EQ(plus, d_solver.mkOp(ADD));
}
} // namespace test
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<std::pair<uint32_t, uint32_t>>() 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
{
projects / cvc5.git / commitdiff