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

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

library glu 2.3
File size: 21.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddVarSubstitute.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routine for simultaneous substitution of an array of
8  variables with another array of variables.]
9
10  Description []
11
12  SeeAlso     [optional]
13
14  Author      [Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
15               Jagesh 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: calBddVarSubstitute.c,v 1.2 2002/09/10 00:27:21 fabio 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 CalHashTableSubstituteApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, int lastIndex, CalHashTable_t ** reqQueForSubstitute, unsigned short opCode);
70static void CalHashTableSubstituteReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueForITE, CalHashTable_t * uniqueTableForId, unsigned short opCode);
71
72/**AutomaticEnd***************************************************************/
73
74/*---------------------------------------------------------------------------*/
75/* Definition of exported functions                                          */
76/*---------------------------------------------------------------------------*/
77
78/**Function********************************************************************
79
80  Synopsis    [Substitute a set of variables by set of another variables.]
81
82  Description [Returns a BDD for f using the substitution defined by current
83  variable association. It is assumed that each variable is replaced
84  by another variable. For the substitution of a variable by a
85  function, use Cal_BddSubstitute instead.]
86
87  SideEffects [None]
88
89  SeeAlso     [Cal_BddSubstitute]
90
91******************************************************************************/
92Cal_Bdd
93Cal_BddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
94{
95  CalRequest_t result;
96  Cal_Bdd userResult;
97 
98  if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
99    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
100    CalAssociation_t *assoc = bddManager->currentAssociation;
101    unsigned short opCode;
102    if (assoc->id == -1){
103      opCode = bddManager->tempOpCode--;
104    }
105    else {
106      opCode = CAL_OP_VAR_SUBSTITUTE + assoc->id;
107    }
108    result = CalBddVarSubstitute(bddManager, f, opCode, assoc);
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/*---------------------------------------------------------------------------*/
122/* Definition of internal functions                                          */
123/*---------------------------------------------------------------------------*/
124
125/*---------------------------------------------------------------------------*/
126/* Definition of static functions                                            */
127/*---------------------------------------------------------------------------*/
128
129/**Function********************************************************************
130
131  Synopsis    [Substitute a set of variables by functions]
132
133  Description [Returns a BDD for f using the substitution defined by current
134  variable association. Each variable is replaced by its associated BDDs. The
135  substitution is effective simultaneously]
136
137  SideEffects [None]
138
139  SeeAlso     [Cal_BddCompose]
140
141******************************************************************************/
142Cal_Bdd_t
143CalBddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd_t f, unsigned
144                    short opCode, CalAssociation_t *assoc)
145{
146  CalRequest_t result;
147  int bddId, bddIndex, lastIndex;
148  CalHashTable_t *hashTable;
149  CalHashTable_t *uniqueTableForId;
150  CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0];
151  CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
152  Cal_BddId_t fId = CalBddGetBddId(f);
153  /*Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];*/
154  int fIndex = bddManager->idToIndex[fId];
155 
156  if (CalOpBddVarSubstitute(bddManager, f, &result)){
157    return result;
158  }
159
160  if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
161    return result;
162  }
163  CalHashTableFindOrAdd(reqQueForSubstitute[fId], f, 
164    bddManager->bddNull, &result);
165
166  /* ReqQueApply */
167  lastIndex = assoc->lastBddIndex;
168  for(bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
169    bddId = bddManager->indexToId[bddIndex];
170    hashTable = reqQueForSubstitute[bddId];
171    if(hashTable->numEntries){
172      CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 
173                                  reqQueForSubstitute, opCode);
174    }
175  }
176
177  /* ReqQueReduce */
178  for(bddIndex = bddManager->numVars - 1; bddIndex >= fIndex; bddIndex--){
179    bddId = bddManager->indexToId[bddIndex];
180    uniqueTableForId = bddManager->uniqueTable[bddId];
181    hashTable = reqQueForSubstitute[bddId];
182    if(hashTable->numEntries){
183      CalHashTableSubstituteReduce(bddManager, hashTable,
184                                   reqQueForITE, uniqueTableForId,
185                                   opCode); 
186    }
187  }
188
189  CalRequestIsForwardedTo(result);
190
191  /* ReqQueCleanUp */
192  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
193    CalHashTableCleanUp(reqQueForSubstitute[bddId]);
194  }
195  CalCacheTableTwoFixResultPointers(bddManager);
196  CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
197  return result;
198}
199
200/**Function********************************************************************
201
202  Synopsis    [required]
203
204  Description [optional]
205
206  SideEffects [required]
207
208  SeeAlso     [optional]
209
210******************************************************************************/
211int
212CalOpBddVarSubstitute(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t *
213            resultBddPtr) 
214{
215  if (bddManager->idToIndex[CalBddGetBddId(f)] >
216      bddManager->currentAssociation->lastBddIndex){ 
217    *resultBddPtr = f;
218    return 1;
219  }
220  return 0;
221}
222
223
224/**Function********************************************************************
225
226  Synopsis    [required]
227
228  Description [optional]
229
230  SideEffects [required]
231
232  SeeAlso     [optional]
233
234******************************************************************************/
235static void
236CalHashTableSubstituteApply(
237  Cal_BddManager_t * bddManager,
238  CalHashTable_t * hashTable,
239  int  lastIndex,
240  CalHashTable_t ** reqQueForSubstitute,
241  unsigned short opCode)
242{
243  int i, numBins = hashTable->numBins;
244  CalBddNode_t **bins = hashTable->bins;
245  CalRequestNode_t *requestNode;
246  Cal_BddId_t bddId;
247  /*Cal_BddIndex_t bddIndex;*/
248  int bddIndex;
249  Cal_Bdd_t f, fx, fxBar, result;
250  Cal_Bdd_t nullBdd = bddManager->bddNull;
251
252  for(i = 0; i < numBins; i++){
253    for(requestNode = bins[i];
254        requestNode != Cal_Nil(CalRequestNode_t);
255        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
256      /* Process the requestNode */
257      CalRequestNodeGetF(requestNode, f);
258      /* Process Left Cofactor */
259      CalBddGetThenBdd(f, fx);
260      bddId = CalBddGetBddId(fx);
261      bddIndex = bddManager->idToIndex[bddId];
262      if(bddIndex <= lastIndex){
263          if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
264            CalRequestIsForwardedTo(result);
265          }
266          else {
267            CalHashTableFindOrAdd(reqQueForSubstitute[bddId], fx, nullBdd, 
268                              &result);
269            CalCacheTableOneInsert(bddManager, fx, result,
270                                   opCode, 1);
271          }
272      }
273      else{
274        result = fx;
275      }
276      CalBddIcrRefCount(result);
277      CalRequestNodePutThenRequest(requestNode, result);
278      /* Process Right Cofactor */
279      CalBddGetElseBdd(f, fxBar);
280      bddId = CalBddGetBddId(fxBar);
281      bddIndex = bddManager->idToIndex[bddId];
282      if(bddIndex <= lastIndex){
283          if (CalCacheTableOneLookup(bddManager, fxBar, opCode, &result)){ 
284            CalRequestIsForwardedTo(result);
285          }
286          else {
287            CalHashTableFindOrAdd(reqQueForSubstitute[bddId], fxBar, nullBdd, 
288                              &result);
289            CalCacheTableOneInsert(bddManager, fxBar, result,
290                                   opCode, 1);
291          }
292      }
293      else{
294        result = fxBar;
295      }
296      CalBddIcrRefCount(result);
297      CalRequestNodePutElseRequest(requestNode, result);
298    }
299  }
300}
301
302/**Function********************************************************************
303
304  Synopsis    [required]
305
306  Description [optional]
307
308  SideEffects [required]
309
310  SeeAlso     [optional]
311
312******************************************************************************/
313static void
314CalHashTableSubstituteReduce(
315  Cal_BddManager_t * bddManager,
316  CalHashTable_t * hashTable,
317  CalHashTable_t ** reqQueForITE,
318  CalHashTable_t * uniqueTableForId,
319  unsigned short opCode)
320{
321  int i, numBins = hashTable->numBins;
322  CalBddNode_t **bins = hashTable->bins;
323  Cal_BddId_t varBddId = hashTable->bddId;
324  CalNodeManager_t *nodeManager = hashTable->nodeManager;
325  /*CalRequestNode_t *requestNodeList = hashTable->requestNodeList;*/
326  CalRequestNode_t *endNode = hashTable->endNode;
327  CalRequestNode_t *requestNodeListForITE = Cal_Nil(CalRequestNode_t);
328  CalRequestNode_t *requestNode, *next;
329  CalBddNode_t *bddNode;
330  Cal_Bdd_t varBdd;
331  Cal_Bdd_t thenBdd, elseBdd, result;
332  Cal_Bdd_t h;
333  Cal_BddIndex_t resultIndex, varBddIndex;
334  int minITEindex = bddManager->numVars;
335  Cal_BddRefCount_t refCount;
336  int bddId, bddIndex;
337  CalHashTable_t *hashTableForITE;
338
339  varBddIndex = bddManager->idToIndex[varBddId];
340  varBdd = bddManager->varBdds[varBddId];
341  h = bddManager->currentAssociation->varAssociation[varBddId];
342  if(!CalBddIsBddNull(bddManager, h)){
343    Cal_BddId_t hId = CalBddGetBddId(h);
344    Cal_BddIndex_t hIndex = bddManager->idToIndex[hId];
345    for(i = 0; i < numBins; i++){
346      for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
347          requestNode != Cal_Nil(CalRequestNode_t);
348          requestNode = next){
349        next = CalRequestNodeGetNextRequestNode(requestNode);
350        /* Process the requestNode */
351        CalRequestNodeGetThenRequest(requestNode, thenBdd);
352        CalRequestNodeGetElseRequest(requestNode, elseBdd);
353        CalRequestIsForwardedTo(thenBdd);
354        CalRequestIsForwardedTo(elseBdd);
355        if(CalBddIsEqual(thenBdd, elseBdd)){
356          CalBddNodeGetRefCount(requestNode, refCount);
357          CalBddAddRefCount(thenBdd, refCount - 2);
358          CalRequestNodePutThenRequest(requestNode, thenBdd);
359          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
360          endNode->nextBddNode = requestNode;
361          endNode = requestNode;
362        }
363        else{
364          if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
365             hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
366            if(CalUniqueTableForIdLookup(bddManager, bddManager->uniqueTable[hId],
367                                         thenBdd, elseBdd, &result) == 1){
368              CalBddDcrRefCount(thenBdd);
369              CalBddDcrRefCount(elseBdd);
370              CalBddNodeGetRefCount(requestNode, refCount);
371              CalBddAddRefCount(result, refCount);
372              CalRequestNodePutThenRequest(requestNode, result);
373              CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
374              endNode->nextBddNode = requestNode;
375              endNode = requestNode;
376            }
377            else if(CalBddIsOutPos(thenBdd)){
378              /* Get a node from the node manager of h */
379              CalNodeManager_t *hNodeManager =
380                  bddManager->nodeManagerArray[hId];
381              CalNodeManagerInitBddNode(hNodeManager, thenBdd, elseBdd,
382                                      Cal_Nil(CalBddNode_t), bddNode);
383              CalBddNodeGetRefCount(requestNode, refCount);
384              CalBddNodePutRefCount(bddNode, refCount);
385              CalHashTableAddDirect(bddManager->uniqueTable[hId], bddNode);
386              bddManager->numNodes++;
387              bddManager->gcCheck--;
388              CalRequestNodePutThenRequestId(requestNode, hId);
389              CalRequestNodePutThenRequestNode(requestNode, bddNode); 
390              CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
391              endNode->nextBddNode = requestNode;
392              endNode = requestNode;
393            }
394            else{
395              /* Get a node from the node manager of h */
396              CalNodeManager_t *hNodeManager =
397                  bddManager->nodeManagerArray[hId];
398              CalBddNot(thenBdd, thenBdd);
399              CalBddNot(elseBdd, elseBdd);
400              CalNodeManagerInitBddNode(hNodeManager, thenBdd, elseBdd,
401                                      Cal_Nil(CalBddNode_t), bddNode);
402              CalBddNodeGetRefCount(requestNode, refCount);
403              CalBddNodePutRefCount(bddNode, refCount);
404              CalHashTableAddDirect(bddManager->uniqueTable[hId], bddNode);
405              bddManager->numNodes++;
406              bddManager->gcCheck--;
407              CalRequestNodePutThenRequestId(requestNode, hId);
408              CalRequestNodePutThenRequestNode(requestNode,
409                                               CalBddNodeNot(bddNode));
410              CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
411              endNode->nextBddNode = requestNode;
412              endNode = requestNode;
413            }
414          }
415          else{
416            CalBddDcrRefCount(thenBdd);
417            CalBddDcrRefCount(elseBdd);
418            result = CalOpITE(bddManager, h, thenBdd, elseBdd, reqQueForITE);
419            if ((resultIndex = bddManager->idToIndex[CalBddGetBddId(result)]) < minITEindex){
420              minITEindex = resultIndex;
421            }
422            CalRequestNodePutThenRequest(requestNode, result);
423            CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
424            CalRequestNodePutNextRequestNode(requestNode,
425                                             requestNodeListForITE);
426            requestNodeListForITE = requestNode;
427          }
428        }
429      }
430    }
431  }
432  else{
433    for(i = 0; i < numBins; i++){
434      for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
435          requestNode != Cal_Nil(CalRequestNode_t);
436          requestNode = next){
437        next = CalRequestNodeGetNextRequestNode(requestNode);
438        /* Process the requestNode */
439        CalRequestNodeGetThenRequest(requestNode, thenBdd);
440        CalRequestNodeGetElseRequest(requestNode, elseBdd);
441        CalRequestIsForwardedTo(thenBdd);
442        CalRequestIsForwardedTo(elseBdd);
443        if(CalBddIsEqual(thenBdd, elseBdd)){
444          CalBddNodeGetRefCount(requestNode, refCount);
445          CalBddAddRefCount(thenBdd, refCount - 2);
446          CalRequestNodePutThenRequest(requestNode, thenBdd);
447          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
448          endNode->nextBddNode = requestNode;
449          endNode = requestNode;
450        }
451        else{
452          if(varBddIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
453             varBddIndex < CalBddGetBddIndex(bddManager, elseBdd)){
454            if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
455                                         thenBdd, elseBdd, &result) == 1){
456              CalBddDcrRefCount(thenBdd);
457              CalBddDcrRefCount(elseBdd);
458              CalBddNodeGetRefCount(requestNode, refCount);
459              CalBddAddRefCount(result, refCount);
460              CalRequestNodePutThenRequest(requestNode, result);
461              CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
462              endNode->nextBddNode = requestNode;
463              endNode = requestNode;
464            }
465            else if(CalBddIsOutPos(thenBdd)){
466              CalRequestNodePutThenRequest(requestNode, thenBdd);
467              CalRequestNodePutElseRequest(requestNode, elseBdd);
468              CalHashTableAddDirect(uniqueTableForId, requestNode);
469              bddManager->numNodes++;
470              bddManager->gcCheck--;
471            }
472            else{
473              CalBddNot(thenBdd, thenBdd);
474              CalBddNot(elseBdd, elseBdd);
475              CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd,
476                                      Cal_Nil(CalBddNode_t), bddNode);
477              CalBddNodeGetRefCount(requestNode, refCount);
478              CalBddNodePutRefCount(bddNode, refCount);
479              CalHashTableAddDirect(uniqueTableForId, bddNode);
480              bddManager->numNodes++;
481              bddManager->gcCheck--;
482              CalRequestNodePutThenRequestId(requestNode, varBddId);
483              CalRequestNodePutThenRequestNode(requestNode,
484                                               CalBddNodeNot(bddNode));
485              CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
486              endNode->nextBddNode = requestNode;
487              endNode = requestNode;
488            }
489          }
490          else{
491            CalBddDcrRefCount(thenBdd);
492            CalBddDcrRefCount(elseBdd);
493            result = CalOpITE(bddManager, varBdd, thenBdd, elseBdd, reqQueForITE);
494            if ((resultIndex = bddManager->idToIndex[CalBddGetBddId(result)]) < minITEindex){
495              minITEindex = resultIndex;
496            }
497            CalRequestNodePutThenRequest(requestNode, result);
498            CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
499            CalRequestNodePutNextRequestNode(requestNode,
500                                             requestNodeListForITE);
501            requestNodeListForITE = requestNode;
502          }
503        }
504      }
505    }
506  }
507
508  /* ITE Apply */
509  for(bddIndex = minITEindex; bddIndex < bddManager->numVars; bddIndex++){
510    bddId = bddManager->indexToId[bddIndex];
511    hashTableForITE = reqQueForITE[bddId];
512    if(hashTableForITE->numEntries){
513      CalHashTableITEApply(bddManager, hashTableForITE, reqQueForITE);
514    }
515  }
516  /* ITE Reduce */
517  for(bddIndex = bddManager->numVars - 1; bddIndex >= minITEindex; bddIndex--){
518    bddId = bddManager->indexToId[bddIndex];
519    hashTableForITE = reqQueForITE[bddId];
520    if(hashTableForITE->numEntries){
521      CalHashTableReduce(bddManager, hashTableForITE,
522          bddManager->uniqueTable[bddId]);
523    }
524  }
525   
526
527  for(requestNode = requestNodeListForITE; 
528      requestNode != Cal_Nil(CalRequestNode_t);
529      requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
530    CalRequestNodeGetThenRequest(requestNode, result);
531    CalBddNodeGetRefCount(requestNode, refCount);
532    CalRequestIsForwardedTo(result);
533    CalBddAddRefCount(result, refCount);
534    CalRequestNodePutThenRequest(requestNode, result);
535  }
536
537  endNode->nextBddNode = requestNodeListForITE;
538  hashTable->endNode = endNode;
539  /* ITE Cleanup */
540  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
541    CalHashTableCleanUp(reqQueForITE[bddId]);
542  }
543}
544
Note: See TracBrowser for help on using the repository browser.