source: vis_dev/glu-2.1/src/cuBdd/cuddGroup.c @ 11

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

src glu

File size: 62.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddGroup.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for group sifting.]
8
9  Description [External procedures included in this file:
10                <ul>
11                <li> Cudd_MakeTreeNode()
12                </ul>
13        Internal procedures included in this file:
14                <ul>
15                <li> cuddTreeSifting()
16                </ul>
17        Static procedures included in this module:
18                <ul>
19                <li> ddTreeSiftingAux()
20                <li> ddCountInternalMtrNodes()
21                <li> ddReorderChildren()
22                <li> ddFindNodeHiLo()
23                <li> ddUniqueCompareGroup()
24                <li> ddGroupSifting()
25                <li> ddCreateGroup()
26                <li> ddGroupSiftingAux()
27                <li> ddGroupSiftingUp()
28                <li> ddGroupSiftingDown()
29                <li> ddGroupMove()
30                <li> ddGroupMoveBackward()
31                <li> ddGroupSiftingBackward()
32                <li> ddMergeGroups()
33                <li> ddDissolveGroup()
34                <li> ddNoCheck()
35                <li> ddSecDiffCheck()
36                <li> ddExtSymmCheck()
37                <li> ddVarGroupCheck()
38                <li> ddSetVarHandled()
39                <li> ddResetVarHandled()
40                <li> ddIsVarHandled()
41                </ul>]
42
43  Author      [Shipra Panda, Fabio Somenzi]
44
45  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
46
47  All rights reserved.
48
49  Redistribution and use in source and binary forms, with or without
50  modification, are permitted provided that the following conditions
51  are met:
52
53  Redistributions of source code must retain the above copyright
54  notice, this list of conditions and the following disclaimer.
55
56  Redistributions in binary form must reproduce the above copyright
57  notice, this list of conditions and the following disclaimer in the
58  documentation and/or other materials provided with the distribution.
59
60  Neither the name of the University of Colorado nor the names of its
61  contributors may be used to endorse or promote products derived from
62  this software without specific prior written permission.
63
64  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
65  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
66  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
67  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
68  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
69  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
70  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
71  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
72  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
73  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
74  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
75  POSSIBILITY OF SUCH DAMAGE.]
76
77******************************************************************************/
78
79#include "util.h"
80#include "cuddInt.h"
81
82/*---------------------------------------------------------------------------*/
83/* Constant declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86/* Constants for lazy sifting */
87#define DD_NORMAL_SIFT  0
88#define DD_LAZY_SIFT    1
89
90/* Constants for sifting up and down */
91#define DD_SIFT_DOWN    0
92#define DD_SIFT_UP      1
93
94/*---------------------------------------------------------------------------*/
95/* Stucture declarations                                                     */
96/*---------------------------------------------------------------------------*/
97
98/*---------------------------------------------------------------------------*/
99/* Type declarations                                                         */
100/*---------------------------------------------------------------------------*/
101
102#ifdef __cplusplus
103extern "C" {
104#endif
105    typedef int (*DD_CHKFP)(DdManager *, int, int);
106#ifdef __cplusplus
107}
108#endif
109
110/*---------------------------------------------------------------------------*/
111/* Variable declarations                                                     */
112/*---------------------------------------------------------------------------*/
113
114#ifndef lint
115static char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.42 2004/08/13 18:04:49 fabio Exp $";
116#endif
117
118static  int     *entry;
119extern  int     ddTotalNumberSwapping;
120#ifdef DD_STATS
121extern  int     ddTotalNISwaps;
122static  int     extsymmcalls;
123static  int     extsymm;
124static  int     secdiffcalls;
125static  int     secdiff;
126static  int     secdiffmisfire;
127#endif
128#ifdef DD_DEBUG
129static  int     pr = 0; /* flag to enable printing while debugging */
130                        /* by depositing a 1 into it */
131#endif
132static unsigned int originalSize;
133
134/*---------------------------------------------------------------------------*/
135/* Macro declarations                                                        */
136/*---------------------------------------------------------------------------*/
137
138#ifdef __cplusplus
139extern "C" {
140#endif
141
142/**AutomaticStart*************************************************************/
143
144/*---------------------------------------------------------------------------*/
145/* Static function prototypes                                                */
146/*---------------------------------------------------------------------------*/
147
148static int ddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
149#ifdef DD_STATS
150static int ddCountInternalMtrNodes (DdManager *table, MtrNode *treenode);
151#endif
152static int ddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
153static void ddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper);
154static int ddUniqueCompareGroup (int *ptrX, int *ptrY);
155static int ddGroupSifting (DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag);
156static void ddCreateGroup (DdManager *table, int x, int y);
157static int ddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag);
158static int ddGroupSiftingUp (DdManager *table, int y, int xLow, DD_CHKFP checkFunction, Move **moves);
159static int ddGroupSiftingDown (DdManager *table, int x, int xHigh, DD_CHKFP checkFunction, Move **moves);
160static int ddGroupMove (DdManager *table, int x, int y, Move **moves);
161static int ddGroupMoveBackward (DdManager *table, int x, int y);
162static int ddGroupSiftingBackward (DdManager *table, Move *moves, int size, int upFlag, int lazyFlag);
163static void ddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high);
164static void ddDissolveGroup (DdManager *table, int x, int y);
165static int ddNoCheck (DdManager *table, int x, int y);
166static int ddSecDiffCheck (DdManager *table, int x, int y);
167static int ddExtSymmCheck (DdManager *table, int x, int y);
168static int ddVarGroupCheck (DdManager * table, int x, int y);
169static int ddSetVarHandled (DdManager *dd, int index);
170static int ddResetVarHandled (DdManager *dd, int index);
171static int ddIsVarHandled (DdManager *dd, int index);
172
173/**AutomaticEnd***************************************************************/
174
175#ifdef __cplusplus
176}
177#endif
178
179/*---------------------------------------------------------------------------*/
180/* Definition of exported functions                                          */
181/*---------------------------------------------------------------------------*/
182
183
184/**Function********************************************************************
185
186  Synopsis    [Creates a new variable group.]
187
188  Description [Creates a new variable group. The group starts at
189  variable and contains size variables. The parameter low is the index
190  of the first variable. If the variable already exists, its current
191  position in the order is known to the manager. If the variable does
192  not exist yet, the position is assumed to be the same as the index.
193  The group tree is created if it does not exist yet.
194  Returns a pointer to the group if successful; NULL otherwise.]
195
196  SideEffects [The variable tree is changed.]
197
198  SeeAlso     [Cudd_MakeZddTreeNode]
199
200******************************************************************************/
201MtrNode *
202Cudd_MakeTreeNode(
203  DdManager * dd /* manager */,
204  unsigned int  low /* index of the first group variable */,
205  unsigned int  size /* number of variables in the group */,
206  unsigned int  type /* MTR_DEFAULT or MTR_FIXED */)
207{
208    MtrNode *group;
209    MtrNode *tree;
210    unsigned int level;
211
212    /* If the variable does not exist yet, the position is assumed to be
213    ** the same as the index. Therefore, applications that rely on
214    ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
215    ** variables have to create the variables before they group them.
216    */
217    level = (low < (unsigned int) dd->size) ? dd->perm[low] : low;
218
219    if (level + size - 1> (int) MTR_MAXHIGH)
220        return(NULL);
221
222    /* If the tree does not exist yet, create it. */
223    tree = dd->tree;
224    if (tree == NULL) {
225        dd->tree = tree = Mtr_InitGroupTree(0, dd->size);
226        if (tree == NULL)
227            return(NULL);
228        tree->index = dd->invperm[0];
229    }
230
231    /* Extend the upper bound of the tree if necessary. This allows the
232    ** application to create groups even before the variables are created.
233    */
234    tree->size = ddMax(tree->size, ddMax(level + size, (unsigned) dd->size));
235
236    /* Create the group. */
237    group = Mtr_MakeGroup(tree, level, size, type);
238    if (group == NULL)
239        return(NULL);
240
241    /* Initialize the index field to the index of the variable currently
242    ** in position low. This field will be updated by the reordering
243    ** procedure to provide a handle to the group once it has been moved.
244    */
245    group->index = (MtrHalfWord) low;
246
247    return(group);
248
249} /* end of Cudd_MakeTreeNode */
250
251
252/*---------------------------------------------------------------------------*/
253/* Definition of internal functions                                          */
254/*---------------------------------------------------------------------------*/
255
256
257/**Function********************************************************************
258
259  Synopsis    [Tree sifting algorithm.]
260
261  Description [Tree sifting algorithm. Assumes that a tree representing
262  a group hierarchy is passed as a parameter. It then reorders each
263  group in postorder fashion by calling ddTreeSiftingAux.  Assumes that
264  no dead nodes are present.  Returns 1 if successful; 0 otherwise.]
265
266  SideEffects [None]
267
268******************************************************************************/
269int
270cuddTreeSifting(
271  DdManager * table /* DD table */,
272  Cudd_ReorderingType method /* reordering method for the groups of leaves */)
273{
274    int i;
275    int nvars;
276    int result;
277    int tempTree;
278
279    /* If no tree is provided we create a temporary one in which all
280    ** variables are in a single group. After reordering this tree is
281    ** destroyed.
282    */
283    tempTree = table->tree == NULL;
284    if (tempTree) {
285        table->tree = Mtr_InitGroupTree(0,table->size);
286        table->tree->index = table->invperm[0];
287    }
288    nvars = table->size;
289
290#ifdef DD_DEBUG
291    if (pr > 0 && !tempTree) (void) fprintf(table->out,"cuddTreeSifting:");
292    Mtr_PrintGroups(table->tree,pr <= 0);
293#endif
294
295#ifdef DD_STATS
296    extsymmcalls = 0;
297    extsymm = 0;
298    secdiffcalls = 0;
299    secdiff = 0;
300    secdiffmisfire = 0;
301
302    (void) fprintf(table->out,"\n");
303    if (!tempTree)
304        (void) fprintf(table->out,"#:IM_NODES  %8d: group tree nodes\n",
305                       ddCountInternalMtrNodes(table,table->tree));
306#endif
307
308    /* Initialize the group of each subtable to itself. Initially
309    ** there are no groups. Groups are created according to the tree
310    ** structure in postorder fashion.
311    */
312    for (i = 0; i < nvars; i++)
313        table->subtables[i].next = i;
314
315
316    /* Reorder. */
317    result = ddTreeSiftingAux(table, table->tree, method);
318
319#ifdef DD_STATS         /* print stats */
320    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
321        (table->groupcheck == CUDD_GROUP_CHECK7 ||
322         table->groupcheck == CUDD_GROUP_CHECK5)) {
323        (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
324        (void) fprintf(table->out,"extsymm = %d",extsymm);
325    }
326    if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
327        table->groupcheck == CUDD_GROUP_CHECK7) {
328        (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
329        (void) fprintf(table->out,"secdiff = %d\n",secdiff);
330        (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
331    }
332#endif
333
334    if (tempTree)
335        Cudd_FreeTree(table);
336    return(result);
337
338} /* end of cuddTreeSifting */
339
340
341/*---------------------------------------------------------------------------*/
342/* Definition of static functions                                            */
343/*---------------------------------------------------------------------------*/
344
345
346/**Function********************************************************************
347
348  Synopsis    [Visits the group tree and reorders each group.]
349
350  Description [Recursively visits the group tree and reorders each
351  group in postorder fashion.  Returns 1 if successful; 0 otherwise.]
352
353  SideEffects [None]
354
355******************************************************************************/
356static int
357ddTreeSiftingAux(
358  DdManager * table,
359  MtrNode * treenode,
360  Cudd_ReorderingType method)
361{
362    MtrNode  *auxnode;
363    int res;
364    Cudd_AggregationType saveCheck;
365
366#ifdef DD_DEBUG
367    Mtr_PrintGroups(treenode,1);
368#endif
369
370    auxnode = treenode;
371    while (auxnode != NULL) {
372        if (auxnode->child != NULL) {
373            if (!ddTreeSiftingAux(table, auxnode->child, method))
374                return(0);
375            saveCheck = table->groupcheck;
376            table->groupcheck = CUDD_NO_CHECK;
377            if (method != CUDD_REORDER_LAZY_SIFT)
378              res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
379            else
380              res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT);
381            table->groupcheck = saveCheck;
382
383            if (res == 0)
384                return(0);
385        } else if (auxnode->size > 1) {
386            if (!ddReorderChildren(table, auxnode, method))
387                return(0);
388        }
389        auxnode = auxnode->younger;
390    }
391
392    return(1);
393
394} /* end of ddTreeSiftingAux */
395
396
397#ifdef DD_STATS
398/**Function********************************************************************
399
400  Synopsis    [Counts the number of internal nodes of the group tree.]
401
402  Description [Counts the number of internal nodes of the group tree.
403  Returns the count.]
404
405  SideEffects [None]
406
407******************************************************************************/
408static int
409ddCountInternalMtrNodes(
410  DdManager * table,
411  MtrNode * treenode)
412{
413    MtrNode *auxnode;
414    int     count,nodeCount;
415
416
417    nodeCount = 0;
418    auxnode = treenode;
419    while (auxnode != NULL) {
420        if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
421            nodeCount++;
422            count = ddCountInternalMtrNodes(table,auxnode->child);
423            nodeCount += count;
424        }
425        auxnode = auxnode->younger;
426    }
427
428    return(nodeCount);
429
430} /* end of ddCountInternalMtrNodes */
431#endif
432
433
434/**Function********************************************************************
435
436  Synopsis    [Reorders the children of a group tree node according to
437  the options.]
438
439  Description [Reorders the children of a group tree node according to
440  the options. After reordering puts all the variables in the group
441  and/or its descendents in a single group. This allows hierarchical
442  reordering.  If the variables in the group do not exist yet, simply
443  does nothing. Returns 1 if successful; 0 otherwise.]
444
445  SideEffects [None]
446
447******************************************************************************/
448static int
449ddReorderChildren(
450  DdManager * table,
451  MtrNode * treenode,
452  Cudd_ReorderingType method)
453{
454    int lower;
455    int upper;
456    int result;
457    unsigned int initialSize;
458
459    ddFindNodeHiLo(table,treenode,&lower,&upper);
460    /* If upper == -1 these variables do not exist yet. */
461    if (upper == -1)
462        return(1);
463
464    if (treenode->flags == MTR_FIXED) {
465        result = 1;
466    } else {
467#ifdef DD_STATS
468        (void) fprintf(table->out," ");
469#endif
470        switch (method) {
471        case CUDD_REORDER_RANDOM:
472        case CUDD_REORDER_RANDOM_PIVOT:
473            result = cuddSwapping(table,lower,upper,method);
474            break;
475        case CUDD_REORDER_SIFT:
476            result = cuddSifting(table,lower,upper);
477            break;
478        case CUDD_REORDER_SIFT_CONVERGE:
479            do {
480                initialSize = table->keys - table->isolated;
481                result = cuddSifting(table,lower,upper);
482                if (initialSize <= table->keys - table->isolated)
483                    break;
484#ifdef DD_STATS
485                else
486                    (void) fprintf(table->out,"\n");
487#endif
488            } while (result != 0);
489            break;
490        case CUDD_REORDER_SYMM_SIFT:
491            result = cuddSymmSifting(table,lower,upper);
492            break;
493        case CUDD_REORDER_SYMM_SIFT_CONV:
494            result = cuddSymmSiftingConv(table,lower,upper);
495            break;
496        case CUDD_REORDER_GROUP_SIFT:
497            if (table->groupcheck == CUDD_NO_CHECK) {
498                result = ddGroupSifting(table,lower,upper,ddNoCheck,
499                                        DD_NORMAL_SIFT);
500            } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
501                result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
502                                        DD_NORMAL_SIFT);
503            } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
504                result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
505                                        DD_NORMAL_SIFT);
506            } else {
507                (void) fprintf(table->err,
508                               "Unknown group ckecking method\n");
509                result = 0;
510            }
511            break;
512        case CUDD_REORDER_GROUP_SIFT_CONV:
513            do {
514                initialSize = table->keys - table->isolated;
515                if (table->groupcheck == CUDD_NO_CHECK) {
516                    result = ddGroupSifting(table,lower,upper,ddNoCheck,
517                                            DD_NORMAL_SIFT);
518                } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
519                    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
520                                            DD_NORMAL_SIFT);
521                } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
522                    result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
523                                            DD_NORMAL_SIFT);
524                } else {
525                    (void) fprintf(table->err,
526                                   "Unknown group ckecking method\n");
527                    result = 0;
528                }
529#ifdef DD_STATS
530                (void) fprintf(table->out,"\n");
531#endif
532                result = cuddWindowReorder(table,lower,upper,
533                                           CUDD_REORDER_WINDOW4);
534                if (initialSize <= table->keys - table->isolated)
535                    break;
536#ifdef DD_STATS
537                else
538                    (void) fprintf(table->out,"\n");
539#endif
540            } while (result != 0);
541            break;
542        case CUDD_REORDER_WINDOW2:
543        case CUDD_REORDER_WINDOW3:
544        case CUDD_REORDER_WINDOW4:
545        case CUDD_REORDER_WINDOW2_CONV:
546        case CUDD_REORDER_WINDOW3_CONV:
547        case CUDD_REORDER_WINDOW4_CONV:
548            result = cuddWindowReorder(table,lower,upper,method);
549            break;
550        case CUDD_REORDER_ANNEALING:
551            result = cuddAnnealing(table,lower,upper);
552            break;
553        case CUDD_REORDER_GENETIC:
554            result = cuddGa(table,lower,upper);
555            break;
556        case CUDD_REORDER_LINEAR:
557            result = cuddLinearAndSifting(table,lower,upper);
558            break;
559        case CUDD_REORDER_LINEAR_CONVERGE:
560            do {
561                initialSize = table->keys - table->isolated;
562                result = cuddLinearAndSifting(table,lower,upper);
563                if (initialSize <= table->keys - table->isolated)
564                    break;
565#ifdef DD_STATS
566                else
567                    (void) fprintf(table->out,"\n");
568#endif
569            } while (result != 0);
570            break;
571        case CUDD_REORDER_EXACT:
572            result = cuddExact(table,lower,upper);
573            break;
574        case CUDD_REORDER_LAZY_SIFT:
575            result = ddGroupSifting(table,lower,upper,ddVarGroupCheck,
576                                    DD_LAZY_SIFT);
577            break;
578        default:
579            return(0);
580        }
581    }
582
583    /* Create a single group for all the variables that were sifted,
584    ** so that they will be treated as a single block by successive
585    ** invocations of ddGroupSifting.
586    */
587    ddMergeGroups(table,treenode,lower,upper);
588
589#ifdef DD_DEBUG
590    if (pr > 0) (void) fprintf(table->out,"ddReorderChildren:");
591#endif
592
593    return(result);
594
595} /* end of ddReorderChildren */
596
597
598/**Function********************************************************************
599
600  Synopsis    [Finds the lower and upper bounds of the group represented
601  by treenode.]
602
603  Description [Finds the lower and upper bounds of the group
604  represented by treenode.  From the index and size fields we need to
605  derive the current positions, and find maximum and minimum.]
606
607  SideEffects [The bounds are returned as side effects.]
608
609  SeeAlso     []
610
611******************************************************************************/
612static void
613ddFindNodeHiLo(
614  DdManager * table,
615  MtrNode * treenode,
616  int * lower,
617  int * upper)
618{
619    int low;
620    int high;
621
622    /* Check whether no variables in this group already exist.
623    ** If so, return immediately. The calling procedure will know from
624    ** the values of upper that no reordering is needed.
625    */
626    if ((int) treenode->low >= table->size) {
627        *lower = table->size;
628        *upper = -1;
629        return;
630    }
631
632    *lower = low = (unsigned int) table->perm[treenode->index];
633    high = (int) (low + treenode->size - 1);
634
635    if (high >= table->size) {
636        /* This is the case of a partially existing group. The aim is to
637        ** reorder as many variables as safely possible.  If the tree
638        ** node is terminal, we just reorder the subset of the group
639        ** that is currently in existence.  If the group has
640        ** subgroups, then we only reorder those subgroups that are
641        ** fully instantiated.  This way we avoid breaking up a group.
642        */
643        MtrNode *auxnode = treenode->child;
644        if (auxnode == NULL) {
645            *upper = (unsigned int) table->size - 1;
646        } else {
647            /* Search the subgroup that strands the table->size line.
648            ** If the first group starts at 0 and goes past table->size
649            ** upper will get -1, thus correctly signaling that no reordering
650            ** should take place.
651            */
652            while (auxnode != NULL) {
653                int thisLower = table->perm[auxnode->low];
654                int thisUpper = thisLower + auxnode->size - 1;
655                if (thisUpper >= table->size && thisLower < table->size)
656                    *upper = (unsigned int) thisLower - 1;
657                auxnode = auxnode->younger;
658            }
659        }
660    } else {
661        /* Normal case: All the variables of the group exist. */
662        *upper = (unsigned int) high;
663    }
664
665#ifdef DD_DEBUG
666    /* Make sure that all variables in group are contiguous. */
667    assert(treenode->size >= *upper - *lower + 1);
668#endif
669
670    return;
671
672} /* end of ddFindNodeHiLo */
673
674
675/**Function********************************************************************
676
677  Synopsis    [Comparison function used by qsort.]
678
679  Description [Comparison function used by qsort to order the variables
680  according to the number of keys in the subtables.  Returns the
681  difference in number of keys between the two variables being
682  compared.]
683
684  SideEffects [None]
685
686******************************************************************************/
687static int
688ddUniqueCompareGroup(
689  int * ptrX,
690  int * ptrY)
691{
692#if 0
693    if (entry[*ptrY] == entry[*ptrX]) {
694        return((*ptrX) - (*ptrY));
695    }
696#endif
697    return(entry[*ptrY] - entry[*ptrX]);
698
699} /* end of ddUniqueCompareGroup */
700
701
702/**Function********************************************************************
703
704  Synopsis    [Sifts from treenode->low to treenode->high.]
705
706  Description [Sifts from treenode->low to treenode->high. If
707  croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
708  end of the initial sifting. If a group is created, it is then sifted
709  again. After sifting one variable, the group that contains it is
710  dissolved.  Returns 1 in case of success; 0 otherwise.]
711
712  SideEffects [None]
713
714******************************************************************************/
715static int
716ddGroupSifting(
717  DdManager * table,
718  int  lower,
719  int  upper,
720  DD_CHKFP checkFunction,
721  int lazyFlag)
722{
723    int         *var;
724    int         i,j,x,xInit;
725    int         nvars;
726    int         classes;
727    int         result;
728    int         *sifted;
729    int         merged;
730    int         dissolve;
731#ifdef DD_STATS
732    unsigned    previousSize;
733#endif
734    int         xindex;
735
736    nvars = table->size;
737
738    /* Order variables to sift. */
739    entry = NULL;
740    sifted = NULL;
741    var = ALLOC(int,nvars);
742    if (var == NULL) {
743        table->errorCode = CUDD_MEMORY_OUT;
744        goto ddGroupSiftingOutOfMem;
745    }
746    entry = ALLOC(int,nvars);
747    if (entry == NULL) {
748        table->errorCode = CUDD_MEMORY_OUT;
749        goto ddGroupSiftingOutOfMem;
750    }
751    sifted = ALLOC(int,nvars);
752    if (sifted == NULL) {
753        table->errorCode = CUDD_MEMORY_OUT;
754        goto ddGroupSiftingOutOfMem;
755    }
756
757    /* Here we consider only one representative for each group. */
758    for (i = 0, classes = 0; i < nvars; i++) {
759        sifted[i] = 0;
760        x = table->perm[i];
761        if ((unsigned) x >= table->subtables[x].next) {
762            entry[i] = table->subtables[x].keys;
763            var[classes] = i;
764            classes++;
765        }
766    }
767
768    qsort((void *)var,classes,sizeof(int),
769          (DD_QSFP) ddUniqueCompareGroup);
770
771    if (lazyFlag) {
772        for (i = 0; i < nvars; i ++) {
773            ddResetVarHandled(table, i);
774        }
775    }
776
777    /* Now sift. */
778    for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
779        if (ddTotalNumberSwapping >= table->siftMaxSwap)
780            break;
781        xindex = var[i];
782        if (sifted[xindex] == 1) /* variable already sifted as part of group */
783            continue;
784        x = table->perm[xindex]; /* find current level of this variable */
785
786        if (x < lower || x > upper || table->subtables[x].bindVar == 1)
787            continue;
788#ifdef DD_STATS
789        previousSize = table->keys - table->isolated;
790#endif
791#ifdef DD_DEBUG
792        /* x is bottom of group */
793        assert((unsigned) x >= table->subtables[x].next);
794#endif
795        if ((unsigned) x == table->subtables[x].next) {
796            dissolve = 1;
797            result = ddGroupSiftingAux(table,x,lower,upper,checkFunction,
798                                        lazyFlag);
799        } else {
800            dissolve = 0;
801            result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
802        }
803        if (!result) goto ddGroupSiftingOutOfMem;
804
805        /* check for aggregation */
806        merged = 0;
807        if (lazyFlag == 0 && table->groupcheck == CUDD_GROUP_CHECK7) {
808            x = table->perm[xindex]; /* find current level */
809            if ((unsigned) x == table->subtables[x].next) { /* not part of a group */
810                if (x != upper && sifted[table->invperm[x+1]] == 0 &&
811                (unsigned) x+1 == table->subtables[x+1].next) {
812                    if (ddSecDiffCheck(table,x,x+1)) {
813                        merged =1;
814                        ddCreateGroup(table,x,x+1);
815                    }
816                }
817                if (x != lower && sifted[table->invperm[x-1]] == 0 &&
818                (unsigned) x-1 == table->subtables[x-1].next) {
819                    if (ddSecDiffCheck(table,x-1,x)) {
820                        merged =1;
821                        ddCreateGroup(table,x-1,x);
822                    }
823                }
824            }
825        }
826
827        if (merged) { /* a group was created */
828            /* move x to bottom of group */
829            while ((unsigned) x < table->subtables[x].next)
830                x = table->subtables[x].next;
831            /* sift */
832            result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
833            if (!result) goto ddGroupSiftingOutOfMem;
834#ifdef DD_STATS
835            if (table->keys < previousSize + table->isolated) {
836                (void) fprintf(table->out,"_");
837            } else if (table->keys > previousSize + table->isolated) {
838                (void) fprintf(table->out,"^");
839            } else {
840                (void) fprintf(table->out,"*");
841            }
842            fflush(table->out);
843        } else {
844            if (table->keys < previousSize + table->isolated) {
845                (void) fprintf(table->out,"-");
846            } else if (table->keys > previousSize + table->isolated) {
847                (void) fprintf(table->out,"+");
848            } else {
849                (void) fprintf(table->out,"=");
850            }
851            fflush(table->out);
852#endif
853        }
854
855        /* Mark variables in the group just sifted. */
856        x = table->perm[xindex];
857        if ((unsigned) x != table->subtables[x].next) {
858            xInit = x;
859            do {
860                j = table->invperm[x];
861                sifted[j] = 1;
862                x = table->subtables[x].next;
863            } while (x != xInit);
864
865            /* Dissolve the group if it was created. */
866            if (lazyFlag == 0 && dissolve) {
867                do {
868                    j = table->subtables[x].next;
869                    table->subtables[x].next = x;
870                    x = j;
871                } while (x != xInit);
872            }
873        }
874
875#ifdef DD_DEBUG
876        if (pr > 0) (void) fprintf(table->out,"ddGroupSifting:");
877#endif
878
879      if (lazyFlag) ddSetVarHandled(table, xindex);
880    } /* for */
881
882    FREE(sifted);
883    FREE(var);
884    FREE(entry);
885
886    return(1);
887
888ddGroupSiftingOutOfMem:
889    if (entry != NULL)  FREE(entry);
890    if (var != NULL)    FREE(var);
891    if (sifted != NULL) FREE(sifted);
892
893    return(0);
894
895} /* end of ddGroupSifting */
896
897
898/**Function********************************************************************
899
900  Synopsis    [Creates a group encompassing variables from x to y in the
901  DD table.]
902
903  Description [Creates a group encompassing variables from x to y in the
904  DD table. In the current implementation it must be y == x+1.
905  Returns 1 in case of success; 0 otherwise.]
906
907  SideEffects [None]
908
909******************************************************************************/
910static void
911ddCreateGroup(
912  DdManager * table,
913  int  x,
914  int  y)
915{
916    int  gybot;
917
918#ifdef DD_DEBUG
919    assert(y == x+1);
920#endif
921
922    /* Find bottom of second group. */
923    gybot = y;
924    while ((unsigned) gybot < table->subtables[gybot].next)
925        gybot = table->subtables[gybot].next;
926
927    /* Link groups. */
928    table->subtables[x].next = y;
929    table->subtables[gybot].next = x;
930
931    return;
932
933} /* ddCreateGroup */
934
935
936/**Function********************************************************************
937
938  Synopsis    [Sifts one variable up and down until it has taken all
939  positions. Checks for aggregation.]
940
941  Description [Sifts one variable up and down until it has taken all
942  positions. Checks for aggregation. There may be at most two sweeps,
943  even if the group grows.  Assumes that x is either an isolated
944  variable, or it is the bottom of a group. All groups may not have
945  been found. The variable being moved is returned to the best position
946  seen during sifting.  Returns 1 in case of success; 0 otherwise.]
947
948  SideEffects [None]
949
950******************************************************************************/
951static int
952ddGroupSiftingAux(
953  DdManager * table,
954  int  x,
955  int  xLow,
956  int  xHigh,
957  DD_CHKFP checkFunction,
958  int lazyFlag)
959{
960    Move *move;
961    Move *moves;        /* list of moves */
962    int  initialSize;
963    int  result;
964    int  y;
965    int  topbot;
966
967#ifdef DD_DEBUG
968    if (pr > 0) (void) fprintf(table->out,
969                               "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);
970    assert((unsigned) x >= table->subtables[x].next); /* x is bottom of group */
971#endif
972
973    initialSize = table->keys - table->isolated;
974    moves = NULL;
975
976    originalSize = initialSize;         /* for lazy sifting */
977
978    /* If we have a singleton, we check for aggregation in both
979    ** directions before we sift.
980    */
981    if ((unsigned) x == table->subtables[x].next) {
982        /* Will go down first, unless x == xHigh:
983        ** Look for aggregation above x.
984        */
985        for (y = x; y > xLow; y--) {
986            if (!checkFunction(table,y-1,y))
987                break;
988            topbot = table->subtables[y-1].next; /* find top of y-1's group */
989            table->subtables[y-1].next = y;
990            table->subtables[x].next = topbot; /* x is bottom of group so its */
991                                               /* next is top of y-1's group */
992            y = topbot + 1; /* add 1 for y--; new y is top of group */
993        }
994        /* Will go up first unless x == xlow:
995        ** Look for aggregation below x.
996        */
997        for (y = x; y < xHigh; y++) {
998            if (!checkFunction(table,y,y+1))
999                break;
1000            /* find bottom of y+1's group */
1001            topbot = y + 1;
1002            while ((unsigned) topbot < table->subtables[topbot].next) {
1003                topbot = table->subtables[topbot].next;
1004            }
1005            table->subtables[topbot].next = table->subtables[y].next;
1006            table->subtables[y].next = y + 1;
1007            y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */
1008        }
1009    }
1010
1011    /* Now x may be in the middle of a group.
1012    ** Find bottom of x's group.
1013    */
1014    while ((unsigned) x < table->subtables[x].next)
1015        x = table->subtables[x].next;
1016
1017    if (x == xLow) { /* Sift down */
1018#ifdef DD_DEBUG
1019        /* x must be a singleton */
1020        assert((unsigned) x == table->subtables[x].next);
1021#endif
1022        if (x == xHigh) return(1);      /* just one variable */
1023
1024        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1025            goto ddGroupSiftingAuxOutOfMem;
1026        /* at this point x == xHigh, unless early term */
1027
1028        /* move backward and stop at best position */
1029        result = ddGroupSiftingBackward(table,moves,initialSize,
1030                                        DD_SIFT_DOWN,lazyFlag);
1031#ifdef DD_DEBUG
1032        assert(table->keys - table->isolated <= (unsigned) initialSize);
1033#endif
1034        if (!result) goto ddGroupSiftingAuxOutOfMem;
1035
1036    } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
1037#ifdef DD_DEBUG
1038        /* x is bottom of group */
1039        assert((unsigned) x >= table->subtables[x].next);
1040#endif
1041        /* Find top of x's group */
1042        x = table->subtables[x].next;
1043
1044        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1045            goto ddGroupSiftingAuxOutOfMem;
1046        /* at this point x == xLow, unless early term */
1047
1048        /* move backward and stop at best position */
1049        result = ddGroupSiftingBackward(table,moves,initialSize,
1050                                        DD_SIFT_UP,lazyFlag);
1051#ifdef DD_DEBUG
1052        assert(table->keys - table->isolated <= (unsigned) initialSize);
1053#endif
1054        if (!result) goto ddGroupSiftingAuxOutOfMem;
1055
1056    } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
1057        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1058            goto ddGroupSiftingAuxOutOfMem;
1059        /* at this point x == xHigh, unless early term */
1060
1061        /* Find top of group */
1062        if (moves) {
1063            x = moves->y;
1064        }
1065        while ((unsigned) x < table->subtables[x].next)
1066            x = table->subtables[x].next;
1067        x = table->subtables[x].next;
1068#ifdef DD_DEBUG
1069        /* x should be the top of a group */
1070        assert((unsigned) x <= table->subtables[x].next);
1071#endif
1072
1073        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1074            goto ddGroupSiftingAuxOutOfMem;
1075
1076        /* move backward and stop at best position */
1077        result = ddGroupSiftingBackward(table,moves,initialSize,
1078                                        DD_SIFT_UP,lazyFlag);
1079#ifdef DD_DEBUG
1080        assert(table->keys - table->isolated <= (unsigned) initialSize);
1081#endif
1082        if (!result) goto ddGroupSiftingAuxOutOfMem;
1083
1084    } else { /* moving up first: shorter */
1085        /* Find top of x's group */
1086        x = table->subtables[x].next;
1087
1088        if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1089            goto ddGroupSiftingAuxOutOfMem;
1090        /* at this point x == xHigh, unless early term */
1091
1092        if (moves) {
1093            x = moves->x;
1094        }
1095        while ((unsigned) x < table->subtables[x].next)
1096            x = table->subtables[x].next;
1097#ifdef DD_DEBUG
1098        /* x is bottom of a group */
1099        assert((unsigned) x >= table->subtables[x].next);
1100#endif
1101
1102        if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1103            goto ddGroupSiftingAuxOutOfMem;
1104
1105        /* move backward and stop at best position */
1106        result = ddGroupSiftingBackward(table,moves,initialSize,
1107                                        DD_SIFT_DOWN,lazyFlag);
1108#ifdef DD_DEBUG
1109        assert(table->keys - table->isolated <= (unsigned) initialSize);
1110#endif
1111        if (!result) goto ddGroupSiftingAuxOutOfMem;
1112    }
1113
1114    while (moves != NULL) {
1115        move = moves->next;
1116        cuddDeallocMove(table, moves);
1117        moves = move;
1118    }
1119
1120    return(1);
1121
1122ddGroupSiftingAuxOutOfMem:
1123    while (moves != NULL) {
1124        move = moves->next;
1125        cuddDeallocMove(table, moves);
1126        moves = move;
1127    }
1128
1129    return(0);
1130
1131} /* end of ddGroupSiftingAux */
1132
1133
1134/**Function********************************************************************
1135
1136  Synopsis    [Sifts up a variable until either it reaches position xLow
1137  or the size of the DD heap increases too much.]
1138
1139  Description [Sifts up a variable until either it reaches position
1140  xLow or the size of the DD heap increases too much. Assumes that y is
1141  the top of a group (or a singleton).  Checks y for aggregation to the
1142  adjacent variables. Records all the moves that are appended to the
1143  list of moves received as input and returned as a side effect.
1144  Returns 1 in case of success; 0 otherwise.]
1145
1146  SideEffects [None]
1147
1148******************************************************************************/
1149static int
1150ddGroupSiftingUp(
1151  DdManager * table,
1152  int  y,
1153  int  xLow,
1154  DD_CHKFP checkFunction,
1155  Move ** moves)
1156{
1157    Move *move;
1158    int  x;
1159    int  size;
1160    int  i;
1161    int  gxtop,gybot;
1162    int  limitSize;
1163    int  xindex, yindex;
1164    int  zindex;
1165    int  z;
1166    int  isolated;
1167    int  L;     /* lower bound on DD size */
1168#ifdef DD_DEBUG
1169    int  checkL;
1170#endif
1171
1172    yindex = table->invperm[y];
1173
1174    /* Initialize the lower bound.
1175    ** The part of the DD below the bottom of y's group will not change.
1176    ** The part of the DD above y that does not interact with any
1177    ** variable of y's group will not change.
1178    ** The rest may vanish in the best case, except for
1179    ** the nodes at level xLow, which will not vanish, regardless.
1180    ** What we use here is not really a lower bound, because we ignore
1181    ** the interactions with all variables except y.
1182    */
1183    limitSize = L = table->keys - table->isolated;
1184    gybot = y;
1185    while ((unsigned) gybot < table->subtables[gybot].next)
1186        gybot = table->subtables[gybot].next;
1187    for (z = xLow + 1; z <= gybot; z++) {
1188        zindex = table->invperm[z];
1189        if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1190            isolated = table->vars[zindex]->ref == 1;
1191            L -= table->subtables[z].keys - isolated;
1192        }
1193    }
1194
1195    x = cuddNextLow(table,y);
1196    while (x >= xLow && L <= limitSize) {
1197#ifdef DD_DEBUG
1198        gybot = y;
1199        while ((unsigned) gybot < table->subtables[gybot].next)
1200            gybot = table->subtables[gybot].next;
1201        checkL = table->keys - table->isolated;
1202        for (z = xLow + 1; z <= gybot; z++) {
1203            zindex = table->invperm[z];
1204            if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1205                isolated = table->vars[zindex]->ref == 1;
1206                checkL -= table->subtables[z].keys - isolated;
1207            }
1208        }
1209        if (pr > 0 && L != checkL) {
1210            (void) fprintf(table->out,
1211                           "Inaccurate lower bound: L = %d checkL = %d\n",
1212                           L, checkL);
1213        }
1214#endif
1215        gxtop = table->subtables[x].next;
1216        if (checkFunction(table,x,y)) {
1217            /* Group found, attach groups */
1218            table->subtables[x].next = y;
1219            i = table->subtables[y].next;
1220            while (table->subtables[i].next != (unsigned) y)
1221                i = table->subtables[i].next;
1222            table->subtables[i].next = gxtop;
1223            move = (Move *)cuddDynamicAllocNode(table);
1224            if (move == NULL) goto ddGroupSiftingUpOutOfMem;
1225            move->x = x;
1226            move->y = y;
1227            move->flags = MTR_NEWNODE;
1228            move->size = table->keys - table->isolated;
1229            move->next = *moves;
1230            *moves = move;
1231        } else if (table->subtables[x].next == (unsigned) x &&
1232                   table->subtables[y].next == (unsigned) y) {
1233            /* x and y are self groups */
1234            xindex = table->invperm[x];
1235            size = cuddSwapInPlace(table,x,y);
1236#ifdef DD_DEBUG
1237            assert(table->subtables[x].next == (unsigned) x);
1238            assert(table->subtables[y].next == (unsigned) y);
1239#endif
1240            if (size == 0) goto ddGroupSiftingUpOutOfMem;
1241            /* Update the lower bound. */
1242            if (cuddTestInteract(table,xindex,yindex)) {
1243                isolated = table->vars[xindex]->ref == 1;
1244                L += table->subtables[y].keys - isolated;
1245            }
1246            move = (Move *)cuddDynamicAllocNode(table);
1247            if (move == NULL) goto ddGroupSiftingUpOutOfMem;
1248            move->x = x;
1249            move->y = y;
1250            move->flags = MTR_DEFAULT;
1251            move->size = size;
1252            move->next = *moves;
1253            *moves = move;
1254
1255#ifdef DD_DEBUG
1256            if (pr > 0) (void) fprintf(table->out,
1257                                       "ddGroupSiftingUp (2 single groups):\n");
1258#endif
1259            if ((double) size > (double) limitSize * table->maxGrowth)
1260                return(1);
1261            if (size < limitSize) limitSize = size;
1262        } else { /* Group move */
1263            size = ddGroupMove(table,x,y,moves);
1264            if (size == 0) goto ddGroupSiftingUpOutOfMem;
1265            /* Update the lower bound. */
1266            z = (*moves)->y;
1267            do {
1268                zindex = table->invperm[z];
1269                if (cuddTestInteract(table,zindex,yindex)) {
1270                    isolated = table->vars[zindex]->ref == 1;
1271                    L += table->subtables[z].keys - isolated;
1272                }
1273                z = table->subtables[z].next;
1274            } while (z != (int) (*moves)->y);
1275            if ((double) size > (double) limitSize * table->maxGrowth)
1276                return(1);
1277            if (size < limitSize) limitSize = size;
1278        }
1279        y = gxtop;
1280        x = cuddNextLow(table,y);
1281    }
1282
1283    return(1);
1284
1285ddGroupSiftingUpOutOfMem:
1286    while (*moves != NULL) {
1287        move = (*moves)->next;
1288        cuddDeallocMove(table, *moves);
1289        *moves = move;
1290    }
1291    return(0);
1292
1293} /* end of ddGroupSiftingUp */
1294
1295
1296/**Function********************************************************************
1297
1298  Synopsis    [Sifts down a variable until it reaches position xHigh.]
1299
1300  Description [Sifts down a variable until it reaches position xHigh.
1301  Assumes that x is the bottom of a group (or a singleton).  Records
1302  all the moves.  Returns 1 in case of success; 0 otherwise.]
1303
1304  SideEffects [None]
1305
1306******************************************************************************/
1307static int
1308ddGroupSiftingDown(
1309  DdManager * table,
1310  int  x,
1311  int  xHigh,
1312  DD_CHKFP checkFunction,
1313  Move ** moves)
1314{
1315    Move *move;
1316    int  y;
1317    int  size;
1318    int  limitSize;
1319    int  gxtop,gybot;
1320    int  R;     /* upper bound on node decrease */
1321    int  xindex, yindex;
1322    int  isolated, allVars;
1323    int  z;
1324    int  zindex;
1325#ifdef DD_DEBUG
1326    int  checkR;
1327#endif
1328
1329    /* If the group consists of simple variables, there is no point in
1330    ** sifting it down. This check is redundant if the projection functions
1331    ** do not have external references, because the computation of the
1332    ** lower bound takes care of the problem.  It is necessary otherwise to
1333    ** prevent the sifting down of simple variables. */
1334    y = x;
1335    allVars = 1;
1336    do {
1337        if (table->subtables[y].keys != 1) {
1338            allVars = 0;
1339            break;
1340        }
1341        y = table->subtables[y].next;
1342    } while (table->subtables[y].next != (unsigned) x);
1343    if (allVars)
1344        return(1);
1345   
1346    /* Initialize R. */
1347    xindex = table->invperm[x];
1348    gxtop = table->subtables[x].next;
1349    limitSize = size = table->keys - table->isolated;
1350    R = 0;
1351    for (z = xHigh; z > gxtop; z--) {
1352        zindex = table->invperm[z];
1353        if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1354            isolated = table->vars[zindex]->ref == 1;
1355            R += table->subtables[z].keys - isolated;
1356        }
1357    }
1358
1359    y = cuddNextHigh(table,x);
1360    while (y <= xHigh && size - R < limitSize) {
1361#ifdef DD_DEBUG
1362        gxtop = table->subtables[x].next;
1363        checkR = 0;
1364        for (z = xHigh; z > gxtop; z--) {
1365            zindex = table->invperm[z];
1366            if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1367                isolated = table->vars[zindex]->ref == 1;
1368                checkR += table->subtables[z].keys - isolated;
1369            }
1370        }
1371        assert(R >= checkR);
1372#endif
1373        /* Find bottom of y group. */
1374        gybot = table->subtables[y].next;
1375        while (table->subtables[gybot].next != (unsigned) y)
1376            gybot = table->subtables[gybot].next;
1377
1378        if (checkFunction(table,x,y)) {
1379            /* Group found: attach groups and record move. */
1380            gxtop = table->subtables[x].next;
1381            table->subtables[x].next = y;
1382            table->subtables[gybot].next = gxtop;
1383            move = (Move *)cuddDynamicAllocNode(table);
1384            if (move == NULL) goto ddGroupSiftingDownOutOfMem;
1385            move->x = x;
1386            move->y = y;
1387            move->flags = MTR_NEWNODE;
1388            move->size = table->keys - table->isolated;
1389            move->next = *moves;
1390            *moves = move;
1391        } else if (table->subtables[x].next == (unsigned) x &&
1392                   table->subtables[y].next == (unsigned) y) {
1393            /* x and y are self groups */
1394            /* Update upper bound on node decrease. */
1395            yindex = table->invperm[y];
1396            if (cuddTestInteract(table,xindex,yindex)) {
1397                isolated = table->vars[yindex]->ref == 1;
1398                R -= table->subtables[y].keys - isolated;
1399            }
1400            size = cuddSwapInPlace(table,x,y);
1401#ifdef DD_DEBUG
1402            assert(table->subtables[x].next == (unsigned) x);
1403            assert(table->subtables[y].next == (unsigned) y);
1404#endif
1405            if (size == 0) goto ddGroupSiftingDownOutOfMem;
1406
1407            /* Record move. */
1408            move = (Move *) cuddDynamicAllocNode(table);
1409            if (move == NULL) goto ddGroupSiftingDownOutOfMem;
1410            move->x = x;
1411            move->y = y;
1412            move->flags = MTR_DEFAULT;
1413            move->size = size;
1414            move->next = *moves;
1415            *moves = move;
1416
1417#ifdef DD_DEBUG
1418            if (pr > 0) (void) fprintf(table->out,
1419                                       "ddGroupSiftingDown (2 single groups):\n");
1420#endif
1421            if ((double) size > (double) limitSize * table->maxGrowth)
1422                return(1);
1423            if (size < limitSize) limitSize = size;
1424
1425            x = y;
1426            y = cuddNextHigh(table,x);
1427        } else { /* Group move */
1428            /* Update upper bound on node decrease: first phase. */
1429            gxtop = table->subtables[x].next;
1430            z = gxtop + 1;
1431            do {
1432                zindex = table->invperm[z];
1433                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1434                    isolated = table->vars[zindex]->ref == 1;
1435                    R -= table->subtables[z].keys - isolated;
1436                }
1437                z++;
1438            } while (z <= gybot);
1439            size = ddGroupMove(table,x,y,moves);
1440            if (size == 0) goto ddGroupSiftingDownOutOfMem;
1441            if ((double) size > (double) limitSize * table->maxGrowth)
1442                return(1);
1443            if (size < limitSize) limitSize = size;
1444
1445            /* Update upper bound on node decrease: second phase. */
1446            gxtop = table->subtables[gybot].next;
1447            for (z = gxtop + 1; z <= gybot; z++) {
1448                zindex = table->invperm[z];
1449                if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1450                    isolated = table->vars[zindex]->ref == 1;
1451                    R += table->subtables[z].keys - isolated;
1452                }
1453            }
1454        }
1455        x = gybot;
1456        y = cuddNextHigh(table,x);
1457    }
1458
1459    return(1);
1460
1461ddGroupSiftingDownOutOfMem:
1462    while (*moves != NULL) {
1463        move = (*moves)->next;
1464        cuddDeallocMove(table, *moves);
1465        *moves = move;
1466    }
1467
1468    return(0);
1469
1470} /* end of ddGroupSiftingDown */
1471
1472
1473/**Function********************************************************************
1474
1475  Synopsis    [Swaps two groups and records the move.]
1476
1477  Description [Swaps two groups and records the move. Returns the
1478  number of keys in the DD table in case of success; 0 otherwise.]
1479
1480  SideEffects [None]
1481
1482******************************************************************************/
1483static int
1484ddGroupMove(
1485  DdManager * table,
1486  int  x,
1487  int  y,
1488  Move ** moves)
1489{
1490    Move *move;
1491    int  size;
1492    int  i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1493    int  swapx,swapy;
1494#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1495    int  initialSize,bestSize;
1496#endif
1497
1498#if DD_DEBUG
1499    /* We assume that x < y */
1500    assert(x < y);
1501#endif
1502    /* Find top, bottom, and size for the two groups. */
1503    xbot = x;
1504    xtop = table->subtables[x].next;
1505    xsize = xbot - xtop + 1;
1506    ybot = y;
1507    while ((unsigned) ybot < table->subtables[ybot].next)
1508        ybot = table->subtables[ybot].next;
1509    ytop = y;
1510    ysize = ybot - ytop + 1;
1511
1512#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1513    initialSize = bestSize = table->keys - table->isolated;
1514#endif
1515    /* Sift the variables of the second group up through the first group */
1516    for (i = 1; i <= ysize; i++) {
1517        for (j = 1; j <= xsize; j++) {
1518            size = cuddSwapInPlace(table,x,y);
1519            if (size == 0) goto ddGroupMoveOutOfMem;
1520#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1521            if (size < bestSize)
1522                bestSize = size;
1523#endif
1524            swapx = x; swapy = y;
1525            y = x;
1526            x = cuddNextLow(table,y);
1527        }
1528        y = ytop + i;
1529        x = cuddNextLow(table,y);
1530    }
1531#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1532    if ((bestSize < initialSize) && (bestSize < size))
1533        (void) fprintf(table->out,"Missed local minimum: initialSize:%d  bestSize:%d  finalSize:%d\n",initialSize,bestSize,size);
1534#endif
1535
1536    /* fix groups */
1537    y = xtop; /* ytop is now where xtop used to be */
1538    for (i = 0; i < ysize - 1; i++) {
1539        table->subtables[y].next = cuddNextHigh(table,y);
1540        y = cuddNextHigh(table,y);
1541    }
1542    table->subtables[y].next = xtop; /* y is bottom of its group, join */
1543                                    /* it to top of its group */
1544    x = cuddNextHigh(table,y);
1545    newxtop = x;
1546    for (i = 0; i < xsize - 1; i++) {
1547        table->subtables[x].next = cuddNextHigh(table,x);
1548        x = cuddNextHigh(table,x);
1549    }
1550    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1551                                    /* it to top of its group */
1552#ifdef DD_DEBUG
1553    if (pr > 0) (void) fprintf(table->out,"ddGroupMove:\n");
1554#endif
1555
1556    /* Store group move */
1557    move = (Move *) cuddDynamicAllocNode(table);
1558    if (move == NULL) goto ddGroupMoveOutOfMem;
1559    move->x = swapx;
1560    move->y = swapy;
1561    move->flags = MTR_DEFAULT;
1562    move->size = table->keys - table->isolated;
1563    move->next = *moves;
1564    *moves = move;
1565
1566    return(table->keys - table->isolated);
1567
1568ddGroupMoveOutOfMem:
1569    while (*moves != NULL) {
1570        move = (*moves)->next;
1571        cuddDeallocMove(table, *moves);
1572        *moves = move;
1573    }
1574    return(0);
1575
1576} /* end of ddGroupMove */
1577
1578
1579/**Function********************************************************************
1580
1581  Synopsis    [Undoes the swap two groups.]
1582
1583  Description [Undoes the swap two groups.  Returns 1 in case of
1584  success; 0 otherwise.]
1585
1586  SideEffects [None]
1587
1588******************************************************************************/
1589static int
1590ddGroupMoveBackward(
1591  DdManager * table,
1592  int  x,
1593  int  y)
1594{
1595    int size;
1596    int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1597
1598
1599#if DD_DEBUG
1600    /* We assume that x < y */
1601    assert(x < y);
1602#endif
1603
1604    /* Find top, bottom, and size for the two groups. */
1605    xbot = x;
1606    xtop = table->subtables[x].next;
1607    xsize = xbot - xtop + 1;
1608    ybot = y;
1609    while ((unsigned) ybot < table->subtables[ybot].next)
1610        ybot = table->subtables[ybot].next;
1611    ytop = y;
1612    ysize = ybot - ytop + 1;
1613
1614    /* Sift the variables of the second group up through the first group */
1615    for (i = 1; i <= ysize; i++) {
1616        for (j = 1; j <= xsize; j++) {
1617            size = cuddSwapInPlace(table,x,y);
1618            if (size == 0)
1619                return(0);
1620            y = x;
1621            x = cuddNextLow(table,y);
1622        }
1623        y = ytop + i;
1624        x = cuddNextLow(table,y);
1625    }
1626
1627    /* fix groups */
1628    y = xtop;
1629    for (i = 0; i < ysize - 1; i++) {
1630        table->subtables[y].next = cuddNextHigh(table,y);
1631        y = cuddNextHigh(table,y);
1632    }
1633    table->subtables[y].next = xtop; /* y is bottom of its group, join */
1634                                    /* to its top */
1635    x = cuddNextHigh(table,y);
1636    newxtop = x;
1637    for (i = 0; i < xsize - 1; i++) {
1638        table->subtables[x].next = cuddNextHigh(table,x);
1639        x = cuddNextHigh(table,x);
1640    }
1641    table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1642                                    /* to its top */
1643#ifdef DD_DEBUG
1644    if (pr > 0) (void) fprintf(table->out,"ddGroupMoveBackward:\n");
1645#endif
1646
1647    return(1);
1648
1649} /* end of ddGroupMoveBackward */
1650
1651
1652/**Function********************************************************************
1653
1654  Synopsis    [Determines the best position for a variables and returns
1655  it there.]
1656
1657  Description [Determines the best position for a variables and returns
1658  it there.  Returns 1 in case of success; 0 otherwise.]
1659
1660  SideEffects [None]
1661
1662******************************************************************************/
1663static int
1664ddGroupSiftingBackward(
1665  DdManager * table,
1666  Move * moves,
1667  int  size,
1668  int  upFlag, 
1669  int  lazyFlag)
1670{
1671    Move *move;
1672    int  res;
1673    Move *end_move;
1674    int diff, tmp_diff;
1675    int index, pairlev;
1676
1677    if (lazyFlag) {
1678        end_move = NULL;
1679
1680        /* Find the minimum size, and the earliest position at which it
1681        ** was achieved. */
1682        for (move = moves; move != NULL; move = move->next) {
1683            if (move->size < size) {
1684                size = move->size;
1685                end_move = move;
1686            } else if (move->size == size) {
1687                if (end_move == NULL) end_move = move;
1688            } 
1689        }
1690
1691        /* Find among the moves that give minimum size the one that
1692        ** minimizes the distance from the corresponding variable. */
1693        if (moves != NULL) {
1694            diff = Cudd_ReadSize(table) + 1;
1695            index = (upFlag == 1) ? 
1696                    table->invperm[moves->x] : table->invperm[moves->y];
1697            pairlev = table->perm[Cudd_bddReadPairIndex(table, index)];
1698
1699            for (move = moves; move != NULL; move = move->next) {
1700                if (move->size == size) {
1701                    if (upFlag == 1) {
1702                        tmp_diff = (move->x > pairlev) ? 
1703                                    move->x - pairlev : pairlev - move->x;
1704                    } else {
1705                        tmp_diff = (move->y > pairlev) ?
1706                                    move->y - pairlev : pairlev - move->y;
1707                    }
1708                    if (tmp_diff < diff) {
1709                        diff = tmp_diff;
1710                        end_move = move;
1711                    } 
1712                }
1713            }
1714        }
1715    } else {
1716        /* Find the minimum size. */
1717        for (move = moves; move != NULL; move = move->next) {
1718            if (move->size < size) {
1719                size = move->size;
1720            } 
1721        }
1722    }
1723
1724    /* In case of lazy sifting, end_move identifies the position at
1725    ** which we want to stop.  Otherwise, we stop as soon as we meet
1726    ** the minimum size. */
1727    for (move = moves; move != NULL; move = move->next) {
1728        if (lazyFlag) {
1729            if (move == end_move) return(1);
1730        } else {
1731            if (move->size == size) return(1);
1732        }
1733        if ((table->subtables[move->x].next == move->x) &&
1734        (table->subtables[move->y].next == move->y)) {
1735            res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1736            if (!res) return(0);
1737#ifdef DD_DEBUG
1738            if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n");
1739            assert(table->subtables[move->x].next == move->x);
1740            assert(table->subtables[move->y].next == move->y);
1741#endif
1742        } else { /* Group move necessary */
1743            if (move->flags == MTR_NEWNODE) {
1744                ddDissolveGroup(table,(int)move->x,(int)move->y);
1745            } else {
1746                res = ddGroupMoveBackward(table,(int)move->x,(int)move->y);
1747                if (!res) return(0);
1748            }
1749        }
1750
1751    }
1752
1753    return(1);
1754
1755} /* end of ddGroupSiftingBackward */
1756
1757
1758/**Function********************************************************************
1759
1760  Synopsis    [Merges groups in the DD table.]
1761
1762  Description [Creates a single group from low to high and adjusts the
1763  index field of the tree node.]
1764
1765  SideEffects [None]
1766
1767******************************************************************************/
1768static void
1769ddMergeGroups(
1770  DdManager * table,
1771  MtrNode * treenode,
1772  int  low,
1773  int  high)
1774{
1775    int i;
1776    MtrNode *auxnode;
1777    int saveindex;
1778    int newindex;
1779
1780    /* Merge all variables from low to high in one group, unless
1781    ** this is the topmost group. In such a case we do not merge lest
1782    ** we lose the symmetry information. */
1783    if (treenode != table->tree) {
1784        for (i = low; i < high; i++)
1785            table->subtables[i].next = i+1;
1786        table->subtables[high].next = low;
1787    }
1788
1789    /* Adjust the index fields of the tree nodes. If a node is the
1790    ** first child of its parent, then the parent may also need adjustment. */
1791    saveindex = treenode->index;
1792    newindex = table->invperm[low];
1793    auxnode = treenode;
1794    do {
1795        auxnode->index = newindex;
1796        if (auxnode->parent == NULL ||
1797                (int) auxnode->parent->index != saveindex)
1798            break;
1799        auxnode = auxnode->parent;
1800    } while (1);
1801    return;
1802
1803} /* end of ddMergeGroups */
1804
1805
1806/**Function********************************************************************
1807
1808  Synopsis    [Dissolves a group in the DD table.]
1809
1810  Description [x and y are variables in a group to be cut in two. The cut
1811  is to pass between x and y.]
1812
1813  SideEffects [None]
1814
1815******************************************************************************/
1816static void
1817ddDissolveGroup(
1818  DdManager * table,
1819  int  x,
1820  int  y)
1821{
1822    int topx;
1823    int boty;
1824
1825    /* find top and bottom of the two groups */
1826    boty = y;
1827    while ((unsigned) boty < table->subtables[boty].next)
1828        boty = table->subtables[boty].next;
1829   
1830    topx = table->subtables[boty].next;
1831
1832    table->subtables[boty].next = y;
1833    table->subtables[x].next = topx;
1834
1835    return;
1836
1837} /* end of ddDissolveGroup */
1838
1839
1840/**Function********************************************************************
1841
1842  Synopsis    [Pretends to check two variables for aggregation.]
1843
1844  Description [Pretends to check two variables for aggregation. Always
1845  returns 0.]
1846
1847  SideEffects [None]
1848
1849******************************************************************************/
1850static int
1851ddNoCheck(
1852  DdManager * table,
1853  int  x,
1854  int  y)
1855{
1856    return(0);
1857
1858} /* end of ddNoCheck */
1859
1860
1861/**Function********************************************************************
1862
1863  Synopsis    [Checks two variables for aggregation.]
1864
1865  Description [Checks two variables for aggregation. The check is based
1866  on the second difference of the number of nodes as a function of the
1867  layer. If the second difference is lower than a given threshold
1868  (typically negative) then the two variables should be aggregated.
1869  Returns 1 if the two variables pass the test; 0 otherwise.]
1870
1871  SideEffects [None]
1872
1873******************************************************************************/
1874static int
1875ddSecDiffCheck(
1876  DdManager * table,
1877  int  x,
1878  int  y)
1879{
1880    double Nx,Nx_1;
1881    double Sx;
1882    double threshold;
1883    int    xindex,yindex;
1884
1885    if (x==0) return(0);
1886
1887#ifdef DD_STATS
1888    secdiffcalls++;
1889#endif
1890    Nx = (double) table->subtables[x].keys;
1891    Nx_1 = (double) table->subtables[x-1].keys;
1892    Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);
1893
1894    threshold = table->recomb / 100.0;
1895    if (Sx < threshold) {
1896        xindex = table->invperm[x];
1897        yindex = table->invperm[y];
1898        if (cuddTestInteract(table,xindex,yindex)) {
1899#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1900            (void) fprintf(table->out,
1901                           "Second difference for %d = %g Pos(%d)\n",
1902                           table->invperm[x],Sx,x);
1903#endif
1904#ifdef DD_STATS
1905            secdiff++;
1906#endif
1907            return(1);
1908        } else {
1909#ifdef DD_STATS
1910            secdiffmisfire++;
1911#endif
1912            return(0);
1913        }
1914
1915    }
1916    return(0);
1917
1918} /* end of ddSecDiffCheck */
1919
1920
1921/**Function********************************************************************
1922
1923  Synopsis    [Checks for extended symmetry of x and y.]
1924
1925  Description [Checks for extended symmetry of x and y. Returns 1 in
1926  case of extended symmetry; 0 otherwise.]
1927
1928  SideEffects [None]
1929
1930******************************************************************************/
1931static int
1932ddExtSymmCheck(
1933  DdManager * table,
1934  int  x,
1935  int  y)
1936{
1937    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
1938    DdNode *one;
1939    int comple;         /* f0 is complemented */
1940    int notproj;        /* f is not a projection function */
1941    int arccount;       /* number of arcs from layer x to layer y */
1942    int TotalRefCount;  /* total reference count of layer y minus 1 */
1943    int counter;        /* number of nodes of layer x that are allowed */
1944                        /* to violate extended symmetry conditions */
1945    int arccounter;     /* number of arcs into layer y that are allowed */
1946                        /* to come from layers other than x */
1947    int i;
1948    int xindex;
1949    int yindex;
1950    int res;
1951    int slots;
1952    DdNodePtr *list;
1953    DdNode *sentinel = &(table->sentinel);
1954
1955    xindex = table->invperm[x];
1956    yindex = table->invperm[y];
1957
1958    /* If the two variables do not interact, we do not want to merge them. */
1959    if (!cuddTestInteract(table,xindex,yindex))
1960        return(0);
1961
1962#ifdef DD_DEBUG
1963    /* Checks that x and y do not contain just the projection functions.
1964    ** With the test on interaction, these test become redundant,
1965    ** because an isolated projection function does not interact with
1966    ** any other variable.
1967    */
1968    if (table->subtables[x].keys == 1) {
1969        assert(table->vars[xindex]->ref != 1);
1970    }
1971    if (table->subtables[y].keys == 1) {
1972        assert(table->vars[yindex]->ref != 1);
1973    }
1974#endif
1975
1976#ifdef DD_STATS
1977    extsymmcalls++;
1978#endif
1979
1980    arccount = 0;
1981    counter = (int) (table->subtables[x].keys *
1982              (table->symmviolation/100.0) + 0.5);
1983    one = DD_ONE(table);
1984
1985    slots = table->subtables[x].slots;
1986    list = table->subtables[x].nodelist;
1987    for (i = 0; i < slots; i++) {
1988        f = list[i];
1989        while (f != sentinel) {
1990            /* Find f1, f0, f11, f10, f01, f00. */
1991            f1 = cuddT(f);
1992            f0 = Cudd_Regular(cuddE(f));
1993            comple = Cudd_IsComplement(cuddE(f));
1994            notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
1995            if (f1->index == yindex) {
1996                arccount++;
1997                f11 = cuddT(f1); f10 = cuddE(f1);
1998            } else {
1999                if ((int) f0->index != yindex) {
2000                    /* If f is an isolated projection function it is
2001                    ** allowed to bypass layer y.
2002                    */
2003                    if (notproj) {
2004                        if (counter == 0)
2005                            return(0);
2006                        counter--; /* f bypasses layer y */
2007                    }
2008                }
2009                f11 = f10 = f1;
2010            }
2011            if ((int) f0->index == yindex) {
2012                arccount++;
2013                f01 = cuddT(f0); f00 = cuddE(f0);
2014            } else {
2015                f01 = f00 = f0;
2016            }
2017            if (comple) {
2018                f01 = Cudd_Not(f01);
2019                f00 = Cudd_Not(f00);
2020            }
2021
2022            /* Unless we are looking at a projection function
2023            ** without external references except the one from the
2024            ** table, we insist that f01 == f10 or f11 == f00
2025            */
2026            if (notproj) {
2027                if (f01 != f10 && f11 != f00) {
2028                    if (counter == 0)
2029                        return(0);
2030                    counter--;
2031                }
2032            }
2033
2034            f = f->next;
2035        } /* while */
2036    } /* for */
2037
2038    /* Calculate the total reference counts of y */
2039    TotalRefCount = -1; /* -1 for projection function */
2040    slots = table->subtables[y].slots;
2041    list = table->subtables[y].nodelist;
2042    for (i = 0; i < slots; i++) {
2043        f = list[i];
2044        while (f != sentinel) {
2045            TotalRefCount += f->ref;
2046            f = f->next;
2047        }
2048    }
2049
2050    arccounter = (int) (table->subtables[y].keys *
2051                 (table->arcviolation/100.0) + 0.5);
2052    res = arccount >= TotalRefCount - arccounter;
2053
2054#if defined(DD_DEBUG) && defined(DD_VERBOSE)
2055    if (res) {
2056        (void) fprintf(table->out,
2057                       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
2058                       xindex,yindex,x,y);
2059    }
2060#endif
2061
2062#ifdef DD_STATS
2063    if (res)
2064        extsymm++;
2065#endif
2066    return(res);
2067
2068} /* end ddExtSymmCheck */
2069
2070
2071/**Function********************************************************************
2072
2073  Synopsis    [Checks for grouping of x and y.]
2074
2075  Description [Checks for grouping of x and y. Returns 1 in
2076  case of grouping; 0 otherwise. This function is used for lazy sifting.]
2077
2078  SideEffects [None]
2079
2080******************************************************************************/
2081static int
2082ddVarGroupCheck(
2083  DdManager * table,
2084  int x,
2085  int y)
2086{
2087    int xindex = table->invperm[x];
2088    int yindex = table->invperm[y];
2089
2090    if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);
2091
2092    if (Cudd_bddReadPairIndex(table, xindex) == yindex) {
2093        if (ddIsVarHandled(table, xindex) ||
2094            ddIsVarHandled(table, yindex)) {
2095            if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
2096                Cudd_bddIsVarToBeGrouped(table, yindex) ) {
2097                if (table->keys - table->isolated <= originalSize) {
2098                    return(1);
2099                }
2100            }
2101        }
2102    }
2103
2104    return(0);
2105
2106} /* end of ddVarGroupCheck */
2107
2108
2109/**Function********************************************************************
2110
2111  Synopsis    [Sets a variable to already handled.]
2112
2113  Description [Sets a variable to already handled. This function is used
2114  for lazy sifting.]
2115
2116  SideEffects [none]
2117
2118  SeeAlso     []
2119
2120******************************************************************************/
2121static int
2122ddSetVarHandled(
2123  DdManager *dd,
2124  int index)
2125{
2126    if (index >= dd->size || index < 0) return(0);
2127    dd->subtables[dd->perm[index]].varHandled = 1;
2128    return(1);
2129
2130} /* end of ddSetVarHandled */
2131
2132
2133/**Function********************************************************************
2134
2135  Synopsis    [Resets a variable to be processed.]
2136
2137  Description [Resets a variable to be processed. This function is used
2138  for lazy sifting.]
2139
2140  SideEffects [none]
2141
2142  SeeAlso     []
2143
2144******************************************************************************/
2145static int
2146ddResetVarHandled(
2147  DdManager *dd,
2148  int index)
2149{
2150    if (index >= dd->size || index < 0) return(0);
2151    dd->subtables[dd->perm[index]].varHandled = 0;
2152    return(1);
2153
2154} /* end of ddResetVarHandled */
2155
2156
2157/**Function********************************************************************
2158
2159  Synopsis    [Checks whether a variables is already handled.]
2160
2161  Description [Checks whether a variables is already handled. This
2162  function is used for lazy sifting.]
2163
2164  SideEffects [none]
2165
2166  SeeAlso     []
2167
2168******************************************************************************/
2169static int
2170ddIsVarHandled(
2171  DdManager *dd,
2172  int index)
2173{
2174    if (index >= dd->size || index < 0) return(-1);
2175    return dd->subtables[dd->perm[index]].varHandled;
2176
2177} /* end of ddIsVarHandled */
Note: See TracBrowser for help on using the repository browser.