mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

a small example passing with cheap eqs

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-05 13:22:09 -07:00
parent 54921d08dc
commit 0ff18dd5a7
1 changed files with 182 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,19 +10,20 @@ namespace lp {
template <typename T>
class lp_bound_propagator {
struct impq_eq { bool operator()(const impq& a, const impq& b) const {return a == b;}};
// Pairs (row,x), (row,y) such that there is the
// row is x - y = c, where c is a constant form a tree.
// The edges of the tree are of the form ((row,x), (row, y)) as from above,
// or ((row, x), (other_row, x)) where the "other_row" is an offset row too.
// vertex represents a pair (row,x) or (row,y) for an offset row.
// The set of all pair are organised in a tree.
// The edges of the tree are of the form ((row,x), (row, y)) for an offset row,
// or ((row, u), (other_row, v)) where the "other_row" is an offset row too,
// and u, v reference the same column
class vertex {
unsigned m_row;
unsigned m_index_in_row; // in the row
bool m_sign; // true if the vertex plays the role of y
vector<unsigned> m_children; // point to m_vertices
svector<unsigned> m_children; // point to m_vertices
impq m_offset; // offset from parent (parent - child = offset)
unsigned m_id; // the index in m_vertices
unsigned m_parent;
unsigned m_level; // the number of hops from the root to reach the vertex,
unsigned m_level; // the distance in hops to the root;
// it is handy to find the common ancestor
public:
vertex() {}
@ -42,15 +43,22 @@ class lp_bound_propagator {
unsigned row() const { return m_row; }
unsigned parent() const { return m_parent; }
unsigned level() const { return m_level; }
const impq& offset() const { return m_offset; }
void add_child(vertex& child) {
child.m_parent = m_id;
m_children.push_back(child.m_id);
child.m_level = m_level + 1;
}
}
const svector<unsigned> & children() const { return m_children; }
std::ostream& print(std::ostream & out) const {
out << "row = " << m_row << ", m_index_in_row = " << m_index_in_row << ", parent = " << (int)m_parent << " , offset = " << m_offset << ", id = " << m_id << ", level = " << m_level << "\n";;
return out;
}
#ifdef Z3DEBUG
bool operator==(const vertex& o) const {
return m_row == o.m_row && m_index_in_row == o.m_index_in_row;
}
#endif
};
hashtable<unsigned, u_hash, u_eq> m_visited_rows;
hashtable<unsigned, u_hash, u_eq> m_visited_columns;
@ -132,23 +140,23 @@ public:
impq(0), // offset
0 // id
);
push_to_verts(xv);
push_vertex(xv);
vertex yv(row_index,
y, // index in row
offset,
1 // id
);
push_to_verts(yv);
push_vertex(yv);
xv.add_child(yv);
TRACE("cheap_eq", print_tree(tout););
SASSERT(tree_is_correct());
}
bool is_offset_row(unsigned row_index,
unsigned & x_index,
lpvar & y_index,
impq& offset) const {
x_index = y_index = UINT_MAX;
const auto & row = lp().get_row(row_index);
for (unsigned k = 0; k < row.size(); k++) {
const auto& c = row[k];
@ -172,17 +180,14 @@ public:
return true;
}
void add_eq(lpvar j, lpvar k) {
NOT_IMPLEMENTED_YET();
}
void check_for_eq_and_add_to_offset_table(lpvar j, const impq & offset) {
lpvar k;
if (m_offsets_to_verts.find(offset, k)) {
SASSERT(j != k);
add_eq(j, k);
void check_for_eq_and_add_to_offset_table(const vertex& v) {
unsigned k; // the other vertex index
if (m_offsets_to_verts.find(v.offset(), k)) {
if (k != v.id())
report_eq(k, v.id());
} else {
m_offsets_to_verts.insert(offset, j);
TRACE("cheap_eq", tout << "registered offset " << v.offset() << " to " << v.id() << "\n";);
m_offsets_to_verts.insert(v.offset(), v.id());
}
}
@ -197,9 +202,8 @@ public:
// we have v_i and v_j, indices of vertices at the same offsets
void report_eq(unsigned v_i, unsigned v_j) {
SASSERT(v_i != v_j);
const vertex& u = m_vertices[v_i];
const vertex& v = m_vertices[v_j];
TRACE("cheap_eq", tout << "v_i = " << v_i << ", v_j = " << v_j << "\nu = "; u.print(tout) << "\nv = "; v.print(tout) <<"\n";);
TRACE("cheap_eq", tout << "v_i = " << v_i << ", v_j = " << v_j << "\nu = ";
m_vertices[v_i].print(tout) << "\nv = "; m_vertices[v_j].print(tout) <<"\n";);
svector<unsigned> path;
find_path_on_tree(path, v_i, v_j);
TRACE("cheap_eq", tout << "path = \n";
@ -209,10 +213,46 @@ public:
}
display_row_of_vertex(v_j, tout);
);
NOT_IMPLEMENTED_YET();
lp::explanation exp = get_explanation_from_path(v_i, path, v_j);
unsigned i_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_i]));
unsigned j_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_j]));
m_imp.add_eq(i_e, j_e, exp);
}
explanation get_explanation_from_path(unsigned v_i,
const svector<unsigned>& path,
unsigned v_j) const {
explanation ex;
unsigned row = m_vertices[v_i].row();
unsigned prev_row = row;
explain_fixed_in_row(row, ex);
for (unsigned k : path) {
row = m_vertices[k].row();
if (row == prev_row)
continue;
prev_row = row;
explain_fixed_in_row(row, ex);
}
row = m_vertices[v_j].row();
if (prev_row != row)
explain_fixed_in_row(row, ex);
return ex;
}
void explain_fixed_in_row(unsigned row, explanation& ex) const {
constraint_index lc, uc;
for (const auto & c : lp().get_row(row)) {
lpvar j = c.var();
if (lp().is_fixed(j)) {
lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
ex.push_back(lc);
ex.push_back(uc);
}
}
}
std::ostream& display_row_of_vertex(unsigned k, std::ostream& out) const {
m_vertices[k].print(out);
return lp().get_int_solver()->display_row_info(out,m_vertices[k].row() );
}
// the path will not include the start and the end
@ -268,77 +308,77 @@ 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;
// // 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;
add_column_edge(v.id(), c.var(), x_index);
add_row_edge(offset, v.row(), x_index, y_index, row_offset);
}
}
// 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_to_verts(xv);
vertex yv(row_index, y_index, offset + row_offset, parent_id + 2);
xv.add_child(yv);
push_to_verts(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 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_to_verts(const vertex& v) {
void push_vertex(const vertex& v) {
TRACE("cheap_eq", tout << "v = "; v.print(tout););
SASSERT(!m_vertices.contains(v));
m_vertices.push_back(v);
}
void add_column_edge(unsigned parent, unsigned row_index, unsigned index_in_row) {
TRACE("cheap_eq", tout << "parent=" << parent << ", row_index = " << row_index << "\n";);
vertex v(row_index, index_in_row, impq(0), m_vertices.size());
m_vertices[parent].add_child(v);
push_to_verts(v);
TRACE("cheap_eq", tout << "tree = "; print_tree(tout););
SASSERT(tree_is_correct());
}
std::ostream& print_tree(std::ostream & out) const {
for (auto & v : m_vertices) {
v.print(out);
@ -356,8 +396,65 @@ public:
impq offset;
if (!is_offset_row(row_index, x_index, y_index, offset))
return;
add_row_edge(impq(0), row_index, x_index, y_index, offset);
TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
vertex root(row_index, x_index, impq(0), 0 /* id */);
push_vertex(root);
vertex v_y(row_index, y_index, offset, 1);
root.add_child(v_y);
push_vertex(v_y);
SASSERT(tree_is_correct());
m_visited_rows.insert(row_index);
explore_under(root);
TRACE("cheap_eq", tout << "done for row_index " << row_index << "\n";);
}
void go_over_vertex_column(vertex & v) {
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)) {
unsigned row_index = c.var();
if (m_visited_rows.contains(row_index))
continue;
m_visited_rows.insert(row_index);
unsigned x_index, y_index;
impq row_offset;
if (!is_offset_row(row_index, x_index, y_index, row_offset))
continue;
TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
// who is it the same column?
if (lp().get_row(row_index)[x_index].var() == j) { // conected to x
vertex x_v(row_index, x_index, v.offset(), m_vertices.size());
v.add_child(x_v);
vertex y_v(row_index, y_index, v.offset() + row_offset, m_vertices.size() + 1);
x_v.add_child(y_v);
push_vertex(x_v); // no need to explore from x_v
push_vertex(y_v);
SASSERT(tree_is_correct());
explore_under(y_v);
} else { // connected to y
vertex y_v(row_index, y_index, v.offset(), m_vertices.size());
v.add_child(y_v);
vertex x_v(row_index, x_index, v.offset() - row_offset, m_vertices.size() + 1);
y_v.add_child(x_v);
push_vertex(y_v); // no need to explore from y_v
push_vertex(x_v);
SASSERT(tree_is_correct());
explore_under(x_v);
}
}
}
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);
go_over_vertex_column(v);
for (unsigned j : v.children()) {
explore_under(m_vertices[j]);
}
}
};
}