ClauseExchange Class Reference

Represents an exchangeable clause with flexible array member. More...

#include <ClauseExchange.hpp>

Collaboration diagram for ClauseExchange:

Public Member Functions
	~ClauseExchange ()=default
	Destructor.
int &	operator[] (unsigned int index)
	Access clause literal by index.
const int &	operator[] (unsigned int index) const
	Access clause literal by index (const version).
int *	begin ()
	Get iterator to the beginning of the clause.
int *	end ()
	Get iterator to the end of the clause.
const int *	begin () const
	Get const iterator to the beginning of the clause.
const int *	end () const
	Get const iterator to the end of the clause.
void	sortLiterals ()
	Sort the literals in ascending order.
void	sortLiteralsDescending ()
	Sort the literals in descending order.
std::string	toString () const
	Convert the clause to a string representation.
ClauseExchange *	toRawPtr ()
	Convert to a raw pointer and increment the reference count.

Static Public Member Functions
static ClauseExchangePtr	create (const unsigned int size, const unsigned int lbd=0, const int from=-1)
	Create a new ClauseExchange object.
static ClauseExchangePtr	create (const int *begin, const int *end, const unsigned int lbd=0, const int from=-1)
	Create a new ClauseExchange object using pointers.
static ClauseExchangePtr	create (const std::vector< int > &v_cls, const unsigned int lbd=0, const int from=-1)
	Create a new ClauseExchange object from a vector of literals.
static ClauseExchangePtr	fromRawPtr (ClauseExchange *ptr)
	Create an intrusive_ptr from a raw pointer.

Public Attributes
unsigned int	lbd
	Literal Block Distance (LBD) of the clause.
int	from
	Source identifier of the clause.
unsigned int	size
	Size of the clause.
std::atomic< unsigned int >	refCounter
	Counter for intrusive_ptr copies and raw pointer conversions.
int	lits [0]
	Flexible array member for storing clause literals (must be last)

Detailed Description

Represents an exchangeable clause with flexible array member.

This class provides a memory-efficient way to store and manage clauses of varying sizes. It uses a flexible array member for storing the actual clause data and supports reference counting through boost::intrusive_ptr.

Todo

Template for metadata for better memory footprint.

Warning

If the size of the clause is greater than 1 the lbd is forced to at least 2

Member Function Documentation

begin() [1/2]

int * ClauseExchange::begin ( )

inline

Get iterator to the beginning of the clause.

Returns

Pointer to the first element of the clause.

begin() [2/2]

const int * ClauseExchange::begin ( ) const

inline

Get const iterator to the beginning of the clause.

Returns

Const pointer to the first element of the clause.

create() [1/3]

static ClauseExchangePtr ClauseExchange::create ( const int * begin, const int * end, const unsigned int lbd = 0, const int from = -1 )

static

Create a new ClauseExchange object using pointers.

Parameters

begin	Start of integer data.
end	End of integer data.
lbd	Literal Block Distance of the clause (default: 0).
from	Source identifier of the clause (default: -1).

Returns

ClauseExchangePtr Smart pointer to the created object.

Exceptions

std::bad_alloc

If memory allocation fails.

create() [2/3]

static ClauseExchangePtr ClauseExchange::create ( const std::vector< int > & v_cls, const unsigned int lbd = 0, const int from = -1 )

static

Create a new ClauseExchange object from a vector of literals.

Parameters

v_cls	Vector containing the clause literals.
lbd	Literal Block Distance of the clause (default: 0).
from	Source identifier of the clause (default: -1).

Returns

ClauseExchangePtr Smart pointer to the created object.

Exceptions

std::bad_alloc

If memory allocation fails.

create() [3/3]

static ClauseExchangePtr ClauseExchange::create ( const unsigned int size, const unsigned int lbd = 0, const int from = -1 )

static

Create a new ClauseExchange object.

Parameters

lbd	Literal Block Distance of the clause (default: 0).
from	Source identifier of the clause (default: -1).

Returns

ClauseExchangePtr Smart pointer to the created object.

Exceptions

std::bad_alloc

If memory allocation fails.

end() [1/2]

int * ClauseExchange::end ( )

inline

Get iterator to the end of the clause.

Returns

Pointer to one past the last element of the clause.

end() [2/2]

const int * ClauseExchange::end ( ) const

inline

Get const iterator to the end of the clause.

Returns

Const pointer to one past the last element of the clause.

fromRawPtr()

static ClauseExchangePtr ClauseExchange::fromRawPtr ( ClauseExchange * ptr )

inlinestatic

Create an intrusive_ptr from a raw pointer.

Parameters

ptr	Raw pointer to a ClauseExchange object.

Returns

ClauseExchangePtr Smart pointer to the object.

operator[]() [1/2]

int & ClauseExchange::operator[] ( unsigned int index )

inline

Access clause literal by index.

Parameters

index

Index of the literal to access.

Returns

Reference to the literal at the specified index.

operator[]() [2/2]

const int & ClauseExchange::operator[] ( unsigned int index ) const

inline

Access clause literal by index (const version).

Parameters

index

Index of the literal to access.

Returns

Const reference to the literal at the specified index.

toRawPtr()

ClauseExchange * ClauseExchange::toRawPtr ( )

inline

Convert to a raw pointer and increment the reference count.

Returns

Raw pointer to this object.

toString()

std::string ClauseExchange::toString

(

)

const

Convert the clause to a string representation.

Returns

String representation of the clause.

---

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

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