From fe100e78651786d5b9b20467bdc9cf1b4f75b7bd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 7 Apr 2026 11:54:43 -0400 Subject: [PATCH] Fix broken term_comparer in m_normalized_terms_to_columns lookup The `m_normalized_terms_to_columns` map in `lar_solver` uses a `term_comparer` that delegates to `lar_term::operator==`, which intentionally returns `false` (with comment "take care not to create identical terms"). This makes `fetch_normalized_term_column` unable to find any term, rendering the Horner module's `interval_from_term` bounds-recovery path dead code. History: `lar_term::operator==` returning `false` has been present since the original "merge LRA" commit (911b24784, 2018). The `m_normalized_terms_to_columns` lookup was added later (dfe0e856, c95f66e0, Aug 2019) as "toward fetching existing terms intervals from lar_solver". The initial code had `lp_assert(find == end)` on registration (always true with broken ==) and `lp_assert(find != end)` on deregister (always false). The very next commit (207c1c50, one day later) removed both asserts, replacing them with soft checks. The `term_comparer` struct delegating to `operator==` was introduced during a later PIMPL refactor (b375faa77). Fix: Replace the `term_comparer` implementation with a structural comparison that checks size and then verifies each coefficient-variable pair via `coeffs().find_core()`. This is localized to the `m_normalized_terms_to_columns` map and does not change `lar_term::operator==`, preserving its intentional semantics elsewhere. Validated: on a QF_UFNIA benchmark, `interval_from_term` lookups go from 0/573 successful to 34/573 successful. Unit test added for the `fetch_normalized_term_column` round-trip. Co-Authored-By: Claude Opus 4.6 (1M context) --- src/math/lp/lar_solver.cpp | 7 +++- src/test/nla_intervals.cpp | 71 +++++++++++++++++++++++++++++++++++++- 2 files changed, 76 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 6e689c004..ff5ff973e 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -36,7 +36,12 @@ namespace lp { struct term_comparer { bool operator()(const lar_term& a, const lar_term& b) const { - return a == b; + if (a.size() != b.size()) return false; + for (const auto& p : a) { + auto const* e = b.coeffs().find_core(p.j()); + if (!e || e->get_data().m_value != p.coeff()) return false; + } + return true; } }; diff --git a/src/test/nla_intervals.cpp b/src/test/nla_intervals.cpp index 5cea168ee..1207c746c 100644 --- a/src/test/nla_intervals.cpp +++ b/src/test/nla_intervals.cpp @@ -207,13 +207,82 @@ void test_nla_intervals_fractional() { VERIFY(true); // Placeholder } +void test_fetch_normalized_term_column() { + std::cout << "test_fetch_normalized_term_column\n"; + + lp::lar_solver s; + + // Create some variables + lpvar x = s.add_var(0, true); // j0 + lpvar y = s.add_var(1, true); // j1 + lpvar z = s.add_var(2, true); // j2 + + // Add a term t = 2*x + 3*y and register it + lp::lar_term t; + t.add_monomial(rational(2), x); + t.add_monomial(rational(3), y); + s.add_term(t.coeffs_as_vector(), UINT_MAX); + s.register_existing_terms(); + + // Now build the same term independently and look it up + lp::lar_term query; + query.add_monomial(rational(2), x); + query.add_monomial(rational(3), y); + lp::mpq a; + lp::lar_term norm_query = query.get_normalized_by_min_var(a); + + std::pair result; + bool found = s.fetch_normalized_term_column(norm_query, result); + VERIFY(found); + std::cout << " round-trip lookup: " << (found ? "PASS" : "FAIL") << "\n"; + + // Build query with variables added in reverse order + lp::lar_term query_rev; + query_rev.add_monomial(rational(3), y); + query_rev.add_monomial(rational(2), x); + lp::lar_term norm_rev = query_rev.get_normalized_by_min_var(a); + + bool found_rev = s.fetch_normalized_term_column(norm_rev, result); + VERIFY(found_rev); + std::cout << " reverse-order lookup: " << (found_rev ? "PASS" : "FAIL") << "\n"; + + // Test a 3-variable term: x - y + 5*z + lp::lar_term t2; + t2.add_monomial(rational(1), x); + t2.add_monomial(rational(-1), y); + t2.add_monomial(rational(5), z); + s.add_term(t2.coeffs_as_vector(), UINT_MAX); + s.register_existing_terms(); + + lp::lar_term query2; + query2.add_monomial(rational(1), x); + query2.add_monomial(rational(-1), y); + query2.add_monomial(rational(5), z); + lp::lar_term norm2 = query2.get_normalized_by_min_var(a); + + found = s.fetch_normalized_term_column(norm2, result); + VERIFY(found); + std::cout << " 3-variable term lookup: " << (found ? "PASS" : "FAIL") << "\n"; + + // Test that a non-registered term is NOT found + lp::lar_term query3; + query3.add_monomial(rational(7), x); + query3.add_monomial(rational(11), y); + lp::lar_term norm3 = query3.get_normalized_by_min_var(a); + + bool found_missing = s.fetch_normalized_term_column(norm3, result); + VERIFY(!found_missing); + std::cout << " non-existent term not found: " << (!found_missing ? "PASS" : "FAIL") << "\n"; +} + void test_nla_intervals() { test_nla_intervals_basic(); - test_nla_intervals_negative(); + test_nla_intervals_negative(); test_nla_intervals_zero_crossing(); test_nla_intervals_power(); test_nla_intervals_mixed_signs(); test_nla_intervals_fractional(); + test_fetch_normalized_term_column(); } } // namespace nla