Expressions

Functions for handling Expressions. More...

Macros
#define	NUXMV_MAKE_INVALID_EXPR()   ((nuxmv_expr){.repr = NULL})
#define	NUXMV_VALID_EXPR(expr)   ((expr).repr != NULL)
	Valid expression.

Functions
nuxmv_expr	nuxmv_make_identifier (nuxmv_env env, nuxmv_symbol symbol, nuxmv_expr_type type)
	Create a new identifier for a symbol.
nuxmv_expr	nuxmv_make_value (nuxmv_env env, nuxmv_symbol val, nuxmv_expr_type type)
	Create a new value for a symbol.
nuxmv_expr	nuxmv_make_op (nuxmv_env env, nuxmv_op_tag op, const nuxmv_expr *args, size_t arg_num)
	Create a structured expression for an operator.
nuxmv_expr	nuxmv_make_parametric_op (nuxmv_env env, nuxmv_op_tag op, const nuxmv_expr *args, size_t arg_num, const int *params, size_t param_num)
	Create a structured parametric expression for an operator.
nuxmv_expr	nuxmv_make_un_op (nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg)
	Create a structured expression for a unary operator.
nuxmv_expr	nuxmv_make_bin_op (nuxmv_env env, nuxmv_op_tag op, nuxmv_expr arg1, nuxmv_expr arg2)
	Create a structured expression for a binary operator.
nuxmv_expr	nuxmv_make_expr_from_string (nuxmv_env env, const char *data, nuxmv_module scope)
	Make an expression from a string.
nuxmv_expr_type	nuxmv_expr_get_type (nuxmv_env env, nuxmv_expr expr)
	Get the type of an expression.
nuxmv_symbol	nuxmv_expr_get_symbol (nuxmv_env env, nuxmv_expr identifier)
	Get the symbol associated to an identifier.
size_t	nuxmv_expr_get_id (nuxmv_env env, nuxmv_expr expr)
	Get the ID of a type.
int	nuxmv_serialize_expr_to_string (nuxmv_env env, nuxmv_expr expr, nuxmv_serialized_chunk_callback callback, void *user_data, char *data, size_t data_size)
	Serialize a expr to a string.
int	nuxmv_expr_contains_temporal_operators (nuxmv_env env, nuxmv_expr expr)
	Test whether an expression contains temporal operators.
int	nuxmv_expr_is_identifier (nuxmv_env env, nuxmv_expr expr)
	Test whether an expression corresponds to an identifier.
int	nuxmv_expr_is_value (nuxmv_env env, nuxmv_expr expr)
	Test whether an expression corresponds to a value.
int	nuxmv_expr_is_op (nuxmv_env env, nuxmv_expr expr)
	Test whether an expression corresponds to an operator.
nuxmv_op_tag	nuxmv_expr_get_op_tag (nuxmv_env env, nuxmv_expr expr)
	Get the tag of an operator.
int	nuxmv_expr_get_argument_num (nuxmv_env env, nuxmv_expr expr)
	Get the number of arguments in an expression.
nuxmv_expr	nuxmv_expr_get_argument (nuxmv_env env, nuxmv_expr expr, int arg_idx)
	Get the i-th argument of a structured expression.
int	nuxmv_expr_is_parametric (nuxmv_env env, nuxmv_expr expr)
	Test whether an expression is parametric.
int	nuxmv_expr_get_parameter_num (nuxmv_env env, nuxmv_expr expr)
	Get the number of parameters in a parametric expression.
int	nuxmv_expr_get_parameter (nuxmv_env env, nuxmv_expr expr, int param_idx)
	Get the i-th parameter value of a structured parametric expression.
int	nuxmv_visit_expr (nuxmv_env env, nuxmv_expr expr, nuxmv_expr_visit_callback callback, nuxmv_expr_visit_order order, void *user_data)
	Visit an expression.
nuxmv_expr	nuxmv_simplify_expr (nuxmv_env env, nuxmv_expr expr)
	Simplify an expression.

Detailed Description

Functions for handling Expressions.

---

Macro Definition Documentation

NUXMV_MAKE_INVALID_EXPR

#define NUXMV_MAKE_INVALID_EXPR

(

)

((nuxmv_expr){.repr = NULL})

Make an invalid expression object

This macro is useful where a function argument requires an optional expression object.

See also

• nuxmv_simulation_constraint()

NUXMV_VALID_EXPR

#define NUXMV_VALID_EXPR

(

expr

)

((expr).repr != NULL)

Valid expression.

This macro checks whether expr is a valid nuxmv_expr.

Parameters

[in]

expr

The expression to inspect.

Returns

true if the option is valid, false otherwise.

Function Documentation

nuxmv_expr_contains_temporal_operators()

int nuxmv_expr_contains_temporal_operators	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Test whether an expression contains temporal operators.

Parameters

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

Returns

1 when the expression contains at least one temporal operator, 0 if not, -1 in case of error.

See also

• nuxmv_make_op()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_get_argument()

nuxmv_expr nuxmv_expr_get_argument	(	nuxmv_env	env,
		nuxmv_expr	expr,
		int	arg_idx
	)

Get the i-th argument of a structured expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The structured expression to inspect.
[in]	arg_idx	The index of the argument counting from 0.

Returns

The argument of the structured expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_make_op()
• nuxmv_expr_get_argument_num()
• nuxmv_expr_get_parameter()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_get_argument_num()

int nuxmv_expr_get_argument_num	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Get the number of arguments in an expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The expression to extract the argument number from.

Returns

The number of arguments in the expression or -1 in case of error.

Note

Should the environment or the expression be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_expr_get_argument()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_get_id()

size_t nuxmv_expr_get_id	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Get the ID of a type.

Parameters

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

Returns

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

nuxmv_expr_get_op_tag()

nuxmv_op_tag nuxmv_expr_get_op_tag	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Get the tag of an operator.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The structured expression to inspect.

Returns

The tag identifying the operator. In case of error, NUXMV_OP_INVALID is returned.

See also

• nuxmv_make_op()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.04

nuxmv_expr_get_parameter()

int nuxmv_expr_get_parameter	(	nuxmv_env	env,
		nuxmv_expr	expr,
		int	param_idx
	)

Get the i-th parameter value of a structured parametric expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The structured parametric expression to inspect.
[in]	param_idx	The index of the parameter counting from 0.

Returns

The parameter value of the structured parametric expression or -1 in case of error.

See also

• nuxmv_make_parametric_op()
• nuxmv_expr_get_parameter_num()
• nuxmv_expr_get_argument()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_expr_get_parameter_num()

int nuxmv_expr_get_parameter_num	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Get the number of parameters in a parametric expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The expression to extract the parameter number from.

Returns

The number of parameters in the expression or -1 in case of error.

Note

Should the environment or the expression be modified, the returned number is no longer valid and shall be discarded.

See also

• nuxmv_expr_get_parameter()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_expr_get_symbol()

nuxmv_symbol nuxmv_expr_get_symbol	(	nuxmv_env	env,
		nuxmv_expr	identifier
	)

Get the symbol associated to an identifier.

Parameters

[in]	env	The environment to inspect.
[in]	identifier	The identifier to inspect.

Returns

The associated symbol. If no symbol is associated or in case of error, NUXMV_VALID_SYMBOL() evaluates to false.

See also

• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_get_type()

nuxmv_expr_type nuxmv_expr_get_type	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Get the type of an expression.

Parameters

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

Returns

The expression type. In case of error, NUXMV_VALID_EXPR_TYPE() evaluates to false.

See also

• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_is_identifier()

int nuxmv_expr_is_identifier	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Test whether an expression corresponds to an identifier.

Parameters

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

Returns

1 when the expression is an identifier for a symbol, 0 if not, -1 in case of error.

See also

• nuxmv_make_identifier()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_is_op()

int nuxmv_expr_is_op	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Test whether an expression corresponds to an operator.

Parameters

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

Returns

1 when the expression is strctured, 0 if not, -1 in case of error.

See also

• nuxmv_make_op()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_expr_is_parametric()

int nuxmv_expr_is_parametric	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Test whether an expression is parametric.

Parameters

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

Returns

1 when the expression is strctured and parametric, 0 if not, -1 in case of error.

See also

• nuxmv_make_parametric_op()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_expr_is_value()

int nuxmv_expr_is_value	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Test whether an expression corresponds to a value.

Parameters

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

Returns

1 when the expression is a value for a symbol, 0 if not, -1 in case of error.

See also

• nuxmv_make_value()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.02

nuxmv_make_bin_op()

nuxmv_expr nuxmv_make_bin_op	(	nuxmv_env	env,
		nuxmv_op_tag	op,
		nuxmv_expr	arg1,
		nuxmv_expr	arg2
	)

Create a structured expression for a binary operator.

Parameters

[in]	env	The environment to modify.
[in]	op	The operation computed by the expression.
[in]	arg1	The first argument of the operator.
[in]	arg2	The second argument of the operator.

Returns

The newly created structured expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_make_op()

Requirements: 03.001.01

nuxmv_make_expr_from_string()

nuxmv_expr nuxmv_make_expr_from_string	(	nuxmv_env	env,
		const char *	data,
		nuxmv_module	scope
	)

Make an expression from a string.

Parameters

[in]	env	The environment to modify.
[in]	data	A null-terminated string containing the expression data.
[in]	scope	A context the expression belongs to, or an invalid module if no context is required.

Returns

The newly created expression corresponding to the string. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• NUXMV_MAKE_INVALID_MODULE()
• nuxmv_expr_get_type()
• nuxmv_visit_expr()
• nuxmv_make_identifier()
• nuxmv_make_value()
• nuxmv_make_op()
• nuxmv_env_get_last_error_message()

Requirements: 03.005

nuxmv_make_identifier()

nuxmv_expr nuxmv_make_identifier	(	nuxmv_env	env,
		nuxmv_symbol	symbol,
		nuxmv_expr_type	type
	)

Create a new identifier for a symbol.

Parameters

[in]	env	The environment to modify.
[in]	symbol	A symbol to identify.
[in]	type	The type for the identifier.

Returns

The newly created identifier. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_expr_is_identifier()
• nuxmv_expr_get_symbol()
• nuxmv_expr_get_type()
• nuxmv_make_expr_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_make_op()

nuxmv_expr nuxmv_make_op	(	nuxmv_env	env,
		nuxmv_op_tag	op,
		const nuxmv_expr *	args,
		size_t	arg_num
	)

Create a structured expression for an operator.

Parameters

[in]	env	The environment to modify.
[in]	op	The operation computed by the expression.
[in]	args	A list of arguments the operator requires as inputs. If no list shall be used (for example with operator NUXMV_OP_PI) it is safe to use NULL or the result of malloc(0), provided that arg_num=0.
[in]	arg_num	The number of arguments in the list. If no list shall be passed, use 0 as actual value of arg_num.

Returns

The newly created structured expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

Note

If the operation requires one or more parameters, refer to nuxmv_make_parametric_op().

See also

• NUXMV_COUNT_OF()
• nuxmv_expr_is_op()
• nuxmv_expr_get_op_tag()
• nuxmv_expr_get_argument()
• nuxmv_expr_contains_temporal_operators()
• nuxmv_visit_expr()
• nuxmv_expr_get_type()
• nuxmv_make_expr_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_make_parametric_op()

nuxmv_expr nuxmv_make_parametric_op	(	nuxmv_env	env,
		nuxmv_op_tag	op,
		const nuxmv_expr *	args,
		size_t	arg_num,
		const int *	params,
		size_t	param_num
	)

Create a structured parametric expression for an operator.

This function shall be used when one of the following operations is needed. Each operation takes one expression in args and a fixed number of parameters as params in the described order:

• NUXMV_OP_BIT_SELECTION
  1. msb (≥ 0): the most significant bit (inclusive) of the selection
  2. lsb (≤ msb): the least significant bit (inclusive) of the selection
• NUXMV_OP_CAST_SIGNED_WORD and NUXMV_OP_CAST_UNSIGNED_WORD
  1. width (> 0) of the result word expression
• NUXMV_OP_EXTEND
  1. amount (≥ 0) of the extension
• NUXMV_OP_RESIZE
  1. width (> 0) of the result word expression

For all other operators, refer to nuxmv_make_op().

Parameters

[in]	env	The environment to modify.
[in]	op	The operation computed by the expression.
[in]	args	A list of arguments the operator requires as inputs.
[in]	arg_num	The number of arguments in the list.
[in]	params	A list of parameters the operator requires as inputs.
[in]	param_num	The number of parameters in the list.

Returns

The newly created structured expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• NUXMV_COUNT_OF()
• nuxmv_expr_is_parametric()
• nuxmv_expr_get_parameter()
• nuxmv_expr_is_op()
• nuxmv_expr_get_op_tag()
• nuxmv_expr_get_argument()
• nuxmv_expr_contains_temporal_operators()
• nuxmv_visit_expr()
• nuxmv_expr_get_type()
• nuxmv_make_expr_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_make_un_op()

nuxmv_expr nuxmv_make_un_op	(	nuxmv_env	env,
		nuxmv_op_tag	op,
		nuxmv_expr	arg
	)

Create a structured expression for a unary operator.

Parameters

[in]	env	The environment to modify.
[in]	op	The operation computed by the expression.
[in]	arg	The argument of the operator.

Returns

The newly created structured expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_make_op()

Requirements: 03.001.01

nuxmv_make_value()

nuxmv_expr nuxmv_make_value	(	nuxmv_env	env,
		nuxmv_symbol	val,
		nuxmv_expr_type	type
	)

Create a new value for a symbol.

Parameters

[in]	env	The environment to modify.
[in]	val	The value for the symbol.
[in]	type	The type of the value.

Returns

The newly created value. In case of error, NUXMV_VALID_EXPR() evaluates to false.

See also

• nuxmv_expr_is_value()
• nuxmv_expr_get_symbol()
• nuxmv_expr_get_type()
• nuxmv_make_expr_from_string()
• nuxmv_env_get_last_error_message()

Requirements: 03.001.01

nuxmv_serialize_expr_to_string()

int nuxmv_serialize_expr_to_string	(	nuxmv_env	env,
		nuxmv_expr	expr,
		nuxmv_serialized_chunk_callback	callback,
		void *	user_data,
		char *	data,
		size_t	data_size
	)

Serialize a expr to a string.

The output is written to the provided buffer. When the serialization process fills up the buffer:

• if a callback is not provided, a value equal to or greater than data_size is returned;
• if a callback is provided, it is invoked with the user-defined context.

The callback is responsible for handling the data chunk (e.g., copying it elsewhere). If the callback returns false, the process is aborted and the function returns the number of bytes written up to that point.

When the serialization process is completed successfully, the output buffer contains a null-terminated string and the callback is called, if any.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The expr to serialize.
[in]	callback	Optional callback function invoked whenever the buffer is full or the serialization process is completed.
[in]	user_data	User-defined context passed to the callback.
[out]	data	The buffer where the serialized expr will be stored.
[in]	data_size	The size of the data buffer.

Returns

• The total number of bytes written, including the terminating null byte, upon successful completion;
• a value equal to or greater than data_size, if no callback is provided and the serialized expression was truncated;
• the accumulated number of bytes for all successful calls of the callback, if the callback eventually requests to stop;
• -1 in case of error.

See also

• nuxmv_env_get_last_error_message()

Requirements: 03.002

nuxmv_simplify_expr()

nuxmv_expr nuxmv_simplify_expr	(	nuxmv_env	env,
		nuxmv_expr	expr
	)

Simplify an expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The expression to simplify.

Returns

A new simplified expression. In case of error, NUXMV_VALID_EXPR() evaluates to false.

TODO: useful?? we need to understand if when building nuxmv expressions we are implicitly performing some simplifications (e.g. a conjunction containing a TRUE is stored as TRUE) See also issue #16.

Requirements: 03.001

nuxmv_visit_expr()

int nuxmv_visit_expr	(	nuxmv_env	env,
		nuxmv_expr	expr,
		nuxmv_expr_visit_callback	callback,
		nuxmv_expr_visit_order	order,
		void *	user_data
	)

Visit an expression.

Parameters

[in]	env	The environment to inspect.
[in]	expr	The expression to visit.
[in]	callback	A user-defined function which is called for each node that composes the given expression.
[in]	order	The order which the expression's nodes are traversed.
[in]	user_data	Any user-defined context data passed to the callback function as-is.

Returns

1 if expression was visited completely, 0 if not, -1 in case of error.

See also

• nuxmv_env_get_last_error_message()

Requirements: 03.001