ClauseDatabaseBufferPerEntity Class Reference

A clause database that maintain separate buffers for each entity, mimicing old painless default behavior. More...

#include <ClauseDatabaseBufferPerEntity.hpp>

Inheritance diagram for ClauseDatabaseBufferPerEntity:

Collaboration diagram for ClauseDatabaseBufferPerEntity:

Public Member Functions
	ClauseDatabaseBufferPerEntity ()=delete
	Default constructor deleted to enforce use of parameterized constructor.
	ClauseDatabaseBufferPerEntity (int maxClauseSize)
	Constructor with a specified maximum clause size.
	~ClauseDatabaseBufferPerEntity () override=default
	Virtual destructor.
bool	addClause (ClauseExchangePtr clause) override
	Adds a clause to the appropriate entity's buffer.
size_t	giveSelection (std::vector< ClauseExchangePtr > &selectedCls, unsigned int literalCountLimit) override
	Selects clauses up to a specified total size.
void	getClauses (std::vector< ClauseExchangePtr > &v_cls) override
	Retrieves all clauses from all entity buffers.
bool	getOneClause (ClauseExchangePtr &cls) override
	Retrieves a single clause from any entity buffer.
size_t	getSize () const override
	Gets the total number of clauses across all entity buffers.
void	clearDatabase () override
	Clears all export buffers.
size_t	shrinkDatabase () override
	Does nothing in this implementation.
Public Member Functions inherited from ClauseDatabase
	ClauseDatabase ()
	Default Constructor.
virtual	~ClauseDatabase ()
	Virtual destructor to ensure proper cleanup of derived classes.

Detailed Description

A clause database that maintain separate buffers for each entity, mimicing old painless default behavior.

This class extends ClauseDatabase to provide a mechanism for storing and managing clauses in separate buffers for different entities thanks to the from attributed in ClauseExchange. It uses fine-grained locking to allow concurrent access where possible.

Since ClauseBuffer is lockfree, all consumption operations (read) can be done concurently. The only synchronization required is on the map of buffers

The maximum size parameter is only used at selection, in the temporary ClauseDatabasePerSize instance.

Constructor & Destructor Documentation

ClauseDatabaseBufferPerEntity()

ClauseDatabaseBufferPerEntity::ClauseDatabaseBufferPerEntity ( int maxClauseSize )

explicit

Constructor with a specified maximum clause size.

Parameters

maxClauseSize

The maximum size of clauses to be stored.

Member Function Documentation

addClause()

bool ClauseDatabaseBufferPerEntity::addClause ( ClauseExchangePtr clause )

overridevirtual

Adds a clause to the appropriate entity's buffer.

Parameters

clause

The clause to be added.

Returns

true if the clause was successfully added, false otherwise.

Note

This method is thread-safe and allows concurrent additions to different buffers.

Implements ClauseDatabase.

clearDatabase()

void ClauseDatabaseBufferPerEntity::clearDatabase ( )

overridevirtual

Clears all export buffers.

Note

This method acquires an exclusive lock and cannot be called concurrently with other operations.

Implements ClauseDatabase.

getClauses()

void ClauseDatabaseBufferPerEntity::getClauses ( std::vector< ClauseExchangePtr > & v_cls )

overridevirtual

Retrieves all clauses from all entity buffers.

Parameters

v_cls

Vector to store the retrieved clauses.

Note

This method acquires a shared lock and can be called concurrently with other read operations.

Implements ClauseDatabase.

getOneClause()

bool ClauseDatabaseBufferPerEntity::getOneClause ( ClauseExchangePtr & cls )

overridevirtual

Retrieves a single clause from any entity buffer.

Parameters

cls	Reference to store the retrieved clause.

Returns

true if a clause was retrieved, false if all buffers are empty.

Note

This method acquires a shared lock and can be called concurrently with other read operations.

Implements ClauseDatabase.

getSize()

size_t ClauseDatabaseBufferPerEntity::getSize ( ) const

overridevirtual

Gets the total number of clauses across all entity buffers.

Returns

The total number of clauses.

Note

This method acquires a shared lock and can be called concurrently with other read operations.

Implements ClauseDatabase.

giveSelection()

size_t ClauseDatabaseBufferPerEntity::giveSelection ( std::vector< ClauseExchangePtr > & selectedCls, unsigned int literalCountLimit )

overridevirtual

Selects clauses up to a specified total size.

Parameters

selectedCls	Vector to store the selected clauses.
literalCountLimit	The maximum number of literals to be selected.

Returns

The number of literals in the selected clauses.

Note

This method acquires a shared lock and can be called concurrently with other read operations.

Implements ClauseDatabase.

shrinkDatabase()

size_t ClauseDatabaseBufferPerEntity::shrinkDatabase ( )

inlineoverridevirtual

Does nothing in this implementation.

Returns

The maximum size_t value.

Implements ClauseDatabase.

---

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

• /github/workspace/src/containers/ClauseDatabaseBufferPerEntity.hpp