diff options
Diffstat (limited to 'src/preprocessing/util/ite_utilities.cpp')
-rw-r--r-- | src/preprocessing/util/ite_utilities.cpp | 55 |
1 files changed, 18 insertions, 37 deletions
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 6dfce4254..833fa59b9 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -307,16 +307,10 @@ void ITECompressor::reset() void ITECompressor::garbageCollect() { reset(); } ITECompressor::Statistics::Statistics() - : d_compressCalls("ite-simp::compressCalls", 0), - d_skolemsAdded("ite-simp::skolems", 0) + : d_compressCalls( + smtStatisticsRegistry().registerInt("ite-simp::compressCalls")), + d_skolemsAdded(smtStatisticsRegistry().registerInt("ite-simp::skolems")) { - smtStatisticsRegistry()->registerStat(&d_compressCalls); - smtStatisticsRegistry()->registerStat(&d_skolemsAdded); -} -ITECompressor::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_compressCalls); - smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded); } Node ITECompressor::push_back_boolean(Node original, Node compressed) @@ -704,35 +698,22 @@ bool ITESimplifier::doneALotOfWorkHeuristic() const } ITESimplifier::Statistics::Statistics() - : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0), - d_unexpected("ite-simp::unexpected", 0), - d_unsimplified("ite-simp::unsimplified", 0), - d_exactMatchFold("ite-simp::exactMatchFold", 0), - d_binaryPredFold("ite-simp::binaryPredFold", 0), - d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0), - d_simpITEVisits("ite-simp::simpITE.visits", 0), - d_inSmaller("ite-simp::inSmaller") -{ - smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded); - smtStatisticsRegistry()->registerStat(&d_unexpected); - smtStatisticsRegistry()->registerStat(&d_unsimplified); - smtStatisticsRegistry()->registerStat(&d_exactMatchFold); - smtStatisticsRegistry()->registerStat(&d_binaryPredFold); - smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds); - smtStatisticsRegistry()->registerStat(&d_simpITEVisits); - smtStatisticsRegistry()->registerStat(&d_inSmaller); -} - -ITESimplifier::Statistics::~Statistics() + : d_maxNonConstantsFolded( + smtStatisticsRegistry().registerInt("ite-simp::maxNonConstantsFolded")), + d_unexpected(smtStatisticsRegistry().registerInt("ite-simp::unexpected")), + d_unsimplified( + smtStatisticsRegistry().registerInt("ite-simp::unsimplified")), + d_exactMatchFold( + smtStatisticsRegistry().registerInt("ite-simp::exactMatchFold")), + d_binaryPredFold( + smtStatisticsRegistry().registerInt("ite-simp::binaryPredFold")), + d_specialEqualityFolds(smtStatisticsRegistry().registerInt( + "ite-simp::specialEqualityFolds")), + d_simpITEVisits( + smtStatisticsRegistry().registerInt("ite-simp::simpITE.visits")), + d_inSmaller(smtStatisticsRegistry().registerHistogram<uint32_t>( + "ite-simp::inSmaller")) { - smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded); - smtStatisticsRegistry()->unregisterStat(&d_unexpected); - smtStatisticsRegistry()->unregisterStat(&d_unsimplified); - smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold); - smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold); - smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds); - smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits); - smtStatisticsRegistry()->unregisterStat(&d_inSmaller); } bool ITESimplifier::isConstantIte(TNode e) |