SVF
Functions | Variables
cuddExact.c File Reference
#include "CUDD/util.h"
#include "CUDD/cuddInt.h"

Go to the source code of this file.

Functions

static int getMaxBinomial (int n)
 
static DdHalfWord ** getMatrix (int rows, int cols)
 
static void freeMatrix (DdHalfWord **matrix)
 
static int getLevelKeys (DdManager *table, int l)
 
static int ddShuffle (DdManager *table, DdHalfWord *permutation, int lower, int upper)
 
static int ddSiftUp (DdManager *table, int x, int xLow)
 
static int updateUB (DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper)
 
static int ddCountRoots (DdManager *table, int lower, int upper)
 
static void ddClearGlobal (DdManager *table, int lower, int maxlevel)
 
static int computeLB (DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level)
 
static int updateEntry (DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper)
 
static void pushDown (DdHalfWord *order, int j, int level)
 
static DdHalfWordinitSymmInfo (DdManager *table, int lower, int upper)
 
static int checkSymmInfo (DdManager *table, DdHalfWord *symmInfo, int index, int level)
 
int cuddExact (DdManager *table, int lower, int upper)
 

Variables

static char rcsid [] DD_UNUSED = "$Id: cuddExact.c,v 1.30 2012/02/05 01:07:18 fabio Exp $"
 

Function Documentation

◆ checkSymmInfo()

static int checkSymmInfo ( DdManager table,
DdHalfWord symmInfo,
int  index,
int  level 
)
static

Function********************************************************************

Synopsis [Check symmetry condition.]

Description [Returns 1 if a variable is the one with the highest index among those belonging to a symmetry group that are in the top part of the BDD. The top part is given by level.]

SideEffects [None]

SeeAlso [initSymmInfo]

Definition at line 1004 of file cuddExact.c.

1009 {
1010  int i;
1011 
1012  i = symmInfo[index];
1013  while (i != index) {
1014  if (index < i && table->perm[i] <= level)
1015  return(0);
1016  i = symmInfo[i];
1017  }
1018  return(1);
1019 
1020 } /* end of checkSymmInfo */

◆ computeLB()

static int computeLB ( DdManager table,
DdHalfWord order,
int  roots,
int  cost,
int  lower,
int  upper,
int  level 
)
static

Function********************************************************************

Synopsis [Computes a lower bound on the size of a BDD.]

Description [Computes a lower bound on the size of a BDD from the following factors:

  • size of the lower part of it;
  • size of the part of the upper part not subjected to reordering;
  • number of roots in the part of the BDD subjected to reordering;
  • variable in the support of the roots in the upper part of the BDD subjected to reordering.

    SideEffects [None]

    SeeAlso []

Definition at line 809 of file cuddExact.c.

818 {
819  int i;
820  int lb = cost;
821  int lb1 = 0;
822  int lb2;
823  int support;
824  DdHalfWord ref;
825 
826  /* The levels not involved in reordering are not going to change.
827  ** Add their sizes to the lower bound.
828  */
829  for (i = 0; i < lower; i++) {
830  lb += getLevelKeys(table,i);
831  }
832  /* If a variable is in the support, then there is going
833  ** to be at least one node labeled by that variable.
834  */
835  for (i = lower; i <= lower+level; i++) {
836  support = table->subtables[i].keys > 1 ||
837  table->vars[order[i-lower]]->ref > 1;
838  lb1 += support;
839  }
840 
841  /* Estimate the number of nodes required to connect the roots to
842  ** the nodes in the bottom part. */
843  if (lower+level+1 < table->size) {
844  if (lower+level < upper)
845  ref = table->vars[order[level+1]]->ref;
846  else
847  ref = table->vars[table->invperm[upper+1]]->ref;
848  lb2 = table->subtables[lower+level+1].keys -
849  (ref > (DdHalfWord) 1) - roots;
850  } else {
851  lb2 = 0;
852  }
853 
854  lb += lb1 > lb2 ? lb1 : lb2;
855 
856  return(lb);
857 
858 } /* end of computeLB */
DdHalfWord ref
Definition: cudd.h:272
unsigned int keys
Definition: cuddInt.h:314
unsigned short DdHalfWord
Definition: cudd.h:259
int size
Definition: cuddInt.h:345
static int getLevelKeys(DdManager *table, int l)
Definition: cuddExact.c:505
DdSubtable * subtables
Definition: cuddInt.h:349
DdNode ** vars
Definition: cuddInt.h:373
int * invperm
Definition: cuddInt.h:371

◆ cuddExact()

int cuddExact ( DdManager table,
int  lower,
int  upper 
)

AutomaticEnd Function********************************************************************

Synopsis [Exact variable ordering algorithm.]

Description [Exact variable ordering algorithm. Finds an optimum order for the variables between lower and upper. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 149 of file cuddExact.c.

153 {
154  int k, i, j;
155  int maxBinomial, oldSubsets, newSubsets;
156  int subsetCost;
157  int size; /* number of variables to be reordered */
158  int unused, nvars, level, result;
159  int upperBound, lowerBound, cost;
160  int roots;
161  char *mask = NULL;
162  DdHalfWord *symmInfo = NULL;
163  DdHalfWord **newOrder = NULL;
164  DdHalfWord **oldOrder = NULL;
165  int *newCost = NULL;
166  int *oldCost = NULL;
167  DdHalfWord **tmpOrder;
168  int *tmpCost;
169  DdHalfWord *bestOrder = NULL;
170  DdHalfWord *order;
171 #ifdef DD_STATS
172  int ddTotalSubsets;
173 #endif
174 
175  /* Restrict the range to be reordered by excluding unused variables
176  ** at the two ends. */
177  while (table->subtables[lower].keys == 1 &&
178  table->vars[table->invperm[lower]]->ref == 1 &&
179  lower < upper)
180  lower++;
181  while (table->subtables[upper].keys == 1 &&
182  table->vars[table->invperm[upper]]->ref == 1 &&
183  lower < upper)
184  upper--;
185  if (lower == upper) return(1); /* trivial problem */
186 
187  /* Apply symmetric sifting to get a good upper bound and to extract
188  ** symmetry information. */
189  result = cuddSymmSiftingConv(table,lower,upper);
190  if (result == 0) goto cuddExactOutOfMem;
191 
192 #ifdef DD_STATS
193  (void) fprintf(table->out,"\n");
194  ddTotalShuffles = 0;
195  ddTotalSubsets = 0;
196 #endif
197 
198  /* Initialization. */
199  nvars = table->size;
200  size = upper - lower + 1;
201  /* Count unused variable among those to be reordered. This is only
202  ** used to compute maxBinomial. */
203  unused = 0;
204  for (i = lower + 1; i < upper; i++) {
205  if (table->subtables[i].keys == 1 &&
206  table->vars[table->invperm[i]]->ref == 1)
207  unused++;
208  }
209 
210  /* Find the maximum number of subsets we may have to store. */
211  maxBinomial = getMaxBinomial(size - unused);
212  if (maxBinomial == -1) goto cuddExactOutOfMem;
213 
214  newOrder = getMatrix(maxBinomial, size);
215  if (newOrder == NULL) goto cuddExactOutOfMem;
216 
217  newCost = ALLOC(int, maxBinomial);
218  if (newCost == NULL) goto cuddExactOutOfMem;
219 
220  oldOrder = getMatrix(maxBinomial, size);
221  if (oldOrder == NULL) goto cuddExactOutOfMem;
222 
223  oldCost = ALLOC(int, maxBinomial);
224  if (oldCost == NULL) goto cuddExactOutOfMem;
225 
226  bestOrder = ALLOC(DdHalfWord, size);
227  if (bestOrder == NULL) goto cuddExactOutOfMem;
228 
229  mask = ALLOC(char, nvars);
230  if (mask == NULL) goto cuddExactOutOfMem;
231 
232  symmInfo = initSymmInfo(table, lower, upper);
233  if (symmInfo == NULL) goto cuddExactOutOfMem;
234 
235  roots = ddCountRoots(table, lower, upper);
236 
237  /* Initialize the old order matrix for the empty subset and the best
238  ** order to the current order. The cost for the empty subset includes
239  ** the cost of the levels between upper and the constants. These levels
240  ** are not going to change. Hence, we count them only once.
241  */
242  oldSubsets = 1;
243  for (i = 0; i < size; i++) {
244  oldOrder[0][i] = bestOrder[i] = (DdHalfWord) table->invperm[i+lower];
245  }
246  subsetCost = table->constants.keys;
247  for (i = upper + 1; i < nvars; i++)
248  subsetCost += getLevelKeys(table,i);
249  oldCost[0] = subsetCost;
250  /* The upper bound is initialized to the current size of the BDDs. */
251  upperBound = table->keys - table->isolated;
252 
253  /* Now consider subsets of increasing size. */
254  for (k = 1; k <= size; k++) {
255 #ifdef DD_STATS
256  (void) fprintf(table->out,"Processing subsets of size %d\n", k);
257  fflush(table->out);
258 #endif
259  newSubsets = 0;
260  level = size - k; /* offset of first bottom variable */
261 
262  for (i = 0; i < oldSubsets; i++) { /* for each subset of size k-1 */
263  order = oldOrder[i];
264  cost = oldCost[i];
265  lowerBound = computeLB(table, order, roots, cost, lower, upper,
266  level);
267  if (lowerBound >= upperBound)
268  continue;
269  /* Impose new order. */
270  result = ddShuffle(table, order, lower, upper);
271  if (result == 0) goto cuddExactOutOfMem;
272  upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
273  /* For each top bottom variable. */
274  for (j = level; j >= 0; j--) {
275  /* Skip unused variables. */
276  if (table->subtables[j+lower-1].keys == 1 &&
277  table->vars[table->invperm[j+lower-1]]->ref == 1) continue;
278  /* Find cost under this order. */
279  subsetCost = cost + getLevelKeys(table, lower + level);
280  newSubsets = updateEntry(table, order, level, subsetCost,
281  newOrder, newCost, newSubsets, mask,
282  lower, upper);
283  if (j == 0)
284  break;
285  if (checkSymmInfo(table, symmInfo, order[j-1], level) == 0)
286  continue;
287  pushDown(order,j-1,level);
288  /* Impose new order. */
289  result = ddShuffle(table, order, lower, upper);
290  if (result == 0) goto cuddExactOutOfMem;
291  upperBound = updateUB(table,upperBound,bestOrder,lower,upper);
292  } /* for each bottom variable */
293  } /* for each subset of size k */
294 
295  /* New orders become old orders in preparation for next iteration. */
296  tmpOrder = oldOrder; tmpCost = oldCost;
297  oldOrder = newOrder; oldCost = newCost;
298  newOrder = tmpOrder; newCost = tmpCost;
299 #ifdef DD_STATS
300  ddTotalSubsets += newSubsets;
301 #endif
302  oldSubsets = newSubsets;
303  }
304  result = ddShuffle(table, bestOrder, lower, upper);
305  if (result == 0) goto cuddExactOutOfMem;
306 #ifdef DD_STATS
307 #ifdef DD_VERBOSE
308  (void) fprintf(table->out,"\n");
309 #endif
310  (void) fprintf(table->out,"#:S_EXACT %8d: total subsets\n",
311  ddTotalSubsets);
312  (void) fprintf(table->out,"#:H_EXACT %8d: total shuffles",
313  ddTotalShuffles);
314 #endif
315 
316  freeMatrix(newOrder);
317  freeMatrix(oldOrder);
318  FREE(bestOrder);
319  FREE(oldCost);
320  FREE(newCost);
321  FREE(symmInfo);
322  FREE(mask);
323  return(1);
324 
325 cuddExactOutOfMem:
326 
327  if (newOrder != NULL) freeMatrix(newOrder);
328  if (oldOrder != NULL) freeMatrix(oldOrder);
329  if (bestOrder != NULL) FREE(bestOrder);
330  if (oldCost != NULL) FREE(oldCost);
331  if (newCost != NULL) FREE(newCost);
332  if (symmInfo != NULL) FREE(symmInfo);
333  if (mask != NULL) FREE(mask);
334  table->errorCode = CUDD_MEMORY_OUT;
335  return(0);
336 
337 } /* end of cuddExact */
DdHalfWord ref
Definition: cudd.h:272
unsigned int keys
Definition: cuddInt.h:314
unsigned short DdHalfWord
Definition: cudd.h:259
static int ddShuffle(DdManager *table, DdHalfWord *permutation, int lower, int upper)
Definition: cuddExact.c:537
static int computeLB(DdManager *table, DdHalfWord *order, int roots, int cost, int lower, int upper, int level)
Definition: cuddExact.c:809
#define FREE(obj)
Definition: util.h:80
static void freeMatrix(DdHalfWord **matrix)
Definition: cuddExact.c:482
static int getMaxBinomial(int n)
Definition: cuddExact.c:359
int size
Definition: cuddInt.h:345
static int getLevelKeys(DdManager *table, int l)
Definition: cuddExact.c:505
static void pushDown(DdHalfWord *order, int j, int level)
Definition: cuddExact.c:930
DdSubtable * subtables
Definition: cuddInt.h:349
static int updateUB(DdManager *table, int oldBound, DdHalfWord *bestOrder, int lower, int upper)
Definition: cuddExact.c:654
int cuddSymmSiftingConv(DdManager *table, int lower, int upper)
Definition: cuddSymmetry.c:439
unsigned int keys
Definition: cuddInt.h:353
#define ALLOC(type, num)
Definition: util.h:76
FILE * out
Definition: cuddInt.h:423
static DdHalfWord ** getMatrix(int rows, int cols)
Definition: cuddExact.c:447
static int checkSymmInfo(DdManager *table, DdHalfWord *symmInfo, int index, int level)
Definition: cuddExact.c:1004
static int ddCountRoots(DdManager *table, int lower, int upper)
Definition: cuddExact.c:696
static DdHalfWord * initSymmInfo(DdManager *table, int lower, int upper)
Definition: cuddExact.c:968
static int updateEntry(DdManager *table, DdHalfWord *order, int level, int cost, DdHalfWord **orders, int *costs, int subsets, char *mask, int lower, int upper)
Definition: cuddExact.c:876
DdNode ** vars
Definition: cuddInt.h:373
int * invperm
Definition: cuddInt.h:371
DdSubtable constants
Definition: cuddInt.h:351
static int result
Definition: cuddGenetic.c:121
int isolated
Definition: cuddInt.h:368
Cudd_ErrorType errorCode
Definition: cuddInt.h:425

◆ ddClearGlobal()

static void ddClearGlobal ( DdManager table,
int  lower,
int  maxlevel 
)
static

Function********************************************************************

Synopsis [Scans the DD and clears the LSB of the next pointers.]

Description [Scans the DD and clears the LSB of the next pointers. The LSB of the next pointers are used as markers to tell whether a node was reached. Once the roots are counted, these flags are reset.]

SideEffects [None]

SeeAlso [ddCountRoots]

Definition at line 763 of file cuddExact.c.

767 {
768  int i,j;
769  DdNode *f;
770  DdNodePtr *nodelist;
771  DdNode *sentinel = &(table->sentinel);
772  int slots;
773 
774  for (i = lower; i <= maxlevel; i++) {
775  nodelist = table->subtables[i].nodelist;
776  slots = table->subtables[i].slots;
777  for (j = 0; j < slots; j++) {
778  f = nodelist[j];
779  while (f != sentinel) {
780  f->next = Cudd_Regular(f->next);
781  f = f->next;
782  }
783  }
784  }
785 
786 } /* end of ddClearGlobal */
Definition: cudd.h:270
#define Cudd_Regular(node)
Definition: cudd.h:384
DdSubtable * subtables
Definition: cuddInt.h:349
DdNode sentinel
Definition: cuddInt.h:328
DdNode * next
Definition: cudd.h:273
DdNode ** nodelist
Definition: cuddInt.h:311
unsigned int slots
Definition: cuddInt.h:313

◆ ddCountRoots()

static int ddCountRoots ( DdManager table,
int  lower,
int  upper 
)
static

Function********************************************************************

Synopsis [Counts the number of roots.]

Description [Counts the number of roots at the levels between lower and upper. The computation is based on breadth-first search. A node is a root if it is not reachable from any previously visited node. (All the nodes at level lower are therefore considered roots.) The visited flag uses the LSB of the next pointer. Returns the root count. The roots that are constant nodes are always ignored.]

SideEffects [None]

SeeAlso [ddClearGlobal]

Definition at line 696 of file cuddExact.c.

700 {
701  int i,j;
702  DdNode *f;
703  DdNodePtr *nodelist;
704  DdNode *sentinel = &(table->sentinel);
705  int slots;
706  int roots = 0;
707  int maxlevel = lower;
708 
709  for (i = lower; i <= upper; i++) {
710  nodelist = table->subtables[i].nodelist;
711  slots = table->subtables[i].slots;
712  for (j = 0; j < slots; j++) {
713  f = nodelist[j];
714  while (f != sentinel) {
715  /* A node is a root of the DAG if it cannot be
716  ** reached by nodes above it. If a node was never
717  ** reached during the previous depth-first searches,
718  ** then it is a root, and we start a new depth-first
719  ** search from it.
720  */
721  if (!Cudd_IsComplement(f->next)) {
722  if (f != table->vars[f->index]) {
723  roots++;
724  }
725  }
726  if (!Cudd_IsConstant(cuddT(f))) {
727  cuddT(f)->next = Cudd_Complement(cuddT(f)->next);
728  if (table->perm[cuddT(f)->index] > maxlevel)
729  maxlevel = table->perm[cuddT(f)->index];
730  }
731  if (!Cudd_IsConstant(cuddE(f))) {
732  Cudd_Regular(cuddE(f))->next =
734  if (table->perm[Cudd_Regular(cuddE(f))->index] > maxlevel)
735  maxlevel = table->perm[Cudd_Regular(cuddE(f))->index];
736  }
737  f = Cudd_Regular(f->next);
738  }
739  }
740  }
741  ddClearGlobal(table, lower, maxlevel);
742 
743  return(roots);
744 
745 } /* end of ddCountRoots */
static void ddClearGlobal(DdManager *table, int lower, int maxlevel)
Definition: cuddExact.c:763
Definition: cudd.h:270
#define Cudd_IsConstant(node)
Definition: cudd.h:339
#define Cudd_Regular(node)
Definition: cudd.h:384
DdSubtable * subtables
Definition: cuddInt.h:349
#define Cudd_IsComplement(node)
Definition: cudd.h:412
DdNode sentinel
Definition: cuddInt.h:328
DdNode * next
Definition: cudd.h:273
DdNode ** nodelist
Definition: cuddInt.h:311
#define Cudd_Complement(node)
Definition: cudd.h:398
#define cuddT(node)
Definition: cuddInt.h:609
DdHalfWord index
Definition: cudd.h:271
unsigned int slots
Definition: cuddInt.h:313
DdNode ** vars
Definition: cuddInt.h:373
#define cuddE(node)
Definition: cuddInt.h:625
int * perm
Definition: cuddInt.h:369

◆ ddShuffle()

static int ddShuffle ( DdManager table,
DdHalfWord permutation,
int  lower,
int  upper 
)
static

Function********************************************************************

Synopsis [Reorders variables according to a given permutation.]

Description [Reorders variables according to a given permutation. The i-th permutation array contains the index of the variable that should be brought to the i-th level. ddShuffle assumes that no dead nodes are present and that the interaction matrix is properly initialized. The reordering is achieved by a series of upward sifts. Returns 1 if successful; 0 otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 537 of file cuddExact.c.

542 {
543  DdHalfWord index;
544  int level;
545  int position;
546 #if 0
547  int numvars;
548 #endif
549  int result;
550 #ifdef DD_STATS
551  unsigned long localTime;
552  int initialSize;
553 #ifdef DD_VERBOSE
554  int finalSize;
555 #endif
556  int previousSize;
557 #endif
558 
559 #ifdef DD_STATS
560  localTime = util_cpu_time();
561  initialSize = table->keys - table->isolated;
562 #endif
563 
564 #if 0
565  numvars = table->size;
566 
567  (void) fprintf(table->out,"%d:", ddTotalShuffles);
568  for (level = 0; level < numvars; level++) {
569  (void) fprintf(table->out," %d", table->invperm[level]);
570  }
571  (void) fprintf(table->out,"\n");
572 #endif
573 
574  for (level = 0; level <= upper - lower; level++) {
575  index = permutation[level];
576  position = table->perm[index];
577 #ifdef DD_STATS
578  previousSize = table->keys - table->isolated;
579 #endif
580  result = ddSiftUp(table,position,level+lower);
581  if (!result) return(0);
582  }
583 
584 #ifdef DD_STATS
585  ddTotalShuffles++;
586 #ifdef DD_VERBOSE
587  finalSize = table->keys - table->isolated;
588  if (finalSize < initialSize) {
589  (void) fprintf(table->out,"-");
590  } else if (finalSize > initialSize) {
591  (void) fprintf(table->out,"+");
592  } else {
593  (void) fprintf(table->out,"=");
594  }
595  if ((ddTotalShuffles & 63) == 0) (void) fprintf(table->out,"\n");
596  fflush(table->out);
597 #endif
598 #endif
599 
600  return(1);
601 
602 } /* end of ddShuffle */
unsigned short DdHalfWord
Definition: cudd.h:259
int size
Definition: cuddInt.h:345
unsigned int keys
Definition: cuddInt.h:353
FILE * out
Definition: cuddInt.h:423
static int numvars
Definition: cuddGenetic.c:107
long util_cpu_time(void)
Definition: cpu_time.c:34
int * invperm
Definition: cuddInt.h:371
static int ddSiftUp(DdManager *table, int x, int xLow)
Definition: cuddExact.c:619
static int result
Definition: cuddGenetic.c:121
int isolated
Definition: cuddInt.h:368
int * perm
Definition: cuddInt.h:369

◆ ddSiftUp()

static int ddSiftUp ( DdManager table,
int  x,
int  xLow 
)
static

Function********************************************************************

Synopsis [Moves one variable up.]

Description [Takes a variable from position x and sifts it up to position xLow; xLow should be less than or equal to x. Returns 1 if successful; 0 otherwise]

SideEffects [None]

SeeAlso []

Definition at line 619 of file cuddExact.c.

623 {
624  int y;
625  int size;
626 
627  y = cuddNextLow(table,x);
628  while (y >= xLow) {
629  size = cuddSwapInPlace(table,y,x);
630  if (size == 0) {
631  return(0);
632  }
633  x = y;
634  y = cuddNextLow(table,x);
635  }
636  return(1);
637 
638 } /* end of ddSiftUp */
int cuddNextLow(DdManager *table, int x)
Definition: cuddReorder.c:737
int cuddSwapInPlace(DdManager *table, int x, int y)
Definition: cuddReorder.c:760

◆ freeMatrix()

static void freeMatrix ( DdHalfWord **  matrix)
static

Function********************************************************************

Synopsis [Frees a two-dimensional matrix allocated by getMatrix.]

Description []

SideEffects [None]

SeeAlso [getMatrix]

Definition at line 482 of file cuddExact.c.

484 {
485  FREE(matrix[0]);
486  FREE(matrix);
487  return;
488 
489 } /* end of freeMatrix */
#define FREE(obj)
Definition: util.h:80

◆ getLevelKeys()

static int getLevelKeys ( DdManager table,
int  l 
)
static

Function********************************************************************

Synopsis [Returns the number of nodes at one level of a unique table.]

Description [Returns the number of nodes at one level of a unique table. The projection function, if isolated, is not counted.]

SideEffects [None]

SeeAlso []

Definition at line 505 of file cuddExact.c.

508 {
509  int isolated;
510  int x; /* x is an index */
511 
512  x = table->invperm[l];
513  isolated = table->vars[x]->ref == 1;
514 
515  return(table->subtables[l].keys - isolated);
516 
517 } /* end of getLevelKeys */
DdHalfWord ref
Definition: cudd.h:272
unsigned int keys
Definition: cuddInt.h:314
DdSubtable * subtables
Definition: cuddInt.h:349
DdNode ** vars
Definition: cuddInt.h:373
int * invperm
Definition: cuddInt.h:371

◆ getMatrix()

static DdHalfWord ** getMatrix ( int  rows,
int  cols 
)
static

Function********************************************************************

Synopsis [Allocates a two-dimensional matrix of ints.]

Description [Allocates a two-dimensional matrix of ints. Returns the pointer to the matrix if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [freeMatrix]

Definition at line 447 of file cuddExact.c.

450 {
451  DdHalfWord **matrix;
452  int i;
453 
454  if (cols*rows == 0) return(NULL);
455  matrix = ALLOC(DdHalfWord *, rows);
456  if (matrix == NULL) return(NULL);
457  matrix[0] = ALLOC(DdHalfWord, cols*rows);
458  if (matrix[0] == NULL) {
459  FREE(matrix);
460  return(NULL);
461  }
462  for (i = 1; i < rows; i++) {
463  matrix[i] = matrix[i-1] + cols;
464  }
465  return(matrix);
466 
467 } /* end of getMatrix */
unsigned short DdHalfWord
Definition: cudd.h:259
#define FREE(obj)
Definition: util.h:80
#define ALLOC(type, num)
Definition: util.h:76

◆ getMaxBinomial()

static int getMaxBinomial ( int  n)
static

AutomaticStart

Function********************************************************************

Synopsis [Returns the maximum value of (n choose k) for a given n.]

Description [Computes the maximum value of (n choose k) for a given n. The maximum value occurs for k = n/2 when n is even, or k = (n-1)/2 when n is odd. The algorithm used in this procedure avoids intermediate overflow problems. It is based on the identity

  binomial(n,k) = n/k * binomial(n-1,k-1).

Returns the computed value if successful; -1 if out of range.]

SideEffects [None]

SeeAlso []

Definition at line 359 of file cuddExact.c.

361 {
362  double i, j, result;
363 
364  if (n < 0 || n > 33) return(-1); /* error */
365  if (n < 2) return(1);
366 
367  for (result = (double)((n+3)/2), i = result+1, j=2; i <= n; i++, j++) {
368  result *= i;
369  result /= j;
370  }
371 
372  return((int)result);
373 
374 } /* end of getMaxBinomial */
static int result
Definition: cuddGenetic.c:121

◆ initSymmInfo()

static DdHalfWord * initSymmInfo ( DdManager table,
int  lower,
int  upper 
)
static

Function********************************************************************

Synopsis [Gathers symmetry information.]

Description [Translates the symmetry information stored in the next field of each subtable from level to indices. This procedure is called immediately after symmetric sifting, so that the next fields are correct. By translating this informaton in terms of indices, we make it independent of subsequent reorderings. The format used is that of the next fields: a circular list where each variable points to the next variable in the same symmetry group. Only the entries between lower and upper are considered. The procedure returns a pointer to an array holding the symmetry information if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [checkSymmInfo]

Definition at line 968 of file cuddExact.c.

972 {
973  int level, index, next, nextindex;
974  DdHalfWord *symmInfo;
975 
976  symmInfo = ALLOC(DdHalfWord, table->size);
977  if (symmInfo == NULL) return(NULL);
978 
979  for (level = lower; level <= upper; level++) {
980  index = table->invperm[level];
981  next = table->subtables[level].next;
982  nextindex = table->invperm[next];
983  symmInfo[index] = nextindex;
984  }
985  return(symmInfo);
986 
987 } /* end of initSymmInfo */
unsigned short DdHalfWord
Definition: cudd.h:259
int size
Definition: cuddInt.h:345
DdSubtable * subtables
Definition: cuddInt.h:349
#define ALLOC(type, num)
Definition: util.h:76
unsigned int next
Definition: cuddInt.h:317
int * invperm
Definition: cuddInt.h:371

◆ pushDown()

static void pushDown ( DdHalfWord order,
int  j,
int  level 
)
static

Function********************************************************************

Synopsis [Pushes a variable in the order down to position "level."]

Description []

SideEffects [None]

SeeAlso []

Definition at line 930 of file cuddExact.c.

934 {
935  int i;
936  DdHalfWord tmp;
937 
938  tmp = order[j];
939  for (i = j; i < level; i++) {
940  order[i] = order[i+1];
941  }
942  order[level] = tmp;
943  return;
944 
945 } /* end of pushDown */
unsigned short DdHalfWord
Definition: cudd.h:259

◆ updateEntry()

static int updateEntry ( DdManager table,
DdHalfWord order,
int  level,
int  cost,
DdHalfWord **  orders,
int *  costs,
int  subsets,
char *  mask,
int  lower,
int  upper 
)
static

Function********************************************************************

Synopsis [Updates entry for a subset.]

Description [Updates entry for a subset. Finds the subset, if it exists. If the new order for the subset has lower cost, or if the subset did not exist, it stores the new order and cost. Returns the number of subsets currently in the table.]

SideEffects [None]

SeeAlso []

Definition at line 876 of file cuddExact.c.

887 {
888  int i, j;
889  int size = upper - lower + 1;
890 
891  /* Build a mask that says what variables are in this subset. */
892  for (i = lower; i <= upper; i++)
893  mask[table->invperm[i]] = 0;
894  for (i = level; i < size; i++)
895  mask[order[i]] = 1;
896 
897  /* Check each subset until a match is found or all subsets are examined. */
898  for (i = 0; i < subsets; i++) {
899  DdHalfWord *subset = orders[i];
900  for (j = level; j < size; j++) {
901  if (mask[subset[j]] == 0)
902  break;
903  }
904  if (j == size) /* no mismatches: success */
905  break;
906  }
907  if (i == subsets || cost < costs[i]) { /* add or replace */
908  for (j = 0; j < size; j++)
909  orders[i][j] = order[j];
910  costs[i] = cost;
911  subsets += (i == subsets);
912  }
913  return(subsets);
914 
915 } /* end of updateEntry */
unsigned short DdHalfWord
Definition: cudd.h:259
int * invperm
Definition: cuddInt.h:371

◆ updateUB()

static int updateUB ( DdManager table,
int  oldBound,
DdHalfWord bestOrder,
int  lower,
int  upper 
)
static

Function********************************************************************

Synopsis [Updates the upper bound and saves the best order seen so far.]

Description [Updates the upper bound and saves the best order seen so far. Returns the current value of the upper bound.]

SideEffects [None]

SeeAlso []

Definition at line 654 of file cuddExact.c.

660 {
661  int i;
662  int newBound = table->keys - table->isolated;
663 
664  if (newBound < oldBound) {
665 #ifdef DD_STATS
666  (void) fprintf(table->out,"New upper bound = %d\n", newBound);
667  fflush(table->out);
668 #endif
669  for (i = lower; i <= upper; i++)
670  bestOrder[i-lower] = (DdHalfWord) table->invperm[i];
671  return(newBound);
672  } else {
673  return(oldBound);
674  }
675 
676 } /* end of updateUB */
unsigned short DdHalfWord
Definition: cudd.h:259
unsigned int keys
Definition: cuddInt.h:353
FILE * out
Definition: cuddInt.h:423
int * invperm
Definition: cuddInt.h:371
int isolated
Definition: cuddInt.h:368

Variable Documentation

◆ DD_UNUSED

char rcsid [] DD_UNUSED = "$Id: cuddExact.c,v 1.30 2012/02/05 01:07:18 fabio Exp $"
static

CFile***********************************************************************

FileName [cuddExact.c]

PackageName [cudd]

Synopsis [Functions for exact variable reordering.]

Description [External procedures included in this file:

Internal procedures included in this module:

Static procedures included in this module:

]

Author [Cheng Hua, Fabio Somenzi]

Copyright [Copyright (c) 1995-2012, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 91 of file cuddExact.c.