diff options
Diffstat (limited to 'src/bdd/cudd/cuddSolve.c')
-rw-r--r-- | src/bdd/cudd/cuddSolve.c | 168 |
1 files changed, 99 insertions, 69 deletions
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c index 18d29dac..47570bf1 100644 --- a/src/bdd/cudd/cuddSolve.c +++ b/src/bdd/cudd/cuddSolve.c @@ -7,24 +7,51 @@ Synopsis [Boolean equation solver and related functions.] Description [External functions included in this modoule: - <ul> - <li> Cudd_SolveEqn() - <li> Cudd_VerifySol() - </ul> - Internal functions included in this module: - <ul> - <li> cuddSolveEqnRecur() - <li> cuddVerifySol() - </ul> ] + <ul> + <li> Cudd_SolveEqn() + <li> Cudd_VerifySol() + </ul> + Internal functions included in this module: + <ul> + <li> cuddSolveEqnRecur() + <li> cuddVerifySol() + </ul> ] SeeAlso [] Author [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.] ******************************************************************************/ @@ -34,6 +61,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -54,7 +82,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddSolve.c,v 1.12 2004/08/13 18:04:51 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -108,15 +136,15 @@ Cudd_SolveEqn( *yIndex = temp = ABC_ALLOC(int, n); if (temp == NULL) { - bdd->errorCode = CUDD_MEMORY_OUT; - (void) fprintf(bdd->out, - "Cudd_SolveEqn: Out of memory for yIndex\n"); - return(NULL); + bdd->errorCode = CUDD_MEMORY_OUT; + (void) fprintf(bdd->out, + "Cudd_SolveEqn: Out of memory for yIndex\n"); + return(NULL); } do { - bdd->reordered = 0; - res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0); + bdd->reordered = 0; + res = cuddSolveEqnRecur(bdd, F, Y, G, n, temp, 0); } while (bdd->reordered == 1); return(res); @@ -148,8 +176,8 @@ Cudd_VerifySol( DdNode *res; do { - bdd->reordered = 0; - res = cuddVerifySol(bdd, F, G, yIndex, n); + bdd->reordered = 0; + res = cuddVerifySol(bdd, F, G, yIndex, n); } while (bdd->reordered == 1); ABC_FREE(yIndex); @@ -199,7 +227,7 @@ cuddSolveEqnRecur( /* Base condition. */ if (Y == one) { - return F; + return F; } /* Cofactor of Y. */ @@ -209,61 +237,61 @@ cuddSolveEqnRecur( /* Universal abstraction of F with respect to the top variable index. */ Fm1 = cuddBddExistAbstractRecur(bdd, Cudd_Not(F), variables[yIndex[i]]); if (Fm1) { - Fm1 = Cudd_Not(Fm1); - cuddRef(Fm1); + Fm1 = Cudd_Not(Fm1); + cuddRef(Fm1); } else { - return(NULL); + return(NULL); } Fn = cuddSolveEqnRecur(bdd, Fm1, nextY, G, n, yIndex, i+1); if (Fn) { - cuddRef(Fn); + cuddRef(Fn); } else { - Cudd_RecursiveDeref(bdd, Fm1); - return(NULL); + Cudd_RecursiveDeref(bdd, Fm1); + return(NULL); } Fv = cuddCofactorRecur(bdd, F, variables[yIndex[i]]); if (Fv) { - cuddRef(Fv); + cuddRef(Fv); } else { - Cudd_RecursiveDeref(bdd, Fm1); - Cudd_RecursiveDeref(bdd, Fn); - return(NULL); + Cudd_RecursiveDeref(bdd, Fm1); + Cudd_RecursiveDeref(bdd, Fn); + return(NULL); } Fvbar = cuddCofactorRecur(bdd, F, Cudd_Not(variables[yIndex[i]])); if (Fvbar) { - cuddRef(Fvbar); + cuddRef(Fvbar); } else { - Cudd_RecursiveDeref(bdd, Fm1); - Cudd_RecursiveDeref(bdd, Fn); - Cudd_RecursiveDeref(bdd, Fv); - return(NULL); + Cudd_RecursiveDeref(bdd, Fm1); + Cudd_RecursiveDeref(bdd, Fn); + Cudd_RecursiveDeref(bdd, Fv); + return(NULL); } /* Build i-th component of the solution. */ w = cuddBddIteRecur(bdd, variables[yIndex[i]], Cudd_Not(Fv), Fvbar); if (w) { - cuddRef(w); + cuddRef(w); } else { - Cudd_RecursiveDeref(bdd, Fm1); - Cudd_RecursiveDeref(bdd, Fn); - Cudd_RecursiveDeref(bdd, Fv); - Cudd_RecursiveDeref(bdd, Fvbar); - return(NULL); + Cudd_RecursiveDeref(bdd, Fm1); + Cudd_RecursiveDeref(bdd, Fn); + Cudd_RecursiveDeref(bdd, Fv); + Cudd_RecursiveDeref(bdd, Fvbar); + return(NULL); } T = cuddBddRestrictRecur(bdd, w, Cudd_Not(Fm1)); if(T) { - cuddRef(T); + cuddRef(T); } else { - Cudd_RecursiveDeref(bdd, Fm1); - Cudd_RecursiveDeref(bdd, Fn); - Cudd_RecursiveDeref(bdd, Fv); - Cudd_RecursiveDeref(bdd, Fvbar); - Cudd_RecursiveDeref(bdd, w); - return(NULL); + Cudd_RecursiveDeref(bdd, Fm1); + Cudd_RecursiveDeref(bdd, Fn); + Cudd_RecursiveDeref(bdd, Fv); + Cudd_RecursiveDeref(bdd, Fvbar); + Cudd_RecursiveDeref(bdd, w); + return(NULL); } Cudd_RecursiveDeref(bdd,Fm1); @@ -273,16 +301,16 @@ cuddSolveEqnRecur( /* Substitute components of solution already found into solution. */ for (j = n-1; j > i; j--) { - w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]); - if(w) { - cuddRef(w); - } else { - Cudd_RecursiveDeref(bdd, Fn); - Cudd_RecursiveDeref(bdd, T); - return(NULL); - } - Cudd_RecursiveDeref(bdd,T); - T = w; + w = cuddBddComposeRecur(bdd,T, G[j], variables[yIndex[j]]); + if(w) { + cuddRef(w); + } else { + Cudd_RecursiveDeref(bdd, Fn); + Cudd_RecursiveDeref(bdd, T); + return(NULL); + } + Cudd_RecursiveDeref(bdd,T); + T = w; } G[i] = T; @@ -319,14 +347,14 @@ cuddVerifySol( R = F; cuddRef(R); for(j = n - 1; j >= 0; j--) { - w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]); - if (w) { - cuddRef(w); - } else { - return(NULL); - } - Cudd_RecursiveDeref(bdd,R); - R = w; + w = Cudd_bddCompose(bdd, R, G[j], yIndex[j]); + if (w) { + cuddRef(w); + } else { + return(NULL); + } + Cudd_RecursiveDeref(bdd,R); + R = w; } cuddDeref(R); @@ -340,5 +368,7 @@ cuddVerifySol( /* Definition of static functions */ /*---------------------------------------------------------------------------*/ + ABC_NAMESPACE_IMPL_END + |