diff options
Diffstat (limited to 'src/theory/arrays/array_info.cpp')
-rw-r--r-- | src/theory/arrays/array_info.cpp | 49 |
1 files changed, 23 insertions, 26 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 164b9b058..4dc7201fb 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -43,26 +43,31 @@ Info::~Info() { in_stores->deleteSelf(); } -ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix) - : ct(c), bck(b), info_map(), - d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"), - d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"), - d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"), - d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"), - d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0), - d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0), - d_maxList(statisticsPrefix + "theory::arrays::maxList",0), - d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) { +ArrayInfo::ArrayInfo(context::Context* c, + Backtracker<TNode>* b, + std::string statisticsPrefix) + : ct(c), + bck(b), + info_map(), + d_mergeInfoTimer(smtStatisticsRegistry().registerTimer( + statisticsPrefix + "mergeInfoTimer")), + d_avgIndexListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgIndexListLength")), + d_avgStoresListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgStoresListLength")), + d_avgInStoresListLength(smtStatisticsRegistry().registerAverage( + statisticsPrefix + "avgInStoresListLength")), + d_listsCount( + smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")), + d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix + + "callsMergeInfo")), + d_maxList( + smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")), + d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>( + statisticsPrefix + "infoTableSize", info_map)) +{ emptyList = new(true) CTNodeList(ct); emptyInfo = new Info(ct, bck); - smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer); - smtStatisticsRegistry()->registerStat(&d_avgIndexListLength); - smtStatisticsRegistry()->registerStat(&d_avgStoresListLength); - smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength); - smtStatisticsRegistry()->registerStat(&d_listsCount); - smtStatisticsRegistry()->registerStat(&d_callsMergeInfo); - smtStatisticsRegistry()->registerStat(&d_maxList); - smtStatisticsRegistry()->registerStat(&d_tableSize); } ArrayInfo::~ArrayInfo() { @@ -75,14 +80,6 @@ ArrayInfo::~ArrayInfo() { } emptyList->deleteSelf(); delete emptyInfo; - smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer); - smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength); - smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength); - smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength); - smtStatisticsRegistry()->unregisterStat(&d_listsCount); - smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo); - smtStatisticsRegistry()->unregisterStat(&d_maxList); - smtStatisticsRegistry()->unregisterStat(&d_tableSize); } bool inList(const CTNodeList* l, const TNode el) { |