klee::IterativeDeepeningTimeSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::IterativeDeepeningTimeSearcher:

Collaboration diagram for klee::IterativeDeepeningTimeSearcher:

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...
Public Member Functions inherited from klee::Searcher
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
Public Types inherited from klee::Searcher
enum	CoreSearchType : std::uint8_t {   DFS , BFS , RandomState , RandomPath ,   NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP ,   NURS_ICnt , NURS_CPICnt , NURS_QC }

Detailed Description

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.

Constructor & Destructor Documentation

IterativeDeepeningTimeSearcher()

IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher ( Searcher *  baseSearcher )

explicit

Parameters

baseSearcher

The underlying searcher (takes ownership).

Definition at line 465 of file Searcher.cpp.

~IterativeDeepeningTimeSearcher()

klee::IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher ( )

overridedefault

Member Function Documentation

empty()

bool IterativeDeepeningTimeSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 513 of file Searcher.cpp.

References baseSearcher, and pausedStates.

printName()

void IterativeDeepeningTimeSearcher::printName ( llvm::raw_ostream &  os )

overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 517 of file Searcher.cpp.

selectState()

ExecutionState & IterativeDeepeningTimeSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

Implements klee::Searcher.

Definition at line 468 of file Searcher.cpp.

References baseSearcher, klee::time::getWallTime(), and startTime.

Here is the call graph for this function:

update()

void IterativeDeepeningTimeSearcher::update ( ExecutionState *  current, const std::vector< ExecutionState * > &  addedStates, const std::vector< ExecutionState * > &  removedStates  )

overridevirtual

Notifies searcher about new or deleted states.

Parameters

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().

Here is the call graph for this function:

Member Data Documentation

baseSearcher

std::unique_ptr<Searcher> klee::IterativeDeepeningTimeSearcher::baseSearcher

private

Definition at line 274 of file Searcher.h.

Referenced by empty(), selectState(), and update().

pausedStates

std::set<ExecutionState*> klee::IterativeDeepeningTimeSearcher::pausedStates

private

Definition at line 277 of file Searcher.h.

Referenced by empty(), and update().

startTime

time::Point klee::IterativeDeepeningTimeSearcher::startTime

private

Definition at line 275 of file Searcher.h.

Referenced by selectState(), and update().

time

time::Span klee::IterativeDeepeningTimeSearcher::time {time::seconds(1)}

private

Definition at line 276 of file Searcher.h.

Referenced by update().

---

The documentation for this class was generated from the following files:

• /Users/cristic/klee/lib/Core/Searcher.h
• /Users/cristic/klee/lib/Core/Searcher.cpp