From 317755776dd7dea3c151f4b4506947e776c4594a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 1 Feb 2026 16:48:19 +0000 Subject: [PATCH] Remove polymorphic_datatypes_example.cpp to fix build - multiple main definitions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- .../c++/polymorphic_datatypes_example.cpp | 150 ------------------ 1 file changed, 150 deletions(-) delete mode 100644 examples/c++/polymorphic_datatypes_example.cpp diff --git a/examples/c++/polymorphic_datatypes_example.cpp b/examples/c++/polymorphic_datatypes_example.cpp deleted file mode 100644 index 55258ff8b..000000000 --- a/examples/c++/polymorphic_datatypes_example.cpp +++ /dev/null @@ -1,150 +0,0 @@ -/** - * Example demonstrating Z3_mk_polymorphic_datatypes API for mutually recursive polymorphic datatypes. - * - * This example creates Tree and Forest datatypes: - * - Tree has constructor: mk-tree(value: T, children: Forest) - * - Forest has constructors: empty() and cons(head: Tree, tail: Forest) - */ - -#include -#include "z3.h" - -int main() { - std::cout << "Polymorphic Recursive Datatypes Example\n\n"; - - // Create context - Z3_config cfg = Z3_mk_config(); - Z3_context ctx = Z3_mk_context(cfg); - Z3_del_config(cfg); - - // Create type parameter T - 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 - 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}; - unsigned tree_sort_refs[2] = {0, 0}; // Both use explicit sorts, not recursive refs - - 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}; - unsigned forest_sort_refs[2] = {0, 0}; // Both use explicit sorts, not recursive refs - - 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:\n"; - std::cout << " Tree: " << Z3_sort_to_string(ctx, sorts[0]) << "\n"; - std::cout << " Forest: " << Z3_sort_to_string(ctx, sorts[1]) << "\n\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); - - // 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 with Int:\n"; - std::cout << " Tree: " << Z3_sort_to_string(ctx, tree_int) << "\n"; - std::cout << " Forest: " << Z3_sort_to_string(ctx, forest_int) << "\n\n"; - - // Get constructors - Z3_func_decl mk_tree_int = Z3_get_datatype_sort_constructor(ctx, tree_int, 0); - 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); - - std::cout << "Constructors:\n"; - std::cout << " mk-tree: " << Z3_func_decl_to_string(ctx, mk_tree_int) << "\n"; - std::cout << " empty: " << Z3_func_decl_to_string(ctx, empty_int) << "\n"; - std::cout << " cons: " << Z3_func_decl_to_string(ctx, cons_int) << "\n\n"; - - // 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 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"; - - // Get accessors and extract value - Z3_func_decl value_acc = Z3_get_datatype_sort_constructor_accessor(ctx, tree_int, 0, 0); - Z3_ast extracted_value = Z3_mk_app(ctx, value_acc, 1, &tree); - std::cout << "Extracted value: " << Z3_ast_to_string(ctx, extracted_value) << "\n\n"; - - // Verify the sort of extracted value is Int - Z3_sort extracted_sort = Z3_get_sort(ctx, extracted_value); - if (Z3_is_eq_sort(ctx, extracted_sort, int_sort)) { - std::cout << "✓ Extracted value has correct sort (Int)\n"; - } - - // Verify the children accessor returns a Forest - Z3_func_decl children_acc = Z3_get_datatype_sort_constructor_accessor(ctx, tree_int, 0, 1); - Z3_ast extracted_children = Z3_mk_app(ctx, children_acc, 1, &tree); - Z3_sort children_sort = Z3_get_sort(ctx, extracted_children); - if (Z3_is_eq_sort(ctx, children_sort, forest_int)) { - std::cout << "✓ Extracted children has correct sort (Forest)\n"; - } - - std::cout << "\nExample completed successfully!\n"; - - Z3_del_context(ctx); - return 0; -}