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 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; |