From: Aina Niemetz Date: Tue, 15 Mar 2022 22:51:42 +0000 (-0700) Subject: api: Remove Sort::isFirstClass(). (#8312) X-Git-Tag: cvc5-1.0.0~249 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8ef445fe7b026e8bee8d76a7ad40cfcf1072517;p=cvc5.git api: Remove Sort::isFirstClass(). (#8312) --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d16dbfa5a..4f3a768a1 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1346,15 +1346,6 @@ bool Sort::isSortConstructor() const CVC5_API_TRY_CATCH_END; } -bool Sort::isFirstClass() const -{ - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - return d_type->isFirstClass(); - //////// - CVC5_API_TRY_CATCH_END; -} - Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; @@ -7255,7 +7246,7 @@ Term Solver::getValue(const Term& term) const CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Cannot get value unless after a SAT or UNKNOWN response."; CVC5_API_SOLVER_CHECK_TERM(term); - CVC5_API_RECOVERABLE_CHECK(term.getSort().isFirstClass()) + CVC5_API_RECOVERABLE_CHECK(term.getSort().getTypeNode().isFirstClass()) << "Cannot get value of a term that is not first class."; CVC5_API_RECOVERABLE_CHECK(!term.getSort().isDatatype() || term.getSort().getDatatype().isWellFounded()) @@ -7277,7 +7268,7 @@ std::vector Solver::getValue(const std::vector& terms) const << "Cannot get value unless after a SAT or UNKNOWN response."; for (const Term& t : terms) { - CVC5_API_RECOVERABLE_CHECK(t.getSort().isFirstClass()) + CVC5_API_RECOVERABLE_CHECK(t.getSort().getTypeNode().isFirstClass()) << "Cannot get value of a term that is not first class."; CVC5_API_RECOVERABLE_CHECK(!t.getSort().isDatatype() || t.getSort().getDatatype().isWellFounded()) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 037c14938..1138eafc8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -522,20 +522,6 @@ class CVC5_EXPORT Sort */ bool isSortConstructor() const; - /** - * Is this a first-class sort? - * First-class sorts are sorts for which: - * 1. we handle equalities between terms of that type, and - * 2. they are allowed to be parameters of parametric sorts (e.g. index or - * element sorts of arrays). - * - * Examples of sorts that are not first-class include sort constructor sorts - * and regular expression sorts. - * - * @return true if this is a first-class sort - */ - bool isFirstClass() const; - /** * @return the underlying datatype of a datatype sort */ diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index e0ab5cfb8..ca54ef007 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -226,7 +226,7 @@ namespace api { this->d_solver == s.d_solver, "sort", sorts, i) \ << "a sort associated with the solver this object is associated " \ "with"; \ - CVC5_API_ARG_CHECK_EXPECTED(s.isFirstClass(), s) \ + CVC5_API_ARG_CHECK_EXPECTED(s.getTypeNode().isFirstClass(), s) \ << "first-class sort as domain sort"; \ i += 1; \ } \ diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 967f0ea1e..61afb909a 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -366,25 +366,6 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isSortConstructor(long pointer); - /** - * Is this a first-class sort? - * First-class sorts are sorts for which: - * (1) we handle equalities between terms of that type, and - * (2) they are allowed to be parameters of parametric sorts (e.g. index or - * element sorts of arrays). - * - * Examples of sorts that are not first-class include sort constructor sorts - * and regular expression sorts. - * - * @return true if this is a first-class sort - */ - public boolean isFirstClass() - { - return isFirstClass(pointer); - } - - private native boolean isFirstClass(long pointer); - /** * @return the underlying datatype of a datatype sort */ diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index a3570dc86..67e143c5c 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -466,20 +466,6 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSortConstructor( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } -/* - * Class: io_github_cvc5_api_Sort - * Method: isFirstClass - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Sort_isFirstClass(JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return static_cast(current->isFirstClass()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - /* * Class: io_github_cvc5_api_Sort * Method: getDatatype diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 1e2c1c93e..9350ca0bf 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -346,7 +346,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isSequence() except + bint isUninterpretedSort() except + bint isSortConstructor() except + - bint isFirstClass() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 53b3f643d..f682af8aa 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2645,22 +2645,6 @@ cdef class Sort: """ return self.csort.isSortConstructor() - def isFirstClass(self): - """ - Is this a first-class sort? - First-class sorts are sorts for which: - - 1. we handle equalities between terms of that type, and - 2. they are allowed to be parameters of parametric sorts - (e.g. index or element sorts of arrays). - - Examples of sorts that are not first-class include sort constructor - sorts and regular expression sorts. - - :return: True if the sort is a first-class sort. - """ - return self.csort.isFirstClass() - def getDatatype(self): """ :return: the underlying datatype of a datatype sort diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index a7192d78e..bcf57ef2d 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -260,17 +260,6 @@ TEST_F(TestApiBlackSort, isSortConstructor) ASSERT_NO_THROW(Sort().isSortConstructor()); } -TEST_F(TestApiBlackSort, isFirstClass) -{ - Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), - d_solver.getIntegerSort()); - ASSERT_TRUE(d_solver.getIntegerSort().isFirstClass()); - ASSERT_TRUE(fun_sort.isFirstClass()); - Sort reSort = d_solver.getRegExpSort(); - ASSERT_FALSE(reSort.isFirstClass()); - ASSERT_NO_THROW(Sort().isFirstClass()); -} - TEST_F(TestApiBlackSort, getDatatype) { Sort dtypeSort = create_datatype_sort(); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 37e62e5bd..f1343366b 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -252,16 +252,6 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isSortConstructor()); } - @Test void isFirstClass() - { - Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort()); - assertTrue(d_solver.getIntegerSort().isFirstClass()); - assertTrue(fun_sort.isFirstClass()); - Sort reSort = d_solver.getRegExpSort(); - assertFalse(reSort.isFirstClass()); - assertDoesNotThrow(() -> d_solver.getNullSort().isFirstClass()); - } - @Test void getDatatype() throws CVC5ApiException { Sort dtypeSort = create_datatype_sort(); diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 1a71461b5..f552a3eb2 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -233,16 +233,6 @@ def test_is_sort_constructor(solver): Sort(solver).isSortConstructor() -def test_is_first_class(solver): - fun_sort = solver.mkFunctionSort(solver.getRealSort(), - solver.getIntegerSort()) - assert solver.getIntegerSort().isFirstClass() - assert fun_sort.isFirstClass() - reSort = solver.getRegExpSort() - assert not reSort.isFirstClass() - Sort(solver).isFirstClass() - - def test_get_datatype(solver): dtypeSort = create_datatype_sort(solver) dtypeSort.getDatatype()