Merge from arrays2 branch.

1 files changed, 272 insertions, 0 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
new file mode 100644
index 000000000..c795de0b9
--- /dev/null
+++ b/src/theory/arrays/array_info.cpp
@@ -0,0 +1,272 @@
+/*********************                                                        */
+/*! \file array_info.cpp
+ ** \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 "array_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+bool inList(const CTNodeList* l, const TNode el) {
+  CTNodeList::const_iterator it = l->begin();
+  for ( ; it!= l->end(); it ++) {
+    if(*it == el)
+      return true;
+  }
+  return false;
+}
+
+void printList (CTNodeList* list) {
+  CTNodeList::const_iterator it = list->begin();
+  Debug("arrays-info")<<"   [ ";
+  for(; it != list->end(); it++ ) {
+    Debug("arrays-info")<<(*it)<<" ";
+  }
+  Debug("arrays-info")<<"] \n";
+}
+
+void printList (List<TNode>* list) {
+  List<TNode>::const_iterator it = list->begin();
+  Debug("arrays-info")<<"   [ ";
+  for(; it != list->end(); it++ ) {
+    Debug("arrays-info")<<(*it)<<" ";
+  }
+  Debug("arrays-info")<<"] \n";
+}
+
+void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
+  std::set<TNode> temp;
+  CTNodeList::const_iterator it;
+  for(it = la->begin() ; it != la->end(); it++ ) {
+    temp.insert((*it));
+  }
+
+  for(it = lb->begin() ; it!= lb->end(); it++ ) {
+    if(temp.count(*it) == 0) {
+      la->push_back(*it);
+    }
+  }
+}
+
+void ArrayInfo::addIndex(const Node a, const TNode i) {
+  Assert(a.getType().isArray());
+  Assert(!i.getType().isArray()); // temporary for flat arrays
+  Debug("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
+  List<TNode>* temp_indices;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_indices = new List<TNode>(bck);
+    temp_indices->append(i);
+
+    temp_info = new Info(ct, bck);
+    temp_info->indices = temp_indices;
+
+    info_map[a] = temp_info;
+  } else {
+    temp_indices = (*it).second->indices;
+    temp_indices->append(i);
+  }
+  if(Debug.isOn("arrays-ind")) {
+    printList((*(info_map.find(a))).second->indices);
+  }
+
+}
+
+void ArrayInfo::addStore(const Node a, const TNode st){
+  Assert(a.getType().isArray());
+  Assert(st.getKind()== kind::STORE); // temporary for flat arrays
+
+  CTNodeList* temp_store;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_store = new(true) CTNodeList(ct);
+    temp_store->push_back(st);
+
+    temp_info = new Info(ct, bck);
+    temp_info->stores = temp_store;
+    info_map[a]=temp_info;
+  } else {
+    temp_store = (*it).second->stores;
+    if(! inList(temp_store, st)) {
+      temp_store->push_back(st);
+    }
+  }
+};
+
+
+void ArrayInfo::addInStore(const TNode a, const TNode b){
+  Debug("arrays-addinstore")<<"Arrays::addInStore "<<a<<" ~ "<<b<<"\n";
+  Assert(a.getType().isArray());
+  Assert(b.getType().isArray());
+
+  CTNodeList* temp_inst;
+  Info* temp_info;
+
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_inst = new(true) CTNodeList(ct);
+    temp_inst->push_back(b);
+
+    temp_info = new Info(ct, bck);
+    temp_info->in_stores = temp_inst;
+    info_map[a] = temp_info;
+  } else {
+    temp_inst = (*it).second->in_stores;
+    if(! inList(temp_inst, b)) {
+      temp_inst->push_back(b);
+    }
+  }
+};
+
+
+
+/**
+ * Returns the information associated with TNode a
+ */
+
+const Info* ArrayInfo::getInfo(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end())
+      return (*it).second;
+  return emptyInfo;
+}
+
+List<TNode>* ArrayInfo::getIndices(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->indices;
+  }
+  return emptyListI;
+}
+
+const CTNodeList* ArrayInfo::getStores(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->stores;
+  }
+  return emptyList;
+}
+
+const CTNodeList* ArrayInfo::getInStores(const TNode a) const{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+  if(it!= info_map.end()) {
+    return (*it).second->in_stores;
+  }
+  return emptyList;
+}
+
+
+void ArrayInfo::mergeInfo(const TNode a, const TNode b){
+  // can't have assertion that find(b) = a !
+  TimerStat::CodeTimer codeTimer(d_mergeInfoTimer);
+  ++d_callsMergeInfo;
+
+  Debug("arrays-mergei")<<"Arrays::mergeInfo merging "<<a<<"\n";
+  Debug("arrays-mergei")<<"                      and "<<b<<"\n";
+
+  CNodeInfoMap::iterator ita = info_map.find(a);
+  CNodeInfoMap::iterator itb = info_map.find(b);
+
+  if(ita != info_map.end()) {
+    Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<a<<"\n";
+    if(Debug.isOn("arrays-mergei"))
+      (*ita).second->print();
+
+    if(itb != info_map.end()) {
+      Debug("arrays-mergei")<<"Arrays::mergeInfo info "<<b<<"\n";
+      if(Debug.isOn("arrays-mergei"))
+        (*itb).second->print();
+
+      List<TNode>* lista_i = (*ita).second->indices;
+      CTNodeList* lista_st = (*ita).second->stores;
+      CTNodeList* lista_inst = (*ita).second->in_stores;
+
+
+      List<TNode>* listb_i = (*itb).second->indices;
+      CTNodeList* listb_st = (*itb).second->stores;
+      CTNodeList* listb_inst = (*itb).second->in_stores;
+
+      lista_i->concat(listb_i);
+      mergeLists(lista_st, listb_st);
+      mergeLists(lista_inst, listb_inst);
+
+      /* sketchy stats */
+
+      //FIXME
+      int s = 0;//lista_i->size();
+      d_maxList.maxAssign(s);
+
+
+      if(s!= 0) {
+        d_avgIndexListLength.addEntry(s);
+        ++d_listsCount;
+      }
+      s = lista_st->size();
+      d_maxList.maxAssign(s);
+      if(s!= 0) {
+        d_avgStoresListLength.addEntry(s);
+        ++d_listsCount;
+      }
+
+      s = lista_inst->size();
+      d_maxList.maxAssign(s);
+      if(s!=0) {
+        d_avgInStoresListLength.addEntry(s);
+        ++d_listsCount;
+      }
+
+      /* end sketchy stats */
+
+    }
+
+  } else {
+    Debug("arrays-mergei")<<" First element has no info \n";
+    if(itb != info_map.end()) {
+      Debug("arrays-mergei")<<" adding second element's info \n";
+      (*itb).second->print();
+
+      List<TNode>* listb_i = (*itb).second->indices;
+      CTNodeList* listb_st = (*itb).second->stores;
+      CTNodeList* listb_inst = (*itb).second->in_stores;
+
+      Info* temp_info = new Info(ct, bck);
+
+      (temp_info->indices)->concat(listb_i);
+      mergeLists(temp_info->stores, listb_st);
+      mergeLists(temp_info->in_stores, listb_inst);
+      info_map[a] = temp_info;
+
+    } else {
+    Debug("arrays-mergei")<<" Second element has no info \n";
+    }
+
+   }
+  Debug("arrays-mergei")<<"Arrays::mergeInfo done \n";
+
+}
+
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */