summaryrefslogtreecommitdiff
path: root/src/theory/arrays/array_info.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/array_info.cpp')
-rw-r--r--src/theory/arrays/array_info.cpp36
1 files changed, 18 insertions, 18 deletions
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 55f013f8c..c63d528a7 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file array_info.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Clark Barrett
- ** Minor contributors (to current version): Dejan Jovanovic
+ ** Top contributors (to current version):
+ ** Morgan Deters, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Contains additional classes to store context dependent information
** for each term of type array
@@ -44,16 +44,16 @@ Info::~Info() {
in_stores->deleteSelf();
}
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b)
+ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
: 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) {
+ 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) {
emptyList = new(true) CTNodeList(ct);
emptyInfo = new Info(ct, bck);
smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
@@ -208,7 +208,7 @@ void ArrayInfo::setNonLinear(const TNode a) {
} else {
(*it).second->isNonLinear = true;
}
-
+
}
void ArrayInfo::setRIntro1Applied(const TNode a) {
@@ -222,7 +222,7 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
} else {
(*it).second->rIntro1Applied = true;
}
-
+
}
void ArrayInfo::setModelRep(const TNode a, const TNode b) {
@@ -236,7 +236,7 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) {
} else {
(*it).second->modelRep = b;
}
-
+
}
void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback