some simplifications in cheap eqs

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

src/math/lp/bound_analyzer_on_row.h

@@ -330,11 +330,19 @@ private:
     }
 
     void analyze_eq() {
-        if (m_bp.lp().settings().cheap_eqs()) {
+        switch (m_bp.lp().settings().cheap_eqs()) {
+        case 0:
+            return;
+        case 1:
             m_bp.try_create_eq(m_row_index);
+            break;
+        case 2:
+            m_bp.try_create_eq_table(m_row_index);
+            break;
+        default:
+            UNREACHABLE();
         }
     }
-
 };
 }
 

src/math/lp/lp_bound_propagator.h

@@ -9,6 +9,11 @@
 namespace lp {
 template <typename T>
 class lp_bound_propagator {
+    typedef std::pair<int, impq> var_offset;
+    typedef pair_hash<int_hash, obj_hash<impq> > var_offset_hash;
+    typedef map<var_offset, unsigned, var_offset_hash, default_eq<var_offset> > var_offset2row_id;
+    var_offset2row_id       m_var_offset2row_id;
+
     struct impq_eq { bool operator()(const impq& a, const impq& b) const {return a == b;}};
 
     // vertex represents a pair (row,x) or (row,y) for an offset row.
@@ -62,14 +67,6 @@ class lp_bound_propagator {
     std::unordered_map<unsigned, unsigned>    m_improved_upper_bounds;
     T&                                        m_imp;
     impq                                      m_zero;
-    typedef std::pair<unsigned, unsigned> upair;
-    struct uphash {
-        unsigned operator()(const upair& p) const { return combine_hash(p.first, p.second); }
-    };
-    struct upeq {
-        unsigned operator()(const upair& p, const upair& q) const { return p == q; }
-    };
-    hashtable<upair, uphash, upeq>  m_reported_pairs; // contain the pairs of columns (first < second)
 public:
     vector<implied_bound> m_ibounds;
     lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {}
@@ -156,7 +153,7 @@ public:
             offset += c.coeff() * lp().get_lower_bound(c.var());
         }
         if (offset.is_zero() &&
-            !pair_is_reported(row[x_index].var(), row[y_index].var())) {
+            !pair_is_reported_or_congruent(row[x_index].var(), row[y_index].var())) {
             lp::explanation ex;
             explain_fixed_in_row(row_index, ex);
             add_eq_on_columns(ex, row[x_index].var(), row[y_index].var());
@@ -164,17 +161,16 @@ public:
         return true;
     }    
 
-    bool pair_is_reported(lpvar j, lpvar k) const {        
+    bool pair_is_reported_or_congruent(lpvar j, lpvar k) const {        
-        return j < k? m_reported_pairs.contains(std::make_pair(j, k)) :
+        return m_imp.congruent_or_irrelevant(lp().column_to_reported_index(j), lp().column_to_reported_index(k));
-            m_reported_pairs.contains(std::make_pair(k, j));
     }
     
     void check_for_eq_and_add_to_offset_table(vertex* v) {
-        vertex *k; // the other vertex index
+        vertex *k; // the other vertex 
         
         if (m_offset_to_verts.find(v->offset(), k)) {
             if (column(k) != column(v) &&
-                !pair_is_reported(column(k),column(v)))
+                !pair_is_reported_or_congruent(column(k),column(v)))
                 report_eq(k, v);
         } else {
             TRACE("cheap_eq", tout << "registered offset " << v->offset() << " to " << v << "\n";);
@@ -211,8 +207,6 @@ public:
 
     void add_eq_on_columns(const explanation& exp, lpvar v_i_col, lpvar v_j_col) {
         SASSERT(v_i_col != v_j_col);
-        upair p = v_i_col < v_j_col? upair(v_i_col, v_j_col) :upair(v_j_col, v_i_col);
-        m_reported_pairs.insert(p);
         unsigned i_e = lp().column_to_reported_index(v_i_col);
         unsigned j_e = lp().column_to_reported_index(v_j_col);
         TRACE("cheap_eq", tout << "reporting eq " << i_e << ", " << j_e << "\n";
@@ -223,6 +217,9 @@ public:
         m_imp.add_eq(i_e, j_e, exp);        
     }
 
+    void try_create_eq_table(unsigned row_index) {
+    }
+    
     explanation get_explanation_from_path(const ptr_vector<vertex>& path) const {
         explanation ex;
         unsigned prev_row = UINT_MAX;

src/math/lp/lp_settings.h

@@ -205,12 +205,12 @@ public:
 private:
     bool             m_enable_hnf;
     bool             m_print_external_var_name;
-    bool             m_cheap_eqs;
+    unsigned         m_cheap_eqs;
 public:
     bool print_external_var_name() const { return m_print_external_var_name; }
     bool& print_external_var_name() { return m_print_external_var_name; }
-    bool cheap_eqs() const { return m_cheap_eqs;}
+    unsigned cheap_eqs() const { return m_cheap_eqs;}
-    bool& cheap_eqs() { return m_cheap_eqs;}
+    unsigned& cheap_eqs() { return m_cheap_eqs;}
     unsigned hnf_cut_period() const { return m_hnf_cut_period; }
     void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period;  }
     unsigned random_next() { return m_rand(); }

src/smt/params/smt_params_helper.pyg

@@ -41,7 +41,7 @@ def_module_params(module_name='smt',
                           ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'),
                           ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
                           ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
-                          ('arith.cheap_eqs', BOOL, True, 'true for extracting cheap equalities'),
+                          ('arith.cheap_eqs', UINT, 0, '0 - do not run, 1 - use tree, 2 - use table'),
                           ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),
                           ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'),
                           ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'),

src/smt/theory_lra.cpp

@@ -1593,6 +1593,19 @@ public:
         m_variable_values.clear();
     }
     
+    bool congruent_or_irrelevant(lpvar k, lpvar j) {
+        theory_var kv = lp().local_to_external(k);
+        if (kv == null_theory_var)
+            return true;
+        theory_var jv = lp().local_to_external(j);
+        if (jv == null_theory_var)
+            return true;
+        
+        enode * n0 = get_enode(kv);
+        enode * n1 = get_enode(jv);
+        return n0->get_root() == n1->get_root();
+    }
+
     void random_update() {
         if (m_nla)
             return;