From e9595eb2836a8878000d6b77c08c5b88c02a948a Mon Sep 17 00:00:00 2001 From: Lev Date: Sun, 29 Jul 2018 21:15:42 -0700 Subject: [PATCH] merge with z3prover Signed-off-by: Lev --- src/tactic/smtlogics/qflia_tactic.cpp | 4 --- src/util/lp/bound_propagator.cpp | 2 -- src/util/lp/lp_core_solver_base_def.h | 2 -- src/util/lp/lp_primal_core_solver.h | 24 +++++++-------- src/util/lp/static_matrix.h | 44 ++------------------------- 5 files changed, 13 insertions(+), 63 deletions(-) diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index ad5b660c3..eed4e4425 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -212,9 +212,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(preamble_st, -#if 1 - mk_smt_tactic()), -#else or_else(mk_ilp_model_finder_tactic(m), mk_pb_tactic(m), and_then(fail_if_not(mk_is_quasi_pb_probe()), @@ -222,7 +219,6 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { mk_fail_if_undecided_tactic()), mk_bounded_tactic(m), mk_smt_tactic())), -#endif main_p); diff --git a/src/util/lp/bound_propagator.cpp b/src/util/lp/bound_propagator.cpp index 199fef9b0..c4fa2aefa 100644 --- a/src/util/lp/bound_propagator.cpp +++ b/src/util/lp/bound_propagator.cpp @@ -16,8 +16,6 @@ const impq & bound_propagator::get_upper_bound(unsigned j) const { return m_lar_solver.m_mpq_lar_core_solver.m_r_upper_bounds()[j]; } void bound_propagator::try_add_bound(mpq v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { - TRACE("try_add_bound", - tout << "v = " << v << ", j = " << j << std::endl;); j = m_lar_solver.adjust_column_index_to_term_index(j); if (m_lar_solver.is_term(j)) { // lp treats terms as not having a free coefficient, restoring it below for the outside consumption diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h index ddae7bf20..f9c1ae632 100644 --- a/src/util/lp/lp_core_solver_base_def.h +++ b/src/util/lp/lp_core_solver_base_def.h @@ -108,8 +108,6 @@ pivot_to_reduced_costs_tableau(unsigned i, unsigned j) { if (r.var() != j) m_d[r.var()] -= a * r.get_val(); } -ls - a = zero_of_type(); // zero the pivot column's m_d finally } diff --git a/src/util/lp/lp_primal_core_solver.h b/src/util/lp/lp_primal_core_solver.h index 2700fc168..d93174bc4 100644 --- a/src/util/lp/lp_primal_core_solver.h +++ b/src/util/lp/lp_primal_core_solver.h @@ -280,17 +280,14 @@ public: if (m_bland_mode_tableau) return find_beneficial_column_in_row_tableau_rows_bland_mode(i, a_ent); // a short row produces short infeasibility explanation and benefits at least one pivot operation - int choice = -1; - int nchoices = 0; + vector*> choices; + unsigned num_of_non_free_basics = 1000000; unsigned len = 100000000; unsigned bj = this->m_basis[i]; bool bj_needs_to_grow = needs_to_grow(bj); for (unsigned k = 0; k < this->m_A.m_rows[i].m_cells.size(); k++) { const row_cell& rc = this->m_A.m_rows[i].m_cells[k]; if (rc.dead()) continue; - const row_cell& rc = this->m_A.m_rows[i].m_cells[k]; - if (rc.dead()) continue; ->>>>>>> e6c612f... trying the new scheme in static_matrix : in progress unsigned j = rc.var(); if (j == bj) continue; @@ -305,23 +302,24 @@ public: if (damage < num_of_non_free_basics) { num_of_non_free_basics = damage; len = this->m_A.m_columns[j].live_size(); - choice = k; - nchoices = 1; + choices.clear(); + choices.push_back(&rc); } else if (damage == num_of_non_free_basics && - this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % (++nchoices))) { - choice = k; + this->m_A.m_columns[j].live_size() <= len && (this->m_settings.random_next() % 2)) { + choices.push_back(&rc); len = this->m_A.m_columns[j].live_size(); } } - if (choice == -1) { + if (choices.size() == 0) { m_inf_row_index_for_tableau = i; return -1; } - const row_cell& rc = this->m_A.m_rows[i].m_cells[choice]; - a_ent = rc.coeff(); - return rc.var(); + const row_cell* rc = choices.size() == 1? choices[0] : + choices[this->m_settings.random_next() % choices.size()]; + a_ent = rc->coeff(); + return rc->var(); } static X positive_infinity() { return convert_struct::convert(std::numeric_limits::max()); diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h index 036f628b7..c75fa4ce8 100644 --- a/src/util/lp/static_matrix.h +++ b/src/util/lp/static_matrix.h @@ -64,9 +64,6 @@ public: bool alive() const { return !dead(); } bool dead() const { return m_i == static_cast(-1); } void set_dead() { m_i = -1;} - - - }; template @@ -79,6 +76,7 @@ public: } row_cell(unsigned j, T const & val) : m_j(j), m_value(val) { } + const T & get_val() const { lp_assert(alive()); return m_value; @@ -126,8 +124,6 @@ public: bool alive() const { return !dead(); } bool dead() const { return m_j == static_cast(-1); } void set_dead() { m_j = static_cast(-1); } - - }; template @@ -252,10 +248,6 @@ public: return m_live_size; } - unsigned cells_size() const { - return m_cells.size(); - } - unsigned cells_size() const { return m_cells.size(); } @@ -304,7 +296,7 @@ public: } m_cells.pop_back(); } - + bool is_correct() const { std::set d0; std::set d1; unsigned alive = 0; @@ -341,38 +333,6 @@ public: lp_assert(is_correct()); } - void swap_with_head_cell(unsigned i) { - lp_assert(i > 0); - lp_assert(m_cells[i].alive()); - column_cell head_copy = m_cells[0]; - if (head_copy.dead()) { - if (m_first_dead == 0) { - m_first_dead = i; - } else { - column_cell * c = &m_cells[m_first_dead]; - for (; c->next_dead_index() != 0; c = &m_cells[c->next_dead_index()]); - lp_assert(c->next_dead_index() == 0); - c->next_dead_index() = i; - } - } - m_cells[0] = m_cells[i]; - m_cells[i] = head_copy; - lp_assert(is_correct()); - } - - column_cell & add_cell(unsigned i, unsigned & index) { - if (m_first_dead != -1) { - auto & ret = m_cells[index = m_first_dead]; - m_first_dead = ret.next_dead_index(); - m_live_size++; - ret.var() = i; - return ret; - } - lp_assert(m_live_size == m_cells.size()); - index = m_live_size++; - m_cells.push_back(column_cell(i)); - return m_cells.back(); - } column_cell & add_cell(unsigned i, unsigned & index) { if (m_first_dead != -1) { auto & ret = m_cells[index = m_first_dead];