#include "nusmv/core/utils/utils.h"
#include "cudd/util.h"
#include "cudd/st.h"
#include "nusmv/core/utils/list.h"
Go to the source code of this file.
Data Structures | |
struct | Dag_DfsFunctions_t |
DFS function struct. More... | |
struct | Dag_Vertex_t |
DAG vertex. More... | |
Defines | |
#define | DAG_ANNOTATION_BIT ((nusmv_ptrint) 1) |
#define | DAG_DEFAULT_DENSITY 20 |
#define | DAG_DEFAULT_GROWTH 1.5 |
#define | DAG_DEFAULT_VERTICES_NO 65537 |
Directed acyclic graphs with sharing. | |
#define | DAG_GC_NO (int) 1 |
#define | DAG_MAX_STAT (int) 2 |
#define | DAG_NODE_NO (int) 0 |
#define | Dag_VertexClear(p) (p = (Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT))) |
Clears (forces) a bit annotation to 0. | |
#define | Dag_VertexGetRef(p) ((Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT))) |
Filters a pointer from bit annotations. | |
#define | Dag_VertexIsSet(p) ((nusmv_ptrint)p & DAG_ANNOTATION_BIT) |
Tests if the edge is annotated. | |
#define | Dag_VertexSet(p) (p = (Dag_Vertex_t*)((nusmv_ptrint)p | DAG_ANNOTATION_BIT)) |
Sets (forces) a bit annotation to 1. | |
#define | DagId(r, s) (Dag_Vertex_t*)((nusmv_ptrint)s ^ (nusmv_ptrint)r) |
Controls the sign of a dag. | |
Typedefs | |
typedef int(* | PF_IVPCPI )(void *, char *, nusmv_ptrint) |
typedef void(* | PF_VPCP )(char *) |
typedef void(* | PF_VPVPCPI )(void *, char *, nusmv_ptrint) |
Functions | |
void | Dag_Dfs (Dag_Vertex_t *dfsRoot, Dag_DfsFunctions_t *dfsFun, char *dfsData) |
Dag_Manager_t * | Dag_ManagerAlloc (void) |
Creates a new DAG manager. | |
Dag_Manager_t * | Dag_ManagerAllocWithParams (int dagInitVerticesNo, int maxDensity, int growthFactor) |
void | Dag_ManagerFree (Dag_Manager_t *dagManager, PF_VPCP freeData, PF_VPCP freeGen) |
Deallocates a DAG manager. | |
void | Dag_ManagerGC (Dag_Manager_t *dagManager, PF_VPCP freeData, PF_VPCP freeGen) |
Garbage collects the DAG manager. | |
Dag_DfsFunctions_t * | Dag_ManagerGetDfsCleanFun (Dag_Manager_t *dagManager) |
void | Dag_PrintStats (Dag_Manager_t *dagManager, int clustSz, FILE *outFile) |
Prints various statistics. | |
Dag_Vertex_t * | Dag_VertexInsert (Dag_Manager_t *dagManager, int vSymb, char *vData, Dag_Vertex_t **vSons, unsigned numSons) |
Vertex insert. | |
Dag_Vertex_t * | Dag_VertexLookup (Dag_Manager_t *dagManager, int vSymb, char *vData, Dag_Vertex_t **vSons, unsigned numSons) |
Vertex lookup. | |
void | Dag_VertexMark (Dag_Vertex_t *v) |
Marks a vertex as permanent. | |
void | Dag_VertexUnmark (Dag_Vertex_t *v) |
Unmarks a vertex (makes it volatile). | |
void | PrintStat (Dag_Vertex_t *dfsRoot, FILE *statFile, char *prefix) |
Visit a DAG to compute some statistics. |
#define DAG_ANNOTATION_BIT ((nusmv_ptrint) 1) |
#define DAG_DEFAULT_VERTICES_NO 65537 |
#define Dag_VertexClear | ( | p | ) | (p = (Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT))) |
Clears (forces) a bit annotation to 0.
The annotation bit is forced to 0 by a bitwise-and with complement of DAG_ANNOTATION_BIT mask.
The value of p changes to the purified value.
#define Dag_VertexGetRef | ( | p | ) | ((Dag_Vertex_t*)((nusmv_ptrint)p & (~ DAG_ANNOTATION_BIT))) |
Filters a pointer from bit annotations.
The annotation bit is filtered to 0. The result is the pointer purified from the bit annotation.
none
#define Dag_VertexIsSet | ( | p | ) | ((nusmv_ptrint)p & DAG_ANNOTATION_BIT) |
Tests if the edge is annotated.
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)
none
#define Dag_VertexSet | ( | p | ) | (p = (Dag_Vertex_t*)((nusmv_ptrint)p | DAG_ANNOTATION_BIT)) |
Sets (forces) a bit annotation to 1.
The annotation bit is forced to 1 by a bitwise-or with DAG_ANNOTATION_BIT mask.
The value of p changes to the purified value.
#define DagId | ( | r, | |||
s | ) | (Dag_Vertex_t*)((nusmv_ptrint)s ^ (nusmv_ptrint)r) |
Controls the sign of a dag.
The pointer is filtered by a bitwise-xor with either DAG_ANNOTATION_BIT or !DAG_ANNOTATION_BIT. The pointer is not altered, but the leftmost bit is complemented when s==DAG_ANNOTATION_BIT and goes unchanged when s!=DAG_ANNOTATION_BIT.
none
typedef int(* PF_IVPCPI)(void *, char *, nusmv_ptrint) |
typedef void(* PF_VPCP)(char *) |
typedef void(* PF_VPVPCPI)(void *, char *, nusmv_ptrint) |
void Dag_Dfs | ( | Dag_Vertex_t * | dfsRoot, | |
Dag_DfsFunctions_t * | dfsFun, | |||
char * | dfsData | |||
) |
Dag_Manager_t* Dag_ManagerAlloc | ( | void | ) |
Creates a new DAG manager.
Allocates the unique table (vTable) and the free list (gcList). Initializes the counters for various statistics (stats). Returns the pointer to the dag manager.
none
Dag_Manager_t* Dag_ManagerAllocWithParams | ( | int | dagInitVerticesNo, | |
int | maxDensity, | |||
int | growthFactor | |||
) |
Deallocates a DAG manager.
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)'.
none
Garbage collects the DAG manager.
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)'.
none
Dag_DfsFunctions_t* Dag_ManagerGetDfsCleanFun | ( | Dag_Manager_t * | dagManager | ) |
void Dag_PrintStats | ( | Dag_Manager_t * | dagManager, | |
int | clustSz, | |||
FILE * | outFile | |||
) |
Prints various statistics.
Prints the following:
none
Dag_Vertex_t* Dag_VertexInsert | ( | Dag_Manager_t * | dagManager, | |
int | vSymb, | |||
char * | vData, | |||
Dag_Vertex_t ** | vSons, | |||
unsigned | numSons | |||
) |
Vertex insert.
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.
none
Dag_Vertex_t* Dag_VertexLookup | ( | Dag_Manager_t * | dagManager, | |
int | vSymb, | |||
char * | vData, | |||
Dag_Vertex_t ** | vSons, | |||
unsigned | numSons | |||
) |
Vertex lookup.
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.
none
void Dag_VertexMark | ( | Dag_Vertex_t * | v | ) |
Marks a vertex as permanent.
Increments the vertex mark by one, so it cannot be deleted by garbage collection unless unmarked.
none
void Dag_VertexUnmark | ( | Dag_Vertex_t * | v | ) |
Unmarks a vertex (makes it volatile).
Decrements the vertex mark by one, so it can be deleted by garbage collection when fatherless.
none
void PrintStat | ( | Dag_Vertex_t * | dfsRoot, | |
FILE * | statFile, | |||
char * | prefix | |||
) |
Visit a DAG to compute some statistics.
Calls Depth First Search on the DAG dfsRoot to populate the struct Statistics. Then calls _PrintStat to print out them.