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

rm_lu

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-04 15:15:08 -08:00
parent 25f103db1a
commit c251151d66
4 changed files with 9 additions and 163 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -795,24 +795,7 @@ namespace lp {
template <typename K, typename L>
void lar_solver::add_last_rows_to_lu(lp_primal_core_solver<K, L>& s) {
auto& f = s.m_factorization;
if (f != nullptr) {
auto columns_to_replace = f->get_set_of_columns_to_replace_for_add_last_rows(s.m_basis_heading);
if (f->m_refactor_counter + columns_to_replace.size() >= 200 || f->has_dense_submatrix()) {
delete f;
f = nullptr;
}
else {
f->add_last_rows_to_B(s.m_basis_heading, columns_to_replace);
}
}
if (f == nullptr) {
init_factorization(f, s.m_A, s.m_basis, m_settings);
if (f->get_status() != LU_status::OK) {
delete f;
f = nullptr;
}
}
lp_assert(false);
}

2
src/math/lp/lp_primal_core_solver.h
View file

@ -418,7 +418,7 @@ public:
// returns the number of iterations
unsigned solve();
lu<static_matrix<T, X>> * factorization() {return this->m_factorization;}
lu<static_matrix<T, X>> * factorization() {return nullptr;}
void delete_factorization();

59
src/math/lp/lu.h
View file

@ -305,66 +305,19 @@ public:
void calculate_Lwave_Pwave_for_last_row(unsigned lowest_row_of_the_bump, T diagonal_element);
void prepare_entering(unsigned entering, indexed_vector<T> & w) {
init_vector_w(entering, w);
lp_assert(false);
}
bool need_to_refactor() { return m_refactor_counter >= 200; }
bool need_to_refactor() { lp_assert(false);
return m_refactor_counter >= 200; }
void adjust_dimension_with_matrix_A() {
lp_assert(m_A.row_count() >= m_dim);
m_dim = m_A.row_count();
m_U.resize(m_dim);
m_Q.resize(m_dim);
m_R.resize(m_dim);
m_row_eta_work_vector.resize(m_dim);
lp_assert(false);
}
std::unordered_set<unsigned> get_set_of_columns_to_replace_for_add_last_rows(const vector<int> & heading) const {
std::unordered_set<unsigned> columns_to_replace;
unsigned m = m_A.row_count();
unsigned m_prev = m_U.dimension();
lp_assert(m_A.column_count() == heading.size());
for (unsigned i = m_prev; i < m; i++) {
for (const row_cell<T> & c : m_A.m_rows[i]) {
int h = heading[c.var()];
if (h < 0) {
continue;
}
columns_to_replace.insert(c.var());
}
}
return columns_to_replace;
}
void add_last_rows_to_B(const vector<int> & heading, const std::unordered_set<unsigned> & columns_to_replace) {
unsigned m = m_A.row_count();
lp_assert(m_A.column_count() == heading.size());
adjust_dimension_with_matrix_A();
m_w_for_extension.resize(m);
// At this moment the LU is correct
// for B extended by only by ones at the diagonal in the lower right corner
for (unsigned j :columns_to_replace) {
lp_assert(heading[j] >= 0);
replace_column_with_only_change_at_last_rows(j, heading[j]);
if (get_status() == LU_status::Degenerated)
break;
}
}
// column j is a basis column, and there is a change in the last rows
void replace_column_with_only_change_at_last_rows(unsigned j, unsigned column_to_change_in_U) {
init_vector_w(j, m_w_for_extension);
replace_column(zero_of_type<T>(), m_w_for_extension, column_to_change_in_U);
}
bool has_dense_submatrix() const {
for (auto m : m_tail)
if (m->is_dense())
return true;
return false;
}
}; // end of lu

92
src/test/lp/lp.cpp
View file

@ -551,90 +551,7 @@ void change_basis(unsigned entering, unsigned leaving, vector<unsigned>& basis,
#ifdef Z3DEBUG
void test_small_lu(lp_settings & settings) {
std::cout << " test_small_lu" << std::endl;
static_matrix<double, double> m(3, 6);
vector<unsigned> basis(3);
basis[0] = 0;
basis[1] = 1;
basis[2] = 3;
m(0, 0) = 1; m(0, 2)= 3.9; m(2, 3) = 11; m(0, 5) = -3;
m(1, 1) = 4; m(1, 4) = 7;
m(2, 0) = 1.8; m(2, 2) = 5; m(2, 4) = 2; m(2, 5) = 8;
#ifdef Z3DEBUG
print_matrix(m, std::cout);
#endif
vector<int> heading = allocate_basis_heading(m.column_count());
vector<unsigned> non_basic_columns;
init_basis_heading_and_non_basic_columns_vector(basis, heading, non_basic_columns);
lu<static_matrix<double, double>> l(m, basis, settings);
lp_assert(l.is_correct(basis));
indexed_vector<double> w(m.row_count());
std::cout << "entering 2, leaving 0" << std::endl;
l.prepare_entering(2, w); // to init vector w
l.replace_column(0, w, heading[0]);
change_basis(2, 0, basis, non_basic_columns, heading);
// #ifdef Z3DEBUG
// std::cout << "we were factoring " << std::endl;
// print_matrix(get_B(l));
// #endif
lp_assert(l.is_correct(basis));
std::cout << "entering 4, leaving 3" << std::endl;
l.prepare_entering(4, w); // to init vector w
l.replace_column(0, w, heading[3]);
change_basis(4, 3, basis, non_basic_columns, heading);
std::cout << "we were factoring " << std::endl;
#ifdef Z3DEBUG
{
auto bl = get_B(l, basis);
print_matrix(&bl, std::cout);
}
#endif
lp_assert(l.is_correct(basis));
std::cout << "entering 5, leaving 1" << std::endl;
l.prepare_entering(5, w); // to init vector w
l.replace_column(0, w, heading[1]);
change_basis(5, 1, basis, non_basic_columns, heading);
std::cout << "we were factoring " << std::endl;
#ifdef Z3DEBUG
{
auto bl = get_B(l, basis);
print_matrix(&bl, std::cout);
}
#endif
lp_assert(l.is_correct(basis));
std::cout << "entering 3, leaving 2" << std::endl;
l.prepare_entering(3, w); // to init vector w
l.replace_column(0, w, heading[2]);
change_basis(3, 2, basis, non_basic_columns, heading);
std::cout << "we were factoring " << std::endl;
#ifdef Z3DEBUG
{
auto bl = get_B(l, basis);
print_matrix(&bl, std::cout);
}
#endif
lp_assert(l.is_correct(basis));
m.add_row();
m.add_column();
m.add_row();
m.add_column();
for (unsigned i = 0; i < m.column_count(); i++) {
m(3, i) = i;
m(4, i) = i * i; // to make the rows linearly independent
}
unsigned j = m.column_count() ;
basis.push_back(j-2);
heading.push_back(basis.size() - 1);
basis.push_back(j-1);
heading.push_back(basis.size() - 1);
auto columns_to_replace = l.get_set_of_columns_to_replace_for_add_last_rows(heading);
l.add_last_rows_to_B(heading, columns_to_replace);
lp_assert(l.is_correct(basis));
}
#endif
@ -827,10 +744,7 @@ void test_larger_lu(lp_settings& settings) {
void test_lu(lp_settings & settings) {
test_small_lu(settings);
test_larger_lu(settings);
test_larger_lu_with_holes(settings);
test_larger_lu_exp(settings);
}
#endif
@ -1785,10 +1699,6 @@ void setup_args_parser(argument_parser & parser) {
parser.add_option_with_after_string_with_help("--time_limit", "time limit in seconds");
parser.add_option_with_help_string("--mpq", "solve for rational numbers");
parser.add_option_with_after_string_with_help("--simplex_strategy", "sets simplex strategy for rational number");
parser.add_option_with_help_string("--test_lu", "test the work of the factorization");
parser.add_option_with_help_string("--test_small_lu", "test the work of the factorization on a smallish matrix");
parser.add_option_with_help_string("--test_larger_lu", "test the work of the factorization");
parser.add_option_with_help_string("--test_larger_lu_with_holes", "test the work of the factorization");
parser.add_option_with_help_string("--test_lp_0", "solve a small lp");
parser.add_option_with_help_string("--solve_some_mps", "solves a list of mps problems");
parser.add_option_with_after_string_with_help("--test_file_directory", "loads files from the directory for testing");