diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.cpp | 49 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 5 | ||||
-rw-r--r-- | src/theory/arrays/inference_manager.cpp | 7 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 63 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 |
5 files changed, 53 insertions, 75 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) { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index bbb9e8c62..15f27eb96 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -25,8 +25,7 @@ #include "context/backtrackable.h" #include "context/cdlist.h" #include "expr/node.h" -#include "util/statistics_registry.h" -#include "util/stats_timer.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -117,7 +116,7 @@ private: IntStat d_listsCount; IntStat d_callsMergeInfo; IntStat d_maxList; - SizeStat<CNodeInfoMap > d_tableSize; + SizeStat<CNodeInfoMap> d_tableSize; /** * checks if a certain element is in the list l diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 48755b7ea..fc3f67cf0 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -29,10 +29,9 @@ namespace arrays { InferenceManager::InferenceManager(Theory& t, TheoryState& state, ProofNodeManager* pnm) - : TheoryInferenceManager(t, state, pnm, "theory::arrays", false), - d_lemmaPg(pnm ? new EagerProofGenerator(pnm, - state.getUserContext(), - "ArrayLemmaProofGenerator") + : TheoryInferenceManager(t, state, pnm, "theory::arrays::", false), + d_lemmaPg(pnm ? new EagerProofGenerator( + pnm, state.getUserContext(), "ArrayLemmaProofGenerator") : nullptr) { } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index ee95b3c82..1a1090f68 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -62,30 +62,34 @@ TheoryArrays::TheoryArrays(context::Context* c, ProofNodeManager* pnm, std::string name) : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name), - d_numRow(name + "theory::arrays::number of Row lemmas", 0), - d_numExt(name + "theory::arrays::number of Ext lemmas", 0), - d_numProp(name + "theory::arrays::number of propagations", 0), - d_numExplain(name + "theory::arrays::number of explanations", 0), - d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear", - 0), - d_numSharedArrayVarSplits( - name + "theory::arrays::number of shared array var splits", 0), - d_numGetModelValSplits( - name + "theory::arrays::number of getModelVal splits", 0), - d_numGetModelValConflicts( - name + "theory::arrays::number of getModelVal conflicts", 0), - d_numSetModelValSplits( - name + "theory::arrays::number of setModelVal splits", 0), - d_numSetModelValConflicts( - name + "theory::arrays::number of setModelVal conflicts", 0), - d_ppEqualityEngine(u, name + "theory::arrays::pp", true), + d_numRow( + smtStatisticsRegistry().registerInt(name + "number of Row lemmas")), + d_numExt( + smtStatisticsRegistry().registerInt(name + "number of Ext lemmas")), + d_numProp( + smtStatisticsRegistry().registerInt(name + "number of propagations")), + d_numExplain( + smtStatisticsRegistry().registerInt(name + "number of explanations")), + d_numNonLinear(smtStatisticsRegistry().registerInt( + name + "number of calls to setNonLinear")), + d_numSharedArrayVarSplits(smtStatisticsRegistry().registerInt( + name + "number of shared array var splits")), + d_numGetModelValSplits(smtStatisticsRegistry().registerInt( + name + "number of getModelVal splits")), + d_numGetModelValConflicts(smtStatisticsRegistry().registerInt( + name + "number of getModelVal conflicts")), + d_numSetModelValSplits(smtStatisticsRegistry().registerInt( + name + "number of setModelVal splits")), + d_numSetModelValConflicts(smtStatisticsRegistry().registerInt( + name + "number of setModelVal conflicts")), + d_ppEqualityEngine(u, name + "pp", true), d_ppFacts(u), d_state(c, u, valuation), d_im(*this, d_state, pnm), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), - d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true), + d_mayEqualEqualityEngine(c, name + "mayEqual", true), d_notify(*this), d_backtracker(c), d_infoMap(c, &d_backtracker, name), @@ -112,17 +116,6 @@ TheoryArrays::TheoryArrays(context::Context* c, d_dstrat(new TheoryArraysDecisionStrategy(this)), d_dstratInit(false) { - smtStatisticsRegistry()->registerStat(&d_numRow); - smtStatisticsRegistry()->registerStat(&d_numExt); - smtStatisticsRegistry()->registerStat(&d_numProp); - smtStatisticsRegistry()->registerStat(&d_numExplain); - smtStatisticsRegistry()->registerStat(&d_numNonLinear); - smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits); - smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits); - smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts); - smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits); - smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts); - d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); @@ -147,16 +140,6 @@ TheoryArrays::~TheoryArrays() { it2->second->deleteSelf(); } delete d_constReadsContext; - smtStatisticsRegistry()->unregisterStat(&d_numRow); - smtStatisticsRegistry()->unregisterStat(&d_numExt); - smtStatisticsRegistry()->unregisterStat(&d_numProp); - smtStatisticsRegistry()->unregisterStat(&d_numExplain); - smtStatisticsRegistry()->unregisterStat(&d_numNonLinear); - smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits); - smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits); - smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts); - smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits); - smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts); } TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; } @@ -166,7 +149,7 @@ ProofRuleChecker* TheoryArrays::getProofChecker() { return &d_checker; } bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; - esi.d_name = d_instanceName + "theory::arrays::ee"; + esi.d_name = d_instanceName + "ee"; return true; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 188573152..7cf8d52e3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -32,7 +32,7 @@ #include "theory/theory.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" -#include "util/statistics_registry.h" +#include "util/statistics_stats.h" namespace cvc5 { namespace theory { @@ -138,7 +138,7 @@ class TheoryArrays : public Theory { Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm = nullptr, - std::string name = ""); + std::string name = "theory::arrays::"); ~TheoryArrays(); //--------------------------------- initialization |