mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 16:40:52 +00:00
Code Activity

Fix broken term_comparer in m_normalized_terms_to_columns lookup

Browse source 
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) <noreply@anthropic.com>
This commit is contained in:
Arie Gurfinkel 2026-04-07 11:54:43 -04:00
parent 1544462f47
commit fe100e7865
2 changed files with 76 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/lar_solver.cpp
View file

@ -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;
}
};

71
src/test/nla_intervals.cpp
View file

@ -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<lp::mpq, lpvar> 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