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

4 files changed, 25 insertions, 25 deletions

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<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 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)