source: vis_dev/glu-2.3/src/cuBdd/cuddSubsetSP.c @ 43

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

library glu 2.3
File size: 53.3 KB
RevLine 
[13]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.34 2009/02/19 16:23:19 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            FREE(excess);
400            FREE(info);
401            return(NULL);
402        } else {
403            if ((nodeStat->oddTopDist != MAXSHORTINT) &&
404                (nodeStat->oddBotDist != MAXSHORTINT))
405                oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
406            else
407                oddLen = MAXSHORTINT;
408
409            if ((nodeStat->evenTopDist != MAXSHORTINT) &&
410                (nodeStat->evenBotDist != MAXSHORTINT))
411                evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
412            else
413                evenLen = MAXSHORTINT;
414
415            pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
416            if (pathLength > maxpath) {
417                (void) fprintf(dd->err, "All computations are bogus, since root has path length greater than max path length within threshold %u, %u\n", maxpath, pathLength);
418                dd->errorCode = CUDD_INTERNAL_ERROR;
419                return(NULL);
420            }
421        }
422
423#ifdef DD_DEBUG
424        numCalls = 0;
425        hits = 0;
426        thishit = 0;
427#endif
428        /* initialize a table to store computed nodes */
429        if (hardlimit) {
430            subsetNodeTable = st_init_table(st_ptrcmp, st_ptrhash);
431        } else {
432            subsetNodeTable = NIL(st_table);
433        }
434        subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable);
435        if (subset != NULL) {
436            cuddRef(subset);
437        }
438        /* record the number of times a computed result for a node is hit */
439
440#ifdef DD_DEBUG
441        (void) fprintf(dd->out, "Hits = %d, New==Node = %d, NumCalls = %d\n",
442                hits, thishit, numCalls);
443#endif
444
445        if (subsetNodeTable != NIL(st_table)) {
446            st_free_table(subsetNodeTable);
447        }
448        st_free_table(info->maxpathTable);
449        st_foreach(pathTable, stPathTableDdFree, (char *)dd);
450
451        FREE(info);
452
453    } else {/* if threshold larger than size of dd */
454        subset = f;
455        cuddRef(subset);
456    }
457    FREE(excess);
458    st_free_table(pathTable);
459    FREE(pathLengthArray);
460    for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
461    FREE(nodeDistPages);
462
463#ifdef DD_DEBUG
464    /* check containment of subset in f */
465    if (subset != NULL) {
466        DdNode *check;
467        check = Cudd_bddIteConstant(dd, subset, f, one);
468        if (check != one) {
469            (void) fprintf(dd->err, "Wrong partition\n");
470            dd->errorCode = CUDD_INTERNAL_ERROR;
471            return(NULL);
472        }
473    }
474#endif
475
476    if (subset != NULL) {
477        cuddDeref(subset);
478        return(subset);
479    } else {
480        return(NULL);
481    }
482
483} /* end of cuddSubsetShortPaths */
484
485
486/*---------------------------------------------------------------------------*/
487/* Definition of static functions                                            */
488/*---------------------------------------------------------------------------*/
489
490
491/**Function********************************************************************
492
493  Synopsis    [Resize the number of pages allocated to store the distances
494  related to each node.]
495
496  Description [Resize the number of pages allocated to store the distances
497  related to each node. The procedure  moves the counter to the
498  next page when the end of the page is reached and allocates new
499  pages when necessary. ]
500
501  SideEffects [Changes the size of  pages, page, page index, maximum
502  number of pages freeing stuff in case of memory out. ]
503
504  SeeAlso     []
505
506******************************************************************************/
507static void
508ResizeNodeDistPages(void)
509{
510    int i;
511    NodeDist_t **newNodeDistPages;
512
513    /* move to next page */
514    nodeDistPage++;
515
516    /* If the current page index is larger than the number of pages
517     * allocated, allocate a new page array. Page numbers are incremented by
518     * INITIAL_PAGES
519     */
520    if (nodeDistPage == maxNodeDistPages) {
521        newNodeDistPages = ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES);
522        if (newNodeDistPages == NULL) {
523            for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]);
524            FREE(nodeDistPages);
525            memOut = 1;
526            return;
527        } else {
528            for (i = 0; i < maxNodeDistPages; i++) {
529                newNodeDistPages[i] = nodeDistPages[i];
530            }
531            /* Increase total page count */
532            maxNodeDistPages += INITIAL_PAGES;
533            FREE(nodeDistPages);
534            nodeDistPages = newNodeDistPages;
535        }
536    }
537    /* Allocate a new page */
538    currentNodeDistPage = nodeDistPages[nodeDistPage] = ALLOC(NodeDist_t,
539                                                              nodeDistPageSize);
540    if (currentNodeDistPage == NULL) {
541        for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]);
542        FREE(nodeDistPages);
543        memOut = 1;
544        return;
545    }
546    /* reset page index */
547    nodeDistPageIndex = 0;
548    return;
549
550} /* end of ResizeNodeDistPages */
551
552
553/**Function********************************************************************
554
555  Synopsis    [Resize the number of pages allocated to store nodes in the BFS
556  traversal of the Bdd  .]
557
558  Description [Resize the number of pages allocated to store nodes in the BFS
559  traversal of the Bdd. The procedure  moves the counter to the
560  next page when the end of the page is reached and allocates new
561  pages when necessary.]
562
563  SideEffects [Changes the size of pages, page, page index, maximum
564  number of pages freeing stuff in case of memory out. ]
565
566  SeeAlso     []
567
568******************************************************************************/
569static void
570ResizeQueuePages(void)
571{
572    int i;
573    DdNode ***newQueuePages;
574
575    queuePage++;
576    /* If the current page index is larger than the number of pages
577     * allocated, allocate a new page array. Page numbers are incremented by
578     * INITIAL_PAGES
579     */
580    if (queuePage == maxQueuePages) {
581        newQueuePages = ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES);
582        if (newQueuePages == NULL) {
583            for (i = 0; i < queuePage; i++) FREE(queuePages[i]);
584            FREE(queuePages);
585            memOut = 1;
586            return;
587        } else {
588            for (i = 0; i < maxQueuePages; i++) {
589                newQueuePages[i] = queuePages[i];
590            }
591            /* Increase total page count */
592            maxQueuePages += INITIAL_PAGES;
593            FREE(queuePages);
594            queuePages = newQueuePages;
595        }
596    }
597    /* Allocate a new page */
598    currentQueuePage = queuePages[queuePage] = ALLOC(DdNode *,queuePageSize);
599    if (currentQueuePage == NULL) {
600        for (i = 0; i < queuePage; i++) FREE(queuePages[i]);
601        FREE(queuePages);
602        memOut = 1;
603        return;
604    }
605    /* reset page index */
606    queuePageIndex = 0;
607    return;
608
609} /* end of ResizeQueuePages */
610
611
612/**Function********************************************************************
613
614  Synopsis    [ Labels each node with its shortest distance from the root]
615
616  Description [ Labels each node with its shortest distance from the root.
617  This is done in a BFS search of the BDD. The nodes are processed
618  in a queue implemented as pages(array) to reduce memory fragmentation.
619  An entry is created for each node visited. The distance from the root
620  to the node with the corresponding  parity is updated. The procedure
621  is called recursively each recusion level handling nodes at a given
622  level from the root.]
623
624
625  SideEffects [Creates entries in the pathTable]
626
627  SeeAlso     [CreatePathTable CreateBotDist]
628
629******************************************************************************/
630static void
631CreateTopDist(
632  st_table * pathTable /* hast table to store path lengths */,
633  int  parentPage /* the pointer to the page on which the first parent in the queue is to be found. */,
634  int  parentQueueIndex /* pointer to the first parent on the page */,
635  int  topLen /* current distance from the root */,
636  DdNode ** childPage /* pointer to the page on which the first child is to be added. */,
637  int  childQueueIndex /* pointer to the first child */,
638  int  numParents /* number of parents to process in this recursive call */,
639  FILE *fp /* where to write messages */)
640{
641    NodeDist_t *nodeStat;
642    DdNode *N, *Nv, *Nnv, *node, *child, *regChild;
643    int  i;
644    int processingDone, childrenCount;
645
646#ifdef DD_DEBUG
647    numCalls++;
648
649    /* assume this procedure comes in with only the root node*/
650    /* set queue index to the next available entry for addition */
651    /* set queue page to page of addition */
652    if ((queuePages[parentPage] == childPage) && (parentQueueIndex ==
653                                                  childQueueIndex)) {
654        fprintf(fp, "Should not happen that they are equal\n");
655    }
656    assert(queuePageIndex == childQueueIndex);
657    assert(currentQueuePage == childPage);
658#endif
659    /* number children added to queue is initialized , needed for
660     * numParents in the next call
661     */
662    childrenCount = 0;
663    /* process all the nodes in this level */
664    while (numParents) {
665        numParents--;
666        if (parentQueueIndex == queuePageSize) {
667            parentPage++;
668            parentQueueIndex = 0;
669        }
670        /* a parent to process */
671        node = *(queuePages[parentPage] + parentQueueIndex);
672        parentQueueIndex++;
673        /* get its children */
674        N = Cudd_Regular(node);
675        Nv = Cudd_T(N);
676        Nnv = Cudd_E(N);
677
678        Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
679        Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
680
681        processingDone = 2;
682        while (processingDone) {
683            /* processing the THEN and the ELSE children, the THEN
684             * child first
685             */
686            if (processingDone == 2) {
687                child = Nv;
688            } else {
689                child = Nnv;
690            }
691
692            regChild = Cudd_Regular(child);
693            /* dont process if the child is a constant */
694            if (!Cudd_IsConstant(child)) {
695                /* check is already visited, if not add a new entry in
696                 * the path Table
697                 */
698                if (!st_lookup(pathTable, regChild, &nodeStat)) {
699                    /* if not in table, has never been visited */
700                    /* create entry for table */
701                    if (nodeDistPageIndex == nodeDistPageSize)
702                        ResizeNodeDistPages();
703                    if (memOut) {
704                        for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
705                        FREE(queuePages);
706                        st_free_table(pathTable);
707                        return;
708                    }
709                    /* New entry for child in path Table is created here */
710                    nodeStat = currentNodeDistPage + nodeDistPageIndex;
711                    nodeDistPageIndex++;
712
713                    /* Initialize fields of the node data */
714                    nodeStat->oddTopDist = MAXSHORTINT;
715                    nodeStat->evenTopDist = MAXSHORTINT;
716                    nodeStat->evenBotDist = MAXSHORTINT;
717                    nodeStat->oddBotDist = MAXSHORTINT;
718                    nodeStat->regResult = NULL;
719                    nodeStat->compResult = NULL;
720                    /* update the table entry element, the distance keeps
721                     * track of the parity of the path from the root
722                     */
723                    if (Cudd_IsComplement(child)) {
724                        nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
725                    } else {
726                        nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
727                    }
728
729                    /* insert entry element for  child in the table */
730                    if (st_insert(pathTable, (char *)regChild,
731                                  (char *)nodeStat) == ST_OUT_OF_MEM) {
732                        memOut = 1;
733                        for (i = 0; i <= nodeDistPage; i++)
734                            FREE(nodeDistPages[i]);
735                        FREE(nodeDistPages);
736                        for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
737                        FREE(queuePages);
738                        st_free_table(pathTable);
739                        return;
740                    }
741
742                    /* Create list element for this child to process its children.
743                     * If this node has been processed already, then it appears
744                     * in the path table and hence is never added to the list
745                     * again.
746                     */
747
748                    if (queuePageIndex == queuePageSize) ResizeQueuePages();
749                    if (memOut) {
750                        for (i = 0; i <= nodeDistPage; i++)
751                            FREE(nodeDistPages[i]);
752                        FREE(nodeDistPages);
753                        st_free_table(pathTable);
754                        return;
755                    }
756                    *(currentQueuePage + queuePageIndex) = child;
757                    queuePageIndex++;
758
759                    childrenCount++;
760                } else {
761                    /* if not been met in a path with this parity before */
762                    /* put in list */
763                    if (((Cudd_IsComplement(child)) && (nodeStat->oddTopDist ==
764                          MAXSHORTINT)) || ((!Cudd_IsComplement(child)) &&
765                                  (nodeStat->evenTopDist == MAXSHORTINT))) {
766
767                        if (queuePageIndex == queuePageSize) ResizeQueuePages();
768                        if (memOut) {
769                            for (i = 0; i <= nodeDistPage; i++)
770                                FREE(nodeDistPages[i]);
771                            FREE(nodeDistPages);
772                            st_free_table(pathTable);
773                            return;
774
775                        }
776                        *(currentQueuePage + queuePageIndex) = child;
777                        queuePageIndex++;
778
779                        /* update the distance with the appropriate parity */
780                        if (Cudd_IsComplement(child)) {
781                            nodeStat->oddTopDist = (DdHalfWord) topLen + 1;
782                        } else {
783                            nodeStat->evenTopDist = (DdHalfWord) topLen + 1;
784                        }
785                        childrenCount++;
786                    }
787
788                } /* end of else (not found in st_table) */
789            } /*end of if Not constant child */
790            processingDone--;
791        } /*end of while processing Nv, Nnv */
792    }  /*end of while numParents */
793
794#ifdef DD_DEBUG
795    assert(queuePages[parentPage] == childPage);
796    assert(parentQueueIndex == childQueueIndex);
797#endif
798
799    if (childrenCount != 0) {
800        topLen++;
801        childPage = currentQueuePage;
802        childQueueIndex = queuePageIndex;
803        CreateTopDist(pathTable, parentPage, parentQueueIndex, topLen,
804                      childPage, childQueueIndex, childrenCount, fp);
805    }
806
807    return;
808
809} /* end of CreateTopDist */
810
811
812/**Function********************************************************************
813
814  Synopsis    [ Labels each node with the shortest distance from the constant.]
815
816  Description [Labels each node with the shortest distance from the constant.
817  This is done in a DFS search of the BDD. Each node has an odd
818  and even parity distance from the sink (since there exists paths to both
819  zero and one) which is less than MAXSHORTINT. At each node these distances
820  are updated using the minimum distance of its children from the constant.
821  SInce now both the length from the root and child is known, the minimum path
822  length(length of the shortest path between the root and the constant that
823  this node lies on) of this node can be calculated and used to update the
824  pathLengthArray]
825
826  SideEffects [Updates Path Table and path length array]
827
828  SeeAlso     [CreatePathTable CreateTopDist AssessPathLength]
829
830******************************************************************************/
831static int
832CreateBotDist(
833  DdNode * node /* current node */,
834  st_table * pathTable /* path table with path lengths */,
835  unsigned int * pathLengthArray /* array that stores number of nodes belonging to a particular path length. */,
836  FILE *fp /* where to write messages */)
837{
838    DdNode *N, *Nv, *Nnv;
839    DdNode *realChild;
840    DdNode *child, *regChild;
841    NodeDist_t *nodeStat, *nodeStatChild;
842    unsigned int  oddLen, evenLen, pathLength;
843    DdHalfWord botDist;
844    int processingDone;
845
846    if (Cudd_IsConstant(node))
847        return(1);
848    N = Cudd_Regular(node);
849    /* each node has one table entry */
850    /* update as you go down the min dist of each node from
851       the root in each (odd and even) parity */
852    if (!st_lookup(pathTable, N, &nodeStat)) {
853        fprintf(fp, "Something wrong, the entry doesn't exist\n");
854        return(0);
855    }
856
857    /* compute length of odd parity distances */
858    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
859        (nodeStat->oddBotDist != MAXSHORTINT))
860        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
861    else
862        oddLen = MAXSHORTINT;
863
864    /* compute length of even parity distances */
865    if (!((nodeStat->evenTopDist == MAXSHORTINT) ||
866          (nodeStat->evenBotDist == MAXSHORTINT)))
867        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
868    else
869        evenLen = MAXSHORTINT;
870
871    /* assign pathlength to minimum of the two */
872    pathLength = (oddLen <= evenLen) ? oddLen : evenLen;
873
874    Nv = Cudd_T(N);
875    Nnv = Cudd_E(N);
876
877    /* process each child */
878    processingDone = 0;
879    while (processingDone != 2) {
880        if (!processingDone) {
881            child = Nv;
882        } else {
883            child = Nnv;
884        }
885
886        realChild = Cudd_NotCond(child, Cudd_IsComplement(node));
887        regChild = Cudd_Regular(child);
888        if (Cudd_IsConstant(realChild)) {
889            /* Found a minterm; count parity and shortest distance
890            ** from the constant.
891            */
892            if (Cudd_IsComplement(child))
893                nodeStat->oddBotDist = 1;
894            else
895                nodeStat->evenBotDist = 1;
896        } else {
897            /* If node not in table, recur. */
898            if (!st_lookup(pathTable, regChild, &nodeStatChild)) {
899                fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n");
900                return(0);
901            }
902
903            if (nodeStatChild->oddBotDist == MAXSHORTINT) {
904                if (nodeStatChild->evenBotDist == MAXSHORTINT) {
905                    if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp))
906                        return(0);
907                } else {
908                    fprintf(fp, "Something wrong, both bot nodeStats should be there\n");
909                    return(0);
910                }
911            }
912
913            /* Update shortest distance from the constant depending on
914            **  parity. */
915
916            if (Cudd_IsComplement(child)) {
917                /* If parity on the edge then add 1 to even distance
918                ** of child to get odd parity distance and add 1 to
919                ** odd distance of child to get even parity
920                ** distance. Change distance of current node only if
921                ** the calculated distance is less than existing
922                ** distance. */
923                if (nodeStatChild->oddBotDist != MAXSHORTINT)
924                    botDist = nodeStatChild->oddBotDist + 1;
925                else
926                    botDist = MAXSHORTINT;
927                if (nodeStat->evenBotDist > botDist )
928                    nodeStat->evenBotDist = botDist;
929
930                if (nodeStatChild->evenBotDist != MAXSHORTINT)
931                    botDist = nodeStatChild->evenBotDist + 1;
932                else
933                    botDist = MAXSHORTINT;
934                if (nodeStat->oddBotDist > botDist)
935                    nodeStat->oddBotDist = botDist;
936
937            } else {
938                /* If parity on the edge then add 1 to even distance
939                ** of child to get even parity distance and add 1 to
940                ** odd distance of child to get odd parity distance.
941                ** Change distance of current node only if the
942                ** calculated distance is lesser than existing
943                ** distance. */
944                if (nodeStatChild->evenBotDist != MAXSHORTINT)
945                    botDist = nodeStatChild->evenBotDist + 1;
946                else
947                    botDist = MAXSHORTINT;
948                if (nodeStat->evenBotDist > botDist)
949                    nodeStat->evenBotDist = botDist;
950
951                if (nodeStatChild->oddBotDist != MAXSHORTINT)
952                    botDist = nodeStatChild->oddBotDist + 1;
953                else
954                    botDist = MAXSHORTINT;
955                if (nodeStat->oddBotDist > botDist)
956                    nodeStat->oddBotDist = botDist;
957            }
958        } /* end of else (if not constant child ) */
959        processingDone++;
960    } /* end of while processing Nv, Nnv */
961
962    /* Compute shortest path length on the fly. */
963    if ((nodeStat->oddTopDist != MAXSHORTINT) &&
964        (nodeStat->oddBotDist != MAXSHORTINT))
965        oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist);
966    else
967        oddLen = MAXSHORTINT;
968
969    if ((nodeStat->evenTopDist != MAXSHORTINT) &&
970        (nodeStat->evenBotDist != MAXSHORTINT))
971        evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist);
972    else
973        evenLen = MAXSHORTINT;
974
975    /* Update path length array that has number of nodes of a particular
976    ** path length. */
977    if (oddLen < pathLength ) {
978        if (pathLength != MAXSHORTINT)
979            pathLengthArray[pathLength]--;
980        if (oddLen != MAXSHORTINT)
981            pathLengthArray[oddLen]++;
982        pathLength = oddLen;
983    }
984    if (evenLen < pathLength ) {
985        if (pathLength != MAXSHORTINT)
986            pathLengthArray[pathLength]--;
987        if (evenLen != MAXSHORTINT)
988            pathLengthArray[evenLen]++;
989    }
990
991    return(1);
992
993} /*end of CreateBotDist */
994
995
996/**Function********************************************************************
997
998  Synopsis    [ The outer procedure to label each node with its shortest
999  distance from the root and constant]
1000
1001  Description [ The outer procedure to label each node with its shortest
1002  distance from the root and constant. Calls CreateTopDist and CreateBotDist.
1003  The basis for computing the distance between root and constant is that
1004  the distance may be the sum of even distances from the node to the root
1005  and constant or the sum of odd distances from the node to the root and
1006  constant.  Both CreateTopDist and CreateBotDist create the odd and
1007  even parity distances from the root and constant respectively.]
1008
1009  SideEffects [None]
1010
1011  SeeAlso     [CreateTopDist CreateBotDist]
1012
1013******************************************************************************/
1014static st_table *
1015CreatePathTable(
1016  DdNode * node /* root of function */,
1017  unsigned int * pathLengthArray /* array of path lengths to store nodes labeled with the various path lengths */,
1018  FILE *fp /* where to write messages */)
1019{
1020
1021    st_table *pathTable;
1022    NodeDist_t *nodeStat;
1023    DdHalfWord topLen;
1024    DdNode *N;
1025    int i, numParents;
1026    int insertValue;
1027    DdNode **childPage;
1028    int parentPage;
1029    int childQueueIndex, parentQueueIndex;
1030
1031    /* Creating path Table for storing data about nodes */
1032    pathTable = st_init_table(st_ptrcmp,st_ptrhash);
1033
1034    /* initializing pages for info about each node */
1035    maxNodeDistPages = INITIAL_PAGES;
1036    nodeDistPages = ALLOC(NodeDist_t *, maxNodeDistPages);
1037    if (nodeDistPages == NULL) {
1038        goto OUT_OF_MEM;
1039    }
1040    nodeDistPage = 0;
1041    currentNodeDistPage = nodeDistPages[nodeDistPage] =
1042        ALLOC(NodeDist_t, nodeDistPageSize);
1043    if (currentNodeDistPage == NULL) {
1044        for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
1045        FREE(nodeDistPages);
1046        goto OUT_OF_MEM;
1047    }
1048    nodeDistPageIndex = 0;
1049
1050    /* Initializing pages for the BFS search queue, implemented as an array. */
1051    maxQueuePages = INITIAL_PAGES;
1052    queuePages = ALLOC(DdNode **, maxQueuePages);
1053    if (queuePages == NULL) {
1054        goto OUT_OF_MEM;
1055    }
1056    queuePage = 0;
1057    currentQueuePage  = queuePages[queuePage] = ALLOC(DdNode *, queuePageSize);
1058    if (currentQueuePage == NULL) {
1059        for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
1060        FREE(queuePages);
1061        goto OUT_OF_MEM;
1062    }
1063    queuePageIndex = 0;
1064
1065    /* Enter the root node into the queue to start with. */
1066    parentPage = queuePage;
1067    parentQueueIndex = queuePageIndex;
1068    topLen = 0;
1069    *(currentQueuePage + queuePageIndex) = node;
1070    queuePageIndex++;
1071    childPage = currentQueuePage;
1072    childQueueIndex = queuePageIndex;
1073
1074    N = Cudd_Regular(node);
1075
1076    if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages();
1077    if (memOut) {
1078        for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
1079        FREE(nodeDistPages);
1080        for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
1081        FREE(queuePages);
1082        st_free_table(pathTable);
1083        goto OUT_OF_MEM;
1084    }
1085
1086    nodeStat = currentNodeDistPage + nodeDistPageIndex;
1087    nodeDistPageIndex++;
1088
1089    nodeStat->oddTopDist = MAXSHORTINT;
1090    nodeStat->evenTopDist = MAXSHORTINT;
1091    nodeStat->evenBotDist = MAXSHORTINT;
1092    nodeStat->oddBotDist = MAXSHORTINT;
1093    nodeStat->regResult = NULL;
1094    nodeStat->compResult = NULL;
1095
1096    insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat);
1097    if (insertValue == ST_OUT_OF_MEM) {
1098        memOut = 1;
1099        for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]);
1100        FREE(nodeDistPages);
1101        for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
1102        FREE(queuePages);
1103        st_free_table(pathTable);
1104        goto OUT_OF_MEM;
1105    } else if (insertValue == 1) {
1106        fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n");
1107        return(NULL);
1108    }
1109
1110    if (Cudd_IsComplement(node)) {
1111        nodeStat->oddTopDist = 0;
1112    } else {
1113        nodeStat->evenTopDist = 0;
1114    }
1115    numParents = 1;
1116    /* call the function that counts the distance of each node from the
1117     * root
1118     */
1119#ifdef DD_DEBUG
1120    numCalls = 0;
1121#endif
1122    CreateTopDist(pathTable, parentPage, parentQueueIndex, (int) topLen,
1123                  childPage, childQueueIndex, numParents, fp);
1124    if (memOut) {
1125        fprintf(fp, "Out of Memory and cant count path lengths\n");
1126        goto OUT_OF_MEM;
1127    }
1128
1129#ifdef DD_DEBUG
1130    numCalls = 0;
1131#endif
1132    /* call the function that counts the distance of each node from the
1133     * constant
1134     */
1135    if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL);
1136
1137    /* free BFS queue pages as no longer required */
1138    for (i = 0; i <= queuePage; i++) FREE(queuePages[i]);
1139    FREE(queuePages);
1140    return(pathTable);
1141
1142OUT_OF_MEM:
1143    (void) fprintf(fp, "Out of Memory, cannot allocate pages\n");
1144    memOut = 1;
1145    return(NULL);
1146
1147} /*end of CreatePathTable */
1148
1149
1150/**Function********************************************************************
1151
1152  Synopsis    [Chooses the maximum allowable path length of nodes under the
1153  threshold.]
1154
1155  Description [Chooses the maximum allowable path length under each node.
1156  The corner cases are when the threshold is larger than the number
1157  of nodes in the BDD iself, in which case 'numVars + 1' is returned.
1158  If all nodes of a particular path length are needed, then the
1159  maxpath returned is the next one with excess nodes = 0;]
1160
1161  SideEffects [None]
1162
1163  SeeAlso     []
1164
1165******************************************************************************/
1166static unsigned int
1167AssessPathLength(
1168  unsigned int * pathLengthArray /* array determining number of nodes belonging to the different path lengths */,
1169  int  threshold /* threshold to determine maximum allowable nodes in the subset */,
1170  int  numVars /* maximum number of variables */,
1171  unsigned int * excess /* number of nodes labeled maxpath required in the subset */,
1172  FILE *fp /* where to write messages */)
1173{
1174    unsigned int i, maxpath;
1175    int temp;
1176
1177    temp = threshold;
1178    i = 0;
1179    maxpath = 0;
1180    /* quit loop if i reaches max number of variables or if temp reaches
1181     * below zero
1182     */
1183    while ((i < (unsigned) numVars+1) && (temp > 0)) {
1184        if (pathLengthArray[i] > 0) {
1185            maxpath = i;
1186            temp = temp - pathLengthArray[i];
1187        }
1188        i++;
1189    }
1190    /* if all nodes of max path are needed */
1191    if (temp >= 0) {
1192        maxpath++; /* now maxpath  becomes the next maxppath or max number
1193                      of variables */
1194        *excess = 0;
1195    } else { /* normal case when subset required is less than size of
1196                original BDD */
1197        *excess = temp + pathLengthArray[maxpath];
1198    }
1199
1200    if (maxpath == 0) {
1201        fprintf(fp, "Path Length array seems to be all zeroes, check\n");
1202    }
1203    return(maxpath);
1204
1205} /* end of AssessPathLength */
1206
1207
1208/**Function********************************************************************
1209
1210  Synopsis    [Builds the BDD with nodes labeled with path length less than or equal to maxpath]
1211
1212  Description [Builds the BDD with nodes labeled with path length
1213  under maxpath and as many nodes labeled maxpath as determined by the
1214  threshold. The procedure uses the path table to determine which nodes
1215  in the original bdd need to be retained. This procedure picks a
1216  shortest path (tie break decided by taking the child with the shortest
1217  distance to the constant) and recurs down the path till it reaches the
1218  constant. the procedure then starts building the subset upward from
1219  the constant. All nodes labeled by path lengths less than the given
1220  maxpath are used to build the subset.  However, in the case of nodes
1221  that have label equal to maxpath, as many are chosen as required by
1222  the threshold. This number is stored in the info structure in the
1223  field thresholdReached. This field is decremented whenever a node
1224  labeled maxpath is encountered and the nodes labeled maxpath are
1225  aggregated in a maxpath table. As soon as the thresholdReached count
1226  goes to 0, the shortest path from this node to the constant is found.
1227  The extraction of nodes with the above labeling is based on the fact
1228  that each node, labeled with a path length, P, has at least one child
1229  labeled P or less. So extracting all nodes labeled a given path length
1230  P ensures complete paths between the root and the constant. Extraction
1231  of a partial number of nodes with a given path length may result in
1232  incomplete paths and hence the additional number of nodes are grabbed
1233  to complete the path. Since the Bdd is built bottom-up, other nodes
1234  labeled maxpath do lie on complete paths.  The procedure may cause the
1235  subset to have a larger or smaller number of nodes than the specified
1236  threshold. The increase in the number of nodes is caused by the
1237  building of a subset and the reduction by recombination. However in
1238  most cases, the recombination overshadows the increase and the
1239  procedure returns a result with lower number of nodes than specified.
1240  The subsetNodeTable is NIL when there is no hard limit on the number
1241  of nodes. Further efforts towards keeping the subset closer to the
1242  threshold number were abandoned in favour of keeping the procedure
1243  simple and fast.]
1244
1245  SideEffects [SubsetNodeTable is changed if it is not NIL.]
1246
1247  SeeAlso     []
1248
1249******************************************************************************/
1250static DdNode *
1251BuildSubsetBdd(
1252  DdManager * dd /* DD manager */,
1253  st_table * pathTable /* path table with path lengths and computed results */,
1254  DdNode * node /* current node */,
1255  struct AssortedInfo * info /* assorted information structure */,
1256  st_table * subsetNodeTable /* table storing computed results */)
1257{
1258    DdNode *N, *Nv, *Nnv;
1259    DdNode *ThenBranch, *ElseBranch, *childBranch;
1260    DdNode *child, *regChild, *regNnv, *regNv;
1261    NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv;
1262    DdNode *neW, *topv, *regNew;
1263    char *entry;
1264    unsigned int topid;
1265    unsigned int childPathLength, oddLen, evenLen, NnvPathLength, NvPathLength;
1266    unsigned int NvBotDist, NnvBotDist;
1267    int tiebreakChild;
1268    int  processingDone, thenDone, elseDone;
1269
1270
1271#ifdef DD_DEBUG
1272    numCalls++;
1273#endif
1274    if (Cudd_IsConstant(node))
1275        return(node);
1276
1277    N = Cudd_Regular(node);
1278    /* Find node in table. */
1279    if (!st_lookup(pathTable, N, &nodeStat)) {
1280        (void) fprintf(dd->err, "Something wrong, node must be in table \n");
1281        dd->errorCode = CUDD_INTERNAL_ERROR;
1282        return(NULL);
1283    }
1284    /* If the node in the table has been visited, then return the corresponding
1285    ** Dd. Since a node can become a subset of itself, its
1286    ** complement (that is te same node reached by a different parity) will
1287    ** become a superset of the original node and result in some minterms
1288    ** that were not in the original set. Hence two different results are
1289    ** maintained, corresponding to the odd and even parities.
1290    */
1291
1292    /* If this node is reached with an odd parity, get odd parity results. */
1293    if (Cudd_IsComplement(node)) {
1294        if  (nodeStat->compResult != NULL) {
1295#ifdef DD_DEBUG
1296            hits++;
1297#endif
1298            return(nodeStat->compResult);
1299        }
1300    } else {
1301        /* if this node is reached with an even parity, get even parity
1302         * results
1303         */
1304        if (nodeStat->regResult != NULL) {
1305#ifdef DD_DEBUG
1306            hits++;
1307#endif
1308            return(nodeStat->regResult);
1309        }
1310    }
1311
1312
1313    /* get children */
1314    Nv = Cudd_T(N);
1315    Nnv = Cudd_E(N);
1316
1317    Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node));
1318    Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node));
1319
1320    /* no child processed */
1321    processingDone = 0;
1322    /* then child not processed */
1323    thenDone = 0;
1324    ThenBranch = NULL;
1325    /* else child not processed */
1326    elseDone = 0;
1327    ElseBranch = NULL;
1328    /* if then child constant, branch is the child */
1329    if (Cudd_IsConstant(Nv)) {
1330        /*shortest path found */
1331        if ((Nv == DD_ONE(dd)) && (info->findShortestPath)) {
1332            info->findShortestPath = 0;
1333        }
1334
1335        ThenBranch = Nv;
1336        cuddRef(ThenBranch);
1337        if (ThenBranch == NULL) {
1338            return(NULL);
1339        }
1340
1341        thenDone++;
1342        processingDone++;
1343        NvBotDist = MAXSHORTINT;
1344    } else {
1345        /* Derive regular child for table lookup. */
1346        regNv = Cudd_Regular(Nv);
1347        /* Get node data for shortest path length. */
1348        if (!st_lookup(pathTable, regNv, &nodeStatNv) ) {
1349            (void) fprintf(dd->err, "Something wrong, node must be in table\n");
1350            dd->errorCode = CUDD_INTERNAL_ERROR;
1351            return(NULL);
1352        }
1353        /* Derive shortest path length for child. */
1354        if ((nodeStatNv->oddTopDist != MAXSHORTINT) &&
1355            (nodeStatNv->oddBotDist != MAXSHORTINT)) {
1356            oddLen = (nodeStatNv->oddTopDist + nodeStatNv->oddBotDist);
1357        } else {
1358            oddLen = MAXSHORTINT;
1359        }
1360
1361        if ((nodeStatNv->evenTopDist != MAXSHORTINT) &&
1362            (nodeStatNv->evenBotDist != MAXSHORTINT)) {
1363            evenLen = (nodeStatNv->evenTopDist +nodeStatNv->evenBotDist);
1364        } else {
1365            evenLen = MAXSHORTINT;
1366        }
1367
1368        NvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
1369        NvBotDist = (oddLen <= evenLen) ? nodeStatNv->oddBotDist:
1370                                                   nodeStatNv->evenBotDist;
1371    }
1372    /* if else child constant, branch is the child */
1373    if (Cudd_IsConstant(Nnv)) {
1374        /*shortest path found */
1375        if ((Nnv == DD_ONE(dd)) && (info->findShortestPath)) {
1376            info->findShortestPath = 0;
1377        }
1378
1379        ElseBranch = Nnv;
1380        cuddRef(ElseBranch);
1381        if (ElseBranch == NULL) {
1382            return(NULL);
1383        }
1384
1385        elseDone++;
1386        processingDone++;
1387        NnvBotDist = MAXSHORTINT;
1388    } else {
1389        /* Derive regular child for table lookup. */
1390        regNnv = Cudd_Regular(Nnv);
1391        /* Get node data for shortest path length. */
1392        if (!st_lookup(pathTable, regNnv, &nodeStatNnv) ) {
1393            (void) fprintf(dd->err, "Something wrong, node must be in table\n");
1394            dd->errorCode = CUDD_INTERNAL_ERROR;
1395            return(NULL);
1396        }
1397        /* Derive shortest path length for child. */
1398        if ((nodeStatNnv->oddTopDist != MAXSHORTINT) &&
1399            (nodeStatNnv->oddBotDist != MAXSHORTINT)) {
1400            oddLen = (nodeStatNnv->oddTopDist + nodeStatNnv->oddBotDist);
1401        } else {
1402            oddLen = MAXSHORTINT;
1403        }
1404
1405        if ((nodeStatNnv->evenTopDist != MAXSHORTINT) &&
1406            (nodeStatNnv->evenBotDist != MAXSHORTINT)) {
1407            evenLen = (nodeStatNnv->evenTopDist +nodeStatNnv->evenBotDist);
1408        } else {
1409            evenLen = MAXSHORTINT;
1410        }
1411
1412        NnvPathLength = (oddLen <= evenLen) ? oddLen : evenLen;
1413        NnvBotDist = (oddLen <= evenLen) ? nodeStatNnv->oddBotDist :
1414                                                   nodeStatNnv->evenBotDist;
1415    }
1416
1417    tiebreakChild = (NvBotDist <= NnvBotDist) ? 1 : 0;
1418    /* while both children not processed */
1419    while (processingDone != 2) {
1420        if (!processingDone) {
1421            /* if no child processed */
1422            /* pick the child with shortest path length and record which one
1423             * picked
1424             */
1425            if ((NvPathLength < NnvPathLength) ||
1426                ((NvPathLength == NnvPathLength) && (tiebreakChild == 1))) {
1427                child = Nv;
1428                regChild = regNv;
1429                thenDone = 1;
1430                childPathLength = NvPathLength;
1431            } else {
1432                child = Nnv;
1433                regChild = regNnv;
1434                elseDone = 1;
1435                childPathLength = NnvPathLength;
1436            } /* then path length less than else path length */
1437        } else {
1438            /* if one child processed, process the other */
1439            if (thenDone) {
1440                child = Nnv;
1441                regChild = regNnv;
1442                elseDone = 1;
1443                childPathLength = NnvPathLength;
1444            } else {
1445                child = Nv;
1446                regChild = regNv;
1447                thenDone = 1;
1448                childPathLength = NvPathLength;
1449            } /* end of else pick the Then child if ELSE child processed */
1450        } /* end of else one child has been processed */
1451
1452        /* ignore (replace with constant 0) all nodes which lie on paths larger
1453         * than the maximum length of the path required
1454         */
1455        if (childPathLength > info->maxpath) {
1456            /* record nodes visited */
1457            childBranch = zero;
1458        } else {
1459            if (childPathLength < info->maxpath) {
1460                if (info->findShortestPath) {
1461                    info->findShortestPath = 0;
1462                }
1463                childBranch = BuildSubsetBdd(dd, pathTable, child, info,
1464                                             subsetNodeTable);
1465
1466            } else { /* Case: path length of node = maxpath */
1467                /* If the node labeled with maxpath is found in the
1468                ** maxpathTable, use it to build the subset BDD.  */
1469                if (st_lookup(info->maxpathTable, (char *)regChild,
1470                              (char **)&entry)) {
1471                    /* When a node that is already been chosen is hit,
1472                    ** the quest for a complete path is over.  */
1473                    if (info->findShortestPath) {
1474                        info->findShortestPath = 0;
1475                    }
1476                    childBranch = BuildSubsetBdd(dd, pathTable, child, info,
1477                                                 subsetNodeTable);
1478                } else {
1479                    /* If node is not found in the maxpathTable and
1480                    ** the threshold has been reached, then if the
1481                    ** path needs to be completed, continue. Else
1482                    ** replace the node with a zero.  */
1483                    if (info->thresholdReached <= 0) {
1484                        if (info->findShortestPath) {
1485                            if (st_insert(info->maxpathTable, (char *)regChild,
1486                                          (char *)NIL(char)) == ST_OUT_OF_MEM) {
1487                                memOut = 1;
1488                                (void) fprintf(dd->err, "OUT of memory\n");
1489                                info->thresholdReached = 0;
1490                                childBranch = zero;
1491                            } else {
1492                                info->thresholdReached--;
1493                                childBranch = BuildSubsetBdd(dd, pathTable,
1494                                                    child, info,subsetNodeTable);
1495                            }
1496                        } else { /* not find shortest path, we dont need this
1497                                    node */
1498                            childBranch = zero;
1499                        }
1500                    } else { /* Threshold hasn't been reached,
1501                             ** need the node. */
1502                        if (st_insert(info->maxpathTable, (char *)regChild,
1503                                      (char *)NIL(char)) == ST_OUT_OF_MEM) {
1504                            memOut = 1;
1505                            (void) fprintf(dd->err, "OUT of memory\n");
1506                            info->thresholdReached = 0;
1507                            childBranch = zero;
1508                        } else {
1509                            info->thresholdReached--;
1510                            if (info->thresholdReached <= 0) {
1511                                info->findShortestPath = 1;
1512                            }
1513                            childBranch = BuildSubsetBdd(dd, pathTable,
1514                                                 child, info, subsetNodeTable);
1515
1516                        } /* end of st_insert successful */
1517                    } /* end of threshold hasnt been reached yet */
1518                } /* end of else node not found in maxpath table */
1519            } /* end of if (path length of node = maxpath) */
1520        } /* end if !(childPathLength > maxpath) */
1521        if (childBranch == NULL) {
1522            /* deref other stuff incase reordering has taken place */
1523            if (ThenBranch != NULL) {
1524                Cudd_RecursiveDeref(dd, ThenBranch);
1525                ThenBranch = NULL;
1526            }
1527            if (ElseBranch != NULL) {
1528                Cudd_RecursiveDeref(dd, ElseBranch);
1529                ElseBranch = NULL;
1530            }
1531            return(NULL);
1532        }
1533
1534        cuddRef(childBranch);
1535
1536        if (child == Nv) {
1537            ThenBranch = childBranch;
1538        } else {
1539            ElseBranch = childBranch;
1540        }
1541        processingDone++;
1542
1543    } /*end of while processing Nv, Nnv */
1544
1545    info->findShortestPath = 0;
1546    topid = Cudd_NodeReadIndex(N);
1547    topv = Cudd_ReadVars(dd, topid);
1548    cuddRef(topv);
1549    neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch);
1550    if (neW != NULL) {
1551        cuddRef(neW);
1552    }
1553    Cudd_RecursiveDeref(dd, topv);
1554    Cudd_RecursiveDeref(dd, ThenBranch);
1555    Cudd_RecursiveDeref(dd, ElseBranch);
1556
1557
1558    /* Hard Limit of threshold has been imposed */
1559    if (subsetNodeTable != NIL(st_table)) {
1560        /* check if a new node is created */
1561        regNew = Cudd_Regular(neW);
1562        /* subset node table keeps all new nodes that have been created to keep
1563         * a running count of how many nodes have been built in the subset.
1564         */
1565        if (!st_lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) {
1566            if (!Cudd_IsConstant(regNew)) {
1567                if (st_insert(subsetNodeTable, (char *)regNew,
1568                              (char *)NULL) == ST_OUT_OF_MEM) {
1569                    (void) fprintf(dd->err, "Out of memory\n");
1570                    return (NULL);
1571                }
1572                if (st_count(subsetNodeTable) > info->threshold) {
1573                    info->thresholdReached = 0;
1574                }
1575            }
1576        }
1577    }
1578
1579
1580    if (neW == NULL) {
1581        return(NULL);
1582    } else {
1583        /*store computed result in regular form*/
1584        if (Cudd_IsComplement(node)) {
1585            nodeStat->compResult = neW;
1586            cuddRef(nodeStat->compResult);
1587            /* if the new node is the same as the corresponding node in the
1588             * original bdd then its complement need not be computed as it
1589             * cannot be larger than the node itself
1590             */
1591            if (neW == node) {
1592#ifdef DD_DEBUG
1593                thishit++;
1594#endif
1595                /* if a result for the node has already been computed, then
1596                 * it can only be smaller than teh node itself. hence store
1597                 * the node result in order not to break recombination
1598                 */
1599                if (nodeStat->regResult != NULL) {
1600                    Cudd_RecursiveDeref(dd, nodeStat->regResult);
1601                }
1602                nodeStat->regResult = Cudd_Not(neW);
1603                cuddRef(nodeStat->regResult);
1604            }
1605
1606        } else {
1607            nodeStat->regResult = neW;
1608            cuddRef(nodeStat->regResult);
1609            if (neW == node) {
1610#ifdef DD_DEBUG
1611                thishit++;
1612#endif
1613                if (nodeStat->compResult != NULL) {
1614                    Cudd_RecursiveDeref(dd, nodeStat->compResult);
1615                }
1616                nodeStat->compResult = Cudd_Not(neW);
1617                cuddRef(nodeStat->compResult);
1618            }
1619        }
1620
1621        cuddDeref(neW);
1622        return(neW);
1623    } /* end of else i.e. Subset != NULL */
1624} /* end of BuildSubsetBdd */
1625
1626
1627/**Function********************************************************************
1628
1629  Synopsis     [Procedure to free te result dds stored in the NodeDist pages.]
1630
1631  Description [None]
1632
1633  SideEffects [None]
1634
1635  SeeAlso     []
1636
1637******************************************************************************/
1638static enum st_retval
1639stPathTableDdFree(
1640  char * key,
1641  char * value,
1642  char * arg)
1643{
1644    NodeDist_t *nodeStat;
1645    DdManager *dd;
1646
1647    nodeStat = (NodeDist_t *)value;
1648    dd = (DdManager *)arg;
1649    if (nodeStat->regResult != NULL) {
1650        Cudd_RecursiveDeref(dd, nodeStat->regResult);
1651    }
1652    if (nodeStat->compResult != NULL) {
1653        Cudd_RecursiveDeref(dd, nodeStat->compResult);
1654    }
1655    return(ST_CONTINUE);
1656
1657} /* end of stPathTableFree */
Note: See TracBrowser for help on using the repository browser.