Add Z3_mk_polymorphic_datatypes API for mutually recursive polymorphic datatypes

[Copilot]

The SMT2 format supports mutually recursive polymorphic datatypes (e.g., Tree<T> and Forest<T>), but the C API only provided Z3_mk_polymorphic_datatype (single datatype) and Z3_mk_datatypes (mutually recursive but non-polymorphic). No API existed for the combination.

Changes

Core API (src/api/z3_api.h, src/api/api_datatype.cpp)

• Added Z3_mk_polymorphic_datatypes function
• Takes per-datatype type parameter arrays: num_params[] and params[][]
• Reuses existing api_datatype_decl helper with type parameters

C++ Binding (src/api/c++/z3++.h)

• Overloaded context::datatypes() with sort_vector const* params argument

Test & Example

• Comprehensive test with Tree<T> / Forest<T> example in src/test/parametric_datatype.cpp
• Standalone example in examples/c++/polymorphic_datatypes_example.cpp

Usage

// Create type parameter T
Z3_sort t_var = Z3_mk_type_variable(ctx, Z3_mk_string_symbol(ctx, "T"));

// Create forward references for mutual recursion
Z3_sort tree_ref = Z3_mk_datatype_sort(ctx, tree_name, 1, &t_var);
Z3_sort forest_ref = Z3_mk_datatype_sort(ctx, forest_name, 1, &t_var);

// Define constructors using forward references
Z3_constructor tree_con = Z3_mk_constructor(ctx, "mk-tree", "is-tree", 
    2, (Z3_symbol[]){value, children}, (Z3_sort[]){t_var, forest_ref}, (unsigned[]){0, 0});
    
Z3_constructor cons_con = Z3_mk_constructor(ctx, "cons", "is-cons",
    2, (Z3_symbol[]){head, tail}, (Z3_sort[]){tree_ref, forest_ref}, (unsigned[]){0, 0});

// Create mutually recursive polymorphic datatypes atomically
Z3_symbol names[] = {tree_name, forest_name};
unsigned num_params[] = {1, 1};
Z3_sort const* type_params[] = {&t_var, &t_var};
Z3_sort sorts[2];
Z3_constructor_list lists[] = {tree_list, forest_list};

Z3_mk_polymorphic_datatypes(ctx, 2, names, num_params, type_params, sorts, lists);

// Instantiate with concrete types
Z3_sort tree_int = Z3_mk_datatype_sort(ctx, tree_name, 1, (Z3_sort[]){int_sort});

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Expose an API function to allow defining polymorphic recursive datatypes</issue_title>
<issue_description>The SMT2 format allows polymorphic datatypes to be defined recursively, but the only API exposed allows defining just one polymorphic data type. It would be nice to expose the most generic form of this API. Happy to volunteer a PR if this sounds good.</issue_description>

Comments on the Issue (you are @copilot in this section)

Custom agent used: agentic-workflows
GitHub Agentic Workflows (gh-aw) - Create, debug, and upgrade AI-powered workflows with intelligent prompt routing

• Fixes Expose an API function to allow defining polymorphic recursive datatypes #8375

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.