smt: instrument ho-matching and ho-var term-enumeration statistics

Add -st statistics counters:
- ho-matching refinements / instances (default_qm_plugin, gated on
  smt.ho_matching)
- ho-var term-enum: terms produced by mf::ho_var::populate_inst_sets
  in the model finder

Wired via a new quantifier_manager_plugin::collect_statistics virtual
forwarded from quantifier_manager::collect_statistics.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/smt/smt_model_finder.cpp

@@ -38,9 +38,15 @@ Revision History:
 #include "smt/smt_model_finder.h"
 #include "smt/smt_context.h"
 #include "tactic/tactic_exception.h"
+#include "util/statistics.h"
 
 namespace smt {
 
+    // Instrumentation: counts terms produced by ho_var term-enumeration
+    // (mf::ho_var::populate_inst_sets). One increment per enumerated term
+    // inserted into an instantiation set. Reset per model_finder instance.
+    static unsigned g_ho_var_term_enum = 0;
+
     namespace mf {
 
         // -----------------------------------
@@ -1447,6 +1453,7 @@ namespace smt {
                     unsigned generation = 0; // todo - inherited from sub-term of t?
                     TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m)
                                                    << " to instantiation set of S" << std::endl;);
+                    ++g_ho_var_term_enum;
                     S->insert(t, generation);                
                 }
             }
@@ -2408,12 +2415,17 @@ namespace smt {
         m_auf_solver(alloc(auf_solver, m)),
         m_dependencies(m),
         m_new_constraints(m) {
+        g_ho_var_term_enum = 0;
     }
 
     model_finder::~model_finder() {
         reset();
     }
 
+    void model_finder::collect_statistics(::statistics & st) const {
+        st.update("ho-var term-enum", g_ho_var_term_enum);
+    }
+
     void model_finder::checkpoint() {
         checkpoint("model_finder");
     }

src/smt/smt_model_finder.h

@@ -52,6 +52,7 @@ Revision History:
 #include "tactic/tactic_exception.h"
 
 class model_instantiation_set;
+class statistics;
 
 namespace smt {
     class context;
@@ -122,6 +123,8 @@ namespace smt {
 
         quantifier_macro_info* operator()(quantifier* q) override;
 
+        void collect_statistics(::statistics & st) const;
+
     };
 }
 

src/smt/smt_quantifier.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include "smt/smt_quick_checker.h"
 #include "smt/mam.h"
 #include "smt/qi_queue.h"
+#include "util/statistics.h"
 #include "util/obj_hashtable.h"
 
 namespace smt {
@@ -580,6 +581,7 @@ namespace smt {
 
     void quantifier_manager::collect_statistics(::statistics & st) const {
         m_imp->m_qi_queue.collect_statistics(st);
+        m_imp->m_plugin->collect_statistics(st);
     }
 
     void quantifier_manager::reset_statistics() {
@@ -627,6 +629,8 @@ namespace smt {
             vector<std::tuple<enode*, enode*>>* m_used_enodes = nullptr;
         };
         ho_match_state m_ho_state;
+        unsigned       m_stat_ho_refine = 0;    // number of times ho-matching refinement is invoked
+        unsigned       m_stat_ho_instances = 0; // number of instances added via ho-matching
     public:
         default_qm_plugin():
             m_qm(nullptr),
@@ -721,6 +725,7 @@ namespace smt {
             vector<std::tuple<enode*, enode*>> used_enodes;
             m_context->add_instance(q, nullptr, new_bindings.size(), new_bindings.data(),
                                     max_gen, st.m_min_top_generation, st.m_max_top_generation, used_enodes);
+            ++m_stat_ho_instances;
         }
 
         bool try_ho_refine(quantifier* qa, app* pat, unsigned num_bindings, enode* const* bindings,
@@ -751,11 +756,21 @@ namespace smt {
                     verbose_stream() << "  s[" << i << "] = " << mk_pp(s.get(i), m) << " sort=" << mk_pp(s.get(i)->get_sort(), m) << "\n";);
 
             m_ho_matcher->refine_ho_match(pat, s);
+            ++m_stat_ho_refine;
             return true;
         }
 
         bool model_based() const override { return m_fparams->m_mbqi; }
 
+        void collect_statistics(::statistics & st) const override {
+            if (m_fparams->m_ho_matching) {
+                st.update("ho-matching refinements", m_stat_ho_refine);
+                st.update("ho-matching instances", m_stat_ho_instances);
+            }
+            if (m_model_finder)
+                m_model_finder->collect_statistics(st);
+        }
+
         bool mbqi_enabled(quantifier *q) const override {
             if (!m_fparams->m_mbqi_id) return true;
             const symbol &s = q->get_qid();

src/smt/smt_quantifier.h

@@ -186,5 +186,7 @@ namespace smt {
                                      unsigned max_generation, unsigned min_top_generation, unsigned max_top_generation,
                                      vector<std::tuple<enode*, enode*>>& used_enodes) { return false; }
 
+        virtual void collect_statistics(::statistics & st) const {}
+
     };
 }