From 665d4f36ffe02d691c04daff75aab7c2eb1b701f Mon Sep 17 00:00:00 2001 From: Arie <123119895+1arie1@users.noreply.github.com> Date: Sun, 12 Apr 2026 17:31:18 -0400 Subject: [PATCH] Fixes for lar_term== operator (#9284) * 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) * Disable operator== for lar_term The operator== for lar_term was never intended to be used. This changes physically disables it to identify what happens to depend on the operator. * Work around missing lar_term== Previous commit disabled lar_term==. This is the only use of the operator that seems meaningful. Changed it to compare by references instead. Compiles, but not sure this is the best solution. * replace with e Signed-off-by: Nikolaj Bjorner * Delete unused ineq::operator== The operator is unused, so there is no need to figure what is the best fix for it. * Remove lp tests that use ineq::operator== --------- Signed-off-by: Nikolaj Bjorner Co-authored-by: Claude Opus 4.6 (1M context) Co-authored-by: Nikolaj Bjorner --- src/math/lp/dioph_eq.cpp | 13 ++---- src/math/lp/lar_solver.cpp | 7 +++- src/math/lp/lar_term.h | 4 +- src/math/lp/nla_types.h | 5 +-- src/test/lp/lp.cpp | 8 ++-- src/test/lp/nla_solver_test.cpp | 7 +++- src/test/nla_intervals.cpp | 71 ++++++++++++++++++++++++++++++++- 7 files changed, 94 insertions(+), 21 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 714eabc3a..5058bfaf3 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -238,18 +238,13 @@ namespace lp { r.c() -= b.c(); return r; } -#if Z3DEBUG - friend bool operator==(const term_o& a, const term_o& b) { + + friend bool eq(const term_o& a, const term_o& b) { term_o t = a.clone(); t += mpq(-1) * b; return t.c() == mpq(0) && t.size() == 0; } - friend bool operator!=(const term_o& a, const term_o& b) { - return ! (a == b); - } - -#endif term_o& operator+=(const term_o& t) { for (const auto& p : t) { add_monomial(p.coeff(), p.j()); @@ -1541,7 +1536,7 @@ namespace lp { term_o t1 = open_ml(t0); t1.add_monomial(mpq(1), j); term_o rs = fix_vars(t1); - if (ls != rs) { + if (!eq(ls, rs)) { TRACE(dio, tout << "ls:"; print_term_o(ls, tout) << "\n"; tout << "rs:"; print_term_o(rs, tout) << "\n";); return false; @@ -2351,7 +2346,7 @@ namespace lp { return false; } - bool ret = ls == fix_vars(open_ml(m_l_matrix.m_rows[ei])); + bool ret = eq(ls, fix_vars(open_ml(m_l_matrix.m_rows[ei]))); if (!ret) { CTRACE(dio, !ret, { 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/math/lp/lar_term.h b/src/math/lp/lar_term.h index cca541801..b2d777493 100644 --- a/src/math/lp/lar_term.h +++ b/src/math/lp/lar_term.h @@ -129,8 +129,8 @@ public: add_monomial(a, v1); add_monomial(b, v2); } - bool operator==(const lar_term & a) const { return false; } // take care not to create identical terms - bool operator!=(const lar_term & a) const { return ! (*this == a);} + bool operator==(const lar_term & a) const = delete; // take care not to create identical terms + bool operator!=(const lar_term & a) const = delete; // some terms get used in add constraint // it is the same as the offset in the m_constraints diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index 401e4eb62..89823e4dc 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -41,9 +41,8 @@ namespace nla { ineq(const lp::lar_term& term, lp::lconstraint_kind cmp, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {} ineq(lpvar v, lp::lconstraint_kind cmp, int i): m_cmp(cmp), m_term(v), m_rs(rational(i)) {} ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {} - bool operator==(const ineq& a) const { - return m_cmp == a.m_cmp && m_term == a.m_term && m_rs == a.m_rs; - } + bool operator==(const ineq& a) const = delete; + bool operator!=(const ineq& a) const = delete; const lp::lar_term& term() const { return m_term; }; lp::lconstraint_kind cmp() const { return m_cmp; }; const rational& rs() const { return m_rs; }; diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ee1989c20..7a2b27155 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1971,28 +1971,28 @@ void test_lp_local(int argn, char **argv) { if (args_parser.option_is_used("-nla_blfmz_mf")) { #ifdef Z3DEBUG - nla::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); + // nla::test_basic_lemma_for_mon_zero_from_monomial_to_factors(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blfmz_fm")) { #ifdef Z3DEBUG - nla::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); + //nla::test_basic_lemma_for_mon_zero_from_factors_to_monomial(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blnt_mf")) { #ifdef Z3DEBUG - nla::test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); + // nla::test_basic_lemma_for_mon_neutral_from_monomial_to_factors(); #endif return finalize(0); } if (args_parser.option_is_used("-nla_blnt_fm")) { #ifdef Z3DEBUG - nla::test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); + // nla::test_basic_lemma_for_mon_neutral_from_factors_to_monomial(); #endif return finalize(0); } diff --git a/src/test/lp/nla_solver_test.cpp b/src/test/lp/nla_solver_test.cpp index 1ec8fe8fa..d2e2e2f19 100644 --- a/src/test/lp/nla_solver_test.cpp +++ b/src/test/lp/nla_solver_test.cpp @@ -150,7 +150,7 @@ void create_abcde(solver & nla, nla.add_monic(lp_be, vec.size(), vec.begin()); } - +#if 0 void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0\n"; enable_trace("nla_solver"); @@ -222,6 +222,7 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() { } +#endif void s_set_column_value_test(lp::lar_solver&s, lpvar j, const rational & v) { s.set_column_value_test(j, lp::impq(v)); @@ -231,6 +232,7 @@ void s_set_column_value_test(lp::lar_solver&s, lpvar j, const lp::impq & v) { s.set_column_value_test(j, v); } +#if 0 void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() { std::cout << "test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1\n"; TRACE(nla_solver,); @@ -367,6 +369,7 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() { VERIFY(found0 && found1); } + void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { std::cout << "test_basic_lemma_for_mon_zero_from_monomial_to_factors\n"; enable_trace("nla_solver"); @@ -420,6 +423,7 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() { } + void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { std::cout << "test_basic_lemma_for_mon_neutral_from_monomial_to_factors\n"; enable_trace("nla_solver"); @@ -489,6 +493,7 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() { VERIFY(found0 && found1); } +#endif void test_horner() { enable_trace("nla_solver"); 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