mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-08 01:57:59 +00:00
Code Activity

remove sector/section stats

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-26 06:12:03 -10:00
parent 881ec43256
commit b2268544d1
3 changed files with 0 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -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 {

18
src/nlsat/nlsat_solver.cpp
View file

@ -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);
}

3
src/nlsat/nlsat_solver.h
View file

@ -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);
/**