From ba504e4243908ea2074fc6f2cdaa8894be78ed22 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Jun 2018 21:22:53 -0700 Subject: [PATCH] debugging mbi Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/dbg_cmds.cpp | 54 +++++++++++++++++++++++++ src/qe/qe_mbi.cpp | 13 +++++- src/qe/qe_term_graph.cpp | 30 +++++++------- src/smt/smt_solver.cpp | 2 +- 4 files changed, 82 insertions(+), 17 deletions(-) diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index bedbf84aa..62d5ea3ea 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -29,6 +29,7 @@ Notes: #include "tactic/arith/bound_manager.h" #include "ast/used_vars.h" #include "ast/rewriter/var_subst.h" +#include "ast/ast_util.h" #include "util/gparams.h" #include "qe/qe_mbp.h" #include "qe/qe_mbi.h" @@ -437,7 +438,58 @@ public: lbool res = mbi.pingpong(pA, pB, vars, itp); ctx.regular_stream() << res << " " << itp << "\n"; } +}; + +class eufi_cmd : public cmd { + expr* m_a; + expr* m_b; + ptr_vector m_vars; +public: + eufi_cmd():cmd("eufi") {} + char const * get_usage() const override { return " (vars)"; } + char const * get_descr(cmd_context & ctx) const override { return "perform model based interpolation"; } + unsigned get_arity() const override { return 3; } + cmd_arg_kind next_arg_kind(cmd_context& ctx) const override { + if (m_a == nullptr) return CPK_EXPR; + if (m_b == nullptr) return CPK_EXPR; + return CPK_FUNC_DECL_LIST; + } + void set_next_arg(cmd_context& ctx, expr * arg) override { + if (m_a == nullptr) + m_a = arg; + else + m_b = arg; + } + void set_next_arg(cmd_context & ctx, unsigned num, func_decl * const * ts) override { + m_vars.append(num, ts); + } + void prepare(cmd_context & ctx) override { m_a = nullptr; m_b = nullptr; m_vars.reset(); } + void execute(cmd_context & ctx) override { + ast_manager& m = ctx.m(); + func_decl_ref_vector vars(m); + for (func_decl* v : m_vars) { + vars.push_back(v); + } + qe::interpolator mbi(m); + expr_ref a(m_a, m); + expr_ref b(m_b, m); + expr_ref itp(m); + solver_factory& sf = ctx.get_solver_factory(); + params_ref p; + solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null); + solver_ref sB = sf(m, p, false /* no proofs */, true, true, symbol::null); + 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_mbi_plugin pA(sA.get(), sNotA.get()); + qe::euf_mbi_plugin pB(sB.get(), sNotB.get()); + lbool res = mbi.pogo(pA, pB, vars, itp); + ctx.regular_stream() << res << " " << itp << "\n"; + } }; @@ -468,6 +520,7 @@ public: expr_ref_vector lits(m); for (func_decl* v : m_vars) vars.push_back(v); for (expr* e : m_lits) lits.push_back(e); + flatten_and(lits); qe::term_graph tg(m); tg.add_lits(lits); expr_ref_vector p = tg.project(vars, false); @@ -504,4 +557,5 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(mbp_cmd)); ctx.insert(alloc(mbi_cmd)); ctx.insert(alloc(euf_project_cmd)); + ctx.insert(alloc(eufi_cmd)); } diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index d47c2ab2c..4b86a10a4 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -30,13 +30,17 @@ Revision History: namespace qe { lbool mbi_plugin::check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { - SASSERT(lits.empty()); + ast_manager& m = lits.get_manager(); + expr_ref_vector lits0(lits); while (true) { + lits.reset(); + lits.append(lits0); switch ((*this)(vars, lits, mdl)) { case mbi_sat: return l_true; case mbi_unsat: if (lits.empty()) return l_false; + TRACE("qe", tout << "block: " << lits << "\n";); block(lits); break; case mbi_undef: @@ -111,6 +115,10 @@ namespace qe { m_solver(s), m_dual_solver(sNot) { + params_ref p; + p.set_bool("smt.core.minimize", true); + m_solver->updt_params(p); + m_dual_solver->updt_params(p); expr_ref_vector fmls(m); m_solver->get_assertions(fmls); expr_fast_mark1 marks; @@ -141,6 +149,7 @@ namespace qe { lits.push_back(m.mk_not(e)); } } + TRACE("qe", tout << "atoms from model: " << lits << "\n";); r = m_dual_solver->check_sat(lits); expr_ref_vector core(m); term_graph tg(m); @@ -148,10 +157,12 @@ namespace qe { case l_false: // use the dual solver to find a 'small' implicant m_dual_solver->get_unsat_core(core); + TRACE("qe", tout << "core: " << core << "\n";); // project the implicant onto vars tg.add_lits(core); lits.reset(); lits.append(tg.project(vars, false)); + TRACE("qe", tout << "project: " << lits << "\n";); return mbi_sat; case l_undef: return mbi_undef; diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 40f3998e7..8e3981e64 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -65,9 +65,9 @@ namespace qe { m_children.push_back(t); } } - + ~term() {} - + class parents { term const& t; public: @@ -168,9 +168,9 @@ namespace qe { arith_term_graph_plugin(term_graph &g) : term_graph_plugin (g.get_ast_manager().mk_family_id("arith")), m_g(g), m(g.get_ast_manager()), m_arith(m) {(void)m_g;} - + virtual ~arith_term_graph_plugin() {} - + bool mk_eq_core (expr *_e1, expr *_e2, expr_ref &res) { expr *e1, *e2; e1 = _e1; @@ -385,7 +385,7 @@ namespace qe { SASSERT(res); return res; } - + void term_graph::internalize_eq(expr *a1, expr* a2) { SASSERT(m_merge.empty()); merge(*internalize_term(a1), *internalize_term(a2)); @@ -415,17 +415,17 @@ namespace qe { void term_graph::merge(term &t1, term &t2) { // -- merge might invalidate term2app cache m_term2app.reset(); - m_pinned.reset(); - + m_pinned.reset(); + term *a = &t1.get_root(); term *b = &t2.get_root(); - + if (a == b) return; - + if (a->get_class_size() > b->get_class_size()) { std::swap(a, b); } - + // Remove parents of it from the cg table. for (term* p : term::parents(b)) { if (!p->is_marked()) { @@ -736,7 +736,7 @@ namespace qe { } } m_tg.reset_marks(); - } + } bool find_app(term &t, expr *&res) { return m_root2rep.find(t.get_root().get_id(), res); @@ -744,7 +744,7 @@ namespace qe { bool find_app(expr *lit, expr *&res) { return m_root2rep.find(m_tg.get_term(lit)->get_root().get_id(), res); - } + } void mk_lits(expr_ref_vector &res) { expr *e = nullptr; @@ -752,7 +752,7 @@ namespace qe { if (!m.is_eq(lit) && find_app(lit, e)) res.push_back(e); } - } + } void mk_pure_equalities(const term &t, expr_ref_vector &res) { expr *rep = nullptr; @@ -842,12 +842,12 @@ namespace qe { return res; } }; - } + } expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { projector p(*this); return p.project(decls, exclude); - } + } expr_ref_vector term_graph::solve(func_decl_ref_vector const &decls, bool exclude) { projector p(*this); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 1e49f7f87..b0a8153a5 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -215,7 +215,7 @@ namespace smt { r.push_back(m_context.get_unsat_core_expr(i)); } - if (m_minimizing_core && smt_params_helper(get_params()).core_minimize()) { + if (!m_minimizing_core && smt_params_helper(get_params()).core_minimize()) { scoped_minimize_core scm(*this); mus mus(*this); mus.add_soft(r.size(), r.c_ptr());