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

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

library glu 2.3
File size: 18.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calAssociation.c]
4
5  PackageName [cal]
6
7  Synopsis    [Contains the routines related to the variable association.]
8
9  Description [optional]
10
11  SeeAlso     [optional]
12
13  Author      [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu)
14               Jagesh Sanghavi  (sanghavi@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: calAssociation.c,v 1.1.1.3 1998/05/04 00:58:50 hsv Exp $]
37
38******************************************************************************/
39
40#include "calInt.h"
41
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47
48/*---------------------------------------------------------------------------*/
49/* Type declarations                                                         */
50/*---------------------------------------------------------------------------*/
51
52
53/*---------------------------------------------------------------------------*/
54/* Stucture declarations                                                     */
55/*---------------------------------------------------------------------------*/
56
57
58/*---------------------------------------------------------------------------*/
59/* Variable declarations                                                     */
60/*---------------------------------------------------------------------------*/
61
62
63/*---------------------------------------------------------------------------*/
64/* Macro declarations                                                        */
65/*---------------------------------------------------------------------------*/
66
67
68/**AutomaticStart*************************************************************/
69
70/*---------------------------------------------------------------------------*/
71/* Static function prototypes                                                */
72/*---------------------------------------------------------------------------*/
73
74static int AssociationIsEqual(Cal_BddManager_t * bddManager, Cal_Bdd_t * p, Cal_Bdd_t * q);
75static int CheckAssoc(Cal_BddManager_t *bddManager, Cal_Bdd *assocInfo, int pairs);
76
77/**AutomaticEnd***************************************************************/
78
79
80/*---------------------------------------------------------------------------*/
81/* Definition of exported functions                                          */
82/*---------------------------------------------------------------------------*/
83/**Function********************************************************************
84
85  Synopsis    [Creates or finds a variable association.]
86
87  Description [Creates or finds a variable association. The association is
88  specified by associationInfo, which is a an array of BDD with
89  Cal_BddNull(bddManager) as the end marker. If pairs is 0, the array is
90  assumed to be an array of variables. In this case, each variable is paired
91  with constant BDD one. Such an association may viewed as specifying a set
92  of variables for use with routines such as Cal_BddExists. If pair is not 0,
93  then the even numbered array elements should be variables and the odd numbered
94  elements should be the BDDs which they are mapped to. In both cases, the
95  return value is an integer identifier for this association. If the given
96  association is equivalent to one which already exists, the same identifier
97  is used for both, and the reference count of the association is increased by
98  one.]
99
100  SideEffects [None]
101
102  SeeAlso     [Cal_AssociationQuit]
103
104******************************************************************************/
105int
106Cal_AssociationInit(Cal_BddManager bddManager,
107                    Cal_Bdd *associationInfoUserBdds,
108                    int  pairs)
109{
110  int i, numAssociations;
111  CalAssociation_t *p, **q;
112  Cal_Bdd_t f;
113  Cal_Bdd_t *varAssociation;
114  Cal_BddId_t j;
115  long last;
116  Cal_Bdd_t *associationInfo;
117 
118  if (!CheckAssoc(bddManager, associationInfoUserBdds, pairs)){
119    return (-1);
120  }
121
122
123/* First count the number of elements */
124  for (i=0; associationInfoUserBdds[i]; i++);
125  if (pairs)  numAssociations = i/2;
126  else numAssociations = i;
127  associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
128  for (j=0; j < i; j++){
129    associationInfo[j] =
130        CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
131  }
132  associationInfo[j] = bddManager->bddNull;
133
134 
135  varAssociation = Cal_MemAlloc(Cal_Bdd_t, bddManager->maxNumVars+1);
136  for(i = 0; i <= bddManager->maxNumVars; i++){
137    varAssociation[i] = bddManager->bddNull;
138  }
139
140 
141  if(pairs){
142    for(i = 0; i < numAssociations; i++){
143      f = associationInfo[(i<<1)];
144      varAssociation[CalBddGetBddId(f)] = associationInfo[(i<<1)+1];
145    }
146  }
147  else{
148    for(i = 0; i < numAssociations; i++){
149      f=associationInfo[i];
150      varAssociation[CalBddGetBddId(f)] = CalBddOne(bddManager);
151    }
152  }
153  /* Check for existence. */
154  for(p = bddManager->associationList; p; p = p->next){
155    if(AssociationIsEqual(bddManager, p->varAssociation, varAssociation)){
156        Cal_MemFree(varAssociation);
157    Cal_MemFree(associationInfo);
158        p->refCount++;
159        return (p->id);
160    }
161  }
162  /* Find the first unused id. */
163  for(q = &bddManager->associationList, p = *q, i = 0;
164      p && p->id == i; q = &p->next, p = *q, ++i){
165  }
166  /*p = Cal_MemAlloc(CalAssociation_t, 1);*/
167  /*p = CAL_BDD_NEW_REC(bddManager, CalAssociation_t);*/
168  p = Cal_MemAlloc(CalAssociation_t, 1);
169  p->id = i;
170  p->next = *q;
171  *q = p;
172  p->varAssociation = varAssociation;
173  last = -1;
174  if(pairs){
175    for(i = 0; i < numAssociations; i++){
176      f = associationInfo[(i<<1)];
177      j = CalBddGetBddIndex(bddManager, f);
178      if((long)j > last){
179          last = j;
180      }
181    }
182  }
183  else{
184    for(i = 0; i < numAssociations; i++){
185      f = associationInfo[i];
186      j = CalBddGetBddIndex(bddManager, f);
187      if((long)j > last){
188          last = j;
189      }
190    }
191  }
192  p->lastBddIndex = last;
193  p->refCount = 1;
194  /* Protect BDDs in the association. */
195  if(pairs){
196    for(i = 0; i < numAssociations; i++){
197      f = associationInfo[(i<<1)+1];
198      CalBddIcrRefCount(f);
199    }
200  }
201  Cal_MemFree(associationInfo);
202  return p->id;
203}
204
205
206/**Function********************************************************************
207
208  Synopsis    [Deletes the variable association given by id]
209
210  Description [Decrements the reference count of the variable association with
211  identifier id, and frees it if the reference count becomes zero.]
212
213  SideEffects [None]
214
215  SeeAlso     [Cal_AssociationInit]
216
217******************************************************************************/
218void
219Cal_AssociationQuit(Cal_BddManager bddManager, int  associationId)
220{
221  Cal_BddId_t i;
222  Cal_Bdd_t f;
223  CalAssociation_t *p, **q;
224
225  if(bddManager->currentAssociation->id == associationId){
226    bddManager->currentAssociation = bddManager->tempAssociation;
227  }
228  for(q = &bddManager->associationList, p = *q; p; q = &p->next, p = *q){
229    if(p->id == associationId){
230      p->refCount--;
231      if(!p->refCount){
232        /* Unprotect the BDDs in the association. */
233        for(i = 1; i <= bddManager->numVars; i++){
234          f = p->varAssociation[i];
235          if(!CalBddIsBddNull(bddManager, f)){
236            CalBddDcrRefCount(f);
237          }
238        }
239        *q = p->next;
240        Cal_MemFree(p->varAssociation);
241        /*CAL_BDD_FREE_REC(bddManager, p, CalAssociation_t);*/
242        Cal_MemFree(p);
243        CalCacheTableTwoFlushAssociationId(bddManager, associationId);
244      }
245      return;
246    }
247  }
248  CalBddWarningMessage("Cal_AssociationQuit: no association with specified ID");
249}
250
251/**Function********************************************************************
252
253  Synopsis    [Sets the current variable association to the one given by id and
254  returns the ID of the old association.]
255
256  Description [Sets the current variable association to the one given by id and
257  returns the ID of the old association.  An id of -1 indicates the temporary
258  association]
259
260  SideEffects [None]
261
262******************************************************************************/
263int
264Cal_AssociationSetCurrent(Cal_BddManager bddManager, int  associationId)
265{
266  int oldAssociationId;
267  CalAssociation_t *p;
268
269  oldAssociationId = bddManager->currentAssociation->id;
270  if(associationId != -1){
271    for(p = bddManager->associationList; p; p = p->next){
272      if(p->id == associationId){
273        bddManager->currentAssociation = p;
274        return (oldAssociationId);
275      }
276    }
277    CalBddWarningMessage(
278        "Cal_AssociationSetCurrent: no variable association with specified ID.\n May have been discarded during dynamic reordering.");
279  }
280  bddManager->currentAssociation = bddManager->tempAssociation;
281  return oldAssociationId;
282}
283
284
285/**Function********************************************************************
286
287  Synopsis    [Adds to the temporary variable association.]
288
289  Description [Pairs is 0 if the information represents only a list of
290  variables rather than a full association.]
291
292  SideEffects [None]
293
294******************************************************************************/
295void
296Cal_TempAssociationAugment(Cal_BddManager bddManager,
297                           Cal_Bdd *associationInfoUserBdds,
298                           int  pairs)
299{
300  int i, j, numAssociations;
301  Cal_Bdd_t f;
302  long last;
303  Cal_Bdd_t *associationInfo;
304 
305  if (CheckAssoc(bddManager, associationInfoUserBdds, pairs) == 0) {
306    return;
307  }
308
309  /*while (associationInfoUserBdds[i++]);*/
310  for (i=0; associationInfoUserBdds[i]; i++);
311  if (pairs) numAssociations = i/2;
312  else numAssociations = i;
313  associationInfo = Cal_MemAlloc(Cal_Bdd_t, i+1);
314  for (j=0; j < i; j++){
315    associationInfo[j] =
316        CalBddGetInternalBdd(bddManager,associationInfoUserBdds[j]);
317  }
318  associationInfo[j] = bddManager->bddNull;
319 
320  last = bddManager->tempAssociation->lastBddIndex;
321  if(pairs){
322    for(i = 0; i < numAssociations; i++){
323      f = associationInfo[(i<<1)];
324      j = CalBddGetBddId(f);
325      if(bddManager->idToIndex[j] > last){
326        last = bddManager->idToIndex[j];
327      }
328      f = bddManager->tempAssociation->varAssociation[j];
329      if(!CalBddIsBddNull(bddManager, f)){
330        CalBddDcrRefCount(f);
331      }
332      f = associationInfo[(i<<1)+1];
333      bddManager->tempAssociation->varAssociation[j] = f;
334      /* Protect BDDs in the association. */
335      CalBddIcrRefCount(f);
336    }
337  }
338  else{
339    for(i = 0; i < numAssociations; i++){
340      f = associationInfo[i];
341      j = CalBddGetBddId(f);
342      if(bddManager->idToIndex[j] > last){
343        last = bddManager->idToIndex[j];
344      }
345      f = bddManager->tempAssociation->varAssociation[j];
346      if(!CalBddIsBddNull(bddManager, f)){
347        CalBddDcrRefCount(f);
348      }
349      bddManager->tempAssociation->varAssociation[j] = CalBddOne(bddManager);
350    } 
351  }
352  bddManager->tempAssociation->lastBddIndex = last;
353  Cal_MemFree(associationInfo);
354}
355
356
357
358/**Function********************************************************************
359
360  Synopsis    [Sets the temporary variable association.]
361 
362  Description [Pairs is 0 if the information represents only a list of
363  variables rather than a full association.]
364
365  SideEffects [None]
366
367******************************************************************************/
368void
369Cal_TempAssociationInit(Cal_BddManager bddManager,
370                        Cal_Bdd *associationInfoUserBdds,
371                        int  pairs)
372{
373  long i;
374  Cal_Bdd_t f;
375
376  /* Clean up old temporary association. */
377  for(i = 1; i <= bddManager->numVars; i++){
378    f = bddManager->tempAssociation->varAssociation[i];
379    if(!CalBddIsBddNull(bddManager, f)){
380      CalBddDcrRefCount(f);
381      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
382    }
383  }
384  bddManager->tempAssociation->lastBddIndex = -1;
385  Cal_TempAssociationAugment(bddManager, associationInfoUserBdds, pairs);
386}
387
388/**Function********************************************************************
389
390  Synopsis    [Cleans up temporary association]
391
392  Description [Cleans up temporary associationoptional]
393
394  SideEffects [None]
395
396******************************************************************************/
397void
398Cal_TempAssociationQuit(Cal_BddManager bddManager)
399{
400  int i;
401  Cal_Bdd_t f;
402
403  /* Clean up old temporary association. */
404  for(i = 1; i <= bddManager->numVars; i++){
405    f = bddManager->tempAssociation->varAssociation[i];
406    if(!CalBddIsBddNull(bddManager, f)){
407      CalBddDcrRefCount(f);
408      bddManager->tempAssociation->varAssociation[i] = bddManager->bddNull;
409    }
410  }
411  bddManager->tempAssociation->lastBddIndex = -1;
412}
413
414
415
416/*---------------------------------------------------------------------------*/
417/* Definition of internal functions                                          */
418/*---------------------------------------------------------------------------*/
419/**Function********************************************************************
420
421  Synopsis    [Frees the variable associations]
422
423  Description [optional]
424
425  SideEffects [required]
426
427  SeeAlso     [optional]
428
429******************************************************************************/
430void
431CalAssociationListFree(Cal_BddManager_t *  bddManager)
432{
433  CalAssociation_t *assoc, *nextAssoc;
434 
435  for(assoc = bddManager->associationList;
436      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
437    nextAssoc = assoc->next;
438    Cal_MemFree(assoc->varAssociation);
439    /*CAL_BDD_FREE_REC(bddManager, assoc, CalAssociation_t);*/
440    Cal_MemFree(assoc);
441  }
442}
443
444/**Function********************************************************************
445
446  Synopsis    [Need to be called after repacking.]
447
448  Description [optional]
449
450  SideEffects [required]
451
452  SeeAlso     [optional]
453
454******************************************************************************/
455void
456CalVarAssociationRepackUpdate(Cal_BddManager_t *  bddManager,
457                              Cal_BddId_t id)
458{
459  CalAssociation_t *assoc, *nextAssoc;
460  int i;
461 
462  for(assoc = bddManager->associationList;
463      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
464    nextAssoc = assoc->next;
465    for (i=1; i <= bddManager->numVars; i++){
466      if (CalBddGetBddId(assoc->varAssociation[i]) == id){
467        CalBddForward(assoc->varAssociation[i]);
468      }
469    }
470  }
471  /* fix temporary association */
472  assoc = bddManager->tempAssociation;
473  for (i=1; i <= bddManager->numVars; i++){
474    if (CalBddGetBddId(assoc->varAssociation[i]) == id){
475      CalBddForward(assoc->varAssociation[i]);
476    }
477  }
478}
479
480/**Function********************************************************************
481
482  Synopsis    [Checks the validity of association.]
483
484  Description [optional]
485
486  SideEffects [required]
487
488  SeeAlso     [optional]
489
490******************************************************************************/
491void
492CalCheckAssociationValidity(Cal_BddManager_t *  bddManager)
493{
494  CalAssociation_t *assoc, *nextAssoc;
495  int i;
496 
497  for(assoc = bddManager->associationList;
498      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
499    nextAssoc = assoc->next;
500    for (i=1; i <= bddManager->numVars; i++){
501      Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
502    }
503  }
504  /* temporary association */
505  assoc = bddManager->tempAssociation;
506  for (i=1; i <= bddManager->numVars; i++){
507    Cal_Assert(CalBddIsForwarded(assoc->varAssociation[i]) == 0);
508  }
509}
510
511/**Function********************************************************************
512
513  Synopsis           [required]
514
515  Description        [optional]
516
517  SideEffects        [required]
518
519  SeeAlso            [optional]
520
521******************************************************************************/
522void
523CalReorderAssociationFix(Cal_BddManager_t *bddManager)
524{
525  CalAssociation_t *assoc, *nextAssoc;
526  int i;
527 
528  for(assoc = bddManager->associationList;
529      assoc != Cal_Nil(CalAssociation_t); assoc = nextAssoc){
530    nextAssoc = assoc->next;
531    for (i=1; i <= bddManager->numVars; i++){
532        if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
533            CalBddIsForwardedTo(assoc->varAssociation[i]);
534        }
535    }
536  }
537  /* fix temporary association */
538  assoc = bddManager->tempAssociation;
539  for (i=1; i <= bddManager->numVars; i++){
540      if (CalBddGetBddId(assoc->varAssociation[i]) != CAL_BDD_NULL_ID){
541          CalBddIsForwardedTo(assoc->varAssociation[i]);
542      }
543  }
544}
545
546/*---------------------------------------------------------------------------*/
547/* Definition of static functions                                            */
548/*---------------------------------------------------------------------------*/
549
550/**Function********************************************************************
551
552  Synopsis    [Checks for equality of two associations]
553
554  Description [Checks for equality of two associations]
555
556  SideEffects [None]
557
558******************************************************************************/
559static int
560AssociationIsEqual(Cal_BddManager_t * bddManager,
561                   Cal_Bdd_t * p,
562                   Cal_Bdd_t * q)
563{
564  int i;
565  for(i = 1; i <= bddManager->maxNumVars; i++){
566    if(CalBddIsEqual(p[i], q[i]) == 0){
567      return (0);
568    }
569  }
570  return (1);
571}
572
573/**Function********************************************************************
574
575  Synopsis           [required]
576
577  Description        [optional]
578
579  SideEffects        [required]
580
581  SeeAlso            [optional]
582
583******************************************************************************/
584static int
585CheckAssoc(Cal_BddManager_t *bddManager, Cal_Bdd *assocInfo, int pairs)
586{
587  CalBddArrayPreProcessing(bddManager, assocInfo);
588  if (pairs){
589    while (assocInfo[0] && assocInfo[1]){
590      if (CalBddTypeAux(bddManager,
591                        CalBddGetInternalBdd(bddManager, assocInfo[0])) !=
592          CAL_BDD_TYPE_POSVAR){ 
593            CalBddWarningMessage("CheckAssoc: first element in pair is not a positive variable"); 
594            return (0);
595          }
596      assocInfo+=2;
597    }
598  }
599  return (1);
600}
601
Note: See TracBrowser for help on using the repository browser.