From 748c884353be09ae4fb69642ce3e13ad4cdf624c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 25 Mar 2022 22:40:42 -0700 Subject: [PATCH] api: Rename *SortConstructor* to *UninterpretedSortConstructor*. (#8406) --- docs/api/java/CMakeLists.txt | 1 - src/api/cpp/cvc5.cpp | 12 +++---- src/api/cpp/cvc5.h | 34 ++++++++++++++----- src/api/java/io/github/cvc5/api/Solver.java | 14 +++++--- src/api/java/io/github/cvc5/api/Sort.java | 23 ++++++++----- src/api/java/jni/solver.cpp | 9 ++--- src/api/java/jni/sort.cpp | 20 ++++++----- src/api/python/cvc5.pxd | 6 ++-- src/api/python/cvc5.pxi | 29 +++++++++++----- src/expr/symbol_table.cpp | 2 +- src/parser/parser.cpp | 8 +++-- test/unit/api/cpp/datatype_api_black.cpp | 4 +-- .../api/cpp/parametric_datatype_black.cpp | 4 +-- test/unit/api/cpp/solver_black.cpp | 9 ++--- test/unit/api/cpp/sort_black.cpp | 20 +++++------ test/unit/api/java/DatatypeTest.java | 4 +-- test/unit/api/java/SolverTest.java | 8 ++--- test/unit/api/java/SortTest.java | 20 +++++------ test/unit/api/python/test_datatype_api.py | 4 +-- test/unit/api/python/test_solver.py | 6 ++-- test/unit/api/python/test_sort.py | 18 +++++----- 21 files changed, 151 insertions(+), 104 deletions(-) diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 974f15e0f..2fcf74767 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -33,7 +33,6 @@ if(BUILD_BINDINGS_JAVA) -cp ${CVC5_JAR_FILE} -tag "apiNote:a:Note:" -notimestamp - --no-module-directories COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's///' {} "\;" COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete DEPENDS cvc5jar ${CVC5_JAR_FILE} diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 7c39e991c..b73920182 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1365,7 +1365,7 @@ bool Sort::isUninterpretedSort() const CVC5_API_TRY_CATCH_END; } -bool Sort::isSortConstructor() const +bool Sort::isUninterpretedSortConstructor() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line @@ -1395,7 +1395,7 @@ Sort Sort::instantiate(const std::vector& params) const CVC5_API_CHECK(!d_type->isParametricDatatype() || d_type->getNumChildren() == params.size() + 1) << "Arity mismatch for instantiated parametric datatype"; - CVC5_API_CHECK(!isSortConstructor() + CVC5_API_CHECK(!d_type->isSortConstructor() || d_type->getSortConstructorArity() == params.size()) << "Arity mismatch for instantiated sort constructor"; //////// all checks before this line @@ -1674,11 +1674,11 @@ std::vector Sort::getUninterpretedSortParamSorts() const /* Sort constructor sort ----------------------------------------------- */ -size_t Sort::getSortConstructorArity() const +size_t Sort::getUninterpretedSortConstructorArity() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isSortConstructor()) << "Not a sort constructor sort."; + CVC5_API_CHECK(d_type->isSortConstructor()) << "Not a sort constructor sort."; //////// all checks before this line return d_type->getSortConstructorArity(); //////// @@ -5600,8 +5600,8 @@ Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const CVC5_API_TRY_CATCH_END; } -Sort Solver::mkSortConstructorSort(const std::string& symbol, - size_t arity) const +Sort Solver::mkUninterpretedSortConstructorSort(const std::string& symbol, + size_t arity) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0"; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index f2156f13b..e2f3d943a 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -584,10 +584,14 @@ class CVC5_EXPORT Sort bool isUninterpretedSort() const; /** - * Is this a sort constructor kind? + * Is this an uninterpreted sort constructor kind? + * + * An uninterpreted sort constructor has arity > 0 and can be instantiated to + * construct uninterpreted sorts with given sort parameters. + * * @return true if this is a sort constructor kind */ - bool isSortConstructor() const; + bool isUninterpretedSortConstructor() const; /** * @return the underlying datatype of a datatype sort @@ -595,8 +599,11 @@ class CVC5_EXPORT Sort Datatype getDatatype() const; /** - * Instantiate a parameterized datatype/sort sort. + * Instantiate a parameterized datatype sort or uninterpreted sort + * constructor sort. + * * Create sorts parameter with Solver::mkParamSort(). + * * @param params the list of sort parameters to instantiate with */ Sort instantiate(const std::vector& params) const; @@ -753,9 +760,9 @@ class CVC5_EXPORT Sort /* Sort constructor sort ----------------------------------------------- */ /** - * @return the arity of a sort constructor sort + * @return the arity of an uninterpreted sort constructor sort */ - size_t getSortConstructorArity() const; + size_t getUninterpretedSortConstructorArity() const; /* Bit-vector sort ----------------------------------------------------- */ @@ -3282,12 +3289,16 @@ class CVC5_EXPORT Solver Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const; /** - * Create a sort constructor sort. + * Create an uninterpreted sort constructor sort. + * + * An uninterpreted sort constructor is an uninterpreted sort with arity > 0. + * * @param symbol the symbol of the sort - * @param arity the arity of the sort - * @return the sort constructor sort + * @param arity the arity of the sort (must be > 0) + * @return the uninterpreted sort constructor sort */ - Sort mkSortConstructorSort(const std::string& symbol, size_t arity) const; + Sort mkUninterpretedSortConstructorSort(const std::string& symbol, + size_t arity) const; /** * Create a tuple sort. @@ -3820,6 +3831,11 @@ class CVC5_EXPORT Solver * (declare-sort ) * \endverbatim * + * @note This corresponds to mkUninterpretedSort(const std::string&) const if + * arity = 0, and to + * mkUninterpretedSortConstructorSort(const std::string&, size_t arity) const + * if arity > 0. + * * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 01fe033b4..5b462bc2f 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -464,19 +464,23 @@ public class Solver implements IPointer, AutoCloseable /** * Create a sort constructor sort. + * + * An uninterpreted sort constructor is an uninterpreted sort with + * arity > 0. + * * @param symbol the symbol of the sort - * @param arity the arity of the sort + * @param arity the arity of the sort (must be > 0) * @return the sort constructor sort * @throws CVC5ApiException */ - public Sort mkSortConstructorSort(String symbol, int arity) throws CVC5ApiException + public Sort mkUninterpretedSortConstructorSort(String symbol, int arity) throws CVC5ApiException { Utils.validateUnsigned(arity, "arity"); - long sortPointer = mkSortConstructorSort(pointer, symbol, arity); + long sortPointer = mkUninterpretedSortConstructorSort(pointer, symbol, arity); return new Sort(this, sortPointer); } - private native long mkSortConstructorSort(long pointer, String symbol, int arity); + private native long mkUninterpretedSortConstructorSort(long pointer, String symbol, int arity); /** * Create a tuple sort. @@ -1555,6 +1559,8 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( declare-sort ) * } + * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and + * to mkUninterpretedSortConstructorSort() const if arity > 0. * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index e600fbaeb..bf85107f6 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -345,15 +345,19 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isUninterpretedSort(long pointer); /** - * Is this a sort constructor kind? + * Is this an uninterpreted sort constructor kind? + * + * An uninterpreted sort constructor is an uninterpreted sort with arity + * > 0. + * * @return true if this is a sort constructor kind */ - public boolean isSortConstructor() + public boolean isUninterpretedSortConstructor() { - return isSortConstructor(pointer); + return isUninterpretedSortConstructor(pointer); } - private native boolean isSortConstructor(long pointer); + private native boolean isUninterpretedSortConstructor(long pointer); /** * @return the underlying datatype of a datatype sort @@ -367,7 +371,8 @@ public class Sort extends AbstractPointer implements Comparable private native long getDatatype(long pointer); /** - * Instantiate a parameterized datatype/sort sort. + * Instantiate a parameterized datatype sort or uninterpreted sort + * constructor sort. * Create sorts parameter with Solver.mkParamSort(). * @param params the list of sort parameters to instantiate with */ @@ -647,14 +652,14 @@ public class Sort extends AbstractPointer implements Comparable /* Sort constructor sort ----------------------------------------------- */ /** - * @return the arity of a sort constructor sort + * @return the arity of an uninterpreted sort constructor sort */ - public int getSortConstructorArity() + public int getUninterpretedSortConstructorArity() { - return getSortConstructorArity(pointer); + return getUninterpretedSortConstructorArity(pointer); } - private native int getSortConstructorArity(long pointer); + private native int getUninterpretedSortConstructorArity(long pointer); /* Bit-vector sort ----------------------------------------------------- */ diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 718d63da8..7eccbf260 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -482,10 +482,11 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUnresolvedSort( /* * Class: io_github_cvc5_api_Solver - * Method: mkSortConstructorSort + * Method: mkUninterpretedSortConstructorSort * Signature: (JLjava/lang/String;I)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort( +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_api_Solver_mkUninterpretedSortConstructorSort( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -493,8 +494,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkSortConstructorSort( Solver* solver = reinterpret_cast(pointer); const char* s = env->GetStringUTFChars(jSymbol, nullptr); std::string cSymbol(s); - Sort* retPointer = - new Sort(solver->mkSortConstructorSort(cSymbol, (size_t)arity)); + Sort* retPointer = new Sort( + solver->mkUninterpretedSortConstructorSort(cSymbol, (size_t)arity)); env->ReleaseStringUTFChars(jSymbol, s); return reinterpret_cast(retPointer); diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index 12ce60ae0..a3d1f135f 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -440,15 +440,17 @@ JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isUninterpretedSort( /* * Class: io_github_cvc5_api_Sort - * Method: isSortConstructor + * Method: isUninterpretedSortConstructor * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Sort_isSortConstructor( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Sort_isUninterpretedSortConstructor(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->isSortConstructor()); + return static_cast(current->isUninterpretedSortConstructor()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } @@ -866,15 +868,17 @@ Java_io_github_cvc5_api_Sort_getUninterpretedSortParamSorts(JNIEnv* env, /* * Class: io_github_cvc5_api_Sort - * Method: getSortConstructorArity + * Method: getUninterpretedSortConstructorArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_io_github_cvc5_api_Sort_getSortConstructorArity( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jint JNICALL +Java_io_github_cvc5_api_Sort_getUninterpretedSortConstructorArity(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getSortConstructorArity()); + return static_cast(current->getUninterpretedSortConstructorArity()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 4f482da9e..b5cbdf7cc 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -234,7 +234,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort mkSequenceSort(Sort elemSort) except + Sort mkUninterpretedSort(const string& symbol) except + Sort mkUnresolvedSort(const string& symbol, size_t arity) except + - Sort mkSortConstructorSort(const string& symbol, size_t arity) except + + Sort mkUninterpretedSortConstructorSort(const string& symbol, size_t arity) except + Sort mkTupleSort(const vector[Sort]& sorts) except + Term mkTerm(Op op) except + Term mkTerm(Op op, const vector[Term]& children) except + @@ -398,7 +398,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isBag() except + bint isSequence() except + bint isUninterpretedSort() except + - bint isSortConstructor() except + + bint isUninterpretedSortConstructor() except + Datatype getDatatype() except + Sort instantiate(const vector[Sort]& params) except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + @@ -419,7 +419,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort getSequenceElementSort() except + bint isUninterpretedSortParameterized() except + vector[Sort] getUninterpretedSortParamSorts() except + - size_t getSortConstructorArity() except + + size_t getUninterpretedSortConstructorArity() except + uint32_t getBitVectorSize() except + uint32_t getFloatingPointExponentSize() except + uint32_t getFloatingPointSignificandSize() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 18e6a1e79..09749b3d5 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -988,15 +988,19 @@ cdef class Solver: sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity) return sort - def mkSortConstructorSort(self, str symbol, size_t arity): + def mkUninterpretedSortConstructorSort(self, str symbol, size_t arity): """Create a sort constructor sort. + An uninterpreted sort constructor is an uninterpreted sort with + arity > 0. + :param symbol: the symbol of the sort - :param arity: the arity of the sort + :param arity: the arity of the sort (must be > 0) :return: the sort constructor sort """ cdef Sort sort = Sort(self) - sort.csort =self.csolver.mkSortConstructorSort(symbol.encode(), arity) + sort.csort = self.csolver.mkUninterpretedSortConstructorSort( + symbol.encode(), arity) return sort @expand_list_arg(num_req_args=0) @@ -1830,6 +1834,11 @@ cdef class Solver: ( declare-sort ) + .. note:: + This corresponds to :py:meth:`Solver.mkUninterpretedSort()` if + arity = 0, and to + :py:meth:`Solver.mkUninterpretedSortConstructorSort()` if arity > 0. + :param symbol: the name of the sort :param arity: the arity of the sort :return: the sort @@ -2749,13 +2758,16 @@ cdef class Sort: """ return self.csort.isUninterpretedSort() - def isSortConstructor(self): + def isUninterpretedSortConstructor(self): """ Is this a sort constructor kind? + An uninterpreted sort constructor is an uninterpreted sort with + arity > 0. + :return: True if this a sort constructor kind. """ - return self.csort.isSortConstructor() + return self.csort.isUninterpretedSortConstructor() def getDatatype(self): """ @@ -2767,7 +2779,8 @@ cdef class Sort: def instantiate(self, params): """ - Instantiate a parameterized datatype/sort sort. + Instantiate a parameterized datatype sort or uninterpreted sort + constructor sort. Create sorts parameter with :py:meth:`Solver.mkParamSort()` :param params: the list of sort parameters to instantiate with @@ -2965,11 +2978,11 @@ cdef class Sort: param_sorts.append(sort) return param_sorts - def getSortConstructorArity(self): + def getUninterpretedSortConstructorArity(self): """ :return: the arity of a sort constructor sort """ - return self.csort.getSortConstructorArity() + return self.csort.getUninterpretedSortConstructorArity() def getBitVectorSize(self): """ diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 7aabb2055..1b0e679ca 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -490,7 +490,7 @@ api::Sort SymbolTable::Implementation::lookupType( "expected parametric datatype"); return p.second.instantiate(params); } - bool isSortConstructor = p.second.isSortConstructor(); + bool isSortConstructor = p.second.isUninterpretedSortConstructor(); if (TraceIsOn("sort")) { Trace("sort") << "instantiating using a sort " diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 9c3877265..a7bf82fb7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -317,7 +317,7 @@ api::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) { Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - api::Sort type = d_solver->mkSortConstructorSort(name, arity); + api::Sort type = d_solver->mkUninterpretedSortConstructorSort(name, arity); defineType(name, vector(arity), type); return type; } @@ -333,7 +333,8 @@ api::Sort Parser::mkUnresolvedType(const std::string& name) api::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - api::Sort unresolved = d_solver->mkSortConstructorSort(name, arity); + api::Sort unresolved = + d_solver->mkUninterpretedSortConstructorSort(name, arity); defineType(name, vector(arity), unresolved); d_unresolved.insert(unresolved); return unresolved; @@ -344,7 +345,8 @@ api::Sort Parser::mkUnresolvedTypeConstructor( { Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - api::Sort unresolved = d_solver->mkSortConstructorSort(name, params.size()); + api::Sort unresolved = + d_solver->mkUninterpretedSortConstructorSort(name, params.size()); defineType(name, params, unresolved); api::Sort t = getSort(name, params); d_unresolved.insert(unresolved); diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index c783f2fa2..79956f679 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -483,7 +483,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ unresTypes.clear(); - Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1); unresTypes.insert(unresList5); std::vector v; @@ -522,7 +522,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) */ // Make unresolved types as placeholders std::set unresTypes; - Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1); unresTypes.insert(unresList); std::vector v; diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp index 6c4bb80e9..219f007ec 100644 --- a/test/unit/api/cpp/parametric_datatype_black.cpp +++ b/test/unit/api/cpp/parametric_datatype_black.cpp @@ -30,8 +30,8 @@ TEST_F(TestApiBlackParametricDatatype, proj_issue387) { Sort s1 = d_solver.getBooleanSort(); - Sort u1 = d_solver.mkSortConstructorSort("_x0", 1); - Sort u2 = d_solver.mkSortConstructorSort("_x1", 1); + Sort u1 = d_solver.mkUninterpretedSortConstructorSort("_x0", 1); + Sort u2 = d_solver.mkUninterpretedSortConstructorSort("_x1", 1); Sort p1 = d_solver.mkParamSort("_x4"); Sort p2 = d_solver.mkParamSort("_x27"); Sort p3 = d_solver.mkParamSort("_x3"); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index e32f4a8e9..717865c71 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -361,11 +361,12 @@ TEST_F(TestApiBlackSolver, mkUnresolvedSort) ASSERT_NO_THROW(d_solver.mkUnresolvedSort("", 1)); } -TEST_F(TestApiBlackSolver, mkSortConstructorSort) +TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort) { - ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2)); - ASSERT_NO_THROW(d_solver.mkSortConstructorSort("", 2)); - ASSERT_THROW(d_solver.mkSortConstructorSort("", 0), CVC5ApiException); + ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("s", 2)); + ASSERT_NO_THROW(d_solver.mkUninterpretedSortConstructorSort("", 2)); + ASSERT_THROW(d_solver.mkUninterpretedSortConstructorSort("", 0), + CVC5ApiException); } TEST_F(TestApiBlackSolver, mkTupleSort) diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 40e00d996..d14d2f4a1 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -246,11 +246,11 @@ TEST_F(TestApiBlackSort, isUninterpreted) ASSERT_NO_THROW(Sort().isUninterpretedSort()); } -TEST_F(TestApiBlackSort, isSortConstructor) +TEST_F(TestApiBlackSort, isUninterpretedSortConstructor) { - Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1); - ASSERT_TRUE(sc_sort.isSortConstructor()); - ASSERT_NO_THROW(Sort().isSortConstructor()); + Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1); + ASSERT_TRUE(sc_sort.isUninterpretedSortConstructor()); + ASSERT_NO_THROW(Sort().isUninterpretedSortConstructor()); } TEST_F(TestApiBlackSort, getDatatype) @@ -410,7 +410,7 @@ TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) { Sort uSort = d_solver.mkUninterpretedSort("u"); ASSERT_FALSE(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkSortConstructorSort("s", 1); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); Sort siSort = sSort.instantiate({uSort}); ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); Sort bvSort = d_solver.mkBitVectorSort(32); @@ -421,7 +421,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) { Sort uSort = d_solver.mkUninterpretedSort("u"); ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts()); - Sort sSort = d_solver.mkSortConstructorSort("s", 2); + 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); @@ -430,7 +430,7 @@ TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) { - Sort sSort = d_solver.mkSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); ASSERT_NO_THROW(sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); ASSERT_THROW(bvSort.getSymbol(), CVC5ApiException); @@ -438,10 +438,10 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) { - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - ASSERT_NO_THROW(sSort.getSortConstructorArity()); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + ASSERT_NO_THROW(sSort.getUninterpretedSortConstructorArity()); Sort bvSort = d_solver.mkBitVectorSort(32); - ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); + ASSERT_THROW(bvSort.getUninterpretedSortConstructorArity(), CVC5ApiException); } TEST_F(TestApiBlackSort, getBitVectorSize) diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 74e4e1ceb..8e05cb164 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -464,7 +464,7 @@ class DatatypeTest * END; */ unresTypes.clear(); - Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort("list5", 1); unresTypes.add(unresList5); List v = new ArrayList<>(); @@ -504,7 +504,7 @@ class DatatypeTest */ // Make unresolved types as placeholders Set unresTypes = new HashSet<>(); - Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + Sort unresList = d_solver.mkUninterpretedSortConstructorSort("plist", 1); unresTypes.add(unresList); List v = new ArrayList<>(); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 5c759b9ea..77cd3b09f 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -342,11 +342,11 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1)); } - @Test void mkSortConstructorSort() throws CVC5ApiException + @Test void mkUninterpretedSortConstructorSort() throws CVC5ApiException { - assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("s", 2)); - assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("", 2)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkSortConstructorSort("", 0)); + assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("s", 2)); + assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("", 2)); + assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort("", 0)); } @Test void mkTupleSort() throws CVC5ApiException diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 87016a0e3..0455f207a 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -238,11 +238,11 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSort()); } - @Test void isSortConstructor() throws CVC5ApiException + @Test void isUninterpretedSortSortConstructor() throws CVC5ApiException { - Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1); - assertTrue(sc_sort.isSortConstructor()); - assertDoesNotThrow(() -> d_solver.getNullSort().isSortConstructor()); + Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1); + assertTrue(sc_sort.isUninterpretedSortConstructor()); + assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSortConstructor()); } @Test void getDatatype() throws CVC5ApiException @@ -400,7 +400,7 @@ class SortTest { Sort uSort = d_solver.mkUninterpretedSort("u"); assertFalse(uSort.isUninterpretedSortParameterized()); - Sort sSort = d_solver.mkSortConstructorSort("s", 1); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 1); Sort siSort = sSort.instantiate(new Sort[] {uSort}); assertTrue(siSort.isUninterpretedSortParameterized()); Sort bvSort = d_solver.mkBitVectorSort(32); @@ -411,7 +411,7 @@ class SortTest { Sort uSort = d_solver.mkUninterpretedSort("u"); assertDoesNotThrow(() -> uSort.getUninterpretedSortParamSorts()); - Sort sSort = d_solver.mkSortConstructorSort("s", 2); + 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); @@ -420,7 +420,7 @@ class SortTest @Test void getUninterpretedSortConstructorName() throws CVC5ApiException { - Sort sSort = d_solver.mkSortConstructorSort("s", 2); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); assertDoesNotThrow(() -> sSort.getSymbol()); Sort bvSort = d_solver.mkBitVectorSort(32); assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); @@ -428,10 +428,10 @@ class SortTest @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException { - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - assertDoesNotThrow(() -> sSort.getSortConstructorArity()); + Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); + assertDoesNotThrow(() -> sSort.getUninterpretedSortConstructorArity()); Sort bvSort = d_solver.mkBitVectorSort(32); - assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity()); + assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortConstructorArity()); } @Test void getBitVectorSize() throws CVC5ApiException diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 89b307bf7..5b2ac50b5 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -466,7 +466,7 @@ def test_datatype_simply_rec(solver): # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil # END unresTypes.clear() - unresList5 = solver.mkSortConstructorSort("list5", 1) + unresList5 = solver.mkUninterpretedSortConstructorSort("list5", 1) unresTypes.add(unresList5) v = [] @@ -503,7 +503,7 @@ def test_datatype_specialized_cons(solver): # Make unresolved types as placeholders unresTypes = set([]) - unresList = solver.mkSortConstructorSort("plist", 1) + unresList = solver.mkUninterpretedSortConstructorSort("plist", 1) unresTypes.add(unresList) v = [] diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index de82dd1a4..ca3862819 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -300,10 +300,10 @@ def test_mk_unresolved_sort(solver): def test_mk_sort_constructor_sort(solver): - solver.mkSortConstructorSort("s", 2) - solver.mkSortConstructorSort("", 2) + solver.mkUninterpretedSortConstructorSort("s", 2) + solver.mkUninterpretedSortConstructorSort("", 2) with pytest.raises(RuntimeError): - solver.mkSortConstructorSort("", 0) + solver.mkUninterpretedSortConstructorSort("", 0) def test_mk_tuple_sort(solver): diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 83c60b312..b530f2c37 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -222,9 +222,9 @@ def test_is_uninterpreted(solver): def test_is_sort_constructor(solver): - sc_sort = solver.mkSortConstructorSort("asdf", 1) - assert sc_sort.isSortConstructor() - Sort(solver).isSortConstructor() + sc_sort = solver.mkUninterpretedSortConstructorSort("asdf", 1) + assert sc_sort.isUninterpretedSortConstructor() + Sort(solver).isUninterpretedSortConstructor() def test_get_datatype(solver): @@ -387,7 +387,7 @@ def test_get_uninterpreted_sort_name(solver): def test_is_uninterpreted_sort_parameterized(solver): uSort = solver.mkUninterpretedSort("u") assert not uSort.isUninterpretedSortParameterized() - sSort = solver.mkSortConstructorSort("s", 1) + sSort = solver.mkUninterpretedSortConstructorSort("s", 1) siSort = sSort.instantiate([uSort]) assert siSort.isUninterpretedSortParameterized() bvSort = solver.mkBitVectorSort(32) @@ -398,7 +398,7 @@ def test_is_uninterpreted_sort_parameterized(solver): def test_get_uninterpreted_sort_paramsorts(solver): uSort = solver.mkUninterpretedSort("u") uSort.getUninterpretedSortParamSorts() - sSort = solver.mkSortConstructorSort("s", 2) + sSort = solver.mkUninterpretedSortConstructorSort("s", 2) siSort = sSort.instantiate([uSort, uSort]) assert len(siSort.getUninterpretedSortParamSorts()) == 2 bvSort = solver.mkBitVectorSort(32) @@ -407,7 +407,7 @@ def test_get_uninterpreted_sort_paramsorts(solver): def test_get_uninterpreted_sort_constructor_name(solver): - sSort = solver.mkSortConstructorSort("s", 2) + sSort = solver.mkUninterpretedSortConstructorSort("s", 2) sSort.getSymbol() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): @@ -415,11 +415,11 @@ def test_get_uninterpreted_sort_constructor_name(solver): def test_get_uninterpreted_sort_constructor_arity(solver): - sSort = solver.mkSortConstructorSort("s", 2) - sSort.getSortConstructorArity() + sSort = solver.mkUninterpretedSortConstructorSort("s", 2) + sSort.getUninterpretedSortConstructorArity() bvSort = solver.mkBitVectorSort(32) with pytest.raises(RuntimeError): - bvSort.getSortConstructorArity() + bvSort.getUninterpretedSortConstructorArity() def test_get_bv_size(solver): -- 2.30.2