Base class for global clause sharing strategies across MPI processes. More...

#include <GlobalSharingStrategy.hpp>

Inheritance diagram for GlobalSharingStrategy:

Collaboration diagram for GlobalSharingStrategy:

Public Member Functions
	GlobalSharingStrategy (const std::shared_ptr< ClauseDatabase > &clauseDB, const std::vector< std::shared_ptr< SharingEntity > > &producers={}, const std::vector< std::shared_ptr< SharingEntity > > &consumers={})
	Constructor for GlobalSharingStrategy.

virtual	~GlobalSharingStrategy ()
	Destructor.

bool	importClause (const ClauseExchangePtr &cls) override
	Imports a clause into the clause database.

void	importClauses (const std::vector< ClauseExchangePtr > &v_cls) override
	Imports multiple clauses into the clause database.

bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client)
	Exports a clause to a specific client.

std::chrono::microseconds	getSleepingTime () override
	Gets the sleeping time for the sharing strategy.

virtual void	joinProcess (int winnerRank, SatResult res, const std::vector< int > &model)
	Handles the process of joining when a solution is found.

void	printStats () override
	Prints the statistics of the sharing strategy.

virtual bool	initMpiVariables ()
	Initializes MPI-related variables.

virtual bool	doSharing () override
	Performs the clause sharing operation.

Public Member Functions inherited from SharingStrategy
	SharingStrategy (const std::vector< std::shared_ptr< SharingEntity > > &producers, const std::vector< std::shared_ptr< SharingEntity > > &consumers, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Constructor for SharingStrategy. Be sure to call connectConstructorProducers after construction, this is due to the base class shared_from_this.

virtual	~SharingStrategy ()
	Virtual destructor.

void	connectConstructorProducers ()
	Add this to the producers' clients list.

virtual void	addProducer (std::shared_ptr< SharingEntity > producer)
	Adds a producer to this strategy.

virtual void	connectProducer (std::shared_ptr< SharingEntity > producer)
	Connect a producer to this strategy. Add (this) to clients of (producer)

virtual void	removeProducer (std::shared_ptr< SharingEntity > producer)
	Removes a producer from this strategy.

Public Member Functions inherited from SharingEntity
	SharingEntity ()
	Construct a new SharingEntity object.

	SharingEntity (const std::vector< std::shared_ptr< SharingEntity > > &clients)
	Construct a new SharingEntity object.

virtual	~SharingEntity ()
	Destroy the SharingEntity object.

int	getSharingId () const
	Get the sharing ID of this entity.

void	setSharingId (int _id)
	Set the sharing ID of this entity.

virtual void	addClient (std::shared_ptr< SharingEntity > client)
	Add a client to this entity.

virtual void	removeClient (std::shared_ptr< SharingEntity > client)
	Remove a specific client from this entity.

size_t	getClientCount () const
	Get the current number of clients.

void	clearClients ()
	Remove all clients.

Protected Attributes
GlobalSharingStatistics	gstats
	Statistics for global sharing.

bool	requests_sent
	Flag indicating if requests to end were sent to the root.

std::vector< MPI_Request >	recv_end_requests
	MPI requests for non-blocking receive of end signals.

MPI_Request	send_end_request
	MPI request for non-root Isend for final synchronization with root.

std::vector< int >	receivedFinalResultRoot
	Buffer for storing results received from other mpi processes.

Protected Attributes inherited from SharingStrategy
std::shared_ptr< ClauseDatabase >	m_clauseDB
	Clause database where exported clauses are stored.

SharingStatistics	stats
	Sharing statistics.

std::vector< std::weak_ptr< SharingEntity > >	m_producers
	The set holding the references to the producers.

std::shared_mutex	m_producersMutex
	Shared mutex for producers list (to become RCU ?)

Protected Attributes inherited from SharingEntity
std::vector< std::weak_ptr< SharingEntity > >	m_clients
	List of weak pointers to client SharingEntities.

std::shared_mutex	m_clientsMutex
	Mutex to protect access to m_clients.

Additional Inherited Members
Protected Member Functions inherited from SharingStrategy
bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client) override
	A SharingStrategy doesn't send a clause to the source client (->from must store the sharingId of its producer)

Protected Member Functions inherited from SharingEntity
bool	exportClause (const ClauseExchangePtr &clause)
	Export a clause to all registered clients.

void	exportClauses (const std::vector< ClauseExchangePtr > &clauses)
	Export multiple clauses to all registered clients.

Detailed Description

Base class for global clause sharing strategies across MPI processes.

This class provides the interface and common functionality for implementing various inter-MPI process clause sharing strategies.

Constructor & Destructor Documentation

◆ GlobalSharingStrategy()

GlobalSharingStrategy::GlobalSharingStrategy	(	const std::shared_ptr< ClauseDatabase > &	clauseDB,
		const std::vector< std::shared_ptr< SharingEntity > > &	producers = {},
		const std::vector< std::shared_ptr< SharingEntity > > &	consumers = {} )

Constructor for GlobalSharingStrategy.

Parameters

clauseDB	Shared pointer to the clause database.
producers	Vector of sharing entities that produce clauses.
consumers	Vector of sharing entities that consume clauses.

Member Function Documentation

◆ doSharing()

virtual bool GlobalSharingStrategy::doSharing ( )

overridevirtual

Performs the clause sharing operation.

Returns: True if sharing is complete and the process can terminate, false otherwise.

Warning: Winner's rank must be smaller 2^16 - 1. See the end of doSharing

Implements SharingStrategy.

Reimplemented in AllGatherSharing, GenericGlobalSharing, and MallobSharing.

◆ exportClauseToClient()

bool GlobalSharingStrategy::exportClauseToClient	(	const ClauseExchangePtr &	clause,
		std::shared_ptr< SharingEntity >	client )

inlinevirtual

Exports a clause to a specific client.

Parameters

clause	Pointer to the clause to be exported.
client	Shared pointer to the client receiving the clause.

Returns: True if the clause was successfully exported, false otherwise.

Reimplemented from SharingEntity.

Reimplemented in MallobSharing.

◆ getSleepingTime()

std::chrono::microseconds GlobalSharingStrategy::getSleepingTime ( )

overridevirtual

Gets the sleeping time for the sharing strategy.

Returns: The sleeping time in microseconds.

Reimplemented from SharingStrategy.

Reimplemented in MallobSharing.

◆ importClause()

bool GlobalSharingStrategy::importClause ( const ClauseExchangePtr & cls )

inlineoverridevirtual

Imports a clause into the clause database.

Parameters

cls	Pointer to the clause to be imported.

Returns: True if the clause was successfully imported, false otherwise.

Implements SharingEntity.

Reimplemented in MallobSharing.

◆ importClauses()

void GlobalSharingStrategy::importClauses ( const std::vector< ClauseExchangePtr > & v_cls )

inlineoverridevirtual

Imports multiple clauses into the clause database.

Parameters

v_cls Vector of clauses to be imported.

Implements SharingEntity.

◆ initMpiVariables()

virtual bool GlobalSharingStrategy::initMpiVariables ( )

virtual

Initializes MPI-related variables.

Returns: True if initialization was successful, false otherwise.

Warning: Be careful to call this only once per instance.

Reimplemented in AllGatherSharing, GenericGlobalSharing, and MallobSharing.

◆ joinProcess()

virtual void GlobalSharingStrategy::joinProcess	(	int	winnerRank,
		SatResult	res,
		const std::vector< int > &	model )

virtual

Handles the process of joining when a solution is found.

Parameters

winnerRank	The rank of the process that found the solution.
res	The result of the SAT solving process.
model	The satisfying assignment, if any.

Reimplemented in AllGatherSharing, GenericGlobalSharing, and MallobSharing.

◆ printStats()

void GlobalSharingStrategy::printStats ( )

overridevirtual

Prints the statistics of the sharing strategy.

Reimplemented from SharingStrategy.

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

/github/workspace/src/sharing/GlobalStrategies/GlobalSharingStrategy.hpp

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ GlobalSharingStrategy()

Member Function Documentation

◆ doSharing()

◆ exportClauseToClient()

◆ getSleepingTime()

◆ importClause()

◆ importClauses()

◆ initMpiVariables()

◆ joinProcess()

◆ printStats()