From 688cf79619fbc291938f63d16ffbe7ee368d23cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jun 2018 09:55:32 -0700 Subject: [PATCH] working on mbi Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/dbg_cmds.cpp | 50 ++++++++++++- src/qe/CMakeLists.txt | 1 + src/qe/qe_mbi.cpp | 93 ++++++++++++++++++++----- src/qe/qe_mbi.h | 16 ++++- src/smt/smt_context.cpp | 66 ++++++++++++------ src/smt/smt_context.h | 2 + 6 files changed, 184 insertions(+), 44 deletions(-) diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index 31fc4b008..c6cd1020e 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -31,6 +31,7 @@ Notes: #include "ast/rewriter/var_subst.h" #include "util/gparams.h" #include "qe/qe_mbp.h" +#include "qe/qe_mbi.h" BINARY_SYM_CMD(get_quantifier_body_cmd, @@ -358,7 +359,7 @@ class mbp_cmd : public cmd { ptr_vector m_vars; public: mbp_cmd():cmd("mbp") {} - char const * get_usage() const override { return ""; } + char const * get_usage() const override { return " ()"; } char const * get_descr(cmd_context & ctx) const override { return "perform model based projection"; } unsigned get_arity() const override { return 2; } cmd_arg_kind next_arg_kind(cmd_context& ctx) const override { @@ -390,6 +391,52 @@ public: } }; +class mbi_cmd : public cmd { + expr* m_a; + expr* m_b; + ptr_vector m_vars; +public: + mbi_cmd():cmd("mbi") {} + 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; + 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); + qe::prop_mbi_plugin pA(sA.get()); + qe::prop_mbi_plugin pB(sB.get()); + lbool res = mbi.binary(pA, pB, vars, itp); + ctx.regular_stream() << res << " " << itp << "\n"; + } + +}; + void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(print_dimacs_cmd)); @@ -416,4 +463,5 @@ void install_dbg_cmds(cmd_context & ctx) { ctx.insert(alloc(instantiate_nested_cmd)); ctx.insert(alloc(set_next_id)); ctx.insert(alloc(mbp_cmd)); + ctx.insert(alloc(mbi_cmd)); } diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt index 2e6052382..d43db34f0 100644 --- a/src/qe/CMakeLists.txt +++ b/src/qe/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(qe qe_dl_plugin.cpp qe_lite.cpp qe_mbp.cpp + qe_mbi.cpp qe_sat_tactic.cpp qe_tactic.cpp qsat.cpp diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index eda233c14..f149af764 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -18,17 +18,22 @@ Revision History: --*/ +#include "ast/ast_util.h" +#include "solver/solver.h" +#include "qe/qe_mbi.h" + namespace qe { - euf_mbi_plugin::euf_mbi_plugin(solver* s): m_solver(s) {} + // ------------------------------- + // prop_mbi - euf_mbi_plugin::~euf_mbi_plugin() {} + prop_mbi_plugin::prop_mbi_plugin(solver* s): m_solver(s) {} - mbi_result euf_mbi_plugin::operator()( - func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override { - // really just a sketch of propositional at this point - scoped_push _sp(m_solver); + // sketch of propositional + + mbi_result prop_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { + ast_manager& m = lits.m(); lbool r = m_solver->check_sat(lits); switch (r) { case l_false: @@ -37,29 +42,77 @@ namespace qe { return mbi_unsat; case l_true: m_solver->get_model(mdl); - // update lits? to be all propositioal literals or an implicant. - // mdl will have map of all constants that we can walk over. + lits.reset(); + for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) { + func_decl* c = mdl->get_constant(i); + if (vars.contains(c)) { + if (m.is_true(mdl->get_const_interp(c))) { + lits.push_back(m.mk_const(c)); + } + else { + lits.push_back(m.mk_not(m.mk_const(c))); + } + } + } return mbi_sat; - case l_undef: + default: return mbi_undef; } } - void euf_mbi_plugin::block(expr_ref_vector const& lits) override { + void prop_mbi_plugin::block(expr_ref_vector const& lits) { + m_solver->assert_expr(mk_not(mk_and(lits))); + } + + // ------------------------------- + // euf_mbi, TBD + + euf_mbi_plugin::euf_mbi_plugin(solver* s): m(s->get_manager()), m_solver(s) {} + + mbi_result euf_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { + lbool r = m_solver->check_sat(lits); + switch (r) { + case l_false: + lits.reset(); + m_solver->get_unsat_core(lits); + return mbi_unsat; + case l_true: + m_solver->get_model(mdl); + lits.reset(); + for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) { + func_decl* c = mdl->get_constant(i); + if (vars.contains(c)) { + if (m.is_true(mdl->get_const_interp(c))) { + lits.push_back(m.mk_const(c)); + } + else { + lits.push_back(m.mk_not(m.mk_const(c))); + } + } + } + return mbi_sat; + default: + return mbi_undef; + } + } + + void euf_mbi_plugin::block(expr_ref_vector const& lits) { m_solver->assert_expr(mk_not(mk_and(lits))); } - /** + + /** -------------------------------------------------------------- * ping-pong interpolation of Gurfinkel & Vizel + * compute a binary interpolant. */ lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) { ast_manager& m = vars.get_manager(); model_ref mdl; - literal_vector lits(m); + expr_ref_vector lits(m); bool turn = true; vector itps, blocks; - ipts.push_back(expr_ref_vector(m)); - ipts.push_back(expr_ref_vector(m)); + itps.push_back(expr_ref_vector(m)); + itps.push_back(expr_ref_vector(m)); blocks.push_back(expr_ref_vector(m)); blocks.push_back(expr_ref_vector(m)); mbi_result last_res = mbi_undef; @@ -74,18 +127,20 @@ namespace qe { return l_true; } break; // continue - case mbi_unsat: - if (last_res == mbi_unsat) { + case mbi_unsat: { + if (lits.empty()) { itp = mk_and(itps[turn]); return l_false; } t2->block(lits); - expr_ref lemma(m.mk_not(mk_and(lits)), m); + expr_ref lemma(mk_not(mk_and(lits))); blocks[turn].push_back(lemma); - itps[turn].push_back(m.mk_implies(mk_and(blocks[!turn]), lemma)); + itp = m.mk_implies(mk_and(blocks[!turn]), lemma); + // TBD: compute closure over variables not in vars + itps[turn].push_back(itp); lits.reset(); // or find a prefix of lits? - next_res = mbi_undef; // hard restart. break; + } case mbi_augment: break; case mbi_undef: diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 4aad92f82..dad29167f 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -29,7 +29,8 @@ namespace qe { }; class mbi_plugin { - virtual ~mbi_plugin(); + public: + virtual ~mbi_plugin() {} /** * \brief Utility that works modulo a background state. * - vars @@ -57,8 +58,18 @@ namespace qe { virtual void block(expr_ref_vector const& lits) = 0; }; - class euf_mbi_plugin : mbi_plugin { + class prop_mbi_plugin : public mbi_plugin { solver_ref m_solver; + public: + prop_mbi_plugin(solver* s); + ~prop_mbi_plugin() override {} + mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override; + void block(expr_ref_vector const& lits) override; + }; + + class euf_mbi_plugin : public mbi_plugin { + ast_manager& m; + solver_ref m_solver; public: euf_mbi_plugin(solver* s); ~euf_mbi_plugin() override {} @@ -70,6 +81,7 @@ namespace qe { * use cases for interpolation. */ class interpolator { + public: static lbool binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp); }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0680d7bcf..8dec3335e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3067,6 +3067,41 @@ namespace smt { return m_asserted_formulas.inconsistent(); } + static bool is_valid_assumption(ast_manager & m, expr * assumption) { + expr* arg; + if (!m.is_bool(assumption)) + return false; + if (is_uninterp_const(assumption)) + return true; + if (m.is_not(assumption, arg) && is_uninterp_const(arg)) + return true; + if (!is_app(assumption)) + return false; + if (to_app(assumption)->get_num_args() == 0) + return true; + if (m.is_not(assumption, arg) && is_app(arg) && to_app(arg)->get_num_args() == 0) + return true; + return false; + } + + void context::internalize_proxies(expr_ref_vector const& asms, vector>& asm2proxy) { + for (expr* e : asms) { + if (is_valid_assumption(m_manager, e)) { + asm2proxy.push_back(std::make_pair(e, expr_ref(e, m_manager))); + } + else { + expr_ref proxy(m_manager), fml(m_manager); + proxy = m_manager.mk_fresh_const("proxy", m_manager.mk_bool_sort()); + fml = m_manager.mk_implies(proxy, e); + m_asserted_formulas.assert_expr(fml); + asm2proxy.push_back(std::make_pair(e, proxy)); + } + } + // The new assertions are of the form 'proxy => assumption' + // so clause simplification is sound even as these are removed after pop_scope. + internalize_assertions(); + } + void context::internalize_assertions() { if (get_cancel_flag()) return; TRACE("internalize_assertions", tout << "internalize_assertions()...\n";); @@ -3102,23 +3137,6 @@ namespace smt { TRACE("after_internalize_assertions", display(tout);); } - bool is_valid_assumption(ast_manager & m, expr * assumption) { - expr* arg; - if (!m.is_bool(assumption)) - return false; - if (is_uninterp_const(assumption)) - return true; - if (m.is_not(assumption, arg) && is_uninterp_const(arg)) - return true; - if (!is_app(assumption)) - return false; - if (to_app(assumption)->get_num_args() == 0) - return true; - if (m.is_not(assumption, arg) && is_app(arg) && to_app(arg)->get_num_args() == 0) - return true; - return false; - } - /** \brief Assumptions must be uninterpreted boolean constants (aka propositional variables). */ @@ -3205,17 +3223,21 @@ namespace smt { if (get_cancel_flag()) return; push_scope(); - for (expr * curr_assumption : asms) { + vector> asm2proxy; + internalize_proxies(asms, asm2proxy); + for (auto const& p: asm2proxy) { + expr_ref curr_assumption = p.second; + expr* orig_assumption = p.first; if (m_manager.is_true(curr_assumption)) continue; SASSERT(is_valid_assumption(m_manager, curr_assumption)); proof * pr = m_manager.mk_asserted(curr_assumption); internalize_assertion(curr_assumption, pr, 0); literal l = get_literal(curr_assumption); - m_literal2assumption.insert(l.index(), curr_assumption); + m_literal2assumption.insert(l.index(), orig_assumption); // mark_as_relevant(l); <<< not needed // internalize_assertion marked l as relevant. SASSERT(is_relevant(l)); - TRACE("assumptions", tout << l << ":" << mk_pp(curr_assumption, m_manager) << "\n";); + TRACE("assumptions", tout << l << ":" << curr_assumption << " " << mk_pp(orig_assumption, m_manager) << "\n";); if (m_manager.proofs_enabled()) assign(l, mk_justification(justification_proof_wrapper(*this, pr))); else @@ -3386,7 +3408,7 @@ namespace smt { setup_context(false); expr_ref_vector asms(m_manager, num_assumptions, assumptions); if (!already_did_theory_assumptions) add_theory_assumptions(asms); - if (!validate_assumptions(asms)) return l_undef; + // introducing proxies: if (!validate_assumptions(asms)) return l_undef; TRACE("unsat_core_bug", tout << asms << "\n";); internalize_assertions(); init_assumptions(asms); @@ -3402,7 +3424,7 @@ namespace smt { setup_context(false); expr_ref_vector asms(cube); add_theory_assumptions(asms); - if (!validate_assumptions(asms)) return l_undef; + // introducing proxies: if (!validate_assumptions(asms)) return l_undef; for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; internalize_assertions(); init_assumptions(asms); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 16c1c7ac3..7e09c3be2 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1536,6 +1536,8 @@ namespace smt { void internalize_assertion(expr * n, proof * pr, unsigned generation); + void internalize_proxies(expr_ref_vector const& asms, vector>& asm2proxy); + void internalize_instance(expr * body, proof * pr, unsigned generation) { internalize_assertion(body, pr, generation); if (relevancy())