diff options
Diffstat (limited to 'src/theory/theory_inference_manager.h')
| -rw-r--r-- | src/theory/theory_inference_manager.h | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 89c4aec3f..a785af186 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -26,8 +26,7 @@ #include "theory/inference_id.h" #include "theory/output_channel.h" #include "theory/trust_node.h" -#include "util/statistics_registry.h" -#include "util/stats_histogram.h" +#include "util/statistics_stats.h" namespace cvc5 { @@ -79,8 +78,8 @@ class TheoryInferenceManager * @param state The state of the theory * @param pnm The proof node manager, which if non-null, enables proofs for * this inference manager - * @param name The name of the inference manager, which is used for giving - * unique names for statistics, + * @param statsName The name of the inference manager, which is used for + * giving unique names for statistics, * @param cacheLemmas Whether all lemmas sent using this theory inference * manager are added to a user-context dependent cache. This means that * only lemmas that are unique after rewriting are sent to the theory engine @@ -89,7 +88,7 @@ class TheoryInferenceManager TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas = true); virtual ~TheoryInferenceManager(); //--------------------------------------- initialization @@ -454,11 +453,11 @@ class TheoryInferenceManager /** The number of internal facts added since the last call to reset. */ uint32_t d_numCurrentFacts; /** Statistics for conflicts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_conflictIdStats; + HistogramStat<InferenceId> d_conflictIdStats; /** Statistics for facts sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_factIdStats; + HistogramStat<InferenceId> d_factIdStats; /** Statistics for lemmas sent via this inference manager. */ - IntegralHistogramStat<InferenceId> d_lemmaIdStats; + HistogramStat<InferenceId> d_lemmaIdStats; }; } // namespace theory |