#include <Substitution.h>

Public Types
enum	Type { NORMAL , PLUS_EPSILON , MINUS_INFINITY , PLUS_INFINITY , INVALID }
	The type of a substitution. More...

Public Member Functions
	Substitution (const carl::Variable &_variable, const Type &_type, carl::PointerSet< Condition > &&_oConditions, smtrat::ConstraintsT &&_sideCondition=smtrat::ConstraintsT())
	Constructs a substitution with no square root term to map to. More...

	Substitution (const carl::Variable &, const smtrat::SqrtEx &_term, const Type &_type, carl::PointerSet< Condition > &&_oConditions, smtrat::ConstraintsT &&_sideCondition=smtrat::ConstraintsT())
	Constructs a substitution with a square root term to map to. More...

	Substitution (const Substitution &_substitution)
	Copy constructor. More...

	~Substitution ()
	The destructor. More...

const carl::Variable &	variable () const

const smtrat::SqrtEx &	term () const

void	setTerm (const smtrat::Rational &_value)
	Sets the substitution term to the given rational. More...

Type &	rType ()

const Type &	type () const

carl::PointerSet< Condition > &	rOriginalConditions ()

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

const smtrat::ConstraintsT &	sideCondition () const

const carl::Variables &	termVariables () const

unsigned	valuate (bool _preferMinusInf=true) const

bool	operator== (const Substitution &) const

void	print (bool _withOrigins=false, bool _withSideConditions=false, std::ostream &_out=std::cout, const std::string &_init="") const
	Prints this substitution on the given stream, with some additional information. More...

Private Attributes
carl::Variable	mVariable
	The variable to substitute. More...

smtrat::SqrtEx *	mpTerm
	The pointer (if != NULL) to the square root term to substitute the variable for. More...

Type	mType
	The type. More...

carl::Variables *	mpTermVariables
	The variables occurring in the term to substitute for. More...

carl::PointerSet< Condition >	mOriginalConditions
	The conditions from which this substitution has been originated. (e.g. [x -> 2] could have had the origins {x-2<=0, x^2-4=0}) More...

smtrat::ConstraintsT	mSideCondition
	The side conditions, which have to hold to make this substitution valid. (e.g. [x -> 1/a] has the side condition {a!=0}) More...

Detailed Description

Definition at line 19 of file Substitution.h.

Member Enumeration Documentation

◆ Type

enum smtrat::vs::Substitution::Type

The type of a substitution.

Enumerator
NORMAL
PLUS_EPSILON
MINUS_INFINITY
PLUS_INFINITY
INVALID

Definition at line 23 of file Substitution.h.

Constructor & Destructor Documentation

◆ Substitution() [1/3]

smtrat::vs::Substitution::Substitution	(	const carl::Variable &	_variable,
		const Type &	_type,
		carl::PointerSet< Condition > &&	_oConditions,
		smtrat::ConstraintsT &&	_sideCondition = `smtrat::ConstraintsT()`
	)

Constructs a substitution with no square root term to map to.

Parameters

_variable	The variable to substitute of the substitution to construct.
_type	The type of the substitution of the substitution to construct.
_oConditions	The original conditions of the substitution to construct.
_sideCondition	The side conditions of the substitution to construct.

Definition at line 13 of file Substitution.cpp.

◆ Substitution() [2/3]

smtrat::vs::Substitution::Substitution	(	const carl::Variable &	_variable,
		const smtrat::SqrtEx &	_term,
		const Type &	_type,
		carl::PointerSet< Condition > &&	_oConditions,
		smtrat::ConstraintsT &&	_sideCondition = `smtrat::ConstraintsT()`
	)

Constructs a substitution with a square root term to map to.

Parameters

_variable	The variable to substitute of the substitution to construct.
_term	The square root term to which the variable maps to.
_type	The type of the substitution of the substitution to construct.
_oConditions	The original conditions of the substitution to construct.
_sideCondition	The side conditions of the substitution to construct.

Definition at line 28 of file Substitution.cpp.

◆ Substitution() [3/3]

smtrat::vs::Substitution::Substitution ( const Substitution & _substitution )

Copy constructor.

Definition at line 43 of file Substitution.cpp.

◆ ~Substitution()

smtrat::vs::Substitution::~Substitution ( )

The destructor.

Definition at line 52 of file Substitution.cpp.

Member Function Documentation

◆ operator==()

bool smtrat::vs::Substitution::operator== ( const Substitution & _substitution ) const

Parameters

The	substitution to compare with.

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

Definition at line 141 of file Substitution.cpp.

Here is the call graph for this function:

◆ originalConditions()

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

inline

Returns: A constant reference to the original conditions of this substitution.

Definition at line 126 of file Substitution.h.

Here is the caller graph for this function:

◆ print()

void smtrat::vs::Substitution::print	(	bool	_withOrigins = `false`,
		bool	_withSideConditions = `false`,
		std::ostream &	_out = `std::cout`,
		const std::string &	_init = `""`
	)		const

Prints this substitution on the given stream, with some additional information.

Parameters

The	substitution to compare with.

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

Parameters

_withOrigins	A flag indicating whether to print also the origins of this substitution.
_withSideConditions	A flag indication whether to also the side conditions of this substitution.
_out	The stream to print on.
_init	The string to print at the beginning of every row.

Definition at line 184 of file Substitution.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ rOriginalConditions()

carl::PointerSet<Condition>& smtrat::vs::Substitution::rOriginalConditions ( )

inline

Returns: A reference to the original conditions of this substitution.

Definition at line 118 of file Substitution.h.

Here is the caller graph for this function:

◆ rType()

Type& smtrat::vs::Substitution::rType ( )

inline

Returns: A reference to the type of this substitution.

Definition at line 102 of file Substitution.h.

◆ setTerm()

void smtrat::vs::Substitution::setTerm ( const smtrat::Rational & _value )

inline

Sets the substitution term to the given rational.

Parameters

_value The value to set the substitution term to.

Definition at line 92 of file Substitution.h.

◆ sideCondition()

const smtrat::ConstraintsT& smtrat::vs::Substitution::sideCondition ( ) const

inline

Returns: A constant reference to the side condition of this substitution.

Definition at line 134 of file Substitution.h.

Here is the caller graph for this function:

◆ term()

const smtrat::SqrtEx& smtrat::vs::Substitution::term ( ) const

inline

Returns: A constant reference to the term this substitution maps its variable to.

Definition at line 83 of file Substitution.h.

Here is the caller graph for this function:

◆ termVariables()

const carl::Variables& smtrat::vs::Substitution::termVariables ( ) const

inline

Returns: A constant reference to the variables occurring in the substitution term.

Definition at line 142 of file Substitution.h.

Here is the caller graph for this function:

◆ type()

const Type& smtrat::vs::Substitution::type ( ) const

inline

Returns: A constant reference to the type of this substitution.

Definition at line 110 of file Substitution.h.

Here is the caller graph for this function:

◆ valuate()

unsigned smtrat::vs::Substitution::valuate ( bool _preferMinusInf = true ) const

Parameters

_preferMinusInf A flag indicating whether to valuate the substitution type best or otherwise worst.

Returns: The valuation of this substitution according to a heuristic.

Definition at line 59 of file Substitution.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ variable()

const carl::Variable& smtrat::vs::Substitution::variable ( ) const

inline

Returns: A constant reference to the variable this substitution substitutes.

Definition at line 75 of file Substitution.h.

Here is the caller graph for this function:

Field Documentation

◆ mOriginalConditions

carl::PointerSet<Condition> smtrat::vs::Substitution::mOriginalConditions

private

The conditions from which this substitution has been originated. (e.g. [x -> 2] could have had the origins {x-2<=0, x^2-4=0})

Definition at line 37 of file Substitution.h.

◆ mpTerm

smtrat::SqrtEx* smtrat::vs::Substitution::mpTerm

private

The pointer (if != NULL) to the square root term to substitute the variable for.

Definition at line 31 of file Substitution.h.

◆ mpTermVariables

carl::Variables* smtrat::vs::Substitution::mpTermVariables

mutableprivate

The variables occurring in the term to substitute for.

Definition at line 35 of file Substitution.h.

◆ mSideCondition

smtrat::ConstraintsT smtrat::vs::Substitution::mSideCondition

private

The side conditions, which have to hold to make this substitution valid. (e.g. [x -> 1/a] has the side condition {a!=0})

Definition at line 39 of file Substitution.h.

◆ mType

Type smtrat::vs::Substitution::mType

private

The type.

Definition at line 33 of file Substitution.h.

◆ mVariable

carl::Variable smtrat::vs::Substitution::mVariable

private

The variable to substitute.

Definition at line 29 of file Substitution.h.

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

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

Public Types

Public Member Functions

Private Attributes

Detailed Description

Member Enumeration Documentation

◆ Type

Constructor & Destructor Documentation

◆ Substitution() [1/3]

◆ Substitution() [2/3]

◆ Substitution() [3/3]

◆ ~Substitution()

Member Function Documentation

◆ operator==()

◆ originalConditions()

◆ print()

◆ rOriginalConditions()

◆ rType()

◆ setTerm()

◆ sideCondition()

◆ term()

◆ termVariables()

◆ type()

◆ valuate()

◆ variable()

Field Documentation

◆ mOriginalConditions

◆ mpTerm

◆ mpTermVariables

◆ mSideCondition

◆ mType

◆ mVariable