mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

code cleaning around m_touched_rows of lar_solver (#6814)

Browse source
This commit is contained in:
Lev Nachmanson 2023-07-14 20:19:13 -07:00 • committed by GitHub
parent 3849f665d6
commit 401ec04ec3
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
9 changed files with 51 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/int_solver.cpp
View file

@ -358,14 +358,14 @@ int_solver::int_solver(lar_solver& lar_slv) :
// this will allow to enable and disable tracking of the pivot rows
struct check_return_helper {
lar_solver& lra;
bool m_track_pivoted_rows;
bool m_track_touched_rows;
check_return_helper(lar_solver& ls) :
lra(ls),
m_track_pivoted_rows(lra.get_track_pivoted_rows()) {
lra.set_track_pivoted_rows(false);
m_track_touched_rows(lra.touched_rows_are_tracked()) {
lra.track_touched_rows(false);
}
~check_return_helper() {
lra.set_track_pivoted_rows(m_track_pivoted_rows);
lra.track_touched_rows(m_track_touched_rows);
}
};

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

@ -16,7 +16,7 @@ namespace lp {
void lar_solver::updt_params(params_ref const& _p) {
smt_params_helper p(_p);
set_track_pivoted_rows(p.arith_bprop_on_pivoted_rows());
track_touched_rows(p.arith_bprop_on_pivoted_rows());
set_cut_strategy(p.arith_branch_cut_ratio());
m_settings.updt_params(_p);
}
@ -28,12 +28,14 @@ namespace lp {
m_term_register(true),
m_constraints(*this) {}
void lar_solver::set_track_pivoted_rows(bool v) {
m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v ? (&m_rows_with_changed_bounds) : nullptr;
// start or ends tracking the rows that were changed by solve()
void lar_solver::track_touched_rows(bool v) {
m_mpq_lar_core_solver.m_r_solver.m_touched_rows = v ? (&m_touched_rows) : nullptr;
}
bool lar_solver::get_track_pivoted_rows() const {
return m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows != nullptr;
// returns true iff the solver tracks the rows that were changed by solve()
bool lar_solver::touched_rows_are_tracked() const {
return m_mpq_lar_core_solver.m_r_solver.m_touched_rows != nullptr;
}
lar_solver::~lar_solver() {
@ -201,12 +203,6 @@ namespace lp {
return m_status;
}
solve_with_core_solver();
if (m_status != lp_status::INFEASIBLE) {
if (m_settings.bound_propagation())
detect_rows_with_changed_bounds();
}
clear_columns_with_changed_bounds();
return m_status;
}
@ -271,11 +267,11 @@ namespace lp {
clean_popped_elements(n, m_incorrect_columns);
for (auto rid : m_row_bounds_to_replay)
insert_row_with_changed_bounds(rid);
add_touched_row(rid);
m_row_bounds_to_replay.reset();
unsigned m = A_r().row_count();
clean_popped_elements(m, m_rows_with_changed_bounds);
clean_popped_elements(m, m_touched_rows);
clean_inf_heap_of_r_solver_after_pop();
lp_assert(
m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
@ -616,17 +612,11 @@ namespace lp {
left_side.push_back(std::make_pair(c, v));
}
void lar_solver::insert_row_with_changed_bounds(unsigned rid) {
m_rows_with_changed_bounds.insert(rid);
}
void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) {
for (auto& rc : m_mpq_lar_core_solver.m_r_A.m_columns[j])
insert_row_with_changed_bounds(rc.var());
void lar_solver::add_touched_row(unsigned rid) {
m_touched_rows.insert(rid);
}
bool lar_solver::use_tableau_costs() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
@ -697,9 +687,9 @@ namespace lp {
void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
if (m_mpq_lar_core_solver.m_r_heading[j] >= 0)
insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]);
add_touched_row(m_mpq_lar_core_solver.m_r_heading[j]);
else
detect_rows_of_bound_change_column_for_nbasic_column_tableau(j);
add_column_rows_to_touched_rows(j);
}
void lar_solver::detect_rows_with_changed_bounds() {
@ -710,6 +700,8 @@ namespace lp {
void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
for (auto j : m_columns_with_changed_bounds)
update_x_and_inf_costs_for_column_with_changed_bounds(j);
// whoever consumes this should clear it
m_columns_with_changed_bounds.clear();
}
@ -1170,10 +1162,10 @@ namespace lp {
ru.update();
}
void lar_solver::mark_rows_for_bound_prop(lpvar j) {
auto& column = A_r().m_columns[j];
void lar_solver::add_column_rows_to_touched_rows(lpvar j) {
const auto& column = A_r().m_columns[j];
for (auto const& r : column)
insert_row_with_changed_bounds(r.var());
add_touched_row(r.var());
}
void lar_solver::pop() {
@ -1457,8 +1449,7 @@ namespace lp {
A_r().add_row();
m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size());
m_mpq_lar_core_solver.m_r_basis.push_back(j);
if (m_settings.bound_propagation())
insert_row_with_changed_bounds(A_r().row_count() - 1);
add_touched_row(A_r().row_count() - 1);
}
else {
m_mpq_lar_core_solver.m_r_heading.push_back(-static_cast<int>(m_mpq_lar_core_solver.m_r_nbasis.size()) - 1);
@ -1545,8 +1536,7 @@ namespace lp {
var_index ret = tv::mask_term(adjusted_term_index);
if (!coeffs.empty()) {
add_row_from_term_no_constraint(m_terms.back(), ret);
if (m_settings.bound_propagation())
insert_row_with_changed_bounds(A_r().row_count() - 1);
add_touched_row(A_r().row_count() - 1);
}
lp_assert(m_var_register.size() == A_r().column_count());
if (m_need_register_terms)
@ -1594,7 +1584,7 @@ namespace lp {
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
increase_by_one_columns_with_changed_bounds();
m_incorrect_columns.increase_size_by_one();
m_rows_with_changed_bounds.increase_size_by_one();
m_touched_rows.increase_size_by_one();
add_new_var_to_core_fields_for_mpq(true);
}
@ -1745,23 +1735,20 @@ namespace lp {
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j)?"feas":"non-feas") << ", and " << (this->column_is_bounded(j)? "bounded":"non-bounded") << std::endl;);
}
// clang-format on
void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
m_columns_with_changed_bounds.insert(j);
TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
}
// clang-format off
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
lconstraint_kind kind,
const mpq& right_side,
constraint_index constr_index,
unsigned& equal_to_j) {
lconstraint_kind kind,
const mpq& right_side,
constraint_index constr_index,
unsigned& equal_to_j) {
update_column_type_and_bound(j, kind, right_side, constr_index);
equal_to_j = null_lpvar;
if (column_is_fixed(j)) {
register_in_fixed_var_table(j, equal_to_j);
}
}
constraint_index lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq& right_side) {

20
src/math/lp/lar_solver.h
View file

@ -86,7 +86,7 @@ class lar_solver : public column_namer {
constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j
u_set m_columns_with_changed_bounds;
u_set m_rows_with_changed_bounds;
u_set m_touched_rows;
unsigned_vector m_row_bounds_to_replay;
u_set m_basic_columns_with_changed_cost;
@ -190,14 +190,12 @@ class lar_solver : public column_namer {
void substitute_terms_in_linear_expression(const vector<std::pair<mpq, var_index>>& left_side_with_terms,
vector<std::pair<mpq, var_index>>& left_side) const;
void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j);
bool use_tableau_costs() const;
bool tableau_with_costs() const;
bool costs_are_used() const;
void change_basic_columns_dependend_on_a_given_nb_column(unsigned j, const numeric_pair<mpq>& delta);
void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j);
unsigned num_changed_bounds() const { return m_rows_with_changed_bounds.size(); }
void insert_row_with_changed_bounds(unsigned rid);
void add_touched_row(unsigned rid);
void detect_rows_with_changed_bounds_for_column(unsigned j);
void detect_rows_with_changed_bounds();
@ -328,11 +326,11 @@ class lar_solver : public column_namer {
void activate_check_on_equal(constraint_index, var_index&);
void activate(constraint_index);
void random_update(unsigned sz, var_index const* vars);
void mark_rows_for_bound_prop(lpvar j);
void add_column_rows_to_touched_rows(lpvar j);
template <typename T>
void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
unsigned num_prop = 0;
for (unsigned i : m_rows_with_changed_bounds) {
for (unsigned i : m_touched_rows) {
num_prop += calculate_implied_bounds_for_row(i, bp);
if (settings().get_cancel_flag())
return;
@ -342,7 +340,7 @@ class lar_solver : public column_namer {
// and add fixed columns this way
if (settings().propagate_eqs()) {
bp.clear_for_eq();
for (unsigned i : m_rows_with_changed_bounds) {
for (unsigned i : m_touched_rows) {
unsigned offset_eqs = stats().m_offset_eqs;
bp.cheap_eq_tree(i);
if (settings().get_cancel_flag())
@ -351,13 +349,13 @@ class lar_solver : public column_namer {
m_row_bounds_to_replay.push_back(i);
}
}
m_rows_with_changed_bounds.clear();
m_touched_rows.clear();
}
template <typename T>
void check_missed_propagations(lp_bound_propagator<T>& bp) {
for (unsigned i = 0; i < A_r().row_count(); i++)
if (!m_rows_with_changed_bounds.contains(i))
if (!m_touched_rows.contains(i))
if (0 < calculate_implied_bounds_for_row(i, bp)) {
verbose_stream() << i << ": " << get_row(i) << "\n";
}
@ -612,8 +610,8 @@ class lar_solver : public column_namer {
bool term_is_used_as_row(unsigned term) const;
bool tighten_term_bounds_by_delta(tv const& t, const impq&);
lar_solver();
void set_track_pivoted_rows(bool v);
bool get_track_pivoted_rows() const;
void track_touched_rows(bool v);
bool touched_rows_are_tracked() const;
~lar_solver() override;
const vector<impq>& r_x() const { return m_mpq_lar_core_solver.m_r_x; }
bool column_is_int(unsigned j) const;

3
src/math/lp/lp_core_solver_base.h
View file

@ -91,7 +91,8 @@ public:
unsigned m_basis_sort_counter;
vector<unsigned> m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
bool m_tracing_basis_changes;
u_set* m_pivoted_rows;
// these rows are changed by adding to them a multiple of the pivot row
u_set* m_touched_rows;
bool m_look_for_feasible_solution_only;
void start_tracing_basis_changes() {

6
src/math/lp/lp_core_solver_base_def.h
View file

@ -58,7 +58,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
m_upper_bounds(upper_bound_values),
m_basis_sort_counter(0),
m_tracing_basis_changes(false),
m_pivoted_rows(nullptr),
m_touched_rows(nullptr),
m_look_for_feasible_solution_only(false) {
lp_assert(bounds_for_boxed_are_set_correctly());
init();
@ -324,8 +324,8 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
return false;
}
if (m_pivoted_rows!= nullptr)
m_pivoted_rows->insert(c.var());
if (m_touched_rows!= nullptr)
m_touched_rows->insert(c.var());
}
if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)

2
src/sat/smt/arith_solver.cpp
View file

@ -396,7 +396,7 @@ namespace arith {
propagate_eqs(b.tv(), ci, k, b, value.get_rational());
#if 0
if (propagation_mode() != BP_NONE)
lp().mark_rows_for_bound_prop(b.tv().id());
lp().add_column_rows_to_touched_rows(b.tv().id());
#endif
}

2
src/smt/theory_arith.h
View file

@ -788,7 +788,7 @@ namespace smt {
//
// -----------------------------------
void mark_row_for_bound_prop(unsigned r1);
void mark_rows_for_bound_prop(theory_var v);
void add_column_rows_to_touched_rows(theory_var v);
void is_row_useful_for_bound_prop(row const & r, int & lower_idx, int & upper_idx) const;
unsigned imply_bound_for_monomial(row const & r, int idx, bool lower);
unsigned imply_bound_for_all_monomials(row const & r, bool lower);

6
src/smt/theory_arith_core.h
View file

@ -2486,7 +2486,7 @@ namespace smt {
set_bound(b, false);
if (propagation_mode() != bound_prop_mode::BP_NONE)
mark_rows_for_bound_prop(v);
add_column_rows_to_touched_rows(v);
return true;
}
@ -2534,7 +2534,7 @@ namespace smt {
set_bound(b, true);
if (propagation_mode() != bound_prop_mode::BP_NONE)
mark_rows_for_bound_prop(v);
add_column_rows_to_touched_rows(v);
return true;
}
@ -2603,7 +2603,7 @@ namespace smt {
\brief Mark all rows that contain v for bound propagation.
*/
template<typename Ext>
void theory_arith<Ext>::mark_rows_for_bound_prop(theory_var v) {
void theory_arith<Ext>::add_column_rows_to_touched_rows(theory_var v) {
for (col_entry const& ce : m_columns[v]) {
if (!ce.is_dead())
mark_row_for_bound_prop(ce.m_row_id);

2
src/smt/theory_lra.cpp
View file

@ -2989,7 +2989,7 @@ public:
}
#if 0
if (should_propagate())
lp().mark_rows_for_bound_prop(b.tv().id());
lp().add_column_rows_to_touched_rows(b.tv().id());
#endif
}