Represent a polynomial (in)equality against zero. More...

#include <Constraint.h>

Collaboration diagram for carl::Constraint< Pol >:

[legend]

Public Member Functions
	Constraint (bool valid=true)

	Constraint (carl::Variable::Arg var, Relation rel, const typename Pol::NumberType &bound=constant_zero< typename Pol::NumberType >::get())

	Constraint (const Pol &lhs, Relation rel)

	Constraint (const BasicConstraint< Pol > &constraint)

	Constraint (const Constraint &constraint)

	Constraint (Constraint &&constraint) noexcept

Constraint &	operator= (const Constraint &constraint)

Constraint &	operator= (Constraint &&constraint) noexcept

	operator const BasicConstraint< Pol > & () const

	operator BasicConstraint< Pol > () const

const BasicConstraint< Pol > &	constr () const
	Returns the associated BasicConstraint. More...

const Pol &	lhs () const

Relation	relation () const

size_t	hash () const

const auto &	variables () const

const Factors< Pol > &	lhs_factorization () const

template<bool gatherCoeff = false>
const VarInfo< Pol > &	var_info (const Variable variable) const

template<bool gatherCoeff = false>
const VarsInfo< Pol > &	var_info () const

unsigned	is_consistent () const
	Checks, whether the constraint is consistent. More...

Constraint	negation () const

uint	maxDegree (const Variable &_variable) const

uint	max_degree () const

Pol	coefficient (const Variable &_var, uint _degree) const
	Calculates the coefficient of the given variable with the given degree. More...

bool	integer_valued () const

bool	realValued () const

bool	hasIntegerValuedVariable () const
	Checks if this constraints contains an integer valued variable. More...

bool	hasRealValuedVariable () const
	Checks if this constraints contains an real valued variable. More...

bool	isPseudoBoolean () const
	Determines whether the constraint is pseudo-boolean. More...

Private Attributes
pool::PoolElement< CachedConstraintContent< Pol > >	m_element

Friends
template<typename P >
bool	operator== (const Constraint< P > &lhs, const Constraint< P > &rhs)

template<typename P >
bool	operator< (const Constraint< P > &lhs, const Constraint< P > &rhs)

template<typename P >
std::ostream &	operator<< (std::ostream &os, const Constraint< P > &c)

Detailed Description

template<typename Pol>
class carl::Constraint< Pol >

Represent a polynomial (in)equality against zero.

Such an (in)equality can be seen as an atomic formula/atom for the theory of real arithmetic.

Definition at line 62 of file Constraint.h.

Constructor & Destructor Documentation

◆ Constraint() [1/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint ( bool valid = true )

inlineexplicit

Definition at line 68 of file Constraint.h.

Here is the caller graph for this function:

◆ Constraint() [2/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint	(	carl::Variable::Arg	var,
		Relation	rel,
		const typename Pol::NumberType &	bound = `constant_zero<typename Pol::NumberType>::get()`
	)

inlineexplicit

Definition at line 70 of file Constraint.h.

◆ Constraint() [3/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint	(	const Pol &	lhs,
		Relation	rel
	)

inlineexplicit

Definition at line 72 of file Constraint.h.

◆ Constraint() [4/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint ( const BasicConstraint< Pol > & constraint )

inlineexplicit

Definition at line 74 of file Constraint.h.

◆ Constraint() [5/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint ( const Constraint< Pol > & constraint )

inline

Definition at line 76 of file Constraint.h.

◆ Constraint() [6/6]

template<typename Pol >

carl::Constraint< Pol >::Constraint ( Constraint< Pol > && constraint )

inlinenoexcept

Definition at line 78 of file Constraint.h.

Member Function Documentation

◆ coefficient()

template<typename Pol >

Pol carl::Constraint< Pol >::coefficient	(	const Variable &	_var,
		uint	_degree
	)		const

inline

Calculates the coefficient of the given variable with the given degree.

Note, that it only computes the coefficient once and stores the result.

Parameters

_var	The variable for which to calculate the coefficient.
_degree	The according degree of the variable for which to calculate the coefficient.

Returns: The ith coefficient of the given variable, where i is the given degree.

Definition at line 232 of file Constraint.h.

◆ constr()

template<typename Pol >

const BasicConstraint<Pol>& carl::Constraint< Pol >::constr ( ) const

inline

Returns the associated BasicConstraint.

Definition at line 101 of file Constraint.h.

Here is the caller graph for this function:

◆ hash()

template<typename Pol >

size_t carl::Constraint< Pol >::hash ( ) const

inline

Returns: A hash value for this constraint.

Definition at line 123 of file Constraint.h.

Here is the caller graph for this function:

◆ hasIntegerValuedVariable()

template<typename Pol >

bool carl::Constraint< Pol >::hasIntegerValuedVariable ( ) const

inline

Checks if this constraints contains an integer valued variable.

Returns: true, if it does; false, otherwise.

Definition at line 257 of file Constraint.h.

Here is the call graph for this function:

◆ hasRealValuedVariable()

template<typename Pol >

bool carl::Constraint< Pol >::hasRealValuedVariable ( ) const

inline

Checks if this constraints contains an real valued variable.

Returns: true, if it does; false, otherwise.

Definition at line 266 of file Constraint.h.

Here is the call graph for this function:

◆ integer_valued()

template<typename Pol >

bool carl::Constraint< Pol >::integer_valued ( ) const

inline

Returns: true, if it contains only integer valued variables.

Definition at line 241 of file Constraint.h.

Here is the call graph for this function:

◆ is_consistent()

template<typename Pol >

unsigned carl::Constraint< Pol >::is_consistent ( ) const

inline

Checks, whether the constraint is consistent.

It differs between, containing variables, consistent, and inconsistent.

Returns: 0, if the constraint is not consistent. 1, if the constraint is consistent. 2, if the constraint still contains variables.

Definition at line 194 of file Constraint.h.

Here is the caller graph for this function:

◆ isPseudoBoolean()

template<typename Pol >

bool carl::Constraint< Pol >::isPseudoBoolean ( ) const

inline

Determines whether the constraint is pseudo-boolean.

Returns: True if this constraint is pseudo-boolean. False otherwise.

Definition at line 275 of file Constraint.h.

Here is the call graph for this function:

◆ lhs()

template<typename Pol >

const Pol& carl::Constraint< Pol >::lhs ( ) const

inline

Returns: The considered polynomial being the left-hand side of this constraint. Hence, the right-hand side of any constraint is always 0.

Definition at line 109 of file Constraint.h.

Here is the caller graph for this function:

◆ lhs_factorization()

template<typename Pol >

const Factors<Pol>& carl::Constraint< Pol >::lhs_factorization ( ) const

inline

Definition at line 143 of file Constraint.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ max_degree()

template<typename Pol >

uint carl::Constraint< Pol >::max_degree ( ) const

inline

Returns: The maximal degree of all variables in this constraint. (Monomial-wise)

Definition at line 216 of file Constraint.h.

Here is the call graph for this function:

◆ maxDegree()

template<typename Pol >

uint carl::Constraint< Pol >::maxDegree ( const Variable & _variable ) const

inline

Parameters

_variable The variable for which to determine the maximal degree.

Returns: The maximal degree of the given variable in this constraint. (Monomial-wise)

Definition at line 208 of file Constraint.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ negation()

template<typename Pol >

Constraint carl::Constraint< Pol >::negation ( ) const

inline

Definition at line 198 of file Constraint.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator BasicConstraint< Pol >()

template<typename Pol >

carl::Constraint< Pol >::operator BasicConstraint< Pol > ( ) const

inline

Definition at line 94 of file Constraint.h.

◆ operator const BasicConstraint< Pol > &()

template<typename Pol >

carl::Constraint< Pol >::operator const BasicConstraint< Pol > & ( ) const

inline

Definition at line 90 of file Constraint.h.

◆ operator=() [1/2]

template<typename Pol >

Constraint& carl::Constraint< Pol >::operator= ( const Constraint< Pol > & constraint )

inline

Definition at line 80 of file Constraint.h.

◆ operator=() [2/2]

template<typename Pol >

Constraint& carl::Constraint< Pol >::operator= ( Constraint< Pol > && constraint )

inlinenoexcept

Definition at line 85 of file Constraint.h.

◆ realValued()

template<typename Pol >

bool carl::Constraint< Pol >::realValued ( ) const

inline

Returns: true, if it contains only real valued variables.

Definition at line 248 of file Constraint.h.

Here is the call graph for this function:

◆ relation()

template<typename Pol >

Relation carl::Constraint< Pol >::relation ( ) const

inline

Returns: The relation symbol of this constraint.

Definition at line 116 of file Constraint.h.

Here is the caller graph for this function:

◆ var_info() [1/2]

template<typename Pol >

template<bool gatherCoeff = false>

const VarsInfo<Pol>& carl::Constraint< Pol >::var_info ( ) const

inline

Definition at line 180 of file Constraint.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ var_info() [2/2]

template<typename Pol >

template<bool gatherCoeff = false>

const VarInfo<Pol>& carl::Constraint< Pol >::var_info ( const Variable variable ) const

inline

Parameters

variable The variable to find variable information for.

Template Parameters

gatherCoeff

Returns: The whole variable information object. Note, that if the given variable is not in this constraints, this method fails. Furthermore, the variable information returned do provide coefficients only, if the given flag gatherCoeff is set to true.

Definition at line 165 of file Constraint.h.

Here is the call graph for this function:

◆ variables()

template<typename Pol >

const auto& carl::Constraint< Pol >::variables ( ) const

inline

Returns: A container containing all variables occurring in the polynomial of this constraint.

Definition at line 130 of file Constraint.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ operator<

template<typename Pol >

template<typename P >

bool operator<	(	const Constraint< P > &	lhs,
		const Constraint< P > &	rhs
	)

friend

Definition at line 298 of file Constraint.h.

◆ operator<<

template<typename Pol >

template<typename P >

std::ostream& operator<<	(	std::ostream &	os,
		const Constraint< P > &	c
	)

friend

◆ operator==

template<typename Pol >

template<typename P >

bool operator==	(	const Constraint< P > &	lhs,
		const Constraint< P > &	rhs
	)

friend

Definition at line 288 of file Constraint.h.

Field Documentation

◆ m_element

template<typename Pol >

pool::PoolElement<CachedConstraintContent<Pol> > carl::Constraint< Pol >::m_element

private

Definition at line 65 of file Constraint.h.

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

carl-formula/arithmetic/Constraint.h

Public Member Functions

Private Attributes

Friends

Detailed Description

template<typename Pol> class carl::Constraint< Pol >

Constructor & Destructor Documentation

◆ Constraint() [1/6]

◆ Constraint() [2/6]

◆ Constraint() [3/6]

◆ Constraint() [4/6]

◆ Constraint() [5/6]

◆ Constraint() [6/6]

Member Function Documentation

◆ coefficient()

◆ constr()

◆ hash()

◆ hasIntegerValuedVariable()

◆ hasRealValuedVariable()

◆ integer_valued()

◆ is_consistent()

◆ isPseudoBoolean()

◆ lhs()

◆ lhs_factorization()

◆ max_degree()

◆ maxDegree()

◆ negation()

◆ operator BasicConstraint< Pol >()

◆ operator const BasicConstraint< Pol > &()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ realValued()

◆ relation()

◆ var_info() [1/2]

◆ var_info() [2/2]

◆ variables()

Friends And Related Function Documentation

◆ operator<

◆ operator<<

◆ operator==

Field Documentation

◆ m_element

template<typename Pol>
class carl::Constraint< Pol >