Skip to content
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

Handle correctly cancelled run #5695

Merged
merged 8 commits into from
Dec 6, 2021
Merged

Handle correctly cancelled run #5695

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
ad98c2d
remove the bound on total iterations in simplex
levnach Dec 5, 2021
6770ed8
remove unncesseray checks in get_freedom_interval_for_column()
levnach Dec 5, 2021
9c0afc4
fix the build of test-z3
levnach Dec 5, 2021
96aa2a0
Revert "remove unncesseray checks in get_freedom_interval_for_column()"
levnach Dec 5, 2021
4df76f1
optimize get_freedom_interval_for_column() for feasible case
levnach Dec 5, 2021
5519e22
add function lar_solver::status_feasible
levnach Dec 5, 2021
0ead8fe
rename status_is_feasible() to is_feasible()
levnach Dec 5, 2021
db67c91
fix the linux build
levnach Dec 6, 2021
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
6 changes: 2 additions & 4 deletions src/math/lp/int_solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -365,8 +365,6 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
m = lcm(m, denominator(a));

if (!inf_l && !inf_u) {
if (l > u)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why are you removing this?

Copy link
Contributor Author

@levnach levnach Dec 5, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It cannot happen if the column is feasible. And we assume here that it is feasible. We have l <= 0 <= u during this loop. Then we adjust l and u by shifting to xj.
I meant it cannot happen when all columns are feasible.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems to me that you are baking in some assumptions about the calling context. Maybe the current calling context is that the tableau is feasible, but this code would be easier to maintain if it doesn't rely on strong assumptions.

Copy link
Contributor Author

@levnach levnach Dec 5, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The calculation will be incorrect if at least one of the basic columns 'i ' is infeasible. The feasibility assumption is already baked in to the code as I understand it.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, the code seems to be correct even when some i is infeasible. Going to reverse the change related to get_freedom...

Copy link
Contributor Author

@levnach levnach Dec 5, 2021 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

From the other side, if we consider the infeasible case, we cannot just "continue" the loop on l==u, expecting that further on we might encounter another infeasible variable that will create l > u!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like we have some optimizations for the feasible case that are not available in general.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

at minimum add an assertion to enforce whatever contract you assume

break;
if (l == u)
continue;
}
Expand All @@ -384,7 +382,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i]));
}
}

VERIFY(l <= zero_of_type<impq>() && zero_of_type<impq>() <= u);
l += xj;
u += xj;

Expand All @@ -399,7 +397,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
tout << "val = " << get_value(j) << "\n";
tout << "return " << (inf_l || inf_u || l <= u);
);
return (inf_l || inf_u || l <= u);
return true;
}


Expand Down
12 changes: 9 additions & 3 deletions src/math/lp/lar_core_solver_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,11 +179,17 @@ void lar_core_solver::solve() {
}
lp_assert(!settings().use_tableau() || r_basis_is_OK());
}
if (m_r_solver.get_status() == lp_status::INFEASIBLE) {
switch (m_r_solver.get_status())
{
case lp_status::INFEASIBLE:
fill_not_improvable_zero_sum();
}
else if (m_r_solver.get_status() != lp_status::UNBOUNDED) {
break;
case lp_status::CANCELLED:
case lp_status::UNBOUNDED: // do nothing in these cases
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

theory_lra only checks against lp_status::OPTIMAL when deciding whether to re-check feasiblity in final_check_eh. Now UNBOUNDED would likely leak too. So shouldn't theory_lra condition the status on being feasible, where feasible is one of OPTIMAL, UNBOUNDED or so?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it seems the right approach. I can fix it later.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The question is how theory_lra handles the return codes.

Can we always assume that if the status is OPTIMAL, FEASIBLE, UNBOUNDED that all bounds are satisfied?

If so, then there are two places to change in theory_lra. It makes no assumptions about feasibility with UNBOUNDED.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes. Or, lp can have a boolean function, smth like, feasible_status(lp_status), providing this abstraction.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

yes please

break;
default: // adjust the status to optimal
m_r_solver.set_status(lp_status::OPTIMAL);
break;
}
lp_assert(r_basis_is_OK());
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
Expand Down
7 changes: 2 additions & 5 deletions src/math/lp/lp_dual_core_solver_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,10 +100,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::done() {
if (this->get_status() == lp_status::OPTIMAL) {
return true;
}
if (this->total_iterations() > this->m_settings.max_total_number_of_iterations) { // debug !!!!
this->set_status(lp_status::ITERATIONS_EXHAUSTED);
return true;
}

return false; // todo, need to be more cases
}

Expand Down Expand Up @@ -747,6 +744,6 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
one_iteration();
} while (this->get_status() != lp_status::FLOATING_POINT_ERROR && this->get_status() != lp_status::DUAL_UNBOUNDED && this->get_status() != lp_status::OPTIMAL &&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&& this->total_iterations() <= this->m_settings.max_total_number_of_iterations);
);
}
}
3 changes: 0 additions & 3 deletions src/math/lp/lp_dual_simplex_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,6 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::decide_on_status_a
break;
case lp_status::DUAL_UNBOUNDED:
lp_unreachable();
case lp_status::ITERATIONS_EXHAUSTED:
this->m_status = lp_status::ITERATIONS_EXHAUSTED;
break;
case lp_status::TIME_EXHAUSTED:
this->m_status = lp_status::TIME_EXHAUSTED;
break;
Expand Down
8 changes: 2 additions & 6 deletions src/math/lp/lp_primal_core_solver_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -956,8 +956,6 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
&&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only));

lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR
Expand Down Expand Up @@ -1097,10 +1095,8 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>::done() {
return true;
}
if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) {
this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true;
}
if (this->total_iterations() >= this->m_settings.max_total_number_of_iterations) {
this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true;
this->set_status(lp_status::CANCELLED);
return true;
}
return false;
}
Expand Down
4 changes: 1 addition & 3 deletions src/math/lp/lp_primal_core_solver_tableau_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -182,9 +182,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
if (this->m_settings.get_cancel_flag()
||
this->iters_with_no_cost_growing() > this->m_settings.max_number_of_iterations_with_no_improvements
||
this->total_iterations() > this->m_settings.max_total_number_of_iterations
) {
) {
this->set_status(lp_status::CANCELLED);
break; // from the loop
}
Expand Down
2 changes: 0 additions & 2 deletions src/math/lp/lp_settings.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,6 @@ enum class lp_status {
FEASIBLE,
FLOATING_POINT_ERROR,
TIME_EXHAUSTED,
ITERATIONS_EXHAUSTED,
EMPTY,
UNSTABLE,
CANCELLED
Expand Down Expand Up @@ -210,7 +209,6 @@ struct lp_settings {
double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros
double ignore_epsilon_of_harris { 10e-5 };
unsigned max_number_of_iterations_with_no_improvements { 2000000 };
unsigned max_total_number_of_iterations { 20000000 };
double time_limit; // the maximum time limit of the total run time in seconds
// dual section
double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein
Expand Down
2 changes: 0 additions & 2 deletions src/math/lp/lp_settings_def.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ const char* lp_status_to_string(lp_status status) {
case lp_status::FEASIBLE: return "FEASIBLE";
case lp_status::FLOATING_POINT_ERROR: return "FLOATING_POINT_ERROR";
case lp_status::TIME_EXHAUSTED: return "TIME_EXHAUSTED";
case lp_status::ITERATIONS_EXHAUSTED: return "ITERATIONS_EXHAUSTED";
case lp_status::EMPTY: return "EMPTY";
case lp_status::UNSTABLE: return "UNSTABLE";
default:
Expand All @@ -62,7 +61,6 @@ lp_status lp_status_from_string(std::string status) {
if (status == "FEASIBLE") return lp_status::FEASIBLE;
if (status == "FLOATING_POINT_ERROR") return lp_status::FLOATING_POINT_ERROR;
if (status == "TIME_EXHAUSTED") return lp_status::TIME_EXHAUSTED;
if (status == "ITERATIONS_EXHAUSTED") return lp_status::ITERATIONS_EXHAUSTED;
if (status == "EMPTY") return lp_status::EMPTY;
lp_unreachable();
return lp_status::UNKNOWN; // it is unreachable
Expand Down
8 changes: 1 addition & 7 deletions src/math/lp/lp_solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,13 +158,7 @@ class lp_solver : public column_namer {
m_settings.time_limit = time_limit_in_seconds;
}

void set_max_iterations_per_stage(unsigned max_iterations) {
m_settings.max_total_number_of_iterations = max_iterations;
}

unsigned get_max_iterations_per_stage() const {
return m_settings.max_total_number_of_iterations;
}

protected:
bool problem_is_empty();

Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_lra.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3095,7 +3095,7 @@ class theory_lra::imp {
default:
TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
// TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED,
// FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE
// FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE
return l_undef;
}
}
Expand Down
4 changes: 0 additions & 4 deletions src/test/lp/lp.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2651,10 +2651,6 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
solver->settings().presolve_with_double_solver_for_lar = true;
}

std::string iter = args_parser.get_option_value("--max_iters");
if (!iter.empty()) {
solver->settings().max_total_number_of_iterations = atoi(iter.c_str());
}
if (args_parser.option_is_used("--compare_with_primal")){
if (reader == nullptr) {
std::cout << "cannot compare with primal, the reader is null " << std::endl;
Expand Down