1 /**CFile***********************************************************************
2
3 FileName [cuddGroup.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions for group sifting.]
8
9 Description [External procedures included in this file:
10 <ul>
11 <li> Cudd_MakeTreeNode()
12 </ul>
13 Internal procedures included in this file:
14 <ul>
15 <li> cuddTreeSifting()
16 </ul>
17 Static procedures included in this module:
18 <ul>
19 <li> ddTreeSiftingAux()
20 <li> ddCountInternalMtrNodes()
21 <li> ddReorderChildren()
22 <li> ddFindNodeHiLo()
23 <li> ddUniqueCompareGroup()
24 <li> ddGroupSifting()
25 <li> ddCreateGroup()
26 <li> ddGroupSiftingAux()
27 <li> ddGroupSiftingUp()
28 <li> ddGroupSiftingDown()
29 <li> ddGroupMove()
30 <li> ddGroupMoveBackward()
31 <li> ddGroupSiftingBackward()
32 <li> ddMergeGroups()
33 <li> ddDissolveGroup()
34 <li> ddNoCheck()
35 <li> ddSecDiffCheck()
36 <li> ddExtSymmCheck()
37 <li> ddVarGroupCheck()
38 <li> ddSetVarHandled()
39 <li> ddResetVarHandled()
40 <li> ddIsVarHandled()
41 </ul>]
42
43 Author [Shipra Panda, Fabio Somenzi]
44
45 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
46
47 All rights reserved.
48
49 Redistribution and use in source and binary forms, with or without
50 modification, are permitted provided that the following conditions
51 are met:
52
53 Redistributions of source code must retain the above copyright
54 notice, this list of conditions and the following disclaimer.
55
56 Redistributions in binary form must reproduce the above copyright
57 notice, this list of conditions and the following disclaimer in the
58 documentation and/or other materials provided with the distribution.
59
60 Neither the name of the University of Colorado nor the names of its
61 contributors may be used to endorse or promote products derived from
62 this software without specific prior written permission.
63
64 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
65 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
66 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
67 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
68 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
69 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
70 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
71 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
72 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
73 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
74 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
75 POSSIBILITY OF SUCH DAMAGE.]
76
77 ******************************************************************************/
78
79 #include "misc/util/util_hack.h"
80 #include "cuddInt.h"
81
82 ABC_NAMESPACE_IMPL_START
83
84
85
86 /*---------------------------------------------------------------------------*/
87 /* Constant declarations */
88 /*---------------------------------------------------------------------------*/
89
90 /* Constants for lazy sifting */
91 #define DD_NORMAL_SIFT 0
92 #define DD_LAZY_SIFT 1
93
94 /* Constants for sifting up and down */
95 #define DD_SIFT_DOWN 0
96 #define DD_SIFT_UP 1
97
98 /*---------------------------------------------------------------------------*/
99 /* Stucture declarations */
100 /*---------------------------------------------------------------------------*/
101
102 /*---------------------------------------------------------------------------*/
103 /* Type declarations */
104 /*---------------------------------------------------------------------------*/
105
106 typedef int (*DD_CHKFP)(DdManager *, int, int);
107
108 /*---------------------------------------------------------------------------*/
109 /* Variable declarations */
110 /*---------------------------------------------------------------------------*/
111
112 #ifndef lint
113 static char rcsid[] DD_UNUSED = "$Id: cuddGroup.c,v 1.44 2009/02/21 18:24:10 fabio Exp $";
114 #endif
115
116 static int *entry;
117 extern int ddTotalNumberSwapping;
118 #ifdef DD_STATS
119 extern int ddTotalNISwaps;
120 static int extsymmcalls;
121 static int extsymm;
122 static int secdiffcalls;
123 static int secdiff;
124 static int secdiffmisfire;
125 #endif
126 #ifdef DD_DEBUG
127 static int pr = 0; /* flag to enable printing while debugging */
128 /* by depositing a 1 into it */
129 #endif
130 static unsigned int originalSize;
131
132 /*---------------------------------------------------------------------------*/
133 /* Macro declarations */
134 /*---------------------------------------------------------------------------*/
135
136 /**AutomaticStart*************************************************************/
137
138 /*---------------------------------------------------------------------------*/
139 /* Static function prototypes */
140 /*---------------------------------------------------------------------------*/
141
142 static int ddTreeSiftingAux (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
143 #ifdef DD_STATS
144 static int ddCountInternalMtrNodes (DdManager *table, MtrNode *treenode);
145 #endif
146 static int ddReorderChildren (DdManager *table, MtrNode *treenode, Cudd_ReorderingType method);
147 static void ddFindNodeHiLo (DdManager *table, MtrNode *treenode, int *lower, int *upper);
148 static int ddUniqueCompareGroup (int *ptrX, int *ptrY);
149 static int ddGroupSifting (DdManager *table, int lower, int upper, DD_CHKFP checkFunction, int lazyFlag);
150 static void ddCreateGroup (DdManager *table, int x, int y);
151 static int ddGroupSiftingAux (DdManager *table, int x, int xLow, int xHigh, DD_CHKFP checkFunction, int lazyFlag);
152 static int ddGroupSiftingUp (DdManager *table, int y, int xLow, DD_CHKFP checkFunction, Move **moves);
153 static int ddGroupSiftingDown (DdManager *table, int x, int xHigh, DD_CHKFP checkFunction, Move **moves);
154 static int ddGroupMove (DdManager *table, int x, int y, Move **moves);
155 static int ddGroupMoveBackward (DdManager *table, int x, int y);
156 static int ddGroupSiftingBackward (DdManager *table, Move *moves, int size, int upFlag, int lazyFlag);
157 static void ddMergeGroups (DdManager *table, MtrNode *treenode, int low, int high);
158 static void ddDissolveGroup (DdManager *table, int x, int y);
159 static int ddNoCheck (DdManager *table, int x, int y);
160 static int ddSecDiffCheck (DdManager *table, int x, int y);
161 static int ddExtSymmCheck (DdManager *table, int x, int y);
162 static int ddVarGroupCheck (DdManager * table, int x, int y);
163 static int ddSetVarHandled (DdManager *dd, int index);
164 static int ddResetVarHandled (DdManager *dd, int index);
165 static int ddIsVarHandled (DdManager *dd, int index);
166
167 /**AutomaticEnd***************************************************************/
168
169 /*---------------------------------------------------------------------------*/
170 /* Definition of exported functions */
171 /*---------------------------------------------------------------------------*/
172
173
174 /**Function********************************************************************
175
176 Synopsis [Creates a new variable group.]
177
178 Description [Creates a new variable group. The group starts at
179 variable and contains size variables. The parameter low is the index
180 of the first variable. If the variable already exists, its current
181 position in the order is known to the manager. If the variable does
182 not exist yet, the position is assumed to be the same as the index.
183 The group tree is created if it does not exist yet.
184 Returns a pointer to the group if successful; NULL otherwise.]
185
186 SideEffects [The variable tree is changed.]
187
188 SeeAlso [Cudd_MakeZddTreeNode]
189
190 ******************************************************************************/
191 MtrNode *
Cudd_MakeTreeNode(DdManager * dd,unsigned int low,unsigned int size,unsigned int type)192 Cudd_MakeTreeNode(
193 DdManager * dd /* manager */,
194 unsigned int low /* index of the first group variable */,
195 unsigned int size /* number of variables in the group */,
196 unsigned int type /* MTR_DEFAULT or MTR_FIXED */)
197 {
198 MtrNode *group;
199 MtrNode *tree;
200 unsigned int level;
201
202 /* If the variable does not exist yet, the position is assumed to be
203 ** the same as the index. Therefore, applications that rely on
204 ** Cudd_bddNewVarAtLevel or Cudd_addNewVarAtLevel to create new
205 ** variables have to create the variables before they group them.
206 */
207 level = (low < (unsigned int) dd->size) ? dd->perm[low] : low;
208
209 if (level + size - 1> (int) MTR_MAXHIGH)
210 return(NULL);
211
212 /* If the tree does not exist yet, create it. */
213 tree = dd->tree;
214 if (tree == NULL) {
215 dd->tree = tree = Mtr_InitGroupTree(0, dd->size);
216 if (tree == NULL)
217 return(NULL);
218 tree->index = dd->invperm[0];
219 }
220
221 /* Extend the upper bound of the tree if necessary. This allows the
222 ** application to create groups even before the variables are created.
223 */
224 tree->size = ddMax(tree->size, ddMax(level + size, (unsigned) dd->size));
225
226 /* Create the group. */
227 group = Mtr_MakeGroup(tree, level, size, type);
228 if (group == NULL)
229 return(NULL);
230
231 /* Initialize the index field to the index of the variable currently
232 ** in position low. This field will be updated by the reordering
233 ** procedure to provide a handle to the group once it has been moved.
234 */
235 group->index = (MtrHalfWord) low;
236
237 return(group);
238
239 } /* end of Cudd_MakeTreeNode */
240
241
242 /*---------------------------------------------------------------------------*/
243 /* Definition of internal functions */
244 /*---------------------------------------------------------------------------*/
245
246
247 /**Function********************************************************************
248
249 Synopsis [Tree sifting algorithm.]
250
251 Description [Tree sifting algorithm. Assumes that a tree representing
252 a group hierarchy is passed as a parameter. It then reorders each
253 group in postorder fashion by calling ddTreeSiftingAux. Assumes that
254 no dead nodes are present. Returns 1 if successful; 0 otherwise.]
255
256 SideEffects [None]
257
258 ******************************************************************************/
259 int
cuddTreeSifting(DdManager * table,Cudd_ReorderingType method)260 cuddTreeSifting(
261 DdManager * table /* DD table */,
262 Cudd_ReorderingType method /* reordering method for the groups of leaves */)
263 {
264 int i;
265 int nvars;
266 int result;
267 int tempTree;
268
269 /* If no tree is provided we create a temporary one in which all
270 ** variables are in a single group. After reordering this tree is
271 ** destroyed.
272 */
273 tempTree = table->tree == NULL;
274 if (tempTree) {
275 table->tree = Mtr_InitGroupTree(0,table->size);
276 table->tree->index = table->invperm[0];
277 }
278 nvars = table->size;
279
280 #ifdef DD_DEBUG
281 if (pr > 0 && !tempTree) (void) fprintf(table->out,"cuddTreeSifting:");
282 Mtr_PrintGroups(table->tree,pr <= 0);
283 #endif
284
285 #ifdef DD_STATS
286 extsymmcalls = 0;
287 extsymm = 0;
288 secdiffcalls = 0;
289 secdiff = 0;
290 secdiffmisfire = 0;
291
292 (void) fprintf(table->out,"\n");
293 if (!tempTree)
294 (void) fprintf(table->out,"#:IM_NODES %8d: group tree nodes\n",
295 ddCountInternalMtrNodes(table,table->tree));
296 #endif
297
298 /* Initialize the group of each subtable to itself. Initially
299 ** there are no groups. Groups are created according to the tree
300 ** structure in postorder fashion.
301 */
302 for (i = 0; i < nvars; i++)
303 table->subtables[i].next = i;
304
305
306 /* Reorder. */
307 result = ddTreeSiftingAux(table, table->tree, method);
308
309 #ifdef DD_STATS /* print stats */
310 if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
311 (table->groupcheck == CUDD_GROUP_CHECK7 ||
312 table->groupcheck == CUDD_GROUP_CHECK5)) {
313 (void) fprintf(table->out,"\nextsymmcalls = %d\n",extsymmcalls);
314 (void) fprintf(table->out,"extsymm = %d",extsymm);
315 }
316 if (!tempTree && method == CUDD_REORDER_GROUP_SIFT &&
317 table->groupcheck == CUDD_GROUP_CHECK7) {
318 (void) fprintf(table->out,"\nsecdiffcalls = %d\n",secdiffcalls);
319 (void) fprintf(table->out,"secdiff = %d\n",secdiff);
320 (void) fprintf(table->out,"secdiffmisfire = %d",secdiffmisfire);
321 }
322 #endif
323
324 if (tempTree)
325 Cudd_FreeTree(table);
326 return(result);
327
328 } /* end of cuddTreeSifting */
329
330
331 /*---------------------------------------------------------------------------*/
332 /* Definition of static functions */
333 /*---------------------------------------------------------------------------*/
334
335
336 /**Function********************************************************************
337
338 Synopsis [Visits the group tree and reorders each group.]
339
340 Description [Recursively visits the group tree and reorders each
341 group in postorder fashion. Returns 1 if successful; 0 otherwise.]
342
343 SideEffects [None]
344
345 ******************************************************************************/
346 static int
ddTreeSiftingAux(DdManager * table,MtrNode * treenode,Cudd_ReorderingType method)347 ddTreeSiftingAux(
348 DdManager * table,
349 MtrNode * treenode,
350 Cudd_ReorderingType method)
351 {
352 MtrNode *auxnode;
353 int res;
354 Cudd_AggregationType saveCheck;
355
356 #ifdef DD_DEBUG
357 Mtr_PrintGroups(treenode,1);
358 #endif
359
360 auxnode = treenode;
361 while (auxnode != NULL) {
362 if (auxnode->child != NULL) {
363 if (!ddTreeSiftingAux(table, auxnode->child, method))
364 return(0);
365 saveCheck = table->groupcheck;
366 table->groupcheck = CUDD_NO_CHECK;
367 if (method != CUDD_REORDER_LAZY_SIFT)
368 res = ddReorderChildren(table, auxnode, CUDD_REORDER_GROUP_SIFT);
369 else
370 res = ddReorderChildren(table, auxnode, CUDD_REORDER_LAZY_SIFT);
371 table->groupcheck = saveCheck;
372
373 if (res == 0)
374 return(0);
375 } else if (auxnode->size > 1) {
376 if (!ddReorderChildren(table, auxnode, method))
377 return(0);
378 }
379 auxnode = auxnode->younger;
380 }
381
382 return(1);
383
384 } /* end of ddTreeSiftingAux */
385
386
387 #ifdef DD_STATS
388 /**Function********************************************************************
389
390 Synopsis [Counts the number of internal nodes of the group tree.]
391
392 Description [Counts the number of internal nodes of the group tree.
393 Returns the count.]
394
395 SideEffects [None]
396
397 ******************************************************************************/
398 static int
ddCountInternalMtrNodes(DdManager * table,MtrNode * treenode)399 ddCountInternalMtrNodes(
400 DdManager * table,
401 MtrNode * treenode)
402 {
403 MtrNode *auxnode;
404 int count,nodeCount;
405
406
407 nodeCount = 0;
408 auxnode = treenode;
409 while (auxnode != NULL) {
410 if (!(MTR_TEST(auxnode,MTR_TERMINAL))) {
411 nodeCount++;
412 count = ddCountInternalMtrNodes(table,auxnode->child);
413 nodeCount += count;
414 }
415 auxnode = auxnode->younger;
416 }
417
418 return(nodeCount);
419
420 } /* end of ddCountInternalMtrNodes */
421 #endif
422
423
424 /**Function********************************************************************
425
426 Synopsis [Reorders the children of a group tree node according to
427 the options.]
428
429 Description [Reorders the children of a group tree node according to
430 the options. After reordering puts all the variables in the group
431 and/or its descendents in a single group. This allows hierarchical
432 reordering. If the variables in the group do not exist yet, simply
433 does nothing. Returns 1 if successful; 0 otherwise.]
434
435 SideEffects [None]
436
437 ******************************************************************************/
438 static int
ddReorderChildren(DdManager * table,MtrNode * treenode,Cudd_ReorderingType method)439 ddReorderChildren(
440 DdManager * table,
441 MtrNode * treenode,
442 Cudd_ReorderingType method)
443 {
444 int lower;
445 int upper = -1;
446 int result;
447 unsigned int initialSize;
448
449 ddFindNodeHiLo(table,treenode,&lower,&upper);
450 /* If upper == -1 these variables do not exist yet. */
451 if (upper == -1)
452 return(1);
453
454 if (treenode->flags == MTR_FIXED) {
455 result = 1;
456 } else {
457 #ifdef DD_STATS
458 (void) fprintf(table->out," ");
459 #endif
460 switch (method) {
461 case CUDD_REORDER_RANDOM:
462 case CUDD_REORDER_RANDOM_PIVOT:
463 result = cuddSwapping(table,lower,upper,method);
464 break;
465 case CUDD_REORDER_SIFT:
466 result = cuddSifting(table,lower,upper);
467 break;
468 case CUDD_REORDER_SIFT_CONVERGE:
469 do {
470 initialSize = table->keys - table->isolated;
471 result = cuddSifting(table,lower,upper);
472 if (initialSize <= table->keys - table->isolated)
473 break;
474 #ifdef DD_STATS
475 else
476 (void) fprintf(table->out,"\n");
477 #endif
478 } while (result != 0);
479 break;
480 case CUDD_REORDER_SYMM_SIFT:
481 result = cuddSymmSifting(table,lower,upper);
482 break;
483 case CUDD_REORDER_SYMM_SIFT_CONV:
484 result = cuddSymmSiftingConv(table,lower,upper);
485 break;
486 case CUDD_REORDER_GROUP_SIFT:
487 if (table->groupcheck == CUDD_NO_CHECK) {
488 result = ddGroupSifting(table,lower,upper,ddNoCheck,
489 DD_NORMAL_SIFT);
490 } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
491 result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
492 DD_NORMAL_SIFT);
493 } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
494 result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
495 DD_NORMAL_SIFT);
496 } else {
497 (void) fprintf(table->err,
498 "Unknown group ckecking method\n");
499 result = 0;
500 }
501 break;
502 case CUDD_REORDER_GROUP_SIFT_CONV:
503 do {
504 initialSize = table->keys - table->isolated;
505 if (table->groupcheck == CUDD_NO_CHECK) {
506 result = ddGroupSifting(table,lower,upper,ddNoCheck,
507 DD_NORMAL_SIFT);
508 } else if (table->groupcheck == CUDD_GROUP_CHECK5) {
509 result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
510 DD_NORMAL_SIFT);
511 } else if (table->groupcheck == CUDD_GROUP_CHECK7) {
512 result = ddGroupSifting(table,lower,upper,ddExtSymmCheck,
513 DD_NORMAL_SIFT);
514 } else {
515 (void) fprintf(table->err,
516 "Unknown group ckecking method\n");
517 result = 0;
518 }
519 #ifdef DD_STATS
520 (void) fprintf(table->out,"\n");
521 #endif
522 result = cuddWindowReorder(table,lower,upper,
523 CUDD_REORDER_WINDOW4);
524 if (initialSize <= table->keys - table->isolated)
525 break;
526 #ifdef DD_STATS
527 else
528 (void) fprintf(table->out,"\n");
529 #endif
530 } while (result != 0);
531 break;
532 case CUDD_REORDER_WINDOW2:
533 case CUDD_REORDER_WINDOW3:
534 case CUDD_REORDER_WINDOW4:
535 case CUDD_REORDER_WINDOW2_CONV:
536 case CUDD_REORDER_WINDOW3_CONV:
537 case CUDD_REORDER_WINDOW4_CONV:
538 result = cuddWindowReorder(table,lower,upper,method);
539 break;
540 case CUDD_REORDER_ANNEALING:
541 result = cuddAnnealing(table,lower,upper);
542 break;
543 case CUDD_REORDER_GENETIC:
544 result = cuddGa(table,lower,upper);
545 break;
546 case CUDD_REORDER_LINEAR:
547 result = cuddLinearAndSifting(table,lower,upper);
548 break;
549 case CUDD_REORDER_LINEAR_CONVERGE:
550 do {
551 initialSize = table->keys - table->isolated;
552 result = cuddLinearAndSifting(table,lower,upper);
553 if (initialSize <= table->keys - table->isolated)
554 break;
555 #ifdef DD_STATS
556 else
557 (void) fprintf(table->out,"\n");
558 #endif
559 } while (result != 0);
560 break;
561 case CUDD_REORDER_EXACT:
562 result = cuddExact(table,lower,upper);
563 break;
564 case CUDD_REORDER_LAZY_SIFT:
565 result = ddGroupSifting(table,lower,upper,ddVarGroupCheck,
566 DD_LAZY_SIFT);
567 break;
568 default:
569 return(0);
570 }
571 }
572
573 /* Create a single group for all the variables that were sifted,
574 ** so that they will be treated as a single block by successive
575 ** invocations of ddGroupSifting.
576 */
577 ddMergeGroups(table,treenode,lower,upper);
578
579 #ifdef DD_DEBUG
580 if (pr > 0) (void) fprintf(table->out,"ddReorderChildren:");
581 #endif
582
583 return(result);
584
585 } /* end of ddReorderChildren */
586
587
588 /**Function********************************************************************
589
590 Synopsis [Finds the lower and upper bounds of the group represented
591 by treenode.]
592
593 Description [Finds the lower and upper bounds of the group
594 represented by treenode. From the index and size fields we need to
595 derive the current positions, and find maximum and minimum.]
596
597 SideEffects [The bounds are returned as side effects.]
598
599 SeeAlso []
600
601 ******************************************************************************/
602 static void
ddFindNodeHiLo(DdManager * table,MtrNode * treenode,int * lower,int * upper)603 ddFindNodeHiLo(
604 DdManager * table,
605 MtrNode * treenode,
606 int * lower,
607 int * upper)
608 {
609 int low;
610 int high;
611
612 /* Check whether no variables in this group already exist.
613 ** If so, return immediately. The calling procedure will know from
614 ** the values of upper that no reordering is needed.
615 */
616 if ((int) treenode->low >= table->size) {
617 *lower = table->size;
618 *upper = -1;
619 return;
620 }
621
622 *lower = low = (unsigned int) table->perm[treenode->index];
623 high = (int) (low + treenode->size - 1);
624
625 if (high >= table->size) {
626 /* This is the case of a partially existing group. The aim is to
627 ** reorder as many variables as safely possible. If the tree
628 ** node is terminal, we just reorder the subset of the group
629 ** that is currently in existence. If the group has
630 ** subgroups, then we only reorder those subgroups that are
631 ** fully instantiated. This way we avoid breaking up a group.
632 */
633 MtrNode *auxnode = treenode->child;
634 if (auxnode == NULL) {
635 *upper = (unsigned int) table->size - 1;
636 } else {
637 /* Search the subgroup that strands the table->size line.
638 ** If the first group starts at 0 and goes past table->size
639 ** upper will get -1, thus correctly signaling that no reordering
640 ** should take place.
641 */
642 while (auxnode != NULL) {
643 int thisLower = table->perm[auxnode->low];
644 int thisUpper = thisLower + auxnode->size - 1;
645 if (thisUpper >= table->size && thisLower < table->size)
646 *upper = (unsigned int) thisLower - 1;
647 auxnode = auxnode->younger;
648 }
649 }
650 } else {
651 /* Normal case: All the variables of the group exist. */
652 *upper = (unsigned int) high;
653 }
654
655 #ifdef DD_DEBUG
656 /* Make sure that all variables in group are contiguous. */
657 assert(treenode->size >= *upper - *lower + 1);
658 #endif
659
660 return;
661
662 } /* end of ddFindNodeHiLo */
663
664
665 /**Function********************************************************************
666
667 Synopsis [Comparison function used by qsort.]
668
669 Description [Comparison function used by qsort to order the variables
670 according to the number of keys in the subtables. Returns the
671 difference in number of keys between the two variables being
672 compared.]
673
674 SideEffects [None]
675
676 ******************************************************************************/
677 static int
ddUniqueCompareGroup(int * ptrX,int * ptrY)678 ddUniqueCompareGroup(
679 int * ptrX,
680 int * ptrY)
681 {
682 #if 0
683 if (entry[*ptrY] == entry[*ptrX]) {
684 return((*ptrX) - (*ptrY));
685 }
686 #endif
687 return(entry[*ptrY] - entry[*ptrX]);
688
689 } /* end of ddUniqueCompareGroup */
690
691
692 /**Function********************************************************************
693
694 Synopsis [Sifts from treenode->low to treenode->high.]
695
696 Description [Sifts from treenode->low to treenode->high. If
697 croupcheck == CUDD_GROUP_CHECK7, it checks for group creation at the
698 end of the initial sifting. If a group is created, it is then sifted
699 again. After sifting one variable, the group that contains it is
700 dissolved. Returns 1 in case of success; 0 otherwise.]
701
702 SideEffects [None]
703
704 ******************************************************************************/
705 static int
ddGroupSifting(DdManager * table,int lower,int upper,DD_CHKFP checkFunction,int lazyFlag)706 ddGroupSifting(
707 DdManager * table,
708 int lower,
709 int upper,
710 DD_CHKFP checkFunction,
711 int lazyFlag)
712 {
713 int *var;
714 int i,j,x,xInit;
715 int nvars;
716 int classes;
717 int result;
718 int *sifted;
719 int merged;
720 int dissolve;
721 #ifdef DD_STATS
722 unsigned previousSize;
723 #endif
724 int xindex;
725
726 nvars = table->size;
727
728 /* Order variables to sift. */
729 entry = NULL;
730 sifted = NULL;
731 var = ABC_ALLOC(int,nvars);
732 if (var == NULL) {
733 table->errorCode = CUDD_MEMORY_OUT;
734 goto ddGroupSiftingOutOfMem;
735 }
736 entry = ABC_ALLOC(int,nvars);
737 if (entry == NULL) {
738 table->errorCode = CUDD_MEMORY_OUT;
739 goto ddGroupSiftingOutOfMem;
740 }
741 sifted = ABC_ALLOC(int,nvars);
742 if (sifted == NULL) {
743 table->errorCode = CUDD_MEMORY_OUT;
744 goto ddGroupSiftingOutOfMem;
745 }
746
747 /* Here we consider only one representative for each group. */
748 for (i = 0, classes = 0; i < nvars; i++) {
749 sifted[i] = 0;
750 x = table->perm[i];
751 if ((unsigned) x >= table->subtables[x].next) {
752 entry[i] = table->subtables[x].keys;
753 var[classes] = i;
754 classes++;
755 }
756 }
757
758 qsort((void *)var,(size_t)classes,sizeof(int),
759 (DD_QSFP) ddUniqueCompareGroup);
760
761 if (lazyFlag) {
762 for (i = 0; i < nvars; i ++) {
763 ddResetVarHandled(table, i);
764 }
765 }
766
767 /* Now sift. */
768 for (i = 0; i < ddMin(table->siftMaxVar,classes); i++) {
769 if (ddTotalNumberSwapping >= table->siftMaxSwap)
770 break;
771 xindex = var[i];
772 if (sifted[xindex] == 1) /* variable already sifted as part of group */
773 continue;
774 x = table->perm[xindex]; /* find current level of this variable */
775
776 if (x < lower || x > upper || table->subtables[x].bindVar == 1)
777 continue;
778 #ifdef DD_STATS
779 previousSize = table->keys - table->isolated;
780 #endif
781 #ifdef DD_DEBUG
782 /* x is bottom of group */
783 assert((unsigned) x >= table->subtables[x].next);
784 #endif
785 if ((unsigned) x == table->subtables[x].next) {
786 dissolve = 1;
787 result = ddGroupSiftingAux(table,x,lower,upper,checkFunction,
788 lazyFlag);
789 } else {
790 dissolve = 0;
791 result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
792 }
793 if (!result) goto ddGroupSiftingOutOfMem;
794
795 /* check for aggregation */
796 merged = 0;
797 if (lazyFlag == 0 && table->groupcheck == CUDD_GROUP_CHECK7) {
798 x = table->perm[xindex]; /* find current level */
799 if ((unsigned) x == table->subtables[x].next) { /* not part of a group */
800 if (x != upper && sifted[table->invperm[x+1]] == 0 &&
801 (unsigned) x+1 == table->subtables[x+1].next) {
802 if (ddSecDiffCheck(table,x,x+1)) {
803 merged =1;
804 ddCreateGroup(table,x,x+1);
805 }
806 }
807 if (x != lower && sifted[table->invperm[x-1]] == 0 &&
808 (unsigned) x-1 == table->subtables[x-1].next) {
809 if (ddSecDiffCheck(table,x-1,x)) {
810 merged =1;
811 ddCreateGroup(table,x-1,x);
812 }
813 }
814 }
815 }
816
817 if (merged) { /* a group was created */
818 /* move x to bottom of group */
819 while ((unsigned) x < table->subtables[x].next)
820 x = table->subtables[x].next;
821 /* sift */
822 result = ddGroupSiftingAux(table,x,lower,upper,ddNoCheck,lazyFlag);
823 if (!result) goto ddGroupSiftingOutOfMem;
824 #ifdef DD_STATS
825 if (table->keys < previousSize + table->isolated) {
826 (void) fprintf(table->out,"_");
827 } else if (table->keys > previousSize + table->isolated) {
828 (void) fprintf(table->out,"^");
829 } else {
830 (void) fprintf(table->out,"*");
831 }
832 fflush(table->out);
833 } else {
834 if (table->keys < previousSize + table->isolated) {
835 (void) fprintf(table->out,"-");
836 } else if (table->keys > previousSize + table->isolated) {
837 (void) fprintf(table->out,"+");
838 } else {
839 (void) fprintf(table->out,"=");
840 }
841 fflush(table->out);
842 #endif
843 }
844
845 /* Mark variables in the group just sifted. */
846 x = table->perm[xindex];
847 if ((unsigned) x != table->subtables[x].next) {
848 xInit = x;
849 do {
850 j = table->invperm[x];
851 sifted[j] = 1;
852 x = table->subtables[x].next;
853 } while (x != xInit);
854
855 /* Dissolve the group if it was created. */
856 if (lazyFlag == 0 && dissolve) {
857 do {
858 j = table->subtables[x].next;
859 table->subtables[x].next = x;
860 x = j;
861 } while (x != xInit);
862 }
863 }
864
865 #ifdef DD_DEBUG
866 if (pr > 0) (void) fprintf(table->out,"ddGroupSifting:");
867 #endif
868
869 if (lazyFlag) ddSetVarHandled(table, xindex);
870 } /* for */
871
872 ABC_FREE(sifted);
873 ABC_FREE(var);
874 ABC_FREE(entry);
875
876 return(1);
877
878 ddGroupSiftingOutOfMem:
879 if (entry != NULL) ABC_FREE(entry);
880 if (var != NULL) ABC_FREE(var);
881 if (sifted != NULL) ABC_FREE(sifted);
882
883 return(0);
884
885 } /* end of ddGroupSifting */
886
887
888 /**Function********************************************************************
889
890 Synopsis [Creates a group encompassing variables from x to y in the
891 DD table.]
892
893 Description [Creates a group encompassing variables from x to y in the
894 DD table. In the current implementation it must be y == x+1.
895 Returns 1 in case of success; 0 otherwise.]
896
897 SideEffects [None]
898
899 ******************************************************************************/
900 static void
ddCreateGroup(DdManager * table,int x,int y)901 ddCreateGroup(
902 DdManager * table,
903 int x,
904 int y)
905 {
906 int gybot;
907
908 #ifdef DD_DEBUG
909 assert(y == x+1);
910 #endif
911
912 /* Find bottom of second group. */
913 gybot = y;
914 while ((unsigned) gybot < table->subtables[gybot].next)
915 gybot = table->subtables[gybot].next;
916
917 /* Link groups. */
918 table->subtables[x].next = y;
919 table->subtables[gybot].next = x;
920
921 return;
922
923 } /* ddCreateGroup */
924
925
926 /**Function********************************************************************
927
928 Synopsis [Sifts one variable up and down until it has taken all
929 positions. Checks for aggregation.]
930
931 Description [Sifts one variable up and down until it has taken all
932 positions. Checks for aggregation. There may be at most two sweeps,
933 even if the group grows. Assumes that x is either an isolated
934 variable, or it is the bottom of a group. All groups may not have
935 been found. The variable being moved is returned to the best position
936 seen during sifting. Returns 1 in case of success; 0 otherwise.]
937
938 SideEffects [None]
939
940 ******************************************************************************/
941 static int
ddGroupSiftingAux(DdManager * table,int x,int xLow,int xHigh,DD_CHKFP checkFunction,int lazyFlag)942 ddGroupSiftingAux(
943 DdManager * table,
944 int x,
945 int xLow,
946 int xHigh,
947 DD_CHKFP checkFunction,
948 int lazyFlag)
949 {
950 Move *move;
951 Move *moves; /* list of moves */
952 int initialSize;
953 int result;
954 int y;
955 int topbot;
956
957 #ifdef DD_DEBUG
958 if (pr > 0) (void) fprintf(table->out,
959 "ddGroupSiftingAux from %d to %d\n",xLow,xHigh);
960 assert((unsigned) x >= table->subtables[x].next); /* x is bottom of group */
961 #endif
962
963 initialSize = table->keys - table->isolated;
964 moves = NULL;
965
966 originalSize = initialSize; /* for lazy sifting */
967
968 /* If we have a singleton, we check for aggregation in both
969 ** directions before we sift.
970 */
971 if ((unsigned) x == table->subtables[x].next) {
972 /* Will go down first, unless x == xHigh:
973 ** Look for aggregation above x.
974 */
975 for (y = x; y > xLow; y--) {
976 if (!checkFunction(table,y-1,y))
977 break;
978 topbot = table->subtables[y-1].next; /* find top of y-1's group */
979 table->subtables[y-1].next = y;
980 table->subtables[x].next = topbot; /* x is bottom of group so its */
981 /* next is top of y-1's group */
982 y = topbot + 1; /* add 1 for y--; new y is top of group */
983 }
984 /* Will go up first unless x == xlow:
985 ** Look for aggregation below x.
986 */
987 for (y = x; y < xHigh; y++) {
988 if (!checkFunction(table,y,y+1))
989 break;
990 /* find bottom of y+1's group */
991 topbot = y + 1;
992 while ((unsigned) topbot < table->subtables[topbot].next) {
993 topbot = table->subtables[topbot].next;
994 }
995 table->subtables[topbot].next = table->subtables[y].next;
996 table->subtables[y].next = y + 1;
997 y = topbot - 1; /* subtract 1 for y++; new y is bottom of group */
998 }
999 }
1000
1001 /* Now x may be in the middle of a group.
1002 ** Find bottom of x's group.
1003 */
1004 while ((unsigned) x < table->subtables[x].next)
1005 x = table->subtables[x].next;
1006
1007 if (x == xLow) { /* Sift down */
1008 #ifdef DD_DEBUG
1009 /* x must be a singleton */
1010 assert((unsigned) x == table->subtables[x].next);
1011 #endif
1012 if (x == xHigh) return(1); /* just one variable */
1013
1014 if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1015 goto ddGroupSiftingAuxOutOfMem;
1016 /* at this point x == xHigh, unless early term */
1017
1018 /* move backward and stop at best position */
1019 result = ddGroupSiftingBackward(table,moves,initialSize,
1020 DD_SIFT_DOWN,lazyFlag);
1021 #ifdef DD_DEBUG
1022 assert(table->keys - table->isolated <= (unsigned) initialSize);
1023 #endif
1024 if (!result) goto ddGroupSiftingAuxOutOfMem;
1025
1026 } else if (cuddNextHigh(table,x) > xHigh) { /* Sift up */
1027 #ifdef DD_DEBUG
1028 /* x is bottom of group */
1029 assert((unsigned) x >= table->subtables[x].next);
1030 #endif
1031 /* Find top of x's group */
1032 x = table->subtables[x].next;
1033
1034 if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1035 goto ddGroupSiftingAuxOutOfMem;
1036 /* at this point x == xLow, unless early term */
1037
1038 /* move backward and stop at best position */
1039 result = ddGroupSiftingBackward(table,moves,initialSize,
1040 DD_SIFT_UP,lazyFlag);
1041 #ifdef DD_DEBUG
1042 assert(table->keys - table->isolated <= (unsigned) initialSize);
1043 #endif
1044 if (!result) goto ddGroupSiftingAuxOutOfMem;
1045
1046 } else if (x - xLow > xHigh - x) { /* must go down first: shorter */
1047 if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1048 goto ddGroupSiftingAuxOutOfMem;
1049 /* at this point x == xHigh, unless early term */
1050
1051 /* Find top of group */
1052 if (moves) {
1053 x = moves->y;
1054 }
1055 while ((unsigned) x < table->subtables[x].next)
1056 x = table->subtables[x].next;
1057 x = table->subtables[x].next;
1058 #ifdef DD_DEBUG
1059 /* x should be the top of a group */
1060 assert((unsigned) x <= table->subtables[x].next);
1061 #endif
1062
1063 if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1064 goto ddGroupSiftingAuxOutOfMem;
1065
1066 /* move backward and stop at best position */
1067 result = ddGroupSiftingBackward(table,moves,initialSize,
1068 DD_SIFT_UP,lazyFlag);
1069 #ifdef DD_DEBUG
1070 assert(table->keys - table->isolated <= (unsigned) initialSize);
1071 #endif
1072 if (!result) goto ddGroupSiftingAuxOutOfMem;
1073
1074 } else { /* moving up first: shorter */
1075 /* Find top of x's group */
1076 x = table->subtables[x].next;
1077
1078 if (!ddGroupSiftingUp(table,x,xLow,checkFunction,&moves))
1079 goto ddGroupSiftingAuxOutOfMem;
1080 /* at this point x == xHigh, unless early term */
1081
1082 if (moves) {
1083 x = moves->x;
1084 }
1085 while ((unsigned) x < table->subtables[x].next)
1086 x = table->subtables[x].next;
1087 #ifdef DD_DEBUG
1088 /* x is bottom of a group */
1089 assert((unsigned) x >= table->subtables[x].next);
1090 #endif
1091
1092 if (!ddGroupSiftingDown(table,x,xHigh,checkFunction,&moves))
1093 goto ddGroupSiftingAuxOutOfMem;
1094
1095 /* move backward and stop at best position */
1096 result = ddGroupSiftingBackward(table,moves,initialSize,
1097 DD_SIFT_DOWN,lazyFlag);
1098 #ifdef DD_DEBUG
1099 assert(table->keys - table->isolated <= (unsigned) initialSize);
1100 #endif
1101 if (!result) goto ddGroupSiftingAuxOutOfMem;
1102 }
1103
1104 while (moves != NULL) {
1105 move = moves->next;
1106 cuddDeallocMove(table, moves);
1107 moves = move;
1108 }
1109
1110 return(1);
1111
1112 ddGroupSiftingAuxOutOfMem:
1113 while (moves != NULL) {
1114 move = moves->next;
1115 cuddDeallocMove(table, moves);
1116 moves = move;
1117 }
1118
1119 return(0);
1120
1121 } /* end of ddGroupSiftingAux */
1122
1123
1124 /**Function********************************************************************
1125
1126 Synopsis [Sifts up a variable until either it reaches position xLow
1127 or the size of the DD heap increases too much.]
1128
1129 Description [Sifts up a variable until either it reaches position
1130 xLow or the size of the DD heap increases too much. Assumes that y is
1131 the top of a group (or a singleton). Checks y for aggregation to the
1132 adjacent variables. Records all the moves that are appended to the
1133 list of moves received as input and returned as a side effect.
1134 Returns 1 in case of success; 0 otherwise.]
1135
1136 SideEffects [None]
1137
1138 ******************************************************************************/
1139 static int
ddGroupSiftingUp(DdManager * table,int y,int xLow,DD_CHKFP checkFunction,Move ** moves)1140 ddGroupSiftingUp(
1141 DdManager * table,
1142 int y,
1143 int xLow,
1144 DD_CHKFP checkFunction,
1145 Move ** moves)
1146 {
1147 Move *move;
1148 int x;
1149 int size;
1150 int i;
1151 int gxtop,gybot;
1152 int limitSize;
1153 int xindex, yindex;
1154 int zindex;
1155 int z;
1156 int isolated;
1157 int L; /* lower bound on DD size */
1158 #ifdef DD_DEBUG
1159 int checkL;
1160 #endif
1161
1162 yindex = table->invperm[y];
1163
1164 /* Initialize the lower bound.
1165 ** The part of the DD below the bottom of y's group will not change.
1166 ** The part of the DD above y that does not interact with any
1167 ** variable of y's group will not change.
1168 ** The rest may vanish in the best case, except for
1169 ** the nodes at level xLow, which will not vanish, regardless.
1170 ** What we use here is not really a lower bound, because we ignore
1171 ** the interactions with all variables except y.
1172 */
1173 limitSize = L = table->keys - table->isolated;
1174 gybot = y;
1175 while ((unsigned) gybot < table->subtables[gybot].next)
1176 gybot = table->subtables[gybot].next;
1177 for (z = xLow + 1; z <= gybot; z++) {
1178 zindex = table->invperm[z];
1179 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1180 isolated = table->vars[zindex]->ref == 1;
1181 L -= table->subtables[z].keys - isolated;
1182 }
1183 }
1184
1185 x = cuddNextLow(table,y);
1186 while (x >= xLow && L <= limitSize) {
1187 #ifdef DD_DEBUG
1188 gybot = y;
1189 while ((unsigned) gybot < table->subtables[gybot].next)
1190 gybot = table->subtables[gybot].next;
1191 checkL = table->keys - table->isolated;
1192 for (z = xLow + 1; z <= gybot; z++) {
1193 zindex = table->invperm[z];
1194 if (zindex == yindex || cuddTestInteract(table,zindex,yindex)) {
1195 isolated = table->vars[zindex]->ref == 1;
1196 checkL -= table->subtables[z].keys - isolated;
1197 }
1198 }
1199 if (pr > 0 && L != checkL) {
1200 (void) fprintf(table->out,
1201 "Inaccurate lower bound: L = %d checkL = %d\n",
1202 L, checkL);
1203 }
1204 #endif
1205 gxtop = table->subtables[x].next;
1206 if (checkFunction(table,x,y)) {
1207 /* Group found, attach groups */
1208 table->subtables[x].next = y;
1209 i = table->subtables[y].next;
1210 while (table->subtables[i].next != (unsigned) y)
1211 i = table->subtables[i].next;
1212 table->subtables[i].next = gxtop;
1213 move = (Move *)cuddDynamicAllocNode(table);
1214 if (move == NULL) goto ddGroupSiftingUpOutOfMem;
1215 move->x = x;
1216 move->y = y;
1217 move->flags = MTR_NEWNODE;
1218 move->size = table->keys - table->isolated;
1219 move->next = *moves;
1220 *moves = move;
1221 } else if (table->subtables[x].next == (unsigned) x &&
1222 table->subtables[y].next == (unsigned) y) {
1223 /* x and y are self groups */
1224 xindex = table->invperm[x];
1225 size = cuddSwapInPlace(table,x,y);
1226 #ifdef DD_DEBUG
1227 assert(table->subtables[x].next == (unsigned) x);
1228 assert(table->subtables[y].next == (unsigned) y);
1229 #endif
1230 if (size == 0) goto ddGroupSiftingUpOutOfMem;
1231 /* Update the lower bound. */
1232 if (cuddTestInteract(table,xindex,yindex)) {
1233 isolated = table->vars[xindex]->ref == 1;
1234 L += table->subtables[y].keys - isolated;
1235 }
1236 move = (Move *)cuddDynamicAllocNode(table);
1237 if (move == NULL) goto ddGroupSiftingUpOutOfMem;
1238 move->x = x;
1239 move->y = y;
1240 move->flags = MTR_DEFAULT;
1241 move->size = size;
1242 move->next = *moves;
1243 *moves = move;
1244
1245 #ifdef DD_DEBUG
1246 if (pr > 0) (void) fprintf(table->out,
1247 "ddGroupSiftingUp (2 single groups):\n");
1248 #endif
1249 if ((double) size > (double) limitSize * table->maxGrowth)
1250 return(1);
1251 if (size < limitSize) limitSize = size;
1252 } else { /* Group move */
1253 size = ddGroupMove(table,x,y,moves);
1254 if (size == 0) goto ddGroupSiftingUpOutOfMem;
1255 /* Update the lower bound. */
1256 z = (*moves)->y;
1257 do {
1258 zindex = table->invperm[z];
1259 if (cuddTestInteract(table,zindex,yindex)) {
1260 isolated = table->vars[zindex]->ref == 1;
1261 L += table->subtables[z].keys - isolated;
1262 }
1263 z = table->subtables[z].next;
1264 } while (z != (int) (*moves)->y);
1265 if ((double) size > (double) limitSize * table->maxGrowth)
1266 return(1);
1267 if (size < limitSize) limitSize = size;
1268 }
1269 y = gxtop;
1270 x = cuddNextLow(table,y);
1271 }
1272
1273 return(1);
1274
1275 ddGroupSiftingUpOutOfMem:
1276 while (*moves != NULL) {
1277 move = (*moves)->next;
1278 cuddDeallocMove(table, *moves);
1279 *moves = move;
1280 }
1281 return(0);
1282
1283 } /* end of ddGroupSiftingUp */
1284
1285
1286 /**Function********************************************************************
1287
1288 Synopsis [Sifts down a variable until it reaches position xHigh.]
1289
1290 Description [Sifts down a variable until it reaches position xHigh.
1291 Assumes that x is the bottom of a group (or a singleton). Records
1292 all the moves. Returns 1 in case of success; 0 otherwise.]
1293
1294 SideEffects [None]
1295
1296 ******************************************************************************/
1297 static int
ddGroupSiftingDown(DdManager * table,int x,int xHigh,DD_CHKFP checkFunction,Move ** moves)1298 ddGroupSiftingDown(
1299 DdManager * table,
1300 int x,
1301 int xHigh,
1302 DD_CHKFP checkFunction,
1303 Move ** moves)
1304 {
1305 Move *move;
1306 int y;
1307 int size;
1308 int limitSize;
1309 int gxtop,gybot;
1310 int R; /* upper bound on node decrease */
1311 int xindex, yindex;
1312 int isolated, allVars;
1313 int z;
1314 int zindex;
1315 #ifdef DD_DEBUG
1316 int checkR;
1317 #endif
1318
1319 /* If the group consists of simple variables, there is no point in
1320 ** sifting it down. This check is redundant if the projection functions
1321 ** do not have external references, because the computation of the
1322 ** lower bound takes care of the problem. It is necessary otherwise to
1323 ** prevent the sifting down of simple variables. */
1324 y = x;
1325 allVars = 1;
1326 do {
1327 if (table->subtables[y].keys != 1) {
1328 allVars = 0;
1329 break;
1330 }
1331 y = table->subtables[y].next;
1332 } while (table->subtables[y].next != (unsigned) x);
1333 if (allVars)
1334 return(1);
1335
1336 /* Initialize R. */
1337 xindex = table->invperm[x];
1338 gxtop = table->subtables[x].next;
1339 limitSize = size = table->keys - table->isolated;
1340 R = 0;
1341 for (z = xHigh; z > gxtop; z--) {
1342 zindex = table->invperm[z];
1343 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1344 isolated = table->vars[zindex]->ref == 1;
1345 R += table->subtables[z].keys - isolated;
1346 }
1347 }
1348
1349 y = cuddNextHigh(table,x);
1350 while (y <= xHigh && size - R < limitSize) {
1351 #ifdef DD_DEBUG
1352 gxtop = table->subtables[x].next;
1353 checkR = 0;
1354 for (z = xHigh; z > gxtop; z--) {
1355 zindex = table->invperm[z];
1356 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1357 isolated = table->vars[zindex]->ref == 1;
1358 checkR += table->subtables[z].keys - isolated;
1359 }
1360 }
1361 assert(R >= checkR);
1362 #endif
1363 /* Find bottom of y group. */
1364 gybot = table->subtables[y].next;
1365 while (table->subtables[gybot].next != (unsigned) y)
1366 gybot = table->subtables[gybot].next;
1367
1368 if (checkFunction(table,x,y)) {
1369 /* Group found: attach groups and record move. */
1370 gxtop = table->subtables[x].next;
1371 table->subtables[x].next = y;
1372 table->subtables[gybot].next = gxtop;
1373 move = (Move *)cuddDynamicAllocNode(table);
1374 if (move == NULL) goto ddGroupSiftingDownOutOfMem;
1375 move->x = x;
1376 move->y = y;
1377 move->flags = MTR_NEWNODE;
1378 move->size = table->keys - table->isolated;
1379 move->next = *moves;
1380 *moves = move;
1381 } else if (table->subtables[x].next == (unsigned) x &&
1382 table->subtables[y].next == (unsigned) y) {
1383 /* x and y are self groups */
1384 /* Update upper bound on node decrease. */
1385 yindex = table->invperm[y];
1386 if (cuddTestInteract(table,xindex,yindex)) {
1387 isolated = table->vars[yindex]->ref == 1;
1388 R -= table->subtables[y].keys - isolated;
1389 }
1390 size = cuddSwapInPlace(table,x,y);
1391 #ifdef DD_DEBUG
1392 assert(table->subtables[x].next == (unsigned) x);
1393 assert(table->subtables[y].next == (unsigned) y);
1394 #endif
1395 if (size == 0) goto ddGroupSiftingDownOutOfMem;
1396
1397 /* Record move. */
1398 move = (Move *) cuddDynamicAllocNode(table);
1399 if (move == NULL) goto ddGroupSiftingDownOutOfMem;
1400 move->x = x;
1401 move->y = y;
1402 move->flags = MTR_DEFAULT;
1403 move->size = size;
1404 move->next = *moves;
1405 *moves = move;
1406
1407 #ifdef DD_DEBUG
1408 if (pr > 0) (void) fprintf(table->out,
1409 "ddGroupSiftingDown (2 single groups):\n");
1410 #endif
1411 if ((double) size > (double) limitSize * table->maxGrowth)
1412 return(1);
1413 if (size < limitSize) limitSize = size;
1414
1415 x = y;
1416 y = cuddNextHigh(table,x);
1417 } else { /* Group move */
1418 /* Update upper bound on node decrease: first phase. */
1419 gxtop = table->subtables[x].next;
1420 z = gxtop + 1;
1421 do {
1422 zindex = table->invperm[z];
1423 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1424 isolated = table->vars[zindex]->ref == 1;
1425 R -= table->subtables[z].keys - isolated;
1426 }
1427 z++;
1428 } while (z <= gybot);
1429 size = ddGroupMove(table,x,y,moves);
1430 if (size == 0) goto ddGroupSiftingDownOutOfMem;
1431 if ((double) size > (double) limitSize * table->maxGrowth)
1432 return(1);
1433 if (size < limitSize) limitSize = size;
1434
1435 /* Update upper bound on node decrease: second phase. */
1436 gxtop = table->subtables[gybot].next;
1437 for (z = gxtop + 1; z <= gybot; z++) {
1438 zindex = table->invperm[z];
1439 if (zindex == xindex || cuddTestInteract(table,xindex,zindex)) {
1440 isolated = table->vars[zindex]->ref == 1;
1441 R += table->subtables[z].keys - isolated;
1442 }
1443 }
1444 }
1445 x = gybot;
1446 y = cuddNextHigh(table,x);
1447 }
1448
1449 return(1);
1450
1451 ddGroupSiftingDownOutOfMem:
1452 while (*moves != NULL) {
1453 move = (*moves)->next;
1454 cuddDeallocMove(table, *moves);
1455 *moves = move;
1456 }
1457
1458 return(0);
1459
1460 } /* end of ddGroupSiftingDown */
1461
1462
1463 /**Function********************************************************************
1464
1465 Synopsis [Swaps two groups and records the move.]
1466
1467 Description [Swaps two groups and records the move. Returns the
1468 number of keys in the DD table in case of success; 0 otherwise.]
1469
1470 SideEffects [None]
1471
1472 ******************************************************************************/
1473 static int
ddGroupMove(DdManager * table,int x,int y,Move ** moves)1474 ddGroupMove(
1475 DdManager * table,
1476 int x,
1477 int y,
1478 Move ** moves)
1479 {
1480 Move *move;
1481 int size;
1482 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1483 int swapx = -1,swapy = -1;
1484 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1485 int initialSize,bestSize;
1486 #endif
1487
1488 #ifdef DD_DEBUG
1489 /* We assume that x < y */
1490 assert(x < y);
1491 #endif
1492 /* Find top, bottom, and size for the two groups. */
1493 xbot = x;
1494 xtop = table->subtables[x].next;
1495 xsize = xbot - xtop + 1;
1496 ybot = y;
1497 while ((unsigned) ybot < table->subtables[ybot].next)
1498 ybot = table->subtables[ybot].next;
1499 ytop = y;
1500 ysize = ybot - ytop + 1;
1501
1502 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1503 initialSize = bestSize = table->keys - table->isolated;
1504 #endif
1505 /* Sift the variables of the second group up through the first group */
1506 for (i = 1; i <= ysize; i++) {
1507 for (j = 1; j <= xsize; j++) {
1508 size = cuddSwapInPlace(table,x,y);
1509 if (size == 0) goto ddGroupMoveOutOfMem;
1510 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1511 if (size < bestSize)
1512 bestSize = size;
1513 #endif
1514 swapx = x; swapy = y;
1515 y = x;
1516 x = cuddNextLow(table,y);
1517 }
1518 y = ytop + i;
1519 x = cuddNextLow(table,y);
1520 }
1521 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1522 if ((bestSize < initialSize) && (bestSize < size))
1523 (void) fprintf(table->out,"Missed local minimum: initialSize:%d bestSize:%d finalSize:%d\n",initialSize,bestSize,size);
1524 #endif
1525
1526 /* fix groups */
1527 y = xtop; /* ytop is now where xtop used to be */
1528 for (i = 0; i < ysize - 1; i++) {
1529 table->subtables[y].next = cuddNextHigh(table,y);
1530 y = cuddNextHigh(table,y);
1531 }
1532 table->subtables[y].next = xtop; /* y is bottom of its group, join */
1533 /* it to top of its group */
1534 x = cuddNextHigh(table,y);
1535 newxtop = x;
1536 for (i = 0; i < xsize - 1; i++) {
1537 table->subtables[x].next = cuddNextHigh(table,x);
1538 x = cuddNextHigh(table,x);
1539 }
1540 table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1541 /* it to top of its group */
1542 #ifdef DD_DEBUG
1543 if (pr > 0) (void) fprintf(table->out,"ddGroupMove:\n");
1544 #endif
1545
1546 /* Store group move */
1547 move = (Move *) cuddDynamicAllocNode(table);
1548 if (move == NULL) goto ddGroupMoveOutOfMem;
1549 move->x = swapx;
1550 move->y = swapy;
1551 move->flags = MTR_DEFAULT;
1552 move->size = table->keys - table->isolated;
1553 move->next = *moves;
1554 *moves = move;
1555
1556 return(table->keys - table->isolated);
1557
1558 ddGroupMoveOutOfMem:
1559 while (*moves != NULL) {
1560 move = (*moves)->next;
1561 cuddDeallocMove(table, *moves);
1562 *moves = move;
1563 }
1564 return(0);
1565
1566 } /* end of ddGroupMove */
1567
1568
1569 /**Function********************************************************************
1570
1571 Synopsis [Undoes the swap two groups.]
1572
1573 Description [Undoes the swap two groups. Returns 1 in case of
1574 success; 0 otherwise.]
1575
1576 SideEffects [None]
1577
1578 ******************************************************************************/
1579 static int
ddGroupMoveBackward(DdManager * table,int x,int y)1580 ddGroupMoveBackward(
1581 DdManager * table,
1582 int x,
1583 int y)
1584 {
1585 int size;
1586 int i,j,xtop,xbot,xsize,ytop,ybot,ysize,newxtop;
1587
1588
1589 #ifdef DD_DEBUG
1590 /* We assume that x < y */
1591 assert(x < y);
1592 #endif
1593
1594 /* Find top, bottom, and size for the two groups. */
1595 xbot = x;
1596 xtop = table->subtables[x].next;
1597 xsize = xbot - xtop + 1;
1598 ybot = y;
1599 while ((unsigned) ybot < table->subtables[ybot].next)
1600 ybot = table->subtables[ybot].next;
1601 ytop = y;
1602 ysize = ybot - ytop + 1;
1603
1604 /* Sift the variables of the second group up through the first group */
1605 for (i = 1; i <= ysize; i++) {
1606 for (j = 1; j <= xsize; j++) {
1607 size = cuddSwapInPlace(table,x,y);
1608 if (size == 0)
1609 return(0);
1610 y = x;
1611 x = cuddNextLow(table,y);
1612 }
1613 y = ytop + i;
1614 x = cuddNextLow(table,y);
1615 }
1616
1617 /* fix groups */
1618 y = xtop;
1619 for (i = 0; i < ysize - 1; i++) {
1620 table->subtables[y].next = cuddNextHigh(table,y);
1621 y = cuddNextHigh(table,y);
1622 }
1623 table->subtables[y].next = xtop; /* y is bottom of its group, join */
1624 /* to its top */
1625 x = cuddNextHigh(table,y);
1626 newxtop = x;
1627 for (i = 0; i < xsize - 1; i++) {
1628 table->subtables[x].next = cuddNextHigh(table,x);
1629 x = cuddNextHigh(table,x);
1630 }
1631 table->subtables[x].next = newxtop; /* x is bottom of its group, join */
1632 /* to its top */
1633 #ifdef DD_DEBUG
1634 if (pr > 0) (void) fprintf(table->out,"ddGroupMoveBackward:\n");
1635 #endif
1636
1637 return(1);
1638
1639 } /* end of ddGroupMoveBackward */
1640
1641
1642 /**Function********************************************************************
1643
1644 Synopsis [Determines the best position for a variables and returns
1645 it there.]
1646
1647 Description [Determines the best position for a variables and returns
1648 it there. Returns 1 in case of success; 0 otherwise.]
1649
1650 SideEffects [None]
1651
1652 ******************************************************************************/
1653 static int
ddGroupSiftingBackward(DdManager * table,Move * moves,int size,int upFlag,int lazyFlag)1654 ddGroupSiftingBackward(
1655 DdManager * table,
1656 Move * moves,
1657 int size,
1658 int upFlag,
1659 int lazyFlag)
1660 {
1661 Move *move;
1662 int res;
1663 Move *end_move = NULL;
1664 int diff, tmp_diff;
1665 int index;
1666 unsigned int pairlev;
1667
1668 if (lazyFlag) {
1669 end_move = NULL;
1670
1671 /* Find the minimum size, and the earliest position at which it
1672 ** was achieved. */
1673 for (move = moves; move != NULL; move = move->next) {
1674 if (move->size < size) {
1675 size = move->size;
1676 end_move = move;
1677 } else if (move->size == size) {
1678 if (end_move == NULL) end_move = move;
1679 }
1680 }
1681
1682 /* Find among the moves that give minimum size the one that
1683 ** minimizes the distance from the corresponding variable. */
1684 if (moves != NULL) {
1685 diff = Cudd_ReadSize(table) + 1;
1686 index = (upFlag == 1) ?
1687 table->invperm[moves->x] : table->invperm[moves->y];
1688 pairlev =
1689 (unsigned) table->perm[Cudd_bddReadPairIndex(table, index)];
1690
1691 for (move = moves; move != NULL; move = move->next) {
1692 if (move->size == size) {
1693 if (upFlag == 1) {
1694 tmp_diff = (move->x > pairlev) ?
1695 move->x - pairlev : pairlev - move->x;
1696 } else {
1697 tmp_diff = (move->y > pairlev) ?
1698 move->y - pairlev : pairlev - move->y;
1699 }
1700 if (tmp_diff < diff) {
1701 diff = tmp_diff;
1702 end_move = move;
1703 }
1704 }
1705 }
1706 }
1707 } else {
1708 /* Find the minimum size. */
1709 for (move = moves; move != NULL; move = move->next) {
1710 if (move->size < size) {
1711 size = move->size;
1712 }
1713 }
1714 }
1715
1716 /* In case of lazy sifting, end_move identifies the position at
1717 ** which we want to stop. Otherwise, we stop as soon as we meet
1718 ** the minimum size. */
1719 for (move = moves; move != NULL; move = move->next) {
1720 if (lazyFlag) {
1721 if (move == end_move) return(1);
1722 } else {
1723 if (move->size == size) return(1);
1724 }
1725 if ((table->subtables[move->x].next == move->x) &&
1726 (table->subtables[move->y].next == move->y)) {
1727 res = cuddSwapInPlace(table,(int)move->x,(int)move->y);
1728 if (!res) return(0);
1729 #ifdef DD_DEBUG
1730 if (pr > 0) (void) fprintf(table->out,"ddGroupSiftingBackward:\n");
1731 assert(table->subtables[move->x].next == move->x);
1732 assert(table->subtables[move->y].next == move->y);
1733 #endif
1734 } else { /* Group move necessary */
1735 if (move->flags == MTR_NEWNODE) {
1736 ddDissolveGroup(table,(int)move->x,(int)move->y);
1737 } else {
1738 res = ddGroupMoveBackward(table,(int)move->x,(int)move->y);
1739 if (!res) return(0);
1740 }
1741 }
1742
1743 }
1744
1745 return(1);
1746
1747 } /* end of ddGroupSiftingBackward */
1748
1749
1750 /**Function********************************************************************
1751
1752 Synopsis [Merges groups in the DD table.]
1753
1754 Description [Creates a single group from low to high and adjusts the
1755 index field of the tree node.]
1756
1757 SideEffects [None]
1758
1759 ******************************************************************************/
1760 static void
ddMergeGroups(DdManager * table,MtrNode * treenode,int low,int high)1761 ddMergeGroups(
1762 DdManager * table,
1763 MtrNode * treenode,
1764 int low,
1765 int high)
1766 {
1767 int i;
1768 MtrNode *auxnode;
1769 int saveindex;
1770 int newindex;
1771
1772 /* Merge all variables from low to high in one group, unless
1773 ** this is the topmost group. In such a case we do not merge lest
1774 ** we lose the symmetry information. */
1775 if (treenode != table->tree) {
1776 for (i = low; i < high; i++)
1777 table->subtables[i].next = i+1;
1778 table->subtables[high].next = low;
1779 }
1780
1781 /* Adjust the index fields of the tree nodes. If a node is the
1782 ** first child of its parent, then the parent may also need adjustment. */
1783 saveindex = treenode->index;
1784 newindex = table->invperm[low];
1785 auxnode = treenode;
1786 do {
1787 auxnode->index = newindex;
1788 if (auxnode->parent == NULL ||
1789 (int) auxnode->parent->index != saveindex)
1790 break;
1791 auxnode = auxnode->parent;
1792 } while (1);
1793 return;
1794
1795 } /* end of ddMergeGroups */
1796
1797
1798 /**Function********************************************************************
1799
1800 Synopsis [Dissolves a group in the DD table.]
1801
1802 Description [x and y are variables in a group to be cut in two. The cut
1803 is to pass between x and y.]
1804
1805 SideEffects [None]
1806
1807 ******************************************************************************/
1808 static void
ddDissolveGroup(DdManager * table,int x,int y)1809 ddDissolveGroup(
1810 DdManager * table,
1811 int x,
1812 int y)
1813 {
1814 int topx;
1815 int boty;
1816
1817 /* find top and bottom of the two groups */
1818 boty = y;
1819 while ((unsigned) boty < table->subtables[boty].next)
1820 boty = table->subtables[boty].next;
1821
1822 topx = table->subtables[boty].next;
1823
1824 table->subtables[boty].next = y;
1825 table->subtables[x].next = topx;
1826
1827 return;
1828
1829 } /* end of ddDissolveGroup */
1830
1831
1832 /**Function********************************************************************
1833
1834 Synopsis [Pretends to check two variables for aggregation.]
1835
1836 Description [Pretends to check two variables for aggregation. Always
1837 returns 0.]
1838
1839 SideEffects [None]
1840
1841 ******************************************************************************/
1842 static int
ddNoCheck(DdManager * table,int x,int y)1843 ddNoCheck(
1844 DdManager * table,
1845 int x,
1846 int y)
1847 {
1848 return(0);
1849
1850 } /* end of ddNoCheck */
1851
1852
1853 /**Function********************************************************************
1854
1855 Synopsis [Checks two variables for aggregation.]
1856
1857 Description [Checks two variables for aggregation. The check is based
1858 on the second difference of the number of nodes as a function of the
1859 layer. If the second difference is lower than a given threshold
1860 (typically negative) then the two variables should be aggregated.
1861 Returns 1 if the two variables pass the test; 0 otherwise.]
1862
1863 SideEffects [None]
1864
1865 ******************************************************************************/
1866 static int
ddSecDiffCheck(DdManager * table,int x,int y)1867 ddSecDiffCheck(
1868 DdManager * table,
1869 int x,
1870 int y)
1871 {
1872 double Nx,Nx_1;
1873 double Sx;
1874 double threshold;
1875 int xindex,yindex;
1876
1877 if (x==0) return(0);
1878
1879 #ifdef DD_STATS
1880 secdiffcalls++;
1881 #endif
1882 Nx = (double) table->subtables[x].keys;
1883 Nx_1 = (double) table->subtables[x-1].keys;
1884 Sx = (table->subtables[y].keys/Nx) - (Nx/Nx_1);
1885
1886 threshold = table->recomb / 100.0;
1887 if (Sx < threshold) {
1888 xindex = table->invperm[x];
1889 yindex = table->invperm[y];
1890 if (cuddTestInteract(table,xindex,yindex)) {
1891 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1892 (void) fprintf(table->out,
1893 "Second difference for %d = %g Pos(%d)\n",
1894 table->invperm[x],Sx,x);
1895 #endif
1896 #ifdef DD_STATS
1897 secdiff++;
1898 #endif
1899 return(1);
1900 } else {
1901 #ifdef DD_STATS
1902 secdiffmisfire++;
1903 #endif
1904 return(0);
1905 }
1906
1907 }
1908 return(0);
1909
1910 } /* end of ddSecDiffCheck */
1911
1912
1913 /**Function********************************************************************
1914
1915 Synopsis [Checks for extended symmetry of x and y.]
1916
1917 Description [Checks for extended symmetry of x and y. Returns 1 in
1918 case of extended symmetry; 0 otherwise.]
1919
1920 SideEffects [None]
1921
1922 ******************************************************************************/
1923 static int
ddExtSymmCheck(DdManager * table,int x,int y)1924 ddExtSymmCheck(
1925 DdManager * table,
1926 int x,
1927 int y)
1928 {
1929 DdNode *f,*f0,*f1,*f01,*f00,*f11,*f10;
1930 DdNode *one;
1931 unsigned comple; /* f0 is complemented */
1932 int notproj; /* f is not a projection function */
1933 int arccount; /* number of arcs from layer x to layer y */
1934 int TotalRefCount; /* total reference count of layer y minus 1 */
1935 int counter; /* number of nodes of layer x that are allowed */
1936 /* to violate extended symmetry conditions */
1937 int arccounter; /* number of arcs into layer y that are allowed */
1938 /* to come from layers other than x */
1939 int i;
1940 int xindex;
1941 int yindex;
1942 int res;
1943 int slots;
1944 DdNodePtr *list;
1945 DdNode *sentinel = &(table->sentinel);
1946
1947 xindex = table->invperm[x];
1948 yindex = table->invperm[y];
1949
1950 /* If the two variables do not interact, we do not want to merge them. */
1951 if (!cuddTestInteract(table,xindex,yindex))
1952 return(0);
1953
1954 #ifdef DD_DEBUG
1955 /* Checks that x and y do not contain just the projection functions.
1956 ** With the test on interaction, these test become redundant,
1957 ** because an isolated projection function does not interact with
1958 ** any other variable.
1959 */
1960 if (table->subtables[x].keys == 1) {
1961 assert(table->vars[xindex]->ref != 1);
1962 }
1963 if (table->subtables[y].keys == 1) {
1964 assert(table->vars[yindex]->ref != 1);
1965 }
1966 #endif
1967
1968 #ifdef DD_STATS
1969 extsymmcalls++;
1970 #endif
1971
1972 arccount = 0;
1973 counter = (int) (table->subtables[x].keys *
1974 (table->symmviolation/100.0) + 0.5);
1975 one = DD_ONE(table);
1976
1977 slots = table->subtables[x].slots;
1978 list = table->subtables[x].nodelist;
1979 for (i = 0; i < slots; i++) {
1980 f = list[i];
1981 while (f != sentinel) {
1982 /* Find f1, f0, f11, f10, f01, f00. */
1983 f1 = cuddT(f);
1984 f0 = Cudd_Regular(cuddE(f));
1985 comple = Cudd_IsComplement(cuddE(f));
1986 notproj = f1 != one || f0 != one || f->ref != (DdHalfWord) 1;
1987 if (f1->index == (unsigned) yindex) {
1988 arccount++;
1989 f11 = cuddT(f1); f10 = cuddE(f1);
1990 } else {
1991 if ((int) f0->index != yindex) {
1992 /* If f is an isolated projection function it is
1993 ** allowed to bypass layer y.
1994 */
1995 if (notproj) {
1996 if (counter == 0)
1997 return(0);
1998 counter--; /* f bypasses layer y */
1999 }
2000 }
2001 f11 = f10 = f1;
2002 }
2003 if ((int) f0->index == yindex) {
2004 arccount++;
2005 f01 = cuddT(f0); f00 = cuddE(f0);
2006 } else {
2007 f01 = f00 = f0;
2008 }
2009 if (comple) {
2010 f01 = Cudd_Not(f01);
2011 f00 = Cudd_Not(f00);
2012 }
2013
2014 /* Unless we are looking at a projection function
2015 ** without external references except the one from the
2016 ** table, we insist that f01 == f10 or f11 == f00
2017 */
2018 if (notproj) {
2019 if (f01 != f10 && f11 != f00) {
2020 if (counter == 0)
2021 return(0);
2022 counter--;
2023 }
2024 }
2025
2026 f = f->next;
2027 } /* while */
2028 } /* for */
2029
2030 /* Calculate the total reference counts of y */
2031 TotalRefCount = -1; /* -1 for projection function */
2032 slots = table->subtables[y].slots;
2033 list = table->subtables[y].nodelist;
2034 for (i = 0; i < slots; i++) {
2035 f = list[i];
2036 while (f != sentinel) {
2037 TotalRefCount += f->ref;
2038 f = f->next;
2039 }
2040 }
2041
2042 arccounter = (int) (table->subtables[y].keys *
2043 (table->arcviolation/100.0) + 0.5);
2044 res = arccount >= TotalRefCount - arccounter;
2045
2046 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
2047 if (res) {
2048 (void) fprintf(table->out,
2049 "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
2050 xindex,yindex,x,y);
2051 }
2052 #endif
2053
2054 #ifdef DD_STATS
2055 if (res)
2056 extsymm++;
2057 #endif
2058 return(res);
2059
2060 } /* end ddExtSymmCheck */
2061
2062
2063 /**Function********************************************************************
2064
2065 Synopsis [Checks for grouping of x and y.]
2066
2067 Description [Checks for grouping of x and y. Returns 1 in
2068 case of grouping; 0 otherwise. This function is used for lazy sifting.]
2069
2070 SideEffects [None]
2071
2072 ******************************************************************************/
2073 static int
ddVarGroupCheck(DdManager * table,int x,int y)2074 ddVarGroupCheck(
2075 DdManager * table,
2076 int x,
2077 int y)
2078 {
2079 int xindex = table->invperm[x];
2080 int yindex = table->invperm[y];
2081
2082 if (Cudd_bddIsVarToBeUngrouped(table, xindex)) return(0);
2083
2084 if (Cudd_bddReadPairIndex(table, xindex) == yindex) {
2085 if (ddIsVarHandled(table, xindex) ||
2086 ddIsVarHandled(table, yindex)) {
2087 if (Cudd_bddIsVarToBeGrouped(table, xindex) ||
2088 Cudd_bddIsVarToBeGrouped(table, yindex) ) {
2089 if (table->keys - table->isolated <= originalSize) {
2090 return(1);
2091 }
2092 }
2093 }
2094 }
2095
2096 return(0);
2097
2098 } /* end of ddVarGroupCheck */
2099
2100
2101 /**Function********************************************************************
2102
2103 Synopsis [Sets a variable to already handled.]
2104
2105 Description [Sets a variable to already handled. This function is used
2106 for lazy sifting.]
2107
2108 SideEffects [none]
2109
2110 SeeAlso []
2111
2112 ******************************************************************************/
2113 static int
ddSetVarHandled(DdManager * dd,int index)2114 ddSetVarHandled(
2115 DdManager *dd,
2116 int index)
2117 {
2118 if (index >= dd->size || index < 0) return(0);
2119 dd->subtables[dd->perm[index]].varHandled = 1;
2120 return(1);
2121
2122 } /* end of ddSetVarHandled */
2123
2124
2125 /**Function********************************************************************
2126
2127 Synopsis [Resets a variable to be processed.]
2128
2129 Description [Resets a variable to be processed. This function is used
2130 for lazy sifting.]
2131
2132 SideEffects [none]
2133
2134 SeeAlso []
2135
2136 ******************************************************************************/
2137 static int
ddResetVarHandled(DdManager * dd,int index)2138 ddResetVarHandled(
2139 DdManager *dd,
2140 int index)
2141 {
2142 if (index >= dd->size || index < 0) return(0);
2143 dd->subtables[dd->perm[index]].varHandled = 0;
2144 return(1);
2145
2146 } /* end of ddResetVarHandled */
2147
2148
2149 /**Function********************************************************************
2150
2151 Synopsis [Checks whether a variables is already handled.]
2152
2153 Description [Checks whether a variables is already handled. This
2154 function is used for lazy sifting.]
2155
2156 SideEffects [none]
2157
2158 SeeAlso []
2159
2160 ******************************************************************************/
2161 static int
ddIsVarHandled(DdManager * dd,int index)2162 ddIsVarHandled(
2163 DdManager *dd,
2164 int index)
2165 {
2166 if (index >= dd->size || index < 0) return(-1);
2167 return dd->subtables[dd->perm[index]].varHandled;
2168
2169 } /* end of ddIsVarHandled */
2170
2171
2172 ABC_NAMESPACE_IMPL_END
2173
2174