From ad063580dc0abded9dd08bf2105965726b90a250 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jul 2026 22:46:06 -0700 Subject: [PATCH] theory_lra: eagerly propagate offset equalities x=y (fixes #10065) When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca), theory_lra previously discovered the implied equality x = y only lazily via assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065 this discovery is starved by E-matching, which unfolds the recursion and bit-blasts an exploding FP subproblem before the branch closes. Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite unit-scaled coefficients and propagate the operand equality x = y directly to the core, so congruence closure merges dependent terms immediately. This mirrors the offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e --- src/math/lp/lp_api.h | 2 ++ src/smt/theory_lra.cpp | 48 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+) diff --git a/src/math/lp/lp_api.h b/src/math/lp/lp_api.h index 56dcb95414..3927040950 100644 --- a/src/math/lp/lp_api.h +++ b/src/math/lp/lp_api.h @@ -108,6 +108,7 @@ namespace lp_api { unsigned m_num_iterations_with_no_progress; unsigned m_need_to_solve_inf; unsigned m_fixed_eqs; + unsigned m_offset_eqs; unsigned m_conflicts; unsigned m_bound_propagations1; unsigned m_bound_propagations2; @@ -129,6 +130,7 @@ namespace lp_api { st.update("arith-pivots", m_need_to_solve_inf); st.update("arith-plateau-iterations", m_num_iterations_with_no_progress); st.update("arith-fixed-eqs", m_fixed_eqs); + st.update("arith-offset-eqs", m_offset_eqs); st.update("arith-conflicts", m_conflicts); st.update("arith-bound-propagations-lp", m_bound_propagations1); st.update("arith-bound-propagations-cheap", m_bound_propagations2); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ba1e0238c6..0001428726 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3532,7 +3532,55 @@ public: ctx().assign_eq(x, y, eq_justification(js)); } + // + // Offset equality propagation. + // When the column t is a term c*x - c*y (two operands with opposite unit + // coefficients) that is fixed at 0, then x = y. Propagate this equality to + // the core so congruence closure can merge terms that depend on x and y. + // Without this, theory_lra only detects such equalities lazily through + // assume_eqs() during final_check, which can be starved (e.g. by E-matching) + // long before it fires. theory_arith performs the analogous propagation in + // propagate_cheap_eq (offset rows). + // + bool propagate_offset_eq(lp::lpvar t, u_dependency* dep, rational const& bound) { + if (!bound.is_zero()) + return false; + if (!lp().column_has_term(t)) + return false; + u_map coeffs; + term2coeffs(lp().get_term(t), coeffs); + if (coeffs.size() != 2) + return false; + auto it = coeffs.begin(); + theory_var w1 = it->m_key; + rational c1 = it->m_value; + ++it; + theory_var w2 = it->m_key; + rational c2 = it->m_value; + if (c1 + c2 != 0) + return false; + if (w1 == w2) + return false; + enode* x = get_enode(w1); + enode* y = get_enode(w2); + if (!x || !y) + return false; + if (x->get_sort() != y->get_sort()) + return false; + if (x->get_root() == y->get_root()) + return false; + if (is_int(w1) != is_int(w2)) + return false; + reset_evidence(); + set_evidence(dep, m_core, m_eqs); + ++m_stats.m_offset_eqs; + assign_eq(w1, w2); + return true; + } + void fixed_var_eh(theory_var v, lp::lpvar t, u_dependency* dep, rational const& bound) { + if (propagate_offset_eq(t, dep, bound)) + return; theory_var w = null_theory_var; enode* x = get_enode(v); if (m_value2var.find(bound, w))