From 5073959ae02b1ff062ffd43a4d62af219db7ce34 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Dec 2022 07:52:17 -0800 Subject: [PATCH] add macro attribute --- src/ast/recfun_decl_plugin.cpp | 1 + src/ast/recfun_decl_plugin.h | 2 ++ 2 files changed, 3 insertions(+) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 558488592..86c3fcf3b 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -408,6 +408,7 @@ namespace recfun { void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) { SASSERT(n_vars == d->get_arity()); + d->m_is_macro = is_macro; is_imm_pred is_i(*u); d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs); } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index c369e2827..bb75a854c 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -117,6 +117,7 @@ namespace recfun { func_decl_ref m_decl; //!< generic declaration expr_ref m_rhs; //!< definition 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); @@ -138,6 +139,7 @@ namespace recfun { bool is_fun_macro() const { return m_cases.size() == 1; } bool is_fun_defined() const { return !is_fun_macro(); } + bool is_macro() const { return m_is_macro; } def* copy(util& dst, ast_translation& tr);