From e7fe90e7b8928cb18d597c6f0e8b0df362f604d7 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 29 Mar 2022 14:36:12 -0700 Subject: [PATCH] api: Add Sort::getInstantiatedParameters(). (#8445) This adds a function to retrieve the sort arguments an instantiated sort has been instantiated with. It further deletes Sort::getDatatypeParamSorts() and Sort::getUninterpretedSortParamSorts(). --- src/api/cpp/cvc5.cpp | 45 +++-------- src/api/cpp/cvc5.h | 30 +++---- src/api/java/io/github/cvc5/api/Sort.java | 47 ++++------- src/api/java/jni/sort.cpp | 70 ++++++---------- src/api/python/cvc5.pxd | 3 +- src/api/python/cvc5.pxi | 46 ++++------- src/expr/type_node.cpp | 4 +- test/unit/api/cpp/sort_black.cpp | 98 ++++++++++++----------- test/unit/api/java/SortTest.java | 81 +++++++++++-------- test/unit/api/python/test_sort.py | 83 +++++++++++-------- 10 files changed, 235 insertions(+), 272 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d0f0957d2..f74955f5f 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1445,6 +1445,18 @@ Sort Sort::instantiate(const std::vector& params) const CVC5_API_TRY_CATCH_END; } +std::vector Sort::getInstantiatedParameters() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_type->isInstantiated()) + << "Expected instantiated parametric sort"; + //////// all checks before this line + return typeNodeVectorToSorts(d_solver, d_type->getInstantiatedParamTypes()); + //////// + CVC5_API_TRY_CATCH_END; +} + Sort Sort::substitute(const Sort& sort, const Sort& replacement) const { CVC5_API_TRY_CATCH_BEGIN; @@ -1672,27 +1684,6 @@ Sort Sort::getSequenceElementSort() const CVC5_API_TRY_CATCH_END; } -/* Uninterpreted sort -------------------------------------------------- */ - -std::vector Sort::getUninterpretedSortParamSorts() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort."; - //////// all checks before this line - - /* This method is not implemented in the NodeManager, since whether a - * uninterpreted sort is parameterized is irrelevant for solving. */ - std::vector params; - for (size_t i = 0, nchildren = d_type->getNumChildren(); i < nchildren; i++) - { - params.push_back((*d_type)[i]); - } - return typeNodeVectorToSorts(d_solver, params); - //////// - CVC5_API_TRY_CATCH_END; -} - /* Sort constructor sort ----------------------------------------------- */ size_t Sort::getUninterpretedSortConstructorArity() const @@ -1745,18 +1736,6 @@ uint32_t Sort::getFloatingPointSignificandSize() const /* Datatype sort ------------------------------------------------------- */ -std::vector Sort::getDatatypeParamSorts() const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(d_type->isParametricDatatype()) - << "Not a parametric datatype sort."; - //////// all checks before this line - return typeNodeVectorToSorts(d_solver, d_type->getDType().getParameters()); - //////// - CVC5_API_TRY_CATCH_END; -} - size_t Sort::getDatatypeArity() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3576f1f00..14e81897e 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -615,14 +615,25 @@ class CVC5_EXPORT Sort * Instantiate a parameterized datatype sort or uninterpreted sort * constructor sort. * - * Create sorts parameter with Solver::mkParamSort(). + * Create sort parameters with Solver::mkParamSort(). * * @warning This method is experimental and may change in future versions. * * @param params the list of sort parameters to instantiate with + * @return the instantiated sort */ Sort instantiate(const std::vector& params) const; + /** + * Get the sorts used to instantiate the sort parameters of a parametric + * sort (parametric datatype or uninterpreted sort constructor sort, + * see Sort::instantiate(const std::vector& const)). + * + * @return the sorts used to instantiate the sort parameters of a + * parametric sort + */ + std::vector getInstantiatedParameters() const; + /** * Substitution of Sorts. * @@ -768,11 +779,6 @@ class CVC5_EXPORT Sort */ bool isUninterpretedSortParameterized() const; - /** - * @return the parameter sorts of an uninterpreted sort - */ - std::vector getUninterpretedSortParamSorts() const; - /* Sort constructor sort ----------------------------------------------- */ /** @@ -801,18 +807,6 @@ class CVC5_EXPORT Sort /* Datatype sort ------------------------------------------------------- */ - /** - * - * Return the parameters of a parametric datatype sort. If this sort is a - * non-instantiated parametric datatype, this returns the parameter sorts of - * the underlying datatype. If this sort is an instantiated parametric - * datatype, then this returns the sort parameters that were used to - * construct the sort via Sort::instantiate(). - * - * @return the parameter sorts of a parametric datatype sort. - */ - std::vector getDatatypeParamSorts() const; - /** * @return the arity of a datatype sort */ diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index fac9c4679..0cd275070 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -399,6 +399,7 @@ public class Sort extends AbstractPointer implements Comparable * @apiNote This method is experimental and may change in future versions. * * @param params the list of sort parameters to instantiate with + * @return the instantiated sort */ public Sort instantiate(List params) { @@ -424,6 +425,22 @@ public class Sort extends AbstractPointer implements Comparable private native long instantiate(long pointer, long[] paramsPointers); + /** + * Get the sorts used to instantiate the sort parameters of a parametric + * sort (parametric datatype or uninterpreted sort constructor sort, + * see Sort.instantiate()). + * + * @return the sorts used to instantiate the sort parameters of a + * parametric sort + */ + public Sort[] getInstantiatedParameters() + { + long[] pointers = getInstantiatedParameters(pointer); + return Utils.getSorts(solver, pointers); + } + + private native long[] getInstantiatedParameters(long pointer); + /** * Substitution of Sorts. * @@ -661,19 +678,6 @@ public class Sort extends AbstractPointer implements Comparable private native long getSequenceElementSort(long pointer); - /* Uninterpreted sort -------------------------------------------------- */ - - /** - * @return the parameter sorts of an uninterpreted sort - */ - public Sort[] getUninterpretedSortParamSorts() - { - long[] pointers = getUninterpretedSortParamSorts(pointer); - return Utils.getSorts(solver, pointers); - } - - private native long[] getUninterpretedSortParamSorts(long pointer); - /* Sort constructor sort ----------------------------------------------- */ /** @@ -722,23 +726,6 @@ public class Sort extends AbstractPointer implements Comparable /* Datatype sort ------------------------------------------------------- */ - /** - * Return the parameters of a parametric datatype sort. If this sort is a - * non-instantiated parametric datatype, this returns the parameter sorts of - * the underlying datatype. If this sort is an instantiated parametric - * datatype, then this returns the sort parameters that were used to - * construct the sort via Sort.instantiate(). - * - * @return the parameter sorts of a datatype sort - */ - public Sort[] getDatatypeParamSorts() - { - long[] pointers = getDatatypeParamSorts(pointer); - return Utils.getSorts(solver, pointers); - } - - private native long[] getDatatypeParamSorts(long pointer); - /** * @return the arity of a datatype sort */ diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index 4d5b6986c..d6c02ed4c 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -468,6 +468,30 @@ Java_io_github_cvc5_api_Sort_isInstantiated(JNIEnv* env, jobject, jlong pointer) CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } +/* + * Class: io_github_cvc5_api_Sort + * Method: getInstantiatedParameters + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL +Java_io_github_cvc5_api_Sort_getInstantiatedParameters(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Sort* current = reinterpret_cast(pointer); + std::vector sorts = current->getInstantiatedParameters(); + std::vector sortPointers(sorts.size()); + for (size_t i = 0; i < sorts.size(); i++) + { + sortPointers[i] = reinterpret_cast(new Sort(sorts[i])); + } + jlongArray ret = env->NewLongArray(sorts.size()); + env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + /* * Class: io_github_cvc5_api_Sort * Method: getDatatype @@ -840,30 +864,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Sort_getSequenceElementSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Sort - * Method: getUninterpretedSortParamSorts - * Signature: (J)[J - */ -JNIEXPORT jlongArray JNICALL -Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env, - jobject, - jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - std::vector sorts = current->getUninterpretedSortParamSorts(); - std::vector sortPointers(sorts.size()); - for (size_t i = 0; i < sorts.size(); i++) - { - sortPointers[i] = reinterpret_cast(new Sort(sorts[i])); - } - jlongArray ret = env->NewLongArray(sorts.size()); - env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_api_Sort * Method: getUninterpretedSortConstructorArity @@ -926,28 +926,6 @@ Java_io_github_cvc5_api_Sort_getFloatingPointSignificandSize(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Sort - * Method: getDatatypeParamSorts - * Signature: (J)[J - */ -JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Sort_getDatatypeParamSorts( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - std::vector sorts = current->getDatatypeParamSorts(); - std::vector sortPointers(sorts.size()); - for (size_t i = 0; i < sorts.size(); i++) - { - sortPointers[i] = reinterpret_cast(new Sort(sorts[i])); - } - jlongArray ret = env->NewLongArray(sorts.size()); - env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_api_Sort * Method: getDatatypeArity diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ce5dd100c..4ee50f615 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -400,6 +400,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isInstantiated() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + + vector[Sort] getInstantiatedParameters() except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + size_t getConstructorArity() except + vector[Sort] getConstructorDomainSorts() except + @@ -416,12 +417,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSetElementSort() except + Sort getBagElementSort() except + Sort getSequenceElementSort() except + - vector[Sort] getUninterpretedSortParamSorts() except + size_t getUninterpretedSortConstructorArity() except + uint32_t getBitVectorSize() except + uint32_t getFloatingPointExponentSize() except + uint32_t getFloatingPointSignificandSize() except + - vector[Sort] getDatatypeParamSorts() except + size_t getDatatypeArity() except + size_t getTupleLength() except + vector[Sort] getTupleSorts() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index a378434ab..66f037ad0 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2837,6 +2837,7 @@ cdef class Sort: versions. :param params: the list of sort parameters to instantiate with + :return: the instantiated sort """ cdef Sort sort = Sort(self.solver) cdef vector[c_Sort] v @@ -2845,6 +2846,22 @@ cdef class Sort: sort.csort = self.csort.instantiate(v) return sort + def getInstantiatedParameters(self): + """ + Get the sorts used to instantiate the sort parameters of a + parametric sort (parametric datatype or uninterpreted sort + constructor sort, see Sort.instantiate()). + + :return the sorts used to instantiate the sort parameters of a + parametric sort + """ + instantiated_sorts = [] + for s in self.csort.getInstantiatedParameters(): + sort = Sort(self.solver) + sort.csort = s + instantiated_sorts.append(sort) + return instantiated_sorts + def substitute(self, sort_or_list_1, sort_or_list_2): """ Substitution of Sorts. @@ -3017,17 +3034,6 @@ cdef class Sort: sort.csort = self.csort.getSequenceElementSort() return sort - def getUninterpretedSortParamSorts(self): - """ - :return: the parameter sorts of an uninterpreted sort - """ - param_sorts = [] - for s in self.csort.getUninterpretedSortParamSorts(): - sort = Sort(self.solver) - sort.csort = s - param_sorts.append(sort) - return param_sorts - def getUninterpretedSortConstructorArity(self): """ :return: the arity of a sort constructor sort @@ -3052,24 +3058,6 @@ cdef class Sort: """ return self.csort.getFloatingPointSignificandSize() - def getDatatypeParamSorts(self): - """ - Return the parameters of a parametric datatype sort. If this sort - is a non-instantiated parametric datatype, this returns the - parameter sorts of the underlying datatype. If this sort is an - instantiated parametric datatype, then this returns the sort - parameters that were used to construct the sort via - :py:meth:`instantiate()`. - - :return: the parameter sorts of a parametric datatype sort - """ - param_sorts = [] - for s in self.csort.getDatatypeParamSorts(): - sort = Sort(self.solver) - sort.csort = s - param_sorts.append(sort) - return param_sorts - def getDatatypeArity(self): """ :return: the arity of a datatype sort diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b784e8ce1..4ef73ddba 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -364,7 +364,9 @@ std::vector TypeNode::getInstantiatedParamTypes() const { Assert(isInstantiated()); vector params; - for (uint32_t i = 1, i_end = getNumChildren(); i < i_end; ++i) + for (uint32_t i = isInstantiatedDatatype() ? 1 : 0, i_end = getNumChildren(); + i < i_end; + ++i) { params.push_back((*this)[i]); } diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 37beffa90..bd37aecdf 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -308,8 +308,7 @@ TEST_F(TestApiBlackSort, instantiate) { // instantiate parametric datatype, check should not fail Sort paramDtypeSort = create_param_datatype_sort(); - ASSERT_NO_THROW( - paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()})); + ASSERT_NO_THROW(paramDtypeSort.instantiate({d_solver.getIntegerSort()})); // instantiate non-parametric datatype sort, check should fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); @@ -318,13 +317,11 @@ TEST_F(TestApiBlackSort, instantiate) DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - ASSERT_THROW( - dtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}), - CVC5ApiException); + ASSERT_THROW(dtypeSort.instantiate({d_solver.getIntegerSort()}), + CVC5ApiException); // instantiate uninterpreted sort constructor Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); - ASSERT_NO_THROW( - sortConsSort.instantiate(std::vector{d_solver.getIntegerSort()})); + ASSERT_NO_THROW(sortConsSort.instantiate({d_solver.getIntegerSort()})); } TEST_F(TestApiBlackSort, isInstantiated) @@ -332,19 +329,65 @@ TEST_F(TestApiBlackSort, isInstantiated) Sort paramDtypeSort = create_param_datatype_sort(); ASSERT_FALSE(paramDtypeSort.isInstantiated()); Sort instParamDtypeSort = - paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}); + paramDtypeSort.instantiate({d_solver.getIntegerSort()}); ASSERT_TRUE(instParamDtypeSort.isInstantiated()); Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); ASSERT_FALSE(sortConsSort.isInstantiated()); - Sort instSortConsSort = - sortConsSort.instantiate(std::vector{d_solver.getIntegerSort()}); + Sort instSortConsSort = sortConsSort.instantiate({d_solver.getIntegerSort()}); ASSERT_TRUE(instSortConsSort.isInstantiated()); ASSERT_FALSE(d_solver.getIntegerSort().isInstantiated()); ASSERT_FALSE(d_solver.mkBitVectorSort(32).isInstantiated()); } +TEST_F(TestApiBlackSort, getInstantiatedParameters) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort bvSort = d_solver.mkBitVectorSort(8); + std::vector instSorts; + + // parametric datatype instantiation + Sort p1 = d_solver.mkParamSort("p1"); + Sort p2 = d_solver.mkParamSort("p2"); + DatatypeDecl pspec = d_solver.mkDatatypeDecl("pdtype", {p1, p2}); + DatatypeConstructorDecl pcons1 = d_solver.mkDatatypeConstructorDecl("cons1"); + DatatypeConstructorDecl pcons2 = d_solver.mkDatatypeConstructorDecl("cons2"); + DatatypeConstructorDecl pnil = d_solver.mkDatatypeConstructorDecl("nil"); + pcons1.addSelector("sel", p1); + pcons2.addSelector("sel", p2); + pspec.addConstructor(pcons1); + pspec.addConstructor(pcons2); + pspec.addConstructor(pnil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(pspec); + + ASSERT_THROW(paramDtypeSort.getInstantiatedParameters(), CVC5ApiException); + + Sort instParamDtypeSort = paramDtypeSort.instantiate({realSort, boolSort}); + + instSorts = instParamDtypeSort.getInstantiatedParameters(); + ASSERT_EQ(instSorts[0], realSort); + ASSERT_EQ(instSorts[1], boolSort); + + // uninterpreted sort constructor sort instantiation + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + ASSERT_THROW(sortConsSort.getInstantiatedParameters(), CVC5ApiException); + + Sort instSortConsSort = + sortConsSort.instantiate({boolSort, intSort, bvSort, realSort}); + + instSorts = instSortConsSort.getInstantiatedParameters(); + ASSERT_EQ(instSorts[0], boolSort); + ASSERT_EQ(instSorts[1], intSort); + ASSERT_EQ(instSorts[2], bvSort); + ASSERT_EQ(instSorts[3], realSort); + + ASSERT_THROW(intSort.getInstantiatedParameters(), CVC5ApiException); + ASSERT_THROW(bvSort.getInstantiatedParameters(), CVC5ApiException); +} + TEST_F(TestApiBlackSort, getFunctionArity) { Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), @@ -428,17 +471,6 @@ TEST_F(TestApiBlackSort, getSymbol) ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); - Sort siSort = sSort.instantiate({uSort, uSort}); - ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2); - Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC5ApiException); -} - TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) { Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); @@ -479,30 +511,6 @@ TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); } -TEST_F(TestApiBlackSort, getDatatypeParamSorts) -{ - // create parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl paramCons = - d_solver.mkDatatypeConstructorDecl("cons"); - DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil"); - paramCons.addSelector("head", sort); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - ASSERT_NO_THROW(paramDtypeSort.getDatatypeParamSorts()); - // create non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", d_solver.getIntegerSort()); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC5ApiException); -} - TEST_F(TestApiBlackSort, getDatatypeArity) { // create datatype sort, check should not fail diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 426b67a56..e2b3ff5ae 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -332,6 +332,53 @@ class SortTest assertFalse(d_solver.mkBitVectorSort(32).isInstantiated()); } + @Test void getInstantiatedParameters() throws CVC5ApiException + { + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort[] instSorts; + + // parametric datatype instantiation + Sort p1 = d_solver.mkParamSort("p1"); + Sort p2 = d_solver.mkParamSort("p2"); + DatatypeDecl pspec = d_solver.mkDatatypeDecl("pdtype", new Sort[] {p1, p2}); + DatatypeConstructorDecl pcons1 = d_solver.mkDatatypeConstructorDecl("cons1"); + DatatypeConstructorDecl pcons2 = d_solver.mkDatatypeConstructorDecl("cons2"); + DatatypeConstructorDecl pnil = d_solver.mkDatatypeConstructorDecl("nil"); + pcons1.addSelector("sel", p1); + pcons2.addSelector("sel", p2); + pspec.addConstructor(pcons1); + pspec.addConstructor(pcons2); + pspec.addConstructor(pnil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(pspec); + + assertThrows(CVC5ApiException.class, () -> paramDtypeSort.getInstantiatedParameters()); + + Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {realSort, boolSort}); + + instSorts = instParamDtypeSort.getInstantiatedParameters(); + assertEquals(instSorts[0], realSort); + assertEquals(instSorts[1], boolSort); + + // uninterpreted sort constructor sort instantiation + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + assertThrows(CVC5ApiException.class, () -> sortConsSort.getInstantiatedParameters()); + + Sort instSortConsSort = + sortConsSort.instantiate(new Sort[] {boolSort, intSort, bvSort, realSort}); + + instSorts = instSortConsSort.getInstantiatedParameters(); + assertEquals(instSorts[0], boolSort); + assertEquals(instSorts[1], intSort); + assertEquals(instSorts[2], bvSort); + assertEquals(instSorts[3], realSort); + + assertThrows(CVC5ApiException.class, () -> intSort.getInstantiatedParameters()); + assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters()); + } + @Test void getFunctionArity() throws CVC5ApiException { Sort funSort = @@ -415,17 +462,6 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } - @Test void getUninterpretedSortParamSorts() throws CVC5ApiException - { - Sort uSort = d_solver.mkUninterpretedSort("u"); - assertDoesNotThrow(() -> uSort.getUninterpretedSortParamSorts()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); - Sort siSort = sSort.instantiate(new Sort[] {uSort, uSort}); - assertEquals(siSort.getUninterpretedSortParamSorts().length, 2); - Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortParamSorts()); - } - @Test void getUninterpretedSortConstructorName() throws CVC5ApiException { Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); @@ -466,29 +502,6 @@ class SortTest assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } - @Test void getDatatypeParamSorts() throws CVC5ApiException - { - // create parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); - DatatypeConstructorDecl paramCons = d_solver.mkDatatypeConstructorDecl("cons"); - DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil"); - paramCons.addSelector("head", sort); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - assertDoesNotThrow(() -> paramDtypeSort.getDatatypeParamSorts()); - // create non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", d_solver.getIntegerSort()); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - assertThrows(CVC5ApiException.class, () -> dtypeSort.getDatatypeParamSorts()); - } - @Test void getDatatypeArity() throws CVC5ApiException { // create datatype sort, check should not fail diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index a78884a93..4c7743db9 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -317,6 +317,55 @@ def test_is_instantiated(solver): assert not solver.getIntegerSort().isInstantiated() assert not solver.mkBitVectorSort(32).isInstantiated() +def test_get_instantiated_parameters(solver): + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + boolSort = solver.getBooleanSort() + bvSort = solver.mkBitVectorSort(8) + + # parametric datatype instantiation + p1 = solver.mkParamSort("p1") + p2 = solver.mkParamSort("p2") + pspec = solver.mkDatatypeDecl("pdtype", [p1, p2]) + pcons1 = solver.mkDatatypeConstructorDecl("cons1") + pcons2 = solver.mkDatatypeConstructorDecl("cons2") + pnil = solver.mkDatatypeConstructorDecl("nil") + pcons1.addSelector("sel", p1) + pcons2.addSelector("sel", p2) + pspec.addConstructor(pcons1) + pspec.addConstructor(pcons2) + pspec.addConstructor(pnil) + paramDtypeSort = solver.mkDatatypeSort(pspec) + + with pytest.raises(RuntimeError): + paramDtypeSort.getInstantiatedParameters() + + instParamDtypeSort = \ + paramDtypeSort.instantiate([realSort, boolSort]); + + instSorts = instParamDtypeSort.getInstantiatedParameters(); + assert instSorts[0] == realSort + assert instSorts[1] == boolSort + + # uninterpreted sort constructor sort instantiation + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4) + with pytest.raises(RuntimeError): + sortConsSort.getInstantiatedParameters() + + instSortConsSort = sortConsSort.instantiate( + [boolSort, intSort, bvSort, realSort]); + + instSorts = instSortConsSort.getInstantiatedParameters() + assert instSorts[0] == boolSort + assert instSorts[1] == intSort + assert instSorts[2] == bvSort + assert instSorts[3] == realSort + + with pytest.raises(RuntimeError): + intSort.getInstantiatedParameters() + with pytest.raises(RuntimeError): + bvSort.getInstantiatedParameters() + def test_get_function_arity(solver): funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), solver.getIntegerSort()) @@ -400,17 +449,6 @@ def test_get_uninterpreted_sort_name(solver): bvSort.getSymbol() -def test_get_uninterpreted_sort_paramsorts(solver): - uSort = solver.mkUninterpretedSort("u") - uSort.getUninterpretedSortParamSorts() - sSort = solver.mkUninterpretedSortConstructorSort("s", 2) - siSort = sSort.instantiate([uSort, uSort]) - assert len(siSort.getUninterpretedSortParamSorts()) == 2 - bvSort = solver.mkBitVectorSort(32) - with pytest.raises(RuntimeError): - bvSort.getUninterpretedSortParamSorts() - - def test_get_uninterpreted_sort_constructor_name(solver): sSort = solver.mkUninterpretedSortConstructorSort("s", 2) sSort.getSymbol() @@ -451,29 +489,6 @@ def test_get_fp_significand_size(solver): setSort.getFloatingPointSignificandSize() -def test_get_datatype_paramsorts(solver): - # create parametric datatype, check should not fail - sort = solver.mkParamSort("T") - paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) - paramCons = solver.mkDatatypeConstructorDecl("cons") - paramNil = solver.mkDatatypeConstructorDecl("nil") - paramCons.addSelector("head", sort) - paramDtypeSpec.addConstructor(paramCons) - paramDtypeSpec.addConstructor(paramNil) - paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) - paramDtypeSort.getDatatypeParamSorts() - # create non-parametric datatype sort, check should fail - dtypeSpec = solver.mkDatatypeDecl("list") - cons = solver.mkDatatypeConstructorDecl("cons") - cons.addSelector("head", solver.getIntegerSort()) - dtypeSpec.addConstructor(cons) - nil = solver.mkDatatypeConstructorDecl("nil") - dtypeSpec.addConstructor(nil) - dtypeSort = solver.mkDatatypeSort(dtypeSpec) - with pytest.raises(RuntimeError): - dtypeSort.getDatatypeParamSorts() - - def test_get_datatype_arity(solver): # create datatype sort, check should not fail dtypeSpec = solver.mkDatatypeDecl("list") -- 2.30.2