diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 1f96f3387..481a72816 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -46,7 +46,6 @@ Notes: namespace qe { void mbi_plugin::set_shared(expr* a, expr* b) { - TRACE("qe", tout << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";); struct fun_proc { obj_hashtable s; void operator()(app* a) { if (is_uninterp(a)) s.insert(a->get_decl()); } @@ -75,6 +74,9 @@ namespace qe { }; intersect_proc symbols_in_b(*this, symbols_in_a.s); quick_for_each_expr(symbols_in_b, marks, b); + TRACE("qe", + tout << mk_pp(a, m) << "\n" << mk_pp(b, m) << "\n"; + for (func_decl* f : m_shared) tout << f->get_name() << " "; tout << "\n";); } lbool mbi_plugin::check(expr_ref_vector& lits, model_ref& mdl) { @@ -349,17 +351,58 @@ namespace qe { /** - \brief add difference certificates to formula. - + \brief add difference certificates to formula. */ void uflia_mbi::add_dcert(model_ref& mdl, expr_ref_vector& lits) { term_graph tg(m); + add_arith_dcert(*mdl.get(), lits); func_decl_ref_vector shared(m_shared_trail); tg.set_vars(shared, false); lits.append(tg.dcert(*mdl.get(), lits)); TRACE("qe", tout << "project: " << lits << "\n";); } + /** + Add disequalities between functions that appear in arithmetic context. + */ + void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits) { + obj_map> apps; + arith_util a(m); + for (expr* e : subterms(lits)) { + if (a.is_int_real(e) && is_uninterp(e) && to_app(e)->get_num_args() > 0) { + func_decl* f = to_app(e)->get_decl(); + auto* v = apps.insert_if_not_there2(f, ptr_vector()); + v->get_data().m_value.push_back(to_app(e)); + } + } + for (auto const& kv : apps) { + ptr_vector const& es = kv.m_value; + expr_ref_vector values(m); + for (expr* e : kv.m_value) values.push_back(mdl(e)); + for (unsigned i = 0; i < es.size(); ++i) { + expr* v1 = values.get(i); + for (unsigned j = i + 1; j < es.size(); ++j) { + expr* v2 = values.get(j); + if (v1 != v2) { + add_arith_dcert(mdl, lits, es[i], es[j]); + } + } + } + } + } + + void uflia_mbi::add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b) { + arith_util arith(m); + SASSERT(a->get_decl() == b->get_decl()); + for (unsigned i = a->get_num_args(); i-- > 0; ) { + expr* arg1 = a->get_arg(i), *arg2 = b->get_arg(i); + if (arith.is_int_real(arg1) && mdl(arg1) != mdl(arg2)) { + lits.push_back(m.mk_not(m.mk_eq(arg1, arg2))); + return; + } + } + } + /** * \brief project private symbols. */ diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 72ff9dbcb..34a2c1799 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -123,6 +123,8 @@ namespace qe { void order_avars(app_ref_vector& avars); void add_dcert(model_ref& mdl, expr_ref_vector& lits); + void add_arith_dcert(model& mdl, expr_ref_vector& lits); + void add_arith_dcert(model& mdl, expr_ref_vector& lits, app* a, app* b); app_ref_vector get_arith_vars(expr_ref_vector const& lits); vector arith_project(model_ref& mdl, app_ref_vector& avars, expr_ref_vector& lits); void project_euf(model_ref& mdl, expr_ref_vector& lits); diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp index d7ff430e2..8b63402fa 100644 --- a/src/qe/qe_solve_plugin.cpp +++ b/src/qe/qe_solve_plugin.cpp @@ -100,7 +100,7 @@ namespace qe { v = e; a_val = rational(1)/a_val; t = mk_term(is_int, a_val, sign, done); - TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << t << "\n";); + TRACE("qe", tout << mk_pp(e, m) << " := " << t << "\n";); return true; } else { @@ -147,7 +147,7 @@ namespace qe { } - expr_ref mk_eq_core (expr *e1, expr *e2) { + expr_ref mk_eq_core(expr *e1, expr *e2) { expr_ref v(m), t(m); if (solve(e1, e2, v, t)) { return expr_ref(m.mk_eq(v, t), m); @@ -201,7 +201,7 @@ namespace qe { return a.mk_ge(arg, mk_zero()); } - bool mk_le_core (expr *arg1, expr * arg2, expr_ref &result) { + bool mk_le_core(expr *arg1, expr * arg2, expr_ref &result) { // t <= -1 ==> t < 0 ==> ! (t >= 0) rational n; if (a.is_int (arg1) && a.is_minus_one (arg2)) { @@ -220,16 +220,16 @@ namespace qe { return false; } - expr * mk_zero () { + expr * mk_zero() { return a.mk_numeral (rational (0), true); } - bool is_one (expr const * n) const { + bool is_one(expr const * n) const { rational val; return a.is_numeral (n, val) && val.is_one (); } - bool mk_ge_core (expr * arg1, expr * arg2, expr_ref &result) { + bool mk_ge_core(expr * arg1, expr * arg2, expr_ref &result) { // t >= 1 ==> t > 0 ==> ! (t <= 0) rational n; if (a.is_int (arg1) && is_one (arg2)) { diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 1dc01678a..9e080de5f 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -725,9 +725,22 @@ namespace qe { TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); } } + remove_duplicates(res); TRACE("qe", tout << "literals: " << res << "\n";); } + void remove_duplicates(expr_ref_vector& v) { + obj_hashtable seen; + unsigned j = 0; + for (expr* e : v) { + if (!seen.contains(e)) { + v[j++] = e; + seen.insert(e); + } + } + v.shrink(j); + } + vector> m_decl2terms; // terms that use function f ptr_vector m_decls; @@ -1202,22 +1215,27 @@ namespace qe { hashtable diseqs; expr_ref_vector result(m); add_lits(lits); - auto const partitions = get_partition(mdl); svector todo; + + // TBD: + // M(f(a1 + 5)) != M(f(x1 + 5)) => a1 + 5 != x1 + 5 part of dcert. + // collect subterms in arith, put equal function subterms in certifiability set + for (expr* e : lits) { expr* ne, *a, *b; if (m.is_not(e, ne) && m.is_eq(ne, a, b) && (is_uninterp(a) || is_uninterp(b))) { - todo.push_back(pair_t(a, b)); + diseqs.insert(pair_t(a, b)); } else if (is_uninterp(e)) { - todo.push_back(pair_t(e, m.mk_false())); + diseqs.insert(pair_t(e, m.mk_false())); } else if (m.is_not(e, ne) && is_uninterp(ne)) { - todo.push_back(pair_t(ne, m.mk_true())); - } + diseqs.insert(pair_t(ne, m.mk_true())); + } } - for (auto& p : todo) diseqs.insert(p); + for (auto& p : diseqs) todo.push_back(p); + auto const partitions = get_partition(mdl); obj_map term2pid; unsigned id = 0; for (auto const& vec : partitions) {