From 0382c489cafbfc28becfaad3462629f616e93e74 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 27 Jan 2026 19:00:46 +0000 Subject: [PATCH] Add Z3_mk_polymorphic_datatypes API for mutually recursive polymorphic datatypes Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/api_datatype.cpp | 43 ++++++++++ src/api/z3_api.h | 24 ++++++ src/test/parametric_datatype.cpp | 142 +++++++++++++++++++++++++++++++ 3 files changed, 209 insertions(+) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index ee381e3e7..62a27a9c0 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -495,6 +495,49 @@ extern "C" { Z3_CATCH; } + void Z3_API Z3_mk_polymorphic_datatypes(Z3_context c, + unsigned num_sorts, + Z3_symbol const sort_names[], + unsigned const num_params[], + Z3_sort const* params[], + Z3_sort sorts[], + Z3_constructor_list constructor_lists[]) { + Z3_TRY; + // Note: LOG macro not auto-generated for this function due to 2D array parameter + RESET_ERROR_CODE(); + ast_manager& m = mk_c(c)->m(); + mk_c(c)->reset_last_result(); + datatype_util data_util(m); + + ptr_vector datas; + for (unsigned i = 0; i < num_sorts; ++i) { + constructor_list* cl = reinterpret_cast(constructor_lists[i]); + datas.push_back(api_datatype_decl(c, sort_names[i], num_params[i], params[i], cl->size(), reinterpret_cast(cl->data()))); + } + sort_ref_vector _sorts(m); + bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts); + del_datatype_decls(datas.size(), datas.data()); + + if (!ok) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + return; + } + + SASSERT(_sorts.size() == num_sorts); + for (unsigned i = 0; i < _sorts.size(); ++i) { + sort* s = _sorts[i].get(); + mk_c(c)->save_multiple_ast_trail(s); + sorts[i] = of_sort(s); + constructor_list* cl = reinterpret_cast(constructor_lists[i]); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); + for (unsigned j = 0; j < cl->size(); ++j) { + constructor* cn = (*cl)[j]; + cn->m_constructor = cnstrs[j]; + } + } + Z3_CATCH; + } + bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort t) { Z3_TRY; LOG_Z3_is_recursive_datatype_sort(c, t); diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 141c32e5a..bc3035a5a 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2221,6 +2221,30 @@ extern "C" { Z3_sort sorts[], Z3_constructor_list constructor_lists[]); + /** + \brief Create mutually recursive polymorphic datatypes. + + \param c logical context. + \param num_sorts number of datatype sorts. + \param sort_names names of datatype sorts. + \param num_params array of number of type parameters for each sort. + \param params array of arrays of type parameters for each sort. + \param sorts array of datatype sorts (output). + \param constructor_lists list of constructors, one list per sort. + + \sa Z3_mk_constructor + \sa Z3_mk_constructor_list + \sa Z3_mk_datatypes + \sa Z3_mk_polymorphic_datatype + */ + void Z3_API Z3_mk_polymorphic_datatypes(Z3_context c, + unsigned num_sorts, + Z3_symbol const sort_names[], + unsigned const num_params[], + Z3_sort const* params[], + Z3_sort sorts[], + Z3_constructor_list constructor_lists[]); + /** \brief Query constructor for declared functions. diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp index 2a31803aa..d4334b06f 100644 --- a/src/test/parametric_datatype.cpp +++ b/src/test/parametric_datatype.cpp @@ -117,6 +117,148 @@ static void test_polymorphic_datatype_api() { Z3_del_context(ctx); } +/** + * Test Z3_mk_polymorphic_datatypes API for mutually recursive polymorphic datatypes. + * + * This test demonstrates creating mutually recursive parametric datatypes Tree and Forest: + * - Tree has constructor mk-tree(value: T, children: Forest) + * - Forest has constructors empty() and cons(head: Tree, tail: Forest) + */ +static void test_polymorphic_datatypes_api() { + std::cout << "\ntest_polymorphic_datatypes_api\n"; + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Create type variable T for polymorphic datatypes + Z3_symbol t_sym = Z3_mk_string_symbol(ctx, "T"); + Z3_sort t_var = Z3_mk_type_variable(ctx, t_sym); + + // Define datatype names + Z3_symbol tree_name = Z3_mk_string_symbol(ctx, "Tree"); + Z3_symbol forest_name = Z3_mk_string_symbol(ctx, "Forest"); + + // Create forward references for mutual recursion + // Tree has index 0, Forest has index 1 + 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 Tree constructor: mk-tree(value: T, children: Forest) + Z3_symbol mk_tree_sym = Z3_mk_string_symbol(ctx, "mk-tree"); + Z3_symbol is_tree_sym = Z3_mk_string_symbol(ctx, "is-tree"); + Z3_symbol value_sym = Z3_mk_string_symbol(ctx, "value"); + Z3_symbol children_sym = Z3_mk_string_symbol(ctx, "children"); + + Z3_symbol tree_field_names[2] = {value_sym, children_sym}; + Z3_sort tree_field_sorts[2] = {t_var, forest_ref}; // T and Forest + unsigned tree_sort_refs[2] = {0, 1}; // 0=not recursive, 1=reference to Forest (index 1) + + Z3_constructor tree_con = Z3_mk_constructor( + ctx, mk_tree_sym, is_tree_sym, 2, tree_field_names, tree_field_sorts, tree_sort_refs + ); + + // Define Forest constructors: + // 1. empty() + Z3_symbol empty_sym = Z3_mk_string_symbol(ctx, "empty"); + Z3_symbol is_empty_sym = Z3_mk_string_symbol(ctx, "is-empty"); + Z3_constructor empty_con = Z3_mk_constructor( + ctx, empty_sym, is_empty_sym, 0, nullptr, nullptr, nullptr + ); + + // 2. cons(head: Tree, tail: Forest) + Z3_symbol cons_sym = Z3_mk_string_symbol(ctx, "cons"); + Z3_symbol is_cons_sym = Z3_mk_string_symbol(ctx, "is-cons"); + Z3_symbol head_sym = Z3_mk_string_symbol(ctx, "head"); + Z3_symbol tail_sym = Z3_mk_string_symbol(ctx, "tail"); + + Z3_symbol forest_field_names[2] = {head_sym, tail_sym}; + Z3_sort forest_field_sorts[2] = {tree_ref, forest_ref}; // Tree and Forest + unsigned forest_sort_refs[2] = {0, 1}; // 0=reference to Tree (index 0), 1=reference to Forest (index 1) + + Z3_constructor cons_con = Z3_mk_constructor( + ctx, cons_sym, is_cons_sym, 2, forest_field_names, forest_field_sorts, forest_sort_refs + ); + + // Create constructor lists + Z3_constructor tree_constructors[1] = {tree_con}; + Z3_constructor forest_constructors[2] = {empty_con, cons_con}; + + Z3_constructor_list tree_list = Z3_mk_constructor_list(ctx, 1, tree_constructors); + Z3_constructor_list forest_list = Z3_mk_constructor_list(ctx, 2, forest_constructors); + + // Setup parameters for Z3_mk_polymorphic_datatypes + Z3_symbol sort_names[2] = {tree_name, forest_name}; + unsigned num_params[2] = {1, 1}; // Both have one type parameter (T) + Z3_sort const* type_params[2] = {&t_var, &t_var}; + Z3_sort sorts[2]; + Z3_constructor_list constructor_lists[2] = {tree_list, forest_list}; + + // Create the mutually recursive polymorphic datatypes + Z3_mk_polymorphic_datatypes(ctx, 2, sort_names, num_params, type_params, sorts, constructor_lists); + + std::cout << "Created mutually recursive polymorphic datatypes Tree and Forest\n"; + std::cout << "Tree sort: " << Z3_sort_to_string(ctx, sorts[0]) << "\n"; + std::cout << "Forest sort: " << Z3_sort_to_string(ctx, sorts[1]) << "\n"; + + // Clean up constructor lists + Z3_del_constructor_list(ctx, tree_list); + Z3_del_constructor_list(ctx, forest_list); + Z3_del_constructor(ctx, tree_con); + Z3_del_constructor(ctx, empty_con); + Z3_del_constructor(ctx, cons_con); + + // Now instantiate with concrete type Int + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort int_params[1] = {int_sort}; + + Z3_sort tree_int = Z3_mk_datatype_sort(ctx, tree_name, 1, int_params); + Z3_sort forest_int = Z3_mk_datatype_sort(ctx, forest_name, 1, int_params); + + std::cout << "Instantiated Tree: " << Z3_sort_to_string(ctx, tree_int) << "\n"; + std::cout << "Instantiated Forest: " << Z3_sort_to_string(ctx, forest_int) << "\n"; + + // Get constructors from Tree + Z3_func_decl mk_tree_int = Z3_get_datatype_sort_constructor(ctx, tree_int, 0); + Z3_func_decl value_acc = Z3_get_datatype_sort_constructor_accessor(ctx, tree_int, 0, 0); + Z3_func_decl children_acc = Z3_get_datatype_sort_constructor_accessor(ctx, tree_int, 0, 1); + + std::cout << "mk-tree constructor: " << Z3_func_decl_to_string(ctx, mk_tree_int) << "\n"; + + // Get constructors from Forest + Z3_func_decl empty_int = Z3_get_datatype_sort_constructor(ctx, forest_int, 0); + Z3_func_decl cons_int = Z3_get_datatype_sort_constructor(ctx, forest_int, 1); + + // Create an empty forest + Z3_ast empty_forest = Z3_mk_app(ctx, empty_int, 0, nullptr); + std::cout << "Empty forest: " << Z3_ast_to_string(ctx, empty_forest) << "\n"; + + // Create a tree with value 42 and empty forest as children + Z3_ast forty_two = Z3_mk_int(ctx, 42, int_sort); + Z3_ast args[2] = {forty_two, empty_forest}; + Z3_ast tree = Z3_mk_app(ctx, mk_tree_int, 2, args); + std::cout << "Tree with value 42: " << Z3_ast_to_string(ctx, tree) << "\n"; + + // Verify the accessor extracts the correct value + Z3_ast extracted_value = Z3_mk_app(ctx, value_acc, 1, &tree); + std::cout << "Extracted value: " << Z3_ast_to_string(ctx, extracted_value) << "\n"; + + // Verify the sort of extracted value is Int + Z3_sort extracted_sort = Z3_get_sort(ctx, extracted_value); + ENSURE(Z3_is_eq_sort(ctx, extracted_sort, int_sort)); + + // Verify the children accessor returns a Forest + Z3_ast extracted_children = Z3_mk_app(ctx, children_acc, 1, &tree); + Z3_sort children_sort = Z3_get_sort(ctx, extracted_children); + std::cout << "Extracted children sort: " << Z3_sort_to_string(ctx, children_sort) << "\n"; + ENSURE(Z3_is_eq_sort(ctx, children_sort, forest_int)); + + std::cout << "test_polymorphic_datatypes_api passed!\n"; + + Z3_del_context(ctx); +} + void tst_parametric_datatype() { test_polymorphic_datatype_api(); + test_polymorphic_datatypes_api(); }