ClauseUtils Namespace Reference

Helping Functions for Clause Management (Hash and Equality) More...

Classes
struct	ClauseExchangeEqual
	Equality functor for ClauseExchange objects. More...
struct	ClauseExchangeHash
	Hash functor for ClauseExchange objects. More...
struct	ClauseExchangePtrEqual
	Equality functor for ClauseExchangePtr objects. More...
struct	ClauseExchangePtrHash
	Hash functor for ClauseExchangePtr objects. More...
struct	ClauseHash
	Hash functor for simple clauses. More...

Functions
size_t	lookup3_hash (size_t key)
	Computes a hash value for a single key using the Jenkins lookup3 algorithm.
size_t	lookup3_hash_clause (const int *clause, unsigned int size)
	Computes a hash value for a clause using the Jenkins lookup3 algorithm.
std::size_t	hashClause (const simpleClause &clause)
	Computes a hash value for a simple clause.
bool	operator== (const simpleClause &lhs, const simpleClause &rhs)
	Equality operator for simple clauses.
int	getLiteralsCount (const std::vector< ClauseExchangePtr > &clauses)
	Calculates the total number of literals in a vector of clauses.

Detailed Description

Helping Functions for Clause Management (Hash and Equality)

Function Documentation

getLiteralsCount()

int ClauseUtils::getLiteralsCount

(

const std::vector< ClauseExchangePtr > &

clauses

)

Calculates the total number of literals in a vector of clauses.

Parameters

clauses

Vector of shared pointers to ClauseExchange objects.

Returns

The total number of literals across all clauses.

hashClause()

std::size_t ClauseUtils::hashClause

(

const simpleClause &

clause

)

Computes a hash value for a simple clause.

Parameters

clause

The simple clause to hash.

Returns

The computed hash value.

lookup3_hash()

size_t ClauseUtils::lookup3_hash ( size_t key )

inline

Computes a hash value for a single key using the Jenkins lookup3 algorithm.

Parameters

key	The key to hash.

Returns

The computed hash value.

lookup3_hash_clause()

size_t ClauseUtils::lookup3_hash_clause ( const int * clause, unsigned int size )

inline

Computes a hash value for a clause using the Jenkins lookup3 algorithm.

Parameters

clause	Pointer to the array of literals in the clause.
size	Number of literals in the clause.

Returns

The computed hash value for the clause.

operator==()

bool ClauseUtils::operator==	(	const simpleClause &	lhs,
		const simpleClause &	rhs )

Equality operator for simple clauses.

Parameters

lhs	The left-hand side simple clause.
rhs	The right-hand side simple clause.

Returns

True if the clauses are equal, false otherwise.