mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +00:00
Code Activity

try optimizing build_interval_and_relation

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-13 10:43:47 -10:00
parent 9104ee1b5b
commit 895f7d5fde
1 changed files with 26 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/nlsat/levelwise.cpp
View file

@ -154,13 +154,13 @@ namespace nlsat {
void fail() { throw nullified_poly_exception(); } void fail() { throw nullified_poly_exception(); }
static void reset_interval(root_function_interval& I) { static void reset_interval(root_function_interval& I) {
I.section = false; I.section = false;
I.l = nullptr; I.l = nullptr;
I.u = nullptr; I.u = nullptr;
I.l_index = 0; I.l_index = 0;
I.u_index = 0; I.u_index = 0;
} }
// PSC-based discriminant: returns the first non-zero, non-constant element from the PSC chain. // PSC-based discriminant: returns the first non-zero, non-constant element from the PSC chain.
polynomial_ref psc_discriminant(polynomial_ref const& p_in, unsigned x) { polynomial_ref psc_discriminant(polynomial_ref const& p_in, unsigned x) {
@ -614,12 +614,14 @@ namespace nlsat {
poly_has_roots.resize(level_ps.size(), false); poly_has_roots.resize(level_ps.size(), false);
anum const& v = sample().value(level); anum const& v = sample().value(level);
auto& rfs = m_rel.m_rfunc;
std::vector<root_function> lhalf;
std::vector<root_function> uhalf;
for (unsigned i = 0; i < level_ps.size(); ++i) { for (unsigned i = 0; i < level_ps.size(); ++i) {
poly* p = level_ps.get(i); poly* p = level_ps.get(i);
scoped_anum_vector roots(m_am); scoped_anum_vector roots(m_am);
// Cacheing roots was not helpful.
// When the sample value is rational use a closest-root isolation // When the sample value is rational use a closest-root isolation
// returning at most two roots // returning at most two roots
if (v.is_basic()) { if (v.is_basic()) {
@ -629,8 +631,12 @@ namespace nlsat {
m_am.isolate_roots_closest(polynomial_ref(p, m_pm), undef_var_assignment(sample(), level), s, roots, idx); m_am.isolate_roots_closest(polynomial_ref(p, m_pm), undef_var_assignment(sample(), level), s, roots, idx);
poly_has_roots[i] = !roots.empty(); poly_has_roots[i] = !roots.empty();
SASSERT(roots.size() == idx.size()); SASSERT(roots.size() == idx.size());
for (unsigned k = 0; k < roots.size(); ++k) for (unsigned k = 0; k < roots.size(); ++k) {
m_rel.m_rfunc.emplace_back(m_am, p, idx[k], roots[k]); if (m_am.compare(roots[k], v) <= 0)
lhalf.emplace_back(m_am, p, idx[k], roots[k]);
else
uhalf.emplace_back(m_am, p, idx[k], roots[k]);
}
continue; continue;
} }
@ -656,22 +662,24 @@ namespace nlsat {
} }
} }
if (lower != UINT_MAX) { if (lower != UINT_MAX) {
m_rel.m_rfunc.emplace_back(m_am, p, lower + 1, roots[lower]); lhalf.emplace_back(m_am, p, lower + 1, roots[lower]);
if (section) if (section)
continue; // only keep the section root for this polynomial continue; // only keep the section root for this polynomial
} }
if (upper != UINT_MAX) if (upper != UINT_MAX)
m_rel.m_rfunc.emplace_back(m_am, p, upper + 1, roots[upper]); uhalf.emplace_back(m_am, p, upper + 1, roots[upper]);
} }
if (m_rel.m_rfunc.empty()) if (lhalf.empty() && uhalf.empty())
return; return;
// Partition: roots <= v come first, then roots > v rfs.clear();
auto& rfs = m_rel.m_rfunc; rfs.reserve(lhalf.size() + uhalf.size());
auto mid = std::partition(rfs.begin(), rfs.end(), [&](root_function const& f) { for (auto& rf : lhalf)
return m_am.compare(f.val, v) <= 0; rfs.emplace_back(std::move(rf));
}); auto mid = rfs.end();
for (auto& rf : uhalf)
rfs.emplace_back(std::move(rf));
// Sort each partition separately. For ties (equal root values), prefer // Sort each partition separately. For ties (equal root values), prefer
// low-degree defining polynomials as interval boundaries: // low-degree defining polynomials as interval boundaries: