1 /**CFile***********************************************************************
7 Synopsis [Clipping functions.]
9 Description [External procedures included in this module:
11 <li> Cudd_bddClippingAnd()
12 <li> Cudd_bddClippingAndAbstract()
14 Internal procedures included in this module:
16 <li> cuddBddClippingAnd()
17 <li> cuddBddClippingAndAbstract()
19 Static procedures included in this module:
21 <li> cuddBddClippingAndRecur()
22 <li> cuddBddClipAndAbsRecur()
27 Author [Fabio Somenzi]
29 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
33 Redistribution and use in source and binary forms, with or without
34 modification, are permitted provided that the following conditions
37 Redistributions of source code must retain the above copyright
38 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
61 ******************************************************************************/
67 /*---------------------------------------------------------------------------*/
68 /* Constant declarations */
69 /*---------------------------------------------------------------------------*/
72 /*---------------------------------------------------------------------------*/
73 /* Stucture declarations */
74 /*---------------------------------------------------------------------------*/
77 /*---------------------------------------------------------------------------*/
78 /* Type declarations */
79 /*---------------------------------------------------------------------------*/
81 /*---------------------------------------------------------------------------*/
82 /* Variable declarations */
83 /*---------------------------------------------------------------------------*/
86 static char rcsid
[] DD_UNUSED
= "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
89 /*---------------------------------------------------------------------------*/
90 /* Macro declarations */
91 /*---------------------------------------------------------------------------*/
94 /**AutomaticStart*************************************************************/
96 /*---------------------------------------------------------------------------*/
97 /* Static function prototypes */
98 /*---------------------------------------------------------------------------*/
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
);
103 /**AutomaticEnd***************************************************************/
106 /*---------------------------------------------------------------------------*/
107 /* Definition of exported functions */
108 /*---------------------------------------------------------------------------*/
111 /**Function********************************************************************
113 Synopsis [Approximates the conjunction of two BDDs f and g.]
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
121 SeeAlso [Cudd_bddAnd]
123 ******************************************************************************/
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 */)
136 res
= cuddBddClippingAnd(dd
,f
,g
,maxDepth
,direction
);
137 } while (dd
->reordered
== 1);
140 } /* end of Cudd_bddClippingAnd */
143 /**Function********************************************************************
145 Synopsis [Approximates the conjunction of two BDDs f and g and
146 simultaneously abstracts the variables in cube.]
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.]
155 SeeAlso [Cudd_bddAndAbstract Cudd_bddClippingAnd]
157 ******************************************************************************/
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 */)
171 res
= cuddBddClippingAndAbstract(dd
,f
,g
,cube
,maxDepth
,direction
);
172 } while (dd
->reordered
== 1);
175 } /* end of Cudd_bddClippingAndAbstract */
178 /*---------------------------------------------------------------------------*/
179 /* Definition of internal functions */
180 /*---------------------------------------------------------------------------*/
183 /**Function********************************************************************
185 Synopsis [Approximates the conjunction of two BDDs f and g.]
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
193 SeeAlso [Cudd_bddClippingAnd]
195 ******************************************************************************/
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 */)
206 res
= cuddBddClippingAndRecur(dd
,f
,g
,maxDepth
,direction
);
210 } /* end of cuddBddClippingAnd */
213 /**Function********************************************************************
215 Synopsis [Approximates the conjunction of two BDDs f and g and
216 simultaneously abstracts the variables in cube.]
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
225 SeeAlso [Cudd_bddClippingAndAbstract]
227 ******************************************************************************/
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 */)
239 res
= cuddBddClipAndAbsRecur(dd
,f
,g
,cube
,maxDepth
,direction
);
243 } /* end of cuddBddClippingAndAbstract */
246 /*---------------------------------------------------------------------------*/
247 /* Definition of static functions */
248 /*---------------------------------------------------------------------------*/
251 /**Function********************************************************************
253 Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]
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.]
261 SeeAlso [cuddBddClippingAnd]
263 ******************************************************************************/
265 cuddBddClippingAndRecur(
272 DdNode
*F
, *ft
, *fe
, *G
, *gt
, *ge
;
273 DdNode
*one
, *zero
, *r
, *t
, *e
;
274 unsigned int topf
, topg
, index
;
278 one
= DD_ONE(manager
);
279 zero
= Cudd_Not(one
);
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
);
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
);
294 return(Cudd_NotCond(one
,(direction
== 0)));
297 /* At this point f and g are not constant. */
300 /* Check cache. Try to increase cache efficiency by sorting the
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
);
315 /* Here we can skip the use of cuddI, because the operands are known
316 ** to be non-constant.
318 topf
= manager
->perm
[F
->index
];
319 topg
= manager
->perm
[G
->index
];
321 /* Compute cofactors. */
326 if (Cudd_IsComplement(f
)) {
338 if (Cudd_IsComplement(g
)) {
346 t
= cuddBddClippingAndRecur(manager
, ft
, gt
, distance
, direction
);
347 if (t
== NULL
) return(NULL
);
349 e
= cuddBddClippingAndRecur(manager
, fe
, ge
, distance
, direction
);
351 Cudd_RecursiveDeref(manager
, t
);
359 if (Cudd_IsComplement(t
)) {
360 r
= cuddUniqueInter(manager
,(int)index
,Cudd_Not(t
),Cudd_Not(e
));
362 Cudd_RecursiveDeref(manager
, t
);
363 Cudd_RecursiveDeref(manager
, e
);
368 r
= cuddUniqueInter(manager
,(int)index
,t
,e
);
370 Cudd_RecursiveDeref(manager
, t
);
371 Cudd_RecursiveDeref(manager
, e
);
378 if (F
->ref
!= 1 || G
->ref
!= 1)
379 cuddCacheInsert2(manager
, cacheOp
, f
, g
, r
);
382 } /* end of cuddBddClippingAndRecur */
385 /**Function********************************************************************
387 Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the
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
397 SeeAlso [Cudd_bddClippingAndAbstract]
399 ******************************************************************************/
401 cuddBddClipAndAbsRecur(
409 DdNode
*F
, *ft
, *fe
, *G
, *gt
, *ge
;
410 DdNode
*one
, *zero
, *r
, *t
, *e
, *Cube
;
411 unsigned int topf
, topg
, topcube
, top
, index
;
415 one
= DD_ONE(manager
);
416 zero
= Cudd_Not(one
);
418 /* Terminal cases. */
419 if (f
== zero
|| g
== zero
|| f
== Cudd_Not(g
)) return(zero
);
420 if (f
== one
&& g
== one
) return(one
);
422 return(cuddBddClippingAndRecur(manager
, f
, g
, distance
, direction
));
424 if (f
== one
|| f
== g
) {
425 return (cuddBddExistAbstractRecur(manager
, g
, cube
));
428 return (cuddBddExistAbstractRecur(manager
, f
, cube
));
430 if (distance
== 0) return(Cudd_NotCond(one
,(direction
== 0)));
432 /* At this point f, g, and cube are not constant. */
436 if (f
> g
) { /* Try to increase cache efficiency. */
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
,
452 /* Here we can skip the use of cuddI, because the operands are known
453 ** to be non-constant.
455 topf
= manager
->perm
[F
->index
];
456 topg
= manager
->perm
[G
->index
];
457 top
= ddMin(topf
, topg
);
458 topcube
= manager
->perm
[cube
->index
];
461 return(cuddBddClipAndAbsRecur(manager
, f
, g
, cuddT(cube
),
462 distance
, direction
));
464 /* Now, topcube >= top. */
470 if (Cudd_IsComplement(f
)) {
482 if (Cudd_IsComplement(g
)) {
490 if (topcube
== top
) {
496 t
= cuddBddClipAndAbsRecur(manager
, ft
, gt
, Cube
, distance
, direction
);
497 if (t
== NULL
) return(NULL
);
499 /* Special case: 1 OR anything = 1. Hence, no need to compute
500 ** the else branch if t is 1.
502 if (t
== one
&& topcube
== top
) {
503 if (F
->ref
!= 1 || G
->ref
!= 1)
504 cuddCacheInsert(manager
, cacheTag
, f
, g
, cube
, one
);
509 e
= cuddBddClipAndAbsRecur(manager
, fe
, ge
, Cube
, distance
, direction
);
511 Cudd_RecursiveDeref(manager
, t
);
516 if (topcube
== top
) { /* abstract */
517 r
= cuddBddClippingAndRecur(manager
, Cudd_Not(t
), Cudd_Not(e
),
518 distance
, (direction
== 0));
520 Cudd_RecursiveDeref(manager
, t
);
521 Cudd_RecursiveDeref(manager
, e
);
526 Cudd_RecursiveDeref(manager
, t
);
527 Cudd_RecursiveDeref(manager
, e
);
534 if (Cudd_IsComplement(t
)) {
535 r
= cuddUniqueInter(manager
,(int)index
,Cudd_Not(t
),Cudd_Not(e
));
537 Cudd_RecursiveDeref(manager
, t
);
538 Cudd_RecursiveDeref(manager
, e
);
543 r
= cuddUniqueInter(manager
,(int)index
,t
,e
);
545 Cudd_RecursiveDeref(manager
, t
);
546 Cudd_RecursiveDeref(manager
, e
);
553 if (F
->ref
!= 1 || G
->ref
!= 1)
554 cuddCacheInsert(manager
, cacheTag
, f
, g
, cube
, r
);
557 } /* end of cuddBddClipAndAbsRecur */