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.cpp43
-rw-r--r--src/theory/arrays/array_info.h58
-rw-r--r--src/theory/arrays/theory_arrays.cpp41
-rw-r--r--src/theory/arrays/theory_arrays.h2
4 files changed, 76 insertions, 68 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index cd0025fe2..e94abe9cb 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -17,10 +17,53 @@
#include "theory/arrays/array_info.h"
+#include "smt/smt_statistics_registry.h"
+
namespace CVC4 {
namespace theory {
namespace arrays {
+ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
+ : ct(c), bck(b), info_map(),
+ d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
+ d_avgIndexListLength("theory::arrays::avgIndexListLength"),
+ d_avgStoresListLength("theory::arrays::avgStoresListLength"),
+ d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
+ d_listsCount("theory::arrays::listsCount",0),
+ d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
+ d_maxList("theory::arrays::maxList",0),
+ d_tableSize("theory::arrays::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() {
+ CNodeInfoMap::iterator it = info_map.begin();
+ for( ; it != info_map.end(); it++ ) {
+ if((*it).second!= emptyInfo) {
+ delete (*it).second;
+ }
+ }
+ 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) {
CTNodeList::const_iterator it = l->begin();
for ( ; it!= l->end(); it ++) {
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index f14788ed5..3e479e0f9 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -27,8 +27,8 @@
#include "context/cdlist.h"
#include "context/cdhashmap.h"
#include "expr/node.h"
-#include "expr/statistics_registry.h"
#include "util/ntuple.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
@@ -163,54 +163,18 @@ public:
d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
d_maxList("theory::arrays::maxList",0),
d_tableSize("theory::arrays::infoTableSize", info_map) {
- StatisticsRegistry::registerStat(&d_mergeInfoTimer);
- StatisticsRegistry::registerStat(&d_avgIndexListLength);
- StatisticsRegistry::registerStat(&d_avgStoresListLength);
- StatisticsRegistry::registerStat(&d_avgInStoresListLength);
- StatisticsRegistry::registerStat(&d_listsCount);
- StatisticsRegistry::registerStat(&d_callsMergeInfo);
- StatisticsRegistry::registerStat(&d_maxList);
- StatisticsRegistry::registerStat(&d_tableSize);
+ currentStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
+ currentStatisticsRegistry()->registerStat(&d_avgIndexListLength);
+ currentStatisticsRegistry()->registerStat(&d_avgStoresListLength);
+ currentStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
+ currentStatisticsRegistry()->registerStat(&d_listsCount);
+ currentStatisticsRegistry()->registerStat(&d_callsMergeInfo);
+ currentStatisticsRegistry()->registerStat(&d_maxList);
+ currentStatisticsRegistry()->registerStat(&d_tableSize);
}*/
- ArrayInfo(context::Context* c, Backtracker<TNode>* b): ct(c), bck(b), info_map(),
- d_mergeInfoTimer("theory::arrays::mergeInfoTimer"),
- d_avgIndexListLength("theory::arrays::avgIndexListLength"),
- d_avgStoresListLength("theory::arrays::avgStoresListLength"),
- d_avgInStoresListLength("theory::arrays::avgInStoresListLength"),
- d_listsCount("theory::arrays::listsCount",0),
- d_callsMergeInfo("theory::arrays::callsMergeInfo",0),
- d_maxList("theory::arrays::maxList",0),
- d_tableSize("theory::arrays::infoTableSize", info_map) {
- emptyList = new(true) CTNodeList(ct);
- emptyInfo = new Info(ct, bck);
- StatisticsRegistry::registerStat(&d_mergeInfoTimer);
- StatisticsRegistry::registerStat(&d_avgIndexListLength);
- StatisticsRegistry::registerStat(&d_avgStoresListLength);
- StatisticsRegistry::registerStat(&d_avgInStoresListLength);
- StatisticsRegistry::registerStat(&d_listsCount);
- StatisticsRegistry::registerStat(&d_callsMergeInfo);
- StatisticsRegistry::registerStat(&d_maxList);
- StatisticsRegistry::registerStat(&d_tableSize);
- }
+ ArrayInfo(context::Context* c, Backtracker<TNode>* b);
- ~ArrayInfo() {
- CNodeInfoMap::iterator it = info_map.begin();
- for( ; it != info_map.end(); it++ ) {
- if((*it).second!= emptyInfo) {
- delete (*it).second;
- }
- }
- emptyList->deleteSelf();
- delete emptyInfo;
- StatisticsRegistry::unregisterStat(&d_mergeInfoTimer);
- StatisticsRegistry::unregisterStat(&d_avgIndexListLength);
- StatisticsRegistry::unregisterStat(&d_avgStoresListLength);
- StatisticsRegistry::unregisterStat(&d_avgInStoresListLength);
- StatisticsRegistry::unregisterStat(&d_listsCount);
- StatisticsRegistry::unregisterStat(&d_callsMergeInfo);
- StatisticsRegistry::unregisterStat(&d_maxList);
- StatisticsRegistry::unregisterStat(&d_tableSize);
- };
+ ~ArrayInfo();
/**
* adds the node a to the map if it does not exist
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index ab57eb260..508a4b323 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -22,6 +22,7 @@
#include "options/arrays_options.h"
#include "options/smt_options.h"
#include "smt/logic_exception.h"
+#include "smt/smt_statistics_registry.h"
#include "smt_util/command.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
@@ -98,16 +99,16 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
d_arrayMerges(c),
d_inCheckModel(false)
{
- StatisticsRegistry::registerStat(&d_numRow);
- StatisticsRegistry::registerStat(&d_numExt);
- StatisticsRegistry::registerStat(&d_numProp);
- StatisticsRegistry::registerStat(&d_numExplain);
- StatisticsRegistry::registerStat(&d_numNonLinear);
- StatisticsRegistry::registerStat(&d_numSharedArrayVarSplits);
- StatisticsRegistry::registerStat(&d_numGetModelValSplits);
- StatisticsRegistry::registerStat(&d_numGetModelValConflicts);
- StatisticsRegistry::registerStat(&d_numSetModelValSplits);
- StatisticsRegistry::registerStat(&d_numSetModelValConflicts);
+ 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);
@@ -137,16 +138,16 @@ TheoryArrays::~TheoryArrays() {
it2->second->deleteSelf();
}
delete d_constReadsContext;
- StatisticsRegistry::unregisterStat(&d_numRow);
- StatisticsRegistry::unregisterStat(&d_numExt);
- StatisticsRegistry::unregisterStat(&d_numProp);
- StatisticsRegistry::unregisterStat(&d_numExplain);
- StatisticsRegistry::unregisterStat(&d_numNonLinear);
- StatisticsRegistry::unregisterStat(&d_numSharedArrayVarSplits);
- StatisticsRegistry::unregisterStat(&d_numGetModelValSplits);
- StatisticsRegistry::unregisterStat(&d_numGetModelValConflicts);
- StatisticsRegistry::unregisterStat(&d_numSetModelValSplits);
- StatisticsRegistry::unregisterStat(&d_numSetModelValConflicts);
+ 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);
}
void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 98cba0420..f1b02d99e 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -22,10 +22,10 @@
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdqueue.h"
-#include "expr/statistics_registry.h"
#include "theory/arrays/array_info.h"
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace theory {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback