From e7b544f11151f09a4a3fbe39b4a176795a82f677 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 13:42:25 -0800 Subject: Upgrade to the latest CUDD 2.4.2. --- src/bdd/cudd/cuddAddIte.c | 211 ++++++++++++++++++++++++++-------------------- 1 file changed, 120 insertions(+), 91 deletions(-) (limited to 'src/bdd/cudd/cuddAddIte.c') diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c index def55537..67f1cf14 100644 --- a/src/bdd/cudd/cuddAddIte.c +++ b/src/bdd/cudd/cuddAddIte.c @@ -7,29 +7,56 @@ Synopsis [ADD ITE function and satellites.] Description [External procedures included in this module: - - Internal procedures included in this module: - - Static procedures included in this module: - ] + + Internal procedures included in this module: + + Static procedures included in this module: + ] Author [Fabio Somenzi] - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ @@ -39,6 +66,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -59,7 +87,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.15 2004/08/13 18:04:45 fabio Exp $"; #endif @@ -74,7 +102,7 @@ static char rcsid[] DD_UNUSED = "$Id: cuddAddIte.c,v 1.1.1.1 2003/02/24 22:23:50 /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static void addVarToConst ARGS((DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero)); +static void addVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *one, DdNode *zero); /**AutomaticEnd***************************************************************/ @@ -107,8 +135,8 @@ Cudd_addIte( DdNode *res; do { - dd->reordered = 0; - res = cuddAddIteRecur(dd,f,g,h); + dd->reordered = 0; + res = cuddAddIteRecur(dd,f,g,h); } while (dd->reordered == 1); return(res); @@ -144,7 +172,7 @@ Cudd_addIteConstant( statLine(dd); /* Trivial cases. */ - if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */ + if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */ return(g); } if (f == (zero = DD_ZERO(dd))) { /* ITE(0,G,H) = H */ @@ -155,7 +183,7 @@ Cudd_addIteConstant( addVarToConst(f,&g,&h,one,zero); /* Check remaining one variable cases. */ - if (g == h) { /* ITE(F,G,G) = G */ + if (g == h) { /* ITE(F,G,G) = G */ return(g); } if (cuddIsConstant(g) && cuddIsConstant(h)) { @@ -169,7 +197,7 @@ Cudd_addIteConstant( /* ITE(F,G,H) = (x,G,H) (non constant) if F = (x,1,0), x < top(G,H). */ if (topf < v && cuddIsConstant(cuddT(f)) && cuddIsConstant(cuddE(f))) { - return(DD_NON_CONSTANT); + return(DD_NON_CONSTANT); } /* Check cache. */ @@ -180,7 +208,7 @@ Cudd_addIteConstant( /* Compute cofactors. */ if (topf <= v) { - v = ddMin(topf,v); /* v = top_var(F,G,H) */ + v = ddMin(topf,v); /* v = top_var(F,G,H) */ Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; @@ -199,13 +227,13 @@ Cudd_addIteConstant( /* Recursive step. */ t = Cudd_addIteConstant(dd,Fv,Gv,Hv); if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) { - cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); - return(DD_NON_CONSTANT); + cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); } e = Cudd_addIteConstant(dd,Fnv,Gnv,Hnv); if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) { - cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); - return(DD_NON_CONSTANT); + cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); } cuddCacheInsert(dd, DD_ADD_ITE_CONSTANT_TAG, f, g, h, t); return(t); @@ -279,24 +307,24 @@ Cudd_addEvalConst( /* Recursive step. */ if (Fv != zero) { - t = Cudd_addEvalConst(dd,Fv,Gv); - if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) { - cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT); - return(DD_NON_CONSTANT); - } - if (Fnv != zero) { - e = Cudd_addEvalConst(dd,Fnv,Gnv); - if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) { - cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT); - return(DD_NON_CONSTANT); + t = Cudd_addEvalConst(dd,Fv,Gv); + if (t == DD_NON_CONSTANT || !cuddIsConstant(t)) { + cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); } - } - cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t); - return(t); + if (Fnv != zero) { + e = Cudd_addEvalConst(dd,Fnv,Gnv); + if (e == DD_NON_CONSTANT || !cuddIsConstant(e) || t != e) { + cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, DD_NON_CONSTANT); + return(DD_NON_CONSTANT); + } + } + cuddCacheInsert2(dd,Cudd_addEvalConst,f,g,t); + return(t); } else { /* Fnv must be != zero */ - e = Cudd_addEvalConst(dd,Fnv,Gnv); - cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e); - return(e); + e = Cudd_addEvalConst(dd,Fnv,Gnv); + cuddCacheInsert2(dd, Cudd_addEvalConst, f, g, e); + return(e); } } /* end of Cudd_addEvalConst */ @@ -323,8 +351,8 @@ Cudd_addCmpl( DdNode *res; do { - dd->reordered = 0; - res = cuddAddCmplRecur(dd,f); + dd->reordered = 0; + res = cuddAddCmplRecur(dd,f); } while (dd->reordered == 1); return(res); @@ -358,39 +386,38 @@ Cudd_addLeq( statLine(dd); if (cuddIsConstant(f)) { - if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g)); - if (f == DD_MINUS_INFINITY(dd)) return(1); - if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */ + if (cuddIsConstant(g)) return(cuddV(f) <= cuddV(g)); + if (f == DD_MINUS_INFINITY(dd)) return(1); + if (f == DD_PLUS_INFINITY(dd)) return(0); /* since f != g */ } if (g == DD_PLUS_INFINITY(dd)) return(1); if (g == DD_MINUS_INFINITY(dd)) return(0); /* since f != g */ /* Check cache. */ - tmp = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *, - DdNode *))Cudd_addLeq,f,g); + tmp = cuddCacheLookup2(dd,(DD_CTFP)Cudd_addLeq,f,g); if (tmp != NULL) { - return(tmp == DD_ONE(dd)); + return(tmp == DD_ONE(dd)); } /* Compute cofactors. One of f and g is not constant. */ topf = cuddI(dd,f->index); topg = cuddI(dd,g->index); if (topf <= topg) { - fv = cuddT(f); fvn = cuddE(f); + fv = cuddT(f); fvn = cuddE(f); } else { - fv = fvn = f; + fv = fvn = f; } if (topg <= topf) { - gv = cuddT(g); gvn = cuddE(g); + gv = cuddT(g); gvn = cuddE(g); } else { - gv = gvn = g; + gv = gvn = g; } res = Cudd_addLeq(dd,fvn,gvn) && Cudd_addLeq(dd,fv,gv); /* Store result in cache and return. */ - cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, DdNode *)) - Cudd_addLeq,f,g,Cudd_NotCond(DD_ONE(dd),res==0)); + cuddCacheInsert2(dd,(DD_CTFP) Cudd_addLeq,f,g, + Cudd_NotCond(DD_ONE(dd),res==0)); return(res); } /* end of Cudd_addLeq */ @@ -424,13 +451,13 @@ cuddAddIteRecur( DdNode *one,*zero; DdNode *r,*Fv,*Fnv,*Gv,*Gnv,*Hv,*Hnv,*t,*e; unsigned int topf,topg,toph,v; - int index = 0; // Suppress "might be used uninitialized" + int index; statLine(dd); /* Trivial cases. */ /* One variable cases. */ - if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */ + if (f == (one = DD_ONE(dd))) { /* ITE(1,G,H) = G */ return(g); } if (f == (zero = DD_ZERO(dd))) { /* ITE(0,G,H) = H */ @@ -441,11 +468,11 @@ cuddAddIteRecur( addVarToConst(f,&g,&h,one,zero); /* Check remaining one variable cases. */ - if (g == h) { /* ITE(F,G,G) = G */ + if (g == h) { /* ITE(F,G,G) = G */ return(g); } - if (g == one) { /* ITE(F,1,0) = F */ + if (g == one) { /* ITE(F,1,0) = F */ if (h == zero) return(f); } @@ -456,12 +483,12 @@ cuddAddIteRecur( /* A shortcut: ITE(F,G,H) = (x,G,H) if F=(x,1,0), x < top(G,H). */ if (topf < v && cuddT(f) == one && cuddE(f) == zero) { - r = cuddUniqueInter(dd,(int)f->index,g,h); - return(r); + r = cuddUniqueInter(dd,(int)f->index,g,h); + return(r); } if (topf < v && cuddT(f) == zero && cuddE(f) == one) { - r = cuddUniqueInter(dd,(int)f->index,h,g); - return(r); + r = cuddUniqueInter(dd,(int)f->index,h,g); + return(r); } /* Check cache. */ @@ -472,20 +499,20 @@ cuddAddIteRecur( /* Compute cofactors. */ if (topf <= v) { - v = ddMin(topf,v); /* v = top_var(F,G,H) */ - index = f->index; + v = ddMin(topf,v); /* v = top_var(F,G,H) */ + index = f->index; Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; } if (topg == v) { - index = g->index; + index = g->index; Gv = cuddT(g); Gnv = cuddE(g); } else { Gv = Gnv = g; } if (toph == v) { - index = h->index; + index = h->index; Hv = cuddT(h); Hnv = cuddE(h); } else { Hv = Hnv = h; @@ -498,16 +525,16 @@ cuddAddIteRecur( e = cuddAddIteRecur(dd,Fnv,Gnv,Hnv); if (e == NULL) { - Cudd_RecursiveDeref(dd,t); - return(NULL); + Cudd_RecursiveDeref(dd,t); + return(NULL); } cuddRef(e); r = (t == e) ? t : cuddUniqueInter(dd,index,t,e); if (r == NULL) { - Cudd_RecursiveDeref(dd,t); - Cudd_RecursiveDeref(dd,e); - return(NULL); + Cudd_RecursiveDeref(dd,t); + Cudd_RecursiveDeref(dd,e); + return(NULL); } cuddDeref(t); cuddDeref(e); @@ -545,14 +572,14 @@ cuddAddCmplRecur( if (cuddIsConstant(f)) { if (f == zero) { - return(one); - } else { - return(zero); - } + return(one); + } else { + return(zero); + } } r = cuddCacheLookup1(dd,Cudd_addCmpl,f); if (r != NULL) { - return(r); + return(r); } Fv = cuddT(f); Fnv = cuddE(f); @@ -561,15 +588,15 @@ cuddAddCmplRecur( cuddRef(t); e = cuddAddCmplRecur(dd,Fnv); if (e == NULL) { - Cudd_RecursiveDeref(dd,t); - return(NULL); + Cudd_RecursiveDeref(dd,t); + return(NULL); } cuddRef(e); r = (t == e) ? t : cuddUniqueInter(dd,(int)f->index,t,e); if (r == NULL) { - Cudd_RecursiveDeref(dd, t); - Cudd_RecursiveDeref(dd, e); - return(NULL); + Cudd_RecursiveDeref(dd, t); + Cudd_RecursiveDeref(dd, e); + return(NULL); } cuddDeref(t); cuddDeref(e); @@ -606,13 +633,15 @@ addVarToConst( DdNode *h = *hp; if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */ - *gp = one; + *gp = one; } if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */ - *hp = zero; + *hp = zero; } } /* end of addVarToConst */ + + ABC_NAMESPACE_IMPL_END -- cgit v1.2.3