From 615dd8b360b6c7e7c4486f57969b2adff19d4907 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 28 Mar 2022 12:25:19 -0700 Subject: [PATCH] api: Remove left-over Sort::getUninterpretedSortName from header. (#8421) --- src/api/cpp/cvc5.h | 5 ----- test/unit/api/cpp/sort_black.cpp | 2 +- test/unit/api/java/SortTest.java | 2 +- 3 files changed, 2 insertions(+), 7 deletions(-) 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()); -- 2.30.2