source: vis_dev/glu-2.3/src/cuBdd/cuddCof.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.5 KB
Line 
1/**CFile***********************************************************************
2
3 FileName [cuddCof.c]
4
5 PackageName [cudd]
6
7 Synopsis [Cofactoring functions.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_Cofactor()
12 </ul>
13 Internal procedures included in this module:
14 <ul>
15 <li> cuddGetBranches()
16 <li> cuddCheckCube()
17 <li> cuddCofactorRecur()
18 </ul>
19 ]
20
21 SeeAlso []
22
23 Author [Fabio Somenzi]
24
25 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
26
27 All rights reserved.
28
29 Redistribution and use in source and binary forms, with or without
30 modification, are permitted provided that the following conditions
31 are met:
32
33 Redistributions of source code must retain the above copyright
34 notice, this list of conditions and the following disclaimer.
35
36 Redistributions in binary form must reproduce the above copyright
37 notice, this list of conditions and the following disclaimer in the
38 documentation and/or other materials provided with the distribution.
39
40 Neither the name of the University of Colorado nor the names of its
41 contributors may be used to endorse or promote products derived from
42 this software without specific prior written permission.
43
44 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
45 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
46 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
47 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
48 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
49 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
50 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
51 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
52 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
53 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
54 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
55 POSSIBILITY OF SUCH DAMAGE.]
56
57******************************************************************************/
58
59#include "util.h"
60#include "cuddInt.h"
61
62/*---------------------------------------------------------------------------*/
63/* Constant declarations */
64/*---------------------------------------------------------------------------*/
65
66
67/*---------------------------------------------------------------------------*/
68/* Stucture declarations */
69/*---------------------------------------------------------------------------*/
70
71
72/*---------------------------------------------------------------------------*/
73/* Type declarations */
74/*---------------------------------------------------------------------------*/
75
76
77/*---------------------------------------------------------------------------*/
78/* Variable declarations */
79/*---------------------------------------------------------------------------*/
80
81#ifndef lint
82static char rcsid[] DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $";
83#endif
84
85/*---------------------------------------------------------------------------*/
86/* Macro declarations */
87/*---------------------------------------------------------------------------*/
88
89
90/**AutomaticStart*************************************************************/
91
92/*---------------------------------------------------------------------------*/
93/* Static function prototypes */
94/*---------------------------------------------------------------------------*/
95
96
97/**AutomaticEnd***************************************************************/
98
99
100/*---------------------------------------------------------------------------*/
101/* Definition of exported functions */
102/*---------------------------------------------------------------------------*/
103
104
105/**Function********************************************************************
106
107 Synopsis [Computes the cofactor of f with respect to g.]
108
109 Description [Computes the cofactor of f with respect to g; g must be
110 the BDD or the ADD of a cube. Returns a pointer to the cofactor if
111 successful; NULL otherwise.]
112
113 SideEffects [None]
114
115 SeeAlso [Cudd_bddConstrain Cudd_bddRestrict]
116
117******************************************************************************/
118DdNode *
119Cudd_Cofactor(
120 DdManager * dd,
121 DdNode * f,
122 DdNode * g)
123{
124 DdNode *res,*zero;
125
126 zero = Cudd_Not(DD_ONE(dd));
127 if (g == zero || g == DD_ZERO(dd)) {
128 (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n");
129 dd->errorCode = CUDD_INVALID_ARG;
130 return(NULL);
131 }
132 do {
133 dd->reordered = 0;
134 res = cuddCofactorRecur(dd,f,g);
135 } while (dd->reordered == 1);
136 return(res);
137
138} /* end of Cudd_Cofactor */
139
140
141/*---------------------------------------------------------------------------*/
142/* Definition of internal functions */
143/*---------------------------------------------------------------------------*/
144
145
146/**Function********************************************************************
147
148 Synopsis [Computes the children of g.]
149
150 Description []
151
152 SideEffects [None]
153
154 SeeAlso []
155
156******************************************************************************/
157void
158cuddGetBranches(
159 DdNode * g,
160 DdNode ** g1,
161 DdNode ** g0)
162{
163 DdNode *G = Cudd_Regular(g);
164
165 *g1 = cuddT(G);
166 *g0 = cuddE(G);
167 if (Cudd_IsComplement(g)) {
168 *g1 = Cudd_Not(*g1);
169 *g0 = Cudd_Not(*g0);
170 }
171
172} /* end of cuddGetBranches */
173
174
175/**Function********************************************************************
176
177 Synopsis [Checks whether g is the BDD of a cube.]
178
179 Description [Checks whether g is the BDD of a cube. Returns 1 in case
180 of success; 0 otherwise. The constant 1 is a valid cube, but all other
181 constant functions cause cuddCheckCube to return 0.]
182
183 SideEffects [None]
184
185 SeeAlso []
186
187******************************************************************************/
188int
189cuddCheckCube(
190 DdManager * dd,
191 DdNode * g)
192{
193 DdNode *g1,*g0,*one,*zero;
194
195 one = DD_ONE(dd);
196 if (g == one) return(1);
197 if (Cudd_IsConstant(g)) return(0);
198
199 zero = Cudd_Not(one);
200 cuddGetBranches(g,&g1,&g0);
201
202 if (g0 == zero) {
203 return(cuddCheckCube(dd, g1));
204 }
205 if (g1 == zero) {
206 return(cuddCheckCube(dd, g0));
207 }
208 return(0);
209
210} /* end of cuddCheckCube */
211
212
213/**Function********************************************************************
214
215 Synopsis [Performs the recursive step of Cudd_Cofactor.]
216
217 Description [Performs the recursive step of Cudd_Cofactor. Returns a
218 pointer to the cofactor if successful; NULL otherwise.]
219
220 SideEffects [None]
221
222 SeeAlso [Cudd_Cofactor]
223
224******************************************************************************/
225DdNode *
226cuddCofactorRecur(
227 DdManager * dd,
228 DdNode * f,
229 DdNode * g)
230{
231 DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r;
232 unsigned int topf,topg;
233 int comple;
234
235 statLine(dd);
236 F = Cudd_Regular(f);
237 if (cuddIsConstant(F)) return(f);
238
239 one = DD_ONE(dd);
240
241 /* The invariant g != 0 is true on entry to this procedure and is
242 ** recursively maintained by it. Therefore it suffices to test g
243 ** against one to make sure it is not constant.
244 */
245 if (g == one) return(f);
246 /* From now on, f and g are known not to be constants. */
247
248 comple = f != F;
249 r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g);
250 if (r != NULL) {
251 return(Cudd_NotCond(r,comple));
252 }
253
254 topf = dd->perm[F->index];
255 G = Cudd_Regular(g);
256 topg = dd->perm[G->index];
257
258 /* We take the cofactors of F because we are going to rely on
259 ** the fact that the cofactors of the complement are the complements
260 ** of the cofactors to better utilize the cache. Variable comple
261 ** remembers whether we have to complement the result or not.
262 */
263 if (topf <= topg) {
264 f1 = cuddT(F); f0 = cuddE(F);
265 } else {
266 f1 = f0 = F;
267 }
268 if (topg <= topf) {
269 g1 = cuddT(G); g0 = cuddE(G);
270 if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); }
271 } else {
272 g1 = g0 = g;
273 }
274
275 zero = Cudd_Not(one);
276 if (topf >= topg) {
277 if (g0 == zero || g0 == DD_ZERO(dd)) {
278 r = cuddCofactorRecur(dd, f1, g1);
279 } else if (g1 == zero || g1 == DD_ZERO(dd)) {
280 r = cuddCofactorRecur(dd, f0, g0);
281 } else {
282 (void) fprintf(dd->out,
283 "Cudd_Cofactor: Invalid restriction 2\n");
284 dd->errorCode = CUDD_INVALID_ARG;
285 return(NULL);
286 }
287 if (r == NULL) return(NULL);
288 } else /* if (topf < topg) */ {
289 t = cuddCofactorRecur(dd, f1, g);
290 if (t == NULL) return(NULL);
291 cuddRef(t);
292 e = cuddCofactorRecur(dd, f0, g);
293 if (e == NULL) {
294 Cudd_RecursiveDeref(dd, t);
295 return(NULL);
296 }
297 cuddRef(e);
298
299 if (t == e) {
300 r = t;
301 } else if (Cudd_IsComplement(t)) {
302 r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e));
303 if (r != NULL)
304 r = Cudd_Not(r);
305 } else {
306 r = cuddUniqueInter(dd,(int)F->index,t,e);
307 }
308 if (r == NULL) {
309 Cudd_RecursiveDeref(dd ,e);
310 Cudd_RecursiveDeref(dd ,t);
311 return(NULL);
312 }
313 cuddDeref(t);
314 cuddDeref(e);
315 }
316
317 cuddCacheInsert2(dd,Cudd_Cofactor,F,g,r);
318
319 return(Cudd_NotCond(r,comple));
320
321} /* end of cuddCofactorRecur */
322
323
324/*---------------------------------------------------------------------------*/
325/* Definition of static functions */
326/*---------------------------------------------------------------------------*/
327
Note: See TracBrowser for help on using the repository browser.