From 815f2c96856e96e977b725254b65d68fc0323947 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 26 Dec 2015 19:20:27 -0800
Subject: Merged my changes from experimental branch (new array decision
 procedure, translation to bit-vectors for QF_NIA).

---
 src/theory/arrays/array_info.cpp | 93 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 92 insertions(+), 1 deletion(-)

(limited to 'src/theory/arrays/array_info.cpp')

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 9b2d3647e..cd0025fe2 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -192,7 +192,58 @@ void ArrayInfo::setConstArr(const TNode a, const TNode constArr) {
   } else {
     (*it).second->constArr = constArr;
   }
-  
+}
+
+void ArrayInfo::setWeakEquivPointer(const TNode a, const TNode pointer) {
+  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->weakEquivPointer = pointer;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->weakEquivPointer = pointer;
+  }
+}
+
+void ArrayInfo::setWeakEquivIndex(const TNode a, const TNode index) {
+  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->weakEquivIndex = index;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->weakEquivIndex = index;
+  }
+}
+
+void ArrayInfo::setWeakEquivSecondary(const TNode a, const TNode secondary) {
+  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->weakEquivSecondary = secondary;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->weakEquivSecondary = secondary;
+  }
+}
+
+void ArrayInfo::setWeakEquivSecondaryReason(const TNode a, const TNode reason) {
+  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->weakEquivSecondaryReason = reason;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->weakEquivSecondaryReason = reason;
+  }
 }
 
 /**
@@ -248,6 +299,46 @@ const TNode ArrayInfo::getConstArr(const TNode a) const
   return TNode();
 }
 
+const TNode ArrayInfo::getWeakEquivPointer(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->weakEquivPointer;
+  }
+  return TNode();
+}
+
+const TNode ArrayInfo::getWeakEquivIndex(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->weakEquivIndex;
+  }
+  return TNode();
+}
+
+const TNode ArrayInfo::getWeakEquivSecondary(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->weakEquivSecondary;
+  }
+  return TNode();
+}
+
+const TNode ArrayInfo::getWeakEquivSecondaryReason(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end()) {
+    return (*it).second->weakEquivSecondaryReason;
+  }
+  return TNode();
+}
+
 const CTNodeList* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {
-- 
cgit v1.2.3