api: Remove left-over Sort::getUninterpretedSortName from header. (#8421)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e2f3d943a9869803dc3960e3ae10e79028cf7ba5..eb99763619638864670103ccc681d50d713cc0cc 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -742,11 +742,6 @@ class CVC5_EXPORT Sort
 
   /* Uninterpreted sort -------------------------------------------------- */
 
-  /**
-   * @return the name of an uninterpreted sort
-   */
-  std::string getUninterpretedSortName() const;
-
   /**
    * @return true if an uninterpreted sort is parameterized
    */

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index d14d2f4a1ef1df77c8869ec2b592d110bfafe93d..9a9368fbc9a5b744a1c0b9cdba40d28db71e43c2 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -398,7 +398,7 @@ TEST_F(TestApiBlackSort, getSequenceElementSort)
   ASSERT_THROW(bvSort.getSequenceElementSort(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSort, getUninterpretedSortName)
+TEST_F(TestApiBlackSort, getSymbol)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
   ASSERT_NO_THROW(uSort.getSymbol());

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 0455f207ab1d533dfc196ce04ae95e815d9656ab..2115c027a961a4063abf56c6a86d9e2712f0ebf0 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -388,7 +388,7 @@ class SortTest
     assertThrows(CVC5ApiException.class, () -> bvSort.getSequenceElementSort());
   }
 
-  @Test void getUninterpretedSortName() throws CVC5ApiException
+  @Test void getSymbol() throws CVC5ApiException
   {
     Sort uSort = d_solver.mkUninterpretedSort("u");
     assertDoesNotThrow(() -> uSort.getSymbol());