From b2268544d142bb6c2add14cc61687457db25b32f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 26 Jan 2026 06:12:03 -1000 Subject: [PATCH] remove sector/section stats Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 4 ---- src/nlsat/nlsat_solver.cpp | 18 ------------------ src/nlsat/nlsat_solver.h | 3 --- 3 files changed, 25 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 751e287c4..7367145fe 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1608,7 +1608,6 @@ namespace nlsat { void process_level_section(bool have_interval) { SASSERT(m_I[m_level].section); - m_solver.record_levelwise_section(); clear_level_state(); // Clear stale state from previous level if (have_interval) { // Check spanning tree threshold first, independent of dynamic heuristic @@ -1616,7 +1615,6 @@ namespace nlsat { fill_relation_pairs_for_section_spanning_tree(); compute_omit_lc_both_sides(true); m_section_relation_mode = section_spanning_tree; - m_solver.record_levelwise_spanning_tree(); } else if (m_dynamic_heuristic) { m_section_relation_mode = choose_best_section_heuristic(); // also fills pairs } else { @@ -1631,7 +1629,6 @@ namespace nlsat { void process_level_sector(bool have_interval) { SASSERT(!m_I[m_level].section); - m_solver.record_levelwise_sector(); clear_level_state(); // Clear stale state from previous level if (have_interval) { // Check spanning tree threshold first, independent of dynamic heuristic @@ -1639,7 +1636,6 @@ namespace nlsat { fill_relation_with_spanning_tree_heuristic(); compute_omit_lc_both_sides(true); m_sector_relation_mode = spanning_tree; - m_solver.record_levelwise_spanning_tree(); } else if (m_dynamic_heuristic) { m_sector_relation_mode = choose_best_sector_heuristic(); // also fills pairs } else { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index e6c0190dc..78306b63f 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -242,9 +242,6 @@ namespace nlsat { unsigned m_irrational_assignments; // number of irrational witnesses unsigned m_levelwise_calls; unsigned m_levelwise_failures; - unsigned m_levelwise_sectors; - unsigned m_levelwise_sections; - unsigned m_levelwise_spanning_tree; unsigned m_lws_initial_fail; void reset() { memset(this, 0, sizeof(*this)); } stats() { reset(); } @@ -2793,9 +2790,6 @@ namespace nlsat { st.update("nlsat irrational assignments", m_stats.m_irrational_assignments); st.update("levelwise calls", m_stats.m_levelwise_calls); st.update("levelwise failures", m_stats.m_levelwise_failures); - st.update("levelwise sectors", m_stats.m_levelwise_sectors); - st.update("levelwise sections", m_stats.m_levelwise_sections); - st.update("levelwise spanning-tree", m_stats.m_levelwise_spanning_tree); } void reset_statistics() { @@ -4667,18 +4661,6 @@ namespace nlsat { } } - void solver::record_levelwise_sector() { - m_imp->m_stats.m_levelwise_sectors++; - } - - void solver::record_levelwise_section() { - m_imp->m_stats.m_levelwise_sections++; - } - - void solver::record_levelwise_spanning_tree() { - m_imp->m_stats.m_levelwise_spanning_tree++; - } - 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 7098e3b0f..abd962e24 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -195,9 +195,6 @@ namespace nlsat { void inc_simplify(); void record_levelwise_result(bool success); - void record_levelwise_sector(); - void record_levelwise_section(); - void record_levelwise_spanning_tree(); void add_bound(bound_constraint const& c); /**