1 /**CFile***********************************************************************
2
3 FileName [cuddSubsetSP.c]
4
5 PackageName [cudd]
6
7 Synopsis [Procedure to subset the given BDD choosing the shortest paths
8 (largest cubes) in the BDD.]
9
10
11 Description [External procedures included in this module:
12 <ul>
13 <li> Cudd_SubsetShortPaths()
14 <li> Cudd_SupersetShortPaths()
15 </ul>
16 Internal procedures included in this module:
17 <ul>
18 <li> cuddSubsetShortPaths()
19 </ul>
20 Static procedures included in this module:
21 <ul>
22 <li> BuildSubsetBdd()
23 <li> CreatePathTable()
24 <li> AssessPathLength()
25 <li> CreateTopDist()
26 <li> CreateBotDist()
27 <li> ResizeNodeDistPages()
28 <li> ResizeQueuePages()
29 <li> stPathTableDdFree()
30 </ul>
31 ]
32
33 SeeAlso [cuddSubsetHB.c]
34
35 Author [Kavita Ravi]
36
37 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
38
39 All rights reserved.
40
41 Redistribution and use in source and binary forms, with or without
42 modification, are permitted provided that the following conditions
43 are met:
44
45 Redistributions of source code must retain the above copyright
46 notice, this list of conditions and the following disclaimer.
47
48 Redistributions in binary form must reproduce the above copyright
49 notice, this list of conditions and the following disclaimer in the
50 documentation and/or other materials provided with the distribution.
51
52 Neither the name of the University of Colorado nor the names of its
53 contributors may be used to endorse or promote products derived from
54 this software without specific prior written permission.
55
56 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
57 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
58 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
59 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
60 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
61 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
62 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
63 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
64 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
65 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
66 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
67 POSSIBILITY OF SUCH DAMAGE.]
68
69 ******************************************************************************/
70
71 #include "misc/util/util_hack.h"
72 #include "cuddInt.h"
73
74 ABC_NAMESPACE_IMPL_START
75
76
77
78 /*---------------------------------------------------------------------------*/
79 /* Constant declarations */
80 /*---------------------------------------------------------------------------*/
81
82 #define DEFAULT_PAGE_SIZE 2048 /* page size to store the BFS queue element type */
83 #define DEFAULT_NODE_DIST_PAGE_SIZE 2048 /* page sizesto store NodeDist_t type */
84 #define MAXSHORTINT ((DdHalfWord) ~0) /* constant defined to store
85 * maximum distance of a node
86 * from the root or the
87 * constant
88 */
89 #define INITIAL_PAGES 128 /* number of initial pages for the
90 * queue/NodeDist_t type */
91
92 /*---------------------------------------------------------------------------*/
93 /* Stucture declarations */
94 /*---------------------------------------------------------------------------*/
95
96 /* structure created to store subset results for each node and distances with
97 * odd and even parity of the node from the root and sink. Main data structure
98 * in this procedure.
99 */
100 struct NodeDist{
101 DdHalfWord oddTopDist;
102 DdHalfWord evenTopDist;
103 DdHalfWord oddBotDist;
104 DdHalfWord evenBotDist;
105 DdNode *regResult;
106 DdNode *compResult;
107 };
108
109 /* assorted information needed by the BuildSubsetBdd procedure. */
110 struct AssortedInfo {
111 unsigned int maxpath;
112 int findShortestPath;
113 int thresholdReached;
114 st__table *maxpathTable;
115 int threshold;
116 };
117
118 /*---------------------------------------------------------------------------*/
119 /* Type declarations */
120 /*---------------------------------------------------------------------------*/
121
122 typedef struct NodeDist NodeDist_t;
123
124 /*---------------------------------------------------------------------------*/
125 /* Variable declarations */
126 /*---------------------------------------------------------------------------*/
127
128 #ifndef lint
129 static char rcsid[] DD_UNUSED = "$Id: cuddSubsetSP.c,v 1.34 2009/02/19 16:23:19 fabio Exp $";
130 #endif
131
132 #ifdef DD_DEBUG
133 static int numCalls;
134 static int hits;
135 static int thishit;
136 #endif
137
138
139 static int memOut; /* flag to indicate out of memory */
140 static DdNode *zero, *one; /* constant functions */
141
142 static NodeDist_t **nodeDistPages; /* pointers to the pages */
143 static int nodeDistPageIndex; /* index to next element */
144 static int nodeDistPage; /* index to current page */
145 static int nodeDistPageSize = DEFAULT_NODE_DIST_PAGE_SIZE; /* page size */
146 static int maxNodeDistPages; /* number of page pointers */
147 static NodeDist_t *currentNodeDistPage; /* current page */
148
149 static DdNode ***queuePages; /* pointers to the pages */
150 static int queuePageIndex; /* index to next element */
151 static int queuePage; /* index to current page */
152 static int queuePageSize = DEFAULT_PAGE_SIZE; /* page size */
153 static int maxQueuePages; /* number of page pointers */
154 static DdNode **currentQueuePage; /* current page */
155
156
157 /*---------------------------------------------------------------------------*/
158 /* Macro declarations */
159 /*---------------------------------------------------------------------------*/
160
161 /**AutomaticStart*************************************************************/
162
163 /*---------------------------------------------------------------------------*/
164 /* Static function prototypes */
165 /*---------------------------------------------------------------------------*/
166
167 static void ResizeNodeDistPages (void);
168 static void ResizeQueuePages (void);
169 static void CreateTopDist ( st__table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp);
170 static int CreateBotDist (DdNode *node, st__table *pathTable, unsigned int *pathLengthArray, FILE *fp);
171 static st__table * CreatePathTable (DdNode *node, unsigned int *pathLengthArray, FILE *fp);
172 static unsigned int AssessPathLength (unsigned int *pathLengthArray, int threshold, int numVars, unsigned int *excess, FILE *fp);
173 static DdNode * BuildSubsetBdd (DdManager *dd, st__table *pathTable, DdNode *node, struct AssortedInfo *info, st__table *subsetNodeTable);
174 static enum st__retval stPathTableDdFree (char *key, char *value, char *arg);
175
176 /**AutomaticEnd***************************************************************/
177
178 /*---------------------------------------------------------------------------*/
179 /* Definition of Exported functions */
180 /*---------------------------------------------------------------------------*/
181
182
183 /**Function********************************************************************
184
185 Synopsis [Extracts a dense subset from a BDD with the shortest paths
186 heuristic.]
187
188 Description [Extracts a dense subset from a BDD. This procedure
189 tries to preserve the shortest paths of the input BDD, because they
190 give many minterms and contribute few nodes. This procedure may
191 increase the number of nodes in trying to create the subset or
192 reduce the number of nodes due to recombination as compared to the
193 original BDD. Hence the threshold may not be strictly adhered to. In
194 practice, recombination overshadows the increase in the number of
195 nodes and results in small BDDs as compared to the threshold. The
196 hardlimit specifies whether threshold needs to be strictly adhered
197 to. If it is set to 1, the procedure ensures that result is never
198 larger than the specified limit but may be considerably less than
199 the threshold. Returns a pointer to the BDD for the subset if
200 successful; NULL otherwise. The value for numVars should be as
201 close as possible to the size of the support of f for better
202 efficiency. However, it is safe to pass the value returned by
203 Cudd_ReadSize for numVars. If 0 is passed, then the value returned
204 by Cudd_ReadSize is used.]
205
206 SideEffects [None]
207
208 SeeAlso [Cudd_SupersetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]
209
210 ******************************************************************************/
211 DdNode *
Cudd_SubsetShortPaths(DdManager * dd,DdNode * f,int numVars,int threshold,int hardlimit)212 Cudd_SubsetShortPaths(
213 DdManager * dd /* manager */,
214 DdNode * f /* function to be subset */,
215 int numVars /* number of variables in the support of f */,
216 int threshold /* maximum number of nodes in the subset */,
217 int hardlimit /* flag: 1 if threshold is a hard limit */)
218 {
219 DdNode *subset;
220
221 memOut = 0;
222 do {
223 dd->reordered = 0;
224 subset = cuddSubsetShortPaths(dd, f, numVars, threshold, hardlimit);
225 } while((dd->reordered ==1) && (!memOut));
226
227 return(subset);
228
229 } /* end of Cudd_SubsetShortPaths */
230
231
232 /**Function********************************************************************
233
234 Synopsis [Extracts a dense superset from a BDD with the shortest paths
235 heuristic.]
236
237 Description [Extracts a dense superset from a BDD. The procedure is
238 identical to the subset procedure except for the fact that it
239 receives the complement of the given function. Extracting the subset
240 of the complement function is equivalent to extracting the superset
241 of the function. This procedure tries to preserve the shortest
242 paths of the complement BDD, because they give many minterms and
243 contribute few nodes. This procedure may increase the number of
244 nodes in trying to create the superset or reduce the number of nodes
245 due to recombination as compared to the original BDD. Hence the
246 threshold may not be strictly adhered to. In practice, recombination
247 overshadows the increase in the number of nodes and results in small
248 BDDs as compared to the threshold. The hardlimit specifies whether
249 threshold needs to be strictly adhered to. If it is set to 1, the
250 procedure ensures that result is never larger than the specified
251 limit but may be considerably less than the threshold. Returns a
252 pointer to the BDD for the superset if successful; NULL
253 otherwise. The value for numVars should be as close as possible to
254 the size of the support of f for better efficiency. However, it is
255 safe to pass the value returned by Cudd_ReadSize for numVar. If 0
256 is passed, then the value returned by Cudd_ReadSize is used.]
257
258 SideEffects [None]
259
260 SeeAlso [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]
261
262 ******************************************************************************/
263 DdNode *
Cudd_SupersetShortPaths(DdManager * dd,DdNode * f,int numVars,int threshold,int hardlimit)264 Cudd_SupersetShortPaths(
265 DdManager * dd /* manager */,
266 DdNode * f /* function to be superset */,
267 int numVars /* number of variables in the support of f */,
268 int threshold /* maximum number of nodes in the subset */,
269 int hardlimit /* flag: 1 if threshold is a hard limit */)
270 {
271 DdNode *subset, *g;
272
273 g = Cudd_Not(f);
274 memOut = 0;
275 do {
276 dd->reordered = 0;
277 subset = cuddSubsetShortPaths(dd, g, numVars, threshold, hardlimit);
278 } while((dd->reordered ==1) && (!memOut));
279
280 return(Cudd_NotCond(subset, (subset != NULL)));
281
282 } /* end of Cudd_SupersetShortPaths */
283
284
285 /*---------------------------------------------------------------------------*/
286 /* Definition of internal functions */
287 /*---------------------------------------------------------------------------*/
288
289
290 /**Function********************************************************************
291
292 Synopsis [The outermost procedure to return a subset of the given BDD
293 with the shortest path lengths.]
294
295 Description [The outermost procedure to return a subset of the given
296 BDD with the largest cubes. The path lengths are calculated, the maximum
297 allowable path length is determined and the number of nodes of this
298 path length that can be used to build a subset. If the threshold is
299 larger than the size of the original BDD, the original BDD is
300 returned. ]
301
302 SideEffects [None]
303
304 SeeAlso [Cudd_SubsetShortPaths]
305
306 ******************************************************************************/
307 DdNode *
cuddSubsetShortPaths(DdManager * dd,DdNode * f,int numVars,int threshold,int hardlimit)308 cuddSubsetShortPaths(
309 DdManager * dd /* DD manager */,
310 DdNode * f /* function to be subset */,
311 int numVars /* total number of variables in consideration */,
312 int threshold /* maximum number of nodes allowed in the subset */,
313 int hardlimit /* flag determining whether thershold should be respected strictly */)
314 {
315 st__table *pathTable;
316 DdNode *N, *subset;
317
318 unsigned int *pathLengthArray;
319 unsigned int maxpath, oddLen, evenLen, pathLength, *excess;
320 int i;
321 NodeDist_t *nodeStat;
322 struct AssortedInfo *info;
323 st__table *subsetNodeTable;
324
325 one = DD_ONE(dd);
326 zero = Cudd_Not(one);
327
328 if (numVars == 0) {
329 /* set default value */
330 numVars = Cudd_ReadSize(dd);
331 }
332
333 if (threshold > numVars) {
334 threshold = threshold - numVars;
335 }
336 if (f == NULL) {
337 fprintf(dd->err, "Cannot partition, nil object\n");
338 dd->errorCode = CUDD_INVALID_ARG;
339 return(NULL);
340 }
341 if (Cudd_IsConstant(f))
342 return (f);
343
344 pathLengthArray = ABC_ALLOC(unsigned int, numVars+1);
345 for (i = 0; i < numVars+1; i++) pathLengthArray[i] = 0;
346
347
348 #ifdef DD_DEBUG
349 numCalls = 0;
350 #endif
351
352 pathTable = CreatePathTable(f, pathLengthArray, dd->err);
353
354 if ((pathTable == NULL) || (memOut)) {
355 if (pathTable != NULL)
356 st__free_table(pathTable);
357 ABC_FREE(pathLengthArray);
358 return (NIL(DdNode));
359 }
360
361 excess = ABC_ALLOC(unsigned int, 1);
362 *excess = 0;
363 maxpath = AssessPathLength(pathLengthArray, threshold, numVars, excess,
364 dd->err);
365
366 if (maxpath != (unsigned) (numVars + 1)) {
367
368 info = ABC_ALLOC(struct AssortedInfo, 1);
369 info->maxpath = maxpath;
370 info->findShortestPath = 0;
371 info->thresholdReached = *excess;
372 info->maxpathTable = st__init_table( st__ptrcmp, st__ptrhash);
373 info->threshold = threshold;
374
375 #ifdef DD_DEBUG
376 (void) fprintf(dd->out, "Path length array\n");
377 for (i = 0; i < (numVars+1); i++) {
378 if (pathLengthArray[i])
379 (void) fprintf(dd->out, "%d ",i);
380 }
381 (void) fprintf(dd->out, "\n");
382 for (i = 0; i < (numVars+1); i++) {
383 if (pathLengthArray[i])
384 (void) fprintf(dd->out, "%d ",pathLengthArray[i]);
385 }
386 (void) fprintf(dd->out, "\n");
387 (void) fprintf(dd->out, "Maxpath = %d, Thresholdreached = %d\n",
388 maxpath, info->thresholdReached);
389 #endif
390
391 N = Cudd_Regular(f);
392 if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
393 fprintf(dd->err, "Something wrong, root node must be in table\n");
394 dd->errorCode = CUDD_INTERNAL_ERROR;
395 ABC_FREE(excess);
396 ABC_FREE(info);
397 return(NULL);
398 } else {
399 if ((nodeStat->oddTopDist != MAXSHORTINT) &&
400 (nodeStat->oddBotDist != MAXSHORTINT))
401 oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
402 else
403 oddLen = MAXSHORTINT;
404
405 if ((nodeStat->evenTopDist != MAXSHORTINT) &&
406 (nodeStat->evenBotDist != MAXSHORTINT))
407 evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
408 else
409 evenLen = MAXSHORTINT;
410
411 pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
412 if (pathLength > maxpath) {
413 (void) fprintf(dd->err, "All computations are bogus, since root has path length greater than max path length within threshold %u, %u\n", maxpath, pathLength);
414 dd->errorCode = CUDD_INTERNAL_ERROR;
415 return(NULL);
416 }
417 }
418
419 #ifdef DD_DEBUG
420 numCalls = 0;
421 hits = 0;
422 thishit = 0;
423 #endif
424 /* initialize a table to store computed nodes */
425 if (hardlimit) {
426 subsetNodeTable = st__init_table( st__ptrcmp, st__ptrhash);
427 } else {
428 subsetNodeTable = NIL( st__table);
429 }
430 subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable);
431 if (subset != NULL) {
432 cuddRef(subset);
433 }
434 /* record the number of times a computed result for a node is hit */
435
436 #ifdef DD_DEBUG
437 (void) fprintf(dd->out, "Hits = %d, New==Node = %d, NumCalls = %d\n",
438 hits, thishit, numCalls);
439 #endif
440
441 if (subsetNodeTable != NIL( st__table)) {
442 st__free_table(subsetNodeTable);
443 }
444 st__free_table(info->maxpathTable);
445 st__foreach(pathTable, stPathTableDdFree, (char *)dd);
446
447 ABC_FREE(info);
448
449 } else {/* if threshold larger than size of dd */
450 subset = f;
451 cuddRef(subset);
452 }
453 ABC_FREE(excess);
454 st__free_table(pathTable);
455 ABC_FREE(pathLengthArray);
456 for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
457 ABC_FREE(nodeDistPages);
458
459 #ifdef DD_DEBUG
460 /* check containment of subset in f */
461 if (subset != NULL) {
462 DdNode *check;
463 check = Cudd_bddIteConstant(dd, subset, f, one);
464 if (check != one) {
465 (void) fprintf(dd->err, "Wrong partition\n");
466 dd->errorCode = CUDD_INTERNAL_ERROR;
467 return(NULL);
468 }
469 }
470 #endif
471
472 if (subset != NULL) {
473 cuddDeref(subset);
474 return(subset);
475 } else {
476 return(NULL);
477 }
478
479 } /* end of cuddSubsetShortPaths */
480
481
482 /*---------------------------------------------------------------------------*/
483 /* Definition of static functions */
484 /*---------------------------------------------------------------------------*/
485
486
487 /**Function********************************************************************
488
489 Synopsis [Resize the number of pages allocated to store the distances
490 related to each node.]
491
492 Description [Resize the number of pages allocated to store the distances
493 related to each node. The procedure moves the counter to the
494 next page when the end of the page is reached and allocates new
495 pages when necessary. ]
496
497 SideEffects [Changes the size of pages, page, page index, maximum
498 number of pages freeing stuff in case of memory out. ]
499
500 SeeAlso []
501
502 ******************************************************************************/
503 static void
ResizeNodeDistPages(void)504 ResizeNodeDistPages(void)
505 {
506 int i;
507 NodeDist_t **newNodeDistPages;
508
509 /* move to next page */
510 nodeDistPage++;
511
512 /* If the current page index is larger than the number of pages
513 * allocated, allocate a new page array. Page numbers are incremented by
514 * INITIAL_PAGES
515 */
516 if (nodeDistPage == maxNodeDistPages) {
517 newNodeDistPages = ABC_ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
518 if (newNodeDistPages == NULL) {
519 for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
520 ABC_FREE(nodeDistPages);
521 memOut = 1;
522 return;
523 } else {
524 for (i = 0; i < maxNodeDistPages; i++) {
525 newNodeDistPages[i] = nodeDistPages[i];
526 }
527 /* Increase total page count */
528 maxNodeDistPages += INITIAL_PAGES;
529 ABC_FREE(nodeDistPages);
530 nodeDistPages = newNodeDistPages;
531 }
532 }
533 /* Allocate a new page */
534 currentNodeDistPage = nodeDistPages[nodeDistPage] = ABC_ALLOC(NodeDist_t,
535 nodeDistPageSize);
536 if (currentNodeDistPage == NULL) {
537 for (i = 0; i < nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
538 ABC_FREE(nodeDistPages);
539 memOut = 1;
540 return;
541 }
542 /* reset page index */
543 nodeDistPageIndex = 0;
544 return;
545
546 } /* end of ResizeNodeDistPages */
547
548
549 /**Function********************************************************************
550
551 Synopsis [Resize the number of pages allocated to store nodes in the BFS
552 traversal of the Bdd .]
553
554 Description [Resize the number of pages allocated to store nodes in the BFS
555 traversal of the Bdd. The procedure moves the counter to the
556 next page when the end of the page is reached and allocates new
557 pages when necessary.]
558
559 SideEffects [Changes the size of pages, page, page index, maximum
560 number of pages freeing stuff in case of memory out. ]
561
562 SeeAlso []
563
564 ******************************************************************************/
565 static void
ResizeQueuePages(void)566 ResizeQueuePages(void)
567 {
568 int i;
569 DdNode ***newQueuePages;
570
571 queuePage++;
572 /* If the current page index is larger than the number of pages
573 * allocated, allocate a new page array. Page numbers are incremented by
574 * INITIAL_PAGES
575 */
576 if (queuePage == maxQueuePages) {
577 newQueuePages = ABC_ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
578 if (newQueuePages == NULL) {
579 for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
580 ABC_FREE(queuePages);
581 memOut = 1;
582 return;
583 } else {
584 for (i = 0; i < maxQueuePages; i++) {
585 newQueuePages[i] = queuePages[i];
586 }
587 /* Increase total page count */
588 maxQueuePages += INITIAL_PAGES;
589 ABC_FREE(queuePages);
590 queuePages = newQueuePages;
591 }
592 }
593 /* Allocate a new page */
594 currentQueuePage = queuePages[queuePage] = ABC_ALLOC(DdNode *,queuePageSize);
595 if (currentQueuePage == NULL) {
596 for (i = 0; i < queuePage; i++) ABC_FREE(queuePages[i]);
597 ABC_FREE(queuePages);
598 memOut = 1;
599 return;
600 }
601 /* reset page index */
602 queuePageIndex = 0;
603 return;
604
605 } /* end of ResizeQueuePages */
606
607
608 /**Function********************************************************************
609
610 Synopsis [ Labels each node with its shortest distance from the root]
611
612 Description [ Labels each node with its shortest distance from the root.
613 This is done in a BFS search of the BDD. The nodes are processed
614 in a queue implemented as pages(array) to reduce memory fragmentation.
615 An entry is created for each node visited. The distance from the root
616 to the node with the corresponding parity is updated. The procedure
617 is called recursively each recusion level handling nodes at a given
618 level from the root.]
619
620
621 SideEffects [Creates entries in the pathTable]
622
623 SeeAlso [CreatePathTable CreateBotDist]
624
625 ******************************************************************************/
626 static void
CreateTopDist(st__table * pathTable,int parentPage,int parentQueueIndex,int topLen,DdNode ** childPage,int childQueueIndex,int numParents,FILE * fp)627 CreateTopDist(
628 st__table * pathTable /* hast table to store path lengths */,
629 int parentPage /* the pointer to the page on which the first parent in the queue is to be found. */,
630 int parentQueueIndex /* pointer to the first parent on the page */,
631 int topLen /* current distance from the root */,
632 DdNode ** childPage /* pointer to the page on which the first child is to be added. */,
633 int childQueueIndex /* pointer to the first child */,
634 int numParents /* number of parents to process in this recursive call */,
635 FILE *fp /* where to write messages */)
636 {
637 NodeDist_t *nodeStat;
638 DdNode *N, *Nv, *Nnv, *node, *child, *regChild;
639 int i;
640 int processingDone, childrenCount;
641
642 #ifdef DD_DEBUG
643 numCalls++;
644
645 /* assume this procedure comes in with only the root node*/
646 /* set queue index to the next available entry for addition */
647 /* set queue page to page of addition */
648 if ((queuePages[parentPage] == childPage) && (parentQueueIndex ==
649 childQueueIndex)) {
650 fprintf(fp, "Should not happen that they are equal\n");
651 }
652 assert(queuePageIndex == childQueueIndex);
653 assert(currentQueuePage == childPage);
654 #endif
655 /* number children added to queue is initialized , needed for
656 * numParents in the next call
657 */
658 childrenCount = 0;
659 /* process all the nodes in this level */
660 while (numParents) {
661 numParents--;
662 if (parentQueueIndex == queuePageSize) {
663 parentPage++;
664 parentQueueIndex = 0;
665 }
666 /* a parent to process */
667 node = *(queuePages[parentPage] + parentQueueIndex);
668 parentQueueIndex++;
669 /* get its children */
670 N = Cudd_Regular(node);
671 Nv = Cudd_T(N);
672 Nnv = Cudd_E(N);
673
674 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
675 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
676
677 processingDone = 2;
678 while (processingDone) {
679 /* processing the THEN and the ELSE children, the THEN
680 * child first
681 */
682 if (processingDone == 2) {
683 child = Nv;
684 } else {
685 child = Nnv;
686 }
687
688 regChild = Cudd_Regular(child);
689 /* dont process if the child is a constant */
690 if (!Cudd_IsConstant(child)) {
691 /* check is already visited, if not add a new entry in
692 * the path Table
693 */
694 if (! st__lookup(pathTable, (const char *)regChild, (char **)&nodeStat)) {
695 /* if not in table, has never been visited */
696 /* create entry for table */
697 if (nodeDistPageIndex == nodeDistPageSize)
698 ResizeNodeDistPages();
699 if (memOut) {
700 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
701 ABC_FREE(queuePages);
702 st__free_table(pathTable);
703 return;
704 }
705 /* New entry for child in path Table is created here */
706 nodeStat = currentNodeDistPage + nodeDistPageIndex;
707 nodeDistPageIndex++;
708
709 /* Initialize fields of the node data */
710 nodeStat->oddTopDist = MAXSHORTINT;
711 nodeStat->evenTopDist = MAXSHORTINT;
712 nodeStat->evenBotDist = MAXSHORTINT;
713 nodeStat->oddBotDist = MAXSHORTINT;
714 nodeStat->regResult = NULL;
715 nodeStat->compResult = NULL;
716 /* update the table entry element, the distance keeps
717 * track of the parity of the path from the root
718 */
719 if (Cudd_IsComplement(child)) {
720 nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
721 } else {
722 nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
723 }
724
725 /* insert entry element for child in the table */
726 if ( st__insert(pathTable, (char *)regChild,
727 (char *)nodeStat) == st__OUT_OF_MEM) {
728 memOut = 1;
729 for (i = 0; i <= nodeDistPage; i++)
730 ABC_FREE(nodeDistPages[i]);
731 ABC_FREE(nodeDistPages);
732 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
733 ABC_FREE(queuePages);
734 st__free_table(pathTable);
735 return;
736 }
737
738 /* Create list element for this child to process its children.
739 * If this node has been processed already, then it appears
740 * in the path table and hence is never added to the list
741 * again.
742 */
743
744 if (queuePageIndex == queuePageSize) ResizeQueuePages();
745 if (memOut) {
746 for (i = 0; i <= nodeDistPage; i++)
747 ABC_FREE(nodeDistPages[i]);
748 ABC_FREE(nodeDistPages);
749 st__free_table(pathTable);
750 return;
751 }
752 *(currentQueuePage + queuePageIndex) = child;
753 queuePageIndex++;
754
755 childrenCount++;
756 } else {
757 /* if not been met in a path with this parity before */
758 /* put in list */
759 if (((Cudd_IsComplement(child)) && (nodeStat->oddTopDist ==
760 MAXSHORTINT)) || ((!Cudd_IsComplement(child)) &&
761 (nodeStat->evenTopDist == MAXSHORTINT))) {
762
763 if (queuePageIndex == queuePageSize) ResizeQueuePages();
764 if (memOut) {
765 for (i = 0; i <= nodeDistPage; i++)
766 ABC_FREE(nodeDistPages[i]);
767 ABC_FREE(nodeDistPages);
768 st__free_table(pathTable);
769 return;
770
771 }
772 *(currentQueuePage + queuePageIndex) = child;
773 queuePageIndex++;
774
775 /* update the distance with the appropriate parity */
776 if (Cudd_IsComplement(child)) {
777 nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
778 } else {
779 nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
780 }
781 childrenCount++;
782 }
783
784 } /* end of else (not found in st__table) */
785 } /*end of if Not constant child */
786 processingDone--;
787 } /*end of while processing Nv, Nnv */
788 } /*end of while numParents */
789
790 #ifdef DD_DEBUG
791 assert(queuePages[parentPage] == childPage);
792 assert(parentQueueIndex == childQueueIndex);
793 #endif
794
795 if (childrenCount != 0) {
796 topLen++;
797 childPage = currentQueuePage;
798 childQueueIndex = queuePageIndex;
799 CreateTopDist(pathTable, parentPage, parentQueueIndex, topLen,
800 childPage, childQueueIndex, childrenCount, fp);
801 }
802
803 return;
804
805 } /* end of CreateTopDist */
806
807
808 /**Function********************************************************************
809
810 Synopsis [ Labels each node with the shortest distance from the constant.]
811
812 Description [Labels each node with the shortest distance from the constant.
813 This is done in a DFS search of the BDD. Each node has an odd
814 and even parity distance from the sink (since there exists paths to both
815 zero and one) which is less than MAXSHORTINT. At each node these distances
816 are updated using the minimum distance of its children from the constant.
817 SInce now both the length from the root and child is known, the minimum path
818 length(length of the shortest path between the root and the constant that
819 this node lies on) of this node can be calculated and used to update the
820 pathLengthArray]
821
822 SideEffects [Updates Path Table and path length array]
823
824 SeeAlso [CreatePathTable CreateTopDist AssessPathLength]
825
826 ******************************************************************************/
827 static int
CreateBotDist(DdNode * node,st__table * pathTable,unsigned int * pathLengthArray,FILE * fp)828 CreateBotDist(
829 DdNode * node /* current node */,
830 st__table * pathTable /* path table with path lengths */,
831 unsigned int * pathLengthArray /* array that stores number of nodes belonging to a particular path length. */,
832 FILE *fp /* where to write messages */)
833 {
834 DdNode *N, *Nv, *Nnv;
835 DdNode *realChild;
836 DdNode *child, *regChild;
837 NodeDist_t *nodeStat, *nodeStatChild;
838 unsigned int oddLen, evenLen, pathLength;
839 DdHalfWord botDist;
840 int processingDone;
841
842 if (Cudd_IsConstant(node))
843 return(1);
844 N = Cudd_Regular(node);
845 /* each node has one table entry */
846 /* update as you go down the min dist of each node from
847 the root in each (odd and even) parity */
848 if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
849 fprintf(fp, "Something wrong, the entry doesn't exist\n");
850 return(0);
851 }
852
853 /* compute length of odd parity distances */
854 if ((nodeStat->oddTopDist != MAXSHORTINT) &&
855 (nodeStat->oddBotDist != MAXSHORTINT))
856 oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
857 else
858 oddLen = MAXSHORTINT;
859
860 /* compute length of even parity distances */
861 if (!((nodeStat->evenTopDist == MAXSHORTINT) ||
862 (nodeStat->evenBotDist == MAXSHORTINT)))
863 evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
864 else
865 evenLen = MAXSHORTINT;
866
867 /* assign pathlength to minimum of the two */
868 pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
869
870 Nv = Cudd_T(N);
871 Nnv = Cudd_E(N);
872
873 /* process each child */
874 processingDone = 0;
875 while (processingDone != 2) {
876 if (!processingDone) {
877 child = Nv;
878 } else {
879 child = Nnv;
880 }
881
882 realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
883 regChild = Cudd_Regular(child);
884 if (Cudd_IsConstant(realChild)) {
885 /* Found a minterm; count parity and shortest distance
886 ** from the constant.
887 */
888 if (Cudd_IsComplement(child))
889 nodeStat->oddBotDist = 1;
890 else
891 nodeStat->evenBotDist = 1;
892 } else {
893 /* If node not in table, recur. */
894 if (! st__lookup(pathTable, (const char *)regChild, (char **)&nodeStatChild)) {
895 fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
896 return(0);
897 }
898
899 if (nodeStatChild->oddBotDist == MAXSHORTINT) {
900 if (nodeStatChild->evenBotDist == MAXSHORTINT) {
901 if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
902 return(0);
903 } else {
904 fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
905 return(0);
906 }
907 }
908
909 /* Update shortest distance from the constant depending on
910 ** parity. */
911
912 if (Cudd_IsComplement(child)) {
913 /* If parity on the edge then add 1 to even distance
914 ** of child to get odd parity distance and add 1 to
915 ** odd distance of child to get even parity
916 ** distance. Change distance of current node only if
917 ** the calculated distance is less than existing
918 ** distance. */
919 if (nodeStatChild->oddBotDist != MAXSHORTINT)
920 botDist = nodeStatChild->oddBotDist + 1;
921 else
922 botDist = MAXSHORTINT;
923 if (nodeStat->evenBotDist > botDist )
924 nodeStat->evenBotDist = botDist;
925
926 if (nodeStatChild->evenBotDist != MAXSHORTINT)
927 botDist = nodeStatChild->evenBotDist + 1;
928 else
929 botDist = MAXSHORTINT;
930 if (nodeStat->oddBotDist > botDist)
931 nodeStat->oddBotDist = botDist;
932
933 } else {
934 /* If parity on the edge then add 1 to even distance
935 ** of child to get even parity distance and add 1 to
936 ** odd distance of child to get odd parity distance.
937 ** Change distance of current node only if the
938 ** calculated distance is lesser than existing
939 ** distance. */
940 if (nodeStatChild->evenBotDist != MAXSHORTINT)
941 botDist = nodeStatChild->evenBotDist + 1;
942 else
943 botDist = MAXSHORTINT;
944 if (nodeStat->evenBotDist > botDist)
945 nodeStat->evenBotDist = botDist;
946
947 if (nodeStatChild->oddBotDist != MAXSHORTINT)
948 botDist = nodeStatChild->oddBotDist + 1;
949 else
950 botDist = MAXSHORTINT;
951 if (nodeStat->oddBotDist > botDist)
952 nodeStat->oddBotDist = botDist;
953 }
954 } /* end of else (if not constant child ) */
955 processingDone++;
956 } /* end of while processing Nv, Nnv */
957
958 /* Compute shortest path length on the fly. */
959 if ((nodeStat->oddTopDist != MAXSHORTINT) &&
960 (nodeStat->oddBotDist != MAXSHORTINT))
961 oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
962 else
963 oddLen = MAXSHORTINT;
964
965 if ((nodeStat->evenTopDist != MAXSHORTINT) &&
966 (nodeStat->evenBotDist != MAXSHORTINT))
967 evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
968 else
969 evenLen = MAXSHORTINT;
970
971 /* Update path length array that has number of nodes of a particular
972 ** path length. */
973 if (oddLen < pathLength ) {
974 if (pathLength != MAXSHORTINT)
975 pathLengthArray[pathLength]--;
976 if (oddLen != MAXSHORTINT)
977 pathLengthArray[oddLen]++;
978 pathLength = oddLen;
979 }
980 if (evenLen < pathLength ) {
981 if (pathLength != MAXSHORTINT)
982 pathLengthArray[pathLength]--;
983 if (evenLen != MAXSHORTINT)
984 pathLengthArray[evenLen]++;
985 }
986
987 return(1);
988
989 } /*end of CreateBotDist */
990
991
992 /**Function********************************************************************
993
994 Synopsis [ The outer procedure to label each node with its shortest
995 distance from the root and constant]
996
997 Description [ The outer procedure to label each node with its shortest
998 distance from the root and constant. Calls CreateTopDist and CreateBotDist.
999 The basis for computing the distance between root and constant is that
1000 the distance may be the sum of even distances from the node to the root
1001 and constant or the sum of odd distances from the node to the root and
1002 constant. Both CreateTopDist and CreateBotDist create the odd and
1003 even parity distances from the root and constant respectively.]
1004
1005 SideEffects [None]
1006
1007 SeeAlso [CreateTopDist CreateBotDist]
1008
1009 ******************************************************************************/
1010 static st__table *
CreatePathTable(DdNode * node,unsigned int * pathLengthArray,FILE * fp)1011 CreatePathTable(
1012 DdNode * node /* root of function */,
1013 unsigned int * pathLengthArray /* array of path lengths to store nodes labeled with the various path lengths */,
1014 FILE *fp /* where to write messages */)
1015 {
1016
1017 st__table *pathTable;
1018 NodeDist_t *nodeStat;
1019 DdHalfWord topLen;
1020 DdNode *N;
1021 int i, numParents;
1022 int insertValue;
1023 DdNode **childPage;
1024 int parentPage;
1025 int childQueueIndex, parentQueueIndex;
1026
1027 /* Creating path Table for storing data about nodes */
1028 pathTable = st__init_table( st__ptrcmp, st__ptrhash);
1029
1030 /* initializing pages for info about each node */
1031 maxNodeDistPages = INITIAL_PAGES;
1032 nodeDistPages = ABC_ALLOC(NodeDist_t *, maxNodeDistPages);
1033 if (nodeDistPages == NULL) {
1034 goto OUT_OF_MEM;
1035 }
1036 nodeDistPage = 0;
1037 currentNodeDistPage = nodeDistPages[nodeDistPage] =
1038 ABC_ALLOC(NodeDist_t, nodeDistPageSize);
1039 if (currentNodeDistPage == NULL) {
1040 for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
1041 ABC_FREE(nodeDistPages);
1042 goto OUT_OF_MEM;
1043 }
1044 nodeDistPageIndex = 0;
1045
1046 /* Initializing pages for the BFS search queue, implemented as an array. */
1047 maxQueuePages = INITIAL_PAGES;
1048 queuePages = ABC_ALLOC(DdNode **, maxQueuePages);
1049 if (queuePages == NULL) {
1050 goto OUT_OF_MEM;
1051 }
1052 queuePage = 0;
1053 currentQueuePage = queuePages[queuePage] = ABC_ALLOC(DdNode *, queuePageSize);
1054 if (currentQueuePage == NULL) {
1055 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
1056 ABC_FREE(queuePages);
1057 goto OUT_OF_MEM;
1058 }
1059 queuePageIndex = 0;
1060
1061 /* Enter the root node into the queue to start with. */
1062 parentPage = queuePage;
1063 parentQueueIndex = queuePageIndex;
1064 topLen = 0;
1065 *(currentQueuePage + queuePageIndex) = node;
1066 queuePageIndex++;
1067 childPage = currentQueuePage;
1068 childQueueIndex = queuePageIndex;
1069
1070 N = Cudd_Regular(node);
1071
1072 if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages();
1073 if (memOut) {
1074 for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
1075 ABC_FREE(nodeDistPages);
1076 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
1077 ABC_FREE(queuePages);
1078 st__free_table(pathTable);
1079 goto OUT_OF_MEM;
1080 }
1081
1082 nodeStat = currentNodeDistPage + nodeDistPageIndex;
1083 nodeDistPageIndex++;
1084
1085 nodeStat->oddTopDist = MAXSHORTINT;
1086 nodeStat->evenTopDist = MAXSHORTINT;
1087 nodeStat->evenBotDist = MAXSHORTINT;
1088 nodeStat->oddBotDist = MAXSHORTINT;
1089 nodeStat->regResult = NULL;
1090 nodeStat->compResult = NULL;
1091
1092 insertValue = st__insert(pathTable, (char *)N, (char *)nodeStat);
1093 if (insertValue == st__OUT_OF_MEM) {
1094 memOut = 1;
1095 for (i = 0; i <= nodeDistPage; i++) ABC_FREE(nodeDistPages[i]);
1096 ABC_FREE(nodeDistPages);
1097 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
1098 ABC_FREE(queuePages);
1099 st__free_table(pathTable);
1100 goto OUT_OF_MEM;
1101 } else if (insertValue == 1) {
1102 fprintf(fp, "Something wrong, the entry exists but didnt show up in st__lookup\n");
1103 return(NULL);
1104 }
1105
1106 if (Cudd_IsComplement(node)) {
1107 nodeStat->oddTopDist = 0;
1108 } else {
1109 nodeStat->evenTopDist = 0;
1110 }
1111 numParents = 1;
1112 /* call the function that counts the distance of each node from the
1113 * root
1114 */
1115 #ifdef DD_DEBUG
1116 numCalls = 0;
1117 #endif
1118 CreateTopDist(pathTable, parentPage, parentQueueIndex, (int) topLen,
1119 childPage, childQueueIndex, numParents, fp);
1120 if (memOut) {
1121 fprintf(fp, "Out of Memory and cant count path lengths\n");
1122 goto OUT_OF_MEM;
1123 }
1124
1125 #ifdef DD_DEBUG
1126 numCalls = 0;
1127 #endif
1128 /* call the function that counts the distance of each node from the
1129 * constant
1130 */
1131 if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL);
1132
1133 /* free BFS queue pages as no longer required */
1134 for (i = 0; i <= queuePage; i++) ABC_FREE(queuePages[i]);
1135 ABC_FREE(queuePages);
1136 return(pathTable);
1137
1138 OUT_OF_MEM:
1139 (void) fprintf(fp, "Out of Memory, cannot allocate pages\n");
1140 memOut = 1;
1141 return(NULL);
1142
1143 } /*end of CreatePathTable */
1144
1145
1146 /**Function********************************************************************
1147
1148 Synopsis [Chooses the maximum allowable path length of nodes under the
1149 threshold.]
1150
1151 Description [Chooses the maximum allowable path length under each node.
1152 The corner cases are when the threshold is larger than the number
1153 of nodes in the BDD iself, in which case 'numVars + 1' is returned.
1154 If all nodes of a particular path length are needed, then the
1155 maxpath returned is the next one with excess nodes = 0;]
1156
1157 SideEffects [None]
1158
1159 SeeAlso []
1160
1161 ******************************************************************************/
1162 static unsigned int
AssessPathLength(unsigned int * pathLengthArray,int threshold,int numVars,unsigned int * excess,FILE * fp)1163 AssessPathLength(
1164 unsigned int * pathLengthArray /* array determining number of nodes belonging to the different path lengths */,
1165 int threshold /* threshold to determine maximum allowable nodes in the subset */,
1166 int numVars /* maximum number of variables */,
1167 unsigned int * excess /* number of nodes labeled maxpath required in the subset */,
1168 FILE *fp /* where to write messages */)
1169 {
1170 unsigned int i, maxpath;
1171 int temp;
1172
1173 temp = threshold;
1174 i = 0;
1175 maxpath = 0;
1176 /* quit loop if i reaches max number of variables or if temp reaches
1177 * below zero
1178 */
1179 while ((i < (unsigned) numVars+1) && (temp > 0)) {
1180 if (pathLengthArray[i] > 0) {
1181 maxpath = i;
1182 temp = temp - pathLengthArray[i];
1183 }
1184 i++;
1185 }
1186 /* if all nodes of max path are needed */
1187 if (temp >= 0) {
1188 maxpath++; /* now maxpath becomes the next maxppath or max number
1189 of variables */
1190 *excess = 0;
1191 } else { /* normal case when subset required is less than size of
1192 original BDD */
1193 *excess = temp + pathLengthArray[maxpath];
1194 }
1195
1196 if (maxpath == 0) {
1197 fprintf(fp, "Path Length array seems to be all zeroes, check\n");
1198 }
1199 return(maxpath);
1200
1201 } /* end of AssessPathLength */
1202
1203
1204 /**Function********************************************************************
1205
1206 Synopsis [Builds the BDD with nodes labeled with path length less than or equal to maxpath]
1207
1208 Description [Builds the BDD with nodes labeled with path length
1209 under maxpath and as many nodes labeled maxpath as determined by the
1210 threshold. The procedure uses the path table to determine which nodes
1211 in the original bdd need to be retained. This procedure picks a
1212 shortest path (tie break decided by taking the child with the shortest
1213 distance to the constant) and recurs down the path till it reaches the
1214 constant. the procedure then starts building the subset upward from
1215 the constant. All nodes labeled by path lengths less than the given
1216 maxpath are used to build the subset. However, in the case of nodes
1217 that have label equal to maxpath, as many are chosen as required by
1218 the threshold. This number is stored in the info structure in the
1219 field thresholdReached. This field is decremented whenever a node
1220 labeled maxpath is encountered and the nodes labeled maxpath are
1221 aggregated in a maxpath table. As soon as the thresholdReached count
1222 goes to 0, the shortest path from this node to the constant is found.
1223 The extraction of nodes with the above labeling is based on the fact
1224 that each node, labeled with a path length, P, has at least one child
1225 labeled P or less. So extracting all nodes labeled a given path length
1226 P ensures complete paths between the root and the constant. Extraction
1227 of a partial number of nodes with a given path length may result in
1228 incomplete paths and hence the additional number of nodes are grabbed
1229 to complete the path. Since the Bdd is built bottom-up, other nodes
1230 labeled maxpath do lie on complete paths. The procedure may cause the
1231 subset to have a larger or smaller number of nodes than the specified
1232 threshold. The increase in the number of nodes is caused by the
1233 building of a subset and the reduction by recombination. However in
1234 most cases, the recombination overshadows the increase and the
1235 procedure returns a result with lower number of nodes than specified.
1236 The subsetNodeTable is NIL when there is no hard limit on the number
1237 of nodes. Further efforts towards keeping the subset closer to the
1238 threshold number were abandoned in favour of keeping the procedure
1239 simple and fast.]
1240
1241 SideEffects [SubsetNodeTable is changed if it is not NIL.]
1242
1243 SeeAlso []
1244
1245 ******************************************************************************/
1246 static DdNode *
BuildSubsetBdd(DdManager * dd,st__table * pathTable,DdNode * node,struct AssortedInfo * info,st__table * subsetNodeTable)1247 BuildSubsetBdd(
1248 DdManager * dd /* DD manager */,
1249 st__table * pathTable /* path table with path lengths and computed results */,
1250 DdNode * node /* current node */,
1251 struct AssortedInfo * info /* assorted information structure */,
1252 st__table * subsetNodeTable /* table storing computed results */)
1253 {
1254 DdNode *N, *Nv, *Nnv;
1255 DdNode *ThenBranch, *ElseBranch, *childBranch;
1256 DdNode *child, *regChild, *regNnv = NULL, *regNv = NULL;
1257 NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv;
1258 DdNode *neW, *topv, *regNew;
1259 char *entry;
1260 unsigned int topid;
1261 unsigned int childPathLength, oddLen, evenLen, NnvPathLength = 0, NvPathLength = 0;
1262 unsigned int NvBotDist, NnvBotDist;
1263 int tiebreakChild;
1264 int processingDone, thenDone, elseDone;
1265
1266
1267 #ifdef DD_DEBUG
1268 numCalls++;
1269 #endif
1270 if (Cudd_IsConstant(node))
1271 return(node);
1272
1273 N = Cudd_Regular(node);
1274 /* Find node in table. */
1275 if (! st__lookup(pathTable, (const char *)N, (char **)&nodeStat)) {
1276 (void) fprintf(dd->err, "Something wrong, node must be in table \n");
1277 dd->errorCode = CUDD_INTERNAL_ERROR;
1278 return(NULL);
1279 }
1280 /* If the node in the table has been visited, then return the corresponding
1281 ** Dd. Since a node can become a subset of itself, its
1282 ** complement (that is te same node reached by a different parity) will
1283 ** become a superset of the original node and result in some minterms
1284 ** that were not in the original set. Hence two different results are
1285 ** maintained, corresponding to the odd and even parities.
1286 */
1287
1288 /* If this node is reached with an odd parity, get odd parity results. */
1289 if (Cudd_IsComplement(node)) {
1290 if (nodeStat->compResult != NULL) {
1291 #ifdef DD_DEBUG
1292 hits++;
1293 #endif
1294 return(nodeStat->compResult);
1295 }
1296 } else {
1297 /* if this node is reached with an even parity, get even parity
1298 * results
1299 */
1300 if (nodeStat->regResult != NULL) {
1301 #ifdef DD_DEBUG
1302 hits++;
1303 #endif
1304 return(nodeStat->regResult);
1305 }
1306 }
1307
1308
1309 /* get children */
1310 Nv = Cudd_T(N);
1311 Nnv = Cudd_E(N);
1312
1313 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1314 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1315
1316 /* no child processed */
1317 processingDone = 0;
1318 /* then child not processed */
1319 thenDone = 0;
1320 ThenBranch = NULL;
1321 /* else child not processed */
1322 elseDone = 0;
1323 ElseBranch = NULL;
1324 /* if then child constant, branch is the child */
1325 if (Cudd_IsConstant(Nv)) {
1326 /*shortest path found */
1327 if ((Nv == DD_ONE(dd)) && (info->findShortestPath)) {
1328 info->findShortestPath = 0;
1329 }
1330
1331 ThenBranch = Nv;
1332 cuddRef(ThenBranch);
1333 if (ThenBranch == NULL) {
1334 return(NULL);
1335 }
1336
1337 thenDone++;
1338 processingDone++;
1339 NvBotDist = MAXSHORTINT;
1340 } else {
1341 /* Derive regular child for table lookup. */
1342 regNv = Cudd_Regular(Nv);
1343 /* Get node data for shortest path length. */
1344 if (! st__lookup(pathTable, (const char *)regNv, (char **)&nodeStatNv) ) {
1345 (void) fprintf(dd->err, "Something wrong, node must be in table\n");
1346 dd->errorCode = CUDD_INTERNAL_ERROR;
1347 return(NULL);
1348 }
1349 /* Derive shortest path length for child. */
1350 if ((nodeStatNv->oddTopDist != MAXSHORTINT) &&
1351 (nodeStatNv->oddBotDist != MAXSHORTINT)) {
1352 oddLen = (nodeStatNv->oddTopDist + nodeStatNv->oddBotDist);
1353 } else {
1354 oddLen = MAXSHORTINT;
1355 }
1356
1357 if ((nodeStatNv->evenTopDist != MAXSHORTINT) &&
1358 (nodeStatNv->evenBotDist != MAXSHORTINT)) {
1359 evenLen = (nodeStatNv->evenTopDist +nodeStatNv->evenBotDist);
1360 } else {
1361 evenLen = MAXSHORTINT;
1362 }
1363
1364 NvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
1365 NvBotDist = (oddLen <= evenLen) ? nodeStatNv->oddBotDist:
1366 nodeStatNv->evenBotDist;
1367 }
1368 /* if else child constant, branch is the child */
1369 if (Cudd_IsConstant(Nnv)) {
1370 /*shortest path found */
1371 if ((Nnv == DD_ONE(dd)) && (info->findShortestPath)) {
1372 info->findShortestPath = 0;
1373 }
1374
1375 ElseBranch = Nnv;
1376 cuddRef(ElseBranch);
1377 if (ElseBranch == NULL) {
1378 return(NULL);
1379 }
1380
1381 elseDone++;
1382 processingDone++;
1383 NnvBotDist = MAXSHORTINT;
1384 } else {
1385 /* Derive regular child for table lookup. */
1386 regNnv = Cudd_Regular(Nnv);
1387 /* Get node data for shortest path length. */
1388 if (! st__lookup(pathTable, (const char *)regNnv, (char **)&nodeStatNnv) ) {
1389 (void) fprintf(dd->err, "Something wrong, node must be in table\n");
1390 dd->errorCode = CUDD_INTERNAL_ERROR;
1391 return(NULL);
1392 }
1393 /* Derive shortest path length for child. */
1394 if ((nodeStatNnv->oddTopDist != MAXSHORTINT) &&
1395 (nodeStatNnv->oddBotDist != MAXSHORTINT)) {
1396 oddLen = (nodeStatNnv->oddTopDist + nodeStatNnv->oddBotDist);
1397 } else {
1398 oddLen = MAXSHORTINT;
1399 }
1400
1401 if ((nodeStatNnv->evenTopDist != MAXSHORTINT) &&
1402 (nodeStatNnv->evenBotDist != MAXSHORTINT)) {
1403 evenLen = (nodeStatNnv->evenTopDist +nodeStatNnv->evenBotDist);
1404 } else {
1405 evenLen = MAXSHORTINT;
1406 }
1407
1408 NnvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
1409 NnvBotDist = (oddLen <= evenLen) ? nodeStatNnv->oddBotDist :
1410 nodeStatNnv->evenBotDist;
1411 }
1412
1413 tiebreakChild = (NvBotDist <= NnvBotDist) ? 1 : 0;
1414 /* while both children not processed */
1415 while (processingDone != 2) {
1416 if (!processingDone) {
1417 /* if no child processed */
1418 /* pick the child with shortest path length and record which one
1419 * picked
1420 */
1421 if ((NvPathLength < NnvPathLength) ||
1422 ((NvPathLength == NnvPathLength) && (tiebreakChild == 1))) {
1423 child = Nv;
1424 regChild = regNv;
1425 thenDone = 1;
1426 childPathLength = NvPathLength;
1427 } else {
1428 child = Nnv;
1429 regChild = regNnv;
1430 elseDone = 1;
1431 childPathLength = NnvPathLength;
1432 } /* then path length less than else path length */
1433 } else {
1434 /* if one child processed, process the other */
1435 if (thenDone) {
1436 child = Nnv;
1437 regChild = regNnv;
1438 elseDone = 1;
1439 childPathLength = NnvPathLength;
1440 } else {
1441 child = Nv;
1442 regChild = regNv;
1443 thenDone = 1;
1444 childPathLength = NvPathLength;
1445 } /* end of else pick the Then child if ELSE child processed */
1446 } /* end of else one child has been processed */
1447
1448 /* ignore (replace with constant 0) all nodes which lie on paths larger
1449 * than the maximum length of the path required
1450 */
1451 if (childPathLength > info->maxpath) {
1452 /* record nodes visited */
1453 childBranch = zero;
1454 } else {
1455 if (childPathLength < info->maxpath) {
1456 if (info->findShortestPath) {
1457 info->findShortestPath = 0;
1458 }
1459 childBranch = BuildSubsetBdd(dd, pathTable, child, info,
1460 subsetNodeTable);
1461
1462 } else { /* Case: path length of node = maxpath */
1463 /* If the node labeled with maxpath is found in the
1464 ** maxpathTable, use it to build the subset BDD. */
1465 if ( st__lookup(info->maxpathTable, (char *)regChild,
1466 (char **)&entry)) {
1467 /* When a node that is already been chosen is hit,
1468 ** the quest for a complete path is over. */
1469 if (info->findShortestPath) {
1470 info->findShortestPath = 0;
1471 }
1472 childBranch = BuildSubsetBdd(dd, pathTable, child, info,
1473 subsetNodeTable);
1474 } else {
1475 /* If node is not found in the maxpathTable and
1476 ** the threshold has been reached, then if the
1477 ** path needs to be completed, continue. Else
1478 ** replace the node with a zero. */
1479 if (info->thresholdReached <= 0) {
1480 if (info->findShortestPath) {
1481 if ( st__insert(info->maxpathTable, (char *)regChild,
1482 (char *)NIL(char)) == st__OUT_OF_MEM) {
1483 memOut = 1;
1484 (void) fprintf(dd->err, "OUT of memory\n");
1485 info->thresholdReached = 0;
1486 childBranch = zero;
1487 } else {
1488 info->thresholdReached--;
1489 childBranch = BuildSubsetBdd(dd, pathTable,
1490 child, info,subsetNodeTable);
1491 }
1492 } else { /* not find shortest path, we dont need this
1493 node */
1494 childBranch = zero;
1495 }
1496 } else { /* Threshold hasn't been reached,
1497 ** need the node. */
1498 if ( st__insert(info->maxpathTable, (char *)regChild,
1499 (char *)NIL(char)) == st__OUT_OF_MEM) {
1500 memOut = 1;
1501 (void) fprintf(dd->err, "OUT of memory\n");
1502 info->thresholdReached = 0;
1503 childBranch = zero;
1504 } else {
1505 info->thresholdReached--;
1506 if (info->thresholdReached <= 0) {
1507 info->findShortestPath = 1;
1508 }
1509 childBranch = BuildSubsetBdd(dd, pathTable,
1510 child, info, subsetNodeTable);
1511
1512 } /* end of st__insert successful */
1513 } /* end of threshold hasnt been reached yet */
1514 } /* end of else node not found in maxpath table */
1515 } /* end of if (path length of node = maxpath) */
1516 } /* end if !(childPathLength > maxpath) */
1517 if (childBranch == NULL) {
1518 /* deref other stuff incase reordering has taken place */
1519 if (ThenBranch != NULL) {
1520 Cudd_RecursiveDeref(dd, ThenBranch);
1521 ThenBranch = NULL;
1522 }
1523 if (ElseBranch != NULL) {
1524 Cudd_RecursiveDeref(dd, ElseBranch);
1525 ElseBranch = NULL;
1526 }
1527 return(NULL);
1528 }
1529
1530 cuddRef(childBranch);
1531
1532 if (child == Nv) {
1533 ThenBranch = childBranch;
1534 } else {
1535 ElseBranch = childBranch;
1536 }
1537 processingDone++;
1538
1539 } /*end of while processing Nv, Nnv */
1540
1541 info->findShortestPath = 0;
1542 topid = Cudd_NodeReadIndex(N);
1543 topv = Cudd_ReadVars(dd, topid);
1544 cuddRef(topv);
1545 neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
1546 if (neW != NULL) {
1547 cuddRef(neW);
1548 }
1549 Cudd_RecursiveDeref(dd, topv);
1550 Cudd_RecursiveDeref(dd, ThenBranch);
1551 Cudd_RecursiveDeref(dd, ElseBranch);
1552
1553
1554 /* Hard Limit of threshold has been imposed */
1555 if (subsetNodeTable != NIL( st__table)) {
1556 /* check if a new node is created */
1557 regNew = Cudd_Regular(neW);
1558 /* subset node table keeps all new nodes that have been created to keep
1559 * a running count of how many nodes have been built in the subset.
1560 */
1561 if (! st__lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
1562 if (!Cudd_IsConstant(regNew)) {
1563 if ( st__insert(subsetNodeTable, (char *)regNew,
1564 (char *)NULL) == st__OUT_OF_MEM) {
1565 (void) fprintf(dd->err, "Out of memory\n");
1566 return (NULL);
1567 }
1568 if ( st__count(subsetNodeTable) > info->threshold) {
1569 info->thresholdReached = 0;
1570 }
1571 }
1572 }
1573 }
1574
1575
1576 if (neW == NULL) {
1577 return(NULL);
1578 } else {
1579 /*store computed result in regular form*/
1580 if (Cudd_IsComplement(node)) {
1581 nodeStat->compResult = neW;
1582 cuddRef(nodeStat->compResult);
1583 /* if the new node is the same as the corresponding node in the
1584 * original bdd then its complement need not be computed as it
1585 * cannot be larger than the node itself
1586 */
1587 if (neW == node) {
1588 #ifdef DD_DEBUG
1589 thishit++;
1590 #endif
1591 /* if a result for the node has already been computed, then
1592 * it can only be smaller than teh node itself. hence store
1593 * the node result in order not to break recombination
1594 */
1595 if (nodeStat->regResult != NULL) {
1596 Cudd_RecursiveDeref(dd, nodeStat->regResult);
1597 }
1598 nodeStat->regResult = Cudd_Not(neW);
1599 cuddRef(nodeStat->regResult);
1600 }
1601
1602 } else {
1603 nodeStat->regResult = neW;
1604 cuddRef(nodeStat->regResult);
1605 if (neW == node) {
1606 #ifdef DD_DEBUG
1607 thishit++;
1608 #endif
1609 if (nodeStat->compResult != NULL) {
1610 Cudd_RecursiveDeref(dd, nodeStat->compResult);
1611 }
1612 nodeStat->compResult = Cudd_Not(neW);
1613 cuddRef(nodeStat->compResult);
1614 }
1615 }
1616
1617 cuddDeref(neW);
1618 return(neW);
1619 } /* end of else i.e. Subset != NULL */
1620 } /* end of BuildSubsetBdd */
1621
1622
1623 /**Function********************************************************************
1624
1625 Synopsis [Procedure to free te result dds stored in the NodeDist pages.]
1626
1627 Description [None]
1628
1629 SideEffects [None]
1630
1631 SeeAlso []
1632
1633 ******************************************************************************/
1634 static enum st__retval
stPathTableDdFree(char * key,char * value,char * arg)1635 stPathTableDdFree(
1636 char * key,
1637 char * value,
1638 char * arg)
1639 {
1640 NodeDist_t *nodeStat;
1641 DdManager *dd;
1642
1643 nodeStat = (NodeDist_t *)value;
1644 dd = (DdManager *)arg;
1645 if (nodeStat->regResult != NULL) {
1646 Cudd_RecursiveDeref(dd, nodeStat->regResult);
1647 }
1648 if (nodeStat->compResult != NULL) {
1649 Cudd_RecursiveDeref(dd, nodeStat->compResult);
1650 }
1651 return( st__CONTINUE);
1652
1653 } /* end of stPathTableFree */
1654
1655
1656 ABC_NAMESPACE_IMPL_END
1657
1658