klee
|
#include <Searcher.h>
Public Member Functions | |
IterativeDeepeningTimeSearcher (Searcher *baseSearcher) | |
~IterativeDeepeningTimeSearcher () override=default | |
ExecutionState & | selectState () override |
void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override |
bool | empty () override |
void | printName (llvm::raw_ostream &os) override |
Prints name of searcher as a klee_message() . More... | |
![]() | |
virtual | ~Searcher ()=default |
virtual ExecutionState & | selectState ()=0 |
virtual void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates)=0 |
virtual bool | empty ()=0 |
virtual void | printName (llvm::raw_ostream &os)=0 |
Prints name of searcher as a klee_message() . More... | |
Private Attributes | |
std::unique_ptr< Searcher > | baseSearcher |
time::Point | startTime |
time::Span | time {time::seconds(1)} |
std::set< ExecutionState * > | pausedStates |
Additional Inherited Members | |
![]() | |
enum | CoreSearchType : std::uint8_t { DFS , BFS , RandomState , RandomPath , NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP , NURS_ICnt , NURS_CPICnt , NURS_QC } |
IterativeDeepeningTimeSearcher implements time-based deepening. States are selected from an underlying searcher. When a state reaches its time limit it is paused (removed from underlying searcher). When the underlying searcher runs out of states, the time budget is increased and all paused states are revived (added to underlying searcher).
Definition at line 273 of file Searcher.h.
|
explicit |
baseSearcher | The underlying searcher (takes ownership). |
Definition at line 465 of file Searcher.cpp.
|
overridedefault |
|
overridevirtual |
Implements klee::Searcher.
Definition at line 513 of file Searcher.cpp.
References baseSearcher, and pausedStates.
|
overridevirtual |
Prints name of searcher as a klee_message()
.
Implements klee::Searcher.
Definition at line 517 of file Searcher.cpp.
|
overridevirtual |
Selects a state for further exploration.
Implements klee::Searcher.
Definition at line 468 of file Searcher.cpp.
References baseSearcher, klee::time::getWallTime(), and startTime.
|
overridevirtual |
Notifies searcher about new or deleted states.
current | The currently selected state for exploration. |
addedStates | The newly branched states with current as common ancestor. |
removedStates | The states that will be terminated. |
Implements klee::Searcher.
Definition at line 474 of file Searcher.cpp.
References baseSearcher, klee::time::getWallTime(), klee::klee_message(), pausedStates, startTime, time, and klee::time::Span::toSeconds().
|
private |
Definition at line 274 of file Searcher.h.
Referenced by empty(), selectState(), and update().
|
private |
Definition at line 277 of file Searcher.h.
|
private |
Definition at line 275 of file Searcher.h.
Referenced by selectState(), and update().
|
private |
Definition at line 276 of file Searcher.h.
Referenced by update().