3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

sketch mbi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-08 17:03:24 -07:00 committed by Arie Gurfinkel
parent 4a2eb909bf
commit 5fc0f56281
2 changed files with 152 additions and 0 deletions

62
src/qe/qe_mbi.cpp Normal file
View file

@ -0,0 +1,62 @@
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
qe_mbi.cpp
Abstract:
Model-based interpolation utilities
Author:
Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
Revision History:
--*/
namespace qe {
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);
bool a_turn = true;
expr_ref_vector itp_a(m), itp_b(m);
mbi_result last_res = mbi_undef;
while (true) {
auto* t1 = a_turn ? &a : &b;
auto* t2 = a_turn ? &b : &a;
mbi_result next_res = (*t1)(vars, lits, mdl);
switch (next_res) {
case mbi_sat:
if (last_res == mbi_sat) {
itp = nullptr;
return l_true;
}
break; // continue
case mbi_unsat:
if (last_res == mbi_unsat) {
// TBD, extract the interpolants
// of what was blocked.
return l_false;
}
t2->block(lits);
lits.reset(); // or find a prefix of lits?
next_res = mbi_undef;
a_turn = !a_turn;
break;
case mbi_augment:
a_turn = !a_turn;
break;
case mbi_undef:
return l_undef;
}
last_res = next_res;
}
}
};

90
src/qe/qe_mbi.h Normal file
View file

@ -0,0 +1,90 @@
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
qe_mbi.h
Abstract:
Model-based interpolation utilities
Author:
Nikolaj Bjorner (nbjorner), Arie Gurfinkel 2018-6-8
Revision History:
--*/
#pragma once
namespace qe {
enum mbi_result {
mbi_sat,
mbi_unsat,
mbi_augment,
mbi_undef,
};
class mbi_plugin {
virtual ~mbi_plugin();
/**
* \brief Utility that works modulo a background state.
* - vars
* variables to preferrably project onto (other variables would require quantification to fit interpolation signature)
* - lits
* set of literals to check satisfiability with respect to.
* - mdl
* optional model for caller.
* on return:
* - mbi_sat:
* populates mdl with a satisfying state, and lits with implicant for background state.
* - mbi_unsat:
* populates lits to be inconsistent with background state.
* For all practical purposes it is a weakening of lits or even a subset of lits.
* - mbi_augment:
* populates lits with strengthening of lits (superset)
* - mbi_undef:
* inconclusive,
*/
virtual mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) = 0;
/**
* \brief Block conjunction of lits from future mbi_augment or mbi_sat.
*/
virtual void block(expr_ref_vector const& lits) = 0;
};
class euf_mbi_plugin : mbi_plugin {
solver_ref m_solver;
public:
euf_mbi_plugin(solver* s);
~euf_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;
};
/**
* use cases for interpolation.
*/
class interpolator {
static lbool binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp);
};
#if 0
TBD some other scenario, e.g., Farkas, Cute/Beautiful/maybe even Selfless
class solver_mbi_plugin : public mbi_plugin {
solver_ref m_solver;
public:
solver_mbi_plugin(solver* s);
~solver_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;
};
#endif
};