NuSMV/code/nusmv/core/dag/dag.h

Go to the documentation of this file.

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


  This file is part of the ``dag'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by University of Genova.
  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_DAG_DAG_H__
#define __NUSMV_CORE_DAG_DAG_H__

#if HAVE_CONFIG_H
# include "nusmv-config.h"
#endif


/* Standard includes. */
#if NUSMV_HAVE_MALLOC_H
# if NUSMV_HAVE_SYS_TYPES_H
#  include <sys/types.h>
# endif
# include <malloc.h>
#elif defined(NUSMV_HAVE_SYS_MALLOC_H) && NUSMV_HAVE_SYS_MALLOC_H
# if NUSMV_HAVE_SYS_TYPES_H
#  include <sys/types.h>
# endif
# include <sys/malloc.h>
#elif NUSMV_HAVE_STDLIB_H
# include <stdlib.h>
#endif

#if NUSMV_HAVE_UNISTD_H
#include <unistd.h>
#endif

/* GLU library includes. */
#include "nusmv/core/utils/utils.h"
#include "cudd/util.h"
#include "cudd/st.h"
#include "nusmv/core/utils/list.h"

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

/* Default parameters for the unique table. */

#define DAG_DEFAULT_VERTICES_NO    65537

#define DAG_DEFAULT_DENSITY           20

#define DAG_DEFAULT_GROWTH           1.5

/* Constants for setting and clearing pointer annotation bit which is
   lowest (rightmost) bit.
*/
#if !defined(NUSMV_SIZEOF_VOID_P) || !defined(NUSMV_SIZEOF_LONG)
#error Constants NUSMV_SIZEOF_VOID_P and NUSMV_SIZEOF_LONG must be defined
#endif

#if (NUSMV_SIZEOF_VOID_P == NUSMV_SIZEOF_LONG)
/* The lowest bit of a pointer is used to store additional info
   (about complementation). We can use this bit only because pointers
   never use it (it is always 0 for any pointer). This is
   ensured by the alignment of pointers which is required to be at
   least 2 bytes.

   Note: in past the highest (leftmost) bit was used as the annotation
   bit. But it appeared that if the library is invoked from Java on
   multi-processor machine then malloc behaves differently and it is
   possible for a pointer to be from the higher half of memory, i.e.
   in memory address the highest bit could be 0 as well as 1. As
   result we could not use it any more and changed the
   implementation.

   Current implementation is similar to CUDD's one.

   Warning: on most machine alignment is 4 bytes which is more than
   enough for us.  However in some case additional compilation options
   (e.g. -malign-double) may be required to force proper alignment.
*/
# define DAG_ANNOTATION_BIT  ((nusmv_ptrint) 1)
#else
/* this fallback setting is for 32-bit only */
/* Size of pointers and long are different (may hide a serious problem) */
# define DAG_ANNOTATION_BIT   ((nusmv_ptrint) 1)
#endif


/* Dag statistics. */

#define DAG_NODE_NO  (int)  0  /* How many nodes created (overall). */

#define DAG_GC_NO    (int)  1  /* How many nodes collected. */

#define DAG_MAX_STAT (int)  2

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/* WARNING [MD] BAD! Using those we lose the check on function parameters!
   They should be substituted */
/* typedef void  (*Dag_ProcPtr_t)(); */   /* Procedures. */
/* typedef int   (*Dag_IntPtr_t)();  */   /* Functions returning int. */

typedef struct DagManager       Dag_Manager_t;       /* The dag manager. */
typedef struct Dag_Vertex       Dag_Vertex_t;        /* The vertices. */
typedef struct Dag_DfsFunctions Dag_DfsFunctions_t;  /* Depth First Search. */

typedef void (*PF_VPVPCPI)(void*, char*, nusmv_ptrint);

typedef int (*PF_IVPCPI)(void*, char*, nusmv_ptrint);
typedef void (*PF_VPCP)(char*);

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

struct Dag_Vertex {
  int             symbol;
  char          * data;

  Dag_Vertex_t* * outList;
  unsigned        numSons;

  Dag_Manager_t * dag;
  int             mark;
  int             visit;
  lsHandle        vHandle;

  char          * gRef;
  int             iRef;
};


/* struct Dag_DfsFunctions { */
/*   Dag_IntPtr_t   Set; */
/*   Dag_ProcPtr_t  FirstVisit; */
/*   Dag_ProcPtr_t  BackVisit; */
/*   Dag_ProcPtr_t  LastVisit; */
/* }; */

struct Dag_DfsFunctions {
  PF_IVPCPI Set;
  PF_VPVPCPI FirstVisit;
  PF_VPVPCPI BackVisit;
  PF_VPVPCPI LastVisit;
};

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

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

#define Dag_VertexGetRef(p)\
((Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))

#define Dag_VertexSet(p)\
(p = (Dag_Vertex_t*)((nusmv_ptrint)p | DAG_ANNOTATION_BIT))

#define Dag_VertexClear(p)\
(p = (Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT)))

#define Dag_VertexIsSet(p)\
((nusmv_ptrint)p & DAG_ANNOTATION_BIT)

#define DagId(r,s) \
  (Dag_Vertex_t*)((nusmv_ptrint)s ^ (nusmv_ptrint)r)

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

void
Dag_Dfs(Dag_Vertex_t* dfsRoot, Dag_DfsFunctions_t* dfsFun, char* dfsData);

Dag_Manager_t* Dag_ManagerAlloc(void);

Dag_Manager_t*
Dag_ManagerAllocWithParams(int dagInitVerticesNo, int maxDensity,
                           int growthFactor);

void
Dag_ManagerFree(Dag_Manager_t* dagManager, PF_VPCP freeData,
                PF_VPCP freeGen);

void
Dag_ManagerGC(Dag_Manager_t* dagManager, PF_VPCP freeData,
              PF_VPCP freeGen);

Dag_DfsFunctions_t* Dag_ManagerGetDfsCleanFun(Dag_Manager_t* dagManager);

void Dag_PrintStats(Dag_Manager_t* dagManager, int clustSz,
                           FILE* outFile);

Dag_Vertex_t*
Dag_VertexLookup(Dag_Manager_t* dagManager,
                 int vSymb,
                 char* vData,
                 Dag_Vertex_t** vSons,
                 unsigned numSons);

Dag_Vertex_t*
Dag_VertexInsert(Dag_Manager_t* dagManager,
                 int vSymb,
                 char* vData,
                 Dag_Vertex_t** vSons,
                 unsigned numSons);

void Dag_VertexMark(Dag_Vertex_t* v);

void Dag_VertexUnmark(Dag_Vertex_t* v);

void PrintStat(Dag_Vertex_t* dfsRoot, FILE* statFile, char* prefix);

#endif /* __NUSMV_CORE_DAG_DAG_H__ */

---