source: vis_dev/glu-2.3/src/calBdd/calReorderBF.c @ 64

Last change on this file since 64 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 49.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calReorderBF.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for dynamic reordering of variables.]
8
9  Description [This method dynamically reorders variables while
10  preserving their locality. This entails both memory and
11  computational overheads.  Conceptually and experimentally it has
12  been observed that these overheads lead to poorer performance
13  compared to the traditional reordering methods. For details, please
14  refer to the work by Rajeev K. Ranjan et al - "Dynamic variable
15  reordering in a breadth-first manipulation based package: Challenges
16  and Solutions"- Proceedings of ICCD'97.]
17
18  SeeAlso     [calReorderDF.c calReorderUtil.c]
19
20  Author      [Rajeev K. Ranjan   (rajeev@ic.eecs.berkeley.edu)
21               Wilsin Gosti (wilsin@ic.eecs.berkeley.edu)]
22  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
23  All rights reserved.
24
25  Permission is hereby granted, without written agreement and without license
26  or royalty fees, to use, copy, modify, and distribute this software and its
27  documentation for any purpose, provided that the above copyright notice and
28  the following two paragraphs appear in all copies of this software.
29
30  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
31  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
32  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
33  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
34
35  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
36  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
37  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
38  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
39  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
40
41  Revision    [$Id: calReorderBF.c,v 1.3 2002/09/10 00:21:02 fabio Exp $]
42
43******************************************************************************/
44
45#include "calInt.h"
46
47/*---------------------------------------------------------------------------*/
48/* Constant declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Type declarations                                                         */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Stucture declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Variable declarations                                                     */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Macro declarations                                                        */
65/*---------------------------------------------------------------------------*/
66
67/**AutomaticStart*************************************************************/
68
69/*---------------------------------------------------------------------------*/
70/* Static function prototypes                                                */
71/*---------------------------------------------------------------------------*/
72
73static void BddReorderFixForwardingNodes(Cal_BddManager bddManager, Cal_BddId_t id);
74static void BddReorderFixAndFreeForwardingNodes(Cal_BddManager bddManager, Cal_BddId_t id, int numLevels);
75static void BddReorderSwapVarIndex(Cal_BddManager_t * bddManager, int varIndex, int forwardCheckFlag);
76static int CofactorFixAndReclaimForwardedNodes(Cal_BddManager_t *bddManager, int cofactorCheckStartIndex, int cofactorCheckEndIndex, int reclaimStartIndex, int reclaimEndIndex);
77static void BddReorderFreeNodes(Cal_BddManager_t * bddManager, int varId);
78#ifdef _CAL_VERBOSE
79static void PrintBddProfileAfterReorder(Cal_BddManager_t *bddManager);
80#endif
81static void BddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor);
82static int BddReorderSiftToBestPos(Cal_BddManager_t * bddManager, int varStartIndex, double maxSizeFactor);
83static void BddSiftPerfromPhaseIV(Cal_BddManager_t *bddManager, int varStartIndex, int bestIndex, int bottomMostSwapIndex);
84static void BddReorderVarWindow(Cal_BddManager bddManager, char *levels);
85static int BddReorderWindow2(Cal_BddManager bddManager, long index, int directionFlag);
86static int BddReorderWindow3(Cal_BddManager bddManager, long index, int directionFlag);
87
88/**AutomaticEnd***************************************************************/
89
90/*---------------------------------------------------------------------------*/
91/* Definition of exported functions                                          */
92/*---------------------------------------------------------------------------*/
93/*---------------------------------------------------------------------------*/
94/* Definition of internal functions                                          */
95/*---------------------------------------------------------------------------*/
96/**Function********************************************************************
97
98  Synopsis    [required]
99
100  Description [optional]
101
102  SideEffects [required]
103
104  SeeAlso     [optional]
105
106******************************************************************************/
107void
108CalBddReorderAuxBF(Cal_BddManager_t * bddManager)
109{
110  Cal_Assert(CalCheckAllValidity(bddManager));
111  CalInitInteract(bddManager);
112#ifdef _CAL_QUANTIFY_
113  quantify_start_recording_data();
114#endif
115  if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
116    char *levels = Cal_MemAlloc(char, bddManager->numVars);
117    BddReorderVarWindow(bddManager, levels);
118    Cal_MemFree(levels);
119  }
120  else {
121    BddReorderVarSift(bddManager, bddManager->maxSiftingGrowth);
122  }
123#ifdef _CAL_QUANTIFY_
124  quantify_stop_recording_data();
125#endif
126  Cal_Assert(CalCheckAllValidity(bddManager));
127  Cal_MemFree(bddManager->interact);
128  bddManager->numReorderings++;
129}
130
131/*---------------------------------------------------------------------------*/
132/* Definition of static functions                                          */
133/*---------------------------------------------------------------------------*/
134
135/**Function********************************************************************
136
137  Synopsis           [Fixes the forwarding nodes in a unique table.]
138
139  Description        [As opposed to CalBddReorderFixCofactors, which fixes
140  the cofactors of the non-forwarding nodes, this routine traverses
141  the list of forwarding nodes and removes the intermediate level of
142  forwarding. Number of levels should be 1 or 2.]
143
144  SideEffects        [required]
145
146  SeeAlso            [optional]
147
148******************************************************************************/
149static void
150BddReorderFixForwardingNodes(Cal_BddManager bddManager,
151                             Cal_BddId_t id) 
152{
153  CalHashTable_t *uniqueTableForId =
154      bddManager->uniqueTable[id];
155  CalBddNode_t *bddNode, *nextBddNode;
156  Cal_Bdd_t thenBdd;
157 
158  /* These are the forwarding nodes. */
159  CalBddNode_t *requestNodeList =
160      uniqueTableForId->startNode.nextBddNode;
161  for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
162    nextBddNode = CalBddNodeGetNextBddNode(bddNode);
163    CalBddNodeGetThenBdd(bddNode, thenBdd);
164    if (CalBddIsForwarded(thenBdd)) {
165      CalBddForward(thenBdd);
166      CalBddNodePutThenBdd(bddNode, thenBdd);
167    }
168    else {
169      /* there should not be anymore double forwarding */
170      break;
171    }
172    Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
173  }
174  /* Adjust the list */
175  uniqueTableForId->endNode->nextBddNode =
176      uniqueTableForId->startNode.nextBddNode;
177  uniqueTableForId->startNode.nextBddNode = bddNode;
178}
179
180/**Function********************************************************************
181
182  Synopsis           [Traverses the forwarding node lists of index,
183  index+1 .. up to index+level. Frees the intermediate forwarding nodes.]
184
185  Description        [optional]
186
187  SideEffects        [required]
188
189  SeeAlso            [optional]
190
191******************************************************************************/
192static void
193BddReorderFixAndFreeForwardingNodes(Cal_BddManager bddManager,
194                                    Cal_BddId_t id, int numLevels)
195{
196  CalHashTable_t *uniqueTableForId;
197  Cal_BddIndex_t index = bddManager->idToIndex[id];
198  CalBddNode_t *nextBddNode, *bddNode, *endNode;
199  Cal_Bdd_t thenBdd;
200  CalNodeManager_t *nodeManager;
201  int i;
202 
203  /* Fixing */
204  for (i=numLevels-1; i >= 0; i--){
205    uniqueTableForId =
206        bddManager->uniqueTable[bddManager->indexToId[index+i]];
207    for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
208         bddNode = nextBddNode){ 
209      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
210      CalBddNodeGetThenBdd(bddNode, thenBdd);
211      if (CalBddIsForwarded(thenBdd)){
212        do{
213          CalBddMark(thenBdd);
214          CalBddForward(thenBdd);
215        } while (CalBddIsForwarded(thenBdd));
216        CalBddNodePutThenBdd(bddNode, thenBdd); 
217      }
218      Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
219    }
220  }
221  /* Freeing */
222  for (i=numLevels-1; i >= 0; i--){
223    uniqueTableForId =
224        bddManager->uniqueTable[bddManager->indexToId[index+i]];
225    endNode = &(uniqueTableForId->startNode);
226    for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
227         bddNode = nextBddNode){ 
228      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
229      CalBddNodeGetThenBdd(bddNode, thenBdd);
230      if (CalBddIsMarked(thenBdd)){
231        do{
232          /* Free the node */
233          nodeManager = bddManager->nodeManagerArray[CalBddGetBddId(thenBdd)];
234          CalNodeManagerFreeNode(nodeManager, CalBddGetBddNode(thenBdd));
235          bddManager->numForwardedNodes--;
236        } while (CalBddIsMarked(thenBdd));
237      }
238      else{
239        endNode->nextBddNode = bddNode;
240        endNode = bddNode;
241      }
242    }
243    uniqueTableForId->endNode = endNode;
244  }
245}
246
247/**Function********************************************************************
248
249  Synopsis    [required]
250
251  Description [Traversesoptional]
252
253  SideEffects [required]
254
255  SeeAlso     [optional]
256
257******************************************************************************/
258static void
259BddReorderSwapVarIndex(Cal_BddManager_t * bddManager, int varIndex,
260                       int forwardCheckFlag)
261{
262  int thenVarIndex;
263  int elseVarIndex;
264  int varId;
265  int nextVarId;
266  int i;
267  int numBins;
268  int refCount;
269  int f0Found;
270  int f1Found;
271  CalHashTable_t *uniqueTableForId;
272  CalHashTable_t *nextUniqueTableForId;
273  CalBddNode_t **bins;
274  CalBddNode_t *bddNode, *startNode;
275  CalBddNode_t *nextBddNode, *processingNodeList;
276  CalBddNode_t *prevBddNode = Cal_Nil(CalBddNode_t);
277  Cal_Bdd_t newF;
278  Cal_Bdd_t f0;
279  Cal_Bdd_t f1;
280  Cal_Bdd_t newF0;
281  Cal_Bdd_t newF1;
282  Cal_Bdd_t f00;
283  Cal_Bdd_t f01;
284  Cal_Bdd_t f10;
285  Cal_Bdd_t f11;
286  CalAssociation_t *assoc;
287 
288  varId = bddManager->indexToId[varIndex];
289  nextVarId = bddManager->indexToId[varIndex + 1];
290 
291  if (CalTestInteract(bddManager, varId, nextVarId)){
292  bddManager->numSwaps++;
293#ifdef _CAL_VERBOSE
294  /*fprintf(stdout," %3d(%3d) going down,  %3d(%3d) going up\n",
295          varId, varIndex, nextVarId, varIndex+1);*/
296#endif
297  uniqueTableForId = bddManager->uniqueTable[varId];
298  nextUniqueTableForId = bddManager->uniqueTable[nextVarId];
299 
300  /*uniqueTableForId->requestNodeList = Cal_Nil(CalBddNode_t);*/
301  processingNodeList = Cal_Nil(CalBddNode_t);
302  numBins = uniqueTableForId->numBins;
303  bins = uniqueTableForId->bins;
304  if (forwardCheckFlag){
305    for(i = 0; i < numBins; ++i) {
306      prevBddNode = Cal_Nil(CalBddNode_t);
307      for(bddNode = bins[i];
308          bddNode != Cal_Nil(CalBddNode_t);
309          bddNode = nextBddNode) {
310        /*
311         * Process one bddNode at a time
312         */
313        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
314        /* The node should not be forwarded */
315        Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
316        /*
317        ** We don't know for sure if the reference count of the node
318        ** could be 0. Let us use the assertion at this point.
319        */
320        Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
321        /*
322        ** If ever the above assetion fails, or if we can convince
323        ** ourselves that the reference count could be zero, we need
324        ** to uncomment the following code.
325        */
326        /*
327        if (CalBddNodeIsRefCountZero(bddNode)){
328          thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
329          elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
330          CalBddNodeDcrRefCount(thenBddNode);
331          CalBddNodeDcrRefCount(elseBddNode);
332          if (prevBddNode){
333            CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
334          }
335          else{
336            bins[i] = nextBddNode;
337          }
338          uniqueTableForId->numEntries--;
339          bddManager->numNodes--;
340          bddManager->numNodesFreed++;
341          CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
342          continue;
343        }
344        */
345        CalBddNodeGetElseBdd(bddNode, f0);
346        CalBddNodeGetThenBdd(bddNode, f1);
347       
348        if (CalBddIsForwarded(f1)) {
349          CalBddForward(f1);
350          CalBddNodePutThenBdd(bddNode, f1);
351        }
352        Cal_Assert(CalBddIsForwarded(f1) == 0);
353       
354        if (CalBddIsForwarded(f0)) {
355          CalBddForward(f0);
356          CalBddNodePutElseBdd(bddNode, f0); 
357        }
358        Cal_Assert(CalBddIsForwarded(f0) == 0);
359        /*
360        ** Get the index of f0 and f1 and create newF0 and newF1 if necessary
361        */
362        elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
363        thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
364       
365        if ((elseVarIndex > (varIndex + 1))
366            && (thenVarIndex > (varIndex + 1))) { 
367          prevBddNode = bddNode;
368          Cal_Assert(CalDoHash2(CalBddGetBddNode(f1),
369                                CalBddGetBddNode(f0), 
370                                uniqueTableForId) == i);
371          continue;
372        }
373 
374        /* This node is going to be forwared */
375        CalBddNodePutNextBddNode(bddNode, processingNodeList);
376        processingNodeList = bddNode;
377       
378        /* Update the unique table appropriately */
379        if (prevBddNode){
380          CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
381        }
382        else{
383          bins[i] = nextBddNode;
384        } 
385        uniqueTableForId->numEntries--;
386        bddManager->numNodes--;
387      }
388    }
389  }
390  else{
391    for(i = 0; i < numBins; i++) {
392      prevBddNode = Cal_Nil(CalBddNode_t);
393      for(bddNode = bins[i];
394          bddNode != Cal_Nil(CalBddNode_t);
395          bddNode = nextBddNode) {
396        /*
397         * Process one bddNode at a time
398         */
399        nextBddNode = CalBddNodeGetNextBddNode(bddNode);
400        /* The node should not be forwarded */
401        Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
402
403        /*
404        ** We don't know for sure if the reference count of the node
405        ** could be 0. Let us use the assertion at this point.
406        */
407        Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
408        /*
409        ** If ever the above assetion fails, or if we can convince
410        ** ourselves that the reference count could be zero, we need
411        ** to uncomment the following code.
412        */
413        /*
414        if (CalBddNodeIsRefCountZero(bddNode)){
415          thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
416          elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
417          CalBddNodeDcrRefCount(thenBddNode);
418          CalBddNodeDcrRefCount(elseBddNode);
419          if (prevBddNode){
420            CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
421          }
422          else{
423            bins[i] = nextBddNode;
424          }
425          uniqueTableForId->numEntries--;
426          bddManager->numNodes--;
427          bddManager->numNodesFreed++;
428          CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
429          continue;
430        }
431        */
432        CalBddNodeGetThenBdd(bddNode, f1);
433        Cal_Assert(CalBddIsForwarded(f1) == 0);
434        CalBddNodeGetElseBdd(bddNode, f0);
435        Cal_Assert(CalBddIsForwarded(f0) == 0);
436        /*
437        ** Get the index of f0 and f1 and create newF0 and newF1 if necessary
438        */
439
440        elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
441        thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
442       
443        if ((elseVarIndex > (varIndex + 1))
444            && (thenVarIndex > (varIndex + 1))) { 
445          prevBddNode = bddNode;
446          continue;
447        }
448 
449        /* This node is going to be forwared */
450        CalBddNodePutNextBddNode(bddNode, processingNodeList);
451        processingNodeList = bddNode;
452       
453        /* Update the unique table appropriately */
454        if (prevBddNode){
455          CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
456        }
457        else{
458          bins[i] = nextBddNode;
459        } 
460        uniqueTableForId->numEntries--;
461        bddManager->numNodes--;
462      }
463    }
464  }
465  bddNode = processingNodeList;
466  /*endNode = uniqueTableForId->endNode;*/
467  startNode = uniqueTableForId->startNode.nextBddNode;
468  while (bddNode != Cal_Nil(CalBddNode_t)) {
469    nextBddNode = CalBddNodeGetNextBddNode(bddNode);
470
471    /*
472     * Get the index of f0 and f1 and create newF0 and newF1 if necessary
473     */
474
475    CalBddNodeGetElseBdd(bddNode, f0);
476    CalBddNodeGetThenBdd(bddNode, f1);
477    elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
478    thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
479
480    if (elseVarIndex > (varIndex + 1)) {
481      f00 = f0;
482      f01 = f0;
483      CalBddGetElseBdd(f1, f10);
484      CalBddGetThenBdd(f1, f11);
485    } else if (thenVarIndex > (varIndex + 1)) {
486      f10 = f1;
487      f11 = f1;
488      CalBddGetElseBdd(f0, f00);
489      CalBddGetThenBdd(f0, f01);
490    }else{
491      CalBddGetElseBdd(f1, f10);
492      CalBddGetThenBdd(f1, f11);
493      CalBddGetElseBdd(f0, f00);
494      CalBddGetThenBdd(f0, f01);
495    }
496    Cal_Assert(CalBddIsForwarded(f10) == 0);
497    Cal_Assert(CalBddIsForwarded(f11) == 0);
498    Cal_Assert(CalBddIsForwarded(f00) == 0);
499    Cal_Assert(CalBddIsForwarded(f01) == 0);
500
501    if (CalBddIsEqual(f10,f00)) {
502      newF0 = f00;
503      f0Found = 1;
504    }
505    else {
506      f0Found = CalUniqueTableForIdFindOrAdd(bddManager, uniqueTableForId, f10,
507                                             f00, &newF0);
508    }
509    CalBddIcrRefCount(newF0);
510    if (CalBddIsEqual(f11, f01)) {
511      newF1 = f01;
512      f1Found = 1;
513    }
514    else {
515      f1Found = CalUniqueTableForIdFindOrAdd(bddManager, uniqueTableForId, f11,
516                                             f01, &newF1);
517    }
518    CalBddIcrRefCount(newF1);
519
520    if (!f0Found){
521      CalBddIcrRefCount(f10);
522      CalBddIcrRefCount(f00);
523    }
524
525    if (!f1Found){
526      CalBddIcrRefCount(f11);
527      CalBddIcrRefCount(f01);
528    }
529
530    CalBddDcrRefCount(f0);
531    CalBddDcrRefCount(f1);
532    /*
533     * Create the new node for f. It cannot exist before, since at
534     * least one of newF0 and newF1 must be dependent on currentIndex.
535     * Otherwise, f00 == f10 and f01 == f11 (redundant nodes).
536     */
537    CalHashTableAddDirectAux(nextUniqueTableForId, newF1, newF0, &newF);
538    bddManager->numNodes++;
539    CalBddNodePutThenBdd(bddNode, newF);
540    CalBddNodePutElseBddNode(bddNode, FORWARD_FLAG);
541    bddManager->numForwardedNodes++;
542    CalBddNodeGetRefCount(bddNode, refCount);
543    CalBddAddRefCount(newF, refCount);
544    Cal_Assert(!CalBddIsRefCountZero(newF));
545    /* Put it in the forwarded list of the unique table */
546    /*
547    endNode->nextBddNode = bddNode;
548    endNode = bddNode;
549    */
550    bddNode->nextBddNode = startNode;
551    startNode = bddNode;
552   
553    bddNode = nextBddNode;
554  }
555  /*uniqueTableForId->endNode = endNode;*/
556  uniqueTableForId->startNode.nextBddNode = startNode;
557
558  BddReorderFreeNodes(bddManager, nextVarId);
559 
560  }
561  else{
562    bddManager->numTrivialSwaps++;
563  }
564 
565  CalFixupAssoc(bddManager, varId, nextVarId, bddManager->tempAssociation);
566  for(assoc = bddManager->associationList; assoc; assoc = assoc->next){
567    CalFixupAssoc(bddManager, varId, nextVarId, assoc);
568  }
569
570  bddManager->idToIndex[varId] = varIndex + 1;
571  bddManager->idToIndex[nextVarId] = varIndex;
572  bddManager->indexToId[varIndex] = nextVarId;
573  bddManager->indexToId[varIndex + 1] = varId;
574
575  Cal_Assert(CalCheckAssoc(bddManager));
576
577#ifdef _CAL_VERBOSE
578  /*fprintf(stdout,"Variable order after swap:\n");*/
579  for (i=0; i<bddManager->numVars; i++){
580    fprintf(stdout, "%3d ", bddManager->indexToId[i]);
581  }
582  fprintf(stdout, "%8d\n", bddManager->numNodes);
583#endif
584}
585
586/**Function********************************************************************
587
588  Synopsis           [required]
589
590  Description        [optional]
591
592  SideEffects        [required]
593
594  SeeAlso            [optional]
595
596******************************************************************************/
597static int
598CofactorFixAndReclaimForwardedNodes(Cal_BddManager_t *bddManager, int
599                                       cofactorCheckStartIndex, int
600                                       cofactorCheckEndIndex, int
601                                       reclaimStartIndex, int reclaimEndIndex)
602{
603  int index, varId;
604  /* Clean up : Need to fix the cofactors of userBDDs and the
605     indices above the varStartIndex only. */
606  if (bddManager->pipelineState == CREATE){
607    /* There are some results computed in pipeline */
608    CalBddReorderFixProvisionalNodes(bddManager);
609  }
610  CalBddReorderFixUserBddPtrs(bddManager);
611  CalReorderAssociationFix(bddManager);
612  for (index = cofactorCheckStartIndex;
613       index <= cofactorCheckEndIndex; index++){ 
614    varId = bddManager->indexToId[index];
615    CalBddReorderFixCofactors(bddManager, varId);
616  }
617  CalBddReorderReclaimForwardedNodes(bddManager, reclaimStartIndex,
618                                     reclaimEndIndex);
619  Cal_Assert(CalCheckAllValidity(bddManager));
620  return 0;
621}
622
623/**Function********************************************************************
624
625  Synopsis    [required]
626
627  Description [optional]
628
629  SideEffects [required]
630
631  SeeAlso     [optional]
632
633******************************************************************************/
634static void
635BddReorderFreeNodes(Cal_BddManager_t * bddManager, int varId)
636{
637  CalBddNode_t *prevNode, *bddNode, *nextBddNode;
638  CalBddNode_t *elseBddNode;
639  CalBddNode_t *thenBddNode;
640  CalHashTable_t *uniqueTableForId;
641  CalBddNode_t **bins;
642  int numBins;
643  int i;
644  long oldNumEntries, numNodesFreed;
645
646  uniqueTableForId = bddManager->uniqueTable[varId];
647  bins = uniqueTableForId->bins;
648  numBins = uniqueTableForId->numBins;
649  oldNumEntries = uniqueTableForId->numEntries;
650
651  if (bddManager->numPeakNodes < (bddManager->numNodes +
652                                  bddManager->numForwardedNodes)){
653    bddManager->numPeakNodes = bddManager->numNodes +
654        bddManager->numForwardedNodes ;
655  }
656 
657  for(i = 0; i < numBins; i++){
658    prevNode = NULL;
659    bddNode = bins[i];
660    while(bddNode != Cal_Nil(CalBddNode_t)){
661      nextBddNode = CalBddNodeGetNextBddNode(bddNode);
662      Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
663      if(CalBddNodeIsRefCountZero(bddNode)){
664        thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
665        elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
666        Cal_Assert(CalBddNodeIsForwarded(thenBddNode) == 0);
667        Cal_Assert(CalBddNodeIsForwarded(elseBddNode) == 0);
668        CalBddNodeDcrRefCount(thenBddNode);
669        CalBddNodeDcrRefCount(elseBddNode);
670        if (prevNode == NULL) {
671          bins[i] = nextBddNode;
672        } else {
673          CalBddNodePutNextBddNode(prevNode, nextBddNode);
674        }
675        CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
676        uniqueTableForId->numEntries--;
677      } else {
678        prevNode = bddNode;
679      }
680      bddNode = nextBddNode;
681    }
682  }
683  numNodesFreed = oldNumEntries - uniqueTableForId->numEntries;
684  bddManager->numNodes -= numNodesFreed;
685  bddManager->numNodesFreed += numNodesFreed;
686}
687
688#ifdef _CAL_VERBOSE
689
690/**Function********************************************************************
691
692  Synopsis           [required]
693
694  Description        [optional]
695
696  SideEffects        [required]
697
698  SeeAlso            [optional]
699
700******************************************************************************/
701static void
702PrintBddProfileAfterReorder(Cal_BddManager_t *bddManager)
703{
704    int i, index, numBins, j;
705    CalHashTable_t *uniqueTableForId;
706    CalBddNode_t *bddNode, *nextBddNode;
707    char *levels = Cal_MemAlloc(char, bddManager->numVars+1);
708    CalBddNode_t *requestNodeList;
709    Cal_Bdd_t thenBdd, elseBdd;
710   
711  /* Now traverse all the nodes in order */
712    for (index = 0; index < bddManager->numVars; index++){
713      fprintf(stdout,"**** %3d ****\n", bddManager->indexToId[index]); 
714      uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
715      numBins = uniqueTableForId->numBins;
716      for (i=1; i<=bddManager->numVars; i++) {
717          levels[i] = 0;
718      }
719      j = 0;
720      for (i = 0; i < numBins; i++){
721          for (bddNode = uniqueTableForId->bins[i]; bddNode;
722               bddNode = nextBddNode){
723              nextBddNode = CalBddNodeGetNextBddNode(bddNode);
724              CalBddNodeGetThenBdd(bddNode, thenBdd);
725              CalBddNodeGetElseBdd(bddNode, elseBdd);
726              if (CalBddIsForwarded(thenBdd) ||
727                  CalBddIsForwarded(elseBdd)){                       
728                j++;
729              }
730              if (CalBddIsForwarded(thenBdd)) {                     
731                  levels[CalBddGetThenBddId(thenBdd)]++;
732              }
733              if (CalBddIsForwarded(elseBdd)) {                     
734                  levels[CalBddGetThenBddId(elseBdd)]++;
735              }
736          }
737      }
738      fprintf(stdout,"\tCofactors (%3d): ", j);
739      for (i=1; i<=bddManager->numVars; i++){
740          if (levels[i]) {
741              fprintf(stdout,"%3d->%3d ", i, levels[i]);
742          }
743      }
744      fprintf(stdout,"\n");
745      for (i=1; i<=bddManager->numVars; i++) {
746          levels[i] = 0;
747      }
748      j = 0;
749      requestNodeList = uniqueTableForId->startNode.nextBddNode;
750      for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
751          Cal_Assert(CalBddNodeIsForwarded(bddNode));
752          nextBddNode = CalBddNodeGetNextBddNode(bddNode);
753          CalBddNodeGetThenBdd(bddNode, thenBdd);
754          Cal_Assert(!CalBddIsForwarded(thenBdd));
755          levels[CalBddGetBddId(thenBdd)]++;
756          j++;
757      }
758      fprintf(stdout,"\tForwarded nodes (%3d): ", j);
759      for (i=1; i<=bddManager->numVars; i++){
760          if (levels[i]) {
761              fprintf(stdout,"%3d->%3d ", i, levels[i]);
762          }
763      }
764      fprintf(stdout,"\n");
765    }
766    Cal_MemFree(levels);
767}
768#endif
769
770/**Function********************************************************************
771
772  Synopsis    [Reorder variables using "sift" algorithm.]
773
774  Description [Reorder variables using "sift" algorithm.]
775
776  SideEffects [None]
777
778******************************************************************************/
779static void
780BddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor)
781{
782  int i,j;
783  int mostNodesId = -1;
784  long mostNodes, varNodes;
785  int *idArray;
786  long numVarsShifted = 0;
787  bddManager->numSwaps = 0;
788 
789  idArray = Cal_MemAlloc(int, bddManager->numVars);
790  for (i = 0; i < bddManager->numVars; i++) {
791    idArray[i] = bddManager->indexToId[i];
792  }
793
794  while (i &&
795         (numVarsShifted <=
796          bddManager->maxNumVarsSiftedPerReordering) &&
797         (bddManager->numSwaps <=
798          bddManager->maxNumSwapsPerReordering)){ 
799    i--;
800    numVarsShifted++;
801/*
802 * Find var with the most number of nodes and do sifting on it.
803 * idArray is used to make sure that a var is not sifted more than
804 * once.
805 */
806    mostNodes = 0;
807    for (j = 0; j <= i; j++){
808      varNodes = bddManager->uniqueTable[idArray[j]]->numEntries;
809      if (varNodes > mostNodes) {
810        mostNodes = varNodes;
811        mostNodesId = j;
812      }
813    }
814 
815    if (mostNodes <= 1) { /* I can put a different stopping criterion */
816      /*
817       * Most number of nodes among the vars not sifted yet is 0. Stop.
818       */
819      break;
820    }
821
822    BddReorderSiftToBestPos(bddManager,
823                            bddManager->idToIndex[idArray[mostNodesId]],
824                            maxSizeFactor); 
825    Cal_Assert(CalCheckAllValidity(bddManager));
826    idArray[mostNodesId] = idArray[i];
827  }
828
829  Cal_MemFree(idArray);
830}
831
832
833/**Function********************************************************************
834
835  Synopsis    [required]
836
837  Description [optional]
838
839  SideEffects [required]
840
841  SeeAlso     [optional]
842
843******************************************************************************/
844static int
845BddReorderSiftToBestPos(Cal_BddManager_t * bddManager, int
846                        varStartIndex, double maxSizeFactor)
847{
848  long curSize;
849  long bestSize;
850  int bestIndex;
851  int varCurIndex;
852  int varId, i;
853  int lastIndex = bddManager->numVars - 1;
854  int numVars = bddManager->numVars;
855  long startSize = bddManager->numNodes;
856  long maxSize =  startSize * maxSizeFactor;
857  int origId = bddManager->indexToId[varStartIndex];
858
859  int topMostSwapIndex = 0; /* the variable has been swapped upto this
860                               index */
861  int bottomMostSwapIndex = lastIndex; /* the variable has been
862                                          swapped upto this index */
863
864  int swapFlag = 0; /* If a swap has taken place after last cleaning
865                       up */
866                       
867 
868  curSize = bestSize = bddManager->numNodes;
869  bestIndex = varStartIndex;
870
871#ifdef _CAL_VERBOSE
872  for (i=0; i<bddManager->numVars; i++){
873    fprintf(stdout, "%3d ", bddManager->indexToId[i]);
874  }
875  fprintf(stdout, "%8d\n", bddManager->numNodes);
876#endif
877 
878  /*
879  ** If varStartIndex > numVars/2, do: Down, Up, Down.
880  ** If varStartIndex < numVars/2, do: Up, Down, Up
881  ** Followed by a cleanup phase in either case.
882  */
883 
884  if (varStartIndex >= (numVars >> 1)){
885    /* Phase I: Downward swap, no forwarding check. */
886    varCurIndex = varStartIndex;
887    while (varCurIndex < lastIndex) {
888      BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
889      swapFlag = 1;
890      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
891        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
892                                               varCurIndex-1,
893                                               varCurIndex+1,
894                                               varCurIndex+1); 
895        swapFlag = 0;
896      }
897      varCurIndex++;
898      curSize = bddManager->numNodes;
899      /*if (curSize > maxSize){*/
900      if (curSize >= (bestSize << 1)){
901        bottomMostSwapIndex = varCurIndex;
902        break;
903      }
904      if (curSize < bestSize) {
905        bestSize = curSize;
906        bestIndex = varCurIndex;
907      }
908    }
909   
910    /* Phase II : Two parts */
911    /*
912    ** Part One: Upward swap until varStartIndex. Fix cofactors and
913    ** fix double pointers.
914    */
915   
916    while (varCurIndex > varStartIndex) {
917      varCurIndex--;
918      BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
919      swapFlag = 1;
920      varId = bddManager->indexToId[varCurIndex];
921      BddReorderFixForwardingNodes(bddManager, varId);
922      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
923        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
924                                               varCurIndex-1,
925                                               varCurIndex,
926                                               bottomMostSwapIndex); 
927        swapFlag = 0;
928      }
929    }
930    curSize = startSize;
931   
932    /*
933    ** Part two: Upward swap all the way to the top. Fix cofactors.
934    */
935    while (varCurIndex > 0) {
936      varCurIndex--;
937      BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
938      swapFlag = 1;
939      curSize = bddManager->numNodes;
940      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
941        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
942                                               varCurIndex-1,
943                                               varCurIndex,
944                                               bottomMostSwapIndex); 
945        swapFlag = 0;
946      }
947      if (curSize > maxSize){
948        topMostSwapIndex = varCurIndex;
949        break;
950      }
951      if (curSize <= bestSize) {
952        bestSize = curSize;
953        bestIndex = varCurIndex;
954      }
955    }
956
957    if (swapFlag){
958      /* Fix user BDD pointers and reclaim forwarding nodes */
959      if (bddManager->pipelineState == CREATE){
960        /* There are some results computed in pipeline */
961        CalBddReorderFixProvisionalNodes(bddManager);
962      }
963      CalBddReorderFixUserBddPtrs(bddManager);
964      CalReorderAssociationFix(bddManager);
965     
966      /* The upward swapping might have stopped short */
967      for (i = 0; i < topMostSwapIndex; i++){
968        varId = bddManager->indexToId[i];
969        CalBddReorderFixCofactors(bddManager, varId);
970      }
971     
972      CalBddReorderReclaimForwardedNodes(bddManager, topMostSwapIndex,
973                                         bottomMostSwapIndex);
974      swapFlag = 0;
975    }
976   
977    Cal_Assert(CalCheckAllValidity(bddManager));
978   
979    /* Phase III : Swap to the min position */
980
981    while (varCurIndex < bestIndex) {
982      BddReorderSwapVarIndex(bddManager, varCurIndex, 0); 
983      swapFlag = 1;
984      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
985        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
986                                               varCurIndex-1,
987                                               varCurIndex+1,
988                                               varCurIndex+1); 
989        swapFlag = 0;
990      }
991      varCurIndex++;
992    }
993  }
994  else{
995    /* Phase I: Upward swap, fix cofactors. */
996    varCurIndex = varStartIndex;
997    while (varCurIndex > 0) {
998      varCurIndex--;
999      BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
1000      swapFlag = 1;
1001      curSize = bddManager->numNodes;
1002      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
1003        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
1004                                               varCurIndex-1,
1005                                               varCurIndex+1,
1006                                               varStartIndex); 
1007        swapFlag = 0;
1008      }
1009      if (curSize > maxSize){
1010        topMostSwapIndex = varCurIndex;
1011        break;
1012      }
1013      if (curSize < bestSize) {
1014        bestSize = curSize;
1015        bestIndex = varCurIndex;
1016      }
1017    }
1018   
1019    if (swapFlag){
1020      /* Fix user BDD pointers and reclaim forwarding nodes */
1021      if (bddManager->pipelineState == CREATE){
1022        /* There are some results computed in pipeline */
1023        CalBddReorderFixProvisionalNodes(bddManager);
1024      }
1025      CalBddReorderFixUserBddPtrs(bddManager);
1026      CalReorderAssociationFix(bddManager);
1027      /* The upward swapping might have stopped short */
1028      for (i = 0; i < topMostSwapIndex; i++){
1029        varId = bddManager->indexToId[i];
1030        CalBddReorderFixCofactors(bddManager, varId);
1031      }
1032      CalBddReorderReclaimForwardedNodes(bddManager, topMostSwapIndex,
1033                                         varStartIndex);
1034      swapFlag = 0;
1035    }
1036   
1037    Cal_Assert(CalCheckAllValidity(bddManager));
1038
1039    /* Phase II : Move all the way down : two parts */
1040
1041    /* Swap it to the original position, no cofactor fixing, fix
1042       double pointers of the variable moving up.*/
1043    while (varCurIndex < varStartIndex){
1044      BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
1045      swapFlag = 1;
1046      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
1047        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
1048                                               varCurIndex-1,
1049                                               varCurIndex+1,
1050                                               varCurIndex+1); 
1051        swapFlag = 0;
1052      }
1053      varCurIndex++;
1054    }
1055    /* Swap to the bottom */
1056    while (varCurIndex < lastIndex){
1057      BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
1058      swapFlag = 1;
1059      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
1060        CofactorFixAndReclaimForwardedNodes(bddManager, 0,
1061                                               varCurIndex-1,
1062                                               varCurIndex+1,
1063                                               varCurIndex+1); 
1064        swapFlag = 0;
1065      }
1066      varCurIndex++;
1067      curSize = bddManager->numNodes;
1068      /* if (curSize > maxSize){ */
1069      if (curSize >= (bestSize << 1)){
1070        bottomMostSwapIndex = varCurIndex;
1071        break;
1072      }
1073      if (curSize <= bestSize) {
1074        bestSize = curSize;
1075        bestIndex = varCurIndex;
1076      }
1077    }
1078
1079    /* Phase III : Move up to the best position */
1080    while (varCurIndex > bestIndex){
1081      varCurIndex--;
1082      BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
1083      swapFlag = 1;
1084      varId = bddManager->indexToId[varCurIndex];
1085      BddReorderFixForwardingNodes(bddManager, varId);
1086      if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
1087        CofactorFixAndReclaimForwardedNodes(bddManager, 0, varCurIndex-1,
1088                                               varCurIndex,
1089                                               bottomMostSwapIndex); 
1090        swapFlag = 0;
1091      }
1092    }
1093  } /* End of else clause (varStartIndex < numVars/2) */
1094
1095#ifdef _CAL_VERBOSE
1096  PrintBddProfileAfterReorder(bddManager);
1097#endif
1098 
1099  if (CalBddIdNeedsRepacking(bddManager, origId)){
1100    if (swapFlag){
1101      if (varStartIndex >= (numVars >> 1)){
1102        CalBddPackNodesAfterReorderForSingleId(bddManager, 0,
1103                                               bestIndex, bestIndex); 
1104      }
1105      /*
1106      else if (bestIndex >= (numVars >> 1)){
1107        int i;
1108        int nodeCounter = 0;
1109        for (i=bestIndex; i<numVars; i++){
1110          nodeCounter +=
1111              bddManager->uniqueTable[bddManager->indexToId[i]]->numEntries;
1112        }
1113        if ((bddManager->numNodes - nodeCounter) >
1114            bddManager->numForwardedNodes){
1115            BddPackNodesAfterReorderForSingleId(bddManager, 1, bestIndex,
1116                                                 bottomMostSwapIndex);
1117        }
1118        else {
1119          BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
1120                                bottomMostSwapIndex);
1121          BddPackNodesAfterReorderForSingleId(bddManager, 0,
1122                                                 bestIndex, bestIndex);
1123        }
1124      }
1125      */
1126      else {
1127        /* Clean up - phase IV */
1128        BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
1129                              bottomMostSwapIndex);
1130        CalBddPackNodesAfterReorderForSingleId(bddManager, 0,
1131                                               bestIndex, bestIndex); 
1132      }
1133    }
1134    else {
1135      CalBddPackNodesAfterReorderForSingleId(bddManager, 0, bestIndex,
1136                                             bestIndex); 
1137    }
1138  }
1139  else if (swapFlag) {
1140    /* clean up - phase IV */
1141    BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
1142                          bottomMostSwapIndex);
1143  }
1144  Cal_Assert(CalCheckAllValidity(bddManager));
1145 
1146#ifdef _CAL_VERBOSE
1147  printf("ID = %3d SI = %3d EI = %3d Nodes = %7d\n", origId,
1148         varStartIndex, bestIndex, bddManager->numNodes);
1149#endif
1150  return bestIndex;
1151}
1152
1153 
1154/**Function********************************************************************
1155
1156  Synopsis    [required]
1157
1158  Description [optional]
1159
1160  SideEffects [required]
1161
1162  SeeAlso     [optional]
1163
1164******************************************************************************/
1165static void
1166BddSiftPerfromPhaseIV(Cal_BddManager_t *bddManager, int varStartIndex,
1167                      int bestIndex, int bottomMostSwapIndex)
1168{
1169  int varCurIndex, varId;
1170 
1171
1172/* We need to perform phase IV */
1173  varCurIndex = bestIndex-1;
1174  while (varCurIndex >= 0) {
1175    varId = bddManager->indexToId[varCurIndex];
1176    CalBddReorderFixCofactors(bddManager, varId);
1177    varCurIndex--;
1178  }
1179  if (bddManager->pipelineState == CREATE){
1180    /* There are some results computed in pipeline */
1181    CalBddReorderFixProvisionalNodes(bddManager);
1182  }
1183  CalBddReorderFixUserBddPtrs(bddManager);
1184  CalReorderAssociationFix(bddManager);
1185  if (varStartIndex >= (bddManager->numVars >> 1)){
1186    CalBddReorderReclaimForwardedNodes(bddManager, bestIndex, bestIndex);
1187  }
1188  else {
1189    CalBddReorderReclaimForwardedNodes(bddManager, bestIndex,
1190                                       bottomMostSwapIndex); 
1191  }
1192}
1193
1194
1195/**Function********************************************************************
1196
1197  Synopsis           [required]
1198
1199  Description        [optional]
1200
1201  SideEffects        [required]
1202
1203  SeeAlso            [optional]
1204
1205******************************************************************************/
1206static void
1207BddReorderVarWindow(Cal_BddManager bddManager, char *levels)
1208{
1209  long i;
1210  int moved;
1211  int anySwapped;
1212  int even;
1213  int lastIndex = bddManager->numVars-1;
1214 
1215#ifdef _CAL_VERBOSE
1216  for (i=0; i<bddManager->numVars; i++){
1217    fprintf(stdout, "%3d ", bddManager->indexToId[i]);
1218  }
1219  fprintf(stdout, "%8d\n", bddManager->numNodes);
1220#endif
1221  for (i=0; i < bddManager->numVars-1; i++) levels[i]=1;
1222  even = 1;
1223  do {
1224    anySwapped=0;
1225    if (even){
1226      /*fprintf(stdout, "Downward Swap\n");*/
1227      for (i=0; i < bddManager->numVars-1; i++){
1228        if (levels[i]) {
1229          if (i < bddManager->numVars-2) {
1230            moved = BddReorderWindow3(bddManager, i, 0);
1231            if (bddManager->numForwardedNodes >
1232                bddManager->maxForwardedNodes){   
1233              CofactorFixAndReclaimForwardedNodes(bddManager, 0,
1234                                                     i-1, 0, i+2);
1235              CalBddPackNodesForMultipleIds(bddManager,
1236                                         bddManager->indexToId[i], 3);
1237            }
1238          }
1239          else {
1240            moved = BddReorderWindow2(bddManager, i, 0);
1241          }
1242          if (moved){
1243            if (i > 0) {
1244              levels[i-1]=1;
1245              if (i > 1) levels[i-2]=1;
1246            }
1247            levels[i]=1;
1248            levels[i+1]=1;
1249            if (i < bddManager->numVars-2) {
1250              levels[i+2]=1;
1251              if (i < bddManager->numVars-3) {
1252                levels[i+3]=1;
1253                if (i < bddManager->numVars-4) levels[i+4]=1;
1254              }
1255            }
1256            anySwapped=1;
1257          }
1258          else {
1259            levels[i]=0;
1260          }
1261        }
1262      }
1263      /* new code added */
1264      for (i = bddManager->numVars-1; i >= 0; i--){
1265        CalBddReorderFixCofactors(bddManager, bddManager->indexToId[i]);
1266      }
1267      CalBddReorderFixUserBddPtrs(bddManager);
1268      if (bddManager->pipelineState == CREATE){
1269        /* There are some results computed in pipeline */
1270        CalBddReorderFixProvisionalNodes(bddManager);
1271      }
1272      CalReorderAssociationFix(bddManager);
1273      CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
1274      /*even = 0;*/
1275    }
1276    else{
1277      /*fprintf(stdout, "Upward Swap\n");*/
1278      for (i=bddManager->numVars-1; i > 0; i--){
1279          /*
1280           * Fix the then and else cofactors. We need to fix it, even
1281           * if this level is not supposed to be moved.
1282           */
1283        if (i > 1) {
1284          CalBddReorderFixCofactors(bddManager,
1285                                 bddManager->indexToId[i-2]); 
1286        }
1287        else {
1288          CalBddReorderFixCofactors(bddManager,
1289                                 bddManager->indexToId[i-1]); 
1290        }
1291        if (levels[i]) {
1292          if (i > 1) {
1293            moved = BddReorderWindow3(bddManager, i-2, 1);
1294            if (bddManager->numForwardedNodes >
1295                bddManager->maxForwardedNodes){ 
1296              CofactorFixAndReclaimForwardedNodes(bddManager, 0,
1297                                                  i-3, 0,
1298                                                  lastIndex); 
1299              CalBddPackNodesForMultipleIds(bddManager,
1300                                            bddManager->indexToId[i-2], 3);
1301            }
1302          }
1303          else {
1304            moved = BddReorderWindow2(bddManager, i-1, 1);
1305          }
1306          if (moved){
1307            if (i < bddManager->numVars-1) {
1308              levels[i+1]=1;
1309              if (i < bddManager->numVars-2) {
1310                levels[i+2]=1;
1311                if (i < bddManager->numVars-3) {
1312                  levels[i+3]=1;
1313                  if (i < bddManager->numVars-4) {
1314                    levels[i+4]=1;
1315                  }
1316                }
1317              }
1318            }
1319            levels[i]=1;
1320            levels[i-1]=1;
1321            if (i > 1) {
1322              levels[i-2]=1;
1323            }
1324            anySwapped=1;
1325          }
1326          else {
1327            levels[i]=0;
1328          }
1329        }
1330      }
1331      even = 1;
1332      CalBddReorderFixUserBddPtrs(bddManager);
1333      if (bddManager->pipelineState == CREATE){
1334        /* There are some results computed in pipeline */
1335        CalBddReorderFixProvisionalNodes(bddManager);
1336      }
1337      CalReorderAssociationFix(bddManager);
1338      CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
1339    }
1340  }
1341  while (anySwapped);
1342  if (!even){ /* Need to do pointer fixing */
1343    for (i = bddManager->numVars-1; i >= 0; i--){
1344      CalBddReorderFixCofactors(bddManager, bddManager->indexToId[i]);
1345    }
1346    CalBddReorderFixUserBddPtrs(bddManager);
1347    if (bddManager->pipelineState == CREATE){
1348      /* There are some results computed in pipeline */
1349      CalBddReorderFixProvisionalNodes(bddManager);
1350    }
1351    CalReorderAssociationFix(bddManager);
1352    CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
1353  }
1354  Cal_Assert(CalCheckAllValidity(bddManager));
1355}
1356
1357/**Function********************************************************************
1358
1359  Synopsis           [required]
1360
1361  Description        [optional]
1362
1363  SideEffects        [required]
1364
1365  SeeAlso            [optional]
1366
1367******************************************************************************/
1368static int
1369BddReorderWindow2(Cal_BddManager bddManager, long index, int directionFlag)
1370{
1371  long curSize, startSize;
1372
1373  startSize = bddManager->numNodes;
1374  BddReorderSwapVarIndex(bddManager, index, 0);
1375  curSize = bddManager->numNodes;
1376  if (curSize > startSize){
1377    BddReorderSwapVarIndex(bddManager, index, 0);
1378  }
1379  if (directionFlag){/* Upward window swap */
1380    BddReorderFixAndFreeForwardingNodes(bddManager,
1381                                        bddManager->indexToId[index],
1382                                        bddManager->numVars-index); 
1383  }
1384  else{
1385    BddReorderFixAndFreeForwardingNodes(bddManager,
1386                                        bddManager->indexToId[index], 2);
1387  }
1388  Cal_Assert(CalCheckValidityOfNodesForWindow(bddManager, index, 2));
1389  return (curSize < startSize);
1390}
1391
1392/**Function********************************************************************
1393
1394  Synopsis           [required]
1395
1396  Description        [optional]
1397
1398  SideEffects        [required]
1399
1400  SeeAlso            [optional]
1401
1402******************************************************************************/
1403static int
1404BddReorderWindow3(Cal_BddManager bddManager, long index, int directionFlag)
1405{
1406  int best;
1407  long curSize, bestSize;
1408  long origSize = bddManager->numNodes;
1409 
1410  /* 1 2 3 */
1411  best = 0;
1412  bestSize = bddManager->numNodes;
1413  BddReorderSwapVarIndex(bddManager, index, 0); 
1414  /* 2 1 3 */
1415  curSize = bddManager->numNodes;
1416  if (curSize < bestSize){
1417    best = 1;
1418    bestSize = curSize;
1419  }
1420  BddReorderSwapVarIndex(bddManager, index+1, 0);
1421  /* 2 3 1 */
1422  curSize = bddManager->numNodes;
1423  if (curSize < bestSize){
1424    best = 2;
1425    bestSize = curSize;
1426  }
1427  BddReorderSwapVarIndex(bddManager, index, 1);
1428  /* 3 2 1 */
1429  curSize = bddManager->numNodes;
1430  if (curSize <= bestSize){
1431    best = 3;
1432    bestSize = curSize;
1433  }
1434  BddReorderSwapVarIndex(bddManager, index+1, 0);
1435  /* 3 1 2 */
1436  curSize = bddManager->numNodes;
1437  if (curSize <= bestSize){
1438    best = 4;
1439    bestSize = curSize;
1440  }
1441  BddReorderSwapVarIndex(bddManager, index, 1);
1442  /* 1 3 2 */
1443  curSize = bddManager->numNodes;
1444  if (curSize <= bestSize){
1445    best = 5;
1446    bestSize = curSize;
1447  }
1448  switch (best) {
1449    case 0:
1450      BddReorderSwapVarIndex(bddManager, index+1, 0);
1451      break;
1452    case 1:
1453      BddReorderSwapVarIndex(bddManager, index+1, 0);
1454      BddReorderSwapVarIndex(bddManager, index, 1);
1455      break;
1456    case 2:
1457      BddReorderSwapVarIndex(bddManager, index, 0);
1458      BddReorderSwapVarIndex(bddManager, index+1, 0);
1459      BddReorderSwapVarIndex(bddManager, index, 1);
1460      break;
1461    case 3:
1462      BddReorderSwapVarIndex(bddManager, index, 0);
1463      BddReorderSwapVarIndex(bddManager, index+1, 0);
1464      break;
1465    case 4:
1466      BddReorderSwapVarIndex(bddManager, index, 0);
1467      break;
1468    case 5:
1469      break;
1470  }
1471  if ((best == 0) || (best == 3)){
1472    CalBddReorderFixCofactors(bddManager, bddManager->indexToId[index]);
1473  }
1474  if (directionFlag){/* Upward window swap */
1475    BddReorderFixAndFreeForwardingNodes(bddManager,
1476                                        bddManager->indexToId[index],
1477                                        bddManager->numVars-index); 
1478  }
1479  else{
1480    BddReorderFixAndFreeForwardingNodes(bddManager,
1481                                        bddManager->indexToId[index], 3);
1482  }
1483  Cal_Assert(CalCheckValidityOfNodesForWindow(bddManager, index, 3));
1484  return ((best > 0) && (origSize > bestSize));
1485}
1486
Note: See TracBrowser for help on using the repository browser.