From 2e684d58d229a4f3eb4bc8a9f3b3c1b9d9bcfe68 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Oct 2020 11:06:31 -0700 Subject: [PATCH] redo purification Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_plugin.cpp | 53 ------------------------------- src/qe/mbp/mbp_plugin.h | 21 +------------ src/sat/smt/q_mbi.cpp | 63 ++++++++++++++++++++++++++++++------- src/sat/smt/q_mbi.h | 4 ++- src/sat/smt/q_model_fixer.h | 15 +++++++-- 5 files changed, 68 insertions(+), 88 deletions(-) diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index 344e4d8f0..2731fc5e2 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -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); - } - } diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 2b74f2740..121c7672e 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -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); } + }; } diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index defc287d3..bf6db5dd9 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -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; } } } diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index 5c6067d51..33bce61d9 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -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(); diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index be541bb4e..a843d3825 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -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); + + }; }