The base class of all passive methods. More...

#include <Method.h>

Inheritance diagram for gsjj::passive::Method:

[legend]

Public Member Functions
	Method ()=delete

virtual	~Method ()

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

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

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

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

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

Protected Member Functions
	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
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

Detailed Description

The base class of all passive methods.

Definition at line 40 of file Method.h.

Constructor & Destructor Documentation

◆ Method() [1/2]

gsjj::passive::Method::Method ( )

delete

◆ ~Method()

gsjj::passive::Method::~Method ( )

virtual

Definition at line 40 of file Method.cpp.

◆ Method() [2/2]

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
	)

protected

Creates the method.

Parameters

SpSet	The set of words to accept
SmSet	The set of words to reject
SSet	The union of SpSet and SmSet
prefixesSet	The prefixes of S
alphabetSet	The used alphabet
n	The number of states in the prospected DFA

Definition at line 25 of file Method.cpp.

Member Function Documentation

◆ constructDFA()

virtual std::unique_ptr<DFA<char> > gsjj::passive::Method::constructDFA ( )

pure virtual

Constructs the DFA induced by the variables according to the method.

If the SAT/SMT problem has not yet been solved, the function automatically solves it. If the SAT/SMT problem is unsolvable, returns a null pointer.

Returns: An unique_ptr to the constructed DFA or an empty pointer if the problem is not solvable

Implemented in gsjj::passive::NonCNF::SATNonCNFMethod, gsjj::passive::CNF::BinaryCNFMethod, gsjj::passive::CNF::SATCNFMethod, and gsjj::passive::SMT::SMTMethod.

◆ hasSolution()

bool gsjj::passive::Method::hasSolution ( ) const

inline

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

Otherwise, return false

Returns: True iff the SAT problem has a solution

Definition at line 60 of file Method.h.

◆ numberOfStates()

unsigned int gsjj::passive::Method::numberOfStates ( ) const

Gives the number of states of the prospected DFA (the n)

Returns: The number of states

Definition at line 43 of file Method.cpp.

◆ setStopTrigger()

virtual void gsjj::passive::Method::setStopTrigger	(	const std::chrono::seconds &	timeLimit,
		std::atomic_bool &	stopTrigger,
		const bool *	stopPointer
	)

pure virtual

Sets the stop trigger for this method.

Since we use three different solvers and each has its own way to stop (CVC4 uses a function to set a time limit, Maple is in C++ so we can use an atomic variable and Limboole is in C and we must use a pointer), we must provide each possibility

Parameters

timeLimit	The time in seconds the method can take. It's used by SMT methods.
stopTrigger	The atomic_bool variable. Once set to true, the method will stop. It's used by CNF methods.
stopPointer	The pointer variable. Once the value is set to true, the method will stop. It's used by NonCNF methods.

Implemented in gsjj::passive::NonCNF::SATNonCNFMethod, gsjj::passive::CNF::BinaryCNFMethod, gsjj::passive::CNF::SATCNFMethod, and gsjj::passive::SMT::SMTMethod.

◆ solve()

virtual bool gsjj::passive::Method::solve ( )

pure virtual

Solves the SAT/SMT problem induced by the method.

Il also creates every variable and clause needed

Returns: True iff the problem is solvable

Implemented in gsjj::passive::NonCNF::SATNonCNFMethod, gsjj::passive::CNF::BinaryCNFMethod, gsjj::passive::CNF::SATCNFMethod, and gsjj::passive::SMT::SMTMethod.

◆ timeToSolve()

double gsjj::passive::Method::timeToSolve ( ) const

Gives the CPU time taken to solve the problem.

Returns: The CPU time taken by the solver

Definition at line 47 of file Method.cpp.

Member Data Documentation

◆ m_alphabet

const std::set<char> gsjj::passive::Method::m_alphabet

protected

$\Sigma$

Definition at line 121 of file Method.h.

◆ m_cpuTimeEnd

double gsjj::passive::Method::m_cpuTimeEnd

protected

Definition at line 127 of file Method.h.

◆ m_cpuTimeStart

double gsjj::passive::Method::m_cpuTimeStart

protected

Definition at line 126 of file Method.h.

◆ m_hasSolution

bool gsjj::passive::Method::m_hasSolution

protected

Definition at line 124 of file Method.h.

◆ m_numberStates

const unsigned int gsjj::passive::Method::m_numberStates

protected

The number of states in the DFA to construct.

Definition at line 109 of file Method.h.

◆ m_prefixes

const std::set<std::string> gsjj::passive::Method::m_prefixes

protected

$Pref(S_+ \cup S_-)$

Definition at line 117 of file Method.h.

◆ m_S

const std::set<std::string> gsjj::passive::Method::m_S

protected

In the code, $S = S_+ \cup S_-$ .

Definition at line 113 of file Method.h.

◆ m_Sm

const std::set<std::string> gsjj::passive::Method::m_Sm

protected

The set of words to reject $S_-$ .

Definition at line 105 of file Method.h.

◆ m_Sp

const std::set<std::string> gsjj::passive::Method::m_Sp

protected

The set of words to accept $S_+$ .

Definition at line 101 of file Method.h.

◆ m_triedSolve

bool gsjj::passive::Method::m_triedSolve

protected

Definition at line 123 of file Method.h.

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

include/gsjj/passive/Method.h
src/passive/Method.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Method() [1/2]

◆ ~Method()

◆ Method() [2/2]

Member Function Documentation

◆ constructDFA()

◆ hasSolution()

◆ numberOfStates()

◆ setStopTrigger()

◆ solve()

◆ timeToSolve()

Member Data Documentation

◆ m_alphabet

◆ m_cpuTimeEnd

◆ m_cpuTimeStart

◆ m_hasSolution

◆ m_numberStates

◆ m_prefixes

◆ m_S

◆ m_Sm

◆ m_Sp

◆ m_triedSolve