mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

align use of spaces before for/if/while

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-17 09:43:40 -07:00
parent 190428ab3f
commit 035baf7cb9
4 changed files with 28 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz/spacer/spacer_context.cpp
View file

@ -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();
}
}

6
src/muz/spacer/spacer_iuc_proof.cpp
View file

@ -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

4
src/muz/spacer/spacer_unsat_core_plugin.cpp
View file

@ -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);

29
src/muz/spacer/spacer_util.cpp
View file

@ -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)));
}