factor out coi, use polynomial elaboration for nlsat solver (#8039)

* factor out coi, use polynomial elaboration for nlsat solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Author: NikolajBjorner

src/ast/sls/sls_arith_base.cpp

@@ -2620,8 +2620,10 @@ namespace sls {
                 display(out, ad) << "\n";
             }
         };
-        for (var_t v = 0; v < m_vars.size(); ++v) {
+        for (var_t v = 0; v < m_vars.size(); ++v) {            
             if (!eval_is_correct(v)) {
+//                if (m.rlimit().is_canceled())
+//                    return;
                 report_error(verbose_stream(), v);
                 TRACE(arith, report_error(tout, v));
                 UNREACHABLE();

src/math/lp/CMakeLists.txt

@@ -24,6 +24,7 @@ z3_add_component(lp
     monomial_bounds.cpp
     nex_creator.cpp
     nla_basics_lemmas.cpp
+    nla_coi.cpp
     nla_common.cpp
     nla_core.cpp
     nla_divisions.cpp

src/math/lp/nla_coi.cpp

@@ -0,0 +1,88 @@
+
+/*++
+  Copyright (c) 2025 Microsoft Corporation
+
+  Author:
+    Lev Nachmanson (levnach)
+    Nikolaj Bjorner (nbjorner)
+  --*/
+
+#include "math/lp/nla_core.h"
+#include "math/lp/nla_coi.h"
+
+namespace nla {
+
+  void coi::init() {
+      indexed_uint_set visited;
+      unsigned_vector todo;
+      vector<occurs> var2occurs;
+      m_term_set.reset();
+      m_mon_set.reset();
+      m_constraint_set.reset();
+      m_var_set.reset();
+      auto& lra = c.lra_solver();
+
+      for (auto ci : lra.constraints().indices()) {
+          auto const& c = lra.constraints()[ci];
+          if (c.is_auxiliary())
+              continue;
+          for (auto const& [coeff, v] : c.coeffs()) {
+              var2occurs.reserve(v + 1);
+              var2occurs[v].constraints.push_back(ci);
+          }
+      }
+
+      for (auto const& m : c.emons()) {
+          for (auto v : m.vars()) {
+              var2occurs.reserve(v + 1);
+              var2occurs[v].monics.push_back(m.var());
+          }
+      }
+
+      for (const auto *t :  lra.terms() ) {
+          for (auto const iv : *t) {
+              auto v = iv.j();
+              var2occurs.reserve(v + 1);
+              var2occurs[v].terms.push_back(t->j());
+          }
+      }
+
+      for (auto const& m : c.to_refine())
+          todo.push_back(m);
+
+      for (unsigned i = 0; i < todo.size(); ++i) {
+          auto v = todo[i];
+          if (visited.contains(v))
+              continue;
+          visited.insert(v);
+          m_var_set.insert(v);
+          var2occurs.reserve(v + 1);
+          for (auto ci : var2occurs[v].constraints) {
+              m_constraint_set.insert(ci);
+              auto const& c = lra.constraints()[ci];
+              for (auto const& [coeff, w] : c.coeffs())
+                  todo.push_back(w);
+          }
+          for (auto w : var2occurs[v].monics)
+              todo.push_back(w);
+
+          for (auto ti : var2occurs[v].terms) {
+              for (auto iv : lra.get_term(ti))
+                  todo.push_back(iv.j());
+              todo.push_back(ti);
+          }
+
+          if (lra.column_has_term(v)) {
+              m_term_set.insert(v);
+              for (auto kv : lra.get_term(v))
+                  todo.push_back(kv.j());
+          }            
+
+          if (c.is_monic_var(v)) {
+              m_mon_set.insert(v);
+              for (auto w : c.emons()[v])
+                  todo.push_back(w);
+          }
+      }
+  }
+}

src/math/lp/nla_coi.h

@@ -0,0 +1,43 @@
+
+/*++
+  Copyright (c) 2025 Microsoft Corporation
+
+  Abstract:
+    Class for computing the cone of influence for NL constraints.
+    It includes variables that come from monomials that have incorrect evaluation and
+    transitively all constraints and variables that are connected.
+
+  Author:
+    Lev Nachmanson (levnach)
+    Nikolaj Bjorner (nbjorner)
+  --*/
+
+#pragma once
+
+namespace nla {
+
+    class core;
+
+    class coi {
+        core& c;
+        indexed_uint_set m_mon_set, m_constraint_set;
+        indexed_uint_set m_term_set, m_var_set;
+
+        struct occurs {
+            unsigned_vector constraints;
+            unsigned_vector monics;
+            unsigned_vector terms;
+        };
+
+    public:
+        coi(core& c) : c(c) {}
+
+        void init();        
+
+        indexed_uint_set const& mons() const { return m_mon_set; }
+        indexed_uint_set const& constraints() const { return m_constraint_set; }
+        indexed_uint_set& terms() { return m_term_set; }
+        indexed_uint_set const &vars() { return m_var_set; }
+
+    };
+}

src/math/lp/nla_core.h

@@ -450,6 +450,12 @@ class core {
     nla_throttle& throttle() { return m_throttle; }
     const nla_throttle& throttle() const { return m_throttle; }
 
+    lp::lar_solver& lra_solver() { return lra; }
+
+    indexed_uint_set const& to_refine() const {
+        return m_to_refine;
+    }
+
 };  // end of core
 
 struct pp_mon {