mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fixing the order

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-06 13:22:18 -07:00 • committed by Nikolaj Bjorner
parent 1344d8f8d7
commit 33ae08ab29
1 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/normal_forms/nnf.cpp
View file

@ -566,7 +566,8 @@ struct nnf::imp {
expr * _then = rs[2]; expr * _then = rs[2];
expr * _else = rs[3]; 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.shrink(fr.m_spos);
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -612,11 +613,13 @@ struct nnf::imp {
app * r; app * r;
if (is_eq(t) == fr.m_pol) { 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)); r = m.mk_and(a, m.mk_or(lhs, not_rhs));
} }
else else {
r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs)); 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.shrink(fr.m_spos);
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -688,8 +691,8 @@ struct nnf::imp {
if (proofs_enabled()) { if (proofs_enabled()) {
expr_ref aux(m); expr_ref aux(m);
aux = m.mk_label(true, names.size(), names.data(), arg); 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)), auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux));
m.mk_iff_oeq(m.mk_rewrite(aux, r))); pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r)));
} }
} }
else { else {