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

6 files changed, 40 insertions, 41 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<cvc5::FloatingPoint>(
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<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 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<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 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 = []