From 854d36b3ebb85579eefd654a18ed882b99649fb5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 10 Apr 2020 10:45:52 -0500
Subject: Add a few stats to strings (#4252)

To give an idea of the high-level behavior.
---
 src/theory/strings/sequences_stats.cpp | 8 +++++++-
 src/theory/strings/sequences_stats.h   | 4 ++++
 src/theory/strings/theory_strings.cpp  | 2 ++
 3 files changed, 13 insertions(+), 1 deletion(-)

(limited to 'src')

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<Inference> 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
-- 
cgit v1.2.3