mirror of
https://github.com/Z3Prover/z3
synced 2025-10-08 00:41:56 +00:00
fixing the order
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
542e015550
commit
aa5645b54b
1 changed files with 9 additions and 6 deletions
|
@ -566,7 +566,8 @@ struct nnf::imp {
|
|||
expr * _then = rs[2];
|
||||
expr * _else = rs[3];
|
||||
|
||||
app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else));
|
||||
expr* a = m.mk_or(_not_cond, _then);
|
||||
app * r = m.mk_and(a, m.mk_or(_cond, _else));
|
||||
m_result_stack.shrink(fr.m_spos);
|
||||
m_result_stack.push_back(r);
|
||||
if (proofs_enabled()) {
|
||||
|
@ -612,11 +613,13 @@ struct nnf::imp {
|
|||
|
||||
app * r;
|
||||
if (is_eq(t) == fr.m_pol) {
|
||||
auto a = m.mk_or(not_lhs, rhs);
|
||||
expr* a = m.mk_or(not_lhs, rhs);
|
||||
r = m.mk_and(a, m.mk_or(lhs, not_rhs));
|
||||
}
|
||||
else
|
||||
r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs));
|
||||
else {
|
||||
expr* a = m.mk_or(lhs, rhs);
|
||||
r = m.mk_and(a, m.mk_or(not_lhs, not_rhs));
|
||||
}
|
||||
m_result_stack.shrink(fr.m_spos);
|
||||
m_result_stack.push_back(r);
|
||||
if (proofs_enabled()) {
|
||||
|
@ -688,8 +691,8 @@ struct nnf::imp {
|
|||
if (proofs_enabled()) {
|
||||
expr_ref aux(m);
|
||||
aux = m.mk_label(true, names.size(), names.data(), arg);
|
||||
pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)),
|
||||
m.mk_iff_oeq(m.mk_rewrite(aux, r)));
|
||||
auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux));
|
||||
pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r)));
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue