mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 09:24:36 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-10 15:04:50 -07:00
parent 5e54cb6693
commit 81dec49492
1 changed files with 3 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/levelwise.cpp
View file

@ -157,21 +157,10 @@ namespace nlsat {
}
/*
Short: build the initial property set Q so the one-cell algorithm can generalize the
conflict around the current sample. The main goal is to eliminate raw input polynomials
whose main variable is x_{m_n} (i.e. level == m_n) by replacing them with properties.
Strategy:
- For factors with level < m_n: add sgn_inv(p) to Q (sign-invariance).
- For factors with level == m_n: add an_del(p) and isolate their indexed roots over the sample;
sort those roots and for each adjacent pair coming from distinct polynomials add
ord_inv(resultant(p_j, p_{j+1})) to Q.
- If any constructed polynomial is nullified on the sample, that is all coefficients are zeroes, then fail.
Result: Q = { sgn_inv(p) | level(p) < m_n } ∪ { an_del(p) | level(p) == m_n } ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent roots }.
prepare the initial properties
*/
// Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
void collect_level_properties(std::vector<poly*> & ps_of_n_level) {
void collect_top_level_properties(std::vector<poly*> & ps_of_n_level) {
for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_P[i];
polynomial_ref pref(p, m_pm);
@ -261,7 +250,7 @@ namespace nlsat {
*/
void init_properties() {
std::vector<poly*> ps_of_n_level;
collect_level_properties(ps_of_n_level);
collect_top_level_properties(ps_of_n_level);
std::vector<std::pair<scoped_anum, poly*>> root_vals;
collect_roots_for_ps(ps_of_n_level, root_vals);
if (!add_adjacent_resultants(root_vals))