From 29b5c47a8d416d2ab1ff2008626c845b58b25d01 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 27 Sep 2023 09:09:38 -0700
Subject: [PATCH] track changed monics efficiently

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp   | 21 ++++++++++-----------
 src/math/lp/nla_core.h     |  3 +--
 src/math/lp/nla_solver.cpp |  1 -
 src/math/lp/nla_solver.h   |  1 -
 4 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index fe4c1a29a..97c9c82d9 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -43,18 +43,17 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim, std_vector<lp:
     m_implied_bounds(implied_bounds) {
     m_nlsat_delay = lp_settings().nlsat_delay();
     lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
-    for (const auto& m : m_emons) {
-        if (columns_with_changed_bounds.contains(m.var())) {
-            m_monics_with_changed_bounds.push_back(m.var());
-            continue;
+        m_monics_with_changed_bounds.reset();
+        for (lpvar j : columns_with_changed_bounds) {
+            if (is_monic_var(j))
+                m_monics_with_changed_bounds.insert(j);
+            else {
+                for (const auto & m: m_emons.get_use_list(j)) {
+                    m_monics_with_changed_bounds.insert(m.var());
+                }
+            }    
         }
-        for (lpvar j : m.vars()) {
-            if (columns_with_changed_bounds.contains(j)) {
-                m_monics_with_changed_bounds.push_back(m.var());
-                break;
-            }
-        }
-    } };
+    };
 }
 
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index b2bb6b348..d5feac8a2 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -88,7 +88,7 @@ class core {
     vector<lemma>            m_lemmas;
     vector<ineq> *           m_literal_vec = nullptr;
     indexed_uint_set         m_to_refine;
-    vector<lpvar>            m_monics_with_changed_bounds;
+    indexed_uint_set         m_monics_with_changed_bounds;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
@@ -125,7 +125,6 @@ public:
     // constructor
     core(lp::lar_solver& s, params_ref const& p, reslimit&, std_vector<lp::implied_bound> & implied_bounds);
     const auto& monics_with_changed_bounds() const { return m_monics_with_changed_bounds; }
-    void reset_monics_with_changed_bounds() { m_monics_with_changed_bounds.reset(); }
     void insert_to_refine(lpvar j);
     void erase_from_to_refine(lpvar j);
     
diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index 236b85d4f..144ecefd3 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -112,6 +112,5 @@ namespace nla {
         init_bound_propagation();
         for (unsigned v : monics_with_changed_bounds()) 
             calculate_implied_bounds_for_monic(v);        
-        reset_monics_with_changed_bounds();
     }
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index 0448d840f..0fe9733f1 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -27,7 +27,6 @@ namespace nla {
         solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
         ~solver();
         const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); }
-        void reset_monics_with_changed_bounds() { m_core->reset_monics_with_changed_bounds(); } 
         void add_monic(lpvar v, unsigned sz, lpvar const* vs);
         void add_idivision(lpvar q, lpvar x, lpvar y);
         void add_rdivision(lpvar q, lpvar x, lpvar y);