mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

more efficiend handling of rounded in cube heuristic rows

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-18 20:27:46 -07:00
parent b47e0cd4fb
commit 43758cbc66
3 changed files with 11 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/int_solver.cpp
View file

@ -266,7 +266,6 @@ lia_move int_solver::find_cube() {
// it can happen that we found an integer solution here // it can happen that we found an integer solution here
return !m_lar_solver->r_basis_has_inf_int()? lia_move::sat: lia_move::undef; return !m_lar_solver->r_basis_has_inf_int()? lia_move::sat: lia_move::undef;
} }
m_lar_solver->x_shifted_in_cube() = true;
m_lar_solver->pop(); m_lar_solver->pop();
m_lar_solver->round_to_integer_solution(); m_lar_solver->round_to_integer_solution();
m_lar_solver->set_status(lp_status::FEASIBLE); m_lar_solver->set_status(lp_status::FEASIBLE);

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

@ -27,8 +27,7 @@ void clear() {lp_assert(false); // not implemented
} }
lar_solver::lar_solver() : m_x_shifted_in_cube(false), lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
m_status(lp_status::UNKNOWN),
m_infeasible_column(-1), m_infeasible_column(-1),
m_mpq_lar_core_solver(m_settings, *this), m_mpq_lar_core_solver(m_settings, *this),
m_int_solver(nullptr), m_int_solver(nullptr),
@ -398,7 +397,7 @@ void lar_solver::pop(unsigned k) {
m_settings.simplex_strategy() = m_simplex_strategy; m_settings.simplex_strategy() = m_simplex_strategy;
lp_assert(sizes_are_correct()); lp_assert(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
lp_assert(x_shifted_in_cube() || ax_is_correct()); lp_assert(m_cube_rounded_rows.size() != 0 || ax_is_correct());
set_status(lp_status::UNKNOWN); set_status(lp_status::UNKNOWN);
} }
@ -875,7 +874,7 @@ void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(
} }
} }
void lar_solver::fix_Ax_b_on_row(unsigned i) { void lar_solver::fix_Ax_b_on_rounded_row(unsigned i) {
unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; unsigned bj = m_mpq_lar_core_solver.m_r_basis[i];
auto& v = m_mpq_lar_core_solver.m_r_x[bj]; auto& v = m_mpq_lar_core_solver.m_r_x[bj];
v = zero_of_type<numeric_pair<mpq>>(); v = zero_of_type<numeric_pair<mpq>>();
@ -884,18 +883,16 @@ void lar_solver::fix_Ax_b_on_row(unsigned i) {
v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()]; v -= c.coeff() * m_mpq_lar_core_solver.m_r_x[c.var()];
} }
} }
void lar_solver::fix_Ax_b() { void lar_solver::fix_Ax_b_on_rounded_rows() {
for (unsigned i = 0; i < A_r().row_count(); i++) { for (unsigned i : m_cube_rounded_rows) {
fix_Ax_b_on_row(i); fix_Ax_b_on_rounded_row(i);
} }
m_cube_rounded_rows.clear();
lp_assert(ax_is_correct()); lp_assert(ax_is_correct());
} }
void lar_solver::solve_with_core_solver() { void lar_solver::solve_with_core_solver() {
if (x_shifted_in_cube()) { fix_Ax_b_on_rounded_rows();
fix_Ax_b();
x_shifted_in_cube() = false;
}
if (!use_tableau()) if (!use_tableau())
add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver); add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver);
if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) { if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) {

11
src/util/lp/lar_solver.h
View file

@ -88,9 +88,7 @@ class lar_solver : public column_namer {
#endif #endif
//////////////////// fields ////////////////////////// //////////////////// fields //////////////////////////
// it is set to true when during the cube heuristic the column values got shifted vector<unsigned> m_cube_rounded_rows;
// and in this case the tableau becames invalid
bool m_x_shifted_in_cube;
lp_settings m_settings; lp_settings m_settings;
lp_status m_status; lp_status m_status;
stacked_value<simplex_strategy_enum> m_simplex_strategy; stacked_value<simplex_strategy_enum> m_simplex_strategy;
@ -119,9 +117,6 @@ public:
indexed_vector<mpq> m_column_buffer; indexed_vector<mpq> m_column_buffer;
// end of fields // end of fields
bool x_shifted_in_cube() const { return m_x_shifted_in_cube; }
bool& x_shifted_in_cube() { return m_x_shifted_in_cube; }
unsigned terms_start_index() const { return m_terms_start_index; } unsigned terms_start_index() const { return m_terms_start_index; }
const vector<lar_term*> & terms() const { return m_terms; } const vector<lar_term*> & terms() const { return m_terms; }
lar_term const& term(unsigned i) const { return *m_terms[i]; } lar_term const& term(unsigned i) const { return *m_terms[i]; }
@ -642,7 +637,7 @@ public:
lar_term get_term_to_maximize(unsigned ext_j) const; lar_term get_term_to_maximize(unsigned ext_j) const;
void set_cut_strategy(unsigned cut_frequency); void set_cut_strategy(unsigned cut_frequency);
bool sum_first_coords(const lar_term& t, mpq & val) const; bool sum_first_coords(const lar_term& t, mpq & val) const;
void fix_Ax_b(); void fix_Ax_b_on_rounded_rows();
void fix_Ax_b_on_row(unsigned); void fix_Ax_b_on_rounded_row(unsigned);
}; };
} }