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/theory_arrays.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/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: |