From e709885e7267026790a3db8f18f511f718823dd5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Oct 2025 18:42:34 -0700
Subject: [PATCH] gcd reduce and use c().val for sign constraints

---
 .clang-format                   |  2 +-
 src/math/lp/nla_stellensatz.cpp | 12 ++++++++----
 src/math/lp/nla_stellensatz.h   |  1 +
 3 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/.clang-format b/.clang-format
index c6d1e16b7..174cf507e 100644
--- a/.clang-format
+++ b/.clang-format
@@ -8,7 +8,7 @@ BasedOnStyle: LLVM
 IndentWidth: 4
 TabWidth: 4
 UseTab: Never
-IndentCaseLabels: false
+
 
 
 
diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index 9154da7da..a990f560d 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -308,8 +308,8 @@ namespace nla {
         }
         bound_assumptions bounds{"units"};
         for (auto v : vars) {
-            if (m_values[v] == 1 || m_values[v] == -1) {
-                bound_assumption b(v, lp::lconstraint_kind::EQ, m_values[v]);
+            if (c().val(v) == 1 || c().val(v) == -1) {
+                bound_assumption b(v, lp::lconstraint_kind::EQ, c().val(v));
                 bounds.bounds.push_back(b);
             }
         }
@@ -396,7 +396,7 @@ namespace nla {
     rational stellensatz::mvalue(lp::lar_term const &t) const {
         rational r(0);
         for (auto cv : t)
-            r += m_values[cv.j()] * cv.coeff();
+            r += c().val(cv.j()) * cv.coeff();
         return r;
     }
 
@@ -474,6 +474,7 @@ namespace nla {
         }    
     }
 
+
     bool stellensatz::is_new_inequality(vector<std::pair<rational, lpvar>> lhs, lp::lconstraint_kind k,
                                         rational const &rhs) {
         std::stable_sort(lhs.begin(), lhs.end(),
@@ -487,6 +488,7 @@ namespace nla {
         return true;
     }
 
+
     lp::constraint_index stellensatz::add_ineq( 
         justification const& just, lp::lar_term & t, lp::lconstraint_kind k,
         rational const & rhs_) {
@@ -494,6 +496,7 @@ namespace nla {
         auto coeffs = t.coeffs_as_vector();
         gcd_normalize(coeffs, k, rhs);
 
+
         if (!is_new_inequality(coeffs, k, rhs))
             return lp::null_ci;
 
@@ -546,7 +549,6 @@ namespace nla {
         for (auto ci : constraints.indices()) 
             insert_monomials_from_constraint(ci);                    
 
-
         auto &constraints = m_solver.lra().constraints();
         unsigned initial_false_constraints = m_false_constraints.size();
         for (unsigned it = 0; it < m_false_constraints.size(); ++it) {
@@ -562,6 +564,7 @@ namespace nla {
                 continue;
 
             for (auto v : vars) {
+
                 if (v >= m_occurs.size())
                     continue;
                 for (unsigned cidx = 0; cidx < m_occurs[v].size(); ++cidx) {
@@ -598,6 +601,7 @@ namespace nla {
         // Eventually it can saturate to full pseudo-elimination of mx.
         // or better: a conflict or a solution.
 
+
         IF_VERBOSE(3, verbose_stream() << "saturate2\n");
         auto &constraints = m_solver.lra().constraints();
         for (auto ci : constraints.indices())
diff --git a/src/math/lp/nla_stellensatz.h b/src/math/lp/nla_stellensatz.h
index 3991ae024..35de3d6c0 100644
--- a/src/math/lp/nla_stellensatz.h
+++ b/src/math/lp/nla_stellensatz.h
@@ -211,6 +211,7 @@ namespace nla {
         lbool add_bounds(svector<lpvar> const &vars, vector<bound_assumption> &bounds);
         void saturate_constraints();
 
+
         void saturate_constraints2();
         void eliminate(lpvar mi);
         void ext_resolve(lpvar j, lp::constraint_index lo, lp::constraint_index hi);