From 06173aa4d79bcb97eeca8672e12b62402798fa25 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 4 Feb 2020 11:51:37 -0800
Subject: [PATCH] do not use nl variables in random_update()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/emonics.h      |  2 ++
 src/math/lp/lar_solver.cpp |  6 +-----
 src/math/lp/nla_core.cpp   | 21 +++++++++++++++++++++
 src/math/lp/nla_core.h     |  3 +++
 src/math/lp/nla_solver.cpp |  4 ++++
 src/math/lp/nla_solver.h   |  1 +
 src/smt/theory_lra.cpp     | 27 +++++++++++++++++++++++++--
 7 files changed, 57 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 04feab465..7daa1281f 100644
--- a/src/math/lp/emonics.h
+++ b/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
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index b766cfeac..c18ee75ba 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/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);
         }
     }
 }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 0d15fd0be..f87497067 100644
--- a/src/math/lp/nla_core.cpp
+++ b/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
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index b032de5b3..d86ea83aa 100644
--- a/src/math/lp/nla_core.h
+++ b/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 {
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 56a74582b..4833ceb98 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/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);
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 5a0d5cb05..cefce8c81 100644
--- a/src/math/lp/nla_solver.h
+++ b/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;
 };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fc33ad1ce..d86f5cb01 100644
--- a/src/smt/theory_lra.cpp
+++ b/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()) {