smtrat::FormulaWithOrigins Class Reference

Stores a formula along with its origins. More...

#include <ModuleInput.h>

Collaboration diagram for smtrat::FormulaWithOrigins:

Public Member Functions
	FormulaWithOrigins ()
	FormulaWithOrigins (const FormulaT &_formula)
	Constructs a formula with empty origins. More...
	FormulaWithOrigins (const FormulaT &_formula, const std::shared_ptr< FormulasT > &_origins)
	Constructs a formula with the given origins. More...
	FormulaWithOrigins (const FormulaWithOrigins &)
const FormulaT &	formula () const
bool	hasOrigins () const
const FormulasT &	origins () const
void	setDeducted (bool _deducted) const
	Sets the deduction flag to the given value. More...
bool	deducted () const

Private Attributes
FormulaT	mFormula
	The formula. More...
std::shared_ptr< FormulasT >	mOrigins
	The formulas origins. More...
bool	mDeducted
	The deduction flag, which indicates, that this formula g is a direct sub-formula of a conjunction of formulas (and g f_1 . More...

Friends
class	ModuleInput
bool	operator< (const FormulaWithOrigins &_fwoA, const FormulaWithOrigins &_fwoB)
bool	operator== (const FormulaWithOrigins &_fwoA, const FormulaWithOrigins &_fwoB)

Detailed Description

Stores a formula along with its origins.

Definition at line 21 of file ModuleInput.h.

Constructor & Destructor Documentation

FormulaWithOrigins() [1/4]

smtrat::FormulaWithOrigins::FormulaWithOrigins

(

)

FormulaWithOrigins() [2/4]

smtrat::FormulaWithOrigins::FormulaWithOrigins ( const FormulaT &  _formula )

inline

Constructs a formula with empty origins.

Parameters

_formula

The formula of the formula with origins to construct.

Definition at line 42 of file ModuleInput.h.

FormulaWithOrigins() [3/4]

smtrat::FormulaWithOrigins::FormulaWithOrigins ( const FormulaT &  _formula, const std::shared_ptr< FormulasT > &  _origins  )

inline

Constructs a formula with the given origins.

Parameters

_formula	The formula of the formula with origins to construct.
_origins	The origins of the formula with origins to construct.

Definition at line 53 of file ModuleInput.h.

FormulaWithOrigins() [4/4]

smtrat::FormulaWithOrigins::FormulaWithOrigins

(

const FormulaWithOrigins &

)

Member Function Documentation

deducted()

bool smtrat::FormulaWithOrigins::deducted ( ) const

inline

Returns

The deduction flag, which indicates, that this formula g is a direct sub-formula of a conjunction of formulas (and g f_1 .. f_n), and, that (implies (and f_1 .. f_n) g) holds.

Definition at line 120 of file ModuleInput.h.

formula()

const FormulaT& smtrat::FormulaWithOrigins::formula ( ) const

inline

Returns

A constant reference to the formula.

Definition at line 86 of file ModuleInput.h.

Here is the caller graph for this function:

hasOrigins()

bool smtrat::FormulaWithOrigins::hasOrigins ( ) const

inline

Returns

true, if this sub-formula of the module input has origins.

Definition at line 94 of file ModuleInput.h.

origins()

const FormulasT& smtrat::FormulaWithOrigins::origins ( ) const

inline

Returns

A constant reference to the origins.

Definition at line 102 of file ModuleInput.h.

setDeducted()

void smtrat::FormulaWithOrigins::setDeducted ( bool  _deducted ) const

inline

Sets the deduction flag to the given value.

Parameters

_deducted

The value to set the deduction flag to.

Definition at line 111 of file ModuleInput.h.

Friends And Related Function Documentation

ModuleInput

friend class ModuleInput

friend

Definition at line 23 of file ModuleInput.h.

operator<

bool operator< ( const FormulaWithOrigins &  _fwoA, const FormulaWithOrigins &  _fwoB  )

friend

Parameters

_fwoA	The first formula with origins to compare.
_fwoB	The second formula with origins to compare.

Returns

true, if the formula of the first formula with origins is less than the formula of the second formula with origins; false, otherwise.

Definition at line 67 of file ModuleInput.h.

operator==

bool operator== ( const FormulaWithOrigins &  _fwoA, const FormulaWithOrigins &  _fwoB  )

friend

Parameters

_fwoA	The first formula with origins to compare.
_fwoB	The second formula with origins to compare.

Returns

true, if the formula of the first formula with origins and the formula of the second formula with origins are equal; false, otherwise.

Definition at line 78 of file ModuleInput.h.

Field Documentation

mDeducted

bool smtrat::FormulaWithOrigins::mDeducted

mutableprivate

The deduction flag, which indicates, that this formula g is a direct sub-formula of a conjunction of formulas (and g f_1 .

. f_n), and, that (implies (and f_1 .. f_n) g) holds.

Definition at line 32 of file ModuleInput.h.

mFormula

FormulaT smtrat::FormulaWithOrigins::mFormula

private

The formula.

Definition at line 27 of file ModuleInput.h.

mOrigins

std::shared_ptr<FormulasT> smtrat::FormulaWithOrigins::mOrigins

private

The formulas origins.

Definition at line 29 of file ModuleInput.h.

---

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

• smtrat-solver/ModuleInput.h