The different simplification techniques implemented in PRS framework. More...

#include <preprocess.hpp>

Inheritance diagram for preprocess:

Collaboration diagram for preprocess:

Public Member Functions
	preprocess (int id_)

int	find (int x)

bool	res_is_empty (int var)

void	update_var_clause_label ()

void	preprocess_init ()

bool	preprocess_resolution ()

bool	preprocess_binary ()

bool	preprocess_up ()

void	get_complete_model ()

int	check_card (int id)

int	preprocess_card ()

int	search_almost_one ()

int	card_elimination ()

int	scc_almost_one ()

void	upd_occur (int v, int s)

bool	preprocess_gauss ()

int	search_xors ()

int	cal_dup_val (int i)

int	ecc_var ()

int	ecc_xor ()

int	gauss_elimination ()

int	rematch_eql (int x)

int	rematch_and (int x)

int	rematch_xor (int x)

bool	cnf2aig ()

int	find_fa (int x)

int	preprocess_circuit ()

void	epcec_preprocess ()

bool	do_epcec ()

bool	_simulate (Bitset **result, int bit_size)

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

void	restoreModel (std::vector< int > &model)
	Restore the original model from the preprocessed one.

int	preprocess_circuit_wrapper ()

int	preprocess_gauss_wrapper ()

int	preprocess_propagation_wrapper ()

int	preprocess_card_wrapper ()

int	preprocess_resolution_wrapper ()

int	preprocess_binary_wrapper ()

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={}) override
	Solve the formula with a given cube.

void	releaseMemory () override
	Release memory used by the preprocessor.

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

void	loadFormula (const char *filename) override
	Load formula from a given dimacs file.

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

void	printStatistics ()
	Print solver statistics.

std::vector< simpleClause >	getSimplifiedFormula ()
	Get the simplified formula after preprocessing.

std::size_t	getClausesCount ()

void	diversify (const SeedGenerator &getSeed)
	Perform native diversification. The Default lambda returns the solver ID.

PreprocessorStats	getPreprocessorStatistics ()
	Get statistics about the preprocessing.

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

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.

Public Member Functions inherited from PreprocessorInterface
	PreprocessorInterface (PreprocessorAlgorithm algo, int id)
	Constructor for PreprocessorInterface.

Public Member Functions inherited from SolverInterface
virtual void	printWinningLog ()
	Print the winning log.

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 Attributes
int	vars

int	clauses

std::vector< std::vector< int > >	clause

std::vector< std::vector< int > >	res_clause

int	flag

int	epcec_out

int	maxvar

int	nxors

int	rins

int *	psign

int *	psum

int *	fixed

int *	cell

int *	used

int *	model

int *	topo_counter

std::vector< int >	epcec_in

std::vector< int >	epcec_rin

std::vector< int > *	inv_C

std::vector< type_gate >	gate

int	maxlen

int	orivars

int	oriclauses

int	res_clauses

int	resolutions

int *	f

int	nlit

int *	a

int *	val

int *	color

int *	varval

int *	q

int *	seen

int *	resseen

int *	clean

int *	mapto

int *	mapfrom

int *	mapval

std::vector< int > *	occurp

std::vector< int > *	occurn

std::vector< int >	clause_delete

std::vector< int >	nxtc

std::vector< int >	resolution

std::vector< std::vector< int > >	card_one

std::vector< std::vector< double > >	mat

std::vector< int > *	occur

std::vector< int >	cdel

int *	abstract

int	gauss_eli_unit

int	gauss_eli_binary

std::vector< xorgate >	xors

std::vector< int >	scc_id

std::vector< std::vector< int > >	scc

std::vector< std::vector< int > >	xor_scc

int	count = 0

int	maxVarCircuit

int	maxVarGauss

int	maxVarCard

int	maxClauseSizeXor

int	maxClauseCircuit

int	maxClauseBinary

int	maxClauseGauss

int	maxClauseCard

std::vector< std::function< int()> >	preprocessors

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

The different simplification techniques implemented in PRS framework.

Member Function Documentation

◆ addClause()

void preprocess::addClause ( ClauseExchangePtr clause )

inlinevirtual

Add a permanent clause to the formula.

Parameters

clause The clause to add.

Implements SolverInterface.

◆ addClauses()

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

inlinevirtual

Add a list of permanent clauses to the formula.

Parameters

clauses The list of clauses to add.

Implements SolverInterface.

◆ addInitialClauses()

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

inlinevirtual

Add a list of initial clauses to the formula.

Parameters

clauses	The list of initial clauses.
nbVars	The number of variables.

Implements SolverInterface.

◆ diversify()

void preprocess::diversify ( const SeedGenerator & getSeed )

inlinevirtual

Perform native diversification. The Default lambda returns the solver ID.

Implements SolverInterface.

◆ getDivisionVariable()

int preprocess::getDivisionVariable ( )

inlinevirtual

Get a variable suitable for search splitting.

Returns: The division variable.

Implements SolverInterface.

◆ getModel()

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

overridevirtual

Return the model in case of SAT result.

Returns: The model as a vector of integers.

Implements SolverInterface.

◆ getPreprocessorStatistics()

PreprocessorStats preprocess::getPreprocessorStatistics ( )

inlinevirtual

Get statistics about the preprocessing.

Returns: A PreprocessorStats object containing statistics.

Implements PreprocessorInterface.

◆ getSimplifiedFormula()

std::vector< simpleClause > preprocess::getSimplifiedFormula ( )

inlinevirtual

Get the simplified formula after preprocessing.

Returns: A vector of simplified clauses.

Implements PreprocessorInterface.

◆ getVariablesCount()

unsigned int preprocess::getVariablesCount ( )

inlinevirtual

Get the current number of variables.

Returns: The number of variables.

Implements SolverInterface.

◆ loadFormula()

void preprocess::loadFormula ( const char * filename )

overridevirtual

Load formula from a given dimacs file.

Parameters

filename The name of the file to load from.

Implements SolverInterface.

◆ printStatistics()

void preprocess::printStatistics ( )

inlinevirtual

Print solver statistics.

Reimplemented from SolverInterface.

◆ releaseMemory()

void preprocess::releaseMemory ( )

overridevirtual

Release memory used by the preprocessor.

Implements PreprocessorInterface.

◆ restoreModel()

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

inlinevirtual

Restore the original model from the preprocessed one.

Parameters

model The model to be restored.

Implements PreprocessorInterface.

◆ setSolverInterrupt()

void preprocess::setSolverInterrupt ( )

inlinevirtual

Interrupt resolution, solving cannot continue until interrupt is unset.

Implements SolverInterface.

◆ solve()

SatResult preprocess::solve ( const std::vector< int > & cube = {} )

overridevirtual

Solve the formula with a given cube.

Parameters

cube	The cube to solve with.

Returns: The result of the solving process.

Implements SolverInterface.

◆ unsetSolverInterrupt()

void preprocess::unsetSolverInterrupt ( )

inlinevirtual

Remove the SAT solving interrupt request.

Implements SolverInterface.

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

/github/workspace/src/preprocessors/PRS-Preprocessors/preprocess.hpp

Public Member Functions

Public Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ addClause()

◆ addClauses()

◆ addInitialClauses()

◆ diversify()

◆ getDivisionVariable()

◆ getModel()

◆ getPreprocessorStatistics()

◆ getSimplifiedFormula()

◆ getVariablesCount()

◆ loadFormula()

◆ printStatistics()

◆ releaseMemory()

◆ restoreModel()

◆ setSolverInterrupt()

◆ solve()

◆ unsetSolverInterrupt()