From b196bd4a9cfc4ae9d582fc3d17c15094287bb36f Mon Sep 17 00:00:00 2001
From: Frank Busse <bb0xfb@gmail.com>
Date: Wed, 7 Oct 2020 17:46:13 +0100
Subject: Searcher: remove addState/removeState functions

---
 lib/Core/Searcher.cpp |  2 +-
 lib/Core/Searcher.h   | 20 +++++---------------
 2 files changed, 6 insertions(+), 16 deletions(-)

(limited to 'lib')

diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index e2f11a87..f8fd2aea 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -420,7 +420,7 @@ void IterativeDeepeningTimeSearcher::update(
           removedStates.end() &&
       elapsed > time) {
     pausedStates.insert(current);
-    baseSearcher->removeState(current);
+    baseSearcher->update(nullptr, {}, {current});
   }
 
   // no states left in underlying searcher: fill with paused states
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 9243b69a..e7f146e0 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -62,16 +62,6 @@ namespace klee {
       os << "<unnamed searcher>\n";
     }
 
-    // utility functions
-
-    void addState(ExecutionState *es, ExecutionState *current = nullptr) {
-      update(current, {es}, std::vector<ExecutionState *>());
-    }
-
-    void removeState(ExecutionState *es, ExecutionState *current = nullptr) {
-      update(current, std::vector<ExecutionState *>(), {es});
-    }
-
     enum CoreSearchType : std::uint8_t {
       DFS,
       BFS,
@@ -259,18 +249,18 @@ namespace klee {
     /// Remove state from the searcher chain, while keeping it in the executor.
     /// This is used here to 'freeze' a state while it is waiting for other
     /// states in its merge group to reach the same instruction.
-    void pauseState(ExecutionState &state){
+    void pauseState(ExecutionState &state) {
       assert(std::find(pausedStates.begin(), pausedStates.end(), &state) == pausedStates.end());
       pausedStates.push_back(&state);
-      baseSearcher->removeState(&state);
+      baseSearcher->update(nullptr, {}, {&state});
     }
 
     /// Continue a paused state
-    void continueState(ExecutionState &state){
+    void continueState(ExecutionState &state) {
       auto it = std::find(pausedStates.begin(), pausedStates.end(), &state);
-      assert( it != pausedStates.end());
+      assert(it != pausedStates.end());
       pausedStates.erase(it);
-      baseSearcher->addState(&state);
+      baseSearcher->update(nullptr, {&state}, {});
     }
 
     ExecutionState &selectState() override;
-- 
cgit 1.4.1