#include <Lingeling.hpp>

Inheritance diagram for Lingeling:

Collaboration diagram for Lingeling:

Public Member Functions
void	loadFormula (const char *filename)
	Load formula from a given dimacs file, return false if failed.

unsigned int	getVariablesCount ()
	Get the number of variables of the current resolution.

int	getDivisionVariable ()
	Get a variable suitable for search splitting.

void	setPhase (const unsigned int var, const bool phase)
	Set initial phase for a given variable.

void	bumpVariableActivity (const int var, const int times)
	Bump activity of a given variable.

void	setSolverInterrupt ()
	Interrupt resolution, solving cannot continue until interrupt is unset.

void	unsetSolverInterrupt ()
	Remove the SAT solving interrupt request.

SatResult	solve (const std::vector< int > &cube)
	Solve the formula with a given cube.

void	addClause (ClauseExchangePtr clause)
	Add a permanent clause to the formula.

void	addClauses (const std::vector< ClauseExchangePtr > &clauses)
	Add a list of permanent clauses to the formula.

void	addInitialClauses (const std::vector< simpleClause > &clauses, unsigned int nbVars) override
	Add a list of initial clauses to the formula.

bool	importClause (const ClauseExchangePtr &clause)
	Add a learned clause to the formula.

void	importClauses (const std::vector< ClauseExchangePtr > &clauses)
	Add a list of learned clauses to the formula.

void	printStatistics ()
	Print solver statistics.

void	printWinningLog () override
	Print the winning log.

std::vector< int >	getModel ()
	Return the model in case of SAT result.

void	diversify (const SeedGenerator &getSeed) override
	Native diversification.

std::vector< int >	getFinalAnalysis ()
	Get the final analysis in case of UNSAT result.

std::vector< int >	getSatAssumptions ()
	Get current assumptions.

	Lingeling (int id, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Constructor.

	Lingeling (const Lingeling &other, int id, const std::shared_ptr< ClauseDatabase > &clauseDB)
	Copy constructor.

	~Lingeling ()
	Destructor.

Public Member Functions inherited from SolverCdclInterface
void	printWinningLog ()
	Print winning log information.

SolverCdclType	getSolverType ()
	Returns solver type for static cast.

	SolverCdclInterface (int solverId, const std::shared_ptr< ClauseDatabase > &clauseDB, SolverCdclType solverCdclType)
	Constructor for SolverCdclInterface.

virtual	~SolverCdclInterface ()
	Virtual destructor.

Public Member Functions inherited from SolverInterface
virtual void	printParameters ()
	Print the parameters set for a solver.

bool	isInitialized ()
	Check if the solver is initialized.

void	setInitialized (bool value)
	Set the initialization status of the solver.

SolverAlgorithmType	getAlgoType ()
	Get the algorithm type of the solver.

unsigned int	getSolverTypeId ()
	Get the solver type ID.

void	setSolverTypeId (unsigned int typeId)
	Set the solver type ID.

unsigned int	getSolverId ()
	Get the solver ID.

void	setSolverId (unsigned int id)
	Set the solver ID.

unsigned int	getSolverTypeCount () const
	Get the current count of instances of this object's most-derived type.

	SolverInterface (SolverAlgorithmType algoType, int solverId)
	Constructor for SolverInterface.

virtual	~SolverInterface ()
	Virtual destructor for SolverInterface.

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
LGL *	solver
	Pointer to a Lingeling solver.

std::atomic< bool >	stopSolver
	Boolean used to determine if the resolution should stop.

ClauseBuffer	clausesToAdd
	Buffer used to add permanent clauses.

boost::lockfree::queue< int, boost::lockfree::fixed_sized< false > >	unitsToImport
	Buffer used to import units.

size_t	unitsBufferSize
	Size of the unit array used by Lingeling.

size_t	clsBufferSize
	Size of the clauses array used by Lingeling.

int *	unitsBuffer
	Unit array used by Lingeling.

int *	clsBuffer
	Clauses array used by Lingeling.

Protected Attributes inherited from SolverCdclInterface
std::shared_ptr< ClauseDatabase >	m_clausesToImport
	Database used to import clauses. Can be common with other solvers.

Protected Attributes inherited from SolverInterface
SolverAlgorithmType	m_algoType

std::atomic< bool >	m_initialized

unsigned int	m_solverTypeId

int	m_solverId

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.

Friends
int	termCallback (void *solverPtr)
	Termination callback.

void	produceUnit (void *sp, int lit)
	Callback to export units.

void	produce (void sp, int cls, int glue)
	Callback to export clauses.

void	consumeUnits (void sp, int start, int *end)
	Callback to import units.

void	consumeCls (void sp, int clause, int glue)
	Callback to import clauses.

Additional Inherited Members
Public Attributes inherited from SolverCdclInterface
SolverCdclType	m_cdclType
	Type of this CDCL solver.

Protected Member Functions inherited from SolverInterface
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.

Protected Member Functions inherited from SharingEntity
virtual bool	exportClauseToClient (const ClauseExchangePtr &clause, std::shared_ptr< SharingEntity > client)
	Export a clause to a specific client.

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.

Static Protected Member Functions inherited from SolverInterface
template<typename Derived >
static unsigned int	getAndIncrementTypeCount ()
	Get and increment the instance count for a specific derived type.

Static Protected Attributes inherited from SolverInterface
static std::unordered_map< std::type_index, std::atomic< unsigned int > >	s_instanceCounts
	Number of existing instances of derived classes.

Detailed Description

Instance of a Lingeling solver.

Member Function Documentation

◆ addClause()

void Lingeling::addClause ( ClauseExchangePtr clause )

virtual

Add a permanent clause to the formula.

Implements SolverInterface.

◆ addClauses()

void Lingeling::addClauses ( const std::vector< ClauseExchangePtr > & clauses )

virtual

Add a list of permanent clauses to the formula.

Implements SolverInterface.

◆ addInitialClauses()

void Lingeling::addInitialClauses	(	const std::vector< simpleClause > &	clauses,
		unsigned int	nbVars )

overridevirtual

Add a list of initial clauses to the formula.

Implements SolverInterface.

◆ bumpVariableActivity()

void Lingeling::bumpVariableActivity	(	const int	var,
		const int	times )

virtual

Bump activity of a given variable.

Implements SolverCdclInterface.

◆ diversify()

void Lingeling::diversify ( const SeedGenerator & getSeed )

overridevirtual

Native diversification.

Implements SolverInterface.

◆ getDivisionVariable()

int Lingeling::getDivisionVariable ( )

virtual

Get a variable suitable for search splitting.

Implements SolverInterface.

◆ getFinalAnalysis()

std::vector< int > Lingeling::getFinalAnalysis ( )

virtual

Get the final analysis in case of UNSAT result.

Returns: Vector of integers representing the final analysis

Implements SolverCdclInterface.

◆ getModel()

std::vector< int > Lingeling::getModel ( )

virtual

Return the model in case of SAT result.

Implements SolverInterface.

◆ getSatAssumptions()

std::vector< int > Lingeling::getSatAssumptions ( )

virtual

Get current assumptions.

Returns: Vector of integers representing the current assumptions

Implements SolverCdclInterface.

◆ getVariablesCount()

unsigned int Lingeling::getVariablesCount ( )

virtual

Get the number of variables of the current resolution.

Implements SolverInterface.

◆ importClause()

bool Lingeling::importClause ( const ClauseExchangePtr & clause )

virtual

Add a learned clause to the formula.

Implements SharingEntity.

◆ importClauses()

void Lingeling::importClauses ( const std::vector< ClauseExchangePtr > & clauses )

virtual

Add a list of learned clauses to the formula.

Implements SharingEntity.

◆ loadFormula()

void Lingeling::loadFormula ( const char * filename )

virtual

Load formula from a given dimacs file, return false if failed.

Implements SolverInterface.

◆ printStatistics()

void Lingeling::printStatistics ( )

virtual

Print solver statistics.

Reimplemented from SolverInterface.

◆ printWinningLog()

void Lingeling::printWinningLog ( )

overridevirtual

Print the winning log.

Reimplemented from SolverInterface.

◆ setPhase()

void Lingeling::setPhase	(	const unsigned int	var,
		const bool	phase )

virtual

Set initial phase for a given variable.

Implements SolverCdclInterface.

◆ setSolverInterrupt()

void Lingeling::setSolverInterrupt ( )

virtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

◆ solve()

SatResult Lingeling::solve ( const std::vector< int > & cube )

virtual

Solve the formula with a given cube.

Implements SolverInterface.

◆ unsetSolverInterrupt()

void Lingeling::unsetSolverInterrupt ( )

virtual

Remove the SAT solving interrupt request.

Implements SolverInterface.

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

/github/workspace/src/solvers/CDCL/Lingeling.hpp

Public Member Functions

Protected Attributes

Friends

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ addClause()

◆ addClauses()

◆ addInitialClauses()

◆ bumpVariableActivity()

◆ diversify()

◆ getDivisionVariable()

◆ getFinalAnalysis()

◆ getModel()

◆ getSatAssumptions()

◆ getVariablesCount()

◆ importClause()

◆ importClauses()

◆ loadFormula()

◆ printStatistics()

◆ printWinningLog()

◆ setPhase()

◆ setSolverInterrupt()

◆ solve()

◆ unsetSolverInterrupt()