SymStateMarked Class Reference

Extension of SymStateWithJoin, which distinguishes among already processed symbolic heaps and symbolic heaps scheduled for processing. More...

#include <symstate.hh>

Inheritance diagram for SymStateMarked:

Collaboration diagram for SymStateMarked:

Public Types
typedef TList::const_iterator	const_iterator
typedef TList::iterator	iterator

Public Member Functions
	SymStateMarked ()
SymStateMarked &	operator= (const SymState &huni)
	import of SymState rewrites the base and invalidates all flags
virtual void	clear ()
virtual void	swap (SymState &)
int	cntPending () const
	return count of heaps pending for execution
bool	isDone (int nth) const
	check if the nth symbolic heap has been already processed
void	setDone (int nth)
	mark the nth symbolic heap as processed
virtual bool	insert (const SymHeap &sh, bool allowThreeWay=true)
	insert given SymHeap object into the state
virtual int	lookup (const SymHeap &sh) const
	look for the given symbolic heap, return its index if found, -1 otherwise
size_t	size () const
	return count of object stored in the container
const SymHeap &	operator[] (int nth) const
	return nth SymHeap object, 0 <= nth < size()
const_iterator	begin () const
	return STL-like iterator to go through the container
iterator	begin ()
	return STL-like iterator to go through the container
const_iterator	end () const
	return STL-like iterator to go through the container
iterator	end ()
	return STL-like iterator to go through the container

Protected Member Functions
virtual void	insertNew (const SymHeap &sh)
	insert new SymHeap that @ must be guaranteed to be not yet in
virtual void	eraseExisting (int nth)
virtual void	swapExisting (int nth, SymHeap &sh)
virtual void	rotateExisting (int idxA, int idxB)
void	updateTraceOf (int idx, Trace::Node *tr, EJoinStatus status)

Private Types
typedef std::vector< bool >	TDone

Private Attributes
TDone	done_
int	cntPending_

Friends
class	SymStateMap

Detailed Description

Extension of SymStateWithJoin, which distinguishes among already processed symbolic heaps and symbolic heaps scheduled for processing.

Newly inserted symbolic heaps are always marked as scheduled. They can be marked as done later, using the setDone() method.

Definition at line 163 of file symstate.hh.

Member Typedef Documentation

typedef TList::const_iterator const_iterator

inherited

Definition at line 43 of file symstate.hh.

typedef TList::iterator iterator

inherited

Definition at line 44 of file symstate.hh.

typedef std::vector<bool> TDone

private

Definition at line 242 of file symstate.hh.

Constructor & Destructor Documentation

SymStateMarked ( )

inline

Definition at line 165 of file symstate.hh.

Member Function Documentation

const_iterator begin ( ) const

inlineinherited

return STL-like iterator to go through the container

Definition at line 77 of file symstate.hh.

References SymState::heaps_.

iterator begin ( )

inlineinherited

return STL-like iterator to go through the container

Definition at line 83 of file symstate.hh.

References SymState::heaps_.

virtual void clear ( )

inlinevirtual

Reimplemented from SymState.

Definition at line 179 of file symstate.hh.

References cntPending_, and done_.

int cntPending ( ) const

inline

return count of heaps pending for execution

Definition at line 189 of file symstate.hh.

References cntPending_.

const_iterator end ( ) const

inlineinherited

return STL-like iterator to go through the container

Definition at line 80 of file symstate.hh.

References SymState::heaps_.

iterator end ( )

inlineinherited

return STL-like iterator to go through the container

Definition at line 86 of file symstate.hh.

References SymState::heaps_.

virtual void eraseExisting ( int  nth )

inlineprotectedvirtual

Reimplemented from SymState.

Definition at line 202 of file symstate.hh.

References cntPending_, and done_.

virtual bool insert ( const SymHeap &  sh, bool  allowThreeWay = true  )

virtualinherited

insert given SymHeap object into the state

Reimplemented from SymState.

virtual void insertNew ( const SymHeap &  sh )

inlineprotectedvirtual

insert new SymHeap that @ must be guaranteed to be not yet in

Reimplemented from SymState.

Definition at line 194 of file symstate.hh.

References cntPending_, and done_.

bool isDone ( int  nth ) const

inline

check if the nth symbolic heap has been already processed

Definition at line 229 of file symstate.hh.

References done_.

virtual int lookup ( const SymHeap &  heap ) const

virtualinherited

look for the given symbolic heap, return its index if found, -1 otherwise

Implements SymState.

SymStateMarked& operator= ( const SymState &  huni )

inline

import of SymState rewrites the base and invalidates all flags

Reimplemented from SymState.

Definition at line 171 of file symstate.hh.

References cntPending_, done_, and SymState::size().

const SymHeap& operator[] ( int  nth ) const

inlineinherited

return nth SymHeap object, 0 <= nth < size()

Definition at line 72 of file symstate.hh.

References SymState::heaps_.

virtual void rotateExisting ( int  idxA, int  idxB  )

protectedvirtual

Reimplemented from SymState.

void setDone ( int  nth )

inline

mark the nth symbolic heap as processed

Definition at line 234 of file symstate.hh.

References cntPending_, and done_.

size_t size ( ) const

inlineinherited

return count of object stored in the container

Definition at line 69 of file symstate.hh.

References SymState::heaps_.

Referenced by operator=().

virtual void swap ( SymState &  )

virtual

Attention

always reinitializes the markers

Reimplemented from SymState.

virtual void swapExisting ( int  nth, SymHeap &  sh  )

inlineprotectedvirtual

Reimplemented from SymState.

Definition at line 211 of file symstate.hh.

References cntPending_, and done_.

void updateTraceOf ( int  idx, Trace::Node *  tr, EJoinStatus  status  )

protectedinherited

Friends And Related Function Documentation

friend class SymStateMap

friend

Definition at line 225 of file symstate.hh.

Field Documentation

int cntPending_

private

Definition at line 245 of file symstate.hh.

Referenced by clear(), cntPending(), eraseExisting(), insertNew(), operator=(), setDone(), and swapExisting().

TDone done_

private

Definition at line 244 of file symstate.hh.

Referenced by clear(), eraseExisting(), insertNew(), isDone(), operator=(), setDone(), and swapExisting().

---

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

• symstate.hh