Formula Class Reference

Represents a SAT formula with unit and non-unit clauses. More...

#include <Formula.hpp>

Collaboration diagram for Formula:

Public Member Functions
bool	push_clause (const std::vector< int > &clause)
	Adds a new clause to the formula.
bool	emplace_clause (std::initializer_list< int > clause)
	Adds a new clause to the formula using an initializer list.
bool	insert_unit (int lit)
	Inserts a unit clause into the formula.
void	delete_nonUnit (unsigned int index)
	Deletes a non-unit clause from the formula.
bool	delete_lit_nonUnit (unsigned int index, int lit)
	Deletes a literal from a non-unit clause.
bool	delete_nonUnit_occurence (int lit, unsigned int index)
	Deletes a clause occurrence from a literal's occurrence list.
void	delete_unit (int lit)
	Deletes a unit clause from the formula.
void	setVarCount (unsigned int varCount)
	Sets the number of variables in the formula.
unsigned int	getVarCount ()
	Gets the number of variables in the formula.
skipzero_span< const int >	getNonUnit (unsigned int i) const
	Gets a non-unit clause from the formula.
unsigned int	getNonUnitEfficientSize (unsigned int i) const
	Gets the number of non-zero literals in a non-unit clause.
const std::unordered_set< int > &	getUnits () const
	Gets the set of unit clauses.
std::unordered_set< int > &	getUnits ()
	Gets a modifiable reference to the set of unit clauses.
skipzero_span< unsigned int >	getOccurenceList (int lit)
	Gets the occurrence list of a literal.
unsigned int	getUnitCount ()
	Gets the number of unit clauses in the formula.
unsigned int	getNonUnitsCount ()
	Gets the number of non-unit clauses in the formula.
unsigned int	getAllClauseCount ()
	Gets the total number of clauses (unit and non-unit) in the formula.
void	shrink_structures ()
	Shrinks the internal data structures to save memory.

Detailed Description

Represents a SAT formula with unit and non-unit clauses.

Warning

still in development

Member Function Documentation

delete_lit_nonUnit()

bool Formula::delete_lit_nonUnit	(	unsigned int	index,
		int	lit )

Deletes a literal from a non-unit clause.

Parameters

index	The index of the clause.
lit	The literal to be deleted.

Returns

False if the clause becomes empty after deletion, true otherwise.

delete_nonUnit()

void Formula::delete_nonUnit

(

unsigned int

index

)

Deletes a non-unit clause from the formula.

Parameters

index

The index of the clause to be deleted.

delete_nonUnit_occurence()

bool Formula::delete_nonUnit_occurence	(	int	lit,
		unsigned int	index )

Deletes a clause occurrence from a literal's occurrence list.

Parameters

lit	The literal.
index	The index of the clause to be removed from the occurrence list.

Returns

True if the operation was successful.

delete_unit()

void Formula::delete_unit ( int lit )

inline

Deletes a unit clause from the formula.

Parameters

lit	The literal representing the unit clause to be deleted.

emplace_clause()

bool Formula::emplace_clause

(

std::initializer_list< int >

clause

)

Adds a new clause to the formula using an initializer list.

Parameters

clause

The clause to be added as an initializer list.

Returns

True if the clause was successfully added, false otherwise.

getAllClauseCount()

unsigned int Formula::getAllClauseCount ( )

inline

Gets the total number of clauses (unit and non-unit) in the formula.

Returns

The total number of clauses.

getNonUnit()

skipzero_span< const int > Formula::getNonUnit ( unsigned int i ) const

inline

Gets a non-unit clause from the formula.

Parameters

i	The index of the non-unit clause.

Returns

A span of the clause literals, skipping zeros.

getNonUnitEfficientSize()

unsigned int Formula::getNonUnitEfficientSize ( unsigned int i ) const

inline

Gets the number of non-zero literals in a non-unit clause.

Parameters

i	The index of the non-unit clause.

Returns

The number of non-zero literals in the clause.

getNonUnitsCount()

unsigned int Formula::getNonUnitsCount ( )

inline

Gets the number of non-unit clauses in the formula.

Returns

The number of non-unit clauses.

getOccurenceList()

skipzero_span< unsigned int > Formula::getOccurenceList ( int lit )

inline

Gets the occurrence list of a literal.

Parameters

lit	The literal.

Returns

A span of clause indices where the literal occurs.

getUnitCount()

unsigned int Formula::getUnitCount ( )

inline

Gets the number of unit clauses in the formula.

Returns

The number of unit clauses.

getUnits() [1/2]

std::unordered_set< int > & Formula::getUnits ( )

inline

Gets a modifiable reference to the set of unit clauses.

Returns

A reference to the set of unit clauses.

getUnits() [2/2]

const std::unordered_set< int > & Formula::getUnits ( ) const

inline

Gets the set of unit clauses.

Returns

A constant reference to the set of unit clauses.

getVarCount()

unsigned int Formula::getVarCount ( )

inline

Gets the number of variables in the formula.

Returns

The number of variables.

insert_unit()

bool Formula::insert_unit

(

int

lit

)

Inserts a unit clause into the formula.

Parameters

lit	The literal to be inserted as a unit clause.

Returns

True if the unit clause was successfully inserted, false otherwise.

push_clause()

bool Formula::push_clause

(

const std::vector< int > &

clause

)

Adds a new clause to the formula.

Parameters

clause

The clause to be added.

Returns

True if the clause was successfully added, false otherwise.

setVarCount()

void Formula::setVarCount ( unsigned int varCount )

inline

Sets the number of variables in the formula.

Parameters

varCount

The number of variables.

---

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

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