diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-26 09:52:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-26 09:52:28 -0500 |
commit | c9fd28a391cfff767b899a65ad365742745910fe (patch) | |
tree | 663ffc3b744c9df9de3781aaf292fa6b79851fdc /src/theory/strings/sequences_stats.cpp | |
parent | 9523b4248da9764fa14f078659b42085a7fe2654 (diff) |
Add stats for string reductions, lemmas and conflicts (#4149)
This PR adds comprehensive stats for reductions, lemmas and conflicts in TheoryStrings. Remaining stats will track all inferences (which are finer grained steps that may lead to lemmas/conflicts).
Additionally this PR refactors calls to OutputChannel::lemma in TheoryStrings / InferenceManager. There are now only 2 calls to lemma(...) during registerTerm(...), one for "atomic" string terms (corresponding to length splits typically) and one for non-atomic terms.
Diffstat (limited to 'src/theory/strings/sequences_stats.cpp')
-rw-r--r-- | src/theory/strings/sequences_stats.cpp | 30 |
1 files changed, 29 insertions, 1 deletions
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index 0f1e93599..fb13cdab2 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -22,14 +22,42 @@ namespace theory { namespace strings { SequencesStatistics::SequencesStatistics() - : d_inferences("theory::strings::inferences") + : d_inferences("theory::strings::inferences"), + d_reductions("theory::strings::reductions"), + d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0), + d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0), + d_conflictsInfer("theory::strings::conflictsInfer", 0), + d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0), + d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0), + d_lemmasRegisterTerm("theory::strings::lemmasRegisterTerm", 0), + d_lemmasRegisterTermAtomic("theory::strings::lemmasRegisterTermAtomic", + 0), + d_lemmasInfer("theory::strings::lemmasInfer", 0) { smtStatisticsRegistry()->registerStat(&d_inferences); + smtStatisticsRegistry()->registerStat(&d_reductions); + smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine); + smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->registerStat(&d_conflictsInfer); + smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc); + smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit); + smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTerm); + smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTermAtomic); + smtStatisticsRegistry()->registerStat(&d_lemmasInfer); } SequencesStatistics::~SequencesStatistics() { smtStatisticsRegistry()->unregisterStat(&d_inferences); + smtStatisticsRegistry()->unregisterStat(&d_reductions); + smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine); + smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix); + smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer); + smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc); + smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit); + smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm); + smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic); + smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer); } } |