From 68fc65dfb303d75eab953523744103ba2b65ac8e Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 20 Oct 2021 12:14:59 -0700 Subject: [PATCH] api: Rename get(BV|FP)*Size functions for consistency. (#7428) --- src/api/cpp/cvc5.cpp | 11 ++++++----- src/api/cpp/cvc5.h | 6 +++--- src/api/java/cvc5/Sort.java | 18 ++++++++--------- src/api/java/jni/cvc5_Sort.cpp | 28 +++++++++++++-------------- src/api/python/cvc5.pxd | 6 +++--- src/api/python/cvc5.pxi | 12 ++++++------ test/api/issue6111.cpp | 2 +- test/python/unit/api/test_sort.py | 12 ++++++------ test/unit/api/java/cvc5/SortTest.java | 18 ++++++++--------- test/unit/api/sort_black.cpp | 18 ++++++++--------- 10 files changed, 65 insertions(+), 66 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 778f700c0..f6a1eed17 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1682,7 +1682,7 @@ size_t Sort::getSortConstructorArity() const /* Bit-vector sort ----------------------------------------------------- */ -uint32_t Sort::getBVSize() const +uint32_t Sort::getBitVectorSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1695,7 +1695,7 @@ uint32_t Sort::getBVSize() const /* Floating-point sort ------------------------------------------------- */ -uint32_t Sort::getFPExponentSize() const +uint32_t Sort::getFloatingPointExponentSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -1706,7 +1706,7 @@ uint32_t Sort::getFPExponentSize() const CVC5_API_TRY_CATCH_END; } -uint32_t Sort::getFPSignificandSize() const +uint32_t Sort::getFloatingPointSignificandSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; @@ -6030,10 +6030,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0"; CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0"; uint32_t bw = exp + sig; - CVC5_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val) + CVC5_API_ARG_CHECK_EXPECTED(bw == val.d_node->getType().getBitVectorSize(), + val) << "a bit-vector constant with bit-width '" << bw << "'"; CVC5_API_ARG_CHECK_EXPECTED( - val.getSort().isBitVector() && val.d_node->isConst(), val) + val.d_node->getType().isBitVector() && val.d_node->isConst(), val) << "bit-vector constant"; //////// all checks before this line return mkValHelper( diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5e0f0d834..ded477a9d 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -700,19 +700,19 @@ class CVC5_EXPORT Sort /** * @return the bit-width of the bit-vector sort */ - uint32_t getBVSize() const; + uint32_t getBitVectorSize() const; /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - uint32_t getFPExponentSize() const; + uint32_t getFloatingPointExponentSize() const; /** * @return the width of the significand of the floating-point sort */ - uint32_t getFPSignificandSize() const; + uint32_t getFloatingPointSignificandSize() const; /* Datatype sort ------------------------------------------------------- */ diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java index f1f541e35..434c07424 100644 --- a/src/api/java/cvc5/Sort.java +++ b/src/api/java/cvc5/Sort.java @@ -725,34 +725,34 @@ public class Sort extends AbstractPointer implements Comparable /** * @return the bit-width of the bit-vector sort */ - public int getBVSize() + public int getBitVectorSize() { - return getBVSize(pointer); + return getBitVectorSize(pointer); } - private native int getBVSize(long pointer); + private native int getBitVectorSize(long pointer); /* Floating-point sort ------------------------------------------------- */ /** * @return the bit-width of the exponent of the floating-point sort */ - public int getFPExponentSize() + public int getFloatingPointExponentSize() { - return getFPExponentSize(pointer); + return getFloatingPointExponentSize(pointer); } - private native int getFPExponentSize(long pointer); + private native int getFloatingPointExponentSize(long pointer); /** * @return the width of the significand of the floating-point sort */ - public int getFPSignificandSize() + public int getFloatingPointSignificandSize() { - return getFPSignificandSize(pointer); + return getFloatingPointSignificandSize(pointer); } - private native int getFPSignificandSize(long pointer); + private native int getFloatingPointSignificandSize(long pointer); /* Datatype sort ------------------------------------------------------- */ diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp index a2754f032..36ba81249 100644 --- a/src/api/java/jni/cvc5_Sort.cpp +++ b/src/api/java/jni/cvc5_Sort.cpp @@ -978,46 +978,44 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env, /* * Class: cvc5_Sort - * Method: getBVSize + * Method: getBitVectorSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getBVSize()); + return static_cast(current->getBitVectorSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPExponentSize + * Method: getFloatingPointExponentSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL +Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getFPExponentSize()); + return static_cast(current->getFloatingPointExponentSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: cvc5_Sort - * Method: getFPSignificandSize + * Method: getFloatingPointSignificandSize * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getFPSignificandSize()); + return static_cast(current->getFloatingPointSignificandSize()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ef9971c20..08bcc956a 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -357,9 +357,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": vector[Sort] getUninterpretedSortParamSorts() except + string getSortConstructorName() except + size_t getSortConstructorArity() except + - uint32_t getBVSize() except + - uint32_t getFPExponentSize() except + - uint32_t getFPSignificandSize() except + + uint32_t getBitVectorSize() except + + uint32_t getFloatingPointExponentSize() except + + uint32_t getFloatingPointSignificandSize() except + vector[Sort] getDatatypeParamSorts() except + size_t getDatatypeArity() except + size_t getTupleLength() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2a35363ea..6b6d391e6 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2396,14 +2396,14 @@ cdef class Sort: def getSortConstructorArity(self): return self.csort.getSortConstructorArity() - def getBVSize(self): - return self.csort.getBVSize() + def getBitVectorSize(self): + return self.csort.getBitVectorSize() - def getFPExponentSize(self): - return self.csort.getFPExponentSize() + def getFloatingPointExponentSize(self): + return self.csort.getFloatingPointExponentSize() - def getFPSignificandSize(self): - return self.csort.getFPSignificandSize() + def getFloatingPointSignificandSize(self): + return self.csort.getFloatingPointSignificandSize() def getDatatypeParamSorts(self): param_sorts = [] diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp index bd7be2ad0..c0366ce23 100644 --- a/test/api/issue6111.cpp +++ b/test/api/issue6111.cpp @@ -27,7 +27,7 @@ int main() solver.setLogic("QF_BV"); Sort bvsort12979 = solver.mkBitVectorSort(12979); Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); - Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + Term zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10); vector args1; args1.push_back(zero); diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py index def539cf4..db8cbff25 100644 --- a/test/python/unit/api/test_sort.py +++ b/test/python/unit/api/test_sort.py @@ -438,26 +438,26 @@ def test_get_uninterpreted_sort_constructor_arity(solver): def test_get_bv_size(solver): bvSort = solver.mkBitVectorSort(32) - bvSort.getBVSize() + bvSort.getBitVectorSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getBVSize() + setSort.getBitVectorSize() def test_get_fp_exponent_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPExponentSize() + fpSort.getFloatingPointExponentSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPExponentSize() + setSort.getFloatingPointExponentSize() def test_get_fp_significand_size(solver): fpSort = solver.mkFloatingPointSort(4, 8) - fpSort.getFPSignificandSize() + fpSort.getFloatingPointSignificandSize() setSort = solver.mkSetSort(solver.getIntegerSort()) with pytest.raises(RuntimeError): - setSort.getFPSignificandSize() + setSort.getFloatingPointSignificandSize() def test_get_datatype_paramsorts(solver): diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java index f2f9edaed..1ea703268 100644 --- a/test/unit/api/java/cvc5/SortTest.java +++ b/test/unit/api/java/cvc5/SortTest.java @@ -458,28 +458,28 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity()); } - @Test void getBVSize() throws CVC5ApiException + @Test void getBitVectorSize() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); - assertDoesNotThrow(() -> bvSort.getBVSize()); + assertDoesNotThrow(() -> bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getBVSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize()); } - @Test void getFPExponentSize() throws CVC5ApiException + @Test void getFloatingPointExponentSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPExponentSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize()); } - @Test void getFPSignificandSize() throws CVC5ApiException + @Test void getFloatingPointSignificandSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - assertDoesNotThrow(() -> fpSort.getFPSignificandSize()); + assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize()); + assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } @Test void getDatatypeParamSorts() throws CVC5ApiException diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index 757bacad6..1e9505ee1 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -470,28 +470,28 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getBVSize) +TEST_F(TestApiBlackSort, getBitVectorSize) { Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_NO_THROW(bvSort.getBVSize()); + ASSERT_NO_THROW(bvSort.getBitVectorSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getBVSize(), CVC5ApiException); + ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPExponentSize) +TEST_F(TestApiBlackSort, getFloatingPointExponentSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPExponentSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getFPSignificandSize) +TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - ASSERT_NO_THROW(fpSort.getFPSignificandSize()); + ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize()); Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException); + ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); } TEST_F(TestApiBlackSort, getDatatypeParamSorts) -- 2.30.2