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

use the simple version of move_non_basic_column_to_bounds

Browse source
This commit is contained in:
Lev Nachmanson 2023-10-05 20:57:54 -07:00
parent bf3817ef7c
commit f847d039bc
5 changed files with 27 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -417,7 +417,7 @@ int gomory::find_basic_var() {
} }
lia_move gomory::operator()() { lia_move gomory::operator()() {
lra.move_non_basic_columns_to_bounds(true); lra.move_non_basic_columns_to_bounds();
int j = find_basic_var(); int j = find_basic_var();
if (j == -1) if (j == -1)
return lia_move::undef; return lia_move::undef;

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

@ -24,7 +24,7 @@ namespace lp {
int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {} int_branch::int_branch(int_solver& lia):lia(lia), lra(lia.lra) {}
lia_move int_branch::operator()() { lia_move int_branch::operator()() {
lra.move_non_basic_columns_to_bounds(true); lra.move_non_basic_columns_to_bounds();
int j = find_inf_int_base_column(); int j = find_inf_int_base_column();
return j == -1? lia_move::sat : create_branch_on_column(j); return j == -1? lia_move::sat : create_branch_on_column(j);
} }

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

@ -43,7 +43,7 @@ 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 feasible solution";); TRACE("cube", tout << "cannot find a feasible solution";);
lra.pop(); lra.pop();
lra.move_non_basic_columns_to_bounds(false); 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;
} }

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

@ -402,7 +402,7 @@ namespace lp {
void lar_solver::prepare_costs_for_r_solver(const lar_term& term) { void lar_solver::prepare_costs_for_r_solver(const lar_term& term) {
TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";); TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
move_non_basic_columns_to_bounds(false); move_non_basic_columns_to_bounds();
auto& rslv = m_mpq_lar_core_solver.m_r_solver; auto& rslv = m_mpq_lar_core_solver.m_r_solver;
lp_assert(costs_are_zeros_for_r_solver()); lp_assert(costs_are_zeros_for_r_solver());
lp_assert(reduced_costs_are_zeroes_for_r_solver()); lp_assert(reduced_costs_are_zeroes_for_r_solver());
@ -419,11 +419,11 @@ namespace lp {
lp_assert(rslv.reduced_costs_are_correct_tableau()); lp_assert(rslv.reduced_costs_are_correct_tableau());
} }
void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) { 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;
for (unsigned j : lcs.m_r_nbasis) { for (unsigned j : lcs.m_r_nbasis) {
if (move_non_basic_column_to_bounds(j, shift_randomly)) if (move_non_basic_column_to_bounds(j))
change = true; change = true;
} }
if (!change) if (!change)
@ -434,46 +434,40 @@ namespace lp {
find_feasible_solution(); find_feasible_solution();
} }
bool lar_solver::move_non_basic_column_to_bounds(unsigned j, bool force_change) { bool lar_solver::move_non_basic_column_to_bounds(unsigned j) {
auto& lcs = m_mpq_lar_core_solver; auto& lcs = m_mpq_lar_core_solver;
auto& val = lcs.m_r_x[j]; auto& val = lcs.m_r_x[j];
switch (lcs.m_column_types()[j]) { switch (lcs.m_column_types()[j]) {
case column_type::boxed: { case column_type::boxed: {
bool at_l = val == lcs.m_r_lower_bounds()[j]; const auto& l = lcs.m_r_lower_bounds()[j];
bool at_u = (!at_l && (val == lcs.m_r_upper_bounds()[j])); if (val == l || val == lcs.m_r_upper_bounds()[j]) return false;
if (!at_l && !at_u) { set_value_for_nbasic_column(j, l);
if (m_settings.random_next() % 2)
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);
else
set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]);
return true; return true;
} }
else if (force_change && m_settings.random_next() % 3 == 0) {
set_value_for_nbasic_column(j, case column_type::lower_bound: {
at_l ? lcs.m_r_upper_bounds()[j] : lcs.m_r_lower_bounds()[j]); const auto& l = lcs.m_r_lower_bounds()[j];
return true;
}
break;
}
case column_type::lower_bound:
if (val != lcs.m_r_lower_bounds()[j]) { if (val != lcs.m_r_lower_bounds()[j]) {
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]); set_value_for_nbasic_column(j, l);
return true; return true;
} }
break; return false;
}
case column_type::fixed: case column_type::fixed:
case column_type::upper_bound: case column_type::upper_bound: {
if (val != lcs.m_r_upper_bounds()[j]) { const auto & u = lcs.m_r_upper_bounds()[j];
set_value_for_nbasic_column(j, lcs.m_r_upper_bounds()[j]); if (val != u) {
set_value_for_nbasic_column(j, u);
return true; return true;
} }
break; return false;
}
case column_type::free_column: case column_type::free_column:
if (column_is_int(j) && !val.is_int()) { if (column_is_int(j) && !val.is_int()) {
set_value_for_nbasic_column(j, impq(floor(val))); set_value_for_nbasic_column(j, impq(floor(val)));
return true; return true;
} }
break; return false;
default: default:
SASSERT(false); SASSERT(false);
} }

4
src/math/lp/lar_solver.h
View file

@ -635,8 +635,8 @@ class lar_solver : public column_namer {
return *m_terms[t.id()]; return *m_terms[t.id()];
} }
lp_status find_feasible_solution(); lp_status find_feasible_solution();
void move_non_basic_columns_to_bounds(bool); void move_non_basic_columns_to_bounds();
bool move_non_basic_column_to_bounds(unsigned j, bool); bool move_non_basic_column_to_bounds(unsigned j);
inline bool r_basis_has_inf_int() const { inline bool r_basis_has_inf_int() const {
for (unsigned j : r_basis()) { for (unsigned j : r_basis()) {
if (column_is_int(j) && !column_value_is_int(j)) if (column_is_int(j) && !column_value_is_int(j))