mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

expose recursive functions with own op-code over API

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-13 11:22:43 +02:00
parent c0b455e010
commit c9fa00aec1
2 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_ast.cpp
View file

@ -1329,6 +1329,9 @@ extern "C" {
} }
} }
if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
return Z3_OP_RECURSIVE;
return Z3_OP_UNINTERPRETED; return Z3_OP_UNINTERPRETED;
Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED); Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
} }

3
src/api/z3_api.h
View file

@ -996,6 +996,8 @@ typedef enum
information is exposed. Tools may use the string representation of the information is exposed. Tools may use the string representation of the
function declaration to obtain more information. function declaration to obtain more information.
- Z3_OP_RECURSIVE: function declared as recursive
- Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols. - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols.
*/ */
typedef enum { typedef enum {
@ -1320,6 +1322,7 @@ typedef enum {
Z3_OP_FPA_BV2RM, Z3_OP_FPA_BV2RM,
Z3_OP_INTERNAL, Z3_OP_INTERNAL,
Z3_OP_RECURSIVE,
Z3_OP_UNINTERPRETED Z3_OP_UNINTERPRETED
} Z3_decl_kind; } Z3_decl_kind;