#include <Condition.h>

Public Member Functions
	Condition (const smtrat::ConstraintT &, size_t _id, size_t=0, bool=false, const carl::PointerSet< Condition > &=carl::PointerSet< Condition >(), bool=false)

	Condition (const Condition &, size_t _id)

	Condition (const Condition &)=delete

	~Condition ()

bool &	rFlag () const

bool	flag () const

bool &	rRecentlyAdded () const

bool	recentlyAdded () const

size_t &	rValuation () const

size_t	valuation () const

size_t	id () const

const smtrat::ConstraintT &	constraint () const

carl::PointerSet< Condition > *	pOriginalConditions () const

const carl::PointerSet< Condition > &	originalConditions () const

double	valuate (const carl::Variable &, size_t, bool) const
	Valuates the constraint according to a variable (it possibly not contains). More...

bool	operator== (const Condition &) const
	Checks the equality of a given condition (right hand side) with this condition (left hand side). More...

bool	operator< (const Condition &) const
	Checks if the given condition (right hand side) is greater than this condition (left hand side). More...

void	print (std::ostream &=std::cout) const
	Prints the condition to an output stream. More...

Private Attributes
bool	mFlag

bool	mRecentlyAdded

size_t	mValuation

size_t	mId

smtrat::ConstraintT	mConstraint

carl::PointerSet< Condition > *	mpOriginalConditions

Static Private Attributes
static const double	INFINITLY_MANY_SOLUTIONS_WEIGHT = 2

Friends
std::ostream &	operator<< (std::ostream &_out, const Condition &_condition)

Detailed Description

Definition at line 20 of file Condition.h.

Constructor & Destructor Documentation

◆ Condition() [1/3]

smtrat::vs::Condition::Condition	(	const smtrat::ConstraintT &	_cons,
		size_t	_id,
		size_t	_val = `0`,
		bool	_flag = `false`,
		const carl::PointerSet< Condition > &	_oConds = `carl::PointerSet<Condition>()`,
		bool	_rAdded = `false`
	)

Definition at line 15 of file Condition.cpp.

◆ Condition() [2/3]

smtrat::vs::Condition::Condition	(	const Condition &	_cond,
		size_t	_id
	)

Definition at line 24 of file Condition.cpp.

◆ Condition() [3/3]

smtrat::vs::Condition::Condition ( const Condition & )

delete

◆ ~Condition()

smtrat::vs::Condition::~Condition ( )

Definition at line 33 of file Condition.cpp.

Member Function Documentation

◆ constraint()

const smtrat::ConstraintT& smtrat::vs::Condition::constraint ( ) const

inline

Definition at line 81 of file Condition.h.

Here is the caller graph for this function:

◆ flag()

bool smtrat::vs::Condition::flag ( ) const

inline

Definition at line 51 of file Condition.h.

Here is the caller graph for this function:

◆ id()

size_t smtrat::vs::Condition::id ( ) const

inline

Definition at line 76 of file Condition.h.

Here is the caller graph for this function:

◆ operator<()

bool smtrat::vs::Condition::operator< ( const Condition & _condition ) const

Checks if the given condition (right hand side) is greater than this condition (left hand side).

Parameters

_condition The condition to compare with (rhs).

Returns: true ,if the given substitution is greater than this substitution; false ,otherwise.

Definition at line 241 of file Condition.cpp.

Here is the call graph for this function:

◆ operator==()

bool smtrat::vs::Condition::operator== ( const Condition & _condition ) const

Checks the equality of a given condition (right hand side) with this condition (left hand side).

Parameters

_condition The condition to compare with (rhs).

Returns: true ,if the given condition is equal to this condition; false ,otherwise.

Definition at line 228 of file Condition.cpp.

Here is the call graph for this function:

◆ originalConditions()

const carl::PointerSet<Condition>& smtrat::vs::Condition::originalConditions ( ) const

inline

Definition at line 91 of file Condition.h.

Here is the caller graph for this function:

◆ pOriginalConditions()

carl::PointerSet<Condition>* smtrat::vs::Condition::pOriginalConditions ( ) const

inline

Definition at line 86 of file Condition.h.

Here is the caller graph for this function:

◆ print()

void smtrat::vs::Condition::print ( std::ostream & _out = std::cout ) const

Prints the condition to an output stream.

Parameters

_out	The output stream, where it should print.

Definition at line 257 of file Condition.cpp.

Here is the call graph for this function:

◆ recentlyAdded()

bool smtrat::vs::Condition::recentlyAdded ( ) const

inline

Definition at line 61 of file Condition.h.

Here is the caller graph for this function:

◆ rFlag()

bool& smtrat::vs::Condition::rFlag ( ) const

inline

Definition at line 46 of file Condition.h.

◆ rRecentlyAdded()

bool& smtrat::vs::Condition::rRecentlyAdded ( ) const

inline

Definition at line 56 of file Condition.h.

◆ rValuation()

size_t& smtrat::vs::Condition::rValuation ( ) const

inline

Definition at line 66 of file Condition.h.

Here is the caller graph for this function:

◆ valuate()

double smtrat::vs::Condition::valuate	(	const carl::Variable &	_consideredVariable,
		size_t	_maxNumberOfVars,
		bool	_preferEquation
	)		const

Valuates the constraint according to a variable (it possibly not contains).

Parameters

_consideredVariable	The variable which is considered in this valuation.
_maxNumberOfVars

Returns: A valuation of the constraint according to an heuristic.

Definition at line 49 of file Condition.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ valuation()

size_t smtrat::vs::Condition::valuation ( ) const

inline

Definition at line 71 of file Condition.h.

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<<	(	std::ostream &	_out,
		const Condition &	_condition
	)

friend

Definition at line 246 of file Condition.cpp.

Field Documentation

◆ INFINITLY_MANY_SOLUTIONS_WEIGHT

const double smtrat::vs::Condition::INFINITLY_MANY_SOLUTIONS_WEIGHT = 2

staticprivate

Definition at line 23 of file Condition.h.

◆ mConstraint

smtrat::ConstraintT smtrat::vs::Condition::mConstraint

private

Definition at line 31 of file Condition.h.

◆ mFlag

bool smtrat::vs::Condition::mFlag

mutableprivate

Definition at line 27 of file Condition.h.

◆ mId

size_t smtrat::vs::Condition::mId

private

Definition at line 30 of file Condition.h.

◆ mpOriginalConditions

carl::PointerSet<Condition>* smtrat::vs::Condition::mpOriginalConditions

private

Definition at line 32 of file Condition.h.

◆ mRecentlyAdded

bool smtrat::vs::Condition::mRecentlyAdded

mutableprivate

Definition at line 28 of file Condition.h.

◆ mValuation

size_t smtrat::vs::Condition::mValuation

mutableprivate

Definition at line 29 of file Condition.h.

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

smtrat-modules/VSModule/Condition.h
smtrat-modules/VSModule/Condition.cpp

Public Member Functions

Private Attributes

Static Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Condition() [1/3]

◆ Condition() [2/3]

◆ Condition() [3/3]

◆ ~Condition()

Member Function Documentation

◆ constraint()

◆ flag()

◆ id()

◆ operator<()

◆ operator==()

◆ originalConditions()

◆ pOriginalConditions()

◆ print()

◆ recentlyAdded()

◆ rFlag()

◆ rRecentlyAdded()

◆ rValuation()

◆ valuate()

◆ valuation()

Friends And Related Function Documentation

◆ operator<<

Field Documentation

◆ INFINITLY_MANY_SOLUTIONS_WEIGHT

◆ mConstraint

◆ mFlag

◆ mId

◆ mpOriginalConditions

◆ mRecentlyAdded

◆ mValuation