source: vis_dev/glu-2.3/src/cuBdd/cuddZddLin.c @ 15

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

library glu 2.3
File size: 27.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddZddLin.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Procedures for dynamic variable ordering of ZDDs.]
8
9  Description [Internal procedures included in this module:
10                    <ul>
11                    <li> cuddZddLinearSifting()
12                    </ul>
13               Static procedures included in this module:
14                    <ul>
15                    <li> cuddZddLinearInPlace()
16                    <li> cuddZddLinerAux()
17                    <li> cuddZddLinearUp()
18                    <li> cuddZddLinearDown()
19                    <li> cuddZddLinearBackward()
20                    <li> cuddZddUndoMoves()
21                    </ul>
22              ]
23
24  SeeAlso     [cuddLinear.c cuddZddReord.c]
25
26  Author      [Fabio Somenzi]
27
28  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
29
30  All rights reserved.
31
32  Redistribution and use in source and binary forms, with or without
33  modification, are permitted provided that the following conditions
34  are met:
35
36  Redistributions of source code must retain the above copyright
37  notice, this list of conditions and the following disclaimer.
38
39  Redistributions in binary form must reproduce the above copyright
40  notice, this list of conditions and the following disclaimer in the
41  documentation and/or other materials provided with the distribution.
42
43  Neither the name of the University of Colorado nor the names of its
44  contributors may be used to endorse or promote products derived from
45  this software without specific prior written permission.
46
47  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
48  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
49  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
50  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
51  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
52  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
53  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
54  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
55  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
56  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
57  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
58  POSSIBILITY OF SUCH DAMAGE.]
59
60******************************************************************************/
61
62#include "util.h"
63#include "cuddInt.h"
64
65/*---------------------------------------------------------------------------*/
66/* Constant declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69#define CUDD_SWAP_MOVE 0
70#define CUDD_LINEAR_TRANSFORM_MOVE 1
71#define CUDD_INVERSE_TRANSFORM_MOVE 2
72
73/*---------------------------------------------------------------------------*/
74/* Stucture declarations                                                     */
75/*---------------------------------------------------------------------------*/
76
77
78/*---------------------------------------------------------------------------*/
79/* Type declarations                                                         */
80/*---------------------------------------------------------------------------*/
81
82
83/*---------------------------------------------------------------------------*/
84/* Variable declarations                                                     */
85/*---------------------------------------------------------------------------*/
86
87#ifndef lint
88static char rcsid[] DD_UNUSED = "$Id: cuddZddLin.c,v 1.14 2004/08/13 18:04:53 fabio Exp $";
89#endif
90
91extern  int     *zdd_entry;
92extern  int     zddTotalNumberSwapping;
93static  int     zddTotalNumberLinearTr;
94static  DdNode  *empty;
95
96
97/*---------------------------------------------------------------------------*/
98/* Macro declarations                                                        */
99/*---------------------------------------------------------------------------*/
100
101
102/**AutomaticStart*************************************************************/
103
104/*---------------------------------------------------------------------------*/
105/* Static function prototypes                                                */
106/*---------------------------------------------------------------------------*/
107
108static int cuddZddLinearInPlace (DdManager * table, int x, int y);
109static int cuddZddLinearAux (DdManager *table, int x, int xLow, int xHigh);
110static Move * cuddZddLinearUp (DdManager *table, int y, int xLow, Move *prevMoves);
111static Move * cuddZddLinearDown (DdManager *table, int x, int xHigh, Move *prevMoves);
112static int cuddZddLinearBackward (DdManager *table, int size, Move *moves);
113static Move* cuddZddUndoMoves (DdManager *table, Move *moves);
114
115/**AutomaticEnd***************************************************************/
116
117
118/*---------------------------------------------------------------------------*/
119/* Definition of exported functions                                          */
120/*---------------------------------------------------------------------------*/
121
122
123/*---------------------------------------------------------------------------*/
124/* Definition of internal functions                                          */
125/*---------------------------------------------------------------------------*/
126
127
128
129
130/**Function********************************************************************
131
132  Synopsis    [Implementation of the linear sifting algorithm for ZDDs.]
133
134  Description [Implementation of the linear sifting algorithm for ZDDs.
135  Assumes that no dead nodes are present.
136    <ol>
137    <li> Order all the variables according to the number of entries
138    in each unique table.
139    <li> Sift the variable up and down and applies the XOR transformation,
140    remembering each time the total size of the DD heap.
141    <li> Select the best permutation.
142    <li> Repeat 3 and 4 for all variables.
143    </ol>
144  Returns 1 if successful; 0 otherwise.]
145
146  SideEffects [None]
147
148  SeeAlso     []
149
150******************************************************************************/
151int
152cuddZddLinearSifting(
153  DdManager * table,
154  int  lower,
155  int  upper)
156{
157    int i;
158    int *var;
159    int size;
160    int x;
161    int result;
162#ifdef DD_STATS
163    int previousSize;
164#endif
165
166    size = table->sizeZ;
167    empty = table->zero;
168
169    /* Find order in which to sift variables. */
170    var = NULL;
171    zdd_entry = ALLOC(int, size);
172    if (zdd_entry == NULL) {
173        table->errorCode = CUDD_MEMORY_OUT;
174        goto cuddZddSiftingOutOfMem;
175    }
176    var = ALLOC(int, size);
177    if (var == NULL) {
178        table->errorCode = CUDD_MEMORY_OUT;
179        goto cuddZddSiftingOutOfMem;
180    }
181
182    for (i = 0; i < size; i++) {
183        x = table->permZ[i];
184        zdd_entry[i] = table->subtableZ[x].keys;
185        var[i] = i;
186    }
187
188    qsort((void *)var, size, sizeof(int), (DD_QSFP)cuddZddUniqueCompare);
189
190    /* Now sift. */
191    for (i = 0; i < ddMin(table->siftMaxVar, size); i++) {
192        if (zddTotalNumberSwapping >= table->siftMaxSwap)
193            break;
194        x = table->permZ[var[i]];
195        if (x < lower || x > upper) continue;
196#ifdef DD_STATS
197        previousSize = table->keysZ;
198#endif
199        result = cuddZddLinearAux(table, x, lower, upper);
200        if (!result)
201            goto cuddZddSiftingOutOfMem;
202#ifdef DD_STATS
203        if (table->keysZ < (unsigned) previousSize) {
204            (void) fprintf(table->out,"-");
205        } else if (table->keysZ > (unsigned) previousSize) {
206            (void) fprintf(table->out,"+");     /* should never happen */
207            (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keysZ , var[i]);
208        } else {
209            (void) fprintf(table->out,"=");
210        }
211        fflush(table->out);
212#endif
213    }
214
215    FREE(var);
216    FREE(zdd_entry);
217
218    return(1);
219
220cuddZddSiftingOutOfMem:
221
222    if (zdd_entry != NULL) FREE(zdd_entry);
223    if (var != NULL) FREE(var);
224
225    return(0);
226
227} /* end of cuddZddLinearSifting */
228
229
230/*---------------------------------------------------------------------------*/
231/* Definition of static functions                                            */
232/*---------------------------------------------------------------------------*/
233
234
235/**Function********************************************************************
236
237  Synopsis    [Linearly combines two adjacent variables.]
238
239  Description [Linearly combines two adjacent variables. It assumes
240  that no dead nodes are present on entry to this procedure.  The
241  procedure then guarantees that no dead nodes will be present when it
242  terminates.  cuddZddLinearInPlace assumes that x &lt; y.  Returns the
243  number of keys in the table if successful; 0 otherwise.]
244
245  SideEffects [None]
246
247  SeeAlso     [cuddZddSwapInPlace cuddLinearInPlace]
248
249******************************************************************************/
250static int
251cuddZddLinearInPlace(
252  DdManager * table,
253  int  x,
254  int  y)
255{
256    DdNodePtr *xlist, *ylist;
257    int         xindex, yindex;
258    int         xslots, yslots;
259    int         xshift, yshift;
260    int         oldxkeys, oldykeys;
261    int         newxkeys, newykeys;
262    int         i;
263    int         posn;
264    DdNode      *f, *f1, *f0, *f11, *f10, *f01, *f00;
265    DdNode      *newf1, *newf0, *g, *next, *previous;
266    DdNode      *special;
267
268#ifdef DD_DEBUG
269    assert(x < y);
270    assert(cuddZddNextHigh(table,x) == y);
271    assert(table->subtableZ[x].keys != 0);
272    assert(table->subtableZ[y].keys != 0);
273    assert(table->subtableZ[x].dead == 0);
274    assert(table->subtableZ[y].dead == 0);
275#endif
276
277    zddTotalNumberLinearTr++;
278
279    /* Get parameters of x subtable. */
280    xindex   = table->invpermZ[x];
281    xlist    = table->subtableZ[x].nodelist;
282    oldxkeys = table->subtableZ[x].keys;
283    xslots   = table->subtableZ[x].slots;
284    xshift   = table->subtableZ[x].shift;
285    newxkeys = 0;
286
287    /* Get parameters of y subtable. */
288    yindex   = table->invpermZ[y];
289    ylist    = table->subtableZ[y].nodelist;
290    oldykeys = table->subtableZ[y].keys;
291    yslots   = table->subtableZ[y].slots;
292    yshift   = table->subtableZ[y].shift;
293    newykeys = oldykeys;
294
295    /* The nodes in the x layer are put in two chains.  The chain
296    ** pointed by g holds the normal nodes. When re-expressed they stay
297    ** in the x list. The chain pointed by special holds the elements
298    ** that will move to the y list.
299    */
300    g = special = NULL;
301    for (i = 0; i < xslots; i++) {
302        f = xlist[i];
303        if (f == NULL) continue;
304        xlist[i] = NULL;
305        while (f != NULL) {
306            next = f->next;
307            f1 = cuddT(f);
308            /* if (f1->index == yindex) */ cuddSatDec(f1->ref);
309            f0 = cuddE(f);
310            /* if (f0->index == yindex) */ cuddSatDec(f0->ref);
311            if ((int) f1->index == yindex && cuddE(f1) == empty &&
312                (int) f0->index != yindex) {
313                f->next = special;
314                special = f;
315            } else {
316                f->next = g;
317                g = f;
318            }
319            f = next;
320        } /* while there are elements in the collision chain */
321    } /* for each slot of the x subtable */
322
323    /* Mark y nodes with pointers from above x. We mark them by
324    **  changing their index to x.
325    */
326    for (i = 0; i < yslots; i++) {
327        f = ylist[i];
328        while (f != NULL) {
329            if (f->ref != 0) {
330                f->index = xindex;
331            }
332            f = f->next;
333        } /* while there are elements in the collision chain */
334    } /* for each slot of the y subtable */
335
336    /* Move special nodes to the y list. */
337    f = special;
338    while (f != NULL) {
339        next = f->next;
340        f1 = cuddT(f);
341        f11 = cuddT(f1);
342        cuddT(f) = f11;
343        cuddSatInc(f11->ref);
344        f0 = cuddE(f);
345        cuddSatInc(f0->ref);
346        f->index = yindex;
347        /* Insert at the beginning of the list so that it will be
348        ** found first if there is a duplicate. The duplicate will
349        ** eventually be moved or garbage collected. No node
350        ** re-expression will add a pointer to it.
351        */
352        posn = ddHash(f11, f0, yshift);
353        f->next = ylist[posn];
354        ylist[posn] = f;
355        newykeys++;
356        f = next;
357    }
358
359    /* Take care of the remaining x nodes that must be re-expressed.
360    ** They form a linked list pointed by g.
361    */
362    f = g;
363    while (f != NULL) {
364#ifdef DD_COUNT
365        table->swapSteps++;
366#endif
367        next = f->next;
368        /* Find f1, f0, f11, f10, f01, f00. */
369        f1 = cuddT(f);
370        if ((int) f1->index == yindex || (int) f1->index == xindex) {
371            f11 = cuddT(f1); f10 = cuddE(f1);
372        } else {
373            f11 = empty; f10 = f1;
374        }
375        f0 = cuddE(f);
376        if ((int) f0->index == yindex || (int) f0->index == xindex) {
377            f01 = cuddT(f0); f00 = cuddE(f0);
378        } else {
379            f01 = empty; f00 = f0;
380        }
381        /* Create the new T child. */
382        if (f01 == empty) {
383            newf1 = f10;
384            cuddSatInc(newf1->ref);
385        } else {
386            /* Check ylist for triple (yindex, f01, f10). */
387            posn = ddHash(f01, f10, yshift);
388            /* For each element newf1 in collision list ylist[posn]. */
389            newf1 = ylist[posn];
390            /* Search the collision chain skipping the marked nodes. */
391            while (newf1 != NULL) {
392                if (cuddT(newf1) == f01 && cuddE(newf1) == f10 &&
393                    (int) newf1->index == yindex) {
394                    cuddSatInc(newf1->ref);
395                    break; /* match */
396                }
397                newf1 = newf1->next;
398            } /* while newf1 */
399            if (newf1 == NULL) {        /* no match */
400                newf1 = cuddDynamicAllocNode(table);
401                if (newf1 == NULL)
402                    goto zddSwapOutOfMem;
403                newf1->index = yindex; newf1->ref = 1;
404                cuddT(newf1) = f01;
405                cuddE(newf1) = f10;
406                /* Insert newf1 in the collision list ylist[pos];
407                ** increase the ref counts of f01 and f10
408                */
409                newykeys++;
410                newf1->next = ylist[posn];
411                ylist[posn] = newf1;
412                cuddSatInc(f01->ref);
413                cuddSatInc(f10->ref);
414            }
415        }
416        cuddT(f) = newf1;
417
418        /* Do the same for f0. */
419        /* Create the new E child. */
420        if (f11 == empty) {
421            newf0 = f00;
422            cuddSatInc(newf0->ref);
423        } else {
424            /* Check ylist for triple (yindex, f11, f00). */
425            posn = ddHash(f11, f00, yshift);
426            /* For each element newf0 in collision list ylist[posn]. */
427            newf0 = ylist[posn];
428            while (newf0 != NULL) {
429                if (cuddT(newf0) == f11 && cuddE(newf0) == f00 &&
430                    (int) newf0->index == yindex) {
431                    cuddSatInc(newf0->ref);
432                    break; /* match */
433                }
434                newf0 = newf0->next;
435            } /* while newf0 */
436            if (newf0 == NULL) {        /* no match */
437                newf0 = cuddDynamicAllocNode(table);
438                if (newf0 == NULL)
439                    goto zddSwapOutOfMem;
440                newf0->index = yindex; newf0->ref = 1;
441                cuddT(newf0) = f11; cuddE(newf0) = f00;
442                /* Insert newf0 in the collision list ylist[posn];
443                ** increase the ref counts of f11 and f00.
444                */
445                newykeys++;
446                newf0->next = ylist[posn];
447                ylist[posn] = newf0;
448                cuddSatInc(f11->ref);
449                cuddSatInc(f00->ref);
450            }
451        }
452        cuddE(f) = newf0;
453
454        /* Re-insert the modified f in xlist.
455        ** The modified f does not already exists in xlist.
456        ** (Because of the uniqueness of the cofactors.)
457        */
458        posn = ddHash(newf1, newf0, xshift);
459        newxkeys++;
460        f->next = xlist[posn];
461        xlist[posn] = f;
462        f = next;
463    } /* while f != NULL */
464
465    /* GC the y layer and move the marked nodes to the x list. */
466
467    /* For each node f in ylist. */
468    for (i = 0; i < yslots; i++) {
469        previous = NULL;
470        f = ylist[i];
471        while (f != NULL) {
472            next = f->next;
473            if (f->ref == 0) {
474                cuddSatDec(cuddT(f)->ref);
475                cuddSatDec(cuddE(f)->ref);
476                cuddDeallocNode(table, f);
477                newykeys--;
478                if (previous == NULL)
479                    ylist[i] = next;
480                else
481                    previous->next = next;
482            } else if ((int) f->index == xindex) { /* move marked node */
483                if (previous == NULL)
484                    ylist[i] = next;
485                else
486                    previous->next = next;
487                f1 = cuddT(f);
488                cuddSatDec(f1->ref);
489                /* Check ylist for triple (yindex, f1, empty). */
490                posn = ddHash(f1, empty, yshift);
491                /* For each element newf1 in collision list ylist[posn]. */
492                newf1 = ylist[posn];
493                while (newf1 != NULL) {
494                    if (cuddT(newf1) == f1 && cuddE(newf1) == empty &&
495                        (int) newf1->index == yindex) {
496                        cuddSatInc(newf1->ref);
497                        break; /* match */
498                    }
499                    newf1 = newf1->next;
500                } /* while newf1 */
501                if (newf1 == NULL) {    /* no match */
502                    newf1 = cuddDynamicAllocNode(table);
503                    if (newf1 == NULL)
504                        goto zddSwapOutOfMem;
505                    newf1->index = yindex; newf1->ref = 1;
506                    cuddT(newf1) = f1; cuddE(newf1) = empty;
507                    /* Insert newf1 in the collision list ylist[posn];
508                    ** increase the ref counts of f1 and empty.
509                    */
510                    newykeys++;
511                    newf1->next = ylist[posn];
512                    ylist[posn] = newf1;
513                    if (posn == i && previous == NULL)
514                        previous = newf1;
515                    cuddSatInc(f1->ref);
516                    cuddSatInc(empty->ref);
517                }
518                cuddT(f) = newf1;
519                f0 = cuddE(f);
520                /* Insert f in x list. */
521                posn = ddHash(newf1, f0, xshift);
522                newxkeys++;
523                newykeys--;
524                f->next = xlist[posn];
525                xlist[posn] = f;
526            } else {
527                previous = f;
528            }
529            f = next;
530        } /* while f */
531    } /* for i */
532
533    /* Set the appropriate fields in table. */
534    table->subtableZ[x].keys     = newxkeys;
535    table->subtableZ[y].keys     = newykeys;
536
537    table->keysZ += newxkeys + newykeys - oldxkeys - oldykeys;
538
539    /* Update univ section; univ[x] remains the same. */
540    table->univ[y] = cuddT(table->univ[x]);
541
542#if 0
543    (void) fprintf(table->out,"x = %d  y = %d\n", x, y);
544    (void) Cudd_DebugCheck(table);
545    (void) Cudd_CheckKeys(table);
546#endif
547
548    return (table->keysZ);
549
550zddSwapOutOfMem:
551    (void) fprintf(table->err, "Error: cuddZddSwapInPlace out of memory\n");
552
553    return (0);
554
555} /* end of cuddZddLinearInPlace */
556
557
558/**Function********************************************************************
559
560  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
561  boundaries.]
562
563  Description [Given xLow <= x <= xHigh moves x up and down between the
564  boundaries. Finds the best position and does the required changes.
565  Returns 1 if successful; 0 otherwise.]
566
567  SideEffects [None]
568
569  SeeAlso     []
570
571******************************************************************************/
572static int
573cuddZddLinearAux(
574  DdManager * table,
575  int  x,
576  int  xLow,
577  int  xHigh)
578{
579    Move        *move;
580    Move        *moveUp;        /* list of up move */
581    Move        *moveDown;      /* list of down move */
582
583    int         initial_size;
584    int         result;
585
586    initial_size = table->keysZ;
587
588#ifdef DD_DEBUG
589    assert(table->subtableZ[x].keys > 0);
590#endif
591
592    moveDown = NULL;
593    moveUp = NULL;
594
595    if (x == xLow) {
596        moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
597        /* At this point x --> xHigh. */
598        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
599            goto cuddZddLinearAuxOutOfMem;
600        /* Move backward and stop at best position. */
601        result = cuddZddLinearBackward(table, initial_size, moveDown);
602        if (!result)
603            goto cuddZddLinearAuxOutOfMem;
604
605    } else if (x == xHigh) {
606        moveUp = cuddZddLinearUp(table, x, xLow, NULL);
607        /* At this point x --> xLow. */
608        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
609            goto cuddZddLinearAuxOutOfMem;
610        /* Move backward and stop at best position. */
611        result = cuddZddLinearBackward(table, initial_size, moveUp);
612        if (!result)
613            goto cuddZddLinearAuxOutOfMem;
614
615    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
616        moveDown = cuddZddLinearDown(table, x, xHigh, NULL);
617        /* At this point x --> xHigh. */
618        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
619            goto cuddZddLinearAuxOutOfMem;
620        moveUp = cuddZddUndoMoves(table,moveDown);
621#ifdef DD_DEBUG
622        assert(moveUp == NULL || moveUp->x == x);
623#endif
624        moveUp = cuddZddLinearUp(table, x, xLow, moveUp);
625        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
626            goto cuddZddLinearAuxOutOfMem;
627        /* Move backward and stop at best position. */
628        result = cuddZddLinearBackward(table, initial_size, moveUp);
629        if (!result)
630            goto cuddZddLinearAuxOutOfMem;
631
632    } else {
633        moveUp = cuddZddLinearUp(table, x, xLow, NULL);
634        /* At this point x --> xHigh. */
635        if (moveUp == (Move *) CUDD_OUT_OF_MEM)
636            goto cuddZddLinearAuxOutOfMem;
637        /* Then move up. */
638        moveDown = cuddZddUndoMoves(table,moveUp);
639#ifdef DD_DEBUG
640        assert(moveDown == NULL || moveDown->y == x);
641#endif
642        moveDown = cuddZddLinearDown(table, x, xHigh, moveDown);
643        if (moveDown == (Move *) CUDD_OUT_OF_MEM)
644            goto cuddZddLinearAuxOutOfMem;
645        /* Move backward and stop at best position. */
646        result = cuddZddLinearBackward(table, initial_size, moveDown);
647        if (!result)
648            goto cuddZddLinearAuxOutOfMem;
649    }
650
651    while (moveDown != NULL) {
652        move = moveDown->next;
653        cuddDeallocMove(table, moveDown);
654        moveDown = move;
655    }
656    while (moveUp != NULL) {
657        move = moveUp->next;
658        cuddDeallocMove(table, moveUp);
659        moveUp = move;
660    }
661
662    return(1);
663
664cuddZddLinearAuxOutOfMem:
665    if (moveDown != (Move *) CUDD_OUT_OF_MEM) {
666        while (moveDown != NULL) {
667            move = moveDown->next;
668            cuddDeallocMove(table, moveDown);
669            moveDown = move;
670        }
671    }
672    if (moveUp != (Move *) CUDD_OUT_OF_MEM) {
673        while (moveUp != NULL) {
674            move = moveUp->next;
675            cuddDeallocMove(table, moveUp);
676            moveUp = move;
677        }
678    }
679
680    return(0);
681
682} /* end of cuddZddLinearAux */
683
684
685/**Function********************************************************************
686
687  Synopsis    [Sifts a variable up applying the XOR transformation.]
688
689  Description [Sifts a variable up applying the XOR
690  transformation. Moves y up until either it reaches the bound (xLow)
691  or the size of the ZDD heap increases too much.  Returns the set of
692  moves in case of success; NULL if memory is full.]
693
694  SideEffects [None]
695
696  SeeAlso     []
697
698******************************************************************************/
699static Move *
700cuddZddLinearUp(
701  DdManager * table,
702  int  y,
703  int  xLow,
704  Move * prevMoves)
705{
706    Move        *moves;
707    Move        *move;
708    int         x;
709    int         size, newsize;
710    int         limitSize;
711
712    moves = prevMoves;
713    limitSize = table->keysZ;
714
715    x = cuddZddNextLow(table, y);
716    while (x >= xLow) {
717        size = cuddZddSwapInPlace(table, x, y);
718        if (size == 0)
719            goto cuddZddLinearUpOutOfMem;
720        newsize = cuddZddLinearInPlace(table, x, y);
721        if (newsize == 0)
722            goto cuddZddLinearUpOutOfMem;
723        move = (Move *) cuddDynamicAllocNode(table);
724        if (move == NULL)
725            goto cuddZddLinearUpOutOfMem;
726        move->x = x;
727        move->y = y;
728        move->next = moves;
729        moves = move;
730        move->flags = CUDD_SWAP_MOVE;
731        if (newsize > size) {
732            /* Undo transformation. The transformation we apply is
733            ** its own inverse. Hence, we just apply the transformation
734            ** again.
735            */
736            newsize = cuddZddLinearInPlace(table,x,y);
737            if (newsize == 0) goto cuddZddLinearUpOutOfMem;
738#ifdef DD_DEBUG
739            if (newsize != size) {
740                (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
741            }
742#endif
743        } else {
744            size = newsize;
745            move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
746        }
747        move->size = size;
748
749        if ((double)size > (double)limitSize * table->maxGrowth)
750            break;
751        if (size < limitSize)
752            limitSize = size;
753
754        y = x;
755        x = cuddZddNextLow(table, y);
756    }
757    return(moves);
758
759cuddZddLinearUpOutOfMem:
760    while (moves != NULL) {
761        move = moves->next;
762        cuddDeallocMove(table, moves);
763        moves = move;
764    }
765    return((Move *) CUDD_OUT_OF_MEM);
766
767} /* end of cuddZddLinearUp */
768
769
770/**Function********************************************************************
771
772  Synopsis    [Sifts a variable down and applies the XOR transformation.]
773
774  Description [Sifts a variable down. Moves x down until either it
775  reaches the bound (xHigh) or the size of the ZDD heap increases too
776  much. Returns the set of moves in case of success; NULL if memory is
777  full.]
778
779  SideEffects [None]
780
781  SeeAlso     []
782
783******************************************************************************/
784static Move *
785cuddZddLinearDown(
786  DdManager * table,
787  int  x,
788  int  xHigh,
789  Move * prevMoves)
790{
791    Move        *moves;
792    Move        *move;
793    int         y;
794    int         size, newsize;
795    int         limitSize;
796
797    moves = prevMoves;
798    limitSize = table->keysZ;
799
800    y = cuddZddNextHigh(table, x);
801    while (y <= xHigh) {
802        size = cuddZddSwapInPlace(table, x, y);
803        if (size == 0)
804            goto cuddZddLinearDownOutOfMem;
805        newsize = cuddZddLinearInPlace(table, x, y);
806        if (newsize == 0)
807            goto cuddZddLinearDownOutOfMem;
808        move = (Move *) cuddDynamicAllocNode(table);
809        if (move == NULL)
810            goto cuddZddLinearDownOutOfMem;
811        move->x = x;
812        move->y = y;
813        move->next = moves;
814        moves = move;
815        move->flags = CUDD_SWAP_MOVE;
816        if (newsize > size) {
817            /* Undo transformation. The transformation we apply is
818            ** its own inverse. Hence, we just apply the transformation
819            ** again.
820            */
821            newsize = cuddZddLinearInPlace(table,x,y);
822            if (newsize == 0) goto cuddZddLinearDownOutOfMem;
823            if (newsize != size) {
824                (void) fprintf(table->err,"Change in size after identity transformation! From %d to %d\n",size,newsize);
825            }
826        } else {
827            size = newsize;
828            move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
829        }
830        move->size = size;
831
832        if ((double)size > (double)limitSize * table->maxGrowth)
833            break;
834        if (size < limitSize)
835            limitSize = size;
836
837        x = y;
838        y = cuddZddNextHigh(table, x);
839    }
840    return(moves);
841
842cuddZddLinearDownOutOfMem:
843    while (moves != NULL) {
844        move = moves->next;
845        cuddDeallocMove(table, moves);
846        moves = move;
847    }
848    return((Move *) CUDD_OUT_OF_MEM);
849
850} /* end of cuddZddLinearDown */
851
852
853/**Function********************************************************************
854
855  Synopsis    [Given a set of moves, returns the ZDD heap to the position
856  giving the minimum size.]
857
858  Description [Given a set of moves, returns the ZDD heap to the
859  position giving the minimum size. In case of ties, returns to the
860  closest position giving the minimum size. Returns 1 in case of
861  success; 0 otherwise.]
862
863  SideEffects [None]
864
865  SeeAlso     []
866
867******************************************************************************/
868static int
869cuddZddLinearBackward(
870  DdManager * table,
871  int  size,
872  Move * moves)
873{
874    Move        *move;
875    int         res;
876
877    /* Find the minimum size among moves. */
878    for (move = moves; move != NULL; move = move->next) {
879        if (move->size < size) {
880            size = move->size;
881        }
882    }
883
884    for (move = moves; move != NULL; move = move->next) {
885        if (move->size == size) return(1);
886        if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
887            res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
888            if (!res) return(0);
889        }
890        res = cuddZddSwapInPlace(table, move->x, move->y);
891        if (!res)
892            return(0);
893        if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
894            res = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
895            if (!res) return(0);
896        }
897    }
898
899    return(1);
900
901} /* end of cuddZddLinearBackward */
902
903
904/**Function********************************************************************
905
906  Synopsis    [Given a set of moves, returns the ZDD heap to the order
907  in effect before the moves.]
908
909  Description [Given a set of moves, returns the ZDD heap to the
910  order in effect before the moves.  Returns 1 in case of success;
911  0 otherwise.]
912
913  SideEffects [None]
914
915******************************************************************************/
916static Move*
917cuddZddUndoMoves(
918  DdManager * table,
919  Move * moves)
920{
921    Move *invmoves = NULL;
922    Move *move;
923    Move *invmove;
924    int size;
925
926    for (move = moves; move != NULL; move = move->next) {
927        invmove = (Move *) cuddDynamicAllocNode(table);
928        if (invmove == NULL) goto cuddZddUndoMovesOutOfMem;
929        invmove->x = move->x;
930        invmove->y = move->y;
931        invmove->next = invmoves;
932        invmoves = invmove;
933        if (move->flags == CUDD_SWAP_MOVE) {
934            invmove->flags = CUDD_SWAP_MOVE;
935            size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
936            if (!size) goto cuddZddUndoMovesOutOfMem;
937        } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
938            invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
939            size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
940            if (!size) goto cuddZddUndoMovesOutOfMem;
941            size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
942            if (!size) goto cuddZddUndoMovesOutOfMem;
943        } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
944#ifdef DD_DEBUG
945            (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
946#endif
947            invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
948            size = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
949            if (!size) goto cuddZddUndoMovesOutOfMem;
950            size = cuddZddLinearInPlace(table,(int)move->x,(int)move->y);
951            if (!size) goto cuddZddUndoMovesOutOfMem;
952        }
953        invmove->size = size;
954    }
955
956    return(invmoves);
957
958cuddZddUndoMovesOutOfMem:
959    while (invmoves != NULL) {
960        move = invmoves->next;
961        cuddDeallocMove(table, invmoves);
962        invmoves = move;
963    }
964    return((Move *) CUDD_OUT_OF_MEM);
965
966} /* end of cuddZddUndoMoves */
967
Note: See TracBrowser for help on using the repository browser.