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 <string>
21 #include <algorithm>
22 #include <set>
23 #include "util/vector.h"
24 #include <utility>
25 #include "util/debug.h"
26 #include "math/lp/lu.h"
27 namespace lp {
28 template <typename T, typename X, typename M> // print the nr x nc submatrix at the top left corner
print_submatrix(square_sparse_matrix<T,X> & m,unsigned mr,unsigned nc,std::ostream & out)29 void print_submatrix(square_sparse_matrix<T, X> & m, unsigned mr, unsigned nc, std::ostream & out) {
30     vector<vector<std::string>> A;
31     vector<unsigned> widths;
32     for (unsigned i = 0; i < m.row_count() && i < mr ; i++) {
33         A.push_back(vector<std::string>());
34         for (unsigned j = 0; j < m.column_count() && j < nc; j++) {
35             A[i].push_back(T_to_string(static_cast<T>(m(i, j))));
36         }
37     }
38 
39     for (unsigned j = 0; j < m.column_count() && j < nc; j++) {
40         widths.push_back(get_width_of_column(j, A));
41     }
42 
43     print_matrix_with_widths(A, widths, out);
44 }
45 
46 template<typename M>
print_matrix(M & m,std::ostream & out)47 void print_matrix(M &m, std::ostream & out) {
48     vector<vector<std::string>> A;
49     vector<unsigned> widths;
50     for (unsigned i = 0; i < m.row_count(); i++) {
51         A.push_back(vector<std::string>());
52         for (unsigned j = 0; j < m.column_count(); j++) {
53             A[i].push_back(T_to_string(m[i][j]));
54         }
55     }
56 
57     for (unsigned j = 0; j < m.column_count(); j++) {
58         widths.push_back(get_width_of_column(j, A));
59     }
60 
61     print_matrix_with_widths(A, widths, out);
62 }
63 
64 template <typename T, typename X>
one_elem_on_diag(const one_elem_on_diag & o)65 one_elem_on_diag<T, X>::one_elem_on_diag(const one_elem_on_diag & o) {
66     m_i = o.m_i;
67     m_val = o.m_val;
68 #ifdef Z3DEBUG
69     m_m = m_n = o.m_m;
70     m_one_over_val = numeric_traits<T>::one() / o.m_val;
71 #endif
72 }
73 
74 #ifdef Z3DEBUG
75 template <typename T, typename X>
get_elem(unsigned i,unsigned j)76 T one_elem_on_diag<T, X>::get_elem(unsigned i, unsigned j) const {
77     if (i == j){
78         if (j == m_i) {
79             return m_one_over_val;
80         }
81         return numeric_traits<T>::one();
82     }
83 
84     return numeric_traits<T>::zero();
85 }
86 #endif
87 template <typename T, typename X>
apply_from_left_to_T(indexed_vector<T> & w,lp_settings & settings)88 void one_elem_on_diag<T, X>::apply_from_left_to_T(indexed_vector<T> & w, lp_settings & settings) {
89     T & t = w[m_i];
90     if (numeric_traits<T>::is_zero(t)) {
91         return;
92     }
93     t /= m_val;
94     if (numeric_traits<T>::precise()) return;
95     if (settings.abs_val_is_smaller_than_drop_tolerance(t)) {
96         w.erase_from_index(m_i);
97         t = numeric_traits<T>::zero();
98     }
99 }
100 
101 // This class supports updates of the columns of B, and solves systems Bx=b,and yB=c
102 // Using Suhl-Suhl method described in the dissertation of Achim Koberstein, Chapter 5
103 template <typename M>
lu(const M & A,vector<unsigned> & basis,lp_settings & settings)104 lu<M>::lu(const M& A,
105           vector<unsigned>& basis,
106           lp_settings & settings):
107     m_status(LU_status::OK),
108     m_dim(A.row_count()),
109     m_A(A),
110     m_Q(m_dim),
111     m_R(m_dim),
112     m_r_wave(m_dim),
113     m_U(A, basis), // create the square matrix that eventually will be factorized
114     m_settings(settings),
115     m_failure(false),
116     m_row_eta_work_vector(A.row_count()),
117     m_refactor_counter(0) {
118     lp_assert(!(numeric_traits<T>::precise() && settings.use_tableau()));
119 #ifdef Z3DEBUG
120     debug_test_of_basis(A, basis);
121 #endif
122     ++m_settings.stats().m_num_factorizations;
123     create_initial_factorization();
124 #ifdef Z3DEBUG
125     // lp_assert(check_correctness());
126 #endif
127 }
128 template <typename M>
lu(const M & A,lp_settings & settings)129 lu<M>::lu(const M& A,
130           lp_settings & settings):
131     m_status(LU_status::OK),
132     m_dim(A.row_count()),
133     m_A(A),
134     m_Q(m_dim),
135     m_R(m_dim),
136     m_r_wave(m_dim),
137     m_U(A), // create the square matrix that eventually will be factorized
138     m_settings(settings),
139     m_failure(false),
140     m_row_eta_work_vector(A.row_count()),
141     m_refactor_counter(0) {
142     lp_assert(A.row_count() == A.column_count());
143     create_initial_factorization();
144 #ifdef Z3DEBUG
145     lp_assert(is_correct());
146 #endif
147 }
148 template <typename M>
debug_test_of_basis(M const & A,vector<unsigned> & basis)149 void lu<M>::debug_test_of_basis( M const & A, vector<unsigned> & basis) {
150     std::set<unsigned> set;
151     for (unsigned i = 0; i < A.row_count(); i++) {
152         lp_assert(basis[i]< A.column_count());
153         set.insert(basis[i]);
154     }
155     lp_assert(set.size() == A.row_count());
156 }
157 
158 template <typename M>
solve_By(indexed_vector<X> & y)159 void lu<M>::solve_By(indexed_vector<X> & y) {
160      lp_assert(false); // not implemented
161      // init_vector_y(y);
162      // solve_By_when_y_is_ready(y);
163  }
164 
165 
166 template <typename M>
solve_By(vector<X> & y)167 void lu<M>::solve_By(vector<X> & y) {
168     init_vector_y(y);
169     solve_By_when_y_is_ready_for_X(y);
170 }
171 
172 template <typename M>
solve_By_when_y_is_ready_for_X(vector<X> & y)173 void lu<M>::solve_By_when_y_is_ready_for_X(vector<X> & y) {
174     if (numeric_traits<T>::precise()) {
175         m_U.solve_U_y(y);
176         m_R.apply_reverse_from_left_to_X(y); // see 24.3 from Chvatal
177         return;
178     }
179     m_U.double_solve_U_y(y);
180     m_R.apply_reverse_from_left_to_X(y); // see 24.3 from Chvatal
181     unsigned i = m_dim;
182     while (i--) {
183         if (is_zero(y[i])) continue;
184         if (m_settings.abs_val_is_smaller_than_drop_tolerance(y[i])){
185             y[i] = zero_of_type<X>();
186         }
187     }
188 }
189 
190 template <typename M>
solve_By_when_y_is_ready_for_T(vector<T> & y,vector<unsigned> & index)191 void lu<M>::solve_By_when_y_is_ready_for_T(vector<T> & y, vector<unsigned> & index) {
192     if (numeric_traits<T>::precise()) {
193         m_U.solve_U_y(y);
194         m_R.apply_reverse_from_left_to_T(y); // see 24.3 from Chvatal
195         unsigned j = m_dim;
196         while (j--) {
197             if (!is_zero(y[j]))
198                 index.push_back(j);
199         }
200         return;
201     }
202     m_U.double_solve_U_y(y);
203     m_R.apply_reverse_from_left_to_T(y); // see 24.3 from Chvatal
204     unsigned i = m_dim;
205     while (i--) {
206         if (is_zero(y[i])) continue;
207         if (m_settings.abs_val_is_smaller_than_drop_tolerance(y[i])){
208             y[i] = zero_of_type<T>();
209         } else {
210             index.push_back(i);
211         }
212     }
213 }
214 
215 template <typename M>
solve_By_for_T_indexed_only(indexed_vector<T> & y,const lp_settings & settings)216 void lu<M>::solve_By_for_T_indexed_only(indexed_vector<T> & y, const lp_settings & settings) {
217     if (numeric_traits<T>::precise()) {
218         vector<unsigned> active_rows;
219         m_U.solve_U_y_indexed_only(y, settings, active_rows);
220         m_R.apply_reverse_from_left(y); // see 24.3 from Chvatal
221         return;
222     }
223     m_U.double_solve_U_y(y, m_settings);
224     m_R.apply_reverse_from_left(y); // see 24.3 from Chvatal
225 }
226 
227 template <typename M>
print_matrix_compact(std::ostream & f)228 void lu<M>::print_matrix_compact(std::ostream & f) {
229     f << "matrix_start" << std::endl;
230     f << "nrows " << m_A.row_count() << std::endl;
231     f << "ncolumns " << m_A.column_count() << std::endl;
232     for (unsigned i = 0; i < m_A.row_count(); i++) {
233         auto & row = m_A.m_rows[i];
234         f << "row " << i << std::endl;
235         for (auto & t : row) {
236             f << "column " << t.m_j << " value " << t.m_value << std::endl;
237         }
238         f << "row_end" << std::endl;
239     }
240     f << "matrix_end" << std::endl;
241 }
242 template <typename M>
print(indexed_vector<T> & w,const vector<unsigned> & basis)243 void lu< M>::print(indexed_vector<T> & w, const vector<unsigned>& basis) {
244     std::string dump_file_name("/tmp/lu");
245     remove(dump_file_name.c_str());
246     std::ofstream f(dump_file_name);
247     if (!f.is_open()) {
248         LP_OUT(m_settings, "cannot open file " << dump_file_name << std::endl);
249         return;
250     }
251     LP_OUT(m_settings, "writing lu dump to " << dump_file_name << std::endl);
252     print_matrix_compact(f);
253     print_vector(basis, f);
254     print_indexed_vector(w, f);
255     f.close();
256 }
257 template <typename M>
solve_Bd(unsigned a_column,indexed_vector<T> & d,indexed_vector<T> & w)258 void lu< M>::solve_Bd(unsigned a_column, indexed_vector<T> & d, indexed_vector<T> & w) {
259     init_vector_w(a_column, w);
260 
261     if (w.m_index.size() * ratio_of_index_size_to_all_size<T>() < d.m_data.size()) { // this const might need some tuning
262         d = w;
263         solve_By_for_T_indexed_only(d, m_settings);
264     } else {
265         d.m_data = w.m_data;
266         d.m_index.clear();
267         solve_By_when_y_is_ready_for_T(d.m_data, d.m_index);
268     }
269 }
270 
271 template <typename M>
solve_Bd_faster(unsigned a_column,indexed_vector<T> & d)272 void lu< M>::solve_Bd_faster(unsigned a_column, indexed_vector<T> & d) { // puts the a_column into d
273     init_vector_w(a_column, d);
274     solve_By_for_T_indexed_only(d, m_settings);
275 }
276 
277 template <typename M>
solve_yB(vector<T> & y)278 void lu< M>::solve_yB(vector<T>& y) {
279     // first solve yU = cb*R(-1)
280     m_R.apply_reverse_from_right_to_T(y); // got y = cb*R(-1)
281     m_U.solve_y_U(y); // got y*U=cb*R(-1)
282     m_Q.apply_reverse_from_right_to_T(y); //
283     for (auto e = m_tail.rbegin(); e != m_tail.rend(); ++e) {
284 #ifdef Z3DEBUG
285         (*e)->set_number_of_columns(m_dim);
286 #endif
287         (*e)->apply_from_right(y);
288     }
289 }
290 
291 template <typename M>
solve_yB_indexed(indexed_vector<T> & y)292 void lu< M>::solve_yB_indexed(indexed_vector<T>& y) {
293     lp_assert(y.is_OK());
294     // first solve yU = cb*R(-1)
295     m_R.apply_reverse_from_right_to_T(y); // got y = cb*R(-1)
296     lp_assert(y.is_OK());
297     m_U.solve_y_U_indexed(y, m_settings); // got y*U=cb*R(-1)
298     lp_assert(y.is_OK());
299     m_Q.apply_reverse_from_right_to_T(y);
300     lp_assert(y.is_OK());
301     for (auto e = m_tail.rbegin(); e != m_tail.rend(); ++e) {
302 #ifdef Z3DEBUG
303         (*e)->set_number_of_columns(m_dim);
304 #endif
305         (*e)->apply_from_right(y);
306         lp_assert(y.is_OK());
307     }
308 }
309 
310 template <typename M>
add_delta_to_solution(const vector<T> & yc,vector<T> & y)311 void lu< M>::add_delta_to_solution(const vector<T>& yc, vector<T>& y){
312     unsigned i = static_cast<unsigned>(y.size());
313     while (i--)
314         y[i]+=yc[i];
315 }
316 
317 template <typename M>
add_delta_to_solution_indexed(indexed_vector<T> & y)318 void lu< M>::add_delta_to_solution_indexed(indexed_vector<T>& y) {
319     // the delta sits in m_y_copy, put result into y
320     lp_assert(y.is_OK());
321     lp_assert(m_y_copy.is_OK());
322     m_ii.clear();
323     m_ii.resize(y.data_size());
324     for (unsigned i : y.m_index)
325         m_ii.set_value(1, i);
326     for (unsigned i : m_y_copy.m_index) {
327         y.m_data[i] += m_y_copy[i];
328         if (m_ii[i] == 0)
329             m_ii.set_value(1, i);
330     }
331     lp_assert(m_ii.is_OK());
332     y.m_index.clear();
333 
334     for (unsigned i : m_ii.m_index) {
335         T & v = y.m_data[i];
336         if (!lp_settings::is_eps_small_general(v, 1e-14))
337             y.m_index.push_back(i);
338         else if (!numeric_traits<T>::is_zero(v))
339             v = zero_of_type<T>();
340     }
341 
342     lp_assert(y.is_OK());
343 }
344 
345 template <typename M>
find_error_of_yB(vector<T> & yc,const vector<T> & y,const vector<unsigned> & m_basis)346 void lu< M>::find_error_of_yB(vector<T>& yc, const vector<T>& y, const vector<unsigned>& m_basis) {
347     unsigned i = m_dim;
348     while (i--) {
349         yc[i] -= m_A.dot_product_with_column(y, m_basis[i]);
350     }
351 }
352 
353 template <typename M>
find_error_of_yB_indexed(const indexed_vector<T> & y,const vector<int> & heading,const lp_settings & settings)354 void lu< M>::find_error_of_yB_indexed(const indexed_vector<T>& y, const vector<int>& heading, const lp_settings& settings) {
355 #if 0 == 1
356     // it is a non efficient version
357     indexed_vector<T> yc = m_y_copy;
358     yc.m_index.clear();
359     lp_assert(!numeric_traits<T>::precise());
360     {
361 
362         vector<unsigned> d_basis(y.m_data.size());
363         for (unsigned j = 0; j < heading.size(); j++) {
364             if (heading[j] >= 0) {
365                 d_basis[heading[j]] = j;
366             }
367         }
368 
369 
370         unsigned i = m_dim;
371         while (i--) {
372             T & v = yc.m_data[i] -= m_A.dot_product_with_column(y.m_data, d_basis[i]);
373             if (settings.abs_val_is_smaller_than_drop_tolerance(v))
374                 v = zero_of_type<T>();
375             else
376                 yc.m_index.push_back(i);
377         }
378     }
379 #endif
380     lp_assert(m_ii.is_OK());
381     m_ii.clear();
382     m_ii.resize(y.data_size());
383     lp_assert(m_y_copy.is_OK());
384     // put the error into m_y_copy
385     for (auto k : y.m_index) {
386         auto & row = m_A.m_rows[k];
387         const T & y_k = y.m_data[k];
388         for (auto & c : row) {
389             unsigned j = c.var();
390             int hj = heading[j];
391             if (hj < 0) continue;
392             if (m_ii.m_data[hj] == 0)
393                 m_ii.set_value(1, hj);
394             m_y_copy.m_data[hj] -= c.coeff() * y_k;
395         }
396     }
397     // add the index of m_y_copy to m_ii
398     for (unsigned i : m_y_copy.m_index) {
399         if (m_ii.m_data[i] == 0)
400             m_ii.set_value(1, i);
401     }
402 
403     // there is no guarantee that m_y_copy is OK here, but its index
404     // is contained in m_ii index
405     m_y_copy.m_index.clear();
406     // setup the index of m_y_copy
407     for (auto k : m_ii.m_index) {
408         T& v = m_y_copy.m_data[k];
409         if (settings.abs_val_is_smaller_than_drop_tolerance(v))
410             v = zero_of_type<T>();
411         else {
412             m_y_copy.set_value(v, k);
413         }
414     }
415     lp_assert(m_y_copy.is_OK());
416 
417 }
418 
419 
420 
421 
422 // solves y*B = y
423 // y is the input
424 template <typename M>
solve_yB_with_error_check_indexed(indexed_vector<T> & y,const vector<int> & heading,const vector<unsigned> & basis,const lp_settings & settings)425 void lu< M>::solve_yB_with_error_check_indexed(indexed_vector<T> & y, const vector<int>& heading,  const vector<unsigned> & basis, const lp_settings & settings) {
426     if (numeric_traits<T>::precise()) {
427         if (y.m_index.size() * ratio_of_index_size_to_all_size<T>() * 3 < m_A.column_count()) {
428             solve_yB_indexed(y);
429         } else {
430             solve_yB(y.m_data);
431             y.restore_index_and_clean_from_data();
432         }
433         return;
434     }
435     lp_assert(m_y_copy.is_OK());
436     lp_assert(y.is_OK());
437     if (y.m_index.size() * ratio_of_index_size_to_all_size<T>() < m_A.column_count()) {
438         m_y_copy = y;
439         solve_yB_indexed(y);
440         lp_assert(y.is_OK());
441         if (y.m_index.size() * ratio_of_index_size_to_all_size<T>() >= m_A.column_count()) {
442             find_error_of_yB(m_y_copy.m_data, y.m_data, basis);
443             solve_yB(m_y_copy.m_data);
444             add_delta_to_solution(m_y_copy.m_data, y.m_data);
445             y.restore_index_and_clean_from_data();
446             m_y_copy.clear_all();
447         } else {
448             find_error_of_yB_indexed(y, heading, settings); // this works with m_y_copy
449             solve_yB_indexed(m_y_copy);
450             add_delta_to_solution_indexed(y);
451         }
452         lp_assert(m_y_copy.is_OK());
453     } else {
454         solve_yB_with_error_check(y.m_data, basis);
455         y.restore_index_and_clean_from_data();
456     }
457 }
458 
459 
460 // solves y*B = y
461 // y is the input
462 template <typename M>
solve_yB_with_error_check(vector<T> & y,const vector<unsigned> & basis)463 void lu< M>::solve_yB_with_error_check(vector<T> & y, const vector<unsigned>& basis) {
464     if (numeric_traits<T>::precise()) {
465         solve_yB(y);
466         return;
467     }
468     auto & yc = m_y_copy.m_data;
469     yc =y; // copy y aside
470     solve_yB(y);
471     find_error_of_yB(yc, y, basis);
472     solve_yB(yc);
473     add_delta_to_solution(yc, y);
474     m_y_copy.clear_all();
475 }
476 template <typename M>
apply_Q_R_to_U(permutation_matrix<T,X> & r_wave)477 void lu< M>::apply_Q_R_to_U(permutation_matrix<T, X> & r_wave) {
478     m_U.multiply_from_right(r_wave);
479     m_U.multiply_from_left_with_reverse(r_wave);
480 }
481 
482 
483 // Solving yB = cb to find the entering variable,
484 // where cb is the cost vector projected to B.
485 // The result is stored in cb.
486 
487 // solving Bd = a ( to find the column d of B^{-1} A_N corresponding to the entering
488 // variable
489 template <typename M>
~lu()490 lu< M>::~lu(){
491     for (auto t : m_tail) {
492         delete t;
493     }
494 }
495 template <typename M>
init_vector_y(vector<X> & y)496 void lu< M>::init_vector_y(vector<X> & y) {
497     apply_lp_list_to_y(y);
498     m_Q.apply_reverse_from_left_to_X(y);
499 }
500 
501 template <typename M>
perform_transformations_on_w(indexed_vector<T> & w)502 void lu< M>::perform_transformations_on_w(indexed_vector<T>& w) {
503     apply_lp_list_to_w(w);
504     m_Q.apply_reverse_from_left(w);
505     // TBD does not compile: lp_assert(numeric_traits<T>::precise() || check_vector_for_small_values(w, m_settings));
506 }
507 
508 // see Chvatal 24.3
509 template <typename M>
init_vector_w(unsigned entering,indexed_vector<T> & w)510 void lu< M>::init_vector_w(unsigned entering, indexed_vector<T> & w) {
511     w.clear();
512     m_A.copy_column_to_indexed_vector(entering, w); // w = a, the column
513     perform_transformations_on_w(w);
514 }
515 template <typename M>
apply_lp_list_to_w(indexed_vector<T> & w)516 void lu< M>::apply_lp_list_to_w(indexed_vector<T> & w) {
517     for (unsigned i = 0; i < m_tail.size(); i++) {
518         m_tail[i]->apply_from_left_to_T(w, m_settings);
519         // TBD does not compile: lp_assert(check_vector_for_small_values(w, m_settings));
520     }
521 }
522 template <typename M>
apply_lp_list_to_y(vector<X> & y)523 void lu< M>::apply_lp_list_to_y(vector<X>& y) {
524     for (unsigned i = 0; i < m_tail.size(); i++) {
525         m_tail[i]->apply_from_left(y, m_settings);
526     }
527 }
528 template <typename M>
swap_rows(int j,int k)529 void lu< M>::swap_rows(int j, int k) {
530     if (j != k) {
531         m_Q.transpose_from_left(j, k);
532         m_U.swap_rows(j, k);
533     }
534 }
535 
536 template <typename M>
swap_columns(int j,int pivot_column)537 void lu< M>::swap_columns(int j, int pivot_column) {
538     if (j == pivot_column)
539         return;
540     m_R.transpose_from_right(j, pivot_column);
541     m_U.swap_columns(j, pivot_column);
542 }
543 template <typename M>
pivot_the_row(int row)544 bool lu< M>::pivot_the_row(int row) {
545     eta_matrix<T, X> * eta_matrix = get_eta_matrix_for_pivot(row);
546     if (get_status() != LU_status::OK) {
547         return false;
548     }
549 
550     if (eta_matrix == nullptr) {
551         m_U.shorten_active_matrix(row, nullptr);
552         return true;
553     }
554     if (!m_U.pivot_with_eta(row, eta_matrix, m_settings))
555         return false;
556     eta_matrix->conjugate_by_permutation(m_Q);
557     push_matrix_to_tail(eta_matrix);
558     return true;
559 }
560 // we're processing the column j now
561 template <typename M>
get_eta_matrix_for_pivot(unsigned j)562 eta_matrix<typename M::coefftype, typename M::argtype> * lu< M>::get_eta_matrix_for_pivot(unsigned j) {
563     eta_matrix<T, X> *ret;
564     if(!m_U.fill_eta_matrix(j, &ret)) {
565         set_status(LU_status::Degenerated);
566     }
567     return ret;
568 }
569 // we're processing the column j now
570 template <typename M>
get_eta_matrix_for_pivot(unsigned j,square_sparse_matrix<T,X> & copy_of_U)571 eta_matrix<typename M::coefftype, typename M::argtype> * lu<M>::get_eta_matrix_for_pivot(unsigned j, square_sparse_matrix<T, X>& copy_of_U) {
572     eta_matrix<T, X> *ret;
573     copy_of_U.fill_eta_matrix(j, &ret);
574     return ret;
575 }
576 
577 // see page 407 of Chvatal
578 template <typename M>
transform_U_to_V_by_replacing_column(indexed_vector<T> & w,unsigned leaving_column)579 unsigned lu<M>::transform_U_to_V_by_replacing_column(indexed_vector<T> & w,
580                                                         unsigned leaving_column) {
581     unsigned column_to_replace = m_R.apply_reverse(leaving_column);
582     m_U.replace_column(column_to_replace, w, m_settings);
583     return column_to_replace;
584 }
585 
586 #ifdef Z3DEBUG
587 template <typename M>
check_vector_w(unsigned entering)588 void lu<M>::check_vector_w(unsigned entering) {
589     T * w = new T[m_dim];
590     m_A.copy_column_to_vector(entering, w);
591     check_apply_lp_lists_to_w(w);
592     delete [] w;
593 }
594 template <typename M>
check_apply_matrix_to_vector(matrix<T,X> * lp,T * w)595 void lu<M>::check_apply_matrix_to_vector(matrix<T, X> *lp, T *w) {
596     if (lp != nullptr) {
597         lp -> set_number_of_rows(m_dim);
598         lp -> set_number_of_columns(m_dim);
599         apply_to_vector(*lp, w);
600     }
601 }
602 
603 template <typename M>
check_apply_lp_lists_to_w(T * w)604 void lu<M>::check_apply_lp_lists_to_w(T * w) {
605     for (unsigned i = 0; i < m_tail.size(); i++) {
606         check_apply_matrix_to_vector(m_tail[i], w);
607     }
608     permutation_matrix<T, X> qr = m_Q.get_reverse();
609     apply_to_vector(qr, w);
610     for (int i = m_dim - 1; i >= 0; i--) {
611         lp_assert(abs(w[i] - w[i]) < 0.0000001);
612     }
613 }
614 
615 #endif
616 template <typename M>
process_column(int j)617 void lu<M>::process_column(int j) {
618     unsigned pi, pj;
619     bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j);
620     if (!success) {
621         //        LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
622         m_failure = true;
623         return;
624     }
625 
626     if (static_cast<int>(pi) == -1) {
627         // LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
628         m_failure = true;
629         return;
630     }
631     swap_columns(j, pj);
632     swap_rows(j, pi);
633     if (!pivot_the_row(j)) {
634         //      LP_OUT(m_settings, "pivot_the_row(" << j << ") failed" << std::endl);
635         m_failure = true;
636     }
637 }
638 template <typename M>
is_correct(const vector<unsigned> & basis)639 bool lu<M>::is_correct(const vector<unsigned>& basis) {
640 #ifdef Z3DEBUG
641     if (get_status() != LU_status::OK) {
642         return false;
643     }
644     dense_matrix<T, X> left_side = get_left_side(basis);
645     dense_matrix<T, X> right_side = get_right_side();
646     return left_side == right_side;
647 #else
648     return true;
649 #endif
650 }
651 
652 template <typename M>
is_correct()653 bool lu<M>::is_correct() {
654 #ifdef Z3DEBUG
655     if (get_status() != LU_status::OK) {
656         return false;
657     }
658     dense_matrix<T, X> left_side = get_left_side();
659     dense_matrix<T, X> right_side = get_right_side();
660     return left_side == right_side;
661 #else
662     return true;
663 #endif
664 }
665 
666 
667 #ifdef Z3DEBUG
668 template <typename M>
tail_product()669 dense_matrix<typename M::coefftype, typename M::argtype> lu<M>::tail_product() {
670     lp_assert(tail_size() > 0);
671     dense_matrix<T, X> left_side = permutation_matrix<T, X>(m_dim);
672     for (unsigned i = 0; i < tail_size(); i++) {
673         matrix<T, X>* lp =  get_lp_matrix(i);
674         lp->set_number_of_rows(m_dim);
675         lp->set_number_of_columns(m_dim);
676         left_side = ((*lp) * left_side);
677     }
678     return left_side;
679 }
680 template <typename M>
get_left_side(const vector<unsigned> & basis)681 dense_matrix<typename M::coefftype, typename M::argtype> lu<M>::get_left_side(const vector<unsigned>& basis) {
682     dense_matrix<T, X> left_side = get_B(*this, basis);
683     for (unsigned i = 0; i < tail_size(); i++) {
684         matrix<T, X>* lp =  get_lp_matrix(i);
685         lp->set_number_of_rows(m_dim);
686         lp->set_number_of_columns(m_dim);
687         left_side = ((*lp) * left_side);
688     }
689     return left_side;
690 }
691 template <typename M>
get_left_side()692 dense_matrix<typename M::coefftype, typename M::argtype> lu<M>::get_left_side() {
693     dense_matrix<T, X> left_side = get_B(*this);
694     for (unsigned i = 0; i < tail_size(); i++) {
695         matrix<T, X>* lp =  get_lp_matrix(i);
696         lp->set_number_of_rows(m_dim);
697         lp->set_number_of_columns(m_dim);
698         left_side = ((*lp) * left_side);
699     }
700     return left_side;
701 }
702 template <typename M>
get_right_side()703 dense_matrix<typename M::coefftype, typename M::argtype>  lu<M>::get_right_side() {
704     auto ret = U() * R();
705     ret = Q() * ret;
706     return ret;
707 }
708 #endif
709 
710 // needed for debugging purposes
711 template <typename M>
copy_w(T * buffer,indexed_vector<T> & w)712 void lu<M>::copy_w(T *buffer, indexed_vector<T> & w) {
713     unsigned i = m_dim;
714     while (i--) {
715         buffer[i] = w[i];
716     }
717 }
718 
719 // needed for debugging purposes
720 template <typename M>
restore_w(T * buffer,indexed_vector<T> & w)721 void lu<M>::restore_w(T *buffer, indexed_vector<T> & w) {
722     unsigned i = m_dim;
723     while (i--) {
724         w[i] = buffer[i];
725     }
726 }
727 template <typename M>
all_columns_and_rows_are_active()728 bool lu<M>::all_columns_and_rows_are_active() {
729     unsigned i = m_dim;
730     while (i--) {
731         lp_assert(m_U.col_is_active(i));
732         lp_assert(m_U.row_is_active(i));
733     }
734     return true;
735 }
736 template <typename M>
too_dense(unsigned j)737 bool lu<M>::too_dense(unsigned j) const {
738     unsigned r = m_dim - j;
739     if (r < 5)
740         return false;
741      // if (j * 5 < m_dim * 4) // start looking for dense only at the bottom  of the rows
742      //    return false;
743     //    return r * r * m_settings.density_threshold <= m_U.get_number_of_nonzeroes_below_row(j);
744     return r * r * m_settings.density_threshold <= m_U.get_n_of_active_elems();
745 }
746 template <typename M>
pivot_in_dense_mode(unsigned i)747 void lu<M>::pivot_in_dense_mode(unsigned i) {
748     int j = m_dense_LU->find_pivot_column_in_row(i);
749     if (j == -1) {
750         m_failure = true;
751         return;
752     }
753     if (i != static_cast<unsigned>(j)) {
754         swap_columns(i, j);
755         m_dense_LU->swap_columns(i, j);
756     }
757     m_dense_LU->pivot(i, m_settings);
758 }
759 template <typename M>
create_initial_factorization()760 void lu<M>::create_initial_factorization(){
761     m_U.prepare_for_factorization();
762     unsigned j;
763     for (j = 0; j < m_dim; j++) {
764         process_column(j);
765         if (m_failure) {
766             set_status(LU_status::Degenerated);
767             return;
768         }
769         if (too_dense(j)) {
770             break;
771         }
772     }
773     if (j == m_dim) {
774         // TBD does not compile: lp_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
775         //        lp_assert(is_correct());
776         // lp_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
777         return;
778     }
779     j++;
780     m_dense_LU = new square_dense_submatrix<T, X>(&m_U, j);
781     for (; j < m_dim; j++) {
782         pivot_in_dense_mode(j);
783         if (m_failure) {
784             set_status(LU_status::Degenerated);
785             return;
786         }
787     }
788     m_dense_LU->update_parent_matrix(m_settings);
789     lp_assert(m_dense_LU->is_L_matrix());
790     m_dense_LU->conjugate_by_permutation(m_Q);
791     push_matrix_to_tail(m_dense_LU);
792     m_refactor_counter = 0;
793     // lp_assert(is_correct());
794     // lp_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
795 }
796 
797 template <typename M>
calculate_r_wave_and_update_U(unsigned bump_start,unsigned bump_end,permutation_matrix<T,X> & r_wave)798 void lu<M>::calculate_r_wave_and_update_U(unsigned bump_start, unsigned bump_end, permutation_matrix<T, X> & r_wave) {
799     if (bump_start > bump_end) {
800         set_status(LU_status::Degenerated);
801         return;
802     }
803     if (bump_start == bump_end) {
804         return;
805     }
806 
807     r_wave[bump_start] = bump_end; // sending the offensive column to the end of the bump
808 
809     for ( unsigned i = bump_start + 1 ; i <= bump_end; i++ ) {
810         r_wave[i] = i - 1;
811     }
812 
813     m_U.multiply_from_right(r_wave);
814     m_U.multiply_from_left_with_reverse(r_wave);
815 }
816 template <typename M>
scan_last_row_to_work_vector(unsigned lowest_row_of_the_bump)817 void lu<M>::scan_last_row_to_work_vector(unsigned lowest_row_of_the_bump) {
818     vector<indexed_value<T>> & last_row_vec = m_U.get_row_values(m_U.adjust_row(lowest_row_of_the_bump));
819     for (auto & iv : last_row_vec) {
820         if (is_zero(iv.m_value)) continue;
821         lp_assert(!m_settings.abs_val_is_smaller_than_drop_tolerance(iv.m_value));
822         unsigned adjusted_col = m_U.adjust_column_inverse(iv.m_index);
823         if (adjusted_col < lowest_row_of_the_bump) {
824             m_row_eta_work_vector.set_value(-iv.m_value, adjusted_col);
825         } else  {
826             m_row_eta_work_vector.set_value(iv.m_value, adjusted_col); // preparing to calculate the real value in the matrix
827         }
828     }
829 }
830 
831 template <typename M>
pivot_and_solve_the_system(unsigned replaced_column,unsigned lowest_row_of_the_bump)832 void lu<M>::pivot_and_solve_the_system(unsigned replaced_column, unsigned lowest_row_of_the_bump) {
833     // we have the system right side at m_row_eta_work_vector now
834     // solve the system column wise
835     for (unsigned j = replaced_column; j < lowest_row_of_the_bump; j++) {
836         T v = m_row_eta_work_vector[j];
837         if (numeric_traits<T>::is_zero(v)) continue; // this column does not contribute to the solution
838         unsigned aj = m_U.adjust_row(j);
839         vector<indexed_value<T>> & row = m_U.get_row_values(aj);
840         for (auto & iv : row) {
841             unsigned col = m_U.adjust_column_inverse(iv.m_index);
842             lp_assert(col >= j || numeric_traits<T>::is_zero(iv.m_value));
843             if (col == j) continue;
844             if (numeric_traits<T>::is_zero(iv.m_value)) {
845                 continue;
846             }
847             // the -v is for solving the system ( to zero the last row), and +v is for pivoting
848             T delta = col < lowest_row_of_the_bump? -v * iv.m_value: v * iv.m_value;
849             lp_assert(numeric_traits<T>::is_zero(delta) == false);
850 
851 
852 
853            // m_row_eta_work_vector.add_value_at_index_with_drop_tolerance(col, delta);
854             if (numeric_traits<T>::is_zero(m_row_eta_work_vector[col])) {
855                 if (!m_settings.abs_val_is_smaller_than_drop_tolerance(delta)){
856                     m_row_eta_work_vector.set_value(delta, col);
857                 }
858             } else {
859                 T t = (m_row_eta_work_vector[col] += delta);
860                 if (m_settings.abs_val_is_smaller_than_drop_tolerance(t)){
861                     m_row_eta_work_vector[col] = numeric_traits<T>::zero();
862                     auto it = std::find(m_row_eta_work_vector.m_index.begin(), m_row_eta_work_vector.m_index.end(), col);
863                     if (it != m_row_eta_work_vector.m_index.end())
864                         m_row_eta_work_vector.m_index.erase(it);
865                 }
866                 }
867         }
868     }
869 }
870 // see Achim Koberstein's thesis page 58, but here we solve the system and pivot to the last
871 // row at the same time
872 template <typename M>
get_row_eta_matrix_and_set_row_vector(unsigned replaced_column,unsigned lowest_row_of_the_bump,const T & pivot_elem_for_checking)873 row_eta_matrix<typename M::coefftype, typename M::argtype> *lu<M>::get_row_eta_matrix_and_set_row_vector(unsigned replaced_column, unsigned lowest_row_of_the_bump, const T &  pivot_elem_for_checking) {
874     if (replaced_column == lowest_row_of_the_bump) return nullptr;
875     scan_last_row_to_work_vector(lowest_row_of_the_bump);
876     pivot_and_solve_the_system(replaced_column, lowest_row_of_the_bump);
877     if (numeric_traits<T>::precise() == false && !is_zero(pivot_elem_for_checking)) {
878         T denom = std::max(T(1), abs(pivot_elem_for_checking));
879         if (
880             !m_settings.abs_val_is_smaller_than_pivot_tolerance((m_row_eta_work_vector[lowest_row_of_the_bump] - pivot_elem_for_checking) / denom)) {
881             set_status(LU_status::Degenerated);
882             //        LP_OUT(m_settings, "diagonal element is off" << std::endl);
883             return nullptr;
884         }
885     }
886 #ifdef Z3DEBUG
887     auto ret = new row_eta_matrix<typename M::coefftype, typename M::argtype>(replaced_column, lowest_row_of_the_bump, m_dim);
888 #else
889     auto ret = new row_eta_matrix<typename M::coefftype, typename M::argtype>(replaced_column, lowest_row_of_the_bump);
890 #endif
891 
892     for (auto j : m_row_eta_work_vector.m_index) {
893         if (j < lowest_row_of_the_bump) {
894             auto & v = m_row_eta_work_vector[j];
895             if (!is_zero(v)) {
896                 if (!m_settings.abs_val_is_smaller_than_drop_tolerance(v)){
897                     ret->push_back(j, v);
898                 }
899                 v = numeric_traits<T>::zero();
900             }
901         }
902     } // now the lowest_row_of_the_bump contains the rest of the row to the right of the bump with correct values
903     return ret;
904 }
905 
906 template <typename M>
replace_column(T pivot_elem_for_checking,indexed_vector<T> & w,unsigned leaving_column_of_U)907 void lu<M>::replace_column(T pivot_elem_for_checking, indexed_vector<T> & w, unsigned leaving_column_of_U){
908     m_refactor_counter++;
909     unsigned replaced_column =  transform_U_to_V_by_replacing_column( w, leaving_column_of_U);
910     unsigned lowest_row_of_the_bump = m_U.lowest_row_in_column(replaced_column);
911     m_r_wave.init(m_dim);
912     calculate_r_wave_and_update_U(replaced_column, lowest_row_of_the_bump, m_r_wave);
913     auto row_eta = get_row_eta_matrix_and_set_row_vector(replaced_column, lowest_row_of_the_bump, pivot_elem_for_checking);
914 
915     if (get_status() == LU_status::Degenerated) {
916         m_row_eta_work_vector.clear_all();
917         return;
918     }
919     m_Q.multiply_by_permutation_from_right(m_r_wave);
920     m_R.multiply_by_permutation_reverse_from_left(m_r_wave);
921     if (row_eta != nullptr) {
922         row_eta->conjugate_by_permutation(m_Q);
923         push_matrix_to_tail(row_eta);
924     }
925     calculate_Lwave_Pwave_for_bump(replaced_column, lowest_row_of_the_bump);
926     // lp_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
927     // lp_assert(w.is_OK() && m_row_eta_work_vector.is_OK());
928 }
929 template <typename M>
calculate_Lwave_Pwave_for_bump(unsigned replaced_column,unsigned lowest_row_of_the_bump)930 void lu<M>::calculate_Lwave_Pwave_for_bump(unsigned replaced_column, unsigned lowest_row_of_the_bump){
931     T diagonal_elem;
932     if (replaced_column < lowest_row_of_the_bump) {
933         diagonal_elem = m_row_eta_work_vector[lowest_row_of_the_bump];
934         //          lp_assert(m_row_eta_work_vector.is_OK());
935         m_U.set_row_from_work_vector_and_clean_work_vector_not_adjusted(m_U.adjust_row(lowest_row_of_the_bump), m_row_eta_work_vector, m_settings);
936     } else {
937         diagonal_elem = m_U(lowest_row_of_the_bump, lowest_row_of_the_bump); // todo - get it more efficiently
938     }
939     if (m_settings.abs_val_is_smaller_than_pivot_tolerance(diagonal_elem)) {
940         set_status(LU_status::Degenerated);
941         return;
942     }
943 
944     calculate_Lwave_Pwave_for_last_row(lowest_row_of_the_bump, diagonal_elem);
945     //         lp_assert(m_U.is_upper_triangular_and_maximums_are_set_correctly_in_rows(m_settings));
946 }
947 
948 template <typename M>
calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump,T diagonal_element)949 void lu<M>::calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump, T diagonal_element) {
950     auto l = new one_elem_on_diag<T, X>(lowest_row_of_the_bump, diagonal_element);
951 #ifdef Z3DEBUG
952     l->set_number_of_columns(m_dim);
953 #endif
954     push_matrix_to_tail(l);
955     m_U.divide_row_by_constant(lowest_row_of_the_bump, diagonal_element, m_settings);
956     l->conjugate_by_permutation(m_Q);
957 }
958 
959 template <typename M>
init_factorization(lu<M> * & factorization,M & m_A,vector<unsigned> & m_basis,lp_settings & m_settings)960 void init_factorization(lu<M>* & factorization, M & m_A, vector<unsigned> & m_basis, lp_settings &m_settings) {
961     if (factorization != nullptr)
962         delete factorization;
963     factorization = new lu<M>(m_A, m_basis, m_settings);
964     // if (factorization->get_status() != LU_status::OK)
965     //     LP_OUT(m_settings, "failing in init_factorization" << std::endl);
966 }
967 
968 #ifdef Z3DEBUG
969 template <typename M>
get_B(lu<M> & f,const vector<unsigned> & basis)970 dense_matrix<typename M::coefftype, typename M::argtype>  get_B(lu<M>& f, const vector<unsigned>& basis) {
971     lp_assert(basis.size() == f.dimension());
972     lp_assert(basis.size() == f.m_U.dimension());
973     dense_matrix<typename M::coefftype, typename M::argtype>  B(f.dimension(), f.dimension());
974     for (unsigned i = 0; i < f.dimension(); i++)
975         for (unsigned j = 0; j < f.dimension(); j++)
976             B.set_elem(i, j, f.B_(i, j, basis));
977 
978     return B;
979 }
980 template <typename M>
get_B(lu<M> & f)981 dense_matrix<typename M::coefftype, typename M::argtype>  get_B(lu<M>& f) {
982     dense_matrix<typename M::coefftype, typename M::argtype>  B(f.dimension(), f.dimension());
983     for (unsigned i = 0; i < f.dimension(); i++)
984         for (unsigned j = 0; j < f.dimension(); j++)
985             B.set_elem(i, j, f.m_A[i][j]);
986 
987     return B;
988 }
989 #endif
990 }
991