summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_stats.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/sequences_stats.h')
-rw-r--r--src/theory/strings/sequences_stats.h4
1 files changed, 4 insertions, 0 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback