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