Add statistic for InferenceId to TheoryInferenceManager. (#5913)

This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index aa0aa4f2ae6da00b2ca77efbaf9a8b9430b9c98c..c406c0ce69b4cfbd7227fa77f71173673e35501e 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -25,7 +25,7 @@ namespace arith {
 InferenceManager::InferenceManager(TheoryArith& ta,
                                    ArithState& astate,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(ta, astate, pnm)
+    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith")
 {
 }
 

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index afcc9a719fae89559cb05f84a8c076a1ece5ee0f..a4b8ecd4421ddfafb893ba0ccb8bb26eaf55ab08 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -27,10 +27,9 @@ namespace arrays {
 InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
-    : TheoryInferenceManager(t, state, pnm),
-      d_lemmaPg(pnm ? new EagerProofGenerator(pnm,
-                                              state.getUserContext(),
-                                              "ArrayLemmaProofGenerator")
+    : TheoryInferenceManager(t, state, pnm, "theory::arrays"),
+      d_lemmaPg(pnm ? new EagerProofGenerator(
+                    pnm, state.getUserContext(), "ArrayLemmaProofGenerator")
                     : nullptr)
 {
 }

diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 0ccd06922c30e9ddf0dd335d30c86c70fc42c594..827be4c7f5bd47e24ec816b0c3623c67e3370be2 100644 (file)
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -24,7 +24,7 @@ namespace bags {
 InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm), d_state(s)
+    : InferenceManagerBuffered(t, s, pnm, "theory::bags"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index f6e056f4241e3fb7da90f0705873e568a8ad1cb3..55a0ff46b54fb5a4cc63a5b13f2c2f02cd0ef6da 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -39,7 +39,7 @@ TheoryBV::TheoryBV(context::Context* c,
       d_ufRemByZero(),
       d_rewriter(),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr),
+      d_im(*this, d_state, nullptr, "theory::bv"),
       d_notify(d_im)
 {
   switch (options::bvSolver())

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 496881a33a0fe186839ffac845cf41a6cfaeb766..b4a536b1429880834a5ea40bf22cd97773567ab5 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -28,7 +28,7 @@ namespace datatypes {
 InferenceManager::InferenceManager(Theory& t,
                                    TheoryState& state,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm),
+    : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"),
       d_inferenceLemmas("theory::datatypes::inferenceLemmas"),
       d_inferenceFacts("theory::datatypes::inferenceFacts"),
       d_inferenceConflicts("theory::datatypes::inferenceConflicts"),
@@ -38,7 +38,7 @@ InferenceManager::InferenceManager(Theory& t,
       d_lemPg(pnm == nullptr
                   ? nullptr
                   : new EagerProofGenerator(
-                        pnm, state.getUserContext(), "datatypes::lemPg"))
+                      pnm, state.getUserContext(), "datatypes::lemPg"))
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   smtStatisticsRegistry()->registerStat(&d_inferenceLemmas);

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 6789043b1b5cd5aed30d0294bd2fd495746bf0a2..f4ede969a9ddedd082903893b751136cd5901d1b 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -24,8 +24,10 @@ namespace theory {
 
 InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
                                                    TheoryState& state,
-                                                   ProofNodeManager* pnm)
-    : TheoryInferenceManager(t, state, pnm), d_processingPendingLemmas(false)
+                                                   ProofNodeManager* pnm,
+                                                   const std::string& name)
+    : TheoryInferenceManager(t, state, pnm, name),
+      d_processingPendingLemmas(false)
 {
 }
 

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index f9cddadd39e1de18dd7428d5e8f61e610598a5e8..d12bd40b3944e1a72904dbbe8a4739b49c997269 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -34,7 +34,8 @@ class InferenceManagerBuffered : public TheoryInferenceManager
  public:
   InferenceManagerBuffered(Theory& t,
                            TheoryState& state,
-                           ProofNodeManager* pnm);
+                           ProofNodeManager* pnm,
+                           const std::string& name);
   virtual ~InferenceManagerBuffered() {}
   /**
    * Do we have a pending fact or lemma?

diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 652c4283950c75276f630131dcffb29ebfc2ccf5..faecb7c912d9d876f5957862a1d1d2739bc8450e 100644 (file)
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -20,7 +20,7 @@ namespace quantifiers {
 
 QuantifiersInferenceManager::QuantifiersInferenceManager(
     Theory& t, QuantifiersState& state, ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, state, pnm)
+    : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers")
 {
 }
 

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index db7fa2c6cb029ef490c5a8cbb2b6400b181f75e9..2a409a304e4a12dbd29e0df29f8ab70ede105ef6 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -49,7 +49,7 @@ TheorySep::TheorySep(context::Context* c,
       d_lemmas_produced_c(u),
       d_bounds_init(false),
       d_state(c, u, valuation),
-      d_im(*this, d_state, nullptr),
+      d_im(*this, d_state, nullptr, "theory::sep"),
       d_notify(*this),
       d_reduce(u),
       d_spatial_assertions(c)

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 161a66bfe6ad1cefbdbf5a9d69015e95faeeafd0..dd2b96703ea953b8b66bd0d3838242c4810abdc8 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -26,7 +26,7 @@ namespace sets {
 InferenceManager::InferenceManager(Theory& t,
                                    SolverState& s,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm), d_state(s)
+    : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 8c487d7c1c4aad20bad0b1d753e522a530c031e4..717a34eeadc2a23dcf5fd3771e048fa5d31be8e3 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -34,7 +34,7 @@ InferenceManager::InferenceManager(Theory& t,
                                    ExtTheory& e,
                                    SequencesStatistics& statistics,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(t, s, pnm),
+    : InferenceManagerBuffered(t, s, pnm, "theory::strings"),
       d_state(s),
       d_termReg(tr),
       d_extt(e),

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index a56d616d9253eb2aec05472deca43a8b95893026..a1c1545bff1bb7532777b471540ac1407680d701 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/theory_inference_manager.h"
 
+#include "smt/smt_statistics_registry.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -24,7 +25,8 @@ namespace theory {
 
 TheoryInferenceManager::TheoryInferenceManager(Theory& t,
                                                TheoryState& state,
-                                               ProofNodeManager* pnm)
+                                               ProofNodeManager* pnm,
+                                               const std::string& name)
     : d_theory(t),
       d_theoryState(state),
       d_out(t.getOutputChannel()),
@@ -34,11 +36,24 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t,
       d_lemmasSent(t.getUserContext()),
       d_numConflicts(0),
       d_numCurrentLemmas(0),
-      d_numCurrentFacts(0)
+      d_numCurrentFacts(0),
+      d_conflictIdStats(name + "::inferencesConflict"),
+      d_factIdStats(name + "::inferencesFact"),
+      d_lemmaIdStats(name + "::inferencesLemma")
 {
   // don't add true lemma
   Node truen = NodeManager::currentNM()->mkConst(true);
   d_lemmasSent.insert(truen);
+  smtStatisticsRegistry()->registerStat(&d_conflictIdStats);
+  smtStatisticsRegistry()->registerStat(&d_factIdStats);
+  smtStatisticsRegistry()->registerStat(&d_lemmaIdStats);
+}
+
+TheoryInferenceManager::~TheoryInferenceManager()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats);
+  smtStatisticsRegistry()->unregisterStat(&d_factIdStats);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats);
 }
 
 void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
@@ -89,6 +104,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
+    d_conflictIdStats << id;
     d_theoryState.notifyInConflict();
     d_out.conflict(conf);
     ++d_numConflicts;
@@ -99,6 +115,7 @@ void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
 {
   if (!d_theoryState.isInConflict())
   {
+    d_conflictIdStats << id;
     d_theoryState.notifyInConflict();
     d_out.trustedConflict(tconf);
   }
@@ -230,6 +247,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
       return false;
     }
   }
+  d_lemmaIdStats << id;
   d_numCurrentLemmas++;
   d_out.trustedLemma(tlem, p);
   return true;
@@ -318,6 +336,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 InferenceId id,
                                                 TNode exp)
 {
+  d_factIdStats << id;
   return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
 }
 
@@ -329,6 +348,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 const std::vector<Node>& args)
 {
   Assert(pfr != PfRule::UNKNOWN);
+  d_factIdStats << id;
   return processInternalFact(atom, pol, pfr, exp, args, nullptr);
 }
 
@@ -339,6 +359,7 @@ bool TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 ProofGenerator* pg)
 {
   Assert(pg != nullptr);
+  d_factIdStats << id;
   return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
 }
 

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 7a125789b9176d7e91f64662fe270ea4fd9d57fe..0142f814a300da86558959204a6ebc95eaf8ddaa 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -70,8 +70,11 @@ class TheoryInferenceManager
   /**
    * Constructor, note that state should be the official state of theory t.
    */
-  TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm);
-  virtual ~TheoryInferenceManager() {}
+  TheoryInferenceManager(Theory& t,
+                         TheoryState& state,
+                         ProofNodeManager* pnm,
+                         const std::string& name);
+  virtual ~TheoryInferenceManager();
   /**
    * Set equality engine, ee is a pointer to the official equality engine
    * of theory.
@@ -432,6 +435,12 @@ class TheoryInferenceManager
   uint32_t d_numCurrentLemmas;
   /** The number of internal facts added since the last call to reset. */
   uint32_t d_numCurrentFacts;
+  /** Statistics for conflicts sent via this inference manager. */
+  IntegralHistogramStat<InferenceId> d_conflictIdStats;
+  /** Statistics for facts sent via this inference manager. */
+  IntegralHistogramStat<InferenceId> d_factIdStats;
+  /** Statistics for lemmas sent via this inference manager. */
+  IntegralHistogramStat<InferenceId> d_lemmaIdStats;
 };
 
 }  // namespace theory

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 3ad94c57136b5c535a49e13afb2d58fcb3e210b5..0328080eee267658178ff01a43d6f527716778f6 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -51,7 +51,7 @@ TheoryUF::TheoryUF(context::Context* c,
       d_functionsTerms(c),
       d_symb(u, instanceName),
       d_state(c, u, valuation),
-      d_im(*this, d_state, pnm),
+      d_im(*this, d_state, pnm, "theory::uf"),
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );