do not use nl variables in random_update()

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

src/math/lp/emonics.h

@@ -325,6 +325,8 @@ public:
 
     bool is_monic_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
 
+    bool is_used_in_monic(lpvar v) const { return v < m_use_lists.size() && m_use_lists[v].m_head != nullptr; }
+
     bool elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector> &lists) const;
     
 }; // end of emonics

src/math/lp/lar_solver.cpp

@@ -1439,15 +1439,11 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v
     for (unsigned i = 0; i < sz; i++) {        
         var_index var = vars[i];
         if (var >= m_terms_start_index) { // handle the term
-            lpvar j = adjust_term_index(var);
-            if (column_is_int(j))
-                continue;
             for (auto it : *m_terms[var - m_terms_start_index]) {
                 column_list.push_back(it.var());
             }
         } else {
-            if (!column_is_int(var))
-                column_list.push_back(var);
+            column_list.push_back(var);
         }
     }
 }

src/math/lp/nla_core.cpp

@@ -1712,4 +1712,25 @@ unsigned core::get_var_weight(lpvar j) const {
 }
 
 
+bool core::is_nl_var(lpvar j) const {
+    if (is_monic_var(j))
+        return true;
+    return m_emons.is_used_in_monic(j);
+}
+
+
+
+bool core::influences_nl_var(lpvar j) const {
+    if (m_lar_solver.is_term(j))
+        j = m_lar_solver.adjust_term_index(j);
+    if (is_nl_var(j))
+        return true;
+    for (const auto & c : m_lar_solver.A_r().m_columns[j]) {
+        lpvar basic_in_row = m_lar_solver.r_basis()[c.var()];
+        if (is_nl_var(basic_in_row))
+            return true;        
+    }
+    return false;
+}
+
 } // end of nla

src/math/lp/nla_core.h

@@ -412,6 +412,9 @@ public:
     dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
     void set_level2var_for_grobner();
     void configure_grobner();
+    bool influences_nl_var(lpvar) const;
+    bool is_nl_var(lpvar) const;
+    bool is_used_in_monic(lpvar) const;
 };  // end of core
 
 struct pp_mon {

src/math/lp/nla_solver.cpp

@@ -51,6 +51,10 @@ void solver::pop(unsigned n) {
 solver::solver(lp::lar_solver& s): m_core(alloc(core, s, m_res_limit))  {
 }
 
+bool solver::influences_nl_var(lpvar j) const {    
+    return m_core->influences_nl_var(j);
+}
+
 solver::~solver() {
     dealloc(m_core);
 }

src/math/lp/nla_solver.h

@@ -44,5 +44,6 @@ public:
     bool need_check();
     lbool check(vector<lemma>&);
     bool is_monic_var(lpvar) const;
+    bool influences_nl_var(lpvar) const;
 };
 }

src/smt/theory_lra.cpp

@@ -1597,12 +1597,35 @@ public:
         m_variable_values.clear();
     }
 
+    bool influences_nl_var(theory_var v) const {
+        if (!m_use_nla)            
+            return false; // that is the legacy solver behavior
+        if (!m_nla)
+            return false;
+            
+        return m_nla->influences_nl_var(get_lpvar(v));
+    }
+    
+    bool can_be_used_in_random_update(theory_var v) const {
+        if (!th.is_relevant_and_shared(get_enode(v)))
+            return false;
+
+        if (is_int(v))
+            return false;
+
+        if (influences_nl_var(v))
+            return false;
+        
+        return true;
+    }
+    
     bool assume_eqs() {        
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
         for (theory_var v = 0; v < sz; ++v) {
-            if (th.is_relevant_and_shared(get_enode(v))) { 
-                vars.push_back(get_lpvar(v));
+            if (th.is_relevant_and_shared(get_enode(v))) {
+                if (can_be_used_in_random_update(v))
+                    vars.push_back(get_lpvar(v));
             }
         }
         if (vars.empty()) {