Contains utility functions for linear inequalities. More...

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.

namespace	mcrl2::data
	Namespace for all data library functionality.

namespace	mcrl2::data::detail

Functions
data_expression	mcrl2::data::detail::negate_inequality (const data_expression &e)

bool	mcrl2::data::detail::is_inequality (const data_expression &e)
	Determine whether a data expression is an inequality.

const data_expression &	mcrl2::data::detail::condition_part (const data_expression &e)

const data_expression &	mcrl2::data::detail::then_part (const data_expression &e)

const data_expression &	mcrl2::data::detail::else_part (const data_expression &e)

static bool	mcrl2::data::detail::split_condition_aux (const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression_list > &non_real_conditions, const bool negate=false)
	Splits a condition in expressions ranging over reals and the others.

void	mcrl2::data::detail::split_condition (const data_expression &e, std::vector< data_expression_list > &real_conditions, std::vector< data_expression > &non_real_conditions)
	This function first splits the given condition e into real conditions and non real conditions. \detail This function first uses split_condition_aux to split the condition e. Then.

Detailed Description

Contains utility functions for linear inequalities.

Namespaces