mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

Whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-10-16 17:01:09 +01:00
parent 0169417c64
commit cda03b4238
1 changed files with 47 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -40,7 +40,7 @@ enum nnf_mode {
transformation will be in skolem normal form. transformation will be in skolem normal form.
If a formula is too expensive to be put into NNF, If a formula is too expensive to be put into NNF,
then nested quantifiers and labels are renamed. then nested quantifiers and labels are renamed.
This mode is sufficient when using E-matching. This mode is sufficient when using E-matching.
*/ */
NNF_QUANT, /* A subformula is put into NNF if it contains NNF_QUANT, /* A subformula is put into NNF if it contains
@ -48,7 +48,7 @@ enum nnf_mode {
quantifier. The result of the transformation will be quantifier. The result of the transformation will be
in skolem normal form, and the body of quantifiers in skolem normal form, and the body of quantifiers
will be in NNF. If a ground formula is too expensive to will be in NNF. If a ground formula is too expensive to
be put into NNF, then nested quantifiers and labels be put into NNF, then nested quantifiers and labels
are renamed. are renamed.
This mode is sufficient when using Superposition This mode is sufficient when using Superposition
@ -89,7 +89,7 @@ class skolemizer {
} }
TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";); TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";);
expr_ref_vector substitution(m()); expr_ref_vector substitution(m());
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
for (unsigned i = num_decls; i > 0; ) { for (unsigned i = num_decls; i > 0; ) {
@ -111,7 +111,7 @@ class skolemizer {
substitution.push_back(0); substitution.push_back(0);
} }
// //
// (VAR num_decls) ... (VAR num_decls+sz-1) // (VAR num_decls) ... (VAR num_decls+sz-1)
// are in positions num_decls .. num_decls+sz-1 // are in positions num_decls .. num_decls+sz-1
// //
std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size());
@ -139,7 +139,7 @@ class skolemizer {
s(body, substitution.size(), substitution.c_ptr(), r); s(body, substitution.size(), substitution.c_ptr(), r);
p = 0; p = 0;
if (m().proofs_enabled()) { if (m().proofs_enabled()) {
if (q->is_forall()) if (q->is_forall())
p = m().mk_skolemization(m().mk_not(q), m().mk_not(r)); p = m().mk_skolemization(m().mk_not(q), m().mk_not(r));
else else
p = m().mk_skolemization(q, r); p = m().mk_skolemization(q, r);
@ -175,7 +175,7 @@ public:
m_cache_pr.insert(q, p); m_cache_pr.insert(q, p);
} }
} }
bool is_sk_hack(expr * p) const { bool is_sk_hack(expr * p) const {
SASSERT(m().is_pattern(p)); SASSERT(m().is_pattern(p));
if (to_app(p)->get_num_args() != 1) if (to_app(p)->get_num_args() != 1)
@ -204,7 +204,7 @@ struct nnf::imp {
unsigned m_i:28; unsigned m_i:28;
unsigned m_pol:1; // pos/neg polarity unsigned m_pol:1; // pos/neg polarity
unsigned m_in_q:1; // true if m_curr is nested in a quantifier unsigned m_in_q:1; // true if m_curr is nested in a quantifier
unsigned m_new_child:1; unsigned m_new_child:1;
unsigned m_cache_result:1; unsigned m_cache_result:1;
unsigned m_spos; // top of the result stack, when the frame was created. unsigned m_spos; // top of the result stack, when the frame was created.
frame(expr_ref&& n, bool pol, bool in_q, bool cache_res, unsigned spos): frame(expr_ref&& n, bool pol, bool in_q, bool cache_res, unsigned spos):
@ -223,22 +223,22 @@ struct nnf::imp {
#define POS_NQ_CIDX 1 // positive polarity and not nested in a quantifier #define POS_NQ_CIDX 1 // positive polarity and not nested in a quantifier
#define NEG_Q_CIDX 2 // negative polarity and nested in a quantifier #define NEG_Q_CIDX 2 // negative polarity and nested in a quantifier
#define POS_Q_CIDX 3 // positive polarity and nested in a quantifier #define POS_Q_CIDX 3 // positive polarity and nested in a quantifier
ast_manager & m_manager; ast_manager & m_manager;
vector<frame> m_frame_stack; vector<frame> m_frame_stack;
expr_ref_vector m_result_stack; expr_ref_vector m_result_stack;
typedef act_cache cache; typedef act_cache cache;
cache * m_cache[4]; cache * m_cache[4];
expr_ref_vector m_todo_defs; expr_ref_vector m_todo_defs;
proof_ref_vector m_todo_proofs; proof_ref_vector m_todo_proofs;
// proof generation goodness ---- // proof generation goodness ----
proof_ref_vector m_result_pr_stack; proof_ref_vector m_result_pr_stack;
cache * m_cache_pr[4]; cache * m_cache_pr[4];
// ------------------------------ // ------------------------------
skolemizer m_skolemizer; skolemizer m_skolemizer;
// configuration ---------------- // configuration ----------------
@ -249,7 +249,7 @@ struct nnf::imp {
name_exprs * m_name_nested_formulas; name_exprs * m_name_nested_formulas;
name_exprs * m_name_quant; name_exprs * m_name_quant;
unsigned long long m_max_memory; // in bytes unsigned long long m_max_memory; // in bytes
imp(ast_manager & m, defined_names & n, params_ref const & p): imp(ast_manager & m, defined_names & n, params_ref const & p):
@ -292,9 +292,9 @@ struct nnf::imp {
m_mode = NNF_FULL; m_mode = NNF_FULL;
else if (mode_sym == "quantifiers") else if (mode_sym == "quantifiers")
m_mode = NNF_QUANT; m_mode = NNF_QUANT;
else else
throw nnf_params_exception("invalid NNF mode"); throw nnf_params_exception("invalid NNF mode");
TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";);
m_ignore_labels = p.ignore_labels(); m_ignore_labels = p.ignore_labels();
@ -327,8 +327,8 @@ struct nnf::imp {
m_frame_stack.push_back(frame({ t, m() }, pol, in_q, cache_res, m_result_stack.size())); m_frame_stack.push_back(frame({ t, m() }, pol, in_q, cache_res, m_result_stack.size()));
} }
static unsigned get_cache_idx(bool pol, bool in_q) { static unsigned get_cache_idx(bool pol, bool in_q) {
return static_cast<unsigned>(in_q) * 2 + static_cast<unsigned>(pol); return static_cast<unsigned>(in_q) * 2 + static_cast<unsigned>(pol);
} }
void cache_result(expr * t, bool pol, bool in_q, expr * v, proof * pr) { void cache_result(expr * t, bool pol, bool in_q, expr * v, proof * pr) {
@ -338,8 +338,8 @@ struct nnf::imp {
m_cache_pr[idx]->insert(t, pr); m_cache_pr[idx]->insert(t, pr);
} }
expr * get_cached(expr * t, bool pol, bool in_q) const { expr * get_cached(expr * t, bool pol, bool in_q) const {
return m_cache[get_cache_idx(pol, in_q)]->find(t); return m_cache[get_cache_idx(pol, in_q)]->find(t);
} }
proof * get_cached_pr(expr * t, bool pol, bool in_q) const { proof * get_cached_pr(expr * t, bool pol, bool in_q) const {
@ -367,12 +367,12 @@ struct nnf::imp {
return false; return false;
} }
void checkpoint() { void checkpoint() {
cooperate("nnf"); cooperate("nnf");
if (memory::get_allocation_size() > m_max_memory) if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG); throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m().canceled()) if (m().canceled())
throw nnf_exception(m().limit().get_cancel_msg()); throw nnf_exception(m().limit().get_cancel_msg());
} }
@ -381,11 +381,11 @@ struct nnf::imp {
m_frame_stack.back().m_new_child = true; m_frame_stack.back().m_new_child = true;
} }
void set_new_child_flag(expr * old_t, expr * new_t) { void set_new_child_flag(expr * old_t, expr * new_t) {
if (old_t != new_t) if (old_t != new_t)
set_new_child_flag(); set_new_child_flag();
} }
void skip(expr * t, bool pol) { void skip(expr * t, bool pol) {
expr * r = pol ? t : m().mk_not(t); expr * r = pol ? t : m().mk_not(t);
m_result_stack.push_back(r); m_result_stack.push_back(r);
@ -447,10 +447,10 @@ struct nnf::imp {
if (pol) { if (pol) {
if (old_e->get_decl() == new_e->get_decl()) if (old_e->get_decl() == new_e->get_decl())
return m().mk_oeq_congruence(old_e, new_e, num_parents, parents); return m().mk_oeq_congruence(old_e, new_e, num_parents, parents);
else else
return m().mk_nnf_pos(old_e, new_e, num_parents, parents); return m().mk_nnf_pos(old_e, new_e, num_parents, parents);
} }
else else
return m().mk_nnf_neg(old_e, new_e, num_parents, parents); return m().mk_nnf_neg(old_e, new_e, num_parents, parents);
} }
@ -467,7 +467,7 @@ struct nnf::imp {
r = m().mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos); r = m().mk_and(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
else else
r = m().mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos); r = m().mk_or(t->get_num_args(), m_result_stack.c_ptr() + fr.m_spos);
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()) {
@ -519,7 +519,7 @@ struct nnf::imp {
r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos); r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos);
else else
r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos); r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos);
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()) {
@ -553,7 +553,7 @@ struct nnf::imp {
default: default:
break; break;
} }
expr * const * rs = m_result_stack.c_ptr() + fr.m_spos; expr * const * rs = m_result_stack.c_ptr() + fr.m_spos;
expr * _cond = rs[0]; expr * _cond = rs[0];
expr * _not_cond = rs[1]; expr * _not_cond = rs[1];
@ -573,7 +573,7 @@ struct nnf::imp {
} }
bool is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); } bool is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); }
bool process_iff_xor(app * t, frame & fr) { bool process_iff_xor(app * t, frame & fr) {
SASSERT(t->get_num_args() == 2); SASSERT(t->get_num_args() == 2);
switch (fr.m_i) { switch (fr.m_i) {
@ -604,7 +604,7 @@ struct nnf::imp {
expr * not_rhs = rs[3]; expr * not_rhs = rs[3];
app * r; app * r;
if (is_eq(t) == fr.m_pol) if (is_eq(t) == fr.m_pol)
r = m().mk_and(m().mk_or(not_lhs, rhs), m().mk_or(lhs, not_rhs)); r = m().mk_and(m().mk_or(not_lhs, rhs), m().mk_or(lhs, not_rhs));
else else
r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs)); r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs));
@ -625,7 +625,7 @@ struct nnf::imp {
else else
return process_default(t, fr); return process_default(t, fr);
} }
bool process_default(app * t, frame & fr) { bool process_default(app * t, frame & fr) {
SASSERT(fr.m_i == 0); SASSERT(fr.m_i == 0);
if (m_mode == NNF_FULL || t->has_quantifiers() || t->has_labels()) { if (m_mode == NNF_FULL || t->has_quantifiers() || t->has_labels()) {
@ -635,10 +635,10 @@ struct nnf::imp {
m_name_nested_formulas->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); m_name_nested_formulas->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2);
else else
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 = m().mk_not(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) {
@ -665,10 +665,10 @@ struct nnf::imp {
expr * arg = m_result_stack.back(); expr * arg = m_result_stack.back();
proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
if (m_ignore_labels && !proofs_enabled()) if (m_ignore_labels && !proofs_enabled())
return true; // the result is already on the stack return true; // the result is already on the stack
buffer<symbol> names; buffer<symbol> names;
bool pos; bool pos;
m().is_label(t, pos, names); m().is_label(t, pos, names);
@ -683,7 +683,7 @@ struct nnf::imp {
pr = m().mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)), 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))); m().mk_iff_oeq(m().mk_rewrite(aux, r)));
} }
} }
else { else {
r = arg; r = arg;
if (proofs_enabled()) { if (proofs_enabled()) {
@ -691,7 +691,7 @@ struct nnf::imp {
pr = m().mk_transitivity(p1, arg_pr); pr = m().mk_transitivity(p1, arg_pr);
} }
} }
m_result_stack.pop_back(); m_result_stack.pop_back();
m_result_stack.push_back(r); m_result_stack.push_back(r);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -728,7 +728,7 @@ struct nnf::imp {
if (m().is_label(t)) { if (m().is_label(t)) {
return process_label(t, fr); return process_label(t, fr);
} }
return process_default(t, fr); return process_default(t, fr);
} }
@ -736,7 +736,7 @@ struct nnf::imp {
skip(v, fr.m_pol); skip(v, fr.m_pol);
return true; return true;
} }
bool process_quantifier(quantifier * q, frame & fr) { bool process_quantifier(quantifier * q, frame & fr) {
expr_ref r(m()); expr_ref r(m());
proof_ref pr(m()); proof_ref pr(m());
@ -756,7 +756,7 @@ struct nnf::imp {
if (q->is_forall() == fr.m_pol || !m_skolemize) { if (q->is_forall() == fr.m_pol || !m_skolemize) {
expr * new_expr = m_result_stack.back(); expr * new_expr = m_result_stack.back();
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
ptr_buffer<expr> new_patterns; ptr_buffer<expr> new_patterns;
if (q->is_forall() == fr.m_pol) { if (q->is_forall() == fr.m_pol) {
@ -772,7 +772,7 @@ struct nnf::imp {
// New quantifier has existential force. // New quantifier has existential force.
// So, ignore patterns // So, ignore patterns
} }
quantifier * new_q = 0; quantifier * new_q = 0;
proof * new_q_pr = 0; proof * new_q_pr = 0;
if (fr.m_pol) { if (fr.m_pol) {
@ -785,7 +785,7 @@ struct nnf::imp {
if (proofs_enabled()) if (proofs_enabled())
new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr); new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr);
} }
m_result_stack.pop_back(); m_result_stack.pop_back();
m_result_stack.push_back(new_q); m_result_stack.push_back(new_q);
if (proofs_enabled()) { if (proofs_enabled()) {
@ -808,7 +808,7 @@ struct nnf::imp {
} }
return true; return true;
} }
void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) { void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) {
// recover result from the top of the stack. // recover result from the top of the stack.
result = m_result_stack.back(); result = m_result_stack.back();
@ -872,7 +872,7 @@ struct nnf::imp {
process(n, r, pr); process(n, r, pr);
unsigned old_sz1 = new_defs.size(); unsigned old_sz1 = new_defs.size();
unsigned old_sz2 = new_def_proofs.size(); unsigned old_sz2 = new_def_proofs.size();
for (unsigned i = 0; i < m_todo_defs.size(); i++) { for (unsigned i = 0; i < m_todo_defs.size(); i++) {
expr_ref dr(m()); expr_ref dr(m());
proof_ref dpr(m()); proof_ref dpr(m());
@ -880,7 +880,7 @@ struct nnf::imp {
new_defs.push_back(dr); new_defs.push_back(dr);
if (proofs_enabled()) { if (proofs_enabled()) {
proof * new_pr = m().mk_modus_ponens(m_todo_proofs.get(i), dpr); proof * new_pr = m().mk_modus_ponens(m_todo_proofs.get(i), dpr);
new_def_proofs.push_back(new_pr); new_def_proofs.push_back(new_pr);
} }
} }
std::reverse(new_defs.c_ptr() + old_sz1, new_defs.c_ptr() + new_defs.size()); std::reverse(new_defs.c_ptr() + old_sz1, new_defs.c_ptr() + new_defs.size());
@ -897,7 +897,7 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) {
nnf::~nnf() { nnf::~nnf() {
dealloc(m_imp); dealloc(m_imp);
} }
void nnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) { void nnf::operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
m_imp->operator()(n, new_defs, new_def_proofs, r, p); m_imp->operator()(n, new_defs, new_def_proofs, r, p);
TRACE("nnf_result", tout << mk_ismt2_pp(n, m_imp->m()) << "\nNNF result:\n" << mk_ismt2_pp(r, m_imp->m()) << "\n";); TRACE("nnf_result", tout << mk_ismt2_pp(n, m_imp->m()) << "\nNNF result:\n" << mk_ismt2_pp(r, m_imp->m()) << "\n";);