From 4f573702101ba23279d39ff22550f4b3193f038d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 28 Mar 2022 18:37:13 -0700 Subject: [PATCH] api: Add Sort::isInstantiated(). (#8425) This further removes Sort::isUinterpretedSortParameterized(). --- src/api/cpp/cvc5.cpp | 26 ++++++++---------- src/api/cpp/cvc5.h | 12 +++++++++ src/api/java/io/github/cvc5/api/Sort.java | 27 ++++++++++++------- src/api/java/jni/sort.cpp | 30 ++++++++++----------- src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 19 ++++++++----- src/expr/type_node.cpp | 6 +++++ src/expr/type_node.h | 6 +++++ test/unit/api/cpp/sort_black.cpp | 33 +++++++++++++++-------- test/unit/api/java/SortTest.java | 30 +++++++++++++-------- test/unit/api/python/test_sort.py | 27 +++++++++++-------- 11 files changed, 137 insertions(+), 81 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5c92c9d3a..8b16ea8bc 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1378,13 +1378,23 @@ Datatype Sort::getDatatype() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isDatatype()) << "Expected datatype sort."; + CVC5_API_CHECK(d_type->isDatatype()) << "Expected datatype sort."; //////// all checks before this line return Datatype(d_solver, d_type->getDType()); //////// CVC5_API_TRY_CATCH_END; } +bool Sort::isInstantiated() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + return d_type->isInstantiated(); + //////// + CVC5_API_TRY_CATCH_END; +} + Sort Sort::instantiate(const std::vector& params) const { CVC5_API_TRY_CATCH_BEGIN; @@ -1639,20 +1649,6 @@ Sort Sort::getSequenceElementSort() const /* Uninterpreted sort -------------------------------------------------- */ -bool Sort::isUninterpretedSortParameterized() 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. */ - return d_type->getNumChildren() > 0; - //////// - CVC5_API_TRY_CATCH_END; -} - std::vector Sort::getUninterpretedSortParamSorts() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index c3e5b93ea..18f66dfa8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -594,6 +594,18 @@ class CVC5_EXPORT Sort */ bool isUninterpretedSortConstructor() const; + /** + * Is this an instantiated (parametric datatype or uninterpreted sort + * constructor) sort? + * + * An instantiated sort is a sort that has been constructed from + * instantiating a sort with sort arguments + * (see Sort::instantiate(const std::vector&) const)). + * + * @return true if this is an instantiated sort + */ + bool isInstantiated() const; + /** * @return the underlying datatype 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 ba97057e4..fac9c4679 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -362,6 +362,23 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isUninterpretedSortConstructor(long pointer); + /** + * Is this an instantiated (parametric datatype or uninterpreted sort + * constructor) sort? + * + * An instantiated sort is a sort that has been constructed from + * instantiating a sort with sort arguments + * (see Sort.instantiate()). + * + * @return true if this is an instantiated sort + */ + public boolean isInstantiated() + { + return isInstantiated(pointer); + } + + private native boolean isInstantiated(long pointer); + /** * @return the underlying datatype of a datatype sort */ @@ -646,16 +663,6 @@ public class Sort extends AbstractPointer implements Comparable /* Uninterpreted sort -------------------------------------------------- */ - /** - * @return true if an uninterpreted sort is parameterezied - */ - public boolean isUninterpretedSortParameterized() - { - return isUninterpretedSortParameterized(pointer); - } - - private native boolean isUninterpretedSortParameterized(long pointer); - /** * @return the parameter sorts of an uninterpreted sort */ diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index a3d1f135f..4d5b6986c 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -454,6 +454,20 @@ Java_io_github_cvc5_api_Sort_isUninterpretedSortConstructor(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } +/* + * Class: io_github_cvc5_api_Sort + * Method: isInstantiated + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isInstantiated(JNIEnv* env, jobject, jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Sort* current = reinterpret_cast(pointer); + return static_cast(current->isInstantiated()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); +} + /* * Class: io_github_cvc5_api_Sort * Method: getDatatype @@ -826,22 +840,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: isUninterpretedSortParameterized - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_api_Sort_isUninterpretedSortParameterized(JNIEnv* env, - jobject, - jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Sort* current = reinterpret_cast(pointer); - return static_cast(current->isUninterpretedSortParameterized()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - /* * Class: io_github_cvc5_api_Sort * Method: getUninterpretedSortParamSorts diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 15fd5f3e9..f03941c27 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -397,6 +397,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isSequence() except + bint isUninterpretedSort() except + bint isUninterpretedSortConstructor() except + + bint isInstantiated() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + @@ -415,7 +416,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSetElementSort() except + Sort getBagElementSort() except + Sort getSequenceElementSort() except + - bint isUninterpretedSortParameterized() except + vector[Sort] getUninterpretedSortParamSorts() except + size_t getUninterpretedSortConstructorArity() except + uint32_t getBitVectorSize() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index b9734761e..23fc5fa69 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2806,6 +2806,19 @@ cdef class Sort: """ return self.csort.isUninterpretedSortConstructor() + def isInstantiated(self): + """ + Is this an instantiated (parametric datatype or uninterpreted sort + constructor) sort? + + An instantiated sort is a sort that has been constructed from + instantiating a sort parameters with sort arguments + (see Sort::instantiate()). + + :return: True if this is an instantiated sort. + """ + return self.csort.isInstantiated() + def getDatatype(self): """ :return: the underlying datatype of a datatype sort @@ -3004,12 +3017,6 @@ cdef class Sort: sort.csort = self.csort.getSequenceElementSort() return sort - def isUninterpretedSortParameterized(self): - """ - :return: True if an uninterpreted sort is parameterized - """ - return self.csort.isUninterpretedSortParameterized() - def getUninterpretedSortParamSorts(self): """ :return: the parameter sorts of an uninterpreted sort diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index de85dfb06..a90efd055 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -417,6 +417,12 @@ bool TypeNode::isInstantiatedDatatype() const { return true; } +bool TypeNode::isInstantiated() const +{ + return isInstantiatedDatatype() + || (isSort() && getNumChildren() > 0); +} + TypeNode TypeNode::instantiateParametricDatatype( const std::vector& params) const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9882c7fc5..8f8985d86 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -597,6 +597,12 @@ private: /** Is this a fully instantiated datatype type */ bool isInstantiatedDatatype() const; + /** + * Return true if this is an instantiated parametric datatype or + * uninterpreted sort constructor type. + */ + bool isInstantiated() const; + /** Is this a sygus datatype type */ bool isSygusDatatype() const; diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 9a9368fbc..37beffa90 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -321,6 +321,28 @@ TEST_F(TestApiBlackSort, instantiate) ASSERT_THROW( dtypeSort.instantiate(std::vector{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()})); +} + +TEST_F(TestApiBlackSort, isInstantiated) +{ + Sort paramDtypeSort = create_param_datatype_sort(); + ASSERT_FALSE(paramDtypeSort.isInstantiated()); + Sort instParamDtypeSort = + paramDtypeSort.instantiate(std::vector{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()}); + ASSERT_TRUE(instSortConsSort.isInstantiated()); + + ASSERT_FALSE(d_solver.getIntegerSort().isInstantiated()); + ASSERT_FALSE(d_solver.mkBitVectorSort(32).isInstantiated()); } TEST_F(TestApiBlackSort, getFunctionArity) @@ -406,17 +428,6 @@ TEST_F(TestApiBlackSort, getSymbol) ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); } -TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - ASSERT_FALSE(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); - Sort siSort = sSort.instantiate({uSort}); - ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException); -} - TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 2115c027a..426b67a56 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -311,6 +311,25 @@ class SortTest Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); assertThrows(CVC5ApiException.class, () -> dtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); + // instantiate uninterpreted sort constructor + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); + } + + @Test void isInstantiated() throws CVC5ApiException + { + Sort paramDtypeSort = create_param_datatype_sort(); + assertFalse(paramDtypeSort.isInstantiated()); + Sort instParamDtypeSort = paramDtypeSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); + assertTrue(instParamDtypeSort.isInstantiated()); + + Sort sortConsSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); + assertFalse(sortConsSort.isInstantiated()); + Sort instSortConsSort = sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()}); + assertTrue(instSortConsSort.isInstantiated()); + + assertFalse(d_solver.getIntegerSort().isInstantiated()); + assertFalse(d_solver.mkBitVectorSort(32).isInstantiated()); } @Test void getFunctionArity() throws CVC5ApiException @@ -396,17 +415,6 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } - @Test void isUninterpretedSortParameterized() throws CVC5ApiException - { - Sort uSort = d_solver.mkUninterpretedSort("u"); - assertFalse(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); - Sort siSort = sSort.instantiate(new Sort[] {uSort}); - assertTrue(siSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.isUninterpretedSortParameterized()); - } - @Test void getUninterpretedSortParamSorts() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index b530f2c37..a78884a93 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -299,7 +299,23 @@ def test_instantiate(solver): dtypeSort = solver.mkDatatypeSort(dtypeSpec) with pytest.raises(RuntimeError): dtypeSort.instantiate([solver.getIntegerSort()]) + # instantiate uninterpreted sort constructor + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + sortConsSort.instantiate([solver.getIntegerSort()]) +def test_is_instantiated(solver): + paramDtypeSort = create_param_datatype_sort(solver) + assert not paramDtypeSort.isInstantiated() + instParamDtypeSort = paramDtypeSort.instantiate([solver.getIntegerSort()]); + assert instParamDtypeSort.isInstantiated() + + sortConsSort = solver.mkUninterpretedSortConstructorSort("s", 1) + assert not sortConsSort.isInstantiated() + instSortConsSort = sortConsSort.instantiate([solver.getIntegerSort()]) + assert instSortConsSort.isInstantiated() + + assert not solver.getIntegerSort().isInstantiated() + assert not solver.mkBitVectorSort(32).isInstantiated() def test_get_function_arity(solver): funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), @@ -384,17 +400,6 @@ def test_get_uninterpreted_sort_name(solver): bvSort.getSymbol() -def test_is_uninterpreted_sort_parameterized(solver): - uSort = solver.mkUninterpretedSort("u") - assert not uSort.isUninterpretedSortParameterized() - sSort = solver.mkUninterpretedSortConstructorSort("s", 1) - siSort = sSort.instantiate([uSort]) - assert siSort.isUninterpretedSortParameterized() - bvSort = solver.mkBitVectorSort(32) - with pytest.raises(RuntimeError): - bvSort.isUninterpretedSortParameterized() - - def test_get_uninterpreted_sort_paramsorts(solver): uSort = solver.mkUninterpretedSort("u") uSort.getUninterpretedSortParamSorts() -- 2.30.2