source: vis_dev/glu-2.3/src/calBdd/calBddSubstitute.c @ 104

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

library glu 2.3
File size: 15.3 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddSubstitute.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routine for simultaneous substitution of an array of
8  variables with an array of functions.]
9
10  Description [Routine for simultaneous substitution of an array of
11  variables with an array of functions.]
12
13  SeeAlso     [optional]
14
15  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
16               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
17               ]
18  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
19  All rights reserved.
20
21  Permission is hereby granted, without written agreement and without license
22  or royalty fees, to use, copy, modify, and distribute this software and its
23  documentation for any purpose, provided that the above copyright notice and
24  the following two paragraphs appear in all copies of this software.
25
26  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
27  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
28  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
29  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30
31  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
32  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
33  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
34  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
35  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
36
37  Revision    [$Id: calBddSubstitute.c,v 1.1.1.4 1998/05/04 00:58:54 hsv Exp $]
38
39******************************************************************************/
40
41#include "calInt.h"
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Type declarations                                                         */
49/*---------------------------------------------------------------------------*/
50
51/*---------------------------------------------------------------------------*/
52/* Stucture declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55
56/*---------------------------------------------------------------------------*/
57/* Variable declarations                                                     */
58/*---------------------------------------------------------------------------*/
59
60/*---------------------------------------------------------------------------*/
61/* Macro declarations                                                        */
62/*---------------------------------------------------------------------------*/
63
64/**AutomaticStart*************************************************************/
65
66/*---------------------------------------------------------------------------*/
67/* Static function prototypes                                                */
68/*---------------------------------------------------------------------------*/
69
70static void CalHashTableSubstituteApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, int lastIndex, CalHashTable_t ** reqQueForSubstitute);
71static void CalHashTableSubstituteReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueForITE, CalHashTable_t * uniqueTableForId);
72
73/**AutomaticEnd***************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Definition of exported functions                                          */
77/*---------------------------------------------------------------------------*/
78
79/**Function********************************************************************
80
81  Synopsis    [Substitute a set of variables by functions]
82
83  Description [Returns a BDD for f using the substitution defined by current
84  variable association. Each variable is replaced by its associated BDDs. The
85  substitution is effective simultaneously]
86
87  SideEffects [None]
88
89  SeeAlso     [Cal_BddCompose]
90
91******************************************************************************/
92Cal_Bdd
93Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
94{
95  CalRequest_t result;
96  int bddId, bddIndex, lastIndex;
97  CalHashTable_t *hashTable;
98  CalHashTable_t *uniqueTableForId;
99  CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0];
100  CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
101  Cal_Bdd_t f;
102 
103  if (CalBddPreProcessing(bddManager, 1, fUserBdd) == 0){
104    return (Cal_Bdd) 0;
105  }
106  f = CalBddGetInternalBdd(bddManager, fUserBdd); 
107  if(CalBddIsBddConst(f)){
108    return CalBddGetExternalBdd(bddManager, f);
109  }
110
111  CalHashTableFindOrAdd(reqQueForSubstitute[CalBddGetBddId(f)], f, 
112    bddManager->bddNull, &result);
113
114  /* ReqQueApply */
115  lastIndex = bddManager->currentAssociation->lastBddIndex;
116  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
117    bddId = bddManager->indexToId[bddIndex];
118    hashTable = reqQueForSubstitute[bddId];
119    if(hashTable->numEntries){
120      CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 
121                                  reqQueForSubstitute);
122    }
123  }
124
125  /* ReqQueReduce */
126  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
127    bddId = bddManager->indexToId[bddIndex];
128    uniqueTableForId = bddManager->uniqueTable[bddId];
129    hashTable = reqQueForSubstitute[bddId];
130    if(hashTable->numEntries){
131      CalHashTableSubstituteReduce(bddManager, hashTable,
132                                   reqQueForITE, uniqueTableForId);
133    }
134  }
135
136  CalRequestIsForwardedTo(result);
137
138  /* ReqQueCleanUp */
139  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
140    CalHashTableCleanUp(reqQueForSubstitute[bddId]);
141  }
142
143  return CalBddGetExternalBdd(bddManager, result);
144}
145
146/*---------------------------------------------------------------------------*/
147/* Definition of internal functions                                          */
148/*---------------------------------------------------------------------------*/
149
150/*---------------------------------------------------------------------------*/
151/* Definition of static functions                                            */
152/*---------------------------------------------------------------------------*/
153
154/**Function********************************************************************
155
156  Synopsis    [required]
157
158  Description [optional]
159
160  SideEffects [required]
161
162  SeeAlso     [optional]
163
164******************************************************************************/
165static void
166CalHashTableSubstituteApply(
167  Cal_BddManager_t * bddManager,
168  CalHashTable_t * hashTable,
169  int  lastIndex,
170  CalHashTable_t ** reqQueForSubstitute)
171{
172  int i, numBins = hashTable->numBins;
173  CalBddNode_t **bins = hashTable->bins;
174  CalRequestNode_t *requestNode;
175  Cal_BddId_t bddId;
176  /*Cal_BddIndex_t bddIndex;*/
177  int bddIndex;
178  Cal_Bdd_t f, calBdd;
179  Cal_Bdd_t nullBdd = bddManager->bddNull;
180
181  for(i = 0; i < numBins; i++){
182    for(requestNode = bins[i];
183        requestNode != Cal_Nil(CalRequestNode_t);
184        requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
185      /* Process the requestNode */
186      CalRequestNodeGetF(requestNode, f);
187      /* Process Left Cofactor */
188      CalBddGetThenBdd(f, calBdd);
189      bddId = CalBddGetBddId(calBdd);
190      bddIndex = bddManager->idToIndex[bddId];
191      if(bddIndex <= lastIndex){
192        CalHashTableFindOrAdd(reqQueForSubstitute[bddId], calBdd, nullBdd, 
193            &calBdd);
194      }
195      CalBddIcrRefCount(calBdd);
196      CalRequestNodePutThenRequest(requestNode, calBdd);
197      /* Process Right Cofactor */
198      CalBddGetElseBdd(f, calBdd);
199      bddId = CalBddGetBddId(calBdd);
200      bddIndex = bddManager->idToIndex[bddId];
201      if(bddIndex <= lastIndex){
202        CalHashTableFindOrAdd(reqQueForSubstitute[bddId], calBdd, nullBdd, 
203            &calBdd);
204      }
205      CalBddIcrRefCount(calBdd);
206      CalRequestNodePutElseRequest(requestNode, calBdd);
207    }
208  }
209}
210
211/**Function********************************************************************
212
213  Synopsis    [required]
214
215  Description [optional]
216
217  SideEffects [required]
218
219  SeeAlso     [optional]
220
221******************************************************************************/
222static void
223CalHashTableSubstituteReduce(
224  Cal_BddManager_t * bddManager,
225  CalHashTable_t * hashTable,
226  CalHashTable_t ** reqQueForITE,
227  CalHashTable_t * uniqueTableForId)
228{
229  int i, numBins = hashTable->numBins;
230  CalBddNode_t **bins = hashTable->bins;
231  Cal_BddId_t varBddId = hashTable->bddId;
232  CalNodeManager_t *nodeManager = hashTable->nodeManager;
233  /*CalRequestNode_t *requestNodeList = hashTable->requestNodeList;*/
234  CalRequestNode_t *endNode = hashTable->endNode;
235  CalRequestNode_t *requestNodeListForITE = Cal_Nil(CalRequestNode_t);
236  CalRequestNode_t *requestNode, *next;
237  CalBddNode_t *bddNode;
238  Cal_Bdd_t varBdd;
239  Cal_Bdd_t thenBdd, elseBdd, result;
240  Cal_Bdd_t h;
241  Cal_BddIndex_t varBddIndex;
242  Cal_BddRefCount_t refCount;
243  int bddId, bddIndex;
244  CalHashTable_t *hashTableForITE;
245
246  varBddIndex = bddManager->idToIndex[varBddId];
247  varBdd = bddManager->varBdds[varBddId];
248  h = bddManager->currentAssociation->varAssociation[varBddId];
249  if(!CalBddIsBddNull(bddManager, h)){
250    for(i = 0; i < numBins; i++){
251      for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
252          requestNode != Cal_Nil(CalRequestNode_t);
253          requestNode = next){
254        next = CalRequestNodeGetNextRequestNode(requestNode);
255        /* Process the requestNode */
256        CalRequestNodeGetThenRequest(requestNode, thenBdd);
257        CalRequestNodeGetElseRequest(requestNode, elseBdd);
258        CalRequestIsForwardedTo(thenBdd);
259        CalRequestIsForwardedTo(elseBdd);
260        if(CalBddIsEqual(thenBdd, elseBdd)){
261          CalBddNodeGetRefCount(requestNode, refCount);
262          CalBddAddRefCount(thenBdd, refCount - 2);
263          CalRequestNodePutThenRequest(requestNode, thenBdd);
264          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
265          endNode->nextBddNode = requestNode;
266          endNode = requestNode;
267        }
268        else{
269          CalBddDcrRefCount(thenBdd);
270          CalBddDcrRefCount(elseBdd);
271          result = CalOpITE(bddManager, h, thenBdd, elseBdd, reqQueForITE);
272          CalRequestNodePutThenRequest(requestNode, result);
273          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
274          CalRequestNodePutNextRequestNode(requestNode,
275              requestNodeListForITE);
276          requestNodeListForITE = requestNode;
277        }
278      }
279    }
280  }
281  else{
282    for(i = 0; i < numBins; i++){
283      for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
284          requestNode != Cal_Nil(CalRequestNode_t);
285          requestNode = next){
286        next = CalRequestNodeGetNextRequestNode(requestNode);
287        /* Process the requestNode */
288        CalRequestNodeGetThenRequest(requestNode, thenBdd);
289        CalRequestNodeGetElseRequest(requestNode, elseBdd);
290        CalRequestIsForwardedTo(thenBdd);
291        CalRequestIsForwardedTo(elseBdd);
292        if(CalBddIsEqual(thenBdd, elseBdd)){
293          CalBddNodeGetRefCount(requestNode, refCount);
294          CalBddAddRefCount(thenBdd, refCount - 2);
295          CalRequestNodePutThenRequest(requestNode, thenBdd);
296          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
297          endNode->nextBddNode = requestNode;
298          endNode = requestNode;
299        }
300        else if(varBddIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
301            varBddIndex < CalBddGetBddIndex(bddManager, elseBdd)){
302          if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
303              thenBdd, elseBdd, &result) == 1){
304            CalBddDcrRefCount(thenBdd);
305            CalBddDcrRefCount(elseBdd);
306            CalBddNodeGetRefCount(requestNode, refCount);
307            CalBddAddRefCount(result, refCount);
308            CalRequestNodePutThenRequest(requestNode, result);
309            CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
310            endNode->nextBddNode = requestNode;
311            endNode = requestNode;
312          }
313          else if(CalBddIsOutPos(thenBdd)){
314            CalRequestNodePutThenRequest(requestNode, thenBdd);
315            CalRequestNodePutElseRequest(requestNode, elseBdd);
316            CalHashTableAddDirect(uniqueTableForId, requestNode);
317            bddManager->numNodes++;
318            bddManager->gcCheck--;
319          }
320          else{
321            CalNodeManagerAllocNode(nodeManager, bddNode);
322            CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
323            CalBddNodePutThenBddNode(bddNode,
324                CalBddGetBddNodeNot(thenBdd));
325            CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
326            CalBddNodePutElseBddNode(bddNode,
327                CalBddGetBddNodeNot(elseBdd));
328            CalBddNodeGetRefCount(requestNode, refCount);
329            CalBddNodePutRefCount(bddNode, refCount);
330            CalHashTableAddDirect(uniqueTableForId, bddNode);
331            bddManager->numNodes++;
332            bddManager->gcCheck--;
333            CalRequestNodePutThenRequestId(requestNode, varBddId);
334            CalRequestNodePutThenRequestNode(requestNode,
335                CalBddNodeNot(bddNode));
336            CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
337            endNode->nextBddNode = requestNode;
338            endNode = requestNode;
339          }
340        }
341        else{
342          CalBddDcrRefCount(thenBdd);
343          CalBddDcrRefCount(elseBdd);
344          result = CalOpITE(bddManager, varBdd, thenBdd, elseBdd, reqQueForITE);
345          CalRequestNodePutThenRequest(requestNode, result);
346          CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
347          CalRequestNodePutNextRequestNode(requestNode,
348              requestNodeListForITE);
349          requestNodeListForITE = requestNode;
350        }
351      }
352    }
353  }
354
355  /* ITE Apply */
356  for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
357    bddId = bddManager->indexToId[bddIndex];
358    hashTableForITE = reqQueForITE[bddId];
359    if(hashTableForITE->numEntries){
360      CalHashTableITEApply(bddManager, hashTableForITE, reqQueForITE);
361    }
362  }
363  /* ITE Reduce */
364  for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
365    bddId = bddManager->indexToId[bddIndex];
366    hashTableForITE = reqQueForITE[bddId];
367    if(hashTableForITE->numEntries){
368      CalHashTableReduce(bddManager, hashTableForITE,
369          bddManager->uniqueTable[bddId]);
370    }
371  }
372   
373
374  /*last = Cal_Nil(CalRequestNode_t);*/
375  for(requestNode = requestNodeListForITE; 
376      requestNode != Cal_Nil(CalRequestNode_t);
377      /*last = requestNode, */
378      requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
379    CalRequestNodeGetThenRequest(requestNode, result);
380    CalBddNodeGetRefCount(requestNode, refCount);
381    CalRequestIsForwardedTo(result);
382    CalBddAddRefCount(result, refCount);
383    CalRequestNodePutThenRequest(requestNode, result);
384  }
385
386  /*CalBddNodePutNextBddNode(endNode, requestNodeListForITE);*/
387  endNode->nextBddNode = requestNodeListForITE;
388  hashTable->endNode = endNode;
389 
390  /* ITE Cleanup */
391  for(bddId = 1; bddId <= bddManager->numVars; bddId++){
392    CalHashTableCleanUp(reqQueForITE[bddId]);
393  }
394}
395
396
397
398
399
400
401
402
403
404
405
406
407
Note: See TracBrowser for help on using the repository browser.