From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 28 Mar 2022 19:25:19 +0000 (-0700)
Subject: api: Remove left-over Sort::getUninterpretedSortName from header. (#8421)
X-Git-Tag: cvc5-1.0.0~151
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=615dd8b360b6c7e7c4486f57969b2adff19d4907;p=cvc5.git

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

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e2f3d943a..eb9976361 100644
--- 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 d14d2f4a1..9a9368fbc 100644
--- 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 0455f207a..2115c027a 100644
--- 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());