mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

improve tracing and a small fix in

Browse source 
lp_core_solver_base::make_column_feasible
This commit is contained in:
Lev Nachmanson 2023-07-04 13:23:56 -07:00
parent 8a49cf62f4
commit e360de6d71
3 changed files with 139 additions and 143 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1810,7 +1810,12 @@ namespace lp {
else else
update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index); update_column_type_and_bound_with_no_ub(j, kind, right_side, constr_index);
} }
// 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";);
}
// clang-format off
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j, void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
lconstraint_kind kind, lconstraint_kind kind,
const mpq& right_side, const mpq& right_side,
@ -1900,117 +1905,110 @@ namespace lp {
} }
} }
// clang-format on
void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j)); lp_assert(column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed || lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed ||
m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed); m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: case LT:
y_of_bound = -1; y_of_bound = -1;
case LE: case LE: {
{ auto up = numeric_pair<mpq>(right_side, y_of_bound);
auto up = numeric_pair<mpq>(right_side, y_of_bound); if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { set_infeasible_column(j);
set_infeasible_column(j); }
} if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return;
if (up >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) return; m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; set_upper_bound_witness(j, ci);
set_upper_bound_witness(j, ci); insert_to_columns_with_changed_bounds(j);
insert_to_columns_with_changed_bounds(j); } break;
} case GT:
break; y_of_bound = 1;
case GT: case GE: {
y_of_bound = 1; auto low = numeric_pair<mpq>(right_side, y_of_bound);
case GE: if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
{ set_infeasible_column(j);
auto low = numeric_pair<mpq>(right_side, y_of_bound); }
if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j); return;
} }
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
return; set_lower_bound_witness(j, ci);
} m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; insert_to_columns_with_changed_bounds(j);
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
}
break;
case EQ:
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
break;
}
default: } break;
UNREACHABLE(); case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j);
}
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
break;
}
default:
UNREACHABLE();
} }
if (m_mpq_lar_core_solver.m_r_upper_bounds[j] == m_mpq_lar_core_solver.m_r_lower_bounds[j]) { if (m_mpq_lar_core_solver.m_r_upper_bounds[j] == m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
} }
} }
// clang-format off
void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j)); lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: case LT:
y_of_bound = -1; y_of_bound = -1;
case LE: case LE: {
{ auto up = numeric_pair<mpq>(right_side, y_of_bound);
auto up = numeric_pair<mpq>(right_side, y_of_bound); if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { set_infeasible_column(j);
set_infeasible_column(j); }
} m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; set_upper_bound_witness(j, ci);
set_upper_bound_witness(j, ci); m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j] ? column_type::fixed : column_type::boxed);
insert_to_columns_with_changed_bounds(j); insert_to_columns_with_changed_bounds(j);
m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j] ? column_type::fixed : column_type::boxed);
} } break;
break; case GT:
case GT: y_of_bound = 1;
y_of_bound = 1; case GE: {
case GE: auto low = numeric_pair<mpq>(right_side, y_of_bound);
{ if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
auto low = numeric_pair<mpq>(right_side, y_of_bound); return;
if (low < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { }
return; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
} set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; insert_to_columns_with_changed_bounds(j);
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); } break;
} case EQ: {
break; auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
case EQ: if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
{ set_infeasible_column(j);
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>()); }
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
set_infeasible_column(j); set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
} }
set_upper_bound_witness(j, ci); default:
set_lower_bound_witness(j, ci); UNREACHABLE();
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
} }
default:
UNREACHABLE();
}
} }
// clang-format off
void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j)); lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
@ -2036,9 +2034,10 @@ namespace lp {
set_infeasible_column(j); set_infeasible_column(j);
} }
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low; m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci); set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed); m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
insert_to_columns_with_changed_bounds(j);
} }
break; break;
case EQ: case EQ:
@ -2059,48 +2058,44 @@ namespace lp {
UNREACHABLE(); UNREACHABLE();
} }
} }
// clang-format on
void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j)); lp_assert(!column_has_lower_bound(j) && !column_has_upper_bound(j));
insert_to_columns_with_changed_bounds(j);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: case LT:
y_of_bound = -1; y_of_bound = -1;
case LE: case LE: {
{ auto up = numeric_pair<mpq>(right_side, y_of_bound);
auto up = numeric_pair<mpq>(right_side, y_of_bound); m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; set_upper_bound_witness(j, ci);
set_upper_bound_witness(j, ci); m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound;
m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound; } break;
} case GT:
break; y_of_bound = 1;
case GT: case GE: {
y_of_bound = 1; auto low = numeric_pair<mpq>(right_side, y_of_bound);
case GE: m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
{ set_lower_bound_witness(j, ci);
auto low = numeric_pair<mpq>(right_side, y_of_bound); m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
insert_to_columns_with_changed_bounds(j);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
}
break;
case EQ:
{
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
}
default: } break;
UNREACHABLE(); case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
set_upper_bound_witness(j, ci);
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_r_upper_bounds[j] = m_mpq_lar_core_solver.m_r_lower_bounds[j] = v;
m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
break;
}
default:
UNREACHABLE();
} }
insert_to_columns_with_changed_bounds(j);
} }
// clang-format off
bool lar_solver::column_corresponds_to_term(unsigned j) const { bool lar_solver::column_corresponds_to_term(unsigned j) const {
return tv::is_term(m_var_register.local_to_external(j)); return tv::is_term(m_var_register.local_to_external(j));
} }
@ -2204,8 +2199,8 @@ namespace lp {
} }
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq& rs, constraint_index& ci, bool& upper_bound) const { bool lar_solver::get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq& rs, constraint_index& ci, bool& upper_bound) const {
lp_assert(t.is_term()) lp_assert(t.is_term());
unsigned j; unsigned j;
bool is_int; bool is_int;
if (!m_var_register.external_is_used(t.index(), j, is_int)) if (!m_var_register.external_is_used(t.index(), j, is_int))
return false; // the term does not have a bound because it does not correspond to a column return false; // the term does not have a bound because it does not correspond to a column

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

@ -135,8 +135,7 @@ class lar_solver : public column_namer {
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); } inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); }
inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); } inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); }
inline void insert_to_columns_with_changed_bounds(unsigned j) { m_columns_with_changed_bounds.insert(j); } void insert_to_columns_with_changed_bounds(unsigned j);
void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index, unsigned&); void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index, unsigned&);
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index); void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);
void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index); void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);

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

@ -310,8 +310,7 @@ public:
if (x < m_lower_bounds[j]) { if (x < m_lower_bounds[j]) {
delta = m_lower_bounds[j] - x; delta = m_lower_bounds[j] - x;
ret = true;; ret = true;;
} } else if (x > m_upper_bounds[j]) {
if (x > m_upper_bounds[j]) {
delta = m_upper_bounds[j] - x; delta = m_upper_bounds[j] - x;
ret = true; ret = true;
} }
@ -554,14 +553,15 @@ public:
} }
void update_x(unsigned j, const X & v) { void update_x(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
m_x[j] = v; m_x[j] = v;
TRACE("lar_solver", tout << "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) { void add_delta_to_x(unsigned j, const X& delta) {
TRACE("lar_solver", tout << "j = " << j << ", delta = " << delta << "\n";); m_x[j] += 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 track_column_feasibility(unsigned j) { void track_column_feasibility(unsigned j) {
if (column_is_feasible(j)) if (column_is_feasible(j))
@ -570,15 +570,17 @@ public:
insert_column_into_inf_heap(j); insert_column_into_inf_heap(j);
} }
void insert_column_into_inf_heap(unsigned j) { void insert_column_into_inf_heap(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";); if (!m_inf_heap.contains(j)) {
if (!m_inf_heap.contains(j))
m_inf_heap.insert(j); m_inf_heap.insert(j);
TRACE("lar_solver", tout << "j = " << j << "\n";);
}
lp_assert(!column_is_feasible(j)); lp_assert(!column_is_feasible(j));
} }
void remove_column_from_inf_heap(unsigned j) { void remove_column_from_inf_heap(unsigned j) {
TRACE("lar_solver", tout << "j = " << j << "\n";); if (m_inf_heap.contains(j)) {
if (m_inf_heap.contains(j)) TRACE("lar_solver", tout << "j = " << j << "\n";);
m_inf_heap.erase(j); m_inf_heap.erase(j);
}
lp_assert(column_is_feasible(j)); lp_assert(column_is_feasible(j));
} }