PreprocessorInterface Class Reference

Interface for preprocessor algorithms in SAT solving. More...

#include <PreprocessorInterface.hpp>

Inheritance diagram for PreprocessorInterface:

Collaboration diagram for PreprocessorInterface:

Public Member Functions
	PreprocessorInterface (PreprocessorAlgorithm algo, int id)
	Constructor for PreprocessorInterface.
virtual std::vector< simpleClause >	getSimplifiedFormula ()=0
	Get the simplified formula after preprocessing.
virtual void	restoreModel (std::vector< int > &model)=0
	Restore the original model from the preprocessed one.
virtual PreprocessorStats	getPreprocessorStatistics ()=0
	Get statistics about the preprocessing.
virtual void	releaseMemory ()=0
	Release memory used by the preprocessor.
Public Member Functions inherited from SolverInterface
virtual unsigned int	getVariablesCount ()=0
	Get the current number of variables.
virtual int	getDivisionVariable ()=0
	Get a variable suitable for search splitting.
virtual void	setSolverInterrupt ()=0
	Interrupt resolution, solving cannot continue until interrupt is unset.
virtual void	unsetSolverInterrupt ()=0
	Remove the SAT solving interrupt request.
virtual void	printWinningLog ()
	Print the winning log.
virtual SatResult	solve (const std::vector< int > &cube)=0
	Solve the formula with a given cube.
virtual void	addClause (ClauseExchangePtr clause)=0
	Add a permanent clause to the formula.
virtual void	addClauses (const std::vector< ClauseExchangePtr > &clauses)=0
	Add a list of permanent clauses to the formula.
virtual void	addInitialClauses (const std::vector< simpleClause > &clauses, unsigned int nbVars)=0
	Add a list of initial clauses to the formula.
virtual void	loadFormula (const char *filename)=0
	Load formula from a given dimacs file.
virtual void	printStatistics ()
	Print solver statistics.
virtual std::vector< int >	getModel ()=0
	Return the model in case of SAT result.
virtual void	printParameters ()
	Print the parameters set for a solver.
virtual void	diversify (const SeedGenerator &getSeed=[](SolverInterface *s) { return s->getSolverId();})=0
	Perform native diversification. The Default lambda returns the solver ID.
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.

Additional Inherited Members
Protected Member Functions inherited from SolverInterface
template<typename Derived >
void	initializeTypeId ()
	Initialize the type ID for a derived class.
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.
Protected Attributes inherited from SolverInterface
SolverAlgorithmType	m_algoType
std::atomic< bool >	m_initialized
unsigned int	m_solverTypeId
int	m_solverId
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

Interface for preprocessor algorithms in SAT solving.

This abstract class defines the interface for preprocessor algorithms used in SAT solving. It inherits from SolverInterface and provides additional methods specific to preprocessors.

Constructor & Destructor Documentation

PreprocessorInterface()

PreprocessorInterface::PreprocessorInterface ( PreprocessorAlgorithm algo, int id )

inline

Constructor for PreprocessorInterface.

Parameters

algo	The preprocessor algorithm type.
id	The unique identifier for the preprocessor.

Member Function Documentation

getPreprocessorStatistics()

virtual PreprocessorStats PreprocessorInterface::getPreprocessorStatistics ( )

pure virtual

Get statistics about the preprocessing.

Returns

A PreprocessorStats object containing statistics.

Implemented in preprocess, and StructuredBVA.

getSimplifiedFormula()

virtual std::vector< simpleClause > PreprocessorInterface::getSimplifiedFormula ( )

pure virtual

Get the simplified formula after preprocessing.

Returns

A vector of simplified clauses.

Implemented in preprocess, and StructuredBVA.

releaseMemory()

virtual void PreprocessorInterface::releaseMemory ( )

pure virtual

Release memory used by the preprocessor.

Implemented in preprocess, and StructuredBVA.

restoreModel()

virtual void PreprocessorInterface::restoreModel ( std::vector< int > & model )

pure virtual

Restore the original model from the preprocessed one.

Parameters

model

The model to be restored.

Implemented in preprocess, and StructuredBVA.

---

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

• /github/workspace/src/preprocessors/PreprocessorInterface.hpp