Variable Types

Functions for handling Variable Types. More...

Macros
#define	NUXMV_VALID_VAR_TYPE(var_type)   ((var_type).repr != NULL)
	Valid variable type.

Functions
nuxmv_var_type	nuxmv_make_simple_var_type (nuxmv_env env, nuxmv_expr_type type)
	Get the variable type corresponding to a type.
nuxmv_var_type	nuxmv_make_var_type_with_domain (nuxmv_env env, const nuxmv_expr *domain, size_t domain_num)
	Get the variable type corresponding to an enumerative.
nuxmv_var_type	nuxmv_make_var_type_with_integer_range (nuxmv_env env, int min, int max)
	Returns the var_type corresponding to the selected bounded int type.
nuxmv_var_type	nuxmv_make_var_type_array (nuxmv_env env, nuxmv_var_type idx, nuxmv_var_type elem)
	Builds an array var_type.
nuxmv_expr_type	nuxmv_var_type_get_expr_type (nuxmv_env env, nuxmv_var_type var_type)
	Get the expression type corresponding to a variable type.
nuxmv_var_type_tag	nuxmv_var_type_get_tag (nuxmv_env env, nuxmv_var_type var_type)
	Get the tag of a var_type.
size_t	nuxmv_var_type_get_id (nuxmv_env env, nuxmv_var_type var_type)
	Get the ID of a var type.
nuxmv_var_type	nuxmv_var_type_array_get_index (nuxmv_env env, nuxmv_var_type var_type)
	Get the var type of the index of an array var type.
nuxmv_var_type	nuxmv_var_type_array_get_element (nuxmv_env env, nuxmv_var_type var_type)
	Get the var type of the element of an array var type.
int	nuxmv_var_type_integer_range_get_min (nuxmv_env env, nuxmv_var_type var_type)
	Get the min value an integer range var type.
int	nuxmv_var_type_integer_range_get_max (nuxmv_env env, nuxmv_var_type var_type)
	Get the max value an integer range var type.
int	nuxmv_var_type_get_domain_num (nuxmv_env env, nuxmv_var_type var_type)
	Get the number of elements of a var type with domain.
nuxmv_expr	nuxmv_var_type_get_domain_element (nuxmv_env env, nuxmv_var_type var_type, int elem_idx)
	Get the domain element at the given index of a var type with domain.

Detailed Description

Functions for handling Variable Types.

---

Macro Definition Documentation

NUXMV_VALID_VAR_TYPE

#define NUXMV_VALID_VAR_TYPE

(

var_type

)

((var_type).repr != NULL)

Valid variable type.

This macro checks whether var_type is a valid nuxmv_var_type.

Parameters

[in]

var_type

The variable type to inspect.

Returns

true if the option is valid, false otherwise.

Function Documentation

nuxmv_make_simple_var_type()

nuxmv_var_type nuxmv_make_simple_var_type	(	nuxmv_env	env,
		nuxmv_expr_type	type
	)

Get the variable type corresponding to a type.

Parameters

[in]	env	The environment to inspect.
[in]	type	The expression type to inspect.

Returns

The simple variable type representing the expression.

See also

• nuxmv_make_boolean_type()
• nuxmv_make_integer_type()
• nuxmv_make_real_type()
• nuxmv_make_set_type()
• nuxmv_make_signed_word_type()
• nuxmv_make_unsigned_word_type()
• nuxmv_make_function_type()

Requirements: 03.001.03

nuxmv_make_var_type_array()

nuxmv_var_type nuxmv_make_var_type_array	(	nuxmv_env	env,
		nuxmv_var_type	idx,
		nuxmv_var_type	elem
	)

Builds an array var_type.

Parameters

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

Returns

The variable type representing the array. In case of error, NUXMV_VALID_VAR_TYPE() evaluates to false.

See also

• nuxmv_make_array_type()

Requirements: ??

nuxmv_make_var_type_with_domain()

nuxmv_var_type nuxmv_make_var_type_with_domain	(	nuxmv_env	env,
		const nuxmv_expr *	domain,
		size_t	domain_num
	)

Get the variable type corresponding to an enumerative.

It specifies enumerative values for the variable type.

Parameters

[in]	env	The environment to inspect.
[in]	domain	The list of identifiers that belongs to the domain. All identifiers shall be of the same type.
[in]	domain_num	The number of values in the list.

Returns

The variable type representing the enumerative. In case of error, NUXMV_VALID_VAR_TYPE() evaluates to false.

See also

• NUXMV_COUNT_OF()
• nuxmv_make_enum_type()
• nuxmv_make_real_type()??
• nuxmv_make_set_type()??
• nuxmv_make_identifier()

Requirements: 03.001.03

nuxmv_make_var_type_with_integer_range()

nuxmv_var_type nuxmv_make_var_type_with_integer_range	(	nuxmv_env	env,
		int	min,
		int	max
	)

Returns the var_type corresponding to the selected bounded int type.

It specifies lower and upper bounds for the var_type.

Parameters

[in]	env	The environment to inspect.
[in]	min	The minimum value in the range, inclusive.
[in]	max	The maximum value in the range, inclusive.

Returns

The variable type representing the array. In case of error, NUXMV_VALID_VAR_TYPE() evaluates to false.

Requirements: 03.001.03

nuxmv_var_type_array_get_element()

nuxmv_var_type nuxmv_var_type_array_get_element	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the var type of the element of an array var type.

Parameters

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

Returns

The var type of the element. In case of error, NUXMV_VALID_VAR_TYPE() evaluates to false.

See also

• nuxmv_make_var_type_array()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_array_get_index()

nuxmv_var_type nuxmv_var_type_array_get_index	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the var type of the index of an array var type.

Parameters

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

Returns

The var type of the index. In case of error, NUXMV_VALID_VAR_TYPE() evaluates to false.

See also

• nuxmv_make_var_type_array()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_get_domain_element()

nuxmv_expr nuxmv_var_type_get_domain_element	(	nuxmv_env	env,
		nuxmv_var_type	var_type,
		int	elem_idx
	)

Get the domain element at the given index of a var type with domain.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The var type with domain to extract the number of elements from.
[in]	elem_idx	The index of the domain element to retrieve.

Returns

The domain element at the given index. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_make_var_type_with_domain()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_get_domain_num()

int nuxmv_var_type_get_domain_num	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the number of elements of a var type with domain.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The var type with domain to extract the number of elements from.

Returns

The number of elements in the var type domain. In case of error, -1 is returned.

See also

• nuxmv_make_var_type_with_domain()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_get_expr_type()

nuxmv_expr_type nuxmv_var_type_get_expr_type	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the expression type corresponding to a variable type.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The variable type to inspect.

Returns

The expression type representing the variable type.

nuxmv_var_type_get_id()

size_t nuxmv_var_type_get_id	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the ID of a var type.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The var 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_var_type_get_tag()

nuxmv_var_type_tag nuxmv_var_type_get_tag	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the tag of a var_type.

Parameters

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

Returns

The tag of the var type, NUXMV_VAR_TYPE_INVALID in case of error.

See also

• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_integer_range_get_max()

int nuxmv_var_type_integer_range_get_max	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the max value an integer range var type.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The integer range var type to extract the max value from.

Returns

The max value of the range. In case of error, INT_MIN is returned.

See also

• nuxmv_make_var_type_with_integer_range()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03

nuxmv_var_type_integer_range_get_min()

int nuxmv_var_type_integer_range_get_min	(	nuxmv_env	env,
		nuxmv_var_type	var_type
	)

Get the min value an integer range var type.

Parameters

[in]	env	The environment to inspect.
[in]	var_type	The integer range var type to extract the min value from.

Returns

The min value of the range. In case of error, INT_MIN is returned.

See also

• nuxmv_make_var_type_with_integer_range()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.03