source: vis_dev/glu-2.3/src/cuBdd/cuddAddFind.c@ 104

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

library glu 2.3
File size: 9.0 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [cuddAddFind.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions to find maximum and minimum in an ADD and to
8 extract the i-th bit.]
9
10 Description [External procedures included in this module:
11 <ul>
12 <li> Cudd_addFindMax()
13 <li> Cudd_addFindMin()
14 <li> Cudd_addIthBit()
15 </ul>
16 Static functions included in this module:
17 <ul>
18 <li> addDoIthBit()
19 </ul>]
20
21 Author [Fabio Somenzi]
22
23 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
24
25 All rights reserved.
26
27 Redistribution and use in source and binary forms, with or without
28 modification, are permitted provided that the following conditions
29 are met:
30
31 Redistributions of source code must retain the above copyright
32 notice, this list of conditions and the following disclaimer.
33
34 Redistributions in binary form must reproduce the above copyright
35 notice, this list of conditions and the following disclaimer in the
36 documentation and/or other materials provided with the distribution.
37
38 Neither the name of the University of Colorado nor the names of its
39 contributors may be used to endorse or promote products derived from
40 this software without specific prior written permission.
41
42 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
43 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
44 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
45 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
46 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
47 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
48 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
49 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
50 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
51 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
52 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
53 POSSIBILITY OF SUCH DAMAGE.]
54
55******************************************************************************/
56
57#include "util.h"
58#include "cuddInt.h"
59
60/*---------------------------------------------------------------------------*/
61/* Constant declarations */
62/*---------------------------------------------------------------------------*/
63
64
65/*---------------------------------------------------------------------------*/
66/* Stucture declarations */
67/*---------------------------------------------------------------------------*/
68
69
70/*---------------------------------------------------------------------------*/
71/* Type declarations */
72/*---------------------------------------------------------------------------*/
73
74
75/*---------------------------------------------------------------------------*/
76/* Variable declarations */
77/*---------------------------------------------------------------------------*/
78
79#ifndef lint
80static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.8 2004/08/13 18:04:45 fabio Exp $";
81#endif
82
83
84/*---------------------------------------------------------------------------*/
85/* Macro declarations */
86/*---------------------------------------------------------------------------*/
87
88#ifdef __cplusplus
89extern "C" {
90#endif
91
92/**AutomaticStart*************************************************************/
93
94/*---------------------------------------------------------------------------*/
95/* Static function prototypes */
96/*---------------------------------------------------------------------------*/
97
98static DdNode * addDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
99
100/**AutomaticEnd***************************************************************/
101
102#ifdef __cplusplus
103}
104#endif
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions */
108/*---------------------------------------------------------------------------*/
109
110/**Function********************************************************************
111
112 Synopsis [Finds the maximum discriminant of f.]
113
114 Description [Returns a pointer to a constant ADD.]
115
116 SideEffects [None]
117
118******************************************************************************/
119DdNode *
120Cudd_addFindMax(
121 DdManager * dd,
122 DdNode * f)
123{
124 DdNode *t, *e, *res;
125
126 statLine(dd);
127 if (cuddIsConstant(f)) {
128 return(f);
129 }
130
131 res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
132 if (res != NULL) {
133 return(res);
134 }
135
136 t = Cudd_addFindMax(dd,cuddT(f));
137 if (t == DD_PLUS_INFINITY(dd)) return(t);
138
139 e = Cudd_addFindMax(dd,cuddE(f));
140
141 res = (cuddV(t) >= cuddV(e)) ? t : e;
142
143 cuddCacheInsert1(dd,Cudd_addFindMax,f,res);
144
145 return(res);
146
147} /* end of Cudd_addFindMax */
148
149
150/**Function********************************************************************
151
152 Synopsis [Finds the minimum discriminant of f.]
153
154 Description [Returns a pointer to a constant ADD.]
155
156 SideEffects [None]
157
158******************************************************************************/
159DdNode *
160Cudd_addFindMin(
161 DdManager * dd,
162 DdNode * f)
163{
164 DdNode *t, *e, *res;
165
166 statLine(dd);
167 if (cuddIsConstant(f)) {
168 return(f);
169 }
170
171 res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
172 if (res != NULL) {
173 return(res);
174 }
175
176 t = Cudd_addFindMin(dd,cuddT(f));
177 if (t == DD_MINUS_INFINITY(dd)) return(t);
178
179 e = Cudd_addFindMin(dd,cuddE(f));
180
181 res = (cuddV(t) <= cuddV(e)) ? t : e;
182
183 cuddCacheInsert1(dd,Cudd_addFindMin,f,res);
184
185 return(res);
186
187} /* end of Cudd_addFindMin */
188
189
190/**Function********************************************************************
191
192 Synopsis [Extracts the i-th bit from an ADD.]
193
194 Description [Produces an ADD from another ADD by replacing all
195 discriminants whose i-th bit is equal to 1 with 1, and all other
196 discriminants with 0. The i-th bit refers to the integer
197 representation of the leaf value. If the value is has a fractional
198 part, it is ignored. Repeated calls to this procedure allow one to
199 transform an integer-valued ADD into an array of ADDs, one for each
200 bit of the leaf values. Returns a pointer to the resulting ADD if
201 successful; NULL otherwise.]
202
203 SideEffects [None]
204
205 SeeAlso [Cudd_addBddIthBit]
206
207******************************************************************************/
208DdNode *
209Cudd_addIthBit(
210 DdManager * dd,
211 DdNode * f,
212 int bit)
213{
214 DdNode *res;
215 DdNode *index;
216
217 /* Use a constant node to remember the bit, so that we can use the
218 ** global cache.
219 */
220 index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
221 if (index == NULL) return(NULL);
222 cuddRef(index);
223
224 do {
225 dd->reordered = 0;
226 res = addDoIthBit(dd, f, index);
227 } while (dd->reordered == 1);
228
229 if (res == NULL) {
230 Cudd_RecursiveDeref(dd, index);
231 return(NULL);
232 }
233 cuddRef(res);
234 Cudd_RecursiveDeref(dd, index);
235 cuddDeref(res);
236 return(res);
237
238} /* end of Cudd_addIthBit */
239
240
241/*---------------------------------------------------------------------------*/
242/* Definition of internal functions */
243/*---------------------------------------------------------------------------*/
244
245
246/*---------------------------------------------------------------------------*/
247/* Definition of static functions */
248/*---------------------------------------------------------------------------*/
249
250
251/**Function********************************************************************
252
253 Synopsis [Performs the recursive step for Cudd_addIthBit.]
254
255 Description [Performs the recursive step for Cudd_addIthBit.
256 Returns a pointer to the BDD if successful; NULL otherwise.]
257
258 SideEffects [None]
259
260 SeeAlso []
261
262******************************************************************************/
263static DdNode *
264addDoIthBit(
265 DdManager * dd,
266 DdNode * f,
267 DdNode * index)
268{
269 DdNode *res, *T, *E;
270 DdNode *fv, *fvn;
271 int mask, value;
272 int v;
273
274 statLine(dd);
275 /* Check terminal case. */
276 if (cuddIsConstant(f)) {
277 mask = 1 << ((int) cuddV(index));
278 value = (int) cuddV(f);
279 return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
280 }
281
282 /* Check cache. */
283 res = cuddCacheLookup2(dd,addDoIthBit,f,index);
284 if (res != NULL) return(res);
285
286 /* Recursive step. */
287 v = f->index;
288 fv = cuddT(f); fvn = cuddE(f);
289
290 T = addDoIthBit(dd,fv,index);
291 if (T == NULL) return(NULL);
292 cuddRef(T);
293
294 E = addDoIthBit(dd,fvn,index);
295 if (E == NULL) {
296 Cudd_RecursiveDeref(dd, T);
297 return(NULL);
298 }
299 cuddRef(E);
300
301 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
302 if (res == NULL) {
303 Cudd_RecursiveDeref(dd, T);
304 Cudd_RecursiveDeref(dd, E);
305 return(NULL);
306 }
307 cuddDeref(T);
308 cuddDeref(E);
309
310 /* Store result. */
311 cuddCacheInsert2(dd,addDoIthBit,f,index,res);
312
313 return(res);
314
315} /* end of addDoIthBit */
316
Note: See TracBrowser for help on using the repository browser.