merge from arrays-clark branch

1 files changed, 23 insertions, 0 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 50ded8758..cd6c38a7f 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -139,6 +139,20 @@ void ArrayInfo::addInStore(const TNode a, const TNode b){
 };
 
 
+void ArrayInfo::setNonLinear(const TNode a) {
+  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->isNonLinear = true;
+    info_map[a] = temp_info;
+  } else {
+    (*it).second->isNonLinear = true;
+  }
+  
+}
+
 
 /**
  * Returns the information associated with TNode a
@@ -152,6 +166,15 @@ const Info* ArrayInfo::getInfo(const TNode a) const{
   return emptyInfo;
 }
 
+const bool ArrayInfo::isNonLinear(const TNode a) const
+{
+  CNodeInfoMap::const_iterator it = info_map.find(a);
+
+  if(it!= info_map.end())
+      return (*it).second->isNonLinear;
+  return false;
+}
+
 List<TNode>* ArrayInfo::getIndices(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
   if(it!= info_map.end()) {