mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-09 10:18:18 -07:00 • committed by Arie Gurfinkel
parent 688cf79619
commit 0784074b67
3 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -429,6 +429,8 @@ public:
params_ref p; params_ref p;
solver_ref sA = sf(m, p, false /* no proofs */, true, true, symbol::null); 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 sB = sf(m, p, false /* no proofs */, true, true, symbol::null);
sA->assert_expr(a);
sB->assert_expr(b);
qe::prop_mbi_plugin pA(sA.get()); qe::prop_mbi_plugin pA(sA.get());
qe::prop_mbi_plugin pB(sB.get()); qe::prop_mbi_plugin pB(sB.get());
lbool res = mbi.binary(pA, pB, vars, itp); lbool res = mbi.binary(pA, pB, vars, itp);

7
src/qe/qe_mbi.cpp
View file

@ -104,6 +104,7 @@ namespace qe {
/** -------------------------------------------------------------- /** --------------------------------------------------------------
* ping-pong interpolation of Gurfinkel & Vizel * ping-pong interpolation of Gurfinkel & Vizel
* compute a binary interpolant. * compute a binary interpolant.
* TBD: also implement the one-sided versions that create clausal interpolants.
*/ */
lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) { lbool interpolator::binary(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) {
ast_manager& m = vars.get_manager(); ast_manager& m = vars.get_manager();
@ -126,14 +127,18 @@ namespace qe {
itp = nullptr; itp = nullptr;
return l_true; return l_true;
} }
TRACE("mbi", tout << "new lits " << lits << "\n";);
break; // continue break; // continue
case mbi_unsat: { case mbi_unsat: {
if (lits.empty()) { if (lits.empty()) {
itp = mk_and(itps[turn]); // TBD, either a => itp and itp => !b
// or b => itp and itp => !a
itp = mk_and(itps[!turn]);
return l_false; return l_false;
} }
t2->block(lits); t2->block(lits);
expr_ref lemma(mk_not(mk_and(lits))); expr_ref lemma(mk_not(mk_and(lits)));
TRACE("mbi", tout << lemma << "\n";);
blocks[turn].push_back(lemma); blocks[turn].push_back(lemma);
itp = 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 // TBD: compute closure over variables not in vars

2
src/smt/smt_context.cpp
View file

@ -3061,7 +3061,7 @@ namespace smt {
bool context::reduce_assertions() { bool context::reduce_assertions() {
if (!m_asserted_formulas.inconsistent()) { if (!m_asserted_formulas.inconsistent()) {
SASSERT(at_base_level()); // SASSERT(at_base_level());
m_asserted_formulas.reduce(); m_asserted_formulas.reduce();
} }
return m_asserted_formulas.inconsistent(); return m_asserted_formulas.inconsistent();