From 5c9fd90031a94fe598c18f9dbeba22dd6b5565f0 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 7 Apr 2020 18:28:17 -0700
Subject: [PATCH] work on random_updates

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/lar_solver.cpp | 14 ++++++++++++++
 src/math/lp/lar_solver.h   |  2 ++
 src/smt/theory_lra.cpp     | 34 +++++++++++-----------------------
 3 files changed, 27 insertions(+), 23 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 4aca609d9..0d76ddf83 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1575,9 +1575,22 @@ var_index lar_solver::add_named_var(unsigned ext_j, bool is_int, const std::stri
     m_var_register.set_name(j, name);
     return j;
 }
+
+unsigned lar_solver::external_to_column_index(unsigned ext_j) const {
+    unsigned j = external_to_local(ext_j);            
+    if (j == null_lpvar)
+        return j;
+    
+    if (tv::is_term(j))
+        return map_term_index_to_column_index(j);
+    
+    return j;
+}
+
 var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
     TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;);
     var_index local_j;
+    SASSERT(!m_term_register.external_is_used(ext_j));
     lp_assert(!tv::is_term(ext_j));
     if (m_var_register.external_is_used(ext_j, local_j))
         return local_j;
@@ -1709,6 +1722,7 @@ bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>
 // do not register in m_var_register this term if ext_i == UINT_MAX
 var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i) {
     TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
+    SASSERT(!m_var_register.external_is_used(ext_i));
     m_term_register.add_var(ext_i, term_is_int(coeffs));   
     lp_assert(all_vars_are_registered(coeffs));
     if (strategy_is_undecided())
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index afb6db79c..399ea3ca8 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -134,6 +134,8 @@ public:
     void set_column_value(unsigned j, const impq& v) {
         m_mpq_lar_core_solver.m_r_x[j] = v;
     }
+
+    unsigned external_to_column_index(unsigned) const;
     
     const mpq& get_column_value_rational(unsigned j) const {
         if (tv::is_term(j)) {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index acc9165f0..ea579d667 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -265,7 +265,6 @@ class theory_lra::imp {
 
     svector<std::pair<theory_var, theory_var> >       m_assume_eq_candidates; 
     unsigned                                          m_assume_eq_head;
-    std::unordered_map<lp::impq, theory_var>          m_var_value_table;
     lp::u_set                                         m_tmp_var_set;
     
     unsigned                                          m_num_conflicts;
@@ -1588,7 +1587,7 @@ public:
 
     bool assume_eqs() {        
         svector<lpvar> vars;
-        m_var_value_table.clear();
+        m_model_eqs.reset();
         m_tmp_var_set.clear();
         m_tmp_var_set.resize(th.get_num_vars());
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
@@ -1600,37 +1599,26 @@ public:
             if (!th.is_relevant_and_shared(n1)) {
                 continue;
             }
-            lpvar vi = lp().external_to_local(v);            
-            if (vi == lp::null_lpvar)
+            lpvar vj = lp().external_to_column_index(v);            
+            if (vj == lp::null_lpvar)
                 continue;
-
-            if (lp::tv::is_term(vi)) {
-                vi = lp().map_term_index_to_column_index(vi);
-            }
-            const auto& vi_val = lp().get_column_value(vi);
-            auto it = m_var_value_table.find(vi_val);
-            if (it == m_var_value_table.end()) {
-                m_var_value_table[vi_val] = v;
+            theory_var other = m_model_eqs.insert_if_not_there(v);
+            if (other == v) {
                 continue;
             }
-            theory_var other = it->second;
-            SASSERT(other != v);
             enode * n2 = get_enode(other);
             if (n1->get_root() == n2->get_root())
                 continue;
-            if (!lp().column_is_fixed(vi)) {
-                vars.push_back(vi);
+            if (!lp().column_is_fixed(vj)) {
+                vars.push_back(vj);
             }
-            else if (!m_tmp_var_set.contains(other)) {
-                m_tmp_var_set.insert(other);
-                lpvar other_j = lp().external_to_local(other);
-                if (lp::tv::is_term(other_j)) {
-                    other_j = lp().map_term_index_to_column_index(other_j);
-                }               
+            else if (!m_tmp_var_set.contains(other) ) {
+                unsigned other_j = lp().external_to_column_index(other);
                 if (!lp().column_is_fixed(other_j)) {
+                    m_tmp_var_set.insert(other);
                     vars.push_back(other_j);
                 }
-            }            
+            } 
         }
         if (vars.empty()) {
             return false;