From 2cff9e277e8a7efb29fe34d73d62015db6cd055e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 3 Dec 2025 15:07:34 -1000 Subject: [PATCH] add stats to track levelwise calls Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 25 +++++++------------------ src/nlsat/nlsat_explain.cpp | 10 ++++++---- src/nlsat/nlsat_solver.cpp | 10 ++++++++++ src/nlsat/nlsat_solver.h | 2 +- 4 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 4c4121d8c..0e094fd4c 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -214,19 +214,8 @@ namespace nlsat { return out; } - bool is_irreducible(poly* p) { - polynomial_ref_vector factors(m_pm); - polynomial_ref pref(p, m_pm); - ::nlsat::factor(pref, m_cache, factors); - unsigned num_factors = factors.size(); - CTRACE(lws, num_factors != 1, ::nlsat::display(tout, m_solver, p) << std::endl; - tout << "{"; - tout << "num_factors:" << num_factors << "\n"; - ::nlsat::display(tout, m_solver, factors); - tout << "}\n"; - ); - - return factors.size() == 1; + bool is_square_free(poly* p) { + return m_pm.is_square_free(p); } /* @@ -533,7 +522,7 @@ namespace nlsat { // add a property to m_Q if an equivalent one is not already present. // Equivalence: same m_prop_tag and same level; polynomials checked for equality // (polynomials are already in primitive form, so constant multipliers are normalized away). - void add_to_Q_if_new(const property & pr, unsigned level) { + void add_to_Q_if_new(const property & pr, unsigned level) { SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly))); for (auto const & q : m_Q[level]) { if (q.m_prop_tag != pr.m_prop_tag) continue; @@ -542,7 +531,7 @@ namespace nlsat { TRACE(lws, display(tout << "matched q:", q) << std::endl;); return; } - SASSERT(!pr.m_poly || is_irreducible(pr.m_poly)); + SASSERT(!pr.m_poly || is_square_free(pr.m_poly)); m_Q[level].push(pr); } @@ -829,7 +818,7 @@ or } void apply_pre_sgn_inv(const property& p) { - SASSERT(is_irreducible(p.m_poly)); + SASSERT(is_square_free(p.m_poly)); scoped_anum_vector roots(m_am); SASSERT(max_var(p.m_poly) == m_level); m_am.isolate_roots(p.m_poly, undef_var_assignment(sample(), m_level), roots); @@ -893,7 +882,7 @@ or /*Assume that p is irreducible, irExpr(p, s) ̸= ∅, ξ.p is irreducible for all ξ ∈ dom(≼), ≼ matches s, and for all ξ ∈ irExpr(p, s) it holds either ξ ≼t l or u ≼t ξ.*/ bool precondition_on_sign_inv(const property &p) { - SASSERT(is_irreducible(p.m_poly)); + SASSERT(is_square_free(p.m_poly)); SASSERT(max_var(p.m_poly) == m_level); return true; @@ -908,7 +897,7 @@ or p(s)= 0, sample(s)(R), an_sub(i− 1)(R), connected(i)(R), sgn_inv(p)(R), an_del(p)(R) ⊢ ord_inv(p)(R) */ void apply_pre_ord_inv(const property& p) { - SASSERT(p.m_prop_tag == prop_enum::ord_inv && is_irreducible(p.m_poly)); + SASSERT(p.m_prop_tag == prop_enum::ord_inv && is_square_free(p.m_poly)); unsigned level = max_var(p.m_poly); auto sign_on_sample = sign(p.m_poly, sample(), m_am); mk_prop(sample_holds, level_t(level)); diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index fdf2c1d51..24a0c94ae 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1144,11 +1144,13 @@ namespace nlsat { var x = m_todo.extract_max_polys(ps); TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";); - if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x, m_cache)) { - std::cout << "s"; - return; + if (m_solver.apply_levelwise()) { + bool levelwise_ok = levelwise_single_cell(ps, max_x, m_cache); + m_solver.record_levelwise_result(levelwise_ok); + if (levelwise_ok) + return; + } - std::cout << "f"; polynomial_ref_vector samples(m_pm); if (x < max_x) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 794b2e265..fa8f76cba 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -239,6 +239,8 @@ namespace nlsat { unsigned m_decisions; unsigned m_stages; unsigned m_irrational_assignments; // number of irrational witnesses + unsigned m_levelwise_calls; + unsigned m_levelwise_successes; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } }; @@ -2750,6 +2752,8 @@ namespace nlsat { st.update("nlsat stages", m_stats.m_stages); st.update("nlsat simplifications", m_stats.m_simplifications); st.update("nlsat irrational assignments", m_stats.m_irrational_assignments); + st.update("levelwise calls", m_stats.m_levelwise_calls); + st.update("levelwise successes", m_stats.m_levelwise_successes); } void reset_statistics() { @@ -4613,6 +4617,12 @@ namespace nlsat { m_imp->m_stats.m_simplifications++; } + void solver::record_levelwise_result(bool success) { + m_imp->m_stats.m_levelwise_calls++; + if (success) + m_imp->m_stats.m_levelwise_successes++; + } + bool solver::has_root_atom(clause const& c) const { return m_imp->has_root_atom(c); } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 4e6957e2b..b1cc29179 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -194,6 +194,7 @@ namespace nlsat { assumption join(assumption a, assumption b); void inc_simplify(); + void record_levelwise_result(bool success); void add_bound(bound_constraint const& c); /** @@ -300,4 +301,3 @@ namespace nlsat { }; }; -