New model-based array procedure

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 13fae2ae5..10c15fd0e 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -63,11 +63,12 @@ class Info {
 public:
   context::CDO<bool> isNonLinear;
   context::CDO<bool> rIntro1Applied;
+  context::CDO<TNode> modelRep;
   CTNodeList* indices;
   CTNodeList* stores;
   CTNodeList* in_stores;
 
-  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false) {
+  Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) {
     indices = new(true)CTNodeList(c);
     stores = new(true)CTNodeList(c);
     in_stores = new(true)CTNodeList(c);
@@ -209,6 +210,7 @@ public:
 
   void setNonLinear(const TNode a);
   void setRIntro1Applied(const TNode a);
+  void setModelRep(const TNode a, const TNode rep);
 
   /**
    * Returns the information associated with TNode a
@@ -220,6 +222,8 @@ public:
 
   const bool rIntro1Applied(const TNode a) const;
 
+  const TNode getModelRep(const TNode a) const;
+
   const CTNodeList* getIndices(const TNode a) const;
 
   const CTNodeList* getStores(const TNode a) const;