1 /**CFile***********************************************************************
2
3 FileName [cuddClip.c]
4
5 PackageName [cudd]
6
7 Synopsis [Clipping functions.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_bddClippingAnd()
12 <li> Cudd_bddClippingAndAbstract()
13 </ul>
14 Internal procedures included in this module:
15 <ul>
16 <li> cuddBddClippingAnd()
17 <li> cuddBddClippingAndAbstract()
18 </ul>
19 Static procedures included in this module:
20 <ul>
21 <li> cuddBddClippingAndRecur()
22 <li> cuddBddClipAndAbsRecur()
23 </ul>
24
25 SeeAlso []
26
27 Author [Fabio Somenzi]
28
29 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
30
31 All rights reserved.
32
33 Redistribution and use in source and binary forms, with or without
34 modification, are permitted provided that the following conditions
35 are met:
36
37 Redistributions of source code must retain the above copyright
38 notice, this list of conditions and the following disclaimer.
39
40 Redistributions in binary form must reproduce the above copyright
41 notice, this list of conditions and the following disclaimer in the
42 documentation and/or other materials provided with the distribution.
43
44 Neither the name of the University of Colorado nor the names of its
45 contributors may be used to endorse or promote products derived from
46 this software without specific prior written permission.
47
48 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
49 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
50 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
51 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
52 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
53 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
54 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
55 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
56 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
57 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
58 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
59 POSSIBILITY OF SUCH DAMAGE.]
60
61 ******************************************************************************/
62
63 #include "misc/util/util_hack.h"
64 #include "cuddInt.h"
65
66 ABC_NAMESPACE_IMPL_START
67
68
69
70
71 /*---------------------------------------------------------------------------*/
72 /* Constant declarations */
73 /*---------------------------------------------------------------------------*/
74
75
76 /*---------------------------------------------------------------------------*/
77 /* Stucture declarations */
78 /*---------------------------------------------------------------------------*/
79
80
81 /*---------------------------------------------------------------------------*/
82 /* Type declarations */
83 /*---------------------------------------------------------------------------*/
84
85 /*---------------------------------------------------------------------------*/
86 /* Variable declarations */
87 /*---------------------------------------------------------------------------*/
88
89 #ifndef lint
90 static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
91 #endif
92
93 /*---------------------------------------------------------------------------*/
94 /* Macro declarations */
95 /*---------------------------------------------------------------------------*/
96
97
98 /**AutomaticStart*************************************************************/
99
100 /*---------------------------------------------------------------------------*/
101 /* Static function prototypes */
102 /*---------------------------------------------------------------------------*/
103
104 static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
105 static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
106
107 /**AutomaticEnd***************************************************************/
108
109
110 /*---------------------------------------------------------------------------*/
111 /* Definition of exported functions */
112 /*---------------------------------------------------------------------------*/
113
114
115 /**Function********************************************************************
116
117 Synopsis [Approximates the conjunction of two BDDs f and g.]
118
119 Description [Approximates the conjunction of two BDDs f and g. Returns a
120 pointer to the resulting BDD if successful; NULL if the intermediate
121 result blows up.]
122
123 SideEffects [None]
124
125 SeeAlso [Cudd_bddAnd]
126
127 ******************************************************************************/
128 DdNode *
Cudd_bddClippingAnd(DdManager * dd,DdNode * f,DdNode * g,int maxDepth,int direction)129 Cudd_bddClippingAnd(
130 DdManager * dd /* manager */,
131 DdNode * f /* first conjunct */,
132 DdNode * g /* second conjunct */,
133 int maxDepth /* maximum recursion depth */,
134 int direction /* under (0) or over (1) approximation */)
135 {
136 DdNode *res;
137
138 do {
139 dd->reordered = 0;
140 res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
141 } while (dd->reordered == 1);
142 return(res);
143
144 } /* end of Cudd_bddClippingAnd */
145
146
147 /**Function********************************************************************
148
149 Synopsis [Approximates the conjunction of two BDDs f and g and
150 simultaneously abstracts the variables in cube.]
151
152 Description [Approximates the conjunction of two BDDs f and g and
153 simultaneously abstracts the variables in cube. The variables are
154 existentially abstracted. Returns a pointer to the resulting BDD if
155 successful; NULL if the intermediate result blows up.]
156
157 SideEffects [None]
158
159 SeeAlso [Cudd_bddAndAbstract Cudd_bddClippingAnd]
160
161 ******************************************************************************/
162 DdNode *
Cudd_bddClippingAndAbstract(DdManager * dd,DdNode * f,DdNode * g,DdNode * cube,int maxDepth,int direction)163 Cudd_bddClippingAndAbstract(
164 DdManager * dd /* manager */,
165 DdNode * f /* first conjunct */,
166 DdNode * g /* second conjunct */,
167 DdNode * cube /* cube of variables to be abstracted */,
168 int maxDepth /* maximum recursion depth */,
169 int direction /* under (0) or over (1) approximation */)
170 {
171 DdNode *res;
172
173 do {
174 dd->reordered = 0;
175 res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
176 } while (dd->reordered == 1);
177 return(res);
178
179 } /* end of Cudd_bddClippingAndAbstract */
180
181
182 /*---------------------------------------------------------------------------*/
183 /* Definition of internal functions */
184 /*---------------------------------------------------------------------------*/
185
186
187 /**Function********************************************************************
188
189 Synopsis [Approximates the conjunction of two BDDs f and g.]
190
191 Description [Approximates the conjunction of two BDDs f and g. Returns a
192 pointer to the resulting BDD if successful; NULL if the intermediate
193 result blows up.]
194
195 SideEffects [None]
196
197 SeeAlso [Cudd_bddClippingAnd]
198
199 ******************************************************************************/
200 DdNode *
cuddBddClippingAnd(DdManager * dd,DdNode * f,DdNode * g,int maxDepth,int direction)201 cuddBddClippingAnd(
202 DdManager * dd /* manager */,
203 DdNode * f /* first conjunct */,
204 DdNode * g /* second conjunct */,
205 int maxDepth /* maximum recursion depth */,
206 int direction /* under (0) or over (1) approximation */)
207 {
208 DdNode *res;
209
210 res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
211
212 return(res);
213
214 } /* end of cuddBddClippingAnd */
215
216
217 /**Function********************************************************************
218
219 Synopsis [Approximates the conjunction of two BDDs f and g and
220 simultaneously abstracts the variables in cube.]
221
222 Description [Approximates the conjunction of two BDDs f and g and
223 simultaneously abstracts the variables in cube. Returns a
224 pointer to the resulting BDD if successful; NULL if the intermediate
225 result blows up.]
226
227 SideEffects [None]
228
229 SeeAlso [Cudd_bddClippingAndAbstract]
230
231 ******************************************************************************/
232 DdNode *
cuddBddClippingAndAbstract(DdManager * dd,DdNode * f,DdNode * g,DdNode * cube,int maxDepth,int direction)233 cuddBddClippingAndAbstract(
234 DdManager * dd /* manager */,
235 DdNode * f /* first conjunct */,
236 DdNode * g /* second conjunct */,
237 DdNode * cube /* cube of variables to be abstracted */,
238 int maxDepth /* maximum recursion depth */,
239 int direction /* under (0) or over (1) approximation */)
240 {
241 DdNode *res;
242
243 res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
244
245 return(res);
246
247 } /* end of cuddBddClippingAndAbstract */
248
249
250 /*---------------------------------------------------------------------------*/
251 /* Definition of static functions */
252 /*---------------------------------------------------------------------------*/
253
254
255 /**Function********************************************************************
256
257 Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
258
259 Description [Implements the recursive step of Cudd_bddClippingAnd by taking
260 the conjunction of two BDDs. Returns a pointer to the result is
261 successful; NULL otherwise.]
262
263 SideEffects [None]
264
265 SeeAlso [cuddBddClippingAnd]
266
267 ******************************************************************************/
268 static DdNode *
cuddBddClippingAndRecur(DdManager * manager,DdNode * f,DdNode * g,int distance,int direction)269 cuddBddClippingAndRecur(
270 DdManager * manager,
271 DdNode * f,
272 DdNode * g,
273 int distance,
274 int direction)
275 {
276 DdNode *F, *ft, *fe, *G, *gt, *ge;
277 DdNode *one, *zero, *r, *t, *e;
278 unsigned int topf, topg, index;
279 DD_CTFP cacheOp;
280
281 statLine(manager);
282 one = DD_ONE(manager);
283 zero = Cudd_Not(one);
284
285 /* Terminal cases. */
286 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
287 if (f == g || g == one) return(f);
288 if (f == one) return(g);
289 if (distance == 0) {
290 /* One last attempt at returning the right result. We sort of
291 ** cheat by calling Cudd_bddLeq. */
292 if (Cudd_bddLeq(manager,f,g)) return(f);
293 if (Cudd_bddLeq(manager,g,f)) return(g);
294 if (direction == 1) {
295 if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
296 Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
297 }
298 return(Cudd_NotCond(one,(direction == 0)));
299 }
300
301 /* At this point f and g are not constant. */
302 distance--;
303
304 /* Check cache. Try to increase cache efficiency by sorting the
305 ** pointers. */
306 if (f > g) {
307 DdNode *tmp = f;
308 f = g; g = tmp;
309 }
310 F = Cudd_Regular(f);
311 G = Cudd_Regular(g);
312 cacheOp = (DD_CTFP)
313 (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
314 if (F->ref != 1 || G->ref != 1) {
315 r = cuddCacheLookup2(manager, cacheOp, f, g);
316 if (r != NULL) return(r);
317 }
318
319 /* Here we can skip the use of cuddI, because the operands are known
320 ** to be non-constant.
321 */
322 topf = manager->perm[F->index];
323 topg = manager->perm[G->index];
324
325 /* Compute cofactors. */
326 if (topf <= topg) {
327 index = F->index;
328 ft = cuddT(F);
329 fe = cuddE(F);
330 if (Cudd_IsComplement(f)) {
331 ft = Cudd_Not(ft);
332 fe = Cudd_Not(fe);
333 }
334 } else {
335 index = G->index;
336 ft = fe = f;
337 }
338
339 if (topg <= topf) {
340 gt = cuddT(G);
341 ge = cuddE(G);
342 if (Cudd_IsComplement(g)) {
343 gt = Cudd_Not(gt);
344 ge = Cudd_Not(ge);
345 }
346 } else {
347 gt = ge = g;
348 }
349
350 t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
351 if (t == NULL) return(NULL);
352 cuddRef(t);
353 e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
354 if (e == NULL) {
355 Cudd_RecursiveDeref(manager, t);
356 return(NULL);
357 }
358 cuddRef(e);
359
360 if (t == e) {
361 r = t;
362 } else {
363 if (Cudd_IsComplement(t)) {
364 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
365 if (r == NULL) {
366 Cudd_RecursiveDeref(manager, t);
367 Cudd_RecursiveDeref(manager, e);
368 return(NULL);
369 }
370 r = Cudd_Not(r);
371 } else {
372 r = cuddUniqueInter(manager,(int)index,t,e);
373 if (r == NULL) {
374 Cudd_RecursiveDeref(manager, t);
375 Cudd_RecursiveDeref(manager, e);
376 return(NULL);
377 }
378 }
379 }
380 cuddDeref(e);
381 cuddDeref(t);
382 if (F->ref != 1 || G->ref != 1)
383 cuddCacheInsert2(manager, cacheOp, f, g, r);
384 return(r);
385
386 } /* end of cuddBddClippingAndRecur */
387
388
389 /**Function********************************************************************
390
391 Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
392 variables in cube.]
393
394 Description [Approximates the AND of two BDDs and simultaneously
395 abstracts the variables in cube. The variables are existentially
396 abstracted. Returns a pointer to the result is successful; NULL
397 otherwise.]
398
399 SideEffects [None]
400
401 SeeAlso [Cudd_bddClippingAndAbstract]
402
403 ******************************************************************************/
404 static DdNode *
cuddBddClipAndAbsRecur(DdManager * manager,DdNode * f,DdNode * g,DdNode * cube,int distance,int direction)405 cuddBddClipAndAbsRecur(
406 DdManager * manager,
407 DdNode * f,
408 DdNode * g,
409 DdNode * cube,
410 int distance,
411 int direction)
412 {
413 DdNode *F, *ft, *fe, *G, *gt, *ge;
414 DdNode *one, *zero, *r, *t, *e, *Cube;
415 unsigned int topf, topg, topcube, top, index;
416 ptruint cacheTag;
417
418 statLine(manager);
419 one = DD_ONE(manager);
420 zero = Cudd_Not(one);
421
422 /* Terminal cases. */
423 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
424 if (f == one && g == one) return(one);
425 if (cube == one) {
426 return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
427 }
428 if (f == one || f == g) {
429 return (cuddBddExistAbstractRecur(manager, g, cube));
430 }
431 if (g == one) {
432 return (cuddBddExistAbstractRecur(manager, f, cube));
433 }
434 if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
435
436 /* At this point f, g, and cube are not constant. */
437 distance--;
438
439 /* Check cache. */
440 if (f > g) { /* Try to increase cache efficiency. */
441 DdNode *tmp = f;
442 f = g; g = tmp;
443 }
444 F = Cudd_Regular(f);
445 G = Cudd_Regular(g);
446 cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
447 DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
448 if (F->ref != 1 || G->ref != 1) {
449 r = cuddCacheLookup(manager, cacheTag,
450 f, g, cube);
451 if (r != NULL) {
452 return(r);
453 }
454 }
455
456 /* Here we can skip the use of cuddI, because the operands are known
457 ** to be non-constant.
458 */
459 topf = manager->perm[F->index];
460 topg = manager->perm[G->index];
461 top = ddMin(topf, topg);
462 topcube = manager->perm[cube->index];
463
464 if (topcube < top) {
465 return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
466 distance, direction));
467 }
468 /* Now, topcube >= top. */
469
470 if (topf == top) {
471 index = F->index;
472 ft = cuddT(F);
473 fe = cuddE(F);
474 if (Cudd_IsComplement(f)) {
475 ft = Cudd_Not(ft);
476 fe = Cudd_Not(fe);
477 }
478 } else {
479 index = G->index;
480 ft = fe = f;
481 }
482
483 if (topg == top) {
484 gt = cuddT(G);
485 ge = cuddE(G);
486 if (Cudd_IsComplement(g)) {
487 gt = Cudd_Not(gt);
488 ge = Cudd_Not(ge);
489 }
490 } else {
491 gt = ge = g;
492 }
493
494 if (topcube == top) {
495 Cube = cuddT(cube);
496 } else {
497 Cube = cube;
498 }
499
500 t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
501 if (t == NULL) return(NULL);
502
503 /* Special case: 1 OR anything = 1. Hence, no need to compute
504 ** the else branch if t is 1.
505 */
506 if (t == one && topcube == top) {
507 if (F->ref != 1 || G->ref != 1)
508 cuddCacheInsert(manager, cacheTag, f, g, cube, one);
509 return(one);
510 }
511 cuddRef(t);
512
513 e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
514 if (e == NULL) {
515 Cudd_RecursiveDeref(manager, t);
516 return(NULL);
517 }
518 cuddRef(e);
519
520 if (topcube == top) { /* abstract */
521 r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
522 distance, (direction == 0));
523 if (r == NULL) {
524 Cudd_RecursiveDeref(manager, t);
525 Cudd_RecursiveDeref(manager, e);
526 return(NULL);
527 }
528 r = Cudd_Not(r);
529 cuddRef(r);
530 Cudd_RecursiveDeref(manager, t);
531 Cudd_RecursiveDeref(manager, e);
532 cuddDeref(r);
533 } else if (t == e) {
534 r = t;
535 cuddDeref(t);
536 cuddDeref(e);
537 } else {
538 if (Cudd_IsComplement(t)) {
539 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
540 if (r == NULL) {
541 Cudd_RecursiveDeref(manager, t);
542 Cudd_RecursiveDeref(manager, e);
543 return(NULL);
544 }
545 r = Cudd_Not(r);
546 } else {
547 r = cuddUniqueInter(manager,(int)index,t,e);
548 if (r == NULL) {
549 Cudd_RecursiveDeref(manager, t);
550 Cudd_RecursiveDeref(manager, e);
551 return(NULL);
552 }
553 }
554 cuddDeref(e);
555 cuddDeref(t);
556 }
557 if (F->ref != 1 || G->ref != 1)
558 cuddCacheInsert(manager, cacheTag, f, g, cube, r);
559 return (r);
560
561 } /* end of cuddBddClipAndAbsRecur */
562
563
564 ABC_NAMESPACE_IMPL_END
565
566
567