mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 05:46:08 +00:00
Code Activity

local optimization

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-19 14:57:38 -10:00
parent 3ebc378fa3
commit 39dbbd0174
1 changed files with 184 additions and 366 deletions
Download patch file Download diff file Expand all files Collapse all files

550
src/nlsat/levelwise.cpp
View file

@ -11,23 +11,23 @@
#include <algorithm> #include <algorithm>
#include <cstdint> #include <cstdint>
#include <set> #include <set>
#include <unordered_map>
#include <utility> #include <utility>
#include <vector> #include <vector>
static bool is_set(unsigned k) { return static_cast<int>(k) != -1; } static bool is_set(unsigned k) { return static_cast<int>(k) != -1; }
// Helper functions for std_vector to mimic svector's get/setx interface // Helper for sparse vector access with default value
template<typename T> template<typename T>
static inline T vec_get(const std_vector<T>& v, size_t idx, T default_val) { static T vec_get(std_vector<T> const& v, unsigned idx, T def) {
if (idx < v.size()) return idx < v.size() ? v[idx] : def;
return static_cast<T>(v[idx]);
return default_val;
} }
// Helper for sparse vector write with auto-resize
template<typename T> template<typename T>
static inline void vec_setx(std_vector<T>& v, size_t idx, T val, T default_val) { static void vec_setx(std_vector<T>& v, unsigned idx, T val, T def) {
if (idx >= v.size()) if (idx >= v.size())
v.resize(idx + 1, default_val); v.resize(idx + 1, def);
v[idx] = val; v[idx] = val;
} }
@ -89,6 +89,16 @@ namespace nlsat {
// Entries are upgraded SIGN -> ORD as needed and cleared when a polynomial is extracted. // Entries are upgraded SIGN -> ORD as needed and cleared when a polynomial is extracted.
std_vector<uint8_t> m_req; std_vector<uint8_t> m_req;
// Scratch set for tracking added polynomial pairs (reused to avoid allocations)
mutable std::set<std::pair<unsigned, unsigned>> m_added_pairs;
// Reusable maps keyed by polynomial ID (more efficient than vectors for sparse IDs)
mutable std::unordered_map<unsigned, uint8_t> m_side_mask;
mutable std::unordered_map<unsigned, unsigned> m_deg_in_order_graph;
mutable std::unordered_map<unsigned, bool> m_omit_lc;
mutable std::unordered_map<unsigned, bool> m_omit_disc;
mutable std::unordered_map<unsigned, unsigned> m_unique_neighbor;
assignment const& sample() const { return m_solver.sample(); } assignment const& sample() const { return m_solver.sample(); }
// Utility: call fn for each distinct irreducible factor of poly // Utility: call fn for each distinct irreducible factor of poly
@ -144,12 +154,12 @@ namespace nlsat {
return m_pm.degree(p, level); return m_pm.degree(p, level);
} }
// Estimate resultant weight for a given set of pairs // Estimate resultant weight for m_rel.m_pairs
unsigned estimate_resultant_weight(std::vector<std::pair<unsigned, unsigned>> const& pairs) const { unsigned estimate_resultant_weight() const {
auto const& rfs = m_rel.m_rfunc; auto const& rfs = m_rel.m_rfunc;
unsigned total = 0; unsigned total = 0;
std::set<std::pair<unsigned, unsigned>> seen; m_added_pairs.clear();
for (auto const& pr : pairs) { for (auto const& pr : m_rel.m_pairs) {
poly* a = rfs[pr.first].ire.p; poly* a = rfs[pr.first].ire.p;
poly* b = rfs[pr.second].ire.p; poly* b = rfs[pr.second].ire.p;
if (!a || !b) continue; if (!a || !b) continue;
@ -157,82 +167,15 @@ namespace nlsat {
unsigned id2 = m_pm.id(b); unsigned id2 = m_pm.id(b);
if (id1 == id2) continue; if (id1 == id2) continue;
auto key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); auto key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (!seen.insert(key).second) continue; if (!m_added_pairs.insert(key).second) continue;
// w(res(a,b)) ≈ w(a) + w(b) // w(res(a,b)) ≈ w(a) + w(b)
total += w(a, m_level) + w(b, m_level); total += w(a, m_level) + w(b, m_level);
} }
return total; return total;
} }
// Generate pairs for biggest_cell heuristic (sector case) // Choose the best sector heuristic based on estimated weight.
std::vector<std::pair<unsigned, unsigned>> get_pairs_biggest_cell_sector() const { // Also fills m_rel.m_pairs with the winning heuristic's pairs.
std::vector<std::pair<unsigned, unsigned>> pairs;
if (is_set(m_l_rf))
for (unsigned j = 0; j < m_l_rf; ++j)
pairs.emplace_back(j, m_l_rf);
if (is_set(m_u_rf))
for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j)
pairs.emplace_back(m_u_rf, j);
if (is_set(m_l_rf) && is_set(m_u_rf))
pairs.emplace_back(m_l_rf, m_u_rf);
return pairs;
}
// Generate pairs for chain heuristic (sector case)
std::vector<std::pair<unsigned, unsigned>> get_pairs_chain_sector() const {
std::vector<std::pair<unsigned, unsigned>> pairs;
if (is_set(m_l_rf))
for (unsigned j = 0; j < m_l_rf; ++j)
pairs.emplace_back(j, j + 1);
if (is_set(m_u_rf))
for (unsigned j = m_u_rf + 1; j < m_rel.m_rfunc.size(); ++j)
pairs.emplace_back(j - 1, j);
if (is_set(m_l_rf) && is_set(m_u_rf))
pairs.emplace_back(m_l_rf, m_u_rf);
return pairs;
}
// Generate pairs for lowest_degree heuristic (sector case)
std::vector<std::pair<unsigned, unsigned>> get_pairs_lowest_degree_sector() const {
std::vector<std::pair<unsigned, unsigned>> pairs;
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
if (n == 0) return pairs;
std::vector<unsigned> degs;
degs.reserve(n);
for (unsigned i = 0; i < n; ++i)
degs.push_back(m_pm.degree(rfs[i].ire.p, m_level));
if (is_set(m_l_rf)) {
unsigned min_idx = m_l_rf;
unsigned min_deg = degs[m_l_rf];
for (int j = static_cast<int>(m_l_rf) - 1; j >= 0; --j) {
unsigned jj = static_cast<unsigned>(j);
pairs.emplace_back(jj, min_idx);
if (degs[jj] < min_deg) {
min_deg = degs[jj];
min_idx = jj;
}
}
}
if (is_set(m_u_rf)) {
unsigned min_idx = m_u_rf;
unsigned min_deg = degs[m_u_rf];
for (unsigned j = m_u_rf + 1; j < n; ++j) {
pairs.emplace_back(min_idx, j);
if (degs[j] < min_deg) {
min_deg = degs[j];
min_idx = j;
}
}
}
if (is_set(m_l_rf) && is_set(m_u_rf))
pairs.emplace_back(m_l_rf, m_u_rf);
return pairs;
}
// Choose the best sector heuristic based on estimated weight
relation_mode choose_best_sector_heuristic() { relation_mode choose_best_sector_heuristic() {
// With fewer than 2 root functions, no pairs can be generated // With fewer than 2 root functions, no pairs can be generated
// so all heuristics are equivalent - use default // so all heuristics are equivalent - use default
@ -244,94 +187,48 @@ namespace nlsat {
return m_sector_relation_mode; return m_sector_relation_mode;
} }
auto pairs_bc = get_pairs_biggest_cell_sector(); // Estimate weights by filling m_rel.m_pairs temporarily.
auto pairs_ch = get_pairs_chain_sector(); // Fill lowest_degree last since it's the most common winner (tie-breaker).
auto pairs_ld = get_pairs_lowest_degree_sector(); m_rel.m_pairs.clear();
fill_relation_with_biggest_cell_heuristic();
unsigned w_bc = estimate_resultant_weight();
unsigned w_bc = estimate_resultant_weight(pairs_bc); m_rel.m_pairs.clear();
unsigned w_ch = estimate_resultant_weight(pairs_ch); fill_relation_with_chain_heuristic();
unsigned w_ld = estimate_resultant_weight(pairs_ld); unsigned w_ch = estimate_resultant_weight();
m_rel.m_pairs.clear();
fill_relation_with_min_degree_resultant_sum();
unsigned w_ld = estimate_resultant_weight();
TRACE(lws, TRACE(lws,
tout << "Level " << m_level << " SECTOR: rfunc.size=" << m_rel.m_rfunc.size() tout << "Level " << m_level << " SECTOR: rfunc.size=" << m_rel.m_rfunc.size()
<< ", m_l_rf=" << (is_set(m_l_rf) ? std::to_string(m_l_rf) : "UNSET") << ", m_l_rf=" << (is_set(m_l_rf) ? std::to_string(m_l_rf) : "UNSET")
<< ", m_u_rf=" << (is_set(m_u_rf) ? std::to_string(m_u_rf) : "UNSET") << ", m_u_rf=" << (is_set(m_u_rf) ? std::to_string(m_u_rf) : "UNSET")
<< ", pairs_bc=" << pairs_bc.size()
<< ", pairs_ch=" << pairs_ch.size()
<< ", pairs_ld=" << pairs_ld.size()
<< "\n weight estimates: biggest_cell=" << w_bc << "\n weight estimates: biggest_cell=" << w_bc
<< ", chain=" << w_ch << ", chain=" << w_ch
<< ", lowest_degree=" << w_ld << "\n"; << ", lowest_degree=" << w_ld << "\n";
); );
if (w_ld <= w_ch && w_ld <= w_bc) return lowest_degree; unsigned w_min = std::min({w_bc, w_ch, w_ld});
if (w_ch <= w_bc) return chain;
// If lowest_degree wins, pairs are already filled
if (w_ld == w_min)
return lowest_degree;
// Otherwise, refill with the winning heuristic
m_rel.m_pairs.clear();
if (w_ch == w_min) {
fill_relation_with_chain_heuristic();
return chain;
}
TRACE(lws, tout << "bc wins\n");
fill_relation_with_biggest_cell_heuristic();
return biggest_cell; return biggest_cell;
} }
// Generate pairs for section heuristics // Choose the best section heuristic based on estimated weight.
std::vector<std::pair<unsigned, unsigned>> get_pairs_biggest_cell_section() const { // Also fills m_rel.m_pairs with the winning heuristic's pairs.
std::vector<std::pair<unsigned, unsigned>> pairs;
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
if (n == 0 || !is_set(m_l_rf)) return pairs;
for (unsigned j = 0; j < m_l_rf; ++j)
pairs.emplace_back(j, m_l_rf);
for (unsigned j = m_l_rf + 1; j < n; ++j)
pairs.emplace_back(m_l_rf, j);
return pairs;
}
std::vector<std::pair<unsigned, unsigned>> get_pairs_chain_section() const {
std::vector<std::pair<unsigned, unsigned>> pairs;
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
if (n == 0 || !is_set(m_l_rf)) return pairs;
for (unsigned j = 0; j + 1 < n; ++j)
pairs.emplace_back(j, j + 1);
return pairs;
}
std::vector<std::pair<unsigned, unsigned>> get_pairs_lowest_degree_section() const {
std::vector<std::pair<unsigned, unsigned>> pairs;
auto const& rfs = m_rel.m_rfunc;
unsigned n = rfs.size();
if (n == 0 || !is_set(m_l_rf)) return pairs;
std::vector<unsigned> degs;
degs.reserve(n);
for (unsigned i = 0; i < n; ++i)
degs.push_back(m_pm.degree(rfs[i].ire.p, m_level));
// Lower partition: [0, m_l_rf)
if (m_l_rf > 0) {
unsigned min_idx = m_l_rf;
unsigned min_deg = degs[m_l_rf];
for (int j = static_cast<int>(m_l_rf) - 1; j >= 0; --j) {
unsigned jj = static_cast<unsigned>(j);
pairs.emplace_back(jj, min_idx);
if (degs[jj] < min_deg) {
min_deg = degs[jj];
min_idx = jj;
}
}
}
// Upper partition: (m_l_rf, n)
if (m_l_rf + 1 < n) {
unsigned min_idx = m_l_rf;
unsigned min_deg = degs[m_l_rf];
for (unsigned j = m_l_rf + 1; j < n; ++j) {
pairs.emplace_back(min_idx, j);
if (degs[j] < min_deg) {
min_deg = degs[j];
min_idx = j;
}
}
}
return pairs;
}
// Choose the best section heuristic based on estimated weight
relation_mode choose_best_section_heuristic() { relation_mode choose_best_section_heuristic() {
// With fewer than 2 root functions, no pairs can be generated // With fewer than 2 root functions, no pairs can be generated
// so all heuristics are equivalent - use default // so all heuristics are equivalent - use default
@ -343,27 +240,41 @@ namespace nlsat {
return m_section_relation_mode; return m_section_relation_mode;
} }
auto pairs_bc = get_pairs_biggest_cell_section(); // Estimate weights by filling m_rel.m_pairs temporarily.
auto pairs_ch = get_pairs_chain_section(); // Fill lowest_degree last since it's the most common winner (tie-breaker).
auto pairs_ld = get_pairs_lowest_degree_section(); m_rel.m_pairs.clear();
fill_relation_pairs_for_section_biggest_cell();
unsigned w_bc = estimate_resultant_weight();
unsigned w_bc = estimate_resultant_weight(pairs_bc); m_rel.m_pairs.clear();
unsigned w_ch = estimate_resultant_weight(pairs_ch); fill_relation_pairs_for_section_chain();
unsigned w_ld = estimate_resultant_weight(pairs_ld); unsigned w_ch = estimate_resultant_weight();
m_rel.m_pairs.clear();
fill_relation_pairs_for_section_lowest_degree();
unsigned w_ld = estimate_resultant_weight();
TRACE(lws, TRACE(lws,
tout << "Level " << m_level << " SECTION: rfunc.size=" << m_rel.m_rfunc.size() tout << "Level " << m_level << " SECTION: rfunc.size=" << m_rel.m_rfunc.size()
<< ", m_l_rf=" << (is_set(m_l_rf) ? std::to_string(m_l_rf) : "UNSET") << ", m_l_rf=" << (is_set(m_l_rf) ? std::to_string(m_l_rf) : "UNSET")
<< ", pairs_bc=" << pairs_bc.size()
<< ", pairs_ch=" << pairs_ch.size()
<< ", pairs_ld=" << pairs_ld.size()
<< "\n weight estimates: biggest_cell=" << w_bc << "\n weight estimates: biggest_cell=" << w_bc
<< ", chain=" << w_ch << ", chain=" << w_ch
<< ", lowest_degree=" << w_ld << "\n"; << ", lowest_degree=" << w_ld << "\n";
); );
if (w_ld <= w_ch && w_ld <= w_bc) return section_lowest_degree; unsigned w_min = std::min({w_bc, w_ch, w_ld});
if (w_ch <= w_bc) return section_chain;
// If lowest_degree wins, pairs are already filled
if (w_ld == w_min)
return section_lowest_degree;
// Otherwise, refill with the winning heuristic
m_rel.m_pairs.clear();
if (w_ch == w_min) {
fill_relation_pairs_for_section_chain();
return section_chain;
}
fill_relation_pairs_for_section_biggest_cell();
return section_biggest_cell; return section_biggest_cell;
} }
@ -579,27 +490,26 @@ namespace nlsat {
// Compute side_mask: track which side(s) each polynomial appears on // Compute side_mask: track which side(s) each polynomial appears on
// bit0 = lower (<= sample), bit1 = upper (> sample), 3 = both sides // bit0 = lower (<= sample), bit1 = upper (> sample), 3 = both sides
void compute_side_mask(std_vector<uint8_t>& side_mask) { void compute_side_mask() {
side_mask.clear(); m_side_mask.clear();
anum const& v = sample().value(m_level); anum const& v = sample().value(m_level);
for (auto const& rf : m_rel.m_rfunc) { for (auto const& rf : m_rel.m_rfunc) {
poly* p = rf.ire.p; poly* p = rf.ire.p;
if (!p) if (!p)
continue; continue;
unsigned id = m_pm.id(p); unsigned id = m_pm.id(p);
uint8_t mask = vec_get(side_mask, id, static_cast<uint8_t>(0)); uint8_t& mask = m_side_mask[id];
if (m_am.compare(rf.val, v) <= 0) if (m_am.compare(rf.val, v) <= 0)
mask |= 1; mask |= 1;
else else
mask |= 2; mask |= 2;
vec_setx(side_mask, id, mask, static_cast<uint8_t>(0));
} }
} }
// Compute deg: count distinct resultant-neighbors for each polynomial // Compute deg: count distinct resultant-neighbors for each polynomial
void compute_resultant_degree(std_vector<unsigned>& deg) { void compute_resultant_degree() {
deg.clear(); m_deg_in_order_graph.clear();
std::set<std::pair<unsigned, unsigned>> added_pairs; m_added_pairs.clear();
for (auto const& pr : m_rel.m_pairs) { for (auto const& pr : m_rel.m_pairs) {
poly* a = m_rel.m_rfunc[pr.first].ire.p; poly* a = m_rel.m_rfunc[pr.first].ire.p;
poly* b = m_rel.m_rfunc[pr.second].ire.p; poly* b = m_rel.m_rfunc[pr.second].ire.p;
@ -610,206 +520,109 @@ namespace nlsat {
if (id1 == id2) if (id1 == id2)
continue; continue;
std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (!added_pairs.insert(key).second) if (!m_added_pairs.insert(key).second)
continue; continue;
vec_setx(deg, id1, vec_get(deg, id1, 0u) + 1, 0u); m_deg_in_order_graph[id1]++;
vec_setx(deg, id2, vec_get(deg, id2, 0u) + 1, 0u); m_deg_in_order_graph[id2]++;
} }
} }
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// SECTOR heuristics // noLdcf heuristic helpers
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
// Sector heuristic 1 (biggest_cell): omit lc for polynomials on both sides // Helper for biggest_cell and lowest_degree heuristics:
void compute_omit_lc_sector_biggest_cell(std_vector<bool>& omit_lc) { // Omit lc for polynomials appearing on both sides of the sample.
omit_lc.clear(); // If require_leaf is true, additionally require deg == 1 (leaf in resultant graph).
void compute_omit_lc_both_sides(bool require_leaf) {
m_omit_lc.clear();
if (m_rel.m_rfunc.empty() || m_rel.m_pairs.empty()) if (m_rel.m_rfunc.empty() || m_rel.m_pairs.empty())
return; return;
std_vector<uint8_t> side_mask; compute_side_mask();
compute_side_mask(side_mask); if (require_leaf)
compute_resultant_degree();
for (unsigned i = 0; i < m_level_ps.size(); ++i) { for (unsigned i = 0; i < m_level_ps.size(); ++i) {
poly* p = m_level_ps.get(i); poly* p = m_level_ps.get(i);
if (!p) if (!p)
continue; continue;
unsigned id = m_pm.id(p); unsigned id = m_pm.id(p);
// Omit if polynomial appears on both sides of the sample auto sm_it = m_side_mask.find(id);
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) == 3) if (sm_it == m_side_mask.end() || sm_it->second != 3)
vec_setx(omit_lc, id, true, false); continue;
if (require_leaf) {
auto deg_it = m_deg_in_order_graph.find(id);
if (deg_it == m_deg_in_order_graph.end() || deg_it->second != 1)
continue;
}
m_omit_lc[id] = true;
} }
} }
// Sector heuristic 2 (chain): omit lc for extremes of chain that appear on other side. // Helper for chain heuristics:
// SMT-RAT logic (OneCellCAD.h lines 975-985): // Omit lc for extremes of chain that appear on the other side.
// - lower2.begin() = polynomial with smallest root below sample (extreme of lower chain) // - Extreme of lower chain (index 0): omit if it also appears on upper side
// - upper2.end()-1 = polynomial with largest root above sample (extreme of upper chain) // - Extreme of upper chain (index n-1): omit if it also appears on lower side
// - Omit ldcf only if the polynomial appears on BOTH sides of the sample void compute_omit_lc_chain_extremes(bool has_lower, bool has_upper) {
void compute_omit_lc_sector_chain(std_vector<bool>& omit_lc) { m_omit_lc.clear();
omit_lc.clear();
if (m_rel.m_rfunc.empty()) if (m_rel.m_rfunc.empty())
return; return;
std_vector<uint8_t> side_mask; compute_side_mask();
compute_side_mask(side_mask);
unsigned n = m_rel.m_rfunc.size(); unsigned n = m_rel.m_rfunc.size();
// Extreme of lower chain: index 0 (if lower partition exists) if (has_lower) {
if (is_set(m_l_rf)) {
poly* p = m_rel.m_rfunc[0].ire.p; poly* p = m_rel.m_rfunc[0].ire.p;
if (p) {
unsigned id = m_pm.id(p);
// Omit ldcf if this polynomial also appears on the upper side
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) & 2)
vec_setx(omit_lc, id, true, false);
}
}
// Extreme of upper chain: last index (if upper partition exists)
if (is_set(m_u_rf)) {
poly* p = m_rel.m_rfunc[n - 1].ire.p;
if (p) {
unsigned id = m_pm.id(p);
// Omit ldcf if this polynomial also appears on the lower side
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) & 1)
vec_setx(omit_lc, id, true, false);
}
}
}
// Sector heuristic 3 (lowest_degree): omit lc for leaves (deg==1) on both sides
void compute_omit_lc_sector_lowest_degree(std_vector<bool>& omit_lc) {
omit_lc.clear();
if (m_rel.m_rfunc.empty() || m_rel.m_pairs.empty())
return;
std_vector<uint8_t> side_mask;
compute_side_mask(side_mask);
std_vector<unsigned> deg;
compute_resultant_degree(deg);
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
poly* p = m_level_ps.get(i);
if (!p)
continue;
unsigned id = m_pm.id(p); unsigned id = m_pm.id(p);
// Omit if polynomial is a leaf (deg==1) and appears on both sides auto it = m_side_mask.find(id);
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) == 3 && if (it != m_side_mask.end() && (it->second & 2))
vec_get(deg, id, 0u) == 1) m_omit_lc[id] = true;
vec_setx(omit_lc, id, true, false); }
if (has_upper) {
poly* p = m_rel.m_rfunc[n - 1].ire.p;
unsigned id = m_pm.id(p);
auto it = m_side_mask.find(id);
if (it != m_side_mask.end() && (it->second & 1))
m_omit_lc[id] = true;
} }
} }
// Dispatch to appropriate sector heuristic // Dispatch to appropriate sector heuristic
void compute_omit_lc_sector(std_vector<bool>& omit_lc) { void compute_omit_lc_sector() {
switch (m_sector_relation_mode) { switch (m_sector_relation_mode) {
case biggest_cell: case biggest_cell:
compute_omit_lc_sector_biggest_cell(omit_lc); compute_omit_lc_both_sides(false);
break; break;
case chain: case chain:
compute_omit_lc_sector_chain(omit_lc); compute_omit_lc_chain_extremes(is_set(m_l_rf), is_set(m_u_rf));
break; break;
case lowest_degree: case lowest_degree:
compute_omit_lc_sector_lowest_degree(omit_lc); compute_omit_lc_both_sides(true);
break; break;
default: default:
omit_lc.clear(); m_omit_lc.clear();
break; break;
} }
} }
// ----------------------------------------------------------------------------
// SECTION heuristics
// ----------------------------------------------------------------------------
// Section heuristic 1 (section_biggest_cell): no omit_lc computation needed
// (ldcf decision is based on ORD_INV tag, handled in add_level_projections_section)
void compute_omit_lc_section_biggest_cell(std_vector<bool>& omit_lc) {
omit_lc.clear();
// No omit_lc for section heuristic 1 - handled differently
}
// Section heuristic 2 (section_chain): omit lc for extremes of chain that appear on other side.
// SMT-RAT logic (OneCellCAD.h lines 240-252):
// - lower.begin() = polynomial with smallest root below sample (extreme of lower chain)
// - upper.end()-1 = polynomial with largest root above sample (extreme of upper chain)
// - Omit ldcf only if the polynomial appears on BOTH sides of the sample
void compute_omit_lc_section_chain(std_vector<bool>& omit_lc) {
omit_lc.clear();
if (m_rel.m_rfunc.empty())
return;
std_vector<uint8_t> side_mask;
compute_side_mask(side_mask);
unsigned n = m_rel.m_rfunc.size();
// In section case, partition is at m_l_rf + 1 (section root is at m_l_rf)
unsigned partition_idx = m_l_rf + 1;
// Extreme of lower chain: index 0 (if lower partition exists, i.e., partition_idx > 0)
if (partition_idx > 0) {
poly* p = m_rel.m_rfunc[0].ire.p;
if (p) {
unsigned id = m_pm.id(p);
// Omit ldcf if this polynomial also appears on the upper side
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) & 2)
vec_setx(omit_lc, id, true, false);
}
}
// Extreme of upper chain: last index (if upper partition exists, i.e., partition_idx < n)
if (partition_idx < n) {
poly* p = m_rel.m_rfunc[n - 1].ire.p;
if (p) {
unsigned id = m_pm.id(p);
// Omit ldcf if this polynomial also appears on the lower side
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) & 1)
vec_setx(omit_lc, id, true, false);
}
}
}
// Section heuristic 3 (section_lowest_degree): omit lc for leaves (deg==1) on both sides
void compute_omit_lc_section_lowest_degree(std_vector<bool>& omit_lc) {
omit_lc.clear();
if (m_rel.m_rfunc.empty() || m_rel.m_pairs.empty())
return;
std_vector<uint8_t> side_mask;
compute_side_mask(side_mask);
std_vector<unsigned> deg;
compute_resultant_degree(deg);
for (unsigned i = 0; i < m_level_ps.size(); ++i) {
poly* p = m_level_ps.get(i);
if (!p)
continue;
unsigned id = m_pm.id(p);
// Omit if polynomial is a leaf (deg==1) and appears on both sides
if (vec_get(side_mask, id, static_cast<uint8_t>(0)) == 3 &&
vec_get(deg, id, 0u) == 1)
vec_setx(omit_lc, id, true, false);
}
}
// Dispatch to appropriate section heuristic // Dispatch to appropriate section heuristic
void compute_omit_lc_section(std_vector<bool>& omit_lc) { void compute_omit_lc_section() {
switch (m_section_relation_mode) { switch (m_section_relation_mode) {
case section_biggest_cell: case section_biggest_cell:
compute_omit_lc_section_biggest_cell(omit_lc); m_omit_lc.clear(); // no omit_lc - handled via ORD_INV tag
break; break;
case section_chain: case section_chain: {
compute_omit_lc_section_chain(omit_lc); unsigned partition_idx = m_l_rf + 1;
compute_omit_lc_chain_extremes(partition_idx > 0, partition_idx < m_rel.m_rfunc.size());
break; break;
}
case section_lowest_degree: case section_lowest_degree:
compute_omit_lc_section_lowest_degree(omit_lc); compute_omit_lc_both_sides(true);
break; break;
default: default:
omit_lc.clear(); m_omit_lc.clear();
break; break;
} }
} }
@ -818,9 +631,9 @@ namespace nlsat {
// resultant relation. Inspired by SMT-RAT's "noDisc" optimization in OneCellCAD.h: // resultant relation. Inspired by SMT-RAT's "noDisc" optimization in OneCellCAD.h:
// if a polynomial is only connected to the section-defining polynomial via resultants, // if a polynomial is only connected to the section-defining polynomial via resultants,
// we do not need its discriminant for transitive root-order reasoning. // we do not need its discriminant for transitive root-order reasoning.
void compute_omit_disc_from_section_relation(std_vector<bool>& omit_disc) { void compute_omit_disc_from_section_relation() {
auto const& I = m_I[m_level]; auto const& I = m_I[m_level];
omit_disc.clear(); m_omit_disc.clear();
if (!I.section) if (!I.section)
return; return;
poly* section_p = I.l.get(); poly* section_p = I.l.get();
@ -834,10 +647,10 @@ namespace nlsat {
// Track the unique (if any) resultant-neighbor for each polynomial and its degree in the // Track the unique (if any) resultant-neighbor for each polynomial and its degree in the
// de-duplicated resultant graph. If deg(p) == 1 and neighbor(p) == section_id, then p is // de-duplicated resultant graph. If deg(p) == 1 and neighbor(p) == section_id, then p is
// a leaf connected only to the section polynomial. // a leaf connected only to the section polynomial.
std_vector<unsigned> unique_neighbor; m_unique_neighbor.clear();
std_vector<unsigned> deg; m_deg_in_order_graph.clear();
std::set<std::pair<unsigned, unsigned>> added_pairs; m_added_pairs.clear();
for (auto const& pr : m_rel.m_pairs) { for (auto const& pr : m_rel.m_pairs) {
poly* a = m_rel.m_rfunc[pr.first].ire.p; poly* a = m_rel.m_rfunc[pr.first].ire.p;
poly* b = m_rel.m_rfunc[pr.second].ire.p; poly* b = m_rel.m_rfunc[pr.second].ire.p;
@ -848,16 +661,16 @@ namespace nlsat {
if (id1 == id2) if (id1 == id2)
continue; continue;
std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (!added_pairs.insert(key).second) if (!m_added_pairs.insert(key).second)
continue; continue;
auto add_neighbor = [&](unsigned id, unsigned other) { auto add_neighbor = [&](unsigned id, unsigned other) {
vec_setx(deg, id, vec_get(deg, id, 0u) + 1, 0u); m_deg_in_order_graph[id]++;
unsigned cur = vec_get(unique_neighbor, id, UINT_MAX); auto it = m_unique_neighbor.find(id);
if (cur == UINT_MAX) if (it == m_unique_neighbor.end())
vec_setx(unique_neighbor, id, other, UINT_MAX); m_unique_neighbor[id] = other;
else if (cur != other) else if (it->second != other)
vec_setx(unique_neighbor, id, UINT_MAX - 1, UINT_MAX); // multiple neighbors it->second = UINT_MAX - 1; // multiple neighbors
}; };
add_neighbor(id1, id2); add_neighbor(id1, id2);
add_neighbor(id2, id1); add_neighbor(id2, id1);
@ -870,15 +683,17 @@ namespace nlsat {
unsigned id = m_pm.id(p); unsigned id = m_pm.id(p);
if (id == section_id) if (id == section_id)
continue; continue;
if (vec_get(deg, id, 0u) != 1) auto deg_it = m_deg_in_order_graph.find(id);
if (deg_it == m_deg_in_order_graph.end() || deg_it->second != 1)
continue; continue;
if (vec_get(unique_neighbor, id, UINT_MAX) != section_id) auto un_it = m_unique_neighbor.find(id);
if (un_it == m_unique_neighbor.end() || un_it->second != section_id)
continue; continue;
// If p vanishes at the sample on the section, we may need p's delineability to // If p vanishes at the sample on the section, we may need p's delineability to
// reason about coinciding root functions; be conservative and keep disc(p). // reason about coinciding root functions; be conservative and keep disc(p).
if (m_am.eval_sign_at(polynomial_ref(p, m_pm), sample()) == 0) if (m_am.eval_sign_at(polynomial_ref(p, m_pm), sample()) == 0)
continue; continue;
vec_setx(omit_disc, id, true, false); m_omit_disc[id] = true;
} }
} }
@ -1229,7 +1044,7 @@ namespace nlsat {
void add_relation_resultants() { void add_relation_resultants() {
std::set<std::pair<unsigned, unsigned>> added_pairs; m_added_pairs.clear();
for (auto const& pr : m_rel.m_pairs) { for (auto const& pr : m_rel.m_pairs) {
poly* a = m_rel.m_rfunc[pr.first].ire.p; poly* a = m_rel.m_rfunc[pr.first].ire.p;
poly* b = m_rel.m_rfunc[pr.second].ire.p; poly* b = m_rel.m_rfunc[pr.second].ire.p;
@ -1240,7 +1055,7 @@ namespace nlsat {
if (id1 == id2) if (id1 == id2)
continue; continue;
std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (!added_pairs.insert(key).second) if (!m_added_pairs.insert(key).second)
continue; continue;
request_factorized(m_todo, psc_resultant(a, b, m_level), inv_req::ord); request_factorized(m_todo, psc_resultant(a, b, m_level), inv_req::ord);
} }
@ -1270,7 +1085,7 @@ namespace nlsat {
std::sort(root_vals.begin(), root_vals.end(), [&](auto const& a, auto const& b) { std::sort(root_vals.begin(), root_vals.end(), [&](auto const& a, auto const& b) {
return m_am.lt(a.first, b.first); return m_am.lt(a.first, b.first);
}); });
std::set<std::pair<unsigned, unsigned>> added_pairs; m_added_pairs.clear();
for (unsigned j = 0; j + 1 < root_vals.size(); ++j) { for (unsigned j = 0; j + 1 < root_vals.size(); ++j) {
poly* p1 = root_vals[j].second; poly* p1 = root_vals[j].second;
poly* p2 = root_vals[j + 1].second; poly* p2 = root_vals[j + 1].second;
@ -1281,7 +1096,7 @@ namespace nlsat {
if (id1 == id2) if (id1 == id2)
continue; continue;
std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1); std::pair<unsigned, unsigned> key = id1 < id2 ? std::make_pair(id1, id2) : std::make_pair(id2, id1);
if (!added_pairs.insert(key).second) if (!m_added_pairs.insert(key).second)
continue; continue;
request_factorized(m_todo, psc_resultant(p1, p2, m_n), inv_req::ord); request_factorized(m_todo, psc_resultant(p1, p2, m_n), inv_req::ord);
} }
@ -1302,15 +1117,16 @@ namespace nlsat {
// Note: Algorithm 1 adds disc + ldcf for ALL polynomials (classical delineability) // Note: Algorithm 1 adds disc + ldcf for ALL polynomials (classical delineability)
// We additionally omit leading coefficients for rootless polynomials when possible // We additionally omit leading coefficients for rootless polynomials when possible
// (cf. projective delineability, Lemma 3.2). // (cf. projective delineability, Lemma 3.2).
std_vector<bool> omit_lc; compute_omit_lc_sector();
compute_omit_lc_sector(omit_lc);
for (unsigned i = 0; i < m_level_ps.size(); ++i) { for (unsigned i = 0; i < m_level_ps.size(); ++i) {
polynomial_ref p(m_level_ps.get(i), m_pm); polynomial_ref p(m_level_ps.get(i), m_pm);
polynomial_ref lc(m_pm); polynomial_ref lc(m_pm);
unsigned deg = m_pm.degree(p, m_level); unsigned deg = m_pm.degree(p, m_level);
lc = m_pm.coeff(p, m_level, deg); lc = m_pm.coeff(p, m_level, deg);
bool add_lc = !vec_get(omit_lc, m_pm.id(p.get()), false); // Let todo_set handle duplicates if witness == lc unsigned pid = m_pm.id(p.get());
auto it = m_omit_lc.find(pid);
bool add_lc = (it == m_omit_lc.end() || !it->second);
if (add_lc && i < usize(m_poly_has_roots) && !m_poly_has_roots[i]) if (add_lc && i < usize(m_poly_has_roots) && !m_poly_has_roots[i])
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0) if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
@ -1319,7 +1135,7 @@ namespace nlsat {
// SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample // SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample
// AND we're adding lc, we do not need to project an additional non-null coefficient witness. // AND we're adding lc, we do not need to project an additional non-null coefficient witness.
polynomial_ref witness = m_witnesses[i]; polynomial_ref witness = m_witnesses[i];
if (add_lc && witness && !is_const(witness)) if (add_lc && witness && !is_const(witness))
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0) if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
witness = polynomial_ref(m_pm); witness = polynomial_ref(m_pm);
add_projections_for(m_todo, p, m_level, witness, add_lc, true); //true for adding the discriminant: always add it in sector, required by Lemma 3.2. add_projections_for(m_todo, p, m_level, witness, add_lc, true); //true for adding the discriminant: always add it in sector, required by Lemma 3.2.
@ -1331,12 +1147,12 @@ namespace nlsat {
poly* section_p = m_I[m_level].l.get(); poly* section_p = m_I[m_level].l.get();
// Compute omission information derived from the chosen relation (still used for heuristics 2/3). // Compute omission information derived from the chosen relation (still used for heuristics 2/3).
std_vector<bool> omit_lc; compute_omit_lc_section();
compute_omit_lc_section(omit_lc);
std_vector<bool> omit_disc;
// SMT-RAT only applies noDisc optimization for section_lowest_degree (heuristic 3) // SMT-RAT only applies noDisc optimization for section_lowest_degree (heuristic 3)
if (m_section_relation_mode == section_lowest_degree) if (m_section_relation_mode == section_lowest_degree)
compute_omit_disc_from_section_relation(omit_disc); compute_omit_disc_from_section_relation();
else
m_omit_disc.clear();
for (unsigned i = 0; i < m_level_ps.size(); ++i) { for (unsigned i = 0; i < m_level_ps.size(); ++i) {
polynomial_ref p(m_level_ps.get(i), m_pm); polynomial_ref p(m_level_ps.get(i), m_pm);
@ -1359,7 +1175,8 @@ namespace nlsat {
add_lc = false; add_lc = false;
} }
else { else {
if (add_lc && vec_get(omit_lc, pid, false)) auto it = m_omit_lc.find(pid);
if (add_lc && it != m_omit_lc.end() && it->second)
add_lc = false; add_lc = false;
if (add_lc && !has_roots) if (add_lc && !has_roots)
@ -1368,9 +1185,8 @@ namespace nlsat {
} }
bool add_disc = true; bool add_disc = true;
if (is_section_poly) { if (is_section_poly)
add_disc = true; add_disc = true;
}
else if (m_section_relation_mode == section_biggest_cell) { else if (m_section_relation_mode == section_biggest_cell) {
// SMT-RAT section heuristic 1 projects discriminants primarily for the defining // SMT-RAT section heuristic 1 projects discriminants primarily for the defining
// polynomial; keep discriminants only for upstream ORD polynomials. // polynomial; keep discriminants only for upstream ORD polynomials.
@ -1387,13 +1203,16 @@ namespace nlsat {
// Only omit discriminants for polynomials that were not required to be order-invariant // Only omit discriminants for polynomials that were not required to be order-invariant
// by upstream projection steps. // by upstream projection steps.
if (add_disc && m_level_tags[i].second != inv_req::ord && vec_get(omit_disc, pid, false)) if (add_disc && m_level_tags[i].second != inv_req::ord) {
add_disc = false; auto it = m_omit_disc.find(pid);
if (it != m_omit_disc.end() && it->second)
add_disc = false;
}
// SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample // SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample
// AND we're adding lc, we do not need to project an additional non-null coefficient witness. // AND we're adding lc, we do not need to project an additional non-null coefficient witness.
polynomial_ref witness = m_witnesses[i]; polynomial_ref witness = m_witnesses[i];
if (add_lc && witness && !is_const(witness)) if (add_lc && witness && !is_const(witness))
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0) if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
witness = polynomial_ref(m_pm); witness = polynomial_ref(m_pm);
@ -1405,8 +1224,9 @@ namespace nlsat {
SASSERT(m_I[m_level].section); SASSERT(m_I[m_level].section);
if (have_interval) { if (have_interval) {
if (m_dynamic_heuristic) if (m_dynamic_heuristic)
m_section_relation_mode = choose_best_section_heuristic(); m_section_relation_mode = choose_best_section_heuristic(); // also fills pairs
fill_relation_pairs_for_section(); else
fill_relation_pairs_for_section();
} }
upgrade_bounds_to_ord(); upgrade_bounds_to_ord();
add_level_projections_section(); add_level_projections_section();
@ -1417,8 +1237,9 @@ namespace nlsat {
SASSERT(!m_I[m_level].section); SASSERT(!m_I[m_level].section);
if (have_interval) { if (have_interval) {
if (m_dynamic_heuristic) if (m_dynamic_heuristic)
m_sector_relation_mode = choose_best_sector_heuristic(); m_sector_relation_mode = choose_best_sector_heuristic(); // also fills pairs
fill_relation_pairs_for_sector(); else
fill_relation_pairs_for_sector();
} }
upgrade_bounds_to_ord(); upgrade_bounds_to_ord();
add_level_projections_sector(); add_level_projections_sector();
@ -1443,12 +1264,10 @@ namespace nlsat {
// Lines 3-8: Θ + I_level + relation ≼ // Lines 3-8: Θ + I_level + relation ≼
bool have_interval = build_interval(); bool have_interval = build_interval();
if (m_I[m_level].section) { if (m_I[m_level].section)
process_level_section(have_interval); process_level_section(have_interval);
} else
else {
process_level_sector(have_interval); process_level_sector(have_interval);
}
} }
void process_top_level() { void process_top_level() {
@ -1486,10 +1305,9 @@ namespace nlsat {
// SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample // SMT-RAT-style coeffNonNull: if the leading coefficient is already non-zero at the sample
// AND we're adding lc, we do not need to project an additional non-null coefficient witness. // AND we're adding lc, we do not need to project an additional non-null coefficient witness.
polynomial_ref witness = m_witnesses[i]; polynomial_ref witness = m_witnesses[i];
if (add_lc && witness && !is_const(witness) && add_lc) { if (add_lc && witness && !is_const(witness) && add_lc)
if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0) if (lc && !is_zero(lc) && m_am.eval_sign_at(lc, sample()) != 0)
witness = polynomial_ref(m_pm); witness = polynomial_ref(m_pm);
}
add_projections_for(m_todo, p, m_n, witness, add_lc, true); add_projections_for(m_todo, p, m_n, witness, add_lc, true);
} }
} }