diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index 6c8824a6a..e470b8d9d 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -249,6 +249,11 @@ namespace recfun { return m_plugin->get_def(s); } + case_def& get_case_def(expr* e) { + SASSERT(is_case_pred(e)); + return get_case_def(to_app(e)->get_name()); + } + case_def& get_case_def(symbol const & s) { SASSERT(m_plugin->has_case_def(s)); return m_plugin->get_case_def(s); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index 6f62cccc0..e0b43c7ed 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -32,7 +32,7 @@ namespace smt { m(m), m_plugin(*reinterpret_cast(m.get_plugin(get_family_id()))), m_util(m_plugin.u()), - m_guards(m), + m_guard_preds(m), m_max_depth(0), m_q_case_expand(), m_q_body_expand() @@ -41,10 +41,6 @@ namespace smt { theory_recfun::~theory_recfun() { reset_queues(); - for (expr* g : m_guards) { - m.dec_ref(g); - } - m_guards.reset(); } char const * theory_recfun::get_name() const { return "recfun"; } @@ -112,12 +108,21 @@ namespace smt { void theory_recfun::push_scope_eh() { TRACEFN("push_scope"); theory::push_scope_eh(); + m_guard_preds_lim.push_back(m_guard_preds.size()); } void theory_recfun::pop_scope_eh(unsigned num_scopes) { TRACEFN("pop_scope " << num_scopes); theory::pop_scope_eh(num_scopes); reset_queues(); + + // restore guards + unsigned new_lim = m_guard_preds_lim.size()-num_scopes; + for (unsigned i = new_lim; i < m_guard_preds.size(); ++i) { + m_guards[m_guard_preds.get(i)->get_decl()].pop_back(); + } + m_guard_preds.resize(m_guard_preds_lim[new_lim]); + m_guard_preds_lim.shrink(new_lim); } void theory_recfun::restart_eh() { @@ -159,22 +164,20 @@ namespace smt { m_q_body_expand.clear(); } - void theory_recfun::max_depth_conflict() { - TRACEFN("max-depth conflict"); + void theory_recfun::max_depth_limit(ptr_vector const& guards) { + TRACEFN("max-depth limit"); literal_vector c; - // make clause `depth_limit => V_{g : guards} ~ g` - { - // first literal must be the depth limit one - app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); - c.push_back(~mk_literal(dlimit)); - SASSERT(ctx().get_assignment(c.back()) == l_true); - } - for (expr * g : m_guards) { - c.push_back(~ mk_literal(g)); + // make clause `depth_limit => V_{g : guards of non-recursive cases} g` + + // first literal must be the depth limit one + app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); + c.push_back(~mk_literal(dlimit)); + SASSERT(ctx().get_assignment(c.back()) == l_false); + + for (expr * g : guards) { + c.push_back(mk_literal(g)); } TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c)); - SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx().get_assignment(l) == l_false; })); // conflict - m_q_clauses.push_back(std::move(c)); } @@ -185,22 +188,11 @@ namespace smt { void theory_recfun::assign_eh(bool_var v, bool is_true) { expr* e = ctx().bool_var2expr(v); if (is_true && u().is_case_pred(e)) { - app* a = to_app(e); TRACEFN("assign_case_pred_true " << mk_pp(e, m)); - // add to set of local assumptions, for depth-limit purpose - SASSERT(!m_guards.contains(a)); - m_guards.push_back(a); - ctx().push_trail(push_back_vector(m_guards)); - - if (m_guards.size() <= get_max_depth()) { - // body-expand - body_expansion b_e(u(), a); - push_body_expand(std::move(b_e)); - } - else { - // too many body-expansions: depth-limit conflict - max_depth_conflict(); - } + app* a = to_app(e); + // body-expand + body_expansion b_e(u(), a); + push_body_expand(std::move(b_e)); } } @@ -297,6 +289,15 @@ namespace smt { if (c.is_immediate()) { body_expansion be(c, e.m_args); assert_body_axiom(be); + + // add to set of local assumptions, for depth-limit purpose + func_decl* d = pred_applied->get_decl(); + m_guard_preds.push_back(pred_applied); + auto& vec = m_guards.insert_if_not_there2(d, ptr_vector())->get_data().m_value; + vec.push_back(pred_applied); + if (vec.size() == get_max_depth()) { + max_depth_limit(vec); + } } } } diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h index a2ec27314..ab09e4f45 100644 --- a/src/smt/theory_recfun.h +++ b/src/smt/theory_recfun.h @@ -70,8 +70,7 @@ namespace smt { ptr_vector m_args; body_expansion(recfun_util& u, app * n) : m_cdef(0), m_args() { - SASSERT(u.is_case_pred(n)); - m_cdef = &u.get_case_def(n->get_name()); + m_cdef = &u.get_case_def(n); m_args.append(n->get_num_args(), n->get_args()); } body_expansion(recfun_case_def const & d, ptr_vector & args) : m_cdef(&d), m_args(args) {} @@ -87,16 +86,18 @@ namespace smt { friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &); - ast_manager& m; - recfun_decl_plugin& m_plugin; - recfun_util& m_util; - stats m_stats; - app_ref_vector m_guards; // true case-preds - unsigned m_max_depth; // for fairness and termination + ast_manager& m; + recfun_decl_plugin& m_plugin; + recfun_util& m_util; + stats m_stats; + obj_map > m_guards; + app_ref_vector m_guard_preds; + unsigned_vector m_guard_preds_lim; + unsigned m_max_depth; // for fairness and termination - vector m_q_case_expand; - vector m_q_body_expand; - vector m_q_clauses; + vector m_q_case_expand; + vector m_q_body_expand; + vector m_q_clauses; recfun_util & u() const { return m_util; } bool is_defined(app * f) const { return u().is_defined(f); } @@ -112,7 +113,7 @@ namespace smt { void assert_case_axioms(case_expansion & e); void assert_body_axiom(body_expansion & e); literal mk_literal(expr* e); - void max_depth_conflict(); + void max_depth_limit(ptr_vector const& guards); literal mk_eq_lit(expr* l, expr* r); bool is_standard_order(recfun::vars const& vars) const { return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0; } protected: