source: vis_dev/glu-2.1/src/cuBdd/cuddSubsetSP.c @ 10

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

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