smtrat::SATModule< Settings >::ClauseInformation Struct Reference

Collaboration diagram for smtrat::SATModule< Settings >::ClauseInformation:

Public Member Functions
	ClauseInformation ()=delete
	ClauseInformation (int _position)
	ClauseInformation (const ClauseInformation &)=default
	ClauseInformation (ClauseInformation &&)=default
	~ClauseInformation ()
void	addOrigin (const FormulaT &_formula)
void	removeOrigin (const FormulaT &_formula)

Data Fields
bool	mStoredInSatisfied
int	mPosition
std::vector< FormulaT >	mOrigins

Detailed Description

template<class Settings>
struct smtrat::SATModule< Settings >::ClauseInformation

Definition at line 161 of file SATModule.h.

Constructor & Destructor Documentation

ClauseInformation() [1/4]

template<class Settings >

smtrat::SATModule< Settings >::ClauseInformation::ClauseInformation ( )

delete

ClauseInformation() [2/4]

template<class Settings >

smtrat::SATModule< Settings >::ClauseInformation::ClauseInformation ( int  _position )

inline

Definition at line 168 of file SATModule.h.

ClauseInformation() [3/4]

template<class Settings >

smtrat::SATModule< Settings >::ClauseInformation::ClauseInformation ( const ClauseInformation &  )

default

ClauseInformation() [4/4]

template<class Settings >

smtrat::SATModule< Settings >::ClauseInformation::ClauseInformation ( ClauseInformation &&  )

default

~ClauseInformation()

template<class Settings >

smtrat::SATModule< Settings >::ClauseInformation::~ClauseInformation ( )

inline

Definition at line 175 of file SATModule.h.

Member Function Documentation

addOrigin()

template<class Settings >

void smtrat::SATModule< Settings >::ClauseInformation::addOrigin ( const FormulaT &  _formula )

inline

Definition at line 177 of file SATModule.h.

removeOrigin()

template<class Settings >

void smtrat::SATModule< Settings >::ClauseInformation::removeOrigin ( const FormulaT &  _formula )

inline

Definition at line 182 of file SATModule.h.

Here is the call graph for this function:

Field Documentation

mOrigins

template<class Settings >

std::vector<FormulaT> smtrat::SATModule< Settings >::ClauseInformation::mOrigins

Definition at line 165 of file SATModule.h.

mPosition

template<class Settings >

int smtrat::SATModule< Settings >::ClauseInformation::mPosition

Definition at line 164 of file SATModule.h.

mStoredInSatisfied

template<class Settings >

bool smtrat::SATModule< Settings >::ClauseInformation::mStoredInSatisfied

Definition at line 163 of file SATModule.h.

---

The documentation for this struct was generated from the following file:

• smtrat-modules/SATModule/SATModule.h