diff options
| author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-22 16:39:28 +0100 |
|---|---|---|
| committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-07-08 21:56:28 +0200 |
| commit | f3ff3b06318cae93db4d682e6451ddbca4760328 (patch) | |
| tree | b984df4d0ab09629ef423831f542ff746ff8e34c /lib/Core/Searcher.h | |
| parent | 07632e75e21e3c61f1ab46f76618cb1b807bd6c3 (diff) | |
| download | klee-f3ff3b06318cae93db4d682e6451ddbca4760328.tar.gz | |
Use vector instead of set to add/remove states
Deterministic adding/removing of states.
Diffstat (limited to 'lib/Core/Searcher.h')
| -rw-r--r-- | lib/Core/Searcher.h | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index d866f521..4ede3640 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -35,8 +35,8 @@ namespace klee { virtual ExecutionState &selectState() = 0; virtual void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates) = 0; + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates) = 0; virtual bool empty() = 0; @@ -55,15 +55,15 @@ namespace klee { // utility functions void addState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, tmp, std::set<ExecutionState*>()); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, tmp, std::vector<ExecutionState *>()); } void removeState(ExecutionState *es, ExecutionState *current = 0) { - std::set<ExecutionState*> tmp; - tmp.insert(es); - update(current, std::set<ExecutionState*>(), tmp); + std::vector<ExecutionState *> tmp; + tmp.push_back(es); + update(current, std::vector<ExecutionState *>(), tmp); } enum CoreSearchType { @@ -86,8 +86,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "DFSSearcher\n"; @@ -100,8 +100,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "BFSSearcher\n"; @@ -114,8 +114,8 @@ namespace klee { public: ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return states.empty(); } void printName(llvm::raw_ostream &os) { os << "RandomSearcher\n"; @@ -146,8 +146,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "WeightedRandomSearcher::"; @@ -172,8 +172,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty(); void printName(llvm::raw_ostream &os) { os << "RandomPathSearcher\n"; @@ -195,8 +195,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "MergingSearcher\n"; @@ -218,8 +218,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && statesAtMerge.empty(); } void printName(llvm::raw_ostream &os) { os << "BumpMergingSearcher\n"; @@ -243,8 +243,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty(); } void printName(llvm::raw_ostream &os) { os << "<BatchingSearcher> timeBudget: " << timeBudget @@ -266,8 +266,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return baseSearcher->empty() && pausedStates.empty(); } void printName(llvm::raw_ostream &os) { os << "IterativeDeepeningTimeSearcher\n"; @@ -286,8 +286,8 @@ namespace klee { ExecutionState &selectState(); void update(ExecutionState *current, - const std::set<ExecutionState*> &addedStates, - const std::set<ExecutionState*> &removedStates); + const std::vector<ExecutionState *> &addedStates, + const std::vector<ExecutionState *> &removedStates); bool empty() { return searchers[0]->empty(); } void printName(llvm::raw_ostream &os) { os << "<InterleavedSearcher> containing " |