The Grinchtein, Leucker and Piterman's unary method. More...

#include <UnaryNonCNFMethod.h>

Inheritance diagram for gsjj::passive::NonCNF::UnaryNonCNFMethod:

Collaboration diagram for gsjj::passive::NonCNF::UnaryNonCNFMethod:

Public Member Functions
	UnaryNonCNFMethod ()=delete

	~UnaryNonCNFMethod ()

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

virtual	~SATNonCNFMethod ()

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

virtual 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
virtual bool	createFormula (std::ostream &stream) override
	Creates the boolean formula (must not be in CNF) and writes it in the stream. More...

std::unique_ptr< DFA< char > >	toDFA (std::istream &stream) const override
	Effectively creates the DFA. More...

virtual std::string	getFileName () const override
	Gives the name of the file in which the boolean formula must be written. More...

	UnaryNonCNFMethod (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::NonCNF::SATNonCNFMethod
bool	isSatisfiable () const
	Reads the output of the SAT solver and checks if the formula was satisfiable or not. More...

	SATNonCNFMethod (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...

Additional Inherited Members
Protected Attributes inherited from gsjj::passive::NonCNF::SATNonCNFMethod
const bool *	mustStop

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

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

Detailed Description

The Grinchtein, Leucker and Piterman's unary method.

It relies on Non CNF SAT solver

Definition at line 14 of file UnaryNonCNFMethod.h.

Constructor & Destructor Documentation

◆ UnaryNonCNFMethod() [1/2]

gsjj::passive::NonCNF::UnaryNonCNFMethod::UnaryNonCNFMethod ( )

delete

◆ ~UnaryNonCNFMethod()

gsjj::passive::NonCNF::UnaryNonCNFMethod::~UnaryNonCNFMethod ( )

Definition at line 16 of file UnaryNonCNFMethod.cpp.

◆ UnaryNonCNFMethod() [2/2]

gsjj::passive::NonCNF::UnaryNonCNFMethod::UnaryNonCNFMethod	(	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 10 of file UnaryNonCNFMethod.cpp.

Member Function Documentation

◆ createFormula()

bool gsjj::passive::NonCNF::UnaryNonCNFMethod::createFormula ( std::ostream & stream )

overrideprotectedvirtual

Creates the boolean formula (must not be in CNF) and writes it in the stream.

Parameters

stream The output stream in which to write

Returns: True iff it is possible to create the formula

Implements gsjj::passive::NonCNF::SATNonCNFMethod.

Definition at line 24 of file UnaryNonCNFMethod.cpp.

◆ getFactoryName()

std::string gsjj::passive::NonCNF::UnaryNonCNFMethod::getFactoryName ( )

static

Definition at line 20 of file UnaryNonCNFMethod.cpp.

◆ getFileName()

std::string gsjj::passive::NonCNF::UnaryNonCNFMethod::getFileName ( ) const

overrideprotectedvirtual

Gives the name of the file in which the boolean formula must be written.

Returns: The name of the file

Implements gsjj::passive::NonCNF::SATNonCNFMethod.

Definition at line 165 of file UnaryNonCNFMethod.cpp.

◆ toDFA()

std::unique_ptr< DFA< char > > gsjj::passive::NonCNF::UnaryNonCNFMethod::toDFA ( std::istream & stream ) const

overrideprotectedvirtual

Effectively creates the DFA.

If this function is called, the boolean formula is satisfiable. The output of the SAT solver is given in the stream

Implements gsjj::passive::NonCNF::SATNonCNFMethod.

Definition at line 105 of file UnaryNonCNFMethod.cpp.

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

include/gsjj/passive/NonCNF/UnaryNonCNFMethod.h
src/passive/NonCNF/UnaryNonCNFMethod.cpp

Public Member Functions

Static Public Member Functions

Protected Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ UnaryNonCNFMethod() [1/2]

◆ ~UnaryNonCNFMethod()

◆ UnaryNonCNFMethod() [2/2]

Member Function Documentation

◆ createFormula()

◆ getFactoryName()

◆ getFileName()

◆ toDFA()