mcrl2/data/standard_utility.h

Include file:

#include "mcrl2/data/standard_utility.h"

Provides utilities for working with data expressions of standard sorts.

Functions

bool mcrl2::data::is_system_defined(const sort_expression &s)

Returns true iff the expression represents a standard sort.

Parameters:

  • s a sort expression.

std::list<data_expression> mcrl2::data::split_conjunction(const data_expression &condition)

Split a disjunctive expression into a set of clauses.

std::list<data_expression> mcrl2::data::split_disjunction(const data_expression &condition)

Split a disjunctive expression into a set of clauses.

Functions

data_expression mcrl2::data::lazy::and_(data_expression const &p, data_expression const &q)

Returns an expression equivalent to p or q.

Parameters:

  • p A data expression

  • q A data expression

Returns: The value p || q

data_expression mcrl2::data::lazy::equal_to(data_expression const &p, data_expression const &q)

Returns an expression equivalent to p == q.

Parameters:

  • p A data expression

  • q A data expression

Returns: The value p == q

data_expression mcrl2::data::lazy::implies(data_expression const &p, data_expression const &q)

Returns an expression equivalent to p implies q.

Parameters:

  • p A data expression

  • q A data expression

Returns: The value p || q

data_expression mcrl2::data::lazy::join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)

Returns and applied to the sequence of data expressions [first, last)

Parameters:

  • first Start of a sequence of data expressions

  • last End of a sequence of data expressions

Returns: And applied to the sequence of data expressions [first, last)

data_expression mcrl2::data::lazy::join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)

Returns or applied to the sequence of data expressions [first, last)

Parameters:

  • first Start of a sequence of data expressions

  • last End of a sequence of data expressions

Returns: Or applied to the sequence of data expressions [first, last)

data_expression mcrl2::data::lazy::not_(data_expression const &p)

Returns an expression equivalent to not p.

Parameters:

  • p A data expression

Returns: The value !p

data_expression mcrl2::data::lazy::not_equal_to(data_expression const &p, data_expression const &q)

Returns an expression equivalent to p == q.

Parameters:

  • p A data expression

  • q A data expression

Returns: The value ! p == q

data_expression mcrl2::data::lazy::or_(data_expression const &p, data_expression const &q)

Returns an expression equivalent to p and q.

Parameters:

  • p A data expression

  • q A data expression

Returns: The value p && q

Functions

data_expression mcrl2::data::sort_bool::bool_(bool b)

Constructs expression of type Bool from an integral type.

Parameters:

  • b A Boolean

bool mcrl2::data::sort_bool::is_boolean_constant(data_expression const &b)

Determines whether b is a Boolean constant.

Parameters:

  • b A data expression