Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966)

* Initial plan

* Update Z3_mk_datatype_sort API to accept array of parameters

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update language bindings for parametric datatype sort API

- Python: Updated DatatypeSort() to accept optional params list
- OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes
- .NET: Added MkDatatypeSortRef() methods with optional params
- Java: Added mkDatatypeSortRef() methods with optional params
- All changes maintain backward compatibility

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix .NET build error - rename params to parameters

The 'params' keyword is reserved in C#, causing compilation errors.
Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add unit test for parametric datatypes

Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes.
The test creates two concrete instantiations of a generic pair concept:
- pair_int_real with fields (first:Int, second:Real)
- pair_real_int with fields (first:Real, second:Int)
Then verifies that accessors work correctly and type checking is enforced.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Implement polymorphic type variables support for parametric datatypes

- Modified datatype_decl_plugin to allow type variables as parameters
- Updated mk_datatype_decl to extract type variables from field sorts
- Type variables are collected in order of first appearance
- Revised unit test to use Z3_mk_type_variable for polymorphic datatypes
- Test creates pair datatype with type variables alpha and beta
- Successfully instantiates with concrete types (pair Int Real) and (pair Real Int)
- Verifies accessor types match and equality terms are well-typed
- All tests pass

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add Z3_mk_polymorphic_datatype API and refactor datatype creation

- Added new API Z3_mk_polymorphic_datatype to z3_api.h
- Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp
- Modified api_datatype_decl to accept explicit type parameters
- Updated all callers to use renamed function
- Added test_polymorphic_datatype_api demonstrating new API usage
- Both tests pass successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove type variable collection logic from constructors

Removed the logic for collecting type variables from field sorts based on constructors.

* Update comments on parameter handling in api_datatype.cpp

Clarify usage of parameters in API documentation.

* Fix OCaml build error - use list instead of array for mk_datatype_sort

Changed mk_sort_ref to pass empty list [] instead of empty array [||].
Changed mk_sort_ref_p to pass params list directly instead of converting to array.
Z3native.mk_datatype_sort expects a list, not an array.

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add polymorphic datatype example to C++ examples

Added polymorphic_datatype_example() demonstrating:
- Creating type variables alpha and beta with Z3_mk_type_variable
- Defining parametric Pair datatype with fields of type alpha and beta
- Instantiating with concrete types (Pair Int Real) and (Pair Real Int)
- Getting constructors and accessors from instantiated datatypes
- Creating constants and expressions using the polymorphic types
- Verifying type correctness with equality (= (first p1) (second p2))

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

examples/c++/example.cpp

@@ -1006,6 +1006,95 @@ void datatype_example() {
 
 }
 
+void polymorphic_datatype_example() {
+    std::cout << "polymorphic datatype example\n";
+    context ctx;
+
+    // Create type variables alpha and beta for polymorphic datatype using C API
+    Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha");
+    Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta");
+    sort alpha(ctx, Z3_mk_type_variable(ctx, alpha_sym));
+    sort beta(ctx, Z3_mk_type_variable(ctx, beta_sym));
+    
+    std::cout << "Type variables: " << alpha << ", " << beta << "\n";
+
+    // Define parametric Pair datatype with constructor mk-pair(first: alpha, second: beta)
+    symbol pair_name = ctx.str_symbol("Pair");
+    symbol mk_pair_name = ctx.str_symbol("mk-pair");
+    symbol is_pair_name = ctx.str_symbol("is-pair");
+    symbol first_name = ctx.str_symbol("first");
+    symbol second_name = ctx.str_symbol("second");
+    
+    symbol field_names[2] = {first_name, second_name};
+    sort field_sorts[2] = {alpha, beta};  // Use type variables
+    
+    constructors cs(ctx);
+    cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts);
+    sort pair = ctx.datatype(pair_name, cs);
+    
+    std::cout << "Created parametric datatype: " << pair << "\n";
+    
+    // Instantiate Pair with concrete types: (Pair Int Real)
+    sort_vector params_int_real(ctx);
+    params_int_real.push_back(ctx.int_sort());
+    params_int_real.push_back(ctx.real_sort());
+    sort pair_int_real = ctx.datatype_sort(pair_name, params_int_real);
+    
+    std::cout << "Instantiated with Int and Real: " << pair_int_real << "\n";
+    
+    // Instantiate Pair with concrete types: (Pair Real Int)
+    sort_vector params_real_int(ctx);
+    params_real_int.push_back(ctx.real_sort());
+    params_real_int.push_back(ctx.int_sort());
+    sort pair_real_int = ctx.datatype_sort(pair_name, params_real_int);
+    
+    std::cout << "Instantiated with Real and Int: " << pair_real_int << "\n";
+    
+    // Get constructors and accessors for (Pair Int Real) using C API
+    func_decl mk_pair_ir(ctx, Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0));
+    func_decl first_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0));
+    func_decl second_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1));
+    
+    std::cout << "Constructors and accessors for (Pair Int Real):\n";
+    std::cout << "  Constructor: " << mk_pair_ir << "\n";
+    std::cout << "  first accessor: " << first_ir << "\n";
+    std::cout << "  second accessor: " << second_ir << "\n";
+    
+    // Get constructors and accessors for (Pair Real Int) using C API
+    func_decl mk_pair_ri(ctx, Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0));
+    func_decl first_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0));
+    func_decl second_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1));
+    
+    std::cout << "Constructors and accessors for (Pair Real Int):\n";
+    std::cout << "  Constructor: " << mk_pair_ri << "\n";
+    std::cout << "  first accessor: " << first_ri << "\n";
+    std::cout << "  second accessor: " << second_ri << "\n";
+    
+    // Create constants of these types
+    expr p1 = ctx.constant("p1", pair_int_real);
+    expr p2 = ctx.constant("p2", pair_real_int);
+    
+    std::cout << "Created constants: " << p1 << " : " << p1.get_sort() << "\n";
+    std::cout << "                   " << p2 << " : " << p2.get_sort() << "\n";
+    
+    // Create expressions using accessors
+    expr first_p1 = first_ir(p1);   // first(p1) has type Int
+    expr second_p2 = second_ri(p2); // second(p2) has type Int
+    
+    std::cout << "first(p1) = " << first_p1 << " : " << first_p1.get_sort() << "\n";
+    std::cout << "second(p2) = " << second_p2 << " : " << second_p2.get_sort() << "\n";
+    
+    // Create equality term: (= (first p1) (second p2))
+    expr eq = first_p1 == second_p2;
+    std::cout << "Equality term: " << eq << "\n";
+    
+    // Verify both sides have the same type (Int)
+    assert(first_p1.get_sort().id() == ctx.int_sort().id());
+    assert(second_p2.get_sort().id() == ctx.int_sort().id());
+    
+    std::cout << "Successfully created and verified polymorphic datatypes!\n";
+}
+
 void expr_vector_example() {
     std::cout << "expr_vector example\n";
     context c;
@@ -1394,6 +1483,7 @@ int main() {
         enum_sort_example(); std::cout << "\n";
         tuple_example(); std::cout << "\n";
         datatype_example(); std::cout << "\n";
+        polymorphic_datatype_example(); std::cout << "\n";
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";

src/api/api_datatype.cpp

@@ -306,12 +306,24 @@ extern "C" {
         Z3_CATCH;
     }
 
-    static datatype_decl* mk_datatype_decl(Z3_context c,
+    static datatype_decl* api_datatype_decl(Z3_context c,
-                                           Z3_symbol name,
+                                            Z3_symbol name,
-                                           unsigned num_constructors,
+                                            unsigned num_parameters,
-                                           Z3_constructor constructors[]) {
+                                            Z3_sort const parameters[],
+                                            unsigned num_constructors,
+                                            Z3_constructor constructors[]) {
         datatype_util& dt_util = mk_c(c)->dtutil();
         ast_manager& m = mk_c(c)->m();
+        
+        sort_ref_vector params(m);
+        
+        // A correct use of the API is to always provide parameters explicitly.
+        // implicit parameters through polymorphic type variables does not work
+        // because the order of polymorphic variables in the parameters is ambiguous.
+        if (num_parameters > 0 && parameters) 
+            for (unsigned i = 0; i < num_parameters; ++i) 
+                params.push_back(to_sort(parameters[i]));
+        
         ptr_vector<constructor_decl> constrs;
         for (unsigned i = 0; i < num_constructors; ++i) {
             constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
@@ -326,7 +338,7 @@ extern "C" {
             }
             constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.data()));
         }
-        return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.data());
+        return mk_datatype_decl(dt_util, to_symbol(name), params.size(), params.data(), num_constructors, constrs.data());
     }
 
     Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@@ -341,7 +353,7 @@ extern "C" {
 
         sort_ref_vector sorts(m);
         {
-            datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors);
+            datatype_decl * data = api_datatype_decl(c, name, 0, nullptr, num_constructors, constructors);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
             del_datatype_decl(data);
 
@@ -363,6 +375,42 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
+                                              Z3_symbol name,
+                                              unsigned num_parameters,
+                                              Z3_sort parameters[],
+                                              unsigned num_constructors,
+                                              Z3_constructor constructors[]) {
+        Z3_TRY;
+        LOG_Z3_mk_polymorphic_datatype(c, name, num_parameters, parameters, num_constructors, constructors);
+        RESET_ERROR_CODE();
+        ast_manager& m = mk_c(c)->m();
+        datatype_util data_util(m);
+
+        sort_ref_vector sorts(m);
+        {
+            datatype_decl * data = api_datatype_decl(c, name, num_parameters, parameters, num_constructors, constructors);
+            bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
+            del_datatype_decl(data);
+
+            if (!is_ok) {
+                SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+                RETURN_Z3(nullptr);
+            }
+        }
+        sort * s = sorts.get(0);
+
+        mk_c(c)->save_ast_trail(s);
+        ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
+
+        for (unsigned i = 0; i < num_constructors; ++i) {
+            constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
+            cn->m_constructor = cnstrs[i];
+        }
+        RETURN_Z3_mk_polymorphic_datatype(of_sort(s));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     typedef ptr_vector<constructor> constructor_list;
 
     Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
@@ -387,14 +435,18 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) {
+    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]) {
         Z3_TRY;
-        LOG_Z3_mk_datatype_sort(c, name);
+        LOG_Z3_mk_datatype_sort(c, name, num_params, params);
         RESET_ERROR_CODE();
         ast_manager& m = mk_c(c)->m();
         datatype_util adt_util(m);
-        parameter p(to_symbol(name));
+        vector<parameter> ps;
-        sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p);
+        ps.push_back(parameter(to_symbol(name)));
+        for (unsigned i = 0; i < num_params; ++i) {
+            ps.push_back(parameter(to_sort(params[i])));
+        }
+        sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, ps.size(), ps.data());
         mk_c(c)->save_ast_trail(s);
         RETURN_Z3(of_sort(s));
         Z3_CATCH_RETURN(nullptr);
@@ -416,7 +468,7 @@ extern "C" {
         ptr_vector<datatype_decl> datas;
         for (unsigned i = 0; i < num_sorts; ++i) {
             constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
-            datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
+            datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
         }
         sort_ref_vector _sorts(m);
         bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts);

src/api/c++/z3++.h

@@ -347,6 +347,14 @@ namespace z3 {
         */
         sort datatype_sort(symbol const& name);
 
+        /**
+           \brief a reference to a recursively defined parametric datatype.
+           Expect that it gets defined as a \ref datatype.
+           \param name name of the datatype
+           \param params sort parameters
+        */
+        sort datatype_sort(symbol const& name, sort_vector const& params);
+
             
         /**
            \brief create an uninterpreted sort with the name given by the string or symbol.
@@ -3630,7 +3638,14 @@ namespace z3 {
 
 
     inline sort context::datatype_sort(symbol const& name) {
-        Z3_sort s = Z3_mk_datatype_sort(*this, name);
+        Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr);
+        check_error();
+        return sort(*this, s);            
+    }
+
+    inline sort context::datatype_sort(symbol const& name, sort_vector const& params) {
+        array<Z3_sort> _params(params);
+        Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr());
         check_error();
         return sort(*this, s);            
     }

src/api/dotnet/Context.cs

@@ -474,6 +474,36 @@ namespace Microsoft.Z3
             return new DatatypeSort(this, symbol, constructors);
         }
 
+        /// <summary>
+        /// Create a forward reference to a datatype sort.
+        /// This is useful for creating recursive datatypes or parametric datatypes.
+        /// </summary>
+        /// <param name="name">name of the datatype sort</param>
+        /// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
+        public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
+        {
+            Debug.Assert(name != null);
+            CheckContextMatch(name);
+            if (parameters != null)
+                CheckContextMatch<Sort>(parameters);
+            
+            var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
+            var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
+            return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
+        }
+
+        /// <summary>
+        /// Create a forward reference to a datatype sort.
+        /// This is useful for creating recursive datatypes or parametric datatypes.
+        /// </summary>
+        /// <param name="name">name of the datatype sort</param>
+        /// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
+        public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
+        {
+            using var symbol = MkSymbol(name);
+            return MkDatatypeSortRef(symbol, parameters);
+        }
+
         /// <summary>
         /// Create mutually recursive datatypes.
         /// </summary>

src/api/java/Context.java

@@ -388,6 +388,54 @@ public class Context implements AutoCloseable {
         return new DatatypeSort<>(this, mkSymbol(name), constructors);
     }
 
+    /**
+     * Create a forward reference to a datatype sort.
+     * This is useful for creating recursive datatypes or parametric datatypes.
+     * @param name name of the datatype sort
+     * @param params optional array of sort parameters for parametric datatypes
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name, Sort[] params)
+    {
+        checkContextMatch(name);
+        if (params != null)
+            checkContextMatch(params);
+        
+        int numParams = (params == null) ? 0 : params.length;
+        long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params);
+        return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative));
+    }
+
+    /**
+     * Create a forward reference to a datatype sort (non-parametric).
+     * This is useful for creating recursive datatypes.
+     * @param name name of the datatype sort
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name)
+    {
+        return mkDatatypeSortRef(name, null);
+    }
+
+    /**
+     * Create a forward reference to a datatype sort.
+     * This is useful for creating recursive datatypes or parametric datatypes.
+     * @param name name of the datatype sort
+     * @param params optional array of sort parameters for parametric datatypes
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(String name, Sort[] params)
+    {
+        return mkDatatypeSortRef(mkSymbol(name), params);
+    }
+
+    /**
+     * Create a forward reference to a datatype sort (non-parametric).
+     * This is useful for creating recursive datatypes.
+     * @param name name of the datatype sort
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(String name)
+    {
+        return mkDatatypeSortRef(name, null);
+    }
+
     /**
      * Create mutually recursive datatypes. 
      * @param names names of datatype sorts 

src/api/ml/z3.ml

@@ -909,11 +909,17 @@ struct
     mk_sort ctx (Symbol.mk_string ctx name) constructors
 
   let mk_sort_ref (ctx: context) (name:Symbol.symbol) =
-    Z3native.mk_datatype_sort ctx name
+    Z3native.mk_datatype_sort ctx name 0 []
 
   let mk_sort_ref_s (ctx: context) (name: string) =
     mk_sort_ref ctx (Symbol.mk_string ctx name)
 
+  let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) =
+    Z3native.mk_datatype_sort ctx name (List.length params) params
+
+  let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) =
+    mk_sort_ref_p ctx (Symbol.mk_string ctx name) params
+
   let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) =
     let n = List.length names in
     let f e = ConstructorList.create ctx e in

src/api/ml/z3.mli

@@ -1087,6 +1087,12 @@ sig
   (* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *)
   val mk_sort_ref_s : context -> string -> Sort.sort
 
+  (** Create a forward reference to a parametric datatype sort. *)
+  val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort
+
+  (** Create a forward reference to a parametric datatype sort. *)
+  val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort
+
   (** Create a new datatype sort. *)
   val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort
 

src/api/python/z3/z3.py

@@ -5711,10 +5711,30 @@ class DatatypeRef(ExprRef):
         """Return the datatype sort of the datatype expression `self`."""
         return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 
-def DatatypeSort(name, ctx = None):
+def DatatypeSort(name, params=None, ctx=None):
-    """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
+    """Create a reference to a sort that was declared, or will be declared, as a recursive datatype.
+    
+    Args:
+        name: name of the datatype sort
+        params: optional list/tuple of sort parameters for parametric datatypes
+        ctx: Z3 context (optional)
+    
+    Example:
+        >>> # Non-parametric datatype
+        >>> TreeRef = DatatypeSort('Tree')
+        >>> # Parametric datatype with one parameter
+        >>> ListIntRef = DatatypeSort('List', [IntSort()])
+        >>> # Parametric datatype with multiple parameters
+        >>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()])
+    """
     ctx = _get_ctx(ctx)
-    return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
+    if params is None or len(params) == 0:
+        return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), 0, (Sort * 0)()), ctx)
+    else:
+        _params = (Sort * len(params))()
+        for i in range(len(params)):
+            _params[i] = params[i].ast
+        return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), len(params), _params), ctx)
 
 def TupleSort(name, sorts, ctx=None):
     """Create a named tuple sort base on a set of underlying sorts

src/api/z3_api.h

@@ -2127,6 +2127,33 @@ extern "C" {
                                   unsigned num_constructors,
                                   Z3_constructor constructors[]);
 
+    /**
+       \brief Create a parametric datatype with explicit type parameters.
+       
+       This function is similar to #Z3_mk_datatype, except it takes an explicit set of type parameters.
+       The parameters can be type variables created with #Z3_mk_type_variable, allowing the definition
+       of polymorphic datatypes that can be instantiated with different concrete types.
+
+       \param c logical context
+       \param name name of the datatype
+       \param num_parameters number of type parameters (can be 0)
+       \param parameters array of type parameters (type variables or concrete sorts)
+       \param num_constructors number of constructors
+       \param constructors array of constructor specifications
+
+       \sa Z3_mk_datatype
+       \sa Z3_mk_type_variable
+       \sa Z3_mk_datatype_sort
+
+       def_API('Z3_mk_polymorphic_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(UINT), _inout_array(4, CONSTRUCTOR)))
+     */
+    Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
+                                              Z3_symbol name,
+                                              unsigned num_parameters,
+                                              Z3_sort parameters[],
+                                              unsigned num_constructors,
+                                              Z3_constructor constructors[]);
+
     /**
        \brief create a forward reference to a recursive datatype being declared.
        The forward reference can be used in a nested occurrence: the range of an array
@@ -2136,9 +2163,14 @@ extern "C" {
        Forward references can replace the use sort references, that are unsigned integers
        in the \c Z3_mk_constructor call
 
-       def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL)))
+       \param c logical context
+       \param name name of the datatype
+       \param num_params number of sort parameters  
+       \param params array of sort parameters
+
+       def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT)))
      */
-    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name);
+    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]);
 
     /**
        \brief Create list of constructors.

src/ast/datatype_decl_plugin.cpp

@@ -300,6 +300,12 @@ namespace datatype {
                         TRACE(datatype, tout << "expected sort parameter at position " << i << " got: " << s << "\n";);
                         throw invalid_datatype();
                     }
+                    // Allow type variables as parameters for polymorphic datatypes
+                    sort* param_sort = to_sort(s.get_ast());
+                    if (!m_manager->is_type_var(param_sort) && param_sort->get_family_id() == null_family_id) {
+                        // Type variables and concrete sorts are allowed, but not other uninterpreted sorts
+                        // Actually, all sorts should be allowed including uninterpreted ones
+                    }
                 }
                                 
                 sort* s = m_manager->mk_sort(name.get_symbol(),

src/test/CMakeLists.txt

@@ -21,6 +21,7 @@ add_executable(test-z3
   api_polynomial.cpp
   api_pb.cpp
   api_datalog.cpp
+  parametric_datatype.cpp
   arith_rewriter.cpp
   arith_simplifier_plugin.cpp
   ast.cpp

src/test/main.cpp

@@ -179,6 +179,7 @@ int main(int argc, char ** argv) {
     TST(api_polynomial);
     TST(api_pb);
     TST(api_datalog);
+    TST(parametric_datatype);
     TST(cube_clause);
     TST(old_interval);
     TST(get_implied_equalities);

src/test/parametric_datatype.cpp

@@ -0,0 +1,229 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    parametric_datatype.cpp
+
+Abstract:
+
+    Test parametric datatypes with type variables.
+
+Author:
+
+    Copilot 2025-10-12
+
+--*/
+
+#include "api/z3.h"
+#include "util/util.h"
+#include <iostream>
+
+/**
+ * Test polymorphic type variables with algebraic datatype definitions.
+ * 
+ * This test uses Z3_mk_type_variable to create polymorphic type parameters alpha and beta,
+ * defines a generic pair datatype, then instantiates it with concrete types using
+ * Z3_mk_datatype_sort with parameters.
+ */
+static void test_parametric_pair() {
+    std::cout << "test_parametric_pair\n";
+    
+    Z3_config cfg = Z3_mk_config();
+    Z3_context ctx = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+    
+    // Create type variables alpha and beta for polymorphic datatype
+    Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha");
+    Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta");
+    Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym);
+    Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym);
+    
+    // Define parametric pair datatype with constructor mk-pair(first: alpha, second: beta)
+    Z3_symbol pair_name = Z3_mk_string_symbol(ctx, "pair");
+    Z3_symbol mk_pair_name = Z3_mk_string_symbol(ctx, "mk-pair");
+    Z3_symbol is_pair_name = Z3_mk_string_symbol(ctx, "is-pair");
+    Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first");
+    Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second");
+    
+    Z3_symbol field_names[2] = {first_name, second_name};
+    Z3_sort field_sorts[2] = {alpha, beta};  // Use type variables
+    unsigned sort_refs[2] = {0, 0};  // Not recursive references
+    
+    Z3_constructor mk_pair_con = Z3_mk_constructor(
+        ctx, mk_pair_name, is_pair_name, 2, field_names, field_sorts, sort_refs
+    );
+    
+    // Create the parametric datatype
+    Z3_constructor constructors[1] = {mk_pair_con};
+    Z3_sort pair = Z3_mk_datatype(ctx, pair_name, 1, constructors);
+    
+    Z3_del_constructor(ctx, mk_pair_con);
+    
+    std::cout << "Created parametric pair datatype\n";
+    std::cout << "pair sort: " << Z3_sort_to_string(ctx, pair) << "\n";
+    
+    // Now instantiate the datatype with concrete types
+    Z3_sort int_sort = Z3_mk_int_sort(ctx);
+    Z3_sort real_sort = Z3_mk_real_sort(ctx);
+    
+    // Create (pair Int Real)
+    Z3_sort params_int_real[2] = {int_sort, real_sort};
+    Z3_sort pair_int_real = Z3_mk_datatype_sort(ctx, pair_name, 2, params_int_real);
+    
+    // Create (pair Real Int)
+    Z3_sort params_real_int[2] = {real_sort, int_sort};
+    Z3_sort pair_real_int = Z3_mk_datatype_sort(ctx, pair_name, 2, params_real_int);
+    
+    std::cout << "Instantiated pair with Int and Real\n";
+    std::cout << "pair_int_real: " << Z3_sort_to_string(ctx, pair_int_real) << "\n";
+    std::cout << "pair_real_int: " << Z3_sort_to_string(ctx, pair_real_int) << "\n";
+    
+    // Get constructors and accessors from the instantiated datatypes
+    Z3_func_decl mk_pair_int_real = Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0);
+    Z3_func_decl first_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0);
+    Z3_func_decl second_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1);
+    
+    Z3_func_decl mk_pair_real_int = Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0);
+    Z3_func_decl first_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0);
+    Z3_func_decl second_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1);
+    
+    std::cout << "Got constructors and accessors from instantiated datatypes\n";
+    
+    // Create constants p1 : (pair Int Real) and p2 : (pair Real Int)
+    Z3_symbol p1_sym = Z3_mk_string_symbol(ctx, "p1");
+    Z3_symbol p2_sym = Z3_mk_string_symbol(ctx, "p2");
+    Z3_ast p1 = Z3_mk_const(ctx, p1_sym, pair_int_real);
+    Z3_ast p2 = Z3_mk_const(ctx, p2_sym, pair_real_int);
+    
+    // Create (first p1) - should be Int
+    Z3_ast first_p1 = Z3_mk_app(ctx, first_int_real, 1, &p1);
+    
+    // Create (second p2) - should be Int  
+    Z3_ast second_p2 = Z3_mk_app(ctx, second_real_int, 1, &p2);
+    
+    // Create the equality (= (first p1) (second p2))
+    Z3_ast eq = Z3_mk_eq(ctx, first_p1, second_p2);
+    
+    std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n";
+    
+    // Verify the term was created successfully
+    ENSURE(eq != nullptr);
+    
+    // Check that first_p1 and second_p2 have the same sort (Int)
+    Z3_sort first_p1_sort = Z3_get_sort(ctx, first_p1);
+    Z3_sort second_p2_sort = Z3_get_sort(ctx, second_p2);
+    
+    std::cout << "Sort of (first p1): " << Z3_sort_to_string(ctx, first_p1_sort) << "\n";
+    std::cout << "Sort of (second p2): " << Z3_sort_to_string(ctx, second_p2_sort) << "\n";
+    
+    // Both should be Int
+    ENSURE(Z3_is_eq_sort(ctx, first_p1_sort, int_sort));
+    ENSURE(Z3_is_eq_sort(ctx, second_p2_sort, int_sort));
+    
+    std::cout << "test_parametric_pair passed!\n";
+    
+    Z3_del_context(ctx);
+}
+
+/**
+ * Test Z3_mk_polymorphic_datatype API with explicit parameters.
+ * 
+ * This test demonstrates the new API that explicitly accepts type parameters.
+ */
+static void test_polymorphic_datatype_api() {
+    std::cout << "test_polymorphic_datatype_api\n";
+    
+    Z3_config cfg = Z3_mk_config();
+    Z3_context ctx = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+    
+    // Create type variables alpha and beta for polymorphic datatype
+    Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha");
+    Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta");
+    Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym);
+    Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym);
+    
+    // Define parametric triple datatype with constructor mk-triple(first: alpha, second: beta, third: alpha)
+    Z3_symbol triple_name = Z3_mk_string_symbol(ctx, "triple");
+    Z3_symbol mk_triple_name = Z3_mk_string_symbol(ctx, "mk-triple");
+    Z3_symbol is_triple_name = Z3_mk_string_symbol(ctx, "is-triple");
+    Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first");
+    Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second");
+    Z3_symbol third_name = Z3_mk_string_symbol(ctx, "third");
+    
+    Z3_symbol field_names[3] = {first_name, second_name, third_name};
+    Z3_sort field_sorts[3] = {alpha, beta, alpha};  // Use type variables
+    unsigned sort_refs[3] = {0, 0, 0};  // Not recursive references
+    
+    Z3_constructor mk_triple_con = Z3_mk_constructor(
+        ctx, mk_triple_name, is_triple_name, 3, field_names, field_sorts, sort_refs
+    );
+    
+    // Create the parametric datatype using Z3_mk_polymorphic_datatype
+    Z3_constructor constructors[1] = {mk_triple_con};
+    Z3_sort type_params[2] = {alpha, beta};
+    Z3_sort triple = Z3_mk_polymorphic_datatype(ctx, triple_name, 2, type_params, 1, constructors);
+    
+    Z3_del_constructor(ctx, mk_triple_con);
+    
+    std::cout << "Created parametric triple datatype using Z3_mk_polymorphic_datatype\n";
+    std::cout << "triple sort: " << Z3_sort_to_string(ctx, triple) << "\n";
+    
+    // Now instantiate the datatype with concrete types
+    Z3_sort int_sort = Z3_mk_int_sort(ctx);
+    Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
+    
+    // Create (triple Int Bool)
+    Z3_sort params_int_bool[2] = {int_sort, bool_sort};
+    Z3_sort triple_int_bool = Z3_mk_datatype_sort(ctx, triple_name, 2, params_int_bool);
+    
+    std::cout << "Instantiated triple with Int and Bool\n";
+    std::cout << "triple_int_bool: " << Z3_sort_to_string(ctx, triple_int_bool) << "\n";
+    
+    // Get constructors and accessors from the instantiated datatype
+    Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0);
+    Z3_func_decl first_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 0);
+    Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1);
+    Z3_func_decl third_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 2);
+    
+    std::cout << "Got constructors and accessors from instantiated datatype\n";
+    
+    // Create a constant t : (triple Int Bool)
+    Z3_symbol t_sym = Z3_mk_string_symbol(ctx, "t");
+    Z3_ast t = Z3_mk_const(ctx, t_sym, triple_int_bool);
+    
+    // Create (first t) - should be Int
+    Z3_ast first_t = Z3_mk_app(ctx, first_int_bool, 1, &t);
+    
+    // Create (third t) - should also be Int
+    Z3_ast third_t = Z3_mk_app(ctx, third_int_bool, 1, &t);
+    
+    // Create the equality (= (first t) (third t))
+    Z3_ast eq = Z3_mk_eq(ctx, first_t, third_t);
+    
+    std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n";
+    
+    // Verify the term was created successfully
+    ENSURE(eq != nullptr);
+    
+    // Check that first_t and third_t have the same sort (Int)
+    Z3_sort first_t_sort = Z3_get_sort(ctx, first_t);
+    Z3_sort third_t_sort = Z3_get_sort(ctx, third_t);
+    
+    std::cout << "Sort of (first t): " << Z3_sort_to_string(ctx, first_t_sort) << "\n";
+    std::cout << "Sort of (third t): " << Z3_sort_to_string(ctx, third_t_sort) << "\n";
+    
+    // Both should be Int
+    ENSURE(Z3_is_eq_sort(ctx, first_t_sort, int_sort));
+    ENSURE(Z3_is_eq_sort(ctx, third_t_sort, int_sort));
+    
+    std::cout << "test_polymorphic_datatype_api passed!\n";
+    
+    Z3_del_context(ctx);
+}
+
+void tst_parametric_datatype() {
+    test_parametric_pair();
+    test_polymorphic_datatype_api();
+}