From 430c11f8794c02fb45f413596bc7929d44c0ee35 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Apr 2022 18:23:18 -0500 Subject: [PATCH] Simplifications to the datatypes API (#8511) This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes. API Changes: (1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors. (2) adds to unit test examples that use this variant instead of using unresolved sorts. (3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental. Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet. Followup PR will add to documentation on elaborate further on how to use the datatypes API. --- src/api/cpp/cvc5.cpp | 63 +++---- src/api/cpp/cvc5.h | 56 ++---- .../github/cvc5/DatatypeConstructorDecl.java | 15 ++ src/api/java/io/github/cvc5/Solver.java | 80 +-------- .../java/jni/datatype_constructor_decl.cpp | 29 ++- src/api/java/jni/solver.cpp | 34 +--- src/api/python/cvc5.pxd | 6 +- src/api/python/cvc5.pxi | 39 ++-- src/parser/parser.cpp | 6 +- test/unit/api/cpp/datatype_api_black.cpp | 99 +++++++---- test/unit/api/cpp/solver_black.cpp | 24 ++- test/unit/api/java/DatatypeTest.java | 166 +++++++++++------- test/unit/api/java/SolverTest.java | 26 ++- test/unit/api/python/test_datatype_api.py | 96 ++++++---- test/unit/api/python/test_solver.py | 27 ++- 15 files changed, 375 insertions(+), 391 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b4cc4cab2..89cd72f3f 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3396,6 +3396,20 @@ void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) CVC5_API_TRY_CATCH_END; } +void DatatypeConstructorDecl::addSelectorUnresolved( + const std::string& name, const std::string& unresDataypeName) +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + //////// all checks before this line + // make the unresolved sort with the given name + internal::TypeNode usort = + d_solver->getNodeManager()->mkUnresolvedDatatypeSort(unresDataypeName); + d_ctor->addArg(name, usort); + //////// + CVC5_API_TRY_CATCH_END; +} + bool DatatypeConstructorDecl::isNull() const { CVC5_API_TRY_CATCH_BEGIN; @@ -4415,7 +4429,6 @@ Sort Grammar::resolve() } std::vector datatypes; - std::set unresTypes; datatypes.reserve(d_ntSyms.size()); @@ -4447,7 +4460,6 @@ Sort Grammar::resolve() << " produced an empty rule list"; datatypes.push_back(*dtDecl.d_dtype); - unresTypes.insert(*ntsToUnres[ntSym].d_type); } std::vector datatypeTypes = @@ -5155,26 +5167,6 @@ Term Solver::mkTermHelper(const Op& op, const std::vector& children) const return Term(this, res); } -std::vector Solver::mkDatatypeSortsInternal( - const std::vector& dtypedecls, - const std::set& unresolvedSorts) const -{ - // Note: dtypedecls and unresolvedSorts are checked in the caller to avoid - // double checks - //////// all checks before this line - - std::vector datatypes; - for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) - { - datatypes.push_back(dtypedecls[i].getDatatype()); - } - - std::vector dtypes = - getNodeManager()->mkMutualDatatypeTypes(datatypes); - std::vector retTypes = Sort::typeNodeVectorToSorts(this, dtypes); - return retTypes; -} - Term Solver::synthFunHelper(const std::string& symbol, const std::vector& boundVars, const Sort& sort, @@ -5493,20 +5485,15 @@ std::vector Solver::mkDatatypeSorts( CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls); CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return mkDatatypeSortsInternal(dtypedecls, {}); - //////// - CVC5_API_TRY_CATCH_END; -} - -std::vector Solver::mkDatatypeSorts( - const std::vector& dtypedecls, - const std::set& unresolvedSorts) const -{ - CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls); - CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts); - //////// all checks before this line - return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts); + std::vector datatypes; + for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i) + { + datatypes.push_back(dtypedecls[i].getDatatype()); + } + std::vector dtypes = + getNodeManager()->mkMutualDatatypeTypes(datatypes); + std::vector retTypes = Sort::typeNodeVectorToSorts(this, dtypes); + return retTypes; //////// CVC5_API_TRY_CATCH_END; } @@ -5531,7 +5518,6 @@ Sort Solver::mkParamSort(const std::optional& symbol) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - internal::TypeNode tn = symbol ? getNodeManager()->mkSort(*symbol) : getNodeManager()->mkSort(); return Sort(this, tn); @@ -5615,7 +5601,8 @@ Sort Solver::mkUninterpretedSort(const std::optional& symbol) const CVC5_API_TRY_CATCH_END; } -Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const +Sort Solver::mkUnresolvedDatatypeSort(const std::string& symbol, + size_t arity) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 2ad9d41c2..9efd98587 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1761,6 +1761,17 @@ class CVC5_EXPORT DatatypeConstructorDecl */ void addSelectorSelf(const std::string& name); + /** + * Add datatype selector declaration whose codomain sort is an unresolved + * datatype with the given name. + * @param name the name of the datatype selector declaration to add + * @param unresDataypeName the name of the unresolved datatype. The codomain + * of the selector will be the resolved datatype with + * the given name. + */ + void addSelectorUnresolved(const std::string& name, + const std::string& unresDataypeName); + /** * @return true if this DatatypeConstructorDecl is a null declaration. */ @@ -2635,8 +2646,6 @@ class CVC5_EXPORT Grammar * with bound variables via purifySygusGTerm, and binding these variables * via a lambda. * - * @note Create unresolved sorts with Solver::mkUnresolvedSort(). - * * @param dt the non-terminal's datatype to which a constructor is added * @param term the sygus operator of the constructor * @param ntsToUnres mapping from non-terminals to their unresolved sorts @@ -3177,30 +3186,6 @@ class CVC5_EXPORT Solver std::vector mkDatatypeSorts( const std::vector& dtypedecls) const; - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * This method is called when the DatatypeDecl objects dtypedecls have been - * built using "unresolved" sorts. - * - * We associate each sort in unresolvedSorts with exactly one datatype from - * dtypedecls. In particular, it must have the same name as exactly one - * datatype declaration in dtypedecls. - * - * When constructing datatypes, unresolved sorts are replaced by the datatype - * sort constructed for the datatype declaration it is associated with. - * - * @note Create unresolved sorts with Solver::mkUnresolvedSort(). - * - * @param dtypedecls the datatype declarations from which the sort is created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - std::vector mkDatatypeSorts( - const std::vector& dtypedecls, - const std::set& unresolvedSorts) const; - /** * Create function sort. * @param sorts the sort of the function arguments @@ -3269,16 +3254,19 @@ class CVC5_EXPORT Solver const std::optional& symbol = std::nullopt) const; /** - * Create an unresolved sort. + * Create an unresolved datatype sort. * * This is for creating yet unresolved sort placeholders for mutually - * recursive datatypes. + * recursive parametric datatypes. * * @param symbol the symbol of the sort * @param arity the number of sort parameters of the sort * @return the unresolved sort + * + * @warning This method is experimental and may change in future versions. */ - Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const; + Sort mkUnresolvedDatatypeSort(const std::string& symbol, + size_t arity = 0) const; /** * Create an uninterpreted sort constructor sort. @@ -4914,16 +4902,6 @@ class CVC5_EXPORT Solver */ Term mkTermHelper(const Op& op, const std::vector& children) const; - /** - * Create a vector of datatype sorts, using unresolved sorts. - * @param dtypedecls the datatype declarations from which the sort is created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - std::vector mkDatatypeSortsInternal( - const std::vector& dtypedecls, - const std::set& unresolvedSorts) const; - /** * Synthesize n-ary function following specified syntactic constraints. * diff --git a/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java index 45e79f1f1..b4e755781 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java @@ -56,6 +56,21 @@ public class DatatypeConstructorDecl extends AbstractPointer private native void addSelectorSelf(long pointer, String name); + /** + * Add datatype selector declaration whose codomain sort is an unresolved + * datatype with the given name. + * @param name the name of the datatype selector declaration to add + * @param unresDataypeName the name of the unresolved datatype. The codomain + * of the selector will be the resolved datatype with + * the given name. + */ + public void addSelectorUnresolved(String name, String unresDataypeName) + { + addSelectorUnresolved(pointer, name, unresDataypeName); + } + + private native void addSelectorUnresolved(long pointer, String name, String unresDataypeName); + /** * @return true if this DatatypeConstructorDecl is a null declaration. */ diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java index 23ad027e4..9fcb261d3 100644 --- a/src/api/java/io/github/cvc5/Solver.java +++ b/src/api/java/io/github/cvc5/Solver.java @@ -247,70 +247,6 @@ public class Solver implements IPointer, AutoCloseable private native long[] mkDatatypeSorts(long pointer, long[] declPointers) throws CVC5ApiException; - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * This method is called when the DatatypeDecl objects dtypedecls have - * been built using "unresolved" sorts. - * - * We associate each sort in unresolvedSorts with exacly one datatype from - * dtypedecls. In particular, it must have the same name as exactly one - * datatype declaration in dtypedecls. - * - * When constructing datatypes, unresolved sorts are replaced by the - * datatype sort constructed for the datatype declaration it is associated - * with. - * - * @api.note Create unresolved sorts with Solver::mkUnresolvedSort(). - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @param unresolvedSorts the set of unresolved sorts - * @return the datatype sorts - * @throws CVC5ApiException - */ - public List mkDatatypeSorts(List dtypedecls, Set unresolvedSorts) - throws CVC5ApiException - { - Sort[] array = mkDatatypeSorts( - dtypedecls.toArray(new DatatypeDecl[0]), unresolvedSorts.toArray(new Sort[0])); - return Arrays.asList(array); - } - - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * This method is called when the DatatypeDecl objects dtypedecls have - * been built using "unresolved" sorts. - * - * We associate each sort in unresolvedSorts with exacly one datatype from - * dtypedecls. In particular, it must have the same name as exactly one - * datatype declaration in dtypedecls. - * - * When constructing datatypes, unresolved sorts are replaced by the - * datatype sort constructed for the datatype declaration it is associated - * with. - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls, Sort[] unresolvedSorts) - throws CVC5ApiException - { - long[] declPointers = Utils.getPointers(dtypedecls); - long[] unresolvedPointers = Utils.getPointers(unresolvedSorts); - long[] sortPointers = mkDatatypeSorts(pointer, declPointers, unresolvedPointers); - Sort[] sorts = Utils.getSorts(this, sortPointers); - return sorts; - } - - private native long[] mkDatatypeSorts( - long pointer, long[] declPointers, long[] unresolvedPointers) throws CVC5ApiException; - /** * Create function sort. * @param domain the sort of the fuction argument @@ -460,27 +396,27 @@ public class Solver implements IPointer, AutoCloseable private native long mkUninterpretedSort(long pointer); /** - * Create an unresolved sort. + * Create an unresolved datatype sort. * * This is for creating yet unresolved sort placeholders for mutually - * recursive datatypes. + * recursive parametric datatypes. * * @param symbol the symbol of the sort * @param arity the number of sort parameters of the sort * @return the unresolved sort * @throws CVC5ApiException */ - public Sort mkUnresolvedSort(String symbol, int arity) throws CVC5ApiException + public Sort mkUnresolvedDatatypeSort(String symbol, int arity) throws CVC5ApiException { Utils.validateUnsigned(arity, "arity"); - long sortPointer = mkUnresolvedSort(pointer, symbol, arity); + long sortPointer = mkUnresolvedDatatypeSort(pointer, symbol, arity); return new Sort(this, sortPointer); } - private native long mkUnresolvedSort(long pointer, String symbol, int arity); + private native long mkUnresolvedDatatypeSort(long pointer, String symbol, int arity); /** - * Create an unresolved sort. + * Create an unresolved datatype sort. * * This is for creating yet unresolved sort placeholders for mutually * recursive datatypes without sort parameters. @@ -489,9 +425,9 @@ public class Solver implements IPointer, AutoCloseable * @return the unresolved sort * @throws CVC5ApiException */ - public Sort mkUnresolvedSort(String symbol) throws CVC5ApiException + public Sort mkUnresolvedDatatypeSort(String symbol) throws CVC5ApiException { - return mkUnresolvedSort(symbol, 0); + return mkUnresolvedDatatypeSort(symbol, 0); } /** diff --git a/src/api/java/jni/datatype_constructor_decl.cpp b/src/api/java/jni/datatype_constructor_decl.cpp index 3c35c22a8..7197dd267 100644 --- a/src/api/java/jni/datatype_constructor_decl.cpp +++ b/src/api/java/jni/datatype_constructor_decl.cpp @@ -65,8 +65,33 @@ Java_io_github_cvc5_DatatypeConstructorDecl_addSelectorSelf(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer; const char* s = env->GetStringUTFChars(jName, nullptr); - std::string cName(s); - current->addSelectorSelf(cName); + std::string sName(s); + current->addSelectorSelf(sName); + env->ReleaseStringUTFChars(jName, s); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: io_github_cvc5_DatatypeConstructorDecl + * Method: addSelectorUnresolved + * Signature: (JLjava/lang/String;Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL +Java_io_github_cvc5_DatatypeConstructorDecl_addSelectorUnresolved( + JNIEnv* env, + jobject, + jlong pointer, + jstring jName, + jstring jUnresDataypeName) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + DatatypeConstructorDecl* current = (DatatypeConstructorDecl*)pointer; + const char* s = env->GetStringUTFChars(jName, nullptr); + std::string sName(s); + const char* du = env->GetStringUTFChars(jUnresDataypeName, nullptr); + std::string duName(du); + current->addSelectorUnresolved(sName, duName); + env->ReleaseStringUTFChars(jUnresDataypeName, du); env->ReleaseStringUTFChars(jName, s); CVC5_JAVA_API_TRY_CATCH_END(env); } diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 4bf41d335..c39d732ad 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -221,7 +221,7 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkDatatypeSort( * Signature: (J[J)[J */ JNIEXPORT jlongArray JNICALL -Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J(JNIEnv* env, +Java_io_github_cvc5_Solver_mkDatatypeSorts(JNIEnv* env, jobject, jlong pointer, jlongArray jDecls) @@ -244,31 +244,6 @@ Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J(JNIEnv* env, CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } -/* - * Class: io_github_cvc5_Solver - * Method: mkDatatypeSorts - * Signature: (J[J[J)[J - */ -JNIEXPORT jlongArray JNICALL -Java_io_github_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env, - jobject, - jlong pointer, - jlongArray jDecls, - jlongArray jUnresolved) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - std::vector decls = - getObjectsFromPointers(env, jDecls); - std::vector cUnresolved = - getObjectsFromPointers(env, jUnresolved); - std::set unresolved(cUnresolved.begin(), cUnresolved.end()); - std::vector sorts = solver->mkDatatypeSorts(decls, unresolved); - jlongArray ret = getPointersFromObjects(env, sorts); - return ret; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_Solver * Method: mkFunctionSort @@ -478,10 +453,10 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUninterpretedSort__J( /* * Class: io_github_cvc5_Solver - * Method: mkUnresolvedSort + * Method: mkUnresolvedDatatypeSort * Signature: (JLjava/lang/String;I)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedDatatypeSort( JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) { CVC5_JAVA_API_TRY_CATCH_BEGIN; @@ -489,7 +464,8 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_Solver_mkUnresolvedSort( Solver* solver = reinterpret_cast(pointer); const char* s = env->GetStringUTFChars(jSymbol, nullptr); std::string cSymbol(s); - Sort* retPointer = new Sort(solver->mkUnresolvedSort(cSymbol, (size_t)arity)); + Sort* retPointer = + new Sort(solver->mkUnresolvedDatatypeSort(cSymbol, (size_t)arity)); env->ReleaseStringUTFChars(jSymbol, s); return reinterpret_cast(retPointer); diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index b823816ca..7f5bf10ef 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -106,6 +106,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass DatatypeConstructorDecl: void addSelector(const string& name, Sort sort) except + void addSelectorSelf(const string& name) except + + void addSelectorUnresolved(const string& name, const string& unresDatatypeName) except + bint isNull() except + string toString() except + @@ -215,8 +216,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Sort mkBitVectorSort(uint32_t size) except + Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except + Sort mkDatatypeSort(DatatypeDecl dtypedecl) except + - vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls, - const set[Sort]& unresolvedSorts) except + + vector[Sort] mkDatatypeSorts(const vector[DatatypeDecl]& dtypedecls) except + Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except + Sort mkParamSort() except + Sort mkParamSort(const string& symbol) except + @@ -227,7 +227,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Sort mkSequenceSort(Sort elemSort) except + Sort mkUninterpretedSort() except + Sort mkUninterpretedSort(const string& symbol) except + - Sort mkUnresolvedSort(const string& symbol, size_t arity) except + + Sort mkUnresolvedDatatypeSort(const string& symbol, size_t arity) except + Sort mkUninterpretedSortConstructorSort(size_t arity) except + Sort mkUninterpretedSortConstructorSort(size_t arity, const string& symbol) except + Sort mkTupleSort(const vector[Sort]& sorts) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 524f067ce..34c29675b 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -394,6 +394,18 @@ cdef class DatatypeConstructorDecl: """ self.cddc.addSelectorSelf(name.encode()) + def addSelectorUnresolved(self, str name, str unresDatatypeName): + """ + Add datatype selector declaration whose codomain sort is an + unresolved datatype with the given name. + + :param name: The name of the datatype selector declaration to add. + :param unresDataypeName: The name of the unresolved datatype. The + codomain of the selector will be the + resolved datatype with the given name. + """ + self.cddc.addSelectorUnresolved(name.encode(), unresDatatypeName.encode()) + def isNull(self): """ :return: True if this DatatypeConstructorDecl is a null object. @@ -857,43 +869,26 @@ cdef class Solver: sort.csort = self.csolver.mkDatatypeSort(dtypedecl.cdd) return sort - def mkDatatypeSorts(self, list dtypedecls, unresolvedSorts = None): + def mkDatatypeSorts(self, list dtypedecls): """ Create a vector of datatype sorts using unresolved sorts. The names of the datatype declarations in dtypedecls must be distinct. - This method is called when the DatatypeDecl objects dtypedecls have - been built using "unresolved" sorts. - - We associate each sort in unresolvedSorts with exacly one datatype - from dtypedecls. In particular, it must have the same name as - exactly one datatype declaration in dtypedecls. - When constructing datatypes, unresolved sorts are replaced by the datatype sort constructed for the datatype declaration it is associated with. :param dtypedecls: The datatype declarations from which the sort is created. - :param unresolvedSorts: The list of unresolved sorts. :return: The datatype sorts. """ - if unresolvedSorts == None: - unresolvedSorts = set([]) - else: - assert isinstance(unresolvedSorts, set) - sorts = [] cdef vector[c_DatatypeDecl] decls for decl in dtypedecls: decls.push_back(( decl).cdd) - cdef c_set[c_Sort] usorts - for usort in unresolvedSorts: - usorts.insert(( usort).csort) - csorts = self.csolver.mkDatatypeSorts( - decls, usorts) + decls) for csort in csorts: sort = Sort(self) sort.csort = csort @@ -1023,9 +1018,9 @@ cdef class Solver: sort.csort = self.csolver.mkUninterpretedSort(name.encode()) return sort - def mkUnresolvedSort(self, str name, size_t arity = 0): + def mkUnresolvedDatatypeSort(self, str name, size_t arity = 0): """ - Create an unresolved sort. + Create an unresolved datatype sort. This is for creating yet unresolved sort placeholders for mutually recursive datatypes. @@ -1035,7 +1030,7 @@ cdef class Solver: :return: The unresolved sort. """ cdef Sort sort = Sort(self) - sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity) + sort.csort = self.csolver.mkUnresolvedDatatypeSort(name.encode(), arity) return sort def mkUninterpretedSortConstructorSort(self, size_t arity, str symbol = None): diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 22593e274..59bc68090 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -324,7 +324,7 @@ cvc5::Sort Parser::mkSortConstructor(const std::string& name, size_t arity) cvc5::Sort Parser::mkUnresolvedType(const std::string& name) { - cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name); + cvc5::Sort unresolved = d_solver->mkUnresolvedDatatypeSort(name); defineType(name, unresolved); return unresolved; } @@ -332,7 +332,7 @@ cvc5::Sort Parser::mkUnresolvedType(const std::string& name) cvc5::Sort Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - cvc5::Sort unresolved = d_solver->mkUnresolvedSort(name, arity); + cvc5::Sort unresolved = d_solver->mkUnresolvedDatatypeSort(name, arity); defineType(name, vector(arity), unresolved); return unresolved; } @@ -343,7 +343,7 @@ cvc5::Sort Parser::mkUnresolvedTypeConstructor( Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; cvc5::Sort unresolved = - d_solver->mkUnresolvedSort(name, params.size()); + d_solver->mkUnresolvedDatatypeSort(name, params.size()); defineType(name, params, unresolved); cvc5::Sort t = getSort(name, params); return unresolved; diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 510eca60e..f4831b9a0 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -85,11 +85,8 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) * END; */ // Make unresolved types as placeholders - std::set unresTypes; - Sort unresTree = d_solver.mkUnresolvedSort("tree"); - Sort unresList = d_solver.mkUnresolvedSort("list"); - unresTypes.insert(unresTree); - unresTypes.insert(unresList); + Sort unresTree = d_solver.mkUnresolvedDatatypeSort("tree"); + Sort unresList = d_solver.mkUnresolvedDatatypeSort("list"); DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); @@ -114,7 +111,7 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) dtdecls.push_back(tree); dtdecls.push_back(list); std::vector dtsorts; - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), dtdecls.size()); for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) { @@ -139,6 +136,52 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC5ApiException); } +TEST_F(TestApiBlackDatatype, mkDatatypeSortsSelUnres) +{ + // Same as above, without unresolved sorts + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); + node.addSelectorUnresolved("left", "tree"); + node.addSelectorUnresolved("right", "tree"); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelectorUnresolved("data", "list"); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelectorUnresolved("car", "tree"); + cons.addSelectorUnresolved("cdr", "tree"); + list.addConstructor(cons); + + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(list); + std::vector dtsorts; + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); + ASSERT_EQ(dtsorts.size(), dtdecls.size()); + for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + { + ASSERT_TRUE(dtsorts[i].isDatatype()); + ASSERT_FALSE(dtsorts[i].getDatatype().isFinite()); + ASSERT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); + } + // verify the resolution was correct + Datatype dtTree = dtsorts[0].getDatatype(); + DatatypeConstructor dtcTreeNode = dtTree[0]; + ASSERT_EQ(dtcTreeNode.getName(), "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; + ASSERT_EQ(dtsTreeNodeLeft.getName(), "left"); + // argument type should have resolved to be recursive + ASSERT_TRUE(dtsTreeNodeLeft.getCodomainSort().isDatatype()); + ASSERT_EQ(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]); +} + TEST_F(TestApiBlackDatatype, datatypeStructs) { Sort intSort = d_solver.getIntegerSort(); @@ -331,13 +374,9 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ // Make unresolved types as placeholders - std::set unresTypes; - Sort unresWList = d_solver.mkUnresolvedSort("wlist"); - Sort unresList = d_solver.mkUnresolvedSort("list"); - Sort unresNs = d_solver.mkUnresolvedSort("ns"); - unresTypes.insert(unresWList); - unresTypes.insert(unresList); - unresTypes.insert(unresNs); + Sort unresWList = d_solver.mkUnresolvedDatatypeSort("wlist"); + Sort unresList = d_solver.mkUnresolvedDatatypeSort("list"); + Sort unresNs = d_solver.mkUnresolvedDatatypeSort("ns"); DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); @@ -367,7 +406,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) dtdecls.push_back(ns); // this is well-founded and has no nested recursion std::vector dtsorts; - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 3); ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); @@ -378,9 +417,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * ns2 = elem2(ndata: array(int,ns2)) | nil2 * END; */ - unresTypes.clear(); - Sort unresNs2 = d_solver.mkUnresolvedSort("ns2"); - unresTypes.insert(unresNs2); + Sort unresNs2 = d_solver.mkUnresolvedDatatypeSort("ns2"); DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); @@ -395,7 +432,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) dtsorts.clear(); // this is not well-founded due to non-simple recursion - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 1); ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray()); ASSERT_EQ( @@ -409,11 +446,8 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * ns3 = elem3(ndata: set(list3)) * END; */ - unresTypes.clear(); - Sort unresNs3 = d_solver.mkUnresolvedSort("ns3"); - unresTypes.insert(unresNs3); - Sort unresList3 = d_solver.mkUnresolvedSort("list3"); - unresTypes.insert(unresList3); + Sort unresNs3 = d_solver.mkUnresolvedDatatypeSort("ns3"); + Sort unresList3 = d_solver.mkUnresolvedDatatypeSort("list3"); DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); @@ -434,7 +468,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) dtsorts.clear(); // both are well-founded and have nested recursion - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 2); ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); @@ -445,11 +479,8 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * ns4 = elem(ndata: list4) * END; */ - unresTypes.clear(); - Sort unresNs4 = d_solver.mkUnresolvedSort("ns4"); - unresTypes.insert(unresNs4); - Sort unresList4 = d_solver.mkUnresolvedSort("list4"); - unresTypes.insert(unresList4); + Sort unresNs4 = d_solver.mkUnresolvedDatatypeSort("ns4"); + Sort unresList4 = d_solver.mkUnresolvedDatatypeSort("list4"); DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); @@ -470,7 +501,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) dtsorts.clear(); // both are well-founded and have nested recursion - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 2); ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded()); @@ -480,9 +511,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil * END; */ - unresTypes.clear(); Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort(1, "list5"); - unresTypes.insert(unresList5); std::vector v; Sort x = d_solver.mkParamSort("X"); @@ -506,7 +535,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) dtdecls.push_back(list5); // well-founded and has nested recursion - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 1); ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded()); } @@ -519,9 +548,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) * END; */ // Make unresolved types as placeholders - std::set unresTypes; Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist"); - unresTypes.insert(unresList); std::vector v; Sort x = d_solver.mkParamSort("X"); @@ -544,7 +571,7 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) std::vector dtsorts; // make the datatype sorts - ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls)); ASSERT_EQ(dtsorts.size(), 1); Datatype d = dtsorts[0].getDatatype(); DatatypeConstructor nilc = d[0]; diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 3cec83f81..cf048ce4f 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -196,8 +196,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException); /* with unresolved sorts */ - Sort unresList = d_solver.mkUnresolvedSort("ulist"); - std::set unresSorts = {unresList}; + Sort unresList = d_solver.mkUnresolvedDatatypeSort("ulist"); DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist"); DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons"); ucons.addSelector("car", unresList); @@ -206,15 +205,15 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil"); ulist.addConstructor(unil); std::vector udecls = {ulist}; - ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls, unresSorts)); + ASSERT_NO_THROW(d_solver.mkDatatypeSorts(udecls)); - ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), CVC5ApiException); + ASSERT_THROW(slv.mkDatatypeSorts(udecls), CVC5ApiException); /* mutually recursive with unresolved parameterized sorts */ Sort p0 = d_solver.mkParamSort("p0"); Sort p1 = d_solver.mkParamSort("p1"); - Sort u0 = d_solver.mkUnresolvedSort("dt0", 1); - Sort u1 = d_solver.mkUnresolvedSort("dt1", 1); + Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1); + Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1); DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0); DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1); DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0"); @@ -223,8 +222,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) ctordecl1.addSelector("s1", u0.instantiate({p1})); dtdecl0.addConstructor(ctordecl0); dtdecl1.addConstructor(ctordecl1); - std::vector dt_sorts = - d_solver.mkDatatypeSorts({dtdecl0, dtdecl1}, {u0, u1}); + std::vector dt_sorts = d_solver.mkDatatypeSorts({dtdecl0, dtdecl1}); Sort isort1 = dt_sorts[1].instantiate({d_solver.getBooleanSort()}); Term t1 = d_solver.mkConst(isort1, "t"); Term t0 = d_solver.mkTerm( @@ -352,12 +350,12 @@ TEST_F(TestApiBlackSolver, mkUninterpretedSort) ASSERT_NO_THROW(d_solver.mkUninterpretedSort("")); } -TEST_F(TestApiBlackSolver, mkUnresolvedSort) +TEST_F(TestApiBlackSolver, mkUnresolvedDatatypeSort) { - ASSERT_NO_THROW(d_solver.mkUnresolvedSort("u")); - ASSERT_NO_THROW(d_solver.mkUnresolvedSort("u", 1)); - ASSERT_NO_THROW(d_solver.mkUnresolvedSort("")); - ASSERT_NO_THROW(d_solver.mkUnresolvedSort("", 1)); + ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u")); + ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("u", 1)); + ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("")); + ASSERT_NO_THROW(d_solver.mkUnresolvedDatatypeSort("", 1)); } TEST_F(TestApiBlackSolver, mkUninterpretedSortConstructorSort) diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 93e38fa99..354d8662f 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -70,11 +70,8 @@ class DatatypeTest * END; */ // Make unresolved types as placeholders - Set unresTypes = new HashSet<>(); - Sort unresTree = d_solver.mkUnresolvedSort("tree", 0); - Sort unresList = d_solver.mkUnresolvedSort("list", 0); - unresTypes.add(unresTree); - unresTypes.add(unresList); + Sort unresTree = d_solver.mkUnresolvedDatatypeSort("tree", 0); + Sort unresList = d_solver.mkUnresolvedDatatypeSort("list", 0); DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); @@ -99,25 +96,25 @@ class DatatypeTest dtdecls.add(tree); dtdecls.add(list); - AtomicReference> atomic = new AtomicReference<>(); - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); - List dtsorts = atomic.get(); - assertEquals(dtsorts.size(), dtdecls.size()); + AtomicReference atomic = new AtomicReference<>(); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); + Sort[] dtsorts = atomic.get(); + assertEquals(dtsorts.length, dtdecls.size()); for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++) { - assertTrue(dtsorts.get(i).isDatatype()); - assertFalse(dtsorts.get(i).getDatatype().isFinite()); - assertEquals(dtsorts.get(i).getDatatype().getName(), dtdecls.get(i).getName()); + assertTrue(dtsorts[i].isDatatype()); + assertFalse(dtsorts[i].getDatatype().isFinite()); + assertEquals(dtsorts[i].getDatatype().getName(), dtdecls.get(i).getName()); } // verify the resolution was correct - Datatype dtTree = dtsorts.get(0).getDatatype(); + Datatype dtTree = dtsorts[0].getDatatype(); DatatypeConstructor dtcTreeNode = dtTree.getConstructor(0); assertEquals(dtcTreeNode.getName(), "node"); DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0); assertEquals(dtsTreeNodeLeft.getName(), "left"); // argument type should have resolved to be recursive assertTrue(dtsTreeNodeLeft.getCodomainSort().isDatatype()); - assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts.get(0)); + assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]); // fails due to empty datatype List dtdeclsBad = new ArrayList<>(); @@ -126,6 +123,55 @@ class DatatypeTest assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(dtdeclsBad)); } + @Test + void mkDatatypeSortsSelUnres() throws CVC5ApiException + { + // Same as above, using unresolved selectors + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); + node.addSelectorUnresolved("left", "tree"); + node.addSelectorUnresolved("right", "tree"); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelectorUnresolved("data", "list"); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelectorUnresolved("car", "tree"); + cons.addSelectorUnresolved("cdr", "tree"); + list.addConstructor(cons); + + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + List dtdecls = new ArrayList<>(); + dtdecls.add(tree); + dtdecls.add(list); + + AtomicReference atomic = new AtomicReference<>(); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); + Sort[] dtsorts = atomic.get(); + assertEquals(dtsorts.length, dtdecls.size()); + for (int i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + { + assertTrue(dtsorts[i].isDatatype()); + assertFalse(dtsorts[i].getDatatype().isFinite()); + assertEquals(dtsorts[i].getDatatype().getName(), dtdecls.get(i).getName()); + } + // verify the resolution was correct + Datatype dtTree = dtsorts[0].getDatatype(); + DatatypeConstructor dtcTreeNode = dtTree.getConstructor(0); + assertEquals(dtcTreeNode.getName(), "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode.getSelector(0); + assertEquals(dtsTreeNodeLeft.getName(), "left"); + // argument type should have resolved to be recursive + assertTrue(dtsTreeNodeLeft.getCodomainSort().isDatatype()); + assertEquals(dtsTreeNodeLeft.getCodomainSort(), dtsorts[0]); + } + @Test void datatypeStructs() throws CVC5ApiException { @@ -316,13 +362,9 @@ class DatatypeTest * END; */ // Make unresolved types as placeholders - Set unresTypes = new HashSet<>(); - Sort unresWList = d_solver.mkUnresolvedSort("wlist", 0); - Sort unresList = d_solver.mkUnresolvedSort("list", 0); - Sort unresNs = d_solver.mkUnresolvedSort("ns", 0); - unresTypes.add(unresWList); - unresTypes.add(unresList); - unresTypes.add(unresNs); + Sort unresWList = d_solver.mkUnresolvedDatatypeSort("wlist", 0); + Sort unresList = d_solver.mkUnresolvedDatatypeSort("list", 0); + Sort unresNs = d_solver.mkUnresolvedDatatypeSort("ns", 0); DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); @@ -350,22 +392,20 @@ class DatatypeTest dtdecls.add(list); dtdecls.add(ns); // this is well-founded and has no nested recursion - AtomicReference> atomic = new AtomicReference<>(); - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); - List dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 3); - assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); - assertTrue(dtsorts.get(1).getDatatype().isWellFounded()); - assertTrue(dtsorts.get(2).getDatatype().isWellFounded()); + AtomicReference atomic = new AtomicReference<>(); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); + Sort[] dtsorts = atomic.get(); + assertEquals(dtsorts.length, 3); + assertTrue(dtsorts[0].getDatatype().isWellFounded()); + assertTrue(dtsorts[1].getDatatype().isWellFounded()); + assertTrue(dtsorts[2].getDatatype().isWellFounded()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE * ns2 = elem2(ndata: array(int,ns2)) | nil2 * END; */ - unresTypes.clear(); - Sort unresNs2 = d_solver.mkUnresolvedSort("ns2", 0); - unresTypes.add(unresNs2); + Sort unresNs2 = d_solver.mkUnresolvedDatatypeSort("ns2", 0); DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); @@ -379,19 +419,19 @@ class DatatypeTest // dtsorts.clear(); // this is not well-founded due to non-simple recursion - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 1); + assertEquals(dtsorts.length, 1); assertTrue( - dtsorts.get(0).getDatatype().getConstructor(0).getSelector(0).getCodomainSort().isArray()); - assertEquals(dtsorts.get(0) + dtsorts[0].getDatatype().getConstructor(0).getSelector(0).getCodomainSort().isArray()); + assertEquals(dtsorts[0] .getDatatype() .getConstructor(0) .getSelector(0) .getCodomainSort() .getArrayElementSort(), - dtsorts.get(0)); - assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); + dtsorts[0]); + assertTrue(dtsorts[0].getDatatype().isWellFounded()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -399,11 +439,8 @@ class DatatypeTest * ns3 = elem3(ndata: set(list3)) * END; */ - unresTypes.clear(); - Sort unresNs3 = d_solver.mkUnresolvedSort("ns3", 0); - unresTypes.add(unresNs3); - Sort unresList3 = d_solver.mkUnresolvedSort("list3", 0); - unresTypes.add(unresList3); + Sort unresNs3 = d_solver.mkUnresolvedDatatypeSort("ns3", 0); + Sort unresList3 = d_solver.mkUnresolvedDatatypeSort("list3", 0); DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); @@ -424,11 +461,11 @@ class DatatypeTest // dtsorts.clear(); // both are well-founded and have nested recursion - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 2); - assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); - assertTrue(dtsorts.get(1).getDatatype().isWellFounded()); + assertEquals(dtsorts.length, 2); + assertTrue(dtsorts[0].getDatatype().isWellFounded()); + assertTrue(dtsorts[1].getDatatype().isWellFounded()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -436,11 +473,8 @@ class DatatypeTest * ns4 = elem(ndata: list4) * END; */ - unresTypes.clear(); - Sort unresNs4 = d_solver.mkUnresolvedSort("ns4", 0); - unresTypes.add(unresNs4); - Sort unresList4 = d_solver.mkUnresolvedSort("list4", 0); - unresTypes.add(unresList4); + Sort unresNs4 = d_solver.mkUnresolvedDatatypeSort("ns4", 0); + Sort unresList4 = d_solver.mkUnresolvedDatatypeSort("list4", 0); DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); @@ -461,20 +495,18 @@ class DatatypeTest // dtsorts.clear(); // both are well-founded and have nested recursion - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 2); - assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); - assertTrue(dtsorts.get(1).getDatatype().isWellFounded()); + assertEquals(dtsorts.length, 2); + assertTrue(dtsorts[0].getDatatype().isWellFounded()); + assertTrue(dtsorts[1].getDatatype().isWellFounded()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil * END; */ - unresTypes.clear(); Sort unresList5 = d_solver.mkUninterpretedSortConstructorSort(1, "list5"); - unresTypes.add(unresList5); List v = new ArrayList<>(); Sort x = d_solver.mkParamSort("X"); @@ -498,10 +530,10 @@ class DatatypeTest dtdecls.add(list5); // well-founded and has nested recursion - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 1); - assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); + assertEquals(dtsorts.length, 1); + assertTrue(dtsorts[0].getDatatype().isWellFounded()); } @Test @@ -513,9 +545,7 @@ class DatatypeTest * END; */ // Make unresolved types as placeholders - Set unresTypes = new HashSet<>(); Sort unresList = d_solver.mkUninterpretedSortConstructorSort(1, "plist"); - unresTypes.add(unresList); List v = new ArrayList<>(); Sort x = d_solver.mkParamSort("X"); @@ -537,17 +567,17 @@ class DatatypeTest dtdecls.add(plist); // make the datatype sorts - AtomicReference> atomic = new AtomicReference<>(); - assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls, unresTypes))); - List dtsorts = atomic.get(); - assertEquals(dtsorts.size(), 1); - Datatype d = dtsorts.get(0).getDatatype(); + AtomicReference atomic = new AtomicReference<>(); + assertDoesNotThrow(() -> atomic.set(d_solver.mkDatatypeSorts(dtdecls))); + Sort[] dtsorts = atomic.get(); + assertEquals(dtsorts.length, 1); + Datatype d = dtsorts[0].getDatatype(); DatatypeConstructor nilc = d.getConstructor(0); Sort isort = d_solver.getIntegerSort(); List iargs = new ArrayList<>(); iargs.add(isort); - Sort listInt = dtsorts.get(0).instantiate(iargs); + Sort listInt = dtsorts[0].instantiate(iargs); AtomicReference atomicTerm = new AtomicReference<>(); // get the specialized constructor term for list[Int] diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 0f5f80e89..5515fa649 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -184,9 +184,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(throwsDecls)); /* with unresolved sorts */ - Sort unresList = d_solver.mkUnresolvedSort("ulist", 1); - Set unresSorts = new HashSet<>(); - unresSorts.add(unresList); + Sort unresList = d_solver.mkUnresolvedDatatypeSort("ulist", 1); DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist"); DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons"); ucons.addSelector("car", unresList); @@ -195,17 +193,16 @@ class SolverTest DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil"); ulist.addConstructor(unil); DatatypeDecl[] udecls = new DatatypeDecl[] {ulist}; - assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls), unresSorts)); + assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls))); - assertThrows( - CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts)); + assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls))); slv.close(); /* mutually recursive with unresolved parameterized sorts */ Sort p0 = d_solver.mkParamSort("p0"); Sort p1 = d_solver.mkParamSort("p1"); - Sort u0 = d_solver.mkUnresolvedSort("dt0", 1); - Sort u1 = d_solver.mkUnresolvedSort("dt1", 1); + Sort u0 = d_solver.mkUnresolvedDatatypeSort("dt0", 1); + Sort u1 = d_solver.mkUnresolvedDatatypeSort("dt1", 1); DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0); DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1); DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0"); @@ -214,8 +211,7 @@ class SolverTest ctordecl1.addSelector("s1", u0.instantiate(new Sort[] {p1})); dtdecl0.addConstructor(ctordecl0); dtdecl1.addConstructor(ctordecl1); - Sort[] dt_sorts = - d_solver.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1}, new Sort[] {u0, u1}); + Sort[] dt_sorts = d_solver.mkDatatypeSorts(new DatatypeDecl[] {dtdecl0, dtdecl1}); Sort isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()}); Term t1 = d_solver.mkConst(isort1, "t"); Term t0 = d_solver.mkTerm(APPLY_SELECTOR, @@ -360,12 +356,12 @@ class SolverTest } @Test - void mkUnresolvedSort() throws CVC5ApiException + void mkUnresolvedDatatypeSort() throws CVC5ApiException { - assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u")); - assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1)); - assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("")); - assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1)); + assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u")); + assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("u", 1)); + assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("")); + assertDoesNotThrow(() -> d_solver.mkUnresolvedDatatypeSort("", 1)); } @Test diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 2fb978dbb..df4485741 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -85,11 +85,8 @@ def test_mk_datatype_sorts(solver): # #Make unresolved types as placeholders - unresTypes = set([]) - unresTree = solver.mkUnresolvedSort("tree") - unresList = solver.mkUnresolvedSort("list") - unresTypes.add(unresTree) - unresTypes.add(unresList) + unresTree = solver.mkUnresolvedDatatypeSort("tree") + unresList = solver.mkUnresolvedDatatypeSort("list") tree = solver.mkDatatypeDecl("tree") node = solver.mkDatatypeConstructorDecl("node") @@ -114,7 +111,7 @@ def test_mk_datatype_sorts(solver): dtdecls.append(tree) dtdecls.append(llist) dtsorts = [] - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == len(dtdecls) for i in range(0, len(dtdecls)): assert dtsorts[i].isDatatype() @@ -138,6 +135,48 @@ def test_mk_datatype_sorts(solver): solver.mkDatatypeSorts(dtdeclsBad) +def test_mk_datatype_sorts_sel_unres(solver): + # Same as above, using unresolved selectors + + tree = solver.mkDatatypeDecl("tree") + node = solver.mkDatatypeConstructorDecl("node") + node.addSelectorUnresolved("left", "tree") + node.addSelectorUnresolved("right", "tree") + tree.addConstructor(node) + + leaf = solver.mkDatatypeConstructorDecl("leaf") + leaf.addSelectorUnresolved("data", "list") + tree.addConstructor(leaf) + + llist = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelectorUnresolved("car", "tree") + cons.addSelectorUnresolved("cdr", "tree") + llist.addConstructor(cons) + + nil = solver.mkDatatypeConstructorDecl("nil") + llist.addConstructor(nil) + + dtdecls = [] + dtdecls.append(tree) + dtdecls.append(llist) + dtsorts = [] + dtsorts = solver.mkDatatypeSorts(dtdecls) + assert len(dtsorts) == len(dtdecls) + for i in range(0, len(dtdecls)): + assert dtsorts[i].isDatatype() + assert not dtsorts[i].getDatatype().isFinite() + assert dtsorts[i].getDatatype().getName() == dtdecls[i].getName() + # verify the resolution was correct + dtTree = dtsorts[0].getDatatype() + dtcTreeNode = dtTree[0] + assert dtcTreeNode.getName() == "node" + dtsTreeNodeLeft = dtcTreeNode[0] + assert dtsTreeNodeLeft.getName() == "left" + # argument type should have resolved to be recursive + assert dtsTreeNodeLeft.getCodomainSort().isDatatype() + assert dtsTreeNodeLeft.getCodomainSort() == dtsorts[0] + def test_datatype_structs(solver): intSort = solver.getIntegerSort() boolSort = solver.getBooleanSort() @@ -327,13 +366,9 @@ def test_datatype_simply_rec(solver): # END # Make unresolved types as placeholders - unresTypes = set([]) - unresWList = solver.mkUnresolvedSort("wlist") - unresList = solver.mkUnresolvedSort("list") - unresNs = solver.mkUnresolvedSort("ns") - unresTypes.add(unresWList) - unresTypes.add(unresList) - unresTypes.add(unresNs) + unresWList = solver.mkUnresolvedDatatypeSort("wlist") + unresList = solver.mkUnresolvedDatatypeSort("list") + unresNs = solver.mkUnresolvedDatatypeSort("ns") wlist = solver.mkDatatypeDecl("wlist") leaf = solver.mkDatatypeConstructorDecl("leaf") @@ -358,7 +393,7 @@ def test_datatype_simply_rec(solver): dtdecls = [wlist, llist, ns] # this is well-founded and has no nested recursion - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 3 assert dtsorts[0].getDatatype().isWellFounded() assert dtsorts[1].getDatatype().isWellFounded() @@ -369,9 +404,7 @@ def test_datatype_simply_rec(solver): # ns2 = elem2(ndata: array(int,ns2)) | nil2 # END - unresTypes.clear() - unresNs2 = solver.mkUnresolvedSort("ns2") - unresTypes.add(unresNs2) + unresNs2 = solver.mkUnresolvedDatatypeSort("ns2") ns2 = solver.mkDatatypeDecl("ns2") elem2 = solver.mkDatatypeConstructorDecl("elem2") @@ -385,7 +418,7 @@ def test_datatype_simply_rec(solver): dtdecls.append(ns2) # this is not well-founded due to non-simple recursion - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 1 assert dtsorts[0].getDatatype()[0][0].getCodomainSort().isArray() assert dtsorts[0].getDatatype()[0][0].getCodomainSort().getArrayElementSort() \ @@ -398,11 +431,8 @@ def test_datatype_simply_rec(solver): # ns3 = elem3(ndata: set(list3)) # END - unresTypes.clear() - unresNs3 = solver.mkUnresolvedSort("ns3") - unresTypes.add(unresNs3) - unresList3 = solver.mkUnresolvedSort("list3") - unresTypes.add(unresList3) + unresNs3 = solver.mkUnresolvedDatatypeSort("ns3") + unresList3 = solver.mkUnresolvedDatatypeSort("list3") list3 = solver.mkDatatypeDecl("list3") cons3 = solver.mkDatatypeConstructorDecl("cons3") @@ -422,7 +452,7 @@ def test_datatype_simply_rec(solver): dtdecls.append(ns3) # both are well-founded and have nested recursion - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 2 assert dtsorts[0].getDatatype().isWellFounded() assert dtsorts[1].getDatatype().isWellFounded() @@ -432,11 +462,8 @@ def test_datatype_simply_rec(solver): # list4 = cons(car: set(ns4), cdr: list4) | nil, # ns4 = elem(ndata: list4) # END - unresTypes.clear() - unresNs4 = solver.mkUnresolvedSort("ns4") - unresTypes.add(unresNs4) - unresList4 = solver.mkUnresolvedSort("list4") - unresTypes.add(unresList4) + unresNs4 = solver.mkUnresolvedDatatypeSort("ns4") + unresList4 = solver.mkUnresolvedDatatypeSort("list4") list4 = solver.mkDatatypeDecl("list4") cons4 = solver.mkDatatypeConstructorDecl("cons4") @@ -456,7 +483,7 @@ def test_datatype_simply_rec(solver): dtdecls.append(ns4) # both are well-founded and have nested recursion - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 2 assert dtsorts[0].getDatatype().isWellFounded() assert dtsorts[1].getDatatype().isWellFounded() @@ -465,9 +492,7 @@ def test_datatype_simply_rec(solver): # DATATYPE # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil # END - unresTypes.clear() unresList5 = solver.mkUninterpretedSortConstructorSort(1, "list5") - unresTypes.add(unresList5) v = [] x = solver.mkParamSort("X") @@ -490,7 +515,7 @@ def test_datatype_simply_rec(solver): dtdecls.append(list5) # well-founded and has nested recursion - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 1 assert dtsorts[0].getDatatype().isWellFounded() @@ -502,10 +527,7 @@ def test_datatype_specialized_cons(solver): # END # Make unresolved types as placeholders - unresTypes = set([]) unresList = solver.mkUninterpretedSortConstructorSort(1, "plist") - unresTypes.add(unresList) - v = [] x = solver.mkParamSort("X") v.append(x) @@ -524,7 +546,7 @@ def test_datatype_specialized_cons(solver): dtdecls = [plist] # make the datatype sorts - dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + dtsorts = solver.mkDatatypeSorts(dtdecls) assert len(dtsorts) == 1 d = dtsorts[0].getDatatype() nilc = d[0] diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index ac8c8b073..b3634674f 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -134,19 +134,18 @@ def test_mk_datatype_sorts(solver): dtypeSpec2.addConstructor(nil2) decls = [dtypeSpec1, dtypeSpec2] - solver.mkDatatypeSorts(decls, set([])) + solver.mkDatatypeSorts(decls) with pytest.raises(RuntimeError): - slv.mkDatatypeSorts(decls, set([])) + slv.mkDatatypeSorts(decls) throwsDtypeSpec = solver.mkDatatypeDecl("list") throwsDecls = [throwsDtypeSpec] with pytest.raises(RuntimeError): - solver.mkDatatypeSorts(throwsDecls, set([])) + solver.mkDatatypeSorts(throwsDecls) # with unresolved sorts - unresList = solver.mkUnresolvedSort("ulist") - unresSorts = set([unresList]) + unresList = solver.mkUnresolvedDatatypeSort("ulist") ulist = solver.mkDatatypeDecl("ulist") ucons = solver.mkDatatypeConstructorDecl("ucons") ucons.addSelector("car", unresList) @@ -156,15 +155,15 @@ def test_mk_datatype_sorts(solver): ulist.addConstructor(unil) udecls = [ulist] - solver.mkDatatypeSorts(udecls, unresSorts) + solver.mkDatatypeSorts(udecls) with pytest.raises(RuntimeError): - slv.mkDatatypeSorts(udecls, unresSorts) + slv.mkDatatypeSorts(udecls) # mutually recursive with unresolved parameterized sorts p0 = solver.mkParamSort("p0") p1 = solver.mkParamSort("p1") - u0 = solver.mkUnresolvedSort("dt0", 1) - u1 = solver.mkUnresolvedSort("dt1", 1) + u0 = solver.mkUnresolvedDatatypeSort("dt0", 1) + u1 = solver.mkUnresolvedDatatypeSort("dt1", 1) dtdecl0 = solver.mkDatatypeDecl("dt0", p0) dtdecl1 = solver.mkDatatypeDecl("dt1", p1) ctordecl0 = solver.mkDatatypeConstructorDecl("c0") @@ -173,7 +172,7 @@ def test_mk_datatype_sorts(solver): ctordecl1.addSelector("s1", u0.instantiate({p1})) dtdecl0.addConstructor(ctordecl0) dtdecl1.addConstructor(ctordecl1) - dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1], {u0, u1}) + dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1]) isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()}) t1 = solver.mkConst(isort1, "t") t0 = solver.mkTerm( @@ -292,10 +291,10 @@ def test_mk_uninterpreted_sort(solver): def test_mk_unresolved_sort(solver): - solver.mkUnresolvedSort("u") - solver.mkUnresolvedSort("u", 1) - solver.mkUnresolvedSort("") - solver.mkUnresolvedSort("", 1) + solver.mkUnresolvedDatatypeSort("u") + solver.mkUnresolvedDatatypeSort("u", 1) + solver.mkUnresolvedDatatypeSort("") + solver.mkUnresolvedDatatypeSort("", 1) def test_mk_sort_constructor_sort(solver): -- 2.30.2