From 46831e7ebbd4a4b076be4eb9e41457e2229414ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 6 Apr 2021 22:32:22 -0700
Subject: [PATCH] provisionary fix for #5127

---
 src/math/lp/lp_bound_propagator.h | 38 +++++++++++++++++++------------
 1 file changed, 24 insertions(+), 14 deletions(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 7ef1ea273..3bbef73e3 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -103,12 +103,14 @@ class lp_bound_propagator {
     // x[m_root->column()] - m_pol[j].pol()*x[j] == const;
     // to bind polarity and the vertex in the table
     struct pol_vert {
-        int m_polarity;
-        const vertex* m_v;
-        pol_vert() {}
-        pol_vert(int p, const vertex* v): m_polarity(p), m_v(v) {}
+        int           m_polarity { -2 };
+        unsigned      m_row_index { 0 };
+        const vertex* m_v { nullptr };
+    pol_vert() {}
+    pol_vert(int p, unsigned r, const vertex* v): m_polarity(p), m_row_index(r), m_v(v) {}
         int pol() const { return m_polarity; }
         const vertex* v() const { return m_v; }
+        unsigned row() const { return m_row_index; }
     };
     u_map<pol_vert>                                     m_pol; 
     // if m_pos.contains(j) then  x[j] = x[m_root->column()] + o
@@ -258,21 +260,29 @@ public:
     // pol for polarity
     int pol(const vertex* v) const { return pol(v->column()); }
     int pol(unsigned j) const { return m_pol[j].pol(); }
-    void set_polarity(const vertex* v, int p) {
+    void set_polarity(const vertex* v, unsigned r, int p) {
         SASSERT(p == 1 || p == -1);
         unsigned j = v->column();
         SASSERT(!m_pol.contains(j));
-        m_pol.insert(j, pol_vert(p, v));
+        m_pol.insert(j, pol_vert(p, r, v));
     }
 
     void check_and_set_polarity(vertex* v, int polarity, unsigned row_index) {
         pol_vert prev_pol;
         if (!m_pol.find(v->column(), prev_pol)) {
-            set_polarity(v, polarity);
+            set_polarity(v, row_index, polarity);
             return;
         }
         if (prev_pol.pol() == polarity)
             return;
+        return;
+        //
+        // TODO disabled pending fix for #5127
+        // the explanation is missing some terms. 
+        // Probably because in this case there isn't a single, but two paths
+        // from u to v. The bounds for the fixed variables for the two paths
+        // have to be taken into account.
+        // 
         const vertex *u = prev_pol.v();
         // we have a path L between u and v with p(L) = -1, that means we can
         // create an equality of the form x + x = a, where x = v->column() = u->column()
@@ -282,7 +292,7 @@ public:
         explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
         set_fixed_vertex(v);
         TRACE("cheap_eq", 
-              tout << "polarity switch: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
+              tout << "polarity switch: " << row_index << " pol: " << polarity << "\nv = "; print(tout , v) << "\nu = "; print(tout, u) << "\n";
               tout << "fixed vertex explanation\n";
               for (auto p : m_fixed_vertex_explanation) 
                   lp().constraints().display(tout, [this](lpvar j) { return lp().get_variable_name(j);}, p.ci()););
@@ -316,7 +326,7 @@ public:
         }
         TRACE("cheap_eq", print_row(tout, row_index););
         m_root = alloc_v(x);
-        set_polarity(m_root, 1); // keep m_root in the positive table
+        set_polarity(m_root, row_index, 1); // keep m_root in the positive table
         if (not_set(y)) {
             set_fixed_vertex(m_root);
             explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
@@ -482,14 +492,14 @@ public:
     }
 
     void explain_fixed_in_row(unsigned row, explanation& ex) const {
-        for (const auto & c : lp().get_row(row)) {
-            if (lp().is_fixed(c.var())) {
+        TRACE("cheap_eq", tout << "explain-row " << row << "\n";);
+        for (const auto & c : lp().get_row(row)) 
+            if (lp().is_fixed(c.var())) 
                 explain_fixed_column(c.var(), ex);
-            }
-        }
     }
 
     void explain_fixed_column(unsigned j, explanation & ex) const {
+        TRACE("cheap_eq", tout << "explain-column " << j << "\n";);
         SASSERT(column_is_fixed(j));
         constraint_index lc, uc;            
         lp().get_bound_constraint_witnesses_for_column(j, lc, uc);
@@ -547,7 +557,7 @@ public:
         out << "\nchildren :\n";
         for (auto c : v->edges()) {
             out << "row = ";
-            print_row(out, c.row());
+            print_row(out << c.row() << ": ", c.row());
             print_tree(out, c.target());
         }
         return out;