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