summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
-rw-r--r--src/theory/strings/theory_strings.cpp22
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback