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-2012, 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 "util.h"
64 #include "cuddInt.h"
65
66
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
70
71
72 /*---------------------------------------------------------------------------*/
73 /* Stucture declarations */
74 /*---------------------------------------------------------------------------*/
75
76
77 /*---------------------------------------------------------------------------*/
78 /* Type declarations */
79 /*---------------------------------------------------------------------------*/
80
81 /*---------------------------------------------------------------------------*/
82 /* Variable declarations */
83 /*---------------------------------------------------------------------------*/
84
85 #ifndef lint
86 static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.9 2012/02/05 01:07:18 fabio Exp $";
87 #endif
88
89 /*---------------------------------------------------------------------------*/
90 /* Macro declarations */
91 /*---------------------------------------------------------------------------*/
92
93
94 /**AutomaticStart*************************************************************/
95
96 /*---------------------------------------------------------------------------*/
97 /* Static function prototypes */
98 /*---------------------------------------------------------------------------*/
99
100 static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
101 static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
102
103 /**AutomaticEnd***************************************************************/
104
105
106 /*---------------------------------------------------------------------------*/
107 /* Definition of exported functions */
108 /*---------------------------------------------------------------------------*/
109
110
111 /**Function********************************************************************
112
113 Synopsis [Approximates the conjunction of two BDDs f and g.]
114
115 Description [Approximates the conjunction of two BDDs f and g. Returns a
116 pointer to the resulting BDD if successful; NULL if the intermediate
117 result blows up.]
118
119 SideEffects [None]
120
121 SeeAlso [Cudd_bddAnd]
122
123 ******************************************************************************/
124 DdNode *
Cudd_bddClippingAnd(DdManager * dd,DdNode * f,DdNode * g,int maxDepth,int direction)125 Cudd_bddClippingAnd(
126 DdManager * dd /* manager */,
127 DdNode * f /* first conjunct */,
128 DdNode * g /* second conjunct */,
129 int maxDepth /* maximum recursion depth */,
130 int direction /* under (0) or over (1) approximation */)
131 {
132 DdNode *res;
133
134 do {
135 dd->reordered = 0;
136 res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
137 } while (dd->reordered == 1);
138 return(res);
139
140 } /* end of Cudd_bddClippingAnd */
141
142
143 /**Function********************************************************************
144
145 Synopsis [Approximates the conjunction of two BDDs f and g and
146 simultaneously abstracts the variables in cube.]
147
148 Description [Approximates the conjunction of two BDDs f and g and
149 simultaneously abstracts the variables in cube. The variables are
150 existentially abstracted. Returns a pointer to the resulting BDD if
151 successful; NULL if the intermediate result blows up.]
152
153 SideEffects [None]
154
155 SeeAlso [Cudd_bddAndAbstract Cudd_bddClippingAnd]
156
157 ******************************************************************************/
158 DdNode *
Cudd_bddClippingAndAbstract(DdManager * dd,DdNode * f,DdNode * g,DdNode * cube,int maxDepth,int direction)159 Cudd_bddClippingAndAbstract(
160 DdManager * dd /* manager */,
161 DdNode * f /* first conjunct */,
162 DdNode * g /* second conjunct */,
163 DdNode * cube /* cube of variables to be abstracted */,
164 int maxDepth /* maximum recursion depth */,
165 int direction /* under (0) or over (1) approximation */)
166 {
167 DdNode *res;
168
169 do {
170 dd->reordered = 0;
171 res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
172 } while (dd->reordered == 1);
173 return(res);
174
175 } /* end of Cudd_bddClippingAndAbstract */
176
177
178 /*---------------------------------------------------------------------------*/
179 /* Definition of internal functions */
180 /*---------------------------------------------------------------------------*/
181
182
183 /**Function********************************************************************
184
185 Synopsis [Approximates the conjunction of two BDDs f and g.]
186
187 Description [Approximates the conjunction of two BDDs f and g. Returns a
188 pointer to the resulting BDD if successful; NULL if the intermediate
189 result blows up.]
190
191 SideEffects [None]
192
193 SeeAlso [Cudd_bddClippingAnd]
194
195 ******************************************************************************/
196 DdNode *
cuddBddClippingAnd(DdManager * dd,DdNode * f,DdNode * g,int maxDepth,int direction)197 cuddBddClippingAnd(
198 DdManager * dd /* manager */,
199 DdNode * f /* first conjunct */,
200 DdNode * g /* second conjunct */,
201 int maxDepth /* maximum recursion depth */,
202 int direction /* under (0) or over (1) approximation */)
203 {
204 DdNode *res;
205
206 res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
207
208 return(res);
209
210 } /* end of cuddBddClippingAnd */
211
212
213 /**Function********************************************************************
214
215 Synopsis [Approximates the conjunction of two BDDs f and g and
216 simultaneously abstracts the variables in cube.]
217
218 Description [Approximates the conjunction of two BDDs f and g and
219 simultaneously abstracts the variables in cube. Returns a
220 pointer to the resulting BDD if successful; NULL if the intermediate
221 result blows up.]
222
223 SideEffects [None]
224
225 SeeAlso [Cudd_bddClippingAndAbstract]
226
227 ******************************************************************************/
228 DdNode *
cuddBddClippingAndAbstract(DdManager * dd,DdNode * f,DdNode * g,DdNode * cube,int maxDepth,int direction)229 cuddBddClippingAndAbstract(
230 DdManager * dd /* manager */,
231 DdNode * f /* first conjunct */,
232 DdNode * g /* second conjunct */,
233 DdNode * cube /* cube of variables to be abstracted */,
234 int maxDepth /* maximum recursion depth */,
235 int direction /* under (0) or over (1) approximation */)
236 {
237 DdNode *res;
238
239 res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
240
241 return(res);
242
243 } /* end of cuddBddClippingAndAbstract */
244
245
246 /*---------------------------------------------------------------------------*/
247 /* Definition of static functions */
248 /*---------------------------------------------------------------------------*/
249
250
251 /**Function********************************************************************
252
253 Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
254
255 Description [Implements the recursive step of Cudd_bddClippingAnd by taking
256 the conjunction of two BDDs. Returns a pointer to the result is
257 successful; NULL otherwise.]
258
259 SideEffects [None]
260
261 SeeAlso [cuddBddClippingAnd]
262
263 ******************************************************************************/
264 static DdNode *
cuddBddClippingAndRecur(DdManager * manager,DdNode * f,DdNode * g,int distance,int direction)265 cuddBddClippingAndRecur(
266 DdManager * manager,
267 DdNode * f,
268 DdNode * g,
269 int distance,
270 int direction)
271 {
272 DdNode *F, *ft, *fe, *G, *gt, *ge;
273 DdNode *one, *zero, *r, *t, *e;
274 unsigned int topf, topg, index;
275 DD_CTFP cacheOp;
276
277 statLine(manager);
278 one = DD_ONE(manager);
279 zero = Cudd_Not(one);
280
281 /* Terminal cases. */
282 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
283 if (f == g || g == one) return(f);
284 if (f == one) return(g);
285 if (distance == 0) {
286 /* One last attempt at returning the right result. We sort of
287 ** cheat by calling Cudd_bddLeq. */
288 if (Cudd_bddLeq(manager,f,g)) return(f);
289 if (Cudd_bddLeq(manager,g,f)) return(g);
290 if (direction == 1) {
291 if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
292 Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
293 }
294 return(Cudd_NotCond(one,(direction == 0)));
295 }
296
297 /* At this point f and g are not constant. */
298 distance--;
299
300 /* Check cache. Try to increase cache efficiency by sorting the
301 ** pointers. */
302 if (f > g) {
303 DdNode *tmp = f;
304 f = g; g = tmp;
305 }
306 F = Cudd_Regular(f);
307 G = Cudd_Regular(g);
308 cacheOp = (DD_CTFP)
309 (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
310 if (F->ref != 1 || G->ref != 1) {
311 r = cuddCacheLookup2(manager, cacheOp, f, g);
312 if (r != NULL) return(r);
313 }
314
315 /* Here we can skip the use of cuddI, because the operands are known
316 ** to be non-constant.
317 */
318 topf = manager->perm[F->index];
319 topg = manager->perm[G->index];
320
321 /* Compute cofactors. */
322 if (topf <= topg) {
323 index = F->index;
324 ft = cuddT(F);
325 fe = cuddE(F);
326 if (Cudd_IsComplement(f)) {
327 ft = Cudd_Not(ft);
328 fe = Cudd_Not(fe);
329 }
330 } else {
331 index = G->index;
332 ft = fe = f;
333 }
334
335 if (topg <= topf) {
336 gt = cuddT(G);
337 ge = cuddE(G);
338 if (Cudd_IsComplement(g)) {
339 gt = Cudd_Not(gt);
340 ge = Cudd_Not(ge);
341 }
342 } else {
343 gt = ge = g;
344 }
345
346 t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
347 if (t == NULL) return(NULL);
348 cuddRef(t);
349 e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
350 if (e == NULL) {
351 Cudd_RecursiveDeref(manager, t);
352 return(NULL);
353 }
354 cuddRef(e);
355
356 if (t == e) {
357 r = t;
358 } else {
359 if (Cudd_IsComplement(t)) {
360 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
361 if (r == NULL) {
362 Cudd_RecursiveDeref(manager, t);
363 Cudd_RecursiveDeref(manager, e);
364 return(NULL);
365 }
366 r = Cudd_Not(r);
367 } else {
368 r = cuddUniqueInter(manager,(int)index,t,e);
369 if (r == NULL) {
370 Cudd_RecursiveDeref(manager, t);
371 Cudd_RecursiveDeref(manager, e);
372 return(NULL);
373 }
374 }
375 }
376 cuddDeref(e);
377 cuddDeref(t);
378 if (F->ref != 1 || G->ref != 1)
379 cuddCacheInsert2(manager, cacheOp, f, g, r);
380 return(r);
381
382 } /* end of cuddBddClippingAndRecur */
383
384
385 /**Function********************************************************************
386
387 Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
388 variables in cube.]
389
390 Description [Approximates the AND of two BDDs and simultaneously
391 abstracts the variables in cube. The variables are existentially
392 abstracted. Returns a pointer to the result is successful; NULL
393 otherwise.]
394
395 SideEffects [None]
396
397 SeeAlso [Cudd_bddClippingAndAbstract]
398
399 ******************************************************************************/
400 static DdNode *
cuddBddClipAndAbsRecur(DdManager * manager,DdNode * f,DdNode * g,DdNode * cube,int distance,int direction)401 cuddBddClipAndAbsRecur(
402 DdManager * manager,
403 DdNode * f,
404 DdNode * g,
405 DdNode * cube,
406 int distance,
407 int direction)
408 {
409 DdNode *F, *ft, *fe, *G, *gt, *ge;
410 DdNode *one, *zero, *r, *t, *e, *Cube;
411 unsigned int topf, topg, topcube, top, index;
412 ptruint cacheTag;
413
414 statLine(manager);
415 one = DD_ONE(manager);
416 zero = Cudd_Not(one);
417
418 /* Terminal cases. */
419 if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
420 if (f == one && g == one) return(one);
421 if (cube == one) {
422 return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
423 }
424 if (f == one || f == g) {
425 return (cuddBddExistAbstractRecur(manager, g, cube));
426 }
427 if (g == one) {
428 return (cuddBddExistAbstractRecur(manager, f, cube));
429 }
430 if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
431
432 /* At this point f, g, and cube are not constant. */
433 distance--;
434
435 /* Check cache. */
436 if (f > g) { /* Try to increase cache efficiency. */
437 DdNode *tmp = f;
438 f = g; g = tmp;
439 }
440 F = Cudd_Regular(f);
441 G = Cudd_Regular(g);
442 cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
443 DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
444 if (F->ref != 1 || G->ref != 1) {
445 r = cuddCacheLookup(manager, cacheTag,
446 f, g, cube);
447 if (r != NULL) {
448 return(r);
449 }
450 }
451
452 /* Here we can skip the use of cuddI, because the operands are known
453 ** to be non-constant.
454 */
455 topf = manager->perm[F->index];
456 topg = manager->perm[G->index];
457 top = ddMin(topf, topg);
458 topcube = manager->perm[cube->index];
459
460 if (topcube < top) {
461 return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
462 distance, direction));
463 }
464 /* Now, topcube >= top. */
465
466 if (topf == top) {
467 index = F->index;
468 ft = cuddT(F);
469 fe = cuddE(F);
470 if (Cudd_IsComplement(f)) {
471 ft = Cudd_Not(ft);
472 fe = Cudd_Not(fe);
473 }
474 } else {
475 index = G->index;
476 ft = fe = f;
477 }
478
479 if (topg == top) {
480 gt = cuddT(G);
481 ge = cuddE(G);
482 if (Cudd_IsComplement(g)) {
483 gt = Cudd_Not(gt);
484 ge = Cudd_Not(ge);
485 }
486 } else {
487 gt = ge = g;
488 }
489
490 if (topcube == top) {
491 Cube = cuddT(cube);
492 } else {
493 Cube = cube;
494 }
495
496 t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
497 if (t == NULL) return(NULL);
498
499 /* Special case: 1 OR anything = 1. Hence, no need to compute
500 ** the else branch if t is 1.
501 */
502 if (t == one && topcube == top) {
503 if (F->ref != 1 || G->ref != 1)
504 cuddCacheInsert(manager, cacheTag, f, g, cube, one);
505 return(one);
506 }
507 cuddRef(t);
508
509 e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
510 if (e == NULL) {
511 Cudd_RecursiveDeref(manager, t);
512 return(NULL);
513 }
514 cuddRef(e);
515
516 if (topcube == top) { /* abstract */
517 r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
518 distance, (direction == 0));
519 if (r == NULL) {
520 Cudd_RecursiveDeref(manager, t);
521 Cudd_RecursiveDeref(manager, e);
522 return(NULL);
523 }
524 r = Cudd_Not(r);
525 cuddRef(r);
526 Cudd_RecursiveDeref(manager, t);
527 Cudd_RecursiveDeref(manager, e);
528 cuddDeref(r);
529 } else if (t == e) {
530 r = t;
531 cuddDeref(t);
532 cuddDeref(e);
533 } else {
534 if (Cudd_IsComplement(t)) {
535 r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
536 if (r == NULL) {
537 Cudd_RecursiveDeref(manager, t);
538 Cudd_RecursiveDeref(manager, e);
539 return(NULL);
540 }
541 r = Cudd_Not(r);
542 } else {
543 r = cuddUniqueInter(manager,(int)index,t,e);
544 if (r == NULL) {
545 Cudd_RecursiveDeref(manager, t);
546 Cudd_RecursiveDeref(manager, e);
547 return(NULL);
548 }
549 }
550 cuddDeref(e);
551 cuddDeref(t);
552 }
553 if (F->ref != 1 || G->ref != 1)
554 cuddCacheInsert(manager, cacheTag, f, g, cube, r);
555 return (r);
556
557 } /* end of cuddBddClipAndAbsRecur */
558
559