From 076cfa5813d5653bb9d95055fd78aac624210f0b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Dec 2018 21:04:35 +0800 Subject: [PATCH] working on revising project0 to project Signed-off-by: Nikolaj Bjorner --- src/qe/qe_mbi.cpp | 252 ++++++++++++++++++++++++++------------- src/qe/qe_mbi.h | 3 + src/qe/qe_term_graph.cpp | 2 + 3 files changed, 177 insertions(+), 80 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index b7f0d0d49..f66240226 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -30,6 +30,7 @@ Notes: #include "ast/ast_util.h" #include "ast/for_each_expr.h" +#include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/arith_decl_plugin.h" #include "model/model_evaluator.h" @@ -329,86 +330,7 @@ namespace qe { if (!get_literals(mdl, lits)) { return mbi_undef; } - TRACE("qe", tout << lits << "\n";); - - // 1. Extract projected variables, add inequalities between - // projected variables and non-projected terms according to model. - // 2. Extract disequalities implied by congruence closure. - // 3. project arithmetic variables from pure literals. - // 4. Add projected definitions as equalities to EUF. - // 5. project remaining literals with respect to EUF. - - app_ref_vector avars = get_arith_vars(mdl, lits); - TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); - - // 2. - term_graph tg1(m); - func_decl_ref_vector no_shared(m); - tg1.set_vars(no_shared, false); - tg1.add_lits(lits); - arith_util a(m); - expr_ref_vector foreign = tg1.shared_occurrences(a.get_family_id()); - obj_hashtable _foreign; - for (expr* e : foreign) _foreign.insert(e); - vector partition = tg1.get_partition(*mdl); - expr_ref_vector diseq = tg1.get_ackerman_disequalities(); - lits.append(diseq); - TRACE("qe", tout << "diseq: " << diseq << "\n"; - tout << "foreign: " << foreign << "\n"; - for (auto const& v : partition) { - tout << "partition: {"; - bool first = true; - for (expr* e : v) { - if (first) first = false; else tout << ", "; - tout << expr_ref(e, m); - } - tout << "}\n"; - } - ); - vector refined_partition; - for (auto & p : partition) { - unsigned j = 0; - for (expr* e : p) { - if (_foreign.contains(e) || - (is_app(e) && m_shared.contains(to_app(e)->get_decl()))) { - p[j++] = e; - } - } - p.shrink(j); - if (!p.empty()) refined_partition.push_back(p); - } - TRACE("qe", - for (auto const& v : refined_partition) { - tout << "partition: {"; - bool first = true; - for (expr* e : v) { - if (first) first = false; else tout << ", "; - tout << expr_ref(e, m); - } - tout << "}\n"; - }); - - - - arith_project_plugin ap(m); - ap.set_check_purified(false); - - // 3. - auto defs = ap.project(*mdl.get(), avars, lits); - - // 4. - for (auto const& def : defs) { - lits.push_back(m.mk_eq(def.var, def.term)); - } - TRACE("qe", tout << "# arith defs " << defs.size() << " avars: " << avars << " " << lits << "\n";); - - // 5. - term_graph tg2(m); - tg2.set_vars(m_shared, false); - tg2.add_lits(lits); - lits.reset(); - lits.append(tg2.project()); - TRACE("qe", tout << "project: " << lits << "\n";); + project0(mdl, lits); return mbi_sat; } default: @@ -421,6 +343,176 @@ namespace qe { } } + /** + 1. extract arithmetical variables, purify. + 2. project private variables from lits + 3. Order arithmetical variables. + 4. Perform arithmetical projection. + 5. Substitute solution into lits + */ + void euf_arith_mbi_plugin::project(model_ref& mdl, expr_ref_vector& lits) { + TRACE("qe", tout << lits << "\n" << *mdl << "\n";); + + // 1. arithmetical variables + app_ref_vector avars = get_arith_vars(mdl, lits); + TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); + + + // 2. project private variables from lits + { + term_graph tg(m); + func_decl_ref_vector shared(m_shared); + for (app* a : avars) shared.push_back(a->get_decl()); + tg.set_vars(shared, false); + tg.add_lits(lits); + lits.reset(); + lits.append(tg.project(*mdl.get())); + TRACE("qe", tout << "project: " << lits << "\n";); + } + + // 3. Order arithmetical variables + order_avars(mdl, lits, avars); + + // 4. Arithmetical projection + arith_project_plugin ap(m); + ap.set_check_purified(false); + auto defs = ap.project(*mdl.get(), avars, lits); + + // 5. Substitute solution + for (auto const& def : defs) { + expr_safe_replace rep(m); + rep.insert(def.var, def.term); + for (unsigned i = 0; i < lits.size(); ++i) { + expr_ref tmp(m); + rep(lits.get(i), tmp); + lits[i] = tmp; + } + } + } + + void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) { + arith_util a(m); + model_evaluator mev(*mdl.get()); + vector> vals; + for (app* v : avars) { + rational val; + expr_ref tmp = mev(v); + VERIFY(a.is_numeral(tmp, val)); + vals.push_back(std::make_pair(val, v)); + } + struct compare_first { + bool operator()(std::pair const& x, + std::pair const& y) const { + return x.first < y.first; + } + }; + // add linear order between avars + compare_first cmp; + std::sort(vals.begin(), vals.end(), cmp); + for (unsigned i = 1; i < vals.size(); ++i) { + if (vals[i-1].first == vals[i].first) { + lits.push_back(m.mk_eq(vals[i-1].second, vals[i].second)); + } + else { + lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second)); + } + } + // sort avars based on depth + struct compare_depth { + bool operator()(app* x, app* y) const { + return x->get_depth() > y->get_depth(); + } + }; + compare_depth cmpd; + std::sort(avars.c_ptr(), avars.c_ptr() + avars.size(), cmpd); + TRACE("qe", tout << lits << "\navars:" << avars << "\n" << *mdl << "\n";); + } + + + void euf_arith_mbi_plugin::project0(model_ref& mdl, expr_ref_vector& lits) { + TRACE("qe", tout << lits << "\n" << *mdl << "\n";); + + + // 1. Extract projected variables, add inequalities between + // projected variables and non-projected terms according to model. + // 2. Extract disequalities implied by congruence closure. + // 3. project arithmetic variables from pure literals. + // 4. Add projected definitions as equalities to EUF. + // 5. project remaining literals with respect to EUF. + + app_ref_vector avars = get_arith_vars(mdl, lits); + TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); + + // 2. + term_graph tg1(m); + func_decl_ref_vector no_shared(m); + tg1.set_vars(no_shared, false); + tg1.add_lits(lits); + arith_util a(m); + expr_ref_vector foreign = tg1.shared_occurrences(a.get_family_id()); + obj_hashtable _foreign; + for (expr* e : foreign) _foreign.insert(e); + vector partition = tg1.get_partition(*mdl); + expr_ref_vector diseq = tg1.get_ackerman_disequalities(); + lits.append(diseq); + TRACE("qe", tout << "diseq: " << diseq << "\n"; + tout << "foreign: " << foreign << "\n"; + for (auto const& v : partition) { + tout << "partition: {"; + bool first = true; + for (expr* e : v) { + if (first) first = false; else tout << ", "; + tout << expr_ref(e, m); + } + tout << "}\n"; + } + ); + vector refined_partition; + for (auto & p : partition) { + unsigned j = 0; + for (expr* e : p) { + if (_foreign.contains(e) || + (is_app(e) && m_shared.contains(to_app(e)->get_decl()))) { + p[j++] = e; + } + } + p.shrink(j); + if (!p.empty()) refined_partition.push_back(p); + } + TRACE("qe", + for (auto const& v : refined_partition) { + tout << "partition: {"; + bool first = true; + for (expr* e : v) { + if (first) first = false; else tout << ", "; + tout << expr_ref(e, m); + } + tout << "}\n"; + }); + + + + arith_project_plugin ap(m); + ap.set_check_purified(false); + + // 3. + auto defs = ap.project(*mdl.get(), avars, lits); + + // 4. + for (auto const& def : defs) { + lits.push_back(m.mk_eq(def.var, def.term)); + } + TRACE("qe", tout << "# arith defs " << defs.size() << " avars: " << avars << " " << lits << "\n";); + + // 5. + term_graph tg2(m); + tg2.set_vars(m_shared, false); + tg2.add_lits(lits); + lits.reset(); + lits.append(tg2.project()); + TRACE("qe", tout << "project: " << lits << "\n";); + } + void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) { collect_atoms(lits); m_fmls.push_back(mk_not(mk_and(lits))); diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 1cc2be0cb..3563c472a 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -115,6 +115,9 @@ namespace qe { app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits); bool get_literals(model_ref& mdl, expr_ref_vector& lits); void collect_atoms(expr_ref_vector const& fmls); + void project0(model_ref& mdl, expr_ref_vector& lits); + void project(model_ref& mdl, expr_ref_vector& lits); + void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars); public: euf_arith_mbi_plugin(solver* s, solver* emptySolver); ~euf_arith_mbi_plugin() override {} diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index b5de20368..a5b01e59d 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -815,6 +815,7 @@ namespace qe { for (expr* r : roots) { args.push_back(r); } + TRACE("qe", tout << "function: " << d->get_name() << "\n";); res.push_back(m.mk_distinct(args.size(), args.c_ptr())); } } @@ -965,6 +966,7 @@ namespace qe { m_pinned.reset(); m_model.reset(); } + expr_ref_vector project() { expr_ref_vector res(m); purify();