1 /**CFile***********************************************************************
2
3 FileName [cuddSubsetHB.c]
4
5 PackageName [cudd]
6
7 Synopsis [Procedure to subset the given BDD by choosing the heavier
8 branches.]
9
10
11 Description [External procedures provided by this module:
12 <ul>
13 <li> Cudd_SubsetHeavyBranch()
14 <li> Cudd_SupersetHeavyBranch()
15 </ul>
16 Internal procedures included in this module:
17 <ul>
18 <li> cuddSubsetHeavyBranch()
19 </ul>
20 Static procedures included in this module:
21 <ul>
22 <li> ResizeCountMintermPages();
23 <li> ResizeNodeDataPages()
24 <li> ResizeCountNodePages()
25 <li> SubsetCountMintermAux()
26 <li> SubsetCountMinterm()
27 <li> SubsetCountNodesAux()
28 <li> SubsetCountNodes()
29 <li> BuildSubsetBdd()
30 </ul>
31 ]
32
33 SeeAlso [cuddSubsetSP.c]
34
35 Author [Kavita Ravi]
36
37 Copyright [Copyright (c) 1995-2012, 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 #ifdef __STDC__
72 #include <float.h>
73 #else
74 #define DBL_MAX_EXP 1024
75 #endif
76 #include "util.h"
77 #include "cuddInt.h"
78
79 /*---------------------------------------------------------------------------*/
80 /* Constant declarations */
81 /*---------------------------------------------------------------------------*/
82
83 #define DEFAULT_PAGE_SIZE 2048
84 #define DEFAULT_NODE_DATA_PAGE_SIZE 1024
85 #define INITIAL_PAGES 128
86
87
88 /*---------------------------------------------------------------------------*/
89 /* Stucture declarations */
90 /*---------------------------------------------------------------------------*/
91
92 /* data structure to store the information on each node. It keeps
93 * the number of minterms represented by the DAG rooted at this node
94 * in terms of the number of variables specified by the user, number
95 * of nodes in this DAG and the number of nodes of its child with
96 * lesser number of minterms that are not shared by the child with
97 * more minterms
98 */
99 struct NodeData {
100 double *mintermPointer;
101 int *nodesPointer;
102 int *lightChildNodesPointer;
103 };
104
105 /*---------------------------------------------------------------------------*/
106 /* Type declarations */
107 /*---------------------------------------------------------------------------*/
108
109 typedef struct NodeData NodeData_t;
110
111 /*---------------------------------------------------------------------------*/
112 /* Variable declarations */
113 /*---------------------------------------------------------------------------*/
114
115 #ifndef lint
116 static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.39 2012/02/05 01:07:19 fabio Exp $";
117 #endif
118
119 static int memOut;
120 #ifdef DEBUG
121 static int num_calls;
122 #endif
123
124 static DdNode *zero, *one; /* constant functions */
125 static double **mintermPages; /* pointers to the pages */
126 static int **nodePages; /* pointers to the pages */
127 static int **lightNodePages; /* pointers to the pages */
128 static double *currentMintermPage; /* pointer to the current
129 page */
130 static double max; /* to store the 2^n value of the number
131 * of variables */
132
133 static int *currentNodePage; /* pointer to the current
134 page */
135 static int *currentLightNodePage; /* pointer to the
136 * current page */
137 static int pageIndex; /* index to next element */
138 static int page; /* index to current page */
139 static int pageSize = DEFAULT_PAGE_SIZE; /* page size */
140 static int maxPages; /* number of page pointers */
141
142 static NodeData_t *currentNodeDataPage; /* pointer to the current
143 page */
144 static int nodeDataPage; /* index to next element */
145 static int nodeDataPageIndex; /* index to next element */
146 static NodeData_t **nodeDataPages; /* index to current page */
147 static int nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
148 /* page size */
149 static int maxNodeDataPages; /* number of page pointers */
150
151
152 /*---------------------------------------------------------------------------*/
153 /* Macro declarations */
154 /*---------------------------------------------------------------------------*/
155
156 /**AutomaticStart*************************************************************/
157
158 /*---------------------------------------------------------------------------*/
159 /* Static function prototypes */
160 /*---------------------------------------------------------------------------*/
161
162 static void ResizeNodeDataPages (void);
163 static void ResizeCountMintermPages (void);
164 static void ResizeCountNodePages (void);
165 static double SubsetCountMintermAux (DdNode *node, double max, st_table *table);
166 static st_table * SubsetCountMinterm (DdNode *node, int nvars);
167 static int SubsetCountNodesAux (DdNode *node, st_table *table, double max);
168 static int SubsetCountNodes (DdNode *node, st_table *table, int nvars);
169 static void StoreNodes (st_table *storeTable, DdManager *dd, DdNode *node);
170 static DdNode * BuildSubsetBdd (DdManager *dd, DdNode *node, int *size, st_table *visitedTable, int threshold, st_table *storeTable, st_table *approxTable);
171
172 /**AutomaticEnd***************************************************************/
173
174
175 /*---------------------------------------------------------------------------*/
176 /* Definition of exported functions */
177 /*---------------------------------------------------------------------------*/
178
179 /**Function********************************************************************
180
181 Synopsis [Extracts a dense subset from a BDD with the heavy branch
182 heuristic.]
183
184 Description [Extracts a dense subset from a BDD. This procedure
185 builds a subset by throwing away one of the children of each node,
186 starting from the root, until the result is small enough. The child
187 that is eliminated from the result is the one that contributes the
188 fewer minterms. Returns a pointer to the BDD of the subset if
189 successful. NULL if the procedure runs out of memory. The parameter
190 numVars is the maximum number of variables to be used in minterm
191 calculation and node count calculation. The optimal number should
192 be as close as possible to the size of the support of f. However,
193 it is safe to pass the value returned by Cudd_ReadSize for numVars
194 when the number of variables is under 1023. If numVars is larger
195 than 1023, it will overflow. If a 0 parameter is passed then the
196 procedure will compute a value which will avoid overflow but will
197 cause underflow with 2046 variables or more.]
198
199 SideEffects [None]
200
201 SeeAlso [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]
202
203 ******************************************************************************/
204 DdNode *
Cudd_SubsetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)205 Cudd_SubsetHeavyBranch(
206 DdManager * dd /* manager */,
207 DdNode * f /* function to be subset */,
208 int numVars /* number of variables in the support of f */,
209 int threshold /* maximum number of nodes in the subset */)
210 {
211 DdNode *subset;
212
213 memOut = 0;
214 do {
215 dd->reordered = 0;
216 subset = cuddSubsetHeavyBranch(dd, f, numVars, threshold);
217 } while ((dd->reordered == 1) && (!memOut));
218
219 return(subset);
220
221 } /* end of Cudd_SubsetHeavyBranch */
222
223
224 /**Function********************************************************************
225
226 Synopsis [Extracts a dense superset from a BDD with the heavy branch
227 heuristic.]
228
229 Description [Extracts a dense superset from a BDD. The procedure is
230 identical to the subset procedure except for the fact that it
231 receives the complement of the given function. Extracting the subset
232 of the complement function is equivalent to extracting the superset
233 of the function. This procedure builds a superset by throwing away
234 one of the children of each node starting from the root of the
235 complement function, until the result is small enough. The child
236 that is eliminated from the result is the one that contributes the
237 fewer minterms.
238 Returns a pointer to the BDD of the superset if successful. NULL if
239 intermediate result causes the procedure to run out of memory. The
240 parameter numVars is the maximum number of variables to be used in
241 minterm calculation and node count calculation. The optimal number
242 should be as close as possible to the size of the support of f.
243 However, it is safe to pass the value returned by Cudd_ReadSize for
244 numVars when the number of variables is under 1023. If numVars is
245 larger than 1023, it will overflow. If a 0 parameter is passed then
246 the procedure will compute a value which will avoid overflow but
247 will cause underflow with 2046 variables or more.]
248
249 SideEffects [None]
250
251 SeeAlso [Cudd_SubsetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]
252
253 ******************************************************************************/
254 DdNode *
Cudd_SupersetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)255 Cudd_SupersetHeavyBranch(
256 DdManager * dd /* manager */,
257 DdNode * f /* function to be superset */,
258 int numVars /* number of variables in the support of f */,
259 int threshold /* maximum number of nodes in the superset */)
260 {
261 DdNode *subset, *g;
262
263 g = Cudd_Not(f);
264 memOut = 0;
265 do {
266 dd->reordered = 0;
267 subset = cuddSubsetHeavyBranch(dd, g, numVars, threshold);
268 } while ((dd->reordered == 1) && (!memOut));
269
270 return(Cudd_NotCond(subset, (subset != NULL)));
271
272 } /* end of Cudd_SupersetHeavyBranch */
273
274
275 /*---------------------------------------------------------------------------*/
276 /* Definition of internal functions */
277 /*---------------------------------------------------------------------------*/
278
279
280 /**Function********************************************************************
281
282 Synopsis [The main procedure that returns a subset by choosing the heavier
283 branch in the BDD.]
284
285 Description [Here a subset BDD is built by throwing away one of the
286 children. Starting at root, annotate each node with the number of
287 minterms (in terms of the total number of variables specified -
288 numVars), number of nodes taken by the DAG rooted at this node and
289 number of additional nodes taken by the child that has the lesser
290 minterms. The child with the lower number of minterms is thrown away
291 and a dyanmic count of the nodes of the subset is kept. Once the
292 threshold is reached the subset is returned to the calling
293 procedure.]
294
295 SideEffects [None]
296
297 SeeAlso [Cudd_SubsetHeavyBranch]
298
299 ******************************************************************************/
300 DdNode *
cuddSubsetHeavyBranch(DdManager * dd,DdNode * f,int numVars,int threshold)301 cuddSubsetHeavyBranch(
302 DdManager * dd /* DD manager */,
303 DdNode * f /* current DD */,
304 int numVars /* maximum number of variables */,
305 int threshold /* threshold size for the subset */)
306 {
307
308 int i, *size;
309 st_table *visitedTable;
310 int numNodes;
311 NodeData_t *currNodeQual;
312 DdNode *subset;
313 st_table *storeTable, *approxTable;
314 DdNode *key, *value;
315 st_generator *stGen;
316
317 if (f == NULL) {
318 fprintf(dd->err, "Cannot subset, nil object\n");
319 dd->errorCode = CUDD_INVALID_ARG;
320 return(NULL);
321 }
322
323 one = Cudd_ReadOne(dd);
324 zero = Cudd_Not(one);
325
326 /* If user does not know numVars value, set it to the maximum
327 * exponent that the pow function can take. The -1 is due to the
328 * discrepancy in the value that pow takes and the value that
329 * log gives.
330 */
331 if (numVars == 0) {
332 /* set default value */
333 numVars = DBL_MAX_EXP - 1;
334 }
335
336 if (Cudd_IsConstant(f)) {
337 return(f);
338 }
339
340 max = pow(2.0, (double)numVars);
341
342 /* Create visited table where structures for node data are allocated and
343 stored in a st_table */
344 visitedTable = SubsetCountMinterm(f, numVars);
345 if ((visitedTable == NULL) || memOut) {
346 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
347 dd->errorCode = CUDD_MEMORY_OUT;
348 return(0);
349 }
350 numNodes = SubsetCountNodes(f, visitedTable, numVars);
351 if (memOut) {
352 (void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
353 dd->errorCode = CUDD_MEMORY_OUT;
354 return(0);
355 }
356
357 if (st_lookup(visitedTable, f, &currNodeQual) == 0) {
358 fprintf(dd->err,
359 "Something is wrong, ought to be node quality table\n");
360 dd->errorCode = CUDD_INTERNAL_ERROR;
361 }
362
363 size = ALLOC(int, 1);
364 if (size == NULL) {
365 dd->errorCode = CUDD_MEMORY_OUT;
366 return(NULL);
367 }
368 *size = numNodes;
369
370 #ifdef DEBUG
371 num_calls = 0;
372 #endif
373 /* table to store nodes being created. */
374 storeTable = st_init_table(st_ptrcmp, st_ptrhash);
375 /* insert the constant */
376 cuddRef(one);
377 if (st_insert(storeTable, Cudd_ReadOne(dd), NULL) ==
378 ST_OUT_OF_MEM) {
379 fprintf(dd->out, "Something wrong, st_table insert failed\n");
380 }
381 /* table to store approximations of nodes */
382 approxTable = st_init_table(st_ptrcmp, st_ptrhash);
383 subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
384 storeTable, approxTable);
385 if (subset != NULL) {
386 cuddRef(subset);
387 }
388
389 stGen = st_init_gen(approxTable);
390 if (stGen == NULL) {
391 st_free_table(approxTable);
392 return(NULL);
393 }
394 while(st_gen(stGen, &key, &value)) {
395 Cudd_RecursiveDeref(dd, value);
396 }
397 st_free_gen(stGen); stGen = NULL;
398 st_free_table(approxTable);
399
400 stGen = st_init_gen(storeTable);
401 if (stGen == NULL) {
402 st_free_table(storeTable);
403 return(NULL);
404 }
405 while(st_gen(stGen, &key, &value)) {
406 Cudd_RecursiveDeref(dd, key);
407 }
408 st_free_gen(stGen); stGen = NULL;
409 st_free_table(storeTable);
410
411 for (i = 0; i <= page; i++) {
412 FREE(mintermPages[i]);
413 }
414 FREE(mintermPages);
415 for (i = 0; i <= page; i++) {
416 FREE(nodePages[i]);
417 }
418 FREE(nodePages);
419 for (i = 0; i <= page; i++) {
420 FREE(lightNodePages[i]);
421 }
422 FREE(lightNodePages);
423 for (i = 0; i <= nodeDataPage; i++) {
424 FREE(nodeDataPages[i]);
425 }
426 FREE(nodeDataPages);
427 st_free_table(visitedTable);
428 FREE(size);
429 #if 0
430 (void) Cudd_DebugCheck(dd);
431 (void) Cudd_CheckKeys(dd);
432 #endif
433
434 if (subset != NULL) {
435 #ifdef DD_DEBUG
436 if (!Cudd_bddLeq(dd, subset, f)) {
437 fprintf(dd->err, "Wrong subset\n");
438 dd->errorCode = CUDD_INTERNAL_ERROR;
439 return(NULL);
440 }
441 #endif
442 cuddDeref(subset);
443 return(subset);
444 } else {
445 return(NULL);
446 }
447 } /* end of cuddSubsetHeavyBranch */
448
449
450 /*---------------------------------------------------------------------------*/
451 /* Definition of static functions */
452 /*---------------------------------------------------------------------------*/
453
454
455 /**Function********************************************************************
456
457 Synopsis [Resize the number of pages allocated to store the node data.]
458
459 Description [Resize the number of pages allocated to store the node data
460 The procedure moves the counter to the next page when the end of
461 the page is reached and allocates new pages when necessary.]
462
463 SideEffects [Changes the size of pages, page, page index, maximum
464 number of pages freeing stuff in case of memory out. ]
465
466 SeeAlso []
467
468 ******************************************************************************/
469 static void
ResizeNodeDataPages(void)470 ResizeNodeDataPages(void)
471 {
472 int i;
473 NodeData_t **newNodeDataPages;
474
475 nodeDataPage++;
476 /* If the current page index is larger than the number of pages
477 * allocated, allocate a new page array. Page numbers are incremented by
478 * INITIAL_PAGES
479 */
480 if (nodeDataPage == maxNodeDataPages) {
481 newNodeDataPages = ALLOC(NodeData_t *,maxNodeDataPages + INITIAL_PAGES);
482 if (newNodeDataPages == NULL) {
483 for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
484 FREE(nodeDataPages);
485 memOut = 1;
486 return;
487 } else {
488 for (i = 0; i < maxNodeDataPages; i++) {
489 newNodeDataPages[i] = nodeDataPages[i];
490 }
491 /* Increase total page count */
492 maxNodeDataPages += INITIAL_PAGES;
493 FREE(nodeDataPages);
494 nodeDataPages = newNodeDataPages;
495 }
496 }
497 /* Allocate a new page */
498 currentNodeDataPage = nodeDataPages[nodeDataPage] =
499 ALLOC(NodeData_t ,nodeDataPageSize);
500 if (currentNodeDataPage == NULL) {
501 for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
502 FREE(nodeDataPages);
503 memOut = 1;
504 return;
505 }
506 /* reset page index */
507 nodeDataPageIndex = 0;
508 return;
509
510 } /* end of ResizeNodeDataPages */
511
512
513 /**Function********************************************************************
514
515 Synopsis [Resize the number of pages allocated to store the minterm
516 counts. ]
517
518 Description [Resize the number of pages allocated to store the minterm
519 counts. The procedure moves the counter to the next page when the
520 end of the page is reached and allocates new pages when necessary.]
521
522 SideEffects [Changes the size of minterm pages, page, page index, maximum
523 number of pages freeing stuff in case of memory out. ]
524
525 SeeAlso []
526
527 ******************************************************************************/
528 static void
ResizeCountMintermPages(void)529 ResizeCountMintermPages(void)
530 {
531 int i;
532 double **newMintermPages;
533
534 page++;
535 /* If the current page index is larger than the number of pages
536 * allocated, allocate a new page array. Page numbers are incremented by
537 * INITIAL_PAGES
538 */
539 if (page == maxPages) {
540 newMintermPages = ALLOC(double *,maxPages + INITIAL_PAGES);
541 if (newMintermPages == NULL) {
542 for (i = 0; i < page; i++) FREE(mintermPages[i]);
543 FREE(mintermPages);
544 memOut = 1;
545 return;
546 } else {
547 for (i = 0; i < maxPages; i++) {
548 newMintermPages[i] = mintermPages[i];
549 }
550 /* Increase total page count */
551 maxPages += INITIAL_PAGES;
552 FREE(mintermPages);
553 mintermPages = newMintermPages;
554 }
555 }
556 /* Allocate a new page */
557 currentMintermPage = mintermPages[page] = ALLOC(double,pageSize);
558 if (currentMintermPage == NULL) {
559 for (i = 0; i < page; i++) FREE(mintermPages[i]);
560 FREE(mintermPages);
561 memOut = 1;
562 return;
563 }
564 /* reset page index */
565 pageIndex = 0;
566 return;
567
568 } /* end of ResizeCountMintermPages */
569
570
571 /**Function********************************************************************
572
573 Synopsis [Resize the number of pages allocated to store the node counts.]
574
575 Description [Resize the number of pages allocated to store the node counts.
576 The procedure moves the counter to the next page when the end of
577 the page is reached and allocates new pages when necessary.]
578
579 SideEffects [Changes the size of pages, page, page index, maximum
580 number of pages freeing stuff in case of memory out.]
581
582 SeeAlso []
583
584 ******************************************************************************/
585 static void
ResizeCountNodePages(void)586 ResizeCountNodePages(void)
587 {
588 int i;
589 int **newNodePages;
590
591 page++;
592
593 /* If the current page index is larger than the number of pages
594 * allocated, allocate a new page array. The number of pages is incremented
595 * by INITIAL_PAGES.
596 */
597 if (page == maxPages) {
598 newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
599 if (newNodePages == NULL) {
600 for (i = 0; i < page; i++) FREE(nodePages[i]);
601 FREE(nodePages);
602 for (i = 0; i < page; i++) FREE(lightNodePages[i]);
603 FREE(lightNodePages);
604 memOut = 1;
605 return;
606 } else {
607 for (i = 0; i < maxPages; i++) {
608 newNodePages[i] = nodePages[i];
609 }
610 FREE(nodePages);
611 nodePages = newNodePages;
612 }
613
614 newNodePages = ALLOC(int *,maxPages + INITIAL_PAGES);
615 if (newNodePages == NULL) {
616 for (i = 0; i < page; i++) FREE(nodePages[i]);
617 FREE(nodePages);
618 for (i = 0; i < page; i++) FREE(lightNodePages[i]);
619 FREE(lightNodePages);
620 memOut = 1;
621 return;
622 } else {
623 for (i = 0; i < maxPages; i++) {
624 newNodePages[i] = lightNodePages[i];
625 }
626 FREE(lightNodePages);
627 lightNodePages = newNodePages;
628 }
629 /* Increase total page count */
630 maxPages += INITIAL_PAGES;
631 }
632 /* Allocate a new page */
633 currentNodePage = nodePages[page] = ALLOC(int,pageSize);
634 if (currentNodePage == NULL) {
635 for (i = 0; i < page; i++) FREE(nodePages[i]);
636 FREE(nodePages);
637 for (i = 0; i < page; i++) FREE(lightNodePages[i]);
638 FREE(lightNodePages);
639 memOut = 1;
640 return;
641 }
642 /* Allocate a new page */
643 currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
644 if (currentLightNodePage == NULL) {
645 for (i = 0; i <= page; i++) FREE(nodePages[i]);
646 FREE(nodePages);
647 for (i = 0; i < page; i++) FREE(lightNodePages[i]);
648 FREE(lightNodePages);
649 memOut = 1;
650 return;
651 }
652 /* reset page index */
653 pageIndex = 0;
654 return;
655
656 } /* end of ResizeCountNodePages */
657
658
659 /**Function********************************************************************
660
661 Synopsis [Recursively counts minterms of each node in the DAG.]
662
663 Description [Recursively counts minterms of each node in the DAG.
664 Similar to the cuddCountMintermAux which recursively counts the
665 number of minterms for the dag rooted at each node in terms of the
666 total number of variables (max). This procedure creates the node
667 data structure and stores the minterm count as part of the node
668 data structure. ]
669
670 SideEffects [Creates structures of type node quality and fills the st_table]
671
672 SeeAlso [SubsetCountMinterm]
673
674 ******************************************************************************/
675 static double
SubsetCountMintermAux(DdNode * node,double max,st_table * table)676 SubsetCountMintermAux(
677 DdNode * node /* function to analyze */,
678 double max /* number of minterms of constant 1 */,
679 st_table * table /* visitedTable table */)
680 {
681
682 DdNode *N,*Nv,*Nnv; /* nodes to store cofactors */
683 double min,*pmin; /* minterm count */
684 double min1, min2; /* minterm count */
685 NodeData_t *dummy;
686 NodeData_t *newEntry;
687 int i;
688
689 #ifdef DEBUG
690 num_calls++;
691 #endif
692
693 /* Constant case */
694 if (Cudd_IsConstant(node)) {
695 if (node == zero) {
696 return(0.0);
697 } else {
698 return(max);
699 }
700 } else {
701
702 /* check if entry for this node exists */
703 if (st_lookup(table, node, &dummy)) {
704 min = *(dummy->mintermPointer);
705 return(min);
706 }
707
708 /* Make the node regular to extract cofactors */
709 N = Cudd_Regular(node);
710
711 /* store the cofactors */
712 Nv = Cudd_T(N);
713 Nnv = Cudd_E(N);
714
715 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
716 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
717
718 min1 = SubsetCountMintermAux(Nv, max,table)/2.0;
719 if (memOut) return(0.0);
720 min2 = SubsetCountMintermAux(Nnv,max,table)/2.0;
721 if (memOut) return(0.0);
722 min = (min1+min2);
723
724 /* if page index is at the bottom, then create a new page */
725 if (pageIndex == pageSize) ResizeCountMintermPages();
726 if (memOut) {
727 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
728 FREE(nodeDataPages);
729 st_free_table(table);
730 return(0.0);
731 }
732
733 /* point to the correct location in the page */
734 pmin = currentMintermPage+pageIndex;
735 pageIndex++;
736
737 /* store the minterm count of this node in the page */
738 *pmin = min;
739
740 /* Note I allocate the struct here. Freeing taken care of later */
741 if (nodeDataPageIndex == nodeDataPageSize) ResizeNodeDataPages();
742 if (memOut) {
743 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
744 FREE(mintermPages);
745 st_free_table(table);
746 return(0.0);
747 }
748
749 newEntry = currentNodeDataPage + nodeDataPageIndex;
750 nodeDataPageIndex++;
751
752 /* points to the correct location in the page */
753 newEntry->mintermPointer = pmin;
754 /* initialize this field of the Node Quality structure */
755 newEntry->nodesPointer = NULL;
756
757 /* insert entry for the node in the table */
758 if (st_insert(table,node, newEntry) == ST_OUT_OF_MEM) {
759 memOut = 1;
760 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
761 FREE(mintermPages);
762 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
763 FREE(nodeDataPages);
764 st_free_table(table);
765 return(0.0);
766 }
767 return(min);
768 }
769
770 } /* end of SubsetCountMintermAux */
771
772
773 /**Function********************************************************************
774
775 Synopsis [Counts minterms of each node in the DAG]
776
777 Description [Counts minterms of each node in the DAG. Similar to the
778 Cudd_CountMinterm procedure except this returns the minterm count for
779 all the nodes in the bdd in an st_table.]
780
781 SideEffects [none]
782
783 SeeAlso [SubsetCountMintermAux]
784
785 ******************************************************************************/
786 static st_table *
SubsetCountMinterm(DdNode * node,int nvars)787 SubsetCountMinterm(
788 DdNode * node /* function to be analyzed */,
789 int nvars /* number of variables node depends on */)
790 {
791 st_table *table;
792 int i;
793
794
795 #ifdef DEBUG
796 num_calls = 0;
797 #endif
798
799 max = pow(2.0,(double) nvars);
800 table = st_init_table(st_ptrcmp,st_ptrhash);
801 if (table == NULL) goto OUT_OF_MEM;
802 maxPages = INITIAL_PAGES;
803 mintermPages = ALLOC(double *,maxPages);
804 if (mintermPages == NULL) {
805 st_free_table(table);
806 goto OUT_OF_MEM;
807 }
808 page = 0;
809 currentMintermPage = ALLOC(double,pageSize);
810 mintermPages[page] = currentMintermPage;
811 if (currentMintermPage == NULL) {
812 FREE(mintermPages);
813 st_free_table(table);
814 goto OUT_OF_MEM;
815 }
816 pageIndex = 0;
817 maxNodeDataPages = INITIAL_PAGES;
818 nodeDataPages = ALLOC(NodeData_t *, maxNodeDataPages);
819 if (nodeDataPages == NULL) {
820 for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
821 FREE(mintermPages);
822 st_free_table(table);
823 goto OUT_OF_MEM;
824 }
825 nodeDataPage = 0;
826 currentNodeDataPage = ALLOC(NodeData_t ,nodeDataPageSize);
827 nodeDataPages[nodeDataPage] = currentNodeDataPage;
828 if (currentNodeDataPage == NULL) {
829 for (i = 0; i <= page ; i++) FREE(mintermPages[i]);
830 FREE(mintermPages);
831 FREE(nodeDataPages);
832 st_free_table(table);
833 goto OUT_OF_MEM;
834 }
835 nodeDataPageIndex = 0;
836
837 (void) SubsetCountMintermAux(node,max,table);
838 if (memOut) goto OUT_OF_MEM;
839 return(table);
840
841 OUT_OF_MEM:
842 memOut = 1;
843 return(NULL);
844
845 } /* end of SubsetCountMinterm */
846
847
848 /**Function********************************************************************
849
850 Synopsis [Recursively counts the number of nodes under the dag.
851 Also counts the number of nodes under the lighter child of
852 this node.]
853
854 Description [Recursively counts the number of nodes under the dag.
855 Also counts the number of nodes under the lighter child of
856 this node. . Note that the same dag may be the lighter child of two
857 different nodes and have different counts. As with the minterm counts,
858 the node counts are stored in pages to be space efficient and the
859 address for these node counts are stored in an st_table associated
860 to each node. ]
861
862 SideEffects [Updates the node data table with node counts]
863
864 SeeAlso [SubsetCountNodes]
865
866 ******************************************************************************/
867 static int
SubsetCountNodesAux(DdNode * node,st_table * table,double max)868 SubsetCountNodesAux(
869 DdNode * node /* current node */,
870 st_table * table /* table to update node count, also serves as visited table. */,
871 double max /* maximum number of variables */)
872 {
873 int tval, eval, i;
874 DdNode *N, *Nv, *Nnv;
875 double minNv, minNnv;
876 NodeData_t *dummyN, *dummyNv, *dummyNnv, *dummyNBar;
877 int *pmin, *pminBar, *val;
878
879 if ((node == NULL) || Cudd_IsConstant(node))
880 return(0);
881
882 /* if this node has been processed do nothing */
883 if (st_lookup(table, node, &dummyN) == 1) {
884 val = dummyN->nodesPointer;
885 if (val != NULL)
886 return(0);
887 } else {
888 return(0);
889 }
890
891 N = Cudd_Regular(node);
892 Nv = Cudd_T(N);
893 Nnv = Cudd_E(N);
894
895 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
896 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
897
898 /* find the minterm counts for the THEN and ELSE branches */
899 if (Cudd_IsConstant(Nv)) {
900 if (Nv == zero) {
901 minNv = 0.0;
902 } else {
903 minNv = max;
904 }
905 } else {
906 if (st_lookup(table, Nv, &dummyNv) == 1)
907 minNv = *(dummyNv->mintermPointer);
908 else {
909 return(0);
910 }
911 }
912 if (Cudd_IsConstant(Nnv)) {
913 if (Nnv == zero) {
914 minNnv = 0.0;
915 } else {
916 minNnv = max;
917 }
918 } else {
919 if (st_lookup(table, Nnv, &dummyNnv) == 1) {
920 minNnv = *(dummyNnv->mintermPointer);
921 }
922 else {
923 return(0);
924 }
925 }
926
927
928 /* recur based on which has larger minterm, */
929 if (minNv >= minNnv) {
930 tval = SubsetCountNodesAux(Nv, table, max);
931 if (memOut) return(0);
932 eval = SubsetCountNodesAux(Nnv, table, max);
933 if (memOut) return(0);
934
935 /* store the node count of the lighter child. */
936 if (pageIndex == pageSize) ResizeCountNodePages();
937 if (memOut) {
938 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
939 FREE(mintermPages);
940 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
941 FREE(nodeDataPages);
942 st_free_table(table);
943 return(0);
944 }
945 pmin = currentLightNodePage + pageIndex;
946 *pmin = eval; /* Here the ELSE child is lighter */
947 dummyN->lightChildNodesPointer = pmin;
948
949 } else {
950 eval = SubsetCountNodesAux(Nnv, table, max);
951 if (memOut) return(0);
952 tval = SubsetCountNodesAux(Nv, table, max);
953 if (memOut) return(0);
954
955 /* store the node count of the lighter child. */
956 if (pageIndex == pageSize) ResizeCountNodePages();
957 if (memOut) {
958 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
959 FREE(mintermPages);
960 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
961 FREE(nodeDataPages);
962 st_free_table(table);
963 return(0);
964 }
965 pmin = currentLightNodePage + pageIndex;
966 *pmin = tval; /* Here the THEN child is lighter */
967 dummyN->lightChildNodesPointer = pmin;
968
969 }
970 /* updating the page index for node count storage. */
971 pmin = currentNodePage + pageIndex;
972 *pmin = tval + eval + 1;
973 dummyN->nodesPointer = pmin;
974
975 /* pageIndex is parallel page index for count_nodes and count_lightNodes */
976 pageIndex++;
977
978 /* if this node has been reached first, it belongs to a heavier
979 branch. Its complement will be reached later on a lighter branch.
980 Hence the complement has zero node count. */
981
982 if (st_lookup(table, Cudd_Not(node), &dummyNBar) == 1) {
983 if (pageIndex == pageSize) ResizeCountNodePages();
984 if (memOut) {
985 for (i = 0; i < page; i++) FREE(mintermPages[i]);
986 FREE(mintermPages);
987 for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
988 FREE(nodeDataPages);
989 st_free_table(table);
990 return(0);
991 }
992 pminBar = currentLightNodePage + pageIndex;
993 *pminBar = 0;
994 dummyNBar->lightChildNodesPointer = pminBar;
995 /* The lighter child has less nodes than the parent.
996 * So if parent 0 then lighter child zero
997 */
998 if (pageIndex == pageSize) ResizeCountNodePages();
999 if (memOut) {
1000 for (i = 0; i < page; i++) FREE(mintermPages[i]);
1001 FREE(mintermPages);
1002 for (i = 0; i < nodeDataPage; i++) FREE(nodeDataPages[i]);
1003 FREE(nodeDataPages);
1004 st_free_table(table);
1005 return(0);
1006 }
1007 pminBar = currentNodePage + pageIndex;
1008 *pminBar = 0;
1009 dummyNBar->nodesPointer = pminBar ; /* maybe should point to zero */
1010
1011 pageIndex++;
1012 }
1013 return(*pmin);
1014 } /*end of SubsetCountNodesAux */
1015
1016
1017 /**Function********************************************************************
1018
1019 Synopsis [Counts the nodes under the current node and its lighter child]
1020
1021 Description [Counts the nodes under the current node and its lighter
1022 child. Calls a recursive procedure to count the number of nodes of
1023 a DAG rooted at a particular node and the number of nodes taken by its
1024 lighter child.]
1025
1026 SideEffects [None]
1027
1028 SeeAlso [SubsetCountNodesAux]
1029
1030 ******************************************************************************/
1031 static int
SubsetCountNodes(DdNode * node,st_table * table,int nvars)1032 SubsetCountNodes(
1033 DdNode * node /* function to be analyzed */,
1034 st_table * table /* node quality table */,
1035 int nvars /* number of variables node depends on */)
1036 {
1037 int num;
1038 int i;
1039
1040 #ifdef DEBUG
1041 num_calls = 0;
1042 #endif
1043
1044 max = pow(2.0,(double) nvars);
1045 maxPages = INITIAL_PAGES;
1046 nodePages = ALLOC(int *,maxPages);
1047 if (nodePages == NULL) {
1048 goto OUT_OF_MEM;
1049 }
1050
1051 lightNodePages = ALLOC(int *,maxPages);
1052 if (lightNodePages == NULL) {
1053 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1054 FREE(mintermPages);
1055 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1056 FREE(nodeDataPages);
1057 FREE(nodePages);
1058 goto OUT_OF_MEM;
1059 }
1060
1061 page = 0;
1062 currentNodePage = nodePages[page] = ALLOC(int,pageSize);
1063 if (currentNodePage == NULL) {
1064 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1065 FREE(mintermPages);
1066 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1067 FREE(nodeDataPages);
1068 FREE(lightNodePages);
1069 FREE(nodePages);
1070 goto OUT_OF_MEM;
1071 }
1072
1073 currentLightNodePage = lightNodePages[page] = ALLOC(int,pageSize);
1074 if (currentLightNodePage == NULL) {
1075 for (i = 0; i <= page; i++) FREE(mintermPages[i]);
1076 FREE(mintermPages);
1077 for (i = 0; i <= nodeDataPage; i++) FREE(nodeDataPages[i]);
1078 FREE(nodeDataPages);
1079 FREE(currentNodePage);
1080 FREE(lightNodePages);
1081 FREE(nodePages);
1082 goto OUT_OF_MEM;
1083 }
1084
1085 pageIndex = 0;
1086 num = SubsetCountNodesAux(node,table,max);
1087 if (memOut) goto OUT_OF_MEM;
1088 return(num);
1089
1090 OUT_OF_MEM:
1091 memOut = 1;
1092 return(0);
1093
1094 } /* end of SubsetCountNodes */
1095
1096
1097 /**Function********************************************************************
1098
1099 Synopsis [Procedure to recursively store nodes that are retained in the subset.]
1100
1101 Description [rocedure to recursively store nodes that are retained in the subset.]
1102
1103 SideEffects [None]
1104
1105 SeeAlso [StoreNodes]
1106
1107 ******************************************************************************/
1108 static void
StoreNodes(st_table * storeTable,DdManager * dd,DdNode * node)1109 StoreNodes(
1110 st_table * storeTable,
1111 DdManager * dd,
1112 DdNode * node)
1113 {
1114 DdNode *N, *Nt, *Ne;
1115 if (Cudd_IsConstant(dd)) {
1116 return;
1117 }
1118 N = Cudd_Regular(node);
1119 if (st_lookup(storeTable, N, NULL)) {
1120 return;
1121 }
1122 cuddRef(N);
1123 if (st_insert(storeTable, N, NULL) == ST_OUT_OF_MEM) {
1124 fprintf(dd->err,"Something wrong, st_table insert failed\n");
1125 }
1126
1127 Nt = Cudd_T(N);
1128 Ne = Cudd_E(N);
1129
1130 StoreNodes(storeTable, dd, Nt);
1131 StoreNodes(storeTable, dd, Ne);
1132 return;
1133
1134 }
1135
1136
1137 /**Function********************************************************************
1138
1139 Synopsis [Builds the subset BDD using the heavy branch method.]
1140
1141 Description [The procedure carries out the building of the subset BDD
1142 starting at the root. Using the three different counts labelling each node,
1143 the procedure chooses the heavier branch starting from the root and keeps
1144 track of the number of nodes it discards at each step, thus keeping count
1145 of the size of the subset BDD dynamically. Once the threshold is satisfied,
1146 the procedure then calls ITE to build the BDD.]
1147
1148 SideEffects [None]
1149
1150 SeeAlso []
1151
1152 ******************************************************************************/
1153 static DdNode *
BuildSubsetBdd(DdManager * dd,DdNode * node,int * size,st_table * visitedTable,int threshold,st_table * storeTable,st_table * approxTable)1154 BuildSubsetBdd(
1155 DdManager * dd /* DD manager */,
1156 DdNode * node /* current node */,
1157 int * size /* current size of the subset */,
1158 st_table * visitedTable /* visited table storing all node data */,
1159 int threshold,
1160 st_table * storeTable,
1161 st_table * approxTable)
1162 {
1163
1164 DdNode *Nv, *Nnv, *N, *topv, *neW;
1165 double minNv, minNnv;
1166 NodeData_t *currNodeQual;
1167 NodeData_t *currNodeQualT;
1168 NodeData_t *currNodeQualE;
1169 DdNode *ThenBranch, *ElseBranch;
1170 unsigned int topid;
1171 char *dummy;
1172
1173 #ifdef DEBUG
1174 num_calls++;
1175 #endif
1176 /*If the size of the subset is below the threshold, dont do
1177 anything. */
1178 if ((*size) <= threshold) {
1179 /* store nodes below this, so we can recombine if possible */
1180 StoreNodes(storeTable, dd, node);
1181 return(node);
1182 }
1183
1184 if (Cudd_IsConstant(node))
1185 return(node);
1186
1187 /* Look up minterm count for this node. */
1188 if (!st_lookup(visitedTable, node, &currNodeQual)) {
1189 fprintf(dd->err,
1190 "Something is wrong, ought to be in node quality table\n");
1191 }
1192
1193 /* Get children. */
1194 N = Cudd_Regular(node);
1195 Nv = Cudd_T(N);
1196 Nnv = Cudd_E(N);
1197
1198 /* complement if necessary */
1199 Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1200 Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1201
1202 if (!Cudd_IsConstant(Nv)) {
1203 /* find out minterms and nodes contributed by then child */
1204 if (!st_lookup(visitedTable, Nv, &currNodeQualT)) {
1205 fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1206 dd->errorCode = CUDD_INTERNAL_ERROR;
1207 return(NULL);
1208 }
1209 else {
1210 minNv = *(((NodeData_t *)currNodeQualT)->mintermPointer);
1211 }
1212 } else {
1213 if (Nv == zero) {
1214 minNv = 0;
1215 } else {
1216 minNv = max;
1217 }
1218 }
1219 if (!Cudd_IsConstant(Nnv)) {
1220 /* find out minterms and nodes contributed by else child */
1221 if (!st_lookup(visitedTable, Nnv, &currNodeQualE)) {
1222 fprintf(dd->out,"Something wrong, couldnt find nodes in node quality table\n");
1223 dd->errorCode = CUDD_INTERNAL_ERROR;
1224 return(NULL);
1225 } else {
1226 minNnv = *(((NodeData_t *)currNodeQualE)->mintermPointer);
1227 }
1228 } else {
1229 if (Nnv == zero) {
1230 minNnv = 0;
1231 } else {
1232 minNnv = max;
1233 }
1234 }
1235
1236 /* keep track of size of subset by subtracting the number of
1237 * differential nodes contributed by lighter child
1238 */
1239 *size = (*(size)) - (int)*(currNodeQual->lightChildNodesPointer);
1240 if (minNv >= minNnv) { /*SubsetCountNodesAux procedure takes
1241 the Then branch in case of a tie */
1242
1243 /* recur with the Then branch */
1244 ThenBranch = (DdNode *)BuildSubsetBdd(dd, Nv, size,
1245 visitedTable, threshold, storeTable, approxTable);
1246 if (ThenBranch == NULL) {
1247 return(NULL);
1248 }
1249 cuddRef(ThenBranch);
1250 /* The Else branch is either a node that already exists in the
1251 * subset, or one whose approximation has been computed, or
1252 * Zero.
1253 */
1254 if (st_lookup(storeTable, Cudd_Regular(Nnv), &dummy)) {
1255 ElseBranch = Nnv;
1256 cuddRef(ElseBranch);
1257 } else {
1258 if (st_lookup(approxTable, Nnv, &dummy)) {
1259 ElseBranch = (DdNode *)dummy;
1260 cuddRef(ElseBranch);
1261 } else {
1262 ElseBranch = zero;
1263 cuddRef(ElseBranch);
1264 }
1265 }
1266
1267 }
1268 else {
1269 /* recur with the Else branch */
1270 ElseBranch = (DdNode *)BuildSubsetBdd(dd, Nnv, size,
1271 visitedTable, threshold, storeTable, approxTable);
1272 if (ElseBranch == NULL) {
1273 return(NULL);
1274 }
1275 cuddRef(ElseBranch);
1276 /* The Then branch is either a node that already exists in the
1277 * subset, or one whose approximation has been computed, or
1278 * Zero.
1279 */
1280 if (st_lookup(storeTable, Cudd_Regular(Nv), &dummy)) {
1281 ThenBranch = Nv;
1282 cuddRef(ThenBranch);
1283 } else {
1284 if (st_lookup(approxTable, Nv, &dummy)) {
1285 ThenBranch = (DdNode *)dummy;
1286 cuddRef(ThenBranch);
1287 } else {
1288 ThenBranch = zero;
1289 cuddRef(ThenBranch);
1290 }
1291 }
1292 }
1293
1294 /* construct the Bdd with the top variable and the two children */
1295 topid = Cudd_NodeReadIndex(N);
1296 topv = Cudd_ReadVars(dd, topid);
1297 cuddRef(topv);
1298 neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
1299 if (neW != NULL) {
1300 cuddRef(neW);
1301 }
1302 Cudd_RecursiveDeref(dd, topv);
1303 Cudd_RecursiveDeref(dd, ThenBranch);
1304 Cudd_RecursiveDeref(dd, ElseBranch);
1305
1306
1307 if (neW == NULL)
1308 return(NULL);
1309 else {
1310 /* store this node in the store table */
1311 if (!st_lookup(storeTable, Cudd_Regular(neW), &dummy)) {
1312 cuddRef(neW);
1313 if (st_insert(storeTable, Cudd_Regular(neW), NULL) ==
1314 ST_OUT_OF_MEM)
1315 return (NULL);
1316 }
1317 /* store the approximation for this node */
1318 if (N != Cudd_Regular(neW)) {
1319 if (st_lookup(approxTable, node, &dummy)) {
1320 fprintf(dd->err, "This node should not be in the approximated table\n");
1321 } else {
1322 cuddRef(neW);
1323 if (st_insert(approxTable, node, neW) ==
1324 ST_OUT_OF_MEM)
1325 return(NULL);
1326 }
1327 }
1328 cuddDeref(neW);
1329 return(neW);
1330 }
1331 } /* end of BuildSubsetBdd */
1332