mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
iterative deepening per recursive function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
35eb6eccd1
commit
c0556b2f64
|
@ -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);
|
||||
|
|
|
@ -32,7 +32,7 @@ namespace smt {
|
|||
m(m),
|
||||
m_plugin(*reinterpret_cast<recfun_decl_plugin*>(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<expr> 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<context, app_ref_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<expr>())->get_data().m_value;
|
||||
vec.push_back(pred_applied);
|
||||
if (vec.size() == get_max_depth()) {
|
||||
max_depth_limit(vec);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -70,8 +70,7 @@ namespace smt {
|
|||
ptr_vector<expr> 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<expr> & 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<func_decl, ptr_vector<expr> > m_guards;
|
||||
app_ref_vector m_guard_preds;
|
||||
unsigned_vector m_guard_preds_lim;
|
||||
unsigned m_max_depth; // for fairness and termination
|
||||
|
||||
vector<case_expansion> m_q_case_expand;
|
||||
vector<body_expansion> m_q_body_expand;
|
||||
vector<literal_vector> m_q_clauses;
|
||||
vector<case_expansion> m_q_case_expand;
|
||||
vector<body_expansion> m_q_body_expand;
|
||||
vector<literal_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<expr> 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:
|
||||
|
|
Loading…
Reference in a new issue