Remove variant of mkDatatypeDecl with one sort parameter (#8543)

Subsumed by the vector version.

Also marks more methods as experimetnal.

diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp
index bbdaa7e0f53261d6ef884fede78b7ac4564fe669..6cfa462e6be08dbf5abc1820b6d5e17270b5ec08 100644 (file)
--- a/examples/api/cpp/datatypes.cpp
+++ b/examples/api/cpp/datatypes.cpp
@@ -100,8 +100,7 @@ void test(Solver& slv, Sort& consListSort)
   // constructor "cons".
   Sort sort = slv.mkParamSort("T");
   DatatypeDecl paramConsListSpec =
-      slv.mkDatatypeDecl("paramlist",
-                         sort);  // give the datatype a name
+      slv.mkDatatypeDecl("paramlist", {sort});  // give the datatype a name
   DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);

diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 03c80c0a0818a01da2e5b1251cb27d7911774629..85ee457413c66725d5007e96b34dbaaf44e5715d 100644 (file)
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -96,8 +96,8 @@ public class Datatypes
     // This example builds a simple parameterized list of sort T, with one
     // constructor "cons".
     Sort sort = slv.mkParamSort("T");
-    DatatypeDecl paramConsListSpec = slv.mkDatatypeDecl("paramlist",
-        sort); // give the datatype a name
+    DatatypeDecl paramConsListSpec = slv.mkDatatypeDecl(
+        "paramlist", new Sort[] {sort}); // give the datatype a name
     DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
     paramCons.addSelector("head", sort);

diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index 24226d44353d421cc1128ffa0147328a50077a41..8678c18703bc07a523e210e8a24b63999a01fab8 100644 (file)
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -85,7 +85,7 @@ def test(slv, consListSort):
     # This example builds a simple parameterized list of sort T, with one
     # constructor "cons".
     sort = slv.mkParamSort("T")
-    paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort)
+    paramConsListSpec = slv.mkDatatypeDecl("paramlist", [sort])
     paramCons = slv.mkDatatypeConstructorDecl("cons")
     paramNil = slv.mkDatatypeConstructorDecl("nil")
     paramCons.addSelector("head", sort)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 2da46514e94b4f7cb3c6eba3bb134fe701a86e63..1c9d85240bd6354c3f8017a6459e92d4b34e77f2 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6057,18 +6057,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype)
   CVC5_API_TRY_CATCH_END;
 }
 
-DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
-                                    const Sort& param,
-                                    bool isCoDatatype)
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_SOLVER_CHECK_SORT(param);
-  //////// all checks before this line
-  return DatatypeDecl(this, name, param, isCoDatatype);
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
                                     const std::vector<Sort>& params,
                                     bool isCoDatatype)

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 78bad1eeec215e5a30d4d2f6c666127d030ec405..eba7dbdb9d6ea85b95166a168c0f24e067be430c 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -1913,7 +1913,11 @@ class CVC5_EXPORT DatatypeDecl
   /** Get the number of constructors (so far) for this Datatype declaration. */
   size_t getNumConstructors() const;
 
-  /** Is this Datatype declaration parametric? */
+  /**
+   * Is this Datatype declaration parametric?
+   *
+   * @warning This method is experimental and may change in future versions.
+   */
   bool isParametric() const;
 
   /**
@@ -3744,18 +3748,9 @@ class CVC5_EXPORT Solver
   /**
    * Create a datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param name the name of the datatype
-   * @param param the sort parameter
-   * @param isCoDatatype true if a codatatype is to be constructed
-   * @return the DatatypeDecl
-   */
-  DatatypeDecl mkDatatypeDecl(const std::string& name,
-                              const Sort& param,
-                              bool isCoDatatype = false);
-
-  /**
-   * Create a datatype declaration.
-   * Create sorts parameter with Solver::mkParamSort().
+   *
+   * @warning This method is experimental and may change in future versions.
+   *
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @param isCoDatatype true if a codatatype is to be constructed

diff --git a/src/api/java/io/github/cvc5/DatatypeDecl.java b/src/api/java/io/github/cvc5/DatatypeDecl.java
index aacbed8ab044f6681db0469c6c983ea60eabf3b8..8fdcaf420c45ee7d8d45a182b8068e11b1ba378b 100644 (file)
--- a/src/api/java/io/github/cvc5/DatatypeDecl.java
+++ b/src/api/java/io/github/cvc5/DatatypeDecl.java
@@ -62,7 +62,11 @@ public class DatatypeDecl extends AbstractPointer
 
   private native int getNumConstructors(long pointer);
 
-  /** @return true if this datatype is parametric */
+  /**
+   * @return true if this DatatypeDecl is parametric
+   *
+   * @api.note This method is experimental and may change in future versions.
+   */
   public boolean isParametric()
   {
     return isParametric(pointer);

diff --git a/src/api/java/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java
index ccff49870da82c82dade4cb5e5b9e5488f8a9acf..feaed83e5571e436af711054bd935abf209b5b07 100644 (file)
--- a/src/api/java/io/github/cvc5/Solver.java
+++ b/src/api/java/io/github/cvc5/Solver.java
@@ -1340,35 +1340,9 @@ public class Solver implements IPointer, AutoCloseable
   /**
    * Create a datatype declaration.
    * Create sorts parameter with Solver::mkParamSort().
-   * @param name the name of the datatype
-   * @param param the sort parameter
-   * @return the DatatypeDecl
-   */
-  public DatatypeDecl mkDatatypeDecl(String name, Sort param)
-  {
-    return mkDatatypeDecl(name, param, false);
-  }
-
-  /**
-   * Create a datatype declaration.
-   * Create sorts parameter with Solver::mkParamSort().
-   * @param name the name of the datatype
-   * @param param the sort parameter
-   * @param isCoDatatype true if a codatatype is to be constructed
-   * @return the DatatypeDecl
-   */
-  public DatatypeDecl mkDatatypeDecl(String name, Sort param, boolean isCoDatatype)
-  {
-    long declPointer = mkDatatypeDecl(pointer, name, param.getPointer(), isCoDatatype);
-    return new DatatypeDecl(this, declPointer);
-  }
-
-  private native long mkDatatypeDecl(
-      long pointer, String name, long paramPointer, boolean isCoDatatype);
-
-  /**
-   * Create a datatype declaration.
-   * Create sorts parameter with Solver::mkParamSort().
+   *
+   * @api.note This method is experimental and may change in future versions.
+   *
    * @param name the name of the datatype
    * @param params a list of sort parameters
    * @return the DatatypeDecl

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index c39d732ad24b54f6660496043c544469697b7d7c..75db6960a5e13f2cbcd5e3574e4e78795f15b08c 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -1451,32 +1451,6 @@ Java_io_github_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2Z(
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
-/*
- * Class:     io_github_cvc5_Solver
- * Method:    mkDatatypeDecl
- * Signature: (JLjava/lang/String;JZ)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ(
-    JNIEnv* env,
-    jobject,
-    jlong pointer,
-    jstring jName,
-    jlong paramPointer,
-    jboolean isCoDatatype)
-{
-  CVC5_JAVA_API_TRY_CATCH_BEGIN;
-  Solver* solver = reinterpret_cast<Solver*>(pointer);
-  const char* s = env->GetStringUTFChars(jName, nullptr);
-  std::string cName(s);
-  Sort* param = reinterpret_cast<Sort*>(paramPointer);
-  DatatypeDecl* retPointer = new DatatypeDecl(
-      solver->mkDatatypeDecl(cName, *param, (bool)isCoDatatype));
-  env->ReleaseStringUTFChars(jName, s);
-  return reinterpret_cast<jlong>(retPointer);
-  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
 /*
  * Class:     io_github_cvc5_Solver
  * Method:    mkDatatypeDecl

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index c4fb71c5cb13008cce7abdd8a6ecc9d0ed320678..c6209434100735122b503f97feb39d12ff0deecc 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -292,8 +292,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5":
         DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name) except +
         DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except +
-        DatatypeDecl mkDatatypeDecl(const string& name, const Sort& param) except +
-        DatatypeDecl mkDatatypeDecl(const string& name, const Sort& param, bint isCoDatatype) except +
         DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params) except +
         DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params, bint isCoDatatype) except +
         # default value for symbol defined in cpp/cvc5.h

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index f43888edd313726fdfac1651f06eea31341a48dc..441648f671d236dcc84e12338870f43a5261025e 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -450,6 +450,9 @@ cdef class DatatypeDecl:
 
     def isParametric(self):
         """
+            .. warning:: This method is experimental and may change in future
+                         versions.
+
             :return: True if this datatype declaration is parametric.
         """
         return self.cdd.isParametric()
@@ -1580,10 +1583,6 @@ cdef class Solver:
             if isinstance(sorts_or_bool, bool):
                 dd.cdd = self.csolver.mkDatatypeDecl(
                         <const string &> name.encode(), <bint> sorts_or_bool)
-            elif isinstance(sorts_or_bool, Sort):
-                dd.cdd = self.csolver.mkDatatypeDecl(
-                        <const string &> name.encode(),
-                        (<Sort> sorts_or_bool).csort)
             elif isinstance(sorts_or_bool, list):
                 for s in sorts_or_bool:
                     v.push_back((<Sort?> s).csort)
@@ -1594,12 +1593,7 @@ cdef class Solver:
                 raise ValueError("Unhandled second argument type {}"
                                  .format(type(sorts_or_bool)))
         elif sorts_or_bool is not None and isCoDatatype is not None:
-            if isinstance(sorts_or_bool, Sort):
-                dd.cdd = self.csolver.mkDatatypeDecl(
-                        <const string &> name.encode(),
-                        (<Sort> sorts_or_bool).csort,
-                        <bint> isCoDatatype)
-            elif isinstance(sorts_or_bool, list):
+            if isinstance(sorts_or_bool, list):
                 for s in sorts_or_bool:
                     v.push_back((<Sort?> s).csort)
                 dd.cdd = self.csolver.mkDatatypeDecl(

diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp
index d7f30cbe18d16e2dcccfb6d9857961d251a066fb..80c1fbc52b0f58fac6960b203a35af33221237bf 100644 (file)
--- a/test/unit/api/cpp/parametric_datatype_black.cpp
+++ b/test/unit/api/cpp/parametric_datatype_black.cpp
@@ -34,7 +34,7 @@ TEST_F(TestApiBlackParametricDatatype, proj_issue387)
   Sort p2 = d_solver.mkParamSort("_x27");
   Sort p3 = d_solver.mkParamSort("_x3");
 
-  DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("_x0", p1);
+  DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("_x0", {p1});
   DatatypeConstructorDecl ctordecl1 =
       d_solver.mkDatatypeConstructorDecl("_x18");
   ASSERT_THROW(ctordecl1.addSelector("_x17", u2.instantiate({p1, p1})),

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 17812748badbf80f9fd559197236aba76297152c..7183d1d0c1f0672b0bbe917aa2a3121933b5961d 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -214,8 +214,8 @@ TEST_F(TestApiBlackSolver, mkDatatypeSorts)
   Sort p1 = d_solver.mkParamSort("p1");
   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);
+  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");
@@ -838,7 +838,7 @@ TEST_F(TestApiBlackSolver, mkTermFromOp)
 
   // list datatype
   Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", {sort});
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);
@@ -2960,7 +2960,7 @@ TEST_F(TestApiBlackSolver, proj_issue378)
   Term t7 = d_solver.mkConst(s2, "_x58");
 
   Sort sp = d_solver.mkParamSort("_x178");
-  dtdecl = d_solver.mkDatatypeDecl("_x176", sp);
+  dtdecl = d_solver.mkDatatypeDecl("_x176", {sp});
   cdecl = d_solver.mkDatatypeConstructorDecl("_x184");
   cdecl.addSelector("_x180", s2);
   dtdecl.addConstructor(cdecl);
@@ -2984,7 +2984,7 @@ TEST_F(TestApiBlackSolver, proj_issue379)
   Sort bsort = d_solver.getBooleanSort();
   Sort psort = d_solver.mkParamSort("_x1");
   DatatypeConstructorDecl cdecl;
-  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("x_0", psort);
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("x_0", {psort});
   cdecl = d_solver.mkDatatypeConstructorDecl("_x8");
   cdecl.addSelector("_x7", bsort);
   dtdecl.addConstructor(cdecl);
@@ -3021,7 +3021,7 @@ TEST_F(TestApiBlackSolver, proj_issue381)
   Sort s1 = d_solver.getBooleanSort();
 
   Sort psort = d_solver.mkParamSort("_x9");
-  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x8", psort);
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x8", {psort});
   DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x22");
   ctor.addSelector("_x19", s1);
   dtdecl.addConstructor(ctor);
@@ -3047,7 +3047,7 @@ TEST_F(TestApiBlackSolver, proj_issue382)
   Sort psort = d_solver.mkParamSort("_x1");
   DatatypeConstructorDecl ctor = d_solver.mkDatatypeConstructorDecl("_x20");
   ctor.addSelector("_x19", psort);
-  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", psort);
+  DatatypeDecl dtdecl = d_solver.mkDatatypeDecl("_x0", {psort});
   dtdecl.addConstructor(ctor);
   Sort s2 = d_solver.mkDatatypeSort(dtdecl);
   Sort s6 = s2.instantiate({s1});

diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp
index 8a716faec49cecdeb3c7cbd18dd74e896990fcc8..c42253dd95a03476f46400d076543b280fe59acc 100644 (file)
--- a/test/unit/api/cpp/sort_black.cpp
+++ b/test/unit/api/cpp/sort_black.cpp
@@ -37,7 +37,7 @@ class TestApiBlackSort : public TestApi
   Sort create_param_datatype_sort()
   {
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", {sort});
     DatatypeConstructorDecl paramCons =
         d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl paramNil =

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index ec4743037cb3abe596bbb3c58156e88b513cc541..a107405973fc4afe4cbcaa99bc4ee5a86dc0d770 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -175,7 +175,7 @@ TEST_F(TestApiBlackTerm, getOp)
 
   // Test Datatypes Ops
   Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", {sort});
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);

diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp
index 86d6b976ed4567fc436a52fc3667b38fcd58c4bf..043cde805f684fdf05fa3a8c0240ff92176c69e8 100644 (file)
--- a/test/unit/api/cpp/term_white.cpp
+++ b/test/unit/api/cpp/term_white.cpp
@@ -50,7 +50,7 @@ TEST_F(TestApiWhiteTerm, getOp)
 
   // Test Datatypes Ops
   Sort sort = d_solver.mkParamSort("T");
-  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+  DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", {sort});
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index bd21caeb98cf7d13228002d35bd6443231759113..6327bb553b8f7ab2e0e88e57ad7a21f1af254957 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -203,8 +203,8 @@ class SolverTest
     Sort p1 = d_solver.mkParamSort("p1");
     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);
+    DatatypeDecl dtdecl0 = d_solver.mkDatatypeDecl("dt0", new Sort[] {p0});
+    DatatypeDecl dtdecl1 = d_solver.mkDatatypeDecl("dt1", new Sort[] {p1});
     DatatypeConstructorDecl ctordecl0 = d_solver.mkDatatypeConstructorDecl("c0");
     ctordecl0.addSelector("s0", u1.instantiate(new Sort[] {p0}));
     DatatypeConstructorDecl ctordecl1 = d_solver.mkDatatypeConstructorDecl("c1");
@@ -821,7 +821,8 @@ class SolverTest
 
     // list datatype
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeDecl listDecl =
+        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
     cons.addSelector("head", sort);

diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 1396b27c7f264f18962e04b0b456256d113adae7..2255153ab438519c1af1830e17448ab43c59b328 100644 (file)
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -58,7 +58,8 @@ class SortTest
   Sort create_param_datatype_sort() throws CVC5ApiException
   {
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeDecl paramDtypeSpec =
+        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl paramCons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
     paramCons.addSelector("head", sort);

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index c8ee81f0a7e35d00c03b8e897ed79b31cc8859e4..5f88904a449b4b0307028f1cd0e5780ef28d8968 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -210,7 +210,8 @@ class TermTest
 
     // Test Datatypes Ops
     Sort sort = d_solver.mkParamSort("T");
-    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeDecl listDecl =
+        d_solver.mkDatatypeDecl("paramlist", new Sort[] {sort});
     DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
     DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
     cons.addSelector("head", sort);

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 53821e1740a7a11b2fd0af08d1ad12270ce9ad93..657df330659433e9d728c646c018f649457c26ef 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -164,8 +164,8 @@ def test_mk_datatype_sorts(solver):
     p1 = solver.mkParamSort("p1")
     u0 = solver.mkUnresolvedDatatypeSort("dt0", 1)
     u1 = solver.mkUnresolvedDatatypeSort("dt1", 1)
-    dtdecl0 = solver.mkDatatypeDecl("dt0", p0)
-    dtdecl1 = solver.mkDatatypeDecl("dt1", p1)
+    dtdecl0 = solver.mkDatatypeDecl("dt0", [p0])
+    dtdecl1 = solver.mkDatatypeDecl("dt1", [p1])
     ctordecl0 = solver.mkDatatypeConstructorDecl("c0")
     ctordecl0.addSelector("s0", u1.instantiate({p0}))
     ctordecl1 = solver.mkDatatypeConstructorDecl("c1")
@@ -813,7 +813,7 @@ def test_mk_term_from_op(solver):
 
     # list datatype
     sort = solver.mkParamSort("T")
-    listDecl = solver.mkDatatypeDecl("paramlist", sort)
+    listDecl = solver.mkDatatypeDecl("paramlist", [sort])
     cons = solver.mkDatatypeConstructorDecl("cons")
     nil = solver.mkDatatypeConstructorDecl("nil")
     cons.addSelector("head", sort)

diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
index 77800d69eebbe0585bd01ae0c076e1d70a4aa803..b70ba22d34a92eda0f885fe17c997b4c9f882028 100644 (file)
--- a/test/unit/api/python/test_sort.py
+++ b/test/unit/api/python/test_sort.py
@@ -41,7 +41,7 @@ def create_datatype_sort(solver):
 
 def create_param_datatype_sort(solver):
     sort = solver.mkParamSort("T")
-    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", [sort])
     paramCons = solver.mkDatatypeConstructorDecl("cons")
     paramNil = solver.mkDatatypeConstructorDecl("nil")
     paramCons.addSelector("head", sort)

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index b9fc1e46a84d2b4c10f03c8f8262971d4180ddee..9416c3a1f18db7a800c785c0b46d07c60bb3f353 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -175,7 +175,7 @@ def test_get_op(solver):
 
     # Test Datatypes Ops
     sort = solver.mkParamSort("T")
-    listDecl = solver.mkDatatypeDecl("paramlist", sort)
+    listDecl = solver.mkDatatypeDecl("paramlist", [sort])
     cons = solver.mkDatatypeConstructorDecl("cons")
     nil = solver.mkDatatypeConstructorDecl("nil")
     cons.addSelector("head", sort)