Instance of a MapleCOMSPS solver. More...

#include <MapleCOMSPSSolver.hpp>

Inheritance diagram for MapleCOMSPSSolver:

Collaboration diagram for MapleCOMSPSSolver:

Public Member Functions
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.

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

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 ()
	Get 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)
	Native diversification.

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

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

virtual	~MapleCOMSPSSolver ()
	Destructor.

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

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

void	setStrengthening (bool b)

void	setParameter (parameter p)

void	initshuffle (int id)

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
MapleCOMSPS::SimpSolver *	solver
	Pointer to a MapleCOMSPS solver.

std::unique_ptr< ClauseDatabase >	unitsToImport
	Buffer used to import clauses (units included).

ClauseBuffer	clausesToAdd
	Buffer used to add permanent clauses.

std::atomic< bool >	stopSolver
	Used to stop or continue the resolution.

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
MapleCOMSPS::Lit	cbkMapleCOMSPSImportUnit (void *)
	Callback to export/import clauses.

bool	cbkMapleCOMSPSImportClause (void , unsigned int , MapleCOMSPS::vec< MapleCOMSPS::Lit > &)

void	cbkMapleCOMSPSExportClause (void *, unsigned int, MapleCOMSPS::vec< MapleCOMSPS::Lit > &)

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 MapleCOMSPS solver.

Member Function Documentation

◆ addClause()

void MapleCOMSPSSolver::addClause ( ClauseExchangePtr clause )

virtual

Add a permanent clause to the formula.

Implements SolverInterface.

◆ addClauses()

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

virtual

Add a list of permanent clauses to the formula.

Implements SolverInterface.

◆ addInitialClauses()

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

overridevirtual

Add a list of initial clauses to the formula.

Implements SolverInterface.

◆ bumpVariableActivity()

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

virtual

Bump activity of a given variable.

Implements SolverCdclInterface.

◆ diversify()

void MapleCOMSPSSolver::diversify ( const SeedGenerator & getSeed )

virtual

Native diversification.

Parameters

noise	added for some radomness
family	to enable some parameters dependent on the family

Implements SolverInterface.

◆ getDivisionVariable()

int MapleCOMSPSSolver::getDivisionVariable ( )

virtual

Get a variable suitable for search splitting.

Implements SolverInterface.

◆ getFinalAnalysis()

std::vector< int > MapleCOMSPSSolver::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 > MapleCOMSPSSolver::getModel ( )

virtual

Return the model in case of SAT result.

Implements SolverInterface.

◆ getSatAssumptions()

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

virtual

Get current assumptions.

Returns: Vector of integers representing the current assumptions

Implements SolverCdclInterface.

◆ getVariablesCount()

unsigned int MapleCOMSPSSolver::getVariablesCount ( )

virtual

Get the number of variables of the current resolution.

Implements SolverInterface.

◆ importClause()

bool MapleCOMSPSSolver::importClause ( const ClauseExchangePtr & clause )

virtual

Add a learned clause to the formula.

Implements SharingEntity.

◆ importClauses()

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

virtual

Add a list of learned clauses to the formula.

Implements SharingEntity.

◆ loadFormula()

void MapleCOMSPSSolver::loadFormula ( const char * filename )

overridevirtual

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

Implements SolverInterface.

◆ printStatistics()

void MapleCOMSPSSolver::printStatistics ( )

virtual

Get solver statistics.

Reimplemented from SolverInterface.

◆ printWinningLog()

void MapleCOMSPSSolver::printWinningLog ( )

overridevirtual

Print the winning log.

Reimplemented from SolverInterface.

◆ setPhase()

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

virtual

Set initial phase for a given variable.

Implements SolverCdclInterface.

◆ setSolverInterrupt()

void MapleCOMSPSSolver::setSolverInterrupt ( )

virtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

◆ solve()

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

virtual

Solve the formula with a given cube.

Implements SolverInterface.

◆ unsetSolverInterrupt()

void MapleCOMSPSSolver::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/MapleCOMSPSSolver.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()