#include <linear_inequalities.h>

Inheritance diagram for mcrl2::data::detail::lhs_t:

Public Member Functions
	lhs_t ()
	Constructor.

	lhs_t (const aterm &t)
	Constructor from an aterm.

template<class ITERATOR >
	lhs_t (const ITERATOR begin, const ITERATOR end)
	Constructor.

template<class ITERATOR , class TRANSFORMER >
	lhs_t (const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
	Constructor.

lhs_t::const_iterator	find (const variable &v) const
	Give an iterator of the factor/variable pair for v, or end() if v does not occur.

lhs_t	erase (const variable &v) const
	Erase a variable and its factor.

const data_expression &	operator[] (const variable &v) const
	Give the factor of variable v.

std::size_t	count (const variable &v) const
	Give the factor of variable v.

template<IsSubstitution SubstitutionFunction>
data_expression	evaluate (const SubstitutionFunction &beta, const rewriter &r) const
	Evaluate the variables in this lhs_t according to the subsitution function.

data_expression	transform_to_data_expression () const

Public Member Functions inherited from atermpp::term_list< variable_with_a_rational_factor >
	term_list () noexcept
	Default constructor. Creates an empty list.

	term_list (const aterm &t) noexcept
	Constructor from an aterm.

	term_list (const term_list< variable_with_a_rational_factor > &t) noexcept
	Copy constructor.

	term_list (term_list< variable_with_a_rational_factor > &&t) noexcept
	Move constructor.

	term_list (Iter first, Iter last)
	Creates a term_list with the elements from first to last.

	term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm)
	Creates a term_list with the elements from first to last converting the elements before inserting.

	term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter)
	Creates a term_list with the elements from first to last, converting and filtering the list.

	term_list (Iter first, Iter last)
	Creates a term_list from the elements from first to last.

	term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm)
	Creates a term_list from the elements from first to last converting the elements before inserting.

	term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter)
	Creates a term_list from the elements from first to last converting and filtering the elements before inserting.

	term_list (R &&r)
	Creates a term_list from the elements in the range.

	term_list (std::initializer_list< variable_with_a_rational_factor > init)
	A constructor based on an initializer list.

term_list &	operator= (const term_list &other) noexcept=default
	This class has user-declared copy constructor so declare copy and move assignment.

term_list &	operator= (term_list &&other) noexcept=default

const term_list< variable_with_a_rational_factor > &	tail () const
	Returns the tail of the list.

void	pop_front ()
	Removes the first element of the list.

const variable_with_a_rational_factor &	front () const
	Returns the first element of the list.

void	push_front (const variable_with_a_rational_factor &el)
	Inserts a new element at the beginning of the current list.

void	emplace_front (Args &&... arguments)
	Construct and insert a new element at the beginning of the current list.

size_type	size () const
	Returns the size of the term_list.

bool	empty () const
	Returns true if the list's size is 0.

const_iterator	begin () const
	Returns a const_iterator pointing to the beginning of the term_list.

const_iterator	end () const
	Returns a const_iterator pointing to the end of the term_list.

const_reverse_iterator	rbegin () const
	Returns a const_reverse_iterator pointing to the end of the term_list.

const_reverse_iterator	rend () const
	Returns a const_iterator pointing to the end of the term_list.

size_type	max_size () const
	Returns the largest possible size of the term_list.

Public Member Functions inherited from atermpp::aterm
	aterm ()
	Default constructor.

	aterm (const aterm &other) noexcept=default
	This class has user-declared copy constructor so declare default copy and move operators.

aterm &	operator= (const aterm &other) noexcept=default

	aterm (aterm &&other) noexcept=default

aterm &	operator= (aterm &&other) noexcept=default

template<class ForwardIterator > requires (mcrl2::utilities::is_iterator<ForwardIterator>::value && !std::is_same_v<typename ForwardIterator::iterator_category, std::input_iterator_tag> && !std::is_same_v<typename ForwardIterator::iterator_category, std::output_iterator_tag>)
	aterm (const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
	Constructor that provides an aterm based on a function symbol and forward iterator providing the arguments.

template<class InputIterator > requires mcrl2::utilities::is_iterator<InputIterator>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end)
	Constructor that provides an aterm based on a function symbol and an input iterator providing the arguments.

template<class InputIterator , class TermConverter > requires mcrl2::utilities::is_iterator<InputIterator>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
	Constructor.

template<typename... Terms>
	aterm (const function_symbol &symbol, const Terms &... arguments)
	Constructor for n-arity function application.

const function_symbol &	function () const
	Returns the function symbol belonging to an aterm.

size_type	size () const
	Returns the number of arguments of this term.

bool	empty () const
	Returns true if the term has no arguments.

const_iterator	begin () const
	Returns an iterator pointing to the first argument.

const_iterator	end () const
	Returns a const_iterator pointing past the last argument.

constexpr size_type	max_size () const
	Returns the largest possible number of arguments.

const aterm &	operator[] (const size_type i) const
	Returns the i-th argument.

Public Member Functions inherited from atermpp::aterm_core
	aterm_core () noexcept
	Default constructor.

	~aterm_core () noexcept
	Standard destructor.

	aterm_core (const detail::_aterm *t) noexcept
	Constructor based on an internal term data structure. This is not for public use.

	aterm_core (const aterm_core &other) noexcept
	Copy constructor.

	aterm_core (aterm_core &&other) noexcept
	Move constructor.

aterm_core &	operator= (const aterm_core &other) noexcept
	Assignment operator.

aterm_core &	assign (const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
	Assignment operator, to be used if busy and forbidden flags are explicitly available.

template<bool CHECK_BUSY_FLAG = true>
aterm_core &	unprotected_assign (const aterm_core &other) noexcept
	Assignment operator, to be used when the busy flags do not need to be set.

aterm_core &	operator= (aterm_core &&other) noexcept
	Move assignment operator.

Public Member Functions inherited from atermpp::unprotected_aterm_core
	unprotected_aterm_core () noexcept
	Default constuctor.

	unprotected_aterm_core (const detail::_aterm *term) noexcept
	Constructor.

bool	type_is_appl () const noexcept
	Dynamic check whether the term is an aterm.

bool	type_is_int () const noexcept
	Dynamic check whether the term is an aterm_int.

bool	type_is_list () const noexcept
	Dynamic check whether the term is an aterm_list.

bool	operator== (const unprotected_aterm_core &t) const
	Comparison operator.

std::weak_ordering	operator<=> (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	defined () const
	Returns true if this term is not equal to the term assigned by the default constructor of aterms, aterm_appls and aterm_int.

void	swap (unprotected_aterm_core &t) noexcept
	Swaps this term with its argument.

const function_symbol &	function () const
	Yields the function symbol in an aterm.

Additional Inherited Members
Public Types inherited from atermpp::term_list< variable_with_a_rational_factor >
using	value_type = variable_with_a_rational_factor
	The type of object, T stored in the term_list.

using	pointer = variable_with_a_rational_factor *
	Pointer to T.

using	reference = variable_with_a_rational_factor &
	Reference to T.

using	const_reference = const variable_with_a_rational_factor &
	Const reference to T.

using	size_type = std::size_t
	An unsigned integral type.

using	difference_type = ptrdiff_t
	A signed integral type.

using	iterator = term_list_iterator< variable_with_a_rational_factor >
	Iterator used to iterate through an term_list.

using	const_iterator = term_list_iterator< variable_with_a_rational_factor >
	Const iterator used to iterate through an term_list.

using	const_reverse_iterator = reverse_term_list_iterator< variable_with_a_rational_factor >
	Const iterator used to iterate through an term_list.

Public Types inherited from atermpp::aterm
using	size_type = std::size_t
	An unsigned integral type.

using	difference_type = ptrdiff_t
	A signed integral type.

using	iterator = term_appl_iterator< aterm >
	Iterator used to iterate through an term_appl.

using	const_iterator = term_appl_iterator< aterm >
	Const iterator used to iterate through an term_appl.

Protected Member Functions inherited from atermpp::term_list< variable_with_a_rational_factor >
	term_list (detail::_aterm_appl<> *t) noexcept
	Constructor for term lists from internally constructed terms delivered as reference.

Protected Member Functions inherited from atermpp::aterm
	aterm (detail::_term_appl *t)
	Constructor.

Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_aterm *	m_term

Detailed Description

Definition at line 173 of file linear_inequalities.h.

Constructor & Destructor Documentation

◆ lhs_t() [1/4]

mcrl2::data::detail::lhs_t::lhs_t ( )

inline

Constructor.

Definition at line 177 of file linear_inequalities.h.

◆ lhs_t() [2/4]

mcrl2::data::detail::lhs_t::lhs_t ( const aterm & t )

inlineexplicit

Constructor from an aterm.

Definition at line 182 of file linear_inequalities.h.

◆ lhs_t() [3/4]

template<class ITERATOR >

mcrl2::data::detail::lhs_t::lhs_t	(	const ITERATOR	begin,
		const ITERATOR	end
	)

inline

Constructor.

Definition at line 188 of file linear_inequalities.h.

◆ lhs_t() [4/4]

template<class ITERATOR , class TRANSFORMER >

mcrl2::data::detail::lhs_t::lhs_t	(	const ITERATOR	begin,
		const ITERATOR	end,
		TRANSFORMER	f
	)

inline

Constructor.

Definition at line 194 of file linear_inequalities.h.

Member Function Documentation

◆ count()

std::size_t mcrl2::data::detail::lhs_t::count ( const variable & v ) const

inline

Give the factor of variable v.

Definition at line 233 of file linear_inequalities.h.

◆ erase()

lhs_t mcrl2::data::detail::lhs_t::erase ( const variable & v ) const

inline

Erase a variable and its factor.

Definition at line 208 of file linear_inequalities.h.

◆ evaluate()

template<IsSubstitution SubstitutionFunction>

data_expression mcrl2::data::detail::lhs_t::evaluate	(	const SubstitutionFunction &	beta,
		const rewriter &	r
	)		const

inline

Evaluate the variables in this lhs_t according to the subsitution function.

Definition at line 245 of file linear_inequalities.h.

◆ find()

lhs_t::const_iterator mcrl2::data::detail::lhs_t::find ( const variable & v ) const

inline

Give an iterator of the factor/variable pair for v, or end() if v does not occur.

Definition at line 199 of file linear_inequalities.h.

◆ operator[]()

const data_expression & mcrl2::data::detail::lhs_t::operator[] ( const variable & v ) const

inline

Give the factor of variable v.

Definition at line 222 of file linear_inequalities.h.

◆ transform_to_data_expression()

data_expression mcrl2::data::detail::lhs_t::transform_to_data_expression ( ) const

inline

Definition at line 266 of file linear_inequalities.h.

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

data/include/mcrl2/data/linear_inequalities.h

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ lhs_t() [1/4]

◆ lhs_t() [2/4]

◆ lhs_t() [3/4]

◆ lhs_t() [4/4]

Member Function Documentation

◆ count()

◆ erase()

◆ evaluate()

◆ find()

◆ operator[]()

◆ transform_to_data_expression()