Collect statistics about normal form inferences (#4127)

This commit adds code to count the number of inferences made of each
inference type for normal form inferences. It extends the Inference
enum in `infer_info.h` and adds two new `sendInference()` methods in the
`InferenceManager` to send and count inferences that have a corresonding
entry in the `Inference` enum.

1 files changed, 27 insertions, 5 deletions

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 389c4e7bf..eebad2274 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -34,11 +34,13 @@ InferenceManager::InferenceManager(TheoryStrings& p,
                                    context::UserContext* u,
                                    SolverState& s,
                                    SkolemCache& skc,
-                                   OutputChannel& out)
+                                   OutputChannel& out,
+                                   SequencesStatistics& statistics)
     : d_parent(p),
       d_state(s),
       d_skCache(skc),
       d_out(out),
+      d_statistics(statistics),
       d_keep(c),
       d_proxyVar(u),
       d_proxyVarToLength(u),
@@ -186,13 +188,33 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
   sendInference(exp, exp_n, eq, c, asLemma);
 }
 
-void InferenceManager::sendInference(const InferInfo& i)
+void InferenceManager::sendInference(const std::vector<Node>& exp,
+                                     const std::vector<Node>& exp_n,
+                                     Node eq,
+                                     Inference infer,
+                                     bool asLemma)
+{
+  d_statistics.d_inferences << infer;
+  std::stringstream ss;
+  ss << infer;
+  sendInference(exp, exp_n, eq, ss.str().c_str(), asLemma);
+}
+
+void InferenceManager::sendInference(const std::vector<Node>& exp,
+                                     Node eq,
+                                     Inference infer,
+                                     bool asLemma)
 {
-  std::stringstream ssi;
-  ssi << i.d_id;
-  sendInference(i.d_ant, i.d_antn, i.d_conc, ssi.str().c_str(), true);
+  d_statistics.d_inferences << infer;
+  std::stringstream ss;
+  ss << infer;
+  sendInference(exp, eq, ss.str().c_str(), asLemma);
 }
 
+void InferenceManager::sendInference(const InferInfo& i)
+{
+  sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true);
+}
 void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
 {
   if (conc.isNull() || conc == d_false)