diff options
Diffstat (limited to 'src/theory/arrays/array_info.h')
| -rw-r--r-- | src/theory/arrays/array_info.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 09230bba7..f3c6385e5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -64,11 +64,12 @@ public: context::CDO<bool> isNonLinear; context::CDO<bool> rIntro1Applied; context::CDO<TNode> modelRep; + context::CDO<TNode> constArr; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()) { + Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -210,6 +211,7 @@ public: void setRIntro1Applied(const TNode a); void setModelRep(const TNode a, const TNode rep); + void setConstArr(const TNode a, const TNode constArr); /** * Returns the information associated with TNode a */ @@ -222,6 +224,8 @@ public: const TNode getModelRep(const TNode a) const; + const TNode getConstArr(const TNode a) const; + const CTNodeList* getIndices(const TNode a) const; const CTNodeList* getStores(const TNode a) const; |