NuSMV/code/nusmv/core/node/node.h File Reference

#include <stdio.h>
#include "cudd/util.h"
#include "nusmv/core/node/NodeMgr.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

Go to the source code of this file.

Defines
#define	caar(_n_) car(car(_n_))
#define	cadr(_n_) car(cdr(_n_))
#define	cdar(_n_) cdr(car(_n_))
#define	cddr(_n_) cdr(cdr(_n_))
#define	node_bdd_setcar(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->left.bddtype = (_b_); }
#define	node_bdd_setcdr(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->right.bddtype = (_b_); }
#define	NODE_CONS_LIST_FOREACH(list, iter)
	standard shortcut for iterating over a cons list
#define	Node_conslist_get(iter) car(iter)
	Get the current element of the node conslist iterator.
#define	NODE_FROM_INT(x) (PTR_FROM_INT(node_ptr, (x)))
	Casts the given int to a node_ptr.
#define	node_get_int(_n_) (_n_)->left.inttype
#define	node_get_lineno(_n_) (_n_)->lineno
#define	node_get_lstring(_n_) (_n_)->left.strtype
#define	node_get_type(_n_) (_n_)->type
#define	node_int_setcar(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->left.inttype = (_b_); }
#define	node_int_setcdr(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->right.inttype = (_b_); }
#define	node_node_setcar(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->left.nodetype = (_b_); }
#define	node_node_setcdr(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->right.nodetype = (_b_); }
#define	NODE_PTR(x) ((node_ptr) (x))
	The header file of the `node` package.
#define	node_str_setcar(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->left.strtype = (_b_); }
#define	node_str_setcdr(_n_, _b_) { /nusmv_assert(!(_n_)->locked);/ (_n_)->right.strtype = (_b_); }
#define	NODE_TO_INT(x) (PTR_TO_INT(x))
	Casts the given node_ptr to an int.
Functions
node_ptr	append (node_ptr, node_ptr)
	DEPRECATED Appends two lists and returns the result.
node_ptr	append_ns (NodeMgr_ptr nodemgr, node_ptr, node_ptr)
	DEPRECATED Appends two lists and returns the result.
node_ptr	car (node_ptr)
	Returns the left branch of a node.
node_ptr	cdr (node_ptr)
	Returns the right branch of a node.
node_ptr	copy_list (NodeMgr_ptr nodemgr, node_ptr l)
	DEPRECATED Returns a copy of a list.
node_ptr	even_elements (NodeMgr_ptr nodemgr, node_ptr)
	DEPRECATED Extracts even elements of list L.
void	free_list (NodeMgr_ptr nodemgr, node_ptr l)
	DEPRECATED Frees all the elements of the list.
int	in_list (node_ptr, node_ptr)
	DEPRECATED Checks list R to see if it contains the element N.
int	is_list_empty (node_ptr)
	DEPRECATED Returns 1 is the list is empty, 0 otherwise.
node_ptr	last (node_ptr)
	DEPRECATED Returns the last cons in X.
unsigned int	llength (node_ptr)
	DEPRECATED Returns the length of list r.
node_ptr	map (NodeMgr_ptr nodemgr, NPFN fun, node_ptr)
	DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list.
node_ptr	map2 (NodeMgr_ptr nodemgr, NPFNN fun, node_ptr, node_ptr)
	DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list. Lists l1 and l2 are traversed in parallel.
node_ptr	map_param (NodeMgr_ptr nodemgr, node_ptr(fun)(node_ptr, void ), node_ptr l, void *)
	DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list.
node_ptr	new_list (void)
	DEPRECATED Returns a new empty list.
node_ptr	Node_conslist_add (NodeMgr_ptr nodemgr, node_ptr list, node_ptr element)
	Add an element to the list.
node_ptr	Node_conslist_remove (NodeMgr_ptr nodemgr, node_ptr list, node_ptr element)
	Remove an element from the list.
node_ptr	Node_find_boolean_type (NodeMgr_ptr nodemgr)
	Builds a boolean type node, suitable for HrcNode, FlatHierarchy.
node_ptr	Node_find_error_type (NodeMgr_ptr nodemgr)
node_ptr	Node_find_integer_type (NodeMgr_ptr nodemgr)
	Builds a integer type node, suitable for HrcNode, FlatHierarchy.
node_ptr	Node_find_real_type (NodeMgr_ptr nodemgr)
	Builds a real type node, suitable for HrcNode, FlatHierarchy.
boolean	Node_is_conslist (node_ptr list)
	Debug function to check if a node_ptr is actually a cons list.
int	node_is_failure (node_ptr node)
	Returns 0 if given node is not a FAILURE node.
int	node_is_leaf (node_ptr node)
boolean	Node_is_relation (node_ptr const expr)
boolean	Node_is_symbol (node_ptr const node)
	Checks if a node is syntactally a symbol.
boolean	Node_is_temporal_op (node_ptr const node)
	True if node is a temporal operator.
void	node_pkg_init (NuSMVEnv_ptr env)
	Initializes the node package.
void	node_pkg_quit (NuSMVEnv_ptr env)
	Deinitializes the packages, finalizing all internal structures.
void	node_set_type (node_ptr, int)
	Replaces the type of the node.
node_ptr	node_subtract (NodeMgr_ptr nodemgr, node_ptr, node_ptr)
	DEPRECATED Deletes from list set2 the elements of list set1.
node_ptr	odd_elements (NodeMgr_ptr nodemgr, node_ptr)
	DEPRECATED Extracts odd elements of list L.
void	print_array_type (const NuSMVEnv_ptr env, FILE *output_stream, const node_ptr body)
	Print an ARRAY_TYPE structure in smv.
node_ptr	reverse (node_ptr)
	DEPRECATED Reverse a list.
node_ptr	reverse_ns (NodeMgr_ptr nodemgr, node_ptr)
	DEPRECATED reverses the list with no side-effect.
void	setcar (node_ptr, node_ptr)
	Replaces the car of X with Y.
void	setcdr (node_ptr, node_ptr)
	Replaces the cdr of X with Y.
void	swap_nodes (node_ptr , node_ptr )
	Swaps two nodes.
void	walk (VPFN fun, node_ptr)
	DEPRECATED Applies FUN to successive cars of LISTs.

Define Documentation

#define caar ( _n_ ) car(car(_n_))

Todo:: Missing synopsis

Todo:: Missing description

#define cadr ( _n_ ) car(cdr(_n_))

Todo:: Missing synopsis

Todo:: Missing description

#define cdar ( _n_ ) cdr(car(_n_))

Todo:: Missing synopsis

Todo:: Missing description

#define cddr ( _n_ ) cdr(cdr(_n_))

Todo:: Missing synopsis

Todo:: Missing description

#define node_bdd_setcar	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->left.bddtype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define node_bdd_setcdr	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->right.bddtype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define NODE_CONS_LIST_FOREACH	(	list,
		iter		)

Value:

for (iter = list;                                                     \
       /* nusmv_assert(Nil == iter || CONS == node_get_type(iter)), */ Nil != iter; \
       iter = cdr(iter))

standard shortcut for iterating over a cons list

Expected types: node_ptr list node_ptr iter

#define Node_conslist_get ( iter ) car(iter)

Get the current element of the node conslist iterator.

optional

required

See also:: optional

#define NODE_FROM_INT ( x ) (PTR_FROM_INT(node_ptr, (x)))

Casts the given int to a node_ptr.

#define node_get_int ( _n_ ) (_n_)->left.inttype

Todo:: Missing synopsis

Todo:: Missing description

#define node_get_lineno ( _n_ ) (_n_)->lineno

Todo:: Missing synopsis

Todo:: Missing description

#define node_get_lstring ( _n_ ) (_n_)->left.strtype

Todo:: Missing synopsis

Todo:: Missing description

#define node_get_type ( _n_ ) (_n_)->type

Todo:: Missing synopsis

Todo:: Missing description

#define node_int_setcar	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->left.inttype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define node_int_setcdr	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->right.inttype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define node_node_setcar	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->left.nodetype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define node_node_setcdr	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->right.nodetype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define NODE_PTR ( x ) ((node_ptr) (x))

The header file of the node package.

Author:: Marco Roveri The node package implements a data structure which offers constructs with e syntax and semantic lisp like.

Casts the given pointer to a node_ptr

#define node_str_setcar	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->left.strtype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define node_str_setcdr	(	_n_,
		_b_		)	{ /nusmv_assert(!(_n_)->locked);/ (_n_)->right.strtype = (_b_); }

Todo:: Missing synopsis

Todo:: Missing description

#define NODE_TO_INT ( x ) (PTR_TO_INT(x))

Casts the given node_ptr to an int.

Function Documentation

node_ptr append	(	node_ptr	,
		node_ptr
	)

DEPRECATED Appends two lists and returns the result.

Constructs a new list by concatenating its arguments.

The modified list is returned. Side effects on the returned list were performed. It is equivalent to the lisp NCONC

node_ptr append_ns	(	NodeMgr_ptr	nodemgr,
		node_ptr	,
		node_ptr
	)

DEPRECATED Appends two lists and returns the result.

Constructs a new list by concatenating its arguments.

The modified list is returned. No side effects on the returned list were performed.

node_ptr car ( node_ptr )

Returns the left branch of a node.

None

See also:: cdr cons

node_ptr cdr ( node_ptr )

Returns the right branch of a node.

None

See also:: car cons

node_ptr copy_list	(	NodeMgr_ptr	nodemgr,
		node_ptr	l
	)

DEPRECATED Returns a copy of a list.

An invoker should free the returned list.

free_list

node_ptr even_elements	(	NodeMgr_ptr	nodemgr,
		node_ptr
	)

DEPRECATED Extracts even elements of list L.

Extracts even elements of list L.

None

See also:: odd_elements

void free_list	(	NodeMgr_ptr	nodemgr,
		node_ptr	l
	)

DEPRECATED Frees all the elements of the list.

Frees all the elements of the list for further use.

None

See also:: car

int in_list	(	node_ptr	,
		node_ptr
	)

DEPRECATED Checks list R to see if it contains the element N.

Checks list R to see if it contains the element N.

None

See also:: node_subtract

int is_list_empty ( node_ptr )

DEPRECATED Returns 1 is the list is empty, 0 otherwise.

None

node_ptr last ( node_ptr )

DEPRECATED Returns the last cons in X.

Returns the last cons in X.

None

See also:: car

unsigned int llength ( node_ptr )

DEPRECATED Returns the length of list r.

Returns the length of list r.

None

node_ptr map	(	NodeMgr_ptr	nodemgr,
		NPFN	fun,
		node_ptr
	)

DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list.

Applies FUN to successive cars of LISTs and returns the results as a list.

None

See also:: map2 walk

node_ptr map2	(	NodeMgr_ptr	nodemgr,
		NPFNN	fun,
		node_ptr	,
		node_ptr
	)

DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list. Lists l1 and l2 are traversed in parallel.

Applies FUN to successive cars of LISTs and returns the results as a list. l1 and l2 must have the same length

None

See also:: map walk

node_ptr map_param	(	NodeMgr_ptr	nodemgr,
		node_ptr()(node_ptr, void )	fun,
		node_ptr	l,
		void *
	)

DEPRECATED Applies FUN to successive cars of LISTs and returns the results as a list.

Applies FUN to successive cars of LISTs and returns the results as a list. Supports custom parameter

None

See also:: map2 walk

node_ptr new_list ( void )

DEPRECATED Returns a new empty list.

None

node_ptr Node_conslist_add	(	NodeMgr_ptr	nodemgr,
		node_ptr	list,
		node_ptr	element
	)

Add an element to the list.

This is a functional interface, so to modify "list" the snippet is:

list = Node_conslist_add(nodemgr, list, element);

node_ptr Node_conslist_remove	(	NodeMgr_ptr	nodemgr,
		node_ptr	list,
		node_ptr	element
	)

Remove an element from the list.

Linear time

node_ptr Node_find_boolean_type ( NodeMgr_ptr nodemgr )

Builds a boolean type node, suitable for HrcNode, FlatHierarchy.

It is of the same shape the parse uses.

node_ptr Node_find_error_type ( NodeMgr_ptr nodemgr )

Todo:: Missing synopsis

Todo:: Missing description

node_ptr Node_find_integer_type ( NodeMgr_ptr nodemgr )

Builds a integer type node, suitable for HrcNode, FlatHierarchy.

It is of the same shape the parse uses.

node_ptr Node_find_real_type ( NodeMgr_ptr nodemgr )

Builds a real type node, suitable for HrcNode, FlatHierarchy.

It is of the same shape the parse uses.

boolean Node_is_conslist ( node_ptr list )

Debug function to check if a node_ptr is actually a cons list.

Debug function to check if a node_ptr is actually a cons list

int node_is_failure ( node_ptr node )

Returns 0 if given node is not a FAILURE node.

int node_is_leaf ( node_ptr node )

Todo:: Missing synopsis

Todo:: Missing description

boolean Node_is_relation ( node_ptr const expr )

Todo:: Missing synopsis

Todo:: Missing description

boolean Node_is_symbol ( node_ptr const node )

Checks if a node is syntactally a symbol.

Checks if a node is syntactally a symbol

boolean Node_is_temporal_op ( node_ptr const node )

True if node is a temporal operator.

No recursion is performed Warning, some case missing. What about PSL, for instance?

void node_pkg_init ( NuSMVEnv_ptr env )

Initializes the node package.

Creates master and printers, and initializes the node structures

See also:: node_pkg_quit

void node_pkg_quit ( NuSMVEnv_ptr env )

Deinitializes the packages, finalizing all internal structures.

See also:: node_pkg_init

void node_set_type	(	node_ptr	,
		int
	)

Replaces the type of the node.

Replaces the type of the node

See also:: car cdr cons setcar node_get_type

node_ptr node_subtract	(	NodeMgr_ptr	nodemgr,
		node_ptr	,
		node_ptr
	)

DEPRECATED Deletes from list set2 the elements of list set1.

Deletes elements of list set1 from list set2 without doing side effect. The resulting list is returned. This is quite inefficient: O(|set1| * |set2|) where |<parameter>| denote the length of the list

None

node_ptr odd_elements	(	NodeMgr_ptr	nodemgr,
		node_ptr
	)

DEPRECATED Extracts odd elements of list L.

Extracts odd elements of list L.

None

See also:: even_elements

void print_array_type	(	const NuSMVEnv_ptr	env,
		FILE *	output_stream,
		const node_ptr	body
	)

Print an ARRAY_TYPE structure in smv.

See also:: print_sexp

node_ptr reverse ( node_ptr )

DEPRECATED Reverse a list.

Returns a new sequence containing the same elements as X but in reverse order.

The orignial list is modified

See also:: last car cons append

node_ptr reverse_ns	(	NodeMgr_ptr	nodemgr,
		node_ptr
	)

DEPRECATED reverses the list with no side-effect.

Returns a reversed version of the given list. The original list is NOT modified

None

void setcar	(	node_ptr	,
		node_ptr
	)

Replaces the car of X with Y.

Replaces the car of X with Y

The car of X is replaced by Y.

See also:: car cdr cons setcdr

void setcdr	(	node_ptr	,
		node_ptr
	)

Replaces the cdr of X with Y.

Replaces the cdr of X with Y

The cdr of X is replaced by Y.

See also:: car cdr cons setcar

void swap_nodes	(	node_ptr *	,
		node_ptr *
	)

Swaps two nodes.

The two nodes are swapped.

void walk	(	VPFN	fun,
		node_ptr
	)

DEPRECATED Applies FUN to successive cars of LISTs.

Applies FUN to successive cars of LISTs.

None

See also:: map

NuSMV/code/nusmv/core/node/node.h File Reference

Defines

Functions

Define Documentation

Function Documentation