mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

cheap_eqs

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-16 17:59:06 -07:00
parent 3b00b34c6f
commit b5fc9635c4
1 changed files with 96 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -68,7 +68,7 @@ class lp_bound_propagator {
// by adjusting the vertices offsets, so they become absolute. // by adjusting the vertices offsets, so they become absolute.
// If the tree is fixed then in addition to checking with the m_offset_to_verts // If the tree is fixed then in addition to checking with the m_offset_to_verts
// we are going to check with the m_fixed_var_tables. // we are going to check with the m_fixed_var_tables.
bool m_tree_is_fixed; vertex* m_fixed_vertex;
map<mpq, vertex*, obj_hash<mpq>, mpq_eq> m_offset_to_verts; map<mpq, vertex*, obj_hash<mpq>, mpq_eq> m_offset_to_verts;
// these maps map a column index to the corresponding index in ibounds // 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_lower_bounds;
@ -79,6 +79,8 @@ class lp_bound_propagator {
signed_index() : m_index(UINT_MAX) {} signed_index() : m_index(UINT_MAX) {}
bool not_set() const { return m_index == UINT_MAX; } bool not_set() const { return m_index == UINT_MAX; }
bool is_set() const { return m_index != UINT_MAX; } bool is_set() const { return m_index != UINT_MAX; }
bool sign() const { return m_sign; }
unsigned index() const { return m_index; }
}; };
T& m_imp; T& m_imp;
@ -90,9 +92,10 @@ public:
m_improved_lower_bounds.clear(); m_improved_lower_bounds.clear();
m_ibounds.reset(); m_ibounds.reset();
} }
lp_bound_propagator(T& imp): m_imp(imp), lp_bound_propagator(T& imp): m_root(nullptr),
m_root(nullptr), m_fixed_vertex(nullptr),
m_tree_is_fixed(false) {} m_imp(imp) {}
const lar_solver& lp() const { return m_imp.lp(); } const lar_solver& lp() const { return m_imp.lp(); }
column_type get_column_type(unsigned j) const { column_type get_column_type(unsigned j) const {
return m_imp.lp().get_column_type(j); return m_imp.lp().get_column_type(j);
@ -227,15 +230,31 @@ public:
return false; return false;
} }
void try_add_equation_with_fixed_tables(vertex *v) {
SASSERT(m_fixed_vertex);
unsigned v_j = column(v);
unsigned j;
if (!lp().find_in_fixed_tables(v->offset(), is_int(v_j), j))
return;
ptr_vector<vertex> path;
find_path_on_tree(path, v, m_fixed_vertex);
explanation ex = get_explanation_from_path(path);
explain_fixed_column(ex, j);
add_eq_on_columns(ex, v_j, column(v));
}
void create_root(unsigned row_index) { void create_root(unsigned row_index) {
SASSERT(!m_root && !m_tree_is_fixed); SASSERT(!m_root && !m_fixed_vertex);
signed_index x, y; signed_index x, y;
mpq offset; mpq offset;
if (!is_offset_row_tree(nullptr, row_index, x, y, offset)) if (!is_offset_row_tree(row_index, x, y, offset))
return; return;
TRACE("cheap_eq", display_row_info(row_index, tout);); TRACE("cheap_eq", display_row_info(row_index, tout););
if (y.not_set()) { if (y.not_set()) {
m_root = alloc(vertex, row_index, x.m_index, offset); m_root = alloc(vertex, row_index, x.m_index, offset);
m_fixed_vertex = m_root;
return; return;
} }
@ -243,52 +262,64 @@ public:
m_root = alloc(vertex, row_index, x.m_index, mpq(0)); m_root = alloc(vertex, row_index, x.m_index, mpq(0));
// we have x + sign_y * y + offset = 0 // we have x + sign_y * y + offset = 0
// x.offset is set to zero as x plays the role of m_root // x.offset is set to zero as x plays the role of m_root
// if sign_y = 1 then y.offset() = -offset - x.offset() // if sign_y = true then y.offset() = offset + x.offset()
// else y.offset() = offset + x.offset() // else y.offset() = - offset - x.offset()
if (y.m_sign) if (!y.m_sign)
offset.neg(); offset.neg();
vertex *v = alloc(vertex, row_index, y.m_index, offset); vertex *v = alloc(vertex, row_index, y.m_index, offset);
m_root->add_child(v); m_root->add_child(v);
} }
// returns the vertex to start exploration from unsigned column(unsigned row, unsigned index) {
return lp().get_row(row)[index].var();
}
// returns the vertex to start exploration from, or nullptr
vertex* add_child_from_row(unsigned row_index, vertex* parent) { vertex* add_child_from_row(unsigned row_index, vertex* parent) {
NOT_IMPLEMENTED_YET(); signed_index x, y;
/* mpq offset;
bool sign, parent_sign; if (!is_offset_row_tree(row_index, x, y, offset))
unsigned index = UINT_MAX, parent_index = ;
const auto & row = lp().get_row(row_index);
for (unsigned k = 0; k < row.size(); k++) {
const auto& c = row[k];
if (column_is_fixed(c.var()) ||
c.var() == column(parent) ||
set_sign_and_index(c.coeff(), index, x_sign))
continue;
return nullptr; return nullptr;
} if (y.not_set()) {
if (index == UINT_MAX) { SASSERT(column(parent) == column(row_index, x.m_index));
// start fixed tree phase if (m_fixed_vertex) {
NOT_IMPLEMENTED_YET(); vertex* v = alloc(vertex, row_index, x.m_index, - offset);
} else { parent->add_child(v);
mpq offset(0); return v;
for (const auto& c : row)
if (column_is_fixed(c.var()))
offset += c.coeff() * get_lower_bound_rational(c.var());
// make x
if (offset.is_zero() &&
!is_equal(row[x_index].var(), row[y_index].var())) {
lp::explanation ex;
explain_fixed_in_row(row_index, ex);
add_eq_on_columns(ex, row[x_index].var(), row[y_index].var());
} }
return true; vertex *v = alloc(vertex, row_index, x.m_index, parent->offset());
m_fixed_vertex = v;
parent->add_child(v);
// need to shift the tree so v.offset() becomes equal to - offset
shift_offsets_by_delta(m_root, - offset - parent->offset());
return v;
}
SASSERT(x.is_set() && y.is_set());
if (column(parent) == column(row_index, x.index())) {
vertex *vx = alloc(vertex, row_index, x.index(), parent->offset());
// mpq x_c = rat_sign(x.sign());
// mpq y_c = rat_sign(y.sign());
// we have x_c*x + y_c*y + offset = 0
// y = - offset/y_c - ( x_c/y_c )vx.offset;
bool x_c_y_c = x.sign() ^ y.sign();
mpq y_offs = (y.sign()? offset: - offset) - (x_c_y_c? - vx->offset() : vx->offset());
vertex *vy = alloc(vertex, row_index, y.index(), y_offs);
parent->add_child(vx);
vx->add_child(vy);
return vy; // start exploring from vy
} else {
vertex *vy = alloc(vertex, row_index, y.index(), parent->offset());
// mpq x_c = rat_sign(x.sign());
// mpq y_c = rat_sign(y.sign());
// we have x_c*x + y_c*y + offset = 0
// x = - offset/x_c - ( y_c/x_c )vy.offset;
bool y_c_x_c = x.sign() ^ y.sign();
mpq x_offs = (x.sign()? offset: -offset) - (y_c_x_c? - vy->offset(): vy->offset());
vertex *vx = alloc(vertex, row_index, y.index(), x_offs);
vy->add_child(vx);
return vx;
} }
*/
NOT_IMPLEMENTED_YET();
return nullptr;
} }
bool is_equal(lpvar j, lpvar k) const { bool is_equal(lpvar j, lpvar k) const {
@ -307,7 +338,7 @@ public:
m_offset_to_verts.insert(v->offset(), v); m_offset_to_verts.insert(v->offset(), v);
} }
if (m_tree_is_fixed) { if (m_fixed_vertex) {
unsigned j; unsigned j;
unsigned v_col = column(v); unsigned v_col = column(v);
if (lp().find_in_fixed_tables(v->offset(), is_int(v_col), j)) { if (lp().find_in_fixed_tables(v->offset(), is_int(v_col), j)) {
@ -472,17 +503,21 @@ public:
} }
void explain_fixed_in_row(unsigned row, explanation& ex) const { void explain_fixed_in_row(unsigned row, explanation& ex) const {
constraint_index lc, uc;
for (const auto & c : lp().get_row(row)) { for (const auto & c : lp().get_row(row)) {
lpvar j = c.var(); if (lp().is_fixed(c.var())) {
if (lp().is_fixed(j)) { explain_fixed_column(ex, c.var());
lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
ex.push_back(lc);
ex.push_back(uc);
} }
} }
} }
void explain_fixed_column(explanation & ex, unsigned j) const {
SASSERT(column_is_fixed(j));
constraint_index lc, uc;
lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
ex.push_back(lc);
ex.push_back(uc);
}
std::ostream& display_row_of_vertex(vertex* k, std::ostream& out) const { std::ostream& display_row_of_vertex(vertex* k, std::ostream& out) const {
return display_row_info(k->row(), out ); return display_row_info(k->row(), out );
} }
@ -579,14 +614,11 @@ public:
return; return;
} }
SASSERT(tree_is_correct()); SASSERT(tree_is_correct());
TRACE("cheap_eq", lp().get_int_solver()->display_row_info(tout, row_index););
SASSERT(tree_is_correct());
explore_under(m_root); explore_under(m_root);
TRACE("cheap_eq", tout << "done for row_index " << row_index << "\n";); TRACE("cheap_eq", tout << "done for row_index " << row_index << "\n";);
TRACE("cheap_eq", tout << "tree size = " << verts_size();); TRACE("cheap_eq", tout << "tree size = " << verts_size(););
delete_tree(m_root); delete_tree(m_root);
m_root = nullptr; m_root = m_fixed_vertex = nullptr;
m_tree_is_fixed = false;
} }
unsigned verts_size() const { unsigned verts_size() const {
@ -651,6 +683,8 @@ public:
} }
void explore_under(vertex * v) { void explore_under(vertex * v) {
if (m_fixed_vertex)
try_add_equation_with_fixed_tables(v);
check_for_eq_and_add_to_offset_table(v); check_for_eq_and_add_to_offset_table(v);
go_over_vertex_column(v); go_over_vertex_column(v);
// v might change in m_vertices expansion // v might change in m_vertices expansion
@ -660,9 +694,8 @@ public:
} }
void switch_to_fixed_mode_in_tree(vertex *v, const mpq& new_v_offset) { void switch_to_fixed_mode_in_tree(vertex *v, const mpq& new_v_offset) {
m_tree_is_fixed = true; SASSERT(v);
if (v == nullptr) m_fixed_vertex = v;
return;
mpq delta = new_v_offset - v->offset(); mpq delta = new_v_offset - v->offset();
shift_offsets_by_delta(m_root, delta); shift_offsets_by_delta(m_root, delta);
SASSERT(v->offset() == new_v_offset); SASSERT(v->offset() == new_v_offset);
@ -675,8 +708,10 @@ public:
} }
} }
// Will return x such that x.m_sign = false.
// In case of only one non fixed column, and the function returns true,
// this column would be represened by x
bool is_offset_row_tree( bool is_offset_row_tree(
vertex* v, // a vertex from this row, or nullptr
unsigned row_index, unsigned row_index,
signed_index & x, signed_index & x,
signed_index & y, signed_index & y,
@ -721,12 +756,6 @@ public:
} }
offset.neg(); offset.neg();
} }
if (!m_tree_is_fixed && y.not_set()) {
SASSERT(v == nullptr || v->index() == x.m_index);
switch_to_fixed_mode_in_tree(v, offset);
}
return true; return true;
} }