From 035baf7cb9de60a3f0e6e2e6c29316c8ef0bb191 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Jun 2018 09:43:40 -0700 Subject: [PATCH] align use of spaces before for/if/while Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_context.cpp | 16 ++++++------ src/muz/spacer/spacer_iuc_proof.cpp | 6 ++--- src/muz/spacer/spacer_unsat_core_plugin.cpp | 4 +-- src/muz/spacer/spacer_util.cpp | 29 +++++++++++---------- 4 files changed, 28 insertions(+), 27 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 5d3ecb3fe..c926017b6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -68,7 +68,7 @@ pob::pob (pob* parent, pred_transformer& pt, m_level (level), m_depth (depth), m_open (true), m_use_farkas (true), m_weakness(0), m_blocked_lvl(0) { - if(add_to_parent && m_parent) { + if (add_to_parent && m_parent) { m_parent->add_child(*this); } } @@ -106,14 +106,14 @@ void pob::inherit(pob const &p) { } void pob::clean () { - if(m_new_post) { + if (m_new_post) { m_post = m_new_post; m_new_post.reset(); } } void pob::close () { - if(!m_open) { return; } + if (!m_open) { return; } reset (); m_open = false; @@ -537,7 +537,7 @@ void lemma::mk_cube_core() { if (!m_cube.empty()) {return;} expr_ref cube(m); if (m_pob || m_body) { - if(m_pob) {cube = m_pob->post();} + if (m_pob) {cube = m_pob->post();} else if (m_body) { // no quantifiers for now SASSERT(!is_quantifier(m_body)); @@ -637,7 +637,7 @@ void lemma::instantiate(expr * const * exprs, expr_ref &result, expr *e) { } void lemma::set_level (unsigned lvl) { - if(m_pob){m_pob->blocked_at(lvl);} + if (m_pob){m_pob->blocked_at(lvl);} m_lvl = lvl; } @@ -1920,7 +1920,7 @@ bool pred_transformer::frames::add_lemma(lemma *new_lemma) if (!new_lemma->get_bindings().empty()) { m_pt.add_lemma_core(old_lemma, true); } - if(is_infty_level(old_lemma->level())) { + if (is_infty_level(old_lemma->level())) { old_lemma->bump(); if (old_lemma->get_bumped() >= 100) { IF_VERBOSE(1, verbose_stream() << "Adding lemma to oo " @@ -3230,7 +3230,7 @@ bool context::is_reachable(pob &n) void context::dump_json() { - if(m_params.spacer_print_json().size()) { + if (m_params.spacer_print_json().size()) { std::ofstream of; of.open(m_params.spacer_print_json().bare_str()); m_json_marshaller.marshal(of); @@ -3241,7 +3241,7 @@ void context::dump_json() void context::predecessor_eh() { for (unsigned i = 0; i < m_callbacks.size(); i++) { - if(m_callbacks[i]->predecessor()) + if (m_callbacks[i]->predecessor()) m_callbacks[i]->predecessor_eh(); } } diff --git a/src/muz/spacer/spacer_iuc_proof.cpp b/src/muz/spacer/spacer_iuc_proof.cpp index 6033c744f..b6a522b76 100644 --- a/src/muz/spacer/spacer_iuc_proof.cpp +++ b/src/muz/spacer/spacer_iuc_proof.cpp @@ -137,7 +137,7 @@ void iuc_proof::compute_marks() // if current node is application of a lemma, then all // active hypotheses are removed - if(cur->get_decl_kind() == PR_LEMMA) need_to_mark_h = false; + if (cur->get_decl_kind() == PR_LEMMA) need_to_mark_h = false; // save results m_a_mark.mark(cur, need_to_mark_a); @@ -212,9 +212,9 @@ void iuc_proof::display_dot(std::ostream& out) { std::string color = "white"; if (this->is_a_marked(curr) && !this->is_b_marked(curr)) color = "red"; - else if(!this->is_a_marked(curr) && this->is_b_marked(curr)) + else if (!this->is_a_marked(curr) && this->is_b_marked(curr)) color = "blue"; - else if(this->is_a_marked(curr) && this->is_b_marked(curr) ) + else if (this->is_a_marked(curr) && this->is_b_marked(curr) ) color = "purple"; // compute node label diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index eff05762b..b96ef3037 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -240,7 +240,7 @@ namespace spacer { func_decl* d = step->get_decl(); symbol sym; - if(!m_learner.is_closed(step) && // if step is not already interpolated + if (!m_learner.is_closed(step) && // if step is not already interpolated is_farkas_lemma(m, step)) { SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); SASSERT(m.has_fact(step)); @@ -415,7 +415,7 @@ namespace spacer { } // 4. find smallest n using guess and check algorithm - for(unsigned n = 1; true; ++n) + for (unsigned n = 1; true; ++n) { params_ref p; p.set_bool("model", true); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index f63fc02d0..246410921 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -420,7 +420,7 @@ namespace { m_todo.append(a->get_num_args(), a->get_args()); } else { - for(expr* e : *a) { + for (expr* e : *a) { if (m_model.is_false(e)) { m_todo.push_back(e); break; @@ -432,7 +432,7 @@ namespace { if (!is_true) m_todo.append(a->get_num_args(), a->get_args()); else { - for(expr * e : *a) { + for (expr * e : *a) { if (m_model.is_true(e)) { m_todo.push_back(e); break; @@ -504,14 +504,15 @@ namespace { m_todo.pop_back(); process_app(a, out); m_visited.mark(a, true); - } while(!m_todo.empty()); + } + while (!m_todo.empty()); } bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) { m_visited.reset(); bool is_true = m_model.is_true(in); - for(expr* e : in) { + for (expr* e : in) { if (is_true || m_model.is_true(e)) { pick_literals(e, out); } @@ -551,7 +552,7 @@ namespace { ast_manager& m = cube.m(); scoped_no_proof _no_pf_(m); goal_ref g(alloc(goal, m, false, false, false)); - for(expr* c : cube) + for (expr* c : cube) g->assert_expr(c); goal_ref_buffer result; @@ -560,7 +561,7 @@ namespace { SASSERT(result.size() == 1); goal* r = result[0]; cube.reset(); - for(unsigned i = 0; i < r->size(); ++i) { + for (unsigned i = 0; i < r->size(); ++i) { cube.push_back(r->form(i)); } } @@ -569,7 +570,7 @@ namespace { ast_manager &m = cube.m(); scoped_no_proof _no_pf_(m); goal_ref g(alloc(goal, m, false, false, false)); - for(expr* c : cube) + for (expr* c : cube) g->assert_expr(c); goal_ref_buffer goals; @@ -582,7 +583,7 @@ namespace { g = goals[0]; cube.reset(); - for(unsigned i = 0; i < g->size(); ++i) { + for (unsigned i = 0; i < g->size(); ++i) { cube.push_back(g->form(i)); } } @@ -687,7 +688,7 @@ namespace { << mk_and(v) << "\n";); TRACE("spacer_normalize", qe::term_graph egraph(out.m()); - for(expr* e : v) egraph.add_lit(to_app(e)); + for (expr* e : v) egraph.add_lit(to_app(e)); tout << "Reduced app:\n" << mk_pp(egraph.to_app(), out.m()) << "\n";); out = mk_and(v); @@ -790,7 +791,7 @@ namespace { if (vars.size() < fv.size()) { vars.resize(fv.size()); } - for(unsigned i = 0, sz = fv.size(); i < sz; ++i) { + for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { sort *s = fv[i] ? fv[i] : m.mk_bool_sort(); vars[i] = mk_zk_const(m, i, s); var_subst vs(m, false); @@ -810,7 +811,7 @@ namespace { void operator()(app *n) { if (m_array.is_select(n) || m.is_eq(n)) { unsigned i = 0; - for(expr * arg : *n) { + for (expr * arg : *n) { if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg); ++i; } @@ -834,7 +835,7 @@ namespace { TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";); - for(expr * term : terms) { + for (expr * term : terms) { expr_ref tval(m); tval = mdl(term); @@ -871,7 +872,7 @@ namespace { tmp.reset(); unsigned j = 0; - for(app* v : vars) + for (app* v : vars) if (!mbqi_project_var(mdl, v, fml)) vars[j++] = v; vars.shrink(j); @@ -903,7 +904,7 @@ namespace { void operator()(expr* n) {} void operator()(app* n) { if (a.is_select(n)) - for(unsigned i = 1; i < n->get_num_args(); ++i) + for (unsigned i = 1; i < n->get_num_args(); ++i) if (is_app(n->get_arg(i))) m_indices.push_back(to_app(n->get_arg(i))); }