From: Andrew Reynolds Date: Fri, 19 Feb 2021 10:07:27 +0000 (-0600) Subject: Remove string stat for inferences (#5932) X-Git-Tag: cvc5-1.0.0~2260 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b30adb7a22091dfcd2f81f7cf04334e2240c19bd;p=cvc5.git 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 0268fa31a..a561cc1b4 100644 --- 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 717a34eea..a161c7854 100644 --- 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 fe6bc548e..6e03f078d 100644 --- 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 e7e45b18f..deda742fe 100644 --- 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 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 d_inferencesNoPf; /**