mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

have theory_recfun use recursive function discriminator to control when it is enabled

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-06 12:09:45 -08:00
parent f004478565
commit cbc5b1f4f6
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/recfun_decl_plugin.cpp
View file

@ -442,17 +442,18 @@ namespace recfun {
return promise_def(&u(), d); return promise_def(&u(), d);
} }
void plugin::inherit(decl_plugin* other, ast_translation& tr) { void plugin::inherit(decl_plugin* _other, ast_translation& tr) {
for (auto [k, v] : static_cast<plugin*>(other)->m_defs) { plugin* other = static_cast<plugin*>(_other);
for (auto [k, v] : other->m_defs) {
func_decl_ref f(tr(k), tr.to()); func_decl_ref f(tr(k), tr.to());
if (m_defs.contains(f)) if (m_defs.contains(f))
continue; continue;
def* d = v->copy(u(), tr); def* d = v->copy(u(), tr);
m_defs.insert(f, d); m_defs.insert(f, d);
for (case_def & c : d->get_cases()) for (case_def & c : d->get_cases())
m_case_defs.insert(c.get_decl(), &c); m_case_defs.insert(c.get_decl(), &c);
} }
m_has_rec_defs = other->m_has_rec_defs;
} }
promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) { promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {

5
src/smt/theory_recfun.cpp
View file

@ -102,9 +102,8 @@ namespace smt {
void theory_recfun::relevant_eh(app * n) { void theory_recfun::relevant_eh(app * n) {
SASSERT(ctx.relevancy()); SASSERT(ctx.relevancy());
// TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); // TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m));
if (u().is_defined(n) && u().has_defs()) { if (u().is_defined(n) && u().has_defs())
push_case_expand(n); push_case_expand(n);
}
} }
void theory_recfun::push_scope_eh() { void theory_recfun::push_scope_eh() {
@ -418,7 +417,7 @@ namespace smt {
} }
void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) { void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
if (u().has_defs() || !m_disabled_guards.empty()) { if (u().has_rec_defs() || !m_disabled_guards.empty()) {
app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds); app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
TRACEFN("add_theory_assumption " << dlimit); TRACEFN("add_theory_assumption " << dlimit);
assumptions.push_back(dlimit); assumptions.push_back(dlimit);