abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddTable.c
Go to the documentation of this file.
1 /**CFile***********************************************************************
2 
3  FileName [cuddTable.c]
4 
5  PackageName [cudd]
6 
7  Synopsis [Unique table management functions.]
8 
9  Description [External procedures included in this module:
10  <ul>
11  <li> Cudd_Prime()
12  </ul>
13  Internal procedures included in this module:
14  <ul>
15  <li> cuddAllocNode()
16  <li> cuddInitTable()
17  <li> cuddFreeTable()
18  <li> cuddGarbageCollect()
19  <li> cuddZddGetNode()
20  <li> cuddZddGetNodeIVO()
21  <li> cuddUniqueInter()
22  <li> cuddUniqueInterIVO()
23  <li> cuddUniqueInterZdd()
24  <li> cuddUniqueConst()
25  <li> cuddRehash()
26  <li> cuddShrinkSubtable()
27  <li> cuddInsertSubtables()
28  <li> cuddDestroySubtables()
29  <li> cuddResizeTableZdd()
30  <li> cuddSlowTableGrowth()
31  </ul>
32  Static procedures included in this module:
33  <ul>
34  <li> ddRehashZdd()
35  <li> ddResizeTable()
36  <li> cuddFindParent()
37  <li> cuddOrderedInsert()
38  <li> cuddOrderedThread()
39  <li> cuddRotateLeft()
40  <li> cuddRotateRight()
41  <li> cuddDoRebalance()
42  <li> cuddCheckCollisionOrdering()
43  </ul>]
44 
45  SeeAlso []
46 
47  Author [Fabio Somenzi]
48 
49  Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
50 
51  All rights reserved.
52 
53  Redistribution and use in source and binary forms, with or without
54  modification, are permitted provided that the following conditions
55  are met:
56 
57  Redistributions of source code must retain the above copyright
58  notice, this list of conditions and the following disclaimer.
59 
60  Redistributions in binary form must reproduce the above copyright
61  notice, this list of conditions and the following disclaimer in the
62  documentation and/or other materials provided with the distribution.
63 
64  Neither the name of the University of Colorado nor the names of its
65  contributors may be used to endorse or promote products derived from
66  this software without specific prior written permission.
67 
68  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
69  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
70  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
71  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
72  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
73  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
74  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
75  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
76  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
77  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
78  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
79  POSSIBILITY OF SUCH DAMAGE.]
80 
81 ******************************************************************************/
82 
83 #include "misc/util/util_hack.h"
84 #include "cuddInt.h"
85 
86 ABC_NAMESPACE_IMPL_START
87 
88 
89 
90 /*---------------------------------------------------------------------------*/
91 /* Constant declarations */
92 /*---------------------------------------------------------------------------*/
93 
94 #ifndef DD_UNSORTED_FREE_LIST
95 #ifdef DD_RED_BLACK_FREE_LIST
96 /* Constants for red/black trees. */
97 #define DD_STACK_SIZE 128
98 #define DD_RED 0
99 #define DD_BLACK 1
100 #define DD_PAGE_SIZE 8192
101 #define DD_PAGE_MASK ~(DD_PAGE_SIZE - 1)
102 #endif
103 #endif
104 
105 /*---------------------------------------------------------------------------*/
106 /* Stucture declarations */
107 /*---------------------------------------------------------------------------*/
108 
109 /* This is a hack for when CUDD_VALUE_TYPE is double */
110 typedef union hack {
111  CUDD_VALUE_TYPE value;
112  unsigned int bits[2];
113 } hack;
114 
115 /*---------------------------------------------------------------------------*/
116 /* Type declarations */
117 /*---------------------------------------------------------------------------*/
118 
119 /*---------------------------------------------------------------------------*/
120 /* Variable declarations */
121 /*---------------------------------------------------------------------------*/
122 
123 #ifndef lint
124 static char rcsid[] DD_UNUSED = "$Id: cuddTable.c,v 1.122 2009/02/19 16:24:28 fabio Exp $";
125 #endif
126 
127 /*---------------------------------------------------------------------------*/
128 /* Macro declarations */
129 /*---------------------------------------------------------------------------*/
130 
131 
132 #ifndef DD_UNSORTED_FREE_LIST
133 #ifdef DD_RED_BLACK_FREE_LIST
134 /* Macros for red/black trees. */
135 #define DD_INSERT_COMPARE(x,y) \
136  (((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK))
137 #define DD_COLOR(p) ((p)->index)
138 #define DD_IS_BLACK(p) ((p)->index == DD_BLACK)
139 #define DD_IS_RED(p) ((p)->index == DD_RED)
140 #define DD_LEFT(p) cuddT(p)
141 #define DD_RIGHT(p) cuddE(p)
142 #define DD_NEXT(p) ((p)->next)
143 #endif
144 #endif
145 
146 
147 /**AutomaticStart*************************************************************/
148 
149 /*---------------------------------------------------------------------------*/
150 /* Static function prototypes */
151 /*---------------------------------------------------------------------------*/
152 
153 static void ddRehashZdd (DdManager *unique, int i);
154 static int ddResizeTable (DdManager *unique, int index);
155 static int cuddFindParent (DdManager *table, DdNode *node);
156 DD_INLINE static void ddFixLimits (DdManager *unique);
157 #ifdef DD_RED_BLACK_FREE_LIST
158 static void cuddOrderedInsert (DdNodePtr *root, DdNodePtr node);
159 static DdNode * cuddOrderedThread (DdNode *root, DdNode *list);
160 static void cuddRotateLeft (DdNodePtr *nodeP);
161 static void cuddRotateRight (DdNodePtr *nodeP);
162 static void cuddDoRebalance (DdNodePtr **stack, int stackN);
163 #endif
164 static void ddPatchTree (DdManager *dd, MtrNode *treenode);
165 #ifdef DD_DEBUG
166 static int cuddCheckCollisionOrdering (DdManager *unique, int i, int j);
167 #endif
168 static void ddReportRefMess (DdManager *unique, int i, const char *caller);
169 
170 /**AutomaticEnd***************************************************************/
171 
172 
173 /*---------------------------------------------------------------------------*/
174 /* Definition of exported functions */
175 /*---------------------------------------------------------------------------*/
176 
177 
178 /**Function********************************************************************
179 
180  Synopsis [Returns the next prime &gt;= p.]
181 
182  Description []
183 
184  SideEffects [None]
185 
186 ******************************************************************************/
187 unsigned int
188 Cudd_Prime(
189  unsigned int p)
190 {
191  int i,pn;
192 
193  p--;
194  do {
195  p++;
196  if (p&1) {
197  pn = 1;
198  i = 3;
199  while ((unsigned) (i * i) <= p) {
200  if (p % i == 0) {
201  pn = 0;
202  break;
203  }
204  i += 2;
205  }
206  } else {
207  pn = 0;
208  }
209  } while (!pn);
210  return(p);
211 
212 } /* end of Cudd_Prime */
213 
214 
215 /*---------------------------------------------------------------------------*/
216 /* Definition of internal functions */
217 /*---------------------------------------------------------------------------*/
218 
219 
220 /**Function********************************************************************
221 
222  Synopsis [Fast storage allocation for DdNodes in the table.]
223 
224  Description [Fast storage allocation for DdNodes in the table. The
225  first 4 bytes of a chunk contain a pointer to the next block; the
226  rest contains DD_MEM_CHUNK spaces for DdNodes. Returns a pointer to
227  a new node if successful; NULL is memory is full.]
228 
229  SideEffects [None]
230 
231  SeeAlso [cuddDynamicAllocNode]
232 
233 ******************************************************************************/
234 DdNode *
235 cuddAllocNode(
236  DdManager * unique)
237 {
238  int i;
239  DdNodePtr *mem;
240  DdNode *list, *node;
241  extern DD_OOMFP MMoutOfMemory;
242  DD_OOMFP saveHandler;
243 
244  if (unique->nextFree == NULL) { /* free list is empty */
245  /* Check for exceeded limits. */
246  if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) >
247  unique->maxLive) {
248  unique->errorCode = CUDD_TOO_MANY_NODES;
249  return(NULL);
250  }
251  if (unique->stash == NULL || unique->memused > unique->maxmemhard) {
252  (void) cuddGarbageCollect(unique,1);
253  mem = NULL;
254  }
255  if (unique->nextFree == NULL) {
256  if (unique->memused > unique->maxmemhard) {
257  unique->errorCode = CUDD_MAX_MEM_EXCEEDED;
258  return(NULL);
259  }
260  /* Try to allocate a new block. */
261  saveHandler = MMoutOfMemory;
262  MMoutOfMemory = Cudd_OutOfMem;
263 // mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1);
264  mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 2);
265  MMoutOfMemory = saveHandler;
266  if (mem == NULL) {
267  /* No more memory: Try collecting garbage. If this succeeds,
268  ** we end up with mem still NULL, but unique->nextFree !=
269  ** NULL. */
270  if (cuddGarbageCollect(unique,1) == 0) {
271  /* Last resort: Free the memory stashed away, if there
272  ** any. If this succeeeds, mem != NULL and
273  ** unique->nextFree still NULL. */
274  if (unique->stash != NULL) {
275  ABC_FREE(unique->stash);
276  unique->stash = NULL;
277  /* Inhibit resizing of tables. */
278  cuddSlowTableGrowth(unique);
279  /* Now try again. */
280 // mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 1);
281  mem = (DdNodePtr *) ABC_ALLOC(DdNode,DD_MEM_CHUNK + 2);
282  }
283  if (mem == NULL) {
284  /* Out of luck. Call the default handler to do
285  ** whatever it specifies for a failed malloc.
286  ** If this handler returns, then set error code,
287  ** print warning, and return. */
288  (*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
289  unique->errorCode = CUDD_MEMORY_OUT;
290 #ifdef DD_VERBOSE
291  (void) fprintf(unique->err,
292  "cuddAllocNode: out of memory");
293  (void) fprintf(unique->err, "Memory in use = %lu\n",
294  unique->memused);
295 #endif
296  return(NULL);
297  }
298  }
299  }
300  if (mem != NULL) { /* successful allocation; slice memory */
301  ptruint offset;
302  unique->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
303  mem[0] = (DdNodePtr) unique->memoryList;
304  unique->memoryList = mem;
305 
306  /* Here we rely on the fact that a DdNode is as large as 4 pointers. */
307 // offset = (ptruint) mem & (sizeof(DdNode) - 1);
308 // mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
309 // assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0);
310 // list = (DdNode *) mem;
311  offset = (ptruint) mem & (32 - 1);
312  mem += (32 - offset) / sizeof(DdNodePtr);
313  assert(((ptruint) mem & (32 - 1)) == 0);
314  list = (DdNode *) mem;
315 
316  i = 1;
317  do {
318  list[i - 1].ref = 0;
319  list[i - 1].next = &list[i];
320  } while (++i < DD_MEM_CHUNK);
321 
322  list[DD_MEM_CHUNK-1].ref = 0;
323  list[DD_MEM_CHUNK-1].next = NULL;
324 
325  unique->nextFree = &list[0];
326  }
327  }
328  }
329  unique->allocated++;
330  node = unique->nextFree;
331  unique->nextFree = node->next;
332  node->Id = (unique->allocated<<4);
333  return(node);
334 
335 } /* end of cuddAllocNode */
336 
337 
338 /**Function********************************************************************
339 
340  Synopsis [Creates and initializes the unique table.]
341 
342  Description [Creates and initializes the unique table. Returns a pointer
343  to the table if successful; NULL otherwise.]
344 
345  SideEffects [None]
346 
347  SeeAlso [Cudd_Init cuddFreeTable]
348 
349 ******************************************************************************/
350 DdManager *
351 cuddInitTable(
352  unsigned int numVars /* Initial number of BDD variables (and subtables) */,
353  unsigned int numVarsZ /* Initial number of ZDD variables (and subtables) */,
354  unsigned int numSlots /* Initial size of the BDD subtables */,
355  unsigned int looseUpTo /* Limit for fast table growth */)
356 {
357  DdManager *unique = ABC_ALLOC(DdManager,1);
358  int i, j;
359  DdNodePtr *nodelist;
360  DdNode *sentinel;
361  unsigned int slots;
362  int shift;
363 
364  if (unique == NULL) {
365  return(NULL);
366  }
367  sentinel = &(unique->sentinel);
368  sentinel->ref = 0;
369  sentinel->index = 0;
370  cuddT(sentinel) = NULL;
371  cuddE(sentinel) = NULL;
372  sentinel->next = NULL;
373  unique->epsilon = DD_EPSILON;
374  unique->maxGrowth = DD_MAX_REORDER_GROWTH;
375  unique->maxGrowthAlt = 2.0 * DD_MAX_REORDER_GROWTH;
376  unique->reordCycle = 0; /* do not use alternate threshold */
377  unique->size = numVars;
378  unique->sizeZ = numVarsZ;
379  unique->maxSize = ddMax(DD_DEFAULT_RESIZE, numVars);
380  unique->maxSizeZ = ddMax(DD_DEFAULT_RESIZE, numVarsZ);
381 
382  /* Adjust the requested number of slots to a power of 2. */
383  slots = 8;
384  while (slots < numSlots) {
385  slots <<= 1;
386  }
387  unique->initSlots = slots;
388  shift = sizeof(int) * 8 - cuddComputeFloorLog2(slots);
389 
390  unique->slots = (numVars + numVarsZ + 1) * slots;
391  unique->keys = 0;
392  unique->maxLive = ~0; /* very large number */
393  unique->keysZ = 0;
394  unique->dead = 0;
395  unique->deadZ = 0;
396  unique->gcFrac = DD_GC_FRAC_HI;
397  unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
398  unique->looseUpTo = looseUpTo;
399  unique->gcEnabled = 1;
400  unique->allocated = 0;
401  unique->reclaimed = 0;
402  unique->subtables = ABC_ALLOC(DdSubtable,unique->maxSize);
403  if (unique->subtables == NULL) {
404  ABC_FREE(unique);
405  return(NULL);
406  }
407  unique->subtableZ = ABC_ALLOC(DdSubtable,unique->maxSizeZ);
408  if (unique->subtableZ == NULL) {
409  ABC_FREE(unique->subtables);
410  ABC_FREE(unique);
411  return(NULL);
412  }
413  unique->perm = ABC_ALLOC(int,unique->maxSize);
414  if (unique->perm == NULL) {
415  ABC_FREE(unique->subtables);
416  ABC_FREE(unique->subtableZ);
417  ABC_FREE(unique);
418  return(NULL);
419  }
420  unique->invperm = ABC_ALLOC(int,unique->maxSize);
421  if (unique->invperm == NULL) {
422  ABC_FREE(unique->subtables);
423  ABC_FREE(unique->subtableZ);
424  ABC_FREE(unique->perm);
425  ABC_FREE(unique);
426  return(NULL);
427  }
428  unique->permZ = ABC_ALLOC(int,unique->maxSizeZ);
429  if (unique->permZ == NULL) {
430  ABC_FREE(unique->subtables);
431  ABC_FREE(unique->subtableZ);
432  ABC_FREE(unique->perm);
433  ABC_FREE(unique->invperm);
434  ABC_FREE(unique);
435  return(NULL);
436  }
437  unique->invpermZ = ABC_ALLOC(int,unique->maxSizeZ);
438  if (unique->invpermZ == NULL) {
439  ABC_FREE(unique->subtables);
440  ABC_FREE(unique->subtableZ);
441  ABC_FREE(unique->perm);
442  ABC_FREE(unique->invperm);
443  ABC_FREE(unique->permZ);
444  ABC_FREE(unique);
445  return(NULL);
446  }
447  unique->map = NULL;
448  unique->stack = ABC_ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1);
449  if (unique->stack == NULL) {
450  ABC_FREE(unique->subtables);
451  ABC_FREE(unique->subtableZ);
452  ABC_FREE(unique->perm);
453  ABC_FREE(unique->invperm);
454  ABC_FREE(unique->permZ);
455  ABC_FREE(unique->invpermZ);
456  ABC_FREE(unique);
457  return(NULL);
458  }
459  unique->stack[0] = NULL; /* to suppress harmless UMR */
460 
461 #ifndef DD_NO_DEATH_ROW
462  unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2);
463  unique->deathRow = ABC_ALLOC(DdNodePtr,unique->deathRowDepth);
464  if (unique->deathRow == NULL) {
465  ABC_FREE(unique->subtables);
466  ABC_FREE(unique->subtableZ);
467  ABC_FREE(unique->perm);
468  ABC_FREE(unique->invperm);
469  ABC_FREE(unique->permZ);
470  ABC_FREE(unique->invpermZ);
471  ABC_FREE(unique->stack);
472  ABC_FREE(unique);
473  return(NULL);
474  }
475  for (i = 0; i < unique->deathRowDepth; i++) {
476  unique->deathRow[i] = NULL;
477  }
478  unique->nextDead = 0;
479  unique->deadMask = unique->deathRowDepth - 1;
480 #endif
481 
482  for (i = 0; (unsigned) i < numVars; i++) {
483  unique->subtables[i].slots = slots;
484  unique->subtables[i].shift = shift;
485  unique->subtables[i].keys = 0;
486  unique->subtables[i].dead = 0;
487  unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
488  unique->subtables[i].bindVar = 0;
489  unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
490  unique->subtables[i].pairIndex = 0;
491  unique->subtables[i].varHandled = 0;
492  unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;
493 
494  nodelist = unique->subtables[i].nodelist = ABC_ALLOC(DdNodePtr,slots);
495  if (nodelist == NULL) {
496  for (j = 0; j < i; j++) {
497  ABC_FREE(unique->subtables[j].nodelist);
498  }
499  ABC_FREE(unique->subtables);
500  ABC_FREE(unique->subtableZ);
501  ABC_FREE(unique->perm);
502  ABC_FREE(unique->invperm);
503  ABC_FREE(unique->permZ);
504  ABC_FREE(unique->invpermZ);
505  ABC_FREE(unique->stack);
506  ABC_FREE(unique);
507  return(NULL);
508  }
509  for (j = 0; (unsigned) j < slots; j++) {
510  nodelist[j] = sentinel;
511  }
512  unique->perm[i] = i;
513  unique->invperm[i] = i;
514  }
515  for (i = 0; (unsigned) i < numVarsZ; i++) {
516  unique->subtableZ[i].slots = slots;
517  unique->subtableZ[i].shift = shift;
518  unique->subtableZ[i].keys = 0;
519  unique->subtableZ[i].dead = 0;
520  unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
521  nodelist = unique->subtableZ[i].nodelist = ABC_ALLOC(DdNodePtr,slots);
522  if (nodelist == NULL) {
523  for (j = 0; (unsigned) j < numVars; j++) {
524  ABC_FREE(unique->subtables[j].nodelist);
525  }
526  ABC_FREE(unique->subtables);
527  for (j = 0; j < i; j++) {
528  ABC_FREE(unique->subtableZ[j].nodelist);
529  }
530  ABC_FREE(unique->subtableZ);
531  ABC_FREE(unique->perm);
532  ABC_FREE(unique->invperm);
533  ABC_FREE(unique->permZ);
534  ABC_FREE(unique->invpermZ);
535  ABC_FREE(unique->stack);
536  ABC_FREE(unique);
537  return(NULL);
538  }
539  for (j = 0; (unsigned) j < slots; j++) {
540  nodelist[j] = NULL;
541  }
542  unique->permZ[i] = i;
543  unique->invpermZ[i] = i;
544  }
545  unique->constants.slots = slots;
546  unique->constants.shift = shift;
547  unique->constants.keys = 0;
548  unique->constants.dead = 0;
549  unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
550  nodelist = unique->constants.nodelist = ABC_ALLOC(DdNodePtr,slots);
551  if (nodelist == NULL) {
552  for (j = 0; (unsigned) j < numVars; j++) {
553  ABC_FREE(unique->subtables[j].nodelist);
554  }
555  ABC_FREE(unique->subtables);
556  for (j = 0; (unsigned) j < numVarsZ; j++) {
557  ABC_FREE(unique->subtableZ[j].nodelist);
558  }
559  ABC_FREE(unique->subtableZ);
560  ABC_FREE(unique->perm);
561  ABC_FREE(unique->invperm);
562  ABC_FREE(unique->permZ);
563  ABC_FREE(unique->invpermZ);
564  ABC_FREE(unique->stack);
565  ABC_FREE(unique);
566  return(NULL);
567  }
568  for (j = 0; (unsigned) j < slots; j++) {
569  nodelist[j] = NULL;
570  }
571 
572  unique->memoryList = NULL;
573  unique->nextFree = NULL;
574 
575  unique->memused = sizeof(DdManager) + (unique->maxSize + unique->maxSizeZ)
576  * (sizeof(DdSubtable) + 2 * sizeof(int)) + (numVars + 1) *
577  slots * sizeof(DdNodePtr) +
578  (ddMax(unique->maxSize,unique->maxSizeZ) + 1) * sizeof(DdNodePtr);
579 #ifndef DD_NO_DEATH_ROW
580  unique->memused += unique->deathRowDepth * sizeof(DdNodePtr);
581 #endif
582 
583  /* Initialize fields concerned with automatic dynamic reordering */
584  unique->reorderings = 0;
585  unique->autoDyn = 0; /* initially disabled */
586  unique->autoDynZ = 0; /* initially disabled */
587  unique->realign = 0; /* initially disabled */
588  unique->realignZ = 0; /* initially disabled */
589  unique->reordered = 0;
590  unique->autoMethod = CUDD_REORDER_SIFT;
591  unique->autoMethodZ = CUDD_REORDER_SIFT;
592  unique->nextDyn = DD_FIRST_REORDER;
593  unique->countDead = ~0;
594  unique->siftMaxVar = DD_SIFT_MAX_VAR;
595  unique->siftMaxSwap = DD_SIFT_MAX_SWAPS;
596  unique->tree = NULL;
597  unique->treeZ = NULL;
598  unique->groupcheck = CUDD_GROUP_CHECK7;
599  unique->recomb = DD_DEFAULT_RECOMB;
600  unique->symmviolation = 0;
601  unique->arcviolation = 0;
602  unique->populationSize = 0;
603  unique->numberXovers = 0;
604  unique->linear = NULL;
605  unique->linearSize = 0;
606 
607  /* Initialize ZDD universe. */
608  unique->univ = (DdNodePtr *)NULL;
609 
610  /* Initialize auxiliary fields. */
611  unique->localCaches = NULL;
612  unique->preGCHook = NULL;
613  unique->postGCHook = NULL;
614  unique->preReorderingHook = NULL;
615  unique->postReorderingHook = NULL;
616  unique->out = stdout;
617  unique->err = stderr;
618  unique->errorCode = CUDD_NO_ERROR;
619 
620  /* Initialize statistical counters. */
621  unique->maxmemhard = ~ 0UL;
622  unique->garbageCollections = 0;
623  unique->GCTime = 0;
624  unique->reordTime = 0;
625 #ifdef DD_STATS
626  unique->nodesDropped = 0;
627  unique->nodesFreed = 0;
628 #endif
629  unique->peakLiveNodes = 0;
630 #ifdef DD_UNIQUE_PROFILE
631  unique->uniqueLookUps = 0;
632  unique->uniqueLinks = 0;
633 #endif
634 #ifdef DD_COUNT
635  unique->recursiveCalls = 0;
636  unique->swapSteps = 0;
637 #ifdef DD_STATS
638  unique->nextSample = 250000;
639 #endif
640 #endif
641 
642  return(unique);
643 
644 } /* end of cuddInitTable */
645 
646 
647 /**Function********************************************************************
648 
649  Synopsis [Frees the resources associated to a unique table.]
650 
651  Description []
652 
653  SideEffects [None]
654 
655  SeeAlso [cuddInitTable]
656 
657 ******************************************************************************/
658 void
659 cuddFreeTable(
660  DdManager * unique)
661 {
662  DdNodePtr *next;
663  DdNodePtr *memlist = unique->memoryList;
664  int i;
665 
666  if (unique->univ != NULL) cuddZddFreeUniv(unique);
667  while (memlist != NULL) {
668  next = (DdNodePtr *) memlist[0]; /* link to next block */
669  ABC_FREE(memlist);
670  memlist = next;
671  }
672  unique->nextFree = NULL;
673  unique->memoryList = NULL;
674 
675  for (i = 0; i < unique->size; i++) {
676  ABC_FREE(unique->subtables[i].nodelist);
677  }
678  for (i = 0; i < unique->sizeZ; i++) {
679  ABC_FREE(unique->subtableZ[i].nodelist);
680  }
681  ABC_FREE(unique->constants.nodelist);
682  ABC_FREE(unique->subtables);
683  ABC_FREE(unique->subtableZ);
684  ABC_FREE(unique->acache);
685  ABC_FREE(unique->perm);
686  ABC_FREE(unique->permZ);
687  ABC_FREE(unique->invperm);
688  ABC_FREE(unique->invpermZ);
689  ABC_FREE(unique->vars);
690  if (unique->map != NULL) ABC_FREE(unique->map);
691  ABC_FREE(unique->stack);
692 #ifndef DD_NO_DEATH_ROW
693  ABC_FREE(unique->deathRow);
694 #endif
695  if (unique->tree != NULL) Mtr_FreeTree(unique->tree);
696  if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ);
697  if (unique->linear != NULL) ABC_FREE(unique->linear);
698  while (unique->preGCHook != NULL)
699  Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK);
700  while (unique->postGCHook != NULL)
701  Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK);
702  while (unique->preReorderingHook != NULL)
703  Cudd_RemoveHook(unique,unique->preReorderingHook->f,
704  CUDD_PRE_REORDERING_HOOK);
705  while (unique->postReorderingHook != NULL)
706  Cudd_RemoveHook(unique,unique->postReorderingHook->f,
707  CUDD_POST_REORDERING_HOOK);
708  ABC_FREE(unique);
709 
710 } /* end of cuddFreeTable */
711 
712 
713 /**Function********************************************************************
714 
715  Synopsis [Performs garbage collection on the unique tables.]
716 
717  Description [Performs garbage collection on the BDD and ZDD unique tables.
718  If clearCache is 0, the cache is not cleared. This should only be
719  specified if the cache has been cleared right before calling
720  cuddGarbageCollect. (As in the case of dynamic reordering.)
721  Returns the total number of deleted nodes.]
722 
723  SideEffects [None]
724 
725  SeeAlso []
726 
727 ******************************************************************************/
728 int
729 cuddGarbageCollect(
730  DdManager * unique,
731  int clearCache)
732 {
733  DdHook *hook;
734  DdCache *cache = unique->cache;
735  DdNode *sentinel = &(unique->sentinel);
736  DdNodePtr *nodelist;
737  int i, j, deleted, totalDeleted, totalDeletedZ;
738  DdCache *c;
739  DdNode *node,*next;
740  DdNodePtr *lastP;
741  int slots;
742  long localTime;
743 #ifndef DD_UNSORTED_FREE_LIST
744 #ifdef DD_RED_BLACK_FREE_LIST
745  DdNodePtr tree;
746 #else
747  DdNodePtr *memListTrav, *nxtNode;
748  DdNode *downTrav, *sentry;
749  int k;
750 #endif
751 #endif
752 
753 #ifndef DD_NO_DEATH_ROW
754  cuddClearDeathRow(unique);
755 #endif
756 
757  hook = unique->preGCHook;
758  while (hook != NULL) {
759  int res = (hook->f)(unique,"DD",NULL);
760  if (res == 0) return(0);
761  hook = hook->next;
762  }
763 
764  if (unique->dead + unique->deadZ == 0) {
765  hook = unique->postGCHook;
766  while (hook != NULL) {
767  int res = (hook->f)(unique,"DD",NULL);
768  if (res == 0) return(0);
769  hook = hook->next;
770  }
771  return(0);
772  }
773 
774  /* If many nodes are being reclaimed, we want to resize the tables
775  ** more aggressively, to reduce the frequency of garbage collection.
776  */
777  if (clearCache && unique->gcFrac == DD_GC_FRAC_LO &&
778  unique->slots <= unique->looseUpTo && unique->stash != NULL) {
779  unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
780 #ifdef DD_VERBOSE
781  (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_HI);
782  (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
783 #endif
784  unique->gcFrac = DD_GC_FRAC_HI;
785  return(0);
786  }
787 
788  localTime = util_cpu_time();
789 
790  unique->garbageCollections++;
791 #ifdef DD_VERBOSE
792  (void) fprintf(unique->err,
793  "garbage collecting (%d dead BDD nodes out of %d, min %d)...",
794  unique->dead, unique->keys, unique->minDead);
795  (void) fprintf(unique->err,
796  " (%d dead ZDD nodes out of %d)...",
797  unique->deadZ, unique->keysZ);
798 #endif
799 
800  /* Remove references to garbage collected nodes from the cache. */
801  if (clearCache) {
802  slots = unique->cacheSlots;
803  for (i = 0; i < slots; i++) {
804  c = &cache[i];
805  if (c->data != NULL) {
806  if (cuddClean(c->f)->ref == 0 ||
807  cuddClean(c->g)->ref == 0 ||
808  (((ptruint)c->f & 0x2) && Cudd_Regular(c->h)->ref == 0) ||
809  (c->data != DD_NON_CONSTANT &&
810  Cudd_Regular(c->data)->ref == 0)) {
811  c->data = NULL;
812  unique->cachedeletions++;
813  }
814  }
815  }
816  cuddLocalCacheClearDead(unique);
817  }
818 
819  /* Now return dead nodes to free list. Count them for sanity check. */
820  totalDeleted = 0;
821 #ifndef DD_UNSORTED_FREE_LIST
822 #ifdef DD_RED_BLACK_FREE_LIST
823  tree = NULL;
824 #endif
825 #endif
826 
827  for (i = 0; i < unique->size; i++) {
828  if (unique->subtables[i].dead == 0) continue;
829  nodelist = unique->subtables[i].nodelist;
830 
831  deleted = 0;
832  slots = unique->subtables[i].slots;
833  for (j = 0; j < slots; j++) {
834  lastP = &(nodelist[j]);
835  node = *lastP;
836  while (node != sentinel) {
837  next = node->next;
838  if (node->ref == 0) {
839  deleted++;
840 #ifndef DD_UNSORTED_FREE_LIST
841 #ifdef DD_RED_BLACK_FREE_LIST
842 #ifdef __osf__
843 #pragma pointer_size save
844 #pragma pointer_size short
845 #endif
846  cuddOrderedInsert(&tree,node);
847 #ifdef __osf__
848 #pragma pointer_size restore
849 #endif
850 #endif
851 #else
852  cuddDeallocNode(unique,node);
853 #endif
854  } else {
855  *lastP = node;
856  lastP = &(node->next);
857  }
858  node = next;
859  }
860  *lastP = sentinel;
861  }
862  if ((unsigned) deleted != unique->subtables[i].dead) {
863  ddReportRefMess(unique, i, "cuddGarbageCollect");
864  }
865  totalDeleted += deleted;
866  unique->subtables[i].keys -= deleted;
867  unique->subtables[i].dead = 0;
868  }
869  if (unique->constants.dead != 0) {
870  nodelist = unique->constants.nodelist;
871  deleted = 0;
872  slots = unique->constants.slots;
873  for (j = 0; j < slots; j++) {
874  lastP = &(nodelist[j]);
875  node = *lastP;
876  while (node != NULL) {
877  next = node->next;
878  if (node->ref == 0) {
879  deleted++;
880 #ifndef DD_UNSORTED_FREE_LIST
881 #ifdef DD_RED_BLACK_FREE_LIST
882 #ifdef __osf__
883 #pragma pointer_size save
884 #pragma pointer_size short
885 #endif
886  cuddOrderedInsert(&tree,node);
887 #ifdef __osf__
888 #pragma pointer_size restore
889 #endif
890 #endif
891 #else
892  cuddDeallocNode(unique,node);
893 #endif
894  } else {
895  *lastP = node;
896  lastP = &(node->next);
897  }
898  node = next;
899  }
900  *lastP = NULL;
901  }
902  if ((unsigned) deleted != unique->constants.dead) {
903  ddReportRefMess(unique, CUDD_CONST_INDEX, "cuddGarbageCollect");
904  }
905  totalDeleted += deleted;
906  unique->constants.keys -= deleted;
907  unique->constants.dead = 0;
908  }
909  if ((unsigned) totalDeleted != unique->dead) {
910  ddReportRefMess(unique, -1, "cuddGarbageCollect");
911  }
912  unique->keys -= totalDeleted;
913  unique->dead = 0;
914 #ifdef DD_STATS
915  unique->nodesFreed += (double) totalDeleted;
916 #endif
917 
918  totalDeletedZ = 0;
919 
920  for (i = 0; i < unique->sizeZ; i++) {
921  if (unique->subtableZ[i].dead == 0) continue;
922  nodelist = unique->subtableZ[i].nodelist;
923 
924  deleted = 0;
925  slots = unique->subtableZ[i].slots;
926  for (j = 0; j < slots; j++) {
927  lastP = &(nodelist[j]);
928  node = *lastP;
929  while (node != NULL) {
930  next = node->next;
931  if (node->ref == 0) {
932  deleted++;
933 #ifndef DD_UNSORTED_FREE_LIST
934 #ifdef DD_RED_BLACK_FREE_LIST
935 #ifdef __osf__
936 #pragma pointer_size save
937 #pragma pointer_size short
938 #endif
939  cuddOrderedInsert(&tree,node);
940 #ifdef __osf__
941 #pragma pointer_size restore
942 #endif
943 #endif
944 #else
945  cuddDeallocNode(unique,node);
946 #endif
947  } else {
948  *lastP = node;
949  lastP = &(node->next);
950  }
951  node = next;
952  }
953  *lastP = NULL;
954  }
955  if ((unsigned) deleted != unique->subtableZ[i].dead) {
956  ddReportRefMess(unique, i, "cuddGarbageCollect");
957  }
958  totalDeletedZ += deleted;
959  unique->subtableZ[i].keys -= deleted;
960  unique->subtableZ[i].dead = 0;
961  }
962 
963  /* No need to examine the constant table for ZDDs.
964  ** If we did we should be careful not to count whatever dead
965  ** nodes we found there among the dead ZDD nodes. */
966  if ((unsigned) totalDeletedZ != unique->deadZ) {
967  ddReportRefMess(unique, -1, "cuddGarbageCollect");
968  }
969  unique->keysZ -= totalDeletedZ;
970  unique->deadZ = 0;
971 #ifdef DD_STATS
972  unique->nodesFreed += (double) totalDeletedZ;
973 #endif
974 
975 
976 #ifndef DD_UNSORTED_FREE_LIST
977 #ifdef DD_RED_BLACK_FREE_LIST
978  unique->nextFree = cuddOrderedThread(tree,unique->nextFree);
979 #else
980  memListTrav = unique->memoryList;
981  sentry = NULL;
982  while (memListTrav != NULL) {
983  ptruint offset;
984  nxtNode = (DdNodePtr *)memListTrav[0];
985 // offset = (ptruint) memListTrav & (sizeof(DdNode) - 1);
986 // memListTrav += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
987  offset = (ptruint) memListTrav & (32 - 1);
988  memListTrav += (32 - offset) / sizeof(DdNodePtr);
989 
990  downTrav = (DdNode *)memListTrav;
991  k = 0;
992  do {
993  if (downTrav[k].ref == 0) {
994  if (sentry == NULL) {
995  unique->nextFree = sentry = &downTrav[k];
996  } else {
997  /* First hook sentry->next to the dead node and then
998  ** reassign sentry to the dead node. */
999  sentry = (sentry->next = &downTrav[k]);
1000  }
1001  }
1002  } while (++k < DD_MEM_CHUNK);
1003  memListTrav = nxtNode;
1004  }
1005  sentry->next = NULL;
1006 #endif
1007 #endif
1008 
1009  unique->GCTime += util_cpu_time() - localTime;
1010 
1011  hook = unique->postGCHook;
1012  while (hook != NULL) {
1013  int res = (hook->f)(unique,"DD",NULL);
1014  if (res == 0) return(0);
1015  hook = hook->next;
1016  }
1017 
1018 #ifdef DD_VERBOSE
1019  (void) fprintf(unique->err," done\n");
1020 #endif
1021 
1022  return(totalDeleted+totalDeletedZ);
1023 
1024 } /* end of cuddGarbageCollect */
1025 
1026 
1027 /**Function********************************************************************
1028 
1029  Synopsis [Wrapper for cuddUniqueInterZdd.]
1030 
1031  Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD
1032  reduction rule. Returns a pointer to the result node under normal
1033  conditions; NULL if reordering occurred or memory was exhausted.]
1034 
1035  SideEffects [None]
1036 
1037  SeeAlso [cuddUniqueInterZdd]
1038 
1039 ******************************************************************************/
1040 DdNode *
1041 cuddZddGetNode(
1042  DdManager * zdd,
1043  int id,
1044  DdNode * T,
1045  DdNode * E)
1046 {
1047  DdNode *node;
1048 
1049  if (T == DD_ZERO(zdd))
1050  return(E);
1051  node = cuddUniqueInterZdd(zdd, id, T, E);
1052  return(node);
1053 
1054 } /* end of cuddZddGetNode */
1055 
1056 
1057 /**Function********************************************************************
1058 
1059  Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable
1060  ordering.]
1061 
1062  Description [Wrapper for cuddUniqueInterZdd that is independent of
1063  variable ordering (IVO). This function does not require parameter
1064  index to precede the indices of the top nodes of g and h in the
1065  variable order. Returns a pointer to the result node under normal
1066  conditions; NULL if reordering occurred or memory was exhausted.]
1067 
1068  SideEffects [None]
1069 
1070  SeeAlso [cuddZddGetNode cuddZddIsop]
1071 
1072 ******************************************************************************/
1073 DdNode *
1074 cuddZddGetNodeIVO(
1075  DdManager * dd,
1076  int index,
1077  DdNode * g,
1078  DdNode * h)
1079 {
1080  DdNode *f, *r, *t;
1081  DdNode *zdd_one = DD_ONE(dd);
1082  DdNode *zdd_zero = DD_ZERO(dd);
1083 
1084  f = cuddUniqueInterZdd(dd, index, zdd_one, zdd_zero);
1085  if (f == NULL) {
1086  return(NULL);
1087  }
1088  cuddRef(f);
1089  t = cuddZddProduct(dd, f, g);
1090  if (t == NULL) {
1091  Cudd_RecursiveDerefZdd(dd, f);
1092  return(NULL);
1093  }
1094  cuddRef(t);
1095  Cudd_RecursiveDerefZdd(dd, f);
1096  r = cuddZddUnion(dd, t, h);
1097  if (r == NULL) {
1098  Cudd_RecursiveDerefZdd(dd, t);
1099  return(NULL);
1100  }
1101  cuddRef(r);
1102  Cudd_RecursiveDerefZdd(dd, t);
1103 
1104  cuddDeref(r);
1105  return(r);
1106 
1107 } /* end of cuddZddGetNodeIVO */
1108 
1109 
1110 /**Function********************************************************************
1111 
1112  Synopsis [Checks the unique table for the existence of an internal node.]
1113 
1114  Description [Checks the unique table for the existence of an internal
1115  node. If it does not exist, it creates a new one. Does not
1116  modify the reference count of whatever is returned. A newly created
1117  internal node comes back with a reference count 0. For a newly
1118  created node, increments the reference counts of what T and E point
1119  to. Returns a pointer to the new node if successful; NULL if memory
1120  is exhausted or if reordering took place.]
1121 
1122  SideEffects [None]
1123 
1124  SeeAlso [cuddUniqueInterZdd]
1125 
1126 ******************************************************************************/
1127 DdNode *
1128 cuddUniqueInter(
1129  DdManager * unique,
1130  int index,
1131  DdNode * T,
1132  DdNode * E)
1133 {
1134  int pos;
1135  unsigned int level;
1136  int retval;
1137  DdNodePtr *nodelist;
1138  DdNode *looking;
1139  DdNodePtr *previousP;
1140  DdSubtable *subtable;
1141  int gcNumber;
1142 
1143 #ifdef DD_UNIQUE_PROFILE
1144  unique->uniqueLookUps++;
1145 #endif
1146 
1147  if (index >= unique->size) {
1148  if (!ddResizeTable(unique,index)) return(NULL);
1149  }
1150 
1151  level = unique->perm[index];
1152  subtable = &(unique->subtables[level]);
1153 
1154 #ifdef DD_DEBUG
1155  assert(level < (unsigned) cuddI(unique,T->index));
1156  assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index));
1157 #endif
1158 
1159  pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
1160  nodelist = subtable->nodelist;
1161  previousP = &(nodelist[pos]);
1162  looking = *previousP;
1163 
1164  while (T < cuddT(looking)) {
1165  previousP = &(looking->next);
1166  looking = *previousP;
1167 #ifdef DD_UNIQUE_PROFILE
1168  unique->uniqueLinks++;
1169 #endif
1170  }
1171  while (T == cuddT(looking) && E < cuddE(looking)) {
1172  previousP = &(looking->next);
1173  looking = *previousP;
1174 #ifdef DD_UNIQUE_PROFILE
1175  unique->uniqueLinks++;
1176 #endif
1177  }
1178  if (T == cuddT(looking) && E == cuddE(looking)) {
1179  if (looking->ref == 0) {
1180  cuddReclaim(unique,looking);
1181  }
1182  return(looking);
1183  }
1184 
1185  /* countDead is 0 if deads should be counted and ~0 if they should not. */
1186  if (unique->autoDyn &&
1187  unique->keys - (unique->dead & unique->countDead) >= unique->nextDyn) {
1188 #ifdef DD_DEBUG
1189  retval = Cudd_DebugCheck(unique);
1190  if (retval != 0) return(NULL);
1191  retval = Cudd_CheckKeys(unique);
1192  if (retval != 0) return(NULL);
1193 #endif
1194  retval = Cudd_ReduceHeap(unique,unique->autoMethod,10); /* 10 = whatever */
1195  if (retval == 0) unique->reordered = 2;
1196 #ifdef DD_DEBUG
1197  retval = Cudd_DebugCheck(unique);
1198  if (retval != 0) unique->reordered = 2;
1199  retval = Cudd_CheckKeys(unique);
1200  if (retval != 0) unique->reordered = 2;
1201 #endif
1202  return(NULL);
1203  }
1204 
1205  if (subtable->keys > subtable->maxKeys) {
1206  if (unique->gcEnabled &&
1207  ((unique->dead > unique->minDead) ||
1208  ((unique->dead > unique->minDead / 2) &&
1209  (subtable->dead > subtable->keys * 0.95)))) { /* too many dead */
1210  (void) cuddGarbageCollect(unique,1);
1211  } else {
1212  cuddRehash(unique,(int)level);
1213  }
1214  /* Update pointer to insertion point. In the case of rehashing,
1215  ** the slot may have changed. In the case of garbage collection,
1216  ** the predecessor may have been dead. */
1217  pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
1218  nodelist = subtable->nodelist;
1219  previousP = &(nodelist[pos]);
1220  looking = *previousP;
1221 
1222  while (T < cuddT(looking)) {
1223  previousP = &(looking->next);
1224  looking = *previousP;
1225 #ifdef DD_UNIQUE_PROFILE
1226  unique->uniqueLinks++;
1227 #endif
1228  }
1229  while (T == cuddT(looking) && E < cuddE(looking)) {
1230  previousP = &(looking->next);
1231  looking = *previousP;
1232 #ifdef DD_UNIQUE_PROFILE
1233  unique->uniqueLinks++;
1234 #endif
1235  }
1236  }
1237 
1238  gcNumber = unique->garbageCollections;
1239  looking = cuddAllocNode(unique);
1240  if (looking == NULL) {
1241  return(NULL);
1242  }
1243  unique->keys++;
1244  subtable->keys++;
1245 
1246  if (gcNumber != unique->garbageCollections) {
1247  DdNode *looking2;
1248  pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
1249  nodelist = subtable->nodelist;
1250  previousP = &(nodelist[pos]);
1251  looking2 = *previousP;
1252 
1253  while (T < cuddT(looking2)) {
1254  previousP = &(looking2->next);
1255  looking2 = *previousP;
1256 #ifdef DD_UNIQUE_PROFILE
1257  unique->uniqueLinks++;
1258 #endif
1259  }
1260  while (T == cuddT(looking2) && E < cuddE(looking2)) {
1261  previousP = &(looking2->next);
1262  looking2 = *previousP;
1263 #ifdef DD_UNIQUE_PROFILE
1264  unique->uniqueLinks++;
1265 #endif
1266  }
1267  }
1268  looking->index = index;
1269  cuddT(looking) = T;
1270  cuddE(looking) = E;
1271  looking->next = *previousP;
1272  *previousP = looking;
1273  cuddSatInc(T->ref); /* we know T is a regular pointer */
1274  cuddRef(E);
1275 
1276 #ifdef DD_DEBUG
1277  cuddCheckCollisionOrdering(unique,level,pos);
1278 #endif
1279 
1280 // assert( Cudd_Regular(T)->Id < 100000000 );
1281 // assert( Cudd_Regular(E)->Id < 100000000 );
1282  return(looking);
1283 
1284 } /* end of cuddUniqueInter */
1285 
1286 
1287 /**Function********************************************************************
1288 
1289  Synopsis [Wrapper for cuddUniqueInter that is independent of variable
1290  ordering.]
1291 
1292  Description [Wrapper for cuddUniqueInter that is independent of
1293  variable ordering (IVO). This function does not require parameter
1294  index to precede the indices of the top nodes of T and E in the
1295  variable order. Returns a pointer to the result node under normal
1296  conditions; NULL if reordering occurred or memory was exhausted.]
1297 
1298  SideEffects [None]
1299 
1300  SeeAlso [cuddUniqueInter Cudd_MakeBddFromZddCover]
1301 
1302 ******************************************************************************/
1303 DdNode *
1304 cuddUniqueInterIVO(
1305  DdManager * unique,
1306  int index,
1307  DdNode * T,
1308  DdNode * E)
1309 {
1310  DdNode *result;
1311  DdNode *v;
1312 
1313  v = cuddUniqueInter(unique, index, DD_ONE(unique),
1314  Cudd_Not(DD_ONE(unique)));
1315  if (v == NULL)
1316  return(NULL);
1317  cuddRef(v);
1318  result = cuddBddIteRecur(unique, v, T, E);
1319  Cudd_RecursiveDeref(unique, v);
1320  return(result);
1321 }
1322 
1323 
1324 /**Function********************************************************************
1325 
1326  Synopsis [Checks the unique table for the existence of an internal
1327  ZDD node.]
1328 
1329  Description [Checks the unique table for the existence of an internal
1330  ZDD node. If it does not exist, it creates a new one. Does not
1331  modify the reference count of whatever is returned. A newly created
1332  internal node comes back with a reference count 0. For a newly
1333  created node, increments the reference counts of what T and E point
1334  to. Returns a pointer to the new node if successful; NULL if memory
1335  is exhausted or if reordering took place.]
1336 
1337  SideEffects [None]
1338 
1339  SeeAlso [cuddUniqueInter]
1340 
1341 ******************************************************************************/
1342 DdNode *
1343 cuddUniqueInterZdd(
1344  DdManager * unique,
1345  int index,
1346  DdNode * T,
1347  DdNode * E)
1348 {
1349  int pos;
1350  unsigned int level;
1351  int retval;
1352  DdNodePtr *nodelist;
1353  DdNode *looking;
1354  DdSubtable *subtable;
1355 
1356 #ifdef DD_UNIQUE_PROFILE
1357  unique->uniqueLookUps++;
1358 #endif
1359 
1360  if (index >= unique->sizeZ) {
1361  if (!cuddResizeTableZdd(unique,index)) return(NULL);
1362  }
1363 
1364  level = unique->permZ[index];
1365  subtable = &(unique->subtableZ[level]);
1366 
1367 #ifdef DD_DEBUG
1368  assert(level < (unsigned) cuddIZ(unique,T->index));
1369  assert(level < (unsigned) cuddIZ(unique,Cudd_Regular(E)->index));
1370 #endif
1371 
1372  if (subtable->keys > subtable->maxKeys) {
1373  if (unique->gcEnabled && ((unique->deadZ > unique->minDead) ||
1374  (10 * subtable->dead > 9 * subtable->keys))) { /* too many dead */
1375  (void) cuddGarbageCollect(unique,1);
1376  } else {
1377  ddRehashZdd(unique,(int)level);
1378  }
1379  }
1380 
1381  pos = ddHash(cuddF2L(T), cuddF2L(E), subtable->shift);
1382  nodelist = subtable->nodelist;
1383  looking = nodelist[pos];
1384 
1385  while (looking != NULL) {
1386  if (cuddT(looking) == T && cuddE(looking) == E) {
1387  if (looking->ref == 0) {
1388  cuddReclaimZdd(unique,looking);
1389  }
1390  return(looking);
1391  }
1392  looking = looking->next;
1393 #ifdef DD_UNIQUE_PROFILE
1394  unique->uniqueLinks++;
1395 #endif
1396  }
1397 
1398  /* countDead is 0 if deads should be counted and ~0 if they should not. */
1399  if (unique->autoDynZ &&
1400  unique->keysZ - (unique->deadZ & unique->countDead) >= unique->nextDyn) {
1401 #ifdef DD_DEBUG
1402  retval = Cudd_DebugCheck(unique);
1403  if (retval != 0) return(NULL);
1404  retval = Cudd_CheckKeys(unique);
1405  if (retval != 0) return(NULL);
1406 #endif
1407  retval = Cudd_zddReduceHeap(unique,unique->autoMethodZ,10); /* 10 = whatever */
1408  if (retval == 0) unique->reordered = 2;
1409 #ifdef DD_DEBUG
1410  retval = Cudd_DebugCheck(unique);
1411  if (retval != 0) unique->reordered = 2;
1412  retval = Cudd_CheckKeys(unique);
1413  if (retval != 0) unique->reordered = 2;
1414 #endif
1415  return(NULL);
1416  }
1417 
1418  unique->keysZ++;
1419  subtable->keys++;
1420 
1421  looking = cuddAllocNode(unique);
1422  if (looking == NULL) return(NULL);
1423  looking->index = index;
1424  cuddT(looking) = T;
1425  cuddE(looking) = E;
1426  looking->next = nodelist[pos];
1427  nodelist[pos] = looking;
1428  cuddRef(T);
1429  cuddRef(E);
1430 
1431  return(looking);
1432 
1433 } /* end of cuddUniqueInterZdd */
1434 
1435 
1436 /**Function********************************************************************
1437 
1438  Synopsis [Checks the unique table for the existence of a constant node.]
1439 
1440  Description [Checks the unique table for the existence of a constant node.
1441  If it does not exist, it creates a new one. Does not
1442  modify the reference count of whatever is returned. A newly created
1443  internal node comes back with a reference count 0. Returns a
1444  pointer to the new node.]
1445 
1446  SideEffects [None]
1447 
1448 ******************************************************************************/
1449 DdNode *
1450 cuddUniqueConst(
1451  DdManager * unique,
1452  CUDD_VALUE_TYPE value)
1453 {
1454  int pos;
1455  DdNodePtr *nodelist;
1456  DdNode *looking;
1457  hack split;
1458 
1459 #ifdef DD_UNIQUE_PROFILE
1460  unique->uniqueLookUps++;
1461 #endif
1462 
1463  if (unique->constants.keys > unique->constants.maxKeys) {
1464  if (unique->gcEnabled && ((unique->dead > unique->minDead) ||
1465  (10 * unique->constants.dead > 9 * unique->constants.keys))) { /* too many dead */
1466  (void) cuddGarbageCollect(unique,1);
1467  } else {
1468  cuddRehash(unique,CUDD_CONST_INDEX);
1469  }
1470  }
1471 
1472  cuddAdjust(value); /* for the case of crippled infinities */
1473 
1474  if (ddAbs(value) < unique->epsilon) {
1475  value = 0.0;
1476  }
1477  split.value = value;
1478 
1479  pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift);
1480  nodelist = unique->constants.nodelist;
1481  looking = nodelist[pos];
1482 
1483  /* Here we compare values both for equality and for difference less
1484  * than epsilon. The first comparison is required when values are
1485  * infinite, since Infinity - Infinity is NaN and NaN < X is 0 for
1486  * every X.
1487  */
1488  while (looking != NULL) {
1489  if (looking->type.value == value ||
1490  ddEqualVal(looking->type.value,value,unique->epsilon)) {
1491  if (looking->ref == 0) {
1492  cuddReclaim(unique,looking);
1493  }
1494  return(looking);
1495  }
1496  looking = looking->next;
1497 #ifdef DD_UNIQUE_PROFILE
1498  unique->uniqueLinks++;
1499 #endif
1500  }
1501 
1502  unique->keys++;
1503  unique->constants.keys++;
1504 
1505  looking = cuddAllocNode(unique);
1506  if (looking == NULL) return(NULL);
1507  looking->index = CUDD_CONST_INDEX;
1508  looking->type.value = value;
1509  looking->next = nodelist[pos];
1510  nodelist[pos] = looking;
1511 
1512  return(looking);
1513 
1514 } /* end of cuddUniqueConst */
1515 
1516 
1517 /**Function********************************************************************
1518 
1519  Synopsis [Rehashes a unique subtable.]
1520 
1521  Description [Doubles the size of a unique subtable and rehashes its
1522  contents.]
1523 
1524  SideEffects [None]
1525 
1526  SeeAlso []
1527 
1528 ******************************************************************************/
1529 void
1530 cuddRehash(
1531  DdManager * unique,
1532  int i)
1533 {
1534  unsigned int slots, oldslots;
1535  int shift, oldshift;
1536  int j, pos;
1537  DdNodePtr *nodelist, *oldnodelist;
1538  DdNode *node, *next;
1539  DdNode *sentinel = &(unique->sentinel);
1540  hack split;
1541  extern DD_OOMFP MMoutOfMemory;
1542  DD_OOMFP saveHandler;
1543 
1544  if (unique->gcFrac == DD_GC_FRAC_HI && unique->slots > unique->looseUpTo) {
1545  unique->gcFrac = DD_GC_FRAC_LO;
1546  unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots);
1547 #ifdef DD_VERBOSE
1548  (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_LO);
1549  (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
1550 #endif
1551  }
1552 
1553  if (unique->gcFrac != DD_GC_FRAC_MIN && unique->memused > unique->maxmem) {
1554  unique->gcFrac = DD_GC_FRAC_MIN;
1555  unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots);
1556 #ifdef DD_VERBOSE
1557  (void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_MIN);
1558  (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
1559 #endif
1560  cuddShrinkDeathRow(unique);
1561  if (cuddGarbageCollect(unique,1) > 0) return;
1562  }
1563 
1564  if (i != CUDD_CONST_INDEX) {
1565  oldslots = unique->subtables[i].slots;
1566  oldshift = unique->subtables[i].shift;
1567  oldnodelist = unique->subtables[i].nodelist;
1568 
1569  /* Compute the new size of the subtable. */
1570  slots = oldslots << 1;
1571  shift = oldshift - 1;
1572 
1573  saveHandler = MMoutOfMemory;
1574  MMoutOfMemory = Cudd_OutOfMem;
1575  nodelist = ABC_ALLOC(DdNodePtr, slots);
1576  MMoutOfMemory = saveHandler;
1577  if (nodelist == NULL) {
1578  (void) fprintf(unique->err,
1579  "Unable to resize subtable %d for lack of memory\n",
1580  i);
1581  /* Prevent frequent resizing attempts. */
1582  (void) cuddGarbageCollect(unique,1);
1583  if (unique->stash != NULL) {
1584  ABC_FREE(unique->stash);
1585  unique->stash = NULL;
1586  /* Inhibit resizing of tables. */
1587  cuddSlowTableGrowth(unique);
1588  }
1589  return;
1590  }
1591  unique->subtables[i].nodelist = nodelist;
1592  unique->subtables[i].slots = slots;
1593  unique->subtables[i].shift = shift;
1594  unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1595 
1596  /* Move the nodes from the old table to the new table.
1597  ** This code depends on the type of hash function.
1598  ** It assumes that the effect of doubling the size of the table
1599  ** is to retain one more bit of the 32-bit hash value.
1600  ** The additional bit is the LSB. */
1601  for (j = 0; (unsigned) j < oldslots; j++) {
1602  DdNodePtr *evenP, *oddP;
1603  node = oldnodelist[j];
1604  evenP = &(nodelist[j<<1]);
1605  oddP = &(nodelist[(j<<1)+1]);
1606  while (node != sentinel) {
1607  next = node->next;
1608  pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
1609  if (pos & 1) {
1610  *oddP = node;
1611  oddP = &(node->next);
1612  } else {
1613  *evenP = node;
1614  evenP = &(node->next);
1615  }
1616  node = next;
1617  }
1618  *evenP = *oddP = sentinel;
1619  }
1620  ABC_FREE(oldnodelist);
1621 
1622 #ifdef DD_VERBOSE
1623  (void) fprintf(unique->err,
1624  "rehashing layer %d: keys %d dead %d new size %d\n",
1625  i, unique->subtables[i].keys,
1626  unique->subtables[i].dead, slots);
1627 #endif
1628  } else {
1629  oldslots = unique->constants.slots;
1630  oldshift = unique->constants.shift;
1631  oldnodelist = unique->constants.nodelist;
1632 
1633  /* The constant subtable is never subjected to reordering.
1634  ** Therefore, when it is resized, it is because it has just
1635  ** reached the maximum load. We can safely just double the size,
1636  ** with no need for the loop we use for the other tables.
1637  */
1638  slots = oldslots << 1;
1639  shift = oldshift - 1;
1640  saveHandler = MMoutOfMemory;
1641  MMoutOfMemory = Cudd_OutOfMem;
1642  nodelist = ABC_ALLOC(DdNodePtr, slots);
1643  MMoutOfMemory = saveHandler;
1644  if (nodelist == NULL) {
1645  (void) fprintf(unique->err,
1646  "Unable to resize constant subtable for lack of memory\n");
1647  (void) cuddGarbageCollect(unique,1);
1648  for (j = 0; j < unique->size; j++) {
1649  unique->subtables[j].maxKeys <<= 1;
1650  }
1651  unique->constants.maxKeys <<= 1;
1652  return;
1653  }
1654  unique->constants.slots = slots;
1655  unique->constants.shift = shift;
1656  unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1657  unique->constants.nodelist = nodelist;
1658  for (j = 0; (unsigned) j < slots; j++) {
1659  nodelist[j] = NULL;
1660  }
1661  for (j = 0; (unsigned) j < oldslots; j++) {
1662  node = oldnodelist[j];
1663  while (node != NULL) {
1664  next = node->next;
1665  split.value = cuddV(node);
1666  pos = ddHash(split.bits[0], split.bits[1], shift);
1667  node->next = nodelist[pos];
1668  nodelist[pos] = node;
1669  node = next;
1670  }
1671  }
1672  ABC_FREE(oldnodelist);
1673 
1674 #ifdef DD_VERBOSE
1675  (void) fprintf(unique->err,
1676  "rehashing constants: keys %d dead %d new size %d\n",
1677  unique->constants.keys,unique->constants.dead,slots);
1678 #endif
1679  }
1680 
1681  /* Update global data */
1682 
1683  unique->memused += (slots - oldslots) * sizeof(DdNodePtr);
1684  unique->slots += (slots - oldslots);
1685  ddFixLimits(unique);
1686 
1687 } /* end of cuddRehash */
1688 
1689 
1690 /**Function********************************************************************
1691 
1692  Synopsis [Shrinks a subtable.]
1693 
1694  Description [Shrinks a subtable.]
1695 
1696  SideEffects [None]
1697 
1698  SeeAlso [cuddRehash]
1699 
1700 ******************************************************************************/
1701 void
1702 cuddShrinkSubtable(
1703  DdManager *unique,
1704  int i)
1705 {
1706  int j;
1707  int shift, posn;
1708  DdNodePtr *nodelist, *oldnodelist;
1709  DdNode *node, *next;
1710  DdNode *sentinel = &(unique->sentinel);
1711  unsigned int slots, oldslots;
1712  extern DD_OOMFP MMoutOfMemory;
1713  DD_OOMFP saveHandler;
1714 
1715  oldnodelist = unique->subtables[i].nodelist;
1716  oldslots = unique->subtables[i].slots;
1717  slots = oldslots >> 1;
1718  saveHandler = MMoutOfMemory;
1719  MMoutOfMemory = Cudd_OutOfMem;
1720  nodelist = ABC_ALLOC(DdNodePtr, slots);
1721  MMoutOfMemory = saveHandler;
1722  if (nodelist == NULL) {
1723  return;
1724  }
1725  unique->subtables[i].nodelist = nodelist;
1726  unique->subtables[i].slots = slots;
1727  unique->subtables[i].shift++;
1728  unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
1729 #ifdef DD_VERBOSE
1730  (void) fprintf(unique->err,
1731  "shrunk layer %d (%d keys) from %d to %d slots\n",
1732  i, unique->subtables[i].keys, oldslots, slots);
1733 #endif
1734 
1735  for (j = 0; (unsigned) j < slots; j++) {
1736  nodelist[j] = sentinel;
1737  }
1738  shift = unique->subtables[i].shift;
1739  for (j = 0; (unsigned) j < oldslots; j++) {
1740  node = oldnodelist[j];
1741  while (node != sentinel) {
1742  DdNode *looking, *T, *E;
1743  DdNodePtr *previousP;
1744  next = node->next;
1745  posn = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
1746  previousP = &(nodelist[posn]);
1747  looking = *previousP;
1748  T = cuddT(node);
1749  E = cuddE(node);
1750  while (T < cuddT(looking)) {
1751  previousP = &(looking->next);
1752  looking = *previousP;
1753 #ifdef DD_UNIQUE_PROFILE
1754  unique->uniqueLinks++;
1755 #endif
1756  }
1757  while (T == cuddT(looking) && E < cuddE(looking)) {
1758  previousP = &(looking->next);
1759  looking = *previousP;
1760 #ifdef DD_UNIQUE_PROFILE
1761  unique->uniqueLinks++;
1762 #endif
1763  }
1764  node->next = *previousP;
1765  *previousP = node;
1766  node = next;
1767  }
1768  }
1769  ABC_FREE(oldnodelist);
1770 
1771  unique->memused += ((long) slots - (long) oldslots) * sizeof(DdNode *);
1772  unique->slots += slots - oldslots;
1773  unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
1774  unique->cacheSlack = (int)
1775  ddMin(unique->maxCacheHard,DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots)
1776  - 2 * (int) unique->cacheSlots;
1777 
1778 } /* end of cuddShrinkSubtable */
1779 
1780 
1781 /**Function********************************************************************
1782 
1783  Synopsis [Inserts n new subtables in a unique table at level.]
1784 
1785  Description [Inserts n new subtables in a unique table at level.
1786  The number n should be positive, and level should be an existing level.
1787  Returns 1 if successful; 0 otherwise.]
1788 
1789  SideEffects [None]
1790 
1791  SeeAlso [cuddDestroySubtables]
1792 
1793 ******************************************************************************/
1794 int
1795 cuddInsertSubtables(
1796  DdManager * unique,
1797  int n,
1798  int level)
1799 {
1800  DdSubtable *newsubtables;
1801  DdNodePtr *newnodelist;
1802  DdNodePtr *newvars;
1803  DdNode *sentinel = &(unique->sentinel);
1804  int oldsize,newsize;
1805  int i,j,index,reorderSave;
1806  unsigned int numSlots = unique->initSlots;
1807  int *newperm, *newinvperm, *newmap=NULL;
1808  DdNode *one, *zero;
1809 
1810 #ifdef DD_DEBUG
1811  assert(n > 0 && level < unique->size);
1812 #endif
1813 
1814  oldsize = unique->size;
1815  /* Easy case: there is still room in the current table. */
1816  if (oldsize + n <= unique->maxSize) {
1817  /* Shift the tables at and below level. */
1818  for (i = oldsize - 1; i >= level; i--) {
1819  unique->subtables[i+n].slots = unique->subtables[i].slots;
1820  unique->subtables[i+n].shift = unique->subtables[i].shift;
1821  unique->subtables[i+n].keys = unique->subtables[i].keys;
1822  unique->subtables[i+n].maxKeys = unique->subtables[i].maxKeys;
1823  unique->subtables[i+n].dead = unique->subtables[i].dead;
1824  unique->subtables[i+n].nodelist = unique->subtables[i].nodelist;
1825  unique->subtables[i+n].bindVar = unique->subtables[i].bindVar;
1826  unique->subtables[i+n].varType = unique->subtables[i].varType;
1827  unique->subtables[i+n].pairIndex = unique->subtables[i].pairIndex;
1828  unique->subtables[i+n].varHandled = unique->subtables[i].varHandled;
1829  unique->subtables[i+n].varToBeGrouped =
1830  unique->subtables[i].varToBeGrouped;
1831 
1832  index = unique->invperm[i];
1833  unique->invperm[i+n] = index;
1834  unique->perm[index] += n;
1835  }
1836  /* Create new subtables. */
1837  for (i = 0; i < n; i++) {
1838  unique->subtables[level+i].slots = numSlots;
1839  unique->subtables[level+i].shift = sizeof(int) * 8 -
1840  cuddComputeFloorLog2(numSlots);
1841  unique->subtables[level+i].keys = 0;
1842  unique->subtables[level+i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
1843  unique->subtables[level+i].dead = 0;
1844  unique->subtables[level+i].bindVar = 0;
1845  unique->subtables[level+i].varType = CUDD_VAR_PRIMARY_INPUT;
1846  unique->subtables[level+i].pairIndex = 0;
1847  unique->subtables[level+i].varHandled = 0;
1848  unique->subtables[level+i].varToBeGrouped = CUDD_LAZY_NONE;
1849 
1850  unique->perm[oldsize+i] = level + i;
1851  unique->invperm[level+i] = oldsize + i;
1852  newnodelist = unique->subtables[level+i].nodelist =
1853  ABC_ALLOC(DdNodePtr, numSlots);
1854  if (newnodelist == NULL) {
1855  unique->errorCode = CUDD_MEMORY_OUT;
1856  return(0);
1857  }
1858  for (j = 0; (unsigned) j < numSlots; j++) {
1859  newnodelist[j] = sentinel;
1860  }
1861  }
1862  if (unique->map != NULL) {
1863  for (i = 0; i < n; i++) {
1864  unique->map[oldsize+i] = oldsize + i;
1865  }
1866  }
1867  } else {
1868  /* The current table is too small: we need to allocate a new,
1869  ** larger one; move all old subtables, and initialize the new
1870  ** subtables.
1871  */
1872  newsize = oldsize + n + DD_DEFAULT_RESIZE;
1873 #ifdef DD_VERBOSE
1874  (void) fprintf(unique->err,
1875  "Increasing the table size from %d to %d\n",
1876  unique->maxSize, newsize);
1877 #endif
1878  /* Allocate memory for new arrays (except nodelists). */
1879  newsubtables = ABC_ALLOC(DdSubtable,newsize);
1880  if (newsubtables == NULL) {
1881  unique->errorCode = CUDD_MEMORY_OUT;
1882  return(0);
1883  }
1884  newvars = ABC_ALLOC(DdNodePtr,newsize);
1885  if (newvars == NULL) {
1886  unique->errorCode = CUDD_MEMORY_OUT;
1887  ABC_FREE(newsubtables);
1888  return(0);
1889  }
1890  newperm = ABC_ALLOC(int,newsize);
1891  if (newperm == NULL) {
1892  unique->errorCode = CUDD_MEMORY_OUT;
1893  ABC_FREE(newsubtables);
1894  ABC_FREE(newvars);
1895  return(0);
1896  }
1897  newinvperm = ABC_ALLOC(int,newsize);
1898  if (newinvperm == NULL) {
1899  unique->errorCode = CUDD_MEMORY_OUT;
1900  ABC_FREE(newsubtables);
1901  ABC_FREE(newvars);
1902  ABC_FREE(newperm);
1903  return(0);
1904  }
1905  if (unique->map != NULL) {
1906  newmap = ABC_ALLOC(int,newsize);
1907  if (newmap == NULL) {
1908  unique->errorCode = CUDD_MEMORY_OUT;
1909  ABC_FREE(newsubtables);
1910  ABC_FREE(newvars);
1911  ABC_FREE(newperm);
1912  ABC_FREE(newinvperm);
1913  return(0);
1914  }
1915  unique->memused += (newsize - unique->maxSize) * sizeof(int);
1916  }
1917  unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
1918  sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
1919  /* Copy levels before insertion points from old tables. */
1920  for (i = 0; i < level; i++) {
1921  newsubtables[i].slots = unique->subtables[i].slots;
1922  newsubtables[i].shift = unique->subtables[i].shift;
1923  newsubtables[i].keys = unique->subtables[i].keys;
1924  newsubtables[i].maxKeys = unique->subtables[i].maxKeys;
1925  newsubtables[i].dead = unique->subtables[i].dead;
1926  newsubtables[i].nodelist = unique->subtables[i].nodelist;
1927  newsubtables[i].bindVar = unique->subtables[i].bindVar;
1928  newsubtables[i].varType = unique->subtables[i].varType;
1929  newsubtables[i].pairIndex = unique->subtables[i].pairIndex;
1930  newsubtables[i].varHandled = unique->subtables[i].varHandled;
1931  newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped;
1932 
1933  newvars[i] = unique->vars[i];
1934  newperm[i] = unique->perm[i];
1935  newinvperm[i] = unique->invperm[i];
1936  }
1937  /* Finish initializing permutation for new table to old one. */
1938  for (i = level; i < oldsize; i++) {
1939  newperm[i] = unique->perm[i];
1940  }
1941  /* Initialize new levels. */
1942  for (i = level; i < level + n; i++) {
1943  newsubtables[i].slots = numSlots;
1944  newsubtables[i].shift = sizeof(int) * 8 -
1945  cuddComputeFloorLog2(numSlots);
1946  newsubtables[i].keys = 0;
1947  newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
1948  newsubtables[i].dead = 0;
1949  newsubtables[i].bindVar = 0;
1950  newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
1951  newsubtables[i].pairIndex = 0;
1952  newsubtables[i].varHandled = 0;
1953  newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE;
1954 
1955  newperm[oldsize + i - level] = i;
1956  newinvperm[i] = oldsize + i - level;
1957  newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
1958  if (newnodelist == NULL) {
1959  /* We are going to leak some memory. We should clean up. */
1960  unique->errorCode = CUDD_MEMORY_OUT;
1961  return(0);
1962  }
1963  for (j = 0; (unsigned) j < numSlots; j++) {
1964  newnodelist[j] = sentinel;
1965  }
1966  }
1967  /* Copy the old tables for levels past the insertion point. */
1968  for (i = level; i < oldsize; i++) {
1969  newsubtables[i+n].slots = unique->subtables[i].slots;
1970  newsubtables[i+n].shift = unique->subtables[i].shift;
1971  newsubtables[i+n].keys = unique->subtables[i].keys;
1972  newsubtables[i+n].maxKeys = unique->subtables[i].maxKeys;
1973  newsubtables[i+n].dead = unique->subtables[i].dead;
1974  newsubtables[i+n].nodelist = unique->subtables[i].nodelist;
1975  newsubtables[i+n].bindVar = unique->subtables[i].bindVar;
1976  newsubtables[i+n].varType = unique->subtables[i].varType;
1977  newsubtables[i+n].pairIndex = unique->subtables[i].pairIndex;
1978  newsubtables[i+n].varHandled = unique->subtables[i].varHandled;
1979  newsubtables[i+n].varToBeGrouped =
1980  unique->subtables[i].varToBeGrouped;
1981 
1982  newvars[i] = unique->vars[i];
1983  index = unique->invperm[i];
1984  newinvperm[i+n] = index;
1985  newperm[index] += n;
1986  }
1987  /* Update the map. */
1988  if (unique->map != NULL) {
1989  for (i = 0; i < oldsize; i++) {
1990  newmap[i] = unique->map[i];
1991  }
1992  for (i = oldsize; i < oldsize + n; i++) {
1993  newmap[i] = i;
1994  }
1995  ABC_FREE(unique->map);
1996  unique->map = newmap;
1997  }
1998  /* Install the new tables and free the old ones. */
1999  ABC_FREE(unique->subtables);
2000  unique->subtables = newsubtables;
2001  unique->maxSize = newsize;
2002  ABC_FREE(unique->vars);
2003  unique->vars = newvars;
2004  ABC_FREE(unique->perm);
2005  unique->perm = newperm;
2006  ABC_FREE(unique->invperm);
2007  unique->invperm = newinvperm;
2008  /* Update the stack for iterative procedures. */
2009  if (newsize > unique->maxSizeZ) {
2010  ABC_FREE(unique->stack);
2011  unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
2012  if (unique->stack == NULL) {
2013  unique->errorCode = CUDD_MEMORY_OUT;
2014  return(0);
2015  }
2016  unique->stack[0] = NULL; /* to suppress harmless UMR */
2017  unique->memused +=
2018  (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2019  * sizeof(DdNode *);
2020  }
2021  }
2022  /* Update manager parameters to account for the new subtables. */
2023  unique->slots += n * numSlots;
2024  ddFixLimits(unique);
2025  unique->size += n;
2026 
2027  /* Now that the table is in a coherent state, create the new
2028  ** projection functions. We need to temporarily disable reordering,
2029  ** because we cannot reorder without projection functions in place.
2030  **/
2031  one = unique->one;
2032  zero = Cudd_Not(one);
2033 
2034  reorderSave = unique->autoDyn;
2035  unique->autoDyn = 0;
2036  for (i = oldsize; i < oldsize + n; i++) {
2037  unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
2038  if (unique->vars[i] == NULL) {
2039  unique->autoDyn = reorderSave;
2040  /* Shift everything back so table remains coherent. */
2041  for (j = oldsize; j < i; j++) {
2042  Cudd_IterDerefBdd(unique,unique->vars[j]);
2043  cuddDeallocNode(unique,unique->vars[j]);
2044  unique->vars[j] = NULL;
2045  }
2046  for (j = level; j < oldsize; j++) {
2047  unique->subtables[j].slots = unique->subtables[j+n].slots;
2048  unique->subtables[j].slots = unique->subtables[j+n].slots;
2049  unique->subtables[j].shift = unique->subtables[j+n].shift;
2050  unique->subtables[j].keys = unique->subtables[j+n].keys;
2051  unique->subtables[j].maxKeys =
2052  unique->subtables[j+n].maxKeys;
2053  unique->subtables[j].dead = unique->subtables[j+n].dead;
2054  ABC_FREE(unique->subtables[j].nodelist);
2055  unique->subtables[j].nodelist =
2056  unique->subtables[j+n].nodelist;
2057  unique->subtables[j+n].nodelist = NULL;
2058  unique->subtables[j].bindVar =
2059  unique->subtables[j+n].bindVar;
2060  unique->subtables[j].varType =
2061  unique->subtables[j+n].varType;
2062  unique->subtables[j].pairIndex =
2063  unique->subtables[j+n].pairIndex;
2064  unique->subtables[j].varHandled =
2065  unique->subtables[j+n].varHandled;
2066  unique->subtables[j].varToBeGrouped =
2067  unique->subtables[j+n].varToBeGrouped;
2068  index = unique->invperm[j+n];
2069  unique->invperm[j] = index;
2070  unique->perm[index] -= n;
2071  }
2072  unique->size = oldsize;
2073  unique->slots -= n * numSlots;
2074  ddFixLimits(unique);
2075  (void) Cudd_DebugCheck(unique);
2076  return(0);
2077  }
2078  cuddRef(unique->vars[i]);
2079  }
2080  if (unique->tree != NULL) {
2081  unique->tree->size += n;
2082  unique->tree->index = unique->invperm[0];
2083  ddPatchTree(unique,unique->tree);
2084  }
2085  unique->autoDyn = reorderSave;
2086 
2087  return(1);
2088 
2089 } /* end of cuddInsertSubtables */
2090 
2091 
2092 /**Function********************************************************************
2093 
2094  Synopsis [Destroys the n most recently created subtables in a unique table.]
2095 
2096  Description [Destroys the n most recently created subtables in a unique
2097  table. n should be positive. The subtables should not contain any live
2098  nodes, except the (isolated) projection function. The projection
2099  functions are freed. Returns 1 if successful; 0 otherwise.]
2100 
2101  SideEffects [The variable map used for fast variable substitution is
2102  destroyed if it exists. In this case the cache is also cleared.]
2103 
2104  SeeAlso [cuddInsertSubtables Cudd_SetVarMap]
2105 
2106 ******************************************************************************/
2107 int
2108 cuddDestroySubtables(
2109  DdManager * unique,
2110  int n)
2111 {
2112  DdSubtable *subtables;
2113  DdNodePtr *nodelist;
2114  DdNodePtr *vars;
2115  int firstIndex, lastIndex;
2116  int index, level, newlevel;
2117  int lowestLevel;
2118  int shift;
2119  int found;
2120 
2121  /* Sanity check and set up. */
2122  if (n <= 0) return(0);
2123  if (n > unique->size) n = unique->size;
2124 
2125  subtables = unique->subtables;
2126  vars = unique->vars;
2127  firstIndex = unique->size - n;
2128  lastIndex = unique->size;
2129 
2130  /* Check for nodes labeled by the variables being destroyed
2131  ** that may still be in use. It is allowed to destroy a variable
2132  ** only if there are no such nodes. Also, find the lowest level
2133  ** among the variables being destroyed. This will make further
2134  ** processing more efficient.
2135  */
2136  lowestLevel = unique->size;
2137  for (index = firstIndex; index < lastIndex; index++) {
2138  level = unique->perm[index];
2139  if (level < lowestLevel) lowestLevel = level;
2140  nodelist = subtables[level].nodelist;
2141  if (subtables[level].keys - subtables[level].dead != 1) return(0);
2142  /* The projection function should be isolated. If the ref count
2143  ** is 1, everything is OK. If the ref count is saturated, then
2144  ** we need to make sure that there are no nodes pointing to it.
2145  ** As for the external references, we assume the application is
2146  ** responsible for them.
2147  */
2148  if (vars[index]->ref != 1) {
2149  if (vars[index]->ref != DD_MAXREF) return(0);
2150  found = cuddFindParent(unique,vars[index]);
2151  if (found) {
2152  return(0);
2153  } else {
2154  vars[index]->ref = 1;
2155  }
2156  }
2157  Cudd_RecursiveDeref(unique,vars[index]);
2158  }
2159 
2160  /* Collect garbage, because we cannot afford having dead nodes pointing
2161  ** to the dead nodes in the subtables being destroyed.
2162  */
2163  (void) cuddGarbageCollect(unique,1);
2164 
2165  /* Here we know we can destroy our subtables. */
2166  for (index = firstIndex; index < lastIndex; index++) {
2167  level = unique->perm[index];
2168  nodelist = subtables[level].nodelist;
2169 #ifdef DD_DEBUG
2170  assert(subtables[level].keys == 0);
2171 #endif
2172  ABC_FREE(nodelist);
2173  unique->memused -= sizeof(DdNodePtr) * subtables[level].slots;
2174  unique->slots -= subtables[level].slots;
2175  unique->dead -= subtables[level].dead;
2176  }
2177 
2178  /* Here all subtables to be destroyed have their keys field == 0 and
2179  ** their hash tables have been freed.
2180  ** We now scan the subtables from level lowestLevel + 1 to level size - 1,
2181  ** shifting the subtables as required. We keep a running count of
2182  ** how many subtables have been moved, so that we know by how many
2183  ** positions each subtable should be shifted.
2184  */
2185  shift = 1;
2186  for (level = lowestLevel + 1; level < unique->size; level++) {
2187  if (subtables[level].keys == 0) {
2188  shift++;
2189  continue;
2190  }
2191  newlevel = level - shift;
2192  subtables[newlevel].slots = subtables[level].slots;
2193  subtables[newlevel].shift = subtables[level].shift;
2194  subtables[newlevel].keys = subtables[level].keys;
2195  subtables[newlevel].maxKeys = subtables[level].maxKeys;
2196  subtables[newlevel].dead = subtables[level].dead;
2197  subtables[newlevel].nodelist = subtables[level].nodelist;
2198  index = unique->invperm[level];
2199  unique->perm[index] = newlevel;
2200  unique->invperm[newlevel] = index;
2201  subtables[newlevel].bindVar = subtables[level].bindVar;
2202  subtables[newlevel].varType = subtables[level].varType;
2203  subtables[newlevel].pairIndex = subtables[level].pairIndex;
2204  subtables[newlevel].varHandled = subtables[level].varHandled;
2205  subtables[newlevel].varToBeGrouped = subtables[level].varToBeGrouped;
2206  }
2207  /* Destroy the map. If a surviving variable is
2208  ** mapped to a dying variable, and the map were used again,
2209  ** an out-of-bounds access to unique->vars would result. */
2210  if (unique->map != NULL) {
2211  cuddCacheFlush(unique);
2212  ABC_FREE(unique->map);
2213  unique->map = NULL;
2214  }
2215 
2216  unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
2217  unique->size -= n;
2218 
2219  return(1);
2220 
2221 } /* end of cuddDestroySubtables */
2222 
2223 
2224 /**Function********************************************************************
2225 
2226  Synopsis [Increases the number of ZDD subtables in a unique table so
2227  that it meets or exceeds index.]
2228 
2229  Description [Increases the number of ZDD subtables in a unique table so
2230  that it meets or exceeds index. When new ZDD variables are created, it
2231  is possible to preserve the functions unchanged, or it is possible to
2232  preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
2233  the covers. Returns 1 if successful; 0 otherwise.]
2234 
2235  SideEffects [None]
2236 
2237  SeeAlso [ddResizeTable]
2238 
2239 ******************************************************************************/
2240 int
2241 cuddResizeTableZdd(
2242  DdManager * unique,
2243  int index)
2244 {
2245  DdSubtable *newsubtables;
2246  DdNodePtr *newnodelist;
2247  int oldsize,newsize;
2248  int i,j,reorderSave;
2249  unsigned int numSlots = unique->initSlots;
2250  int *newperm, *newinvperm;
2251 
2252  oldsize = unique->sizeZ;
2253  /* Easy case: there is still room in the current table. */
2254  if (index < unique->maxSizeZ) {
2255  for (i = oldsize; i <= index; i++) {
2256  unique->subtableZ[i].slots = numSlots;
2257  unique->subtableZ[i].shift = sizeof(int) * 8 -
2258  cuddComputeFloorLog2(numSlots);
2259  unique->subtableZ[i].keys = 0;
2260  unique->subtableZ[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2261  unique->subtableZ[i].dead = 0;
2262  unique->permZ[i] = i;
2263  unique->invpermZ[i] = i;
2264  newnodelist = unique->subtableZ[i].nodelist =
2265  ABC_ALLOC(DdNodePtr, numSlots);
2266  if (newnodelist == NULL) {
2267  unique->errorCode = CUDD_MEMORY_OUT;
2268  return(0);
2269  }
2270  for (j = 0; (unsigned) j < numSlots; j++) {
2271  newnodelist[j] = NULL;
2272  }
2273  }
2274  } else {
2275  /* The current table is too small: we need to allocate a new,
2276  ** larger one; move all old subtables, and initialize the new
2277  ** subtables up to index included.
2278  */
2279  newsize = index + DD_DEFAULT_RESIZE;
2280 #ifdef DD_VERBOSE
2281  (void) fprintf(unique->err,
2282  "Increasing the ZDD table size from %d to %d\n",
2283  unique->maxSizeZ, newsize);
2284 #endif
2285  newsubtables = ABC_ALLOC(DdSubtable,newsize);
2286  if (newsubtables == NULL) {
2287  unique->errorCode = CUDD_MEMORY_OUT;
2288  return(0);
2289  }
2290  newperm = ABC_ALLOC(int,newsize);
2291  if (newperm == NULL) {
2292  unique->errorCode = CUDD_MEMORY_OUT;
2293  return(0);
2294  }
2295  newinvperm = ABC_ALLOC(int,newsize);
2296  if (newinvperm == NULL) {
2297  unique->errorCode = CUDD_MEMORY_OUT;
2298  return(0);
2299  }
2300  unique->memused += (newsize - unique->maxSizeZ) * ((numSlots+1) *
2301  sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
2302  if (newsize > unique->maxSize) {
2303  ABC_FREE(unique->stack);
2304  unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
2305  if (unique->stack == NULL) {
2306  unique->errorCode = CUDD_MEMORY_OUT;
2307  return(0);
2308  }
2309  unique->stack[0] = NULL; /* to suppress harmless UMR */
2310  unique->memused +=
2311  (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2312  * sizeof(DdNode *);
2313  }
2314  for (i = 0; i < oldsize; i++) {
2315  newsubtables[i].slots = unique->subtableZ[i].slots;
2316  newsubtables[i].shift = unique->subtableZ[i].shift;
2317  newsubtables[i].keys = unique->subtableZ[i].keys;
2318  newsubtables[i].maxKeys = unique->subtableZ[i].maxKeys;
2319  newsubtables[i].dead = unique->subtableZ[i].dead;
2320  newsubtables[i].nodelist = unique->subtableZ[i].nodelist;
2321  newperm[i] = unique->permZ[i];
2322  newinvperm[i] = unique->invpermZ[i];
2323  }
2324  for (i = oldsize; i <= index; i++) {
2325  newsubtables[i].slots = numSlots;
2326  newsubtables[i].shift = sizeof(int) * 8 -
2327  cuddComputeFloorLog2(numSlots);
2328  newsubtables[i].keys = 0;
2329  newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2330  newsubtables[i].dead = 0;
2331  newperm[i] = i;
2332  newinvperm[i] = i;
2333  newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
2334  if (newnodelist == NULL) {
2335  unique->errorCode = CUDD_MEMORY_OUT;
2336  return(0);
2337  }
2338  for (j = 0; (unsigned) j < numSlots; j++) {
2339  newnodelist[j] = NULL;
2340  }
2341  }
2342  ABC_FREE(unique->subtableZ);
2343  unique->subtableZ = newsubtables;
2344  unique->maxSizeZ = newsize;
2345  ABC_FREE(unique->permZ);
2346  unique->permZ = newperm;
2347  ABC_FREE(unique->invpermZ);
2348  unique->invpermZ = newinvperm;
2349  }
2350  unique->slots += (index + 1 - unique->sizeZ) * numSlots;
2351  ddFixLimits(unique);
2352  unique->sizeZ = index + 1;
2353 
2354  /* Now that the table is in a coherent state, update the ZDD
2355  ** universe. We need to temporarily disable reordering,
2356  ** because we cannot reorder without universe in place.
2357  */
2358 
2359  reorderSave = unique->autoDynZ;
2360  unique->autoDynZ = 0;
2361  cuddZddFreeUniv(unique);
2362  if (!cuddZddInitUniv(unique)) {
2363  unique->autoDynZ = reorderSave;
2364  return(0);
2365  }
2366  unique->autoDynZ = reorderSave;
2367 
2368  return(1);
2369 
2370 } /* end of cuddResizeTableZdd */
2371 
2372 
2373 /**Function********************************************************************
2374 
2375  Synopsis [Adjusts parameters of a table to slow down its growth.]
2376 
2377  Description []
2378 
2379  SideEffects [None]
2380 
2381  SeeAlso []
2382 
2383 ******************************************************************************/
2384 void
2385 cuddSlowTableGrowth(
2386  DdManager *unique)
2387 {
2388  int i;
2389 
2390  unique->maxCacheHard = unique->cacheSlots - 1;
2391  unique->cacheSlack = - (int) (unique->cacheSlots + 1);
2392  for (i = 0; i < unique->size; i++) {
2393  unique->subtables[i].maxKeys <<= 2;
2394  }
2395  unique->gcFrac = DD_GC_FRAC_MIN;
2396  unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots);
2397  cuddShrinkDeathRow(unique);
2398  (void) fprintf(unique->err,"Slowing down table growth: ");
2399  (void) fprintf(unique->err,"GC fraction = %.2f\t", unique->gcFrac);
2400  (void) fprintf(unique->err,"minDead = %u\n", unique->minDead);
2401 
2402 } /* end of cuddSlowTableGrowth */
2403 
2404 
2405 /*---------------------------------------------------------------------------*/
2406 /* Definition of static functions */
2407 /*---------------------------------------------------------------------------*/
2408 
2409 
2410 /**Function********************************************************************
2411 
2412  Synopsis [Rehashes a ZDD unique subtable.]
2413 
2414  Description []
2415 
2416  SideEffects [None]
2417 
2418  SeeAlso [cuddRehash]
2419 
2420 ******************************************************************************/
2421 static void
2422 ddRehashZdd(
2423  DdManager * unique,
2424  int i)
2425 {
2426  unsigned int slots, oldslots;
2427  int shift, oldshift;
2428  int j, pos;
2429  DdNodePtr *nodelist, *oldnodelist;
2430  DdNode *node, *next;
2431  extern DD_OOMFP MMoutOfMemory;
2432  DD_OOMFP saveHandler;
2433 
2434  if (unique->slots > unique->looseUpTo) {
2435  unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots);
2436 #ifdef DD_VERBOSE
2437  if (unique->gcFrac == DD_GC_FRAC_HI) {
2438  (void) fprintf(unique->err,"GC fraction = %.2f\t",
2439  DD_GC_FRAC_LO);
2440  (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
2441  }
2442 #endif
2443  unique->gcFrac = DD_GC_FRAC_LO;
2444  }
2445 
2446  assert(i != CUDD_MAXINDEX);
2447  oldslots = unique->subtableZ[i].slots;
2448  oldshift = unique->subtableZ[i].shift;
2449  oldnodelist = unique->subtableZ[i].nodelist;
2450 
2451  /* Compute the new size of the subtable. Normally, we just
2452  ** double. However, after reordering, a table may be severely
2453  ** overloaded. Therefore, we iterate. */
2454  slots = oldslots;
2455  shift = oldshift;
2456  do {
2457  slots <<= 1;
2458  shift--;
2459  } while (slots * DD_MAX_SUBTABLE_DENSITY < unique->subtableZ[i].keys);
2460 
2461  saveHandler = MMoutOfMemory;
2462  MMoutOfMemory = Cudd_OutOfMem;
2463  nodelist = ABC_ALLOC(DdNodePtr, slots);
2464  MMoutOfMemory = saveHandler;
2465  if (nodelist == NULL) {
2466  (void) fprintf(unique->err,
2467  "Unable to resize ZDD subtable %d for lack of memory.\n",
2468  i);
2469  (void) cuddGarbageCollect(unique,1);
2470  for (j = 0; j < unique->sizeZ; j++) {
2471  unique->subtableZ[j].maxKeys <<= 1;
2472  }
2473  return;
2474  }
2475  unique->subtableZ[i].nodelist = nodelist;
2476  unique->subtableZ[i].slots = slots;
2477  unique->subtableZ[i].shift = shift;
2478  unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
2479  for (j = 0; (unsigned) j < slots; j++) {
2480  nodelist[j] = NULL;
2481  }
2482  for (j = 0; (unsigned) j < oldslots; j++) {
2483  node = oldnodelist[j];
2484  while (node != NULL) {
2485  next = node->next;
2486  pos = ddHash(cuddF2L(cuddT(node)), cuddF2L(cuddE(node)), shift);
2487  node->next = nodelist[pos];
2488  nodelist[pos] = node;
2489  node = next;
2490  }
2491  }
2492  ABC_FREE(oldnodelist);
2493 
2494 #ifdef DD_VERBOSE
2495  (void) fprintf(unique->err,
2496  "rehashing layer %d: keys %d dead %d new size %d\n",
2497  i, unique->subtableZ[i].keys,
2498  unique->subtableZ[i].dead, slots);
2499 #endif
2500 
2501  /* Update global data. */
2502  unique->memused += (slots - oldslots) * sizeof(DdNode *);
2503  unique->slots += (slots - oldslots);
2504  ddFixLimits(unique);
2505 
2506 } /* end of ddRehashZdd */
2507 
2508 
2509 /**Function********************************************************************
2510 
2511  Synopsis [Increases the number of subtables in a unique table so
2512  that it meets or exceeds index.]
2513 
2514  Description [Increases the number of subtables in a unique table so
2515  that it meets or exceeds index. Returns 1 if successful; 0 otherwise.]
2516 
2517  SideEffects [None]
2518 
2519  SeeAlso [cuddResizeTableZdd]
2520 
2521 ******************************************************************************/
2522 static int
2523 ddResizeTable(
2524  DdManager * unique,
2525  int index)
2526 {
2527  DdSubtable *newsubtables;
2528  DdNodePtr *newnodelist;
2529  DdNodePtr *newvars;
2530  DdNode *sentinel = &(unique->sentinel);
2531  int oldsize,newsize;
2532  int i,j,reorderSave;
2533  int numSlots = unique->initSlots;
2534  int *newperm, *newinvperm, *newmap = NULL;
2535  DdNode *one, *zero;
2536 
2537  oldsize = unique->size;
2538  /* Easy case: there is still room in the current table. */
2539  if (index < unique->maxSize) {
2540  for (i = oldsize; i <= index; i++) {
2541  unique->subtables[i].slots = numSlots;
2542  unique->subtables[i].shift = sizeof(int) * 8 -
2543  cuddComputeFloorLog2(numSlots);
2544  unique->subtables[i].keys = 0;
2545  unique->subtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2546  unique->subtables[i].dead = 0;
2547  unique->subtables[i].bindVar = 0;
2548  unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
2549  unique->subtables[i].pairIndex = 0;
2550  unique->subtables[i].varHandled = 0;
2551  unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;
2552 
2553  unique->perm[i] = i;
2554  unique->invperm[i] = i;
2555  newnodelist = unique->subtables[i].nodelist =
2556  ABC_ALLOC(DdNodePtr, numSlots);
2557  if (newnodelist == NULL) {
2558  for (j = oldsize; j < i; j++) {
2559  ABC_FREE(unique->subtables[j].nodelist);
2560  }
2561  unique->errorCode = CUDD_MEMORY_OUT;
2562  return(0);
2563  }
2564  for (j = 0; j < numSlots; j++) {
2565  newnodelist[j] = sentinel;
2566  }
2567  }
2568  if (unique->map != NULL) {
2569  for (i = oldsize; i <= index; i++) {
2570  unique->map[i] = i;
2571  }
2572  }
2573  } else {
2574  /* The current table is too small: we need to allocate a new,
2575  ** larger one; move all old subtables, and initialize the new
2576  ** subtables up to index included.
2577  */
2578  newsize = index + DD_DEFAULT_RESIZE;
2579 #ifdef DD_VERBOSE
2580  (void) fprintf(unique->err,
2581  "Increasing the table size from %d to %d\n",
2582  unique->maxSize, newsize);
2583 #endif
2584  newsubtables = ABC_ALLOC(DdSubtable,newsize);
2585  if (newsubtables == NULL) {
2586  unique->errorCode = CUDD_MEMORY_OUT;
2587  return(0);
2588  }
2589  newvars = ABC_ALLOC(DdNodePtr,newsize);
2590  if (newvars == NULL) {
2591  ABC_FREE(newsubtables);
2592  unique->errorCode = CUDD_MEMORY_OUT;
2593  return(0);
2594  }
2595  newperm = ABC_ALLOC(int,newsize);
2596  if (newperm == NULL) {
2597  ABC_FREE(newsubtables);
2598  ABC_FREE(newvars);
2599  unique->errorCode = CUDD_MEMORY_OUT;
2600  return(0);
2601  }
2602  newinvperm = ABC_ALLOC(int,newsize);
2603  if (newinvperm == NULL) {
2604  ABC_FREE(newsubtables);
2605  ABC_FREE(newvars);
2606  ABC_FREE(newperm);
2607  unique->errorCode = CUDD_MEMORY_OUT;
2608  return(0);
2609  }
2610  if (unique->map != NULL) {
2611  newmap = ABC_ALLOC(int,newsize);
2612  if (newmap == NULL) {
2613  ABC_FREE(newsubtables);
2614  ABC_FREE(newvars);
2615  ABC_FREE(newperm);
2616  ABC_FREE(newinvperm);
2617  unique->errorCode = CUDD_MEMORY_OUT;
2618  return(0);
2619  }
2620  unique->memused += (newsize - unique->maxSize) * sizeof(int);
2621  }
2622  unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
2623  sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
2624  if (newsize > unique->maxSizeZ) {
2625  ABC_FREE(unique->stack);
2626  unique->stack = ABC_ALLOC(DdNodePtr,newsize + 1);
2627  if (unique->stack == NULL) {
2628  ABC_FREE(newsubtables);
2629  ABC_FREE(newvars);
2630  ABC_FREE(newperm);
2631  ABC_FREE(newinvperm);
2632  if (unique->map != NULL) {
2633  ABC_FREE(newmap);
2634  }
2635  unique->errorCode = CUDD_MEMORY_OUT;
2636  return(0);
2637  }
2638  unique->stack[0] = NULL; /* to suppress harmless UMR */
2639  unique->memused +=
2640  (newsize - ddMax(unique->maxSize,unique->maxSizeZ))
2641  * sizeof(DdNode *);
2642  }
2643  for (i = 0; i < oldsize; i++) {
2644  newsubtables[i].slots = unique->subtables[i].slots;
2645  newsubtables[i].shift = unique->subtables[i].shift;
2646  newsubtables[i].keys = unique->subtables[i].keys;
2647  newsubtables[i].maxKeys = unique->subtables[i].maxKeys;
2648  newsubtables[i].dead = unique->subtables[i].dead;
2649  newsubtables[i].nodelist = unique->subtables[i].nodelist;
2650  newsubtables[i].bindVar = unique->subtables[i].bindVar;
2651  newsubtables[i].varType = unique->subtables[i].varType;
2652  newsubtables[i].pairIndex = unique->subtables[i].pairIndex;
2653  newsubtables[i].varHandled = unique->subtables[i].varHandled;
2654  newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped;
2655 
2656  newvars[i] = unique->vars[i];
2657  newperm[i] = unique->perm[i];
2658  newinvperm[i] = unique->invperm[i];
2659  }
2660  for (i = oldsize; i <= index; i++) {
2661  newsubtables[i].slots = numSlots;
2662  newsubtables[i].shift = sizeof(int) * 8 -
2663  cuddComputeFloorLog2(numSlots);
2664  newsubtables[i].keys = 0;
2665  newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
2666  newsubtables[i].dead = 0;
2667  newsubtables[i].bindVar = 0;
2668  newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
2669  newsubtables[i].pairIndex = 0;
2670  newsubtables[i].varHandled = 0;
2671  newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE;
2672 
2673  newperm[i] = i;
2674  newinvperm[i] = i;
2675  newnodelist = newsubtables[i].nodelist = ABC_ALLOC(DdNodePtr, numSlots);
2676  if (newnodelist == NULL) {
2677  unique->errorCode = CUDD_MEMORY_OUT;
2678  return(0);
2679  }
2680  for (j = 0; j < numSlots; j++) {
2681  newnodelist[j] = sentinel;
2682  }
2683  }
2684  if (unique->map != NULL) {
2685  for (i = 0; i < oldsize; i++) {
2686  newmap[i] = unique->map[i];
2687  }
2688  for (i = oldsize; i <= index; i++) {
2689  newmap[i] = i;
2690  }
2691  ABC_FREE(unique->map);
2692  unique->map = newmap;
2693  }
2694  ABC_FREE(unique->subtables);
2695  unique->subtables = newsubtables;
2696  unique->maxSize = newsize;
2697  ABC_FREE(unique->vars);
2698  unique->vars = newvars;
2699  ABC_FREE(unique->perm);
2700  unique->perm = newperm;
2701  ABC_FREE(unique->invperm);
2702  unique->invperm = newinvperm;
2703  }
2704 
2705  /* Now that the table is in a coherent state, create the new
2706  ** projection functions. We need to temporarily disable reordering,
2707  ** because we cannot reorder without projection functions in place.
2708  **/
2709  one = unique->one;
2710  zero = Cudd_Not(one);
2711 
2712  unique->size = index + 1;
2713  unique->slots += (index + 1 - oldsize) * numSlots;
2714  ddFixLimits(unique);
2715 
2716  reorderSave = unique->autoDyn;
2717  unique->autoDyn = 0;
2718  for (i = oldsize; i <= index; i++) {
2719  unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
2720  if (unique->vars[i] == NULL) {
2721  unique->autoDyn = reorderSave;
2722  for (j = oldsize; j < i; j++) {
2723  Cudd_IterDerefBdd(unique,unique->vars[j]);
2724  cuddDeallocNode(unique,unique->vars[j]);
2725  unique->vars[j] = NULL;
2726  }
2727  for (j = oldsize; j <= index; j++) {
2728  ABC_FREE(unique->subtables[j].nodelist);
2729  unique->subtables[j].nodelist = NULL;
2730  }
2731  unique->size = oldsize;
2732  unique->slots -= (index + 1 - oldsize) * numSlots;
2733  ddFixLimits(unique);
2734  return(0);
2735  }
2736  cuddRef(unique->vars[i]);
2737  }
2738  unique->autoDyn = reorderSave;
2739 
2740  return(1);
2741 
2742 } /* end of ddResizeTable */
2743 
2744 
2745 /**Function********************************************************************
2746 
2747  Synopsis [Searches the subtables above node for a parent.]
2748 
2749  Description [Searches the subtables above node for a parent. Returns 1
2750  as soon as one parent is found. Returns 0 is the search is fruitless.]
2751 
2752  SideEffects [None]
2753 
2754  SeeAlso []
2755 
2756 ******************************************************************************/
2757 static int
2758 cuddFindParent(
2759  DdManager * table,
2760  DdNode * node)
2761 {
2762  int i,j;
2763  int slots;
2764  DdNodePtr *nodelist;
2765  DdNode *f;
2766 
2767  for (i = cuddI(table,node->index) - 1; i >= 0; i--) {
2768  nodelist = table->subtables[i].nodelist;
2769  slots = table->subtables[i].slots;
2770 
2771  for (j = 0; j < slots; j++) {
2772  f = nodelist[j];
2773  while (cuddT(f) > node) {
2774  f = f->next;
2775  }
2776  while (cuddT(f) == node && Cudd_Regular(cuddE(f)) > node) {
2777  f = f->next;
2778  }
2779  if (cuddT(f) == node && Cudd_Regular(cuddE(f)) == node) {
2780  return(1);
2781  }
2782  }
2783  }
2784 
2785  return(0);
2786 
2787 } /* end of cuddFindParent */
2788 
2789 
2790 /**Function********************************************************************
2791 
2792  Synopsis [Adjusts the values of table limits.]
2793 
2794  Description [Adjusts the values of table fields controlling the.
2795  sizes of subtables and computed table. If the computed table is too small
2796  according to the new values, it is resized.]
2797 
2798  SideEffects [Modifies manager fields. May resize computed table.]
2799 
2800  SeeAlso []
2801 
2802 ******************************************************************************/
2803 DD_INLINE
2804 static void
2805 ddFixLimits(
2806  DdManager *unique)
2807 {
2808  unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
2809  unique->cacheSlack = (int) ddMin(unique->maxCacheHard,
2810  DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots) -
2811  2 * (int) unique->cacheSlots;
2812  if (unique->cacheSlots < unique->slots/2 && unique->cacheSlack >= 0)
2813  cuddCacheResize(unique);
2814  return;
2815 
2816 } /* end of ddFixLimits */
2817 
2818 
2819 #ifndef DD_UNSORTED_FREE_LIST
2820 #ifdef DD_RED_BLACK_FREE_LIST
2821 /**Function********************************************************************
2822 
2823  Synopsis [Inserts a DdNode in a red/black search tree.]
2824 
2825  Description [Inserts a DdNode in a red/black search tree. Nodes from
2826  the same "page" (defined by DD_PAGE_MASK) are linked in a LIFO list.]
2827 
2828  SideEffects [None]
2829 
2830  SeeAlso [cuddOrderedThread]
2831 
2832 ******************************************************************************/
2833 static void
2834 cuddOrderedInsert(
2835  DdNodePtr * root,
2836  DdNodePtr node)
2837 {
2838  DdNode *scan;
2839  DdNodePtr *scanP;
2840  DdNodePtr *stack[DD_STACK_SIZE];
2841  int stackN = 0;
2842 
2843  scanP = root;
2844  while ((scan = *scanP) != NULL) {
2845  stack[stackN++] = scanP;
2846  if (DD_INSERT_COMPARE(node, scan) == 0) { /* add to page list */
2847  DD_NEXT(node) = DD_NEXT(scan);
2848  DD_NEXT(scan) = node;
2849  return;
2850  }
2851  scanP = (node < scan) ? &DD_LEFT(scan) : &DD_RIGHT(scan);
2852  }
2853  DD_RIGHT(node) = DD_LEFT(node) = DD_NEXT(node) = NULL;
2854  DD_COLOR(node) = DD_RED;
2855  *scanP = node;
2856  stack[stackN] = &node;
2857  cuddDoRebalance(stack,stackN);
2858 
2859 } /* end of cuddOrderedInsert */
2860 
2861 
2862 /**Function********************************************************************
2863 
2864  Synopsis [Threads all the nodes of a search tree into a linear list.]
2865 
2866  Description [Threads all the nodes of a search tree into a linear
2867  list. For each node of the search tree, the "left" child, if non-null, has
2868  a lower address than its parent, and the "right" child, if non-null, has a
2869  higher address than its parent.
2870  The list is sorted in order of increasing addresses. The search
2871  tree is destroyed as a result of this operation. The last element of
2872  the linear list is made to point to the address passed in list. Each
2873  node if the search tree is a linearly-linked list of nodes from the
2874  same memory page (as defined in DD_PAGE_MASK). When a node is added to
2875  the linear list, all the elements of the linked list are added.]
2876 
2877  SideEffects [The search tree is destroyed as a result of this operation.]
2878 
2879  SeeAlso [cuddOrderedInsert]
2880 
2881 ******************************************************************************/
2882 static DdNode *
2883 cuddOrderedThread(
2884  DdNode * root,
2885  DdNode * list)
2886 {
2887  DdNode *current, *next, *prev, *end;
2888 
2889  current = root;
2890  /* The first word in the node is used to implement a stack that holds
2891  ** the nodes from the root of the tree to the current node. Here we
2892  ** put the root of the tree at the bottom of the stack.
2893  */
2894  *((DdNodePtr *) current) = NULL;
2895 
2896  while (current != NULL) {
2897  if (DD_RIGHT(current) != NULL) {
2898  /* If possible, we follow the "right" link. Eventually we'll
2899  ** find the node with the largest address in the current tree.
2900  ** In this phase we use the first word of a node to implemen
2901  ** a stack of the nodes on the path from the root to "current".
2902  ** Also, we disconnect the "right" pointers to indicate that
2903  ** we have already followed them.
2904  */
2905  next = DD_RIGHT(current);
2906  DD_RIGHT(current) = NULL;
2907  *((DdNodePtr *)next) = current;
2908  current = next;
2909  } else {
2910  /* We can't proceed along the "right" links any further.
2911  ** Hence "current" is the largest element in the current tree.
2912  ** We make this node the new head of "list". (Repeating this
2913  ** operation until the tree is empty yields the desired linear
2914  ** threading of all nodes.)
2915  */
2916  prev = *((DdNodePtr *) current); /* save prev node on stack in prev */
2917  /* Traverse the linked list of current until the end. */
2918  for (end = current; DD_NEXT(end) != NULL; end = DD_NEXT(end));
2919  DD_NEXT(end) = list; /* attach "list" at end and make */
2920  list = current; /* "current" the new head of "list" */
2921  /* Now, if current has a "left" child, we push it on the stack.
2922  ** Otherwise, we just continue with the parent of "current".
2923  */
2924  if (DD_LEFT(current) != NULL) {
2925  next = DD_LEFT(current);
2926  *((DdNodePtr *) next) = prev;
2927  current = next;
2928  } else {
2929  current = prev;
2930  }
2931  }
2932  }
2933 
2934  return(list);
2935 
2936 } /* end of cuddOrderedThread */
2937 
2938 
2939 /**Function********************************************************************
2940 
2941  Synopsis [Performs the left rotation for red/black trees.]
2942 
2943  Description []
2944 
2945  SideEffects [None]
2946 
2947  SeeAlso [cuddRotateRight]
2948 
2949 ******************************************************************************/
2950 DD_INLINE
2951 static void
2952 cuddRotateLeft(
2953  DdNodePtr * nodeP)
2954 {
2955  DdNode *newRoot;
2956  DdNode *oldRoot = *nodeP;
2957 
2958  *nodeP = newRoot = DD_RIGHT(oldRoot);
2959  DD_RIGHT(oldRoot) = DD_LEFT(newRoot);
2960  DD_LEFT(newRoot) = oldRoot;
2961 
2962 } /* end of cuddRotateLeft */
2963 
2964 
2965 /**Function********************************************************************
2966 
2967  Synopsis [Performs the right rotation for red/black trees.]
2968 
2969  Description []
2970 
2971  SideEffects [None]
2972 
2973  SeeAlso [cuddRotateLeft]
2974 
2975 ******************************************************************************/
2976 DD_INLINE
2977 static void
2978 cuddRotateRight(
2979  DdNodePtr * nodeP)
2980 {
2981  DdNode *newRoot;
2982  DdNode *oldRoot = *nodeP;
2983 
2984  *nodeP = newRoot = DD_LEFT(oldRoot);
2985  DD_LEFT(oldRoot) = DD_RIGHT(newRoot);
2986  DD_RIGHT(newRoot) = oldRoot;
2987 
2988 } /* end of cuddRotateRight */
2989 
2990 
2991 /**Function********************************************************************
2992 
2993  Synopsis [Rebalances a red/black tree.]
2994 
2995  Description []
2996 
2997  SideEffects [None]
2998 
2999  SeeAlso []
3000 
3001 ******************************************************************************/
3002 static void
3003 cuddDoRebalance(
3004  DdNodePtr ** stack,
3005  int stackN)
3006 {
3007  DdNodePtr *xP, *parentP, *grandpaP;
3008  DdNode *x, *y, *parent, *grandpa;
3009 
3010  xP = stack[stackN];
3011  x = *xP;
3012  /* Work our way back up, re-balancing the tree. */
3013  while (--stackN >= 0) {
3014  parentP = stack[stackN];
3015  parent = *parentP;
3016  if (DD_IS_BLACK(parent)) break;
3017  /* Since the root is black, here a non-null grandparent exists. */
3018  grandpaP = stack[stackN-1];
3019  grandpa = *grandpaP;
3020  if (parent == DD_LEFT(grandpa)) {
3021  y = DD_RIGHT(grandpa);
3022  if (y != NULL && DD_IS_RED(y)) {
3023  DD_COLOR(parent) = DD_BLACK;
3024  DD_COLOR(y) = DD_BLACK;
3025  DD_COLOR(grandpa) = DD_RED;
3026  x = grandpa;
3027  stackN--;
3028  } else {
3029  if (x == DD_RIGHT(parent)) {
3030  cuddRotateLeft(parentP);
3031  DD_COLOR(x) = DD_BLACK;
3032  } else {
3033  DD_COLOR(parent) = DD_BLACK;
3034  }
3035  DD_COLOR(grandpa) = DD_RED;
3036  cuddRotateRight(grandpaP);
3037  break;
3038  }
3039  } else {
3040  y = DD_LEFT(grandpa);
3041  if (y != NULL && DD_IS_RED(y)) {
3042  DD_COLOR(parent) = DD_BLACK;
3043  DD_COLOR(y) = DD_BLACK;
3044  DD_COLOR(grandpa) = DD_RED;
3045  x = grandpa;
3046  stackN--;
3047  } else {
3048  if (x == DD_LEFT(parent)) {
3049  cuddRotateRight(parentP);
3050  DD_COLOR(x) = DD_BLACK;
3051  } else {
3052  DD_COLOR(parent) = DD_BLACK;
3053  }
3054  DD_COLOR(grandpa) = DD_RED;
3055  cuddRotateLeft(grandpaP);
3056  }
3057  }
3058  }
3059  DD_COLOR(*(stack[0])) = DD_BLACK;
3060 
3061 } /* end of cuddDoRebalance */
3062 #endif
3063 #endif
3064 
3065 
3066 /**Function********************************************************************
3067 
3068  Synopsis [Fixes a variable tree after the insertion of new subtables.]
3069 
3070  Description [Fixes a variable tree after the insertion of new subtables.
3071  After such an insertion, the low fields of the tree below the insertion
3072  point are inconsistent.]
3073 
3074  SideEffects [None]
3075 
3076  SeeAlso []
3077 
3078 ******************************************************************************/
3079 static void
3080 ddPatchTree(
3081  DdManager *dd,
3082  MtrNode *treenode)
3083 {
3084  MtrNode *auxnode = treenode;
3085 
3086  while (auxnode != NULL) {
3087  auxnode->low = dd->perm[auxnode->index];
3088  if (auxnode->child != NULL) {
3089  ddPatchTree(dd, auxnode->child);
3090  }
3091  auxnode = auxnode->younger;
3092  }
3093 
3094  return;
3095 
3096 } /* end of ddPatchTree */
3097 
3098 
3099 #ifdef DD_DEBUG
3100 /**Function********************************************************************
3101 
3102  Synopsis [Checks whether a collision list is ordered.]
3103 
3104  Description []
3105 
3106  SideEffects [None]
3107 
3108  SeeAlso []
3109 
3110 ******************************************************************************/
3111 static int
3112 cuddCheckCollisionOrdering(
3113  DdManager *unique,
3114  int i,
3115  int j)
3116 {
3117  int slots;
3118  DdNode *node, *next;
3119  DdNodePtr *nodelist;
3120  DdNode *sentinel = &(unique->sentinel);
3121 
3122  nodelist = unique->subtables[i].nodelist;
3123  slots = unique->subtables[i].slots;
3124  node = nodelist[j];
3125  if (node == sentinel) return(1);
3126  next = node->next;
3127  while (next != sentinel) {
3128  if (cuddT(node) < cuddT(next) ||
3129  (cuddT(node) == cuddT(next) && cuddE(node) < cuddE(next))) {
3130  (void) fprintf(unique->err,
3131  "Unordered list: index %u, position %d\n", i, j);
3132  return(0);
3133  }
3134  node = next;
3135  next = node->next;
3136  }
3137  return(1);
3138 
3139 } /* end of cuddCheckCollisionOrdering */
3140 #endif
3141 
3142 
3143 
3144 
3145 /**Function********************************************************************
3146 
3147  Synopsis [Reports problem in garbage collection.]
3148 
3149  Description []
3150 
3151  SideEffects [None]
3152 
3153  SeeAlso [cuddGarbageCollect cuddGarbageCollectZdd]
3154 
3155 ******************************************************************************/
3156 static void
3157 ddReportRefMess(
3158  DdManager *unique /* manager */,
3159  int i /* table in which the problem occurred */,
3160  const char *caller /* procedure that detected the problem */)
3161 {
3162  if (i == CUDD_CONST_INDEX) {
3163  (void) fprintf(unique->err,
3164  "%s: problem in constants\n", caller);
3165  } else if (i != -1) {
3166  (void) fprintf(unique->err,
3167  "%s: problem in table %d\n", caller, i);
3168  }
3169  (void) fprintf(unique->err, " dead count != deleted\n");
3170  (void) fprintf(unique->err, " This problem is often due to a missing \
3171 call to Cudd_Ref\n or to an extra call to Cudd_RecursiveDeref.\n \
3172 See the CUDD Programmer's Guide for additional details.");
3173  abort();
3174 
3175 } /* end of ddReportRefMess */
3176 
3177 
3178 ABC_NAMESPACE_IMPL_END
3179 
ddReportRefMess
static void ddReportRefMess(DdManager *unique, int i, const char *caller)
Definition: cuddTable.c:3157
Cudd_IterDerefBdd
void Cudd_IterDerefBdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:217
DdNode::ref
DdHalfWord ref
Definition: cudd.h:280
DdManager::allocated
ABC_INT64_T allocated
Definition: cuddInt.h:382
Cudd_Prime
unsigned int Cudd_Prime(unsigned int p)
Definition: cuddTable.c:188
DD_MAXREF
#define DD_MAXREF
Definition: cuddInt.h:100
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
DdManager::groupcheck
Cudd_AggregationType groupcheck
Definition: cuddInt.h:426
DdSubtable::keys
unsigned int keys
Definition: cuddInt.h:330
cuddCacheFlush
void cuddCacheFlush(DdManager *table)
Definition: cuddCache.c:1047
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
DD_OOMFP
void(* DD_OOMFP)(long)
Definition: cudd.h:324
cuddZddInitUniv
int cuddZddInitUniv(DdManager *zdd)
Definition: cuddInit.c:252
ddHash
#define ddHash(f, g, s)
Definition: cuddInt.h:737
DdManager::reordTime
long reordTime
Definition: cuddInt.h:454
DdNode::Id
ABC_INT64_T Id
Definition: cudd.h:286
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
Cudd_OutOfMem
void Cudd_OutOfMem(long size)
Definition: cuddUtil.c:2837
DdManager::autoMethod
Cudd_ReorderingType autoMethod
Definition: cuddInt.h:418
cuddIZ
#define cuddIZ(dd, index)
Definition: cuddInt.h:704
DD_SIFT_MAX_VAR
#define DD_SIFT_MAX_VAR
Definition: cuddInt.h:147
DdManager::peakLiveNodes
unsigned int peakLiveNodes
Definition: cuddInt.h:465
DdManager::maxSizeZ
int maxSizeZ
Definition: cuddInt.h:364
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdCache::f
DdNode * f
Definition: cuddInt.h:317
DdManager::map
int * map
Definition: cuddInt.h:391
DdNode
Definition: cudd.h:278
ddPatchTree
static void ddPatchTree(DdManager *dd, MtrNode *treenode)
Definition: cuddTable.c:3080
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
DdManager::deadZ
unsigned int deadZ
Definition: cuddInt.h:372
MtrNode::size
MtrHalfWord size
Definition: mtr.h:134
DdCache::data
DdNode * data
Definition: cuddInt.h:319
DdManager::siftMaxSwap
int siftMaxSwap
Definition: cuddInt.h:412
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
DdManager::preReorderingHook
DdHook * preReorderingHook
Definition: cuddInt.h:439
DdManager::deadMask
unsigned deadMask
Definition: cuddInt.h:404
DdManager::invpermZ
int * invpermZ
Definition: cuddInt.h:389
DdManager::reordCycle
int reordCycle
Definition: cuddInt.h:415
hack::bits
unsigned int bits[2]
Definition: cuddTable.c:112
DdManager::size
int size
Definition: cuddInt.h:361
DdManager::gcFrac
double gcFrac
Definition: cuddInt.h:375
DdManager
struct DdManager DdManager
Definition: cudd.h:293
DdManager::maxCacheHard
unsigned int maxCacheHard
Definition: cuddInt.h:359
cuddUniqueConst
DdNode * cuddUniqueConst(DdManager *unique, CUDD_VALUE_TYPE value)
Definition: cuddTable.c:1450
DdManager::slots
unsigned int slots
Definition: cuddInt.h:368
DdCache::h
ptruint h
Definition: cuddInt.h:318
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddReclaim
void cuddReclaim(DdManager *table, DdNode *n)
Definition: cuddRef.c:584
DdManager::maxGrowthAlt
double maxGrowthAlt
Definition: cuddInt.h:414
pos
bool pos
Definition: globals.c:30
DdManager::realign
int realign
Definition: cuddInt.h:420
DdManager::maxGrowth
double maxGrowth
Definition: cuddInt.h:413
cuddShrinkSubtable
void cuddShrinkSubtable(DdManager *unique, int i)
Definition: cuddTable.c:1702
DdManager::err
FILE * err
Definition: cuddInt.h:442
DdCache::g
DdNode * g
Definition: cuddInt.h:317
DdManager::garbageCollections
int garbageCollections
Definition: cuddInt.h:452
DdManager::populationSize
int populationSize
Definition: cuddInt.h:430
Mtr_FreeTree
void Mtr_FreeTree(MtrNode *node)
Definition: mtrBasic.c:188
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DD_FIRST_REORDER
#define DD_FIRST_REORDER
Definition: cuddInt.h:151
DdManager::autoMethodZ
Cudd_ReorderingType autoMethodZ
Definition: cuddInt.h:419
DdSubtable::bindVar
int bindVar
Definition: cuddInt.h:334
DdManager::subtables
DdSubtable * subtables
Definition: cuddInt.h:365
DdManager::permZ
int * permZ
Definition: cuddInt.h:387
DdNodePtr
DdNode * DdNodePtr
Definition: cuddInt.h:268
DD_EPSILON
#define DD_EPSILON
Definition: cuddInt.h:109
DdManager::tree
MtrNode * tree
Definition: cuddInt.h:424
util_cpu_time
#define util_cpu_time
Definition: util_hack.h:36
DdSubtable
struct DdSubtable DdSubtable
DD_MAX_SUBTABLE_DENSITY
#define DD_MAX_SUBTABLE_DENSITY
Definition: cuddInt.h:126
DD_DEFAULT_RECOMB
#define DD_DEFAULT_RECOMB
Definition: cuddInt.h:149
DdHook::f
DD_HFP f
Definition: cuddInt.h:246
DdManager::deathRow
DdNode ** deathRow
Definition: cuddInt.h:401
DdManager::stack
DdNode ** stack
Definition: cuddInt.h:380
DD_UNUSED
static char rcsid[] DD_UNUSED
Definition: cuddTable.c:124
DdNode
struct DdNode DdNode
Definition: cudd.h:270
util_hack.h
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
ptruint
ABC_PTRUINT_T ptruint
Definition: cuddInt.h:261
DD_INLINE
#define DD_INLINE
Definition: cuddInt.h:90
DdManager::countDead
unsigned int countDead
Definition: cuddInt.h:423
MtrNode::younger
struct MtrNode * younger
Definition: mtr.h:139
DdManager::initSlots
unsigned int initSlots
Definition: cuddInt.h:379
DdSubtable::varType
Cudd_VariableType varType
Definition: cuddInt.h:336
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdManager::nextDyn
unsigned int nextDyn
Definition: cuddInt.h:422
DD_GC_FRAC_HI
#define DD_GC_FRAC_HI
Definition: cuddInt.h:134
DdManager::dead
unsigned int dead
Definition: cuddInt.h:371
cuddFreeTable
void cuddFreeTable(DdManager *unique)
Definition: cuddTable.c:659
cuddUniqueInterIVO
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1304
DdManager::cacheSlots
unsigned int cacheSlots
Definition: cuddInt.h:353
cuddZddProduct
DdNode * cuddZddProduct(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddZddFuncs.c:380
cuddDestroySubtables
int cuddDestroySubtables(DdManager *unique, int n)
Definition: cuddTable.c:2108
DdManager::maxLive
unsigned int maxLive
Definition: cuddInt.h:373
DdNode::value
CUDD_VALUE_TYPE value
Definition: cudd.h:283
DdManager::recomb
int recomb
Definition: cuddInt.h:427
DdManager::sentinel
DdNode sentinel
Definition: cuddInt.h:344
cuddResizeTableZdd
int cuddResizeTableZdd(DdManager *unique, int index)
Definition: cuddTable.c:2241
DdManager::stash
char * stash
Definition: cuddInt.h:399
MtrNode::index
MtrHalfWord index
Definition: mtr.h:135
DdManager::postReorderingHook
DdHook * postReorderingHook
Definition: cuddInt.h:440
DdManager::keys
unsigned int keys
Definition: cuddInt.h:369
cuddGarbageCollect
int cuddGarbageCollect(DdManager *unique, int clearCache)
Definition: cuddTable.c:729
DdSubtable::dead
unsigned int dead
Definition: cuddInt.h:332
one
static DdNode * one
Definition: cuddDecomp.c:112
DdManager::out
FILE * out
Definition: cuddInt.h:441
DD_SIFT_MAX_SWAPS
#define DD_SIFT_MAX_SWAPS
Definition: cuddInt.h:148
DdManager::realignZ
int realignZ
Definition: cuddInt.h:421
DdManager::cache
DdCache * cache
Definition: cuddInt.h:352
DdNode::next
DdNode * next
Definition: cudd.h:281
DD_GC_FRAC_LO
#define DD_GC_FRAC_LO
Definition: cuddInt.h:133
DdSubtable::varToBeGrouped
Cudd_LazyGroupType varToBeGrouped
Definition: cuddInt.h:339
cuddComputeFloorLog2
int cuddComputeFloorLog2(unsigned int value)
Definition: cuddCache.c:1079
DdManager::maxSize
int maxSize
Definition: cuddInt.h:363
ddAbs
#define ddAbs(x)
Definition: cuddInt.h:846
cuddFindParent
static int cuddFindParent(DdManager *table, DdNode *node)
Definition: cuddTable.c:2758
cuddZddFreeUniv
void cuddZddFreeUniv(DdManager *zdd)
Definition: cuddInit.c:301
cuddRehash
void cuddRehash(DdManager *unique, int i)
Definition: cuddTable.c:1530
DdSubtable::maxKeys
unsigned int maxKeys
Definition: cuddInt.h:331
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
DdManager::linear
long * linear
Definition: cuddInt.h:395
cuddInsertSubtables
int cuddInsertSubtables(DdManager *unique, int n, int level)
Definition: cuddTable.c:1795
DdManager::GCTime
long GCTime
Definition: cuddInt.h:453
DdManager::gcEnabled
int gcEnabled
Definition: cuddInt.h:376
ddMax
#define ddMax(x, y)
Definition: cuddInt.h:832
if
if(last==0)
Definition: sparse_int.h:34
DdManager::symmviolation
int symmviolation
Definition: cuddInt.h:428
abort
VOID_HACK abort()
DdManager::numberXovers
int numberXovers
Definition: cuddInt.h:431
CUDD_CONST_INDEX
#define CUDD_CONST_INDEX
Definition: cudd.h:117
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:327
ddResizeTable
static int ddResizeTable(DdManager *unique, int index)
Definition: cuddTable.c:2523
Cudd_DebugCheck
int Cudd_DebugCheck(DdManager *table)
Definition: cuddCheck.c:142
DdManager::linearSize
int linearSize
Definition: cuddInt.h:393
size
static int size
Definition: cuddSign.c:86
cuddF2L
#define cuddF2L(f)
Definition: cuddInt.h:718
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
MtrNode::low
MtrHalfWord low
Definition: mtr.h:133
DdManager::localCaches
DdLocalCache * localCaches
Definition: cuddInt.h:432
DdManager::reorderings
int reorderings
Definition: cuddInt.h:410
DD_MAX_CACHE_TO_SLOTS_RATIO
#define DD_MAX_CACHE_TO_SLOTS_RATIO
Definition: cuddInt.h:144
DdManager::cacheSlack
int cacheSlack
Definition: cuddInt.h:358
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
ddRehashZdd
static void ddRehashZdd(DdManager *unique, int i)
Definition: cuddTable.c:2422
hack::value
CUDD_VALUE_TYPE value
Definition: cuddTable.c:111
DdManager::nextDead
int nextDead
Definition: cuddInt.h:403
MtrNode
Definition: mtr.h:131
DdSubtable::varHandled
int varHandled
Definition: cuddInt.h:338
cuddLocalCacheClearDead
void cuddLocalCacheClearDead(DdManager *manager)
Definition: cuddLCache.c:352
cuddDeallocNode
#define cuddDeallocNode(unique, node)
Definition: cuddInt.h:547
DD_GC_FRAC_MIN
#define DD_GC_FRAC_MIN
Definition: cuddInt.h:135
cuddReclaimZdd
void cuddReclaimZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:638
Cudd_RemoveHook
int Cudd_RemoveHook(DdManager *dd, DD_HFP f, Cudd_HookType where)
Definition: cuddAPI.c:3306
ddEqualVal
#define ddEqualVal(x, y, e)
Definition: cuddInt.h:861
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
DdManager::memoryList
DdNode ** memoryList
Definition: cuddInt.h:397
cuddSlowTableGrowth
void cuddSlowTableGrowth(DdManager *unique)
Definition: cuddTable.c:2385
DdManager::memused
unsigned long memused
Definition: cuddInt.h:449
DdNode::type
union DdNode::@29 type
DdManager::siftMaxVar
int siftMaxVar
Definition: cuddInt.h:411
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
Cudd_zddReduceHeap
int Cudd_zddReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddZddReord.c:171
cuddZddUnion
DdNode * cuddZddUnion(DdManager *zdd, DdNode *P, DdNode *Q)
Definition: cuddZddSetop.c:553
CUDD_VALUE_TYPE
#define CUDD_VALUE_TYPE
Definition: cudd.h:94
DdManager::deathRowDepth
int deathRowDepth
Definition: cuddInt.h:402
DdManager::nextFree
DdNode * nextFree
Definition: cuddInt.h:398
DdHook::next
struct DdHook * next
Definition: cuddInt.h:247
DD_DEFAULT_RESIZE
#define DD_DEFAULT_RESIZE
Definition: cuddInt.h:102
cuddClearDeathRow
void cuddClearDeathRow(DdManager *table)
Definition: cuddRef.c:726
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
DdNode::index
DdHalfWord index
Definition: cudd.h:279
DdManager::looseUpTo
unsigned int looseUpTo
Definition: cuddInt.h:377
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
hack
ABC_NAMESPACE_IMPL_START union hack hack
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:329
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
DdManager::maxmemhard
unsigned long maxmemhard
Definition: cuddInt.h:451
DdManager::postGCHook
DdHook * postGCHook
Definition: cuddInt.h:438
DdSubtable::pairIndex
int pairIndex
Definition: cuddInt.h:337
Cudd_CheckKeys
int Cudd_CheckKeys(DdManager *table)
Definition: cuddCheck.c:458
DD_MAX_REORDER_GROWTH
#define DD_MAX_REORDER_GROWTH
Definition: cuddInt.h:150
cuddClean
#define cuddClean(p)
Definition: cuddInt.h:804
DdManager::epsilon
CUDD_VALUE_TYPE epsilon
Definition: cuddInt.h:407
DdManager::one
DdNode * one
Definition: cuddInt.h:345
CUDD_MAXINDEX
#define CUDD_MAXINDEX
Definition: cudd.h:112
DdManager::treeZ
MtrNode * treeZ
Definition: cuddInt.h:425
DdManager::autoDynZ
int autoDynZ
Definition: cuddInt.h:417
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
ddFixLimits
static DD_INLINE void ddFixLimits(DdManager *unique)
Definition: cuddTable.c:2805
cuddZddGetNodeIVO
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Definition: cuddTable.c:1074
value
int value
Definition: misc/espresso/main.h:90
DdManager::arcviolation
int arcviolation
Definition: cuddInt.h:429
assert
#define assert(ex)
Definition: util_old.h:213
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:367
DdManager::cachedeletions
double cachedeletions
Definition: cuddInt.h:460
result
static int result
Definition: cuddGenetic.c:125
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
DdManager::maxmem
unsigned long maxmem
Definition: cuddInt.h:450
cuddInitTable
DdManager * cuddInitTable(unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int looseUpTo)
Definition: cuddTable.c:351
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
DD_MEM_CHUNK
#define DD_MEM_CHUNK
Definition: cuddInt.h:104
cuddAdjust
#define cuddAdjust(x)
Definition: cuddInt.h:979
DdManager::autoDyn
int autoDyn
Definition: cuddInt.h:416
cuddUniqueInterZdd
DdNode * cuddUniqueInterZdd(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1343
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdSubtable::shift
int shift
Definition: cuddInt.h:328
DdManager::acache
DdCache * acache
Definition: cuddInt.h:351
cuddShrinkDeathRow
void cuddShrinkDeathRow(DdManager *table)
Definition: cuddRef.c:688
DdManager::keysZ
unsigned int keysZ
Definition: cuddInt.h:370
DdManager::preGCHook
DdHook * preGCHook
Definition: cuddInt.h:437
MtrNode::child
struct MtrNode * child
Definition: mtr.h:137
DdManager::perm
int * perm
Definition: cuddInt.h:386
cuddAllocNode
DdNode * cuddAllocNode(DdManager *unique)
Definition: cuddTable.c:235
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
zero
static DdNode * zero
Definition: cuddApa.c:100
DdManager::minDead
unsigned int minDead
Definition: cuddInt.h:374
cuddSatInc
#define cuddSatInc(x)
Definition: cuddInt.h:878
cuddCacheResize
void cuddCacheResize(DdManager *table)
Definition: cuddCache.c:925
DdManager::reclaimed
double reclaimed
Definition: cuddInt.h:384
DdManager::subtableZ
DdSubtable * subtableZ
Definition: cuddInt.h:366
MMoutOfMemory
#define MMoutOfMemory
Definition: util_hack.h:38
DdManager::univ
DdNode ** univ
Definition: cuddInt.h:392
DD_NON_CONSTANT
#define DD_NON_CONSTANT
Definition: cuddInt.h:123
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:633