From acba737109e440f0b57494bc999dd80169ae64ea Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 10 Jan 2022 11:27:04 -0800 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 16 +++------------- src/api/cpp/cvc5.h | 7 ------- src/api/cpp/cvc5_checks.h | 8 ++++---- src/api/java/io/github/cvc5/api/Sort.java | 12 ------------ src/api/java/jni/sort.cpp | 15 --------------- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 9 --------- src/parser/smt2/smt2.cpp | 2 +- test/regress/regress1/sygus/node-discrete.sy | 2 +- test/unit/api/cpp/datatype_api_black.cpp | 17 ----------------- test/unit/api/cpp/sort_black.cpp | 17 ----------------- test/unit/api/java/DatatypeTest.java | 17 ----------------- test/unit/api/java/SortTest.java | 15 --------------- test/unit/api/python/test_datatype_api.py | 17 ----------------- test/unit/api/python/test_sort.py | 14 -------------- 15 files changed, 9 insertions(+), 160 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aa1f2eb6e..e2f645340 100644 --- 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& 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 nodes = Term::termVectorToNodes(terms); std::vector nodeReplacements = Term::termVectorToNodes(replacements); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 2ebbff313..b3dc03250 100644 --- 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 71b17cef1..5bd427e7e 100644 --- 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 d8c162c10..326920a4e 100644 --- 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 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 ea3a70bd4..689b26e53 100644 --- 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(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(pointer); - Sort* sort = reinterpret_cast(sortPointer); - return static_cast(current->isComparableTo(*sort)); - 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 226bd2645..e0e72638a 100644 --- 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 e455c1872..2789e6594 100644 --- 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 8c6763e92..9f847b702 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1005,7 +1005,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& 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 a0ed0b5c2..35d00b0a5 100644 --- 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 949c137cb..b06e20fbf 100644 --- 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 911a151e7..4b2c2ae0b 100644 --- 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 f1d51e150..0867ad6b5 100644 --- 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 511bb6534..3022af024 100644 --- 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 a818c512e..a9a82ce5f 100644 --- 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 a0a2cbea8..a53a88c8f 100644 --- 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) -- 2.30.2