From 20fc573d5b12e84d90ece113cdd7c938afe11ee0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jun 2018 11:24:56 -0700 Subject: [PATCH 1/2] add laxer check for oeq_quant_intro Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 +-- src/cmd_context/extra_cmds/dbg_cmds.cpp | 4 +- src/math/simplex/model_based_opt.cpp | 7 +- src/qe/qe_arith.cpp | 11 ++- src/qe/qe_mbi.cpp | 113 +++++++++--------------- src/qe/qe_mbi.h | 12 +-- src/qe/qe_solve_plugin.cpp | 2 +- src/qe/qe_term_graph.cpp | 39 ++++++-- 8 files changed, 95 insertions(+), 103 deletions(-) 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) {} From 7844476a7d47e114a3488a0b27e066ead50d1fd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jun 2018 17:04:47 -0700 Subject: [PATCH 2/2] fixes to term-graph, add proof-checker routines for PR_BIND, remove orphaned file Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 10 +- src/ast/proofs/proof_checker.cpp | 13 ++ src/muz/spacer/spacer_util.cpp | 2 +- src/muz/transforms/dl_mk_coi_filter.cpp | 1 - src/qe/qe_term_graph.cpp | 155 ++++++++++++++++++++---- src/qe/qe_term_graph.h | 2 +- src/tactic/extension_model_converter.h | 49 -------- 7 files changed, 153 insertions(+), 79 deletions(-) delete mode 100644 src/tactic/extension_model_converter.h diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index d451c2c05..0ea2f3cd5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1122,11 +1122,11 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : nullptr; case OP_DISTINCT: return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); - case PR_BIND: { - ptr_buffer sorts; - for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i])); - return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); - } + case PR_BIND: { + ptr_buffer sorts; + for (unsigned i = 0; i < num_args; ++i) sorts.push_back(m_manager->get_sort(args[i])); + return mk_func_decl(k, num_parameters, parameters, num_args, sorts.c_ptr(), range); + } default: break; } diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index c98f63d28..b8d7b2b46 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -335,6 +335,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { return false; } case PR_QUANT_INTRO: { + if (match_proof(p, p1) && + match_fact(p, fact) && + match_fact(p1.get(), fml) && + (is_lambda(fact) || is_lambda(fml))) + return true; + if (match_proof(p, p1) && match_fact(p, fact) && match_fact(p1.get(), fml) && @@ -361,6 +367,13 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { UNREACHABLE(); return false; } + case PR_BIND: + // it is a lambda expression returning a proof object. + if (!is_lambda(to_app(p)->get_arg(0))) + return false; + // check that body is a proof object. + return true; + case PR_DISTRIBUTIVITY: { if (match_fact(p, fact) && match_proof(p) && diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 146434c0a..42b40c665 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -690,7 +690,7 @@ namespace { qe::term_graph egraph(out.m()); for (expr* e : v) egraph.add_lit(to_app(e)); tout << "Reduced app:\n" - << mk_pp(egraph.to_app(), out.m()) << "\n";); + << mk_pp(egraph.to_expr(), out.m()) << "\n";); out = mk_and(v); } } diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index e37444c5e..457905a56 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -23,7 +23,6 @@ Author: #include "ast/ast_pp.h" #include "tactic/generic_model_converter.h" #include "ast/ast_util.h" -#include "tactic/extension_model_converter.h" namespace datalog { rule_set * mk_coi_filter::operator()(rule_set const & source) { diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 81729fb37..5cf1206a3 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -200,13 +200,12 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - out << "expr: " << m_expr << " class: "; - term const* r = this; - do { + out << get_id() << ": " << m_expr << " - "; + term const* r = &this->get_next(); + while (r != this) { out << r->get_id() << " "; r = &r->get_next(); } - while (r != this); out << "\n"; return out; } @@ -554,7 +553,7 @@ namespace qe { } } - expr_ref term_graph::to_app() { + expr_ref term_graph::to_expr() { expr_ref_vector lits(m); to_lits(lits); return mk_and(lits); @@ -587,8 +586,15 @@ namespace qe { app* a = ::to_app(e); expr_ref_buffer kids(m); for (term* ch : term::children(t)) { - if (!m_root2rep.find(ch->get_root().get_id(), e)) return nullptr; - kids.push_back(e); + // prefer a node that resembles current child, + // otherwise, pick a root representative, if present. + if (m_term2app.find(ch->get_id(), e)) + kids.push_back(e); + else if (m_root2rep.find(ch->get_root().get_id(), e)) + kids.push_back(e); + else + return nullptr; + TRACE("qe_verbose", tout << *ch << " -> " << mk_pp(e, m) << "\n";); } expr* pure = m.mk_app(a->get_decl(), kids.size(), kids.c_ptr()); m_pinned.push_back(pure); @@ -602,6 +608,12 @@ namespace qe { return m.is_unique_value(t1) && !m.is_unique_value(t2); } + struct term_depth { + bool operator()(term const* t1, term const* t2) const { + return get_depth(t1->get_expr()) < get_depth(t2->get_expr()); + } + }; + void purify() { // - propagate representatives up over parents. // use work-list + marking to propagate. @@ -615,10 +627,12 @@ namespace qe { worklist.push_back(t); t->set_mark(true); } + // traverse worklist in order of depth. + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); - while (!worklist.empty()) { - term* t = worklist.back(); - worklist.pop_back(); + for (unsigned i = 0; i < worklist.size(); ++i) { + term* t = worklist[i]; t->set_mark(false); if (m_term2app.contains(t->get_id())) continue; @@ -629,8 +643,8 @@ namespace qe { if (!pure) continue; m_term2app.insert(t->get_id(), pure); - expr* rep = nullptr; - // ensure that the root has a representative + TRACE("qe_verbose", tout << "purified " << *t << " " << mk_pp(pure, m) << "\n";); + expr* rep = nullptr; // ensure that the root has a representative m_root2rep.find(t->get_root().get_id(), rep); // update rep with pure if it is better @@ -653,7 +667,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");); + TRACE("qe", display(tout << "after purify\n");); } void solve_core() { @@ -664,10 +678,11 @@ namespace qe { worklist.push_back(t); t->set_mark(true); } + term_depth td; + std::sort(worklist.begin(), worklist.end(), td); - while (!worklist.empty()) { - term* t = worklist.back(); - worklist.pop_back(); + for (unsigned i = 0; i < worklist.size(); ++i) { + term* t = worklist[i]; t->set_mark(false); if (m_term2app.contains(t->get_id())) continue; @@ -695,11 +710,16 @@ namespace qe { } bool find_app(term &t, expr *&res) { - return m_root2rep.find(t.get_root().get_id(), res); + return + m_term2app.find(t.get_id(), res) || + m_root2rep.find(t.get_root().get_id(), res); } bool find_app(expr *lit, expr *&res) { - return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res); + term const* t = m_tg.get_term(lit); + return + m_term2app.find(t->get_id(), res) || + m_root2rep.find(t->get_root().get_id(), res); } void mk_lits(expr_ref_vector &res) { @@ -711,6 +731,90 @@ namespace qe { TRACE("qe", tout << "literals: " << res << "\n";); } + void lits2pure(expr_ref_vector& res) { + expr *e1 = nullptr, *e2 = nullptr, *p1 = nullptr, *p2 = nullptr; + for (auto *lit : m_tg.m_lits) { + if (m.is_eq(lit, e1, e2)) { + if (find_app(e1, p1) && find_app(e2, p2)) { + if (p1 != p2) + res.push_back(m.mk_eq(p1, p2)); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + else if (m.is_distinct(lit)) { + ptr_buffer diff; + for (expr* arg : *to_app(lit)) { + if (find_app(arg, p1)) { + diff.push_back(p1); + } + } + if (diff.size() > 1) { + res.push_back(m.mk_distinct(diff.size(), diff.c_ptr())); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + else if (find_app(lit, p1)) { + res.push_back(p1); + } + else { + TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); + } + } + TRACE("qe", tout << "literals: " << res << "\n";); + } + + void mk_distinct(expr_ref_vector& res) { + vector> decl2terms; // terms that use function f + ptr_vector decls; + decl2terms.reset(); + // Collect the projected function symbols. + for (term *t : m_tg.m_terms) { + expr* e = t->get_expr(); + if (!is_app(e)) continue; + if (!is_projected(*t)) continue; + app* a = to_app(e); + func_decl* d = a->get_decl(); + if (d->get_arity() == 0) continue; + unsigned id = d->get_decl_id(); + decl2terms.reserve(id+1); + if (decl2terms[id].empty()) decls.push_back(d); + decl2terms[id].push_back(t); + } + + // + // for each projected function that occurs + // (may occur) in multiple congruence classes, + // produce assertions that non-congruent arguments + // are forced distinct. + // + for (func_decl* d : decls) { + unsigned id = d->get_decl_id(); + ptr_vector const& terms = decl2terms[id]; + if (terms.size() <= 1) continue; + unsigned arity = d->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + obj_hashtable roots; + for (term* t : terms) { + expr* arg = to_app(t->get_expr())->get_arg(i); + term const& root = m_tg.get_term(arg)->get_root(); + roots.insert(root.get_expr()); + } + if (roots.size() > 1) { + ptr_buffer args; + for (expr* r : roots) { + args.push_back(r); + } + res.push_back(m.mk_distinct(args.size(), args.c_ptr())); + } + } + } + TRACE("qe", tout << res << "\n";); + } + void mk_pure_equalities(const term &t, expr_ref_vector &res) { SASSERT(t.is_root()); expr *rep = nullptr; @@ -830,7 +934,15 @@ namespace qe { } std::ostream& display(std::ostream& out) const { - + m_tg.display(out); + out << "term2app:\n"; + for (auto const& kv : m_term2app) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } + out << "root2rep:\n"; + for (auto const& kv : m_root2rep) { + out << kv.m_key << " |-> " << mk_pp(kv.m_value, m) << "\n"; + } return out; } @@ -849,9 +961,8 @@ namespace qe { expr_ref_vector project() { expr_ref_vector res(m); purify(); - mk_lits(res); - mk_pure_equalities(res); - model_complete(res); + lits2pure(res); + mk_distinct(res); reset(); return res; } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 19b694a76..2ab234a96 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -102,7 +102,7 @@ namespace qe { // deprecate? void to_lits(expr_ref_vector &lits, bool all_equalities = false); - expr_ref to_app(); + expr_ref to_expr(); /** * Return literals obtained by projecting added literals diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h deleted file mode 100644 index 0816fdd8b..000000000 --- a/src/tactic/extension_model_converter.h +++ /dev/null @@ -1,49 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - extension_model_converter.h - -Abstract: - - Model converter that introduces new interpretations into a model. - It used to be called elim_var_model_converter - -Author: - - Leonardo (leonardo) 2011-10-21 - -Notes: - ---*/ -#ifndef EXTENSION_MODEL_CONVERTER_H_ -#define EXTENSION_MODEL_CONVERTER_H_ - -#include "ast/ast.h" -#include "tactic/model_converter.h" - - -class extension_model_converter : public model_converter { - func_decl_ref_vector m_vars; - expr_ref_vector m_defs; -public: - extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) { - } - - ~extension_model_converter() override; - - ast_manager & m() const { return m_vars.get_manager(); } - - void operator()(model_ref & md) override; - - void display(std::ostream & out) override; - - // register a variable that was eliminated - void insert(func_decl * v, expr * def); - - model_converter * translate(ast_translation & translator) override; -}; - - -#endif