mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-04 08:07:56 +00:00
Code Activity

Update Z3_mk_datatype_sort API to accept array of parameters

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-11 17:41:49 +00:00
parent 0ffc97c0df
commit e0055e5c9f
3 changed files with 31 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_datatype.cpp
View file

@ -387,14 +387,18 @@ extern "C" {
Z3_CATCH; 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; Z3_TRY;
LOG_Z3_mk_datatype_sort(c, name); LOG_Z3_mk_datatype_sort(c, name, num_params, params);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
datatype_util adt_util(m); datatype_util adt_util(m);
parameter p(to_symbol(name)); vector<parameter> ps;
sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p); 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); mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s)); RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);

17
src/api/c++/z3++.h
View file

@ -343,6 +343,14 @@ namespace z3 {
*/ */
sort datatype_sort(symbol const& name); 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. \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) { 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(); check_error();
return sort(*this, s); return sort(*this, s);
} }

9
src/api/z3_api.h
View file

@ -2136,9 +2136,14 @@ extern "C" {
Forward references can replace the use sort references, that are unsigned integers Forward references can replace the use sort references, that are unsigned integers
in the \c Z3_mk_constructor call 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. \brief Create list of constructors.