From: Andrew Reynolds Date: Fri, 10 Apr 2020 15:45:52 +0000 (-0500) Subject: Add a few stats to strings (#4252) X-Git-Tag: cvc5-1.0.0~3389 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=854d36b3ebb85579eefd654a18ed882b99649fb5;p=cvc5.git Add a few stats to strings (#4252) To give an idea of the high-level behavior. --- diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp index afcfb1a60..c830a68bd 100644 --- a/src/theory/strings/sequences_stats.cpp +++ b/src/theory/strings/sequences_stats.cpp @@ -22,7 +22,9 @@ namespace theory { namespace strings { SequencesStatistics::SequencesStatistics() - : d_inferences("theory::strings::inferences"), + : d_checkRuns("theory::strings::checkRuns", 0), + d_strategyRuns("theory::strings::strategyRuns", 0), + d_inferences("theory::strings::inferences"), d_cdSimplifications("theory::strings::cdSimplifications"), d_reductions("theory::strings::reductions"), d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"), @@ -38,6 +40,8 @@ SequencesStatistics::SequencesStatistics() 0), d_lemmasInfer("theory::strings::lemmasInfer", 0) { + smtStatisticsRegistry()->registerStat(&d_checkRuns); + smtStatisticsRegistry()->registerStat(&d_strategyRuns); smtStatisticsRegistry()->registerStat(&d_inferences); smtStatisticsRegistry()->registerStat(&d_cdSimplifications); smtStatisticsRegistry()->registerStat(&d_reductions); @@ -56,6 +60,8 @@ SequencesStatistics::SequencesStatistics() SequencesStatistics::~SequencesStatistics() { + smtStatisticsRegistry()->unregisterStat(&d_checkRuns); + smtStatisticsRegistry()->unregisterStat(&d_strategyRuns); smtStatisticsRegistry()->unregisterStat(&d_inferences); 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 63d9f55eb..8a1564587 100644 --- a/src/theory/strings/sequences_stats.h +++ b/src/theory/strings/sequences_stats.h @@ -55,6 +55,10 @@ class SequencesStatistics public: SequencesStatistics(); ~SequencesStatistics(); + /** Number of calls to run a check where strategy is present */ + IntStat d_checkRuns; + /** Number of calls to run the strategy */ + IntStat d_strategyRuns; //--------------- inferences /** Counts the number of applications of each type of inference */ HistogramStat d_inferences; diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 609822fe1..81e43c595 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -737,12 +737,14 @@ void TheoryStrings::check(Effort e) { } Trace("strings-eqc") << std::endl; } + ++(d_statistics.d_checkRuns); unsigned sbegin = itsr->second.first; unsigned send = itsr->second.second; bool addedLemma = false; bool addedFact; Trace("strings-check") << "Full effort check..." << std::endl; do{ + ++(d_statistics.d_strategyRuns); Trace("strings-check") << " * Run strategy..." << std::endl; runStrategy(sbegin, send); // flush the facts