1 /**CFile***********************************************************************
7 Synopsis [Functions for group sifting.]
9 Description [External procedures included in this file:
11 <li> Cudd_MakeTreeNode()
13 Internal procedures included in this file:
15 <li> cuddTreeSifting()
17 Static procedures included in this module:
19 <li> ddTreeSiftingAux()
20 <li> ddCountInternalMtrNodes()
21 <li> ddReorderChildren()
23 <li> ddUniqueCompareGroup()
26 <li> ddGroupSiftingAux()
27 <li> ddGroupSiftingUp()
28 <li> ddGroupSiftingDown()
30 <li> ddGroupMoveBackward()
31 <li> ddGroupSiftingBackward()
33 <li> ddDissolveGroup()
37 <li> ddVarGroupCheck()
38 <li> ddSetVarHandled()
39 <li> ddResetVarHandled()
43 Author [Shipra Panda, Fabio Somenzi]
45 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
49 Redistribution and use in source and binary forms, with or without
50 modification, are permitted provided that the following conditions
53 Redistributions of source code must retain the above copyright
54 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
77 ******************************************************************************/
82 /*---------------------------------------------------------------------------*/
83 /* Constant declarations */
84 /*---------------------------------------------------------------------------*/
86 /* Constants for lazy sifting */
87 #define DD_NORMAL_SIFT 0
88 #define DD_LAZY_SIFT 1
90 /* Constants for sifting up and down */
91 #define DD_SIFT_DOWN 0
94 /*---------------------------------------------------------------------------*/
95 /* Stucture declarations */
96 /*---------------------------------------------------------------------------*/
98 /*---------------------------------------------------------------------------*/
99 /* Type declarations */
100 /*---------------------------------------------------------------------------*/
105 typedef int (*DD_CHKFP
)(DdManager
*, int, int);
110 /*---------------------------------------------------------------------------*/
111 /* Variable declarations */
112 /*---------------------------------------------------------------------------*/
115 static char rcsid
[] DD_UNUSED
= "$Id: cuddGroup.c,v 1.44 2009/02/21 18:24:10 fabio Exp $";
119 extern int ddTotalNumberSwapping
;
121 extern int ddTotalNISwaps
;
122 static int extsymmcalls
;
124 static int secdiffcalls
;
126 static int secdiffmisfire
;
129 static int pr
= 0; /* flag to enable printing while debugging */
130 /* by depositing a 1 into it */
132 static unsigned int originalSize
;
134 /*---------------------------------------------------------------------------*/
135 /* Macro declarations */
136 /*---------------------------------------------------------------------------*/
142 /**AutomaticStart*************************************************************/
144 /*---------------------------------------------------------------------------*/
145 /* Static function prototypes */
146 /*---------------------------------------------------------------------------*/
148 static int ddTreeSiftingAux (DdManager
*table
, MtrNode
*treenode
, Cudd_ReorderingType method
);
150 static int ddCountInternalMtrNodes (DdManager
*table
, MtrNode
*treenode
);
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
);
173 /**AutomaticEnd***************************************************************/
179 /*---------------------------------------------------------------------------*/
180 /* Definition of exported functions */
181 /*---------------------------------------------------------------------------*/
184 /**Function********************************************************************
186 Synopsis [Creates a new variable group.]
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.]
196 SideEffects [The variable tree is changed.]
198 SeeAlso [Cudd_MakeZddTreeNode]
200 ******************************************************************************/
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 */)
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.
217 level
= (low
< (unsigned int) dd
->size
) ? dd
->perm
[low
] : low
;
219 if (level
+ size
- 1> (int) MTR_MAXHIGH
)
222 /* If the tree does not exist yet, create it. */
225 dd
->tree
= tree
= Mtr_InitGroupTree(0, dd
->size
);
228 tree
->index
= dd
->invperm
[0];
231 /* Extend the upper bound of the tree if necessary. This allows the
232 ** application to create groups even before the variables are created.
234 tree
->size
= ddMax(tree
->size
, ddMax(level
+ size
, (unsigned) dd
->size
));
236 /* Create the group. */
237 group
= Mtr_MakeGroup(tree
, level
, size
, type
);
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.
245 group
->index
= (MtrHalfWord
) low
;
249 } /* end of Cudd_MakeTreeNode */
252 /*---------------------------------------------------------------------------*/
253 /* Definition of internal functions */
254 /*---------------------------------------------------------------------------*/
257 /**Function********************************************************************
259 Synopsis [Tree sifting algorithm.]
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.]
268 ******************************************************************************/
271 DdManager
* table
/* DD table */,
272 Cudd_ReorderingType method
/* reordering method for the groups of leaves */)
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
283 tempTree
= table
->tree
== NULL
;
285 table
->tree
= Mtr_InitGroupTree(0,table
->size
);
286 table
->tree
->index
= table
->invperm
[0];
291 if (pr
> 0 && !tempTree
) (void) fprintf(table
->out
,"cuddTreeSifting:");
292 Mtr_PrintGroups(table
->tree
,pr
<= 0);
302 (void) fprintf(table
->out
,"\n");
304 (void) fprintf(table
->out
,"#:IM_NODES %8d: group tree nodes\n",
305 ddCountInternalMtrNodes(table
,table
->tree
));
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.
312 for (i
= 0; i
< nvars
; i
++)
313 table
->subtables
[i
].next
= i
;
317 result
= ddTreeSiftingAux(table
, table
->tree
, method
);
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
);
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
);
335 Cudd_FreeTree(table
);
338 } /* end of cuddTreeSifting */
341 /*---------------------------------------------------------------------------*/
342 /* Definition of static functions */
343 /*---------------------------------------------------------------------------*/
346 /**Function********************************************************************
348 Synopsis [Visits the group tree and reorders each group.]
350 Description [Recursively visits the group tree and reorders each
351 group in postorder fashion. Returns 1 if successful; 0 otherwise.]
355 ******************************************************************************/
360 Cudd_ReorderingType method
)
364 Cudd_AggregationType saveCheck
;
367 Mtr_PrintGroups(treenode
,1);
371 while (auxnode
!= NULL
) {
372 if (auxnode
->child
!= NULL
) {
373 if (!ddTreeSiftingAux(table
, auxnode
->child
, method
))
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
);
380 res
= ddReorderChildren(table
, auxnode
, CUDD_REORDER_LAZY_SIFT
);
381 table
->groupcheck
= saveCheck
;
385 } else if (auxnode
->size
> 1) {
386 if (!ddReorderChildren(table
, auxnode
, method
))
389 auxnode
= auxnode
->younger
;
394 } /* end of ddTreeSiftingAux */
398 /**Function********************************************************************
400 Synopsis [Counts the number of internal nodes of the group tree.]
402 Description [Counts the number of internal nodes of the group tree.
407 ******************************************************************************/
409 ddCountInternalMtrNodes(
419 while (auxnode
!= NULL
) {
420 if (!(MTR_TEST(auxnode
,MTR_TERMINAL
))) {
422 count
= ddCountInternalMtrNodes(table
,auxnode
->child
);
425 auxnode
= auxnode
->younger
;
430 } /* end of ddCountInternalMtrNodes */
434 /**Function********************************************************************
436 Synopsis [Reorders the children of a group tree node according to
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.]
447 ******************************************************************************/
452 Cudd_ReorderingType method
)
457 unsigned int initialSize
;
459 ddFindNodeHiLo(table
,treenode
,&lower
,&upper
);
460 /* If upper == -1 these variables do not exist yet. */
464 if (treenode
->flags
== MTR_FIXED
) {
468 (void) fprintf(table
->out
," ");
471 case CUDD_REORDER_RANDOM
:
472 case CUDD_REORDER_RANDOM_PIVOT
:
473 result
= cuddSwapping(table
,lower
,upper
,method
);
475 case CUDD_REORDER_SIFT
:
476 result
= cuddSifting(table
,lower
,upper
);
478 case CUDD_REORDER_SIFT_CONVERGE
:
480 initialSize
= table
->keys
- table
->isolated
;
481 result
= cuddSifting(table
,lower
,upper
);
482 if (initialSize
<= table
->keys
- table
->isolated
)
486 (void) fprintf(table
->out
,"\n");
488 } while (result
!= 0);
490 case CUDD_REORDER_SYMM_SIFT
:
491 result
= cuddSymmSifting(table
,lower
,upper
);
493 case CUDD_REORDER_SYMM_SIFT_CONV
:
494 result
= cuddSymmSiftingConv(table
,lower
,upper
);
496 case CUDD_REORDER_GROUP_SIFT
:
497 if (table
->groupcheck
== CUDD_NO_CHECK
) {
498 result
= ddGroupSifting(table
,lower
,upper
,ddNoCheck
,
500 } else if (table
->groupcheck
== CUDD_GROUP_CHECK5
) {
501 result
= ddGroupSifting(table
,lower
,upper
,ddExtSymmCheck
,
503 } else if (table
->groupcheck
== CUDD_GROUP_CHECK7
) {
504 result
= ddGroupSifting(table
,lower
,upper
,ddExtSymmCheck
,
507 (void) fprintf(table
->err
,
508 "Unknown group ckecking method\n");
512 case CUDD_REORDER_GROUP_SIFT_CONV
:
514 initialSize
= table
->keys
- table
->isolated
;
515 if (table
->groupcheck
== CUDD_NO_CHECK
) {
516 result
= ddGroupSifting(table
,lower
,upper
,ddNoCheck
,
518 } else if (table
->groupcheck
== CUDD_GROUP_CHECK5
) {
519 result
= ddGroupSifting(table
,lower
,upper
,ddExtSymmCheck
,
521 } else if (table
->groupcheck
== CUDD_GROUP_CHECK7
) {
522 result
= ddGroupSifting(table
,lower
,upper
,ddExtSymmCheck
,
525 (void) fprintf(table
->err
,
526 "Unknown group ckecking method\n");
530 (void) fprintf(table
->out
,"\n");
532 result
= cuddWindowReorder(table
,lower
,upper
,
533 CUDD_REORDER_WINDOW4
);
534 if (initialSize
<= table
->keys
- table
->isolated
)
538 (void) fprintf(table
->out
,"\n");
540 } while (result
!= 0);
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
);
550 case CUDD_REORDER_ANNEALING
:
551 result
= cuddAnnealing(table
,lower
,upper
);
553 case CUDD_REORDER_GENETIC
:
554 result
= cuddGa(table
,lower
,upper
);
556 case CUDD_REORDER_LINEAR
:
557 result
= cuddLinearAndSifting(table
,lower
,upper
);
559 case CUDD_REORDER_LINEAR_CONVERGE
:
561 initialSize
= table
->keys
- table
->isolated
;
562 result
= cuddLinearAndSifting(table
,lower
,upper
);
563 if (initialSize
<= table
->keys
- table
->isolated
)
567 (void) fprintf(table
->out
,"\n");
569 } while (result
!= 0);
571 case CUDD_REORDER_EXACT
:
572 result
= cuddExact(table
,lower
,upper
);
574 case CUDD_REORDER_LAZY_SIFT
:
575 result
= ddGroupSifting(table
,lower
,upper
,ddVarGroupCheck
,
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.
587 ddMergeGroups(table
,treenode
,lower
,upper
);
590 if (pr
> 0) (void) fprintf(table
->out
,"ddReorderChildren:");
595 } /* end of ddReorderChildren */
598 /**Function********************************************************************
600 Synopsis [Finds the lower and upper bounds of the group represented
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.]
607 SideEffects [The bounds are returned as side effects.]
611 ******************************************************************************/
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.
626 if ((int) treenode
->low
>= table
->size
) {
627 *lower
= table
->size
;
632 *lower
= low
= (unsigned int) table
->perm
[treenode
->index
];
633 high
= (int) (low
+ treenode
->size
- 1);
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.
643 MtrNode
*auxnode
= treenode
->child
;
644 if (auxnode
== NULL
) {
645 *upper
= (unsigned int) table
->size
- 1;
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.
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
;
661 /* Normal case: All the variables of the group exist. */
662 *upper
= (unsigned int) high
;
666 /* Make sure that all variables in group are contiguous. */
667 assert(treenode
->size
>= *upper
- *lower
+ 1);
672 } /* end of ddFindNodeHiLo */
675 /**Function********************************************************************
677 Synopsis [Comparison function used by qsort.]
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
686 ******************************************************************************/
688 ddUniqueCompareGroup(
693 if (entry
[*ptrY
] == entry
[*ptrX
]) {
694 return((*ptrX
) - (*ptrY
));
697 return(entry
[*ptrY
] - entry
[*ptrX
]);
699 } /* end of ddUniqueCompareGroup */
702 /**Function********************************************************************
704 Synopsis [Sifts from treenode->low to treenode->high.]
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.]
714 ******************************************************************************/
720 DD_CHKFP checkFunction
,
732 unsigned previousSize
;
738 /* Order variables to sift. */
741 var
= ALLOC(int,nvars
);
743 table
->errorCode
= CUDD_MEMORY_OUT
;
744 goto ddGroupSiftingOutOfMem
;
746 entry
= ALLOC(int,nvars
);
748 table
->errorCode
= CUDD_MEMORY_OUT
;
749 goto ddGroupSiftingOutOfMem
;
751 sifted
= ALLOC(int,nvars
);
752 if (sifted
== NULL
) {
753 table
->errorCode
= CUDD_MEMORY_OUT
;
754 goto ddGroupSiftingOutOfMem
;
757 /* Here we consider only one representative for each group. */
758 for (i
= 0, classes
= 0; i
< nvars
; i
++) {
761 if ((unsigned) x
>= table
->subtables
[x
].next
) {
762 entry
[i
] = table
->subtables
[x
].keys
;
768 qsort((void *)var
,classes
,sizeof(int),
769 (DD_QSFP
) ddUniqueCompareGroup
);
772 for (i
= 0; i
< nvars
; i
++) {
773 ddResetVarHandled(table
, i
);
778 for (i
= 0; i
< ddMin(table
->siftMaxVar
,classes
); i
++) {
779 if (ddTotalNumberSwapping
>= table
->siftMaxSwap
)
782 if (sifted
[xindex
] == 1) /* variable already sifted as part of group */
784 x
= table
->perm
[xindex
]; /* find current level of this variable */
786 if (x
< lower
|| x
> upper
|| table
->subtables
[x
].bindVar
== 1)
789 previousSize
= table
->keys
- table
->isolated
;
792 /* x is bottom of group */
793 assert((unsigned) x
>= table
->subtables
[x
].next
);
795 if ((unsigned) x
== table
->subtables
[x
].next
) {
797 result
= ddGroupSiftingAux(table
,x
,lower
,upper
,checkFunction
,
801 result
= ddGroupSiftingAux(table
,x
,lower
,upper
,ddNoCheck
,lazyFlag
);
803 if (!result
) goto ddGroupSiftingOutOfMem
;
805 /* check for aggregation */
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)) {
814 ddCreateGroup(table
,x
,x
+1);
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
)) {
821 ddCreateGroup(table
,x
-1,x
);
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
;
832 result
= ddGroupSiftingAux(table
,x
,lower
,upper
,ddNoCheck
,lazyFlag
);
833 if (!result
) goto ddGroupSiftingOutOfMem
;
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
,"^");
840 (void) fprintf(table
->out
,"*");
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
,"+");
849 (void) fprintf(table
->out
,"=");
855 /* Mark variables in the group just sifted. */
856 x
= table
->perm
[xindex
];
857 if ((unsigned) x
!= table
->subtables
[x
].next
) {
860 j
= table
->invperm
[x
];
862 x
= table
->subtables
[x
].next
;
863 } while (x
!= xInit
);
865 /* Dissolve the group if it was created. */
866 if (lazyFlag
== 0 && dissolve
) {
868 j
= table
->subtables
[x
].next
;
869 table
->subtables
[x
].next
= x
;
871 } while (x
!= xInit
);
876 if (pr
> 0) (void) fprintf(table
->out
,"ddGroupSifting:");
879 if (lazyFlag
) ddSetVarHandled(table
, xindex
);
888 ddGroupSiftingOutOfMem
:
889 if (entry
!= NULL
) FREE(entry
);
890 if (var
!= NULL
) FREE(var
);
891 if (sifted
!= NULL
) FREE(sifted
);
895 } /* end of ddGroupSifting */
898 /**Function********************************************************************
900 Synopsis [Creates a group encompassing variables from x to y in the
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.]
909 ******************************************************************************/
922 /* Find bottom of second group. */
924 while ((unsigned) gybot
< table
->subtables
[gybot
].next
)
925 gybot
= table
->subtables
[gybot
].next
;
928 table
->subtables
[x
].next
= y
;
929 table
->subtables
[gybot
].next
= x
;
933 } /* ddCreateGroup */
936 /**Function********************************************************************
938 Synopsis [Sifts one variable up and down until it has taken all
939 positions. Checks for aggregation.]
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.]
950 ******************************************************************************/
957 DD_CHKFP checkFunction
,
961 Move
*moves
; /* list of moves */
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 */
973 initialSize
= table
->keys
- table
->isolated
;
976 originalSize
= initialSize
; /* for lazy sifting */
978 /* If we have a singleton, we check for aggregation in both
979 ** directions before we sift.
981 if ((unsigned) x
== table
->subtables
[x
].next
) {
982 /* Will go down first, unless x == xHigh:
983 ** Look for aggregation above x.
985 for (y
= x
; y
> xLow
; y
--) {
986 if (!checkFunction(table
,y
-1,y
))
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 */
994 /* Will go up first unless x == xlow:
995 ** Look for aggregation below x.
997 for (y
= x
; y
< xHigh
; y
++) {
998 if (!checkFunction(table
,y
,y
+1))
1000 /* find bottom of y+1's group */
1002 while ((unsigned) topbot
< table
->subtables
[topbot
].next
) {
1003 topbot
= table
->subtables
[topbot
].next
;
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 */
1011 /* Now x may be in the middle of a group.
1012 ** Find bottom of x's group.
1014 while ((unsigned) x
< table
->subtables
[x
].next
)
1015 x
= table
->subtables
[x
].next
;
1017 if (x
== xLow
) { /* Sift down */
1019 /* x must be a singleton */
1020 assert((unsigned) x
== table
->subtables
[x
].next
);
1022 if (x
== xHigh
) return(1); /* just one variable */
1024 if (!ddGroupSiftingDown(table
,x
,xHigh
,checkFunction
,&moves
))
1025 goto ddGroupSiftingAuxOutOfMem
;
1026 /* at this point x == xHigh, unless early term */
1028 /* move backward and stop at best position */
1029 result
= ddGroupSiftingBackward(table
,moves
,initialSize
,
1030 DD_SIFT_DOWN
,lazyFlag
);
1032 assert(table
->keys
- table
->isolated
<= (unsigned) initialSize
);
1034 if (!result
) goto ddGroupSiftingAuxOutOfMem
;
1036 } else if (cuddNextHigh(table
,x
) > xHigh
) { /* Sift up */
1038 /* x is bottom of group */
1039 assert((unsigned) x
>= table
->subtables
[x
].next
);
1041 /* Find top of x's group */
1042 x
= table
->subtables
[x
].next
;
1044 if (!ddGroupSiftingUp(table
,x
,xLow
,checkFunction
,&moves
))
1045 goto ddGroupSiftingAuxOutOfMem
;
1046 /* at this point x == xLow, unless early term */
1048 /* move backward and stop at best position */
1049 result
= ddGroupSiftingBackward(table
,moves
,initialSize
,
1050 DD_SIFT_UP
,lazyFlag
);
1052 assert(table
->keys
- table
->isolated
<= (unsigned) initialSize
);
1054 if (!result
) goto ddGroupSiftingAuxOutOfMem
;
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 */
1061 /* Find top of group */
1065 while ((unsigned) x
< table
->subtables
[x
].next
)
1066 x
= table
->subtables
[x
].next
;
1067 x
= table
->subtables
[x
].next
;
1069 /* x should be the top of a group */
1070 assert((unsigned) x
<= table
->subtables
[x
].next
);
1073 if (!ddGroupSiftingUp(table
,x
,xLow
,checkFunction
,&moves
))
1074 goto ddGroupSiftingAuxOutOfMem
;
1076 /* move backward and stop at best position */
1077 result
= ddGroupSiftingBackward(table
,moves
,initialSize
,
1078 DD_SIFT_UP
,lazyFlag
);
1080 assert(table
->keys
- table
->isolated
<= (unsigned) initialSize
);
1082 if (!result
) goto ddGroupSiftingAuxOutOfMem
;
1084 } else { /* moving up first: shorter */
1085 /* Find top of x's group */
1086 x
= table
->subtables
[x
].next
;
1088 if (!ddGroupSiftingUp(table
,x
,xLow
,checkFunction
,&moves
))
1089 goto ddGroupSiftingAuxOutOfMem
;
1090 /* at this point x == xHigh, unless early term */
1095 while ((unsigned) x
< table
->subtables
[x
].next
)
1096 x
= table
->subtables
[x
].next
;
1098 /* x is bottom of a group */
1099 assert((unsigned) x
>= table
->subtables
[x
].next
);
1102 if (!ddGroupSiftingDown(table
,x
,xHigh
,checkFunction
,&moves
))
1103 goto ddGroupSiftingAuxOutOfMem
;
1105 /* move backward and stop at best position */
1106 result
= ddGroupSiftingBackward(table
,moves
,initialSize
,
1107 DD_SIFT_DOWN
,lazyFlag
);
1109 assert(table
->keys
- table
->isolated
<= (unsigned) initialSize
);
1111 if (!result
) goto ddGroupSiftingAuxOutOfMem
;
1114 while (moves
!= NULL
) {
1116 cuddDeallocMove(table
, moves
);
1122 ddGroupSiftingAuxOutOfMem
:
1123 while (moves
!= NULL
) {
1125 cuddDeallocMove(table
, moves
);
1131 } /* end of ddGroupSiftingAux */
1134 /**Function********************************************************************
1136 Synopsis [Sifts up a variable until either it reaches position xLow
1137 or the size of the DD heap increases too much.]
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.]
1148 ******************************************************************************/
1154 DD_CHKFP checkFunction
,
1167 int L
; /* lower bound on DD size */
1172 yindex
= table
->invperm
[y
];
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.
1183 limitSize
= L
= table
->keys
- table
->isolated
;
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
;
1195 x
= cuddNextLow(table
,y
);
1196 while (x
>= xLow
&& L
<= limitSize
) {
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
;
1209 if (pr
> 0 && L
!= checkL
) {
1210 (void) fprintf(table
->out
,
1211 "Inaccurate lower bound: L = %d checkL = %d\n",
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
;
1227 move
->flags
= MTR_NEWNODE
;
1228 move
->size
= table
->keys
- table
->isolated
;
1229 move
->next
= *moves
;
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
);
1237 assert(table
->subtables
[x
].next
== (unsigned) x
);
1238 assert(table
->subtables
[y
].next
== (unsigned) y
);
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
;
1246 move
= (Move
*)cuddDynamicAllocNode(table
);
1247 if (move
== NULL
) goto ddGroupSiftingUpOutOfMem
;
1250 move
->flags
= MTR_DEFAULT
;
1252 move
->next
= *moves
;
1256 if (pr
> 0) (void) fprintf(table
->out
,
1257 "ddGroupSiftingUp (2 single groups):\n");
1259 if ((double) size
> (double) limitSize
* table
->maxGrowth
)
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. */
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
;
1273 z
= table
->subtables
[z
].next
;
1274 } while (z
!= (int) (*moves
)->y
);
1275 if ((double) size
> (double) limitSize
* table
->maxGrowth
)
1277 if (size
< limitSize
) limitSize
= size
;
1280 x
= cuddNextLow(table
,y
);
1285 ddGroupSiftingUpOutOfMem
:
1286 while (*moves
!= NULL
) {
1287 move
= (*moves
)->next
;
1288 cuddDeallocMove(table
, *moves
);
1293 } /* end of ddGroupSiftingUp */
1296 /**Function********************************************************************
1298 Synopsis [Sifts down a variable until it reaches position xHigh.]
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.]
1306 ******************************************************************************/
1312 DD_CHKFP checkFunction
,
1320 int R
; /* upper bound on node decrease */
1322 int isolated
, allVars
;
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. */
1337 if (table
->subtables
[y
].keys
!= 1) {
1341 y
= table
->subtables
[y
].next
;
1342 } while (table
->subtables
[y
].next
!= (unsigned) x
);
1347 xindex
= table
->invperm
[x
];
1348 gxtop
= table
->subtables
[x
].next
;
1349 limitSize
= size
= table
->keys
- table
->isolated
;
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
;
1359 y
= cuddNextHigh(table
,x
);
1360 while (y
<= xHigh
&& size
- R
< limitSize
) {
1362 gxtop
= table
->subtables
[x
].next
;
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
;
1371 assert(R
>= checkR
);
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
;
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
;
1387 move
->flags
= MTR_NEWNODE
;
1388 move
->size
= table
->keys
- table
->isolated
;
1389 move
->next
= *moves
;
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
;
1400 size
= cuddSwapInPlace(table
,x
,y
);
1402 assert(table
->subtables
[x
].next
== (unsigned) x
);
1403 assert(table
->subtables
[y
].next
== (unsigned) y
);
1405 if (size
== 0) goto ddGroupSiftingDownOutOfMem
;
1408 move
= (Move
*) cuddDynamicAllocNode(table
);
1409 if (move
== NULL
) goto ddGroupSiftingDownOutOfMem
;
1412 move
->flags
= MTR_DEFAULT
;
1414 move
->next
= *moves
;
1418 if (pr
> 0) (void) fprintf(table
->out
,
1419 "ddGroupSiftingDown (2 single groups):\n");
1421 if ((double) size
> (double) limitSize
* table
->maxGrowth
)
1423 if (size
< limitSize
) limitSize
= size
;
1426 y
= cuddNextHigh(table
,x
);
1427 } else { /* Group move */
1428 /* Update upper bound on node decrease: first phase. */
1429 gxtop
= table
->subtables
[x
].next
;
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
;
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
)
1443 if (size
< limitSize
) limitSize
= size
;
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
;
1456 y
= cuddNextHigh(table
,x
);
1461 ddGroupSiftingDownOutOfMem
:
1462 while (*moves
!= NULL
) {
1463 move
= (*moves
)->next
;
1464 cuddDeallocMove(table
, *moves
);
1470 } /* end of ddGroupSiftingDown */
1473 /**Function********************************************************************
1475 Synopsis [Swaps two groups and records the move.]
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.]
1482 ******************************************************************************/
1492 int i
,j
,xtop
,xbot
,xsize
,ytop
,ybot
,ysize
,newxtop
;
1494 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1495 int initialSize
,bestSize
;
1499 /* We assume that x < y */
1502 /* Find top, bottom, and size for the two groups. */
1504 xtop
= table
->subtables
[x
].next
;
1505 xsize
= xbot
- xtop
+ 1;
1507 while ((unsigned) ybot
< table
->subtables
[ybot
].next
)
1508 ybot
= table
->subtables
[ybot
].next
;
1510 ysize
= ybot
- ytop
+ 1;
1512 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
1513 initialSize
= bestSize
= table
->keys
- table
->isolated
;
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
)
1524 swapx
= x
; swapy
= y
;
1526 x
= cuddNextLow(table
,y
);
1529 x
= cuddNextLow(table
,y
);
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
);
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
);
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
);
1546 for (i
= 0; i
< xsize
- 1; i
++) {
1547 table
->subtables
[x
].next
= cuddNextHigh(table
,x
);
1548 x
= cuddNextHigh(table
,x
);
1550 table
->subtables
[x
].next
= newxtop
; /* x is bottom of its group, join */
1551 /* it to top of its group */
1553 if (pr
> 0) (void) fprintf(table
->out
,"ddGroupMove:\n");
1556 /* Store group move */
1557 move
= (Move
*) cuddDynamicAllocNode(table
);
1558 if (move
== NULL
) goto ddGroupMoveOutOfMem
;
1561 move
->flags
= MTR_DEFAULT
;
1562 move
->size
= table
->keys
- table
->isolated
;
1563 move
->next
= *moves
;
1566 return(table
->keys
- table
->isolated
);
1568 ddGroupMoveOutOfMem
:
1569 while (*moves
!= NULL
) {
1570 move
= (*moves
)->next
;
1571 cuddDeallocMove(table
, *moves
);
1576 } /* end of ddGroupMove */
1579 /**Function********************************************************************
1581 Synopsis [Undoes the swap two groups.]
1583 Description [Undoes the swap two groups. Returns 1 in case of
1584 success; 0 otherwise.]
1588 ******************************************************************************/
1590 ddGroupMoveBackward(
1596 int i
,j
,xtop
,xbot
,xsize
,ytop
,ybot
,ysize
,newxtop
;
1600 /* We assume that x < y */
1604 /* Find top, bottom, and size for the two groups. */
1606 xtop
= table
->subtables
[x
].next
;
1607 xsize
= xbot
- xtop
+ 1;
1609 while ((unsigned) ybot
< table
->subtables
[ybot
].next
)
1610 ybot
= table
->subtables
[ybot
].next
;
1612 ysize
= ybot
- ytop
+ 1;
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
);
1621 x
= cuddNextLow(table
,y
);
1624 x
= cuddNextLow(table
,y
);
1629 for (i
= 0; i
< ysize
- 1; i
++) {
1630 table
->subtables
[y
].next
= cuddNextHigh(table
,y
);
1631 y
= cuddNextHigh(table
,y
);
1633 table
->subtables
[y
].next
= xtop
; /* y is bottom of its group, join */
1635 x
= cuddNextHigh(table
,y
);
1637 for (i
= 0; i
< xsize
- 1; i
++) {
1638 table
->subtables
[x
].next
= cuddNextHigh(table
,x
);
1639 x
= cuddNextHigh(table
,x
);
1641 table
->subtables
[x
].next
= newxtop
; /* x is bottom of its group, join */
1644 if (pr
> 0) (void) fprintf(table
->out
,"ddGroupMoveBackward:\n");
1649 } /* end of ddGroupMoveBackward */
1652 /**Function********************************************************************
1654 Synopsis [Determines the best position for a variables and returns
1657 Description [Determines the best position for a variables and returns
1658 it there. Returns 1 in case of success; 0 otherwise.]
1662 ******************************************************************************/
1664 ddGroupSiftingBackward(
1676 unsigned int pairlev
;
1681 /* Find the minimum size, and the earliest position at which it
1683 for (move
= moves
; move
!= NULL
; move
= move
->next
) {
1684 if (move
->size
< size
) {
1687 } else if (move
->size
== size
) {
1688 if (end_move
== NULL
) end_move
= move
;
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
];
1699 (unsigned) table
->perm
[Cudd_bddReadPairIndex(table
, index
)];
1701 for (move
= moves
; move
!= NULL
; move
= move
->next
) {
1702 if (move
->size
== size
) {
1704 tmp_diff
= (move
->x
> pairlev
) ?
1705 move
->x
- pairlev
: pairlev
- move
->x
;
1707 tmp_diff
= (move
->y
> pairlev
) ?
1708 move
->y
- pairlev
: pairlev
- move
->y
;
1710 if (tmp_diff
< diff
) {
1718 /* Find the minimum size. */
1719 for (move
= moves
; move
!= NULL
; move
= move
->next
) {
1720 if (move
->size
< size
) {
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
) {
1731 if (move
== end_move
) return(1);
1733 if (move
->size
== size
) return(1);
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);
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
);
1744 } else { /* Group move necessary */
1745 if (move
->flags
== MTR_NEWNODE
) {
1746 ddDissolveGroup(table
,(int)move
->x
,(int)move
->y
);
1748 res
= ddGroupMoveBackward(table
,(int)move
->x
,(int)move
->y
);
1749 if (!res
) return(0);
1757 } /* end of ddGroupSiftingBackward */
1760 /**Function********************************************************************
1762 Synopsis [Merges groups in the DD table.]
1764 Description [Creates a single group from low to high and adjusts the
1765 index field of the tree node.]
1769 ******************************************************************************/
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
;
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
];
1797 auxnode
->index
= newindex
;
1798 if (auxnode
->parent
== NULL
||
1799 (int) auxnode
->parent
->index
!= saveindex
)
1801 auxnode
= auxnode
->parent
;
1805 } /* end of ddMergeGroups */
1808 /**Function********************************************************************
1810 Synopsis [Dissolves a group in the DD table.]
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.]
1817 ******************************************************************************/
1827 /* find top and bottom of the two groups */
1829 while ((unsigned) boty
< table
->subtables
[boty
].next
)
1830 boty
= table
->subtables
[boty
].next
;
1832 topx
= table
->subtables
[boty
].next
;
1834 table
->subtables
[boty
].next
= y
;
1835 table
->subtables
[x
].next
= topx
;
1839 } /* end of ddDissolveGroup */
1842 /**Function********************************************************************
1844 Synopsis [Pretends to check two variables for aggregation.]
1846 Description [Pretends to check two variables for aggregation. Always
1851 ******************************************************************************/
1860 } /* end of ddNoCheck */
1863 /**Function********************************************************************
1865 Synopsis [Checks two variables for aggregation.]
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.]
1875 ******************************************************************************/
1887 if (x
==0) return(0);
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
);
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
);
1920 } /* end of ddSecDiffCheck */
1923 /**Function********************************************************************
1925 Synopsis [Checks for extended symmetry of x and y.]
1927 Description [Checks for extended symmetry of x and y. Returns 1 in
1928 case of extended symmetry; 0 otherwise.]
1932 ******************************************************************************/
1939 DdNode
*f
,*f0
,*f1
,*f01
,*f00
,*f11
,*f10
;
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 */
1955 DdNode
*sentinel
= &(table
->sentinel
);
1957 xindex
= table
->invperm
[x
];
1958 yindex
= table
->invperm
[y
];
1960 /* If the two variables do not interact, we do not want to merge them. */
1961 if (!cuddTestInteract(table
,xindex
,yindex
))
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.
1970 if (table
->subtables
[x
].keys
== 1) {
1971 assert(table
->vars
[xindex
]->ref
!= 1);
1973 if (table
->subtables
[y
].keys
== 1) {
1974 assert(table
->vars
[yindex
]->ref
!= 1);
1983 counter
= (int) (table
->subtables
[x
].keys
*
1984 (table
->symmviolation
/100.0) + 0.5);
1985 one
= DD_ONE(table
);
1987 slots
= table
->subtables
[x
].slots
;
1988 list
= table
->subtables
[x
].nodelist
;
1989 for (i
= 0; i
< slots
; i
++) {
1991 while (f
!= sentinel
) {
1992 /* Find f1, f0, f11, f10, f01, f00. */
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
) {
1999 f11
= cuddT(f1
); f10
= cuddE(f1
);
2001 if ((int) f0
->index
!= yindex
) {
2002 /* If f is an isolated projection function it is
2003 ** allowed to bypass layer y.
2008 counter
--; /* f bypasses layer y */
2013 if ((int) f0
->index
== yindex
) {
2015 f01
= cuddT(f0
); f00
= cuddE(f0
);
2020 f01
= Cudd_Not(f01
);
2021 f00
= Cudd_Not(f00
);
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
2029 if (f01
!= f10
&& f11
!= f00
) {
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
++) {
2046 while (f
!= sentinel
) {
2047 TotalRefCount
+= f
->ref
;
2052 arccounter
= (int) (table
->subtables
[y
].keys
*
2053 (table
->arcviolation
/100.0) + 0.5);
2054 res
= arccount
>= TotalRefCount
- arccounter
;
2056 #if defined(DD_DEBUG) && defined(DD_VERBOSE)
2058 (void) fprintf(table
->out
,
2059 "Found extended symmetry! x = %d\ty = %d\tPos(%d,%d)\n",
2070 } /* end ddExtSymmCheck */
2073 /**Function********************************************************************
2075 Synopsis [Checks for grouping of x and y.]
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.]
2082 ******************************************************************************/
2089 int xindex
= table
->invperm
[x
];
2090 int yindex
= table
->invperm
[y
];
2092 if (Cudd_bddIsVarToBeUngrouped(table
, xindex
)) return(0);
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
) {
2108 } /* end of ddVarGroupCheck */
2111 /**Function********************************************************************
2113 Synopsis [Sets a variable to already handled.]
2115 Description [Sets a variable to already handled. This function is used
2122 ******************************************************************************/
2128 if (index
>= dd
->size
|| index
< 0) return(0);
2129 dd
->subtables
[dd
->perm
[index
]].varHandled
= 1;
2132 } /* end of ddSetVarHandled */
2135 /**Function********************************************************************
2137 Synopsis [Resets a variable to be processed.]
2139 Description [Resets a variable to be processed. This function is used
2146 ******************************************************************************/
2152 if (index
>= dd
->size
|| index
< 0) return(0);
2153 dd
->subtables
[dd
->perm
[index
]].varHandled
= 0;
2156 } /* end of ddResetVarHandled */
2159 /**Function********************************************************************
2161 Synopsis [Checks whether a variables is already handled.]
2163 Description [Checks whether a variables is already handled. This
2164 function is used for lazy sifting.]
2170 ******************************************************************************/
2176 if (index
>= dd
->size
|| index
< 0) return(-1);
2177 return dd
->subtables
[dd
->perm
[index
]].varHandled
;
2179 } /* end of ddIsVarHandled */