mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

working on mbi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-09 09:55:32 -07:00 • committed by Arie Gurfinkel
parent e6468726f5
commit 688cf79619
6 changed files with 184 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

50
src/cmd_context/extra_cmds/dbg_cmds.cpp
View file

@ -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<expr> m_vars;
public:
mbp_cmd():cmd("mbp") {}
char const * get_usage() const override { return "<expr>"; }
char const * get_usage() const override { return "<expr> (<vars>)"; }
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<func_decl> m_vars;
public:
mbi_cmd():cmd("mbi") {}
char const * get_usage() const override { return "<expr> <expr> (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));
}

1
src/qe/CMakeLists.txt
View file

@ -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

93
src/qe/qe_mbi.cpp
View file

@ -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<expr_ref_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:

16
src/qe/qe_mbi.h
View file

@ -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);
};

66
src/smt/smt_context.cpp
View file

@ -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<std::pair<expr*,expr_ref>>& 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<std::pair<expr*,expr_ref>> 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);

2
src/smt/smt_context.h
View file

@ -1536,6 +1536,8 @@ namespace smt {
void internalize_assertion(expr * n, proof * pr, unsigned generation);
void internalize_proxies(expr_ref_vector const& asms, vector<std::pair<expr*,expr_ref>>& asm2proxy);
void internalize_instance(expr * body, proof * pr, unsigned generation) {
internalize_assertion(body, pr, generation);
if (relevancy())