api: Remove Sort::isComparableTo(). (#7903)

Since we do not support arithmetic subtyping on the API level anymore,
this function is obsolete. Consequently, this now requires that
replacement terms as arguments to Term::substitute() are of the same
sort as the replaced terms.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index aa1f2eb6e6da599b4fd388387350d657bb7fb1fb..e2f645340c2f3d6c059445ea36ebb717a496afab 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1391,16 +1391,6 @@ bool Sort::isSubsortOf(const Sort& s) const
   CVC5_API_TRY_CATCH_END;
 }
 
-bool Sort::isComparableTo(const Sort& s) const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_ARG_CHECK_SOLVER("sort", s);
-  //////// all checks before this line
-  return d_type->isComparableTo(*s.d_type);
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 Datatype Sort::getDatatype() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -2483,8 +2473,8 @@ Term Term::substitute(const Term& term, const Term& replacement) const
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_TERM(term);
   CVC5_API_CHECK_TERM(replacement);
-  CVC5_API_CHECK(term.getSort().isComparableTo(replacement.getSort()))
-      << "Expecting terms of comparable sort in substitute";
+  CVC5_API_CHECK(term.getSort() == replacement.getSort())
+      << "Expecting terms of the same sort in substitute";
   //////// all checks before this line
   return Term(
       d_solver,
@@ -2500,7 +2490,7 @@ Term Term::substitute(const std::vector<Term>& terms,
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK(terms.size() == replacements.size())
       << "Expecting vectors of the same arity in substitute";
-  CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms, replacements);
+  CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms, replacements);
   //////// all checks before this line
   std::vector<Node> nodes = Term::termVectorToNodes(terms);
   std::vector<Node> nodeReplacements = Term::termVectorToNodes(replacements);

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 2ebbff313ff5b939665d5f1217babc496390d426..b3dc03250c2206bd1a49eec633cb800a3613c05a 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -573,13 +573,6 @@ class CVC5_EXPORT Sort
    */
   bool isSubsortOf(const Sort& s) const;
 
-  /**
-   * Is this sort comparable to the given sort (i.e., do they share
-   * a common ancestor in the subsort tree)?
-   * @return true if this sort is comparable to s
-   */
-  bool isComparableTo(const Sort& s) 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 71b17cef119a000e481121b92e03253d53e25cb6..5bd427e7e07eda20cfe9b40ecfcf269e51531247 100644 (file)
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -298,9 +298,9 @@ namespace api {
  * Term check for member functions of classes other than class Solver.
  * Check if each term in both the given container is not null, associated with
  * the solver object this object is associated with, and their sorts are
- * pairwise comparable to.
+ * pairwise equal.
  */
-#define CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_COMPARABLE_TO(terms1, terms2)  \
+#define CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms1, terms2)  \
   do                                                                        \
   {                                                                         \
     size_t i = 0;                                                           \
@@ -317,8 +317,8 @@ namespace api {
           this->d_solver == t2.d_solver, "term", terms2, i)                 \
           << "a term associated with the solver this object is associated " \
              "with";                                                        \
-      CVC5_API_CHECK(t1.getSort().isComparableTo(t2.getSort()))             \
-          << "Expecting terms of comparable sort at index " << i;           \
+      CVC5_API_CHECK(t1.getSort() == t2.getSort())                          \
+          << "Expecting terms of the same sort at index " << i;             \
       i += 1;                                                               \
     }                                                                       \
   } while (0)

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index d8c162c10279be2fbc59adc113e94d1dbcb16da9..326920a4e94835655e6347d55d828cbd5fc31437 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -415,18 +415,6 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
 
   private native boolean isSubsortOf(long pointer, long sortPointer);
 
-  /**
-   * Is this sort comparable to the given sort (i.e., do they share
-   * a common ancestor in the subsort tree)?
-   * @return true if this sort is comparable to s
-   */
-  public boolean isComparableTo(Sort s)
-  {
-    return isComparableTo(pointer, s.getPointer());
-  }
-
-  private native boolean isComparableTo(long pointer, long sortPointer);
-
   /**
    * @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 ea3a70bd421c47c26cb07efb331d52629882a98b..689b26e530578726eabebbe028e4ffcc4a5873be 100644 (file)
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -509,21 +509,6 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSubsortOf(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
 }
 
-/*
- * Class:     io_github_cvc5_api_Sort
- * Method:    isComparableTo
- * Signature: (JJ)Z
- */
-JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isComparableTo(
-    JNIEnv* env, jobject, jlong pointer, jlong sortPointer)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Sort* current = reinterpret_cast<Sort*>(pointer);
-  Sort* sort = reinterpret_cast<Sort*>(sortPointer);
-  return static_cast<jboolean>(current->isComparableTo(*sort));
-  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 226bd2645ec3b2a0cebaa741c1298f129615f740..e0e72638adbd3bf70140fcce0350df10478f58dd 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -348,7 +348,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isFirstClass() except +
         bint isFunctionLike() except +
         bint isSubsortOf(Sort s) except +
-        bint isComparableTo(Sort s) 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 e455c1872b986a8498c0eaf7180c7d85652c1177..2789e65948d77c610a1d9ed0a0c63054290fafe3 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2629,15 +2629,6 @@ cdef class Sort:
         """
         return self.csort.isSubsortOf(sort.csort)
 
-    def isComparableTo(self, Sort sort):
-        """
-            Is this sort comparable to the given sort
-            (i.e., do they share a common ancestor in the subsort tree)?
-
-            :return: True if this sort is comparable to s
-        """
-        return self.csort.isComparableTo(sort.csort)
-
     def getDatatype(self):
         """
             :return: the underlying datatype of a datatype sort

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8c6763e9242337b54671a283e260fbc06c9c6d10..9f847b70233cb9afc80b0818a02f377dca58e44f 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1005,7 +1005,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
     api::Term constVal = args[0];
 
-    if (!p.d_type.getArrayElementSort().isComparableTo(constVal.getSort()))
+    if (p.d_type.getArrayElementSort() != constVal.getSort())
     {
       std::stringstream ss;
       ss << "type mismatch inside array constant term:" << std::endl

diff --git a/test/regress/regress1/sygus/node-discrete.sy b/test/regress/regress1/sygus/node-discrete.sy
index a0ed0b5c21c2d8297e4c94b1c9ee06059d108511..35d00b0a51ea39bdabe2849610dbcf98a12f066c 100644 (file)
--- a/test/regress/regress1/sygus/node-discrete.sy
+++ b/test/regress/regress1/sygus/node-discrete.sy
@@ -76,7 +76,7 @@
 )
 
 (define-fun nilPState () PState
-  (mkPState nilSL ((as const (Array State Real)) 0))
+  (mkPState nilSL ((as const (Array State Real)) 0.0))
 )
 (define-fun-rec appendStateToPState ((s State) (r Real) (p PState)) PState
   (let ((pstates (states p)))

diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp
index 949c137cbbb3dba807e4ea85260b5a9771c7d5d1..b06e20fbfa929559dd41a9e0556bdecb9751beae 100644 (file)
--- a/test/unit/api/cpp/datatype_api_black.cpp
+++ b/test/unit/api/cpp/datatype_api_black.cpp
@@ -302,23 +302,6 @@ TEST_F(TestApiBlackDatatype, parametricDatatype)
   ASSERT_NE(pairIntInt, pairRealInt);
   ASSERT_NE(pairIntReal, pairRealInt);
 
-  ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal));
-  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal));
-  ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal));
-  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal));
-  ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt));
-  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt));
-  ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt));
-  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt));
-  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal));
-  ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal));
-  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal));
-  ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal));
-  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt));
-  ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt));
-  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt));
-  ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt));
-
   ASSERT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
   ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
   ASSERT_FALSE(pairRealInt.isSubsortOf(pairRealReal));

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 911a151e7595b57743a643221c74c154e8e1400d..4b2c2ae0b6e30ad620d0a54bf079d3c93933ca99 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -295,16 +295,6 @@ TEST_F(TestApiBlackSort, isSubsortOf)
   ASSERT_NO_THROW(Sort().isSubsortOf(Sort()));
 }
 
-TEST_F(TestApiBlackSort, isComparableTo)
-{
-  ASSERT_TRUE(
-      d_solver.getIntegerSort().isComparableTo(d_solver.getIntegerSort()));
-  ASSERT_TRUE(d_solver.getIntegerSort().isComparableTo(d_solver.getRealSort()));
-  ASSERT_FALSE(
-      d_solver.getIntegerSort().isComparableTo(d_solver.getBooleanSort()));
-  ASSERT_NO_THROW(Sort().isComparableTo(Sort()));
-}
-
 TEST_F(TestApiBlackSort, getDatatype)
 {
   Sort dtypeSort = create_datatype_sort();
@@ -596,21 +586,14 @@ TEST_F(TestApiBlackSort, sortSubtyping)
   Sort realSort = d_solver.getRealSort();
   ASSERT_TRUE(intSort.isSubsortOf(realSort));
   ASSERT_FALSE(realSort.isSubsortOf(intSort));
-  ASSERT_TRUE(intSort.isComparableTo(realSort));
-  ASSERT_TRUE(realSort.isComparableTo(intSort));
 
   Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
   Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
-  ASSERT_FALSE(arraySortII.isComparableTo(intSort));
-  // we do not support subtyping for arrays
-  ASSERT_FALSE(arraySortII.isComparableTo(arraySortIR));
 
   Sort setSortI = d_solver.mkSetSort(intSort);
   Sort setSortR = d_solver.mkSetSort(realSort);
   // we don't support subtyping for sets
-  ASSERT_FALSE(setSortI.isComparableTo(setSortR));
   ASSERT_FALSE(setSortI.isSubsortOf(setSortR));
-  ASSERT_FALSE(setSortR.isComparableTo(setSortI));
   ASSERT_FALSE(setSortR.isSubsortOf(setSortI));
 }
 

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index f1d51e15063962d7bbd6bf0c4606c18a0e14cdf6..0867ad6b5c8f1ffc3b6cc793c92df2821c3e6aa6 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -275,23 +275,6 @@ class DatatypeTest
     assertNotEquals(pairIntInt, pairRealInt);
     assertNotEquals(pairIntReal, pairRealInt);
 
-    assertTrue(pairRealReal.isComparableTo(pairRealReal));
-    assertFalse(pairIntReal.isComparableTo(pairRealReal));
-    assertFalse(pairRealInt.isComparableTo(pairRealReal));
-    assertFalse(pairIntInt.isComparableTo(pairRealReal));
-    assertFalse(pairRealReal.isComparableTo(pairRealInt));
-    assertFalse(pairIntReal.isComparableTo(pairRealInt));
-    assertTrue(pairRealInt.isComparableTo(pairRealInt));
-    assertFalse(pairIntInt.isComparableTo(pairRealInt));
-    assertFalse(pairRealReal.isComparableTo(pairIntReal));
-    assertTrue(pairIntReal.isComparableTo(pairIntReal));
-    assertFalse(pairRealInt.isComparableTo(pairIntReal));
-    assertFalse(pairIntInt.isComparableTo(pairIntReal));
-    assertFalse(pairRealReal.isComparableTo(pairIntInt));
-    assertFalse(pairIntReal.isComparableTo(pairIntInt));
-    assertFalse(pairRealInt.isComparableTo(pairIntInt));
-    assertTrue(pairIntInt.isComparableTo(pairIntInt));
-
     assertTrue(pairRealReal.isSubsortOf(pairRealReal));
     assertFalse(pairIntReal.isSubsortOf(pairRealReal));
     assertFalse(pairRealInt.isSubsortOf(pairRealReal));

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 511bb65345f321e8be9dae713d1e5e13db9f0b95..3022af024aedfb3c0986135b3af6577fb3bc1a57 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -284,14 +284,6 @@ class SortTest
     assertDoesNotThrow(() -> d_solver.getNullSort().isSubsortOf(d_solver.getNullSort()));
   }
 
-  @Test void isComparableTo()
-  {
-    assertTrue(d_solver.getIntegerSort().isComparableTo(d_solver.getIntegerSort()));
-    assertTrue(d_solver.getIntegerSort().isComparableTo(d_solver.getRealSort()));
-    assertFalse(d_solver.getIntegerSort().isComparableTo(d_solver.getBooleanSort()));
-    assertDoesNotThrow(() -> d_solver.getNullSort().isComparableTo(d_solver.getNullSort()));
-  }
-
   @Test void getDatatype() throws CVC5ApiException
   {
     Sort dtypeSort = create_datatype_sort();
@@ -581,21 +573,14 @@ class SortTest
     Sort realSort = d_solver.getRealSort();
     assertTrue(intSort.isSubsortOf(realSort));
     assertFalse(realSort.isSubsortOf(intSort));
-    assertTrue(intSort.isComparableTo(realSort));
-    assertTrue(realSort.isComparableTo(intSort));
 
     Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
     Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
-    assertFalse(arraySortII.isComparableTo(intSort));
-    // we do not support subtyping for arrays
-    assertFalse(arraySortII.isComparableTo(arraySortIR));
 
     Sort setSortI = d_solver.mkSetSort(intSort);
     Sort setSortR = d_solver.mkSetSort(realSort);
     // we don't support subtyping for sets
-    assertFalse(setSortI.isComparableTo(setSortR));
     assertFalse(setSortI.isSubsortOf(setSortR));
-    assertFalse(setSortR.isComparableTo(setSortI));
     assertFalse(setSortR.isSubsortOf(setSortI));
   }
 

diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py
index a818c512ea33d49669b61dae699d8311ac76170b..a9a82ce5fba9e29a420ced617bec51bacc374dc1 100644 (file)
--- a/test/unit/api/python/test_datatype_api.py
+++ b/test/unit/api/python/test_datatype_api.py
@@ -300,23 +300,6 @@ def test_parametric_datatype(solver):
     assert pairIntInt != pairRealInt
     assert pairIntReal != pairRealInt
 
-    assert pairRealReal.isComparableTo(pairRealReal)
-    assert not pairIntReal.isComparableTo(pairRealReal)
-    assert not pairRealInt.isComparableTo(pairRealReal)
-    assert not pairIntInt.isComparableTo(pairRealReal)
-    assert not pairRealReal.isComparableTo(pairRealInt)
-    assert not pairIntReal.isComparableTo(pairRealInt)
-    assert pairRealInt.isComparableTo(pairRealInt)
-    assert not pairIntInt.isComparableTo(pairRealInt)
-    assert not pairRealReal.isComparableTo(pairIntReal)
-    assert pairIntReal.isComparableTo(pairIntReal)
-    assert not pairRealInt.isComparableTo(pairIntReal)
-    assert not pairIntInt.isComparableTo(pairIntReal)
-    assert not pairRealReal.isComparableTo(pairIntInt)
-    assert not pairIntReal.isComparableTo(pairIntInt)
-    assert not pairRealInt.isComparableTo(pairIntInt)
-    assert pairIntInt.isComparableTo(pairIntInt)
-
     assert pairRealReal.isSubsortOf(pairRealReal)
     assert not pairIntReal.isSubsortOf(pairRealReal)
     assert not pairRealInt.isSubsortOf(pairRealReal)

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index a0a2cbea8693b55594c59466c7c790db03248721..a53a88c8ffc0b5e69e8f56533aa8025d7463db5d 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -264,13 +264,6 @@ def test_is_subsort_of(solver):
     Sort(solver).isSubsortOf(Sort(solver))
 
 
-def test_is_comparable_to(solver):
-    assert solver.getIntegerSort().isComparableTo(solver.getIntegerSort())
-    assert solver.getIntegerSort().isComparableTo(solver.getRealSort())
-    assert not solver.getIntegerSort().isComparableTo(solver.getBooleanSort())
-    Sort(solver).isComparableTo(Sort(solver))
-
-
 def test_get_datatype(solver):
     dtypeSort = create_datatype_sort(solver)
     dtypeSort.getDatatype()
@@ -565,21 +558,14 @@ def test_sort_subtyping(solver):
     realSort = solver.getRealSort()
     assert intSort.isSubsortOf(realSort)
     assert not realSort.isSubsortOf(intSort)
-    assert intSort.isComparableTo(realSort)
-    assert realSort.isComparableTo(intSort)
 
     arraySortII = solver.mkArraySort(intSort, intSort)
     arraySortIR = solver.mkArraySort(intSort, realSort)
-    assert not arraySortII.isComparableTo(intSort)
-    # we do not support subtyping for arrays
-    assert not arraySortII.isComparableTo(arraySortIR)
 
     setSortI = solver.mkSetSort(intSort)
     setSortR = solver.mkSetSort(realSort)
     # we don't support subtyping for sets
-    assert not setSortI.isComparableTo(setSortR)
     assert not setSortI.isSubsortOf(setSortR)
-    assert not setSortR.isComparableTo(setSortI)
     assert not setSortR.isSubsortOf(setSortI)