From fb035c063494bde126dbbd26c2007bc6ac310e1b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 31 Jul 2020 16:59:57 -0700
Subject: [PATCH] fixed a but with insertion of a null vertex
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
src/math/lp/lp_bound_propagator.h | 16 ++++++++--------
1 file changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 64955ad4b..30f7fcd72 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -76,9 +76,9 @@ class lp_bound_propagator {
const vertex* m_fixed_vertex;
explanation m_fixed_vertex_explanation;
// 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
- 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;
// to bind polarity and the vertex in the table
struct pol_vert {
@@ -205,9 +205,9 @@ public:
void try_add_equation_with_val_table(const vertex *v) {
SASSERT(m_fixed_vertex);
unsigned v_j = v->column();
- vertex *u = nullptr;
+ const vertex *u = nullptr;
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;
}
unsigned j = u->column();
@@ -350,9 +350,9 @@ public:
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";);
- vertex *k; // the other vertex
+ const vertex *k; // the other vertex
if (table.find(val(v), k)) {
TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
if (k->column() != v->column() &&
@@ -397,7 +397,7 @@ public:
}
// 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(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 = ";
@@ -471,7 +471,7 @@ public:
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());
}