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