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

Last change on this file since 13 was 13, checked in by cecile, 13 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.