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 "misc/util/util_hack.h"
58 #include "cuddInt.h"
59
60 ABC_NAMESPACE_IMPL_START
61
62
63
64 /*---------------------------------------------------------------------------*/
65 /* Constant declarations */
66 /*---------------------------------------------------------------------------*/
67
68
69 /*---------------------------------------------------------------------------*/
70 /* Stucture declarations */
71 /*---------------------------------------------------------------------------*/
72
73
74 /*---------------------------------------------------------------------------*/
75 /* Type declarations */
76 /*---------------------------------------------------------------------------*/
77
78
79 /*---------------------------------------------------------------------------*/
80 /* Variable declarations */
81 /*---------------------------------------------------------------------------*/
82
83 #ifndef lint
84 static char rcsid[] DD_UNUSED = "$Id: cuddAddFind.c,v 1.8 2004/08/13 18:04:45 fabio Exp $";
85 #endif
86
87
88 /*---------------------------------------------------------------------------*/
89 /* Macro declarations */
90 /*---------------------------------------------------------------------------*/
91
92 /**AutomaticStart*************************************************************/
93
94 /*---------------------------------------------------------------------------*/
95 /* Static function prototypes */
96 /*---------------------------------------------------------------------------*/
97
98 static DdNode * addDoIthBit (DdManager *dd, DdNode *f, DdNode *index);
99
100 /**AutomaticEnd***************************************************************/
101
102 /*---------------------------------------------------------------------------*/
103 /* Definition of exported functions */
104 /*---------------------------------------------------------------------------*/
105
106 /**Function********************************************************************
107
108 Synopsis [Finds the maximum discriminant of f.]
109
110 Description [Returns a pointer to a constant ADD.]
111
112 SideEffects [None]
113
114 ******************************************************************************/
115 DdNode *
Cudd_addFindMax(DdManager * dd,DdNode * f)116 Cudd_addFindMax(
117 DdManager * dd,
118 DdNode * f)
119 {
120 DdNode *t, *e, *res;
121
122 statLine(dd);
123 if (cuddIsConstant(f)) {
124 return(f);
125 }
126
127 res = cuddCacheLookup1(dd,Cudd_addFindMax,f);
128 if (res != NULL) {
129 return(res);
130 }
131
132 t = Cudd_addFindMax(dd,cuddT(f));
133 if (t == DD_PLUS_INFINITY(dd)) return(t);
134
135 e = Cudd_addFindMax(dd,cuddE(f));
136
137 res = (cuddV(t) >= cuddV(e)) ? t : e;
138
139 cuddCacheInsert1(dd,Cudd_addFindMax,f,res);
140
141 return(res);
142
143 } /* end of Cudd_addFindMax */
144
145
146 /**Function********************************************************************
147
148 Synopsis [Finds the minimum discriminant of f.]
149
150 Description [Returns a pointer to a constant ADD.]
151
152 SideEffects [None]
153
154 ******************************************************************************/
155 DdNode *
Cudd_addFindMin(DdManager * dd,DdNode * f)156 Cudd_addFindMin(
157 DdManager * dd,
158 DdNode * f)
159 {
160 DdNode *t, *e, *res;
161
162 statLine(dd);
163 if (cuddIsConstant(f)) {
164 return(f);
165 }
166
167 res = cuddCacheLookup1(dd,Cudd_addFindMin,f);
168 if (res != NULL) {
169 return(res);
170 }
171
172 t = Cudd_addFindMin(dd,cuddT(f));
173 if (t == DD_MINUS_INFINITY(dd)) return(t);
174
175 e = Cudd_addFindMin(dd,cuddE(f));
176
177 res = (cuddV(t) <= cuddV(e)) ? t : e;
178
179 cuddCacheInsert1(dd,Cudd_addFindMin,f,res);
180
181 return(res);
182
183 } /* end of Cudd_addFindMin */
184
185
186 /**Function********************************************************************
187
188 Synopsis [Extracts the i-th bit from an ADD.]
189
190 Description [Produces an ADD from another ADD by replacing all
191 discriminants whose i-th bit is equal to 1 with 1, and all other
192 discriminants with 0. The i-th bit refers to the integer
193 representation of the leaf value. If the value is has a fractional
194 part, it is ignored. Repeated calls to this procedure allow one to
195 transform an integer-valued ADD into an array of ADDs, one for each
196 bit of the leaf values. Returns a pointer to the resulting ADD if
197 successful; NULL otherwise.]
198
199 SideEffects [None]
200
201 SeeAlso [Cudd_addBddIthBit]
202
203 ******************************************************************************/
204 DdNode *
Cudd_addIthBit(DdManager * dd,DdNode * f,int bit)205 Cudd_addIthBit(
206 DdManager * dd,
207 DdNode * f,
208 int bit)
209 {
210 DdNode *res;
211 DdNode *index;
212
213 /* Use a constant node to remember the bit, so that we can use the
214 ** global cache.
215 */
216 index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
217 if (index == NULL) return(NULL);
218 cuddRef(index);
219
220 do {
221 dd->reordered = 0;
222 res = addDoIthBit(dd, f, index);
223 } while (dd->reordered == 1);
224
225 if (res == NULL) {
226 Cudd_RecursiveDeref(dd, index);
227 return(NULL);
228 }
229 cuddRef(res);
230 Cudd_RecursiveDeref(dd, index);
231 cuddDeref(res);
232 return(res);
233
234 } /* end of Cudd_addIthBit */
235
236
237 /*---------------------------------------------------------------------------*/
238 /* Definition of internal functions */
239 /*---------------------------------------------------------------------------*/
240
241
242 /*---------------------------------------------------------------------------*/
243 /* Definition of static functions */
244 /*---------------------------------------------------------------------------*/
245
246
247 /**Function********************************************************************
248
249 Synopsis [Performs the recursive step for Cudd_addIthBit.]
250
251 Description [Performs the recursive step for Cudd_addIthBit.
252 Returns a pointer to the BDD if successful; NULL otherwise.]
253
254 SideEffects [None]
255
256 SeeAlso []
257
258 ******************************************************************************/
259 static DdNode *
addDoIthBit(DdManager * dd,DdNode * f,DdNode * index)260 addDoIthBit(
261 DdManager * dd,
262 DdNode * f,
263 DdNode * index)
264 {
265 DdNode *res, *T, *E;
266 DdNode *fv, *fvn;
267 int mask, value;
268 int v;
269
270 statLine(dd);
271 /* Check terminal case. */
272 if (cuddIsConstant(f)) {
273 mask = 1 << ((int) cuddV(index));
274 value = (int) cuddV(f);
275 return((value & mask) == 0 ? DD_ZERO(dd) : DD_ONE(dd));
276 }
277
278 /* Check cache. */
279 res = cuddCacheLookup2(dd,addDoIthBit,f,index);
280 if (res != NULL) return(res);
281
282 /* Recursive step. */
283 v = f->index;
284 fv = cuddT(f); fvn = cuddE(f);
285
286 T = addDoIthBit(dd,fv,index);
287 if (T == NULL) return(NULL);
288 cuddRef(T);
289
290 E = addDoIthBit(dd,fvn,index);
291 if (E == NULL) {
292 Cudd_RecursiveDeref(dd, T);
293 return(NULL);
294 }
295 cuddRef(E);
296
297 res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
298 if (res == NULL) {
299 Cudd_RecursiveDeref(dd, T);
300 Cudd_RecursiveDeref(dd, E);
301 return(NULL);
302 }
303 cuddDeref(T);
304 cuddDeref(E);
305
306 /* Store result. */
307 cuddCacheInsert2(dd,addDoIthBit,f,index,res);
308
309 return(res);
310
311 } /* end of addDoIthBit */
312
313
314 ABC_NAMESPACE_IMPL_END
315
316
317