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 <utility>
21 #include <memory>
22 #include <string>
23 #include "util/vector.h"
24 #include "util/debug.h"
25 #include "math/lp/lu_def.h"
26 namespace lp {
27 template double dot_product<double, double>(vector<double> const&, vector<double> const&);
28 template lu<static_matrix<double, double>>::lu(static_matrix<double, double> const&, vector<unsigned int>&, lp_settings&);
29 template void lu<static_matrix<double, double>>::push_matrix_to_tail(tail_matrix<double, double>*);
30 template void lu<static_matrix<double, double>>::replace_column(double, indexed_vector<double>&, unsigned);
31 template void lu<static_matrix<double, double>>::solve_Bd(unsigned int, indexed_vector<double>&, indexed_vector<double>&);
32 template lu<static_matrix<double, double>>::~lu();
33 template void lu<static_matrix<mpq, mpq>>::push_matrix_to_tail(tail_matrix<mpq, mpq>*);
34 template void lu<static_matrix<mpq, mpq>>::solve_Bd(unsigned int, indexed_vector<mpq>&, indexed_vector<mpq>&);
35 template lu<static_matrix<mpq, mpq>>::~lu();
36 template void lu<static_matrix<mpq, impq>>::push_matrix_to_tail(tail_matrix<mpq, impq >*);
37 template void lu<static_matrix<mpq, impq>>::solve_Bd(unsigned int, indexed_vector<mpq>&, indexed_vector<mpq>&);
38 template lu<static_matrix<mpq, impq>>::~lu();
39 template mpq dot_product<mpq, mpq>(vector<mpq > const&, vector<mpq > const&);
40 template void init_factorization<static_matrix<double, double>>
41     (lu<static_matrix<double, double>>*&, static_matrix<double, double>&, vector<unsigned int>&, lp_settings&);
42 template void init_factorization<static_matrix<mpq, mpq>>
43     (lu<static_matrix<mpq,mpq>>*&, static_matrix<mpq, mpq>&, vector<unsigned int>&, lp_settings&);
44 template void init_factorization<static_matrix<mpq, impq>>(lu<static_matrix<mpq, impq> >*&, static_matrix<mpq, impq >&, vector<unsigned int>&, lp_settings&);
45 template void print_matrix<square_sparse_matrix<double, double>>(square_sparse_matrix<double, double>&, std::ostream & out);
46 template void print_matrix<static_matrix<mpq,mpq>>(static_matrix<mpq, mpq>&, std::ostream&);
47 template void print_matrix<static_matrix<mpq, impq> >(static_matrix<mpq, impq >&, std::ostream&);
48 template void print_matrix<static_matrix<double, double>>(static_matrix<double, double>&, std::ostream & out);
49 #ifdef Z3DEBUG
50 template bool lu<static_matrix<double, double>>::is_correct(const vector<unsigned>& basis);
51 template bool lu<static_matrix<mpq, impq>>::is_correct( vector<unsigned int> const &);
52 template dense_matrix<double, double> get_B<static_matrix<double, double>>(lu<static_matrix<double, double>>&, const vector<unsigned>& basis);
53 template dense_matrix<mpq, mpq> get_B<static_matrix<mpq, mpq>>(lu<static_matrix<mpq, mpq>>&, vector<unsigned int> const&);
54 
55 #endif
56 
57 template bool lu<static_matrix<double, double>>::pivot_the_row(int); // NOLINT
58 template void lu<static_matrix<double, double>>::init_vector_w(unsigned int, indexed_vector<double>&);
59 template void lu<static_matrix<double, double>>::solve_By(vector<double>&);
60 template void lu<static_matrix<double, double>>::solve_By_when_y_is_ready_for_X(vector<double>&);
61 template void lu<static_matrix<double, double>>::solve_yB_with_error_check(vector<double>&, const vector<unsigned>& basis);
62 template void lu<static_matrix<double, double>>::solve_yB_with_error_check_indexed(indexed_vector<double>&, vector<int> const&,  const vector<unsigned> & basis, const lp_settings&);
63 template void lu<static_matrix<mpq, mpq>>::replace_column(mpq, indexed_vector<mpq>&, unsigned);
64 template void lu<static_matrix<mpq, mpq>>::solve_By(vector<mpq >&);
65 template void lu<static_matrix<mpq, mpq>>::solve_By_when_y_is_ready_for_X(vector<mpq >&);
66 template void lu<static_matrix<mpq, mpq>>::solve_yB_with_error_check(vector<mpq >&, const vector<unsigned>& basis);
67 template void lu<static_matrix<mpq, mpq>>::solve_yB_with_error_check_indexed(indexed_vector<mpq>&, vector< int > const&,  const vector<unsigned> & basis, const lp_settings&);
68 template void lu<static_matrix<mpq, impq> >::solve_yB_with_error_check_indexed(indexed_vector<mpq>&, vector< int > const&,  const vector<unsigned> & basis, const lp_settings&);
69 template void lu<static_matrix<mpq, impq> >::init_vector_w(unsigned int, indexed_vector<mpq>&);
70 template void lu<static_matrix<mpq, impq> >::replace_column(mpq, indexed_vector<mpq>&, unsigned);
71 template void lu<static_matrix<mpq, impq> >::solve_Bd_faster(unsigned int, indexed_vector<mpq>&);
72 template void lu<static_matrix<mpq, impq> >::solve_By(vector<impq >&);
73 template void lu<static_matrix<mpq, impq> >::solve_By_when_y_is_ready_for_X(vector<impq >&);
74 template void lu<static_matrix<mpq, impq> >::solve_yB_with_error_check(vector<mpq >&, const vector<unsigned>& basis);
75 template void lu<static_matrix<mpq, mpq>>::solve_By(indexed_vector<mpq>&);
76 template void lu<static_matrix<double, double>>::solve_By(indexed_vector<double>&);
77 template void lu<static_matrix<double, double>>::solve_yB_indexed(indexed_vector<double>&);
78 template void lu<static_matrix<mpq, impq> >::solve_yB_indexed(indexed_vector<mpq>&);
79 template void lu<static_matrix<mpq, mpq>>::solve_By_for_T_indexed_only(indexed_vector<mpq>&, lp_settings const&);
80 template void lu<static_matrix<double, double>>::solve_By_for_T_indexed_only(indexed_vector<double>&, lp_settings const&);
81 #ifdef Z3DEBUG
82 template void print_matrix<tail_matrix<double, double>>(tail_matrix<double, double>&, std::ostream&);
83 #endif
84 }
85