summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_stats.h
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-02-11 15:55:31 +0100
committerGitHub <noreply@github.com>2021-02-11 15:55:31 +0100
commit1d0492104a200f6fa5cc7a1cee539436ee26ea99 (patch)
treea66ff6b0bc869f1e84dceb03ddbcc7910e23c77c /src/theory/strings/sequences_stats.h
parentb3f05d5c25facaf0c34ee79faed060bda3f61a8d (diff)
Merge InferenceIds into one enum (#5892)
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories. It merges all InferencedIds into one global enum and makes all theories use them.
Diffstat (limited to 'src/theory/strings/sequences_stats.h')
-rw-r--r--src/theory/strings/sequences_stats.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index e35d951f7..e7e45b18f 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -61,12 +61,12 @@ class SequencesStatistics
IntStat d_strategyRuns;
//--------------- inferences
/** Counts the number of applications of each type of inference */
- HistogramStat<Inference> d_inferences;
+ 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.
*/
- HistogramStat<Inference> d_inferencesNoPf;
+ HistogramStat<InferenceId> d_inferencesNoPf;
/**
* Counts the number of applications of each type of context-dependent
* simplification. The sum of this map is equal to the number of EXTF or
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback