source: vis_dev/glu-2.3/src/cuBdd/cuddSubsetHB.c @ 19

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

library glu 2.3
File size: 39.9 KB
Line 
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-2004, Regents of the University of Colorado
38
39  All rights reserved.
40
41  Redistribution and use in source and binary forms, with or without
42  modification, are permitted provided that the following conditions
43  are met:
44
45  Redistributions of source code must retain the above copyright
46  notice, this list of conditions and the following disclaimer.
47
48  Redistributions in binary form must reproduce the above copyright
49  notice, this list of conditions and the following disclaimer in the
50  documentation and/or other materials provided with the distribution.
51
52  Neither the name of the University of Colorado nor the names of its
53  contributors may be used to endorse or promote products derived from
54  this software without specific prior written permission.
55
56  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
57  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
58  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
59  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
60  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
61  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
62  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
63  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
64  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
65  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
66  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
67  POSSIBILITY OF SUCH DAMAGE.]
68
69******************************************************************************/
70
71#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 */
99struct NodeData {
100    double *mintermPointer;
101    int *nodesPointer;
102    int *lightChildNodesPointer;
103};
104
105/*---------------------------------------------------------------------------*/
106/* Type declarations                                                         */
107/*---------------------------------------------------------------------------*/
108
109typedef struct NodeData NodeData_t;
110
111/*---------------------------------------------------------------------------*/
112/* Variable declarations                                                     */
113/*---------------------------------------------------------------------------*/
114
115#ifndef lint
116static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.37 2009/02/20 02:14:58 fabio Exp $";
117#endif
118
119static int memOut;
120#ifdef DEBUG
121static  int             num_calls;
122#endif
123
124static  DdNode          *zero, *one; /* constant functions */
125static  double          **mintermPages; /* pointers to the pages */
126static  int             **nodePages; /* pointers to the pages */
127static  int             **lightNodePages; /* pointers to the pages */
128static  double          *currentMintermPage; /* pointer to the current
129                                                   page */
130static  double          max; /* to store the 2^n value of the number
131                              * of variables */
132
133static  int             *currentNodePage; /* pointer to the current
134                                                   page */
135static  int             *currentLightNodePage; /* pointer to the
136                                                *  current page */
137static  int             pageIndex; /* index to next element */
138static  int             page; /* index to current page */
139static  int             pageSize = DEFAULT_PAGE_SIZE; /* page size */
140static  int             maxPages; /* number of page pointers */
141
142static  NodeData_t      *currentNodeDataPage; /* pointer to the current
143                                                 page */
144static  int             nodeDataPage; /* index to next element */
145static  int             nodeDataPageIndex; /* index to next element */
146static  NodeData_t      **nodeDataPages; /* index to current page */
147static  int             nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
148                                                     /* page size */
149static  int             maxNodeDataPages; /* number of page pointers */
150
151
152/*---------------------------------------------------------------------------*/
153/* Macro declarations                                                        */
154/*---------------------------------------------------------------------------*/
155
156/**AutomaticStart*************************************************************/
157
158/*---------------------------------------------------------------------------*/
159/* Static function prototypes                                                */
160/*---------------------------------------------------------------------------*/
161
162static void ResizeNodeDataPages (void);
163static void ResizeCountMintermPages (void);
164static void ResizeCountNodePages (void);
165static double SubsetCountMintermAux (DdNode *node, double max, st_table *table);
166static st_table * SubsetCountMinterm (DdNode *node, int nvars);
167static int SubsetCountNodesAux (DdNode *node, st_table *table, double max);
168static int SubsetCountNodes (DdNode *node, st_table *table, int nvars);
169static void StoreNodes (st_table *storeTable, DdManager *dd, DdNode *node);
170static 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******************************************************************************/
204DdNode *
205Cudd_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******************************************************************************/
254DdNode *
255Cudd_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******************************************************************************/
300DdNode *
301cuddSubsetHeavyBranch(
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    char *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, (char *)Cudd_ReadOne(dd), NIL(char)) ==
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, (char **)&key, (char **)&value)) {
395        Cudd_RecursiveDeref(dd, (DdNode *)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, (char **)&key, (char **)&value)) {
406        Cudd_RecursiveDeref(dd, (DdNode *)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******************************************************************************/
469static void
470ResizeNodeDataPages(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******************************************************************************/
528static void
529ResizeCountMintermPages(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******************************************************************************/
585static void
586ResizeCountNodePages(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******************************************************************************/
675static double
676SubsetCountMintermAux(
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,(char *)node, (char *)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******************************************************************************/
786static st_table *
787SubsetCountMinterm(
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
841OUT_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******************************************************************************/
867static int
868SubsetCountNodesAux(
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******************************************************************************/
1031static int
1032SubsetCountNodes(
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
1090OUT_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******************************************************************************/
1108static void
1109StoreNodes(
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, (char *)N, NIL(char *))) {
1120        return;
1121    }
1122    cuddRef(N);
1123    if (st_insert(storeTable, (char *)N, NIL(char)) == 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******************************************************************************/
1153static DdNode *
1154BuildSubsetBdd(
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, (char *)Cudd_Regular(Nnv), &dummy)) {
1255          ElseBranch = Nnv;
1256          cuddRef(ElseBranch);
1257        } else {
1258          if (st_lookup(approxTable, (char *)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, (char *)Cudd_Regular(Nv), &dummy)) {
1281          ThenBranch = Nv;
1282          cuddRef(ThenBranch);
1283        } else {
1284          if (st_lookup(approxTable, (char *)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, (char *)Cudd_Regular(neW), &dummy)) {
1312          cuddRef(neW);
1313          if (!st_insert(storeTable, (char *)Cudd_Regular(neW), NIL(char)))
1314              return (NULL);
1315        }
1316        /* store the approximation for this node */
1317        if (N !=  Cudd_Regular(neW)) {
1318            if (st_lookup(approxTable, (char *)node, &dummy)) {
1319                fprintf(dd->err, "This node should not be in the approximated table\n");
1320            } else {
1321                cuddRef(neW);
1322                if (!st_insert(approxTable, (char *)node, (char *)neW))
1323                    return(NULL);
1324            }
1325        }
1326        cuddDeref(neW);
1327        return(neW);
1328    }
1329} /* end of BuildSubsetBdd */
Note: See TracBrowser for help on using the repository browser.