mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

add macro attribute

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-02 07:52:17 -08:00
parent 54a8d65617
commit 5073959ae0
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/recfun_decl_plugin.cpp
View file

@ -408,6 +408,7 @@ namespace recfun {
void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
SASSERT(n_vars == d->get_arity()); SASSERT(n_vars == d->get_arity());
d->m_is_macro = is_macro;
is_imm_pred is_i(*u); is_imm_pred is_i(*u);
d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs); d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs);
} }

2
src/ast/recfun_decl_plugin.h
View file

@ -117,6 +117,7 @@ namespace recfun {
func_decl_ref m_decl; //!< generic declaration func_decl_ref m_decl; //!< generic declaration
expr_ref m_rhs; //!< definition expr_ref m_rhs; //!< definition
family_id m_fid; family_id m_fid;
bool m_is_macro;
def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range, bool is_generated); def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range, bool is_generated);
@ -138,6 +139,7 @@ namespace recfun {
bool is_fun_macro() const { return m_cases.size() == 1; } bool is_fun_macro() const { return m_cases.size() == 1; }
bool is_fun_defined() const { return !is_fun_macro(); } bool is_fun_defined() const { return !is_fun_macro(); }
bool is_macro() const { return m_is_macro; }
def* copy(util& dst, ast_translation& tr); def* copy(util& dst, ast_translation& tr);