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

update coding style to C++11

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-28 19:17:32 +02:00
parent 44100a3a08
commit 6d71d9e816
1 changed files with 20 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/tactic/arith/fm_tactic.cpp
View file

@ -197,23 +197,21 @@ class fm_tactic : public tactic {
bool has_lower = false; bool has_lower = false;
bool has_upper = false; bool has_upper = false;
TRACE("fm_mc", tout << "processing " << x->get_name() << "\n";); TRACE("fm_mc", tout << "processing " << x->get_name() << "\n";);
clauses::iterator it = m_clauses[i].begin(); for (expr* cl : m_clauses[i]) {
clauses::iterator end = m_clauses[i].end();
for (; it != end; ++it) {
if (!m.inc()) if (!m.inc())
throw tactic_exception(m.limit().get_cancel_msg()); throw tactic_exception(m.limit().get_cancel_msg());
switch (process(x, *it, u, *md, val)) { switch (process(x, cl, u, *md, val)) {
case NONE: case NONE:
TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";); TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(cl, m) << "\n";);
break; break;
case LOWER: case LOWER:
TRACE("fm_mc", tout << "lower bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";); TRACE("fm_mc", tout << "lower bound: " << val << " for:\n" << mk_ismt2_pp(cl, m) << "\n";);
if (!has_lower || val > lower) if (!has_lower || val > lower)
lower = val; lower = val;
has_lower = true; has_lower = true;
break; break;
case UPPER: case UPPER:
TRACE("fm_mc", tout << "upper bound: " << val << " for:\n" << mk_ismt2_pp(*it, m) << "\n";); TRACE("fm_mc", tout << "upper bound: " << val << " for:\n" << mk_ismt2_pp(cl, m) << "\n";);
if (!has_upper || val < upper) if (!has_upper || val < upper)
upper = val; upper = val;
has_upper = true; has_upper = true;
@ -1168,18 +1166,12 @@ class fm_tactic : public tactic {
} }
// x_cost_lt is not a total order on variables // x_cost_lt is not a total order on variables
std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int)); std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
TRACE("fm", TRACE("fm",
svector<x_cost>::iterator it2 = x_cost_vector.begin(); for (auto const& [v,c] : x_cost_vector)
svector<x_cost>::iterator end2 = x_cost_vector.end(); tout << "(" << mk_ismt2_pp(m_var2expr.get(v), m) << " " << c << ") ";
for (; it2 != end2; ++it2) {
tout << "(" << mk_ismt2_pp(m_var2expr.get(it2->first), m) << " " << it2->second << ") ";
}
tout << "\n";); tout << "\n";);
svector<x_cost>::iterator it2 = x_cost_vector.begin(); for (auto const& [v, c] : x_cost_vector)
svector<x_cost>::iterator end2 = x_cost_vector.end(); xs.push_back(v);
for (; it2 != end2; ++it2) {
xs.push_back(it2->first);
}
} }
void cleanup_constraints(constraints & cs) { void cleanup_constraints(constraints & cs) {
@ -1215,11 +1207,9 @@ class fm_tactic : public tactic {
void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const { void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const {
all_int = true; all_int = true;
unit_coeff = true; unit_coeff = true;
constraints::const_iterator it = cs.begin(); for (auto const * c : cs) {
constraints::const_iterator end = cs.end();
for (; it != end; ++it) {
bool curr_unit_coeff; bool curr_unit_coeff;
analyze(*(*it), x, all_int, curr_unit_coeff); analyze(*c, x, all_int, curr_unit_coeff);
if (!all_int) if (!all_int)
return; return;
if (!curr_unit_coeff) if (!curr_unit_coeff)
@ -1243,12 +1233,8 @@ class fm_tactic : public tactic {
} }
void copy_constraints(constraints const & s, clauses & t) { void copy_constraints(constraints const & s, clauses & t) {
constraints::const_iterator it = s.begin(); for (auto const* cp : s)
constraints::const_iterator end = s.end(); t.push_back(to_expr(*cp));
for (; it != end; ++it) {
app * c = to_expr(*(*it));
t.push_back(c);
}
} }
clauses tmp_clauses; clauses tmp_clauses;
@ -1262,10 +1248,8 @@ class fm_tactic : public tactic {
} }
void mark_constraints_dead(constraints const & cs) { void mark_constraints_dead(constraints const & cs) {
constraints::const_iterator it = cs.begin(); for (auto* cp : cs)
constraints::const_iterator end = cs.end(); cp->m_dead = true;
for (; it != end; ++it)
(*it)->m_dead = true;
} }
void mark_constraints_dead(var x) { void mark_constraints_dead(var x) {
@ -1514,14 +1498,8 @@ class fm_tactic : public tactic {
} }
void copy_remaining(vector<constraints> & v2cs) { void copy_remaining(vector<constraints> & v2cs) {
vector<constraints>::iterator it = v2cs.begin(); for (constraints& cs : v2cs) {
vector<constraints>::iterator end = v2cs.end(); for (constraint* c : cs) {
for (; it != end; ++it) {
constraints & cs = *it;
constraints::iterator it2 = cs.begin();
constraints::iterator end2 = cs.end();
for (; it2 != end2; ++it2) {
constraint * c = *it2;
if (!c->m_dead) { if (!c->m_dead) {
c->m_dead = true; c->m_dead = true;
expr * new_f = to_expr(*c); expr * new_f = to_expr(*c);
@ -1604,11 +1582,9 @@ class fm_tactic : public tactic {
} }
void display_constraints(std::ostream & out, constraints const & cs) const { void display_constraints(std::ostream & out, constraints const & cs) const {
constraints::const_iterator it = cs.begin(); for (auto const* cp : cs) {
constraints::const_iterator end = cs.end();
for (; it != end; ++it) {
out << " "; out << " ";
display(out, *(*it)); display(out, *cp);
out << "\n"; out << "\n";
} }
} }