propagate cheap eqs

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/bound_analyzer_on_row.h

@@ -13,9 +13,8 @@ Abstract:
     In the same loop trying to pin variables by pushing the partial sum up, denoting the variable related to it by _l
 
 Author:
-
+    Lev Nachmanson  (levnach)
-    Lev Nachmanson (levnach)
+    Nikolaj Bjorner (nbjorner)
-
 Revision History:
 
 
@@ -31,7 +30,7 @@ template <typename C, typename B> // C plays a role of a container, B - lp_bound
 class bound_analyzer_on_row {
     const C&                           m_row;
     B &                                m_bp;
-    unsigned                           m_row_or_term_index;
+    unsigned                           m_row_index;
     int                                m_column_of_u; // index of an unlimited from above monoid
     // -1 means that such a value is not found, -2 means that at least two of such monoids were found
     int                                m_column_of_l; // index of an unlimited from below monoid
@@ -48,7 +47,7 @@ public :
         :
         m_row(it),
         m_bp(bp),
-        m_row_or_term_index(row_or_term_index),
+        m_row_index(row_or_term_index),
         m_column_of_u(-1),
         m_column_of_l(-1),
         m_rs(rs)
@@ -62,7 +61,7 @@ public :
                             B & bp) {
         bound_analyzer_on_row a(row, bj, rs, row_or_term_index, bp);
         a.analyze();
-        // TBD: a.analyze_eq();
+        a.analyze_eq();
     }
 
 private:
@@ -84,37 +83,6 @@ private:
             limit_all_monoids_from_above();
     }
 
-
-    void analyze_eq() {
-        lpvar x = null_lpvar, y = null_lpvar;
-        for (const auto & c : m_row) {
-            if (m_bp.get_column_type(c.var()) == column_type::fixed)
-                continue;
-            if (x == null_lpvar && c.coeff().is_one())
-                x = c.var();
-            else if (y == null_lpvar && c.coeff().is_minus_one())
-                y = c.var();
-            else 
-                return;
-        }        
-        if (x == null_lpvar || y == null_lpvar)
-            return;
-        impq value;
-        for (const auto & c : m_row) {
-            if (m_bp.get_column_type(c.var()) == column_type::fixed)
-                value += c.coeff() * lb(c.var());
-        }
-        if (!value.is_zero()) {
-            // insert / check offset table to infer equalities
-            // of the form y = z from offset table collision:
-            // value = (x - y)
-            // value = (x - z)
-        } 
-        else {
-            // m_bp.try_add_fixed(x, y, m_row_or_term_index);
-        }
-    }
-
     bool bound_is_available(unsigned j, bool lower_bound) {
         return (lower_bound && lower_bound_is_available(j)) ||
             (!lower_bound && upper_bound_is_available(j));
@@ -327,7 +295,7 @@ private:
     // }
 
     void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
-        m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_or_term_index, strict);
+        m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_index, strict);
     }
     
     void advance_u(unsigned j) {
@@ -361,6 +329,24 @@ private:
         }
     }
 
+    void analyze_eq() {
+        unsigned x = UINT_MAX, y = UINT_MAX;
+        unsigned k = 0;
+        for (const auto& c : m_row) {
+            if (!m_bp.lp().column_is_fixed(c.var())) {
+                if (x == UINT_MAX && c.coeff().is_one())
+                    x = k;
+                else if (y == UINT_MAX && c.coeff().is_minus_one())
+                    y = k;
+                else 
+                    return;
+            }
+            k++;
+        }        
+        if (x == UINT_MAX || y == UINT_MAX)
+            return;
+        m_bp.try_create_eq(x, y, m_row_index);
+    }
 
 };
 }

src/math/lp/indexed_vector.h

@@ -83,7 +83,7 @@ public:
         return m_data.size();
     }
 
-    unsigned size() {
+    unsigned size() const {
         return m_index.size();
     }
 

src/math/lp/lar_solver.h

@@ -161,20 +161,7 @@ class lar_solver : public column_namer {
     bool use_lu() const;
     bool sizes_are_correct() const;
     bool implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const;
-    template <typename T>
+    
-    void analyze_new_bounds_on_row(
-        unsigned row_index,
-        lp_bound_propagator<T>& bp) {
-        lp_assert(!use_tableau());
-        unsigned j =  m_mpq_lar_core_solver.m_r_basis[row_index]; // basis column for the row
-        bound_analyzer_on_row<indexed_vector<mpq>, lp_bound_propagator<T>>::analyze_row(
-            m_mpq_lar_core_solver.get_pivot_row(),
-            j,
-            zero_of_type<numeric_pair<mpq>>(),
-            row_index,
-            bp);
-    }
-
     template <typename T>
     void analyze_new_bounds_on_row_tableau(
         unsigned row_index,
@@ -196,17 +183,8 @@ class lar_solver : public column_namer {
     void substitute_basis_var_in_terms_for_row(unsigned i);
     template <typename T>
     void calculate_implied_bounds_for_row(unsigned i, lp_bound_propagator<T> & bp) {
-        if (use_tableau()) {
+        SASSERT(use_tableau());
-            analyze_new_bounds_on_row_tableau(i, bp);
+        analyze_new_bounds_on_row_tableau(i, bp);
-        } else {
-            m_mpq_lar_core_solver.calculate_pivot_row(i);
-            substitute_basis_var_in_terms_for_row(i);
-            analyze_new_bounds_on_row(i, bp);
-        }
-    }
-    template <typename T>
-    void propagate_bounds_on_a_term(const lar_term& t, lp_bound_propagator<T> & bp, unsigned term_offset) {
-        NOT_IMPLEMENTED_YET();
     }
     static void clean_popped_elements(unsigned n, u_set& set);
     static void shrink_inf_set_after_pop(unsigned n, u_set & set);
@@ -346,28 +324,14 @@ public:
     void activate(constraint_index ci);
     void random_update(unsigned sz, var_index const * vars);
     template <typename T>
-    void propagate_bounds_on_terms(lp_bound_propagator<T> & bp) {
-        for (unsigned i = 0; i < m_terms.size(); i++) {
-            if (term_is_used_as_row(i))
-                continue; // this term is used a left side of a constraint,
-            // it was processed as a touched row if needed
-            propagate_bounds_on_a_term(*m_terms[i], bp, i);
-        }
-    }
-    template <typename T>
     void propagate_bounds_for_touched_rows(lp_bound_propagator<T> & bp) {
-        if (!use_tableau())
+        SASSERT(use_tableau());
-            return; // todo: consider to remove the restriction
-        
         for (unsigned i : m_rows_with_changed_bounds) {
             calculate_implied_bounds_for_row(i, bp);
             if (settings().get_cancel_flag())
                 return;
         }
         m_rows_with_changed_bounds.clear();
-        if (!use_tableau()) {
-            propagate_bounds_on_terms(bp);
-        }
     }
     bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
     inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
@@ -591,7 +555,7 @@ public:
         return false;
     }
     void round_to_integer_solution();
-    inline const row_strip<mpq> &  get_row(unsigned i) { return A_r().m_rows[i]; }
+    inline const row_strip<mpq> &  get_row(unsigned i) const { return A_r().m_rows[i]; }
     bool row_is_correct(unsigned i) const;
     bool ax_is_correct() const;
     bool get_equality_and_right_side_for_term_on_current_x(tv const& t, mpq &rs, constraint_index& ci, bool &upper_bound) const;

src/math/lp/lp_bound_propagator.h

@@ -1,18 +1,40 @@
 /*
   Copyright (c) 2017 Microsoft Corporation
-  Author: Lev Nachmanson
+  Author:
+  Nickolaj Bjorner (nbjorner)
+  Lev Nachmanson   (levnach)
 */
 #pragma once
 #include "math/lp/lp_settings.h"
 namespace lp {
 template <typename T>
 class lp_bound_propagator {
+
+    // defining a graph on columns x, y such that there is a row x - y = c, where c is a constant    
+    struct vertex {        
+        unsigned           m_row; 
+        unsigned           m_index; // in the row
+        bool               m_sign; // true if the vertex plays the role of y
+        vector<unsigned>   m_adjacent_edges; // points to the
+        vertex(unsigned row, unsigned index) : m_row(row), m_index(index) {}
+    };
+
+    // an edge can be between columns in the same row or between two different rows in the same column
+    struct edge { 
+        unsigned  m_a;
+        unsigned  m_b;
+        impq      m_offset;
+    };
+    vector<vertex> m_vertices;
+    vector<edge>   m_edges;
+    
     std::unordered_map<unsigned, unsigned> m_improved_lower_bounds; // these maps map a column index to the corresponding index in ibounds
     std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
     T& m_imp;
 public:
     vector<implied_bound> m_ibounds;
     lp_bound_propagator(T& imp): m_imp(imp) {}
+    const lar_solver& lp() const { return m_imp.lp(); }
     column_type get_column_type(unsigned j) const {
         return m_imp.lp().get_column_type(j);
     }
@@ -65,5 +87,30 @@ public:
     void consume(const mpq& a, constraint_index ci) {
         m_imp.consume(a, ci);
     }
+
+    void create_initial_xy(unsigned x, unsigned y, unsigned row_index) {
+        impq value;
+        const auto& row =  lp().get_row(row_index);
+        for (unsigned k = 0; k < row.size(); k++) {
+            if (k == x || k == y)
+                continue;
+            const auto& c = row[k];
+            value += c.coeff() * lp().get_lower_bound(c.var());
+        }
+        vertex xv(row_index, x);
+        m_vertices.push_back(xv);
+        vertex yv(row_index, y);
+        m_vertices.push_back(yv);
+        
+        NOT_IMPLEMENTED_YET();
+    }
+    
+    void try_create_eq(unsigned x, unsigned y, unsigned row_index) {
+        m_vertices.clear();
+        m_edges.clear();
+        create_initial_xy(x, y, row_index);
+        NOT_IMPLEMENTED_YET();
+        
+    }
 };
 }

src/smt/theory_lra.cpp

@@ -4033,4 +4033,3 @@ template  class lp::lp_bound_propagator<smt::theory_lra::imp>;
 template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
 template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
 template void lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>&);
-template void lp::lar_solver::propagate_bounds_on_terms<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);