diff options
Diffstat (limited to 'src/theory/arrays/array_info.h')
-rw-r--r-- | src/theory/arrays/array_info.h | 239 |
1 files changed, 239 insertions, 0 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h new file mode 100644 index 000000000..6eb20e30a --- /dev/null +++ b/src/theory/arrays/array_info.h @@ -0,0 +1,239 @@ +/*! \file array_info.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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 + ** + ** + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H +#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H +#include "util/backtrackable.h" +#include "context/cdlist.h" +#include "context/cdmap.h" +#include "expr/node.h" +#include "util/stats.h" +#include "util/ntuple.h" +#include <ext/hash_set> +#include <ext/hash_map> +#include <iostream> +#include <map> + +namespace CVC4 { +namespace theory { +namespace arrays { + +typedef context::CDList<TNode> CTNodeList; + +struct TNodeQuadHashFunction { + size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const { + TNode n1 = q.first; + TNode n2 = q.second; + TNode n3 = q.third; + TNode n4 = q.fourth; + return (size_t) (n1.getId()*0x9e3779b9 + n2.getId()*0x30000059 + + n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF); + + } +};/* struct TNodeQuadHashFunction */ + +void printList (CTNodeList* list); +void printList( List<TNode>* list); + +bool inList(const CTNodeList* l, const TNode el); + +/** + * Small class encapsulating the information + * in the map. It's a class and not a struct to + * call the destructor. + */ + +class Info { +public: + List<TNode>* indices; + CTNodeList* stores; + CTNodeList* in_stores; + + Info(context::Context* c, Backtracker<TNode>* bck) { + indices = new List<TNode>(bck); + stores = new(true)CTNodeList(c); + in_stores = new(true)CTNodeList(c); + + } + + ~Info() { + //FIXME! + //indices->deleteSelf(); + stores->deleteSelf(); + in_stores->deleteSelf(); + } + + /** + * prints the information + */ + void print() const { + Assert(indices != NULL && stores!= NULL); // && equals != NULL); + Debug("arrays-info")<<" indices "; + printList(indices); + Debug("arrays-info")<<" stores "; + printList(stores); + Debug("arrays-info")<<" in_stores "; + printList(in_stores); + } +}; + + +typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap; + +/** + * Class keeping track of the following information for canonical + * representatives of type array [a] : + * indices at which it is being read (all i for which there is a + * term of the form SELECT a i) + * all store terms in the congruence class + * stores in which it appears (terms of the form STORE a _ _ ) + * + */ +class ArrayInfo { +private: + context::Context* ct; + Backtracker<TNode>* bck; + CNodeInfoMap info_map; + + CTNodeList* emptyList; + List<TNode>* emptyListI; + + + /* == STATISTICS == */ + + /** time spent in preregisterTerm() */ + TimerStat d_mergeInfoTimer; + AverageStat d_avgIndexListLength; + AverageStat d_avgStoresListLength; + AverageStat d_avgInStoresListLength; + IntStat d_listsCount; + IntStat d_callsMergeInfo; + IntStat d_maxList; + SizeStat<CNodeInfoMap > d_tableSize; + + /** + * checks if a certain element is in the list l + * FIXME: better way to check for duplicates? + */ + + /** + * helper method that merges two lists into the first + * without adding duplicates + */ + void mergeLists(CTNodeList* la, const CTNodeList* lb) const; + +public: + const Info* emptyInfo; +/* + ArrayInfo(): ct(NULl), info + 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) { + 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): 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); + emptyListI = new List<TNode>(bck); + 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(){ + 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); + }; + + /** + * adds the node a to the map if it does not exist + * and it initializes the info. checks for duplicate i's + */ + void addIndex(const Node a, const TNode i); + void addStore(const Node a, const TNode st); + void addInStore(const TNode a, const TNode st); + + + /** + * Returns the information associated with TNode a + */ + + const Info* getInfo(const TNode a) const; + + List<TNode>* getIndices(const TNode a) const; + + const CTNodeList* getStores(const TNode a) const; + + const CTNodeList* getInStores(const TNode a) const; + + /** + * merges the information of nodes a and b + * the nodes do not have to actually be in the map. + * pre-condition + * a should be the canonical representative of b + */ + void mergeInfo(const TNode a, const TNode b); +}; + + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARRAYS__ARRAY_INFO_H */ |