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

Stores all information regarding a Boolean abstraction of a constraint. More...

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

Public Member Functions
	Abstraction (ModuleInput::iterator _position, const FormulaT &_reabstraction)
	Constructs abstraction information, for a literal which does actually not belong to an abstraction. More...
	Abstraction (const Abstraction &)=delete

Data Fields
bool	consistencyRelevant
	A flag, which is set to false, if the constraint corresponding to the abstraction does not occur in the received formula and, hence, does not need to be part of a consistency check. More...
bool	isDeduction
	A flag, which is set to false, if the constraint corresponding to the abstraction is redundant and hence there is no need to include it to a consistency check. More...
int	updateInfo
	<0, if the corresponding constraint must still be added to the passed formula; >0, if the corresponding constraint must still be removed to the passed formula; 0, otherwise. More...
bool	updatedReabstraction
ModuleInput::iterator	position
	The position of the corresponding constraint in the passed formula. More...
FormulaT	reabstraction
	The constraint corresponding to this abstraction. More...
std::shared_ptr< std::vector< FormulaT > >	origins

Detailed Description

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

Stores all information regarding a Boolean abstraction of a constraint.

Definition at line 105 of file SATModule.h.

Constructor & Destructor Documentation

Abstraction() [1/2]

template<class Settings >

smtrat::SATModule< Settings >::Abstraction::Abstraction ( ModuleInput::iterator  _position, const FormulaT &  _reabstraction  )

inline

Constructs abstraction information, for a literal which does actually not belong to an abstraction.

Parameters

_position	The end of the passed formula of this module.
_constraint	The constraint to abstract.

Definition at line 148 of file SATModule.h.

Abstraction() [2/2]

template<class Settings >

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

delete

Field Documentation

consistencyRelevant

template<class Settings >

bool smtrat::SATModule< Settings >::Abstraction::consistencyRelevant

A flag, which is set to false, if the constraint corresponding to the abstraction does not occur in the received formula and, hence, does not need to be part of a consistency check.

Definition at line 111 of file SATModule.h.

isDeduction

template<class Settings >

bool smtrat::SATModule< Settings >::Abstraction::isDeduction

A flag, which is set to false, if the constraint corresponding to the abstraction is redundant and hence there is no need to include it to a consistency check.

(NOT YET USED)

Definition at line 117 of file SATModule.h.

origins

template<class Settings >

std::shared_ptr<std::vector<FormulaT> > smtrat::SATModule< Settings >::Abstraction::origins

Definition at line 141 of file SATModule.h.

position

template<class Settings >

ModuleInput::iterator smtrat::SATModule< Settings >::Abstraction::position

The position of the corresponding constraint in the passed formula.

It points to the end if the constraint is not part of the passed formula.

Definition at line 132 of file SATModule.h.

reabstraction

template<class Settings >

FormulaT smtrat::SATModule< Settings >::Abstraction::reabstraction

The constraint corresponding to this abstraction.

It is NULL, if the literal for which we store this abstraction does actually not belong to an abstraction.

Definition at line 138 of file SATModule.h.

updatedReabstraction

template<class Settings >

bool smtrat::SATModule< Settings >::Abstraction::updatedReabstraction

Definition at line 126 of file SATModule.h.

updateInfo

template<class Settings >

int smtrat::SATModule< Settings >::Abstraction::updateInfo

<0, if the corresponding constraint must still be added to the passed formula; >0, if the corresponding constraint must still be removed to the passed formula; 0, otherwise.

Definition at line 124 of file SATModule.h.

---

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

• smtrat-modules/SATModule/SATModule.h