Handle correctly cancelled run #5695
Conversation
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
| @@ -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) | |||
There was a problem hiding this comment.
why are you removing this?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Actually, the code seems to be correct even when some i is infeasible. Going to reverse the change related to get_freedom...
There was a problem hiding this comment.
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!
There was a problem hiding this comment.
It looks like we have some optimizations for the feasible case that are not available in general.
There was a problem hiding this comment.
at minimum add an assertion to enforce whatever contract you assume
| else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { | ||
| break; | ||
| case lp_status::CANCELLED: | ||
| case lp_status::UNBOUNDED: // do nothing in these cases |
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
Yes, it seems the right approach. I can fix it later.
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Yes. Or, lp can have a boolean function, smth like, feasible_status(lp_status), providing this abstraction.
Signed-off-by: Lev Nachmanson <[email protected]>
This reverts commit 6770ed8.
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
src/math/lp/lar_solver.cpp
Outdated
| @@ -797,7 +797,17 @@ namespace lp { | |||
| lp_assert(((stats().m_make_feasible% 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); | |||
| } | |||
|
|
|||
|
|
|||
| bool lar_solver::status_is_feasible(lp_status st) { | |||
There was a problem hiding this comment.
just call it is_feasible() and use get_status() internally.
There was a problem hiding this comment.
The use case is here:
Line 1532 in 0242566
The new code would be
if (!lp().is_feasible() || lp().has_changed_columns())
or even the has_changed_columns() really implies that the solver is not in the feasible state.
Signed-off-by: Lev Nachmanson <[email protected]>
Signed-off-by: Lev Nachmanson <[email protected]>
No description provided.