mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

use ast_util::mk_not to avoid redundant double negations during nff

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-06 11:57:46 -08:00
parent 78f9e6b31a
commit a4c2a2b22c
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -22,6 +22,7 @@ Notes:
#include "ast/normal_forms/nnf.h" #include "ast/normal_forms/nnf.h"
#include "ast/normal_forms/nnf_params.hpp" #include "ast/normal_forms/nnf_params.hpp"
#include "ast/used_vars.h" #include "ast/used_vars.h"
#include "ast/ast_util.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "ast/act_cache.h" #include "ast/act_cache.h"
#include "ast/rewriter/var_subst.h" #include "ast/rewriter/var_subst.h"
@ -137,7 +138,7 @@ class skolemizer {
if (is_sk_hack(p)) { if (is_sk_hack(p)) {
expr * sk_hack = to_app(p)->get_arg(0); expr * sk_hack = to_app(p)->get_arg(0);
if (q->get_kind() == forall_k) // check whether is in negative/positive context. if (q->get_kind() == forall_k) // check whether is in negative/positive context.
tmp = m.mk_or(body, m.mk_not(sk_hack)); // negative context tmp = m.mk_or(body, mk_not(m, sk_hack)); // negative context
else else
tmp = m.mk_and(body, sk_hack); // positive context tmp = m.mk_and(body, sk_hack); // positive context
body = tmp; body = tmp;
@ -148,7 +149,7 @@ class skolemizer {
p = nullptr; p = nullptr;
if (m_proofs_enabled) { if (m_proofs_enabled) {
if (q->get_kind() == forall_k) if (q->get_kind() == forall_k)
p = m.mk_skolemization(m.mk_not(q), m.mk_not(r)); p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
else else
p = m.mk_skolemization(q, r); p = m.mk_skolemization(q, r);
} }
@ -388,7 +389,7 @@ struct nnf::imp {
} }
void skip(expr * t, bool pol) { void skip(expr * t, bool pol) {
expr * r = pol ? t : m.mk_not(t); expr * r = pol ? t : mk_not(m, t);
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r)); m_result_pr_stack.push_back(m.mk_oeq_reflexivity(r));
@ -639,7 +640,7 @@ struct nnf::imp {
m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
if (!fr.m_pol) if (!fr.m_pol)
n2 = m.mk_not(n2); n2 = mk_not(m, n2);
m_result_stack.push_back(n2); m_result_stack.push_back(n2);
if (proofs_enabled()) { if (proofs_enabled()) {
if (!fr.m_pol) { if (!fr.m_pol) {