mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
debugging mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
Arie Gurfinkel
parent
e0aaf4452b
commit
ba504e4243
4 changed files with 82 additions and 17 deletions
|
|
@ -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<func_decl> m_vars;
|
||||
public:
|
||||
eufi_cmd():cmd("eufi") {}
|
||||
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(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));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue