From 6a6cb3822ce39f55d3c5ec145624fda51158b927 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 6 Jun 2019 16:13:49 -0700
Subject: [PATCH] before getting explanations for monomials upper and low
 bounds

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp          | 23 -----------------------
 src/math/lp/lar_solver.h            |  4 ----
 src/math/lp/lp_bound_propagator.cpp | 24 ++++++++++++++++++++++++
 src/math/lp/lp_bound_propagator.h   |  1 +
 src/smt/theory_lra.cpp              |  2 +-
 5 files changed, 26 insertions(+), 28 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 8cb420ee1..ef81eebb3 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -224,29 +224,6 @@ void lar_solver::propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagat
 }
 
 
-void lar_solver::explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp) {
-    unsigned i = ib.m_row_or_term_index;
-    int bound_sign = ib.m_is_lower_bound? 1: -1;
-    int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
-    unsigned bound_j = ib.m_j;
-    if (is_term(bound_j)) {
-        bound_j = m_var_register.external_to_local(bound_j);
-    }
-    for (auto const& r : A_r().m_rows[i]) {
-        unsigned j = r.var();
-        if (j == bound_j) continue;
-        mpq const& a = r.get_val();
-        int a_sign = is_pos(a)? 1: -1;
-        int sign = j_sign * a_sign;
-        const ul_pair & ul =  m_columns_to_ul_pairs[j];
-        // todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
-        auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
-        lp_assert(is_valid(witness));
-        bp.consume(a, witness);
-    }
-    // lp_assert(implied_bound_is_correctly_explained(ib, explanation));
-}
-
 
 bool lar_solver::term_is_used_as_row(unsigned term) const {
     lp_assert(is_term(term));
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 74516db64..d6d8ebd95 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -315,10 +315,6 @@ public:
     
     void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator & bp, unsigned term_offset);
 
-
-    void explain_implied_bound(implied_bound & ib, lp_bound_propagator & bp);
-
-
     bool term_is_used_as_row(unsigned term) const;
     
     void propagate_bounds_on_terms(lp_bound_propagator & bp);
diff --git a/src/math/lp/lp_bound_propagator.cpp b/src/math/lp/lp_bound_propagator.cpp
index d63b4ff2d..c6946eeb1 100644
--- a/src/math/lp/lp_bound_propagator.cpp
+++ b/src/math/lp/lp_bound_propagator.cpp
@@ -114,4 +114,28 @@ void lp_bound_propagator::try_add_bound(mpq  v, unsigned j, bool is_low, bool co
         }
      }
 }
+void lp_bound_propagator::explain_implied_bound(implied_bound & ib) {
+    unsigned i = ib.m_row_or_term_index;
+    int bound_sign = ib.m_is_lower_bound? 1: -1;
+    int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;
+    unsigned bound_j = ib.m_j;
+    if (m_lar_solver.is_term(bound_j)) {
+        bound_j = m_lar_solver.m_var_register.external_to_local(bound_j);
+    }
+    for (auto const& r : m_lar_solver.A_r().m_rows[i]) {
+        unsigned j = r.var();
+        if (j == bound_j) continue;
+        mpq const& a = r.get_val();
+        int a_sign = is_pos(a)? 1: -1;
+        int sign = j_sign * a_sign;
+        const ul_pair & ul =  m_lar_solver.m_columns_to_ul_pairs[j];
+        // todo : process witnesses from monomials!!!!!!!!!!!!!!!!!!!!!
+        auto witness = sign > 0? ul.upper_bound_witness(): ul.lower_bound_witness();
+        lp_assert(is_valid(witness));
+        consume(a, witness);
+    }
+    // lp_assert(implied_bound_is_correctly_explained(ib, explanation));
+}
+
+
 }
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index a3f4c9802..d39cf46d8 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -32,6 +32,7 @@ public:
                                       lp::lconstraint_kind kind,
                                       const rational & bval) {return true;}
     unsigned number_of_found_bounds() const { return m_ibounds.size(); }
+    void explain_implied_bound(implied_bound & ib);
     virtual void consume(mpq const& v, lp::constraint_index j) = 0;
 };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f00d53085..d2aeacd33 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2375,7 +2375,7 @@ public:
                 m_params.reset();
                 m_explanation.clear();
                 local_bound_propagator bp(*this);
-                lp().explain_implied_bound(be, bp);
+                bp.explain_implied_bound(be);
             }
             CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
             updt_unassigned_bounds(v, -1);