mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
edit tracing, add lar_solver::column_is_feasible()
This commit is contained in:
parent
4cb158a79b
commit
0fceb80e0f
|
@ -213,7 +213,7 @@ namespace lp {
|
|||
|
||||
void lar_solver::fill_explanation_from_crossed_bounds_column(explanation& evidence) const {
|
||||
lp_assert(static_cast<int>(get_column_type(m_crossed_bounds_column)) >= static_cast<int>(column_type::boxed));
|
||||
lp_assert(!m_mpq_lar_core_solver.m_r_solver.column_is_feasible(m_crossed_bounds_column));
|
||||
lp_assert(!column_is_feasible(m_crossed_bounds_column));
|
||||
|
||||
// this is the case when the lower bound is in conflict with the upper one
|
||||
const ul_pair& ul = m_columns_to_ul_pairs[m_crossed_bounds_column];
|
||||
|
@ -673,7 +673,7 @@ namespace lp {
|
|||
m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -A_r().get_val(c) * delta);
|
||||
TRACE("change_x_del",
|
||||
tout << "changed basis column " << bj << ", it is " <<
|
||||
(m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj) ? "feas" : "inf") << std::endl;);
|
||||
(column_is_feasible(bj) ? "feas" : "inf") << std::endl;);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1327,7 +1327,7 @@ namespace lp {
|
|||
became_feas.clear();
|
||||
for (unsigned j : m_mpq_lar_core_solver.m_r_solver.inf_heap()) {
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0);
|
||||
if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j))
|
||||
if (column_is_feasible(j))
|
||||
became_feas.push_back(j);
|
||||
}
|
||||
for (unsigned j : became_feas)
|
||||
|
@ -1738,16 +1738,18 @@ namespace lp {
|
|||
lconstraint_kind kind,
|
||||
const mpq& right_side,
|
||||
constraint_index constr_index) {
|
||||
TRACE("lar_solver_feas", tout << "j = " << j << " was " << (this->column_is_feasible(j)?"feas":"non-feas") << std::endl;);
|
||||
m_constraints.activate(constr_index);
|
||||
if (column_has_upper_bound(j))
|
||||
update_column_type_and_bound_with_ub(j, kind, right_side, constr_index);
|
||||
else
|
||||
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 << (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
|
||||
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,
|
||||
|
|
|
@ -481,6 +481,7 @@ class lar_solver : public column_namer {
|
|||
unsigned map_term_index_to_column_index(unsigned j) const;
|
||||
bool column_is_fixed(unsigned j) const;
|
||||
bool column_is_free(unsigned j) const;
|
||||
bool column_is_feasible(unsigned j) const { return m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j);}
|
||||
unsigned column_to_reported_index(unsigned j) const;
|
||||
lp_settings& settings();
|
||||
lp_settings const& settings() const;
|
||||
|
|
|
@ -540,29 +540,28 @@ public:
|
|||
|
||||
|
||||
void update_x_with_feasibility_tracking(unsigned j, const X & v) {
|
||||
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
|
||||
TRACE("lar_solver_feas_bug", tout << "j = " << j << ", v = " << v << "\n";);
|
||||
m_x[j] = v;
|
||||
track_column_feasibility(j);
|
||||
}
|
||||
|
||||
void add_delta_to_x_and_track_feasibility(unsigned j, const X & del) {
|
||||
TRACE("lar_solver", tout << "del = " << del << ", was x[" << j << "] = " << m_x[j] << "\n";);
|
||||
TRACE("lar_solver_feas_bug", tout << "del = " << del << ", was x[" << j << "] = " << m_x[j] << "\n";);
|
||||
m_x[j] += del;
|
||||
TRACE("lar_solver", tout << "became x[" << j << "] = " << m_x[j] << "\n";);
|
||||
TRACE("lar_solver_feas_bug", tout << "became x[" << j << "] = " << m_x[j] << "\n";);
|
||||
track_column_feasibility(j);
|
||||
}
|
||||
|
||||
void update_x(unsigned j, const X & v) {
|
||||
m_x[j] = v;
|
||||
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << (column_is_feasible(j)? " feas":" non-feas") << "\n";);
|
||||
TRACE("lar_solver_feas", tout << "not tracking feas j = " << j << ", v = " << v << (column_is_feasible(j)? " feas":" non-feas") << "\n";);
|
||||
}
|
||||
// clang-format on
|
||||
void add_delta_to_x(unsigned j, const X& delta) {
|
||||
m_x[j] += delta;
|
||||
TRACE("lar_solver", tout << "j = " << j << " v = " << m_x[j] << " delta = " << delta << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
|
||||
}
|
||||
// clang-format off
|
||||
|
||||
|
||||
void add_delta_to_x(unsigned j, const X& delta) {
|
||||
m_x[j] += delta;
|
||||
TRACE("lar_solver_feas", tout << "not tracking feas j = " << j << " v = " << m_x[j] << " delta = " << delta << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
|
||||
}
|
||||
|
||||
void track_column_feasibility(unsigned j) {
|
||||
if (column_is_feasible(j))
|
||||
remove_column_from_inf_heap(j);
|
||||
|
@ -572,7 +571,7 @@ public:
|
|||
void insert_column_into_inf_heap(unsigned j) {
|
||||
if (!m_inf_heap.contains(j)) {
|
||||
m_inf_heap.insert(j);
|
||||
TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";);
|
||||
TRACE("lar_solver_inf_heap", tout << "insert into inf_heap j = " << j << "\n";);
|
||||
}
|
||||
lp_assert(!column_is_feasible(j));
|
||||
}
|
||||
|
@ -585,7 +584,7 @@ public:
|
|||
}
|
||||
|
||||
void clear_inf_heap() {
|
||||
TRACE("lar_solver",);
|
||||
TRACE("lar_solver_feas",);
|
||||
m_inf_heap.clear();
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue