mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add TRACE stmts, more efficient remove from inf_heap
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
167e0dc66d
commit
ff875c936f
|
@ -393,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);
|
||||
}
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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);
|
||||
|
|
Loading…
Reference in a new issue