1 /**CFile***********************************************************************
2
3 FileName [cuddZddGroup.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions for ZDD group sifting.]
8
9 Description [External procedures included in this file:
10 <ul>
11 <li> Cudd_MakeZddTreeNode()
12 </ul>
13 Internal procedures included in this file:
14 <ul>
15 <li> cuddZddTreeSifting()
16 </ul>
17 Static procedures included in this module:
18 <ul>
19 <li> zddTreeSiftingAux()
20 <li> zddCountInternalMtrNodes()
21 <li> zddReorderChildren()
22 <li> zddFindNodeHiLo()
23 <li> zddUniqueCompareGroup()
24 <li> zddGroupSifting()
25 <li> zddGroupSiftingAux()
26 <li> zddGroupSiftingUp()
27 <li> zddGroupSiftingDown()
28 <li> zddGroupMove()
29 <li> zddGroupMoveBackward()
30 <li> zddGroupSiftingBackward()
31 <li> zddMergeGroups()
32 </ul>]
33
34 Author [Fabio Somenzi]
35
36 Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado
37
38 All rights reserved.
39
40 Redistribution and use in source and binary forms, with or without
41 modification, are permitted provided that the following conditions
42 are met:
43
44 Redistributions of source code must retain the above copyright
45 notice, this list of conditions and the following disclaimer.
46
47 Redistributions in binary form must reproduce the above copyright
48 notice, this list of conditions and the following disclaimer in the
49 documentation and/or other materials provided with the distribution.
50
51 Neither the name of the University of Colorado nor the names of its
52 contributors may be used to endorse or promote products derived from
53 this software without specific prior written permission.
54
55 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
56 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
57 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
58 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
59 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
60 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
61 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
62 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
63 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
64 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
65 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
66 POSSIBILITY OF SUCH DAMAGE.]
67
68 ******************************************************************************/
69
70 #include "util.h"
71 #include "cuddInt.h"
72
73 /*---------------------------------------------------------------------------*/
74 /* Constant declarations */
75 /*---------------------------------------------------------------------------*/
76
77 /*---------------------------------------------------------------------------*/
78 /* Stucture declarations */
79 /*---------------------------------------------------------------------------*/
80
81 /*---------------------------------------------------------------------------*/
82 /* Type declarations */
83 /*---------------------------------------------------------------------------*/
84
85 /*---------------------------------------------------------------------------*/
86 /* Variable declarations */
87 /*---------------------------------------------------------------------------*/
88
89 #ifndef lint
90 static char rcsid[] DD_UNUSED = "$Id: cuddZddGroup.c,v 1.22 2012/02/05 01:07:19 fabio Exp $";
91 #endif
92
93 static int *entry;
94 extern int zddTotalNumberSwapping;
95 #ifdef DD_STATS
96 static int extsymmcalls;
97 static int extsymm;
98 static int secdiffcalls;
99 static int secdiff;
100 static int secdiffmisfire;
101 #endif
102 #ifdef DD_DEBUG
103 static int pr = 0; /* flag to enable printing while debugging */
104 /* by depositing a 1 into it */
105 #endif
106
107 /*---------------------------------------------------------------------------*/
108 /* Macro declarations */
109 /*---------------------------------------------------------------------------*/
110
111 /**AutomaticStart*************************************************************/
112
113 /*---------------------------------------------------------------------------*/
114 /* Static function prototypes */
115 /*---------------------------------------------------------------------------*/
116
117 static int zddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
118 #ifdef DD_STATS
119 static int zddCountInternalMtrNodes (DdManager *table, MtrNode *treenode);
120 #endif
121 static int zddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
122 static void zddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper);
123 static int zddUniqueCompareGroup (int *ptrX, int *ptrY);
124 static int zddGroupSifting (DdManager *table, int lower, int upper);
125 static int zddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh);
126 static int zddGroupSiftingUp (DdManager *table, int y, int xLow, Move **moves);
127 static int zddGroupSiftingDown (DdManager *table, int x, int xHigh, Move **moves);
128 static int zddGroupMove (DdManager *table, int x, int y, Move **moves);
129 static int zddGroupMoveBackward (DdManager *table, int x, int y);
130 static int zddGroupSiftingBackward (DdManager *table, Move *moves, int size);
131 static void zddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high);
132
133 /**AutomaticEnd***************************************************************/
134
135
136 /*---------------------------------------------------------------------------*/
137 /* Definition of exported functions */
138 /*---------------------------------------------------------------------------*/
139
140
141 /**Function********************************************************************
142
143 Synopsis [Creates a new ZDD variable group.]
144
145 Description [Creates a new ZDD variable group. The group starts at
146 variable and contains size variables. The parameter low is the index
147 of the first variable. If the variable already exists, its current
148 position in the order is known to the manager. If the variable does
149 not exist yet, the position is assumed to be the same as the index.
150 The group tree is created if it does not exist yet.
151 Returns a pointer to the group if successful; NULL otherwise.]
152
153 SideEffects [The ZDD variable tree is changed.]
154
155 SeeAlso [Cudd_MakeTreeNode]
156
157 ******************************************************************************/
158 MtrNode *
Cudd_MakeZddTreeNode(DdManager * dd,unsigned int low,unsigned int size,unsigned int type)159 Cudd_MakeZddTreeNode(
160 DdManager * dd /* manager */,
161 unsigned int low /* index of the first group variable */,
162 unsigned int size /* number of variables in the group */,
163 unsigned int type /* MTR_DEFAULT or MTR_FIXED */)
164 {
165 MtrNode *group;
166 MtrNode *tree;
167 unsigned int level;
168
169 /* If the variable does not exist yet, the position is assumed to be
170 ** the same as the index. Therefore, applications that rely on
171 ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
172 ** variables have to create the variables before they group them.
173 */
174 level = (low < (unsigned int) dd->sizeZ) ? dd->permZ[low] : low;
175
176 if (level + size - 1> (int) MTR_MAXHIGH)
177 return(NULL);
178
179 /* If the tree does not exist yet, create it. */
180 tree = dd->treeZ;
181 if (tree == NULL) {
182 dd->treeZ = tree = Mtr_InitGroupTree(0, dd->sizeZ);
183 if (tree == NULL)
184 return(NULL);
185 tree->index = dd->invpermZ[0];
186 }
187
188 /* Extend the upper bound of the tree if necessary. This allows the
189 ** application to create groups even before the variables are created.
190 */
191 tree->size = ddMax(tree->size, level + size);
192
193 /* Create the group. */
194 group = Mtr_MakeGroup(tree, level, size, type);
195 if (group == NULL)
196 return(NULL);
197
198 /* Initialize the index field to the index of the variable currently
199 ** in position low. This field will be updated by the reordering
200 ** procedure to provide a handle to the group once it has been moved.
201 */
202 group->index = (MtrHalfWord) low;
203
204 return(group);
205
206 } /* end of Cudd_MakeZddTreeNode */
207
208
209 /*---------------------------------------------------------------------------*/
210 /* Definition of internal functions */
211 /*---------------------------------------------------------------------------*/
212
213
214 /**Function********************************************************************
215
216 Synopsis [Tree sifting algorithm for ZDDs.]
217
218 Description [Tree sifting algorithm for ZDDs. Assumes that a tree
219 representing a group hierarchy is passed as a parameter. It then
220 reorders each group in postorder fashion by calling
221 zddTreeSiftingAux. Assumes that no dead nodes are present. Returns
222 1 if successful; 0 otherwise.]
223
224 SideEffects [None]
225
226 ******************************************************************************/
227 int
cuddZddTreeSifting(DdManager * table,Cudd_ReorderingType method)228 cuddZddTreeSifting(
229 DdManager * table /* DD table */,
230 Cudd_ReorderingType method /* reordering method for the groups of leaves */)
231 {
232 int i;
233 int nvars;
234 int result;
235 int tempTree;
236
237 /* If no tree is provided we create a temporary one in which all
238 ** variables are in a single group. After reordering this tree is
239 ** destroyed.
240 */
241 tempTree = table->treeZ == NULL;
242 if (tempTree) {
243 table->treeZ = Mtr_InitGroupTree(0,table->sizeZ);
244 table->treeZ->index = table->invpermZ[0];
245 }
246 nvars = table->sizeZ;
247
248 #ifdef DD_DEBUG
249 if (pr > 0 && !tempTree)
250 (void) fprintf(table->out,"cuddZddTreeSifting:");
251 Mtr_PrintGroups(table->treeZ,pr <= 0);
252 #endif
253 #if 0
254 /* Debugging code. */
255 if (table->tree && table->treeZ) {
256 (void) fprintf(table->out,"\n");
257 Mtr_PrintGroups(table->tree, 0);
258 cuddPrintVarGroups(table,table->tree,0,0);
259 for (i = 0; i < table->size; i++) {
260 (void) fprintf(table->out,"%s%d",
261 (i == 0) ? "" : ",", table->invperm[i]);
262 }
263 (void) fprintf(table->out,"\n");
264 for (i = 0; i < table->size; i++) {
265 (void) fprintf(table->out,"%s%d",
266 (i == 0) ? "" : ",", table->perm[i]);
267 }
268 (void) fprintf(table->out,"\n\n");
269 Mtr_PrintGroups(table->treeZ,0);
270 cuddPrintVarGroups(table,table->treeZ,1,0);
271 for (i = 0; i < table->sizeZ; i++) {
272 (void) fprintf(table->out,"%s%d",
273 (i == 0) ? "" : ",", table->invpermZ[i]);
274 }
275 (void) fprintf(table->out,"\n");
276 for (i = 0; i < table->sizeZ; i++) {
277 (void) fprintf(table->out,"%s%d",
278 (i == 0) ? "" : ",", table->permZ[i]);
279 }
280 (void) fprintf(table->out,"\n");
281 }
282 /* End of debugging code. */
283 #endif
284 #ifdef DD_STATS
285 extsymmcalls = 0;
286 extsymm = 0;
287 secdiffcalls = 0;
288 secdiff = 0;
289 secdiffmisfire = 0;
290
291 (void) fprintf(table->out,"\n");
292 if (!tempTree)
293 (void) fprintf(table->out,"#:IM_NODES %8d: group tree nodes\n",
294 zddCountInternalMtrNodes(table,table->treeZ));
295 #endif
296
297 /* Initialize the group of each subtable to itself. Initially
298 ** there are no groups. Groups are created according to the tree
299 ** structure in postorder fashion.
300 */
301 for (i = 0; i < nvars; i++)
302 table->subtableZ[i].next = i;
303
304 /* Reorder. */
305 result = zddTreeSiftingAux(table, table->treeZ, method);
306
307 #ifdef DD_STATS /* print stats */
308 if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
309 (table->groupcheck == CUDD_GROUP_CHECK7 ||
310 table->groupcheck == CUDD_GROUP_CHECK5)) {
311 (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
312 (void) fprintf(table->out,"extsymm = %d",extsymm);
313 }
314 if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
315 table->groupcheck == CUDD_GROUP_CHECK7) {
316 (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
317 (void) fprintf(table->out,"secdiff = %d\n",secdiff);
318 (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
319 }
320 #endif
321
322 if (tempTree)
323 Cudd_FreeZddTree(table);
324 return(result);
325
326 } /* end of cuddZddTreeSifting */
327
328
329 /*---------------------------------------------------------------------------*/
330 /* Definition of static functions */
331 /*---------------------------------------------------------------------------*/
332
333
334 /**Function********************************************************************
335
336 Synopsis [Visits the group tree and reorders each group.]
337
338 Description [Recursively visits the group tree and reorders each
339 group in postorder fashion. Returns 1 if successful; 0 otherwise.]
340
341 SideEffects [None]
342
343 ******************************************************************************/
344 static int
zddTreeSiftingAux(DdManager * table,MtrNode * treenode,Cudd_ReorderingType method)345 zddTreeSiftingAux(
346 DdManager * table,
347 MtrNode * treenode,
348 Cudd_ReorderingType method)
349 {
350 MtrNode *auxnode;
351 int res;
352
353 #ifdef DD_DEBUG
354 Mtr_PrintGroups(treenode,1);
355 #endif
356
357 auxnode = treenode;
358 while (auxnode != NULL) {
359 if (auxnode->child != NULL) {
360 if (!zddTreeSiftingAux(table, auxnode->child, method))
361 return(0);
362 res = zddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
363 if (res == 0)
364 return(0);
365 } else if (auxnode->size > 1) {
366 if (!zddReorderChildren(table, auxnode, method))
367 return(0);
368 }
369 auxnode = auxnode->younger;
370 }
371
372 return(1);
373
374 } /* end of zddTreeSiftingAux */
375
376
377 #ifdef DD_STATS
378 /**Function********************************************************************
379
380 Synopsis [Counts the number of internal nodes of the group tree.]
381
382 Description [Counts the number of internal nodes of the group tree.
383 Returns the count.]
384
385 SideEffects [None]
386
387 ******************************************************************************/
388 static int
zddCountInternalMtrNodes(DdManager * table,MtrNode * treenode)389 zddCountInternalMtrNodes(
390 DdManager * table,
391 MtrNode * treenode)
392 {
393 MtrNode *auxnode;
394 int count,nodeCount;
395
396
397 nodeCount = 0;
398 auxnode = treenode;
399 while (auxnode != NULL) {
400 if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
401 nodeCount++;
402 count = zddCountInternalMtrNodes(table,auxnode->child);
403 nodeCount += count;
404 }
405 auxnode = auxnode->younger;
406 }
407
408 return(nodeCount);
409
410 } /* end of zddCountInternalMtrNodes */
411 #endif
412
413
414 /**Function********************************************************************
415
416 Synopsis [Reorders the children of a group tree node according to
417 the options.]
418
419 Description [Reorders the children of a group tree node according to
420 the options. After reordering puts all the variables in the group
421 and/or its descendents in a single group. This allows hierarchical
422 reordering. If the variables in the group do not exist yet, simply
423 does nothing. Returns 1 if successful; 0 otherwise.]
424
425 SideEffects [None]
426
427 ******************************************************************************/
428 static int
zddReorderChildren(DdManager * table,MtrNode * treenode,Cudd_ReorderingType method)429 zddReorderChildren(
430 DdManager * table,
431 MtrNode * treenode,
432 Cudd_ReorderingType method)
433 {
434 int lower;
435 int upper;
436 int result;
437 unsigned int initialSize;
438
439 zddFindNodeHiLo(table,treenode,&lower,&upper);
440 /* If upper == -1 these variables do not exist yet. */
441 if (upper == -1)
442 return(1);
443
444 if (treenode->flags == MTR_FIXED) {
445 result = 1;
446 } else {
447 #ifdef DD_STATS
448 (void) fprintf(table->out," ");
449 #endif
450 switch (method) {
451 case CUDD_REORDER_RANDOM:
452 case CUDD_REORDER_RANDOM_PIVOT:
453 result = cuddZddSwapping(table,lower,upper,method);
454 break;
455 case CUDD_REORDER_SIFT:
456 result = cuddZddSifting(table,lower,upper);
457 break;
458 case CUDD_REORDER_SIFT_CONVERGE:
459 do {
460 initialSize = table->keysZ;
461 result = cuddZddSifting(table,lower,upper);
462 if (initialSize <= table->keysZ)
463 break;
464 #ifdef DD_STATS
465 else
466 (void) fprintf(table->out,"\n");
467 #endif
468 } while (result != 0);
469 break;
470 case CUDD_REORDER_SYMM_SIFT:
471 result = cuddZddSymmSifting(table,lower,upper);
472 break;
473 case CUDD_REORDER_SYMM_SIFT_CONV:
474 result = cuddZddSymmSiftingConv(table,lower,upper);
475 break;
476 case CUDD_REORDER_GROUP_SIFT:
477 result = zddGroupSifting(table,lower,upper);
478 break;
479 case CUDD_REORDER_LINEAR:
480 result = cuddZddLinearSifting(table,lower,upper);
481 break;
482 case CUDD_REORDER_LINEAR_CONVERGE:
483 do {
484 initialSize = table->keysZ;
485 result = cuddZddLinearSifting(table,lower,upper);
486 if (initialSize <= table->keysZ)
487 break;
488 #ifdef DD_STATS
489 else
490 (void) fprintf(table->out,"\n");
491 #endif
492 } while (result != 0);
493 break;
494 default:
495 return(0);
496 }
497 }
498
499 /* Create a single group for all the variables that were sifted,
500 ** so that they will be treated as a single block by successive
501 ** invocations of zddGroupSifting.
502 */
503 zddMergeGroups(table,treenode,lower,upper);
504
505 #ifdef DD_DEBUG
506 if (pr > 0) (void) fprintf(table->out,"zddReorderChildren:");
507 #endif
508
509 return(result);
510
511 } /* end of zddReorderChildren */
512
513
514 /**Function********************************************************************
515
516 Synopsis [Finds the lower and upper bounds of the group represented
517 by treenode.]
518
519 Description [Finds the lower and upper bounds of the group represented
520 by treenode. The high and low fields of treenode are indices. From
521 those we need to derive the current positions, and find maximum and
522 minimum.]
523
524 SideEffects [The bounds are returned as side effects.]
525
526 SeeAlso []
527
528 ******************************************************************************/
529 static void
zddFindNodeHiLo(DdManager * table,MtrNode * treenode,int * lower,int * upper)530 zddFindNodeHiLo(
531 DdManager * table,
532 MtrNode * treenode,
533 int * lower,
534 int * upper)
535 {
536 int low;
537 int high;
538
539 /* Check whether no variables in this group already exist.
540 ** If so, return immediately. The calling procedure will know from
541 ** the values of upper that no reordering is needed.
542 */
543 if ((int) treenode->low >= table->sizeZ) {
544 *lower = table->sizeZ;
545 *upper = -1;
546 return;
547 }
548
549 *lower = low = (unsigned int) table->permZ[treenode->index];
550 high = (int) (low + treenode->size - 1);
551
552 if (high >= table->sizeZ) {
553 /* This is the case of a partially existing group. The aim is to
554 ** reorder as many variables as safely possible. If the tree
555 ** node is terminal, we just reorder the subset of the group
556 ** that is currently in existence. If the group has
557 ** subgroups, then we only reorder those subgroups that are
558 ** fully instantiated. This way we avoid breaking up a group.
559 */
560 MtrNode *auxnode = treenode->child;
561 if (auxnode == NULL) {
562 *upper = (unsigned int) table->sizeZ - 1;
563 } else {
564 /* Search the subgroup that strands the table->sizeZ line.
565 ** If the first group starts at 0 and goes past table->sizeZ
566 ** upper will get -1, thus correctly signaling that no reordering
567 ** should take place.
568 */
569 while (auxnode != NULL) {
570 int thisLower = table->permZ[auxnode->low];
571 int thisUpper = thisLower + auxnode->size - 1;
572 if (thisUpper >= table->sizeZ && thisLower < table->sizeZ)
573 *upper = (unsigned int) thisLower - 1;
574 auxnode = auxnode->younger;
575 }
576 }
577 } else {
578 /* Normal case: All the variables of the group exist. */
579 *upper = (unsigned int) high;
580 }
581
582 #ifdef DD_DEBUG
583 /* Make sure that all variables in group are contiguous. */
584 assert(treenode->size >= *upper - *lower + 1);
585 #endif
586
587 return;
588
589 } /* end of zddFindNodeHiLo */
590
591
592 /**Function********************************************************************
593
594 Synopsis [Comparison function used by qsort.]
595
596 Description [Comparison function used by qsort to order the variables
597 according to the number of keys in the subtables. Returns the
598 difference in number of keys between the two variables being
599 compared.]
600
601 SideEffects [None]
602
603 ******************************************************************************/
604 static int
zddUniqueCompareGroup(int * ptrX,int * ptrY)605 zddUniqueCompareGroup(
606 int * ptrX,
607 int * ptrY)
608 {
609 #if 0
610 if (entry[*ptrY] == entry[*ptrX]) {
611 return((*ptrX) - (*ptrY));
612 }
613 #endif
614 return(entry[*ptrY] - entry[*ptrX]);
615
616 } /* end of zddUniqueCompareGroup */
617
618
619 /**Function********************************************************************
620
621 Synopsis [Sifts from treenode->low to treenode->high.]
622
623 Description [Sifts from treenode->low to treenode->high. If
624 croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
625 end of the initial sifting. If a group is created, it is then sifted
626 again. After sifting one variable, the group that contains it is
627 dissolved. Returns 1 in case of success; 0 otherwise.]
628
629 SideEffects [None]
630
631 ******************************************************************************/
632 static int
zddGroupSifting(DdManager * table,int lower,int upper)633 zddGroupSifting(
634 DdManager * table,
635 int lower,
636 int upper)
637 {
638 int *var;
639 int i,j,x,xInit;
640 int nvars;
641 int classes;
642 int result;
643 int *sifted;
644 #ifdef DD_STATS
645 unsigned previousSize;
646 #endif
647 int xindex;
648
649 nvars = table->sizeZ;
650
651 /* Order variables to sift. */
652 entry = NULL;
653 sifted = NULL;
654 var = ALLOC(int,nvars);
655 if (var == NULL) {
656 table->errorCode = CUDD_MEMORY_OUT;
657 goto zddGroupSiftingOutOfMem;
658 }
659 entry = ALLOC(int,nvars);
660 if (entry == NULL) {
661 table->errorCode = CUDD_MEMORY_OUT;
662 goto zddGroupSiftingOutOfMem;
663 }
664 sifted = ALLOC(int,nvars);
665 if (sifted == NULL) {
666 table->errorCode = CUDD_MEMORY_OUT;
667 goto zddGroupSiftingOutOfMem;
668 }
669
670 /* Here we consider only one representative for each group. */
671 for (i = 0, classes = 0; i < nvars; i++) {
672 sifted[i] = 0;
673 x = table->permZ[i];
674 if ((unsigned) x >= table->subtableZ[x].next) {
675 entry[i] = table->subtableZ[x].keys;
676 var[classes] = i;
677 classes++;
678 }
679 }
680
681 qsort((void *)var,classes,sizeof(int),(DD_QSFP)zddUniqueCompareGroup);
682
683 /* Now sift. */
684 for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
685 if (zddTotalNumberSwapping >= table->siftMaxSwap)
686 break;
687 if (util_cpu_time() - table->startTime > table->timeLimit) {
688 table->autoDynZ = 0; /* prevent further reordering */
689 break;
690 }
691 xindex = var[i];
692 if (sifted[xindex] == 1) /* variable already sifted as part of group */
693 continue;
694 x = table->permZ[xindex]; /* find current level of this variable */
695 if (x < lower || x > upper)
696 continue;
697 #ifdef DD_STATS
698 previousSize = table->keysZ;
699 #endif
700 #ifdef DD_DEBUG
701 /* x is bottom of group */
702 assert((unsigned) x >= table->subtableZ[x].next);
703 #endif
704 result = zddGroupSiftingAux(table,x,lower,upper);
705 if (!result) goto zddGroupSiftingOutOfMem;
706
707 #ifdef DD_STATS
708 if (table->keysZ < previousSize) {
709 (void) fprintf(table->out,"-");
710 } else if (table->keysZ > previousSize) {
711 (void) fprintf(table->out,"+");
712 } else {
713 (void) fprintf(table->out,"=");
714 }
715 fflush(table->out);
716 #endif
717
718 /* Mark variables in the group just sifted. */
719 x = table->permZ[xindex];
720 if ((unsigned) x != table->subtableZ[x].next) {
721 xInit = x;
722 do {
723 j = table->invpermZ[x];
724 sifted[j] = 1;
725 x = table->subtableZ[x].next;
726 } while (x != xInit);
727 }
728
729 #ifdef DD_DEBUG
730 if (pr > 0) (void) fprintf(table->out,"zddGroupSifting:");
731 #endif
732 } /* for */
733
734 FREE(sifted);
735 FREE(var);
736 FREE(entry);
737
738 return(1);
739
740 zddGroupSiftingOutOfMem:
741 if (entry != NULL) FREE(entry);
742 if (var != NULL) FREE(var);
743 if (sifted != NULL) FREE(sifted);
744
745 return(0);
746
747 } /* end of zddGroupSifting */
748
749
750 /**Function********************************************************************
751
752 Synopsis [Sifts one variable up and down until it has taken all
753 positions. Checks for aggregation.]
754
755 Description [Sifts one variable up and down until it has taken all
756 positions. Checks for aggregation. There may be at most two sweeps,
757 even if the group grows. Assumes that x is either an isolated
758 variable, or it is the bottom of a group. All groups may not have
759 been found. The variable being moved is returned to the best position
760 seen during sifting. Returns 1 in case of success; 0 otherwise.]
761
762 SideEffects [None]
763
764 ******************************************************************************/
765 static int
zddGroupSiftingAux(DdManager * table,int x,int xLow,int xHigh)766 zddGroupSiftingAux(
767 DdManager * table,
768 int x,
769 int xLow,
770 int xHigh)
771 {
772 Move *move;
773 Move *moves; /* list of moves */
774 int initialSize;
775 int result;
776
777
778 #ifdef DD_DEBUG
779 if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingAux from %d to %d\n",xLow,xHigh);
780 assert((unsigned) x >= table->subtableZ[x].next); /* x is bottom of group */
781 #endif
782
783 initialSize = table->keysZ;
784 moves = NULL;
785
786 if (x == xLow) { /* Sift down */
787 #ifdef DD_DEBUG
788 /* x must be a singleton */
789 assert((unsigned) x == table->subtableZ[x].next);
790 #endif
791 if (x == xHigh) return(1); /* just one variable */
792
793 if (!zddGroupSiftingDown(table,x,xHigh,&moves))
794 goto zddGroupSiftingAuxOutOfMem;
795 /* at this point x == xHigh, unless early term */
796
797 /* move backward and stop at best position */
798 result = zddGroupSiftingBackward(table,moves,initialSize);
799 #ifdef DD_DEBUG
800 assert(table->keysZ <= (unsigned) initialSize);
801 #endif
802 if (!result) goto zddGroupSiftingAuxOutOfMem;
803
804 } else if (cuddZddNextHigh(table,x) > xHigh) { /* Sift up */
805 #ifdef DD_DEBUG
806 /* x is bottom of group */
807 assert((unsigned) x >= table->subtableZ[x].next);
808 #endif
809 /* Find top of x's group */
810 x = table->subtableZ[x].next;
811
812 if (!zddGroupSiftingUp(table,x,xLow,&moves))
813 goto zddGroupSiftingAuxOutOfMem;
814 /* at this point x == xLow, unless early term */
815
816 /* move backward and stop at best position */
817 result = zddGroupSiftingBackward(table,moves,initialSize);
818 #ifdef DD_DEBUG
819 assert(table->keysZ <= (unsigned) initialSize);
820 #endif
821 if (!result) goto zddGroupSiftingAuxOutOfMem;
822
823 } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
824 if (!zddGroupSiftingDown(table,x,xHigh,&moves))
825 goto zddGroupSiftingAuxOutOfMem;
826 /* at this point x == xHigh, unless early term */
827
828 /* Find top of group */
829 if (moves) {
830 x = moves->y;
831 }
832 while ((unsigned) x < table->subtableZ[x].next)
833 x = table->subtableZ[x].next;
834 x = table->subtableZ[x].next;
835 #ifdef DD_DEBUG
836 /* x should be the top of a group */
837 assert((unsigned) x <= table->subtableZ[x].next);
838 #endif
839
840 if (!zddGroupSiftingUp(table,x,xLow,&moves))
841 goto zddGroupSiftingAuxOutOfMem;
842
843 /* move backward and stop at best position */
844 result = zddGroupSiftingBackward(table,moves,initialSize);
845 #ifdef DD_DEBUG
846 assert(table->keysZ <= (unsigned) initialSize);
847 #endif
848 if (!result) goto zddGroupSiftingAuxOutOfMem;
849
850 } else { /* moving up first: shorter */
851 /* Find top of x's group */
852 x = table->subtableZ[x].next;
853
854 if (!zddGroupSiftingUp(table,x,xLow,&moves))
855 goto zddGroupSiftingAuxOutOfMem;
856 /* at this point x == xHigh, unless early term */
857
858 if (moves) {
859 x = moves->x;
860 }
861 while ((unsigned) x < table->subtableZ[x].next)
862 x = table->subtableZ[x].next;
863 #ifdef DD_DEBUG
864 /* x is bottom of a group */
865 assert((unsigned) x >= table->subtableZ[x].next);
866 #endif
867
868 if (!zddGroupSiftingDown(table,x,xHigh,&moves))
869 goto zddGroupSiftingAuxOutOfMem;
870
871 /* move backward and stop at best position */
872 result = zddGroupSiftingBackward(table,moves,initialSize);
873 #ifdef DD_DEBUG
874 assert(table->keysZ <= (unsigned) initialSize);
875 #endif
876 if (!result) goto zddGroupSiftingAuxOutOfMem;
877 }
878
879 while (moves != NULL) {
880 move = moves->next;
881 cuddDeallocMove(table, moves);
882 moves = move;
883 }
884
885 return(1);
886
887 zddGroupSiftingAuxOutOfMem:
888 while (moves != NULL) {
889 move = moves->next;
890 cuddDeallocMove(table, moves);
891 moves = move;
892 }
893
894 return(0);
895
896 } /* end of zddGroupSiftingAux */
897
898
899 /**Function********************************************************************
900
901 Synopsis [Sifts up a variable until either it reaches position xLow
902 or the size of the DD heap increases too much.]
903
904 Description [Sifts up a variable until either it reaches position
905 xLow or the size of the DD heap increases too much. Assumes that y is
906 the top of a group (or a singleton). Checks y for aggregation to the
907 adjacent variables. Records all the moves that are appended to the
908 list of moves received as input and returned as a side effect.
909 Returns 1 in case of success; 0 otherwise.]
910
911 SideEffects [None]
912
913 ******************************************************************************/
914 static int
zddGroupSiftingUp(DdManager * table,int y,int xLow,Move ** moves)915 zddGroupSiftingUp(
916 DdManager * table,
917 int y,
918 int xLow,
919 Move ** moves)
920 {
921 Move *move;
922 int x;
923 int size;
924 int gxtop;
925 int limitSize;
926
927 limitSize = table->keysZ;
928
929 x = cuddZddNextLow(table,y);
930 while (x >= xLow) {
931 gxtop = table->subtableZ[x].next;
932 if (table->subtableZ[x].next == (unsigned) x &&
933 table->subtableZ[y].next == (unsigned) y) {
934 /* x and y are self groups */
935 size = cuddZddSwapInPlace(table,x,y);
936 #ifdef DD_DEBUG
937 assert(table->subtableZ[x].next == (unsigned) x);
938 assert(table->subtableZ[y].next == (unsigned) y);
939 #endif
940 if (size == 0) goto zddGroupSiftingUpOutOfMem;
941 move = (Move *)cuddDynamicAllocNode(table);
942 if (move == NULL) goto zddGroupSiftingUpOutOfMem;
943 move->x = x;
944 move->y = y;
945 move->flags = MTR_DEFAULT;
946 move->size = size;
947 move->next = *moves;
948 *moves = move;
949
950 #ifdef DD_DEBUG
951 if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingUp (2 single groups):\n");
952 #endif
953 if ((double) size > (double) limitSize * table->maxGrowth)
954 return(1);
955 if (size < limitSize) limitSize = size;
956 } else { /* group move */
957 size = zddGroupMove(table,x,y,moves);
958 if (size == 0) goto zddGroupSiftingUpOutOfMem;
959 if ((double) size > (double) limitSize * table->maxGrowth)
960 return(1);
961 if (size < limitSize) limitSize = size;
962 }
963 y = gxtop;
964 x = cuddZddNextLow(table,y);
965 }
966
967 return(1);
968
969 zddGroupSiftingUpOutOfMem:
970 while (*moves != NULL) {
971 move = (*moves)->next;
972 cuddDeallocMove(table, *moves);
973 *moves = move;
974 }
975 return(0);
976
977 } /* end of zddGroupSiftingUp */
978
979
980 /**Function********************************************************************
981
982 Synopsis [Sifts down a variable until it reaches position xHigh.]
983
984 Description [Sifts down a variable until it reaches position xHigh.
985 Assumes that x is the bottom of a group (or a singleton). Records
986 all the moves. Returns 1 in case of success; 0 otherwise.]
987
988 SideEffects [None]
989
990 ******************************************************************************/
991 static int
zddGroupSiftingDown(DdManager * table,int x,int xHigh,Move ** moves)992 zddGroupSiftingDown(
993 DdManager * table,
994 int x,
995 int xHigh,
996 Move ** moves)
997 {
998 Move *move;
999 int y;
1000 int size;
1001 int limitSize;
1002 int gybot;
1003
1004
1005 /* Initialize R */
1006 limitSize = size = table->keysZ;
1007 y = cuddZddNextHigh(table,x);
1008 while (y <= xHigh) {
1009 /* Find bottom of y group. */
1010 gybot = table->subtableZ[y].next;
1011 while (table->subtableZ[gybot].next != (unsigned) y)
1012 gybot = table->subtableZ[gybot].next;
1013
1014 if (table->subtableZ[x].next == (unsigned) x &&
1015 table->subtableZ[y].next == (unsigned) y) {
1016 /* x and y are self groups */
1017 size = cuddZddSwapInPlace(table,x,y);
1018 #ifdef DD_DEBUG
1019 assert(table->subtableZ[x].next == (unsigned) x);
1020 assert(table->subtableZ[y].next == (unsigned) y);
1021 #endif
1022 if (size == 0) goto zddGroupSiftingDownOutOfMem;
1023
1024 /* Record move. */
1025 move = (Move *) cuddDynamicAllocNode(table);
1026 if (move == NULL) goto zddGroupSiftingDownOutOfMem;
1027 move->x = x;
1028 move->y = y;
1029 move->flags = MTR_DEFAULT;
1030 move->size = size;
1031 move->next = *moves;
1032 *moves = move;
1033
1034 #ifdef DD_DEBUG
1035 if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingDown (2 single groups):\n");
1036 #endif
1037 if ((double) size > (double) limitSize * table->maxGrowth)
1038 return(1);
1039 if (size < limitSize) limitSize = size;
1040 x = y;
1041 y = cuddZddNextHigh(table,x);
1042 } else { /* Group move */
1043 size = zddGroupMove(table,x,y,moves);
1044 if (size == 0) goto zddGroupSiftingDownOutOfMem;
1045 if ((double) size > (double) limitSize * table->maxGrowth)
1046 return(1);
1047 if (size < limitSize) limitSize = size;
1048 }
1049 x = gybot;
1050 y = cuddZddNextHigh(table,x);
1051 }
1052
1053 return(1);
1054
1055 zddGroupSiftingDownOutOfMem:
1056 while (*moves != NULL) {
1057 move = (*moves)->next;
1058 cuddDeallocMove(table, *moves);
1059 *moves = move;
1060 }
1061
1062 return(0);
1063
1064 } /* end of zddGroupSiftingDown */
1065
1066
1067 /**Function********************************************************************
1068
1069 Synopsis [Swaps two groups and records the move.]
1070
1071 Description [Swaps two groups and records the move. Returns the
1072 number of keys in the DD table in case of success; 0 otherwise.]
1073
1074 SideEffects [None]
1075
1076 ******************************************************************************/
1077 static int
zddGroupMove(DdManager * table,int x,int y,Move ** moves)1078 zddGroupMove(
1079 DdManager * table,
1080 int x,
1081 int y,
1082 Move ** moves)
1083 {
1084 Move *move;
1085 int size;
1086 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1087 int swapx,swapy;
1088 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1089 int initialSize,bestSize;
1090 #endif
1091
1092 #ifdef DD_DEBUG
1093 /* We assume that x < y */
1094 assert(x < y);
1095 #endif
1096 /* Find top, bottom, and size for the two groups. */
1097 xbot = x;
1098 xtop = table->subtableZ[x].next;
1099 xsize = xbot - xtop + 1;
1100 ybot = y;
1101 while ((unsigned) ybot < table->subtableZ[ybot].next)
1102 ybot = table->subtableZ[ybot].next;
1103 ytop = y;
1104 ysize = ybot - ytop + 1;
1105
1106 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1107 initialSize = bestSize = table->keysZ;
1108 #endif
1109 /* Sift the variables of the second group up through the first group */
1110 for (i = 1; i <= ysize; i++) {
1111 for (j = 1; j <= xsize; j++) {
1112 size = cuddZddSwapInPlace(table,x,y);
1113 if (size == 0) goto zddGroupMoveOutOfMem;
1114 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1115 if (size < bestSize)
1116 bestSize = size;
1117 #endif
1118 swapx = x; swapy = y;
1119 y = x;
1120 x = cuddZddNextLow(table,y);
1121 }
1122 y = ytop + i;
1123 x = cuddZddNextLow(table,y);
1124 }
1125 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1126 if ((bestSize < initialSize) && (bestSize < size))
1127 (void) fprintf(table->out,"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size);
1128 #endif
1129
1130 /* fix groups */
1131 y = xtop; /* ytop is now where xtop used to be */
1132 for (i = 0; i < ysize - 1; i++) {
1133 table->subtableZ[y].next = cuddZddNextHigh(table,y);
1134 y = cuddZddNextHigh(table,y);
1135 }
1136 table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1137 /* it to top of its group */
1138 x = cuddZddNextHigh(table,y);
1139 newxtop = x;
1140 for (i = 0; i < xsize - 1; i++) {
1141 table->subtableZ[x].next = cuddZddNextHigh(table,x);
1142 x = cuddZddNextHigh(table,x);
1143 }
1144 table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1145 /* it to top of its group */
1146 #ifdef DD_DEBUG
1147 if (pr > 0) (void) fprintf(table->out,"zddGroupMove:\n");
1148 #endif
1149
1150 /* Store group move */
1151 move = (Move *) cuddDynamicAllocNode(table);
1152 if (move == NULL) goto zddGroupMoveOutOfMem;
1153 move->x = swapx;
1154 move->y = swapy;
1155 move->flags = MTR_DEFAULT;
1156 move->size = table->keysZ;
1157 move->next = *moves;
1158 *moves = move;
1159
1160 return(table->keysZ);
1161
1162 zddGroupMoveOutOfMem:
1163 while (*moves != NULL) {
1164 move = (*moves)->next;
1165 cuddDeallocMove(table, *moves);
1166 *moves = move;
1167 }
1168 return(0);
1169
1170 } /* end of zddGroupMove */
1171
1172
1173 /**Function********************************************************************
1174
1175 Synopsis [Undoes the swap two groups.]
1176
1177 Description [Undoes the swap two groups. Returns 1 in case of
1178 success; 0 otherwise.]
1179
1180 SideEffects [None]
1181
1182 ******************************************************************************/
1183 static int
zddGroupMoveBackward(DdManager * table,int x,int y)1184 zddGroupMoveBackward(
1185 DdManager * table,
1186 int x,
1187 int y)
1188 {
1189 int size;
1190 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1191
1192
1193 #ifdef DD_DEBUG
1194 /* We assume that x < y */
1195 assert(x < y);
1196 #endif
1197
1198 /* Find top, bottom, and size for the two groups. */
1199 xbot = x;
1200 xtop = table->subtableZ[x].next;
1201 xsize = xbot - xtop + 1;
1202 ybot = y;
1203 while ((unsigned) ybot < table->subtableZ[ybot].next)
1204 ybot = table->subtableZ[ybot].next;
1205 ytop = y;
1206 ysize = ybot - ytop + 1;
1207
1208 /* Sift the variables of the second group up through the first group */
1209 for (i = 1; i <= ysize; i++) {
1210 for (j = 1; j <= xsize; j++) {
1211 size = cuddZddSwapInPlace(table,x,y);
1212 if (size == 0)
1213 return(0);
1214 y = x;
1215 x = cuddZddNextLow(table,y);
1216 }
1217 y = ytop + i;
1218 x = cuddZddNextLow(table,y);
1219 }
1220
1221 /* fix groups */
1222 y = xtop;
1223 for (i = 0; i < ysize - 1; i++) {
1224 table->subtableZ[y].next = cuddZddNextHigh(table,y);
1225 y = cuddZddNextHigh(table,y);
1226 }
1227 table->subtableZ[y].next = xtop; /* y is bottom of its group, join */
1228 /* to its top */
1229 x = cuddZddNextHigh(table,y);
1230 newxtop = x;
1231 for (i = 0; i < xsize - 1; i++) {
1232 table->subtableZ[x].next = cuddZddNextHigh(table,x);
1233 x = cuddZddNextHigh(table,x);
1234 }
1235 table->subtableZ[x].next = newxtop; /* x is bottom of its group, join */
1236 /* to its top */
1237 #ifdef DD_DEBUG
1238 if (pr > 0) (void) fprintf(table->out,"zddGroupMoveBackward:\n");
1239 #endif
1240
1241 return(1);
1242
1243 } /* end of zddGroupMoveBackward */
1244
1245
1246 /**Function********************************************************************
1247
1248 Synopsis [Determines the best position for a variables and returns
1249 it there.]
1250
1251 Description [Determines the best position for a variables and returns
1252 it there. Returns 1 in case of success; 0 otherwise.]
1253
1254 SideEffects [None]
1255
1256 ******************************************************************************/
1257 static int
zddGroupSiftingBackward(DdManager * table,Move * moves,int size)1258 zddGroupSiftingBackward(
1259 DdManager * table,
1260 Move * moves,
1261 int size)
1262 {
1263 Move *move;
1264 int res;
1265
1266
1267 for (move = moves; move != NULL; move = move->next) {
1268 if (move->size < size) {
1269 size = move->size;
1270 }
1271 }
1272
1273 for (move = moves; move != NULL; move = move->next) {
1274 if (move->size == size) return(1);
1275 if ((table->subtableZ[move->x].next == move->x) &&
1276 (table->subtableZ[move->y].next == move->y)) {
1277 res = cuddZddSwapInPlace(table,(int)move->x,(int)move->y);
1278 if (!res) return(0);
1279 #ifdef DD_DEBUG
1280 if (pr > 0) (void) fprintf(table->out,"zddGroupSiftingBackward:\n");
1281 assert(table->subtableZ[move->x].next == move->x);
1282 assert(table->subtableZ[move->y].next == move->y);
1283 #endif
1284 } else { /* Group move necessary */
1285 res = zddGroupMoveBackward(table,(int)move->x,(int)move->y);
1286 if (!res) return(0);
1287 }
1288 }
1289
1290 return(1);
1291
1292 } /* end of zddGroupSiftingBackward */
1293
1294
1295 /**Function********************************************************************
1296
1297 Synopsis [Merges groups in the DD table.]
1298
1299 Description [Creates a single group from low to high and adjusts the
1300 idex field of the tree node.]
1301
1302 SideEffects [None]
1303
1304 ******************************************************************************/
1305 static void
zddMergeGroups(DdManager * table,MtrNode * treenode,int low,int high)1306 zddMergeGroups(
1307 DdManager * table,
1308 MtrNode * treenode,
1309 int low,
1310 int high)
1311 {
1312 int i;
1313 MtrNode *auxnode;
1314 int saveindex;
1315 int newindex;
1316
1317 /* Merge all variables from low to high in one group, unless
1318 ** this is the topmost group. In such a case we do not merge lest
1319 ** we lose the symmetry information. */
1320 if (treenode != table->treeZ) {
1321 for (i = low; i < high; i++)
1322 table->subtableZ[i].next = i+1;
1323 table->subtableZ[high].next = low;
1324 }
1325
1326 /* Adjust the index fields of the tree nodes. If a node is the
1327 ** first child of its parent, then the parent may also need adjustment. */
1328 saveindex = treenode->index;
1329 newindex = table->invpermZ[low];
1330 auxnode = treenode;
1331 do {
1332 auxnode->index = newindex;
1333 if (auxnode->parent == NULL ||
1334 (int) auxnode->parent->index != saveindex)
1335 break;
1336 auxnode = auxnode->parent;
1337 } while (1);
1338 return;
1339
1340 } /* end of zddMergeGroups */
1341