From 939091e2b5d8327685e1fe2804041d8351c80e0a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 7 Mar 2025 15:51:12 -1000
Subject: [PATCH] fix write_bound_lemma to include term definitions

---
 src/math/lp/dioph_eq.cpp   |  4 +-
 src/math/lp/lar_solver.cpp | 80 +++++++++++++++++++++++++++++---------
 2 files changed, 63 insertions(+), 21 deletions(-)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index f50ee5964..e31493189 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1848,10 +1848,8 @@ namespace lp {
             SASSERT((upper && bound < lra.get_upper_bound(j).x) ||
                     (!upper && bound > lra.get_lower_bound(j).x));
             lconstraint_kind kind = upper ? lconstraint_kind::LE : lconstraint_kind::GE;
-            u_dependency* dep = lra.get_bound_constraint_witnesses_for_column(j);
+            u_dependency* dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j);
             dep = lra.join_deps(dep, explain_fixed_in_meta_term(m_lspace.m_data));
-            u_dependency* j_bound_dep = upper ? lra.get_column_upper_bound_witness(j) : lra.get_column_lower_bound_witness(j);
-            dep = lra.join_deps(dep, j_bound_dep);
             dep = lra.join_deps(dep, explain_fixed(lra.get_term(j)));
             TRACE("dio", tout << "jterm:";
                   print_lar_term_L(lra.get_term(j), tout) << "\ndep:";
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 07ecc867d..bff371d0d 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2584,20 +2584,20 @@ namespace lp {
                 return;
             }
         }
-    
-        // Start SMT2 file
+            // Start SMT2 file
         out << "(set-info : \"generated at " << location;
         out << " for " << (is_low ? "lower" : "upper") << " bound of variable " << j << ",";
         out << " bound value: " << bound_val << (is_strict ? (is_low ? " < " : " > ") : (is_low ? " <= " : " >= ")) << "x" << j << "\")\n";
-    
+        
         // Collect all variables used in dependencies
         std::unordered_set<unsigned> vars_used;
         vars_used.insert(j);
         bool is_int = column_is_int(j);
+        
         // Linearize the dependencies
         svector<constraint_index> deps;
         m_dependencies.linearize(bound_dep, deps);
-    
+        
         // Collect variables from constraints
         for (auto ci : deps) {
             const auto& c = m_constraints[ci];
@@ -2607,31 +2607,75 @@ namespace lp {
                     is_int = false;
             }
         }
-            
+        
+        // Collect variables from terms
+        std::unordered_set<unsigned> term_variables;
+        for (unsigned var : vars_used) {
+            if (column_has_term(var)) {
+                const lar_term& term = get_term(var);
+                for (const auto& p : term) {
+                    term_variables.insert(p.j());
+                    if (!column_is_int(p.j()))
+                        is_int = false;
+                }
+            }
+        }
+        // Add term variables to vars_used
+        vars_used.insert(term_variables.begin(), term_variables.end());
+                
         if (is_int) {
             out << "(set-logic QF_LIA)\n\n";
         }
-    
+        
         // Declare variables
         out << "; Variable declarations\n";
         for (unsigned var : vars_used) {
             out << "(declare-const x" << var << " " << (column_is_int(var) ? "Int" : "Real") << ")\n";
         }
         out << "\n";
-    
+        
+        // Define term relationships
+        out << "; Term definitions\n";
+        for (unsigned var : vars_used) {
+            if (column_has_term(var)) {
+                const lar_term& term = get_term(var);
+                out << "(assert (= x" << var << " ";
+                    
+                if (term.size() == 0) {
+                    out << "0";
+                } else {
+                    if (term.size() > 1) out << "(+ ";
+                        
+                    bool first = true;
+                    for (const auto& p : term) {
+                        if (first) first = false;
+                        else out << " ";
+                            
+                        if (p.coeff().is_one()) {
+                            out << "x" << p.j();
+                        } else {
+                            out << "(* " << format_smt2_constant(p.coeff()) << " x" << p.j() << ")";
+                        }
+                    }
+                        
+                    if (term.size() > 1) out << ")";
+                }
+                    
+                out << "))\n";
+            }
+        }
+        out << "\n";
+        
         // Add assertions for the dependencies
         out << "; Bound dependencies\n";
-    
+        
         for (auto ci : deps) {
             const auto& c = m_constraints[ci];
             out << "(assert ";
-        
+            
             // Handle the constraint type and expression
             auto k = c.kind();
-        
-            // Handle empty constraint (just constant)
-            SASSERT(c.coeffs().size());
-        
+            
             // Normal constraint with variables
             switch (k) {
             case LE: out << "(<= "; break;
@@ -2641,7 +2685,7 @@ namespace lp {
             case EQ: out << "(= "; break;
             default: out << "(unknown-constraint-type "; break;
             }
-        
+            
             // Left-hand side (variables)
             if (c.coeffs().size() == 1) {
                 // Single variable
@@ -2663,13 +2707,13 @@ namespace lp {
                 }
                 out << ") ";
             }
-        
+            
             // Right-hand side (constant)
             out << format_smt2_constant(c.rhs());
             out << "))\n";
         }
         out << "\n";
-    
+        
         // Now add the assertion that contradicts the bound
         out << "; Negation of the derived bound\n";
         if (is_low) {
@@ -2686,11 +2730,11 @@ namespace lp {
             }
         }
         out << "\n";
-    
+        
         // Check sat and get model if available
         out << "(check-sat)\n";
         out << "(exit)\n";
-    }
+        }
 } // namespace lp