From: Andrew Reynolds Date: Sat, 2 Apr 2022 19:21:46 +0000 (-0500) Subject: Remove variant of mkDatatypeDecl with one sort parameter (#8543) X-Git-Tag: cvc5-1.0.0~36 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=40910fb3c633a22acf990ce4a544c8594b92b56d;p=cvc5.git 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 bbdaa7e0f..6cfa462e6 100644 --- 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 03c80c0a0..85ee45741 100644 --- 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 24226d443..8678c1870 100644 --- 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 2da46514e..1c9d85240 100644 --- 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& params, bool isCoDatatype) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 78bad1eee..eba7dbdb9 100644 --- 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 aacbed8ab..8fdcaf420 100644 --- 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 ccff49870..feaed83e5 100644 --- 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 c39d732ad..75db6960a 100644 --- 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(pointer); - const char* s = env->GetStringUTFChars(jName, nullptr); - std::string cName(s); - Sort* param = reinterpret_cast(paramPointer); - DatatypeDecl* retPointer = new DatatypeDecl( - solver->mkDatatypeDecl(cName, *param, (bool)isCoDatatype)); - env->ReleaseStringUTFChars(jName, s); - return reinterpret_cast(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 c4fb71c5c..c62094341 100644 --- 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 f43888edd..441648f67 100644 --- 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( name.encode(), sorts_or_bool) - elif isinstance(sorts_or_bool, Sort): - dd.cdd = self.csolver.mkDatatypeDecl( - name.encode(), - ( sorts_or_bool).csort) elif isinstance(sorts_or_bool, list): for s in sorts_or_bool: v.push_back(( 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( - name.encode(), - ( sorts_or_bool).csort, - isCoDatatype) - elif isinstance(sorts_or_bool, list): + if isinstance(sorts_or_bool, list): for s in sorts_or_bool: v.push_back(( 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 d7f30cbe1..80c1fbc52 100644 --- 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 17812748b..7183d1d0c 100644 --- 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 8a716faec..c42253dd9 100644 --- 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 ec4743037..a10740597 100644 --- 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 86d6b976e..043cde805 100644 --- 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 bd21caeb9..6327bb553 100644 --- 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 1396b27c7..2255153ab 100644 --- 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 c8ee81f0a..5f88904a4 100644 --- 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 53821e174..657df3306 100644 --- 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 77800d69e..b70ba22d3 100644 --- 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 b9fc1e46a..9416c3a1f 100644 --- 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)