cudd  3.0.0
The University of Colorado Decision Diagram Package
ntr.h
Go to the documentation of this file.
1 
46 #ifndef _NTR
47 #define _NTR
48 
49 /*---------------------------------------------------------------------------*/
50 /* Nested includes */
51 /*---------------------------------------------------------------------------*/
52 
53 #include "dddmp.h"
54 #include "bnet.h"
55 
56 #ifdef __cplusplus
57 extern "C" {
58 #endif
59 
60 /*---------------------------------------------------------------------------*/
61 /* Constant declarations */
62 /*---------------------------------------------------------------------------*/
63 
64 #define PI_PS_FROM_FILE 0
65 #define PI_PS_DFS 1
66 #define PI_PS_GIVEN 2
67 
68 #define NTR_IMAGE_MONO 0
69 #define NTR_IMAGE_PART 1
70 #define NTR_IMAGE_CLIP 2
71 #define NTR_IMAGE_DEPEND 3
72 
73 #define NTR_UNDER_APPROX 0
74 #define NTR_OVER_APPROX 1
75 
76 #define NTR_FROM_NEW 0
77 #define NTR_FROM_REACHED 1
78 #define NTR_FROM_RESTRICT 2
79 #define NTR_FROM_COMPACT 3
80 #define NTR_FROM_SQUEEZE 4
81 #define NTR_FROM_UNDERAPPROX 5
82 #define NTR_FROM_OVERAPPROX 6
83 
84 #define NTR_GROUP_NONE 0
85 #define NTR_GROUP_DEFAULT 1
86 #define NTR_GROUP_FIXED 2
87 
88 #define NTR_SHORT_NONE 0
89 #define NTR_SHORT_BELLMAN 1
90 #define NTR_SHORT_FLOYD 2
91 #define NTR_SHORT_SQUARE 3
92 
93 /*---------------------------------------------------------------------------*/
94 /* Stucture declarations */
95 /*---------------------------------------------------------------------------*/
96 
97 /*---------------------------------------------------------------------------*/
98 /* Type declarations */
99 /*---------------------------------------------------------------------------*/
100 
104 typedef struct NtrOptions {
105  long initialTime;
106  int verify;
107  char *file1;
108  char *file2;
109  int second;
110  int traverse;
111  int depend;
112  int image;
113  double imageClip;
114  int approx;
115  int threshold;
116  int from;
117  int groupnsps;
118  int closure;
119  double closureClip;
120  int envelope;
121  int scc;
122  int zddtest;
124  int maxflow;
125  int shortPath;
127  char *sinkfile;
128  int partition;
129  int char2vect;
130  int density;
131  double quality;
132  int decomp;
133  int cofest;
134  double clip;
135  int dontcares;
137  int clauses;
138  int noBuild;
139  int stateOnly;
140  char *node;
141  int locGlob;
142  int progress;
143  int cacheSize;
144  size_t maxMemory;
145  size_t maxMemHard;
146  unsigned int maxLive;
147  int slots;
148  int ordering;
149  char *orderPiPs;
151  int autoDyn;
153  char *treefile;
155  int countDead;
157  int maxGrowth;
163  int recomb;
164  int nodrop;
166  int gaOnOff;
169  int bdddump;
170  int dumpFmt;
172  char *dumpfile;
173  int store;
174  char *storefile;
175  int load;
176  char *loadfile;
177  int verb;
178  int32_t seed;
179 } NtrOptions;
180 
184 typedef struct NtrHeapSlot NtrHeapSlot;
185 
189 typedef struct NtrHeap NtrHeap;
190 
194 typedef struct NtrPartTR {
195  int nparts;
204  int nlatches;
205  DdNode **x;
206  DdNode **y;
207 } NtrPartTR;
208 
209 /*---------------------------------------------------------------------------*/
210 /* Variable declarations */
211 /*---------------------------------------------------------------------------*/
212 
213 /*---------------------------------------------------------------------------*/
214 /* Macro declarations */
215 /*---------------------------------------------------------------------------*/
216 
217 #ifndef TRUE
218 # define TRUE 1
219 #endif
220 #ifndef FALSE
221 # define FALSE 0
222 #endif
223 
230 #define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
231 
232 
235 /*---------------------------------------------------------------------------*/
236 /* Function prototypes */
237 /*---------------------------------------------------------------------------*/
238 
239 extern int Ntr_buildDDs (BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2);
240 extern NtrPartTR * Ntr_buildTR (DdManager *dd, BnetNetwork *net, NtrOptions *option, int image);
241 extern DdNode * Ntr_TransitiveClosure (DdManager *dd, NtrPartTR *TR, NtrOptions *option);
242 extern int Ntr_Trav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
243 extern int Ntr_SCC (DdManager *dd, BnetNetwork *net, NtrOptions *option);
244 extern int Ntr_ClosureTrav (DdManager *dd, BnetNetwork *net, NtrOptions *option);
245 extern void Ntr_freeTR (DdManager *dd, NtrPartTR *TR);
246 extern NtrPartTR * Ntr_cloneTR (NtrPartTR *TR);
247 extern DdNode * Ntr_initState (DdManager *dd, BnetNetwork *net, NtrOptions *option);
248 extern DdNode * Ntr_getStateCube (DdManager *dd, BnetNetwork *net, char *filename, int pr);
249 extern int Ntr_Envelope (DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option);
250 extern int Ntr_TestMinimization (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
251 extern int Ntr_TestDensity (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
252 extern int Ntr_TestDecomp (DdManager *dd, BnetNetwork *net1, NtrOptions *option);
253 extern int Ntr_VerifyEquivalence (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
254 extern int Ntr_TestCofactorEstimate (DdManager * dd, BnetNetwork * net, NtrOptions * option);
255 extern int Ntr_TestClipping (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
256 extern int Ntr_TestEquivAndContain (DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option);
257 extern int Ntr_TestClosestCube (DdManager * dd, BnetNetwork * net, NtrOptions * option);
258 extern int Ntr_TestTwoLiteralClauses (DdManager * dd, BnetNetwork * net1, NtrOptions * option);
259 extern int Ntr_TestCharToVect(DdManager * dd, BnetNetwork * net1, NtrOptions * option);
260 extern int Ntr_maxflow (DdManager *dd, BnetNetwork *net, NtrOptions *option);
261 extern 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);
262 extern int Ntr_testZDD (DdManager *dd, BnetNetwork *net, NtrOptions *option);
263 extern int Ntr_testISOP (DdManager *dd, BnetNetwork *net, NtrOptions *option);
264 extern NtrHeap * Ntr_InitHeap (int size);
265 extern void Ntr_FreeHeap (NtrHeap *heap);
266 extern int Ntr_HeapInsert (NtrHeap *heap, void *item, int key);
267 extern int Ntr_HeapExtractMin (NtrHeap *heap, void *item, int *key);
268 extern int Ntr_HeapCount (NtrHeap *heap);
269 extern NtrHeap * Ntr_HeapClone (NtrHeap *source);
270 extern void Ntr_HeapForeach (NtrHeap *heap, void (*f)(void *e, void *arg), void *arg);
271 extern int Ntr_TestHeap (NtrHeap *heap, int i);
272 extern int Ntr_ShortestPaths (DdManager *dd, BnetNetwork *net, NtrOptions *option);
273 
277 #ifdef __cplusplus
278 }
279 #endif
280 
281 #endif /* _NTR */
DdManager
Specialized DD symbol table.
Definition: cuddInt.h:395
NtrOptions::progress
int progress
Definition: ntr.h:142
NtrPartTR
struct NtrPartTR NtrPartTR
Data structure for partitioned transition relation.
NtrOptions::nodrop
int nodrop
Definition: ntr.h:164
NtrOptions::store
int store
Definition: ntr.h:173
NtrOptions
struct NtrOptions NtrOptions
Options for nanotrav.
NtrPartTR::factors
NtrHeap * factors
Definition: ntr.h:203
NtrOptions::cacheSize
int cacheSize
Definition: ntr.h:143
NtrOptions::stateOnly
int stateOnly
Definition: ntr.h:139
NtrOptions::maxMemHard
size_t maxMemHard
Definition: ntr.h:145
NtrPartTR::nscube
DdNode ** nscube
Definition: ntr.h:199
NtrOptions::autoMethod
Cudd_ReorderingType autoMethod
Definition: ntr.h:152
NtrOptions
Options for nanotrav.
Definition: ntr.h:104
NtrHeapSlot
Entry of NtrHeap.
Definition: ntrHeap.c:66
NtrPartTR::xw
DdNode * xw
Definition: ntr.h:202
NtrOptions::clip
double clip
Definition: ntr.h:134
NtrOptions::maxMemory
size_t maxMemory
Definition: ntr.h:144
NtrOptions::populationSize
int populationSize
Definition: ntr.h:167
NtrPartTR::part
DdNode ** part
Definition: ntr.h:196
NtrOptions::traverse
int traverse
Definition: ntr.h:110
NtrOptions::reordering
Cudd_ReorderingType reordering
Definition: ntr.h:150
Ntr_Envelope
int Ntr_Envelope(DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option)
Poor man's outer envelope computation.
Definition: ntr.c:1535
NtrOptions::selectiveTrace
int selectiveTrace
Definition: ntr.h:126
NtrOptions::storefile
char * storefile
Definition: ntr.h:174
NtrOptions::dontcares
int dontcares
Definition: ntr.h:135
NtrOptions::second
int second
Definition: ntr.h:109
NtrOptions::treefile
char * treefile
Definition: ntr.h:153
Ntr_TestDensity
int Ntr_TestDensity(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests BDD density-related functions.
Definition: ntrBddTest.c:185
NtrOptions::locGlob
int locGlob
Definition: ntr.h:141
Ntr_SCC
int Ntr_SCC(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Computes the SCCs of the STG.
Definition: ntr.c:934
NtrOptions::dumpFmt
int dumpFmt
Definition: ntr.h:170
BnetNetwork
Very simple boolean network data structure.
Definition: bnet.h:138
NtrOptions::seed
int32_t seed
Definition: ntr.h:178
NtrOptions::shortPath
int shortPath
Definition: ntr.h:125
NtrOptions::ordering
int ordering
Definition: ntr.h:148
NtrOptions::approx
int approx
Definition: ntr.h:114
NtrOptions::char2vect
int char2vect
Definition: ntr.h:129
Ntr_TestClosestCube
int Ntr_TestClosestCube(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests the Cudd_bddClosestCube function.
Definition: ntrBddTest.c:556
NtrOptions::image
int image
Definition: ntr.h:112
Ntr_TestDecomp
int Ntr_TestDecomp(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests BDD decomposition functions.
Definition: ntrBddTest.c:232
NtrOptions::gaOnOff
int gaOnOff
Definition: ntr.h:166
DdNode
Decision diagram node.
Definition: cuddInt.h:257
Ntr_InitHeap
NtrHeap * Ntr_InitHeap(int size)
Initializes a priority queue.
Definition: ntrHeap.c:127
NtrOptions::signatures
int signatures
Definition: ntr.h:165
Cudd_AggregationType
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123
NtrOptions::partition
int partition
Definition: ntr.h:128
Ntr_TestMinimization
int Ntr_TestMinimization(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD minimization functions.
Definition: ntrBddTest.c:116
Ntr_maxflow
int Ntr_maxflow(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Maximum 0-1 flow between source and sink states.
Definition: ntr.c:1639
NtrOptions::countDead
int countDead
Definition: ntr.h:155
Ntr_freeTR
void Ntr_freeTR(DdManager *dd, NtrPartTR *TR)
Frees the transition relation for a network.
Definition: ntr.c:625
NtrOptions::firstReorder
int firstReorder
Definition: ntr.h:154
NtrOptions::clauses
int clauses
Definition: ntr.h:137
Ntr_testZDD
int Ntr_testZDD(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests ZDDs.
Definition: ntrZddTest.c:95
NtrOptions::bdddump
int bdddump
Definition: ntr.h:169
Ntr_cloneTR
NtrPartTR * Ntr_cloneTR(NtrPartTR *TR)
Makes a copy of a transition relation.
Definition: ntr.c:669
Ntr_VerifyEquivalence
int Ntr_VerifyEquivalence(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Verify equivalence of combinational networks.
Definition: ntrBddTest.c:285
NtrPartTR::nparts
int nparts
Definition: ntr.h:195
NtrOptions::arcviolation
int arcviolation
Definition: ntr.h:159
NtrOptions::maxflow
int maxflow
Definition: ntr.h:124
Ntr_HeapForeach
void Ntr_HeapForeach(NtrHeap *heap, void(*f)(void *e, void *arg), void *arg)
Calls a function on all items in a heap.
Definition: ntrHeap.c:282
Ntr_buildDDs
int Ntr_buildDDs(BnetNetwork *net, DdManager *dd, NtrOptions *option, BnetNetwork *net2)
Builds DDs for a network outputs and next state functions.
Definition: ntr.c:126
Ntr_ClosureTrav
int Ntr_ClosureTrav(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Transitive closure traversal procedure.
Definition: ntr.c:1180
NtrOptions::closureClip
double closureClip
Definition: ntr.h:119
NtrOptions::maxGrowth
int maxGrowth
Definition: ntr.h:157
NtrPartTR::preiabs
DdNode * preiabs
Definition: ntr.h:200
NtrOptions::file2
char * file2
Definition: ntr.h:108
NtrOptions::orderPiPs
char * orderPiPs
Definition: ntr.h:149
NtrPartTR::y
DdNode ** y
Definition: ntr.h:206
Ntr_HeapClone
NtrHeap * Ntr_HeapClone(NtrHeap *source)
Clones a priority queue.
Definition: ntrHeap.c:256
Ntr_ShortestPaths
int Ntr_ShortestPaths(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Computes shortest paths in a state graph.
Definition: ntrShort.c:110
Ntr_maximum01Flow
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)
Symbolic Dinit's algorithm.
Definition: ntrMflow.c:158
NtrOptions::load
int load
Definition: ntr.h:175
NtrOptions::depend
int depend
Definition: ntr.h:111
NtrOptions::recomb
int recomb
Definition: ntr.h:163
NtrOptions::density
int density
Definition: ntr.h:130
NtrOptions::loadfile
char * loadfile
Definition: ntr.h:176
NtrOptions::sinkfile
char * sinkfile
Definition: ntr.h:127
NtrOptions::zddtest
int zddtest
Definition: ntr.h:122
NtrOptions::imageClip
double imageClip
Definition: ntr.h:113
NtrOptions::envelope
int envelope
Definition: ntr.h:120
Ntr_TestCofactorEstimate
int Ntr_TestCofactorEstimate(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests BDD cofactor estimate functions.
Definition: ntrBddTest.c:352
NtrOptions::decomp
int decomp
Definition: ntr.h:132
NtrOptions::groupnsps
int groupnsps
Definition: ntr.h:117
NtrOptions::groupcheck
Cudd_AggregationType groupcheck
Definition: ntr.h:158
NtrOptions::dumpfile
char * dumpfile
Definition: ntr.h:172
Ntr_HeapCount
int Ntr_HeapCount(NtrHeap *heap)
Returns the number of items in a priority queue.
Definition: ntrHeap.c:239
NtrOptions::verify
int verify
Definition: ntr.h:106
NtrOptions::node
char * node
Definition: ntr.h:140
bnet.h
Simple-minded package to read a blif file.
NtrOptions::symmviolation
int symmviolation
Definition: ntr.h:161
NtrOptions::numberXovers
int numberXovers
Definition: ntr.h:168
NtrPartTR::x
DdNode ** x
Definition: ntr.h:205
NtrHeap
Heap-based priority queue.
Definition: ntrHeap.c:74
NtrPartTR
Data structure for partitioned transition relation.
Definition: ntr.h:194
NtrOptions::threshold
int threshold
Definition: ntr.h:115
NtrOptions::file1
char * file1
Definition: ntr.h:107
Cudd_ReorderingType
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94
Ntr_TestHeap
int Ntr_TestHeap(NtrHeap *heap, int i)
Tests the heap property of a priority queue.
Definition: ntrHeap.c:305
NtrOptions::scc
int scc
Definition: ntr.h:121
NtrOptions::quality
double quality
Definition: ntr.h:131
Ntr_getStateCube
DdNode * Ntr_getStateCube(DdManager *dd, BnetNetwork *net, char *filename, int pr)
Reads a state cube from a file or creates a random one.
Definition: ntr.c:1429
NtrOptions::closure
int closure
Definition: ntr.h:118
Ntr_Trav
int Ntr_Trav(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Poor man's traversal procedure.
Definition: ntr.c:777
NtrPartTR::pcube
DdNode ** pcube
Definition: ntr.h:198
NtrPartTR::icube
DdNode ** icube
Definition: ntr.h:197
NtrOptions::autoDyn
int autoDyn
Definition: ntr.h:151
Ntr_FreeHeap
void Ntr_FreeHeap(NtrHeap *heap)
Frees a priority queue.
Definition: ntrHeap.c:155
Ntr_TestEquivAndContain
int Ntr_TestEquivAndContain(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD equivalence and containment with don't cares.
Definition: ntrBddTest.c:472
NtrOptions::closestCube
int closestCube
Definition: ntr.h:136
NtrOptions::slots
int slots
Definition: ntr.h:147
NtrOptions::initialTime
long initialTime
Definition: ntr.h:105
Ntr_TestCharToVect
int Ntr_TestCharToVect(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Test char-to-vect conversion.
Definition: ntrBddTest.c:738
NtrOptions::printcover
int printcover
Definition: ntr.h:123
NtrOptions::noBuild
int noBuild
Definition: ntr.h:138
Ntr_TestClipping
int Ntr_TestClipping(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD clipping functions.
Definition: ntrBddTest.c:399
Ntr_TestTwoLiteralClauses
int Ntr_TestTwoLiteralClauses(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests extraction of two-literal clauses.
Definition: ntrBddTest.c:652
NtrPartTR::prepabs
DdNode * prepabs
Definition: ntr.h:201
Ntr_TransitiveClosure
DdNode * Ntr_TransitiveClosure(DdManager *dd, NtrPartTR *TR, NtrOptions *option)
Builds the transitive closure of a transition relation.
Definition: ntr.c:1266
Ntr_initState
DdNode * Ntr_initState(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Builds the BDD of the initial state(s).
Definition: ntr.c:1366
Ntr_HeapExtractMin
int Ntr_HeapExtractMin(NtrHeap *heap, void *item, int *key)
Extracts the element with the minimum key from a priority queue.
Definition: ntrHeap.c:212
NtrOptions::maxLive
unsigned int maxLive
Definition: ntr.h:146
NtrOptions::verb
int verb
Definition: ntr.h:177
Ntr_testISOP
int Ntr_testISOP(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Builds ZDD covers.
Definition: ntrZddTest.c:302
NtrPartTR::nlatches
int nlatches
Definition: ntr.h:204
NtrOptions::cofest
int cofest
Definition: ntr.h:133
Ntr_HeapInsert
int Ntr_HeapInsert(NtrHeap *heap, void *item, int key)
Inserts an item in a priority queue.
Definition: ntrHeap.c:176
Ntr_buildTR
NtrPartTR * Ntr_buildTR(DdManager *dd, BnetNetwork *net, NtrOptions *option, int image)
Builds the transition relation for a network.
Definition: ntr.c:329
NtrOptions::from
int from
Definition: ntr.h:116