glu-2.2: src/calBdd/calPipeline.c Source File

00001 
00042 #include "calInt.h"
00043 
00044 /*---------------------------------------------------------------------------*/
00045 /* Constant declarations                                                     */
00046 /*---------------------------------------------------------------------------*/
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Type declarations                                                         */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Stucture declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Variable declarations                                                     */
00059 /*---------------------------------------------------------------------------*/
00060 
00061 /*---------------------------------------------------------------------------*/
00062 /* Macro declarations                                                        */
00063 /*---------------------------------------------------------------------------*/
00064 
00067 /*---------------------------------------------------------------------------*/
00068 /* Static function prototypes                                                */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 
00075 /*---------------------------------------------------------------------------*/
00076 /* Definition of exported functions                                          */
00077 /*---------------------------------------------------------------------------*/
00090 void
00091 Cal_PipelineSetDepth(Cal_BddManager bddManager, int depth)
00092 {
00093   int i, j;
00094   if(depth > 6){
00095     CalBddWarningMessage("PipelineDepth can not exceed 6\n");
00096     CalBddWarningMessage("setting PipelineDepth to 6\n");
00097     depth = 6;
00098   }
00099   if(bddManager->maxDepth < depth){
00100     int oldMaxDepth = bddManager->maxDepth;
00101     bddManager->depth = bddManager->maxDepth = depth;
00102     bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
00103                                  bddManager->maxDepth);
00104     for(i = oldMaxDepth; i < bddManager->maxDepth; i++){
00105       bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
00106       for(j = 0; j < bddManager->numVars+1; j++){
00107         bddManager->reqQue[i][j] =
00108             CalHashTableInit(bddManager, j);
00109       }
00110     }
00111   }
00112   else{
00113     bddManager->depth = depth;
00114   }  
00115 }
00116 
00129 int
00130 Cal_PipelineInit(Cal_BddManager bddManager, Cal_BddOp_t bddOp)
00131 {
00132   CalBddPostProcessing(bddManager);
00133   if(bddManager->pipelineState != READY){
00134     CalBddWarningMessage("Pipeline cannot be initialized");
00135     return 0;
00136   }
00137   else{
00138     bddManager->pipelineState = CREATE;
00139     switch(bddOp){
00140     case CAL_AND :
00141       bddManager->pipelineFn = CalOpAnd;
00142       break;
00143     case CAL_OR  :
00144       bddManager->pipelineFn = CalOpOr;
00145       break;
00146     case CAL_XOR :
00147       bddManager->pipelineFn = CalOpXor;
00148       break;
00149     default  :
00150       CalBddWarningMessage("Unknown Bdd Operation type");
00151       return 0;
00152     }
00153     return 1;
00154   }  
00155 }
00156 
00169 Cal_Bdd
00170 Cal_PipelineCreateProvisionalBdd(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
00171                                  Cal_Bdd gUserBdd)
00172 {
00173   int insertDepth, operandDepth;
00174   CalRequestNode_t *requestNode;
00175   Cal_Bdd_t provisionalBdd, f, g;
00176   Cal_BddId_t bddId;
00177   Cal_Bdd userNode;
00178   
00179   insertDepth = 0;
00180   
00181   f = CalBddGetInternalBdd(bddManager, fUserBdd);
00182   g = CalBddGetInternalBdd(bddManager, gUserBdd);
00183   if(bddManager->pipelineState != CREATE){
00184     CalBddWarningMessage("Provisional Bdd not created: Pipeline is not initialized");
00185     return (Cal_Bdd) 0;
00186   }
00187   if(CalBddIsMarked(f)){
00188     CalBddGetDepth(f, operandDepth);
00189     if(insertDepth <= operandDepth){
00190       insertDepth = operandDepth + 1;
00191     }
00192   }
00193   if(CalBddIsMarked(g)){
00194     CalBddGetDepth(g, operandDepth);
00195     if(insertDepth <= operandDepth){
00196       insertDepth = operandDepth + 1;
00197     }
00198   }
00199   if (bddManager->pipelineDepth <= insertDepth){
00200     bddManager->pipelineDepth = insertDepth + 1;
00201   }
00202   if (insertDepth >= MAX_INSERT_DEPTH){
00203     CalBddWarningMessage("Provisional Bdd not created");
00204     CalBddWarningMessage("Maximum pipeline depth is reached");
00205     return (Cal_Bdd) 0;
00206   }
00207 
00208   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00209   CalRequestNodePutF(requestNode, f);
00210   CalRequestNodePutG(requestNode, g);
00211   CalRequestNodeMark(requestNode);
00212   CalRequestNodePutDepth(requestNode, insertDepth);
00213   CalRequestNodePutNextRequestNode(requestNode,
00214       bddManager->requestNodeListArray[insertDepth]);
00215   bddManager->requestNodeListArray[insertDepth] = requestNode;
00216 
00217   CalBddGetMinId2(bddManager, f, g, bddId);
00218   CalBddPutBddId(provisionalBdd, bddId);
00219   CalBddPutBddNode(provisionalBdd, (CalBddNode_t *)requestNode);
00220 
00221   CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], userNode);
00222   CalBddNodePutThenBdd(userNode, provisionalBdd);
00223   CalBddNodePutElseBdd(userNode, bddManager->bddOne);
00224   CalBddNodePutNextBddNode(userNode,
00225                            bddManager->userProvisionalNodeList);
00226   bddManager->userProvisionalNodeList = userNode;
00227   CalBddNodeIcrRefCount(userNode);
00228   return userNode;
00229 }
00230 
00243 int
00244 Cal_PipelineExecute(Cal_BddManager bddManager)
00245 {
00246   CalRequestNode_t **requestNodeListArray, *node, *nextNode;
00247   int  i;
00248   Cal_Bdd_t thenBdd;
00249   int automaticDepthControlFlag = 0;
00250   int pipelineDepth;
00251   
00252   if(bddManager->pipelineState != CREATE){
00253     CalBddWarningMessage("Pipeline cannot be executed");
00254     return 0;
00255   }
00256 
00257   /* Check if we need to control the depth value using some heuristic */
00258   if (bddManager->depth == 0) automaticDepthControlFlag = 1;
00259   
00260   requestNodeListArray = bddManager->requestNodeListArray;
00261   pipelineDepth = bddManager->pipelineDepth;
00262   while(pipelineDepth){
00263     if (automaticDepthControlFlag){
00264       if (bddManager->numNodes < 10000) bddManager->depth = 4;
00265       else if (bddManager->numNodes < 100000) bddManager->depth = 2;
00266       else bddManager->depth = 1;
00267     }
00268     if(bddManager->depth > pipelineDepth){
00269       bddManager->depth = pipelineDepth;
00270     }
00271     CalRequestNodeListArrayOp(bddManager, requestNodeListArray,
00272                               bddManager->pipelineFn);
00273     pipelineDepth -= bddManager->depth;
00274 
00275     /* Lock the results, in case garbage collection needs to be
00276        invoked */
00277     for (i=0; i<bddManager->depth; i++){
00278       for (node = requestNodeListArray[i]; node; node = nextNode){
00279         nextNode = CalBddNodeGetNextBddNode(node);
00280         CalBddNodeGetThenBdd(node, thenBdd);
00281         CalBddIcrRefCount(thenBdd);
00282       }
00283     }
00284     /* Save the current pipelineDepth */
00285     bddManager->currentPipelineDepth = pipelineDepth;
00286     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00287       /* Abort, may be we should clean up a little bit */
00288       fprintf(stderr,"Bdd Overflow: Aborting\n");
00289       return 0;
00290     }
00291     requestNodeListArray += bddManager->depth;
00292   }
00293   /* Need to decrement the reference counts */
00294   for (i=0; i<bddManager->pipelineDepth; i++){
00295     for (node=bddManager->requestNodeListArray[i]; node; node = nextNode){
00296       nextNode = CalBddNodeGetNextBddNode(node);
00297       CalBddNodeGetThenBdd(node, thenBdd);
00298       CalBddDcrRefCount(thenBdd);
00299     }
00300   }
00301   bddManager->pipelineState = UPDATE;
00302   return 1;
00303 }
00304   
00317 Cal_Bdd
00318 Cal_PipelineUpdateProvisionalBdd(Cal_BddManager bddManager,
00319                                  Cal_Bdd provisionalBdd) 
00320 {
00321   Cal_Bdd_t calBdd = CalBddGetInternalBdd(bddManager, provisionalBdd);
00322   if(bddManager->pipelineState != UPDATE){
00323     CalBddWarningMessage("Provisional Bdd cannot be updated");
00324     return (Cal_Bdd) 0;
00325   }
00326   CalBddGetThenBdd(calBdd, calBdd);
00327   return CalBddGetExternalBdd(bddManager, calBdd);
00328 }
00329 
00343 int
00344 Cal_BddIsProvisional(Cal_BddManager bddManager, Cal_Bdd userBdd)
00345 {
00346   Cal_Bdd_t internalBdd = CalBddGetInternalBdd(bddManager, userBdd);
00347   return CalBddIsMarked(internalBdd);
00348 }
00349 
00362 void
00363 Cal_PipelineQuit(Cal_BddManager bddManager)
00364 {
00365   CalRequestNode_t *requestNode, *next;
00366   int i;
00367 
00368   bddManager->pipelineState = READY;
00369   for(i = 0; i < bddManager->pipelineDepth; i++){
00370     for(requestNode = bddManager->requestNodeListArray[i], 
00371         bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00372         requestNode != Cal_Nil(CalRequestNode_t);
00373         requestNode = next){
00374       next = CalRequestNodeGetNextRequestNode(requestNode);
00375       CalNodeManagerFreeNode(bddManager->nodeManagerArray[0], requestNode);
00376     }
00377     bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00378   }
00379   bddManager->pipelineDepth = 0;
00380   for (requestNode = bddManager->userProvisionalNodeList; requestNode;
00381        requestNode = next){
00382     next = CalRequestNodeGetNextRequestNode(requestNode);
00383     CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00384                            requestNode);
00385   }
00386   bddManager->userProvisionalNodeList = Cal_Nil(CalRequestNode_t);
00387 }
00388 
00389 /*---------------------------------------------------------------------------*/
00390 /* Definition of internal functions                                          */
00391 /*---------------------------------------------------------------------------*/
00403 void
00404 CalBddReorderFixProvisionalNodes(Cal_BddManager_t *bddManager)
00405 {
00406   CalRequestNode_t **requestNodeListArray =
00407       bddManager->requestNodeListArray;
00408   CalRequestNode_t *node, *nextNode;
00409   int i;
00410   Cal_Bdd_t thenBdd, elseBdd;
00411   
00412   for (i=0;
00413        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00414        i++){ 
00415     for (node = *requestNodeListArray; node; node = nextNode){
00416       nextNode = CalBddNodeGetNextBddNode(node);
00417       Cal_Assert(CalBddNodeIsForwarded(node));
00418       CalBddNodeGetThenBdd(node, thenBdd);
00419       if (CalBddIsForwarded(thenBdd)) {
00420         CalBddForward(thenBdd);
00421       }
00422       CalBddNodePutThenBdd(node, thenBdd);
00423       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00424     }
00425     requestNodeListArray++;
00426   }
00427   for (; i<bddManager->pipelineDepth; i++){
00428     for (node = *requestNodeListArray; node; node = nextNode){
00429       nextNode = CalBddNodeGetNextBddNode(node);
00430       Cal_Assert(CalBddNodeIsForwarded(node) == 0);
00431       CalBddNodeGetThenBdd(node, thenBdd);
00432       if (CalBddIsForwarded(thenBdd)) {
00433         CalBddForward(thenBdd);
00434       }
00435       CalBddNodePutThenBdd(node, thenBdd);
00436       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00437       CalBddNodeGetElseBdd(node, elseBdd);
00438       if (CalBddIsForwarded(elseBdd)) {
00439         CalBddForward(elseBdd);
00440       }
00441       CalBddNodePutElseBdd(node, elseBdd);
00442       Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00443     }
00444     requestNodeListArray++;
00445   }
00446 }
00447 
00459 void
00460 CalCheckPipelineValidity(Cal_BddManager_t *bddManager)
00461 {
00462   CalRequestNode_t **requestNodeListArray =
00463       bddManager->requestNodeListArray;
00464   CalRequestNode_t *node, *nextNode;
00465   int i;
00466   Cal_Bdd_t thenBdd, elseBdd;
00467   
00468   for (i=0;
00469        i<bddManager->pipelineDepth-bddManager->currentPipelineDepth;
00470        i++){ 
00471     for (node = *requestNodeListArray; node; node = nextNode){
00472       nextNode = CalBddNodeGetNextBddNode(node);
00473       Cal_Assert(CalBddNodeIsForwarded(node));
00474       CalBddNodeGetThenBdd(node, thenBdd);
00475       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00476     }
00477     requestNodeListArray++;
00478   }
00479   for (; i<bddManager->pipelineDepth; i++){
00480     for (node = *requestNodeListArray; node; node = nextNode){
00481       nextNode = CalBddNodeGetNextBddNode(node);
00482       Cal_Assert(CalBddNodeIsForwarded(node) == 0); 
00483       CalBddNodeGetThenBdd(node, thenBdd);
00484       /*Cal_Assert(CalBddIsForwarded(thenBdd) == 0);*/
00485       /* This is possible since the actual BDD of thenBdd could have been
00486          computed and it is forwarded, however this node is not yet
00487          updated with the result */
00488       CalBddNodeGetElseBdd(node, elseBdd);
00489       /*Cal_Assert(CalBddIsForwarded(elseBdd) == 0);*/
00490     }
00491     requestNodeListArray++;
00492   }
00493 }
00494 /*---------------------------------------------------------------------------*/
00495 /* Definition of static functions                                            */
00496 /*---------------------------------------------------------------------------*/
00497