From 8d1e954709fbeba1408ea27a2bc182add4839663 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Jun 2025 20:37:51 -0700
Subject: [PATCH] introduce notion of auxiliary constraints created by
 nla_solver lemmas

notes: auxiliary constraints could extend to Gomory and B&B.
---
 src/math/lp/lar_constraints.h | 13 +++++++++++--
 src/math/lp/lar_solver.cpp    |  8 ++++++++
 src/math/lp/lar_solver.h      |  6 ++++++
 src/math/lp/nra_solver.cpp    |  2 ++
 src/smt/theory_lra.cpp        |  2 ++
 5 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h
index 1105382e7..7b9acaf97 100644
--- a/src/math/lp/lar_constraints.h
+++ b/src/math/lp/lar_constraints.h
@@ -41,14 +41,15 @@ class lar_base_constraint {
     lconstraint_kind m_kind;
     mpq              m_right_side;
     bool             m_active;
+    bool             m_is_auxiliary;
     unsigned         m_j;
     u_dependency*    m_dep;
 
-   public:
+public:
 
     virtual vector<std::pair<mpq, lpvar>> coeffs() const = 0;
     lar_base_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) :
-        m_kind(kind), m_right_side(right_side), m_active(false), m_j(j), m_dep(dep) {}
+        m_kind(kind), m_right_side(right_side), m_active(false), m_is_auxiliary(false), m_j(j), m_dep(dep) {}
     virtual ~lar_base_constraint() = default;
 
     lconstraint_kind kind() const { return m_kind; }
@@ -60,6 +61,9 @@ class lar_base_constraint {
     void deactivate() { m_active = false; }
     bool is_active() const { return m_active; }
 
+    bool is_auxiliary() const { return m_is_auxiliary; }
+    void set_auxiliary() { m_is_auxiliary = true; }
+
     virtual unsigned size() const = 0;
     virtual mpq get_free_coeff_of_left_side() const { return zero_of_type<mpq>();}
 };
@@ -96,10 +100,13 @@ class constraint_set {
     stacked_value<unsigned>        m_constraint_count;
     unsigned_vector                m_active;
     stacked_value<unsigned>        m_active_lim;    
+    bool                           m_is_auxiliary_mode = false;
 
     constraint_index add(lar_base_constraint* c) {
         constraint_index ci = m_constraints.size();
         m_constraints.push_back(c);
+        if (m_is_auxiliary_mode)
+            c->set_auxiliary();
         return ci;
     }
 
@@ -146,6 +153,8 @@ public:
             c->~lar_base_constraint();
     }
 
+    void set_auxiliary(bool m) { m_is_auxiliary_mode = m; }
+
     void push() {
         m_constraint_count = m_constraints.size();
         m_constraint_count.push();
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 68c97cec3..0fd257685 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1744,6 +1744,14 @@ namespace lp {
         A_r().m_columns.pop_back();
     }
 
+    lar_solver::scoped_auxiliary::scoped_auxiliary(lar_solver& s) : s(s) {
+        s.m_imp->m_constraints.set_auxiliary(true);
+    }
+
+    lar_solver::scoped_auxiliary::~scoped_auxiliary() {
+        s.m_imp->m_constraints.set_auxiliary(false);
+    }
+
     void lar_solver::remove_last_column_from_basis_tableau(unsigned j) {
         auto& rslv = get_core_solver().m_r_solver;
         int i = rslv.m_basis_heading[j];
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 12ce46a46..468601aa2 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -319,6 +319,12 @@ public:
     bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side);
     lpvar add_term(const vector<std::pair<mpq, lpvar>>& coeffs, unsigned ext_i);
     void register_existing_terms();
+    class scoped_auxiliary {
+        lar_solver& s;
+    public:
+        scoped_auxiliary(lar_solver& s);
+        ~scoped_auxiliary();
+    };
     constraint_index add_var_bound(lpvar, lconstraint_kind, const mpq&);
     constraint_index add_var_bound_check_on_equal(lpvar, lconstraint_kind, const mpq&, lpvar&);
 
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index d8269e7f6..5603c4aed 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -63,6 +63,8 @@ struct solver::imp {
 
         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);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fd71ac433..252bf473f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2040,6 +2040,8 @@ public:
     }
 
     final_check_status check_nla() {
+        // TODO - enable or remove if found useful internals are corrected:
+        // lp::lar_solver::scoped_auxiliary _sa(lp()); // new atoms are auxilairy and are not used in nra_solver
         if (!m.inc()) {
             TRACE(arith, tout << "canceled\n";);
             return FC_GIVEUP;