diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 22 |
1 files changed, 1 insertions, 21 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index a26669fbf..1006076d5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -71,7 +71,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_notify(*this), d_equalityEngine(d_notify, c, "theory::strings", true), d_state(c, d_equalityEngine, d_valuation), - d_im(*this, c, u, d_state, d_sk_cache, out), + d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics), d_pregistered_terms_cache(u), d_registered_terms_cache(u), d_functionsTerms(c), @@ -1155,26 +1155,6 @@ Node TheoryStrings::ppRewrite(TNode atom) { return atom; } -// Stats -TheoryStrings::Statistics::Statistics() - : d_splits("theory::strings::NumOfSplitOnDemands", 0), - d_eq_splits("theory::strings::NumOfEqSplits", 0), - d_deq_splits("theory::strings::NumOfDiseqSplits", 0), - d_loop_lemmas("theory::strings::NumOfLoops", 0) -{ - smtStatisticsRegistry()->registerStat(&d_splits); - smtStatisticsRegistry()->registerStat(&d_eq_splits); - smtStatisticsRegistry()->registerStat(&d_deq_splits); - smtStatisticsRegistry()->registerStat(&d_loop_lemmas); -} - -TheoryStrings::Statistics::~Statistics(){ - smtStatisticsRegistry()->unregisterStat(&d_splits); - smtStatisticsRegistry()->unregisterStat(&d_eq_splits); - smtStatisticsRegistry()->unregisterStat(&d_deq_splits); - smtStatisticsRegistry()->unregisterStat(&d_loop_lemmas); -} - /** run the given inference step */ void TheoryStrings::runInferStep(InferStep s, int effort) { |