From 0a0e925f27a5fde1c9d86c52a97123de9d31bb3c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 22 Sep 2025 11:26:48 +0300
Subject: [PATCH] updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/CMakeLists.txt       |  1 +
 src/math/lp/nla_core.h           |  1 +
 src/math/lp/nla_mul_saturate.cpp | 44 ++++++++++++++++++++++++++++++--
 src/math/lp/nla_mul_saturate.h   |  5 ++++
 4 files changed, 49 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt
index 5c156d38a..7dea022b2 100644
--- a/src/math/lp/CMakeLists.txt
+++ b/src/math/lp/CMakeLists.txt
@@ -30,6 +30,7 @@ z3_add_component(lp
     nla_grobner.cpp
     nla_intervals.cpp
     nla_monotone_lemmas.cpp
+    nla_mul_saturate.cpp
     nla_order_lemmas.cpp
     nla_powers.cpp
     nla_pp.cpp
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 6121a79a7..d8fa9d78e 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -60,6 +60,7 @@ class core {
     friend class monomial_bounds;
     friend class nra::solver;
     friend class divisions;
+    friend class mul_saturate;
 
     unsigned m_nlsat_delay = 0;
     unsigned m_nlsat_delay_bound = 0;
diff --git a/src/math/lp/nla_mul_saturate.cpp b/src/math/lp/nla_mul_saturate.cpp
index c366606a2..fe1a3a043 100644
--- a/src/math/lp/nla_mul_saturate.cpp
+++ b/src/math/lp/nla_mul_saturate.cpp
@@ -10,13 +10,53 @@
   Check if the system with new constraints is LP feasible.
   If it is not, then produce a lemma that explains the infeasibility.
 
+  The lemma is in terms of the original constraints and bounds.
+
   --*/
 
-#include "math/lp/nla_mul_saturate.h"
 #include "math/lp/nla_core.h"
+#include "math/lp/nla_mul_saturate.h"
+
 
 namespace nla {
 
-    mul_saturate::mul_saturate(core* core) : common(core) {}
+    mul_saturate::mul_saturate(core* core) : 
+        common(core), 
+        lra(m_core.lra) {}
 
+    lbool mul_saturate::saturate() {
+        lra.push();
+        for (auto j : c().m_to_refine) {
+            auto& m = c().emons()[j];
+            for (auto& con : lra.constraints().active()) {                
+                for (auto v : m.vars()) {
+                    for (auto [coeff, u] : con.coeffs()) {
+                        if (u == v) {
+                            // add new constraint
+                            // multiply by remaining vars
+                        }
+                    }
+                }
+            }
+        }       
+        // record new monomials that are created and recursively down-saturate with respect to these.
+
+        auto st = lra.solve();
+        lbool r = l_undef;
+        if (st == lp::lp_status::INFEASIBLE) {
+            // now we need to filter new constraints into bounds and old constraints.
+
+            r = l_false;
+        }
+        if (st == lp::lp_status::OPTIMAL || st == lp::lp_status::FEASIBLE) {
+            // TODO: check model just in case it got lucky.           
+        }
+        lra.pop(1);
+        return r;
+    }
+
+    lp::lar_base_constraint* mul_saturate::multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x) {
+
+        return nullptr;
+    }
 }
diff --git a/src/math/lp/nla_mul_saturate.h b/src/math/lp/nla_mul_saturate.h
index 5c1c273d2..fac751bb6 100644
--- a/src/math/lp/nla_mul_saturate.h
+++ b/src/math/lp/nla_mul_saturate.h
@@ -7,9 +7,14 @@
 namespace nla {
 
     class core;
+    class lar_solver;
     class mul_saturate : common {
+        lp::lar_solver& lra;
+        lp::lar_base_constraint* multiply_constraint(lp::lar_base_constraint const& c, monic const& m, lpvar x);
     public:
         mul_saturate(core* core);
+
+        lbool saturate();
     };
 
 }