mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

rename in lar_solver and memory corruption bug in cheap_eq

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-05 16:08:49 -07:00
parent 4936ace7cd
commit 6a678fd5be
5 changed files with 28 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/int_branch.cpp
View file

@ -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);

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

@ -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;
}

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

@ -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 {

90
src/math/lp/lp_bound_propagator.h
View file

@ -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<unsigned, u_hash, u_eq> m_visited_columns;
vector<vertex> m_vertices;
map<impq, lpvar, obj_hash<impq>, impq_eq> m_offsets_to_verts;
// these maps map a column index to the corresponding index in ibounds
std::unordered_map<unsigned, unsigned> m_improved_lower_bounds;
std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
T& m_imp;
T& m_imp;
impq m_zero;
public:
vector<implied_bound> 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]);
}
}
};
}

2
src/math/lp/nra_solver.cpp
View file

@ -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.