Base class for classes that provide information about the structure of. More...

#include <info.h>

Public Member Functions
constexpr	Info (bool a_full, bool a_reverse)
	Constructor that initializes the rewriter.

Compare_Result	compare_guard (const data_expression &guard1, const data_expression &guard2, const std::vector< variable > &f_variables) const
	Compares two guards.

Compare_Result	compare_term (const data_expression &term1, const data_expression &term2) const
	Compares two terms.

std::size_t	get_number_of_arguments (const data_expression &a_term) const
	Returns the number of arguments of the main operator of a term.

data_expression	get_operator (const data_expression &term) const
	Returns the main operator of the term `term`;.

Static Public Member Functions
static bool	occurs (const data_expression &t1, const data_expression &t2)

Protected Member Functions
Compare_Result	lexico (const Compare_Result &a_result1, const Compare_Result &a_result2) const

Compare_Result	compare_address (const atermpp::aterm &term1, const atermpp::aterm &term2) const

double	get_guard_structure (const data_expression &guard, const std::vector< variable > &f_variables) const
	Returns an integer corresponding to the structure of the guard passed as argument `guard`.

Compare_Result	compare_guard_structure (const data_expression &guard1, const data_expression &guard2, const std::vector< variable > &f_variables) const
	Compares the structure of two guards.

Compare_Result	compare_guard_equality (const data_expression &guard1, const data_expression &guard2) const
	Compares two guards by their arguments.

Compare_Result	compare_term_free_variables (const data_expression &term1, const data_expression &term2) const

Compare_Result	compare_term_type (const data_expression &term1, const data_expression &term2) const
	Compares terms by their type.

Compare_Result	compare_term_occurs (const data_expression &term1, const data_expression &term2) const
	Compares terms by checking whether one is a part of the other.

Protected Attributes
const bool	f_full
	Flag indicating whether or not the arguments of equality functions are taken into account.

const bool	f_reverse
	Flag indicating whether or not the result of the comparison between the first two arguments.

Detailed Description

Base class for classes that provide information about the structure of.

data expressions in one of the internal formats of the rewriter.

Definition at line 31 of file info.h.

Constructor & Destructor Documentation

◆ Info()

constexpr mcrl2::data::detail::Info::Info	(	bool	a_full,
		bool	a_reverse
	)

inlineconstexpr

Constructor that initializes the rewriter.

Definition at line 181 of file info.h.

Member Function Documentation

◆ compare_address()

Compare_Result mcrl2::data::detail::Info::compare_address	(	const atermpp::aterm &	term1,
		const atermpp::aterm &	term2
	)		const

inlineprotected

Definition at line 51 of file info.h.

◆ compare_guard()

Compare_Result mcrl2::data::detail::Info::compare_guard	(	const data_expression &	guard1,
		const data_expression &	guard2,
		const std::vector< variable > &	f_variables
	)		const

inline

Compares two guards.

Definition at line 193 of file info.h.

◆ compare_guard_equality()

Compare_Result mcrl2::data::detail::Info::compare_guard_equality	(	const data_expression &	guard1,
		const data_expression &	guard2
	)		const

inlineprotected

Compares two guards by their arguments.

Definition at line 114 of file info.h.

◆ compare_guard_structure()

Compare_Result mcrl2::data::detail::Info::compare_guard_structure	(	const data_expression &	guard1,
		const data_expression &	guard2,
		const std::vector< variable > &	f_variables
	)		const

inlineprotected

Compares the structure of two guards.

Definition at line 100 of file info.h.

◆ compare_term()

Compare_Result mcrl2::data::detail::Info::compare_term	(	const data_expression &	term1,
		const data_expression &	term2
	)		const

inline

Compares two terms.

Definition at line 205 of file info.h.

◆ compare_term_free_variables()

Compare_Result mcrl2::data::detail::Info::compare_term_free_variables	(	const data_expression &	term1,
		const data_expression &	term2
	)		const

inlineprotected

Definition at line 136 of file info.h.

◆ compare_term_occurs()

Compare_Result mcrl2::data::detail::Info::compare_term_occurs	(	const data_expression &	term1,
		const data_expression &	term2
	)		const

inlineprotected

Compares terms by checking whether one is a part of the other.

Definition at line 166 of file info.h.

◆ compare_term_type()

Compare_Result mcrl2::data::detail::Info::compare_term_type	(	const data_expression &	term1,
		const data_expression &	term2
	)		const

inlineprotected

Compares terms by their type.

Definition at line 152 of file info.h.

◆ get_guard_structure()

double mcrl2::data::detail::Info::get_guard_structure	(	const data_expression &	guard,
		const std::vector< variable > &	f_variables
	)		const

inlineprotected

Returns an integer corresponding to the structure of the guard passed as argument guard.

Uses the ordering provided by f_variables.

Definition at line 68 of file info.h.

◆ get_number_of_arguments()

std::size_t mcrl2::data::detail::Info::get_number_of_arguments ( const data_expression & a_term ) const

inline

Returns the number of arguments of the main operator of a term.

Parameters

a_term An expression in the internal format of the rewriter with the jitty strategy.

Returns: 0, if aterm is a constant or a variable. The number of arguments of the main operator, otherwise.

Definition at line 223 of file info.h.

◆ get_operator()

data_expression mcrl2::data::detail::Info::get_operator ( const data_expression & term ) const

inline

Returns the main operator of the term term;.

Definition at line 236 of file info.h.

◆ lexico()

Compare_Result mcrl2::data::detail::Info::lexico	(	const Compare_Result &	a_result1,
		const Compare_Result &	a_result2
	)		const

inlineprotected

Definition at line 44 of file info.h.

◆ occurs()

static bool mcrl2::data::detail::Info::occurs	(	const data_expression &	t1,
		const data_expression &	t2
	)

inlinestatic

Definition at line 187 of file info.h.

Member Data Documentation

◆ f_full

const bool mcrl2::data::detail::Info::f_full

protected

Flag indicating whether or not the arguments of equality functions are taken into account.

when determining the order of expressions.

Definition at line 37 of file info.h.

◆ f_reverse

const bool mcrl2::data::detail::Info::f_reverse

protected

Flag indicating whether or not the result of the comparison between the first two arguments.

weighs stronger than the result of the comparison between the second pair of arguments of an

equation, when determining the order of expressions.

Definition at line 42 of file info.h.

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

data/include/mcrl2/data/detail/prover/info.h

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Info()

Member Function Documentation

◆ compare_address()

◆ compare_guard()

◆ compare_guard_equality()

◆ compare_guard_structure()

◆ compare_term()

◆ compare_term_free_variables()

◆ compare_term_occurs()

◆ compare_term_type()

◆ get_guard_structure()

◆ get_number_of_arguments()

◆ get_operator()

◆ lexico()

◆ occurs()

Member Data Documentation

◆ f_full

◆ f_reverse