diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2015-12-26 19:20:27 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2015-12-26 19:20:27 -0800 |
commit | 815f2c96856e96e977b725254b65d68fc0323947 (patch) | |
tree | 1d11fc7b9da181ca4a5c7d92b6e53ba549f1de3e /src/theory/arrays/array_info.h | |
parent | 36eb9ee46b9fa3d4b14c943bc2f434663a2844ef (diff) |
Merged my changes from experimental branch (new array decision procedure,
translation to bit-vectors for QF_NIA).
Diffstat (limited to 'src/theory/arrays/array_info.h')
-rw-r--r-- | src/theory/arrays/array_info.h | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index d9f77d50f..f14788ed5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -66,11 +66,23 @@ public: context::CDO<bool> rIntro1Applied; context::CDO<TNode> modelRep; context::CDO<TNode> constArr; + context::CDO<TNode> weakEquivPointer; + context::CDO<TNode> weakEquivIndex; + context::CDO<TNode> weakEquivSecondary; + context::CDO<TNode> weakEquivSecondaryReason; CTNodeList* indices; CTNodeList* stores; CTNodeList* in_stores; - Info(context::Context* c, Backtracker<TNode>* bck) : isNonLinear(c, false), rIntro1Applied(c, false), modelRep(c,TNode()), constArr(c,TNode()) { + Info(context::Context* c, Backtracker<TNode>* bck) + : isNonLinear(c, false), + rIntro1Applied(c, false), + modelRep(c,TNode()), + constArr(c,TNode()), + weakEquivPointer(c,TNode()), + weakEquivIndex(c,TNode()), + weakEquivSecondary(c,TNode()), + weakEquivSecondaryReason(c,TNode()) { indices = new(true)CTNodeList(c); stores = new(true)CTNodeList(c); in_stores = new(true)CTNodeList(c); @@ -213,6 +225,10 @@ public: void setModelRep(const TNode a, const TNode rep); void setConstArr(const TNode a, const TNode constArr); + void setWeakEquivPointer(const TNode a, const TNode pointer); + void setWeakEquivIndex(const TNode a, const TNode index); + void setWeakEquivSecondary(const TNode a, const TNode secondary); + void setWeakEquivSecondaryReason(const TNode a, const TNode reason); /** * Returns the information associated with TNode a */ @@ -226,6 +242,10 @@ public: const TNode getModelRep(const TNode a) const; const TNode getConstArr(const TNode a) const; + const TNode getWeakEquivPointer(const TNode a) const; + const TNode getWeakEquivIndex(const TNode a) const; + const TNode getWeakEquivSecondary(const TNode a) const; + const TNode getWeakEquivSecondaryReason(const TNode a) const; const CTNodeList* getIndices(const TNode a) const; |