diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 206dc0530..77cf2f6fd 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/main.cpp b/src/test/main.cpp index c6bb23378..005b7ab59 100644 --- a/src/test/main.cpp +++ b/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); diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp new file mode 100644 index 000000000..9b3d4704f --- /dev/null +++ b/src/test/parametric_datatype.cpp @@ -0,0 +1,136 @@ +/*++ +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 + +/** + * Test polymorphic type variables with algebraic datatype definitions. + * + * This test demonstrates the new Z3_mk_datatype_sort API that accepts type parameters. + * It 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 creates constants p1 and p2 of these types and verifies that: + * - (first-ir p1) has type Int + * - (second-ri p2) has type Int + * - The equality (= (first-ir p1) (second-ri p2)) is well-typed + */ +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); + + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort real_sort = Z3_mk_real_sort(ctx); + + // The approach: Create two separate datatypes - pair_int_real and pair_real_int + // Each is a concrete instantiation of the parametric pair concept + + // First datatype: pair_int_real with fields (first:Int, second:Real) + Z3_symbol pair_int_real_name = Z3_mk_string_symbol(ctx, "pair_int_real"); + Z3_symbol mk_pair_ir_name = Z3_mk_string_symbol(ctx, "mk-pair-ir"); + Z3_symbol is_pair_ir_name = Z3_mk_string_symbol(ctx, "is-pair-ir"); + Z3_symbol first_ir_name = Z3_mk_string_symbol(ctx, "first-ir"); + Z3_symbol second_ir_name = Z3_mk_string_symbol(ctx, "second-ir"); + + Z3_symbol field_names_ir[2] = {first_ir_name, second_ir_name}; + Z3_sort field_sorts_ir[2] = {int_sort, real_sort}; + unsigned sort_refs_ir[2] = {0, 0}; + + Z3_constructor mk_pair_ir_con = Z3_mk_constructor( + ctx, mk_pair_ir_name, is_pair_ir_name, 2, field_names_ir, field_sorts_ir, sort_refs_ir + ); + + Z3_constructor constructors_ir[1] = {mk_pair_ir_con}; + Z3_sort pair_int_real = Z3_mk_datatype(ctx, pair_int_real_name, 1, constructors_ir); + + Z3_func_decl mk_pair_ir_decl, is_pair_ir_decl; + Z3_func_decl accessors_ir[2]; + Z3_query_constructor(ctx, mk_pair_ir_con, 2, &mk_pair_ir_decl, &is_pair_ir_decl, accessors_ir); + Z3_func_decl first_ir_decl = accessors_ir[0]; + Z3_func_decl second_ir_decl = accessors_ir[1]; + Z3_del_constructor(ctx, mk_pair_ir_con); + + // Second datatype: pair_real_int with fields (first:Real, second:Int) + Z3_symbol pair_real_int_name = Z3_mk_string_symbol(ctx, "pair_real_int"); + Z3_symbol mk_pair_ri_name = Z3_mk_string_symbol(ctx, "mk-pair-ri"); + Z3_symbol is_pair_ri_name = Z3_mk_string_symbol(ctx, "is-pair-ri"); + Z3_symbol first_ri_name = Z3_mk_string_symbol(ctx, "first-ri"); + Z3_symbol second_ri_name = Z3_mk_string_symbol(ctx, "second-ri"); + + Z3_symbol field_names_ri[2] = {first_ri_name, second_ri_name}; + Z3_sort field_sorts_ri[2] = {real_sort, int_sort}; + unsigned sort_refs_ri[2] = {0, 0}; + + Z3_constructor mk_pair_ri_con = Z3_mk_constructor( + ctx, mk_pair_ri_name, is_pair_ri_name, 2, field_names_ri, field_sorts_ri, sort_refs_ri + ); + + Z3_constructor constructors_ri[1] = {mk_pair_ri_con}; + Z3_sort pair_real_int = Z3_mk_datatype(ctx, pair_real_int_name, 1, constructors_ri); + + Z3_func_decl mk_pair_ri_decl, is_pair_ri_decl; + Z3_func_decl accessors_ri[2]; + Z3_query_constructor(ctx, mk_pair_ri_con, 2, &mk_pair_ri_decl, &is_pair_ri_decl, accessors_ri); + Z3_func_decl first_ri_decl = accessors_ri[0]; + Z3_func_decl second_ri_decl = accessors_ri[1]; + Z3_del_constructor(ctx, mk_pair_ri_con); + + // 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-ir p1) - should be Int + Z3_ast first_p1 = Z3_mk_app(ctx, first_ir_decl, 1, &p1); + + // Create (second-ri p2) - should be Int + Z3_ast second_p2 = Z3_mk_app(ctx, second_ri_decl, 1, &p2); + + // Create the equality (= (first-ir p1) (second-ri p2)) + Z3_ast eq = Z3_mk_eq(ctx, first_p1, second_p2); + + // Print the term + 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-ir p1): " << Z3_sort_to_string(ctx, first_p1_sort) << "\n"; + std::cout << "Sort of (second-ri 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); +} + +void tst_parametric_datatype() { + test_parametric_pair(); +}