Added internal support for constant arrays.

1 files changed, 24 insertions, 0 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index dc907ba0b..9b2d3647e 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -181,6 +181,20 @@ void ArrayInfo::setModelRep(const TNode a, const TNode b) {
   
 }
 
+void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
+  Assert(a.getType().isArray());
+  Info* temp_info;
+  CNodeInfoMap::iterator it = info_map.find(a);
+  if(it == info_map.end()) {
+    temp_info = new Info(ct, bck);
+    temp_info->constArr = constArr;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->constArr = constArr;
+  }
+  
+}
+
 /**
  * Returns the information associated with TNode a
  */
@@ -224,6 +238,16 @@ const TNode ArrayInfo::getModelRep(const TNode a) const
   return TNode();
 }
 
+const TNode ArrayInfo::getConstArr(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->constArr;
+  }
+  return TNode();
+}
+
 const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {