api: Remove Sort::isFirstClass(). (#8312)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d16dbfa5a7b216db7ce3a9e8ee2bfc9edea4c1bb..4f3a768a16af5fd172b9377459856fcdaf81d39f 100644 (file)
--- 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<Term> Solver::getValue(const std::vector<Term>& 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 037c149382f8dac99fc5a00403aa95b7bb5149b9..1138eafc8878d736018e932dd9a49ea5e1f14eb6 100644 (file)
--- 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 e0ab5cfb8eb17e430c434d42d0515766fff39156..ca54ef00708234831e884bbb422f8bdfd3265f3f 100644 (file)
--- 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 967f0ea1ec941a69db8752b0d94e57f33bada1c9..61afb909a5909b787c028a3afd4be4a3f1894d7a 100644 (file)
--- 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<Sort>
 
   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 a3570dc86216a764411dad7a8ec9904fdf47b46c..67e143c5c01408b0859862b63041bb4b5c43dbd9 100644 (file)
--- 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<jboolean>(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<Sort*>(pointer);
-  return static_cast<jboolean>(current->isFirstClass());
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
-}
-
 /*
  * Class:     io_github_cvc5_api_Sort
  * Method:    getDatatype

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 1e2c1c93e2dd2a24138b59c2ce500f58300fbe29..9350ca0bf77580dd2de578abc9e7ebea0cd96669 100644 (file)
--- 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 53b3f643dead0abce86ff135218573d8637d71c3..f682af8aac104c40352829f62faa6afd55decc43 100644 (file)
--- 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 a7192d78e9acec4de9cd6f81be162b93c08b39d2..bcf57ef2db6af6f18e2351488d5b2fc239976b31 100644 (file)
--- 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 37e62e5bd27c5e66a2a6f089e96a77e58c17cdc0..f1343366bbe5d41aa13040490edd5a716ea16168 100644 (file)
--- 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 1a71461b5b46c0ea3cc454c58b0991f0ce43e2ad..f552a3eb200bde2a7ea2aba7885776cb919f6bf8 100644 (file)
--- 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()