The binary method with a CNF SAT solver. More...

#include <BinaryCNFMethod.h>

Inheritance diagram for gsjj::passive::CNF::BinaryCNFMethod:

Collaboration diagram for gsjj::passive::CNF::BinaryCNFMethod:

Public Member Functions
	BinaryCNFMethod ()=delete

virtual	~BinaryCNFMethod ()

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 Types
typedef std::map< std::pair< std::string, unsigned int >, Gate * >	m_mapType

Protected Member Functions
	BinaryCNFMethod (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)

virtual void	createVariables ()

virtual Gate *	createFormula ()

Gate *	equal (const std::string &u, const std::string &v)

Gate *	phi_different (const std::string &u, const std::string &v)

Gate *	phi_not_q_i (const std::string &u, unsigned int i)

unsigned int	toState (const std::string &u) const

std::unique_ptr< DFA< char > >	toDFA () const

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::unique_ptr< BC >	m_solver

SimplifyOptions	m_simplify_opts

unsigned int	m_binarySize
	More...

m_mapType	m_stateToVar

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< BinaryCNFMethod >
static bool	s_registered
	Useful to make sure the template is correctly used by the compiler. More...

Detailed Description

The binary method with a CNF SAT solver.

Since we need to use a tool to translate the boolean formula in CNF, this implementation is different from the other methods relying on CNF Solvers.

Definition at line 22 of file BinaryCNFMethod.h.

Member Typedef Documentation

◆ m_mapType

typedef std::map<std::pair<std::string, unsigned int>, Gate*> gsjj::passive::CNF::BinaryCNFMethod::m_mapType

protected

Definition at line 36 of file BinaryCNFMethod.h.

Constructor & Destructor Documentation

◆ BinaryCNFMethod() [1/2]

gsjj::passive::CNF::BinaryCNFMethod::BinaryCNFMethod ( )

delete

◆ ~BinaryCNFMethod()

gsjj::passive::CNF::BinaryCNFMethod::~BinaryCNFMethod ( )

virtual

Definition at line 40 of file BinaryCNFMethod.cpp.

◆ BinaryCNFMethod() [2/2]

gsjj::passive::CNF::BinaryCNFMethod::BinaryCNFMethod	(	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 21 of file BinaryCNFMethod.cpp.

Member Function Documentation

◆ constructDFA()

std::unique_ptr< DFA< char > > gsjj::passive::CNF::BinaryCNFMethod::constructDFA ( )

overridevirtual

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

Implements gsjj::passive::Method.

Definition at line 67 of file BinaryCNFMethod.cpp.

◆ createFormula()

Gate * gsjj::passive::CNF::BinaryCNFMethod::createFormula ( )

protectedvirtual

Definition at line 110 of file BinaryCNFMethod.cpp.

◆ createVariables()

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

protectedvirtual

Definition at line 101 of file BinaryCNFMethod.cpp.

◆ equal()

Gate * gsjj::passive::CNF::BinaryCNFMethod::equal	(	const std::string &	u,
		const std::string &	v
	)

protected

Definition at line 159 of file BinaryCNFMethod.cpp.

◆ getFactoryName()

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

static

Definition at line 93 of file BinaryCNFMethod.cpp.

◆ phi_different()

Gate * gsjj::passive::CNF::BinaryCNFMethod::phi_different	(	const std::string &	u,
		const std::string &	v
	)

protected

Definition at line 163 of file BinaryCNFMethod.cpp.

◆ phi_not_q_i()

Gate * gsjj::passive::CNF::BinaryCNFMethod::phi_not_q_i	(	const std::string &	u,
		unsigned int	i
	)

protected

Definition at line 184 of file BinaryCNFMethod.cpp.

◆ setStopTrigger()

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

overridevirtual

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.

Implements gsjj::passive::Method.

Definition at line 97 of file BinaryCNFMethod.cpp.

◆ solve()

bool gsjj::passive::CNF::BinaryCNFMethod::solve ( )

overridevirtual

Solves the SAT/SMT problem induced by the method.

Il also creates every variable and clause needed

Returns: True iff the problem is solvable

Implements gsjj::passive::Method.

Definition at line 44 of file BinaryCNFMethod.cpp.

◆ toDFA()

std::unique_ptr< DFA< char > > gsjj::passive::CNF::BinaryCNFMethod::toDFA ( ) const

protected

Definition at line 216 of file BinaryCNFMethod.cpp.

◆ toState()

unsigned int gsjj::passive::CNF::BinaryCNFMethod::toState ( const std::string & u ) const

protected

Definition at line 208 of file BinaryCNFMethod.cpp.

Member Data Documentation

◆ m_binarySize

unsigned int gsjj::passive::CNF::BinaryCNFMethod::m_binarySize

protected

$m = log_2(n)$

Definition at line 58 of file BinaryCNFMethod.h.

◆ m_simplify_opts

SimplifyOptions gsjj::passive::CNF::BinaryCNFMethod::m_simplify_opts

protected

Definition at line 54 of file BinaryCNFMethod.h.

◆ m_solver

std::unique_ptr<BC> gsjj::passive::CNF::BinaryCNFMethod::m_solver

protected

Definition at line 53 of file BinaryCNFMethod.h.

◆ m_stateToVar

m_mapType gsjj::passive::CNF::BinaryCNFMethod::m_stateToVar

protected

Definition at line 59 of file BinaryCNFMethod.h.

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

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

Public Member Functions

Static Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ m_mapType

Constructor & Destructor Documentation

◆ BinaryCNFMethod() [1/2]

◆ ~BinaryCNFMethod()

◆ BinaryCNFMethod() [2/2]

Member Function Documentation

◆ constructDFA()

◆ createFormula()

◆ createVariables()

◆ equal()

◆ getFactoryName()

◆ phi_different()

◆ phi_not_q_i()

◆ setStopTrigger()

◆ solve()

◆ toDFA()

◆ toState()

Member Data Documentation

◆ m_binarySize

◆ m_simplify_opts

◆ m_solver

◆ m_stateToVar