diff options
Diffstat (limited to 'src/theory/theory_inference_manager.cpp')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index e52321c49..3bc7351fe 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -31,7 +31,7 @@ namespace theory { TheoryInferenceManager::TheoryInferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm, - const std::string& name, + const std::string& statsName, bool cacheLemmas) : d_theory(t), d_theoryState(state), @@ -45,23 +45,20 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_numConflicts(0), d_numCurrentLemmas(0), d_numCurrentFacts(0), - d_conflictIdStats(name + "::inferencesConflict"), - d_factIdStats(name + "::inferencesFact"), - d_lemmaIdStats(name + "::inferencesLemma") + d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesConflict")), + d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesFact")), + d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>( + statsName + "inferencesLemma")) { // don't add true lemma Node truen = NodeManager::currentNM()->mkConst(true); d_lemmasSent.insert(truen); - smtStatisticsRegistry()->registerStat(&d_conflictIdStats); - smtStatisticsRegistry()->registerStat(&d_factIdStats); - smtStatisticsRegistry()->registerStat(&d_lemmaIdStats); } TheoryInferenceManager::~TheoryInferenceManager() { - smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats); - smtStatisticsRegistry()->unregisterStat(&d_factIdStats); - smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats); } void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) |