mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #6400

Browse source 
bi-implication was treated as an atomic formula leading to incorrect projection.
This commit is contained in:
Nikolaj Bjorner 2022-10-17 11:00:21 -07:00
parent 541aba308c
commit d4885abdc0
3 changed files with 24 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -405,8 +405,18 @@ public:
if (!m.is_bool(*m_a) || !m.is_bool(*m_b)) if (!m.is_bool(*m_a) || !m.is_bool(*m_b))
throw default_exception("interpolation requires two Boolean arguments"); throw default_exception("interpolation requires two Boolean arguments");
expr_ref itp(m); expr_ref itp(m);
mbi.pogo(ctx.get_solver_factory(), *m_a, *m_b, itp); lbool r = mbi.pogo(ctx.get_solver_factory(), *m_a, *m_b, itp);
ctx.regular_stream() << itp << "\n"; switch (r) {
case l_true:
ctx.regular_stream() << "sat\n";
break;
case l_undef:
ctx.regular_stream() << "unknown\n";
break;
case l_false:
ctx.regular_stream() << itp << "\n";
break;
}
} }
}; };

24
src/qe/mbp/mbp_term_graph.cpp
View file

@ -307,9 +307,8 @@ namespace mbp {
term *term_graph::mk_term(expr *a) { term *term_graph::mk_term(expr *a) {
expr_ref e(a, m); expr_ref e(a, m);
term * t = alloc(term, e, m_app2term); term * t = alloc(term, e, m_app2term);
if (t->get_num_args() == 0 && m.is_unique_value(a)){ if (t->get_num_args() == 0 && m.is_unique_value(a))
t->mark_as_interpreted(); t->mark_as_interpreted();
}
m_terms.push_back(t); m_terms.push_back(t);
m_app2term.insert(a->get_id(), t); m_app2term.insert(a->get_id(), t);
@ -700,30 +699,23 @@ namespace mbp {
if (p1 != p2) if (p1 != p2)
res.push_back(m.mk_eq(p1, p2)); res.push_back(m.mk_eq(p1, p2));
} }
else { else
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
} }
else if (m.is_distinct(lit)) { else if (m.is_distinct(lit)) {
ptr_buffer<expr> diff; ptr_buffer<expr> diff;
for (expr* arg : *to_app(lit)) { for (expr* arg : *to_app(lit))
if (find_app(arg, p1)) { if (find_app(arg, p1))
diff.push_back(p1); diff.push_back(p1);
} if (diff.size() > 1)
}
if (diff.size() > 1) {
res.push_back(m.mk_distinct(diff.size(), diff.data())); res.push_back(m.mk_distinct(diff.size(), diff.data()));
} else
else {
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
} }
else if (find_app(lit, p1)) { else if (find_app(lit, p1))
res.push_back(p1); res.push_back(p1);
} else
else {
TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";); TRACE("qe", tout << "skipping " << mk_pp(lit, m) << "\n";);
}
} }
remove_duplicates(res); remove_duplicates(res);
TRACE("qe", tout << "literals: " << res << "\n";); TRACE("qe", tout << "literals: " << res << "\n";);

9
src/qe/qe_mbi.cpp
View file

@ -127,6 +127,7 @@ namespace qe {
mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) {
lbool r = m_solver->check_sat(lits); lbool r = m_solver->check_sat(lits);
TRACE("qe", tout << r << " " << lits << "\n");
switch (r) { switch (r) {
case l_false: case l_false:
lits.reset(); lits.reset();
@ -138,12 +139,10 @@ namespace qe {
for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) { for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) {
func_decl* c = mdl->get_constant(i); func_decl* c = mdl->get_constant(i);
if (is_shared(c)) { if (is_shared(c)) {
if (m.is_true(mdl->get_const_interp(c))) { if (m.is_true(mdl->get_const_interp(c)))
lits.push_back(m.mk_const(c)); lits.push_back(m.mk_const(c));
} else if (m.is_false(mdl->get_const_interp(c)))
else if (m.is_false(mdl->get_const_interp(c))) {
lits.push_back(m.mk_not(m.mk_const(c))); lits.push_back(m.mk_not(m.mk_const(c)));
}
} }
} }
return mbi_sat; return mbi_sat;
@ -172,7 +171,7 @@ namespace qe {
if (m_atom_set.contains(a)) { if (m_atom_set.contains(a)) {
// continue // continue
} }
else if (m.is_eq(a)) { else if (m.is_eq(a) && !m.is_iff(a)) {
m_atoms.push_back(a); m_atoms.push_back(a);
m_atom_set.insert(a); m_atom_set.insert(a);
} }