Functions for handling Expression Types. More...

Macros
#define	NUXMV_VALID_EXPR_TYPE(expr_type) ((expr_type).repr != NULL)
	Valid expression type.

Functions
nuxmv_expr_type	nuxmv_make_boolean_type (nuxmv_env env)
	Create a Boolean type.

nuxmv_expr_type	nuxmv_make_integer_type (nuxmv_env env)
	Create an integer type.

nuxmv_expr_type	nuxmv_make_real_type (nuxmv_env env)
	Create a real type.

nuxmv_expr_type	nuxmv_make_enum_type (nuxmv_env env)
	Create an enumerative type whose variants are symbolic tags.

nuxmv_expr_type	nuxmv_make_set_type (nuxmv_env env, nuxmv_expr_type elem)
	Create a set type.

nuxmv_expr_type	nuxmv_make_signed_word_type (nuxmv_env env, size_t width)
	Create a signed word type.

nuxmv_expr_type	nuxmv_make_unsigned_word_type (nuxmv_env env, size_t width)
	Create an unsigned word type.

nuxmv_expr_type	nuxmv_make_array_type (nuxmv_env env, nuxmv_expr_type idx, nuxmv_expr_type elem)
	Create an array type.

nuxmv_expr_type	nuxmv_make_function_type (nuxmv_env env, const nuxmv_expr_type *args, size_t arg_num, nuxmv_expr_type result)
	Create a new (uninterpreted) function type.

nuxmv_expr_type_tag	nuxmv_expr_type_get_tag (nuxmv_env env, nuxmv_expr_type type)
	Get the tag of a type.

size_t	nuxmv_expr_type_get_id (nuxmv_env env, nuxmv_expr_type type)
	Get the ID of a type.

int	nuxmv_word_type_get_width (nuxmv_env env, nuxmv_expr_type type)
	Get the width of a (un)signed word type.

nuxmv_expr_type	nuxmv_array_type_get_index (nuxmv_env env, nuxmv_expr_type type)
	Get the type of the index of an array type.

nuxmv_expr_type	nuxmv_array_type_get_element (nuxmv_env env, nuxmv_expr_type type)
	Get the type of the elements of an array type.

int	nuxmv_function_type_get_argument_num (nuxmv_env env, nuxmv_expr_type type)
	Get the number of arguments of a function type.

nuxmv_expr_type	nuxmv_function_type_get_argument (nuxmv_env env, nuxmv_expr_type type, int arg_idx)
	Get the i-th argument type of a function type.

nuxmv_expr_type	nuxmv_function_type_get_result (nuxmv_env env, nuxmv_expr_type type)
	Get the type of the result of a function type.

nuxmv_expr_type	nuxmv_set_type_get_element (nuxmv_env env, nuxmv_expr_type type)
	Get the type of the elements of a set type.

Detailed Description

Functions for handling Expression Types.

Macro Definition Documentation

◆ NUXMV_VALID_EXPR_TYPE

#define NUXMV_VALID_EXPR_TYPE ( expr_type ) ((expr_type).repr != NULL)

Valid expression type.

This macro checks whether type is a valid nuxmv_expr_type.

Parameters

[in] expr_type The expression type to inspect.

Returns: true if the option is valid, false otherwise.

Function Documentation

◆ nuxmv_array_type_get_element()

nuxmv_expr_type nuxmv_array_type_get_element	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the type of the elements of an array type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The array type to extract the element type from.

Returns: The type of the elements. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_array_type_get_index()

nuxmv_expr_type nuxmv_array_type_get_index	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the type of the index of an array type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The array type to extract the index type from.

Returns: The type of the index. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_expr_type_get_id()

size_t nuxmv_expr_type_get_id	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the ID of a type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The expression type to extract the ID from.

Returns: The ID of the type, which is a positive integer that is unique in the given environment. 0 is returned in case of error.

◆ nuxmv_expr_type_get_tag()

nuxmv_expr_type_tag nuxmv_expr_type_get_tag	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the tag of a type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The expression type to extract the tag from.

Returns: The tag of the expression, NUXMV_TYPE_INVALID in case of error.

See also

nuxmv_env_get_last_error_message()

Requirements: 03.001.03

◆ nuxmv_function_type_get_argument()

nuxmv_expr_type nuxmv_function_type_get_argument	(	nuxmv_env	env,
		nuxmv_expr_type	type,
		int	arg_idx
	)

Get the i-th argument type of a function type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The function type to extract the argument type from.
[in]	arg_idx	The index of the argument counting from 0.

Returns: The option of the environment. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_function_type_get_argument_num()

int nuxmv_function_type_get_argument_num	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the number of arguments of a function type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The function type to extract the argument type number from.

Returns: The number of arguments in the module or -1 in case of error.

Note: Should the environment or the function type be modified, the returned number is no longer valid and shall be discarded.

See also

Requirements: 03.001.03

◆ nuxmv_function_type_get_result()

nuxmv_expr_type nuxmv_function_type_get_result	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the type of the result of a function type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The function type to extract the result type from.

Returns: The type of result. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_array_type()

nuxmv_expr_type nuxmv_make_array_type	(	nuxmv_env	env,
		nuxmv_expr_type	idx,
		nuxmv_expr_type	elem
	)

Create an array type.

Parameters

[in]	env	The environment to modify.
[in]	idx	A type for the array index.
[in]	elem	A type for the array's elements.

Returns: The newly created array type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_boolean_type()

nuxmv_expr_type nuxmv_make_boolean_type ( nuxmv_env env )

Create a Boolean type.

Parameters

[in] env The environment to modify.

Returns: The newly created type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_enum_type()

nuxmv_expr_type nuxmv_make_enum_type ( nuxmv_env env )

Create an enumerative type whose variants are symbolic tags.

Parameters

[in] env The environment to modify.

Returns: The newly created enumerative type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_function_type()

nuxmv_expr_type nuxmv_make_function_type	(	nuxmv_env	env,
		const nuxmv_expr_type *	args,
		size_t	arg_num,
		nuxmv_expr_type	result
	)

Create a new (uninterpreted) function type.

Parameters

[in]	env	The environment to modify.
[in]	args	A list of function's arguments.
[in]	arg_num	The number of arguments in the list.
[in]	result	The type of the result returned by the function.

Returns: The newly created function type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_integer_type()

nuxmv_expr_type nuxmv_make_integer_type ( nuxmv_env env )

Create an integer type.

Parameters

[in] env The environment to modify.

Returns: The newly created integer type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_real_type()

nuxmv_expr_type nuxmv_make_real_type ( nuxmv_env env )

Create a real type.

Parameters

[in] env The environment to modify.

Returns: The newly created real type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_set_type()

nuxmv_expr_type nuxmv_make_set_type	(	nuxmv_env	env,
		nuxmv_expr_type	elem
	)

Create a set type.

Parameters

[in]	env	The environment to modify.
[in]	elem	A type for the elements in the set.

Returns: The newly created set type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Note: This function must be used only with expressions. The usage with with variables is not allowed.

Requirements: 03.001.03

◆ nuxmv_make_signed_word_type()

nuxmv_expr_type nuxmv_make_signed_word_type	(	nuxmv_env	env,
		size_t	width
	)

Create a signed word type.

Parameters

[in]	env	The environment to modify.
[in]	width	The number of bits for the word.

Returns: The newly created word type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_make_unsigned_word_type()

nuxmv_expr_type nuxmv_make_unsigned_word_type	(	nuxmv_env	env,
		size_t	width
	)

Create an unsigned word type.

Parameters

[in]	env	The environment to modify.
[in]	width	The number of bits for the word.

Returns: The newly created word type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_set_type_get_element()

nuxmv_expr_type nuxmv_set_type_get_element	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the type of the elements of a set type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The set type to extract the element type from.

Returns: The type of result. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

Requirements: 03.001.03

◆ nuxmv_word_type_get_width()

int nuxmv_word_type_get_width	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the width of a (un)signed word type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The expression type to extract the width from.

Returns: The width of the (un)signed word or -1 in case of error.

See also

Requirements: 03.001.03

Macros

Functions

Detailed Description

Macro Definition Documentation

◆ NUXMV_VALID_EXPR_TYPE

Function Documentation

◆ nuxmv_array_type_get_element()

◆ nuxmv_array_type_get_index()

◆ nuxmv_expr_type_get_id()

◆ nuxmv_expr_type_get_tag()

◆ nuxmv_function_type_get_argument()

◆ nuxmv_function_type_get_argument_num()

◆ nuxmv_function_type_get_result()

◆ nuxmv_make_array_type()

◆ nuxmv_make_boolean_type()

◆ nuxmv_make_enum_type()

◆ nuxmv_make_function_type()

◆ nuxmv_make_integer_type()

◆ nuxmv_make_real_type()

◆ nuxmv_make_set_type()

◆ nuxmv_make_signed_word_type()

◆ nuxmv_make_unsigned_word_type()

◆ nuxmv_set_type_get_element()

◆ nuxmv_word_type_get_width()