source: vis_dev/glu-2.3/src/cuBdd/cuddSubsetSP.c@ 77

Last change on this file since 77 was 13, checked in by cecile, 15 years ago

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