mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Add Z3_is_recursive_datatype_sort to the API

Browse source 
It does not seem to be possible to test if a datatype sort is recursive.
This commit is contained in:
Josh Berdine 2025-04-08 16:50:59 +01:00
parent 14e2aadad0
commit 386c331eb9
2 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_datatype.cpp
View file

@ -443,6 +443,16 @@ extern "C" {
Z3_CATCH;
}
bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort t) {
Z3_TRY;
LOG_Z3_is_recursive_datatype_sort(c, t);
RESET_ERROR_CODE();
sort * s = to_sort(t);
datatype_util& dt_util = mk_c(c)->dtutil();
return dt_util.is_datatype(s) && dt_util.is_recursive(s);
Z3_CATCH_RETURN(false);
}
unsigned Z3_API Z3_get_datatype_sort_num_constructors(Z3_context c, Z3_sort t) {
Z3_TRY;
LOG_Z3_get_datatype_sort_num_constructors(c, t);

7
src/api/z3_api.h
View file

@ -4588,6 +4588,13 @@ extern "C" {
*/
Z3_func_decl Z3_API Z3_get_tuple_sort_field_decl(Z3_context c, Z3_sort t, unsigned i);
/**
\brief Check if \c s is a recursive datatype sort.
def_API('Z3_is_recursive_datatype_sort', BOOL, (_in(CONTEXT), _in(SORT)))
*/
bool Z3_API Z3_is_recursive_datatype_sort(Z3_context c, Z3_sort s);
/**
\brief Return number of constructors for datatype.