source: vis_dev/glu-2.3/src/calBdd/calBddSupport.c @ 26

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

library glu 2.3
File size: 8.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calBddSupport.c]
4
5  PackageName [cal]
6
7  Synopsis    [Routines related to the support of a BDD.]
8             
9
10  Description [ ]
11
12  SeeAlso     [optional]
13
14  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
15               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
16               Originally written by David Long.
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: calBddSupport.c,v 1.1.1.3 1998/05/04 00:58:54 hsv Exp $]
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/* Variable declarations                                                     */
56/*---------------------------------------------------------------------------*/
57
58/*---------------------------------------------------------------------------*/
59/* Macro declarations                                                        */
60/*---------------------------------------------------------------------------*/
61
62/**AutomaticStart*************************************************************/
63
64/*---------------------------------------------------------------------------*/
65/* Static function prototypes                                                */
66/*---------------------------------------------------------------------------*/
67
68static Cal_Bdd_t * CalBddSupportStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t * support);
69static void CalBddUnmarkNodes(Cal_BddManager_t * bddManager, Cal_Bdd_t f);
70static int CalBddDependsOnStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_BddIndex_t varIndex, int mark);
71
72/**AutomaticEnd***************************************************************/
73
74/*---------------------------------------------------------------------------*/
75/* Definition of exported functions                                          */
76/*---------------------------------------------------------------------------*/
77
78/**Function********************************************************************
79
80  Name        [Cal_BddSupport]
81
82  Synopsis    [returns the support of f as a null-terminated array of variables]
83
84  Description [optional]
85
86  SideEffects [None]
87
88  SeeAlso     [optional]
89
90******************************************************************************/
91void
92Cal_BddSupport(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
93               Cal_Bdd *support)
94{
95  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
96    Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
97    Cal_Bdd_t *internalSupport = Cal_MemAlloc(Cal_Bdd_t, bddManager->numVars+1);
98    Cal_Bdd_t *end;
99    int i = 0;
100    end = CalBddSupportStep(bddManager, f, internalSupport);
101    *end = CalBddNull(bddManager);
102    CalBddUnmarkNodes(bddManager, f);
103    while (CalBddIsBddNull(bddManager, internalSupport[i]) == 0){
104      *support = CalBddGetExternalBdd(bddManager, internalSupport[i]);
105      support++;
106      i++;
107    }
108    Cal_MemFree(internalSupport);
109  }
110  *support = (Cal_Bdd) 0;
111}
112
113/**Function********************************************************************
114
115  Name        [Cal_BddDependsOn]
116
117  Synopsis    [Returns 1 if f depends on var and returns 0 otherwise.]
118
119  Description [Returns 1 if f depends on var and returns 0 otherwise.]
120
121  SideEffects [None]
122
123******************************************************************************/
124int
125Cal_BddDependsOn(Cal_BddManager bddManager, Cal_Bdd  fUserBdd,
126                 Cal_Bdd varUserBdd)
127{
128  Cal_BddIndex_t bddIndex;
129  Cal_Bdd_t f, var;
130 
131  if(CalBddPreProcessing(bddManager, 2, fUserBdd, varUserBdd)){
132    f = CalBddGetInternalBdd(bddManager, fUserBdd);
133    var = CalBddGetInternalBdd(bddManager, varUserBdd);
134    if(CalBddIsBddConst(var)){
135      return 1;
136    }
137    bddIndex = CalBddGetBddIndex(bddManager, var);
138    CalBddDependsOnStep(bddManager, f, bddIndex, 1);
139    return CalBddDependsOnStep(bddManager, f, bddIndex, 0);
140  }
141  return (0);
142}
143
144
145/*---------------------------------------------------------------------------*/
146/* Definition of internal functions                                          */
147/*---------------------------------------------------------------------------*/
148
149/*---------------------------------------------------------------------------*/
150/* Definition of static functions                                            */
151/*---------------------------------------------------------------------------*/
152
153/**Function********************************************************************
154
155  Name        [CalBddSupportStep]
156
157  Synopsis    [returns the support of f as a null-terminated array of variables]
158
159  Description [optional]
160
161  SideEffects [required]
162
163  SeeAlso     [optional]
164
165******************************************************************************/
166static Cal_Bdd_t *
167CalBddSupportStep(
168  Cal_BddManager_t * bddManager,
169  Cal_Bdd_t  f,
170  Cal_Bdd_t * support)
171{
172  Cal_Bdd_t tempBdd;
173
174  if(CalBddIsMarked(f) || CalBddIsBddConst(f)){
175    return support;
176  }
177  tempBdd = bddManager->varBdds[CalBddGetBddId(f)];
178  if(!CalBddIsMarked(tempBdd)){
179    CalBddMark(tempBdd);
180    *support = tempBdd;
181    ++support;
182  }
183  CalBddMark(f);
184  CalBddGetThenBdd(f, tempBdd);
185  support = CalBddSupportStep(bddManager, tempBdd, support);
186  CalBddGetElseBdd(f, tempBdd);
187  return CalBddSupportStep(bddManager, tempBdd, support);
188}
189
190
191/**Function********************************************************************
192
193  Name        [CalBddUnmarkNodes]
194
195  Synopsis    [recursively unmarks the nodes]
196
197  Description [optional]
198
199  SideEffects [required]
200
201  SeeAlso     [optional]
202
203******************************************************************************/
204static void
205CalBddUnmarkNodes(
206  Cal_BddManager_t * bddManager,
207  Cal_Bdd_t  f)
208{
209  Cal_Bdd_t tempBdd;
210
211  if(!CalBddIsMarked(f) || CalBddIsBddConst(f)){
212    return;
213  }
214  CalBddUnmark(f);
215  tempBdd = bddManager->varBdds[CalBddGetBddId(f)];
216  CalBddUnmark(tempBdd);
217  CalBddGetThenBdd(f, tempBdd);
218  CalBddUnmarkNodes(bddManager, tempBdd);
219  CalBddGetElseBdd(f, tempBdd);
220  CalBddUnmarkNodes(bddManager, tempBdd);
221}
222
223
224/**Function********************************************************************
225
226
227  Synopsis    [required]
228
229  Description [optional]
230
231  SideEffects [required]
232
233  SeeAlso     [optional]
234
235******************************************************************************/
236static int
237CalBddDependsOnStep(
238  Cal_BddManager_t * bddManager,
239  Cal_Bdd_t  f,
240  Cal_BddIndex_t  varIndex,
241  int  mark)
242{
243  Cal_BddIndex_t fIndex;
244  Cal_Bdd_t tempBdd;
245
246  fIndex=CalBddGetBddIndex(bddManager, f);
247  if(fIndex > varIndex){
248    return 0;
249  }
250  if(fIndex == varIndex){
251    return 1;
252  }
253  if((mark && CalBddIsMarked(f)) || (!mark && !CalBddIsMarked(f))){
254    return (0);
255  }
256  if(mark){
257    CalBddMark(f);
258  }
259  else{
260    CalBddUnmark(f);
261  }
262  CalBddGetThenBdd(f, tempBdd);
263  if(CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark)){
264    return 1;
265  }
266  CalBddGetElseBdd(f, tempBdd);
267  return CalBddDependsOnStep(bddManager, tempBdd, varIndex, mark);
268}
269
270
271
272
273
274
275
276
277
278
279
Note: See TracBrowser for help on using the repository browser.