diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 60184962f..b72b88f55 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1380,72 +1380,6 @@ namespace lp { return m_mpq_lar_core_solver.column_is_free(j); } - // column is at lower or upper bound, lower and upper bound are different. - // the lower/upper bound is not strict. - // the LP obtained by making the bound strict is infeasible - // -> the column has to be fixed - bool lar_solver::is_fixed_at_bound(column_index const& j, vector>& bounds) { - if (column_is_fixed(j)) - return false; - mpq val; - if (!has_value(j, val)) - return false; - lp::lconstraint_kind k; - if (column_has_upper_bound(j) && - get_upper_bound(j).x == val) { - push(); - k = column_is_int(j) ? LE : LT; - auto ci = mk_var_bound(j, k, column_is_int(j) ? val - 1 : val); - update_column_type_and_bound(j, k, column_is_int(j) ? val - 1 : val, ci); - auto st = find_feasible_solution(); - bool infeasible = st == lp_status::INFEASIBLE; - if (infeasible) { - explanation exp; - get_infeasibility_explanation(exp); - unsigned_vector cis; - exp.remove(ci); - verbose_stream() << "tight upper bound " << j << " " << val << "\n"; - bounds.push_back({exp, j, true, val}); - } - pop(1); - return infeasible; - } - if (column_has_lower_bound(j) && - get_lower_bound(j).x == val) { - push(); - k = column_is_int(j) ? GE : GT; - auto ci = mk_var_bound(j, k, column_is_int(j) ? val + 1 : val); - update_column_type_and_bound(j, k, column_is_int(j) ? val + 1 : val, ci); - auto st = find_feasible_solution(); - bool infeasible = st == lp_status::INFEASIBLE; - if (infeasible) { - explanation exp; - get_infeasibility_explanation(exp); - exp.remove(ci); - verbose_stream() << "tight lower bound " << j << " " << val << "\n"; - bounds.push_back({exp, j, false, val}); - } - pop(1); - return infeasible; - } - - return false; - } - - bool lar_solver::has_fixed_at_bound(vector>& bounds) { - verbose_stream() << "has-fixed-at-bound\n"; - for (unsigned j = 0; j < A_r().m_columns.size(); ++j) { - auto ci = column_index(j); - if (is_fixed_at_bound(ci, bounds)) - verbose_stream() << "fixed " << j << "\n"; - } - verbose_stream() << "num fixed " << bounds.size() << "\n"; - if (!bounds.empty()) - find_feasible_solution(); - return !bounds.empty(); - } - - // below is the initialization functionality of lar_solver bool lar_solver::strategy_is_undecided() const { diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index a257ae4e8..fd6fef8fd 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -364,9 +364,6 @@ class lar_solver : public column_namer { } } - bool is_fixed_at_bound(column_index const& j, vector>& bounds); - bool has_fixed_at_bound(vector>& bounds); - bool is_fixed(column_index const& j) const { return column_is_fixed(j); } inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } bool external_is_used(unsigned) const; @@ -396,10 +393,6 @@ class lar_solver : public column_namer { m_mpq_lar_core_solver.m_r_solver.inf_heap().clear(); } - inline void remove_column_from_inf_set(unsigned j) { - m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_heap(j); - } - void pivot(int entering, int leaving) { m_mpq_lar_core_solver.pivot(entering, leaving); } diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h index d05d34753..00d079f77 100644 --- a/src/math/lp/lp_core_solver_base.h +++ b/src/math/lp/lp_core_solver_base.h @@ -55,7 +55,7 @@ private: lp_status m_status; public: bool current_x_is_feasible() const { - TRACE("feas", + TRACE("feas_bug", if (!m_inf_heap.empty()) { tout << "column " << *m_inf_heap.begin() << " is infeasible" << std::endl; print_column_info(*m_inf_heap.begin(), tout); @@ -572,13 +572,13 @@ public: void insert_column_into_inf_heap(unsigned j) { if (!m_inf_heap.contains(j)) { m_inf_heap.insert(j); - TRACE("lar_solver", tout << "j = " << j << "\n";); + TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";); } lp_assert(!column_is_feasible(j)); } void remove_column_from_inf_heap(unsigned j) { if (m_inf_heap.contains(j)) { - TRACE("lar_solver", tout << "j = " << j << "\n";); + TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";); m_inf_heap.erase(j); } lp_assert(column_is_feasible(j)); diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h index 2a4a278a6..79e0d7590 100644 --- a/src/math/lp/lp_primal_core_solver.h +++ b/src/math/lp/lp_primal_core_solver.h @@ -341,6 +341,7 @@ namespace lp { int find_smallest_inf_column() { if (this->inf_heap().empty()) return -1; + return this->inf_heap().min_value(); } @@ -393,7 +394,10 @@ namespace lp { const X &new_val_for_leaving = get_val_for_leaving(leaving); X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent; this->m_x[leaving] = new_val_for_leaving; - this->remove_column_from_inf_heap(leaving); + // this will remove the leaving from the heap + TRACE("lar_solver_inf_heap", tout << "leaving = " << leaving + << " removed from inf_heap()\n";); + this->inf_heap().erase_min(); advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta); if (this->current_x_is_feasible()) this->set_status(lp_status::OPTIMAL); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5372a3b33..b21424e65 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1659,10 +1659,7 @@ public: unsigned old_idx = m_final_check_idx; switch (is_sat) { case l_true: - TRACE("arith", display(tout)); - - // if (lp().has_fixed_at_bound()) // explain and propagate. - + TRACE("arith", display(tout)); #if 0 m_dist.reset(); m_dist.push(0, 1);