source: vis_dev/glu-2.3/src/cuBdd/cuddGroup.c @ 88

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

library glu 2.3

File size: 61.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.44 2009/02/21 18:24:10 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#ifdef 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#ifdef 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;
1676    unsigned int pairlev;
1677
1678    if (lazyFlag) {
1679        end_move = NULL;
1680
1681        /* Find the minimum size, and the earliest position at which it
1682        ** was achieved. */
1683        for (move = moves; move != NULL; move = move->next) {
1684            if (move->size < size) {
1685                size = move->size;
1686                end_move = move;
1687            } else if (move->size == size) {
1688                if (end_move == NULL) end_move = move;
1689            }
1690        }
1691
1692        /* Find among the moves that give minimum size the one that
1693        ** minimizes the distance from the corresponding variable. */
1694        if (moves != NULL) {
1695            diff = Cudd_ReadSize(table) + 1;
1696            index = (upFlag == 1) ?
1697                    table->invperm[moves->x] : table->invperm[moves->y];
1698            pairlev =
1699                (unsigned) table->perm[Cudd_bddReadPairIndex(table, index)];
1700
1701            for (move = moves; move != NULL; move = move->next) {
1702                if (move->size == size) {
1703                    if (upFlag == 1) {
1704                        tmp_diff = (move->x > pairlev) ?
1705                                    move->x - pairlev : pairlev - move->x;
1706                    } else {
1707                        tmp_diff = (move->y > pairlev) ?
1708                                    move->y - pairlev : pairlev - move->y;
1709                    }
1710                    if (tmp_diff < diff) {
1711                        diff = tmp_diff;
1712                        end_move = move;
1713                    }
1714                }
1715            }
1716        }
1717    } else {
1718        /* Find the minimum size. */
1719        for (move = moves; move != NULL; move = move->next) {
1720            if (move->size < size) {
1721                size = move->size;
1722            }
1723        }
1724    }
1725
1726    /* In case of lazy sifting, end_move identifies the position at
1727    ** which we want to stop.  Otherwise, we stop as soon as we meet
1728    ** the minimum size. */
1729    for (move = moves; move != NULL; move = move->next) {
1730        if (lazyFlag) {
1731            if (move == end_move) return(1);
1732        } else {
1733            if (move->size == size) return(1);
1734        }
1735        if ((table->subtables[move->x].next == move->x) &&
1736        (table->subtables[move->y].next == move->y)) {
1737            res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1738            if (!res) return(0);
1739#ifdef DD_DEBUG
1740            if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n");
1741            assert(table->subtables[move->x].next == move->x);
1742            assert(table->subtables[move->y].next == move->y);
1743#endif
1744        } else { /* Group move necessary */
1745            if (move->flags == MTR_NEWNODE) {
1746                ddDissolveGroup(table,(int)move->x,(int)move->y);
1747            } else {
1748                res = ddGroupMoveBackward(table,(int)move->x,(int)move->y);
1749                if (!res) return(0);
1750            }
1751        }
1752
1753    }
1754
1755    return(1);
1756
1757} /* end of ddGroupSiftingBackward */
1758
1759
1760/**Function********************************************************************
1761
1762  Synopsis    [Merges groups in the DD table.]
1763
1764  Description [Creates a single group from low to high and adjusts the
1765  index field of the tree node.]
1766
1767  SideEffects [None]
1768
1769******************************************************************************/
1770static void
1771ddMergeGroups(
1772  DdManager * table,
1773  MtrNode * treenode,
1774  int  low,
1775  int  high)
1776{
1777    int i;
1778    MtrNode *auxnode;
1779    int saveindex;
1780    int newindex;
1781
1782    /* Merge all variables from low to high in one group, unless
1783    ** this is the topmost group. In such a case we do not merge lest
1784    ** we lose the symmetry information. */
1785    if (treenode != table->tree) {
1786        for (i = low; i < high; i++)
1787            table->subtables[i].next = i+1;
1788        table->subtables[high].next = low;
1789    }
1790
1791    /* Adjust the index fields of the tree nodes. If a node is the
1792    ** first child of its parent, then the parent may also need adjustment. */
1793    saveindex = treenode->index;
1794    newindex = table->invperm[low];
1795    auxnode = treenode;
1796    do {
1797        auxnode->index = newindex;
1798        if (auxnode->parent == NULL ||
1799                (int) auxnode->parent->index != saveindex)
1800            break;
1801        auxnode = auxnode->parent;
1802    } while (1);
1803    return;
1804
1805} /* end of ddMergeGroups */
1806
1807
1808/**Function********************************************************************
1809
1810  Synopsis    [Dissolves a group in the DD table.]
1811
1812  Description [x and y are variables in a group to be cut in two. The cut
1813  is to pass between x and y.]
1814
1815  SideEffects [None]
1816
1817******************************************************************************/
1818static void
1819ddDissolveGroup(
1820  DdManager * table,
1821  int  x,
1822  int  y)
1823{
1824    int topx;
1825    int boty;
1826
1827    /* find top and bottom of the two groups */
1828    boty = y;
1829    while ((unsigned) boty < table->subtables[boty].next)
1830        boty = table->subtables[boty].next;
1831
1832    topx = table->subtables[boty].next;
1833
1834    table->subtables[boty].next = y;
1835    table->subtables[x].next = topx;
1836
1837    return;
1838
1839} /* end of ddDissolveGroup */
1840
1841
1842/**Function********************************************************************
1843
1844  Synopsis    [Pretends to check two variables for aggregation.]
1845
1846  Description [Pretends to check two variables for aggregation. Always
1847  returns 0.]
1848
1849  SideEffects [None]
1850
1851******************************************************************************/
1852static int
1853ddNoCheck(
1854  DdManager * table,
1855  int  x,
1856  int  y)
1857{
1858    return(0);
1859
1860} /* end of ddNoCheck */
1861
1862
1863/**Function********************************************************************
1864
1865  Synopsis    [Checks two variables for aggregation.]
1866
1867  Description [Checks two variables for aggregation. The check is based
1868  on the second difference of the number of nodes as a function of the
1869  layer. If the second difference is lower than a given threshold
1870  (typically negative) then the two variables should be aggregated.
1871  Returns 1 if the two variables pass the test; 0 otherwise.]
1872
1873  SideEffects [None]
1874
1875******************************************************************************/
1876static int
1877ddSecDiffCheck(
1878  DdManager * table,
1879  int  x,
1880  int  y)
1881{
1882    double Nx,Nx_1;
1883    double Sx;
1884    double threshold;
1885    int    xindex,yindex;
1886
1887    if (x==0) return(0);
1888
1889#ifdef DD_STATS
1890    secdiffcalls++;
1891#endif
1892    Nx = (double) table->subtables[x].keys;
1893    Nx_1 = (double) table->subtables[x-1].keys;
1894    Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);
1895
1896    threshold = table->recomb / 100.0;
1897    if (Sx < threshold) {
1898        xindex = table->invperm[x];
1899        yindex = table->invperm[y];
1900        if (cuddTestInteract(table,xindex,yindex)) {
1901#if defined(DD_DEBUG) && defined(DD_VERBOSE)
1902            (void) fprintf(table->out,
1903                           "Second difference for %d = %g Pos(%d)\n",
1904                           table->invperm[x],Sx,x);
1905#endif
1906#ifdef DD_STATS
1907            secdiff++;
1908#endif
1909            return(1);
1910        } else {
1911#ifdef DD_STATS
1912            secdiffmisfire++;
1913#endif
1914            return(0);
1915        }
1916
1917    }
1918    return(0);
1919
1920} /* end of ddSecDiffCheck */
1921
1922
1923/**Function********************************************************************
1924
1925  Synopsis    [Checks for extended symmetry of x and y.]
1926
1927  Description [Checks for extended symmetry of x and y. Returns 1 in
1928  case of extended symmetry; 0 otherwise.]
1929
1930  SideEffects [None]
1931
1932******************************************************************************/
1933static int
1934ddExtSymmCheck(
1935  DdManager * table,
1936  int  x,
1937  int  y)
1938{
1939    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
1940    DdNode *one;
1941    unsigned comple;    /* f0 is complemented */
1942    int notproj;        /* f is not a projection function */
1943    int arccount;       /* number of arcs from layer x to layer y */
1944    int TotalRefCount;  /* total reference count of layer y minus 1 */
1945    int counter;        /* number of nodes of layer x that are allowed */
1946                        /* to violate extended symmetry conditions */
1947    int arccounter;     /* number of arcs into layer y that are allowed */
1948                        /* to come from layers other than x */
1949    int i;
1950    int xindex;
1951    int yindex;
1952    int res;
1953    int slots;
1954    DdNodePtr *list;
1955    DdNode *sentinel = &(table->sentinel);
1956
1957    xindex = table->invperm[x];
1958    yindex = table->invperm[y];
1959
1960    /* If the two variables do not interact, we do not want to merge them. */
1961    if (!cuddTestInteract(table,xindex,yindex))
1962        return(0);
1963
1964#ifdef DD_DEBUG
1965    /* Checks that x and y do not contain just the projection functions.
1966    ** With the test on interaction, these test become redundant,
1967    ** because an isolated projection function does not interact with
1968    ** any other variable.
1969    */
1970    if (table->subtables[x].keys == 1) {
1971        assert(table->vars[xindex]->ref != 1);
1972    }
1973    if (table->subtables[y].keys == 1) {
1974        assert(table->vars[yindex]->ref != 1);
1975    }
1976#endif
1977
1978#ifdef DD_STATS
1979    extsymmcalls++;
1980#endif
1981
1982    arccount = 0;
1983    counter = (int) (table->subtables[x].keys *
1984              (table->symmviolation/100.0) + 0.5);
1985    one = DD_ONE(table);
1986
1987    slots = table->subtables[x].slots;
1988    list = table->subtables[x].nodelist;
1989    for (i = 0; i < slots; i++) {
1990        f = list[i];
1991        while (f != sentinel) {
1992            /* Find f1, f0, f11, f10, f01, f00. */
1993            f1 = cuddT(f);
1994            f0 = Cudd_Regular(cuddE(f));
1995            comple = Cudd_IsComplement(cuddE(f));
1996            notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
1997            if (f1->index == (unsigned) yindex) {
1998                arccount++;
1999                f11 = cuddT(f1); f10 = cuddE(f1);
2000            } else {
2001                if ((int) f0->index != yindex) {
2002                    /* If f is an isolated projection function it is
2003                    ** allowed to bypass layer y.
2004                    */
2005                    if (notproj) {
2006                        if (counter == 0)
2007                            return(0);
2008                        counter--; /* f bypasses layer y */
2009                    }
2010                }
2011                f11 = f10 = f1;
2012            }
2013            if ((int) f0->index == yindex) {
2014                arccount++;
2015                f01 = cuddT(f0); f00 = cuddE(f0);
2016            } else {
2017                f01 = f00 = f0;
2018            }
2019            if (comple) {
2020                f01 = Cudd_Not(f01);
2021                f00 = Cudd_Not(f00);
2022            }
2023
2024            /* Unless we are looking at a projection function
2025            ** without external references except the one from the
2026            ** table, we insist that f01 == f10 or f11 == f00
2027            */
2028            if (notproj) {
2029                if (f01 != f10 && f11 != f00) {
2030                    if (counter == 0)
2031                        return(0);
2032                    counter--;
2033                }
2034            }
2035
2036            f = f->next;
2037        } /* while */
2038    } /* for */
2039
2040    /* Calculate the total reference counts of y */
2041    TotalRefCount = -1; /* -1 for projection function */
2042    slots = table->subtables[y].slots;
2043    list = table->subtables[y].nodelist;
2044    for (i = 0; i < slots; i++) {
2045        f = list[i];
2046        while (f != sentinel) {
2047            TotalRefCount += f->ref;
2048            f = f->next;
2049        }
2050    }
2051
2052    arccounter = (int) (table->subtables[y].keys *
2053                 (table->arcviolation/100.0) + 0.5);
2054    res = arccount >= TotalRefCount - arccounter;
2055
2056#if defined(DD_DEBUG) && defined(DD_VERBOSE)
2057    if (res) {
2058        (void) fprintf(table->out,
2059                       "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
2060                       xindex,yindex,x,y);
2061    }
2062#endif
2063
2064#ifdef DD_STATS
2065    if (res)
2066        extsymm++;
2067#endif
2068    return(res);
2069
2070} /* end ddExtSymmCheck */
2071
2072
2073/**Function********************************************************************
2074
2075  Synopsis    [Checks for grouping of x and y.]
2076
2077  Description [Checks for grouping of x and y. Returns 1 in
2078  case of grouping; 0 otherwise. This function is used for lazy sifting.]
2079
2080  SideEffects [None]
2081
2082******************************************************************************/
2083static int
2084ddVarGroupCheck(
2085  DdManager * table,
2086  int x,
2087  int y)
2088{
2089    int xindex = table->invperm[x];
2090    int yindex = table->invperm[y];
2091
2092    if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);
2093
2094    if (Cudd_bddReadPairIndex(table, xindex) == yindex) {
2095        if (ddIsVarHandled(table, xindex) ||
2096            ddIsVarHandled(table, yindex)) {
2097            if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
2098                Cudd_bddIsVarToBeGrouped(table, yindex) ) {
2099                if (table->keys - table->isolated <= originalSize) {
2100                    return(1);
2101                }
2102            }
2103        }
2104    }
2105
2106    return(0);
2107
2108} /* end of ddVarGroupCheck */
2109
2110
2111/**Function********************************************************************
2112
2113  Synopsis    [Sets a variable to already handled.]
2114
2115  Description [Sets a variable to already handled. This function is used
2116  for lazy sifting.]
2117
2118  SideEffects [none]
2119
2120  SeeAlso     []
2121
2122******************************************************************************/
2123static int
2124ddSetVarHandled(
2125  DdManager *dd,
2126  int index)
2127{
2128    if (index >= dd->size || index < 0) return(0);
2129    dd->subtables[dd->perm[index]].varHandled = 1;
2130    return(1);
2131
2132} /* end of ddSetVarHandled */
2133
2134
2135/**Function********************************************************************
2136
2137  Synopsis    [Resets a variable to be processed.]
2138
2139  Description [Resets a variable to be processed. This function is used
2140  for lazy sifting.]
2141
2142  SideEffects [none]
2143
2144  SeeAlso     []
2145
2146******************************************************************************/
2147static int
2148ddResetVarHandled(
2149  DdManager *dd,
2150  int index)
2151{
2152    if (index >= dd->size || index < 0) return(0);
2153    dd->subtables[dd->perm[index]].varHandled = 0;
2154    return(1);
2155
2156} /* end of ddResetVarHandled */
2157
2158
2159/**Function********************************************************************
2160
2161  Synopsis    [Checks whether a variables is already handled.]
2162
2163  Description [Checks whether a variables is already handled. This
2164  function is used for lazy sifting.]
2165
2166  SideEffects [none]
2167
2168  SeeAlso     []
2169
2170******************************************************************************/
2171static int
2172ddIsVarHandled(
2173  DdManager *dd,
2174  int index)
2175{
2176    if (index >= dd->size || index < 0) return(-1);
2177    return dd->subtables[dd->perm[index]].varHandled;
2178
2179} /* end of ddIsVarHandled */
Note: See TracBrowser for help on using the repository browser.