api: Rename get(BV|FP)*Size functions for consistency. (#7428)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 778f700c04d3578841501d079f3f2e393812f759..f6a1eed17406b24570902daa8cddfd1902510afc 100644 (file)
--- 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<cvc5::FloatingPoint>(

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 5e0f0d83450bdc72a340108271b3719bc866ac46..ded477a9d191e899553f8b0fb83252e476cab5dc 100644 (file)
--- 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 f1f541e35506799de9116096541912a66e2a2511..434c074243c77e8a74f882aaca47a532c8cadd68 100644 (file)
--- 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<Sort>
   /**
    * @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 a2754f0320d2d3b5eb5517b3dcacdb8684da0f5f..36ba81249597ec63448ab0dbdb2767fadc060938 100644 (file)
--- 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<Sort*>(pointer);
-  return static_cast<jint>(current->getBVSize());
+  return static_cast<jint>(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<Sort*>(pointer);
-  return static_cast<jint>(current->getFPExponentSize());
+  return static_cast<jint>(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<Sort*>(pointer);
-  return static_cast<jint>(current->getFPSignificandSize());
+  return static_cast<jint>(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 ef9971c20f94299797484af1b87f36107f5e8ffd..08bcc956a135802b2a4609afb615e9c13d60ed5c 100644 (file)
--- 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 2a35363ea19703e5d1ad66d7d88d4b5261d1a76e..6b6d391e6e62d1fa8c61c74580b90b85a915302f 100644 (file)
--- 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 bd7be2ad08bfb00b269e4941a16a36496c35bb2b..c0366ce23a0677f993b4cfdcc31c0febefa5fadb 100644 (file)
--- 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<Term> args1;
   args1.push_back(zero);

diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py
index def539cf439f78e9facf7a69419061b093352902..db8cbff25771575bf57c633ad9fbfa8678a4c60c 100644 (file)
--- 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 f2f9edaed694449a0abd60b06eee5675c023cde7..1ea703268cf2186acc7e9760346b2838974aae34 100644 (file)
--- 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 757bacad630e12425b3ac6c7557416fd0a0f5837..1e9505ee18b4b6438f17b2b50bb83d71428f82f7 100644 (file)
--- 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)