diff options
Diffstat (limited to 'src/bdd/cudd/cuddAddNeg.c')
-rw-r--r-- | src/bdd/cudd/cuddAddNeg.c | 101 |
1 files changed, 65 insertions, 36 deletions
diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c index d99d0357..c21c995a 100644 --- a/src/bdd/cudd/cuddAddNeg.c +++ b/src/bdd/cudd/cuddAddNeg.c @@ -4,35 +4,63 @@ PackageName [cudd] - Synopsis [function to compute the negation of an ADD.] + Synopsis [Function to compute the negation of an ADD.] Description [External procedures included in this module: - <ul> - <li> Cudd_addNegate() - <li> Cudd_addRoundOff() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddAddNegateRecur() - <li> cuddAddRoundOffRecur() - </ul> ] + <ul> + <li> Cudd_addNegate() + <li> Cudd_addRoundOff() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddAddNegateRecur() + <li> cuddAddRoundOffRecur() + </ul> ] Author [Fabio Somenzi, Balakrishna Kumthekar] - 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.] ******************************************************************************/ -#include "util_hack.h" +#include "util_hack.h" #include "cuddInt.h" ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -53,7 +81,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.1.1.1 2003/02/24 22:23:50 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddAddNeg.c,v 1.12 2009/02/20 02:14:58 fabio Exp $"; #endif @@ -96,7 +124,7 @@ Cudd_addNegate( DdNode *res; do { - res = cuddAddNegateRecur(dd,f); + res = cuddAddNegateRecur(dd,f); } while (dd->reordered == 1); return(res); @@ -126,7 +154,7 @@ Cudd_addRoundOff( double trunc = pow(10.0,(double)N); do { - res = cuddAddRoundOffRecur(dd,f,trunc); + res = cuddAddRoundOffRecur(dd,f,trunc); } while (dd->reordered == 1); return(res); @@ -154,14 +182,14 @@ cuddAddNegateRecur( DdNode * f) { DdNode *res, - *fv, *fvn, - *T, *E; + *fv, *fvn, + *T, *E; statLine(dd); /* Check terminal cases. */ if (cuddIsConstant(f)) { - res = cuddUniqueConst(dd,-cuddV(f)); - return(res); + res = cuddUniqueConst(dd,-cuddV(f)); + return(res); } /* Check cache */ @@ -177,15 +205,15 @@ cuddAddNegateRecur( E = cuddAddNegateRecur(dd,fvn); if (E == NULL) { - Cudd_RecursiveDeref(dd,T); - return(NULL); + Cudd_RecursiveDeref(dd,T); + return(NULL); } cuddRef(E); res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E); if (res == 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); @@ -217,15 +245,15 @@ cuddAddRoundOffRecur( DdNode *res, *fv, *fvn, *T, *E; double n; - DdNode *(*cacheOp)(DdManager *, DdNode *); - + DD_CTFP1 cacheOp; + statLine(dd); if (cuddIsConstant(f)) { n = ceil(cuddV(f)*trunc)/trunc; - res = cuddUniqueConst(dd,n); - return(res); + res = cuddUniqueConst(dd,n); + return(res); } - cacheOp = (DdNode *(*)(DdManager *, DdNode *)) Cudd_addRoundOff; + cacheOp = (DD_CTFP1) Cudd_addRoundOff; res = cuddCacheLookup1(dd,cacheOp,f); if (res != NULL) { return(res); @@ -241,14 +269,14 @@ cuddAddRoundOffRecur( E = cuddAddRoundOffRecur(dd,fvn,trunc); if (E == NULL) { Cudd_RecursiveDeref(dd,T); - return(NULL); + return(NULL); } cuddRef(E); res = (T == E) ? T : cuddUniqueInter(dd,(int)f->index,T,E); if (res == NULL) { Cudd_RecursiveDeref(dd,T); - Cudd_RecursiveDeref(dd,E); - return(NULL); + Cudd_RecursiveDeref(dd,E); + return(NULL); } cuddDeref(T); cuddDeref(E); @@ -256,12 +284,13 @@ cuddAddRoundOffRecur( /* Store result. */ cuddCacheInsert1(dd,cacheOp,f,res); return(res); - + } /* end of cuddAddRoundOffRecur */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ + ABC_NAMESPACE_IMPL_END |