Remove string stat for inferences (#5932)

This is now subsumed by the general stat in TheoryInferenceManager

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 0268fa31a247d1507b082282e9c106cf6df2d2ed..a561cc1b4955b1610f417a9d7c6fd555c5af6472 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -137,71 +137,76 @@ const char* toString(InferenceId i)
     case InferenceId::SETS_RELS_TUPLE_REDUCTION:
       return "SETS_RELS_TUPLE_REDUCTION";
 
-    case InferenceId::STRINGS_I_NORM_S: return "I_NORM_S";
-    case InferenceId::STRINGS_I_CONST_MERGE: return "I_CONST_MERGE";
-    case InferenceId::STRINGS_I_CONST_CONFLICT: return "I_CONST_CONFLICT";
-    case InferenceId::STRINGS_I_NORM: return "I_NORM";
-    case InferenceId::STRINGS_UNIT_INJ: return "UNIT_INJ";
-    case InferenceId::STRINGS_UNIT_CONST_CONFLICT: return "UNIT_CONST_CONFLICT";
-    case InferenceId::STRINGS_UNIT_INJ_DEQ: return "UNIT_INJ_DEQ";
-    case InferenceId::STRINGS_CARD_SP: return "CARD_SP";
-    case InferenceId::STRINGS_CARDINALITY: return "CARDINALITY";
-    case InferenceId::STRINGS_I_CYCLE_E: return "I_CYCLE_E";
-    case InferenceId::STRINGS_I_CYCLE: return "I_CYCLE";
-    case InferenceId::STRINGS_F_CONST: return "F_CONST";
-    case InferenceId::STRINGS_F_UNIFY: return "F_UNIFY";
-    case InferenceId::STRINGS_F_ENDPOINT_EMP: return "F_ENDPOINT_EMP";
-    case InferenceId::STRINGS_F_ENDPOINT_EQ: return "F_ENDPOINT_EQ";
-    case InferenceId::STRINGS_F_NCTN: return "F_NCTN";
-    case InferenceId::STRINGS_N_EQ_CONF: return "N_EQ_CONF";
-    case InferenceId::STRINGS_N_ENDPOINT_EMP: return "N_ENDPOINT_EMP";
-    case InferenceId::STRINGS_N_UNIFY: return "N_UNIFY";
-    case InferenceId::STRINGS_N_ENDPOINT_EQ: return "N_ENDPOINT_EQ";
-    case InferenceId::STRINGS_N_CONST: return "N_CONST";
-    case InferenceId::STRINGS_INFER_EMP: return "INFER_EMP";
-    case InferenceId::STRINGS_SSPLIT_CST_PROP: return "SSPLIT_CST_PROP";
-    case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "SSPLIT_VAR_PROP";
-    case InferenceId::STRINGS_LEN_SPLIT: return "LEN_SPLIT";
-    case InferenceId::STRINGS_LEN_SPLIT_EMP: return "LEN_SPLIT_EMP";
-    case InferenceId::STRINGS_SSPLIT_CST: return "SSPLIT_CST";
-    case InferenceId::STRINGS_SSPLIT_VAR: return "SSPLIT_VAR";
-    case InferenceId::STRINGS_FLOOP: return "FLOOP";
-    case InferenceId::STRINGS_FLOOP_CONFLICT: return "FLOOP_CONFLICT";
-    case InferenceId::STRINGS_NORMAL_FORM: return "NORMAL_FORM";
-    case InferenceId::STRINGS_N_NCTN: return "N_NCTN";
-    case InferenceId::STRINGS_LEN_NORM: return "LEN_NORM";
-    case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT: return "DEQ_DISL_EMP_SPLIT";
+    case InferenceId::STRINGS_I_NORM_S: return "STRINGS_I_NORM_S";
+    case InferenceId::STRINGS_I_CONST_MERGE: return "STRINGS_I_CONST_MERGE";
+    case InferenceId::STRINGS_I_CONST_CONFLICT:
+      return "STRINGS_I_CONST_CONFLICT";
+    case InferenceId::STRINGS_I_NORM: return "STRINGS_I_NORM";
+    case InferenceId::STRINGS_UNIT_INJ: return "STRINGS_UNIT_INJ";
+    case InferenceId::STRINGS_UNIT_CONST_CONFLICT:
+      return "STRINGS_UNIT_CONST_CONFLICT";
+    case InferenceId::STRINGS_UNIT_INJ_DEQ: return "STRINGS_UNIT_INJ_DEQ";
+    case InferenceId::STRINGS_CARD_SP: return "STRINGS_CARD_SP";
+    case InferenceId::STRINGS_CARDINALITY: return "STRINGS_CARDINALITY";
+    case InferenceId::STRINGS_I_CYCLE_E: return "STRINGS_I_CYCLE_E";
+    case InferenceId::STRINGS_I_CYCLE: return "STRINGS_I_CYCLE";
+    case InferenceId::STRINGS_F_CONST: return "STRINGS_F_CONST";
+    case InferenceId::STRINGS_F_UNIFY: return "STRINGS_F_UNIFY";
+    case InferenceId::STRINGS_F_ENDPOINT_EMP: return "STRINGS_F_ENDPOINT_EMP";
+    case InferenceId::STRINGS_F_ENDPOINT_EQ: return "STRINGS_F_ENDPOINT_EQ";
+    case InferenceId::STRINGS_F_NCTN: return "STRINGS_F_NCTN";
+    case InferenceId::STRINGS_N_EQ_CONF: return "STRINGS_N_EQ_CONF";
+    case InferenceId::STRINGS_N_ENDPOINT_EMP: return "STRINGS_N_ENDPOINT_EMP";
+    case InferenceId::STRINGS_N_UNIFY: return "STRINGS_N_UNIFY";
+    case InferenceId::STRINGS_N_ENDPOINT_EQ: return "STRINGS_N_ENDPOINT_EQ";
+    case InferenceId::STRINGS_N_CONST: return "STRINGS_N_CONST";
+    case InferenceId::STRINGS_INFER_EMP: return "STRINGS_INFER_EMP";
+    case InferenceId::STRINGS_SSPLIT_CST_PROP: return "STRINGS_SSPLIT_CST_PROP";
+    case InferenceId::STRINGS_SSPLIT_VAR_PROP: return "STRINGS_SSPLIT_VAR_PROP";
+    case InferenceId::STRINGS_LEN_SPLIT: return "STRINGS_LEN_SPLIT";
+    case InferenceId::STRINGS_LEN_SPLIT_EMP: return "STRINGS_LEN_SPLIT_EMP";
+    case InferenceId::STRINGS_SSPLIT_CST: return "STRINGS_SSPLIT_CST";
+    case InferenceId::STRINGS_SSPLIT_VAR: return "STRINGS_SSPLIT_VAR";
+    case InferenceId::STRINGS_FLOOP: return "STRINGS_FLOOP";
+    case InferenceId::STRINGS_FLOOP_CONFLICT: return "STRINGS_FLOOP_CONFLICT";
+    case InferenceId::STRINGS_NORMAL_FORM: return "STRINGS_NORMAL_FORM";
+    case InferenceId::STRINGS_N_NCTN: return "STRINGS_N_NCTN";
+    case InferenceId::STRINGS_LEN_NORM: return "STRINGS_LEN_NORM";
+    case InferenceId::STRINGS_DEQ_DISL_EMP_SPLIT:
+      return "STRINGS_DEQ_DISL_EMP_SPLIT";
     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT:
-      return "DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
+      return "STRINGS_DEQ_DISL_FIRST_CHAR_EQ_SPLIT";
     case InferenceId::STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT:
-      return "DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
-    case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "DEQ_STRINGS_EQ";
-    case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT: return "DEQ_DISL_STRINGS_SPLIT";
-    case InferenceId::STRINGS_DEQ_LENS_EQ: return "DEQ_LENS_EQ";
-    case InferenceId::STRINGS_DEQ_NORM_EMP: return "DEQ_NORM_EMP";
-    case InferenceId::STRINGS_DEQ_LENGTH_SP: return "DEQ_LENGTH_SP";
-    case InferenceId::STRINGS_CODE_PROXY: return "CODE_PROXY";
-    case InferenceId::STRINGS_CODE_INJ: return "CODE_INJ";
-    case InferenceId::STRINGS_RE_NF_CONFLICT: return "RE_NF_CONFLICT";
-    case InferenceId::STRINGS_RE_UNFOLD_POS: return "RE_UNFOLD_POS";
-    case InferenceId::STRINGS_RE_UNFOLD_NEG: return "RE_UNFOLD_NEG";
-    case InferenceId::STRINGS_RE_INTER_INCLUDE: return "RE_INTER_INCLUDE";
-    case InferenceId::STRINGS_RE_INTER_CONF: return "RE_INTER_CONF";
-    case InferenceId::STRINGS_RE_INTER_INFER: return "RE_INTER_INFER";
-    case InferenceId::STRINGS_RE_DELTA: return "RE_DELTA";
-    case InferenceId::STRINGS_RE_DELTA_CONF: return "RE_DELTA_CONF";
-    case InferenceId::STRINGS_RE_DERIVE: return "RE_DERIVE";
-    case InferenceId::STRINGS_EXTF: return "EXTF";
-    case InferenceId::STRINGS_EXTF_N: return "EXTF_N";
-    case InferenceId::STRINGS_EXTF_D: return "EXTF_D";
-    case InferenceId::STRINGS_EXTF_D_N: return "EXTF_D_N";
-    case InferenceId::STRINGS_EXTF_EQ_REW: return "EXTF_EQ_REW";
-    case InferenceId::STRINGS_CTN_TRANS: return "CTN_TRANS";
-    case InferenceId::STRINGS_CTN_DECOMPOSE: return "CTN_DECOMPOSE";
-    case InferenceId::STRINGS_CTN_NEG_EQUAL: return "CTN_NEG_EQUAL";
-    case InferenceId::STRINGS_CTN_POS: return "CTN_POS";
-    case InferenceId::STRINGS_REDUCTION: return "REDUCTION";
-    case InferenceId::STRINGS_PREFIX_CONFLICT: return "PREFIX_CONFLICT";
+      return "STRINGS_DEQ_DISL_FIRST_CHAR_STRING_SPLIT";
+    case InferenceId::STRINGS_DEQ_STRINGS_EQ: return "STRINGS_DEQ_STRINGS_EQ";
+    case InferenceId::STRINGS_DEQ_DISL_STRINGS_SPLIT:
+      return "STRINGS_DEQ_DISL_STRINGS_SPLIT";
+    case InferenceId::STRINGS_DEQ_LENS_EQ: return "STRINGS_DEQ_LENS_EQ";
+    case InferenceId::STRINGS_DEQ_NORM_EMP: return "STRINGS_DEQ_NORM_EMP";
+    case InferenceId::STRINGS_DEQ_LENGTH_SP: return "STRINGS_DEQ_LENGTH_SP";
+    case InferenceId::STRINGS_CODE_PROXY: return "STRINGS_CODE_PROXY";
+    case InferenceId::STRINGS_CODE_INJ: return "STRINGS_CODE_INJ";
+    case InferenceId::STRINGS_RE_NF_CONFLICT: return "STRINGS_RE_NF_CONFLICT";
+    case InferenceId::STRINGS_RE_UNFOLD_POS: return "STRINGS_RE_UNFOLD_POS";
+    case InferenceId::STRINGS_RE_UNFOLD_NEG: return "STRINGS_RE_UNFOLD_NEG";
+    case InferenceId::STRINGS_RE_INTER_INCLUDE:
+      return "STRINGS_RE_INTER_INCLUDE";
+    case InferenceId::STRINGS_RE_INTER_CONF: return "STRINGS_RE_INTER_CONF";
+    case InferenceId::STRINGS_RE_INTER_INFER: return "STRINGS_RE_INTER_INFER";
+    case InferenceId::STRINGS_RE_DELTA: return "STRINGS_RE_DELTA";
+    case InferenceId::STRINGS_RE_DELTA_CONF: return "STRINGS_RE_DELTA_CONF";
+    case InferenceId::STRINGS_RE_DERIVE: return "STRINGS_RE_DERIVE";
+    case InferenceId::STRINGS_EXTF: return "STRINGS_EXTF";
+    case InferenceId::STRINGS_EXTF_N: return "STRINGS_EXTF_N";
+    case InferenceId::STRINGS_EXTF_D: return "STRINGS_EXTF_D";
+    case InferenceId::STRINGS_EXTF_D_N: return "STRINGS_EXTF_D_N";
+    case InferenceId::STRINGS_EXTF_EQ_REW: return "STRINGS_EXTF_EQ_REW";
+    case InferenceId::STRINGS_CTN_TRANS: return "STRINGS_CTN_TRANS";
+    case InferenceId::STRINGS_CTN_DECOMPOSE: return "STRINGS_CTN_DECOMPOSE";
+    case InferenceId::STRINGS_CTN_NEG_EQUAL: return "STRINGS_CTN_NEG_EQUAL";
+    case InferenceId::STRINGS_CTN_POS: return "STRINGS_CTN_POS";
+    case InferenceId::STRINGS_REDUCTION: return "STRINGS_REDUCTION";
+    case InferenceId::STRINGS_PREFIX_CONFLICT: return "STRINGS_PREFIX_CONFLICT";
 
     case InferenceId::UF_HO_APP_ENCODE: return "UF_HO_APP_ENCODE";
     case InferenceId::UF_HO_APP_CONV_SKOLEM: return "UF_HO_APP_CONV_SKOLEM";

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 717a34eeadc2a23dcf5fd3771e048fa5d31be8e3..a161c7854191fb025fc49040c9b326a6015c6f6d 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -288,7 +288,6 @@ void InferenceManager::processConflict(const InferInfo& ii)
 {
   Assert(!d_state.isInConflict());
   // setup the fact to reproduce the proof in the call below
-  d_statistics.d_inferences << ii.getId();
   if (d_ipc != nullptr)
   {
     d_ipc->notifyFact(ii);
@@ -332,7 +331,6 @@ bool InferenceManager::processFact(InferInfo& ii)
   for (const Node& fact : facts)
   {
     ii.d_conc = fact;
-    d_statistics.d_inferences << ii.getId();
     bool polarity = fact.getKind() != NOT;
     TNode atom = polarity ? fact : fact[0];
     bool curRet = false;
@@ -387,7 +385,6 @@ bool InferenceManager::processLemma(InferInfo& ii)
   }
   // ensure that the proof generator is ready to explain the final conclusion
   // of the lemma (ii.d_conc).
-  d_statistics.d_inferences << ii.getId();
   if (d_ipc != nullptr)
   {
     d_ipc->notifyFact(ii);

diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index fe6bc548eccb1a52faf41c38cf36f8519043f292..6e03f078dcc76f1f802b0df24c6208805b12d59d 100644 (file)
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -24,7 +24,6 @@ namespace strings {
 SequencesStatistics::SequencesStatistics()
     : d_checkRuns("theory::strings::checkRuns", 0),
       d_strategyRuns("theory::strings::strategyRuns", 0),
-      d_inferences("theory::strings::inferences"),
       d_inferencesNoPf("theory::strings::inferencesNoPf"),
       d_cdSimplifications("theory::strings::cdSimplifications"),
       d_reductions("theory::strings::reductions"),
@@ -43,7 +42,6 @@ SequencesStatistics::SequencesStatistics()
 {
   smtStatisticsRegistry()->registerStat(&d_checkRuns);
   smtStatisticsRegistry()->registerStat(&d_strategyRuns);
-  smtStatisticsRegistry()->registerStat(&d_inferences);
   smtStatisticsRegistry()->registerStat(&d_inferencesNoPf);
   smtStatisticsRegistry()->registerStat(&d_cdSimplifications);
   smtStatisticsRegistry()->registerStat(&d_reductions);
@@ -64,7 +62,6 @@ SequencesStatistics::~SequencesStatistics()
 {
   smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
   smtStatisticsRegistry()->unregisterStat(&d_strategyRuns);
-  smtStatisticsRegistry()->unregisterStat(&d_inferences);
   smtStatisticsRegistry()->unregisterStat(&d_inferencesNoPf);
   smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications);
   smtStatisticsRegistry()->unregisterStat(&d_reductions);

diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index e7e45b18f3878e23f63c57fac2fb7ba2645ded90..deda742fe976d2e896cdd5e35fa3512c004e77fb 100644 (file)
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -60,11 +60,11 @@ class SequencesStatistics
   /** Number of calls to run the strategy */
   IntStat d_strategyRuns;
   //--------------- inferences
-  /** Counts the number of applications of each type of inference */
-  HistogramStat<InferenceId> d_inferences;
   /**
    * Counts the number of applications of each type of inference that were not
-   * processed as a proof step. This is a subset of d_inferences.
+   * processed as a proof step. This is a subset of the statistics in
+   * TheoryInferenceManager, i.e.
+   * (theory::strings::inferences{Facts,Lemmas,Conflicts}).
    */
   HistogramStat<InferenceId> d_inferencesNoPf;
   /**