diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1b1be9b52..d451c2c05 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2847,10 +2847,10 @@ proof * ast_manager::mk_bind_proof(quantifier * q, proof * p) { } proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) { - if (!p) return nullptr; - SASSERT(q1->get_num_decls() == q2->get_num_decls()); - SASSERT(has_fact(p)); - SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p))); + if (!p) return nullptr; + SASSERT(q1->get_num_decls() == q2->get_num_decls()); + SASSERT(has_fact(p)); + SASSERT(is_eq(get_fact(p)) || is_lambda(get_fact(p))); return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2)); } @@ -2858,7 +2858,7 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof if (!p) return nullptr; SASSERT(q1->get_num_decls() == q2->get_num_decls()); SASSERT(has_fact(p)); - SASSERT(is_oeq(get_fact(p))); + SASSERT(is_oeq(get_fact(p)) || is_lambda(get_fact(p))); return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_oeq(q1, q2)); } diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 18c29b97b..235576735 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -480,11 +480,9 @@ public: solver_ref sNotA = sf(m, p, false /* no proofs */, true, true, symbol::null); solver_ref sNotB = sf(m, p, false /* no proofs */, true, true, symbol::null); sA->assert_expr(a); - sNotA->assert_expr(m.mk_not(a)); sB->assert_expr(b); - sNotB->assert_expr(m.mk_not(b)); qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get()); - qe::euf_arith_mbi_plugin pB(sB.get(), sNotB.get()); + qe::prop_mbi_plugin pB(sB.get()); pA.set_shared(vars); pB.set_shared(vars); lbool res = mbi.pogo(pA, pB, itp); diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index e791d3546..d1bb90f0c 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -266,6 +266,7 @@ namespace opt { void model_based_opt::update_value(unsigned x, rational const& val) { rational old_val = m_var2value[x]; m_var2value[x] = val; + SASSERT(val.is_int() || !is_int(x)); unsigned_vector const& row_ids = m_var2row_ids[x]; for (unsigned row_id : row_ids) { rational coeff = get_coefficient(row_id, x); @@ -530,6 +531,7 @@ namespace opt { SASSERT(t_le == dst.m_type && t_le == src.m_type); SASSERT(src_c.is_int()); SASSERT(dst_c.is_int()); + SASSERT(m_var2value[x].is_int()); rational abs_src_c = abs(src_c); rational abs_dst_c = abs(dst_c); @@ -805,6 +807,7 @@ namespace opt { unsigned v = m_var2value.size(); m_var2value.push_back(value); m_var2is_int.push_back(is_int); + SASSERT(value.is_int() || !is_int); m_var2row_ids.push_back(unsigned_vector()); return v; } @@ -1017,7 +1020,6 @@ namespace opt { else { result = def(m_rows[glb_index], x); } - m_var2value[x] = eval(result); } // The number of matching lower and upper bounds is small. @@ -1114,8 +1116,7 @@ namespace opt { } def result = project(y, compute_def); if (compute_def) { - result = (result * D) + u; - m_var2value[x] = eval(result); + result = (result * D) + u; } SASSERT(!compute_def || eval(result) == eval(x)); return result; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index ff4c7dc52..8729edb36 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -41,7 +41,7 @@ namespace qe { bool m_check_purified; // check that variables are properly pure void insert_mul(expr* x, rational const& v, obj_map& ts) { - TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";); + // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";); rational w; if (ts.find(x, w)) { ts.insert(x, w + v); @@ -92,8 +92,8 @@ namespace qe { rational r1, r2; expr_ref val1 = eval(e1); expr_ref val2 = eval(e2); - TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";); - TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";); + //TRACE("qe", tout << mk_pp(e1, m) << " " << val1 << "\n";); + //TRACE("qe", tout << mk_pp(e2, m) << " " << val2 << "\n";); if (!a.is_numeral(val1, r1)) return false; if (!a.is_numeral(val2, r2)) return false; SASSERT(r1 != r2); @@ -306,14 +306,14 @@ namespace qe { return vector(); } model_evaluator eval(model); - TRACE("qe", model_smt2_pp(tout, m, model, 0);); + TRACE("qe", tout << model;); // eval.set_model_completion(true); opt::model_based_opt mbo; obj_map tids; expr_ref_vector pinned(m); unsigned j = 0; - TRACE("qe", tout << "fmls: " << fmls << "\n";); + TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";); for (unsigned i = 0; i < fmls.size(); ++i) { expr * fml = fmls.get(i); if (!linearize(mbo, eval, fml, fmls, tids)) { @@ -325,7 +325,6 @@ namespace qe { } } fmls.shrink(j); - TRACE("qe", tout << "linearized: " << fmls << "\n";); // fmls holds residue, // mbo holds linear inequalities that are in scope diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 86fc1ac3c..0b0a9fe10 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -25,52 +25,6 @@ Notes: Other theories: DT, ARR reduced to EUF BV is EUF/Boolean. - Purify EUF1 & LIRA1 & EUF2 & LIRA2 - - Then EUF1 & EUF2 |- false - LIRA1 & LIRA2 |- false - - Sketch of approach by example: - - A: s <= 2a <= t & f(a) = q - - B: t <= 2b <= s + 1 & f(b) != q - - 1. Extract arithmetic consequences of A over shared vocabulary. - - A -> s <= t & (even(t) | s < t) - - 2a. Send to B, have B solve shared variables with EUF_B. - epsilon b . B & A_pure - epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t) - = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t) - = even(t) & t = s - b := t div 2 - - B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1 - - 3a. Send purified result to A - A & B_pure -> false - - Invoke the ping-pong principle to extract interpolant. - - 2b. Solve for shared variables with EUF. - - epsilon a . A - = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q - - 3b. Send to B. Produces core - s < t & f((s + 1) div 2) = q - - 4b Solve again in arithmetic for shared variables with EUF. - - epsion a . A & (s >= t | f((s + 1) div 2) != q) - - a := t div 2 | s = t & f(t div 2) = q & even(t) - - Send to B, produces core (s != t | f(t div 2) != q) - - 5b. There is no longer a solution for A. A is unsat. --*/ @@ -240,15 +194,24 @@ namespace qe { // euf_arith_mbi struct euf_arith_mbi_plugin::is_atom_proc { - ast_manager& m; - expr_ref_vector& m_atoms; - is_atom_proc(expr_ref_vector& atoms): m(atoms.m()), m_atoms(atoms) {} + ast_manager& m; + expr_ref_vector& m_atoms; + obj_hashtable& m_atom_set; + + is_atom_proc(expr_ref_vector& atoms, obj_hashtable& atom_set): + m(atoms.m()), m_atoms(atoms), m_atom_set(atom_set) {} + void operator()(app* a) { - if (m.is_eq(a)) { + if (m_atom_set.contains(a)) { + // continue + } + else if (m.is_eq(a)) { m_atoms.push_back(a); + m_atom_set.insert(a); } else if (m.is_bool(a) && a->get_family_id() != m.get_basic_family_id()) { m_atoms.push_back(a); + m_atom_set.insert(a); } } void operator()(expr*) {} @@ -275,38 +238,44 @@ namespace qe { euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot): mbi_plugin(s->get_manager()), m_atoms(m), + m_fmls(m), m_solver(s), m_dual_solver(sNot) { params_ref p; p.set_bool("core.minimize", true); m_solver->updt_params(p); m_dual_solver->updt_params(p); - expr_ref_vector fmls(m); - m_solver->get_assertions(fmls); + m_solver->get_assertions(m_fmls); + collect_atoms(m_fmls); + } + + void euf_arith_mbi_plugin::collect_atoms(expr_ref_vector const& fmls) { expr_fast_mark1 marks; - is_atom_proc proc(m_atoms); + is_atom_proc proc(m_atoms, m_atom_set); for (expr* e : fmls) { quick_for_each_expr(proc, marks, e); } } bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) { - model_evaluator mev(*mdl.get()); - lits.reset(); - for (expr* e : m_atoms) { - if (mev.is_true(e)) { - lits.push_back(e); - } - else if (mev.is_false(e)) { - lits.push_back(m.mk_not(e)); - } + lits.reset(); + for (expr* e : m_atoms) { + if (mdl->is_true(e)) { + lits.push_back(e); } - TRACE("qe", tout << "atoms from model: " << lits << "\n";); - lbool r = m_dual_solver->check_sat(lits); + else if (mdl->is_false(e)) { + lits.push_back(m.mk_not(e)); + } + } + TRACE("qe", tout << "atoms from model: " << lits << "\n";); + solver_ref dual = m_dual_solver->translate(m, m_dual_solver->get_params()); + dual->assert_expr(mk_not(mk_and(m_fmls))); + lbool r = dual->check_sat(lits); + TRACE("qe", dual->display(tout << "dual result " << r << "\n");); if (l_false == r) { - // use the dual solver to find a 'small' implicant - lits.reset(); - m_dual_solver->get_unsat_core(lits); + // use the dual solver to find a 'small' implicant + lits.reset(); + dual->get_unsat_core(lits); return true; } else { @@ -351,15 +320,15 @@ namespace qe { 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";); + TRACE("qe", tout << "# arith defs " << defs.size() << " avars: " << avars << " " << lits << "\n";); // 3. Project the remaining literals with respect to EUF. term_graph tg(m); tg.set_vars(m_shared, false); tg.add_lits(lits); lits.reset(); - lits.append(tg.project(*mdl)); - //lits.append(tg.project()); + //lits.append(tg.project(*mdl)); + lits.append(tg.project()); TRACE("qe", tout << "project: " << lits << "\n";); return mbi_sat; } @@ -374,7 +343,9 @@ namespace qe { } void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) { - m_solver->assert_expr(mk_not(mk_and(lits))); + collect_atoms(lits); + m_fmls.push_back(mk_not(mk_and(lits))); + m_solver->assert_expr(m_fmls.back()); } diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 22a0864ba..928bb7845 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -104,17 +104,19 @@ namespace qe { }; class euf_arith_mbi_plugin : public mbi_plugin { - expr_ref_vector m_atoms; - solver_ref m_solver; - solver_ref m_dual_solver; + expr_ref_vector m_atoms; + obj_hashtable m_atom_set; + expr_ref_vector m_fmls; + solver_ref m_solver; + solver_ref m_dual_solver; struct is_atom_proc; struct is_arith_var_proc; app_ref_vector get_arith_vars(expr_ref_vector const& lits); bool get_literals(model_ref& mdl, expr_ref_vector& lits); - + void collect_atoms(expr_ref_vector const& fmls); public: - euf_arith_mbi_plugin(solver* s, solver* sNot); + euf_arith_mbi_plugin(solver* s, solver* emptySolver); ~euf_arith_mbi_plugin() override {} mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void block(expr_ref_vector const& lits) override; diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp index 1f314848f..6ec840de1 100644 --- a/src/qe/qe_solve_plugin.cpp +++ b/src/qe/qe_solve_plugin.cpp @@ -99,7 +99,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) << " " << e << " := " << t << "\n";); + TRACE("qe", tout << mk_pp(lhs, m) << " " << mk_pp(rhs, m) << " " << mk_pp(e, m) << " := " << t << "\n";); return true; } else { diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 510868366..81729fb37 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -125,7 +125,7 @@ namespace qe { children(term const* _t):t(*_t) {} ptr_vector::const_iterator begin() const { return t.m_children.begin(); } ptr_vector::const_iterator end() const { return t.m_children.end(); } - }; + }; // Congruence table hash function is based on // roots of children and function declaration. @@ -198,8 +198,23 @@ namespace qe { } while (curr != this); } + + std::ostream& display(std::ostream& out) const { + out << "expr: " << m_expr << " class: "; + term const* r = this; + do { + out << r->get_id() << " "; + r = &r->get_next(); + } + while (r != this); + out << "\n"; + return out; + } }; + static std::ostream& operator<<(std::ostream& out, term const& t) { + return t.display(out); + } bool term_graph::is_variable_proc::operator()(const expr * e) const { if (!is_app(e)) return false; @@ -516,10 +531,7 @@ namespace qe { void term_graph::display(std::ostream &out) { for (term * t : m_terms) { - out << mk_pp(t->get_expr(), m) << " is root " << t->is_root() - << " cls sz " << t->get_class_size() - << " term " << t - << "\n"; + out << *t; } } @@ -608,7 +620,7 @@ namespace qe { term* t = worklist.back(); worklist.pop_back(); t->set_mark(false); - if (m_term2app.contains(t->get_id())) + if (m_term2app.contains(t->get_id())) continue; if (!t->is_theory() && is_projected(*t)) continue; @@ -641,6 +653,7 @@ namespace qe { // and can be mined using other means, such as theory // aware core minimization m_tg.reset_marks(); + TRACE("qe", m_tg.display(tout << "after purify\n");); } void solve_core() { @@ -695,6 +708,7 @@ namespace qe { if (!m.is_eq(lit) && find_app(lit, e)) res.push_back(e); } + TRACE("qe", tout << "literals: " << res << "\n";); } void mk_pure_equalities(const term &t, expr_ref_vector &res) { @@ -736,7 +750,8 @@ namespace qe { while (r != &t); } - void mk_equalities(bool pure, expr_ref_vector &res) { + template + void mk_equalities(expr_ref_vector &res) { for (term *t : m_tg.m_terms) { if (!t->is_root()) continue; if (!m_root2rep.contains(t->get_id())) continue; @@ -745,14 +760,15 @@ namespace qe { else mk_unpure_equalities(*t, res); } + TRACE("qe", tout << "literals: " << res << "\n";); } void mk_pure_equalities(expr_ref_vector &res) { - return mk_equalities(true, res); + mk_equalities(res); } void mk_unpure_equalities(expr_ref_vector &res) { - return mk_equalities(false, res); + mk_equalities(res); } // TBD: generalize for also the case of a (:var n) @@ -813,6 +829,11 @@ namespace qe { TRACE("qe", tout << "after distinct: " << res << "\n";); } + std::ostream& display(std::ostream& out) const { + + return out; + } + public: projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {}