Base class for every method that relies on a non-CNF SAT solver. More...

#include <SATNonCNFMethod.h>

Inheritance diagram for gsjj::passive::NonCNF::SATNonCNFMethod:

[legend]

Collaboration diagram for gsjj::passive::NonCNF::SATNonCNFMethod:

Public Member Functions
	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...

Protected Member Functions
virtual std::string	getFileName () const =0
	Gives the name of the file in which the boolean formula must be written. More...

bool	isSatisfiable () const
	Reads the output of the SAT solver and checks if the formula was satisfiable or not. More...

virtual bool	createFormula (std::ostream &stream)=0
	Creates the boolean formula (must not be in CNF) and writes it in the stream. More...

virtual std::unique_ptr< DFA< char > >	toDFA (std::istream &stream) const =0
	Effectively creates the DFA. 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...

Protected Attributes
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

Detailed Description

Base class for every method that relies on a non-CNF SAT solver.

It creates a non-CNF SAT solver

Definition at line 26 of file SATNonCNFMethod.h.

Constructor & Destructor Documentation

◆ SATNonCNFMethod() [1/2]

gsjj::passive::NonCNF::SATNonCNFMethod::SATNonCNFMethod ( )

delete

◆ ~SATNonCNFMethod()

gsjj::passive::NonCNF::SATNonCNFMethod::~SATNonCNFMethod ( )

virtual

Definition at line 18 of file SATNonCNFMethod.cpp.

◆ SATNonCNFMethod() [2/2]

gsjj::passive::NonCNF::SATNonCNFMethod::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

Definition at line 13 of file SATNonCNFMethod.cpp.

Member Function Documentation

◆ constructDFA()

std::unique_ptr< DFA< char > > gsjj::passive::NonCNF::SATNonCNFMethod::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 53 of file SATNonCNFMethod.cpp.

◆ createFormula()

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

protectedpure virtual

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

Implemented in gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod, gsjj::passive::NonCNF::BinaryNonCNFMethod, and gsjj::passive::NonCNF::UnaryNonCNFMethod.

◆ getFileName()

virtual std::string gsjj::passive::NonCNF::SATNonCNFMethod::getFileName ( ) const

protectedpure virtual

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

Returns: The name of the file

Implemented in gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod, gsjj::passive::NonCNF::BinaryNonCNFMethod, and gsjj::passive::NonCNF::UnaryNonCNFMethod.

◆ isSatisfiable()

bool gsjj::passive::NonCNF::SATNonCNFMethod::isSatisfiable ( ) const

protected

Reads the output of the SAT solver and checks if the formula was satisfiable or not.

Returns: True iff the formula was satisfiable

Definition at line 80 of file SATNonCNFMethod.cpp.

◆ setStopTrigger()

void gsjj::passive::NonCNF::SATNonCNFMethod::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 76 of file SATNonCNFMethod.cpp.

◆ solve()

bool gsjj::passive::NonCNF::SATNonCNFMethod::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 22 of file SATNonCNFMethod.cpp.

◆ toDFA()

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

protectedpure virtual

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

Implemented in gsjj::passive::NonCNF::HeuleVerwerNonCNFMethod, gsjj::passive::NonCNF::BinaryNonCNFMethod, and gsjj::passive::NonCNF::UnaryNonCNFMethod.

Member Data Documentation

◆ mustStop

const bool* gsjj::passive::NonCNF::SATNonCNFMethod::mustStop

protected

Definition at line 67 of file SATNonCNFMethod.h.

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

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

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ SATNonCNFMethod() [1/2]

◆ ~SATNonCNFMethod()

◆ SATNonCNFMethod() [2/2]

Member Function Documentation

◆ constructDFA()

◆ createFormula()

◆ getFileName()

◆ isSatisfiable()

◆ setStopTrigger()

◆ solve()

◆ toDFA()

Member Data Documentation

◆ mustStop