From bf06678feedf5495d8d53a520747e456811cfa19 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 30 Mar 2022 12:39:52 -0700 Subject: [PATCH] api: Add Sort::getUninterpretedSortConstructor(). (#8459) This further introduces TypeNode::isInstantiatedUninterpretedSort(). --- src/api/cpp/cvc5.cpp | 12 ++++++++++++ src/api/cpp/cvc5.h | 10 +++++++++- src/api/java/io/github/cvc5/api/Sort.java | 14 ++++++++++++++ src/api/java/jni/sort.cpp | 17 +++++++++++++++++ src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 11 +++++++++++ src/expr/type_node.cpp | 16 ++++++++++++++-- src/expr/type_node.h | 16 +++++++++++++++- test/unit/api/cpp/sort_black.cpp | 14 ++++++++++++++ test/unit/api/java/SortTest.java | 13 +++++++++++++ test/unit/api/python/test_sort.py | 12 ++++++++++++ 11 files changed, 132 insertions(+), 4 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a0604537c..1d1e0f5ec 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1386,6 +1386,18 @@ bool Sort::isUninterpretedSortConstructor() const CVC5_API_TRY_CATCH_END; } +Sort Sort::getUninterpretedSortConstructor() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(d_type->isInstantiatedUninterpretedSort()) + << "Expected instantiated uninterpreted sort."; + //////// all checks before this line + return Sort(d_solver, d_type->getUninterpretedSortConstructor()); + //////// + CVC5_API_TRY_CATCH_END; +} + Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 2ca093399..d3b8fab56 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -585,6 +585,14 @@ class CVC5_EXPORT Sort */ bool isInstantiated() const; + /** + * Get the associated uninterpreted sort constructor of an instantiated + * uninterpreted sort. + * + * @return the uninterpreted sort constructor sort + */ + Sort getUninterpretedSortConstructor() const; + /** * @return the underlying datatype of a datatype sort */ @@ -758,7 +766,7 @@ class CVC5_EXPORT Sort */ bool isUninterpretedSortParameterized() const; - /* Sort constructor sort ----------------------------------------------- */ + /* Uninterpreted sort constructor sort --------------------------------- */ /** * @return the arity of an uninterpreted sort 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 a81993302..9f4cd1c9e 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -379,6 +379,20 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isInstantiated(long pointer); + /** + * Get the associated uninterpreted sort constructor of an instantiated + * uninterpreted sort. + * + * @return the uninterpreted sort constructor sort + */ + public Sort getUninterpretedSortConstructor() + { + long sortPointer = getUninterpretedSortConstructor(pointer); + return new Sort(solver, sortPointer); + } + + private native long getUninterpretedSortConstructor(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 0fc9f4574..5f7d7302a 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -492,6 +492,23 @@ Java_io_github_cvc5_api_Sort_getInstantiatedParameters(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } +/* + * Class: io_github_cvc5_api_Sort + * Method: getUninterpretedSortConstructor + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Sort_getUninterpretedSortConstructor(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Sort* current = reinterpret_cast(pointer); + Sort* retPointer = new Sort(current->getUninterpretedSortConstructor()); + return reinterpret_cast(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Sort * Method: getDatatype diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ad354bb84..40a7b613f 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -398,6 +398,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": bint isUninterpretedSort() except + bint isUninterpretedSortConstructor() except + bint isInstantiated() except + + Sort getUninterpretedSortConstructor() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + vector[Sort] getInstantiatedParameters() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index a8e5b13ef..24f6f23b5 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2919,6 +2919,17 @@ cdef class Sort: """ return self.csort.isInstantiated() + def getUninterpretedSortConstructor(self): + """ + Get the associated uninterpreted sort constructor of an + instantiated uninterpreted sort. + + :return: the uninterpreted sort constructor sort + """ + cdef Sort sort = Sort(self.solver) + sort.csort = self.csort.getUninterpretedSortConstructor() + return sort + def getDatatype(self): """ :return: the underlying datatype of a datatype sort diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9b4fd46c1..e84a7046d 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -422,10 +422,14 @@ bool TypeNode::isInstantiatedDatatype() const { return true; } +bool TypeNode::isInstantiatedUninterpretedSort() const +{ + return isUninterpretedSort() && getNumChildren() > 0; +} + bool TypeNode::isInstantiated() const { - return isInstantiatedDatatype() - || (isUninterpretedSort() && getNumChildren() > 0); + return isInstantiatedDatatype() || isInstantiatedUninterpretedSort(); } TypeNode TypeNode::instantiate(const std::vector& params) const @@ -461,6 +465,14 @@ std::string TypeNode::getName() const return getAttribute(expr::VarNameAttr()); } +TypeNode TypeNode::getUninterpretedSortConstructor() const +{ + Assert(isInstantiatedUninterpretedSort()); + NodeBuilder nb(kind::SORT_TYPE); + nb << NodeManager::operatorFromType(*this); + return nb.constructTypeNode(); +} + bool TypeNode::isParameterInstantiatedDatatype(size_t n) const { Assert(getKind() == kind::PARAMETRIC_DATATYPE); diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 495f5b383..d8e7abd38 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -370,7 +370,7 @@ private: } /** - * Very basic pretty printer for Node. + * Very basic pretty printer for TypeNode. * * @param out output stream to print to. * @param indent number of spaces to indent the formula by. @@ -603,6 +603,12 @@ private: /** Is this a fully instantiated datatype type */ bool isInstantiatedDatatype() const; + /** + * Is this an uninterpreted sort constructed from instantiating an + * uninterpreted sort constructor? + */ + bool isInstantiatedUninterpretedSort() const; + /** * Return true if this is an instantiated parametric datatype or * uninterpreted sort constructor type. @@ -671,6 +677,14 @@ private: */ std::string getName() const; + /** + * Get the uninterpreted sort constructor type this instantiated + * uninterpreted sort has been constructed from. + * + * Asserts that this is an instantiated uninterpreted sort. + */ + TypeNode getUninterpretedSortConstructor() const; + /** Get the most general base type of the type */ TypeNode getBaseType() const; diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 35c32e030..759fd1543 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -386,6 +386,20 @@ TEST_F(TestApiBlackSort, getInstantiatedParameters) ASSERT_THROW(bvSort.getInstantiatedParameters(), CVC5ApiException); } +TEST_F(TestApiBlackSort, getUninterpretedSortConstructor) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + ASSERT_THROW(sortConsSort.getUninterpretedSortConstructor(), + CVC5ApiException); + Sort instSortConsSort = + sortConsSort.instantiate({boolSort, intSort, bvSort, realSort}); + ASSERT_EQ(sortConsSort, instSortConsSort.getUninterpretedSortConstructor()); +} + TEST_F(TestApiBlackSort, getFunctionArity) { Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index e2b3ff5ae..b8071b77c 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -379,6 +379,19 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters()); } + @Test void getUninterpretedSortConstructor() throws CVC5ApiException + { + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + Sort boolSort = d_solver.getBooleanSort(); + Sort bvSort = d_solver.mkBitVectorSort(8); + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 4); + assertThrows(CVC5ApiException.class, () -> sortConsSort.getUninterpretedSortConstructor()); + Sort instSortConsSort = + sortConsSort.instantiate(new Sort[] {boolSort, intSort, bvSort, realSort}); + assertEquals(sortConsSort, instSortConsSort.getUninterpretedSortConstructor()); + } + @Test void getFunctionArity() throws CVC5ApiException { Sort funSort = diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 4c7743db9..ab2375059 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -366,6 +366,18 @@ def test_get_instantiated_parameters(solver): with pytest.raises(RuntimeError): bvSort.getInstantiatedParameters() +def test_get_uninterpreted_sort_constructor(solver): + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + boolSort = solver.getBooleanSort() + bvSort = solver.mkBitVectorSort(8) + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 4) + with pytest.raises(RuntimeError): + sortConsSort.getUninterpretedSortConstructor() + instSortConsSort = \ + sortConsSort.instantiate([boolSort, intSort, bvSort, realSort]); + assert sortConsSort == instSortConsSort.getUninterpretedSortConstructor() + def test_get_function_arity(solver): funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), solver.getIntegerSort()) -- 2.30.2