source: icGREP/icgrep-devel/cudd-2.5.1/nanotrav/ntr.h @ 5815

Last change on this file since 5815 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 12.3 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [ntr.h]
4
5  PackageName [ntr]
6
7  Synopsis    [Simple-minded package to do traversal.]
8
9  Description []
10
11  SeeAlso     []
12
13  Author      [Fabio Somenzi]
14
15  Copyright   [Copyright (c) 1995-2012, Regents of the University of Colorado
16
17  All rights reserved.
18
19  Redistribution and use in source and binary forms, with or without
20  modification, are permitted provided that the following conditions
21  are met:
22
23  Redistributions of source code must retain the above copyright
24  notice, this list of conditions and the following disclaimer.
25
26  Redistributions in binary form must reproduce the above copyright
27  notice, this list of conditions and the following disclaimer in the
28  documentation and/or other materials provided with the distribution.
29
30  Neither the name of the University of Colorado nor the names of its
31  contributors may be used to endorse or promote products derived from
32  this software without specific prior written permission.
33
34  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45  POSSIBILITY OF SUCH DAMAGE.]
46
47  Revision    [$Id: ntr.h,v 1.28 2012/02/05 01:53:01 fabio Exp fabio $]
48
49******************************************************************************/
50
51#ifndef _NTR
52#define _NTR
53
54/*---------------------------------------------------------------------------*/
55/* Nested includes                                                           */
56/*---------------------------------------------------------------------------*/
57
58#include "dddmp.h"
59#include "bnet.h"
60
61#ifdef __cplusplus
62extern "C" {
63#endif
64
65/*---------------------------------------------------------------------------*/
66/* Constant declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69#define PI_PS_FROM_FILE 0
70#define PI_PS_DFS       1
71#define PI_PS_GIVEN     2
72
73#define NTR_IMAGE_MONO 0
74#define NTR_IMAGE_PART 1
75#define NTR_IMAGE_CLIP 2
76#define NTR_IMAGE_DEPEND 3
77
78#define NTR_UNDER_APPROX 0
79#define NTR_OVER_APPROX 1
80
81#define NTR_FROM_NEW 0
82#define NTR_FROM_REACHED 1
83#define NTR_FROM_RESTRICT 2
84#define NTR_FROM_COMPACT 3
85#define NTR_FROM_SQUEEZE 4
86#define NTR_FROM_UNDERAPPROX 5
87#define NTR_FROM_OVERAPPROX 6
88
89#define NTR_GROUP_NONE 0
90#define NTR_GROUP_DEFAULT 1
91#define NTR_GROUP_FIXED 2
92
93#define NTR_SHORT_NONE 0
94#define NTR_SHORT_BELLMAN 1
95#define NTR_SHORT_FLOYD 2
96#define NTR_SHORT_SQUARE 3
97
98/*---------------------------------------------------------------------------*/
99/* Stucture declarations                                                     */
100/*---------------------------------------------------------------------------*/
101
102/*---------------------------------------------------------------------------*/
103/* Type declarations                                                         */
104/*---------------------------------------------------------------------------*/
105
106typedef struct  NtrOptions {
107    long        initialTime;    /* this is here for convenience */
108    int         verify;         /* read two networks and compare them */
109    char        *file1;         /* first network file name */
110    char        *file2;         /* second network file name */
111    int         second;         /* a second network is given */
112    int         traverse;       /* do reachability analysis */
113    int         depend;         /* do latch dependence analysis */
114    int         image;          /* monolithic, partitioned, or clip */
115    double      imageClip;      /* clipping depth in image computation */
116    int         approx;         /* under or over approximation */
117    int         threshold;      /* approximation threshold */
118    int         from;           /* method to compute from states */
119    int         groupnsps;      /* group present state and next state vars */
120    int         closure;        /* use transitive closure */
121    double      closureClip;    /* clipping depth in closure computation */
122    int         envelope;       /* compute outer envelope */
123    int         scc;            /* compute strongly connected components */
124    int         zddtest;        /* do zdd test */
125    int         printcover;     /* print ISOP covers when testing ZDDs */
126    int         maxflow;        /* compute maximum flow in network */
127    int         shortPath;      /* compute shortest paths in network */
128    int         selectiveTrace; /* use selective trace in shortest paths */
129    char        *sinkfile;      /* file for externally provided sink node */
130    int         partition;      /* test McMillan conjunctive partitioning */
131    int         char2vect;      /* test char-to-vect decomposition */
132    int         density;        /* test density-related functions */
133    double      quality;        /* quality parameter for density functions */
134    int         decomp;         /* test decomposition functions */
135    int         cofest;         /* test cofactor estimation */
136    double      clip;           /* test clipping functions */
137    int         dontcares;      /* test equivalence and containment with DCs */
138    int         closestCube;    /* test Cudd_bddClosestCube */
139    int         clauses;        /* test extraction of two-literal clauses */
140    int         noBuild;        /* do not build BDDs; just echo order */
141    int         stateOnly;      /* ignore primary outputs */
142    char        *node;          /* only node for which to build BDD */
143    int         locGlob;        /* build global or local BDDs */
144    int         progress;       /* report output names while building BDDs */
145    int         cacheSize;      /* computed table initial size */
146    unsigned long maxMemory;    /* target maximum memory */
147    unsigned long maxMemHard;   /* maximum allowed memory */
148    unsigned int maxLive;       /* maximum number of nodes */
149    int         slots;          /* unique subtable initial slots */
150    int         ordering;       /* FANIN DFS ... */
151    char        *orderPiPs;     /* file for externally provided order */
152    Cudd_ReorderingType reordering; /* NONE RANDOM PIVOT SIFTING ... */
153    int         autoDyn;        /* ON OFF */
154    Cudd_ReorderingType autoMethod; /* RANDOM PIVOT SIFTING CONVERGE ... */
155    char        *treefile;      /* file name for variable tree */
156    int         firstReorder;   /* when to do first reordering */
157    int         countDead;      /* count dead nodes toward triggering
158                                   reordering */
159    int         maxGrowth;      /* maximum growth during reordering (%) */
160    Cudd_AggregationType groupcheck; /* grouping function */
161    int         arcviolation;   /* percent violation of arcs in
162                                   extended symmetry check */
163    int         symmviolation;  /* percent symm violation in
164                                   extended symmetry check */
165    int         recomb;         /* recombination parameter for grouping */
166    int         nodrop;         /* don't drop intermediate BDDs ASAP */
167    int         signatures;     /* computation of signatures */
168    int         gaOnOff;        /* whether to run GA at the end */
169    int         populationSize; /* population size for GA */
170    int         numberXovers;   /* number of crossovers for GA */
171    int         bdddump;        /* ON OFF */
172    int         dumpFmt;        /* 0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal
173                                ** 4 -> factored form */
174    char        *dumpfile;      /* filename for dump */
175    int         store;          /* iteration at which to store Reached */
176    char        *storefile;     /* filename for storing Reached */
177    int         load;           /* load initial states from file */
178    char        *loadfile;      /* filename for loading states */
179    int         verb;           /* level of verbosity */
180} NtrOptions;
181
182typedef struct NtrHeapSlot {
183    void *item;
184    int key;
185} NtrHeapSlot;
186
187typedef struct NtrHeap {
188    int size;
189    int nslots;
190    NtrHeapSlot *slots;
191} NtrHeap;
192
193typedef struct NtrPartTR {
194    int nparts;                 /* number of parts */
195    DdNode **part;              /* array of parts */
196    DdNode **icube;             /* quantification cubes for image */
197    DdNode **pcube;             /* quantification cubes for preimage */
198    DdNode **nscube;            /* next state variables in each part */
199    DdNode *preiabs;            /* present state vars and inputs in no part */
200    DdNode *prepabs;            /* inputs in no part */
201    DdNode *xw;                 /* cube of all present states and PIs */
202    NtrHeap *factors;           /* factors extracted from the image */
203    int nlatches;               /* number of latches */
204    DdNode **x;                 /* array of present state variables */
205    DdNode **y;                 /* array of next state variables */
206} NtrPartTR;
207
208/*---------------------------------------------------------------------------*/
209/* Variable declarations                                                     */
210/*---------------------------------------------------------------------------*/
211
212/*---------------------------------------------------------------------------*/
213/* Macro declarations                                                        */
214/*---------------------------------------------------------------------------*/
215
216#ifndef TRUE
217#   define TRUE 1
218#endif
219#ifndef FALSE
220#   define FALSE 0
221#endif
222
223/**Macro***********************************************************************
224
225  Synopsis     [Returns 1 if the two arguments are identical strings.]
226
227  Description  []
228
229  SideEffects  [none]
230
231  SeeAlso      []
232
233******************************************************************************/
234#define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
235
236
237/**AutomaticStart*************************************************************/
238
239/*---------------------------------------------------------------------------*/
240/* Function prototypes                                                       */
241/*---------------------------------------------------------------------------*/
242
243extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2);
244extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image);
245extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option);
246extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
247extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option);
248extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
249extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR);
250extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR);
251extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option);
252extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr);
253extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option);
254extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
255extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
256extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
257extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
258extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option);
259extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
260extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
261extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option);
262extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option);
263extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option);
264extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option);
265extern double Ntr_maximum01Flow (DdManager *bdd, DdNode *sx, DdNode *ty, DdNode *E, DdNode **F, DdNode **cut, DdNode **x, DdNode **y, DdNode **z, int n, int pr);
266extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option);
267extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option);
268extern NtrHeap * Ntr_InitHeap (int size);
269extern void Ntr_FreeHeap (NtrHeap *heap);
270extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key);
271extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key);
272extern int Ntr_HeapCount (NtrHeap *heap);
273extern NtrHeap * Ntr_HeapClone (NtrHeap *source);
274extern int Ntr_TestHeap (NtrHeap *heap, int i);
275extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option);
276
277/**AutomaticEnd***************************************************************/
278
279#ifdef __cplusplus
280}
281#endif
282
283#endif /* _NTR */
Note: See TracBrowser for help on using the repository browser.