source: vis_dev/glu-2.3/src/cuBdd/cuddLinear.c @ 91

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

library glu 2.3

File size: 38.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddLinear.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Functions for DD reduction by linear transformations.]
8
9  Description [ Internal procedures included in this module:
10                <ul>
11                <li> cuddLinearAndSifting()
12                <li> cuddLinearInPlace()
13                <li> cuddUpdateInteractionMatrix()
14                <li> cuddInitLinear()
15                <li> cuddResizeLinear()
16                </ul>
17        Static procedures included in this module:
18                <ul>
19                <li> ddLinearUniqueCompare()
20                <li> ddLinearAndSiftingAux()
21                <li> ddLinearAndSiftingUp()
22                <li> ddLinearAndSiftingDown()
23                <li> ddLinearAndSiftingBackward()
24                <li> ddUndoMoves()
25                <li> cuddXorLinear()
26                </ul>]
27
28  Author      [Fabio Somenzi]
29
30  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
31
32  All rights reserved.
33
34  Redistribution and use in source and binary forms, with or without
35  modification, are permitted provided that the following conditions
36  are met:
37
38  Redistributions of source code must retain the above copyright
39  notice, this list of conditions and the following disclaimer.
40
41  Redistributions in binary form must reproduce the above copyright
42  notice, this list of conditions and the following disclaimer in the
43  documentation and/or other materials provided with the distribution.
44
45  Neither the name of the University of Colorado nor the names of its
46  contributors may be used to endorse or promote products derived from
47  this software without specific prior written permission.
48
49  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
50  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
51  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
52  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
53  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
54  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
55  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
56  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
57  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
58  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
59  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
60  POSSIBILITY OF SUCH DAMAGE.]
61
62******************************************************************************/
63
64#include "util.h"
65#include "cuddInt.h"
66
67/*---------------------------------------------------------------------------*/
68/* Constant declarations                                                     */
69/*---------------------------------------------------------------------------*/
70
71#define CUDD_SWAP_MOVE 0
72#define CUDD_LINEAR_TRANSFORM_MOVE 1
73#define CUDD_INVERSE_TRANSFORM_MOVE 2
74#if SIZEOF_LONG == 8
75#define BPL 64
76#define LOGBPL 6
77#else
78#define BPL 32
79#define LOGBPL 5
80#endif
81
82/*---------------------------------------------------------------------------*/
83/* Stucture declarations                                                     */
84/*---------------------------------------------------------------------------*/
85
86/*---------------------------------------------------------------------------*/
87/* Type declarations                                                         */
88/*---------------------------------------------------------------------------*/
89
90/*---------------------------------------------------------------------------*/
91/* Variable declarations                                                     */
92/*---------------------------------------------------------------------------*/
93
94#ifndef lint
95static char rcsid[] DD_UNUSED = "$Id: cuddLinear.c,v 1.28 2009/02/19 16:21:03 fabio Exp $";
96#endif
97
98static  int     *entry;
99
100#ifdef DD_STATS
101extern  int     ddTotalNumberSwapping;
102extern  int     ddTotalNISwaps;
103static  int     ddTotalNumberLinearTr;
104#endif
105
106#ifdef DD_DEBUG
107static  int     zero = 0;
108#endif
109
110/*---------------------------------------------------------------------------*/
111/* Macro declarations                                                        */
112/*---------------------------------------------------------------------------*/
113
114/**AutomaticStart*************************************************************/
115
116/*---------------------------------------------------------------------------*/
117/* Static function prototypes                                                */
118/*---------------------------------------------------------------------------*/
119
120static int ddLinearUniqueCompare (int *ptrX, int *ptrY);
121static int ddLinearAndSiftingAux (DdManager *table, int x, int xLow, int xHigh);
122static Move * ddLinearAndSiftingUp (DdManager *table, int y, int xLow, Move *prevMoves);
123static Move * ddLinearAndSiftingDown (DdManager *table, int x, int xHigh, Move *prevMoves);
124static int ddLinearAndSiftingBackward (DdManager *table, int size, Move *moves);
125static Move* ddUndoMoves (DdManager *table, Move *moves);
126static void cuddXorLinear (DdManager *table, int x, int y);
127
128/**AutomaticEnd***************************************************************/
129
130
131/*---------------------------------------------------------------------------*/
132/* Definition of exported functions                                          */
133/*---------------------------------------------------------------------------*/
134
135
136/**Function********************************************************************
137
138  Synopsis    [Prints the linear transform matrix.]
139
140  Description [Prints the linear transform matrix. Returns 1 in case of
141  success; 0 otherwise.]
142
143  SideEffects [none]
144
145  SeeAlso     []
146
147******************************************************************************/
148int
149Cudd_PrintLinear(
150  DdManager * table)
151{
152    int i,j,k;
153    int retval;
154    int nvars = table->linearSize;
155    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
156    long word;
157
158    for (i = 0; i < nvars; i++) {
159        for (j = 0; j < wordsPerRow; j++) {
160            word = table->linear[i*wordsPerRow + j];
161            for (k = 0; k < BPL; k++) {
162                retval = fprintf(table->out,"%ld",word & 1);
163                if (retval == 0) return(0);
164                word >>= 1;
165            }
166        }
167        retval = fprintf(table->out,"\n");
168        if (retval == 0) return(0);
169    }
170    return(1);
171
172} /* end of Cudd_PrintLinear */
173
174
175/**Function********************************************************************
176
177  Synopsis    [Reads an entry of the linear transform matrix.]
178
179  Description [Reads an entry of the linear transform matrix.]
180
181  SideEffects [none]
182
183  SeeAlso     []
184
185******************************************************************************/
186int
187Cudd_ReadLinear(
188  DdManager * table /* CUDD manager */,
189  int  x /* row index */,
190  int  y /* column index */)
191{
192    int nvars = table->size;
193    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
194    long word;
195    int bit;
196    int result;
197
198    assert(table->size == table->linearSize);
199
200    word = wordsPerRow * x + (y >> LOGBPL);
201    bit  = y & (BPL-1);
202    result = (int) ((table->linear[word] >> bit) & 1);
203    return(result);
204
205} /* end of Cudd_ReadLinear */
206
207
208/*---------------------------------------------------------------------------*/
209/* Definition of internal functions                                          */
210/*---------------------------------------------------------------------------*/
211
212
213/**Function********************************************************************
214
215  Synopsis    [BDD reduction based on combination of sifting and linear
216  transformations.]
217
218  Description [BDD reduction based on combination of sifting and linear
219  transformations.  Assumes that no dead nodes are present.
220    <ol>
221    <li> Order all the variables according to the number of entries
222    in each unique table.
223    <li> Sift the variable up and down, remembering each time the
224    total size of the DD heap. At each position, linear transformation
225    of the two adjacent variables is tried and is accepted if it reduces
226    the size of the DD.
227    <li> Select the best permutation.
228    <li> Repeat 3 and 4 for all variables.
229    </ol>
230  Returns 1 if successful; 0 otherwise.]
231
232  SideEffects [None]
233
234******************************************************************************/
235int
236cuddLinearAndSifting(
237  DdManager * table,
238  int  lower,
239  int  upper)
240{
241    int         i;
242    int         *var;
243    int         size;
244    int         x;
245    int         result;
246#ifdef DD_STATS
247    int         previousSize;
248#endif
249
250#ifdef DD_STATS
251    ddTotalNumberLinearTr = 0;
252#endif
253
254    size = table->size;
255
256    var = NULL;
257    entry = NULL;
258    if (table->linear == NULL) {
259        result = cuddInitLinear(table);
260        if (result == 0) goto cuddLinearAndSiftingOutOfMem;
261#if 0
262        (void) fprintf(table->out,"\n");
263        result = Cudd_PrintLinear(table);
264        if (result == 0) goto cuddLinearAndSiftingOutOfMem;
265#endif
266    } else if (table->size != table->linearSize) {
267        result = cuddResizeLinear(table);
268        if (result == 0) goto cuddLinearAndSiftingOutOfMem;
269#if 0
270        (void) fprintf(table->out,"\n");
271        result = Cudd_PrintLinear(table);
272        if (result == 0) goto cuddLinearAndSiftingOutOfMem;
273#endif
274    }
275
276    /* Find order in which to sift variables. */
277    entry = ALLOC(int,size);
278    if (entry == NULL) {
279        table->errorCode = CUDD_MEMORY_OUT;
280        goto cuddLinearAndSiftingOutOfMem;
281    }
282    var = ALLOC(int,size);
283    if (var == NULL) {
284        table->errorCode = CUDD_MEMORY_OUT;
285        goto cuddLinearAndSiftingOutOfMem;
286    }
287
288    for (i = 0; i < size; i++) {
289        x = table->perm[i];
290        entry[i] = table->subtables[x].keys;
291        var[i] = i;
292    }
293
294    qsort((void *)var,size,sizeof(int),(DD_QSFP)ddLinearUniqueCompare);
295
296    /* Now sift. */
297    for (i = 0; i < ddMin(table->siftMaxVar,size); i++) {
298        x = table->perm[var[i]];
299        if (x < lower || x > upper) continue;
300#ifdef DD_STATS
301        previousSize = table->keys - table->isolated;
302#endif
303        result = ddLinearAndSiftingAux(table,x,lower,upper);
304        if (!result) goto cuddLinearAndSiftingOutOfMem;
305#ifdef DD_STATS
306        if (table->keys < (unsigned) previousSize + table->isolated) {
307            (void) fprintf(table->out,"-");
308        } else if (table->keys > (unsigned) previousSize + table->isolated) {
309            (void) fprintf(table->out,"+");     /* should never happen */
310            (void) fprintf(table->out,"\nSize increased from %d to %d while sifting variable %d\n", previousSize, table->keys - table->isolated, var[i]);
311        } else {
312            (void) fprintf(table->out,"=");
313        }
314        fflush(table->out);
315#endif
316#ifdef DD_DEBUG
317        (void) Cudd_DebugCheck(table);
318#endif
319    }
320
321    FREE(var);
322    FREE(entry);
323
324#ifdef DD_STATS
325    (void) fprintf(table->out,"\n#:L_LINSIFT %8d: linear trans.",
326                   ddTotalNumberLinearTr);
327#endif
328
329    return(1);
330
331cuddLinearAndSiftingOutOfMem:
332
333    if (entry != NULL) FREE(entry);
334    if (var != NULL) FREE(var);
335
336    return(0);
337
338} /* end of cuddLinearAndSifting */
339
340
341/**Function********************************************************************
342
343  Synopsis    [Linearly combines two adjacent variables.]
344
345  Description [Linearly combines two adjacent variables. Specifically,
346  replaces the top variable with the exclusive nor of the two variables.
347  It assumes that no dead nodes are present on entry to this
348  procedure.  The procedure then guarantees that no dead nodes will be
349  present when it terminates.  cuddLinearInPlace assumes that x &lt;
350  y.  Returns the number of keys in the table if successful; 0
351  otherwise.]
352
353  SideEffects [The two subtables corrresponding to variables x and y are
354  modified. The global counters of the unique table are also affected.]
355
356  SeeAlso     [cuddSwapInPlace]
357
358******************************************************************************/
359int
360cuddLinearInPlace(
361  DdManager * table,
362  int  x,
363  int  y)
364{
365    DdNodePtr *xlist, *ylist;
366    int    xindex, yindex;
367    int    xslots, yslots;
368    int    xshift, yshift;
369    int    oldxkeys, oldykeys;
370    int    newxkeys, newykeys;
371    int    comple, newcomplement;
372    int    i;
373    int    posn;
374    int    isolated;
375    DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10,*newf1,*newf0;
376    DdNode *g,*next,*last;
377    DdNodePtr *previousP;
378    DdNode *tmp;
379    DdNode *sentinel = &(table->sentinel);
380#ifdef DD_DEBUG
381    int    count, idcheck;
382#endif
383
384#ifdef DD_DEBUG
385    assert(x < y);
386    assert(cuddNextHigh(table,x) == y);
387    assert(table->subtables[x].keys != 0);
388    assert(table->subtables[y].keys != 0);
389    assert(table->subtables[x].dead == 0);
390    assert(table->subtables[y].dead == 0);
391#endif
392
393    xindex = table->invperm[x];
394    yindex = table->invperm[y];
395
396    if (cuddTestInteract(table,xindex,yindex)) {
397#ifdef DD_STATS
398        ddTotalNumberLinearTr++;
399#endif
400        /* Get parameters of x subtable. */
401        xlist = table->subtables[x].nodelist;
402        oldxkeys = table->subtables[x].keys;
403        xslots = table->subtables[x].slots;
404        xshift = table->subtables[x].shift;
405
406        /* Get parameters of y subtable. */
407        ylist = table->subtables[y].nodelist;
408        oldykeys = table->subtables[y].keys;
409        yslots = table->subtables[y].slots;
410        yshift = table->subtables[y].shift;
411
412        newxkeys = 0;
413        newykeys = oldykeys;
414
415        /* Check whether the two projection functions involved in this
416        ** swap are isolated. At the end, we'll be able to tell how many
417        ** isolated projection functions are there by checking only these
418        ** two functions again. This is done to eliminate the isolated
419        ** projection functions from the node count.
420        */
421        isolated = - ((table->vars[xindex]->ref == 1) +
422                     (table->vars[yindex]->ref == 1));
423
424        /* The nodes in the x layer are put in a chain.
425        ** The chain is handled as a FIFO; g points to the beginning and
426        ** last points to the end.
427        */
428        g = NULL;
429#ifdef DD_DEBUG
430        last = NULL;
431#endif
432        for (i = 0; i < xslots; i++) {
433            f = xlist[i];
434            if (f == sentinel) continue;
435            xlist[i] = sentinel;
436            if (g == NULL) {
437                g = f;
438            } else {
439                last->next = f;
440            }
441            while ((next = f->next) != sentinel) {
442                f = next;
443            } /* while there are elements in the collision chain */
444            last = f;
445        } /* for each slot of the x subtable */
446#ifdef DD_DEBUG
447        /* last is always assigned in the for loop because there is at
448        ** least one key */
449        assert(last != NULL);
450#endif
451        last->next = NULL;
452
453#ifdef DD_COUNT
454        table->swapSteps += oldxkeys;
455#endif
456        /* Take care of the x nodes that must be re-expressed.
457        ** They form a linked list pointed by g.
458        */
459        f = g;
460        while (f != NULL) {
461            next = f->next;
462            /* Find f1, f0, f11, f10, f01, f00. */
463            f1 = cuddT(f);
464#ifdef DD_DEBUG
465            assert(!(Cudd_IsComplement(f1)));
466#endif
467            if ((int) f1->index == yindex) {
468                f11 = cuddT(f1); f10 = cuddE(f1);
469            } else {
470                f11 = f10 = f1;
471            }
472#ifdef DD_DEBUG
473            assert(!(Cudd_IsComplement(f11)));
474#endif
475            f0 = cuddE(f);
476            comple = Cudd_IsComplement(f0);
477            f0 = Cudd_Regular(f0);
478            if ((int) f0->index == yindex) {
479                f01 = cuddT(f0); f00 = cuddE(f0);
480            } else {
481                f01 = f00 = f0;
482            }
483            if (comple) {
484                f01 = Cudd_Not(f01);
485                f00 = Cudd_Not(f00);
486            }
487            /* Decrease ref count of f1. */
488            cuddSatDec(f1->ref);
489            /* Create the new T child. */
490            if (f11 == f00) {
491                newf1 = f11;
492                cuddSatInc(newf1->ref);
493            } else {
494                /* Check ylist for triple (yindex,f11,f00). */
495                posn = ddHash(f11, f00, yshift);
496                /* For each element newf1 in collision list ylist[posn]. */
497                previousP = &(ylist[posn]);
498                newf1 = *previousP;
499                while (f11 < cuddT(newf1)) {
500                    previousP = &(newf1->next);
501                    newf1 = *previousP;
502                }
503                while (f11 == cuddT(newf1) && f00 < cuddE(newf1)) {
504                    previousP = &(newf1->next);
505                    newf1 = *previousP;
506                }
507                if (cuddT(newf1) == f11 && cuddE(newf1) == f00) {
508                    cuddSatInc(newf1->ref);
509                } else { /* no match */
510                    newf1 = cuddDynamicAllocNode(table);
511                    if (newf1 == NULL)
512                        goto cuddLinearOutOfMem;
513                    newf1->index = yindex; newf1->ref = 1;
514                    cuddT(newf1) = f11;
515                    cuddE(newf1) = f00;
516                    /* Insert newf1 in the collision list ylist[posn];
517                    ** increase the ref counts of f11 and f00.
518                    */
519                    newykeys++;
520                    newf1->next = *previousP;
521                    *previousP = newf1;
522                    cuddSatInc(f11->ref);
523                    tmp = Cudd_Regular(f00);
524                    cuddSatInc(tmp->ref);
525                }
526            }
527            cuddT(f) = newf1;
528#ifdef DD_DEBUG
529            assert(!(Cudd_IsComplement(newf1)));
530#endif
531
532            /* Do the same for f0, keeping complement dots into account. */
533            /* decrease ref count of f0 */
534            tmp = Cudd_Regular(f0);
535            cuddSatDec(tmp->ref);
536            /* create the new E child */
537            if (f01 == f10) {
538                newf0 = f01;
539                tmp = Cudd_Regular(newf0);
540                cuddSatInc(tmp->ref);
541            } else {
542                /* make sure f01 is regular */
543                newcomplement = Cudd_IsComplement(f01);
544                if (newcomplement) {
545                    f01 = Cudd_Not(f01);
546                    f10 = Cudd_Not(f10);
547                }
548                /* Check ylist for triple (yindex,f01,f10). */
549                posn = ddHash(f01, f10, yshift);
550                /* For each element newf0 in collision list ylist[posn]. */
551                previousP = &(ylist[posn]);
552                newf0 = *previousP;
553                while (f01 < cuddT(newf0)) {
554                    previousP = &(newf0->next);
555                    newf0 = *previousP;
556                }
557                while (f01 == cuddT(newf0) && f10 < cuddE(newf0)) {
558                    previousP = &(newf0->next);
559                    newf0 = *previousP;
560                }
561                if (cuddT(newf0) == f01 && cuddE(newf0) == f10) {
562                    cuddSatInc(newf0->ref);
563                } else { /* no match */
564                    newf0 = cuddDynamicAllocNode(table);
565                    if (newf0 == NULL)
566                        goto cuddLinearOutOfMem;
567                    newf0->index = yindex; newf0->ref = 1;
568                    cuddT(newf0) = f01;
569                    cuddE(newf0) = f10;
570                    /* Insert newf0 in the collision list ylist[posn];
571                    ** increase the ref counts of f01 and f10.
572                    */
573                    newykeys++;
574                    newf0->next = *previousP;
575                    *previousP = newf0;
576                    cuddSatInc(f01->ref);
577                    tmp = Cudd_Regular(f10);
578                    cuddSatInc(tmp->ref);
579                }
580                if (newcomplement) {
581                    newf0 = Cudd_Not(newf0);
582                }
583            }
584            cuddE(f) = newf0;
585
586            /* Re-insert the modified f in xlist.
587            ** The modified f does not already exists in xlist.
588            ** (Because of the uniqueness of the cofactors.)
589            */
590            posn = ddHash(newf1, newf0, xshift);
591            newxkeys++;
592            previousP = &(xlist[posn]);
593            tmp = *previousP;
594            while (newf1 < cuddT(tmp)) {
595                previousP = &(tmp->next);
596                tmp = *previousP;
597            }
598            while (newf1 == cuddT(tmp) && newf0 < cuddE(tmp)) {
599                previousP = &(tmp->next);
600                tmp = *previousP;
601            }
602            f->next = *previousP;
603            *previousP = f;
604            f = next;
605        } /* while f != NULL */
606
607        /* GC the y layer. */
608
609        /* For each node f in ylist. */
610        for (i = 0; i < yslots; i++) {
611            previousP = &(ylist[i]);
612            f = *previousP;
613            while (f != sentinel) {
614                next = f->next;
615                if (f->ref == 0) {
616                    tmp = cuddT(f);
617                    cuddSatDec(tmp->ref);
618                    tmp = Cudd_Regular(cuddE(f));
619                    cuddSatDec(tmp->ref);
620                    cuddDeallocNode(table,f);
621                    newykeys--;
622                } else {
623                    *previousP = f;
624                    previousP = &(f->next);
625                }
626                f = next;
627            } /* while f */
628            *previousP = sentinel;
629        } /* for every collision list */
630
631#ifdef DD_DEBUG
632#if 0
633        (void) fprintf(table->out,"Linearly combining %d and %d\n",x,y);
634#endif
635        count = 0;
636        idcheck = 0;
637        for (i = 0; i < yslots; i++) {
638            f = ylist[i];
639            while (f != sentinel) {
640                count++;
641                if (f->index != (DdHalfWord) yindex)
642                    idcheck++;
643                f = f->next;
644            }
645        }
646        if (count != newykeys) {
647            fprintf(table->err,"Error in finding newykeys\toldykeys = %d\tnewykeys = %d\tactual = %d\n",oldykeys,newykeys,count);
648        }
649        if (idcheck != 0)
650            fprintf(table->err,"Error in id's of ylist\twrong id's = %d\n",idcheck);
651        count = 0;
652        idcheck = 0;
653        for (i = 0; i < xslots; i++) {
654            f = xlist[i];
655            while (f != sentinel) {
656                count++;
657                if (f->index != (DdHalfWord) xindex)
658                    idcheck++;
659                f = f->next;
660            }
661        }
662        if (count != newxkeys || newxkeys != oldxkeys) {
663            fprintf(table->err,"Error in finding newxkeys\toldxkeys = %d \tnewxkeys = %d \tactual = %d\n",oldxkeys,newxkeys,count);
664        }
665        if (idcheck != 0)
666            fprintf(table->err,"Error in id's of xlist\twrong id's = %d\n",idcheck);
667#endif
668
669        isolated += (table->vars[xindex]->ref == 1) +
670                    (table->vars[yindex]->ref == 1);
671        table->isolated += isolated;
672
673        /* Set the appropriate fields in table. */
674        table->subtables[y].keys = newykeys;
675
676        /* Here we should update the linear combination table
677        ** to record that x <- x EXNOR y. This is done by complementing
678        ** the (x,y) entry of the table.
679        */
680
681        table->keys += newykeys - oldykeys;
682
683        cuddXorLinear(table,xindex,yindex);
684    }
685
686#ifdef DD_DEBUG
687    if (zero) {
688        (void) Cudd_DebugCheck(table);
689    }
690#endif
691
692    return(table->keys - table->isolated);
693
694cuddLinearOutOfMem:
695    (void) fprintf(table->err,"Error: cuddLinearInPlace out of memory\n");
696
697    return (0);
698
699} /* end of cuddLinearInPlace */
700
701
702/**Function********************************************************************
703
704  Synopsis    [Updates the interaction matrix.]
705
706  Description []
707
708  SideEffects [none]
709
710  SeeAlso     []
711
712******************************************************************************/
713void
714cuddUpdateInteractionMatrix(
715  DdManager * table,
716  int  xindex,
717  int  yindex)
718{
719    int i;
720    for (i = 0; i < yindex; i++) {
721        if (i != xindex && cuddTestInteract(table,i,yindex)) {
722            if (i < xindex) {
723                cuddSetInteract(table,i,xindex);
724            } else {
725                cuddSetInteract(table,xindex,i);
726            }
727        }
728    }
729    for (i = yindex+1; i < table->size; i++) {
730        if (i != xindex && cuddTestInteract(table,yindex,i)) {
731            if (i < xindex) {
732                cuddSetInteract(table,i,xindex);
733            } else {
734                cuddSetInteract(table,xindex,i);
735            }
736        }
737    }
738
739} /* end of cuddUpdateInteractionMatrix */
740
741
742/**Function********************************************************************
743
744  Synopsis    [Initializes the linear transform matrix.]
745
746  Description [Initializes the linear transform matrix.  Returns 1 if
747  successful; 0 otherwise.]
748
749  SideEffects [none]
750
751  SeeAlso     []
752
753******************************************************************************/
754int
755cuddInitLinear(
756  DdManager * table)
757{
758    int words;
759    int wordsPerRow;
760    int nvars;
761    int word;
762    int bit;
763    int i;
764    long *linear;
765
766    nvars = table->size;
767    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
768    words = wordsPerRow * nvars;
769    table->linear = linear = ALLOC(long,words);
770    if (linear == NULL) {
771        table->errorCode = CUDD_MEMORY_OUT;
772        return(0);
773    }
774    table->memused += words * sizeof(long);
775    table->linearSize = nvars;
776    for (i = 0; i < words; i++) linear[i] = 0;
777    for (i = 0; i < nvars; i++) {
778        word = wordsPerRow * i + (i >> LOGBPL);
779        bit  = i & (BPL-1);
780        linear[word] = 1 << bit;
781    }
782    return(1);
783
784} /* end of cuddInitLinear */
785
786
787/**Function********************************************************************
788
789  Synopsis    [Resizes the linear transform matrix.]
790
791  Description [Resizes the linear transform matrix.  Returns 1 if
792  successful; 0 otherwise.]
793
794  SideEffects [none]
795
796  SeeAlso     []
797
798******************************************************************************/
799int
800cuddResizeLinear(
801  DdManager * table)
802{
803    int words,oldWords;
804    int wordsPerRow,oldWordsPerRow;
805    int nvars,oldNvars;
806    int word,oldWord;
807    int bit;
808    int i,j;
809    long *linear,*oldLinear;
810
811    oldNvars = table->linearSize;
812    oldWordsPerRow = ((oldNvars - 1) >> LOGBPL) + 1;
813    oldWords = oldWordsPerRow * oldNvars;
814    oldLinear = table->linear;
815
816    nvars = table->size;
817    wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
818    words = wordsPerRow * nvars;
819    table->linear = linear = ALLOC(long,words);
820    if (linear == NULL) {
821        table->errorCode = CUDD_MEMORY_OUT;
822        return(0);
823    }
824    table->memused += (words - oldWords) * sizeof(long);
825    for (i = 0; i < words; i++) linear[i] = 0;
826
827    /* Copy old matrix. */
828    for (i = 0; i < oldNvars; i++) {
829        for (j = 0; j < oldWordsPerRow; j++) {
830            oldWord = oldWordsPerRow * i + j;
831            word = wordsPerRow * i + j;
832            linear[word] = oldLinear[oldWord];
833        }
834    }
835    FREE(oldLinear);
836
837    /* Add elements to the diagonal. */
838    for (i = oldNvars; i < nvars; i++) {
839        word = wordsPerRow * i + (i >> LOGBPL);
840        bit  = i & (BPL-1);
841        linear[word] = 1 << bit;
842    }
843    table->linearSize = nvars;
844
845    return(1);
846
847} /* end of cuddResizeLinear */
848
849
850/*---------------------------------------------------------------------------*/
851/* Definition of static functions                                            */
852/*---------------------------------------------------------------------------*/
853
854
855/**Function********************************************************************
856
857  Synopsis    [Comparison function used by qsort.]
858
859  Description [Comparison function used by qsort to order the
860  variables according to the number of keys in the subtables.
861  Returns the difference in number of keys between the two
862  variables being compared.]
863
864  SideEffects [None]
865
866******************************************************************************/
867static int
868ddLinearUniqueCompare(
869  int * ptrX,
870  int * ptrY)
871{
872#if 0
873    if (entry[*ptrY] == entry[*ptrX]) {
874        return((*ptrX) - (*ptrY));
875    }
876#endif
877    return(entry[*ptrY] - entry[*ptrX]);
878
879} /* end of ddLinearUniqueCompare */
880
881
882/**Function********************************************************************
883
884  Synopsis    [Given xLow <= x <= xHigh moves x up and down between the
885  boundaries.]
886
887  Description [Given xLow <= x <= xHigh moves x up and down between the
888  boundaries. At each step a linear transformation is tried, and, if it
889  decreases the size of the DD, it is accepted. Finds the best position
890  and does the required changes.  Returns 1 if successful; 0 otherwise.]
891
892  SideEffects [None]
893
894******************************************************************************/
895static int
896ddLinearAndSiftingAux(
897  DdManager * table,
898  int  x,
899  int  xLow,
900  int  xHigh)
901{
902
903    Move        *move;
904    Move        *moveUp;                /* list of up moves */
905    Move        *moveDown;              /* list of down moves */
906    int         initialSize;
907    int         result;
908
909    initialSize = table->keys - table->isolated;
910
911    moveDown = NULL;
912    moveUp = NULL;
913
914    if (x == xLow) {
915        moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
916        /* At this point x --> xHigh unless bounding occurred. */
917        if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
918        /* Move backward and stop at best position. */
919        result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
920        if (!result) goto ddLinearAndSiftingAuxOutOfMem;
921
922    } else if (x == xHigh) {
923        moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
924        /* At this point x --> xLow unless bounding occurred. */
925        if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
926        /* Move backward and stop at best position. */
927        result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
928        if (!result) goto ddLinearAndSiftingAuxOutOfMem;
929
930    } else if ((x - xLow) > (xHigh - x)) { /* must go down first: shorter */
931        moveDown = ddLinearAndSiftingDown(table,x,xHigh,NULL);
932        /* At this point x --> xHigh unless bounding occurred. */
933        if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
934        moveUp = ddUndoMoves(table,moveDown);
935#ifdef DD_DEBUG
936        assert(moveUp == NULL || moveUp->x == x);
937#endif
938        moveUp = ddLinearAndSiftingUp(table,x,xLow,moveUp);
939        if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
940        /* Move backward and stop at best position. */
941        result = ddLinearAndSiftingBackward(table,initialSize,moveUp);
942        if (!result) goto ddLinearAndSiftingAuxOutOfMem;
943
944    } else { /* must go up first: shorter */
945        moveUp = ddLinearAndSiftingUp(table,x,xLow,NULL);
946        /* At this point x --> xLow unless bounding occurred. */
947        if (moveUp == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
948        moveDown = ddUndoMoves(table,moveUp);
949#ifdef DD_DEBUG
950        assert(moveDown == NULL || moveDown->y == x);
951#endif
952        moveDown = ddLinearAndSiftingDown(table,x,xHigh,moveDown);
953        if (moveDown == (Move *) CUDD_OUT_OF_MEM) goto ddLinearAndSiftingAuxOutOfMem;
954        /* Move backward and stop at best position. */
955        result = ddLinearAndSiftingBackward(table,initialSize,moveDown);
956        if (!result) goto ddLinearAndSiftingAuxOutOfMem;
957    }
958
959    while (moveDown != NULL) {
960        move = moveDown->next;
961        cuddDeallocMove(table, moveDown);
962        moveDown = move;
963    }
964    while (moveUp != NULL) {
965        move = moveUp->next;
966        cuddDeallocMove(table, moveUp);
967        moveUp = move;
968    }
969
970    return(1);
971
972ddLinearAndSiftingAuxOutOfMem:
973    while (moveDown != NULL) {
974        move = moveDown->next;
975        cuddDeallocMove(table, moveDown);
976        moveDown = move;
977    }
978    while (moveUp != NULL) {
979        move = moveUp->next;
980        cuddDeallocMove(table, moveUp);
981        moveUp = move;
982    }
983
984    return(0);
985
986} /* end of ddLinearAndSiftingAux */
987
988
989/**Function********************************************************************
990
991  Synopsis    [Sifts a variable up and applies linear transformations.]
992
993  Description [Sifts a variable up and applies linear transformations.
994  Moves y up until either it reaches the bound (xLow) or the size of
995  the DD heap increases too much.  Returns the set of moves in case of
996  success; NULL if memory is full.]
997
998  SideEffects [None]
999
1000******************************************************************************/
1001static Move *
1002ddLinearAndSiftingUp(
1003  DdManager * table,
1004  int  y,
1005  int  xLow,
1006  Move * prevMoves)
1007{
1008    Move        *moves;
1009    Move        *move;
1010    int         x;
1011    int         size, newsize;
1012    int         limitSize;
1013    int         xindex, yindex;
1014    int         isolated;
1015    int         L;      /* lower bound on DD size */
1016#ifdef DD_DEBUG
1017    int checkL;
1018    int z;
1019    int zindex;
1020#endif
1021
1022    moves = prevMoves;
1023    yindex = table->invperm[y];
1024
1025    /* Initialize the lower bound.
1026    ** The part of the DD below y will not change.
1027    ** The part of the DD above y that does not interact with y will not
1028    ** change. The rest may vanish in the best case, except for
1029    ** the nodes at level xLow, which will not vanish, regardless.
1030    */
1031    limitSize = L = table->keys - table->isolated;
1032    for (x = xLow + 1; x < y; x++) {
1033        xindex = table->invperm[x];
1034        if (cuddTestInteract(table,xindex,yindex)) {
1035            isolated = table->vars[xindex]->ref == 1;
1036            L -= table->subtables[x].keys - isolated;
1037        }
1038    }
1039    isolated = table->vars[yindex]->ref == 1;
1040    L -= table->subtables[y].keys - isolated;
1041
1042    x = cuddNextLow(table,y);
1043    while (x >= xLow && L <= limitSize) {
1044        xindex = table->invperm[x];
1045#ifdef DD_DEBUG
1046        checkL = table->keys - table->isolated;
1047        for (z = xLow + 1; z < y; z++) {
1048            zindex = table->invperm[z];
1049            if (cuddTestInteract(table,zindex,yindex)) {
1050                isolated = table->vars[zindex]->ref == 1;
1051                checkL -= table->subtables[z].keys - isolated;
1052            }
1053        }
1054        isolated = table->vars[yindex]->ref == 1;
1055        checkL -= table->subtables[y].keys - isolated;
1056        if (L != checkL) {
1057            (void) fprintf(table->out, "checkL(%d) != L(%d)\n",checkL,L);
1058        }
1059#endif
1060        size = cuddSwapInPlace(table,x,y);
1061        if (size == 0) goto ddLinearAndSiftingUpOutOfMem;
1062        newsize = cuddLinearInPlace(table,x,y);
1063        if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
1064        move = (Move *) cuddDynamicAllocNode(table);
1065        if (move == NULL) goto ddLinearAndSiftingUpOutOfMem;
1066        move->x = x;
1067        move->y = y;
1068        move->next = moves;
1069        moves = move;
1070        move->flags = CUDD_SWAP_MOVE;
1071        if (newsize >= size) {
1072            /* Undo transformation. The transformation we apply is
1073            ** its own inverse. Hence, we just apply the transformation
1074            ** again.
1075            */
1076            newsize = cuddLinearInPlace(table,x,y);
1077            if (newsize == 0) goto ddLinearAndSiftingUpOutOfMem;
1078#ifdef DD_DEBUG
1079            if (newsize != size) {
1080                (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
1081            }
1082#endif
1083        } else if (cuddTestInteract(table,xindex,yindex)) {
1084            size = newsize;
1085            move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1086            cuddUpdateInteractionMatrix(table,xindex,yindex);
1087        }
1088        move->size = size;
1089        /* Update the lower bound. */
1090        if (cuddTestInteract(table,xindex,yindex)) {
1091            isolated = table->vars[xindex]->ref == 1;
1092            L += table->subtables[y].keys - isolated;
1093        }
1094        if ((double) size > (double) limitSize * table->maxGrowth) break;
1095        if (size < limitSize) limitSize = size;
1096        y = x;
1097        x = cuddNextLow(table,y);
1098    }
1099    return(moves);
1100
1101ddLinearAndSiftingUpOutOfMem:
1102    while (moves != NULL) {
1103        move = moves->next;
1104        cuddDeallocMove(table, moves);
1105        moves = move;
1106    }
1107    return((Move *) CUDD_OUT_OF_MEM);
1108
1109} /* end of ddLinearAndSiftingUp */
1110
1111
1112/**Function********************************************************************
1113
1114  Synopsis    [Sifts a variable down and applies linear transformations.]
1115
1116  Description [Sifts a variable down and applies linear
1117  transformations. Moves x down until either it reaches the bound
1118  (xHigh) or the size of the DD heap increases too much. Returns the
1119  set of moves in case of success; NULL if memory is full.]
1120
1121  SideEffects [None]
1122
1123******************************************************************************/
1124static Move *
1125ddLinearAndSiftingDown(
1126  DdManager * table,
1127  int  x,
1128  int  xHigh,
1129  Move * prevMoves)
1130{
1131    Move        *moves;
1132    Move        *move;
1133    int         y;
1134    int         size, newsize;
1135    int         R;      /* upper bound on node decrease */
1136    int         limitSize;
1137    int         xindex, yindex;
1138    int         isolated;
1139#ifdef DD_DEBUG
1140    int         checkR;
1141    int         z;
1142    int         zindex;
1143#endif
1144
1145    moves = prevMoves;
1146    /* Initialize R */
1147    xindex = table->invperm[x];
1148    limitSize = size = table->keys - table->isolated;
1149    R = 0;
1150    for (y = xHigh; y > x; y--) {
1151        yindex = table->invperm[y];
1152        if (cuddTestInteract(table,xindex,yindex)) {
1153            isolated = table->vars[yindex]->ref == 1;
1154            R += table->subtables[y].keys - isolated;
1155        }
1156    }
1157
1158    y = cuddNextHigh(table,x);
1159    while (y <= xHigh && size - R < limitSize) {
1160#ifdef DD_DEBUG
1161        checkR = 0;
1162        for (z = xHigh; z > x; z--) {
1163            zindex = table->invperm[z];
1164            if (cuddTestInteract(table,xindex,zindex)) {
1165                isolated = table->vars[zindex]->ref == 1;
1166                checkR += table->subtables[z].keys - isolated;
1167            }
1168        }
1169        if (R != checkR) {
1170            (void) fprintf(table->out, "checkR(%d) != R(%d)\n",checkR,R);
1171        }
1172#endif
1173        /* Update upper bound on node decrease. */
1174        yindex = table->invperm[y];
1175        if (cuddTestInteract(table,xindex,yindex)) {
1176            isolated = table->vars[yindex]->ref == 1;
1177            R -= table->subtables[y].keys - isolated;
1178        }
1179        size = cuddSwapInPlace(table,x,y);
1180        if (size == 0) goto ddLinearAndSiftingDownOutOfMem;
1181        newsize = cuddLinearInPlace(table,x,y);
1182        if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
1183        move = (Move *) cuddDynamicAllocNode(table);
1184        if (move == NULL) goto ddLinearAndSiftingDownOutOfMem;
1185        move->x = x;
1186        move->y = y;
1187        move->next = moves;
1188        moves = move;
1189        move->flags = CUDD_SWAP_MOVE;
1190        if (newsize >= size) {
1191            /* Undo transformation. The transformation we apply is
1192            ** its own inverse. Hence, we just apply the transformation
1193            ** again.
1194            */
1195            newsize = cuddLinearInPlace(table,x,y);
1196            if (newsize == 0) goto ddLinearAndSiftingDownOutOfMem;
1197            if (newsize != size) {
1198                (void) fprintf(table->out,"Change in size after identity transformation! From %d to %d\n",size,newsize);
1199            }
1200        } else if (cuddTestInteract(table,xindex,yindex)) {
1201            size = newsize;
1202            move->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1203            cuddUpdateInteractionMatrix(table,xindex,yindex);
1204        }
1205        move->size = size;
1206        if ((double) size > (double) limitSize * table->maxGrowth) break;
1207        if (size < limitSize) limitSize = size;
1208        x = y;
1209        y = cuddNextHigh(table,x);
1210    }
1211    return(moves);
1212
1213ddLinearAndSiftingDownOutOfMem:
1214    while (moves != NULL) {
1215        move = moves->next;
1216        cuddDeallocMove(table, moves);
1217        moves = move;
1218    }
1219    return((Move *) CUDD_OUT_OF_MEM);
1220
1221} /* end of ddLinearAndSiftingDown */
1222
1223
1224/**Function********************************************************************
1225
1226  Synopsis    [Given a set of moves, returns the DD heap to the order
1227  giving the minimum size.]
1228
1229  Description [Given a set of moves, returns the DD heap to the
1230  position giving the minimum size. In case of ties, returns to the
1231  closest position giving the minimum size. Returns 1 in case of
1232  success; 0 otherwise.]
1233
1234  SideEffects [None]
1235
1236******************************************************************************/
1237static int
1238ddLinearAndSiftingBackward(
1239  DdManager * table,
1240  int  size,
1241  Move * moves)
1242{
1243    Move *move;
1244    int res;
1245
1246    for (move = moves; move != NULL; move = move->next) {
1247        if (move->size < size) {
1248            size = move->size;
1249        }
1250    }
1251
1252    for (move = moves; move != NULL; move = move->next) {
1253        if (move->size == size) return(1);
1254        if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
1255            res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1256            if (!res) return(0);
1257        }
1258        res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1259        if (!res) return(0);
1260        if (move->flags == CUDD_INVERSE_TRANSFORM_MOVE) {
1261            res = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1262            if (!res) return(0);
1263        }
1264    }
1265
1266    return(1);
1267
1268} /* end of ddLinearAndSiftingBackward */
1269
1270
1271/**Function********************************************************************
1272
1273  Synopsis    [Given a set of moves, returns the DD heap to the order
1274  in effect before the moves.]
1275
1276  Description [Given a set of moves, returns the DD heap to the
1277  order in effect before the moves.  Returns 1 in case of success;
1278  0 otherwise.]
1279
1280  SideEffects [None]
1281
1282******************************************************************************/
1283static Move*
1284ddUndoMoves(
1285  DdManager * table,
1286  Move * moves)
1287{
1288    Move *invmoves = NULL;
1289    Move *move;
1290    Move *invmove;
1291    int size;
1292
1293    for (move = moves; move != NULL; move = move->next) {
1294        invmove = (Move *) cuddDynamicAllocNode(table);
1295        if (invmove == NULL) goto ddUndoMovesOutOfMem;
1296        invmove->x = move->x;
1297        invmove->y = move->y;
1298        invmove->next = invmoves;
1299        invmoves = invmove;
1300        if (move->flags == CUDD_SWAP_MOVE) {
1301            invmove->flags = CUDD_SWAP_MOVE;
1302            size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1303            if (!size) goto ddUndoMovesOutOfMem;
1304        } else if (move->flags == CUDD_LINEAR_TRANSFORM_MOVE) {
1305            invmove->flags = CUDD_INVERSE_TRANSFORM_MOVE;
1306            size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1307            if (!size) goto ddUndoMovesOutOfMem;
1308            size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1309            if (!size) goto ddUndoMovesOutOfMem;
1310        } else { /* must be CUDD_INVERSE_TRANSFORM_MOVE */
1311#ifdef DD_DEBUG
1312            (void) fprintf(table->err,"Unforseen event in ddUndoMoves!\n");
1313#endif
1314            invmove->flags = CUDD_LINEAR_TRANSFORM_MOVE;
1315            size = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1316            if (!size) goto ddUndoMovesOutOfMem;
1317            size = cuddLinearInPlace(table,(int)move->x,(int)move->y);
1318            if (!size) goto ddUndoMovesOutOfMem;
1319        }
1320        invmove->size = size;
1321    }
1322
1323    return(invmoves);
1324
1325ddUndoMovesOutOfMem:
1326    while (invmoves != NULL) {
1327        move = invmoves->next;
1328        cuddDeallocMove(table, invmoves);
1329        invmoves = move;
1330    }
1331    return((Move *) CUDD_OUT_OF_MEM);
1332
1333} /* end of ddUndoMoves */
1334
1335
1336/**Function********************************************************************
1337
1338  Synopsis    [XORs two rows of the linear transform matrix.]
1339
1340  Description [XORs two rows of the linear transform matrix and replaces
1341  the first row with the result.]
1342
1343  SideEffects [none]
1344
1345  SeeAlso     []
1346
1347******************************************************************************/
1348static void
1349cuddXorLinear(
1350  DdManager * table,
1351  int  x,
1352  int  y)
1353{
1354    int i;
1355    int nvars = table->size;
1356    int wordsPerRow = ((nvars - 1) >> LOGBPL) + 1;
1357    int xstart = wordsPerRow * x;
1358    int ystart = wordsPerRow * y;
1359    long *linear = table->linear;
1360
1361    for (i = 0; i < wordsPerRow; i++) {
1362        linear[xstart+i] ^= linear[ystart+i];
1363    }
1364
1365} /* end of cuddXorLinear */
Note: See TracBrowser for help on using the repository browser.