From 6ba4ba142f6d006db5c410b080ee46a5a5167607 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Oct 2025 14:16:34 -0700
Subject: [PATCH] separate bounds introduction

---
 src/math/lp/nla_bounds.cpp      | 54 ++++++++++++++++++++++++++-------
 src/math/lp/nla_bounds.h        | 11 +++----
 src/math/lp/nla_stellensatz.cpp |  3 ++
 3 files changed, 50 insertions(+), 18 deletions(-)

diff --git a/src/math/lp/nla_bounds.cpp b/src/math/lp/nla_bounds.cpp
index 57b5a1ba2..23138f05c 100644
--- a/src/math/lp/nla_bounds.cpp
+++ b/src/math/lp/nla_bounds.cpp
@@ -25,18 +25,50 @@ namespace nla {
         for (lpvar i : c().to_refine()) {
             auto const &m = c().emons()[i];
             for (lpvar j : m.vars()) {
-                if (!c().var_is_free(j))
-                    continue;
-                if (m.is_bound_propagated())
-                    continue;
-                c().emons().set_bound_propagated(m);
-                // split the free variable (j <= 0, or j > 0), and return
-                auto i(ineq(j, lp::lconstraint_kind::LE, rational::zero()));
-                c().add_literal(i);
-                TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
-                ++c().lp_settings().stats().m_nla_add_bounds;
-                return;
+                if (add_bounds_to_free_variable(m, j) ||
+                    add_bounds_to_variable_at_value(j, 0) ||
+                    add_bounds_to_variable_at_value(j, 1) ||
+                    add_bounds_to_variable_at_value(j, -1)) {
+                    ++c().lp_settings().stats().m_nla_add_bounds;
+                    return;
+                }
             }
         }
     }
+
+    bool bounds::add_bounds_to_free_variable(monic const& m, lp::lpvar j) {
+        if (!c().var_is_free(j))
+            return false;
+        if (m.is_bound_propagated())
+            return false;
+        c().emons().set_bound_propagated(m);
+        // split the free variable (j <= 0, or j > 0), and return
+        auto i(ineq(j, lp::lconstraint_kind::LE, rational::zero()));
+        c().add_literal(i);
+        TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
+        return true;
+    }
+
+    bool bounds::add_bounds_to_variable_at_value(lp::lpvar j, int value) {
+        // disable new functionality
+        return false;
+        auto v = c().val(j);
+        if (v != value)
+            return false;
+        if (c().var_is_fixed(j))
+            return false;
+        // fix a bound that hasn't already been fixed.
+        if (c().has_lower_bound(j) && c().get_lower_bound(j) == value) {
+            auto i(ineq(j, lp::lconstraint_kind::LE, rational(value)));
+            TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
+            c().add_literal(i);
+        }
+        else {
+            auto i(ineq(j, lp::lconstraint_kind::GE, rational(value)));
+            TRACE(nla_solver, c().print_ineq(i, tout) << "\n");
+            c().add_literal(i);
+        }
+        return true;
+    }
+
 }  // namespace nla
diff --git a/src/math/lp/nla_bounds.h b/src/math/lp/nla_bounds.h
index 2d46f32fb..b710c646c 100644
--- a/src/math/lp/nla_bounds.h
+++ b/src/math/lp/nla_bounds.h
@@ -18,19 +18,16 @@
 --*/
 #pragma once
 
-
-
 #include "math/lp/nla_common.h"
-#include "math/lp/nla_intervals.h"
-#include "math/lp/nex.h"
-#include "math/lp/cross_nested.h"
-#include "util/uint_set.h"
-#include "math/grobner/pdd_solver.h"
+
 
 namespace nla {
     class core;
 
     class bounds : common {
+
+        bool add_bounds_to_free_variable(monic const& m, lp::lpvar j);
+        bool add_bounds_to_variable_at_value(lp::lpvar j, int i);
     public:
         bounds(core *core);
         void operator()();
diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index 1e5661be4..05632ddb8 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -58,6 +58,7 @@ namespace nla {
         saturate_basic_linearize();
         TRACE(arith, display(tout << "stellensatz after saturation\n"));
         lbool r = m_solver.solve();
+        // IF_VERBOSE(0, verbose_stream() << "stellensatz " << r << "\n");
         if (r == l_false)
             add_lemma();
         return r;
@@ -1507,9 +1508,11 @@ namespace nla {
     lbool stellensatz::solver::solve() {
         while (true) {
             lbool r = solve_lra();
+            // IF_VERBOSE(0, verbose_stream() << "solve lra " << r << "\n");
             if (r != l_true)
                 return r;
             r = solve_lia();
+            // IF_VERBOSE(0, verbose_stream() << "solve lia " << r << "\n");
             if (r != l_true)
                 return r;
             unsigned sz = lra_solver->number_of_vars();