summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/array_info.cpp49
-rw-r--r--src/theory/arrays/array_info.h5
-rw-r--r--src/theory/arrays/inference_manager.cpp7
-rw-r--r--src/theory/arrays/theory_arrays.cpp63
-rw-r--r--src/theory/arrays/theory_arrays.h4
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback