cudd
3.0.0
The University of Colorado Decision Diagram Package
|
Go to the documentation of this file.
64 #define PI_PS_FROM_FILE 0
68 #define NTR_IMAGE_MONO 0
69 #define NTR_IMAGE_PART 1
70 #define NTR_IMAGE_CLIP 2
71 #define NTR_IMAGE_DEPEND 3
73 #define NTR_UNDER_APPROX 0
74 #define NTR_OVER_APPROX 1
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
84 #define NTR_GROUP_NONE 0
85 #define NTR_GROUP_DEFAULT 1
86 #define NTR_GROUP_FIXED 2
88 #define NTR_SHORT_NONE 0
89 #define NTR_SHORT_BELLMAN 1
90 #define NTR_SHORT_FLOYD 2
91 #define NTR_SHORT_SQUARE 3
230 #define STRING_EQUAL(s1,s2) (strcmp((s1),(s2)) == 0)
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);
Specialized DD symbol table.
Definition: cuddInt.h:395
int progress
Definition: ntr.h:142
struct NtrPartTR NtrPartTR
Data structure for partitioned transition relation.
int nodrop
Definition: ntr.h:164
int store
Definition: ntr.h:173
struct NtrOptions NtrOptions
Options for nanotrav.
NtrHeap * factors
Definition: ntr.h:203
int cacheSize
Definition: ntr.h:143
int stateOnly
Definition: ntr.h:139
size_t maxMemHard
Definition: ntr.h:145
DdNode ** nscube
Definition: ntr.h:199
Cudd_ReorderingType autoMethod
Definition: ntr.h:152
Options for nanotrav.
Definition: ntr.h:104
Entry of NtrHeap.
Definition: ntrHeap.c:66
DdNode * xw
Definition: ntr.h:202
double clip
Definition: ntr.h:134
size_t maxMemory
Definition: ntr.h:144
int populationSize
Definition: ntr.h:167
DdNode ** part
Definition: ntr.h:196
int traverse
Definition: ntr.h:110
Cudd_ReorderingType reordering
Definition: ntr.h:150
int Ntr_Envelope(DdManager *dd, NtrPartTR *TR, FILE *dfp, NtrOptions *option)
Poor man's outer envelope computation.
Definition: ntr.c:1535
int selectiveTrace
Definition: ntr.h:126
char * storefile
Definition: ntr.h:174
int dontcares
Definition: ntr.h:135
int second
Definition: ntr.h:109
char * treefile
Definition: ntr.h:153
int Ntr_TestDensity(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests BDD density-related functions.
Definition: ntrBddTest.c:185
int locGlob
Definition: ntr.h:141
int Ntr_SCC(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Computes the SCCs of the STG.
Definition: ntr.c:934
int dumpFmt
Definition: ntr.h:170
Very simple boolean network data structure.
Definition: bnet.h:138
int32_t seed
Definition: ntr.h:178
int shortPath
Definition: ntr.h:125
int ordering
Definition: ntr.h:148
int approx
Definition: ntr.h:114
int char2vect
Definition: ntr.h:129
int Ntr_TestClosestCube(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests the Cudd_bddClosestCube function.
Definition: ntrBddTest.c:556
int image
Definition: ntr.h:112
int Ntr_TestDecomp(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests BDD decomposition functions.
Definition: ntrBddTest.c:232
int gaOnOff
Definition: ntr.h:166
Decision diagram node.
Definition: cuddInt.h:257
NtrHeap * Ntr_InitHeap(int size)
Initializes a priority queue.
Definition: ntrHeap.c:127
int signatures
Definition: ntr.h:165
Cudd_AggregationType
Type of aggregation methods.
Definition: cudd.h:123
int partition
Definition: ntr.h:128
int Ntr_TestMinimization(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD minimization functions.
Definition: ntrBddTest.c:116
int Ntr_maxflow(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Maximum 0-1 flow between source and sink states.
Definition: ntr.c:1639
int countDead
Definition: ntr.h:155
void Ntr_freeTR(DdManager *dd, NtrPartTR *TR)
Frees the transition relation for a network.
Definition: ntr.c:625
int firstReorder
Definition: ntr.h:154
int clauses
Definition: ntr.h:137
int Ntr_testZDD(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests ZDDs.
Definition: ntrZddTest.c:95
int bdddump
Definition: ntr.h:169
NtrPartTR * Ntr_cloneTR(NtrPartTR *TR)
Makes a copy of a transition relation.
Definition: ntr.c:669
int Ntr_VerifyEquivalence(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Verify equivalence of combinational networks.
Definition: ntrBddTest.c:285
int nparts
Definition: ntr.h:195
int arcviolation
Definition: ntr.h:159
int maxflow
Definition: ntr.h:124
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
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
int Ntr_ClosureTrav(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Transitive closure traversal procedure.
Definition: ntr.c:1180
double closureClip
Definition: ntr.h:119
int maxGrowth
Definition: ntr.h:157
DdNode * preiabs
Definition: ntr.h:200
char * file2
Definition: ntr.h:108
char * orderPiPs
Definition: ntr.h:149
DdNode ** y
Definition: ntr.h:206
NtrHeap * Ntr_HeapClone(NtrHeap *source)
Clones a priority queue.
Definition: ntrHeap.c:256
int Ntr_ShortestPaths(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Computes shortest paths in a state graph.
Definition: ntrShort.c:110
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
int load
Definition: ntr.h:175
int depend
Definition: ntr.h:111
int recomb
Definition: ntr.h:163
int density
Definition: ntr.h:130
char * loadfile
Definition: ntr.h:176
char * sinkfile
Definition: ntr.h:127
int zddtest
Definition: ntr.h:122
double imageClip
Definition: ntr.h:113
int envelope
Definition: ntr.h:120
int Ntr_TestCofactorEstimate(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Tests BDD cofactor estimate functions.
Definition: ntrBddTest.c:352
int decomp
Definition: ntr.h:132
int groupnsps
Definition: ntr.h:117
Cudd_AggregationType groupcheck
Definition: ntr.h:158
char * dumpfile
Definition: ntr.h:172
int Ntr_HeapCount(NtrHeap *heap)
Returns the number of items in a priority queue.
Definition: ntrHeap.c:239
int verify
Definition: ntr.h:106
char * node
Definition: ntr.h:140
Simple-minded package to read a blif file.
int symmviolation
Definition: ntr.h:161
int numberXovers
Definition: ntr.h:168
DdNode ** x
Definition: ntr.h:205
Heap-based priority queue.
Definition: ntrHeap.c:74
Data structure for partitioned transition relation.
Definition: ntr.h:194
int threshold
Definition: ntr.h:115
char * file1
Definition: ntr.h:107
Cudd_ReorderingType
Type of reordering algorithm.
Definition: cudd.h:94
int Ntr_TestHeap(NtrHeap *heap, int i)
Tests the heap property of a priority queue.
Definition: ntrHeap.c:305
int scc
Definition: ntr.h:121
double quality
Definition: ntr.h:131
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
int closure
Definition: ntr.h:118
int Ntr_Trav(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Poor man's traversal procedure.
Definition: ntr.c:777
DdNode ** pcube
Definition: ntr.h:198
DdNode ** icube
Definition: ntr.h:197
int autoDyn
Definition: ntr.h:151
void Ntr_FreeHeap(NtrHeap *heap)
Frees a priority queue.
Definition: ntrHeap.c:155
int Ntr_TestEquivAndContain(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD equivalence and containment with don't cares.
Definition: ntrBddTest.c:472
int closestCube
Definition: ntr.h:136
int slots
Definition: ntr.h:147
long initialTime
Definition: ntr.h:105
int Ntr_TestCharToVect(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Test char-to-vect conversion.
Definition: ntrBddTest.c:738
int printcover
Definition: ntr.h:123
int noBuild
Definition: ntr.h:138
int Ntr_TestClipping(DdManager *dd, BnetNetwork *net1, BnetNetwork *net2, NtrOptions *option)
Tests BDD clipping functions.
Definition: ntrBddTest.c:399
int Ntr_TestTwoLiteralClauses(DdManager *dd, BnetNetwork *net1, NtrOptions *option)
Tests extraction of two-literal clauses.
Definition: ntrBddTest.c:652
DdNode * prepabs
Definition: ntr.h:201
DdNode * Ntr_TransitiveClosure(DdManager *dd, NtrPartTR *TR, NtrOptions *option)
Builds the transitive closure of a transition relation.
Definition: ntr.c:1266
DdNode * Ntr_initState(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Builds the BDD of the initial state(s).
Definition: ntr.c:1366
int Ntr_HeapExtractMin(NtrHeap *heap, void *item, int *key)
Extracts the element with the minimum key from a priority queue.
Definition: ntrHeap.c:212
unsigned int maxLive
Definition: ntr.h:146
int verb
Definition: ntr.h:177
int Ntr_testISOP(DdManager *dd, BnetNetwork *net, NtrOptions *option)
Builds ZDD covers.
Definition: ntrZddTest.c:302
int nlatches
Definition: ntr.h:204
int cofest
Definition: ntr.h:133
int Ntr_HeapInsert(NtrHeap *heap, void *item, int key)
Inserts an item in a priority queue.
Definition: ntrHeap.c:176
NtrPartTR * Ntr_buildTR(DdManager *dd, BnetNetwork *net, NtrOptions *option, int image)
Builds the transition relation for a network.
Definition: ntr.c:329
int from
Definition: ntr.h:116