From f977b48161daaebf68010ea9d64890a074667ed0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 17 Feb 2025 13:59:23 -0800
Subject: [PATCH] adjust solve_for to handle rationals

---
 src/math/lp/lar_solver.cpp |  5 +++--
 src/smt/theory_lra.cpp     | 33 +++++++++++++++++++--------------
 2 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 2836e6838..2ed233122 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -684,6 +684,7 @@ namespace lp {
             return;
         tabu.insert(j);
         IF_VERBOSE(10, verbose_stream() << "solve for " << j << " base " << is_base(j) << " " << column_is_fixed(j) << "\n");
+        TRACE("arith", tout << "solve for " << j << " base " << is_base(j) << " " << column_is_fixed(j) << "\n");
         if (column_is_fixed(j)) 
             return;
         
@@ -711,7 +712,6 @@ namespace lp {
         lp::impq lo, hi;
         bool lo_valid = true, hi_valid = true;
         for (auto const& v : t) {
-
             if (v.coeff().is_pos()) {
                 if (lo_valid && column_has_lower_bound(v.j()))
                     lo += column_lower_bound(v.j()) * v.coeff();
@@ -756,7 +756,8 @@ namespace lp {
             update_column_type_and_bound(j, hi.y == 0 ? lconstraint_kind::LE : lconstraint_kind::LT, hi.x, dep);
         }
 
-        if (!column_is_fixed(j)) 
+        TRACE("arith", print_term(t, tout << "j" << j << " := ") << "\n");
+        if (!column_is_fixed(j))             
             sols.push_back({j, t});
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ec83cc0d1..827175fb2 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3642,7 +3642,7 @@ public:
         term = a.mk_numeral(lp().get_value(j), a.is_int(n->get_expr()));
         reset_evidence();
         add_explain(j);
-        guard = extract_explain();
+        guard = mk_and(extract_explain());
     }
 
     void add_explain(unsigned j) {
@@ -3650,7 +3650,7 @@ public:
         set_evidence(d, m_core, m_eqs);
     }
 
-    expr_ref extract_explain() {
+    expr_ref_vector extract_explain() {
         expr_ref_vector es(m);
         for (auto [l, r] : m_eqs)
             es.push_back(a.mk_eq(l->get_expr(), r->get_expr()));
@@ -3665,32 +3665,34 @@ public:
             es[j++] = es.get(i);
         }
         es.shrink(j);
-        return mk_and(es);
+        return es;
     }
 
     void solve_term(enode* n, lp::lar_term & lt, expr_ref& term, expr_ref& guard) {
         bool is_int = a.is_int(n->get_expr());
         bool all_int = is_int;
         lp::lar_term t;
-        rational coeff(0);
+        rational coeff(0), lc(1);
         expr_ref_vector guards(m);
         reset_evidence();
+        // extract coeff
         for (auto const& cv : lt) {
+            all_int &= lp().column_is_int(cv.j());
             if (lp().column_is_fixed(cv.j())) {
                 coeff += lp().get_value(cv.j()) * cv.coeff();
                 add_explain(cv.j());
             }
-            else
+            else {
                 t.add_monomial(cv.coeff(), cv.j());
+                lc = lcm(denominator(cv.coeff()), lc);
+            }
         }
-        guards.push_back(extract_explain());
-        rational lc = denominator(coeff);
-        for (auto const& cv : t) {
-            lc = lcm(denominator(cv.coeff()), lc);
-            all_int &= lp().column_is_int(cv.j());
-        }
+        // extract lc
+        lc = lcm(lc, denominator(coeff));
+        
+        guards.append(extract_explain());
         if (lc != 1)
-            t *= lc, coeff *= lc;        
+            t *= lc, coeff *= lc;
         term = mk_term(t, is_int);
         if (coeff != 0)
             term = a.mk_add(term, a.mk_numeral(coeff, is_int));
@@ -3699,12 +3701,15 @@ public:
             guard = mk_and(guards);
             return;
         }
-        expr_ref lce(a.mk_numeral(lc, true), m);
+        expr_ref lce(a.mk_numeral(lc, is_int), m);
         if (all_int) 
             guards.push_back(m.mk_eq(a.mk_mod(term, lce), a.mk_int(0)));
         else if (is_int) 
             guards.push_back(a.mk_is_int(a.mk_div(term, lce)));
-        term = a.mk_idiv(term, lce);   
+        if (is_int)
+            term = a.mk_idiv(term, lce);
+        else
+            term = a.mk_div(term, lce);
         guard = mk_and(guards);
     }