src/cuBdd/cuddCof.c File Reference
#include "util.h"#include "cuddInt.h"
Go to the source code of this file.
Functions | |
| DdNode * | Cudd_Cofactor (DdManager *dd, DdNode *f, DdNode *g) |
| void | cuddGetBranches (DdNode *g, DdNode **g1, DdNode **g0) |
| int | cuddCheckCube (DdManager *dd, DdNode *g) |
| DdNode * | cuddCofactorRecur (DdManager *dd, DdNode *f, DdNode *g) |
Variables | |
| static char rcsid[] | DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $" |
Function Documentation
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Computes the cofactor of f with respect to g.]
Description [Computes the cofactor of f with respect to g; g must be the BDD or the ADD of a cube. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_bddConstrain Cudd_bddRestrict]
Definition at line 119 of file cuddCof.c.
00123 { 00124 DdNode *res,*zero; 00125 00126 zero = Cudd_Not(DD_ONE(dd)); 00127 if (g == zero || g == DD_ZERO(dd)) { 00128 (void) fprintf(dd->err,"Cudd_Cofactor: Invalid restriction 1\n"); 00129 dd->errorCode = CUDD_INVALID_ARG; 00130 return(NULL); 00131 } 00132 do { 00133 dd->reordered = 0; 00134 res = cuddCofactorRecur(dd,f,g); 00135 } while (dd->reordered == 1); 00136 return(res); 00137 00138 } /* end of Cudd_Cofactor */
Function********************************************************************
Synopsis [Checks whether g is the BDD of a cube.]
Description [Checks whether g is the BDD of a cube. Returns 1 in case of success; 0 otherwise. The constant 1 is a valid cube, but all other constant functions cause cuddCheckCube to return 0.]
SideEffects [None]
SeeAlso []
Definition at line 189 of file cuddCof.c.
00192 { 00193 DdNode *g1,*g0,*one,*zero; 00194 00195 one = DD_ONE(dd); 00196 if (g == one) return(1); 00197 if (Cudd_IsConstant(g)) return(0); 00198 00199 zero = Cudd_Not(one); 00200 cuddGetBranches(g,&g1,&g0); 00201 00202 if (g0 == zero) { 00203 return(cuddCheckCube(dd, g1)); 00204 } 00205 if (g1 == zero) { 00206 return(cuddCheckCube(dd, g0)); 00207 } 00208 return(0); 00209 00210 } /* end of cuddCheckCube */
Function********************************************************************
Synopsis [Performs the recursive step of Cudd_Cofactor.]
Description [Performs the recursive step of Cudd_Cofactor. Returns a pointer to the cofactor if successful; NULL otherwise.]
SideEffects [None]
SeeAlso [Cudd_Cofactor]
Definition at line 226 of file cuddCof.c.
00230 { 00231 DdNode *one,*zero,*F,*G,*g1,*g0,*f1,*f0,*t,*e,*r; 00232 unsigned int topf,topg; 00233 int comple; 00234 00235 statLine(dd); 00236 F = Cudd_Regular(f); 00237 if (cuddIsConstant(F)) return(f); 00238 00239 one = DD_ONE(dd); 00240 00241 /* The invariant g != 0 is true on entry to this procedure and is 00242 ** recursively maintained by it. Therefore it suffices to test g 00243 ** against one to make sure it is not constant. 00244 */ 00245 if (g == one) return(f); 00246 /* From now on, f and g are known not to be constants. */ 00247 00248 comple = f != F; 00249 r = cuddCacheLookup2(dd,Cudd_Cofactor,F,g); 00250 if (r != NULL) { 00251 return(Cudd_NotCond(r,comple)); 00252 } 00253 00254 topf = dd->perm[F->index]; 00255 G = Cudd_Regular(g); 00256 topg = dd->perm[G->index]; 00257 00258 /* We take the cofactors of F because we are going to rely on 00259 ** the fact that the cofactors of the complement are the complements 00260 ** of the cofactors to better utilize the cache. Variable comple 00261 ** remembers whether we have to complement the result or not. 00262 */ 00263 if (topf <= topg) { 00264 f1 = cuddT(F); f0 = cuddE(F); 00265 } else { 00266 f1 = f0 = F; 00267 } 00268 if (topg <= topf) { 00269 g1 = cuddT(G); g0 = cuddE(G); 00270 if (g != G) { g1 = Cudd_Not(g1); g0 = Cudd_Not(g0); } 00271 } else { 00272 g1 = g0 = g; 00273 } 00274 00275 zero = Cudd_Not(one); 00276 if (topf >= topg) { 00277 if (g0 == zero || g0 == DD_ZERO(dd)) { 00278 r = cuddCofactorRecur(dd, f1, g1); 00279 } else if (g1 == zero || g1 == DD_ZERO(dd)) { 00280 r = cuddCofactorRecur(dd, f0, g0); 00281 } else { 00282 (void) fprintf(dd->out, 00283 "Cudd_Cofactor: Invalid restriction 2\n"); 00284 dd->errorCode = CUDD_INVALID_ARG; 00285 return(NULL); 00286 } 00287 if (r == NULL) return(NULL); 00288 } else /* if (topf < topg) */ { 00289 t = cuddCofactorRecur(dd, f1, g); 00290 if (t == NULL) return(NULL); 00291 cuddRef(t); 00292 e = cuddCofactorRecur(dd, f0, g); 00293 if (e == NULL) { 00294 Cudd_RecursiveDeref(dd, t); 00295 return(NULL); 00296 } 00297 cuddRef(e); 00298 00299 if (t == e) { 00300 r = t; 00301 } else if (Cudd_IsComplement(t)) { 00302 r = cuddUniqueInter(dd,(int)F->index,Cudd_Not(t),Cudd_Not(e)); 00303 if (r != NULL) 00304 r = Cudd_Not(r); 00305 } else { 00306 r = cuddUniqueInter(dd,(int)F->index,t,e); 00307 } 00308 if (r == NULL) { 00309 Cudd_RecursiveDeref(dd ,e); 00310 Cudd_RecursiveDeref(dd ,t); 00311 return(NULL); 00312 } 00313 cuddDeref(t); 00314 cuddDeref(e); 00315 } 00316 00317 cuddCacheInsert2(dd,Cudd_Cofactor,F,g,r); 00318 00319 return(Cudd_NotCond(r,comple)); 00320 00321 } /* end of cuddCofactorRecur */
Function********************************************************************
Synopsis [Computes the children of g.]
Description []
SideEffects [None]
SeeAlso []
Definition at line 158 of file cuddCof.c.
00162 { 00163 DdNode *G = Cudd_Regular(g); 00164 00165 *g1 = cuddT(G); 00166 *g0 = cuddE(G); 00167 if (Cudd_IsComplement(g)) { 00168 *g1 = Cudd_Not(*g1); 00169 *g0 = Cudd_Not(*g0); 00170 } 00171 00172 } /* end of cuddGetBranches */
Variable Documentation
char rcsid [] DD_UNUSED = "$Id: cuddCof.c,v 1.9 2004/08/13 18:04:47 fabio Exp $" [static] |
CFile***********************************************************************
FileName [cuddCof.c]
PackageName [cudd]
Synopsis [Cofactoring functions.]
Description [External procedures included in this module:
Internal procedures included in this module:
]
SeeAlso []
Author [Fabio Somenzi]
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.]
