mirror of
https://github.com/Z3Prover/z3
synced 2025-11-05 13:56:03 +00:00
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 <nbjorner@microsoft.com>
This commit is contained in:
Copilot
Nikolaj Bjorner
parent
493481a27e
commit
df334cb54c
13 changed files with 554 additions and 18 deletions
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue