Merge branch 'bfs' of https://github.com/antiAgainst/klee into antiAgainst-bfs

1 files changed, 34 insertions, 0 deletions

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index d08cd1b1..778ef0ef 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -88,6 +88,40 @@ void DFSSearcher::update(ExecutionState *current,
 
 ///
 
+ExecutionState &BFSSearcher::selectState() {
+  return *states.front();
+}
+
+void BFSSearcher::update(ExecutionState *current,
+                         const std::set<ExecutionState*> &addedStates,
+                         const std::set<ExecutionState*> &removedStates) {
+  states.insert(states.end(),
+                addedStates.begin(),
+                addedStates.end());
+  for (std::set<ExecutionState*>::const_iterator it = removedStates.begin(),
+         ie = removedStates.end(); it != ie; ++it) {
+    ExecutionState *es = *it;
+    if (es == states.front()) {
+      states.pop_front();
+    } else {
+      bool ok = false;
+
+      for (std::deque<ExecutionState*>::iterator it = states.begin(),
+             ie = states.end(); it != ie; ++it) {
+        if (es==*it) {
+          states.erase(it);
+          ok = true;
+          break;
+        }
+      }
+
+      assert(ok && "invalid state removed");
+    }
+  }
+}
+
+///
+
 ExecutionState &RandomSearcher::selectState() {
   return *states[theRNG.getInt32()%states.size()];
 }