Skip to content

[code-simplifier] Simplify int_cube: remove goto, use aggregate/brace init #9874

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
NikolajBjorner wants to merge 1 commit into
base: master
Choose a base branch
from
+17 −31
Open

[code-simplifier] Simplify int_cube: remove goto, use aggregate/brace init #9874

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 17 additions & 31 deletions src/math/lp/int_cube.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,17 +179,13 @@ namespace lp {
return lra.tighten_term_bounds_by_delta(i, delta);
if (lra.column_has_upper_bound(i)) {
impq u = lra.get_upper_bound(i); // copy: add_term invalidates bound references
vector<std::pair<mpq, unsigned>> coeffs;
coeffs.push_back(std::make_pair(mpq(1), i));
coeffs.push_back(std::make_pair(delta.x, x_e));
vector<std::pair<mpq, unsigned>> coeffs = {{mpq(1), i}, {delta.x, x_e}};
unsigned s = lra.add_term(coeffs, UINT_MAX);
lra.add_var_bound(s, is_zero(u.y) ? lconstraint_kind::LE : lconstraint_kind::LT, u.x);
}
if (lra.column_has_lower_bound(i)) {
impq l = lra.get_lower_bound(i); // copy: add_term invalidates bound references
vector<std::pair<mpq, unsigned>> coeffs;
coeffs.push_back(std::make_pair(mpq(1), i));
coeffs.push_back(std::make_pair(-delta.x, x_e));
vector<std::pair<mpq, unsigned>> coeffs = {{mpq(1), i}, {-delta.x, x_e}};
unsigned s = lra.add_term(coeffs, UINT_MAX);
lra.add_var_bound(s, is_zero(l.y) ? lconstraint_kind::GE : lconstraint_kind::GT, l.x);
}
Expand All @@ -214,10 +210,7 @@ namespace lp {
const impq& v = lra.get_column_value(j);
if (v.is_int())
continue;
flip_candidate f;
f.m_j = j;
f.m_lo = floor(v);
flips.push_back(f);
flips.push_back({j, floor(v), false});
}
lra.round_to_integer_solution();
for (auto& f : flips)
Expand Down Expand Up @@ -273,14 +266,13 @@ namespace lp {
for (unsigned fi = 0; fi < flips.size(); ++fi)
flip_of_var[flips[fi].m_j] = fi;
// occurrences of the flip candidates in the bounded rows
vector<vector<std::pair<unsigned, mpq>>> occs;
occs.resize(flips.size());
vector<vector<std::pair<unsigned, mpq>>> occs(flips.size());
for (unsigned ri = 0; ri < rows.size(); ++ri) {
const lar_term& t = lra.get_term(rows[ri].m_j);
for (lar_term::ival p : t) {
auto it = flip_of_var.find(p.j());
if (it != flip_of_var.end())
occs[it->second].push_back(std::make_pair(ri, p.coeff()));
occs[it->second].push_back({ri, p.coeff()});
}
}

Expand Down Expand Up @@ -332,30 +324,24 @@ namespace lp {

impq int_cube::get_cube_delta_for_term(const lar_term& t) const {
if (t.size() == 2) {
bool seen_minus = false;
bool seen_plus = false;
for(lar_term::ival p : t) {
if (!lia.column_is_int(p.j()))
goto usual_delta;
const mpq & c = p.coeff();
if (c == one_of_type<mpq>()) {
seen_plus = true;
} else if (c == -one_of_type<mpq>()) {
seen_minus = true;
} else {
goto usual_delta;
}
bool seen_minus = false, seen_plus = false, all_ok = true;
for (lar_term::ival p : t) {
if (!lia.column_is_int(p.j())) { all_ok = false; break; }
const mpq& c = p.coeff();
if (c == one_of_type<mpq>()) seen_plus = true;
else if (c == -one_of_type<mpq>()) seen_minus = true;
else { all_ok = false; break; }
}
if (all_ok) {
if (seen_minus && seen_plus)
return zero_of_type<impq>();
return impq(0, 1);
}
if (seen_minus && seen_plus)
return zero_of_type<impq>();
return impq(0, 1);
}
usual_delta:
mpq delta = zero_of_type<mpq>();
for (lar_term::ival p : t)
if (lia.column_is_int(p.j()))
delta += abs(p.coeff());

delta *= mpq(1, 2);
return impq(delta);
}
Expand Down
Loading