source: vis_dev/glu-2.3/src/calBdd/calBddSwapVars.c @ 66

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

library glu 2.3
File size: 20.9 KB
RevLine 
[13]1/**CFile***********************************************************************
2
3  FileName    [calBddSwapVars.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routine for swapping two variables.]
8
9  Description [Routine for swapping two variables.]
10
11  SeeAlso     [None]
12
13  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
14               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
15               ]
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: calBddSwapVars.c,v 1.1.1.3 1998/05/04 00:58:55 hsv Exp $]
37
38******************************************************************************/
39
40#include "calInt.h"
41
42/*---------------------------------------------------------------------------*/
43/* Constant declarations                                                     */
44/*---------------------------------------------------------------------------*/
45
46/*---------------------------------------------------------------------------*/
47/* Type declarations                                                         */
48/*---------------------------------------------------------------------------*/
49
50/*---------------------------------------------------------------------------*/
51/* Stucture declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54
55/*---------------------------------------------------------------------------*/
56/* Variable declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Macro declarations                                                        */
61/*---------------------------------------------------------------------------*/
62
63/**AutomaticStart*************************************************************/
64
65/*---------------------------------------------------------------------------*/
66/* Static function prototypes                                                */
67/*---------------------------------------------------------------------------*/
68
69static void CalHashTableSwapVarsApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t gIndex, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose, CalHashTable_t ** reqQueForITE);
70static void CalHashTableSwapVarsPlusApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose);
71static void CalHashTableSwapVarsMinusApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, Cal_BddIndex_t hIndex, CalHashTable_t ** reqQueForSwapVars, CalHashTable_t ** reqQueForSwapVarsPlus, CalHashTable_t ** reqQueForSwapVarsMinus, CalHashTable_t ** reqQueForCompose);
72
73/**AutomaticEnd***************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions                                          */
77/*---------------------------------------------------------------------------*/
78
79/**Function********************************************************************
80
81  Synopsis    [Return a function obtained by swapping two variables]
82
83  Description [Returns the BDD obtained by simultaneously substituting variable
84  g by variable h and variable h and variable g in the BDD f]
85
86  SideEffects [None]
87
88  SeeAlso     [Cal_BddSubstitute]
89
90******************************************************************************/
91Cal_Bdd
92Cal_BddSwapVars(Cal_BddManager  bddManager, Cal_Bdd  fUserBdd,
93                Cal_Bdd gUserBdd,
94                Cal_Bdd hUserBdd)
95{
96  Cal_Bdd_t f,g,h,tmpBdd;
97  Cal_BddIndex_t gIndex, hIndex;
98  CalRequest_t result;
99  int bddId, bddIndex;
100  CalHashTable_t *hashTable;
101  CalHashTable_t *uniqueTableForId;
102  CalHashTable_t **reqQueForSwapVars = bddManager->reqQue[0];
103  CalHashTable_t **reqQueForSwapVarsPlus = bddManager->reqQue[1];
104  CalHashTable_t **reqQueForSwapVarsMinus = bddManager->reqQue[2];
105  CalHashTable_t **reqQueForCompose = bddManager->reqQue[3];
106  CalHashTable_t **reqQueForITE = bddManager->reqQue[4]; 
107 
108  if (CalBddPreProcessing(bddManager, 3, fUserBdd, gUserBdd, hUserBdd) == 0){
109        return (Cal_Bdd) 0;
110  }
111  f = CalBddGetInternalBdd(bddManager, fUserBdd);
112  g = CalBddGetInternalBdd(bddManager, gUserBdd);
113  h = CalBddGetInternalBdd(bddManager, hUserBdd);
114
115  if(CalBddIsBddConst(g) || CalBddIsBddConst(h)){
116    CalBddWarningMessage("Unacceptable arguments for Cal_BddSwapVars");
117    return (Cal_Bdd) 0;
118  }
119  if(CalBddIsEqual(g, h)){
120    /*
121    CalBddIcrRefCount(f);
122    */
123    return CalBddGetExternalBdd(bddManager, f);
124  }
125  if(CalBddGetBddIndex(bddManager, g) > CalBddGetBddIndex(bddManager, h)){
126    tmpBdd = g;
127    g = h;
128    h = tmpBdd;
129  }
130
131  gIndex = CalBddGetBddIndex(bddManager, g);
132  hIndex = CalBddGetBddIndex(bddManager, h);
133
134  CalBddGetMinId2(bddManager, f, g, bddId);
135  CalHashTableFindOrAdd(reqQueForSwapVars[bddId], f, 
136      bddManager->bddNull, &result);
137
138  /* ReqQueApply */
139  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
140    bddId = bddManager->indexToId[bddIndex];
141    hashTable = reqQueForSwapVars[bddId];
142    if(hashTable->numEntries){
143      CalHashTableSwapVarsApply(bddManager, hashTable, gIndex, hIndex,
144          reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
145          reqQueForCompose, reqQueForITE);
146    }
147    hashTable = reqQueForSwapVarsPlus[bddId];
148    if(hashTable->numEntries){
149      CalHashTableSwapVarsPlusApply(bddManager, hashTable, hIndex,
150          reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
151          reqQueForCompose);
152    }
153    hashTable = reqQueForSwapVarsMinus[bddId];
154    if(hashTable->numEntries){
155      CalHashTableSwapVarsMinusApply(bddManager, hashTable, hIndex,
156          reqQueForSwapVars, reqQueForSwapVarsPlus, reqQueForSwapVarsMinus,
157          reqQueForCompose);
158    }
159    hashTable = reqQueForCompose[bddId];
160    if(hashTable->numEntries){
161      CalHashTableComposeApply(bddManager, hashTable, hIndex,
162          reqQueForCompose, reqQueForITE);
163    }
164    hashTable = reqQueForITE[bddId];
165    if(hashTable->numEntries){
166      CalHashTableITEApply(bddManager, hashTable, reqQueForITE);
167    }
168  }
169
170  /* ReqQueReduce */
171  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
172    bddId = bddManager->indexToId[bddIndex];
173    uniqueTableForId = bddManager->uniqueTable[bddId];
174    hashTable = reqQueForSwapVars[bddId];
175    if(hashTable->numEntries){
176      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
177    }
178    hashTable = reqQueForSwapVarsPlus[bddId];
179    if(hashTable->numEntries){
180      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
181    }
182    hashTable = reqQueForSwapVarsMinus[bddId];
183    if(hashTable->numEntries){
184      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
185    }
186    hashTable = reqQueForCompose[bddId];
187    if(hashTable->numEntries){
188      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
189    }
190    hashTable = reqQueForITE[bddId];
191    if(hashTable->numEntries){
192      CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
193    }
194  }
195
196  CalRequestIsForwardedTo(result);
197
198  /* ReqQueCleanUp */
199  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
200    CalHashTableCleanUp(reqQueForSwapVars[bddId]);
201    CalHashTableCleanUp(reqQueForSwapVarsPlus[bddId]);
202    CalHashTableCleanUp(reqQueForSwapVarsMinus[bddId]);
203    CalHashTableCleanUp(reqQueForCompose[bddId]);
204    CalHashTableCleanUp(reqQueForITE[bddId]);
205  }
206  return CalBddGetExternalBdd(bddManager, result);
207}
208
209/*---------------------------------------------------------------------------*/
210/* Definition of internal functions                                          */
211/*---------------------------------------------------------------------------*/
212
213/*---------------------------------------------------------------------------*/
214/* Definition of static functions                                            */
215/*---------------------------------------------------------------------------*/
216
217/**Function********************************************************************
218
219  Synopsis    [required]
220
221  Description [optional]
222
223  SideEffects [required]
224
225  SeeAlso     [optional]
226
227******************************************************************************/
228static void
229CalHashTableSwapVarsApply(
230  Cal_BddManager_t * bddManager,
231  CalHashTable_t * hashTable,
232  Cal_BddIndex_t  gIndex,
233  Cal_BddIndex_t  hIndex,
234  CalHashTable_t ** reqQueForSwapVars,
235  CalHashTable_t ** reqQueForSwapVarsPlus,
236  CalHashTable_t ** reqQueForSwapVarsMinus,
237  CalHashTable_t ** reqQueForCompose,
238  CalHashTable_t ** reqQueForITE)
239{
240  int i, numBins = hashTable->numBins;
241  CalBddNode_t **bins = hashTable->bins;
242  CalRequestNode_t *requestNode;
243  Cal_BddId_t bddId;
244  Cal_BddIndex_t fIndex, bddIndex;
245  Cal_Bdd_t f, calBdd;
246  Cal_Bdd_t thenBdd, elseBdd;
247  Cal_Bdd_t nullBdd = bddManager->bddNull;
248  Cal_Bdd_t result;
249
250  for(i = 0; i < numBins; i++){
251    for(requestNode = bins[i];
252        requestNode != Cal_Nil(CalRequestNode_t);
253        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
254      CalRequestNodeGetF(requestNode, f);
255      fIndex = CalBddGetBddIndex(bddManager, f);
256      if(fIndex < gIndex){
257        /* left cofactor */
258        CalBddGetThenBdd(f, calBdd);
259        bddId = CalBddGetBddId(calBdd);
260        bddIndex = bddManager->idToIndex[bddId];
261        if(bddIndex <= hIndex){
262          if(bddIndex > gIndex){
263            bddId = bddManager->indexToId[gIndex];
264          }
265          CalHashTableFindOrAdd(reqQueForSwapVars[bddId],
266              calBdd, nullBdd, &calBdd);
267        }
268        CalBddIcrRefCount(calBdd);
269        CalRequestNodePutThenRequest(requestNode, calBdd);
270        /* right cofactor */
271        CalBddGetElseBdd(f, calBdd);
272        bddId = CalBddGetBddId(calBdd);
273        bddIndex = bddManager->idToIndex[bddId];
274        if(bddIndex <= hIndex){
275          if(bddIndex > gIndex){
276            bddId = bddManager->indexToId[gIndex];
277          }
278          CalHashTableFindOrAdd(reqQueForSwapVars[bddId],
279              calBdd, nullBdd, &calBdd);
280        }
281        CalBddIcrRefCount(calBdd);
282        CalRequestNodePutElseRequest(requestNode, calBdd);
283      }
284      else if(fIndex == gIndex){
285        /* SwapVarsPlus */
286        CalBddGetThenBdd(f, thenBdd);
287        CalBddGetElseBdd(f, elseBdd);
288        if(CalBddGetBddIndex(bddManager, thenBdd) == hIndex){
289          CalBddGetThenBdd(thenBdd, thenBdd);
290        }
291        if(CalBddGetBddIndex(bddManager, elseBdd) == hIndex){
292          CalBddGetThenBdd(elseBdd, elseBdd);
293        }
294        if(CalBddIsEqual(thenBdd, elseBdd)){
295          if(hIndex > CalBddGetBddIndex(bddManager, thenBdd)){
296            CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(thenBdd)], 
297                thenBdd, CalBddOne(bddManager), &result);
298          }
299          else{
300            result = thenBdd;
301          }
302        }
303        else if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
304            hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
305          bddId = bddManager->indexToId[hIndex];
306          if(!CalUniqueTableForIdFindOrAdd(bddManager, 
307              bddManager->uniqueTable[bddId], thenBdd, elseBdd, &result)){
308            CalBddIcrRefCount(thenBdd);
309            CalBddIcrRefCount(elseBdd);
310          }
311        }
312        else{
313          CalBddGetMinId2(bddManager, thenBdd, elseBdd, bddId);
314          CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId],
315              thenBdd, elseBdd, &result);
316        }
317        CalBddIcrRefCount(result);
318        CalRequestNodePutThenRequest(requestNode, result);
319        /* SwapVarsMinus */
320        CalBddGetThenBdd(f, thenBdd);
321        CalBddGetElseBdd(f, elseBdd);
322        if(CalBddGetBddIndex(bddManager, thenBdd) == hIndex){
323          CalBddGetElseBdd(thenBdd, thenBdd);
324        }
325        if(CalBddGetBddIndex(bddManager, elseBdd) == hIndex){
326          CalBddGetElseBdd(elseBdd, elseBdd);
327        }
328        if(CalBddIsEqual(thenBdd, elseBdd)){
329          if(hIndex > CalBddGetBddIndex(bddManager, thenBdd)){
330            CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(thenBdd)], 
331                thenBdd, CalBddZero(bddManager), &result);
332          }
333          else{
334            result = thenBdd;
335          }
336        }
337        else if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
338            hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
339          bddId = bddManager->indexToId[hIndex];
340          if(!CalUniqueTableForIdFindOrAdd(bddManager, 
341              bddManager->uniqueTable[bddId], thenBdd, elseBdd, &result)){
342            CalBddIcrRefCount(thenBdd);
343            CalBddIcrRefCount(elseBdd);
344          }
345        }
346        else{
347          CalBddGetMinId2(bddManager, thenBdd, elseBdd, bddId);
348          CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId],
349              thenBdd, elseBdd, &result);
350        }
351        CalBddIcrRefCount(result);
352        CalRequestNodePutElseRequest(requestNode, result);
353      }
354      else{ /* fIndex > gIndex */
355        CalComposeRequestCreate(bddManager,
356            f, CalBddOne(bddManager), hIndex,
357            reqQueForCompose, reqQueForITE, &result);
358        CalBddIcrRefCount(result);
359        CalRequestNodePutThenRequest(requestNode, result);
360        CalComposeRequestCreate(bddManager,
361            f, CalBddZero(bddManager), hIndex,
362            reqQueForCompose, reqQueForITE, &result);
363        CalBddIcrRefCount(result);
364        CalRequestNodePutElseRequest(requestNode, result);
365      }
366    }
367  }
368}
369
370
371/**Function********************************************************************
372
373  Synopsis    [required]
374
375  Description [optional]
376
377  SideEffects [required]
378
379  SeeAlso     [optional]
380
381******************************************************************************/
382static void
383CalHashTableSwapVarsPlusApply(
384  Cal_BddManager_t * bddManager,
385  CalHashTable_t * hashTable,
386  Cal_BddIndex_t  hIndex,
387  CalHashTable_t ** reqQueForSwapVars,
388  CalHashTable_t ** reqQueForSwapVarsPlus,
389  CalHashTable_t ** reqQueForSwapVarsMinus,
390  CalHashTable_t ** reqQueForCompose)
391{
392  int i, numBins = hashTable->numBins;
393  CalBddNode_t **bins = hashTable->bins;
394  CalRequestNode_t *requestNode;
395  Cal_BddId_t bddId;
396  Cal_Bdd_t f1, f2, g1, g2;
397  Cal_Bdd_t result;
398
399  for(i = 0; i < numBins; i++){
400    for(requestNode = bins[i];
401        requestNode != Cal_Nil(CalRequestNode_t);
402        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
403      CalRequestNodeGetCofactors(bddManager, requestNode, f1, f2, g1, g2);
404      /* left cofactor */ 
405      if(CalBddGetBddIndex(bddManager, f1) == hIndex){
406        CalBddGetThenBdd(f1, f1);
407      }
408      if(CalBddGetBddIndex(bddManager, g1) == hIndex){
409        CalBddGetThenBdd(g1, g1);
410      }
411      if(CalBddIsEqual(f1, g1)){
412        if(hIndex > CalBddGetBddIndex(bddManager, f1)){
413          CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f1)], 
414              f1, CalBddOne(bddManager), &result);
415        }
416        else{
417          result = f1;
418        }
419      }
420      else if(hIndex < CalBddGetBddIndex(bddManager, f1) &&
421          hIndex < CalBddGetBddIndex(bddManager, g1)){
422        bddId = bddManager->indexToId[hIndex];
423        if(!CalUniqueTableForIdFindOrAdd(bddManager, 
424            bddManager->uniqueTable[bddId], f1, g1, &result)){
425          CalBddIcrRefCount(f1);
426          CalBddIcrRefCount(g1);
427        }
428      }
429      else{
430        CalBddGetMinId2(bddManager, f1, g1, bddId);
431        CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId], f1, g1, &result);
432      }
433      CalBddIcrRefCount(result);
434      CalRequestNodePutThenRequest(requestNode, result);
435      /* right cofactor */
436      if(CalBddGetBddIndex(bddManager, f2) == hIndex){
437        CalBddGetThenBdd(f2, f2);
438      }
439      if(CalBddGetBddIndex(bddManager, g2) == hIndex){
440        CalBddGetThenBdd(g2, g2);
441      }
442      if(CalBddIsEqual(f2, g2)){
443        if(hIndex > CalBddGetBddIndex(bddManager, f2)){
444          CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f2)], 
445              f2, CalBddOne(bddManager), &result);
446        }
447        else{
448          result = f2;
449        }
450      }
451      else if(hIndex < CalBddGetBddIndex(bddManager, f2) &&
452          hIndex < CalBddGetBddIndex(bddManager, g2)){
453        bddId = bddManager->indexToId[hIndex];
454        if(!CalUniqueTableForIdFindOrAdd(bddManager, 
455            bddManager->uniqueTable[bddId], f2, g2, &result)){
456          CalBddIcrRefCount(f2);
457          CalBddIcrRefCount(g2);
458        }
459      }
460      else{
461        CalBddGetMinId2(bddManager, f2, g2, bddId);
462        CalHashTableFindOrAdd(reqQueForSwapVarsPlus[bddId], f2, g2, &result);
463      }
464      CalBddIcrRefCount(result);
465      CalRequestNodePutElseRequest(requestNode, result);
466    }
467  }
468}
469
470/**Function********************************************************************
471
472  Synopsis    [required]
473
474  Description [optional]
475
476  SideEffects [required]
477
478  SeeAlso     [optional]
479
480******************************************************************************/
481static void
482CalHashTableSwapVarsMinusApply(
483  Cal_BddManager_t * bddManager,
484  CalHashTable_t * hashTable,
485  Cal_BddIndex_t  hIndex,
486  CalHashTable_t ** reqQueForSwapVars,
487  CalHashTable_t ** reqQueForSwapVarsPlus,
488  CalHashTable_t ** reqQueForSwapVarsMinus,
489  CalHashTable_t ** reqQueForCompose)
490{
491  int i, numBins = hashTable->numBins;
492  CalBddNode_t **bins = hashTable->bins;
493  CalRequestNode_t *requestNode;
494  Cal_BddId_t bddId;
495  Cal_Bdd_t f1, f2, g1, g2;
496  Cal_Bdd_t result;
497
498  for(i = 0; i < numBins; i++){
499    for(requestNode = bins[i];
500        requestNode != Cal_Nil(CalRequestNode_t);
501        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
502      CalRequestNodeGetCofactors(bddManager, requestNode, f1, f2, g1, g2);
503      /* left cofactor */ 
504      if(CalBddGetBddIndex(bddManager, f1) == hIndex){
505        CalBddGetElseBdd(f1, f1);
506      }
507      if(CalBddGetBddIndex(bddManager, g1) == hIndex){
508        CalBddGetElseBdd(g1, g1);
509      }
510      if(CalBddIsEqual(f1, g1)){
511        if(hIndex > CalBddGetBddIndex(bddManager, f1)){
512          CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f1)], 
513              f1, CalBddZero(bddManager), &result);
514        }
515        else{
516          result = f1;
517        }
518      }
519      else if(hIndex < CalBddGetBddIndex(bddManager, f1) &&
520          hIndex < CalBddGetBddIndex(bddManager, g1)){
521        bddId = bddManager->indexToId[hIndex];
522        if(!CalUniqueTableForIdFindOrAdd(bddManager,
523            bddManager->uniqueTable[bddId], f1, g1, &result)){
524          CalBddIcrRefCount(f1);
525          CalBddIcrRefCount(g1);
526        }
527      }
528      else{
529        CalBddGetMinId2(bddManager, f1, g1, bddId);
530        CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId], f1, g1, &result);
531      }
532      CalBddIcrRefCount(result);
533      CalRequestNodePutThenRequest(requestNode, result);
534      /* right cofactor */
535      if(CalBddGetBddIndex(bddManager, f2) == hIndex){
536        CalBddGetElseBdd(f2, f2);
537      }
538      if(CalBddGetBddIndex(bddManager, g2) == hIndex){
539        CalBddGetElseBdd(g2, g2);
540      }
541      if(CalBddIsEqual(f2, g2)){
542        if(hIndex > CalBddGetBddIndex(bddManager, f2)){
543          CalHashTableFindOrAdd(reqQueForCompose[CalBddGetBddId(f2)], 
544              f2, CalBddZero(bddManager), &result);
545        }
546        else{
547          result = f2;
548        }
549      }
550      else if(hIndex < CalBddGetBddIndex(bddManager, f2) &&
551          hIndex < CalBddGetBddIndex(bddManager, g2)){
552        bddId = bddManager->indexToId[hIndex];
553        if(!CalUniqueTableForIdFindOrAdd(bddManager, 
554            bddManager->uniqueTable[bddId], f2, g2, &result)){
555          CalBddIcrRefCount(f2);
556          CalBddIcrRefCount(g2);
557        }
558      }
559      else{
560        CalBddGetMinId2(bddManager, f2, g2, bddId);
561        CalHashTableFindOrAdd(reqQueForSwapVarsMinus[bddId], f2, g2, &result);
562      }
563      CalBddIcrRefCount(result);
564      CalRequestNodePutElseRequest(requestNode, result);
565    }
566  }
567}
568
569
570
571
572
573
574
575
576
577
578
579
580
581
Note: See TracBrowser for help on using the repository browser.