From cda03b4238852544b27a750603c4b3d4178bba8f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 16 Oct 2017 17:01:09 +0100 Subject: [PATCH] Whitespace --- src/ast/normal_forms/nnf.cpp | 94 ++++++++++++++++++------------------ 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 014568812..42b4e9350 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -40,7 +40,7 @@ enum nnf_mode { transformation will be in skolem normal form. If a formula is too expensive to be put into NNF, then nested quantifiers and labels are renamed. - + This mode is sufficient when using E-matching. */ 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 in skolem normal form, and the body of quantifiers 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. This mode is sufficient when using Superposition @@ -89,7 +89,7 @@ class skolemizer { } TRACE("skolemizer", tout << "skid: " << q->get_skid() << "\n";); - + expr_ref_vector substitution(m()); unsigned num_decls = q->get_num_decls(); for (unsigned i = num_decls; i > 0; ) { @@ -111,7 +111,7 @@ class skolemizer { 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 // std::reverse(substitution.c_ptr(), substitution.c_ptr() + substitution.size()); @@ -139,7 +139,7 @@ class skolemizer { s(body, substitution.size(), substitution.c_ptr(), r); p = 0; if (m().proofs_enabled()) { - if (q->is_forall()) + if (q->is_forall()) p = m().mk_skolemization(m().mk_not(q), m().mk_not(r)); else p = m().mk_skolemization(q, r); @@ -175,7 +175,7 @@ public: m_cache_pr.insert(q, p); } } - + bool is_sk_hack(expr * p) const { SASSERT(m().is_pattern(p)); if (to_app(p)->get_num_args() != 1) @@ -204,7 +204,7 @@ struct nnf::imp { unsigned m_i:28; unsigned m_pol:1; // pos/neg polarity 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_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): @@ -223,22 +223,22 @@ struct nnf::imp { #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 POS_Q_CIDX 3 // positive polarity and nested in a quantifier - + ast_manager & m_manager; vector m_frame_stack; expr_ref_vector m_result_stack; - + typedef act_cache cache; cache * m_cache[4]; expr_ref_vector m_todo_defs; proof_ref_vector m_todo_proofs; - + // proof generation goodness ---- proof_ref_vector m_result_pr_stack; cache * m_cache_pr[4]; // ------------------------------ - + skolemizer m_skolemizer; // configuration ---------------- @@ -249,7 +249,7 @@ struct nnf::imp { name_exprs * m_name_nested_formulas; name_exprs * m_name_quant; - + unsigned long long m_max_memory; // in bytes imp(ast_manager & m, defined_names & n, params_ref const & p): @@ -292,9 +292,9 @@ struct nnf::imp { m_mode = NNF_FULL; else if (mode_sym == "quantifiers") m_mode = NNF_QUANT; - else + else throw nnf_params_exception("invalid NNF mode"); - + TRACE("nnf", tout << "nnf-mode: " << m_mode << " " << mode_sym << "\n" << _p << "\n";); 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())); } - static unsigned get_cache_idx(bool pol, bool in_q) { - return static_cast(in_q) * 2 + static_cast(pol); + static unsigned get_cache_idx(bool pol, bool in_q) { + return static_cast(in_q) * 2 + static_cast(pol); } 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); } - expr * get_cached(expr * t, bool pol, bool in_q) const { - return m_cache[get_cache_idx(pol, in_q)]->find(t); + expr * get_cached(expr * t, bool pol, bool in_q) const { + return m_cache[get_cache_idx(pol, in_q)]->find(t); } proof * get_cached_pr(expr * t, bool pol, bool in_q) const { @@ -367,12 +367,12 @@ struct nnf::imp { return false; } - + void checkpoint() { cooperate("nnf"); if (memory::get_allocation_size() > m_max_memory) throw nnf_exception(Z3_MAX_MEMORY_MSG); - if (m().canceled()) + if (m().canceled()) throw nnf_exception(m().limit().get_cancel_msg()); } @@ -381,11 +381,11 @@ struct nnf::imp { m_frame_stack.back().m_new_child = true; } - void set_new_child_flag(expr * old_t, expr * new_t) { - if (old_t != new_t) - set_new_child_flag(); + void set_new_child_flag(expr * old_t, expr * new_t) { + if (old_t != new_t) + set_new_child_flag(); } - + void skip(expr * t, bool pol) { expr * r = pol ? t : m().mk_not(t); m_result_stack.push_back(r); @@ -447,10 +447,10 @@ struct nnf::imp { if (pol) { if (old_e->get_decl() == new_e->get_decl()) 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); } - else + else 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); else 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.push_back(r); if (proofs_enabled()) { @@ -519,7 +519,7 @@ struct nnf::imp { r = m().mk_or(2, m_result_stack.c_ptr() + fr.m_spos); else r = m().mk_and(2, m_result_stack.c_ptr() + fr.m_spos); - + m_result_stack.shrink(fr.m_spos); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -553,7 +553,7 @@ struct nnf::imp { default: break; } - + expr * const * rs = m_result_stack.c_ptr() + fr.m_spos; expr * _cond = rs[0]; 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 process_iff_xor(app * t, frame & fr) { SASSERT(t->get_num_args() == 2); switch (fr.m_i) { @@ -604,7 +604,7 @@ struct nnf::imp { expr * not_rhs = rs[3]; 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)); else r = m().mk_and(m().mk_or(lhs, rhs), m().mk_or(not_lhs, not_rhs)); @@ -625,7 +625,7 @@ struct nnf::imp { else return process_default(t, fr); } - + bool process_default(app * t, frame & fr) { SASSERT(fr.m_i == 0); 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); else m_name_quant->operator()(t, m_todo_defs, m_todo_proofs, n2, pr2); - + if (!fr.m_pol) n2 = m().mk_not(n2); - + m_result_stack.push_back(n2); if (proofs_enabled()) { if (!fr.m_pol) { @@ -665,10 +665,10 @@ struct nnf::imp { expr * arg = m_result_stack.back(); 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 - + buffer names; bool pos; 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)), m().mk_iff_oeq(m().mk_rewrite(aux, r))); } - } + } else { r = arg; if (proofs_enabled()) { @@ -691,7 +691,7 @@ struct nnf::imp { pr = m().mk_transitivity(p1, arg_pr); } } - + m_result_stack.pop_back(); m_result_stack.push_back(r); if (proofs_enabled()) { @@ -728,7 +728,7 @@ struct nnf::imp { if (m().is_label(t)) { return process_label(t, fr); } - + return process_default(t, fr); } @@ -736,7 +736,7 @@ struct nnf::imp { skip(v, fr.m_pol); return true; } - + bool process_quantifier(quantifier * q, frame & fr) { expr_ref r(m()); proof_ref pr(m()); @@ -756,7 +756,7 @@ struct nnf::imp { if (q->is_forall() == fr.m_pol || !m_skolemize) { expr * new_expr = m_result_stack.back(); proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0; - + ptr_buffer new_patterns; if (q->is_forall() == fr.m_pol) { @@ -772,7 +772,7 @@ struct nnf::imp { // New quantifier has existential force. // So, ignore patterns } - + quantifier * new_q = 0; proof * new_q_pr = 0; if (fr.m_pol) { @@ -785,7 +785,7 @@ struct nnf::imp { if (proofs_enabled()) new_q_pr = m().mk_nnf_neg(q, new_q, 1, &new_expr_pr); } - + m_result_stack.pop_back(); m_result_stack.push_back(new_q); if (proofs_enabled()) { @@ -808,7 +808,7 @@ struct nnf::imp { } return true; } - + void recover_result(expr * t, expr_ref & result, proof_ref & result_pr) { // recover result from the top of the stack. result = m_result_stack.back(); @@ -872,7 +872,7 @@ struct nnf::imp { process(n, r, pr); unsigned old_sz1 = new_defs.size(); unsigned old_sz2 = new_def_proofs.size(); - + for (unsigned i = 0; i < m_todo_defs.size(); i++) { expr_ref dr(m()); proof_ref dpr(m()); @@ -880,7 +880,7 @@ struct nnf::imp { new_defs.push_back(dr); if (proofs_enabled()) { 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()); @@ -897,7 +897,7 @@ nnf::nnf(ast_manager & m, defined_names & n, params_ref const & p) { nnf::~nnf() { 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) { 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";);