source: vis_dev/glu-2.3/src/calBdd/calReduce.c @ 23

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

library glu 2.3
File size: 23.9 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [calReduce.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines for optimizing a BDD with respect to a don't
8  care set (cofactor and restrict).]
9
10  Description []
11
12  SeeAlso     [None]
13
14  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and
15               Jagesh V. Sanghavi (sanghavi@eecs.berkeley.edu]
16
17  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
18  All rights reserved.
19
20  Permission is hereby granted, without written agreement and without license
21  or royalty fees, to use, copy, modify, and distribute this software and its
22  documentation for any purpose, provided that the above copyright notice and
23  the following two paragraphs appear in all copies of this software.
24
25  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
26  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
27  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
28  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
29
30  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
31  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
32  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
33  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
34  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
35
36  Revision    [$Id: calReduce.c,v 1.3 2002/09/21 20:39:25 fabio Exp $]
37
38******************************************************************************/
39
40#include "calInt.h"
41
42/*---------------------------------------------------------------------------*/
43/* Constant declarations                                                     */
44/*---------------------------------------------------------------------------*/
45
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Stucture declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56
57/*---------------------------------------------------------------------------*/
58/* Variable declarations                                                     */
59/*---------------------------------------------------------------------------*/
60
61
62/*---------------------------------------------------------------------------*/
63/* Macro declarations                                                        */
64/*---------------------------------------------------------------------------*/
65
66
67/**AutomaticStart*************************************************************/
68
69/*---------------------------------------------------------------------------*/
70/* Static function prototypes                                                */
71/*---------------------------------------------------------------------------*/
72
73static Cal_Bdd_t BddReduceBF(Cal_BddManager_t * bddManager, CalOpProc_t calOpProc, Cal_Bdd_t f, Cal_Bdd_t c);
74static Cal_Bdd_t BddCofactorBF(Cal_BddManager_t * bddManager, CalOpProc_t calOpProc, Cal_Bdd_t f, Cal_Bdd_t c);
75static void HashTableReduceApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reduceHashTableArray, CalHashTable_t ** orHashTableArray, CalOpProc_t calOpProc);
76static void HashTableCofactorApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** cofactorHashTableArray, CalOpProc_t calOpProc);
77static void HashTableCofactorReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t * uniqueTableForId);
78
79/**AutomaticEnd***************************************************************/
80
81
82/*---------------------------------------------------------------------------*/
83/* Definition of exported functions                                          */
84/*---------------------------------------------------------------------------*/
85/**Function********************************************************************
86
87  Synopsis    [Returns the generalized cofactor of BDD f with respect
88  to BDD c.]
89
90  Description [Returns the generalized cofactor of BDD f with respect
91  to BDD c. The constrain operator given by Coudert et al (ICCAD90) is
92  used to find the generalized cofactor.]
93
94  SideEffects [None.]
95
96  SeeAlso     [Cal_BddReduce]
97
98******************************************************************************/
99Cal_Bdd
100Cal_BddCofactor(Cal_BddManager  bddManager, Cal_Bdd fUserBdd,
101                Cal_Bdd cUserBdd)
102{
103  Cal_Bdd_t result;
104  Cal_Bdd userResult;
105  if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){
106    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
107    Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd);
108    result = BddCofactorBF(bddManager, CalOpCofactor, f, c);
109    userResult =  CalBddGetExternalBdd(bddManager, result);
110    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
111      Cal_BddFree(bddManager, userResult);
112      Cal_BddManagerGC(bddManager);
113      return (Cal_Bdd) 0;
114    }
115    return userResult;
116  }
117  return (Cal_Bdd) 0;
118}
119
120
121/**Function********************************************************************
122
123  Synopsis    [Returns a BDD which agrees with f for all valuations
124  which satisfy c.]
125
126  Description [Returns a BDD which agrees with f for all valuations
127  which satisfy c. The result is usually smaller in terms of number of
128  BDD nodes than f. This operation is typically used in state space
129  searches to simplify the representation for the set of states wich
130  will be expanded at each step.]
131
132  SideEffects [None]
133
134  SeeAlso     [Cal_BddCofactor]
135
136******************************************************************************/
137Cal_Bdd
138Cal_BddReduce(Cal_BddManager  bddManager, Cal_Bdd fUserBdd,
139              Cal_Bdd cUserBdd)
140{
141  if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){
142    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
143    Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd);
144    Cal_Bdd_t result;
145    Cal_Bdd userResult;
146
147    result = BddReduceBF(bddManager, CalOpCofactor, f, c);
148    userResult =  CalBddGetExternalBdd(bddManager, result);
149
150    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
151      Cal_BddFree(bddManager, userResult);
152      Cal_BddManagerGC(bddManager);
153      return (Cal_Bdd) 0;
154    }
155    if (Cal_BddSize(bddManager, userResult, 1) <
156        Cal_BddSize(bddManager, fUserBdd, 1)){
157      return userResult;
158    }
159    else{
160      Cal_BddFree(bddManager, userResult);
161      return Cal_BddIdentity(bddManager, fUserBdd);
162    }
163  }
164  return (Cal_Bdd) 0;
165}
166
167
168/**Function********************************************************************
169
170  Synopsis    [Returns a minimal BDD whose function contains fMin and is
171  contained in fMax.]
172
173  Description [Returns a minimal BDD f which is contains fMin and is
174  contained in fMax ( fMin <= f <= fMax).
175  This operation is typically used in state space searches to simplify
176  the representation for the set of states wich will be expanded at
177  each step (Rk Rk-1' <= f <= Rk).]
178
179  SideEffects [None]
180
181  SeeAlso     [Cal_BddReduce]
182
183******************************************************************************/
184Cal_Bdd
185Cal_BddBetween(Cal_BddManager  bddManager, Cal_Bdd fMinUserBdd,
186               Cal_Bdd fMaxUserBdd)
187{
188  if (CalBddPreProcessing(bddManager, 2, fMinUserBdd, fMaxUserBdd)){
189    Cal_Bdd_t fMin = CalBddGetInternalBdd(bddManager, fMinUserBdd);
190    Cal_Bdd_t fMax = CalBddGetInternalBdd(bddManager, fMaxUserBdd);
191    Cal_Bdd_t fMaxNot, careSet, result;
192    Cal_Bdd resultUserBdd;
193    long fMinSize, fMaxSize, resultSize;
194
195    CalBddNot(fMax, fMaxNot);
196    careSet = CalBddOpBF(bddManager, CalOpOr, fMin, fMaxNot);
197    result = BddReduceBF(bddManager, CalOpCofactor, fMin, careSet);
198    resultUserBdd =  CalBddGetExternalBdd(bddManager, result);
199    if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
200      Cal_BddFree(bddManager, resultUserBdd);
201      Cal_BddManagerGC(bddManager);
202      return (Cal_Bdd) 0;
203    }
204    fMinSize = Cal_BddSize(bddManager, fMinUserBdd, 1);
205    fMaxSize = Cal_BddSize(bddManager, fMaxUserBdd, 1);
206    resultSize = Cal_BddSize(bddManager, resultUserBdd, 1);
207    if (resultSize < fMinSize){
208      if (resultSize < fMaxSize){
209        return resultUserBdd;
210      }
211      else {
212        Cal_BddFree(bddManager, resultUserBdd);
213        return Cal_BddIdentity(bddManager, fMaxUserBdd);
214      }
215    }
216    Cal_BddFree(bddManager, resultUserBdd);
217    if (fMinSize < fMaxSize){
218      return Cal_BddIdentity(bddManager, fMinUserBdd);
219    }
220    else{
221      return Cal_BddIdentity(bddManager, fMaxUserBdd);
222    }
223  }
224  return (Cal_Bdd) 0;
225}
226
227
228/*---------------------------------------------------------------------------*/
229/* Definition of internal functions                                          */
230/*---------------------------------------------------------------------------*/
231/**Function********************************************************************
232
233  Synopsis    [required]
234
235  Description [optional]
236
237  SideEffects [required]
238
239  SeeAlso     [optional]
240
241******************************************************************************/
242int
243CalOpCofactor(
244  Cal_BddManager_t * bddManager,
245  Cal_Bdd_t  f,
246  Cal_Bdd_t  c,
247  Cal_Bdd_t * resultBddPtr)
248{
249  if (CalBddIsBddConst(c)){
250    if (CalBddIsBddZero(bddManager, c)){
251      *resultBddPtr = bddManager->bddNull;
252    }
253    else {
254      *resultBddPtr = f;
255    }
256    return 1;
257  }
258  if (CalBddIsBddConst(f)){
259    *resultBddPtr = f;
260    return 1;
261  }
262  return 0;
263}
264
265/*---------------------------------------------------------------------------*/
266/* Definition of static functions                                            */
267/*---------------------------------------------------------------------------*/
268/**Function********************************************************************
269
270  Synopsis    [required]
271
272  Description [optional]
273
274  SideEffects [required]
275
276  SeeAlso     [optional]
277
278******************************************************************************/
279static Cal_Bdd_t
280BddReduceBF(
281  Cal_BddManager_t * bddManager,
282  CalOpProc_t calOpProc,
283  Cal_Bdd_t  f,
284  Cal_Bdd_t  c)
285{
286  Cal_Bdd_t result;
287  CalHashTable_t  *hashTable;
288  CalHashTable_t **orHashTableArray = bddManager->reqQue[0];
289  CalHashTable_t **reduceHashTableArray = bddManager->reqQue[1];
290  CalHashTable_t *uniqueTableForId;
291 
292  /*Cal_BddIndex_t minIndex;*/
293  int minIndex;
294  int bddIndex;
295  Cal_BddId_t bddId, minId;
296 
297 
298  if ((*calOpProc)(bddManager, f, c, &result) == 1){
299    return result;
300  }
301
302  CalBddGetMinIdAndMinIndex(bddManager, f, c, minId, minIndex);
303  CalHashTableFindOrAdd(reduceHashTableArray[minId], f, c, &result); 
304  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
305    bddId = bddManager->indexToId[bddIndex];
306    hashTable = reduceHashTableArray[bddId];
307    if(hashTable->numEntries){
308      HashTableReduceApply(bddManager, hashTable, reduceHashTableArray,
309                           orHashTableArray, CalOpCofactor);
310    }
311  }
312  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
313    bddId = bddManager->indexToId[bddIndex];
314    uniqueTableForId = bddManager->uniqueTable[bddId];
315    hashTable = reduceHashTableArray[bddId];
316    if(hashTable->numEntries){
317        HashTableCofactorReduce(bddManager, hashTable, uniqueTableForId);
318    }
319  }
320  CalRequestIsForwardedTo(result);
321  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
322    bddId = bddManager->indexToId[bddIndex];
323    CalHashTableCleanUp(reduceHashTableArray[bddId]);
324  }
325  return result;
326}
327
328/**Function********************************************************************
329
330  Synopsis    [required]
331
332  Description [optional]
333
334  SideEffects [required]
335
336  SeeAlso     [optional]
337
338******************************************************************************/
339static Cal_Bdd_t
340BddCofactorBF(Cal_BddManager_t * bddManager,
341              CalOpProc_t calOpProc,
342              Cal_Bdd_t  f,
343              Cal_Bdd_t  c)
344{
345  Cal_Bdd_t result;
346  CalHashTable_t  *hashTable;
347  CalHashTable_t **cofactorHashTableArray = bddManager->reqQue[0];
348  CalHashTable_t *uniqueTableForId;
349 
350/*Cal_BddIndex_t minIndex;*/
351  int minIndex;
352  int bddIndex;
353  Cal_BddId_t bddId, minId;
354 
355  if (CalBddIsBddZero(bddManager, c)){
356    CalBddWarningMessage("Bdd Cofactor Called with zero care set");
357    return bddManager->bddOne;
358  }
359 
360  if (calOpProc(bddManager, f, c, &result) == 1){
361    return result;
362  }
363
364  CalBddGetMinIdAndMinIndex(bddManager, f, c, minId, minIndex);
365  CalHashTableFindOrAdd(cofactorHashTableArray[minId], f, c, &result); 
366  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
367    bddId = bddManager->indexToId[bddIndex];
368    hashTable = cofactorHashTableArray[bddId];
369    if(hashTable->numEntries){
370      HashTableCofactorApply(bddManager, hashTable, cofactorHashTableArray,
371                             calOpProc); 
372    }
373  }
374  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
375    bddId = bddManager->indexToId[bddIndex];
376    uniqueTableForId = bddManager->uniqueTable[bddId];
377    hashTable = cofactorHashTableArray[bddId];
378    if(hashTable->numEntries){
379        HashTableCofactorReduce(bddManager, hashTable, uniqueTableForId);
380    }
381  }
382  CalRequestIsForwardedTo(result);
383  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
384    bddId = bddManager->indexToId[bddIndex];
385    CalHashTableCleanUp(cofactorHashTableArray[bddId]);
386  }
387  return result;
388}
389
390/**Function********************************************************************
391
392  Synopsis    [required]
393
394  Description [optional]
395
396  SideEffects [required]
397
398  SeeAlso     [optional]
399
400******************************************************************************/
401static void
402HashTableReduceApply(Cal_BddManager_t * bddManager,
403                     CalHashTable_t * hashTable,
404                     CalHashTable_t ** reduceHashTableArray,
405                     CalHashTable_t ** orHashTableArray,
406                     CalOpProc_t calOpProc)
407{
408  int i, numBins = hashTable->numBins;
409  CalRequestNode_t *requestNode, *last, *nextRequestNode, *requestNodeList;
410  Cal_Bdd_t f, c, fx, cx, fxbar, cxbar, result, orResult;
411  Cal_BddId_t bddId, minId;
412  /*Cal_BddIndex_t minIndex;*/
413  int minIndex;
414  int bddIndex;
415  CalHashTable_t *orHashTable;
416 
417  requestNodeList = Cal_Nil(CalRequestNode_t);
418  for(i = 0; i < numBins; i++){
419    last = Cal_Nil(CalRequestNode_t);
420    for (requestNode =  hashTable->bins[i]; requestNode !=
421                                                Cal_Nil(CalRequestNode_t);
422         requestNode = nextRequestNode){
423      nextRequestNode = CalRequestNodeGetNextRequestNode(requestNode); 
424      CalRequestNodeGetF(requestNode, f);
425      CalRequestNodeGetG(requestNode, c);
426      CalBddGetMinId2(bddManager, f, c, minId);
427      CalBddGetCofactors(c, minId, cx, cxbar);
428      if (CalBddGetBddId(f) != minId){
429        if (CalOpOr(bddManager, cx, cxbar, &orResult) == 0){
430          CalBddNormalize(cx, cxbar);
431          CalBddGetMinId2(bddManager, cx, cxbar, minId);
432          CalHashTableFindOrAdd(orHashTableArray[minId], cx, cxbar, &orResult);
433        }
434        CalRequestNodePutElseRequest(requestNode, orResult);
435        if (last == Cal_Nil(CalRequestNode_t)){
436          hashTable->bins[i] = nextRequestNode;
437        }
438        else {
439          CalRequestNodePutNextRequestNode(last, nextRequestNode);
440        }
441        CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
442        requestNodeList = requestNode;
443      }
444      else{
445        last = requestNode;
446        CalBddGetCofactors(f, minId, fx, fxbar);
447        if((*calOpProc)(bddManager, fx, cx, &result) == 0){
448          CalBddGetMinId2(bddManager, fx, cx, bddId);
449          CalHashTableFindOrAdd(reduceHashTableArray[bddId], fx, cx, &result);
450        }
451        if (CalBddIsBddNull(bddManager, result) == 0){
452          CalBddIcrRefCount(result);
453        }
454        CalRequestNodePutThenRequest(requestNode, result);
455        if((*calOpProc)(bddManager, fxbar, cxbar, &result) == 0){
456          CalBddGetMinId2(bddManager, fxbar, cxbar, bddId);
457          CalHashTableFindOrAdd(reduceHashTableArray[bddId], fxbar, cxbar,
458                                &result);
459        }
460        if (CalBddIsBddNull(bddManager, result) == 0){
461          CalBddIcrRefCount(result);
462        }
463        CalRequestNodePutElseRequest(requestNode, result);
464      }
465    }
466  }
467  minIndex = bddManager->idToIndex[hashTable->bddId];
468  for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
469    bddId = bddManager->indexToId[bddIndex];
470    orHashTable = orHashTableArray[bddId];
471    if(orHashTable->numEntries){
472      CalHashTableApply(bddManager, orHashTable, orHashTableArray, CalOpOr);
473    }
474  }
475 
476  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
477    CalHashTable_t *uniqueTableForId;
478    bddId = bddManager->indexToId[bddIndex];
479    uniqueTableForId = bddManager->uniqueTable[bddId];
480    orHashTable = orHashTableArray[bddId];
481    if(orHashTable->numEntries){
482      CalHashTableReduce(bddManager, orHashTable, uniqueTableForId);
483    }
484  }
485  for (requestNode = requestNodeList; requestNode; requestNode =
486                                                       nextRequestNode){
487    nextRequestNode = CalRequestNodeGetNextRequestNode(requestNode);
488    CalRequestNodeGetElseRequest(requestNode, orResult);
489    CalRequestIsForwardedTo(orResult);
490    CalRequestNodeGetThenRequest(requestNode, f);
491    CalBddGetMinId2(bddManager, f, orResult, minId);
492    CalHashTableFindOrAdd(reduceHashTableArray[minId], f, orResult,
493                          &result);
494    CalRequestNodePutThenRequest(requestNode, result);
495    CalRequestNodePutElseRequest(requestNode, result);
496    CalBddAddRefCount(result, 2);
497    CalHashTableAddDirect(hashTable, requestNode);
498  }
499 
500  /* Clean up the orHashTableArray */
501  for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
502    bddId = bddManager->indexToId[bddIndex];
503    CalHashTableCleanUp(orHashTableArray[bddId]);
504  }
505}
506
507/**Function********************************************************************
508
509  Synopsis    [required]
510
511  Description [optional]
512
513  SideEffects [required]
514
515  SeeAlso     [optional]
516
517******************************************************************************/
518static void
519HashTableCofactorApply(Cal_BddManager_t * bddManager,
520                       CalHashTable_t * hashTable,
521                       CalHashTable_t ** cofactorHashTableArray,
522                       CalOpProc_t calOpProc)
523{
524  int i, numBins = hashTable->numBins;
525  CalBddNode_t **bins = hashTable->bins;
526  CalRequestNode_t *requestNode;
527  Cal_Bdd_t f, c, fx, cx, fxbar, cxbar, result;
528  Cal_BddId_t bddId, minId;
529
530  for(i = 0; i < numBins; i++){
531    for(requestNode = bins[i];
532        requestNode != Cal_Nil(CalRequestNode_t);
533        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
534      CalRequestNodeGetF(requestNode, f);
535      CalRequestNodeGetG(requestNode, c);
536      CalBddGetMinId2(bddManager, f, c, minId);
537      CalBddGetCofactors(f, minId, fx, fxbar);
538      CalBddGetCofactors(c, minId, cx, cxbar);
539      if((*calOpProc)(bddManager, fx, cx, &result) == 0){
540        CalBddGetMinId2(bddManager, fx, cx, bddId);
541        CalHashTableFindOrAdd(cofactorHashTableArray[bddId], fx, cx, &result);
542      }
543      if (CalBddIsBddNull(bddManager, result) == 0){
544        CalBddIcrRefCount(result);
545      }
546      CalRequestNodePutThenRequest(requestNode, result);
547      if((*calOpProc)(bddManager, fxbar, cxbar, &result) == 0){
548        CalBddGetMinId2(bddManager, fxbar, cxbar, bddId);
549        CalHashTableFindOrAdd(cofactorHashTableArray[bddId], fxbar, cxbar,
550                              &result);
551      }
552      if (CalBddIsBddNull(bddManager, result) == 0){
553          CalBddIcrRefCount(result);
554      }
555      CalRequestNodePutElseRequest(requestNode, result);
556    }
557  }
558}
559
560/**Function********************************************************************
561
562  Synopsis    [required]
563
564  Description [optional]
565
566  SideEffects [required]
567
568  SeeAlso     [optional]
569
570******************************************************************************/
571static void
572HashTableCofactorReduce(Cal_BddManager_t * bddManager,
573                        CalHashTable_t * hashTable,
574                        CalHashTable_t * uniqueTableForId)
575{
576  int i, numBins = hashTable->numBins;
577  CalBddNode_t **bins = hashTable->bins;
578  Cal_BddId_t currentBddId = uniqueTableForId->bddId;
579  CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
580  CalRequestNode_t  *requestNode, *next, *endNode;
581  CalBddNode_t *bddNode;
582  Cal_Bdd_t thenBdd, elseBdd, result;
583  Cal_BddRefCount_t refCount;
584
585  endNode = hashTable->endNode;
586  for(i = 0; i < numBins; i++){
587    for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
588        requestNode != Cal_Nil(CalRequestNode_t);
589        requestNode = next){
590      next = CalRequestNodeGetNextRequestNode(requestNode);
591      /* Process the requestNode */
592      CalRequestNodeGetThenRequest(requestNode, thenBdd);
593      CalRequestNodeGetElseRequest(requestNode, elseBdd);
594      if (CalBddIsBddNull(bddManager, thenBdd)){
595        CalRequestIsForwardedTo(elseBdd);
596        CalBddNodeGetRefCount(requestNode, refCount);
597        CalBddAddRefCount(elseBdd, refCount - 1);
598        CalRequestNodePutThenRequest(requestNode, elseBdd);
599        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
600        endNode->nextBddNode = requestNode;
601        endNode = requestNode;
602        continue;
603      }
604      else if (CalBddIsBddNull(bddManager, elseBdd)){
605        CalRequestIsForwardedTo(thenBdd);
606        CalBddNodeGetRefCount(requestNode, refCount);
607        CalBddAddRefCount(thenBdd, refCount - 1);
608        CalRequestNodePutThenRequest(requestNode, thenBdd);
609        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
610        endNode->nextBddNode = requestNode;
611        endNode = requestNode;
612        continue;
613      }
614      CalRequestIsForwardedTo(thenBdd);
615      CalRequestIsForwardedTo(elseBdd);
616      if(CalBddIsEqual(thenBdd, elseBdd)){
617        CalBddNodeGetRefCount(requestNode, refCount);
618        CalBddAddRefCount(thenBdd, refCount - 2);
619        CalRequestNodePutThenRequest(requestNode, thenBdd);
620        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
621        endNode->nextBddNode = requestNode;
622        endNode = requestNode;
623      }
624      else if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
625          thenBdd, elseBdd, &result) == 1){
626        CalBddDcrRefCount(thenBdd);
627        CalBddDcrRefCount(elseBdd);
628        CalBddNodeGetRefCount(requestNode, refCount);
629        CalBddAddRefCount(result, refCount);
630        CalRequestNodePutThenRequest(requestNode, result);
631        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
632        endNode->nextBddNode = requestNode;
633        endNode = requestNode;
634      }
635      else if(CalBddIsOutPos(thenBdd)){
636        CalRequestNodePutThenRequest(requestNode, thenBdd);
637        CalRequestNodePutElseRequest(requestNode, elseBdd);
638        CalHashTableAddDirect(uniqueTableForId, requestNode);
639        bddManager->numNodes++;
640        bddManager->gcCheck--;
641      }
642      else{
643        CalNodeManagerAllocNode(nodeManager, bddNode);
644        CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
645        CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
646        CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
647        CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
648        CalBddNodeGetRefCount(requestNode, refCount);
649        CalBddNodePutRefCount(bddNode, refCount);
650        CalHashTableAddDirect(uniqueTableForId, bddNode);
651        bddManager->numNodes++;
652        bddManager->gcCheck--;
653        CalRequestNodePutThenRequestId(requestNode, currentBddId);
654        CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
655        CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
656        endNode->nextBddNode = requestNode;
657        endNode = requestNode;
658      }
659    }
660  }
661  hashTable->endNode = endNode;
662}
663 
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
Note: See TracBrowser for help on using the repository browser.