1 /**CFile***********************************************************************
3 FileName [cuddAddIte.c]
7 Synopsis [ADD ITE function and satellites.]
9 Description [External procedures included in this module:
12 <li> Cudd_addIteConstant()
13 <li> Cudd_addEvalConst()
17 Internal procedures included in this module:
19 <li> cuddAddIteRecur()
20 <li> cuddAddCmplRecur()
22 Static procedures included in this module:
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 ******************************************************************************/
66 /*---------------------------------------------------------------------------*/
67 /* Constant declarations */
68 /*---------------------------------------------------------------------------*/
71 /*---------------------------------------------------------------------------*/
72 /* Stucture declarations */
73 /*---------------------------------------------------------------------------*/
76 /*---------------------------------------------------------------------------*/
77 /* Type declarations */
78 /*---------------------------------------------------------------------------*/
81 /*---------------------------------------------------------------------------*/
82 /* Variable declarations */
83 /*---------------------------------------------------------------------------*/
86 static char rcsid
[] DD_UNUSED
= "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $";
90 /*---------------------------------------------------------------------------*/
91 /* Macro declarations */
92 /*---------------------------------------------------------------------------*/
95 /**AutomaticStart*************************************************************/
97 /*---------------------------------------------------------------------------*/
98 /* Static function prototypes */
99 /*---------------------------------------------------------------------------*/
101 static void addVarToConst (DdNode
*f
, DdNode
**gp
, DdNode
**hp
, DdNode
*one
, DdNode
*zero
);
103 /**AutomaticEnd***************************************************************/
106 /*---------------------------------------------------------------------------*/
107 /* Definition of exported functions */
108 /*---------------------------------------------------------------------------*/
111 /**Function********************************************************************
113 Synopsis [Implements ITE(f,g,h).]
115 Description [Implements ITE(f,g,h). This procedure assumes that f is
116 a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL
121 SeeAlso [Cudd_bddIte Cudd_addIteConstant Cudd_addApply]
123 ******************************************************************************/
135 res
= cuddAddIteRecur(dd
,f
,g
,h
);
136 } while (dd
->reordered
== 1);
139 } /* end of Cudd_addIte */
142 /**Function********************************************************************
144 Synopsis [Implements ITEconstant for ADDs.]
146 Description [Implements ITEconstant for ADDs. f must be a 0-1 ADD.
147 Returns a pointer to the resulting ADD (which may or may not be
148 constant) or DD_NON_CONSTANT. No new nodes are created. This function
149 can be used, for instance, to check that g has a constant value
150 (specified by h) whenever f is 1. If the constant value is unknown,
151 then one should use Cudd_addEvalConst.]
155 SeeAlso [Cudd_addIte Cudd_addEvalConst Cudd_bddIteConstant]
157 ******************************************************************************/
166 DdNode
*Fv
,*Fnv
,*Gv
,*Gnv
,*Hv
,*Hnv
,*r
,*t
,*e
;
167 unsigned int topf
,topg
,toph
,v
;
171 if (f
== (one
= DD_ONE(dd
))) { /* ITE(1,G,H) = G */
174 if (f
== (zero
= DD_ZERO(dd
))) { /* ITE(0,G,H) = H */
178 /* From now on, f is known not to be a constant. */
179 addVarToConst(f
,&g
,&h
,one
,zero
);
181 /* Check remaining one variable cases. */
182 if (g
== h
) { /* ITE(F,G,G) = G */
185 if (cuddIsConstant(g
) && cuddIsConstant(h
)) {
186 return(DD_NON_CONSTANT
);
189 topf
= cuddI(dd
,f
->index
);
190 topg
= cuddI(dd
,g
->index
);
191 toph
= cuddI(dd
,h
->index
);
192 v
= ddMin(topg
,toph
);
194 /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */
195 if (topf
< v
&& cuddIsConstant(cuddT(f
)) && cuddIsConstant(cuddE(f
))) {
196 return(DD_NON_CONSTANT
);
200 r
= cuddConstantLookup(dd
,DD_ADD_ITE_CONSTANT_TAG
,f
,g
,h
);
205 /* Compute cofactors. */
207 v
= ddMin(topf
,v
); /* v = top_var(F,G,H) */
208 Fv
= cuddT(f
); Fnv
= cuddE(f
);
213 Gv
= cuddT(g
); Gnv
= cuddE(g
);
218 Hv
= cuddT(h
); Hnv
= cuddE(h
);
223 /* Recursive step. */
224 t
= Cudd_addIteConstant(dd
,Fv
,Gv
,Hv
);
225 if (t
== DD_NON_CONSTANT
|| !cuddIsConstant(t
)) {
226 cuddCacheInsert(dd
, DD_ADD_ITE_CONSTANT_TAG
, f
, g
, h
, DD_NON_CONSTANT
);
227 return(DD_NON_CONSTANT
);
229 e
= Cudd_addIteConstant(dd
,Fnv
,Gnv
,Hnv
);
230 if (e
== DD_NON_CONSTANT
|| !cuddIsConstant(e
) || t
!= e
) {
231 cuddCacheInsert(dd
, DD_ADD_ITE_CONSTANT_TAG
, f
, g
, h
, DD_NON_CONSTANT
);
232 return(DD_NON_CONSTANT
);
234 cuddCacheInsert(dd
, DD_ADD_ITE_CONSTANT_TAG
, f
, g
, h
, t
);
237 } /* end of Cudd_addIteConstant */
240 /**Function********************************************************************
242 Synopsis [Checks whether ADD g is constant whenever ADD f is 1.]
244 Description [Checks whether ADD g is constant whenever ADD f is 1. f
245 must be a 0-1 ADD. Returns a pointer to the resulting ADD (which may
246 or may not be constant) or DD_NON_CONSTANT. If f is identically 0,
247 the check is assumed to be successful, and the background value is
248 returned. No new nodes are created.]
252 SeeAlso [Cudd_addIteConstant Cudd_addLeq]
254 ******************************************************************************/
262 DdNode
*Fv
,*Fnv
,*Gv
,*Gnv
,*r
,*t
,*e
;
263 unsigned int topf
,topg
;
266 assert(!Cudd_IsComplement(f
));
270 /* Terminal cases. */
271 if (f
== DD_ONE(dd
) || cuddIsConstant(g
)) {
274 if (f
== (zero
= DD_ZERO(dd
))) {
275 return(dd
->background
);
279 assert(!cuddIsConstant(f
));
281 /* From now on, f and g are known not to be constants. */
283 topf
= cuddI(dd
,f
->index
);
284 topg
= cuddI(dd
,g
->index
);
287 r
= cuddConstantLookup(dd
,DD_ADD_EVAL_CONST_TAG
,f
,g
,g
);
292 /* Compute cofactors. */
294 Fv
= cuddT(f
); Fnv
= cuddE(f
);
299 Gv
= cuddT(g
); Gnv
= cuddE(g
);
304 /* Recursive step. */
306 t
= Cudd_addEvalConst(dd
,Fv
,Gv
);
307 if (t
== DD_NON_CONSTANT
|| !cuddIsConstant(t
)) {
308 cuddCacheInsert2(dd
, Cudd_addEvalConst
, f
, g
, DD_NON_CONSTANT
);
309 return(DD_NON_CONSTANT
);
312 e
= Cudd_addEvalConst(dd
,Fnv
,Gnv
);
313 if (e
== DD_NON_CONSTANT
|| !cuddIsConstant(e
) || t
!= e
) {
314 cuddCacheInsert2(dd
, Cudd_addEvalConst
, f
, g
, DD_NON_CONSTANT
);
315 return(DD_NON_CONSTANT
);
318 cuddCacheInsert2(dd
,Cudd_addEvalConst
,f
,g
,t
);
320 } else { /* Fnv must be != zero */
321 e
= Cudd_addEvalConst(dd
,Fnv
,Gnv
);
322 cuddCacheInsert2(dd
, Cudd_addEvalConst
, f
, g
, e
);
326 } /* end of Cudd_addEvalConst */
329 /**Function********************************************************************
331 Synopsis [Computes the complement of an ADD a la C language.]
333 Description [Computes the complement of an ADD a la C language: The
334 complement of 0 is 1 and the complement of everything else is 0.
335 Returns a pointer to the resulting ADD if successful; NULL otherwise.]
339 SeeAlso [Cudd_addNegate]
341 ******************************************************************************/
351 res
= cuddAddCmplRecur(dd
,f
);
352 } while (dd
->reordered
== 1);
355 } /* end of Cudd_addCmpl */
358 /**Function********************************************************************
360 Synopsis [Determines whether f is less than or equal to g.]
362 Description [Returns 1 if f is less than or equal to g; 0 otherwise.
363 No new nodes are created. This procedure works for arbitrary ADDs.
364 For 0-1 ADDs Cudd_addEvalConst is more efficient.]
368 SeeAlso [Cudd_addIteConstant Cudd_addEvalConst Cudd_bddLeq]
370 ******************************************************************************/
377 DdNode
*tmp
, *fv
, *fvn
, *gv
, *gvn
;
378 unsigned int topf
, topg
, res
;
380 /* Terminal cases. */
381 if (f
== g
) return(1);
384 if (cuddIsConstant(f
)) {
385 if (cuddIsConstant(g
)) return(cuddV(f
) <= cuddV(g
));
386 if (f
== DD_MINUS_INFINITY(dd
)) return(1);
387 if (f
== DD_PLUS_INFINITY(dd
)) return(0); /* since f != g */
389 if (g
== DD_PLUS_INFINITY(dd
)) return(1);
390 if (g
== DD_MINUS_INFINITY(dd
)) return(0); /* since f != g */
393 tmp
= cuddCacheLookup2(dd
,(DD_CTFP
)Cudd_addLeq
,f
,g
);
395 return(tmp
== DD_ONE(dd
));
398 /* Compute cofactors. One of f and g is not constant. */
399 topf
= cuddI(dd
,f
->index
);
400 topg
= cuddI(dd
,g
->index
);
402 fv
= cuddT(f
); fvn
= cuddE(f
);
407 gv
= cuddT(g
); gvn
= cuddE(g
);
412 res
= Cudd_addLeq(dd
,fvn
,gvn
) && Cudd_addLeq(dd
,fv
,gv
);
414 /* Store result in cache and return. */
415 cuddCacheInsert2(dd
,(DD_CTFP
) Cudd_addLeq
,f
,g
,
416 Cudd_NotCond(DD_ONE(dd
),res
==0));
419 } /* end of Cudd_addLeq */
422 /*---------------------------------------------------------------------------*/
423 /* Definition of internal functions */
424 /*---------------------------------------------------------------------------*/
427 /**Function********************************************************************
429 Synopsis [Implements the recursive step of Cudd_addIte(f,g,h).]
431 Description [Implements the recursive step of Cudd_addIte(f,g,h).
432 Returns a pointer to the resulting ADD if successful; NULL
437 SeeAlso [Cudd_addIte]
439 ******************************************************************************/
448 DdNode
*r
,*Fv
,*Fnv
,*Gv
,*Gnv
,*Hv
,*Hnv
,*t
,*e
;
449 unsigned int topf
,topg
,toph
,v
;
455 /* One variable cases. */
456 if (f
== (one
= DD_ONE(dd
))) { /* ITE(1,G,H) = G */
459 if (f
== (zero
= DD_ZERO(dd
))) { /* ITE(0,G,H) = H */
463 /* From now on, f is known to not be a constant. */
464 addVarToConst(f
,&g
,&h
,one
,zero
);
466 /* Check remaining one variable cases. */
467 if (g
== h
) { /* ITE(F,G,G) = G */
471 if (g
== one
) { /* ITE(F,1,0) = F */
472 if (h
== zero
) return(f
);
475 topf
= cuddI(dd
,f
->index
);
476 topg
= cuddI(dd
,g
->index
);
477 toph
= cuddI(dd
,h
->index
);
478 v
= ddMin(topg
,toph
);
480 /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */
481 if (topf
< v
&& cuddT(f
) == one
&& cuddE(f
) == zero
) {
482 r
= cuddUniqueInter(dd
,(int)f
->index
,g
,h
);
485 if (topf
< v
&& cuddT(f
) == zero
&& cuddE(f
) == one
) {
486 r
= cuddUniqueInter(dd
,(int)f
->index
,h
,g
);
491 r
= cuddCacheLookup(dd
,DD_ADD_ITE_TAG
,f
,g
,h
);
496 /* Compute cofactors. */
498 v
= ddMin(topf
,v
); /* v = top_var(F,G,H) */
500 Fv
= cuddT(f
); Fnv
= cuddE(f
);
506 Gv
= cuddT(g
); Gnv
= cuddE(g
);
512 Hv
= cuddT(h
); Hnv
= cuddE(h
);
517 /* Recursive step. */
518 t
= cuddAddIteRecur(dd
,Fv
,Gv
,Hv
);
519 if (t
== NULL
) return(NULL
);
522 e
= cuddAddIteRecur(dd
,Fnv
,Gnv
,Hnv
);
524 Cudd_RecursiveDeref(dd
,t
);
529 r
= (t
== e
) ? t
: cuddUniqueInter(dd
,index
,t
,e
);
531 Cudd_RecursiveDeref(dd
,t
);
532 Cudd_RecursiveDeref(dd
,e
);
538 cuddCacheInsert(dd
,DD_ADD_ITE_TAG
,f
,g
,h
,r
);
542 } /* end of cuddAddIteRecur */
545 /**Function********************************************************************
547 Synopsis [Performs the recursive step of Cudd_addCmpl.]
549 Description [Performs the recursive step of Cudd_addCmpl. Returns a
550 pointer to the resulting ADD if successful; NULL otherwise.]
554 SeeAlso [Cudd_addCmpl]
556 ******************************************************************************/
563 DdNode
*r
,*Fv
,*Fnv
,*t
,*e
;
569 if (cuddIsConstant(f
)) {
576 r
= cuddCacheLookup1(dd
,Cudd_addCmpl
,f
);
582 t
= cuddAddCmplRecur(dd
,Fv
);
583 if (t
== NULL
) return(NULL
);
585 e
= cuddAddCmplRecur(dd
,Fnv
);
587 Cudd_RecursiveDeref(dd
,t
);
591 r
= (t
== e
) ? t
: cuddUniqueInter(dd
,(int)f
->index
,t
,e
);
593 Cudd_RecursiveDeref(dd
, t
);
594 Cudd_RecursiveDeref(dd
, e
);
599 cuddCacheInsert1(dd
,Cudd_addCmpl
,f
,r
);
602 } /* end of cuddAddCmplRecur */
605 /*---------------------------------------------------------------------------*/
606 /* Definition of static functions */
607 /*---------------------------------------------------------------------------*/
610 /**Function********************************************************************
612 Synopsis [Replaces variables with constants if possible (part of
619 ******************************************************************************/
631 if (f
== g
) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
635 if (f
== h
) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
639 } /* end of addVarToConst */