mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fixed a but with insertion of a null vertex

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-07-31 16:59:57 -07:00
parent 566a0d540a
commit fb035c0634
1 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -76,9 +76,9 @@ class lp_bound_propagator {
const vertex* m_fixed_vertex; const vertex* m_fixed_vertex;
explanation m_fixed_vertex_explanation; explanation m_fixed_vertex_explanation;
// a pair (o, j) belongs to m_vals_to_verts iff x[j] = x[m_root->column()] + o // a pair (o, j) belongs to m_vals_to_verts iff x[j] = x[m_root->column()] + o
map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts; map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts;
// a pair (o, j) belongs to m_vals_to_verts_neg iff -x[j] = x[m_root->column()] + o // a pair (o, j) belongs to m_vals_to_verts_neg iff -x[j] = x[m_root->column()] + o
map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts_neg; map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts_neg;
// x[m_root->column()] - m_pol[j].pol()*x[j] == const; // x[m_root->column()] - m_pol[j].pol()*x[j] == const;
// to bind polarity and the vertex in the table // to bind polarity and the vertex in the table
struct pol_vert { struct pol_vert {
@ -205,9 +205,9 @@ public:
void try_add_equation_with_val_table(const vertex *v) { void try_add_equation_with_val_table(const vertex *v) {
SASSERT(m_fixed_vertex); SASSERT(m_fixed_vertex);
unsigned v_j = v->column(); unsigned v_j = v->column();
vertex *u = nullptr; const vertex *u = nullptr;
if (!m_vals_to_verts.find(val(v_j), u)) { if (!m_vals_to_verts.find(val(v_j), u)) {
m_vals_to_verts.insert(val(v_j), u); m_vals_to_verts.insert(val(v_j), v);
return; return;
} }
unsigned j = u->column(); unsigned j = u->column();
@ -350,9 +350,9 @@ public:
return m_imp.is_equal(col_to_imp(j), col_to_imp(k)); return m_imp.is_equal(col_to_imp(j), col_to_imp(k));
} }
void check_for_eq_and_add_to_val_table(vertex* v, map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>>& table) { void check_for_eq_and_add_to_val_table(vertex* v, map<mpq, const vertex*, obj_hash<mpq>, default_eq<mpq>>& table) {
TRACE("cheap_eq", tout << "v="; print(tout, v) << "\n";); TRACE("cheap_eq", tout << "v="; print(tout, v) << "\n";);
vertex *k; // the other vertex const vertex *k; // the other vertex
if (table.find(val(v), k)) { if (table.find(val(v), k)) {
TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";); TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
if (k->column() != v->column() && if (k->column() != v->column() &&
@ -397,7 +397,7 @@ public:
} }
// we have v_i and v_j, indices of vertices at the same offsets // we have v_i and v_j, indices of vertices at the same offsets
void report_eq(vertex* v_i, vertex* v_j) { void report_eq(const vertex* v_i, const vertex* v_j) {
SASSERT(v_i != v_j); SASSERT(v_i != v_j);
SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column())); SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column()));
TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = "; TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = ";
@ -471,7 +471,7 @@ public:
ex.push_back(uc); ex.push_back(uc);
} }
std::ostream& display_row_of_vertex(vertex* k, std::ostream& out) const { std::ostream& display_row_of_vertex(const vertex* k, std::ostream& out) const {
return print_row(out, k->row()); return print_row(out, k->row());
} }