From 7ffebbd60ce3258b1c1bb08063ba95ce2127bc63 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 14 Aug 2025 10:56:24 -0700 Subject: [PATCH] more accurate init of the relation between polynomial properties Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 144 ++++++++++++++++++++++++++++++++-------- 1 file changed, 115 insertions(+), 29 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index b82a81662..855fb9a35 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -3,6 +3,7 @@ #include #include #include +#include namespace nlsat { // Local enums reused from previous scaffolding @@ -12,6 +13,8 @@ namespace nlsat { ir_ord, an_del, non_null, + ord_inv_reducible, + ord_inv_irreducible, sgn_inv_reducible, sgn_inv_irreducible, connected, @@ -22,9 +25,8 @@ namespace nlsat { _count }; - static unsigned score(prop_enum pe) { - return static_cast(prop_enum::_count) - static_cast(pe); - } + unsigned prop_count() { return static_cast(prop_enum::_count);} + // no score-based ordering; precedence is defined by m_p_relation only struct property { prop_enum prop; @@ -39,9 +41,73 @@ namespace nlsat { std::vector m_Q; // the set of properties to prove as in single_cell bool m_fail = false; unsigned m_i; // current level + // Property precedence relation stored as pairs (lesser, greater) + std::vector> m_p_relation; + // Transitive closure matrix: dom[a][b] == true iff a ▹ b (a strictly dominates b). + // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser. + std::vector> m_prop_dom; // max_x plays the role of n in algorith 1 of the levelwise paper. impl(polynomial_ref_vector const& ps, var max_x, assignment const& s) : m_P(ps), m_n(max_x), m_s(s) { + init_relation(); + } + + #ifdef Z3DEBUG + + bool check_prop_init() { + std::cout << "checked\n"; + for (unsigned k = 0; k < prop_count(); ++k) + if (m_prop_dom[k][k]) + return false; + return !dominates(prop_enum::ord_inv_irreducible, prop_enum::non_null); + } + #endif + + void init_relation() { + m_p_relation.clear(); + auto add = [&](prop_enum lesser, prop_enum greater) { m_p_relation.emplace_back(lesser, greater); }; + // m_p_relation stores edges (lesser -> greater). We later invert these to build dom (greater ▹ lesser). + // The edges below follow Figure 8. Examples include: an_del -> ir_ord, sample -> ir_ord. + add(prop_enum::holds, prop_enum::repr); + add(prop_enum::repr, prop_enum::sample); + add(prop_enum::sample, prop_enum::an_sub); + add(prop_enum::an_sub, prop_enum::connected); + // connected < sgn_inv_* + add(prop_enum::connected, prop_enum::sgn_inv_reducible); + add(prop_enum::connected, prop_enum::sgn_inv_irreducible); + // sgn_inv_* < ord_inv_* (same reducibility) + add(prop_enum::sgn_inv_reducible, prop_enum::ord_inv_reducible); + add(prop_enum::sgn_inv_irreducible, prop_enum::ord_inv_irreducible); + // ord_inv_* < non_null + + add(prop_enum::ord_inv_reducible, prop_enum::non_null); + add(prop_enum::ord_inv_irreducible, prop_enum::non_null); + // non_null < an_del + add(prop_enum::non_null, prop_enum::an_del); + // an_del < ir_ord + add(prop_enum::an_del, prop_enum::ir_ord); + // Additional explicit edge from Fig 8 + add(prop_enum::sample, prop_enum::ir_ord); + + // Build transitive closure matrix for quick comparisons + unsigned N = prop_count(); + m_prop_dom.assign(N, std::vector(N, false)); + for (auto const& pr : m_p_relation) { + unsigned lesser = static_cast(pr.first); + unsigned greater = static_cast(pr.second); + // Build dominance relation as: greater ▹ lesser + m_prop_dom[greater][lesser] = true; + } + // Floyd-Warshall style closure on a tiny fixed-size set + for (unsigned k = 0; k < N; ++k) + for (unsigned i = 0; i < N; ++i) + if (m_prop_dom[i][k]) + for (unsigned j = 0; j < N; ++j) + if (m_prop_dom[k][j]) + m_prop_dom[i][j] = true; + + + SASSERT(check_prop_init()); } std::vector seed_properties() { std::vector Q; @@ -58,42 +124,62 @@ namespace nlsat { bool status; }; + bool dominates(prop_enum a, prop_enum b) { + return m_prop_dom[static_cast(a)][static_cast(b)]; + } std::vector greatest_to_refine() { - // Deterministic order: use ascending polynomial id as key - std::map best_by_poly; - for (const auto& q : m_Q) { - if (q.level != m_i) - continue; - if (q.prop == prop_enum::sgn_inv_irreducible) - continue; - unsigned pid = polynomial::manager::id(q.p); - auto it = best_by_poly.find(pid); - if (it == best_by_poly.end() || score(q.prop) > score(it->second.prop)) - best_by_poly[pid] = q; + // Collect candidates on current level, excluding sgn_inv_irreducible + std::vector cand; + cand.reserve(m_Q.size()); + for (const auto& q : m_Q) + if (q.level == m_i && q.prop != prop_enum::sgn_inv_irreducible) + cand.push_back(q); + if (cand.empty()) return {}; + + // Determine maxima w.r.t. ▹ using the transitive closure matrix + + std::vector dominated(cand.size(), false); + for (size_t i = 0; i < cand.size(); ++i) { + for (size_t j = 0; j < cand.size(); ++j) { + if (i != j && dominates(cand[j].prop, cand[i].prop)) { + dominated[i] = true; + break; + } + } } + + // Extract non-dominated (greatest) candidates; keep deterministic order by (poly id, prop enum) + struct Key { unsigned pid; unsigned pprop; size_t idx; }; + std::vector keys; + keys.reserve(cand.size()); + for (size_t i = 0; i < cand.size(); ++i) { + if (!dominated[i]) { + keys.push_back(Key{ polynomial::manager::id(cand[i].p), static_cast(cand[i].prop), i }); + } + } + std::sort(keys.begin(), keys.end(), [](Key const& a, Key const& b){ + if (a.pid != b.pid) return a.pid < b.pid; + return a.pprop < b.pprop; + }); std::vector ret; - ret.reserve(best_by_poly.size()); - for (auto const& kv : best_by_poly) - ret.push_back(kv.second); + ret.reserve(keys.size()); + for (auto const& k : keys) ret.push_back(cand[k.idx]); return ret; } result_struct construct_interval() { result_struct ret; /*foreach q ∈ Q |i where q is the greatest element with respect to ▹ (from Definition 4.5) and q ̸= sgn_inv(p) for an irreducible p -do -2 Q := apply_pre(i, Q ,q,(s)) // Algorithm 3 -3 if Q= FAIL then -4 return FAIL - */ - std::vector to_refine = greatest_to_refine(); - for (const auto & q : this->m_Q) { - if (false) - ; - } - return ret; + do + 2 Q := apply_pre(i, Q ,q,(s)) // Algorithm 3 + 3 if Q= FAIL then + 4 return FAIL +*/ + std::vector to_refine = greatest_to_refine(); + // refine using to_refine (TBD) + return ret; } // return an empty vector on failure std::vector single_cell() { @@ -108,7 +194,7 @@ do } return ret; // the order is reversed! - } + } }; // constructor levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s)