diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
| commit | 56013a80a76b0d46f6f8497d7570e51877dbf99d (patch) | |
| tree | 9d4ed01590a15b13b91485333fd497e26889e0c0 /src/theory/arrays/theory_arrays.h | |
| parent | b273e586629c5759dc88cd962e52a89f65b674a7 (diff) | |
bug fixes to models, array rewriter with previously failing testcases
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a47c8440e..9bf1201f3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -218,12 +218,12 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: - /** Helper functions for collectModelInfo */ - void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache); - void collectArrays(TNode n, std::set<Node>& arraySet, std::set<Node>& cache); + /** Helper function for collectModelInfo */ + void collectTerms(TNode n, std::set<Node>& termSet); + public: - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo(TheoryModel* m, bool fullModel); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -337,7 +337,7 @@ class TheoryArrays : public Theory { context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther; context::CDO<bool> d_sharedTerms; context::CDList<TNode> d_reads; - context::CDList<TNode> d_readsInternal; + context::CDHashSet<TNode, TNodeHashFunction> d_readsInternal; std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache; // The decision requests we have for the core |