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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a9f7d884a0ae0e78b1a67be249fedcf8f666d9ac..024fa82393a209a9d7a57fac07845839ac26289b 100644 (file)
--- 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 a4ba3ee90578dffa5d10a2661f46ac58feb84aab..726e74363e6f0c7e4f6b78b8dcebb050759d1574 100644 (file)
--- 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 6f86928ca191171ef63433838f4db750ab349d8d..1e24222b3a492fa057e715703354077107a66bf4 100644 (file)
--- 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 2e4404362557e97aa11a3ad9e8071f85dc223cb4..8008ebada03e87fe0e5c0276938308452b96a1a7 100644 (file)
--- 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<Solver*>(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<jlong>(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 8b9a88adcf843bcf04d932d2a9a171ed6743df10..cc1bad1cdb6a477efd2a922c4828311e48ef17ce 100644 (file)
--- 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 2bf72e913531a4b1797a8b53bfb42eaaa49c792e..9c4f59c35c89aa406fe967af32fab468271e1a24 100644 (file)
--- 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 fecf228a5ddd6a8bafd97c752a4765a6341a491a..a4f6bc7221bedcbccb140f9e711ed047cff9ae09 100644 (file)
--- 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<Sort> 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<Sort> 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 31034a15e2bcbed78371805d995bb457ec88df0b..f3bc91eaab913cec2cce6f84eb122728438eef3f 100644 (file)
--- 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<Sort> 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<Sort> 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 e94785b085f93fde9f74bdffeb25b856fd08e96f..002a08ff1b4409724d784be61db4118c7d03d117 100644 (file)
--- 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<Sort> 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<Sort> 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 5d651e82ad4db9b969d86b0ef3317204a5eea4ba..ca0032c22f238fd626a25284ab099cc2295b5c2b 100644 (file)
--- 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<Sort> 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 af34e098e129aa71841c3f304aec68c82f5173a7..2d7e1c8d9928250af649ed73c9bb1c26316ac4ac 100644 (file)
--- 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 d9d6a6c366530c4b2f409fea07f9cd5e05ac6f02..1e9dbcf1f50ec66a1bd1ba0402e8ad8cba0c22a8 100644 (file)
--- 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)