diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 6a023c282..28d994835 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -257,6 +257,15 @@ class TheoryArrays : public Theory { private: + TNode weakEquivGetRep(TNode node); + TNode weakEquivGetRepIndex(TNode node, TNode index); + void visitAllLeaves(TNode reason, std::vector<TNode>& conjunctions); + void weakEquivBuildCond(TNode node, TNode index, std::vector<TNode>& conjunctions); + void weakEquivMakeRep(TNode node); + void weakEquivMakeRepIndex(TNode node); + void weakEquivAddSecondary(TNode index, TNode arrayFrom, TNode arrayTo, TNode reason); + void checkWeakEquiv(bool arraysMerged); + // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module class NotifyClass : public eq::EqualityEngineNotify { TheoryArrays& d_arrays; @@ -394,6 +403,12 @@ class TheoryArrays : public Theory { typedef context::CDHashMap<Node,Node,NodeHashFunction> DefValMap; DefValMap d_defValues; + typedef std::hash_map<std::pair<TNode, TNode>, CTNodeList*, TNodePairHashFunction> ReadBucketMap; + ReadBucketMap d_readBucketTable; + context::Context* d_readTableContext; + context::CDList<Node> d_arrayMerges; + std::vector<CTNodeList*> d_readBucketAllocations; + Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); @@ -411,17 +426,6 @@ class TheoryArrays : public Theory { std::vector<Node> d_decisions; bool d_inCheckModel; int d_topLevel; - void convertNodeToAssumptions(TNode node, std::vector<TNode>& assumptions, TNode nodeSkip); - void preRegisterStores(TNode s); - void checkModel(Effort e); - bool hasLoop(TNode node, TNode target); - typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; - NodeMap d_getModelValCache; - NodeMap d_lastVal; - Node getModelVal(TNode node); - Node getModelValRec(TNode node); - bool setModelVal(TNode node, TNode val, bool invert, - bool explain, std::vector<TNode>& assumptions); public: |