From 5163411f9b90a339167a41fb3d46a4811420a4db Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 15 Oct 2025 20:51:21 +0200 Subject: [PATCH] Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) * Initial plan * Update Z3_mk_datatype_sort API to accept array of parameters Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update language bindings for parametric datatype sort API - Python: Updated DatatypeSort() to accept optional params list - OCaml: Added mk_sort_ref_p/mk_sort_ref_ps for parametric datatypes - .NET: Added MkDatatypeSortRef() methods with optional params - Java: Added mkDatatypeSortRef() methods with optional params - All changes maintain backward compatibility Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix .NET build error - rename params to parameters The 'params' keyword is reserved in C#, causing compilation errors. Renamed parameter from 'params' to 'parameters' in MkDatatypeSortRef methods. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add unit test for parametric datatypes Added test_parametric_datatype.cpp to demonstrate polymorphic datatypes. The test 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 verifies that accessors work correctly and type checking is enforced. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement polymorphic type variables support for parametric datatypes - Modified datatype_decl_plugin to allow type variables as parameters - Updated mk_datatype_decl to extract type variables from field sorts - Type variables are collected in order of first appearance - Revised unit test to use Z3_mk_type_variable for polymorphic datatypes - Test creates pair datatype with type variables alpha and beta - Successfully instantiates with concrete types (pair Int Real) and (pair Real Int) - Verifies accessor types match and equality terms are well-typed - All tests pass Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add Z3_mk_polymorphic_datatype API and refactor datatype creation - Added new API Z3_mk_polymorphic_datatype to z3_api.h - Renamed static mk_datatype_decl to api_datatype_decl in api_datatype.cpp - Modified api_datatype_decl to accept explicit type parameters - Updated all callers to use renamed function - Added test_polymorphic_datatype_api demonstrating new API usage - Both tests pass successfully Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove type variable collection logic from constructors Removed the logic for collecting type variables from field sorts based on constructors. * Update comments on parameter handling in api_datatype.cpp Clarify usage of parameters in API documentation. * Fix OCaml build error - use list instead of array for mk_datatype_sort Changed mk_sort_ref to pass empty list [] instead of empty array [||]. Changed mk_sort_ref_p to pass params list directly instead of converting to array. Z3native.mk_datatype_sort expects a list, not an array. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add polymorphic datatype example to C++ examples Added polymorphic_datatype_example() demonstrating: - Creating type variables alpha and beta with Z3_mk_type_variable - Defining parametric Pair datatype with fields of type alpha and beta - Instantiating with concrete types (Pair Int Real) and (Pair Real Int) - Getting constructors and accessors from instantiated datatypes - Creating constants and expressions using the polymorphic types - Verifying type correctness with equality (= (first p1) (second p2)) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- examples/c++/example.cpp | 90 ++++++++++++ src/api/api_datatype.cpp | 74 ++++++++-- src/api/c++/z3++.h | 17 ++- src/api/dotnet/Context.cs | 30 ++++ src/api/java/Context.java | 48 +++++++ src/api/ml/z3.ml | 8 +- src/api/ml/z3.mli | 6 + src/api/python/z3/z3.py | 26 +++- src/api/z3_api.h | 36 ++++- src/ast/datatype_decl_plugin.cpp | 6 + src/test/CMakeLists.txt | 1 + src/test/main.cpp | 1 + src/test/parametric_datatype.cpp | 229 +++++++++++++++++++++++++++++++ 13 files changed, 554 insertions(+), 18 deletions(-) create mode 100644 src/test/parametric_datatype.cpp diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 06f3ffe3e..c3902dfff 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -1006,6 +1006,95 @@ void datatype_example() { } +void polymorphic_datatype_example() { + std::cout << "polymorphic datatype example\n"; + context ctx; + + // Create type variables alpha and beta for polymorphic datatype using C API + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + sort alpha(ctx, Z3_mk_type_variable(ctx, alpha_sym)); + sort beta(ctx, Z3_mk_type_variable(ctx, beta_sym)); + + std::cout << "Type variables: " << alpha << ", " << beta << "\n"; + + // Define parametric Pair datatype with constructor mk-pair(first: alpha, second: beta) + symbol pair_name = ctx.str_symbol("Pair"); + symbol mk_pair_name = ctx.str_symbol("mk-pair"); + symbol is_pair_name = ctx.str_symbol("is-pair"); + symbol first_name = ctx.str_symbol("first"); + symbol second_name = ctx.str_symbol("second"); + + symbol field_names[2] = {first_name, second_name}; + sort field_sorts[2] = {alpha, beta}; // Use type variables + + constructors cs(ctx); + cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts); + sort pair = ctx.datatype(pair_name, cs); + + std::cout << "Created parametric datatype: " << pair << "\n"; + + // Instantiate Pair with concrete types: (Pair Int Real) + sort_vector params_int_real(ctx); + params_int_real.push_back(ctx.int_sort()); + params_int_real.push_back(ctx.real_sort()); + sort pair_int_real = ctx.datatype_sort(pair_name, params_int_real); + + std::cout << "Instantiated with Int and Real: " << pair_int_real << "\n"; + + // Instantiate Pair with concrete types: (Pair Real Int) + sort_vector params_real_int(ctx); + params_real_int.push_back(ctx.real_sort()); + params_real_int.push_back(ctx.int_sort()); + sort pair_real_int = ctx.datatype_sort(pair_name, params_real_int); + + std::cout << "Instantiated with Real and Int: " << pair_real_int << "\n"; + + // Get constructors and accessors for (Pair Int Real) using C API + func_decl mk_pair_ir(ctx, Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0)); + func_decl first_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0)); + func_decl second_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1)); + + std::cout << "Constructors and accessors for (Pair Int Real):\n"; + std::cout << " Constructor: " << mk_pair_ir << "\n"; + std::cout << " first accessor: " << first_ir << "\n"; + std::cout << " second accessor: " << second_ir << "\n"; + + // Get constructors and accessors for (Pair Real Int) using C API + func_decl mk_pair_ri(ctx, Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0)); + func_decl first_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0)); + func_decl second_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1)); + + std::cout << "Constructors and accessors for (Pair Real Int):\n"; + std::cout << " Constructor: " << mk_pair_ri << "\n"; + std::cout << " first accessor: " << first_ri << "\n"; + std::cout << " second accessor: " << second_ri << "\n"; + + // Create constants of these types + expr p1 = ctx.constant("p1", pair_int_real); + expr p2 = ctx.constant("p2", pair_real_int); + + std::cout << "Created constants: " << p1 << " : " << p1.get_sort() << "\n"; + std::cout << " " << p2 << " : " << p2.get_sort() << "\n"; + + // Create expressions using accessors + expr first_p1 = first_ir(p1); // first(p1) has type Int + expr second_p2 = second_ri(p2); // second(p2) has type Int + + std::cout << "first(p1) = " << first_p1 << " : " << first_p1.get_sort() << "\n"; + std::cout << "second(p2) = " << second_p2 << " : " << second_p2.get_sort() << "\n"; + + // Create equality term: (= (first p1) (second p2)) + expr eq = first_p1 == second_p2; + std::cout << "Equality term: " << eq << "\n"; + + // Verify both sides have the same type (Int) + assert(first_p1.get_sort().id() == ctx.int_sort().id()); + assert(second_p2.get_sort().id() == ctx.int_sort().id()); + + std::cout << "Successfully created and verified polymorphic datatypes!\n"; +} + void expr_vector_example() { std::cout << "expr_vector example\n"; context c; @@ -1394,6 +1483,7 @@ int main() { enum_sort_example(); std::cout << "\n"; tuple_example(); std::cout << "\n"; datatype_example(); std::cout << "\n"; + polymorphic_datatype_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n"; substitute_example(); std::cout << "\n"; diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 2509434f8..886165455 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -306,12 +306,24 @@ extern "C" { Z3_CATCH; } - static datatype_decl* mk_datatype_decl(Z3_context c, - Z3_symbol name, - unsigned num_constructors, - Z3_constructor constructors[]) { + static datatype_decl* api_datatype_decl(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort const parameters[], + unsigned num_constructors, + Z3_constructor constructors[]) { datatype_util& dt_util = mk_c(c)->dtutil(); ast_manager& m = mk_c(c)->m(); + + sort_ref_vector params(m); + + // A correct use of the API is to always provide parameters explicitly. + // implicit parameters through polymorphic type variables does not work + // because the order of polymorphic variables in the parameters is ambiguous. + if (num_parameters > 0 && parameters) + for (unsigned i = 0; i < num_parameters; ++i) + params.push_back(to_sort(parameters[i])); + ptr_vector constrs; for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(constructors[i]); @@ -326,7 +338,7 @@ extern "C" { } constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.data())); } - return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.data()); + return mk_datatype_decl(dt_util, to_symbol(name), params.size(), params.data(), num_constructors, constrs.data()); } Z3_sort Z3_API Z3_mk_datatype(Z3_context c, @@ -341,7 +353,7 @@ extern "C" { sort_ref_vector sorts(m); { - datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors); + datatype_decl * data = api_datatype_decl(c, name, 0, nullptr, num_constructors, constructors); bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts); del_datatype_decl(data); @@ -363,6 +375,42 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort parameters[], + unsigned num_constructors, + Z3_constructor constructors[]) { + Z3_TRY; + LOG_Z3_mk_polymorphic_datatype(c, name, num_parameters, parameters, num_constructors, constructors); + RESET_ERROR_CODE(); + ast_manager& m = mk_c(c)->m(); + datatype_util data_util(m); + + sort_ref_vector sorts(m); + { + datatype_decl * data = api_datatype_decl(c, name, num_parameters, parameters, num_constructors, constructors); + bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts); + del_datatype_decl(data); + + if (!is_ok) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); + } + } + sort * s = sorts.get(0); + + mk_c(c)->save_ast_trail(s); + ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); + + for (unsigned i = 0; i < num_constructors; ++i) { + constructor* cn = reinterpret_cast(constructors[i]); + cn->m_constructor = cnstrs[i]; + } + RETURN_Z3_mk_polymorphic_datatype(of_sort(s)); + Z3_CATCH_RETURN(nullptr); + } + typedef ptr_vector constructor_list; Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c, @@ -387,14 +435,18 @@ extern "C" { Z3_CATCH; } - Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) { + Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]) { Z3_TRY; - LOG_Z3_mk_datatype_sort(c, name); + LOG_Z3_mk_datatype_sort(c, name, num_params, params); RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); datatype_util adt_util(m); - parameter p(to_symbol(name)); - sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p); + vector ps; + ps.push_back(parameter(to_symbol(name))); + for (unsigned i = 0; i < num_params; ++i) { + ps.push_back(parameter(to_sort(params[i]))); + } + sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, ps.size(), ps.data()); mk_c(c)->save_ast_trail(s); RETURN_Z3(of_sort(s)); Z3_CATCH_RETURN(nullptr); @@ -416,7 +468,7 @@ extern "C" { ptr_vector datas; for (unsigned i = 0; i < num_sorts; ++i) { constructor_list* cl = reinterpret_cast(constructor_lists[i]); - datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast(cl->data()))); + datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, 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); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9fb84236d..71f3ff79b 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -343,6 +343,14 @@ namespace z3 { */ sort datatype_sort(symbol const& name); + /** + \brief a reference to a recursively defined parametric datatype. + Expect that it gets defined as a \ref datatype. + \param name name of the datatype + \param params sort parameters + */ + sort datatype_sort(symbol const& name, sort_vector const& params); + /** \brief create an uninterpreted sort with the name given by the string or symbol. @@ -3625,7 +3633,14 @@ namespace z3 { inline sort context::datatype_sort(symbol const& name) { - Z3_sort s = Z3_mk_datatype_sort(*this, name); + Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr); + check_error(); + return sort(*this, s); + } + + inline sort context::datatype_sort(symbol const& name, sort_vector const& params) { + array _params(params); + Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr()); check_error(); return sort(*this, s); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 9293b1a31..49f183428 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -474,6 +474,36 @@ namespace Microsoft.Z3 return new DatatypeSort(this, symbol, constructors); } + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null) + { + Debug.Assert(name != null); + CheckContextMatch(name); + if (parameters != null) + CheckContextMatch(parameters); + + var numParams = (parameters == null) ? 0 : (uint)parameters.Length; + var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters); + return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative)); + } + + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null) + { + using var symbol = MkSymbol(name); + return MkDatatypeSortRef(symbol, parameters); + } + /// /// Create mutually recursive datatypes. /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 2350b52ae..691ecd737 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -388,6 +388,54 @@ public class Context implements AutoCloseable { return new DatatypeSort<>(this, mkSymbol(name), constructors); } + /** + * Create a forward reference to a datatype sort. + * This is useful for creating recursive datatypes or parametric datatypes. + * @param name name of the datatype sort + * @param params optional array of sort parameters for parametric datatypes + **/ + public DatatypeSort mkDatatypeSortRef(Symbol name, Sort[] params) + { + checkContextMatch(name); + if (params != null) + checkContextMatch(params); + + int numParams = (params == null) ? 0 : params.length; + long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params); + return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative)); + } + + /** + * Create a forward reference to a datatype sort (non-parametric). + * This is useful for creating recursive datatypes. + * @param name name of the datatype sort + **/ + public DatatypeSort mkDatatypeSortRef(Symbol name) + { + return mkDatatypeSortRef(name, null); + } + + /** + * Create a forward reference to a datatype sort. + * This is useful for creating recursive datatypes or parametric datatypes. + * @param name name of the datatype sort + * @param params optional array of sort parameters for parametric datatypes + **/ + public DatatypeSort mkDatatypeSortRef(String name, Sort[] params) + { + return mkDatatypeSortRef(mkSymbol(name), params); + } + + /** + * Create a forward reference to a datatype sort (non-parametric). + * This is useful for creating recursive datatypes. + * @param name name of the datatype sort + **/ + public DatatypeSort mkDatatypeSortRef(String name) + { + return mkDatatypeSortRef(name, null); + } + /** * Create mutually recursive datatypes. * @param names names of datatype sorts diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 4d5238957..cc7294aba 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -909,11 +909,17 @@ struct mk_sort ctx (Symbol.mk_string ctx name) constructors let mk_sort_ref (ctx: context) (name:Symbol.symbol) = - Z3native.mk_datatype_sort ctx name + Z3native.mk_datatype_sort ctx name 0 [] let mk_sort_ref_s (ctx: context) (name: string) = mk_sort_ref ctx (Symbol.mk_string ctx name) + let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) = + Z3native.mk_datatype_sort ctx name (List.length params) params + + let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) = + mk_sort_ref_p ctx (Symbol.mk_string ctx name) params + let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) = let n = List.length names in let f e = ConstructorList.create ctx e in diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 7afc01918..6764b0e2d 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -1087,6 +1087,12 @@ sig (* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *) val mk_sort_ref_s : context -> string -> Sort.sort + (** Create a forward reference to a parametric datatype sort. *) + val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort + + (** Create a forward reference to a parametric datatype sort. *) + val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort + (** Create a new datatype sort. *) val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 051265a78..128726dae 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -5474,10 +5474,30 @@ class DatatypeRef(ExprRef): """Return the datatype sort of the datatype expression `self`.""" return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) -def DatatypeSort(name, ctx = None): - """Create a reference to a sort that was declared, or will be declared, as a recursive datatype""" +def DatatypeSort(name, params=None, ctx=None): + """Create a reference to a sort that was declared, or will be declared, as a recursive datatype. + + Args: + name: name of the datatype sort + params: optional list/tuple of sort parameters for parametric datatypes + ctx: Z3 context (optional) + + Example: + >>> # Non-parametric datatype + >>> TreeRef = DatatypeSort('Tree') + >>> # Parametric datatype with one parameter + >>> ListIntRef = DatatypeSort('List', [IntSort()]) + >>> # Parametric datatype with multiple parameters + >>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()]) + """ ctx = _get_ctx(ctx) - return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx) + if params is None or len(params) == 0: + return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), 0, (Sort * 0)()), ctx) + else: + _params = (Sort * len(params))() + for i in range(len(params)): + _params[i] = params[i].ast + return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), len(params), _params), ctx) def TupleSort(name, sorts, ctx=None): """Create a named tuple sort base on a set of underlying sorts diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9de58e057..baa2fa34c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2127,6 +2127,33 @@ extern "C" { unsigned num_constructors, Z3_constructor constructors[]); + /** + \brief Create a parametric datatype with explicit type parameters. + + This function is similar to #Z3_mk_datatype, except it takes an explicit set of type parameters. + The parameters can be type variables created with #Z3_mk_type_variable, allowing the definition + of polymorphic datatypes that can be instantiated with different concrete types. + + \param c logical context + \param name name of the datatype + \param num_parameters number of type parameters (can be 0) + \param parameters array of type parameters (type variables or concrete sorts) + \param num_constructors number of constructors + \param constructors array of constructor specifications + + \sa Z3_mk_datatype + \sa Z3_mk_type_variable + \sa Z3_mk_datatype_sort + + def_API('Z3_mk_polymorphic_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(UINT), _inout_array(4, CONSTRUCTOR))) + */ + Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c, + Z3_symbol name, + unsigned num_parameters, + Z3_sort parameters[], + unsigned num_constructors, + Z3_constructor constructors[]); + /** \brief create a forward reference to a recursive datatype being declared. The forward reference can be used in a nested occurrence: the range of an array @@ -2136,9 +2163,14 @@ extern "C" { Forward references can replace the use sort references, that are unsigned integers in the \c Z3_mk_constructor call - def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL))) + \param c logical context + \param name name of the datatype + \param num_params number of sort parameters + \param params array of sort parameters + + def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT))) */ - Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name); + Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]); /** \brief Create list of constructors. diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index f91afc9ac..5bb918c5f 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -300,6 +300,12 @@ namespace datatype { TRACE(datatype, tout << "expected sort parameter at position " << i << " got: " << s << "\n";); throw invalid_datatype(); } + // Allow type variables as parameters for polymorphic datatypes + sort* param_sort = to_sort(s.get_ast()); + if (!m_manager->is_type_var(param_sort) && param_sort->get_family_id() == null_family_id) { + // Type variables and concrete sorts are allowed, but not other uninterpreted sorts + // Actually, all sorts should be allowed including uninterpreted ones + } } sort* s = m_manager->mk_sort(name.get_symbol(), 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..2958b934c --- /dev/null +++ b/src/test/parametric_datatype.cpp @@ -0,0 +1,229 @@ +/*++ +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 uses Z3_mk_type_variable to create polymorphic type parameters alpha and beta, + * defines a generic pair datatype, then instantiates it with concrete types using + * Z3_mk_datatype_sort with parameters. + */ +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); + + // Create type variables alpha and beta for polymorphic datatype + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym); + Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym); + + // Define parametric pair datatype with constructor mk-pair(first: alpha, second: beta) + Z3_symbol pair_name = Z3_mk_string_symbol(ctx, "pair"); + Z3_symbol mk_pair_name = Z3_mk_string_symbol(ctx, "mk-pair"); + Z3_symbol is_pair_name = Z3_mk_string_symbol(ctx, "is-pair"); + Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first"); + Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second"); + + Z3_symbol field_names[2] = {first_name, second_name}; + Z3_sort field_sorts[2] = {alpha, beta}; // Use type variables + unsigned sort_refs[2] = {0, 0}; // Not recursive references + + Z3_constructor mk_pair_con = Z3_mk_constructor( + ctx, mk_pair_name, is_pair_name, 2, field_names, field_sorts, sort_refs + ); + + // Create the parametric datatype + Z3_constructor constructors[1] = {mk_pair_con}; + Z3_sort pair = Z3_mk_datatype(ctx, pair_name, 1, constructors); + + Z3_del_constructor(ctx, mk_pair_con); + + std::cout << "Created parametric pair datatype\n"; + std::cout << "pair sort: " << Z3_sort_to_string(ctx, pair) << "\n"; + + // Now instantiate the datatype with concrete types + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort real_sort = Z3_mk_real_sort(ctx); + + // Create (pair Int Real) + Z3_sort params_int_real[2] = {int_sort, real_sort}; + Z3_sort pair_int_real = Z3_mk_datatype_sort(ctx, pair_name, 2, params_int_real); + + // Create (pair Real Int) + Z3_sort params_real_int[2] = {real_sort, int_sort}; + Z3_sort pair_real_int = Z3_mk_datatype_sort(ctx, pair_name, 2, params_real_int); + + std::cout << "Instantiated pair with Int and Real\n"; + std::cout << "pair_int_real: " << Z3_sort_to_string(ctx, pair_int_real) << "\n"; + std::cout << "pair_real_int: " << Z3_sort_to_string(ctx, pair_real_int) << "\n"; + + // Get constructors and accessors from the instantiated datatypes + Z3_func_decl mk_pair_int_real = Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0); + Z3_func_decl first_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0); + Z3_func_decl second_int_real = Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1); + + Z3_func_decl mk_pair_real_int = Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0); + Z3_func_decl first_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0); + Z3_func_decl second_real_int = Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1); + + std::cout << "Got constructors and accessors from instantiated datatypes\n"; + + // 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 p1) - should be Int + Z3_ast first_p1 = Z3_mk_app(ctx, first_int_real, 1, &p1); + + // Create (second p2) - should be Int + Z3_ast second_p2 = Z3_mk_app(ctx, second_real_int, 1, &p2); + + // Create the equality (= (first p1) (second p2)) + Z3_ast eq = Z3_mk_eq(ctx, first_p1, second_p2); + + 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 p1): " << Z3_sort_to_string(ctx, first_p1_sort) << "\n"; + std::cout << "Sort of (second 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); +} + +/** + * Test Z3_mk_polymorphic_datatype API with explicit parameters. + * + * This test demonstrates the new API that explicitly accepts type parameters. + */ +static void test_polymorphic_datatype_api() { + std::cout << "test_polymorphic_datatype_api\n"; + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + // Create type variables alpha and beta for polymorphic datatype + Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha"); + Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta"); + Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym); + Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym); + + // Define parametric triple datatype with constructor mk-triple(first: alpha, second: beta, third: alpha) + Z3_symbol triple_name = Z3_mk_string_symbol(ctx, "triple"); + Z3_symbol mk_triple_name = Z3_mk_string_symbol(ctx, "mk-triple"); + Z3_symbol is_triple_name = Z3_mk_string_symbol(ctx, "is-triple"); + Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first"); + Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second"); + Z3_symbol third_name = Z3_mk_string_symbol(ctx, "third"); + + Z3_symbol field_names[3] = {first_name, second_name, third_name}; + Z3_sort field_sorts[3] = {alpha, beta, alpha}; // Use type variables + unsigned sort_refs[3] = {0, 0, 0}; // Not recursive references + + Z3_constructor mk_triple_con = Z3_mk_constructor( + ctx, mk_triple_name, is_triple_name, 3, field_names, field_sorts, sort_refs + ); + + // Create the parametric datatype using Z3_mk_polymorphic_datatype + Z3_constructor constructors[1] = {mk_triple_con}; + Z3_sort type_params[2] = {alpha, beta}; + Z3_sort triple = Z3_mk_polymorphic_datatype(ctx, triple_name, 2, type_params, 1, constructors); + + Z3_del_constructor(ctx, mk_triple_con); + + std::cout << "Created parametric triple datatype using Z3_mk_polymorphic_datatype\n"; + std::cout << "triple sort: " << Z3_sort_to_string(ctx, triple) << "\n"; + + // Now instantiate the datatype with concrete types + Z3_sort int_sort = Z3_mk_int_sort(ctx); + Z3_sort bool_sort = Z3_mk_bool_sort(ctx); + + // Create (triple Int Bool) + Z3_sort params_int_bool[2] = {int_sort, bool_sort}; + Z3_sort triple_int_bool = Z3_mk_datatype_sort(ctx, triple_name, 2, params_int_bool); + + std::cout << "Instantiated triple with Int and Bool\n"; + std::cout << "triple_int_bool: " << Z3_sort_to_string(ctx, triple_int_bool) << "\n"; + + // Get constructors and accessors from the instantiated datatype + Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0); + Z3_func_decl first_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 0); + Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1); + Z3_func_decl third_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 2); + + std::cout << "Got constructors and accessors from instantiated datatype\n"; + + // Create a constant t : (triple Int Bool) + Z3_symbol t_sym = Z3_mk_string_symbol(ctx, "t"); + Z3_ast t = Z3_mk_const(ctx, t_sym, triple_int_bool); + + // Create (first t) - should be Int + Z3_ast first_t = Z3_mk_app(ctx, first_int_bool, 1, &t); + + // Create (third t) - should also be Int + Z3_ast third_t = Z3_mk_app(ctx, third_int_bool, 1, &t); + + // Create the equality (= (first t) (third t)) + Z3_ast eq = Z3_mk_eq(ctx, first_t, third_t); + + std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n"; + + // Verify the term was created successfully + ENSURE(eq != nullptr); + + // Check that first_t and third_t have the same sort (Int) + Z3_sort first_t_sort = Z3_get_sort(ctx, first_t); + Z3_sort third_t_sort = Z3_get_sort(ctx, third_t); + + std::cout << "Sort of (first t): " << Z3_sort_to_string(ctx, first_t_sort) << "\n"; + std::cout << "Sort of (third t): " << Z3_sort_to_string(ctx, third_t_sort) << "\n"; + + // Both should be Int + ENSURE(Z3_is_eq_sort(ctx, first_t_sort, int_sort)); + ENSURE(Z3_is_eq_sort(ctx, third_t_sort, int_sort)); + + std::cout << "test_polymorphic_datatype_api passed!\n"; + + Z3_del_context(ctx); +} + +void tst_parametric_datatype() { + test_parametric_pair(); + test_polymorphic_datatype_api(); +}