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

Go to the documentation of this file.

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


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

  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_MGR_H__
#define __NUSMV_CORE_NODE_NODE_MGR_H__

#include "nusmv/core/cinit/NuSMVEnv.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define Nil ((node_ptr)0)

#define FAILURE_NODE ((node_ptr)(-1))

#define CLOSED_NODE (node_ptr)(-2)

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef union value_ node_val;

typedef struct node node_rec;
typedef struct node * node_ptr;

typedef node_ptr (*NPFN)(node_ptr);
typedef node_ptr (*NPFNN)(node_ptr, node_ptr);

typedef void  (*VPFN)(node_ptr);

typedef boolean (*BPFN)(node_ptr);

typedef int (*custom_print_sexp_t)(FILE *, node_ptr);
typedef int (*out_func_t)(void*, char*);
typedef int (*custom_print_node_t)(out_func_t, FILE *, node_ptr,
                                   int *, char **, int *, int *, int *);

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

union value_ {
  int inttype;
  struct node *nodetype;
  struct string_ * strtype;
  void * bddtype;
};


struct node {
  struct node *link;
  /*char locked; */ /* this field should be a bit into the others
                       (e.g. in type) */
  short int type;
  int lineno;
  node_val left;
  node_val right;
  void* extra_data; /* added to handle rbc */
};

typedef struct NodeMgr_TAG*  NodeMgr_ptr;


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

#define NODE_MGR(self) \
         ((NodeMgr_ptr) self)

#define NODE_MGR_CHECK_INSTANCE(self) \
         (nusmv_assert(NODE_MGR(self) != NODE_MGR(NULL)))


/* shorthands to avoid columns explosions in code when building
   expressions. See relative NodeMgr methods */

#define find_node(mgr, t, l, r)                 \
  NodeMgr_find_node(mgr, t, l, r)

#define new_node(mgr, t, l, r)                  \
  NodeMgr_new_node(mgr, t, l, r)

#define new_lined_node(mgr, t, l, r, lineno)            \
  NodeMgr_new_lined_node(mgr, t, l, r, lineno)

#define free_node(mgr, n)                       \
  NodeMgr_free_node(mgr, n)

#define find_atom(mgr, n)                       \
  NodeMgr_find_atom(mgr, n)

/* same as old "cons", but with the node manager */

#define cons(mgr, x, y)                         \
  NodeMgr_cons(mgr, x, y)

/* this is not enough, we need the normalizer */

#define NODEMGR_ASSERT_IS_NODE_NORMALIZED(nodemgr, node) \
  (nusmv_assert(node == find_atom(nodemgr, node)))

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

NodeMgr_ptr NodeMgr_create(const NuSMVEnv_ptr env);

void NodeMgr_destroy(NodeMgr_ptr self);

void NodeMgr_show_profile_stats(NodeMgr_ptr self,
                                           FILE* stream);

/* Fresh nodes */

node_ptr NodeMgr_new_node(NodeMgr_ptr self, int type,
                                     node_ptr left, node_ptr right);

node_ptr NodeMgr_new_lined_node(NodeMgr_ptr self,
                                           int type,
                                           node_ptr left,
                                           node_ptr right,
                                           int lineno);

/* Hashed nodes */

void NodeMgr_free_node(NodeMgr_ptr self, node_ptr node);

node_ptr NodeMgr_find_node(NodeMgr_ptr self, int type,
                                     node_ptr x, node_ptr y);

node_ptr NodeMgr_find_atom(NodeMgr_ptr self,
                                  node_ptr node);

node_ptr NodeMgr_cons(NodeMgr_ptr self, node_ptr x, node_ptr y);

/* ONLY FOR DEBUGGING. DO NOT USE! */

void NodeMgr_self_check(NodeMgr_ptr self, boolean check_repeated);

#endif /* __NUSMV_CORE_NODE_NODE_MGR_H__ */

---