1 /*++
2 Copyright (c) 2017 Microsoft Corporation
3
4 Module Name:
5
6 <name>
7
8 Abstract:
9
10 <abstract>
11
12 Author:
13
14 Lev Nachmanson (levnach)
15
16 Revision History:
17
18
19 --*/
20 #include <set>
21 #include <string>
22 #include "util/vector.h"
23 #include "math/lp/lp_utils.h"
24 #include "math/lp/lp_core_solver_base.h"
25 namespace lp {
26
27 template <typename T, typename X> lp_core_solver_base<T, X>::
lp_core_solver_base(static_matrix<T,X> & A,vector<X> & b,vector<unsigned> & basis,vector<unsigned> & nbasis,vector<int> & heading,vector<X> & x,vector<T> & costs,lp_settings & settings,const column_namer & column_names,const vector<column_type> & column_types,const vector<X> & lower_bound_values,const vector<X> & upper_bound_values)28 lp_core_solver_base(static_matrix<T, X> & A,
29 vector<X> & b, // the right side vector
30 vector<unsigned> & basis,
31 vector<unsigned> & nbasis,
32 vector<int> & heading,
33 vector<X> & x,
34 vector<T> & costs,
35 lp_settings & settings,
36 const column_namer& column_names,
37 const vector<column_type> & column_types,
38 const vector<X> & lower_bound_values,
39 const vector<X> & upper_bound_values):
40 m_total_iterations(0),
41 m_iters_with_no_cost_growing(0),
42 m_status(lp_status::FEASIBLE),
43 m_inf_set(A.column_count()),
44 m_using_infeas_costs(false),
45 m_pivot_row_of_B_1(A.row_count()),
46 m_pivot_row(A.column_count()),
47 m_A(A),
48 m_b(b),
49 m_basis(basis),
50 m_nbasis(nbasis),
51 m_basis_heading(heading),
52 m_x(x),
53 m_costs(costs),
54 m_settings(settings),
55 m_y(m_m()),
56 m_factorization(nullptr),
57 m_column_names(column_names),
58 m_w(m_m()),
59 m_d(m_n()),
60 m_ed(m_m()),
61 m_column_types(column_types),
62 m_lower_bounds(lower_bound_values),
63 m_upper_bounds(upper_bound_values),
64 m_column_norms(m_n()),
65 m_copy_of_xB(m_m()),
66 m_basis_sort_counter(0),
67 m_steepest_edge_coefficients(A.column_count()),
68 m_tracing_basis_changes(false),
69 m_pivoted_rows(nullptr),
70 m_look_for_feasible_solution_only(false) {
71 lp_assert(bounds_for_boxed_are_set_correctly());
72 init();
73 init_basis_heading_and_non_basic_columns_vector();
74 }
75
76 template <typename T, typename X> void lp_core_solver_base<T, X>::
allocate_basis_heading()77 allocate_basis_heading() { // the rest of initialization will be handled by the factorization class
78 init_basis_heading_and_non_basic_columns_vector();
79 lp_assert(basis_heading_is_correct());
80 }
81 template <typename T, typename X> void lp_core_solver_base<T, X>::
init()82 init() {
83 allocate_basis_heading();
84 if (m_settings.use_lu())
85 init_factorization(m_factorization, m_A, m_basis, m_settings);
86 }
87
88 // i is the pivot row, and j is the pivot column
89 template <typename T, typename X> void lp_core_solver_base<T, X>::
pivot_to_reduced_costs_tableau(unsigned i,unsigned j)90 pivot_to_reduced_costs_tableau(unsigned i, unsigned j) {
91 if (j >= m_d.size())
92 return;
93 T &a = m_d[j];
94 if (is_zero(a))
95 return;
96 for (const row_cell<T> & r: m_A.m_rows[i]){
97 if (r.var() != j)
98 m_d[r.var()] -= a * r.coeff();
99 }
100 a = zero_of_type<T>(); // zero the pivot column's m_d finally
101 }
102
103
104 template <typename T, typename X> void lp_core_solver_base<T, X>::
fill_cb(T * y)105 fill_cb(T * y) const {
106 for (unsigned i = 0; i < m_m(); i++) {
107 y[i] = m_costs[m_basis[i]];
108 }
109 }
110
111
112 template <typename T, typename X> void lp_core_solver_base<T, X>::
fill_cb(vector<T> & y)113 fill_cb(vector<T> & y) const {
114 for (unsigned i = 0; i < m_m(); i++) {
115 y[i] = m_costs[m_basis[i]];
116 }
117 }
118
119 template <typename T, typename X> void lp_core_solver_base<T, X>::
solve_yB(vector<T> & y)120 solve_yB(vector<T> & y) const {
121 fill_cb(y); // now y = cB, that is the projection of costs to basis
122 m_factorization->solve_yB_with_error_check(y, m_basis);
123 }
124
125 // template <typename T, typename X> void lp_core_solver_base<T, X>::
126 // update_index_of_ed() {
127 // m_index_of_ed.clear();
128 // unsigned i = static_cast<unsigned>(m_ed.size());
129 // while (i--) {
130 // if (!is_zero(m_ed[i]))
131 // m_index_of_ed.push_back(i);
132 // }
133 // }
solve_Bd(unsigned entering,indexed_vector<T> & column)134 template <typename T, typename X> void lp_core_solver_base<T, X>::solve_Bd(unsigned entering, indexed_vector<T> & column) {
135 lp_assert(!m_settings.use_tableau());
136 if (m_factorization == nullptr) {
137 init_factorization(m_factorization, m_A, m_basis, m_settings);
138 }
139 m_factorization->solve_Bd_faster(entering, column);
140 }
141
solve_Bd(unsigned,indexed_vector<T> &,indexed_vector<T> &)142 template <typename T, typename X> void lp_core_solver_base<T, X>::solve_Bd(unsigned , indexed_vector<T>& , indexed_vector<T> &) const {
143 NOT_IMPLEMENTED_YET();
144 }
145
146 template <typename T, typename X> void lp_core_solver_base<T, X>::
solve_Bd(unsigned entering)147 solve_Bd(unsigned entering) {
148 lp_assert(m_ed.is_OK());
149 m_factorization->solve_Bd(entering, m_ed, m_w);
150 if (this->precise())
151 m_columns_nz[entering] = m_ed.m_index.size();
152 lp_assert(m_ed.is_OK());
153 lp_assert(m_w.is_OK());
154 #ifdef Z3DEBUG
155 // auto B = get_B(*m_factorization, m_basis);
156 // vector<T> a(m_m());
157 // m_A.copy_column_to_vector(entering, a);
158 // vector<T> cd(m_ed.m_data);
159 // B.apply_from_left(cd, m_settings);
160 // lp_assert(vectors_are_equal(cd , a));
161 #endif
162 }
163
164 template <typename T, typename X> void lp_core_solver_base<T, X>::
pretty_print(std::ostream & out)165 pretty_print(std::ostream & out) {
166 core_solver_pretty_printer<T, X> pp(*this, out);
167 pp.print();
168 }
169
170 template <typename T, typename X> void lp_core_solver_base<T, X>::
save_state(T * w_buffer,T * d_buffer)171 save_state(T * w_buffer, T * d_buffer) {
172 copy_m_w(w_buffer);
173 copy_m_ed(d_buffer);
174 }
175
176 template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_state(T * w_buffer,T * d_buffer)177 restore_state(T * w_buffer, T * d_buffer) {
178 restore_m_w(w_buffer);
179 restore_m_ed(d_buffer);
180 }
181
182 template <typename T, typename X> void lp_core_solver_base<T, X>::
copy_m_w(T * buffer)183 copy_m_w(T * buffer) {
184 unsigned i = m_m();
185 while (i --) {
186 buffer[i] = m_w[i];
187 }
188 }
189
190 template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_m_w(T * buffer)191 restore_m_w(T * buffer) {
192 m_w.m_index.clear();
193 unsigned i = m_m();
194 while (i--) {
195 if (!is_zero(m_w[i] = buffer[i]))
196 m_w.m_index.push_back(i);
197 }
198 }
199
200 // needed for debugging
201 template <typename T, typename X> void lp_core_solver_base<T, X>::
copy_m_ed(T * buffer)202 copy_m_ed(T * buffer) {
203 unsigned i = m_m();
204 while (i --) {
205 buffer[i] = m_ed[i];
206 }
207 }
208
209 template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_m_ed(T * buffer)210 restore_m_ed(T * buffer) {
211 unsigned i = m_m();
212 while (i --) {
213 m_ed[i] = buffer[i];
214 }
215 }
216
217 template <typename T, typename X> bool lp_core_solver_base<T, X>::
A_mult_x_is_off()218 A_mult_x_is_off() const {
219 lp_assert(m_x.size() == m_A.column_count());
220 if (numeric_traits<T>::precise()) {
221 for (unsigned i = 0; i < m_m(); i++) {
222 X delta = m_b[i] - m_A.dot_product_with_row(i, m_x);
223 if (delta != numeric_traits<X>::zero()) {
224 return true;
225 }
226 }
227 return false;
228 }
229 T feps = convert_struct<T, double>::convert(m_settings.refactor_tolerance);
230 X one = convert_struct<X, double>::convert(1.0);
231 for (unsigned i = 0; i < m_m(); i++) {
232 X delta = abs(m_b[i] - m_A.dot_product_with_row(i, m_x));
233 X eps = feps * (one + T(0.1) * abs(m_b[i]));
234
235 if (delta > eps) {
236 #if 0
237 LP_OUT(m_settings, "x is off ("
238 << "m_b[" << i << "] = " << m_b[i] << " "
239 << "left side = " << m_A.dot_product_with_row(i, m_x) << ' '
240 << "delta = " << delta << ' '
241 << "iters = " << total_iterations() << ")" << std::endl);
242 #endif
243 return true;
244 }
245 }
246 return false;
247 }
248 template <typename T, typename X> bool lp_core_solver_base<T, X>::
A_mult_x_is_off_on_index(const vector<unsigned> & index)249 A_mult_x_is_off_on_index(const vector<unsigned> & index) const {
250 lp_assert(m_x.size() == m_A.column_count());
251 if (numeric_traits<T>::precise()) return false;
252 #if RUN_A_MULT_X_IS_OFF_FOR_PRECESE
253 for (unsigned i : index) {
254 X delta = m_b[i] - m_A.dot_product_with_row(i, m_x);
255 if (delta != numeric_traits<X>::zero()) {
256 return true;
257 }
258 }
259 return false;
260 #endif
261 // todo(levnach) run on m_ed.m_index only !!!!!
262 T feps = convert_struct<T, double>::convert(m_settings.refactor_tolerance);
263 X one = convert_struct<X, double>::convert(1.0);
264 for (unsigned i : index) {
265 X delta = abs(m_b[i] - m_A.dot_product_with_row(i, m_x));
266 X eps = feps * (one + T(0.1) * abs(m_b[i]));
267
268 if (delta > eps) {
269 #if 0
270 LP_OUT(m_settings, "x is off ("
271 << "m_b[" << i << "] = " << m_b[i] << " "
272 << "left side = " << m_A.dot_product_with_row(i, m_x) << ' '
273 << "delta = " << delta << ' '
274 << "iters = " << total_iterations() << ")" << std::endl);
275 #endif
276 return true;
277 }
278 }
279 return false;
280 }
281
282 // from page 182 of Istvan Maros's book
283 template <typename T, typename X> void lp_core_solver_base<T, X>::
calculate_pivot_row_of_B_1(unsigned pivot_row)284 calculate_pivot_row_of_B_1(unsigned pivot_row) {
285 lp_assert(! use_tableau());
286 lp_assert(m_pivot_row_of_B_1.is_OK());
287 m_pivot_row_of_B_1.clear();
288 m_pivot_row_of_B_1.set_value(numeric_traits<T>::one(), pivot_row);
289 lp_assert(m_pivot_row_of_B_1.is_OK());
290 m_factorization->solve_yB_with_error_check_indexed(m_pivot_row_of_B_1, m_basis_heading, m_basis, m_settings);
291 lp_assert(m_pivot_row_of_B_1.is_OK());
292 }
293
294
295 template <typename T, typename X> void lp_core_solver_base<T, X>::
calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row)296 calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
297 m_pivot_row.clear();
298
299 for (unsigned i : m_pivot_row_of_B_1.m_index) {
300 const T & pi_1 = m_pivot_row_of_B_1[i];
301 if (numeric_traits<T>::is_zero(pi_1)) {
302 continue;
303 }
304 for (auto & c : m_A.m_rows[i]) {
305 unsigned j = c.var();
306 if (m_basis_heading[j] < 0) {
307 m_pivot_row.add_value_at_index_with_drop_tolerance(j, c.coeff() * pi_1);
308 }
309 }
310 }
311 if (precise()) {
312 m_rows_nz[pivot_row] = m_pivot_row.m_index.size();
313 }
314 }
315
316 template <typename T, typename X> void lp_core_solver_base<T, X>::
add_delta_to_entering(unsigned entering,const X & delta)317 add_delta_to_entering(unsigned entering, const X& delta) {
318 m_x[entering] += delta;
319 if (!use_tableau())
320 for (unsigned i : m_ed.m_index) {
321 if (!numeric_traits<X>::precise())
322 m_copy_of_xB[i] = m_x[m_basis[i]];
323 m_x[m_basis[i]] -= delta * m_ed[i];
324 }
325 else
326 for (const auto & c : m_A.m_columns[entering]) {
327 unsigned i = c.var();
328 m_x[m_basis[i]] -= delta * m_A.get_val(c);
329 }
330 }
331
332
333 template <typename T, typename X> void lp_core_solver_base<T, X>::
print_statistics(char const * str,X cost,std::ostream & out)334 print_statistics(char const* str, X cost, std::ostream & out) {
335 if (str!= nullptr)
336 out << str << " ";
337 out << "iterations = " << (total_iterations() - 1) << ", cost = " << T_to_string(cost)
338 << ", nonzeros = " << (m_factorization != nullptr? m_factorization->get_number_of_nonzeroes() : m_A.number_of_non_zeroes()) << std::endl;
339 }
340
341 template <typename T, typename X> bool lp_core_solver_base<T, X>::
print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream & str)342 print_statistics_with_iterations_and_check_that_the_time_is_over(std::ostream & str) {
343 unsigned total_iterations = inc_total_iterations();
344 if (m_settings.report_frequency != 0) {
345 if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
346 print_statistics("", X(), str);
347 }
348 }
349 return time_is_over();
350 }
351
352 template <typename T, typename X> bool lp_core_solver_base<T, X>::
print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const * str,std::ostream & out)353 print_statistics_with_iterations_and_nonzeroes_and_cost_and_check_that_the_time_is_over(char const* str, std::ostream & out) {
354 unsigned total_iterations = inc_total_iterations();
355 if (m_settings.report_frequency != 0)
356 if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
357 print_statistics(str, get_cost(), out);
358 }
359 return time_is_over();
360 }
361
362 template <typename T, typename X> bool lp_core_solver_base<T, X>::
print_statistics_with_cost_and_check_that_the_time_is_over(X cost,std::ostream & out)363 print_statistics_with_cost_and_check_that_the_time_is_over(X cost, std::ostream & out) {
364 unsigned total_iterations = inc_total_iterations();
365 if (m_settings.report_frequency != 0)
366 if (m_settings.print_statistics && (total_iterations % m_settings.report_frequency == 0)) {
367 print_statistics("", cost, out);
368 }
369 return time_is_over();
370 }
371
372 template <typename T, typename X> void lp_core_solver_base<T, X>::
set_non_basic_x_to_correct_bounds()373 set_non_basic_x_to_correct_bounds() {
374 for (unsigned j : non_basis()) {
375 switch (m_column_types[j]) {
376 case column_type::boxed:
377 m_x[j] = m_d[j] < 0? m_upper_bounds[j]: m_lower_bounds[j];
378 break;
379 case column_type::lower_bound:
380 m_x[j] = m_lower_bounds[j];
381 lp_assert(column_is_dual_feasible(j));
382 break;
383 case column_type::upper_bound:
384 m_x[j] = m_upper_bounds[j];
385 lp_assert(column_is_dual_feasible(j));
386 break;
387 default:
388 break;
389 }
390 }
391 }
392 template <typename T, typename X> bool lp_core_solver_base<T, X>::
column_is_dual_feasible(unsigned j)393 column_is_dual_feasible(unsigned j) const {
394 switch (m_column_types[j]) {
395 case column_type::fixed:
396 case column_type::boxed:
397 return (x_is_at_lower_bound(j) && d_is_not_negative(j)) ||
398 (x_is_at_upper_bound(j) && d_is_not_positive(j));
399 case column_type::lower_bound:
400 return x_is_at_lower_bound(j) && d_is_not_negative(j);
401 case column_type::upper_bound:
402 lp_assert(false); // impossible case
403 case column_type::free_column:
404 return numeric_traits<X>::is_zero(m_d[j]);
405 default:
406 lp_unreachable();
407 }
408 lp_unreachable();
409 return false;
410 }
411 template <typename T, typename X> bool lp_core_solver_base<T, X>::
d_is_not_negative(unsigned j)412 d_is_not_negative(unsigned j) const {
413 if (numeric_traits<T>::precise()) {
414 return m_d[j] >= numeric_traits<T>::zero();
415 }
416 return m_d[j] > -T(0.00001);
417 }
418
419 template <typename T, typename X> bool lp_core_solver_base<T, X>::
d_is_not_positive(unsigned j)420 d_is_not_positive(unsigned j) const {
421 if (numeric_traits<T>::precise()) {
422 return m_d[j] <= numeric_traits<T>::zero();
423 }
424 return m_d[j] < T(0.00001);
425 }
426
427
428 template <typename T, typename X> bool lp_core_solver_base<T, X>::
time_is_over()429 time_is_over() {
430 if (m_settings.get_cancel_flag()) {
431 m_status = lp_status::TIME_EXHAUSTED;
432 return true;
433 }
434 else {
435 return false;
436 }
437 }
438
439 template <typename T, typename X> void lp_core_solver_base<T, X>::
rs_minus_Anx(vector<X> & rs)440 rs_minus_Anx(vector<X> & rs) {
441 unsigned row = m_m();
442 while (row--) {
443 auto &rsv = rs[row] = m_b[row];
444 for (auto & it : m_A.m_rows[row]) {
445 unsigned j = it.var();
446 if (m_basis_heading[j] < 0) {
447 rsv -= m_x[j] * it.coeff();
448 }
449 }
450 }
451 }
452
453 template <typename T, typename X> bool lp_core_solver_base<T, X>::
find_x_by_solving()454 find_x_by_solving() {
455 solve_Ax_eq_b();
456 bool ret= !A_mult_x_is_off();
457 return ret;
458 }
459
column_is_feasible(unsigned j)460 template <typename T, typename X> bool lp_core_solver_base<T, X>::column_is_feasible(unsigned j) const {
461 const X& x = this->m_x[j];
462 switch (this->m_column_types[j]) {
463 case column_type::fixed:
464 case column_type::boxed:
465 if (this->above_bound(x, this->m_upper_bounds[j])) {
466 return false;
467 } else if (this->below_bound(x, this->m_lower_bounds[j])) {
468 return false;
469 } else {
470 return true;
471 }
472 break;
473 case column_type::lower_bound:
474 if (this->below_bound(x, this->m_lower_bounds[j])) {
475 return false;
476 } else {
477 return true;
478 }
479 break;
480 case column_type::upper_bound:
481 if (this->above_bound(x, this->m_upper_bounds[j])) {
482 return false;
483 } else {
484 return true;
485 }
486 break;
487 case column_type::free_column:
488 return true;
489 break;
490 default:
491 lp_unreachable();
492 }
493 return false; // it is unreachable
494 }
495
calc_current_x_is_feasible_include_non_basis()496 template <typename T, typename X> bool lp_core_solver_base<T, X>::calc_current_x_is_feasible_include_non_basis() const {
497 unsigned j = this->m_n();
498 while (j--) {
499 if (!column_is_feasible(j)) {
500 TRACE("lar_solver", tout << "infeasible column: "; print_column_info(j, tout) << "\n";);
501 return false;
502 }
503 }
504 return true;
505 }
506
inf_set_is_correct()507 template <typename T, typename X> bool lp_core_solver_base<T, X>::inf_set_is_correct() const {
508 for (unsigned j = 0; j < this->m_n(); j++) {
509 bool belongs_to_set = m_inf_set.contains(j);
510 bool is_feas = column_is_feasible(j);
511 if (is_feas == belongs_to_set) {
512 TRACE("lp_core", tout << "incorrectly set column in inf set "; print_column_info(j, tout) << "\n";);
513 return false;
514 }
515 }
516 return true;
517 }
518
519 template <typename T, typename X> bool lp_core_solver_base<T, X>::
update_basis_and_x(int entering,int leaving,X const & tt)520 update_basis_and_x(int entering, int leaving, X const & tt) {
521
522 if (!is_zero(tt)) {
523 add_delta_to_entering(entering, tt);
524 if ((!numeric_traits<T>::precise()) && A_mult_x_is_off_on_index(m_ed.m_index) && !find_x_by_solving()) {
525 init_factorization(m_factorization, m_A, m_basis, m_settings);
526 if (!find_x_by_solving()) {
527 restore_x(entering, tt);
528 if(A_mult_x_is_off()) {
529 m_status = lp_status::FLOATING_POINT_ERROR;
530 m_iters_with_no_cost_growing++;
531 return false;
532 }
533
534 init_factorization(m_factorization, m_A, m_basis, m_settings);
535 m_iters_with_no_cost_growing++;
536 if (m_factorization->get_status() != LU_status::OK) {
537 std::stringstream s;
538 // s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
539 m_status = lp_status::FLOATING_POINT_ERROR;
540 return false;
541 }
542 return false;
543 }
544 }
545 }
546
547 bool refactor = m_factorization->need_to_refactor();
548 if (!refactor) {
549 const T & pivot = this->m_pivot_row[entering]; // m_ed[m_factorization->basis_heading(leaving)] is the same but the one that we are using is more precise
550 m_factorization->replace_column(pivot, m_w, m_basis_heading[leaving]);
551 if (m_factorization->get_status() == LU_status::OK) {
552 change_basis(entering, leaving);
553 return true;
554 }
555 }
556 // need to refactor == true
557 change_basis(entering, leaving);
558 init_lu();
559 if (m_factorization->get_status() != LU_status::OK) {
560 if (m_look_for_feasible_solution_only && !precise()) {
561 m_status = lp_status::UNSTABLE;
562 delete m_factorization;
563 m_factorization = nullptr;
564 return false;
565 }
566 // LP_OUT(m_settings, "failing refactor for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations() << std::endl);
567 restore_x_and_refactor(entering, leaving, tt);
568 if (m_status == lp_status::FLOATING_POINT_ERROR)
569 return false;
570 CASSERT("A_off", !A_mult_x_is_off());
571 m_iters_with_no_cost_growing++;
572 // LP_OUT(m_settings, "rolled back after failing of init_factorization()" << std::endl);
573 m_status = lp_status::UNSTABLE;
574 return false;
575 }
576 return true;
577 }
578
579
580 template <typename T, typename X> bool lp_core_solver_base<T, X>::
divide_row_by_pivot(unsigned pivot_row,unsigned pivot_col)581 divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
582 lp_assert(numeric_traits<T>::precise());
583 int pivot_index = -1;
584 auto & row = m_A.m_rows[pivot_row];
585 unsigned size = row.size();
586 for (unsigned j = 0; j < size; j++) {
587 auto & c = row[j];
588 if (c.var() == pivot_col) {
589 pivot_index = static_cast<int>(j);
590 break;
591 }
592 }
593 if (pivot_index == -1)
594 return false;
595 auto & pivot_cell = row[pivot_index];
596 T & coeff = pivot_cell.coeff();
597 if (is_zero(coeff))
598 return false;
599
600 this->m_b[pivot_row] /= coeff;
601 for (unsigned j = 0; j < size; j++) {
602 auto & c = row[j];
603 if (c.var() != pivot_col) {
604 c.coeff() /= coeff;
605 }
606 }
607 coeff = one_of_type<T>();
608 CASSERT("check_static_matrix", m_A.is_correct());
609 return true;
610 }
611 template <typename T, typename X> bool lp_core_solver_base<T, X>::
pivot_column_tableau(unsigned j,unsigned piv_row_index)612 pivot_column_tableau(unsigned j, unsigned piv_row_index) {
613 if (!divide_row_by_pivot(piv_row_index, j))
614 return false;
615 auto &column = m_A.m_columns[j];
616 int pivot_col_cell_index = -1;
617 for (unsigned k = 0; k < column.size(); k++) {
618 if (column[k].var() == piv_row_index) {
619 pivot_col_cell_index = k;
620 break;
621 }
622 }
623 if (pivot_col_cell_index < 0)
624 return false;
625
626 if (pivot_col_cell_index != 0) {
627 lp_assert(column.size() > 1);
628 // swap the pivot column cell with the head cell
629 auto c = column[0];
630 column[0] = column[pivot_col_cell_index];
631 column[pivot_col_cell_index] = c;
632
633 m_A.m_rows[piv_row_index][column[0].offset()].offset() = 0;
634 m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
635 }
636 while (column.size() > 1) {
637 auto & c = column.back();
638 lp_assert(c.var() != piv_row_index);
639 if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
640 return false;
641 }
642 if (m_pivoted_rows!= nullptr)
643 m_pivoted_rows->insert(c.var());
644 }
645
646 if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)
647 pivot_to_reduced_costs_tableau(piv_row_index, j);
648 return true;
649 }
650
651
652 template <typename T, typename X> bool lp_core_solver_base<T, X>::
basis_has_no_doubles()653 basis_has_no_doubles() const {
654 std::set<unsigned> bm;
655 for (unsigned i = 0; i < m_m(); i++) {
656 bm.insert(m_basis[i]);
657 }
658 return bm.size() == m_m();
659 }
660
661 template <typename T, typename X> bool lp_core_solver_base<T, X>::
non_basis_has_no_doubles()662 non_basis_has_no_doubles() const {
663 std::set<int> bm;
664 for (auto j : m_nbasis) {
665 bm.insert(j);
666 }
667 return bm.size() == m_nbasis.size();
668 }
669
670 template <typename T, typename X> bool lp_core_solver_base<T, X>::
basis_is_correctly_represented_in_heading()671 basis_is_correctly_represented_in_heading() const {
672 for (unsigned i = 0; i < m_m(); i++) {
673 if (m_basis_heading[m_basis[i]] != static_cast<int>(i))
674 return false;
675 }
676 return true;
677 }
678 template <typename T, typename X> bool lp_core_solver_base<T, X>::
non_basis_is_correctly_represented_in_heading()679 non_basis_is_correctly_represented_in_heading() const {
680 for (unsigned i = 0; i < m_nbasis.size(); i++) {
681 if (m_basis_heading[m_nbasis[i]] != - static_cast<int>(i) - 1)
682 return false;
683 }
684 for (unsigned j = 0; j < m_A.column_count(); j++) {
685 if (m_basis_heading[j] >= 0) {
686 lp_assert(static_cast<unsigned>(m_basis_heading[j]) < m_A.row_count() && m_basis[m_basis_heading[j]] == j);
687 }
688 }
689 return true;
690 }
691
692 template <typename T, typename X> bool lp_core_solver_base<T, X>::
basis_heading_is_correct()693 basis_heading_is_correct() const {
694 if ( m_A.column_count() > 10 ) { // for the performance reason
695 return true;
696 }
697 lp_assert(m_basis_heading.size() == m_A.column_count());
698 lp_assert(m_basis.size() == m_A.row_count());
699 lp_assert(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller
700 if (!basis_has_no_doubles()) {
701 return false;
702 }
703
704 if (!non_basis_has_no_doubles()) {
705 return false;
706 }
707
708 if (!basis_is_correctly_represented_in_heading()) {
709 return false;
710 }
711
712 if (!non_basis_is_correctly_represented_in_heading()) {
713 return false;
714 }
715
716
717 return true;
718 }
719
720 template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_x_and_refactor(int entering,int leaving,X const & t)721 restore_x_and_refactor(int entering, int leaving, X const & t) {
722 this->restore_basis_change(entering, leaving);
723 restore_x(entering, t);
724 init_factorization(m_factorization, m_A, m_basis, m_settings);
725 if (m_factorization->get_status() == LU_status::Degenerated) {
726 LP_OUT(m_settings, "cannot refactor" << std::endl);
727 m_status = lp_status::FLOATING_POINT_ERROR;
728 return;
729 }
730 // solve_Ax_eq_b();
731 if (A_mult_x_is_off()) {
732 LP_OUT(m_settings, "cannot restore solution" << std::endl);
733 m_status = lp_status::FLOATING_POINT_ERROR;
734 return;
735 }
736 }
737
738 template <typename T, typename X> void lp_core_solver_base<T, X>::
restore_x(unsigned entering,X const & t)739 restore_x(unsigned entering, X const & t) {
740 if (is_zero(t)) return;
741 m_x[entering] -= t;
742 for (unsigned i : m_ed.m_index) {
743 m_x[m_basis[i]] = m_copy_of_xB[i];
744 }
745 }
746
747 template <typename T, typename X> void lp_core_solver_base<T, X>::
fill_reduced_costs_from_m_y_by_rows()748 fill_reduced_costs_from_m_y_by_rows() {
749 unsigned j = m_n();
750 while (j--) {
751 if (m_basis_heading[j] < 0)
752 m_d[j] = m_costs[j];
753 else
754 m_d[j] = numeric_traits<T>::zero();
755 }
756
757 unsigned i = m_m();
758 while (i--) {
759 const T & y = m_y[i];
760 if (is_zero(y)) continue;
761 for (row_cell<T> & c : m_A.m_rows[i]) {
762 j = c.var();
763 if (m_basis_heading[j] < 0) {
764 m_d[j] -= y * c.coeff();
765 }
766 }
767 }
768 }
769
770 template <typename T, typename X> void lp_core_solver_base<T, X>::
copy_rs_to_xB(vector<X> & rs)771 copy_rs_to_xB(vector<X> & rs) {
772 unsigned j = m_m();
773 while (j--) {
774 m_x[m_basis[j]] = rs[j];
775 }
776 }
777
778 template <typename T, typename X> std::string lp_core_solver_base<T, X>::
column_name(unsigned column)779 column_name(unsigned column) const {
780 return m_column_names.get_variable_name(column);
781 }
782
783 template <typename T, typename X> void lp_core_solver_base<T, X>::
copy_right_side(vector<X> & rs)784 copy_right_side(vector<X> & rs) {
785 unsigned i = m_m();
786 while (i --) {
787 rs[i] = m_b[i];
788 }
789 }
790
791 template <typename T, typename X> void lp_core_solver_base<T, X>::
add_delta_to_xB(vector<X> & del)792 add_delta_to_xB(vector<X> & del) {
793 unsigned i = m_m();
794 while (i--) {
795 this->m_x[this->m_basis[i]] -= del[i];
796 }
797 }
798
799 template <typename T, typename X> void lp_core_solver_base<T, X>::
find_error_in_BxB(vector<X> & rs)800 find_error_in_BxB(vector<X>& rs){
801 unsigned row = m_m();
802 while (row--) {
803 auto &rsv = rs[row];
804 for (auto & it : m_A.m_rows[row]) {
805 unsigned j = it.var();
806 if (m_basis_heading[j] >= 0) {
807 rsv -= m_x[j] * it.coeff();
808 }
809 }
810 }
811 }
812
813 // recalculates the projection of x to B, such that Ax = b
814 template <typename T, typename X> void lp_core_solver_base<T, X>::
solve_Ax_eq_b()815 solve_Ax_eq_b() {
816 if (numeric_traits<X>::precise()) {
817 vector<X> rs(m_m());
818 rs_minus_Anx(rs);
819 m_factorization->solve_By(rs);
820 copy_rs_to_xB(rs);
821 } else {
822 vector<X> rs(m_m());
823 rs_minus_Anx(rs);
824 vector<X> rrs = rs; // another copy of rs
825 m_factorization->solve_By(rs);
826 copy_rs_to_xB(rs);
827 find_error_in_BxB(rrs);
828 m_factorization->solve_By(rrs);
829 add_delta_to_xB(rrs);
830 }
831 }
832
833
834
835
836 template <typename T, typename X> void lp_core_solver_base<T, X>::
snap_non_basic_x_to_bound_and_free_to_zeroes()837 snap_non_basic_x_to_bound_and_free_to_zeroes() {
838 for (unsigned j : non_basis()) {
839 lp_assert(j < m_x.size());
840 switch (m_column_types[j]) {
841 case column_type::fixed:
842 case column_type::boxed:
843 case column_type::lower_bound:
844 m_x[j] = m_lower_bounds[j];
845 break;
846 case column_type::upper_bound:
847 m_x[j] = m_upper_bounds[j];
848 break;
849 default:
850 m_x[j] = zero_of_type<X>();
851 break;
852 }
853 }
854 }
855 template <typename T, typename X> void lp_core_solver_base<T, X>::
snap_xN_to_bounds_and_fill_xB()856 snap_xN_to_bounds_and_fill_xB() {
857 snap_non_basic_x_to_bound();
858 solve_Ax_eq_b();
859 }
860
861 template <typename T, typename X> void lp_core_solver_base<T, X>::
snap_xN_to_bounds_and_free_columns_to_zeroes()862 snap_xN_to_bounds_and_free_columns_to_zeroes() {
863 snap_non_basic_x_to_bound_and_free_to_zeroes();
864 solve_Ax_eq_b();
865 }
866
867 template <typename T, typename X> void lp_core_solver_base<T, X>::
init_reduced_costs_for_one_iteration()868 init_reduced_costs_for_one_iteration() {
869 solve_yB(m_y);
870 fill_reduced_costs_from_m_y_by_rows();
871 }
872
873 template <typename T, typename X> non_basic_column_value_position lp_core_solver_base<T, X>::
get_non_basic_column_value_position(unsigned j)874 get_non_basic_column_value_position(unsigned j) const {
875 switch (m_column_types[j]) {
876 case column_type::fixed:
877 return x_is_at_lower_bound(j)? at_fixed : not_at_bound;
878 case column_type::free_column:
879 return free_of_bounds;
880 case column_type::boxed:
881 return x_is_at_lower_bound(j)? at_lower_bound :(
882 x_is_at_upper_bound(j)? at_upper_bound:
883 not_at_bound
884 );
885 case column_type::lower_bound:
886 return x_is_at_lower_bound(j)? at_lower_bound : not_at_bound;
887 case column_type::upper_bound:
888 return x_is_at_upper_bound(j)? at_upper_bound : not_at_bound;
889 default:
890 lp_unreachable();
891 }
892 lp_unreachable();
893 return at_lower_bound;
894 }
895
init_lu()896 template <typename T, typename X> void lp_core_solver_base<T, X>::init_lu() {
897 init_factorization(this->m_factorization, this->m_A, this->m_basis, this->m_settings);
898 }
899
pivots_in_column_and_row_are_different(int entering,int leaving)900 template <typename T, typename X> int lp_core_solver_base<T, X>::pivots_in_column_and_row_are_different(int entering, int leaving) const {
901 const T & column_p = this->m_ed[this->m_basis_heading[leaving]];
902 const T & row_p = this->m_pivot_row[entering];
903 if (is_zero(column_p) || is_zero(row_p)) return true; // pivots cannot be zero
904 // the pivots have to have the same sign
905 if (column_p < 0) {
906 if (row_p > 0)
907 return 2;
908 } else { // column_p > 0
909 if (row_p < 0)
910 return 2;
911 }
912 T diff_normalized = abs((column_p - row_p) / (numeric_traits<T>::one() + abs(row_p)));
913 if ( !this->m_settings.abs_val_is_smaller_than_harris_tolerance(diff_normalized / T(10)))
914 return 1;
915 return 0;
916 }
transpose_rows_tableau(unsigned i,unsigned j)917 template <typename T, typename X> void lp_core_solver_base<T, X>::transpose_rows_tableau(unsigned i, unsigned j) {
918 transpose_basis(i, j);
919 m_A.transpose_rows(i, j);
920 }
921 // j is the new basic column, j_basic - the leaving column
pivot_column_general(unsigned j,unsigned j_basic,indexed_vector<T> & w)922 template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
923 lp_assert(m_basis_heading[j] < 0);
924 lp_assert(m_basis_heading[j_basic] >= 0);
925 unsigned row_index = m_basis_heading[j_basic];
926 if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) {
927 if (m_factorization->need_to_refactor()) {
928 init_lu();
929 }
930 else {
931 m_factorization->prepare_entering(j, w); // to init vector w
932 m_factorization->replace_column(zero_of_type<T>(), w, row_index);
933 }
934 if (m_factorization->get_status() != LU_status::OK) {
935 init_lu();
936 return false;
937 }
938 else {
939 change_basis(j, j_basic);
940 }
941 }
942 else { // the tableau case
943 if (pivot_column_tableau(j, row_index))
944 change_basis(j, j_basic);
945 else return false;
946 }
947 return true;
948 }
949
pivot_fixed_vars_from_basis()950 template <typename T, typename X> void lp_core_solver_base<T, X>::pivot_fixed_vars_from_basis() {
951 // run over basis and non-basis at the same time
952 indexed_vector<T> w(m_basis.size()); // the buffer
953 unsigned i = 0; // points to basis
954 for (; i < m_basis.size(); i++) {
955 unsigned basic_j = m_basis[i];
956
957 if (get_column_type(basic_j) != column_type::fixed) continue;
958 T a;
959 unsigned j;
960 for (auto &c : m_A.m_rows[i]) {
961 j = c.var();
962 if (j == basic_j)
963 continue;
964 if (get_column_type(j) != column_type::fixed) {
965 if (pivot_column_general(j, basic_j, w))
966 break;
967 }
968 }
969 }
970 }
971
remove_from_basis(unsigned basic_j)972 template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis(unsigned basic_j) {
973 indexed_vector<T> w(m_basis.size()); // the buffer
974 unsigned i = m_basis_heading[basic_j];
975 for (auto &c : m_A.m_rows[i]) {
976 if (c.var() == basic_j)
977 continue;
978 if (pivot_column_general(c.var(), basic_j, w))
979 return true;
980 }
981 return false;
982 }
983
remove_from_basis(unsigned basic_j,const impq & val)984 template <typename T, typename X> bool lp_core_solver_base<T, X>::remove_from_basis(unsigned basic_j, const impq& val) {
985 indexed_vector<T> w(m_basis.size()); // the buffer
986 unsigned i = m_basis_heading[basic_j];
987 for (auto &c : m_A.m_rows[i]) {
988 if (c.var() == basic_j)
989 continue;
990 if (pivot_column_general(c.var(), basic_j, w))
991 return true;
992 }
993 return false;
994 }
995
996
997 template <typename T, typename X> bool
infeasibility_costs_are_correct()998 lp_core_solver_base<T, X>::infeasibility_costs_are_correct() const {
999 if (! this->m_using_infeas_costs)
1000 return true;
1001 lp_assert(costs_on_nbasis_are_zeros());
1002 for (unsigned j :this->m_basis) {
1003 if (!infeasibility_cost_is_correct_for_column(j)) {
1004 TRACE("lar_solver", tout << "incorrect cost for column " << j << std::endl;);
1005 return false;
1006 }
1007 if (!is_zero(m_d[j])) {
1008 TRACE("lar_solver", tout << "non zero inf cost for basis j = " << j << std::endl;);
1009 return false;
1010 }
1011 }
1012 return true;
1013 }
1014
1015 template <typename T, typename X> bool
infeasibility_cost_is_correct_for_column(unsigned j)1016 lp_core_solver_base<T, X>::infeasibility_cost_is_correct_for_column(unsigned j) const {
1017 T r = (!this->m_settings.use_breakpoints_in_feasibility_search)? -one_of_type<T>(): one_of_type<T>();
1018
1019 switch (this->m_column_types[j]) {
1020 case column_type::fixed:
1021 case column_type::boxed:
1022 if (this->x_above_upper_bound(j)) {
1023 return (this->m_costs[j] == r);
1024 }
1025 if (this->x_below_low_bound(j)) {
1026 return (this->m_costs[j] == -r);
1027 }
1028 return is_zero(this->m_costs[j]);
1029
1030 case column_type::lower_bound:
1031 if (this->x_below_low_bound(j)) {
1032 return this->m_costs[j] == -r;
1033 }
1034 return is_zero(this->m_costs[j]);
1035
1036 case column_type::upper_bound:
1037 if (this->x_above_upper_bound(j)) {
1038 return this->m_costs[j] == r;
1039 }
1040 return is_zero(this->m_costs[j]);
1041 case column_type::free_column:
1042 return is_zero(this->m_costs[j]);
1043 default:
1044 lp_assert(false);
1045 return true;
1046 }
1047 }
1048
1049 template <typename T, typename X>
calculate_pivot_row(unsigned i)1050 void lp_core_solver_base<T, X>::calculate_pivot_row(unsigned i) {
1051 lp_assert(!use_tableau());
1052 lp_assert(m_pivot_row.is_OK());
1053 m_pivot_row_of_B_1.clear();
1054 m_pivot_row_of_B_1.resize(m_m());
1055 m_pivot_row.clear();
1056 m_pivot_row.resize(m_n());
1057 if (m_settings.use_tableau()) {
1058 unsigned basic_j = m_basis[i];
1059 for (auto & c : m_A.m_rows[i]) {
1060 if (c.var() != basic_j)
1061 m_pivot_row.set_value(c.coeff(), c.var());
1062 }
1063 return;
1064 }
1065
1066 calculate_pivot_row_of_B_1(i);
1067 calculate_pivot_row_when_pivot_row_of_B1_is_ready(i);
1068 }
1069
1070
1071 }
1072