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