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<expr> _foreign;
- for (expr* e : foreign) _foreign.insert(e);
- vector<expr_ref_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<expr_ref_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<std::pair<rational, app*>> 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<rational, app*> const& x,
+ std::pair<rational, app*> 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<expr> _foreign;
+ for (expr* e : foreign) _foreign.insert(e);
+ vector<expr_ref_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<expr_ref_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();