mcrl2::data::cardinality_calculator Class Reference

#include <cardinality.h>

Public Member Functions
	cardinality_calculator (const data_specification &specification, const rewriter &r)
std::size_t	operator() (const sort_expression &s) const
	Counts the number of elements in a sort.

Protected Member Functions
bool	is_a_new_unique_element (const data_expression &t, const std::vector< data_expression > already_found_elements, bool &determined) const

Protected Attributes
const data_specification &	m_specification
const rewriter &	m_rewriter

Detailed Description

Definition at line 22 of file cardinality.h.

Constructor & Destructor Documentation

cardinality_calculator()

mcrl2::data::cardinality_calculator::cardinality_calculator ( const data_specification &  specification, const rewriter &  r  )

inline

Definition at line 57 of file cardinality.h.

Member Function Documentation

is_a_new_unique_element()

bool mcrl2::data::cardinality_calculator::is_a_new_unique_element ( const data_expression &  t, const std::vector< data_expression >  already_found_elements, bool &  determined  ) const

inlineprotected

Definition at line 31 of file cardinality.h.

operator()()

std::size_t mcrl2::data::cardinality_calculator::operator() ( const sort_expression &  s ) const

inline

Counts the number of elements in a sort.

The returned value is either the number of elements, or zero if the number of elements cannot be determined, or is infinite.

Parameters

s	The sort expression to be determined.

Definition at line 66 of file cardinality.h.

Member Data Documentation

m_rewriter

const rewriter& mcrl2::data::cardinality_calculator::m_rewriter

protected

Definition at line 27 of file cardinality.h.

m_specification

const data_specification& mcrl2::data::cardinality_calculator::m_specification

protected

Definition at line 26 of file cardinality.h.

---

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

• data/include/mcrl2/data/cardinality.h