The Heule and Verwer method. More...

#include <HeuleVerwerCNFMethod.h>

Inheritance diagram for gsjj::passive::CNF::HeuleVerwerCNFMethod:

Collaboration diagram for gsjj::passive::CNF::HeuleVerwerCNFMethod:

Public Member Functions
	HeuleVerwerCNFMethod ()=delete

	~HeuleVerwerCNFMethod ()

Public Member Functions inherited from gsjj::passive::CNF::SATCNFMethod
	SATCNFMethod ()=delete

virtual	~SATCNFMethod ()

bool	solve () override
	Solves the SAT/SMT problem induced by the method. More...

std::unique_ptr< DFA< char > >	constructDFA () override
	Constructs the DFA induced by the variables according to the method. More...

virtual void	setStopTrigger (const std::chrono::seconds &timeLimit, std::atomic_bool &stopTrigger, const bool *stopPointer) override
	Sets the stop trigger for this method. More...

Public Member Functions inherited from gsjj::passive::Method
	Method ()=delete

virtual	~Method ()

bool	hasSolution () const
	If solve() has been called and if there exists a solution, return True. More...

unsigned int	numberOfStates () const
	Gives the number of states of the prospected DFA (the n) More...

double	timeToSolve () const
	Gives the CPU time taken to solve the problem. More...

Static Public Member Functions
static std::string	getFactoryName ()

Protected Member Functions
void	createVariables () override
	Creates all needed variables for the method. More...

void	createClauses () override
	Creates all needed clauses for the method. More...

std::unique_ptr< DFA< char > >	toDFA (const Minisat::vec< Minisat::lbool > &model) const override
	Effectively creates the DFA from the values of the variables in the given model. More...

	HeuleVerwerCNFMethod (const std::set< std::string > &SpSet, const std::set< std::string > &SmSet, const std::set< std::string > &SSet, const std::set< std::string > &prefixesSet, const std::set< char > &alphabetSet, unsigned int n)

Protected Member Functions inherited from gsjj::passive::CNF::SATCNFMethod
Minisat::Var	newVariable ()
	Creates a new variable in the SAT solver. More...

void	addClause (const Minisat::vec< Minisat::Lit > &clause)
	Adds a new clause to the SAT solver. More...

	SATCNFMethod (const std::set< std::string > &SpSet, const std::set< std::string > &SmSet, const std::set< std::string > &SSet, const std::set< std::string > &prefixesSet, const std::set< char > &alphabetSet, unsigned int n)

Protected Member Functions inherited from gsjj::passive::Method
	Method (const std::set< std::string > &SpSet, const std::set< std::string > &SmSet, const std::set< std::string > &SSet, const std::set< std::string > &prefixesSet, const std::set< char > &alphabetSet, unsigned int n)
	Creates the method. More...

Protected Attributes
std::map< std::pair< std::string, unsigned int >, Minisat::Var >	m_xVars

std::map< std::tuple< unsigned int, char, unsigned int >, Minisat::Var >	m_dVars

std::map< unsigned int, Minisat::Var >	m_fVars

Protected Attributes inherited from gsjj::passive::Method
const std::set< std::string >	m_Sp
	The set of words to accept . More...

const std::set< std::string >	m_Sm
	The set of words to reject . More...

const unsigned int	m_numberStates
	The number of states in the DFA to construct. More...

const std::set< std::string >	m_S
	In the code, $S = S_+ \cup S_-$ . More...

const std::set< std::string >	m_prefixes
	$Pref(S_+ \cup S_-)$ More...

const std::set< char >	m_alphabet
	$\Sigma$ More...

bool	m_triedSolve

bool	m_hasSolution

double	m_cpuTimeStart

double	m_cpuTimeEnd

Additional Inherited Members
Static Protected Attributes inherited from gsjj::passive::RegisterInFactory< HeuleVerwerCNFMethod >
static bool	s_registered
	Useful to make sure the template is correctly used by the compiler. More...

Detailed Description

The Heule and Verwer method.

Definition at line 18 of file HeuleVerwerCNFMethod.h.

Constructor & Destructor Documentation

◆ HeuleVerwerCNFMethod() [1/2]

gsjj::passive::CNF::HeuleVerwerCNFMethod::HeuleVerwerCNFMethod ( )

delete

◆ ~HeuleVerwerCNFMethod()

gsjj::passive::CNF::HeuleVerwerCNFMethod::~HeuleVerwerCNFMethod ( )

Definition at line 22 of file HeuleVerwerCNFMethod.cpp.

◆ HeuleVerwerCNFMethod() [2/2]

gsjj::passive::CNF::HeuleVerwerCNFMethod::HeuleVerwerCNFMethod	(	const std::set< std::string > &	SpSet,
		const std::set< std::string > &	SmSet,
		const std::set< std::string > &	SSet,
		const std::set< std::string > &	prefixesSet,
		const std::set< char > &	alphabetSet,
		unsigned int	n
	)

protected

Definition at line 16 of file HeuleVerwerCNFMethod.cpp.

Member Function Documentation

◆ createClauses()

void gsjj::passive::CNF::HeuleVerwerCNFMethod::createClauses ( )

overrideprotectedvirtual

Creates all needed clauses for the method.

Implements gsjj::passive::CNF::SATCNFMethod.

Definition at line 56 of file HeuleVerwerCNFMethod.cpp.

◆ createVariables()

void gsjj::passive::CNF::HeuleVerwerCNFMethod::createVariables ( )

overrideprotectedvirtual

Creates all needed variables for the method.

Implements gsjj::passive::CNF::SATCNFMethod.

Definition at line 29 of file HeuleVerwerCNFMethod.cpp.

◆ getFactoryName()

std::string gsjj::passive::CNF::HeuleVerwerCNFMethod::getFactoryName ( )

static

Definition at line 25 of file HeuleVerwerCNFMethod.cpp.

◆ toDFA()

std::unique_ptr< DFA< char > > gsjj::passive::CNF::HeuleVerwerCNFMethod::toDFA ( const Minisat::vec< Minisat::lbool > & model ) const

overrideprotectedvirtual

Effectively creates the DFA from the values of the variables in the given model.

Parameters

model The model

Returns: An unique_ptr to the constructed DFA

Implements gsjj::passive::CNF::SATCNFMethod.

Definition at line 183 of file HeuleVerwerCNFMethod.cpp.

Member Data Documentation

◆ m_dVars

std::map<std::tuple<unsigned int, char, unsigned int>, Minisat::Var> gsjj::passive::CNF::HeuleVerwerCNFMethod::m_dVars

protected

Definition at line 27 of file HeuleVerwerCNFMethod.h.

◆ m_fVars

std::map<unsigned int, Minisat::Var> gsjj::passive::CNF::HeuleVerwerCNFMethod::m_fVars

protected

Definition at line 28 of file HeuleVerwerCNFMethod.h.

◆ m_xVars

std::map<std::pair<std::string, unsigned int>, Minisat::Var> gsjj::passive::CNF::HeuleVerwerCNFMethod::m_xVars

protected

Definition at line 26 of file HeuleVerwerCNFMethod.h.

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

include/gsjj/passive/CNF/HeuleVerwerCNFMethod.h
src/passive/CNF/HeuleVerwerCNFMethod.cpp

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ HeuleVerwerCNFMethod() [1/2]

◆ ~HeuleVerwerCNFMethod()

◆ HeuleVerwerCNFMethod() [2/2]

Member Function Documentation

◆ createClauses()

◆ createVariables()

◆ getFactoryName()

◆ toDFA()

Member Data Documentation

◆ m_dVars

◆ m_fVars

◆ m_xVars