From f3ff3b06318cae93db4d682e6451ddbca4760328 Mon Sep 17 00:00:00 2001
From: Martin Nowack <martin@se.inf.tu-dresden.de>
Date: Tue, 22 Mar 2016 16:39:28 +0100
Subject: Use vector instead of set to add/remove states

Deterministic adding/removing of states.
---
 lib/Core/Searcher.h | 56 ++++++++++++++++++++++++++---------------------------
 1 file changed, 28 insertions(+), 28 deletions(-)

(limited to 'lib/Core/Searcher.h')

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 "
-- 
cgit 1.4.1