mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

A sketch of vurtego

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-13 19:33:18 -07:00
parent f0e105612c
commit a56c9faedb
2 changed files with 86 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

79
src/qe/qe_mbi.cpp
View file

@ -259,7 +259,7 @@ namespace qe {
app_ref_vector& m_vars;
arith_util arith;
obj_hashtable<func_decl> m_exclude;
is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared):
is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared):
m(vars.m()), m_vars(vars), arith(m) {
for (func_decl* f : shared) m_exclude.insert(f);
}
@ -326,7 +326,7 @@ namespace qe {
arith_util a(m);
// populate set of arithmetic variables to be projected.
app_ref_vector avars(m);
is_arith_var_proc _proc(avars, m_shared);
is_arith_var_proc _proc(avars, m_shared);
for (expr* l : lits) quick_for_each_expr(_proc, l);
TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";);
@ -457,4 +457,79 @@ namespace qe {
}
}
lbool interpolator::vurtego(mbi_plugin& a, mbi_plugin& b, expr_ref& itp, model_ref &mdl) {
/**
Assumptions on mbi_plugin()
Let local be assertions local to the plugin
Let blocked be clauses added by blocked, kept separately from local
mbi_plugin::check(lits, mdl, bool force_model):
if lits.empty() and mdl == nullptr then
if is_sat(local & blocked) then
return l_true, mbp of local, mdl of local & blocked
else
return l_false
else if !lits.empty() then
if is_sat(local & mdl & blocked)
return l_true, lits, extension of mdl to local
else if is_sat(local & lits & blocked)
if (force_model) then
return l_false, core of model, nullptr
else
return l_true, mbp of local, mdl of local & blocked
else if !is_sat(local & lits) then
return l_false, mbp of local, nullptr
else if is_sat(local & lits) && !is_sat(local & lits & blocked)
MISSING CASE. IS IT POSSIBLE?
MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
mbi_plugin::block(phi): add phi to blocked
probably should use the operator() instead of check.
mbi_augment -- means consistent with lits but not with the mdl
mbi_sat -- means consistent with lits and mdl
*/
expr_ref_vector lits(m), itps(m);
while (true) {
// when lits.empty(), this picks an A-implicant consistent with B
// when !lits.empty(), checks whether mdl of shared vocab extends to A
switch (a.check_ag(lits, mdl, !lits.empty())) {
case l_true:
if (!lits.empty())
// mdl is a model for a && b
return l_true;
switch (b.check_ag(lits, mdl, false)) {
case l_true:
/* can return true if know that b did not change
the model. For now, cycle back to A. */
SASSERT(!lits.empty());
SASSERT(mdl);
break;
case l_false:
// Force a different A-implicant
a.block(lits);
lits.reset();
mdl.reset();
break;
case l_undef:
return l_undef;
}
case l_false:
if (lits.empty()) {
// no more A-implicants, terminate
itp = mk_and(itps);
return l_false;
}
// force B to pick a different model or a different implicant
b.block(lits);
itps.push_back(mk_not(mk_and(lits)));
lits.reset();
mdl.reset();
break;
case l_undef:
return l_undef;
}
}
}
};

12
src/qe/qe_mbi.h
View file

@ -39,9 +39,9 @@ namespace qe {
/**
* Set the shared symbols.
*/
virtual void set_shared(func_decl_ref_vector const& vars) {
m_shared.reset();
m_shared.append(vars);
virtual void set_shared(func_decl_ref_vector const& vars) {
m_shared.reset();
m_shared.append(vars);
}
/**
@ -75,6 +75,11 @@ namespace qe {
*/
lbool check(expr_ref_vector& lits, model_ref& mdl);
virtual lbool check_ag(expr_ref_vector& lits, model_ref& mdl, bool force_model) {
return l_undef;
}
};
class prop_mbi_plugin : public mbi_plugin {
@ -120,6 +125,7 @@ namespace qe {
interpolator(ast_manager& m):m(m) {}
lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp);
lbool vurtego(mbi_plugin &a, mbi_plugin &b, expr_ref &itp, model_ref &mdl);
};
};