From 306b2908d6638a642bfa0ad86a8ea54f7dc16524 Mon Sep 17 00:00:00 2001 From: jurajsic Date: Fri, 4 Oct 2024 15:10:25 +0200 Subject: [PATCH] add statistic for the number of noodler final checks that actually need to be solved --- src/smt/theory_str_noodler/theory_str_noodler.cpp | 1 + src/smt/theory_str_noodler/theory_str_noodler.h | 1 + src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp | 2 ++ 3 files changed, 4 insertions(+) diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp index 7346d88fe38..8283a8a9316 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp @@ -126,6 +126,7 @@ namespace smt::noodler { void theory_str_noodler::collect_statistics(::statistics & st) const { STRACE("str", tout << "collecting statistics" << std::endl;); + st.update("noodler-final_checks", num_of_solving_final_checks); for (const auto& [heur_name, heur_stats] : this->statistics) { st.update(statistics_bullshit_names.at(heur_name)[0], heur_stats.num_start); st.update(statistics_bullshit_names.at(heur_name)[1], heur_stats.num_finish); diff --git a/src/smt/theory_str_noodler/theory_str_noodler.h b/src/smt/theory_str_noodler/theory_str_noodler.h index a24365a9546..ce423c98856 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler.h +++ b/src/smt/theory_str_noodler/theory_str_noodler.h @@ -131,6 +131,7 @@ namespace smt::noodler { // the length formula from the last run that was sat expr_ref sat_length_formula; + unsigned num_of_solving_final_checks = 0; // number of final checks that lead to solving string formula (i.e. not solved by loop protection nor by language (dis)equalities) std::map statistics { {"underapprox", {0, 0, 0}}, // underapprox of the stabilization-based procedure {"stabilization", {0, 0, 0}}, // stabilization-based procedure diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp index 1ecde8b4807..b0f47492a87 100644 --- a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp +++ b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp @@ -85,6 +85,8 @@ namespace smt::noodler { } } + ++num_of_solving_final_checks; + bool contains_word_equations = !this->m_word_eq_todo_rel.empty(); bool contains_word_disequations = !this->m_word_diseq_todo_rel.empty(); bool contains_conversions = !this->m_conversion_todo.empty();