From 6c98b2f66aaee9e8f266bee816d730cc5ffee821 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 16 Dec 2021 20:24:23 -0800 Subject: [PATCH] api: Add Solver::mkUnresolvedSort(). (#7817) This adds a function to create unresolved sorts for mutually recursive datatpes. This function creates an uninterpreted sort if the arity of the unresolved sort is 0, and a sort constructor sort otherwise. --- src/api/cpp/cvc5.cpp | 13 ++++++++ src/api/cpp/cvc5.h | 16 ++++++++-- src/api/java/io/github/cvc5/api/Solver.java | 21 +++++++++++++ src/api/java/jni/solver.cpp | 20 +++++++++++++ src/api/python/cvc5.pxd | 1 + src/api/python/cvc5.pxi | 14 +++++++++ test/unit/api/cpp/datatype_api_black.cpp | 20 ++++++------- test/unit/api/cpp/solver_black.cpp | 33 ++++++++++++++++++++- test/unit/api/java/DatatypeTest.java | 22 +++++++------- test/unit/api/java/SolverTest.java | 32 +++++++++++++++++++- test/unit/api/python/test_datatype_api.py | 20 ++++++------- test/unit/api/python/test_solver.py | 30 ++++++++++++++++++- 12 files changed, 206 insertions(+), 36 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index a9f7d884a..024fa8239 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5746,6 +5746,19 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const CVC5_API_TRY_CATCH_END; } +Sort Solver::mkUnresolvedSort(const std::string& symbol, size_t arity) const +{ + CVC5_API_TRY_CATCH_BEGIN; + //////// all checks before this line + if (arity) + { + return Sort(this, getNodeManager()->mkSortConstructor(symbol, arity)); + } + return Sort(this, getNodeManager()->mkSort(symbol)); + //////// + CVC5_API_TRY_CATCH_END; +} + Sort Solver::mkSortConstructorSort(const std::string& symbol, size_t arity) const { diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index a4ba3ee90..726e74363 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2613,7 +2613,7 @@ class CVC5_EXPORT Grammar * with bound variables via purifySygusGTerm, and binding these variables * via a lambda. * - * @note Create unresolved sorts with Solver::mkUninterpretedSort(). + * @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 @@ -3178,7 +3178,7 @@ class CVC5_EXPORT Solver * 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::mkUninterpretedSort(). + * @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 @@ -3255,6 +3255,18 @@ class CVC5_EXPORT Solver */ Sort mkUninterpretedSort(const std::string& symbol) const; + /** + * Create an unresolved sort. + * + * This is for creating yet unresolved sort placeholders for mutually + * recursive datatypes. + * + * @param symbol the symbol of the sort + * @param arity the number of sort parameters of the sort + * @return the unresolved sort + */ + Sort mkUnresolvedSort(const std::string& symbol, size_t arity = 0) const; + /** * Create a sort constructor sort. * @param symbol the symbol of 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 6f86928ca..1e24222b3 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -254,6 +254,8 @@ public class Solver implements IPointer, AutoCloseable * datatype sort constructed for the datatype declaration it is associated * with. * + * @apiNote Create unresolved sorts with Solver::mkUnresolvedSort(). + * * @param dtypedecls the datatype declarations from which the sort is * created * @param unresolvedSorts the set of unresolved sorts @@ -418,6 +420,25 @@ public class Solver implements IPointer, AutoCloseable private native long mkUninterpretedSort(long pointer, String symbol); + /** + * Create an unresolved sort. + * + * This is for creating yet unresolved sort placeholders for mutually + * recursive datatypes. + * + * @param symbol the symbol of the sort + * @param arity the number of sort parameters of the sort + * @return the unresolved sort + */ + public Sort mkUnresolvedSort(String symbol, int arity) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = mkUnresolvedSort(pointer, symbol, arity); + return new Sort(this, sortPointer); + } + + private native long mkUnresolvedSort(long pointer, String symbol, int arity); + /** * Create a sort constructor sort. * @param symbol the symbol of the sort diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 2e4404362..8008ebada 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -460,6 +460,26 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedSort( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } +/* + * Class: io_github_cvc5_api_Solver + * Method: mkUnresolvedSort + * Signature: (JLjava/lang/String;I)J + */ +JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUnresolvedSort( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + 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)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast(retPointer); + + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + /* * Class: io_github_cvc5_api_Solver * Method: mkSortConstructorSort diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 8b9a88adc..cc1bad1cd 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -184,6 +184,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort mkBagSort(Sort elemSort) except + 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 mkTupleSort(const vector[Sort]& sorts) except + Term mkTerm(Op op) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2bf72e913..9c4f59c35 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -956,6 +956,20 @@ cdef class Solver: sort.csort = self.csolver.mkUninterpretedSort(name.encode()) return sort + def mkUnresolvedSort(self, str name, size_t arity = 0): + """Create an unresolved sort. + + This is for creating yet unresolved sort placeholders for mutually + recursive datatypes. + + :param symbol: the name of the sort + :param arity: the number of sort parameters of the sort + :return: the unresolved sort + """ + cdef Sort sort = Sort(self) + sort.csort = self.csolver.mkUnresolvedSort(name.encode(), arity) + return sort + def mkSortConstructorSort(self, str symbol, size_t arity): """Create a sort constructor sort. diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index fecf228a5..a4f6bc722 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -88,8 +88,8 @@ TEST_F(TestApiBlackDatatype, mkDatatypeSorts) */ // Make unresolved types as placeholders std::set unresTypes; - Sort unresTree = d_solver.mkUninterpretedSort("tree"); - Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresTree = d_solver.mkUnresolvedSort("tree"); + Sort unresList = d_solver.mkUnresolvedSort("list"); unresTypes.insert(unresTree); unresTypes.insert(unresList); @@ -349,9 +349,9 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) */ // Make unresolved types as placeholders std::set unresTypes; - Sort unresWList = d_solver.mkUninterpretedSort("wlist"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - Sort unresNs = d_solver.mkUninterpretedSort("ns"); + 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); @@ -399,7 +399,7 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ unresTypes.clear(); - Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + Sort unresNs2 = d_solver.mkUnresolvedSort("ns2"); unresTypes.insert(unresNs2); DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); @@ -430,9 +430,9 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ unresTypes.clear(); - Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + Sort unresNs3 = d_solver.mkUnresolvedSort("ns3"); unresTypes.insert(unresNs3); - Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + Sort unresList3 = d_solver.mkUnresolvedSort("list3"); unresTypes.insert(unresList3); DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); @@ -468,9 +468,9 @@ TEST_F(TestApiBlackDatatype, datatypeSimplyRec) * END; */ unresTypes.clear(); - Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + Sort unresNs4 = d_solver.mkUnresolvedSort("ns4"); unresTypes.insert(unresNs4); - Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + Sort unresList4 = d_solver.mkUnresolvedSort("list4"); unresTypes.insert(unresList4); DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 31034a15e..f3bc91eaa 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -153,7 +153,7 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) ASSERT_THROW(d_solver.mkDatatypeSorts(throwsDecls), CVC5ApiException); /* with unresolved sorts */ - Sort unresList = d_solver.mkUninterpretedSort("ulist"); + Sort unresList = d_solver.mkUnresolvedSort("ulist"); std::set unresSorts = {unresList}; DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist"); DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons"); @@ -167,6 +167,29 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts) ASSERT_THROW(slv.mkDatatypeSorts(udecls, unresSorts), 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); + DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0); + DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1); + DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0"); + ctordecl0.addSelector("s0", u1.instantiate({p0})); + DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("c1"); + ctordecl1.addSelector("s1", u0.instantiate({p1})); + dtdecl0.addConstructor(ctordecl0); + dtdecl1.addConstructor(ctordecl1); + std::vector dt_sorts = + d_solver.mkDatatypeSorts({dtdecl0, dtdecl1}, {u0, u1}); + Sort isort1 = dt_sorts[1].instantiate({d_solver.getBooleanSort()}); + Term t1 = d_solver.mkConst(isort1, "t"); + Term t0 = d_solver.mkTerm( + APPLY_SELECTOR, + t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), + t1); + ASSERT_EQ(dt_sorts[0].instantiate({d_solver.getBooleanSort()}), t0.getSort()); + /* Note: More tests are in datatype_api_black. */ } @@ -286,6 +309,14 @@ TEST_F(TestApiBlackSolver, mkUninterpretedSort) ASSERT_NO_THROW(d_solver.mkUninterpretedSort("")); } +TEST_F(TestApiBlackSolver, mkUnresolvedSort) +{ + 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)); +} + TEST_F(TestApiBlackSolver, mkSortConstructorSort) { ASSERT_NO_THROW(d_solver.mkSortConstructorSort("s", 2)); diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index e94785b08..002a08ff1 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -55,7 +55,7 @@ class DatatypeTest assertDoesNotThrow(() -> nilConstr.getConstructorTerm()); } - @Test void mkDatatypeSorts() + @Test void mkDatatypeSorts() throws CVC5ApiException { /* Create two mutual datatypes corresponding to this definition * block: @@ -67,8 +67,8 @@ class DatatypeTest */ // Make unresolved types as placeholders Set unresTypes = new HashSet<>(); - Sort unresTree = d_solver.mkUninterpretedSort("tree"); - Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresTree = d_solver.mkUnresolvedSort("tree", 0); + Sort unresList = d_solver.mkUnresolvedSort("list", 0); unresTypes.add(unresTree); unresTypes.add(unresList); @@ -322,9 +322,9 @@ class DatatypeTest */ // Make unresolved types as placeholders Set unresTypes = new HashSet<>(); - Sort unresWList = d_solver.mkUninterpretedSort("wlist"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - Sort unresNs = d_solver.mkUninterpretedSort("ns"); + 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); @@ -372,7 +372,7 @@ class DatatypeTest * END; */ unresTypes.clear(); - Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + Sort unresNs2 = d_solver.mkUnresolvedSort("ns2", 0); unresTypes.add(unresNs2); DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); @@ -409,9 +409,9 @@ class DatatypeTest * END; */ unresTypes.clear(); - Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + Sort unresNs3 = d_solver.mkUnresolvedSort("ns3", 0); unresTypes.add(unresNs3); - Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + Sort unresList3 = d_solver.mkUnresolvedSort("list3", 0); unresTypes.add(unresList3); DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); @@ -448,9 +448,9 @@ class DatatypeTest * END; */ unresTypes.clear(); - Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + Sort unresNs4 = d_solver.mkUnresolvedSort("ns4", 0); unresTypes.add(unresNs4); - Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + Sort unresList4 = d_solver.mkUnresolvedSort("list4", 0); unresTypes.add(unresList4); DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 5d651e82a..ca0032c22 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -167,7 +167,7 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(throwsDecls)); /* with unresolved sorts */ - Sort unresList = d_solver.mkUninterpretedSort("ulist"); + Sort unresList = d_solver.mkUnresolvedSort("ulist", 1); Set unresSorts = new HashSet<>(); unresSorts.add(unresList); DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist"); @@ -184,6 +184,28 @@ class SolverTest CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts)); 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); + DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", p0); + DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", p1); + DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0"); + ctordecl0.addSelector("s0", u1.instantiate(new Sort[] {p0})); + DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("c1"); + 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 isort1 = dt_sorts[1].instantiate(new Sort[] {d_solver.getBooleanSort()}); + Term t1 = d_solver.mkConst(isort1, "t"); + Term t0 = d_solver.mkTerm(APPLY_SELECTOR, + t1.getSort().getDatatype().getConstructor("c1").getSelector("s1").getSelectorTerm(), + t1); + assertEquals(dt_sorts[0].instantiate(new Sort[] {d_solver.getBooleanSort()}), t0.getSort()); + /* Note: More tests are in datatype_api_black. */ } @@ -312,6 +334,14 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("")); } + @Test void mkUnresolvedSort() throws CVC5ApiException + { + assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 0)); + assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1)); + assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 0)); + assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1)); + } + @Test void mkSortConstructorSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("s", 2)); diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index af34e098e..2d7e1c8d9 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -86,8 +86,8 @@ def test_mk_datatype_sorts(solver): #Make unresolved types as placeholders unresTypes = set([]) - unresTree = solver.mkUninterpretedSort("tree") - unresList = solver.mkUninterpretedSort("list") + unresTree = solver.mkUnresolvedSort("tree") + unresList = solver.mkUnresolvedSort("list") unresTypes.add(unresTree) unresTypes.add(unresList) @@ -346,9 +346,9 @@ def test_datatype_simply_rec(solver): # Make unresolved types as placeholders unresTypes = set([]) - unresWList = solver.mkUninterpretedSort("wlist") - unresList = solver.mkUninterpretedSort("list") - unresNs = solver.mkUninterpretedSort("ns") + unresWList = solver.mkUnresolvedSort("wlist") + unresList = solver.mkUnresolvedSort("list") + unresNs = solver.mkUnresolvedSort("ns") unresTypes.add(unresWList) unresTypes.add(unresList) unresTypes.add(unresNs) @@ -391,7 +391,7 @@ def test_datatype_simply_rec(solver): # END unresTypes.clear() - unresNs2 = solver.mkUninterpretedSort("ns2") + unresNs2 = solver.mkUnresolvedSort("ns2") unresTypes.add(unresNs2) ns2 = solver.mkDatatypeDecl("ns2") @@ -421,9 +421,9 @@ def test_datatype_simply_rec(solver): # END unresTypes.clear() - unresNs3 = solver.mkUninterpretedSort("ns3") + unresNs3 = solver.mkUnresolvedSort("ns3") unresTypes.add(unresNs3) - unresList3 = solver.mkUninterpretedSort("list3") + unresList3 = solver.mkUnresolvedSort("list3") unresTypes.add(unresList3) list3 = solver.mkDatatypeDecl("list3") @@ -457,9 +457,9 @@ def test_datatype_simply_rec(solver): # ns4 = elem(ndata: list4) # END unresTypes.clear() - unresNs4 = solver.mkUninterpretedSort("ns4") + unresNs4 = solver.mkUnresolvedSort("ns4") unresTypes.add(unresNs4) - unresList4 = solver.mkUninterpretedSort("list4") + unresList4 = solver.mkUnresolvedSort("list4") unresTypes.add(unresList4) list4 = solver.mkDatatypeDecl("list4") diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index d9d6a6c36..1e9dbcf1f 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -145,7 +145,7 @@ def test_mk_datatype_sorts(solver): solver.mkDatatypeSorts(throwsDecls, set([])) # with unresolved sorts - unresList = solver.mkUninterpretedSort("ulist") + unresList = solver.mkUnresolvedSort("ulist") unresSorts = set([unresList]) ulist = solver.mkDatatypeDecl("ulist") ucons = solver.mkDatatypeConstructorDecl("ucons") @@ -160,6 +160,27 @@ def test_mk_datatype_sorts(solver): with pytest.raises(RuntimeError): slv.mkDatatypeSorts(udecls, unresSorts) + # mutually recursive with unresolved parameterized sorts + p0 = solver.mkParamSort("p0") + p1 = solver.mkParamSort("p1") + u0 = solver.mkUnresolvedSort("dt0", 1) + u1 = solver.mkUnresolvedSort("dt1", 1) + dtdecl0 = solver.mkDatatypeDecl("dt0", p0) + dtdecl1 = solver.mkDatatypeDecl("dt1", p1) + ctordecl0 = solver.mkDatatypeConstructorDecl("c0") + ctordecl0.addSelector("s0", u1.instantiate({p0})) + ctordecl1 = solver.mkDatatypeConstructorDecl("c1") + ctordecl1.addSelector("s1", u0.instantiate({p1})) + dtdecl0.addConstructor(ctordecl0) + dtdecl1.addConstructor(ctordecl1) + dt_sorts = solver.mkDatatypeSorts([dtdecl0, dtdecl1], {u0, u1}) + isort1 = dt_sorts[1].instantiate({solver.getBooleanSort()}) + t1 = solver.mkConst(isort1, "t") + t0 = solver.mkTerm( + Kind.ApplySelector, + t1.getSort().getDatatype().getSelector("s1").getSelectorTerm(), + t1) + assert dt_sorts[0].instantiate({solver.getBooleanSort()}) == t0.getSort() def test_mk_function_sort(solver): funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ @@ -271,6 +292,13 @@ def test_mk_uninterpreted_sort(solver): solver.mkUninterpretedSort("") +def test_mk_unresolved_sort(solver): + solver.mkUnresolvedSort("u") + solver.mkUnresolvedSort("u", 1) + solver.mkUnresolvedSort("") + solver.mkUnresolvedSort("", 1) + + def test_mk_sort_constructor_sort(solver): solver.mkSortConstructorSort("s", 2) solver.mkSortConstructorSort("", 2) -- 2.30.2