mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

always call find_feasible_solution in move_nbasic_columns_to_bounds()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-04-27 15:29:09 -07:00
parent ba40a5752f
commit f8037ffda4
2 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/int_cube.cpp
View file

@ -35,6 +35,7 @@ namespace lp {
lra.push(); lra.push();
if (!tighten_terms_for_cube()) { if (!tighten_terms_for_cube()) {
lra.pop(); lra.pop();
lra.set_status(lp_status::OPTIMAL);
return lia_move::undef; return lia_move::undef;
} }
@ -42,7 +43,6 @@ namespace lp {
if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) {
TRACE("cube", tout << "cannot find a feasiblie solution";); TRACE("cube", tout << "cannot find a feasiblie solution";);
lra.pop(); lra.pop();
lra.set_status(lp_status::OPTIMAL);
lra.move_non_basic_columns_to_bounds(); lra.move_non_basic_columns_to_bounds();
// it can happen that we found an integer solution here // it can happen that we found an integer solution here
return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef; return !lra.r_basis_has_inf_int()? lia_move::sat: lia_move::undef;

8
src/math/lp/lar_solver.cpp
View file

@ -465,14 +465,9 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
lp_assert(rslv.reduced_costs_are_correct_tableau()); lp_assert(rslv.reduced_costs_are_correct_tableau());
} }
bool feasible(lp_status st) {
return st == lp_status::FEASIBLE || st == lp_status::OPTIMAL;
}
void lar_solver::move_non_basic_columns_to_bounds() { void lar_solver::move_non_basic_columns_to_bounds() {
auto & lcs = m_mpq_lar_core_solver; auto & lcs = m_mpq_lar_core_solver;
bool change = false; bool change = false;
bool feas = feasible(get_status());
for (unsigned j : lcs.m_r_nbasis) { for (unsigned j : lcs.m_r_nbasis) {
if (move_non_basic_column_to_bounds(j)) if (move_non_basic_column_to_bounds(j))
change = true; change = true;
@ -481,9 +476,8 @@ void lar_solver::move_non_basic_columns_to_bounds() {
if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change) if (settings().simplex_strategy() == simplex_strategy_enum::tableau_costs && change)
update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
if (feas && change) { if (change) {
find_feasible_solution(); find_feasible_solution();
SASSERT(feasible(get_status()));
} }
} }