diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-26 20:12:47 -0400 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-03-27 20:34:30 -0400 |
commit | d45b7e9594003f1d17bd5d512e6eeb68b70f6a53 (patch) | |
tree | 708effbf9205079774d7cc4e8ef48053e96fcfa1 /src/theory/arrays/array_info.h | |
parent | 2d091366f7d437c3839307b1ad732a6999333fe0 (diff) |
New model-based array procedure
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; |