merge from arrays-clark branch

1 files changed, 9 insertions, 4 deletions

diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index d1c435b48..3eae369ca 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -55,9 +55,10 @@ namespace theory {
 namespace arrays {
 
 typedef context::CDList<TNode> CTNodeList;
+typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
 
-struct TNodeQuadHashFunction {
-  size_t operator()(const quad<CVC4::TNode, CVC4::TNode, CVC4::TNode, CVC4::TNode>& q ) const {
+struct RowLemmaTypeHashFunction {
+  size_t operator()(const RowLemmaType& q ) const {
     TNode n1 = q.first;
     TNode n2 = q.second;
     TNode n3 = q.third;
@@ -66,7 +67,7 @@ struct TNodeQuadHashFunction {
         n3.getId()*0x60000005 + n4.getId()*0x07FFFFFF);
 
   }
-};/* struct TNodeQuadHashFunction */
+};/* struct RowLemmaTypeHashFunction */
 
 void printList (CTNodeList* list);
 void printList( List<TNode>* list);
@@ -81,11 +82,12 @@ bool inList(const CTNodeList* l, const TNode el);
 
 class Info {
 public:
+  context::CDO<bool> isNonLinear;
   List<TNode>* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false) {
     indices = new List<TNode>(bck);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -228,6 +230,7 @@ public:
   void addStore(const Node a, const TNode st);
   void addInStore(const TNode a, const TNode st);
 
+  void setNonLinear(const TNode a);
 
   /**
    * Returns the information associated with TNode a
@@ -235,6 +238,8 @@ public:
 
   const Info* getInfo(const TNode a) const;
 
+  const bool isNonLinear(const TNode a) const;
+
   List<TNode>* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;