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

restore move_non_basic_to_bounds

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-10-05 18:14:52 -07:00
parent b61f4ac51f
commit bf3817ef7c
4 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/core_solver_pretty_printer_def.h
View file

@ -279,10 +279,12 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print()
print_row(i); print_row(i);
} }
m_out << std::endl; m_out << std::endl;
if (m_core_solver.inf_heap().size()) { if (!m_core_solver.inf_heap().empty()) {
m_out << "inf columns: "; m_out << "inf columns: size() = " << m_core_solver.inf_heap().size() << std::endl;
print_vector(m_core_solver.inf_heap(), m_out); print_vector(m_core_solver.inf_heap(), m_out);
m_out << std::endl; m_out << std::endl;
} else {
m_out << "inf columns: none\n";
} }
} }

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

@ -181,7 +181,10 @@ namespace lp {
lp_status lar_solver::get_status() const { return m_status; } lp_status lar_solver::get_status() const { return m_status; }
void lar_solver::set_status(lp_status s) { m_status = s; } void lar_solver::set_status(lp_status s) {
TRACE("lar_solver", tout << "setting status to " << s << "\n";);
m_status = s;
}
lp_status lar_solver::find_feasible_solution() { lp_status lar_solver::find_feasible_solution() {
stats().m_make_feasible++; stats().m_make_feasible++;
@ -419,9 +422,7 @@ namespace lp {
void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) { void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
auto& lcs = m_mpq_lar_core_solver; auto& lcs = m_mpq_lar_core_solver;
bool change = false; bool change = false;
for (unsigned j : m_columns_with_changed_bounds) { for (unsigned j : lcs.m_r_nbasis) {
if (lcs.m_r_heading[j] >= 0)
continue;
if (move_non_basic_column_to_bounds(j, shift_randomly)) if (move_non_basic_column_to_bounds(j, shift_randomly))
change = true; change = true;
} }
@ -439,7 +440,7 @@ namespace lp {
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]; bool at_l = val == lcs.m_r_lower_bounds()[j];
bool at_u = !at_l && (val == lcs.m_r_upper_bounds()[j]); bool at_u = (!at_l && (val == lcs.m_r_upper_bounds()[j]));
if (!at_l && !at_u) { if (!at_l && !at_u) {
if (m_settings.random_next() % 2) if (m_settings.random_next() % 2)
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]); set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);

1
src/math/lp/lp_core_solver_base.h
View file

@ -564,6 +564,7 @@ public:
} }
void insert_column_into_inf_heap(unsigned j) { void insert_column_into_inf_heap(unsigned j) {
if (!m_inf_heap.contains(j)) { if (!m_inf_heap.contains(j)) {
m_inf_heap.reserve(j+1);
m_inf_heap.insert(j); m_inf_heap.insert(j);
TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";); TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";);
} }

2
src/util/heap.h
View file

@ -159,7 +159,7 @@ public:
} }
unsigned size() const { unsigned size() const {
return m_value2indices.size(); return m_values.size() - 1;
} }
void reserve(int s) { void reserve(int s) {