mCRL2
Loading...
Searching...
No Matches
mcrl2::data::linear_inequality Class Reference

#include <linear_inequalities.h>

Inheritance diagram for mcrl2::data::linear_inequality:
atermpp::aterm atermpp::aterm_core atermpp::unprotected_aterm_core

Public Member Functions

 linear_inequality ()
 Constructor yielding an inconsistent inequality.
 
 linear_inequality (const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t)
 Basic constructor.
 
 linear_inequality (const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r)
 constructor.
 
 linear_inequality (const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false)
 constructor.
 
 linear_inequality (const data_expression &e, const rewriter &r)
 Constructor that constructs a linear inequality out of a data expression.
 
detail::lhs_t::const_iterator lhs_begin () const
 
detail::lhs_t::const_iterator lhs_end () const
 
const detail::lhs_tlhs () const
 
const data_expressionrhs () const
 
data_expression get_factor_for_a_variable (const variable &x)
 
detail::comparison_t comparison () const
 
data_expression transform_to_data_expression () const
 
bool is_false (const rewriter &r) const
 
bool is_true (const rewriter &r) const
 
bool typical_pair (data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const
 Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn, d> where c2,...,cn, d are real constants.
 
linear_inequality invert (const rewriter &r)
 
void add_variables (std::set< variable > &variable_set) const
 
- 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.
 
atermoperator= (const aterm &other) noexcept=default
 
 aterm (aterm &&other) noexcept=default
 
atermoperator= (aterm &&other) noexcept=default
 
template<class ForwardIterator , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr>
 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 , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr>
 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 , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>
 aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)
 
 aterm (const function_symbol &sym)
 Constructor.
 
template<typename ... Terms>
 aterm (const function_symbol &symbol, const Terms &...arguments)
 Constructor for n-arity function application.
 
const function_symbolfunction () 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 atermoperator[] (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_coreoperator= (const aterm_core &other) noexcept
 Assignment operator.
 
aterm_coreassign (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_coreunprotected_assign (const aterm_core &other) noexcept
 Assignment operator, to be used when the busy flags do not need to be set.
 
aterm_coreoperator= (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.
 
bool operator!= (const unprotected_aterm_core &t) const
 Inequality operator on two unprotected aterms.
 
bool operator< (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool operator> (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool operator<= (const unprotected_aterm_core &t) const
 Comparison operator for two unprotected aterms.
 
bool 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_symbolfunction () const
 Yields the function symbol in an aterm.
 

Static Protected Member Functions

static void parse_and_store_expression (const data_expression &e, detail::map_based_lhs_t &new_lhs, data_expression &new_rhs, const rewriter &r, const bool negate=false, const data_expression &factor=real_one())
 

Additional Inherited Members

- Public Types inherited from atermpp::aterm
typedef std::size_t size_type
 An unsigned integral type.
 
typedef ptrdiff_t difference_type
 A signed integral type.
 
typedef term_appl_iterator< atermiterator
 Iterator used to iterate through an term_appl.
 
typedef term_appl_iterator< atermconst_iterator
 Const iterator used to iterate through an term_appl.
 
- Protected Member Functions inherited from atermpp::aterm
 aterm (detail::_term_appl *t)
 Constructor.
 
- Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_atermm_term
 

Detailed Description

Definition at line 556 of file linear_inequalities.h.

Constructor & Destructor Documentation

◆ linear_inequality() [1/5]

mcrl2::data::linear_inequality::linear_inequality ( )
inline

Constructor yielding an inconsistent inequality.

Definition at line 639 of file linear_inequalities.h.

◆ linear_inequality() [2/5]

mcrl2::data::linear_inequality::linear_inequality ( const detail::lhs_t lhs,
const data_expression r,
detail::comparison_t  t 
)
inline

Basic constructor.

Definition at line 644 of file linear_inequalities.h.

◆ linear_inequality() [3/5]

mcrl2::data::linear_inequality::linear_inequality ( const detail::lhs_t lhs,
const data_expression rhs,
detail::comparison_t  comparison,
const rewriter r 
)
inline

constructor.

Definition at line 655 of file linear_inequalities.h.

◆ linear_inequality() [4/5]

mcrl2::data::linear_inequality::linear_inequality ( const data_expression lhs,
const data_expression rhs,
const detail::comparison_t  comparison,
const rewriter r,
const bool  negate = false 
)
inline

constructor.

Definition at line 675 of file linear_inequalities.h.

◆ linear_inequality() [5/5]

mcrl2::data::linear_inequality::linear_inequality ( const data_expression e,
const rewriter r 
)
inline

Constructor that constructs a linear inequality out of a data expression.

The data expression e is expected to have the form lhs op rhs where op is one of <=,<,==,>,>= and lhs and rhs satisfy the syntax t ::= x | c*t | t*c | t+t | t-t | -t where x is a variable and c is a real constant.

Parameters
eContains the expression to become a linear inequality.
rA rewriter used to evaluate the expression.

Definition at line 723 of file linear_inequalities.h.

Member Function Documentation

◆ add_variables()

void mcrl2::data::linear_inequality::add_variables ( std::set< variable > &  variable_set) const
inline

Definition at line 900 of file linear_inequalities.h.

◆ comparison()

detail::comparison_t mcrl2::data::linear_inequality::comparison ( ) const
inline

Definition at line 787 of file linear_inequalities.h.

◆ get_factor_for_a_variable()

data_expression mcrl2::data::linear_inequality::get_factor_for_a_variable ( const variable x)
inline

Definition at line 782 of file linear_inequalities.h.

◆ invert()

linear_inequality mcrl2::data::linear_inequality::invert ( const rewriter r)
inline

Definition at line 877 of file linear_inequalities.h.

◆ is_false()

bool mcrl2::data::linear_inequality::is_false ( const rewriter r) const
inline

Definition at line 816 of file linear_inequalities.h.

◆ is_true()

bool mcrl2::data::linear_inequality::is_true ( const rewriter r) const
inline

Definition at line 823 of file linear_inequalities.h.

◆ lhs()

const detail::lhs_t & mcrl2::data::linear_inequality::lhs ( ) const
inline

Definition at line 772 of file linear_inequalities.h.

◆ lhs_begin()

detail::lhs_t::const_iterator mcrl2::data::linear_inequality::lhs_begin ( ) const
inline

Definition at line 762 of file linear_inequalities.h.

◆ lhs_end()

detail::lhs_t::const_iterator mcrl2::data::linear_inequality::lhs_end ( ) const
inline

Definition at line 767 of file linear_inequalities.h.

◆ parse_and_store_expression()

static void mcrl2::data::linear_inequality::parse_and_store_expression ( const data_expression e,
detail::map_based_lhs_t new_lhs,
data_expression new_rhs,
const rewriter r,
const bool  negate = false,
const data_expression factor = real_one() 
)
inlinestaticprotected

Definition at line 567 of file linear_inequalities.h.

◆ rhs()

const data_expression & mcrl2::data::linear_inequality::rhs ( ) const
inline

Definition at line 777 of file linear_inequalities.h.

◆ transform_to_data_expression()

data_expression mcrl2::data::linear_inequality::transform_to_data_expression ( ) const
inline

Definition at line 801 of file linear_inequalities.h.

◆ typical_pair()

bool mcrl2::data::linear_inequality::typical_pair ( data_expression lhs_expression,
data_expression rhs_expression,
detail::comparison_t comparison_operator,
const rewriter r 
) const
inline

Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn, d> where c2,...,cn, d are real constants.

Returns
The return value indicates whether the left and right hand side have been negated when yielding the typical pair.

Definition at line 833 of file linear_inequalities.h.


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