mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

redo purification

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-29 11:06:31 -07:00
parent da0e140e1c
commit 2e684d58d2
5 changed files with 68 additions and 88 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/qe/mbp/mbp_plugin.cpp
View file

@ -325,57 +325,4 @@ namespace mbp {
}
}
void project_plugin::purify(euf_inverter& inv, model& mdl, app_ref_vector const& vars, expr_ref_vector& lits) {
TRACE("mbp", tout << lits << "\n" << mdl << "\n";);
model_evaluator eval(mdl);
extract_literals(mdl, vars, lits);
if (!m.inc())
return;
eval.set_expand_array_equalities(true);
m_non_ground.reset();
m_to_visit.reset();
m_visited.reset();
m_cache.reset();
m_pure_eqs.reset();
for (expr* v : vars)
m_non_ground.mark(v);
for (unsigned i = 0; m.inc() && i < lits.size(); ++i)
lits[i] = purify(inv, eval, lits.get(i), lits);
lits.append(m_pure_eqs);
TRACE("mbp", tout << lits << "\n";);
}
expr* project_plugin::purify(euf_inverter& inv, model_evaluator& eval, expr* e, expr_ref_vector& lits) {
mark_non_ground(e);
m_to_visit.push_back(e);
while (!m_to_visit.empty()) {
expr* t = m_to_visit.back();
if (m_cache.get(t->get_id(), nullptr))
m_to_visit.pop_back();
else if (!is_app(t) || !m_non_ground.is_marked(t)) {
m_cache.setx(t->get_id(), t);
m_to_visit.pop_back();
}
else
purify_app(inv, eval, to_app(t), lits);
}
return m_cache.get(e->get_id());
}
void project_plugin::purify_app(euf_inverter& inv, model_evaluator& eval, app* t, expr_ref_vector& lits) {
if (is_uninterp(t) && t->get_num_args() > 0) {
expr_ref t_value = eval(t);
expr* s = inv.invert_app(t, t_value);
m_cache.setx(t->get_id(), s);
if (s != t)
m_pure_eqs.push_back(m.mk_eq(t, s));
unsigned i = 0;
for (expr* arg : *t)
inv.invert_arg(t, i++, eval(arg), lits);
m_to_visit.pop_back();
}
else
visit_app(t);
}
}

21
src/qe/mbp/mbp_plugin.h
View file

@ -35,17 +35,6 @@ namespace mbp {
def(const expr_ref& v, expr_ref& t): var(v), term(t) {}
};
/***
* An EUF inverter provides two services:
* 1. It inverts an uninterpreted function application f(s1,s2) with 'value' to a ground term evaluating to the same
* 2. It adds constraints for arguments to s_i with 'value' to be within the bounds of the model value.
*/
class euf_inverter {
public:
virtual expr* invert_app(app* t, expr* value) = 0;
virtual void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) = 0;
};
class project_plugin {
ast_manager& m;
expr_mark m_visited;
@ -67,9 +56,6 @@ namespace mbp {
void mark_non_ground(expr* e);
expr* purify(euf_inverter& inv, model_evaluator& eval, expr* e, expr_ref_vector& lits);
void purify_app(euf_inverter& inv, model_evaluator& eval, app* t, expr_ref_vector& lits);
public:
project_plugin(ast_manager& m) :m(m), m_cache(m), m_args(m), m_pure_eqs(m) {}
virtual ~project_plugin() {}
@ -103,12 +89,6 @@ namespace mbp {
*/
void extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls);
/*
* Purify literals into linear inequalities or constraints without arithmetic variables.
*/
void purify(euf_inverter& inv, model& model, app_ref_vector const& vars, expr_ref_vector& fmls);
static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
static void erase(expr_ref_vector& lits, unsigned& i);
@ -125,6 +105,7 @@ namespace mbp {
}
bool is_non_ground(expr* t) const { return m_non_ground.is_marked(t); }
};
}

63
src/sat/smt/q_mbi.cpp
View file

@ -36,8 +36,7 @@ namespace q {
m_qs(s),
m(s.get_manager()),
m_model_fixer(ctx, m_qs),
m_fresh_trail(m)
{
m_fresh_trail(m) {
auto* ap = alloc(mbp::arith_project_plugin, m);
ap->set_check_purified(false);
ap->set_apply_projection(true);
@ -120,9 +119,9 @@ namespace q {
if (is_exists(q))
qlit.neg();
unsigned i = 0;
{
if (!qb->var_args.empty()) {
::solver::scoped_push _sp(*m_solver);
restrict_domains(*mdl0, *qb);
add_domain_eqs(*mdl0, *qb);
for (; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) {
m_solver->get_model(mdl1);
proj = solver_project(*mdl1, *qb);
@ -133,7 +132,7 @@ namespace q {
}
}
if (i == 0) {
qb->domain_eqs.reset();
add_domain_bounds(*mdl0, *qb);
proj = solver_project(*mdl0, *qb);
if (!proj)
return l_undef;
@ -212,14 +211,17 @@ namespace q {
expr_ref_vector fmls(qb.vbody);
app_ref_vector vars(qb.vars);
fmls.append(qb.domain_eqs);
eliminate_nested_vars(fmls, qb);
mbp::project_plugin proj(m);
proj.purify(m_model_fixer, *m_model, vars, fmls);
proj.extract_literals(*m_model, vars, fmls);
for (unsigned i = 0; i < vars.size(); ++i) {
app* v = vars.get(i);
auto* p = get_plugin(v);
if (p)
(*p)(*m_model, vars, fmls);
}
#if 0
// should be redundant
expr_safe_replace esubst(m);
for (app* v : qb.vars) {
expr_ref val = assign_value(*m_model, v);
@ -228,6 +230,7 @@ namespace q {
esubst.insert(v, val);
}
esubst(fmls);
#endif
return mk_and(fmls);
}
@ -238,7 +241,7 @@ namespace q {
* Add also disjunctions to the quantifier "domain_eqs", to track the constraints
* added to the solver.
*/
void mbqi::restrict_domains(model& mdl, q_body& qb) {
void mbqi::add_domain_eqs(model& mdl, q_body& qb) {
qb.domain_eqs.reset();
var_subst subst(m);
for (auto p : qb.var_args) {
@ -256,6 +259,43 @@ namespace q {
}
}
/*
* Add bounds to sub-terms under uninterpreted functions for projection.
*/
void mbqi::add_domain_bounds(model& mdl, q_body& qb) {
qb.domain_eqs.reset();
for (app* v : qb.vars)
m_model->register_decl(v->get_decl(), mdl(v));
if (qb.var_args.empty())
return;
var_subst subst(m);
for (auto p : qb.var_args) {
expr_ref _term = subst(p.first, qb.vars);
app_ref term(to_app(_term), m);
expr_ref value = (*m_model)(term->get_arg(p.second));
m_model_fixer.invert_arg(term, p.second, value, qb.domain_eqs);
}
}
/*
* Remove occurrences of free functions that contain variables.
*/
void mbqi::eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb) {
if (qb.var_args.empty())
return;
expr_safe_replace rep(m);
var_subst subst(m);
for (auto p : qb.var_args) {
expr_ref _term = subst(p.first, qb.vars);
app_ref term(to_app(_term), m);
expr_ref value = (*m_model)(term);
expr* s = m_model_fixer.invert_app(term, value);
rep.insert(term, s);
}
rep(fmls);
}
/*
* Add domain restrictions for every non-ground arguments to uninterpreted functions.
*/
@ -265,10 +305,11 @@ namespace q {
if (is_ground(s))
continue;
if (is_uninterp(s) && to_app(s)->get_num_args() > 0) {
app* a = to_app(s);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (is_ground(a->get_arg(i)))
qb.var_args.push_back(std::make_pair(a, i));
unsigned i = 0;
for (expr* arg : *to_app(s)) {
if (!is_ground(arg) && !is_uninterp(arg))
qb.var_args.push_back(std::make_pair(to_app(s), i));
++i;
}
}
}

4
src/sat/smt/q_mbi.h
View file

@ -61,7 +61,9 @@ namespace q {
expr_ref basic_project(model& mdl, quantifier* q, app_ref_vector& vars);
expr_ref solver_project(model& mdl, q_body& qb);
expr_ref assign_value(model& mdl, app* v);
void restrict_domains(model& mdl, q_body& qb);
void add_domain_eqs(model& mdl, q_body& qb);
void add_domain_bounds(model& mdl, q_body& qb);
void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb);
void extract_var_args(expr* t, q_body& qb);
void init_model();
void init_solver();

15
src/sat/smt/q_model_fixer.h
View file

@ -70,7 +70,7 @@ namespace q {
struct eq { bool operator()(indexed_decl const& a, indexed_decl const& b) const { return a.idx == b.idx && a.f == b.f; } };
};
class model_fixer : public quantifier2macro_infos, public mbp::euf_inverter {
class model_fixer : public quantifier2macro_infos {
euf::solver& ctx;
solver& m_qs;
ast_manager& m;
@ -113,8 +113,17 @@ namespace q {
*/
expr_ref restrict_arg(app* t, unsigned i);
expr* invert_app(app* t, expr* value) override;
void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) override;
/*
* Create inequality constraints for the i'th argument of t based on the current model.
*/
void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits);
/*
* Replace term that contains uninterpreted function over free variables with a ground term.
*/
expr* invert_app(app* t, expr* value);
};
}