mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Add 2 new API functions to get depth & groundness of exprs (#7479)

Browse source 
* Update api_ast.cpp

* Update z3_api.h
This commit is contained in:
Nuno Lopes 2024-12-30 16:49:43 +00:00 committed by GitHub
parent f99e1ee581
commit 322dcec531
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/api/api_ast.cpp
View file

@ -425,6 +425,20 @@ extern "C" {
RETURN_Z3(of_app(reinterpret_cast<app*>(a))); RETURN_Z3(of_app(reinterpret_cast<app*>(a)));
} }
bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a) {
LOG_Z3_is_ground(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, 0);
return is_ground(to_expr(a));
}
unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a) {
LOG_Z3_get_depth(c, a);
RESET_ERROR_CODE();
CHECK_IS_EXPR(a, 0);
return get_depth(to_expr(a));
}
Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) { Z3_func_decl Z3_API Z3_to_func_decl(Z3_context c, Z3_ast a) {
LOG_Z3_to_func_decl(c, a); LOG_Z3_to_func_decl(c, a);
RESET_ERROR_CODE(); RESET_ERROR_CODE();

10
src/api/z3_api.h
View file

@ -4992,6 +4992,16 @@ extern "C" {
*/ */
bool Z3_API Z3_is_app(Z3_context c, Z3_ast a); bool Z3_API Z3_is_app(Z3_context c, Z3_ast a);
/**
def_API('Z3_is_ground', BOOL, (_in(CONTEXT), _in(AST)))
*/
bool Z3_API Z3_is_ground(Z3_context c, Z3_ast a);
/**
def_API('Z3_get_depth', UINT, (_in(CONTEXT), _in(AST)))
*/
unsigned Z3_API Z3_get_depth(Z3_context c, Z3_ast a);
/** /**
def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST))) def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST)))
*/ */