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

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``node'' package of NuSMV version 2.
  Copyright (C) 1998-2001 by CMU and FBK-irst.
  Copyright (C) 2011 by FBK.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>. 

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_NODE_NODE_H__
#define __NUSMV_CORE_NODE_NODE_H__

#include <stdio.h> /* for FILE* */

#include "cudd/util.h" /* [MD] Is it necessary? */
#include "nusmv/core/node/NodeMgr.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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

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

#define Node_conslist_get(iter) \
  car(iter)

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

#if NUSMV_SIZEOF_VOID_P == 8 && NUSMV_SIZEOF_INT == 4
#if NUSMV_SIZEOF_LONG == 8

#define NODE_FROM_INT(x)                                \
  (PTR_FROM_INT(node_ptr, (0x00000000FFFFFFFFL & ((nusmv_ptrint)x))))
#else
/* Long is 4 bytes, thus we need to use long long (Windows 64bits) */
#define NODE_FROM_INT(x)                                \
  (PTR_FROM_INT(node_ptr, (0x00000000FFFFFFFFLL & ((nusmv_ptrint)x))))
#endif
#else
#define NODE_FROM_INT(x)                        \
  (PTR_FROM_INT(node_ptr, (x)))
#endif

#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_get_type(_n_) (_n_)->type

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

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

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

#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_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_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_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_); }


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

void node_pkg_init(NuSMVEnv_ptr env);

void node_pkg_quit(NuSMVEnv_ptr env);

void swap_nodes(node_ptr *, node_ptr *);

int node_is_failure(node_ptr node);

int node_is_leaf(node_ptr node);

boolean Node_is_symbol(node_ptr const node);

boolean Node_is_relation(node_ptr const expr);

boolean Node_is_temporal_op(node_ptr const node);

node_ptr car(node_ptr);

node_ptr cdr(node_ptr);

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

void setcar(node_ptr, node_ptr);

void setcdr(node_ptr, node_ptr);

void node_set_type(node_ptr, int);

/* Node Types interface *******************************************************/

node_ptr Node_find_boolean_type(NodeMgr_ptr nodemgr);

node_ptr Node_find_integer_type(NodeMgr_ptr nodemgr);

node_ptr Node_find_real_type(NodeMgr_ptr nodemgr);

node_ptr Node_find_error_type(NodeMgr_ptr nodemgr);



/* Conslist interface */
/* The following functions are deprecated and should never be used in new code
   (they are the interface to the nodelist type) */
/* Constructors, Destructors, Copiers and Cleaners ****************************/

node_ptr new_list(void);

node_ptr copy_list(NodeMgr_ptr nodemgr, node_ptr l);

void     free_list(NodeMgr_ptr nodemgr, node_ptr l);


/* Getters and Setters ********************************************************/

unsigned int      llength(node_ptr);


/* Queries  *******************************************************************/

int      is_list_empty(node_ptr);

int      in_list(node_ptr, node_ptr);

boolean Node_is_conslist(node_ptr list);


/* Miscellaneous **************************************************************/

void     walk(VPFN fun, node_ptr);

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

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

node_ptr append(node_ptr, node_ptr);

node_ptr append_ns(NodeMgr_ptr nodemgr, node_ptr, node_ptr);

node_ptr reverse(node_ptr);

node_ptr reverse_ns(NodeMgr_ptr nodemgr, node_ptr);

node_ptr last(node_ptr);

node_ptr map(NodeMgr_ptr nodemgr, NPFN fun, node_ptr);

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

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

node_ptr even_elements(NodeMgr_ptr nodemgr, node_ptr);

node_ptr odd_elements(NodeMgr_ptr nodemgr, node_ptr);

node_ptr node_subtract(NodeMgr_ptr nodemgr, node_ptr, node_ptr);

/******************************************************************************/

#endif /* __NUSMV_CORE_NODE_NODE_H__ */

---