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