summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_stats.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-02-19 04:07:27 -0600
committerGitHub <noreply@github.com>2021-02-19 11:07:27 +0100
commitb30adb7a22091dfcd2f81f7cf04334e2240c19bd (patch)
tree893214af0f7d0b67cd2edbe92b8348aefe71342e /src/theory/strings/sequences_stats.h
parentce58453982ddd53a5fc08d9db4c6c3f49b852838 (diff)
Remove string stat for inferences (#5932)
This is now subsumed by the general stat in TheoryInferenceManager
Diffstat (limited to 'src/theory/strings/sequences_stats.h')
-rw-r--r--src/theory/strings/sequences_stats.h6
1 files changed, 3 insertions, 3 deletions
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<InferenceId> 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<InferenceId> d_inferencesNoPf;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback