Instance of a KissatINCSolver solver. More...

#include <KissatINCSolver.hpp>

Inheritance diagram for KissatINCSolver:

Collaboration diagram for KissatINCSolver:

Public Member Functions
void	setBumpVar (int v)

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) override
	Add a learned clause to the formula.

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

void	printStatistics ()
	Get solver statistics.

void	printWinningLog () override
	Print the winning log.

void	setFamily (KissatFamily family)

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

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

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

virtual	~KissatINCSolver ()
	Destructor.

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

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

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
int	bump_var

kissat_mab *	solver
	Pointer to a KissatINCSolver solver.

KissatFamily	family

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
char	KissatIncImportClause (void , kissat )
	Callback to export/import clauses used by real kissat.

char	KissatIncExportClause (void , kissat )

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

Member Function Documentation

◆ addClause()

void KissatINCSolver::addClause ( ClauseExchangePtr clause )

virtual

Add a permanent clause to the formula.

Implements SolverInterface.

◆ addClauses()

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

virtual

Add a list of permanent clauses to the formula.

Implements SolverInterface.

◆ addInitialClauses()

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

overridevirtual

Add a list of initial clauses to the formula.

Implements SolverInterface.

◆ bumpVariableActivity()

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

virtual

Bump activity of a given variable.

Implements SolverCdclInterface.

◆ diversify()

void KissatINCSolver::diversify ( const SeedGenerator & getSeed )

overridevirtual

Native diversification.

Implements SolverInterface.

◆ getDivisionVariable()

int KissatINCSolver::getDivisionVariable ( )

virtual

Get a variable suitable for search splitting.

Implements SolverInterface.

◆ getFinalAnalysis()

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

virtual

Return the model in case of SAT result.

Implements SolverInterface.

◆ getSatAssumptions()

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

virtual

Get current assumptions.

Returns: Vector of integers representing the current assumptions

Implements SolverCdclInterface.

◆ getVariablesCount()

unsigned int KissatINCSolver::getVariablesCount ( )

virtual

Get the number of variables of the current resolution.

Implements SolverInterface.

◆ importClause()

bool KissatINCSolver::importClause ( const ClauseExchangePtr & clause )

overridevirtual

Add a learned clause to the formula.

Implements SharingEntity.

◆ importClauses()

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

overridevirtual

Add a list of learned clauses to the formula.

Implements SharingEntity.

◆ loadFormula()

void KissatINCSolver::loadFormula ( const char * filename )

virtual

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

Implements SolverInterface.

◆ printStatistics()

void KissatINCSolver::printStatistics ( )

virtual

Get solver statistics.

Reimplemented from SolverInterface.

◆ printWinningLog()

void KissatINCSolver::printWinningLog ( )

overridevirtual

Print the winning log.

Reimplemented from SolverInterface.

◆ setPhase()

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

virtual

Set initial phase for a given variable.

Implements SolverCdclInterface.

◆ setSolverInterrupt()

void KissatINCSolver::setSolverInterrupt ( )

virtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

◆ solve()

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

virtual

Solve the formula with a given cube.

Implements SolverInterface.

◆ unsetSolverInterrupt()

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