1 /**CFile***********************************************************************
3 FileName [cuddSubsetSP.c]
7 Synopsis [Procedure to subset the given BDD choosing the shortest paths
8 (largest cubes) in the BDD.]
11 Description [External procedures included in this module:
13 <li> Cudd_SubsetShortPaths()
14 <li> Cudd_SupersetShortPaths()
16 Internal procedures included in this module:
18 <li> cuddSubsetShortPaths()
20 Static procedures included in this module:
23 <li> CreatePathTable()
24 <li> AssessPathLength()
27 <li> ResizeNodeDistPages()
28 <li> ResizeQueuePages()
29 <li> stPathTableDdFree()
33 SeeAlso [cuddSubsetHB.c]
37 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
41 Redistribution and use in source and binary forms, with or without
42 modification, are permitted provided that the following conditions
45 Redistributions of source code must retain the above copyright
46 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
69 ******************************************************************************/
74 /*---------------------------------------------------------------------------*/
75 /* Constant declarations */
76 /*---------------------------------------------------------------------------*/
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
85 #define INITIAL_PAGES 128 /* number of initial pages for the
86 * queue/NodeDist_t type */
88 /*---------------------------------------------------------------------------*/
89 /* Stucture declarations */
90 /*---------------------------------------------------------------------------*/
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
97 DdHalfWord oddTopDist
;
98 DdHalfWord evenTopDist
;
99 DdHalfWord oddBotDist
;
100 DdHalfWord evenBotDist
;
105 /* assorted information needed by the BuildSubsetBdd procedure. */
106 struct AssortedInfo
{
107 unsigned int maxpath
;
108 int findShortestPath
;
109 int thresholdReached
;
110 st_table
*maxpathTable
;
114 /*---------------------------------------------------------------------------*/
115 /* Type declarations */
116 /*---------------------------------------------------------------------------*/
118 typedef struct NodeDist NodeDist_t
;
120 /*---------------------------------------------------------------------------*/
121 /* Variable declarations */
122 /*---------------------------------------------------------------------------*/
125 static char rcsid
[] DD_UNUSED
= "$Id: cuddSubsetSP.c,v 1.34 2009/02/19 16:23:19 fabio Exp $";
135 static int memOut
; /* flag to indicate out of memory */
136 static DdNode
*zero
, *one
; /* constant functions */
138 static NodeDist_t
**nodeDistPages
; /* pointers to the pages */
139 static int nodeDistPageIndex
; /* index to next element */
140 static int nodeDistPage
; /* index to current page */
141 static int nodeDistPageSize
= DEFAULT_NODE_DIST_PAGE_SIZE
; /* page size */
142 static int maxNodeDistPages
; /* number of page pointers */
143 static NodeDist_t
*currentNodeDistPage
; /* current page */
145 static DdNode
***queuePages
; /* pointers to the pages */
146 static int queuePageIndex
; /* index to next element */
147 static int queuePage
; /* index to current page */
148 static int queuePageSize
= DEFAULT_PAGE_SIZE
; /* page size */
149 static int maxQueuePages
; /* number of page pointers */
150 static DdNode
**currentQueuePage
; /* current page */
153 /*---------------------------------------------------------------------------*/
154 /* Macro declarations */
155 /*---------------------------------------------------------------------------*/
161 /**AutomaticStart*************************************************************/
163 /*---------------------------------------------------------------------------*/
164 /* Static function prototypes */
165 /*---------------------------------------------------------------------------*/
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
);
176 /**AutomaticEnd***************************************************************/
182 /*---------------------------------------------------------------------------*/
183 /* Definition of Exported functions */
184 /*---------------------------------------------------------------------------*/
187 /**Function********************************************************************
189 Synopsis [Extracts a dense subset from a BDD with the shortest paths
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.]
212 SeeAlso [Cudd_SupersetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize]
214 ******************************************************************************/
216 Cudd_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 */)
228 subset
= cuddSubsetShortPaths(dd
, f
, numVars
, threshold
, hardlimit
);
229 } while((dd
->reordered
==1) && (!memOut
));
233 } /* end of Cudd_SubsetShortPaths */
236 /**Function********************************************************************
238 Synopsis [Extracts a dense superset from a BDD with the shortest paths
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.]
264 SeeAlso [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]
266 ******************************************************************************/
268 Cudd_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 */)
281 subset
= cuddSubsetShortPaths(dd
, g
, numVars
, threshold
, hardlimit
);
282 } while((dd
->reordered
==1) && (!memOut
));
284 return(Cudd_NotCond(subset
, (subset
!= NULL
)));
286 } /* end of Cudd_SupersetShortPaths */
289 /*---------------------------------------------------------------------------*/
290 /* Definition of internal functions */
291 /*---------------------------------------------------------------------------*/
294 /**Function********************************************************************
296 Synopsis [The outermost procedure to return a subset of the given BDD
297 with the shortest path lengths.]
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
308 SeeAlso [Cudd_SubsetShortPaths]
310 ******************************************************************************/
312 cuddSubsetShortPaths(
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 */)
322 unsigned int *pathLengthArray
;
323 unsigned int maxpath
, oddLen
, evenLen
, pathLength
, *excess
;
325 NodeDist_t
*nodeStat
;
326 struct AssortedInfo
*info
;
327 st_table
*subsetNodeTable
;
330 zero
= Cudd_Not(one
);
333 /* set default value */
334 numVars
= Cudd_ReadSize(dd
);
337 if (threshold
> numVars
) {
338 threshold
= threshold
- numVars
;
341 fprintf(dd
->err
, "Cannot partition, nil object\n");
342 dd
->errorCode
= CUDD_INVALID_ARG
;
345 if (Cudd_IsConstant(f
))
348 pathLengthArray
= ALLOC(unsigned int, numVars
+1);
349 for (i
= 0; i
< numVars
+1; i
++) pathLengthArray
[i
] = 0;
356 pathTable
= CreatePathTable(f
, pathLengthArray
, dd
->err
);
358 if ((pathTable
== NULL
) || (memOut
)) {
359 if (pathTable
!= NULL
)
360 st_free_table(pathTable
);
361 FREE(pathLengthArray
);
362 return (NIL(DdNode
));
365 excess
= ALLOC(unsigned int, 1);
367 maxpath
= AssessPathLength(pathLengthArray
, threshold
, numVars
, excess
,
370 if (maxpath
!= (unsigned) (numVars
+ 1)) {
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
;
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
);
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
]);
390 (void) fprintf(dd
->out
, "\n");
391 (void) fprintf(dd
->out
, "Maxpath = %d, Thresholdreached = %d\n",
392 maxpath
, info
->thresholdReached
);
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
;
403 if ((nodeStat
->oddTopDist
!= MAXSHORTINT
) &&
404 (nodeStat
->oddBotDist
!= MAXSHORTINT
))
405 oddLen
= (nodeStat
->oddTopDist
+ nodeStat
->oddBotDist
);
407 oddLen
= MAXSHORTINT
;
409 if ((nodeStat
->evenTopDist
!= MAXSHORTINT
) &&
410 (nodeStat
->evenBotDist
!= MAXSHORTINT
))
411 evenLen
= (nodeStat
->evenTopDist
+nodeStat
->evenBotDist
);
413 evenLen
= MAXSHORTINT
;
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
;
428 /* initialize a table to store computed nodes */
430 subsetNodeTable
= st_init_table(st_ptrcmp
, st_ptrhash
);
432 subsetNodeTable
= NIL(st_table
);
434 subset
= BuildSubsetBdd(dd
, pathTable
, f
, info
, subsetNodeTable
);
435 if (subset
!= NULL
) {
438 /* record the number of times a computed result for a node is hit */
441 (void) fprintf(dd
->out
, "Hits = %d, New==Node = %d, NumCalls = %d\n",
442 hits
, thishit
, numCalls
);
445 if (subsetNodeTable
!= NIL(st_table
)) {
446 st_free_table(subsetNodeTable
);
448 st_free_table(info
->maxpathTable
);
449 st_foreach(pathTable
, stPathTableDdFree
, (char *)dd
);
453 } else {/* if threshold larger than size of dd */
458 st_free_table(pathTable
);
459 FREE(pathLengthArray
);
460 for (i
= 0; i
<= nodeDistPage
; i
++) FREE(nodeDistPages
[i
]);
464 /* check containment of subset in f */
465 if (subset
!= NULL
) {
467 check
= Cudd_bddIteConstant(dd
, subset
, f
, one
);
469 (void) fprintf(dd
->err
, "Wrong partition\n");
470 dd
->errorCode
= CUDD_INTERNAL_ERROR
;
476 if (subset
!= NULL
) {
483 } /* end of cuddSubsetShortPaths */
486 /*---------------------------------------------------------------------------*/
487 /* Definition of static functions */
488 /*---------------------------------------------------------------------------*/
491 /**Function********************************************************************
493 Synopsis [Resize the number of pages allocated to store the distances
494 related to each node.]
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. ]
501 SideEffects [Changes the size of pages, page, page index, maximum
502 number of pages freeing stuff in case of memory out. ]
506 ******************************************************************************/
508 ResizeNodeDistPages(void)
511 NodeDist_t
**newNodeDistPages
;
513 /* move to next page */
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
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
]);
528 for (i
= 0; i
< maxNodeDistPages
; i
++) {
529 newNodeDistPages
[i
] = nodeDistPages
[i
];
531 /* Increase total page count */
532 maxNodeDistPages
+= INITIAL_PAGES
;
534 nodeDistPages
= newNodeDistPages
;
537 /* Allocate a new page */
538 currentNodeDistPage
= nodeDistPages
[nodeDistPage
] = ALLOC(NodeDist_t
,
540 if (currentNodeDistPage
== NULL
) {
541 for (i
= 0; i
< nodeDistPage
; i
++) FREE(nodeDistPages
[i
]);
546 /* reset page index */
547 nodeDistPageIndex
= 0;
550 } /* end of ResizeNodeDistPages */
553 /**Function********************************************************************
555 Synopsis [Resize the number of pages allocated to store nodes in the BFS
556 traversal of the Bdd .]
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.]
563 SideEffects [Changes the size of pages, page, page index, maximum
564 number of pages freeing stuff in case of memory out. ]
568 ******************************************************************************/
570 ResizeQueuePages(void)
573 DdNode
***newQueuePages
;
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
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
]);
588 for (i
= 0; i
< maxQueuePages
; i
++) {
589 newQueuePages
[i
] = queuePages
[i
];
591 /* Increase total page count */
592 maxQueuePages
+= INITIAL_PAGES
;
594 queuePages
= newQueuePages
;
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
]);
605 /* reset page index */
609 } /* end of ResizeQueuePages */
612 /**Function********************************************************************
614 Synopsis [ Labels each node with its shortest distance from the root]
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.]
625 SideEffects [Creates entries in the pathTable]
627 SeeAlso [CreatePathTable CreateBotDist]
629 ******************************************************************************/
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 */)
641 NodeDist_t
*nodeStat
;
642 DdNode
*N
, *Nv
, *Nnv
, *node
, *child
, *regChild
;
644 int processingDone
, childrenCount
;
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
==
654 fprintf(fp
, "Should not happen that they are equal\n");
656 assert(queuePageIndex
== childQueueIndex
);
657 assert(currentQueuePage
== childPage
);
659 /* number children added to queue is initialized , needed for
660 * numParents in the next call
663 /* process all the nodes in this level */
666 if (parentQueueIndex
== queuePageSize
) {
668 parentQueueIndex
= 0;
670 /* a parent to process */
671 node
= *(queuePages
[parentPage
] + parentQueueIndex
);
673 /* get its children */
674 N
= Cudd_Regular(node
);
678 Nv
= Cudd_NotCond(Nv
, Cudd_IsComplement(node
));
679 Nnv
= Cudd_NotCond(Nnv
, Cudd_IsComplement(node
));
682 while (processingDone
) {
683 /* processing the THEN and the ELSE children, the THEN
686 if (processingDone
== 2) {
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
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();
704 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
706 st_free_table(pathTable
);
709 /* New entry for child in path Table is created here */
710 nodeStat
= currentNodeDistPage
+ nodeDistPageIndex
;
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
723 if (Cudd_IsComplement(child
)) {
724 nodeStat
->oddTopDist
= (DdHalfWord
) topLen
+ 1;
726 nodeStat
->evenTopDist
= (DdHalfWord
) topLen
+ 1;
729 /* insert entry element for child in the table */
730 if (st_insert(pathTable
, (char *)regChild
,
731 (char *)nodeStat
) == ST_OUT_OF_MEM
) {
733 for (i
= 0; i
<= nodeDistPage
; i
++)
734 FREE(nodeDistPages
[i
]);
736 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
738 st_free_table(pathTable
);
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
748 if (queuePageIndex
== queuePageSize
) ResizeQueuePages();
750 for (i
= 0; i
<= nodeDistPage
; i
++)
751 FREE(nodeDistPages
[i
]);
753 st_free_table(pathTable
);
756 *(currentQueuePage
+ queuePageIndex
) = child
;
761 /* if not been met in a path with this parity before */
763 if (((Cudd_IsComplement(child
)) && (nodeStat
->oddTopDist
==
764 MAXSHORTINT
)) || ((!Cudd_IsComplement(child
)) &&
765 (nodeStat
->evenTopDist
== MAXSHORTINT
))) {
767 if (queuePageIndex
== queuePageSize
) ResizeQueuePages();
769 for (i
= 0; i
<= nodeDistPage
; i
++)
770 FREE(nodeDistPages
[i
]);
772 st_free_table(pathTable
);
776 *(currentQueuePage
+ queuePageIndex
) = child
;
779 /* update the distance with the appropriate parity */
780 if (Cudd_IsComplement(child
)) {
781 nodeStat
->oddTopDist
= (DdHalfWord
) topLen
+ 1;
783 nodeStat
->evenTopDist
= (DdHalfWord
) topLen
+ 1;
788 } /* end of else (not found in st_table) */
789 } /*end of if Not constant child */
791 } /*end of while processing Nv, Nnv */
792 } /*end of while numParents */
795 assert(queuePages
[parentPage
] == childPage
);
796 assert(parentQueueIndex
== childQueueIndex
);
799 if (childrenCount
!= 0) {
801 childPage
= currentQueuePage
;
802 childQueueIndex
= queuePageIndex
;
803 CreateTopDist(pathTable
, parentPage
, parentQueueIndex
, topLen
,
804 childPage
, childQueueIndex
, childrenCount
, fp
);
809 } /* end of CreateTopDist */
812 /**Function********************************************************************
814 Synopsis [ Labels each node with the shortest distance from the constant.]
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
826 SideEffects [Updates Path Table and path length array]
828 SeeAlso [CreatePathTable CreateTopDist AssessPathLength]
830 ******************************************************************************/
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 */)
838 DdNode
*N
, *Nv
, *Nnv
;
840 DdNode
*child
, *regChild
;
841 NodeDist_t
*nodeStat
, *nodeStatChild
;
842 unsigned int oddLen
, evenLen
, pathLength
;
846 if (Cudd_IsConstant(node
))
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");
857 /* compute length of odd parity distances */
858 if ((nodeStat
->oddTopDist
!= MAXSHORTINT
) &&
859 (nodeStat
->oddBotDist
!= MAXSHORTINT
))
860 oddLen
= (nodeStat
->oddTopDist
+ nodeStat
->oddBotDist
);
862 oddLen
= MAXSHORTINT
;
864 /* compute length of even parity distances */
865 if (!((nodeStat
->evenTopDist
== MAXSHORTINT
) ||
866 (nodeStat
->evenBotDist
== MAXSHORTINT
)))
867 evenLen
= (nodeStat
->evenTopDist
+nodeStat
->evenBotDist
);
869 evenLen
= MAXSHORTINT
;
871 /* assign pathlength to minimum of the two */
872 pathLength
= (oddLen
<= evenLen
) ? oddLen
: evenLen
;
877 /* process each child */
879 while (processingDone
!= 2) {
880 if (!processingDone
) {
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.
892 if (Cudd_IsComplement(child
))
893 nodeStat
->oddBotDist
= 1;
895 nodeStat
->evenBotDist
= 1;
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");
903 if (nodeStatChild
->oddBotDist
== MAXSHORTINT
) {
904 if (nodeStatChild
->evenBotDist
== MAXSHORTINT
) {
905 if (!CreateBotDist(realChild
, pathTable
, pathLengthArray
, fp
))
908 fprintf(fp
, "Something wrong, both bot nodeStats should be there\n");
913 /* Update shortest distance from the constant depending on
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
923 if (nodeStatChild
->oddBotDist
!= MAXSHORTINT
)
924 botDist
= nodeStatChild
->oddBotDist
+ 1;
926 botDist
= MAXSHORTINT
;
927 if (nodeStat
->evenBotDist
> botDist
)
928 nodeStat
->evenBotDist
= botDist
;
930 if (nodeStatChild
->evenBotDist
!= MAXSHORTINT
)
931 botDist
= nodeStatChild
->evenBotDist
+ 1;
933 botDist
= MAXSHORTINT
;
934 if (nodeStat
->oddBotDist
> botDist
)
935 nodeStat
->oddBotDist
= botDist
;
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
944 if (nodeStatChild
->evenBotDist
!= MAXSHORTINT
)
945 botDist
= nodeStatChild
->evenBotDist
+ 1;
947 botDist
= MAXSHORTINT
;
948 if (nodeStat
->evenBotDist
> botDist
)
949 nodeStat
->evenBotDist
= botDist
;
951 if (nodeStatChild
->oddBotDist
!= MAXSHORTINT
)
952 botDist
= nodeStatChild
->oddBotDist
+ 1;
954 botDist
= MAXSHORTINT
;
955 if (nodeStat
->oddBotDist
> botDist
)
956 nodeStat
->oddBotDist
= botDist
;
958 } /* end of else (if not constant child ) */
960 } /* end of while processing Nv, Nnv */
962 /* Compute shortest path length on the fly. */
963 if ((nodeStat
->oddTopDist
!= MAXSHORTINT
) &&
964 (nodeStat
->oddBotDist
!= MAXSHORTINT
))
965 oddLen
= (nodeStat
->oddTopDist
+ nodeStat
->oddBotDist
);
967 oddLen
= MAXSHORTINT
;
969 if ((nodeStat
->evenTopDist
!= MAXSHORTINT
) &&
970 (nodeStat
->evenBotDist
!= MAXSHORTINT
))
971 evenLen
= (nodeStat
->evenTopDist
+nodeStat
->evenBotDist
);
973 evenLen
= MAXSHORTINT
;
975 /* Update path length array that has number of nodes of a particular
977 if (oddLen
< pathLength
) {
978 if (pathLength
!= MAXSHORTINT
)
979 pathLengthArray
[pathLength
]--;
980 if (oddLen
!= MAXSHORTINT
)
981 pathLengthArray
[oddLen
]++;
984 if (evenLen
< pathLength
) {
985 if (pathLength
!= MAXSHORTINT
)
986 pathLengthArray
[pathLength
]--;
987 if (evenLen
!= MAXSHORTINT
)
988 pathLengthArray
[evenLen
]++;
993 } /*end of CreateBotDist */
996 /**Function********************************************************************
998 Synopsis [ The outer procedure to label each node with its shortest
999 distance from the root and constant]
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.]
1011 SeeAlso [CreateTopDist CreateBotDist]
1013 ******************************************************************************/
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 */)
1021 st_table
*pathTable
;
1022 NodeDist_t
*nodeStat
;
1029 int childQueueIndex
, parentQueueIndex
;
1031 /* Creating path Table for storing data about nodes */
1032 pathTable
= st_init_table(st_ptrcmp
,st_ptrhash
);
1034 /* initializing pages for info about each node */
1035 maxNodeDistPages
= INITIAL_PAGES
;
1036 nodeDistPages
= ALLOC(NodeDist_t
*, maxNodeDistPages
);
1037 if (nodeDistPages
== NULL
) {
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
);
1048 nodeDistPageIndex
= 0;
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
) {
1057 currentQueuePage
= queuePages
[queuePage
] = ALLOC(DdNode
*, queuePageSize
);
1058 if (currentQueuePage
== NULL
) {
1059 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
1065 /* Enter the root node into the queue to start with. */
1066 parentPage
= queuePage
;
1067 parentQueueIndex
= queuePageIndex
;
1069 *(currentQueuePage
+ queuePageIndex
) = node
;
1071 childPage
= currentQueuePage
;
1072 childQueueIndex
= queuePageIndex
;
1074 N
= Cudd_Regular(node
);
1076 if (nodeDistPageIndex
== nodeDistPageSize
) ResizeNodeDistPages();
1078 for (i
= 0; i
<= nodeDistPage
; i
++) FREE(nodeDistPages
[i
]);
1079 FREE(nodeDistPages
);
1080 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
1082 st_free_table(pathTable
);
1086 nodeStat
= currentNodeDistPage
+ nodeDistPageIndex
;
1087 nodeDistPageIndex
++;
1089 nodeStat
->oddTopDist
= MAXSHORTINT
;
1090 nodeStat
->evenTopDist
= MAXSHORTINT
;
1091 nodeStat
->evenBotDist
= MAXSHORTINT
;
1092 nodeStat
->oddBotDist
= MAXSHORTINT
;
1093 nodeStat
->regResult
= NULL
;
1094 nodeStat
->compResult
= NULL
;
1096 insertValue
= st_insert(pathTable
, (char *)N
, (char *)nodeStat
);
1097 if (insertValue
== ST_OUT_OF_MEM
) {
1099 for (i
= 0; i
<= nodeDistPage
; i
++) FREE(nodeDistPages
[i
]);
1100 FREE(nodeDistPages
);
1101 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
1103 st_free_table(pathTable
);
1105 } else if (insertValue
== 1) {
1106 fprintf(fp
, "Something wrong, the entry exists but didnt show up in st_lookup\n");
1110 if (Cudd_IsComplement(node
)) {
1111 nodeStat
->oddTopDist
= 0;
1113 nodeStat
->evenTopDist
= 0;
1116 /* call the function that counts the distance of each node from the
1122 CreateTopDist(pathTable
, parentPage
, parentQueueIndex
, (int) topLen
,
1123 childPage
, childQueueIndex
, numParents
, fp
);
1125 fprintf(fp
, "Out of Memory and cant count path lengths\n");
1132 /* call the function that counts the distance of each node from the
1135 if (!CreateBotDist(node
, pathTable
, pathLengthArray
, fp
)) return(NULL
);
1137 /* free BFS queue pages as no longer required */
1138 for (i
= 0; i
<= queuePage
; i
++) FREE(queuePages
[i
]);
1143 (void) fprintf(fp
, "Out of Memory, cannot allocate pages\n");
1147 } /*end of CreatePathTable */
1150 /**Function********************************************************************
1152 Synopsis [Chooses the maximum allowable path length of nodes under the
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;]
1165 ******************************************************************************/
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 */)
1174 unsigned int i
, maxpath
;
1180 /* quit loop if i reaches max number of variables or if temp reaches
1183 while ((i
< (unsigned) numVars
+1) && (temp
> 0)) {
1184 if (pathLengthArray
[i
] > 0) {
1186 temp
= temp
- pathLengthArray
[i
];
1190 /* if all nodes of max path are needed */
1192 maxpath
++; /* now maxpath becomes the next maxppath or max number
1195 } else { /* normal case when subset required is less than size of
1197 *excess
= temp
+ pathLengthArray
[maxpath
];
1201 fprintf(fp
, "Path Length array seems to be all zeroes, check\n");
1205 } /* end of AssessPathLength */
1208 /**Function********************************************************************
1210 Synopsis [Builds the BDD with nodes labeled with path length less than or equal to maxpath]
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
1245 SideEffects [SubsetNodeTable is changed if it is not NIL.]
1249 ******************************************************************************/
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 */)
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
;
1265 unsigned int childPathLength
, oddLen
, evenLen
, NnvPathLength
, NvPathLength
;
1266 unsigned int NvBotDist
, NnvBotDist
;
1268 int processingDone
, thenDone
, elseDone
;
1274 if (Cudd_IsConstant(node
))
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
;
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.
1292 /* If this node is reached with an odd parity, get odd parity results. */
1293 if (Cudd_IsComplement(node
)) {
1294 if (nodeStat
->compResult
!= NULL
) {
1298 return(nodeStat
->compResult
);
1301 /* if this node is reached with an even parity, get even parity
1304 if (nodeStat
->regResult
!= NULL
) {
1308 return(nodeStat
->regResult
);
1317 Nv
= Cudd_NotCond(Nv
, Cudd_IsComplement(node
));
1318 Nnv
= Cudd_NotCond(Nnv
, Cudd_IsComplement(node
));
1320 /* no child processed */
1322 /* then child not processed */
1325 /* else child not processed */
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;
1336 cuddRef(ThenBranch
);
1337 if (ThenBranch
== NULL
) {
1343 NvBotDist
= MAXSHORTINT
;
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
;
1353 /* Derive shortest path length for child. */
1354 if ((nodeStatNv
->oddTopDist
!= MAXSHORTINT
) &&
1355 (nodeStatNv
->oddBotDist
!= MAXSHORTINT
)) {
1356 oddLen
= (nodeStatNv
->oddTopDist
+ nodeStatNv
->oddBotDist
);
1358 oddLen
= MAXSHORTINT
;
1361 if ((nodeStatNv
->evenTopDist
!= MAXSHORTINT
) &&
1362 (nodeStatNv
->evenBotDist
!= MAXSHORTINT
)) {
1363 evenLen
= (nodeStatNv
->evenTopDist
+nodeStatNv
->evenBotDist
);
1365 evenLen
= MAXSHORTINT
;
1368 NvPathLength
= (oddLen
<= evenLen
) ? oddLen
: evenLen
;
1369 NvBotDist
= (oddLen
<= evenLen
) ? nodeStatNv
->oddBotDist
:
1370 nodeStatNv
->evenBotDist
;
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;
1380 cuddRef(ElseBranch
);
1381 if (ElseBranch
== NULL
) {
1387 NnvBotDist
= MAXSHORTINT
;
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
;
1397 /* Derive shortest path length for child. */
1398 if ((nodeStatNnv
->oddTopDist
!= MAXSHORTINT
) &&
1399 (nodeStatNnv
->oddBotDist
!= MAXSHORTINT
)) {
1400 oddLen
= (nodeStatNnv
->oddTopDist
+ nodeStatNnv
->oddBotDist
);
1402 oddLen
= MAXSHORTINT
;
1405 if ((nodeStatNnv
->evenTopDist
!= MAXSHORTINT
) &&
1406 (nodeStatNnv
->evenBotDist
!= MAXSHORTINT
)) {
1407 evenLen
= (nodeStatNnv
->evenTopDist
+nodeStatNnv
->evenBotDist
);
1409 evenLen
= MAXSHORTINT
;
1412 NnvPathLength
= (oddLen
<= evenLen
) ? oddLen
: evenLen
;
1413 NnvBotDist
= (oddLen
<= evenLen
) ? nodeStatNnv
->oddBotDist
:
1414 nodeStatNnv
->evenBotDist
;
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
1425 if ((NvPathLength
< NnvPathLength
) ||
1426 ((NvPathLength
== NnvPathLength
) && (tiebreakChild
== 1))) {
1430 childPathLength
= NvPathLength
;
1435 childPathLength
= NnvPathLength
;
1436 } /* then path length less than else path length */
1438 /* if one child processed, process the other */
1443 childPathLength
= NnvPathLength
;
1448 childPathLength
= NvPathLength
;
1449 } /* end of else pick the Then child if ELSE child processed */
1450 } /* end of else one child has been processed */
1452 /* ignore (replace with constant 0) all nodes which lie on paths larger
1453 * than the maximum length of the path required
1455 if (childPathLength
> info
->maxpath
) {
1456 /* record nodes visited */
1459 if (childPathLength
< info
->maxpath
) {
1460 if (info
->findShortestPath
) {
1461 info
->findShortestPath
= 0;
1463 childBranch
= BuildSubsetBdd(dd
, pathTable
, child
, info
,
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
,
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;
1476 childBranch
= BuildSubsetBdd(dd
, pathTable
, child
, info
,
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
) {
1488 (void) fprintf(dd
->err
, "OUT of memory\n");
1489 info
->thresholdReached
= 0;
1492 info
->thresholdReached
--;
1493 childBranch
= BuildSubsetBdd(dd
, pathTable
,
1494 child
, info
,subsetNodeTable
);
1496 } else { /* not find shortest path, we dont need this
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
) {
1505 (void) fprintf(dd
->err
, "OUT of memory\n");
1506 info
->thresholdReached
= 0;
1509 info
->thresholdReached
--;
1510 if (info
->thresholdReached
<= 0) {
1511 info
->findShortestPath
= 1;
1513 childBranch
= BuildSubsetBdd(dd
, pathTable
,
1514 child
, info
, subsetNodeTable
);
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
);
1527 if (ElseBranch
!= NULL
) {
1528 Cudd_RecursiveDeref(dd
, ElseBranch
);
1534 cuddRef(childBranch
);
1537 ThenBranch
= childBranch
;
1539 ElseBranch
= childBranch
;
1543 } /*end of while processing Nv, Nnv */
1545 info
->findShortestPath
= 0;
1546 topid
= Cudd_NodeReadIndex(N
);
1547 topv
= Cudd_ReadVars(dd
, topid
);
1549 neW
= cuddBddIteRecur(dd
, topv
, ThenBranch
, ElseBranch
);
1553 Cudd_RecursiveDeref(dd
, topv
);
1554 Cudd_RecursiveDeref(dd
, ThenBranch
);
1555 Cudd_RecursiveDeref(dd
, ElseBranch
);
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.
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");
1572 if (st_count(subsetNodeTable
) > info
->threshold
) {
1573 info
->thresholdReached
= 0;
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
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
1599 if (nodeStat
->regResult
!= NULL
) {
1600 Cudd_RecursiveDeref(dd
, nodeStat
->regResult
);
1602 nodeStat
->regResult
= Cudd_Not(neW
);
1603 cuddRef(nodeStat
->regResult
);
1607 nodeStat
->regResult
= neW
;
1608 cuddRef(nodeStat
->regResult
);
1613 if (nodeStat
->compResult
!= NULL
) {
1614 Cudd_RecursiveDeref(dd
, nodeStat
->compResult
);
1616 nodeStat
->compResult
= Cudd_Not(neW
);
1617 cuddRef(nodeStat
->compResult
);
1623 } /* end of else i.e. Subset != NULL */
1624 } /* end of BuildSubsetBdd */
1627 /**Function********************************************************************
1629 Synopsis [Procedure to free te result dds stored in the NodeDist pages.]
1637 ******************************************************************************/
1638 static enum st_retval
1644 NodeDist_t
*nodeStat
;
1647 nodeStat
= (NodeDist_t
*)value
;
1648 dd
= (DdManager
*)arg
;
1649 if (nodeStat
->regResult
!= NULL
) {
1650 Cudd_RecursiveDeref(dd
, nodeStat
->regResult
);
1652 if (nodeStat
->compResult
!= NULL
) {
1653 Cudd_RecursiveDeref(dd
, nodeStat
->compResult
);
1655 return(ST_CONTINUE
);
1657 } /* end of stPathTableFree */