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

make default argument to ensure_def and mk_def explicit

Browse source 
- insert also macro definitions into models
This commit is contained in:
Nikolaj Bjorner 2023-05-02 12:18:31 -07:00
parent c64d61bd0a
commit f17691715b
4 changed files with 28 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_ast.cpp
View file

@ -120,10 +120,8 @@ extern "C" {
RESET_ERROR_CODE();
//
recfun::promise_def def =
mk_c(c)->recfun().get_plugin().mk_def(to_symbol(s),
domain_size,
to_sorts(domain),
to_sort(range));
mk_c(c)->recfun().get_plugin().mk_def(
to_symbol(s), domain_size, to_sorts(domain), to_sort(range), false);
func_decl* d = def.get_def()->get_decl();
mk_c(c)->save_ast_trail(d);
RETURN_Z3(of_func_decl(d));

4
src/ast/recfun_decl_plugin.cpp
View file

@ -492,7 +492,7 @@ namespace recfun {
def* plugin::mk_def(replace& subst, bool is_macro,
symbol const& name, unsigned n, sort ** params, sort * range,
unsigned n_vars, var ** vars, expr * rhs) {
promise_def d = mk_def(name, n, params, range);
promise_def d = mk_def(name, n, params, range, false);
SASSERT(! m_defs.contains(d.get_def()->get_decl()));
set_definition(subst, d, is_macro, n_vars, vars, rhs);
return d.get_def();
@ -581,7 +581,7 @@ namespace recfun {
}
symbol fresh_name("fold-rec-" + std::to_string(m().mk_fresh_id()));
auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort());
auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort(), false);
func_decl* f = pd.get_def()->get_decl();
expr_ref new_body(m().mk_app(f, n, args.data()), m());
set_definition(subst, pd, false, n, vars, max_expr);

5
src/ast/recfun_decl_plugin.h
View file

@ -192,9 +192,9 @@ namespace recfun {
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false);
promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated);
promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false);
promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated);
void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs);
@ -248,6 +248,7 @@ namespace recfun {
bool is_defined(expr * e) const { return is_app_of(e, m_fid, OP_FUN_DEFINED); }
bool is_defined(func_decl* f) const { return is_decl_of(f, m_fid, OP_FUN_DEFINED); }
bool is_generated(func_decl* f) const { return is_defined(f) && f->get_parameter(0).get_int() == 1; }
bool is_macro(func_decl* f) { return is_defined(f) && get_def(f).is_macro(); }
bool is_num_rounds(expr * e) const { return is_app_of(e, m_fid, OP_NUM_ROUNDS); }
bool owns_app(app * e) const { return e->get_family_id() == m_fid; }

36
src/cmd_context/cmd_context.cpp
View file

@ -361,7 +361,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
vars.push_back(m().mk_var(i, domain[i]));
rvars.push_back(m().mk_var(i, domain[arity - i - 1]));
}
recfun::promise_def d = p.ensure_def(s, arity, domain, t->get_sort());
recfun::promise_def d = p.ensure_def(s, arity, domain, t->get_sort(), false);
// recursive functions have opposite calling convention from macros!
var_subst sub(m(), true);
@ -984,7 +984,7 @@ recfun::decl::plugin& cmd_context::get_recfun_plugin() {
recfun::promise_def cmd_context::decl_rec_fun(const symbol &name, unsigned int arity, sort *const *domain, sort *range) {
SASSERT(logic_has_recfun());
return get_recfun_plugin().mk_def(name, arity, domain, range);
return get_recfun_plugin().mk_def(name, arity, domain, range, false);
}
void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector<symbol> const& ids, expr* rhs) {
@ -1982,25 +1982,31 @@ void cmd_context::complete_model(model_ref& md) const {
}
}
for (auto kd : m_func_decls) {
symbol const & k = kd.m_key;
func_decls & v = kd.m_value;
for (auto& [k, v] : m_func_decls) {
IF_VERBOSE(12, verbose_stream() << "(model.completion " << k << ")\n"; );
for (unsigned i = 0; i < v.get_num_entries(); i++) {
func_decl * f = v.get_entry(i);
if (!md->has_interpretation(f)) {
sort * range = f->get_range();
expr * some_val = m().get_some_value(range);
if (f->get_arity() > 0) {
func_interp * fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(some_val);
md->register_decl(f, fi);
}
else
md->register_decl(f, some_val);
if (md->has_interpretation(f))
continue;
macro_decls decls;
expr* body = nullptr;
if (m_macros.find(k, decls))
body = decls.find(f->get_arity(), f->get_domain());
sort * range = f->get_range();
if (!body)
body = m().get_some_value(range);
if (f->get_arity() > 0) {
func_interp * fi = alloc(func_interp, m(), f->get_arity());
fi->set_else(body);
md->register_decl(f, fi);
}
else
md->register_decl(f, body);
}
}
verbose_stream() << *md << "\n";
}
/**