Internal functions and data structures of the dag package.

static void 
CleanBack(
  Dag_Vertex_t * f, 
  char * cleanData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for cleaning.

Side Effects None

Defined in dagDfs.c

static void 
CleanFirst(
  Dag_Vertex_t * f, 
  char * cleanData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for cleaning.

Side Effects None

Defined in dagDfs.c

static void 
CleanLast(
  Dag_Vertex_t * f, 
  char * cleanData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for cleaning.

Side Effects None

Defined in dagDfs.c

static int 
CleanSet(
  Dag_Vertex_t * f, 
  char * cleanData, 
  nusmv_ptrint  sign 
)
Dfs Set for cleaning.

Side Effects None

Defined in dagDfs.c

static void 
DFS(
  Dag_Vertex_t * v, 
  Dag_DfsFunctions_t * dfsFun, 
  char * dfsData, 
  nusmv_ptrint  vBit 
)
The parameters are:

Side Effects none

Defined in dagDfs.c

int 
DagVertexComp(
  const char * v1, 
  const char * v2 
)
Gets two vertex pointers v1, v2, (as char pointers) and compares the symbol, the generic data reference and the pointers to the sons. Returns -1 if v1 < v2, 0 if v1 = v2 and 1 if v1 > v2, in lexicographic order of fields.

Side Effects None

Defined in dagVertex.c

int 
DagVertexHash(
  char* v, 
  int  modulus 
)
Calculate a preliminary index as follows: v -> symbol + 8 low order bits of (int) (v -> data) + 16 low order bits of each son up to MAXSON + 1 for each son whose edge is annotated Return the modulus of the index and the actual hash size.

Side Effects None

Defined in dagVertex.c

void 
DagVertexInit(
  Dag_Manager_t * dagManager, 
  Dag_Vertex_t * v 
)
Performs several tasks:

Side Effects none

Defined in dagVertex.c

void 
Dag_Dfs(
  Dag_Vertex_t* dfsRoot, 
  Dag_DfsFunctions_t* dfsFun, 
  char* dfsData 
)
The parameters are: The function increments the DFS code for the dag manager owning dfsRoot and starts the DFS. Increment of the code guarantees that each node is visited once and only once. dfsFun -> Set() may change the default behaviour by forcing to DFS to visit nodes more than once, or by preventing DFS to do a complete visit.

Side Effects none

Defined in dagDfs.c

Dag_Manager_t * 
Dag_ManagerAlloc(
    
)
Allocates the unique table (vTable) and the free list (gcList). Initializes the counters for various statistics (stats). Returns the pointer to the dag manager.

Side Effects none

See Also Dag_ManagerAllocWithParams Dag_ManagerFree
Defined in dagManager.c

void 
Dag_ManagerFree(
  Dag_Manager_t * dagManager, 
  Dag_ProcPtr_t  freeData, 
  Dag_ProcPtr_t  freeGen 
)
Forces a total garbage collection and then deallocates the dag manager. `freeData' can be used to deallocate `data' fields (user data pointers) in the nodes, while `freeGen' is applied to `gRef' fields (user generic pointers). `freeData' and `freeGen' are in the form `void f(char * r)'.

Side Effects none

See Also Dag_ManagerGC
Defined in dagManager.c

void 
Dag_ManagerGC(
  Dag_Manager_t * dagManager, 
  Dag_ProcPtr_t  freeData, 
  Dag_ProcPtr_t  freeGen 
)
Sweeps out useless vertices, i.e., vertices that are not marked as permanent, that are not descendants of permanent vertices, or whose brother (if any) is neither permanent nor descendant of a permanent vertex. The search starts from vertices that are in the garbage bin and whose mark is 0. `freeData' can be used to deallocate `data' fields (user data pointers) in the nodes, while `freeGen' is applied to `gRef' fields (user generic pointers). `freeData' and `freeGen' are in the form `void f(char * r)'.

Side Effects none

See Also Dag_ManagerFree
Defined in dagManager.c

void 
Dag_PrintStats(
  Dag_Manager_t * dagManager, 
  int  clustSz, 
  FILE * outFile 
)
Prints the following:

Side Effects none

Defined in dagStat.c

Dag_Vertex_t * 
Dag_VertexInsert(
  Dag_Manager_t * dagManager, 
  int  vSymb, 
  char * vData, 
  Dag_Vertex_t ** vSons, 
  unsigned  numSons 
)
Adds a vertex into the DAG and returns a reference to it: Returns NIL(Dag_vertex_t) if there is no dagManager and if vSymb is negative.

Side Effects none

Defined in dagVertex.c

Dag_Vertex_t * 
Dag_VertexLookup(
  Dag_Manager_t * dagManager, 
  int  vSymb, 
  char * vData, 
  Dag_Vertex_t** vSons, 
  unsigned  numSons 
)
Uniquely adds a new vertex into the DAG and returns a reference to it: Returns NIL(Dag_vertex_t) if there is no dagManager and if vSymb is negative.

Side Effects none

Defined in dagVertex.c

void 
Dag_VertexMark(
  Dag_Vertex_t * v 
)
Increments the vertex mark by one, so it cannot be deleted by garbage collection unless unmarked.

Side Effects none

Defined in dagVertex.c

void 
Dag_VertexUnmark(
  Dag_Vertex_t * v 
)
Decrements the vertex mark by one, so it can be deleted by garbage collection when fatherless.

Side Effects none

Defined in dagVertex.c

static void 
GC(
  Dag_Vertex_t * v, 
  Dag_ProcPtr_t  freeData, 
  Dag_ProcPtr_t  freeGen 
)
Gets a vertex to be freed. If the vertex has permanent or non-orphan brothers it is rescued. Otherwise the brother is unconnected and the sons marks are updated. GC is then propagated to each fatherless son.

Side Effects none

Defined in dagManager.c

 
(
    
)
The annotation bit is forced to 0 by a bitwise-and with complement of DAG_ANNOTATION_BIT mask.

Side Effects The value of p changes to the purified value.

Defined in dag.h

 
(
    
)
The annotation bit is filtered to 0. The result is the pointer purified from the bit annotation.

Side Effects none

Defined in dag.h

 
(
    
)
The annotation bit is forced to 1 by a bitwise-or with DAG_ANNOTATION_BIT mask.

Side Effects The value of p changes to the purified value.

Defined in dag.h

 
(
    
)
Uses a bitwise-and with DAG_ANNOTATION_BIT to test the annotation bit of p. The result is either 0(false) or not 0(true)

Side Effects none

Defined in dag.h

Last updated on 2010/11/03 21h:54