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

Last change on this file since 104 was 13, checked in by cecile, 15 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.