mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fixes #6439 #6436

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-04 09:35:58 -07:00
parent 626380b3c7
commit 84af521514
5 changed files with 17 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.h
View file

@ -1387,6 +1387,7 @@ inline bool is_app_of(expr const * n, family_id fid, decl_kind k) { return n->ge
inline bool is_sort_of(sort const * s, family_id fid, decl_kind k) { return s->is_sort_of(fid, k); }
inline bool is_uninterp_const(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id; }
inline bool is_uninterp(expr const * n) { return n->get_kind() == AST_APP && to_app(n)->get_family_id() == null_family_id; }
inline bool is_uninterp(func_decl const * n) { return n->get_family_id() == null_family_id; }
inline bool is_decl_of(func_decl const * d, family_id fid, decl_kind k) { return d->get_family_id() == fid && d->get_decl_kind() == k; }
inline bool is_ground(expr const * n) { return is_app(n) && to_app(n)->is_ground(); }
inline bool is_non_ground(expr const * n) { return ( ! is_ground(n)); }