mcrl2/data/consistency.h

Include file:

#include "mcrl2/data/consistency.h"

This file contains some functions that are present in all libraries except the data library. In the data library they have different names, or are located in different namespaces. Note that this file can not be used everywhere, in particular not when people expose the sort_bool namespace.

Functions

data_expression mcrl2::data::and_(const data_expression &x, const data_expression &y)

Returns: The conjunction of x and y

sort_expression mcrl2::data::bool_()

Returns: The boolean sort

const data_expression &mcrl2::data::false_()

Returns: The expression false

data_expression mcrl2::data::imp(const data_expression &x, const data_expression &y)

Returns: The implication of x and y

bool mcrl2::data::is_and(const data_expression &x)

Test if x is a conjunction.

Parameters:

  • x a data expression

bool mcrl2::data::is_bool(const sort_expression &x)

Returns: Test if x is the boolean sort

bool mcrl2::data::is_equal_to(const data_expression &x)

Test if x is an equality.

Parameters:

  • x a data expression

bool mcrl2::data::is_false(const data_expression &x)

Test if x is false.

Parameters:

  • x a data expression

bool mcrl2::data::is_imp(const data_expression &x)

Test if x is an implication.

Parameters:

  • x a data expression

bool mcrl2::data::is_not(const data_expression &x)

Test if x is a negation.

Parameters:

  • x a data expression

bool mcrl2::data::is_not_equal_to(const data_expression &x)

Test if x is an inequality.

Parameters:

  • x a data expression

bool mcrl2::data::is_or(const data_expression &x)

Test if x is a disjunction.

Parameters:

  • x a data expression

bool mcrl2::data::is_true(const data_expression &x)

Test if x is true.

Parameters:

  • x a data expression

data_expression mcrl2::data::make_exists(const data::variable_list &v, const data_expression &x)

Make an existential quantification. It checks for an empty variable list, which is not allowed.

Parameters:

  • v A sequence of data variables

  • x A data expression

Returns: The value exists v.x

data_expression mcrl2::data::make_forall(const data::variable_list &v, const data_expression &x)

Make a universal quantification. It checks for an empty variable list, which is not allowed.

Parameters:

  • v A sequence of data variables

  • x A data expression

Returns: The value forall v.x

data_expression mcrl2::data::not_(const data_expression &x)

Returns: The negation of x

data_expression mcrl2::data::or_(const data_expression &x, const data_expression &y)

Returns: The disjunction of x and y

const data_expression &mcrl2::data::true_()

Returns: The expression true