separate out bounds

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

src/math/lp/CMakeLists.txt

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

src/math/lp/nla_bounds.cpp

@@ -0,0 +1,42 @@
+
+/*++
+  Copyright (c) 2025 Microsoft Corporation
+
+  Module Name:
+
+  nla_bounds.cpp
+
+  Author:
+    Lev Nachmanson (levnach)
+    Nikolaj Bjorner (nbjorner)
+
+--*/
+
+#include "nla_bounds.h"
+#include "nla_core.h"
+
+
+namespace nla {
+
+    bounds::bounds(core *c) : common(c) {}
+
+    // looking for a free variable inside of a monic to split
+    void bounds::operator()() {
+        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;
+            }
+        }
+    }
+}  // namespace nla

src/math/lp/nla_bounds.h

@@ -0,0 +1,40 @@
+
+/*++
+  Copyright (c) 2025 Microsoft Corporation
+
+  Module Name:
+
+  nla_bounds.h
+
+  Author:
+    Lev Nachmanson (levnach)
+    Nikolaj Bjorner (nbjorner)
+
+  Abstract:
+     Create bounds for variables that occur in non-linear monomials.
+     The bounds should ensure that variables are either fixes at -1, 0, 1, below or above these values.
+     This ensures that basic lemmas that case split on values -1, 0, 1 are robust under model changes.
+
+--*/
+#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 {
+    public:
+        bounds(core *core);
+        void operator()();
+    
+    };
+
+}  // namespace nla

src/math/lp/nla_core.cpp

@@ -37,7 +37,8 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     m_monomial_bounds(this),
     m_stellensatz(this),
     m_horner(this),
-    m_grobner(this),
+    m_grobner(this), 
+    m_bounds(this),
     m_emons(m_evars),
     m_use_nra_model(false),
     m_nra(s, m_nra_lim, *this, p),
@@ -1268,24 +1269,6 @@ void core::check_bounded_divisions() {
     clear();
     m_divisions.check_bounded_divisions();
 }
-// looking for a free variable inside of a monic to split
-void core::add_bounds() {
-    for (auto i : m_to_refine) {
-        auto const& m = m_emons[i];
-        for (lpvar j : m.vars()) {
-            if (!var_is_free(j))
-                continue;
-	    if (m.is_bound_propagated())
-                continue;
-	    m_emons.set_bound_propagated(m);
-            // split the free variable (j <= 0, or j > 0), and return
-            m_literals.push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
-            TRACE(nla_solver, print_ineq(m_literals.back(), tout) << "\n");                  
-            ++lp_settings().stats().m_nla_add_bounds;
-            return;
-        }
-    }    
-}
 
 lbool core::check() {
     lp_settings().stats().m_nla_calls++;
@@ -1321,7 +1304,7 @@ lbool core::check() {
     {
         std::function<void(void)> check1 = [&]() { if (no_effect() && run_horner) m_horner.horner_lemmas(); };
         std::function<void(void)> check2 = [&]() { if (no_effect() && run_grobner) m_grobner(); };
-        std::function<void(void)> check3 = [&]() { if (no_effect() && run_bounds) add_bounds(); };
+        std::function<void(void)> check3 = [&]() { if (no_effect() && run_bounds) m_bounds(); };
 
         std::pair<unsigned, std::function<void(void)>> checks[] =
             { {1, check1},

src/math/lp/nla_core.h

@@ -14,14 +14,15 @@
 #include "math/lp/factorization.h"
 #include "math/lp/lp_types.h"
 #include "math/lp/var_eqs.h"
-#include "math/lp/nla_tangent_lemmas.h"
 #include "math/lp/nla_basics_lemmas.h"
-#include "math/lp/nla_order_lemmas.h"
+#include "math/lp/nla_bounds.h"
-#include "math/lp/nla_monotone_lemmas.h"
-#include "math/lp/nla_grobner.h"
-#include "math/lp/nla_powers.h"
 #include "math/lp/nla_divisions.h"
+#include "math/lp/nla_grobner.h"
+#include "math/lp/nla_monotone_lemmas.h"
+#include "math/lp/nla_order_lemmas.h"
+#include "math/lp/nla_powers.h"
 #include "math/lp/nla_stellensatz.h"
+#include "math/lp/nla_tangent_lemmas.h"
 #include "math/lp/emonics.h"
 #include "math/lp/nex.h"
 #include "math/lp/horner.h"
@@ -95,6 +96,7 @@ class core {
     bool                     m_check_feasible = false;
     horner                   m_horner;
     grobner                  m_grobner;
+    bounds                   m_bounds;
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable indexed_uint_set m_active_var_set;
@@ -113,7 +115,6 @@ class core {
 
 
     void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
-    void add_bounds();
 
     bool refine_pseudo_linear();
     bool is_pseudo_linear(monic const& m) const;    
@@ -454,6 +455,9 @@ public:
     bool use_nra_model() const { return m_use_nra_model; }
     vector<nla::lemma> const& lemmas() const { return m_lemmas; }
     vector<nla::ineq> const& literals() const { return m_literals; }
+    void add_literal(const ineq &n) {
+        m_literals.push_back(n);
+    }
     vector<lp::equality> const& equalities() const { return m_equalities; }
     vector<lp::fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
     bool should_check_feasible() const { return m_check_feasible; }

src/math/lp/nla_stellensatz.cpp

@@ -317,9 +317,11 @@ namespace nla {
         lhs.add_monomial(rational(1), j);
         if (non_unit != lp::null_lpvar) {
             lhs.add_monomial(rational(-sign), non_unit);
-            add_ineq(bounds, lhs, lp::lconstraint_kind::EQ, rational(0));
+            add_ineq(bounds, lhs, lp::lconstraint_kind::GE, rational(0));
+            add_ineq(bounds, lhs, lp::lconstraint_kind::LE, rational(0));
         } else {
-            add_ineq(bounds, lhs, lp::lconstraint_kind::EQ, rational(sign));
+            add_ineq(bounds, lhs, lp::lconstraint_kind::GE, rational(sign));
+            add_ineq(bounds, lhs, lp::lconstraint_kind::LE, rational(sign));
         }
     }
 
@@ -617,8 +619,8 @@ namespace nla {
 
         while (!to_refine.empty()) {
             lpvar j = to_refine.erase_min();            
-            IF_VERBOSE(2, verbose_stream() << "refining " << m_mon2vars[j] << "\n");
             unsigned sz = m_monomials_to_refine.size();
+            TRACE(arith, tout << "refining " << m_mon2vars[j] << " sz " << sz << "\n");
             eliminate(j);
             for (unsigned i = sz; i < m_monomials_to_refine.size(); ++i) {
                 auto e = m_monomials_to_refine.elem_at(i);
@@ -678,6 +680,7 @@ namespace nla {
                 // punt on equality constraints for now
             }
         }
+        TRACE(arith, tout << "eliminate " << m_mon2vars[mi] << " los: " << los << " his: " << his << "\n");
         if (los.empty() || his.empty())
             return;
         IF_VERBOSE(3, verbose_stream() << "lo " << los << " hi " << his << "\n");
@@ -1522,7 +1525,7 @@ namespace nla {
             TRACE(arith, s.display(tout));
             if (!s.saturate_factors())
                 return l_false;
-            // s.saturate_constraints(); ?
+            s.saturate_constraints2();
             if (sz == lra_solver->number_of_vars())
                 return l_undef;
         }