From 9eb19b56c77be09b97d9b57fd5d4e6293ab10134 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 3 Mar 2025 07:43:37 -0800
Subject: [PATCH] a version where cut variables are excluded from recursive
 branch and cuts

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/gomory.cpp     |  6 +++++-
 src/math/lp/int_branch.cpp |  2 ++
 src/math/lp/int_solver.cpp | 16 ++++++++++++++++
 src/math/lp/int_solver.h   |  3 +++
 4 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index c6f9a4123..7dc167755 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -323,7 +323,7 @@ public:
         
         m_dep = nullptr;
         for (auto c : *m_ex) 
-         	m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
+            m_dep = lia.lra.join_deps(lia.lra.dep_manager().mk_leaf(c.ci()), m_dep);
 
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout);
               lia.lra.display(tout));
@@ -354,6 +354,9 @@ public:
         // 1) c is integral and x integral varible with an integral value
         // 2) the value of x is at a bound and has no infinitesimals.
 
+        if (lia.is_cut_var(k))
+            return false;
+
         
         unsigned j;
         for (const auto & p : row) {
@@ -491,6 +494,7 @@ public:
         };
         auto add_cut = [&](const lar_term& t, const mpq& k, u_dependency * dep) {
             lp::lpvar j = lra.add_term(t.coeffs_as_vector(), UINT_MAX);
+            lia.add_cut_var(j);
             lra.update_column_type_and_bound(j, lp::lconstraint_kind::GE,  k, dep); 
         };
         auto _check_feasible = [&](void) {
diff --git a/src/math/lp/int_branch.cpp b/src/math/lp/int_branch.cpp
index 3e3b9e555..b47686e9c 100644
--- a/src/math/lp/int_branch.cpp
+++ b/src/math/lp/int_branch.cpp
@@ -74,6 +74,8 @@ int int_branch::find_inf_int_base_column() {
         j = lra.r_basis()[k];
         if (!lia.column_is_int_inf(j))
             continue;
+        if (lia.is_cut_var(j))
+            continue;
         usage = lra.usage_in_terms(j);
         if (lia.is_boxed(j) &&  (range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x - rational(2*usage)) <= small_value) {
             result = j;
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index f39718c00..715f54eea 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -584,6 +584,22 @@ namespace lp {
         return lra.column_count();
     }
 
+    void int_solver::add_cut_var(unsigned j) {
+        struct insert : public trail {
+            uint_set& s;
+            unsigned j;
+            insert(uint_set& s, unsigned j): s(s), j(j) {}
+            void undo() override { s.remove(j); }            
+        };
+        m_cut_vars.insert(j);
+        lra.trail().push(insert(m_cut_vars, j));
+    }
+    
+    bool int_solver::is_cut_var(unsigned j) const {
+        return m_cut_vars.contains(j);
+    }
+
+
 
     static void set_lower(impq & l, bool & inf_l, impq const & v ) {
         if (inf_l || v > l) {
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index 2c42ec16f..8cfcd7867 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -46,6 +46,7 @@ class int_solver {
     lar_core_solver&    lrac;
     imp*                m_imp; 
     vector<equality>       m_equalities;
+    uint_set            m_cut_vars;
     bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
     bool is_boxed(unsigned j) const;
     bool is_free(unsigned j) const;
@@ -86,6 +87,8 @@ public:
     u_dependency* column_upper_bound_constraint(unsigned j) const;
     u_dependency* column_lower_bound_constraint(unsigned j) const;
     bool current_solution_is_inf_on_cut() const;
+    void add_cut_var(unsigned j);
+    bool is_cut_var(unsigned j) const;
 
     bool shift_var(unsigned j, unsigned range);
     std::ostream&  display_row_info(std::ostream & out, unsigned row_index) const;