mirror of
https://github.com/Z3Prover/z3
synced 2025-11-06 22:36: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
GitHub
parent
e669fbe557
commit
5163411f9b
13 changed files with 554 additions and 18 deletions
|
|
@ -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<constructor_decl> constrs;
|
||||
for (unsigned i = 0; i < num_constructors; ++i) {
|
||||
constructor* cn = reinterpret_cast<constructor*>(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<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
|
||||
|
||||
for (unsigned i = 0; i < num_constructors; ++i) {
|
||||
constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
|
||||
cn->m_constructor = cnstrs[i];
|
||||
}
|
||||
RETURN_Z3_mk_polymorphic_datatype(of_sort(s));
|
||||
Z3_CATCH_RETURN(nullptr);
|
||||
}
|
||||
|
||||
typedef ptr_vector<constructor> 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<parameter> 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<datatype_decl> datas;
|
||||
for (unsigned i = 0; i < num_sorts; ++i) {
|
||||
constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
|
||||
datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
|
||||
datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, 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);
|
||||
|
|
|
|||
|
|
@ -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<Z3_sort> _params(params);
|
||||
Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr());
|
||||
check_error();
|
||||
return sort(*this, s);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -474,6 +474,36 @@ namespace Microsoft.Z3
|
|||
return new DatatypeSort(this, symbol, constructors);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create a forward reference to a datatype sort.
|
||||
/// This is useful for creating recursive datatypes or parametric datatypes.
|
||||
/// </summary>
|
||||
/// <param name="name">name of the datatype sort</param>
|
||||
/// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
|
||||
public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
|
||||
{
|
||||
Debug.Assert(name != null);
|
||||
CheckContextMatch(name);
|
||||
if (parameters != null)
|
||||
CheckContextMatch<Sort>(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));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create a forward reference to a datatype sort.
|
||||
/// This is useful for creating recursive datatypes or parametric datatypes.
|
||||
/// </summary>
|
||||
/// <param name="name">name of the datatype sort</param>
|
||||
/// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
|
||||
public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
|
||||
{
|
||||
using var symbol = MkSymbol(name);
|
||||
return MkDatatypeSortRef(symbol, parameters);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Create mutually recursive datatypes.
|
||||
/// </summary>
|
||||
|
|
|
|||
|
|
@ -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 <R> DatatypeSort<R> 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 <R> DatatypeSort<R> 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 <R> DatatypeSort<R> 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 <R> DatatypeSort<R> mkDatatypeSortRef(String name)
|
||||
{
|
||||
return mkDatatypeSortRef(name, null);
|
||||
}
|
||||
|
||||
/**
|
||||
* Create mutually recursive datatypes.
|
||||
* @param names names of datatype sorts
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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