From 6a678fd5be17f3672e98ae01ac21ced5cbb5dd38 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 5 Jun 2020 16:08:49 -0700 Subject: [PATCH] rename in lar_solver and memory corruption bug in cheap_eq Signed-off-by: Lev Nachmanson --- src/math/lp/int_branch.cpp | 2 +- src/math/lp/lar_solver.cpp | 16 +++--- src/math/lp/lar_solver.h | 4 +- src/math/lp/lp_bound_propagator.h | 90 +++++-------------------------- src/math/lp/nra_solver.cpp | 2 +- 5 files changed, 28 insertions(+), 86 deletions(-) diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp index 31c5274f9..347d5a47a 100644 --- a/src/math/lp/int_branch.cpp +++ b/src/math/lp/int_branch.cpp @@ -34,7 +34,7 @@ lia_move int_branch::create_branch_on_column(int j) { TRACE("check_main_int", tout << "branching" << std::endl;); lp_assert(lia.m_t.is_empty()); lp_assert(j != -1); - lia.m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j)); + lia.m_t.add_monomial(mpq(1), lra.column_to_reported_index(j)); if (lia.is_free(j)) { lia.m_upper = lia.random() % 2; lia.m_k = mpq(0); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 5f757747e..44cec7ed0 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -157,13 +157,17 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { } } -unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { +// Returns the column index without changes, +// but in the case the column was created as +// the slack variable to a term return the term index. +// It is the same index that was returned by add_var(), or +// by add_term() +unsigned lar_solver::column_to_reported_index(unsigned j) const { SASSERT(j < m_var_register.size()); - if (!tv::is_term(j)) { - unsigned ext_var_or_term = m_var_register.local_to_external(j); - j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term; - } else { - UNREACHABLE(); + SASSERT(!tv::is_term(j)); + unsigned ext_var_or_term = m_var_register.local_to_external(j); + if (tv::is_term(ext_var_or_term)) { + j = ext_var_or_term; } return j; } diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 4c3a7ac4d..573a9be41 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -460,7 +460,7 @@ public: unsigned map_term_index_to_column_index(unsigned j) const; bool column_is_fixed(unsigned j) const; bool column_is_free(unsigned j) const; - unsigned adjust_column_index_to_term_index(unsigned j) const; + unsigned column_to_reported_index(unsigned j) const; lp_settings & settings(); lp_settings const & settings() const; column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; } @@ -511,7 +511,7 @@ public: } inline tv column2tv(column_index const& c) const { - return tv::raw(adjust_column_index_to_term_index(c)); + return tv::raw(column_to_reported_index(c)); } inline std::ostream& print_column_info(unsigned j, std::ostream& out) const { diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index a919537fb..bf0b7413d 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -36,8 +36,7 @@ class lp_bound_propagator { m_offset(offset), m_id(id), m_parent(-1), - m_level(0) - {} + m_level(0) {} unsigned index_in_row() const { return m_index_in_row; } unsigned id() const { return m_id; } unsigned row() const { return m_row; } @@ -64,14 +63,14 @@ class lp_bound_propagator { hashtable m_visited_columns; vector m_vertices; map, impq_eq> m_offsets_to_verts; - // these maps map a column index to the corresponding index in ibounds std::unordered_map m_improved_lower_bounds; std::unordered_map m_improved_upper_bounds; - T& m_imp; + T& m_imp; + impq m_zero; public: vector m_ibounds; - lp_bound_propagator(T& imp): m_imp(imp) {} + lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {} const lar_solver& lp() const { return m_imp.lp(); } column_type get_column_type(unsigned j) const { return m_imp.lp().get_column_type(j); @@ -86,7 +85,7 @@ public: } void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { - j = m_imp.lp().adjust_column_index_to_term_index(j); + j = m_imp.lp().column_to_reported_index(j); lconstraint_kind kind = is_low? GE : LE; if (strict) @@ -137,7 +136,7 @@ public: } vertex xv(row_index, x, // index in row - impq(0), // offset + m_zero, // offset 0 // id ); push_vertex(xv); @@ -193,6 +192,7 @@ public: } void clear_for_eq() { + // todo: do not clear the first two? m_visited_rows.reset(); m_visited_columns.reset(); m_vertices.reset(); @@ -218,8 +218,8 @@ public: lpvar v_j_col = get_column(m_vertices[v_j]); if (lp().column_is_int(v_i_col) != lp().column_is_int(v_j_col)) return; - unsigned i_e = lp().adjust_column_index_to_term_index(v_i_col); - unsigned j_e = lp().adjust_column_index_to_term_index(v_j_col); + unsigned i_e = lp().column_to_reported_index(v_i_col); + unsigned j_e = lp().column_to_reported_index(v_j_col); m_imp.add_eq(i_e, j_e, exp); } @@ -312,69 +312,6 @@ public: return true; } - // // offset is measured from the initial vertex in the search - // void search_for_collision(const vertex& v, const impq& offset) { - // TRACE("cheap_eq", tout << "v_i = " ; v.print(tout) << "\noffset = " << offset << "\n";); - // unsigned registered_vert; - - // if (m_offsets_to_verts.find(offset, registered_vert)) { - // if (registered_vert != v.id()) - // report_eq(registered_vert, v.id()); - // } else { - // m_offsets_to_verts.insert(offset, v.id()); - // } - // lpvar j = get_column(v); - // if (m_visited_columns.contains(j)) - // return; - // m_visited_columns.insert(j); - // for (const auto & c : lp().get_column(j)) { - // if (m_visited_rows.contains(c.var())) - // continue; - // m_visited_rows.insert(c.var()); - // unsigned x_index, y_index; - // impq row_offset; - // if (!is_offset_row(c.var(), x_index, y_index, row_offset)) - // return; - // TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, c.var());); - // if (lp().get_row(c.var())[x_index].var() == j) { // conected to x - // add_column_edge(v.id(), c.var(), x_index); - // add_row_edge(offset, c.var(), x_index, y_index, row_offset); - // } else { // connected to y - // add_column_edge(v.id(), c.var(), y_index); - // add_row_edge(offset - // } - // } - // } - - // row[x_index] gives x, and row[y_index] gives y - // offset is accumulated during the recursion - // edge_offset is the one in x - y = edge_offset - // The parent is taken from m_vertices.back() - // void add_row_edge(const impq& offset, - // unsigned row_index, - // unsigned x_index, - // unsigned y_index, - // const impq& row_offset) { - // TRACE("cheap_eq", tout << "offset = " << offset << - // " , row_index = " << row_index << ", x_index = " << x_index << ", y_index = " << y_index << ", row_offset = " << row_offset << "\n"; ); - // unsigned parent_id = m_vertices.size() - 1; - // vertex xv(row_index, x_index, offset, parent_id + 1); - // if (parent_id != UINT_MAX) { - // m_vertices[parent_id].add_child(xv); - // } - // push_vertex(xv); - // vertex yv(row_index, y_index, offset + row_offset, parent_id + 2); - // xv.add_child(yv); - // push_vertex(yv); - // TRACE("cheap_eq", print_tree(tout);); - // m_visited_rows.insert(row_index); - // search_for_collision(xv, offset); - // TRACE("cheap_eq", print_tree(tout);); - // SASSERT(tree_is_correct()); - // search_for_collision(yv, offset + row_offset); - // SASSERT(tree_is_correct()); - // } - void push_vertex(const vertex& v) { TRACE("cheap_eq", tout << "v = "; v.print(tout);); SASSERT(!m_vertices.contains(v)); @@ -394,8 +331,8 @@ public: } void try_create_eq(unsigned row_index) { - clear_for_eq(); TRACE("cheap_eq", tout << "row_index = " << row_index << "\n";); + clear_for_eq(); unsigned x_index, y_index; impq offset; if (!is_offset_row(row_index, x_index, y_index, offset)) @@ -453,12 +390,13 @@ public: void explore_under(vertex& v) { SASSERT(v.children().size() <= 1); // because we have not collected the vertices // from the column, so there might be only one child from the row - check_for_eq_and_add_to_offset_table(v); + check_for_eq_and_add_to_offset_table(v); + unsigned v_id = v.id(); go_over_vertex_column(v); - for (unsigned j : v.children()) { + // v might change in m_vertices expansion + for (unsigned j : m_vertices[v_id].children()) { explore_under(m_vertices[j]); } } - }; } diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index f741a04f7..1b8f37fe5 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -196,7 +196,7 @@ struct solver::imp { } // void add_term(unsigned term_column) { - lp::tv ti = lp::tv::raw(s.adjust_column_index_to_term_index(term_column)); + lp::tv ti = lp::tv::raw(s.column_to_reported_index(term_column)); const lp::lar_term& t = s.get_term(ti); // code that creates a polynomial equality between the linear coefficients and // variable representing the term.