mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Code Activity

Add Z3_mk_polymorphic_datatypes API for mutually recursive polymorphic datatypes

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-27 19:00:46 +00:00
parent ce80556d93
commit 0382c489ca
3 changed files with 209 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/api/api_datatype.cpp
View file

@ -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<datatype_decl> datas;
for (unsigned i = 0; i < num_sorts; ++i) {
constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
datas.push_back(api_datatype_decl(c, sort_names[i], num_params[i], params[i], 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);
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_list*>(constructor_lists[i]);
ptr_vector<func_decl> 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);

24
src/api/z3_api.h
View file

@ -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.

142
src/test/parametric_datatype.cpp
View file

@ -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<T> and Forest<T>:
* - Tree<T> has constructor mk-tree(value: T, children: Forest<T>)
* - Forest<T> has constructors empty() and cons(head: Tree<T>, tail: Forest<T>)
*/
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<T> constructor: mk-tree(value: T, children: Forest<T>)
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<T>
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<T> 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<T>, tail: Forest<T>)
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<T> and Forest<T>
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<T> and Forest<T>\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<Int>: " << Z3_sort_to_string(ctx, tree_int) << "\n";
std::cout << "Instantiated Forest<Int>: " << Z3_sort_to_string(ctx, forest_int) << "\n";
// Get constructors from Tree<Int>
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<Int>
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<Int>
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();
}