From a94548b57cb4fdd3be53d6bd016a6b8489bf8a70 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 25 Mar 2022 15:43:35 -0700 Subject: [PATCH] api: Remove Sort::isParametricDatatype(). (#8405) Previously, Sort::isParametricDatatype() returned true for both instantiated and non-instantiated parametric datatypes. This deletes the method, instead one can check getDatatype().isParametric(). Parametric datatypes will be distinguished from instantiated parametric datatypes via a forthcoming method Sort::isInstantiated. Co-authored-by: ajreynol --- src/api/cpp/cvc5.cpp | 25 ++++++++--------------- src/api/cpp/cvc5.h | 10 --------- src/api/java/io/github/cvc5/api/Sort.java | 11 ---------- src/api/java/jni/sort.cpp | 14 ------------- src/api/python/cvc5.pxd | 1 - src/api/python/cvc5.pxi | 8 -------- src/expr/symbol_table.cpp | 5 +++-- src/parser/parser.cpp | 20 ++++++++++-------- test/unit/api/cpp/sort_black.cpp | 7 ------- test/unit/api/java/SortTest.java | 7 ------- test/unit/api/python/test_sort.py | 6 ------ 11 files changed, 23 insertions(+), 91 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4544fd7d2..fa9afe101 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1248,16 +1248,6 @@ bool Sort::isDatatype() const CVC5_API_TRY_CATCH_END; } -bool Sort::isParametricDatatype() const -{ - CVC5_API_TRY_CATCH_BEGIN; - //////// all checks before this line - if (!d_type->isDatatype()) return false; - return d_type->isParametricDatatype(); - //////// - CVC5_API_TRY_CATCH_END; -} - bool Sort::isConstructor() const { CVC5_API_TRY_CATCH_BEGIN; @@ -1400,9 +1390,9 @@ Sort Sort::instantiate(const std::vector& params) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; CVC5_API_CHECK_DOMAIN_SORTS(params); - CVC5_API_CHECK(isParametricDatatype() || isSortConstructor()) + CVC5_API_CHECK(d_type->isParametricDatatype() || d_type->isSortConstructor()) << "Expected parametric datatype or sort constructor sort."; - CVC5_API_CHECK(!isParametricDatatype() + CVC5_API_CHECK(!d_type->isParametricDatatype() || d_type->getNumChildren() == params.size() + 1) << "Arity mismatch for instantiated parametric datatype"; CVC5_API_CHECK(!isSortConstructor() @@ -1714,7 +1704,7 @@ uint32_t Sort::getFloatingPointExponentSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + CVC5_API_CHECK(d_type->isFloatingPoint()) << "Not a floating-point sort."; //////// all checks before this line return d_type->getFloatingPointExponentSize(); //////// @@ -1725,7 +1715,7 @@ uint32_t Sort::getFloatingPointSignificandSize() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isFloatingPoint()) << "Not a floating-point sort."; + CVC5_API_CHECK(d_type->isFloatingPoint()) << "Not a floating-point sort."; //////// all checks before this line return d_type->getFloatingPointSignificandSize(); //////// @@ -1738,7 +1728,8 @@ std::vector Sort::getDatatypeParamSorts() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort."; + CVC5_API_CHECK(d_type->isParametricDatatype()) + << "Not a parametric datatype sort."; //////// all checks before this line return typeNodeVectorToSorts(d_solver, d_type->getParamTypes()); //////// @@ -1749,7 +1740,7 @@ size_t Sort::getDatatypeArity() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isDatatype()) << "Not a datatype sort."; + CVC5_API_CHECK(d_type->isDatatype()) << "Not a datatype sort."; //////// all checks before this line return d_type->isParametricDatatype() ? d_type->getNumChildren() - 1 : 0; //////// @@ -1773,7 +1764,7 @@ std::vector Sort::getTupleSorts() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isTuple()) << "Not a tuple sort."; + CVC5_API_CHECK(d_type->isTuple()) << "Not a tuple sort."; //////// all checks before this line return typeNodeVectorToSorts(d_solver, d_type->getTupleTypes()); //////// diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 16552edb7..7a81dacb6 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -505,16 +505,6 @@ class CVC5_EXPORT Sort */ bool isDatatype() const; - /** - * Is this a parametric datatype sort? A parametric datatype sort is either - * one that is returned by a call to Solver::mkDatatypeSort() or - * Solver::mkDatatypeSorts() for a parametric datatype, or an instantiated - * datatype sort returned by Sort::instantiate() for parametric datatype - * sort `s`. - * @return true if the sort is a parametric datatype sort - */ - bool isParametricDatatype() const; - /** * Is this a constructor sort? * @return true if the sort is a constructor sort diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 61afb909a..e600fbaeb 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -199,17 +199,6 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isDatatype(long pointer); - /** - * Is this a parametric datatype sort? - * @return true if the sort is a parametric datatype sort - */ - public boolean isParametricDatatype() - { - return isParametricDatatype(pointer); - } - - private native boolean isParametricDatatype(long pointer); - /** * Is this a constructor sort? * @return true if the sort is a constructor sort diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index 67e143c5c..12ce60ae0 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -249,20 +249,6 @@ Java_io_github_cvc5_api_Sort_isDatatype(JNIEnv* env, jobject, jlong pointer) CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } -/* - * Class: io_github_cvc5_api_Sort - * Method: isParametricDatatype - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isParametricDatatype( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return static_cast(current->isParametricDatatype()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - /* * Class: io_github_cvc5_api_Sort * Method: isConstructor diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index a5ca0470e..f923a0263 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -387,7 +387,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isBitVector() except + bint isFloatingPoint() except + bint isDatatype() except + - bint isParametricDatatype() except + bint isConstructor() except + bint isSelector() except + bint isTester() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index cece9c3fb..963ab70b8 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2655,14 +2655,6 @@ cdef class Sort: """ return self.csort.isDatatype() - def isParametricDatatype(self): - """ - Is this a parametric datatype sort? - - :return: True if the sort is a parametric datatype sort. - """ - return self.csort.isParametricDatatype() - def isConstructor(self): """ Is this a constructor sort? diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 66b690a89..7aabb2055 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -485,8 +485,9 @@ api::Sort SymbolTable::Implementation::lookupType( } if (p.second.isDatatype()) { - PrettyCheckArgument( - p.second.isParametricDatatype(), name, "expected parametric datatype"); + PrettyCheckArgument(p.second.getDatatype().isParametric(), + name, + "expected parametric datatype"); return p.second.instantiate(params); } bool isSortConstructor = p.second.isSortConstructor(); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index acb8b78a5..9c3877265 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -384,9 +384,9 @@ std::vector Parser::bindMutualDatatypeTypes( if (isDeclared(name, SYM_SORT)) { throw ParserException(name + " already declared"); } - if (t.isParametricDatatype()) + if (dt.isParametric()) { - std::vector paramTypes = t.getDatatypeParamSorts(); + std::vector paramTypes = dt.getParameters(); defineType(name, paramTypes, t); } else @@ -566,11 +566,16 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { // Type ascriptions only have an effect on the node structure if this is a // parametric datatype. - if (s.isParametricDatatype()) + // get the datatype that t belongs to + api::Sort etyped = etype.getConstructorCodomainSort(); + api::Datatype d = etyped.getDatatype(); + // Note that we check whether the datatype is parametric, and not whether + // etyped is a parametric datatype, since e.g. the smt2 parser constructs + // an arbitrary instantitated constructor term before it is resolved. + // Hence, etyped is an instantiated datatype type, but we correctly + // check if its datatype is parametric. + if (d.isParametric()) { - // get the datatype that t belongs to - api::Sort etyped = etype.getConstructorCodomainSort(); - api::Datatype d = etyped.getDatatype(); // lookup by name api::DatatypeConstructor dc = d.getConstructor(t.toString()); // ask the constructor for the specialized constructor term @@ -582,8 +587,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) { std::stringstream ss; ss << "Type ascription on constructor not satisfied, term " << t - << " expected sort " << s << " but has sort " - << t.getSort().getConstructorCodomainSort(); + << " expected sort " << s << " but has sort " << etyped; parseError(ss.str()); } return t; diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index bcf57ef2d..40e00d996 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -144,13 +144,6 @@ TEST_F(TestApiBlackSort, isDatatype) ASSERT_NO_THROW(Sort().isDatatype()); } -TEST_F(TestApiBlackSort, isParametricDatatype) -{ - Sort param_dt_sort = create_param_datatype_sort(); - ASSERT_TRUE(param_dt_sort.isParametricDatatype()); - ASSERT_NO_THROW(Sort().isParametricDatatype()); -} - TEST_F(TestApiBlackSort, isConstructor) { Sort dt_sort = create_datatype_sort(); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index f1343366b..87016a0e3 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -147,13 +147,6 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isDatatype()); } - @Test void isParametricDatatype() throws CVC5ApiException - { - Sort param_dt_sort = create_param_datatype_sort(); - assertTrue(param_dt_sort.isParametricDatatype()); - assertDoesNotThrow(() -> d_solver.getNullSort().isParametricDatatype()); - } - @Test void isConstructor() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index f552a3eb2..83c60b312 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -133,12 +133,6 @@ def test_is_datatype(solver): Sort(solver).isDatatype() -def test_is_parametric_datatype(solver): - param_dt_sort = create_param_datatype_sort(solver) - assert param_dt_sort.isParametricDatatype() - Sort(solver).isParametricDatatype() - - def test_is_constructor(solver): dt_sort = create_datatype_sort(solver) dt = dt_sort.getDatatype() -- 2.30.2