Merge pull request #188 from VeriFIT/final_check_stat

Add noodler final_check statistic

Author: jurajsic

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

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<std::string, DecProcStats> statistics {
             {"underapprox", {0, 0, 0}}, // underapprox of the stabilization-based procedure
             {"stabilization", {0, 0, 0}}, // stabilization-based procedure

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();