src/misc/extra/extraBddAuto.c File Reference
#include "extra.h"
Include dependency graph for extraBddAuto.c:
Go to the source code of this file.
Function Documentation
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 313 of file extraBddAuto.c.
00314 { 00315 DdNode * bRes; 00316 do { 00317 dd->reordered = 0; 00318 bRes = extraBddSpaceCanonVars( dd, bSpace ); 00319 } while (dd->reordered == 1); 00320 return bRes; 00321 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 358 of file extraBddAuto.c.
00359 { 00360 DdNode * zRes; 00361 DdNode * zEquPos; 00362 DdNode * zEquNeg; 00363 zEquPos = Extra_bddSpaceEquationsPos( dd, bSpace ); Cudd_Ref( zEquPos ); 00364 zEquNeg = Extra_bddSpaceEquationsNeg( dd, bSpace ); Cudd_Ref( zEquNeg ); 00365 zRes = Cudd_zddUnion( dd, zEquPos, zEquNeg ); Cudd_Ref( zRes ); 00366 Cudd_RecursiveDerefZdd( dd, zEquPos ); 00367 Cudd_RecursiveDerefZdd( dd, zEquNeg ); 00368 Cudd_Deref( zRes ); 00369 return zRes; 00370 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 406 of file extraBddAuto.c.
00407 { 00408 DdNode * zRes; 00409 do { 00410 dd->reordered = 0; 00411 zRes = extraBddSpaceEquationsNeg( dd, bSpace ); 00412 } while (dd->reordered == 1); 00413 return zRes; 00414 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 384 of file extraBddAuto.c.
00385 { 00386 DdNode * zRes; 00387 do { 00388 dd->reordered = 0; 00389 zRes = extraBddSpaceEquationsPos( dd, bSpace ); 00390 } while (dd->reordered == 1); 00391 return zRes; 00392 }
Function*************************************************************
Synopsis []
Description [Returns the array of ZDDs with the number equal to the number of vars in the DD manager. If the given var is non-canonical, this array contains the referenced ZDD representing literals in the corresponding EXOR equation.]
SideEffects []
SeeAlso []
Definition at line 494 of file extraBddAuto.c.
00495 { 00496 DdNode ** pzRes; 00497 int * pVarsNonCan; 00498 DdNode * zEquRem; 00499 int iVarNonCan; 00500 DdNode * zExor, * zTemp; 00501 00502 // get the set of non-canonical variables 00503 pVarsNonCan = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); 00504 Extra_SupportArray( dd, bFuncRed, pVarsNonCan ); 00505 00506 // allocate storage for the EXOR sets 00507 pzRes = ALLOC( DdNode *, dd->size ); 00508 memset( pzRes, 0, sizeof(DdNode *) * dd->size ); 00509 00510 // go through all the equations 00511 zEquRem = zEquations; Cudd_Ref( zEquRem ); 00512 while ( zEquRem != z0 ) 00513 { 00514 // extract one product 00515 zExor = Extra_zddSelectOneSubset( dd, zEquRem ); Cudd_Ref( zExor ); 00516 // remove it from the set 00517 zEquRem = Cudd_zddDiff( dd, zTemp = zEquRem, zExor ); Cudd_Ref( zEquRem ); 00518 Cudd_RecursiveDerefZdd( dd, zTemp ); 00519 00520 // locate the non-canonical variable 00521 iVarNonCan = -1; 00522 for ( zTemp = zExor; zTemp != z1; zTemp = cuddT(zTemp) ) 00523 { 00524 if ( pVarsNonCan[zTemp->index/2] == 1 ) 00525 { 00526 assert( iVarNonCan == -1 ); 00527 iVarNonCan = zTemp->index/2; 00528 } 00529 } 00530 assert( iVarNonCan != -1 ); 00531 00532 if ( Extra_zddLitCountComb( dd, zExor ) > 1 ) 00533 pzRes[ iVarNonCan ] = zExor; // takes ref 00534 else 00535 Cudd_RecursiveDerefZdd( dd, zExor ); 00536 } 00537 Cudd_RecursiveDerefZdd( dd, zEquRem ); 00538 00539 free( pVarsNonCan ); 00540 return pzRes; 00541 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 250 of file extraBddAuto.c.
00251 { 00252 DdNode * bRes; 00253 do { 00254 dd->reordered = 0; 00255 bRes = extraBddSpaceFromFunction( dd, bF, bG ); 00256 } while (dd->reordered == 1); 00257 return bRes; 00258 }
CFile****************************************************************
FileName [extraBddAuto.c]
PackageName [extra]
Synopsis [Computation of autosymmetries.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 2.0. Started - September 1, 2003.]
Revision [
- Id
- extraBddAuto.c,v 1.0 2003/05/21 18:03:50 alanmi Exp
]AutomaticStart AutomaticEnd Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 150 of file extraBddAuto.c.
00151 { 00152 int * pSupport; 00153 int * pPermute; 00154 int * pPermuteBack; 00155 DdNode ** pCompose; 00156 DdNode * bCube, * bTemp; 00157 DdNode * bSpace, * bFunc1, * bFunc2, * bSpaceShift; 00158 int nSupp, Counter; 00159 int i, lev; 00160 00161 // get the support 00162 pSupport = ALLOC( int, ddMax(dd->size,dd->sizeZ) ); 00163 Extra_SupportArray( dd, bFunc, pSupport ); 00164 nSupp = 0; 00165 for ( i = 0; i < dd->size; i++ ) 00166 if ( pSupport[i] ) 00167 nSupp++; 00168 00169 // make sure the manager has enough variables 00170 if ( 2*nSupp > dd->size ) 00171 { 00172 printf( "Cannot derive linear space, because DD manager does not have enough variables.\n" ); 00173 fflush( stdout ); 00174 free( pSupport ); 00175 return NULL; 00176 } 00177 00178 // create the permutation arrays 00179 pPermute = ALLOC( int, dd->size ); 00180 pPermuteBack = ALLOC( int, dd->size ); 00181 pCompose = ALLOC( DdNode *, dd->size ); 00182 for ( i = 0; i < dd->size; i++ ) 00183 { 00184 pPermute[i] = i; 00185 pPermuteBack[i] = i; 00186 pCompose[i] = dd->vars[i]; Cudd_Ref( pCompose[i] ); 00187 } 00188 00189 // remap the function in such a way that the variables are interleaved 00190 Counter = 0; 00191 bCube = b1; Cudd_Ref( bCube ); 00192 for ( lev = 0; lev < dd->size; lev++ ) 00193 if ( pSupport[ dd->invperm[lev] ] ) 00194 { // var "dd->invperm[lev]" on level "lev" should go to level 2*Counter; 00195 pPermute[ dd->invperm[lev] ] = dd->invperm[2*Counter]; 00196 // var from level 2*Counter+1 should go back to the place of this var 00197 pPermuteBack[ dd->invperm[2*Counter+1] ] = dd->invperm[lev]; 00198 // the permutation should be defined in such a way that variable 00199 // on level 2*Counter is replaced by an EXOR of itself and var on the next level 00200 Cudd_Deref( pCompose[ dd->invperm[2*Counter] ] ); 00201 pCompose[ dd->invperm[2*Counter] ] = 00202 Cudd_bddXor( dd, dd->vars[ dd->invperm[2*Counter] ], dd->vars[ dd->invperm[2*Counter+1] ] ); 00203 Cudd_Ref( pCompose[ dd->invperm[2*Counter] ] ); 00204 // add this variable to the cube 00205 bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[ dd->invperm[2*Counter] ] ); Cudd_Ref( bCube ); 00206 Cudd_RecursiveDeref( dd, bTemp ); 00207 // increment the counter 00208 Counter ++; 00209 } 00210 00211 // permute the functions 00212 bFunc1 = Cudd_bddPermute( dd, bFunc, pPermute ); Cudd_Ref( bFunc1 ); 00213 // compose to gate the function depending on both vars 00214 bFunc2 = Cudd_bddVectorCompose( dd, bFunc1, pCompose ); Cudd_Ref( bFunc2 ); 00215 // gate the vector space 00216 // L(a) = ForAll x [ F(x) = F(x+a) ] = Not( Exist x [ F(x) (+) F(x+a) ] ) 00217 bSpaceShift = Cudd_bddXorExistAbstract( dd, bFunc1, bFunc2, bCube ); Cudd_Ref( bSpaceShift ); 00218 bSpaceShift = Cudd_Not( bSpaceShift ); 00219 // permute the space back into the original mapping 00220 bSpace = Cudd_bddPermute( dd, bSpaceShift, pPermuteBack ); Cudd_Ref( bSpace ); 00221 Cudd_RecursiveDeref( dd, bFunc1 ); 00222 Cudd_RecursiveDeref( dd, bFunc2 ); 00223 Cudd_RecursiveDeref( dd, bSpaceShift ); 00224 Cudd_RecursiveDeref( dd, bCube ); 00225 00226 for ( i = 0; i < dd->size; i++ ) 00227 Cudd_RecursiveDeref( dd, pCompose[i] ); 00228 free( pPermute ); 00229 free( pPermuteBack ); 00230 free( pCompose ); 00231 free( pSupport ); 00232 00233 Cudd_Deref( bSpace ); 00234 return bSpace; 00235 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 292 of file extraBddAuto.c.
00293 { 00294 DdNode * bRes; 00295 do { 00296 dd->reordered = 0; 00297 bRes = extraBddSpaceFromFunctionNeg( dd, bFunc ); 00298 } while (dd->reordered == 1); 00299 return bRes; 00300 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 271 of file extraBddAuto.c.
00272 { 00273 DdNode * bRes; 00274 do { 00275 dd->reordered = 0; 00276 bRes = extraBddSpaceFromFunctionPos( dd, bFunc ); 00277 } while (dd->reordered == 1); 00278 return bRes; 00279 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 449 of file extraBddAuto.c.
00450 { 00451 DdNode * bRes; 00452 do { 00453 dd->reordered = 0; 00454 bRes = extraBddSpaceFromMatrixNeg( dd, zA ); 00455 } while (dd->reordered == 1); 00456 return bRes; 00457 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 428 of file extraBddAuto.c.
00429 { 00430 DdNode * bRes; 00431 do { 00432 dd->reordered = 0; 00433 bRes = extraBddSpaceFromMatrixPos( dd, zA ); 00434 } while (dd->reordered == 1); 00435 return bRes; 00436 }
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 334 of file extraBddAuto.c.
00335 { 00336 DdNode * bNegCube; 00337 DdNode * bResult; 00338 bNegCube = Extra_bddSupportNegativeCube( dd, bCanonVars ); Cudd_Ref( bNegCube ); 00339 bResult = Cudd_Cofactor( dd, bFunc, bNegCube ); Cudd_Ref( bResult ); 00340 Cudd_RecursiveDeref( dd, bNegCube ); 00341 Cudd_Deref( bResult ); 00342 return bResult; 00343 }
Function*************************************************************
Synopsis [Counts the number of literals in one combination.]
Description []
SideEffects []
SeeAlso []
Definition at line 470 of file extraBddAuto.c.
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceCanonVars().]
Description []
SideEffects []
SeeAlso []
Definition at line 997 of file extraBddAuto.c.
00998 { 00999 DdNode * bRes, * bFR; 01000 statLine( dd ); 01001 01002 bFR = Cudd_Regular(bF); 01003 if ( cuddIsConstant(bFR) ) 01004 return bF; 01005 01006 if ( bRes = cuddCacheLookup1(dd, extraBddSpaceCanonVars, bF) ) 01007 return bRes; 01008 else 01009 { 01010 DdNode * bF0, * bF1; 01011 DdNode * bRes, * bRes0; 01012 01013 if ( bFR != bF ) // bF is complemented 01014 { 01015 bF0 = Cudd_Not( cuddE(bFR) ); 01016 bF1 = Cudd_Not( cuddT(bFR) ); 01017 } 01018 else 01019 { 01020 bF0 = cuddE(bFR); 01021 bF1 = cuddT(bFR); 01022 } 01023 01024 if ( bF0 == b0 ) 01025 { 01026 bRes = extraBddSpaceCanonVars( dd, bF1 ); 01027 if ( bRes == NULL ) 01028 return NULL; 01029 } 01030 else if ( bF1 == b0 ) 01031 { 01032 bRes = extraBddSpaceCanonVars( dd, bF0 ); 01033 if ( bRes == NULL ) 01034 return NULL; 01035 } 01036 else 01037 { 01038 bRes0 = extraBddSpaceCanonVars( dd, bF0 ); 01039 if ( bRes0 == NULL ) 01040 return NULL; 01041 cuddRef( bRes0 ); 01042 01043 bRes = cuddUniqueInter( dd, bFR->index, bRes0, b0 ); 01044 if ( bRes == NULL ) 01045 { 01046 Cudd_RecursiveDeref( dd,bRes0 ); 01047 return NULL; 01048 } 01049 cuddDeref( bRes0 ); 01050 } 01051 01052 cuddCacheInsert1( dd, extraBddSpaceCanonVars, bF, bRes ); 01053 return bRes; 01054 } 01055 }
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceEquationsNev().]
Description []
SideEffects []
SeeAlso []
Definition at line 1198 of file extraBddAuto.c.
01199 { 01200 DdNode * zRes; 01201 statLine( dd ); 01202 01203 if ( bF == b0 ) 01204 return z1; 01205 if ( bF == b1 ) 01206 return z0; 01207 01208 if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsNeg, bF) ) 01209 return zRes; 01210 else 01211 { 01212 DdNode * bFR, * bF0, * bF1; 01213 DdNode * zPos0, * zPos1, * zNeg1; 01214 DdNode * zRes, * zRes0, * zRes1; 01215 01216 bFR = Cudd_Regular(bF); 01217 if ( bFR != bF ) // bF is complemented 01218 { 01219 bF0 = Cudd_Not( cuddE(bFR) ); 01220 bF1 = Cudd_Not( cuddT(bFR) ); 01221 } 01222 else 01223 { 01224 bF0 = cuddE(bFR); 01225 bF1 = cuddT(bFR); 01226 } 01227 01228 if ( bF0 == b0 ) 01229 { 01230 zRes = extraBddSpaceEquationsNeg( dd, bF1 ); 01231 if ( zRes == NULL ) 01232 return NULL; 01233 } 01234 else if ( bF1 == b0 ) 01235 { 01236 zRes0 = extraBddSpaceEquationsNeg( dd, bF0 ); 01237 if ( zRes0 == NULL ) 01238 return NULL; 01239 cuddRef( zRes0 ); 01240 01241 // add the current element to the set 01242 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes0 ); 01243 if ( zRes == NULL ) 01244 { 01245 Cudd_RecursiveDerefZdd(dd, zRes0); 01246 return NULL; 01247 } 01248 cuddDeref( zRes0 ); 01249 } 01250 else 01251 { 01252 zPos0 = extraBddSpaceEquationsNeg( dd, bF0 ); 01253 if ( zPos0 == NULL ) 01254 return NULL; 01255 cuddRef( zPos0 ); 01256 01257 zPos1 = extraBddSpaceEquationsNeg( dd, bF1 ); 01258 if ( zPos1 == NULL ) 01259 { 01260 Cudd_RecursiveDerefZdd(dd, zPos0); 01261 return NULL; 01262 } 01263 cuddRef( zPos1 ); 01264 01265 zNeg1 = extraBddSpaceEquationsPos( dd, bF1 ); 01266 if ( zNeg1 == NULL ) 01267 { 01268 Cudd_RecursiveDerefZdd(dd, zPos0); 01269 Cudd_RecursiveDerefZdd(dd, zPos1); 01270 return NULL; 01271 } 01272 cuddRef( zNeg1 ); 01273 01274 01275 zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); 01276 if ( zRes0 == NULL ) 01277 { 01278 Cudd_RecursiveDerefZdd(dd, zNeg1); 01279 Cudd_RecursiveDerefZdd(dd, zPos0); 01280 Cudd_RecursiveDerefZdd(dd, zPos1); 01281 return NULL; 01282 } 01283 cuddRef( zRes0 ); 01284 01285 zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); 01286 if ( zRes1 == NULL ) 01287 { 01288 Cudd_RecursiveDerefZdd(dd, zRes0); 01289 Cudd_RecursiveDerefZdd(dd, zNeg1); 01290 Cudd_RecursiveDerefZdd(dd, zPos0); 01291 Cudd_RecursiveDerefZdd(dd, zPos1); 01292 return NULL; 01293 } 01294 cuddRef( zRes1 ); 01295 Cudd_RecursiveDerefZdd(dd, zNeg1); 01296 Cudd_RecursiveDerefZdd(dd, zPos0); 01297 Cudd_RecursiveDerefZdd(dd, zPos1); 01298 // only zRes0 and zRes1 are refed at this point 01299 01300 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); 01301 if ( zRes == NULL ) 01302 { 01303 Cudd_RecursiveDerefZdd(dd, zRes0); 01304 Cudd_RecursiveDerefZdd(dd, zRes1); 01305 return NULL; 01306 } 01307 cuddDeref( zRes0 ); 01308 cuddDeref( zRes1 ); 01309 } 01310 01311 cuddCacheInsert1( dd, extraBddSpaceEquationsNeg, bF, zRes ); 01312 return zRes; 01313 } 01314 }
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceEquationsPos().]
Description []
SideEffects []
SeeAlso []
Definition at line 1068 of file extraBddAuto.c.
01069 { 01070 DdNode * zRes; 01071 statLine( dd ); 01072 01073 if ( bF == b0 ) 01074 return z1; 01075 if ( bF == b1 ) 01076 return z0; 01077 01078 if ( zRes = cuddCacheLookup1Zdd(dd, extraBddSpaceEquationsPos, bF) ) 01079 return zRes; 01080 else 01081 { 01082 DdNode * bFR, * bF0, * bF1; 01083 DdNode * zPos0, * zPos1, * zNeg1; 01084 DdNode * zRes, * zRes0, * zRes1; 01085 01086 bFR = Cudd_Regular(bF); 01087 if ( bFR != bF ) // bF is complemented 01088 { 01089 bF0 = Cudd_Not( cuddE(bFR) ); 01090 bF1 = Cudd_Not( cuddT(bFR) ); 01091 } 01092 else 01093 { 01094 bF0 = cuddE(bFR); 01095 bF1 = cuddT(bFR); 01096 } 01097 01098 if ( bF0 == b0 ) 01099 { 01100 zRes1 = extraBddSpaceEquationsPos( dd, bF1 ); 01101 if ( zRes1 == NULL ) 01102 return NULL; 01103 cuddRef( zRes1 ); 01104 01105 // add the current element to the set 01106 zRes = cuddZddGetNode( dd, 2*bFR->index, z1, zRes1 ); 01107 if ( zRes == NULL ) 01108 { 01109 Cudd_RecursiveDerefZdd(dd, zRes1); 01110 return NULL; 01111 } 01112 cuddDeref( zRes1 ); 01113 } 01114 else if ( bF1 == b0 ) 01115 { 01116 zRes = extraBddSpaceEquationsPos( dd, bF0 ); 01117 if ( zRes == NULL ) 01118 return NULL; 01119 } 01120 else 01121 { 01122 zPos0 = extraBddSpaceEquationsPos( dd, bF0 ); 01123 if ( zPos0 == NULL ) 01124 return NULL; 01125 cuddRef( zPos0 ); 01126 01127 zPos1 = extraBddSpaceEquationsPos( dd, bF1 ); 01128 if ( zPos1 == NULL ) 01129 { 01130 Cudd_RecursiveDerefZdd(dd, zPos0); 01131 return NULL; 01132 } 01133 cuddRef( zPos1 ); 01134 01135 zNeg1 = extraBddSpaceEquationsNeg( dd, bF1 ); 01136 if ( zNeg1 == NULL ) 01137 { 01138 Cudd_RecursiveDerefZdd(dd, zPos0); 01139 Cudd_RecursiveDerefZdd(dd, zPos1); 01140 return NULL; 01141 } 01142 cuddRef( zNeg1 ); 01143 01144 01145 zRes0 = cuddZddIntersect( dd, zPos0, zPos1 ); 01146 if ( zRes0 == NULL ) 01147 { 01148 Cudd_RecursiveDerefZdd(dd, zNeg1); 01149 Cudd_RecursiveDerefZdd(dd, zPos0); 01150 Cudd_RecursiveDerefZdd(dd, zPos1); 01151 return NULL; 01152 } 01153 cuddRef( zRes0 ); 01154 01155 zRes1 = cuddZddIntersect( dd, zPos0, zNeg1 ); 01156 if ( zRes1 == NULL ) 01157 { 01158 Cudd_RecursiveDerefZdd(dd, zRes0); 01159 Cudd_RecursiveDerefZdd(dd, zNeg1); 01160 Cudd_RecursiveDerefZdd(dd, zPos0); 01161 Cudd_RecursiveDerefZdd(dd, zPos1); 01162 return NULL; 01163 } 01164 cuddRef( zRes1 ); 01165 Cudd_RecursiveDerefZdd(dd, zNeg1); 01166 Cudd_RecursiveDerefZdd(dd, zPos0); 01167 Cudd_RecursiveDerefZdd(dd, zPos1); 01168 // only zRes0 and zRes1 are refed at this point 01169 01170 zRes = cuddZddGetNode( dd, 2*bFR->index, zRes1, zRes0 ); 01171 if ( zRes == NULL ) 01172 { 01173 Cudd_RecursiveDerefZdd(dd, zRes0); 01174 Cudd_RecursiveDerefZdd(dd, zRes1); 01175 return NULL; 01176 } 01177 cuddDeref( zRes0 ); 01178 cuddDeref( zRes1 ); 01179 } 01180 01181 cuddCacheInsert1( dd, extraBddSpaceEquationsPos, bF, zRes ); 01182 return zRes; 01183 } 01184 }
Function********************************************************************
Synopsis [Performs the recursive steps of Extra_bddSpaceFromFunction.]
Description []
SideEffects []
SeeAlso []
Definition at line 559 of file extraBddAuto.c.
00560 { 00561 DdNode * bRes; 00562 DdNode * bFR, * bGR; 00563 00564 bFR = Cudd_Regular( bF ); 00565 bGR = Cudd_Regular( bG ); 00566 if ( cuddIsConstant(bFR) ) 00567 { 00568 if ( bF == bG ) 00569 return b1; 00570 else 00571 return b0; 00572 } 00573 if ( cuddIsConstant(bGR) ) 00574 return b0; 00575 // both bFunc and bCore are not constants 00576 00577 // the operation is commutative - normalize the problem 00578 if ( (unsigned)bF > (unsigned)bG ) 00579 return extraBddSpaceFromFunction(dd, bG, bF); 00580 00581 00582 if ( bRes = cuddCacheLookup2(dd, extraBddSpaceFromFunction, bF, bG) ) 00583 return bRes; 00584 else 00585 { 00586 DdNode * bF0, * bF1; 00587 DdNode * bG0, * bG1; 00588 DdNode * bTemp1, * bTemp2; 00589 DdNode * bRes0, * bRes1; 00590 int LevelF, LevelG; 00591 int index; 00592 00593 LevelF = dd->perm[bFR->index]; 00594 LevelG = dd->perm[bGR->index]; 00595 if ( LevelF <= LevelG ) 00596 { 00597 index = dd->invperm[LevelF]; 00598 if ( bFR != bF ) 00599 { 00600 bF0 = Cudd_Not( cuddE(bFR) ); 00601 bF1 = Cudd_Not( cuddT(bFR) ); 00602 } 00603 else 00604 { 00605 bF0 = cuddE(bFR); 00606 bF1 = cuddT(bFR); 00607 } 00608 } 00609 else 00610 { 00611 index = dd->invperm[LevelG]; 00612 bF0 = bF1 = bF; 00613 } 00614 00615 if ( LevelG <= LevelF ) 00616 { 00617 if ( bGR != bG ) 00618 { 00619 bG0 = Cudd_Not( cuddE(bGR) ); 00620 bG1 = Cudd_Not( cuddT(bGR) ); 00621 } 00622 else 00623 { 00624 bG0 = cuddE(bGR); 00625 bG1 = cuddT(bGR); 00626 } 00627 } 00628 else 00629 bG0 = bG1 = bG; 00630 00631 bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG0 ); 00632 if ( bTemp1 == NULL ) 00633 return NULL; 00634 cuddRef( bTemp1 ); 00635 00636 bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG1 ); 00637 if ( bTemp2 == NULL ) 00638 { 00639 Cudd_RecursiveDeref( dd, bTemp1 ); 00640 return NULL; 00641 } 00642 cuddRef( bTemp2 ); 00643 00644 00645 bRes0 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); 00646 if ( bRes0 == NULL ) 00647 { 00648 Cudd_RecursiveDeref( dd, bTemp1 ); 00649 Cudd_RecursiveDeref( dd, bTemp2 ); 00650 return NULL; 00651 } 00652 cuddRef( bRes0 ); 00653 Cudd_RecursiveDeref( dd, bTemp1 ); 00654 Cudd_RecursiveDeref( dd, bTemp2 ); 00655 00656 00657 bTemp1 = extraBddSpaceFromFunction( dd, bF0, bG1 ); 00658 if ( bTemp1 == NULL ) 00659 { 00660 Cudd_RecursiveDeref( dd, bRes0 ); 00661 return NULL; 00662 } 00663 cuddRef( bTemp1 ); 00664 00665 bTemp2 = extraBddSpaceFromFunction( dd, bF1, bG0 ); 00666 if ( bTemp2 == NULL ) 00667 { 00668 Cudd_RecursiveDeref( dd, bRes0 ); 00669 Cudd_RecursiveDeref( dd, bTemp1 ); 00670 return NULL; 00671 } 00672 cuddRef( bTemp2 ); 00673 00674 bRes1 = cuddBddAndRecur( dd, bTemp1, bTemp2 ); 00675 if ( bRes1 == NULL ) 00676 { 00677 Cudd_RecursiveDeref( dd, bRes0 ); 00678 Cudd_RecursiveDeref( dd, bTemp1 ); 00679 Cudd_RecursiveDeref( dd, bTemp2 ); 00680 return NULL; 00681 } 00682 cuddRef( bRes1 ); 00683 Cudd_RecursiveDeref( dd, bTemp1 ); 00684 Cudd_RecursiveDeref( dd, bTemp2 ); 00685 00686 00687 00688 // consider the case when Res0 and Res1 are the same node 00689 if ( bRes0 == bRes1 ) 00690 bRes = bRes1; 00691 // consider the case when Res1 is complemented 00692 else if ( Cudd_IsComplement(bRes1) ) 00693 { 00694 bRes = cuddUniqueInter(dd, index, Cudd_Not(bRes1), Cudd_Not(bRes0)); 00695 if ( bRes == NULL ) 00696 { 00697 Cudd_RecursiveDeref(dd,bRes0); 00698 Cudd_RecursiveDeref(dd,bRes1); 00699 return NULL; 00700 } 00701 bRes = Cudd_Not(bRes); 00702 } 00703 else 00704 { 00705 bRes = cuddUniqueInter( dd, index, bRes1, bRes0 ); 00706 if ( bRes == NULL ) 00707 { 00708 Cudd_RecursiveDeref(dd,bRes0); 00709 Cudd_RecursiveDeref(dd,bRes1); 00710 return NULL; 00711 } 00712 } 00713 cuddDeref( bRes0 ); 00714 cuddDeref( bRes1 ); 00715 00716 // insert the result into cache 00717 cuddCacheInsert2(dd, extraBddSpaceFromFunction, bF, bG, bRes); 00718 return bRes; 00719 } 00720 } /* end of extraBddSpaceFromFunction */
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
Description []
SideEffects []
SeeAlso []
Definition at line 866 of file extraBddAuto.c.
00867 { 00868 DdNode * bRes, * bFR; 00869 statLine( dd ); 00870 00871 bFR = Cudd_Regular(bF); 00872 if ( cuddIsConstant(bFR) ) 00873 return b0; 00874 00875 if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionNeg, bF) ) 00876 return bRes; 00877 else 00878 { 00879 DdNode * bF0, * bF1; 00880 DdNode * bPos0, * bPos1; 00881 DdNode * bNeg0, * bNeg1; 00882 DdNode * bRes0, * bRes1; 00883 00884 if ( bFR != bF ) // bF is complemented 00885 { 00886 bF0 = Cudd_Not( cuddE(bFR) ); 00887 bF1 = Cudd_Not( cuddT(bFR) ); 00888 } 00889 else 00890 { 00891 bF0 = cuddE(bFR); 00892 bF1 = cuddT(bFR); 00893 } 00894 00895 00896 bPos0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); 00897 if ( bPos0 == NULL ) 00898 return NULL; 00899 cuddRef( bPos0 ); 00900 00901 bPos1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); 00902 if ( bPos1 == NULL ) 00903 { 00904 Cudd_RecursiveDeref( dd, bPos0 ); 00905 return NULL; 00906 } 00907 cuddRef( bPos1 ); 00908 00909 bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); 00910 if ( bRes0 == NULL ) 00911 { 00912 Cudd_RecursiveDeref( dd, bPos0 ); 00913 Cudd_RecursiveDeref( dd, bPos1 ); 00914 return NULL; 00915 } 00916 cuddRef( bRes0 ); 00917 Cudd_RecursiveDeref( dd, bPos0 ); 00918 Cudd_RecursiveDeref( dd, bPos1 ); 00919 00920 00921 bNeg0 = extraBddSpaceFromFunctionPos( dd, bF0 ); 00922 if ( bNeg0 == NULL ) 00923 { 00924 Cudd_RecursiveDeref( dd, bRes0 ); 00925 return NULL; 00926 } 00927 cuddRef( bNeg0 ); 00928 00929 bNeg1 = extraBddSpaceFromFunctionPos( dd, bF1 ); 00930 if ( bNeg1 == NULL ) 00931 { 00932 Cudd_RecursiveDeref( dd, bRes0 ); 00933 Cudd_RecursiveDeref( dd, bNeg0 ); 00934 return NULL; 00935 } 00936 cuddRef( bNeg1 ); 00937 00938 bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); 00939 if ( bRes1 == NULL ) 00940 { 00941 Cudd_RecursiveDeref( dd, bRes0 ); 00942 Cudd_RecursiveDeref( dd, bNeg0 ); 00943 Cudd_RecursiveDeref( dd, bNeg1 ); 00944 return NULL; 00945 } 00946 cuddRef( bRes1 ); 00947 Cudd_RecursiveDeref( dd, bNeg0 ); 00948 Cudd_RecursiveDeref( dd, bNeg1 ); 00949 00950 00951 // consider the case when Res0 and Res1 are the same node 00952 if ( bRes0 == bRes1 ) 00953 bRes = bRes1; 00954 // consider the case when Res1 is complemented 00955 else if ( Cudd_IsComplement(bRes1) ) 00956 { 00957 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); 00958 if ( bRes == NULL ) 00959 { 00960 Cudd_RecursiveDeref(dd,bRes0); 00961 Cudd_RecursiveDeref(dd,bRes1); 00962 return NULL; 00963 } 00964 bRes = Cudd_Not(bRes); 00965 } 00966 else 00967 { 00968 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); 00969 if ( bRes == NULL ) 00970 { 00971 Cudd_RecursiveDeref(dd,bRes0); 00972 Cudd_RecursiveDeref(dd,bRes1); 00973 return NULL; 00974 } 00975 } 00976 cuddDeref( bRes0 ); 00977 cuddDeref( bRes1 ); 00978 00979 cuddCacheInsert1( dd, extraBddSpaceFromFunctionNeg, bF, bRes ); 00980 return bRes; 00981 } 00982 }
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
Description []
SideEffects []
SeeAlso []
Definition at line 735 of file extraBddAuto.c.
00736 { 00737 DdNode * bRes, * bFR; 00738 statLine( dd ); 00739 00740 bFR = Cudd_Regular(bF); 00741 if ( cuddIsConstant(bFR) ) 00742 return b1; 00743 00744 if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromFunctionPos, bF) ) 00745 return bRes; 00746 else 00747 { 00748 DdNode * bF0, * bF1; 00749 DdNode * bPos0, * bPos1; 00750 DdNode * bNeg0, * bNeg1; 00751 DdNode * bRes0, * bRes1; 00752 00753 if ( bFR != bF ) // bF is complemented 00754 { 00755 bF0 = Cudd_Not( cuddE(bFR) ); 00756 bF1 = Cudd_Not( cuddT(bFR) ); 00757 } 00758 else 00759 { 00760 bF0 = cuddE(bFR); 00761 bF1 = cuddT(bFR); 00762 } 00763 00764 00765 bPos0 = extraBddSpaceFromFunctionPos( dd, bF0 ); 00766 if ( bPos0 == NULL ) 00767 return NULL; 00768 cuddRef( bPos0 ); 00769 00770 bPos1 = extraBddSpaceFromFunctionPos( dd, bF1 ); 00771 if ( bPos1 == NULL ) 00772 { 00773 Cudd_RecursiveDeref( dd, bPos0 ); 00774 return NULL; 00775 } 00776 cuddRef( bPos1 ); 00777 00778 bRes0 = cuddBddAndRecur( dd, bPos0, bPos1 ); 00779 if ( bRes0 == NULL ) 00780 { 00781 Cudd_RecursiveDeref( dd, bPos0 ); 00782 Cudd_RecursiveDeref( dd, bPos1 ); 00783 return NULL; 00784 } 00785 cuddRef( bRes0 ); 00786 Cudd_RecursiveDeref( dd, bPos0 ); 00787 Cudd_RecursiveDeref( dd, bPos1 ); 00788 00789 00790 bNeg0 = extraBddSpaceFromFunctionNeg( dd, bF0 ); 00791 if ( bNeg0 == NULL ) 00792 { 00793 Cudd_RecursiveDeref( dd, bRes0 ); 00794 return NULL; 00795 } 00796 cuddRef( bNeg0 ); 00797 00798 bNeg1 = extraBddSpaceFromFunctionNeg( dd, bF1 ); 00799 if ( bNeg1 == NULL ) 00800 { 00801 Cudd_RecursiveDeref( dd, bRes0 ); 00802 Cudd_RecursiveDeref( dd, bNeg0 ); 00803 return NULL; 00804 } 00805 cuddRef( bNeg1 ); 00806 00807 bRes1 = cuddBddAndRecur( dd, bNeg0, bNeg1 ); 00808 if ( bRes1 == NULL ) 00809 { 00810 Cudd_RecursiveDeref( dd, bRes0 ); 00811 Cudd_RecursiveDeref( dd, bNeg0 ); 00812 Cudd_RecursiveDeref( dd, bNeg1 ); 00813 return NULL; 00814 } 00815 cuddRef( bRes1 ); 00816 Cudd_RecursiveDeref( dd, bNeg0 ); 00817 Cudd_RecursiveDeref( dd, bNeg1 ); 00818 00819 00820 // consider the case when Res0 and Res1 are the same node 00821 if ( bRes0 == bRes1 ) 00822 bRes = bRes1; 00823 // consider the case when Res1 is complemented 00824 else if ( Cudd_IsComplement(bRes1) ) 00825 { 00826 bRes = cuddUniqueInter( dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0) ); 00827 if ( bRes == NULL ) 00828 { 00829 Cudd_RecursiveDeref(dd,bRes0); 00830 Cudd_RecursiveDeref(dd,bRes1); 00831 return NULL; 00832 } 00833 bRes = Cudd_Not(bRes); 00834 } 00835 else 00836 { 00837 bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 ); 00838 if ( bRes == NULL ) 00839 { 00840 Cudd_RecursiveDeref(dd,bRes0); 00841 Cudd_RecursiveDeref(dd,bRes1); 00842 return NULL; 00843 } 00844 } 00845 cuddDeref( bRes0 ); 00846 cuddDeref( bRes1 ); 00847 00848 cuddCacheInsert1( dd, extraBddSpaceFromFunctionPos, bF, bRes ); 00849 return bRes; 00850 } 00851 }
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
Description []
SideEffects []
SeeAlso []
Definition at line 1448 of file extraBddAuto.c.
01449 { 01450 DdNode * bRes; 01451 statLine( dd ); 01452 01453 if ( zA == z0 ) 01454 return b1; 01455 if ( zA == z1 ) 01456 return b0; 01457 01458 if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixNeg, zA) ) 01459 return bRes; 01460 else 01461 { 01462 DdNode * bP0, * bP1; 01463 DdNode * bN0, * bN1; 01464 DdNode * bRes0, * bRes1; 01465 01466 bP0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); 01467 if ( bP0 == NULL ) 01468 return NULL; 01469 cuddRef( bP0 ); 01470 01471 bP1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); 01472 if ( bP1 == NULL ) 01473 { 01474 Cudd_RecursiveDeref( dd, bP0 ); 01475 return NULL; 01476 } 01477 cuddRef( bP1 ); 01478 01479 bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); 01480 if ( bRes0 == NULL ) 01481 { 01482 Cudd_RecursiveDeref( dd, bP0 ); 01483 Cudd_RecursiveDeref( dd, bP1 ); 01484 return NULL; 01485 } 01486 cuddRef( bRes0 ); 01487 Cudd_RecursiveDeref( dd, bP0 ); 01488 Cudd_RecursiveDeref( dd, bP1 ); 01489 01490 01491 bN0 = extraBddSpaceFromMatrixNeg( dd, cuddE(zA) ); 01492 if ( bN0 == NULL ) 01493 { 01494 Cudd_RecursiveDeref( dd, bRes0 ); 01495 return NULL; 01496 } 01497 cuddRef( bN0 ); 01498 01499 bN1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); 01500 if ( bN1 == NULL ) 01501 { 01502 Cudd_RecursiveDeref( dd, bRes0 ); 01503 Cudd_RecursiveDeref( dd, bN0 ); 01504 return NULL; 01505 } 01506 cuddRef( bN1 ); 01507 01508 bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); 01509 if ( bRes1 == NULL ) 01510 { 01511 Cudd_RecursiveDeref( dd, bRes0 ); 01512 Cudd_RecursiveDeref( dd, bN0 ); 01513 Cudd_RecursiveDeref( dd, bN1 ); 01514 return NULL; 01515 } 01516 cuddRef( bRes1 ); 01517 Cudd_RecursiveDeref( dd, bN0 ); 01518 Cudd_RecursiveDeref( dd, bN1 ); 01519 01520 01521 // consider the case when Res0 and Res1 are the same node 01522 if ( bRes0 == bRes1 ) 01523 bRes = bRes1; 01524 // consider the case when Res1 is complemented 01525 else if ( Cudd_IsComplement(bRes1) ) 01526 { 01527 bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); 01528 if ( bRes == NULL ) 01529 { 01530 Cudd_RecursiveDeref(dd,bRes0); 01531 Cudd_RecursiveDeref(dd,bRes1); 01532 return NULL; 01533 } 01534 bRes = Cudd_Not(bRes); 01535 } 01536 else 01537 { 01538 bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); 01539 if ( bRes == NULL ) 01540 { 01541 Cudd_RecursiveDeref(dd,bRes0); 01542 Cudd_RecursiveDeref(dd,bRes1); 01543 return NULL; 01544 } 01545 } 01546 cuddDeref( bRes0 ); 01547 cuddDeref( bRes1 ); 01548 01549 cuddCacheInsert1( dd, extraBddSpaceFromMatrixNeg, zA, bRes ); 01550 return bRes; 01551 } 01552 }
Function*************************************************************
Synopsis [Performs the recursive step of Extra_bddSpaceFromFunctionPos().]
Description []
SideEffects []
SeeAlso []
Definition at line 1330 of file extraBddAuto.c.
01331 { 01332 DdNode * bRes; 01333 statLine( dd ); 01334 01335 if ( zA == z0 ) 01336 return b1; 01337 if ( zA == z1 ) 01338 return b1; 01339 01340 if ( bRes = cuddCacheLookup1(dd, extraBddSpaceFromMatrixPos, zA) ) 01341 return bRes; 01342 else 01343 { 01344 DdNode * bP0, * bP1; 01345 DdNode * bN0, * bN1; 01346 DdNode * bRes0, * bRes1; 01347 01348 bP0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); 01349 if ( bP0 == NULL ) 01350 return NULL; 01351 cuddRef( bP0 ); 01352 01353 bP1 = extraBddSpaceFromMatrixPos( dd, cuddT(zA) ); 01354 if ( bP1 == NULL ) 01355 { 01356 Cudd_RecursiveDeref( dd, bP0 ); 01357 return NULL; 01358 } 01359 cuddRef( bP1 ); 01360 01361 bRes0 = cuddBddAndRecur( dd, bP0, bP1 ); 01362 if ( bRes0 == NULL ) 01363 { 01364 Cudd_RecursiveDeref( dd, bP0 ); 01365 Cudd_RecursiveDeref( dd, bP1 ); 01366 return NULL; 01367 } 01368 cuddRef( bRes0 ); 01369 Cudd_RecursiveDeref( dd, bP0 ); 01370 Cudd_RecursiveDeref( dd, bP1 ); 01371 01372 01373 bN0 = extraBddSpaceFromMatrixPos( dd, cuddE(zA) ); 01374 if ( bN0 == NULL ) 01375 { 01376 Cudd_RecursiveDeref( dd, bRes0 ); 01377 return NULL; 01378 } 01379 cuddRef( bN0 ); 01380 01381 bN1 = extraBddSpaceFromMatrixNeg( dd, cuddT(zA) ); 01382 if ( bN1 == NULL ) 01383 { 01384 Cudd_RecursiveDeref( dd, bRes0 ); 01385 Cudd_RecursiveDeref( dd, bN0 ); 01386 return NULL; 01387 } 01388 cuddRef( bN1 ); 01389 01390 bRes1 = cuddBddAndRecur( dd, bN0, bN1 ); 01391 if ( bRes1 == NULL ) 01392 { 01393 Cudd_RecursiveDeref( dd, bRes0 ); 01394 Cudd_RecursiveDeref( dd, bN0 ); 01395 Cudd_RecursiveDeref( dd, bN1 ); 01396 return NULL; 01397 } 01398 cuddRef( bRes1 ); 01399 Cudd_RecursiveDeref( dd, bN0 ); 01400 Cudd_RecursiveDeref( dd, bN1 ); 01401 01402 01403 // consider the case when Res0 and Res1 are the same node 01404 if ( bRes0 == bRes1 ) 01405 bRes = bRes1; 01406 // consider the case when Res1 is complemented 01407 else if ( Cudd_IsComplement(bRes1) ) 01408 { 01409 bRes = cuddUniqueInter( dd, zA->index/2, Cudd_Not(bRes1), Cudd_Not(bRes0) ); 01410 if ( bRes == NULL ) 01411 { 01412 Cudd_RecursiveDeref(dd,bRes0); 01413 Cudd_RecursiveDeref(dd,bRes1); 01414 return NULL; 01415 } 01416 bRes = Cudd_Not(bRes); 01417 } 01418 else 01419 { 01420 bRes = cuddUniqueInter( dd, zA->index/2, bRes1, bRes0 ); 01421 if ( bRes == NULL ) 01422 { 01423 Cudd_RecursiveDeref(dd,bRes0); 01424 Cudd_RecursiveDeref(dd,bRes1); 01425 return NULL; 01426 } 01427 } 01428 cuddDeref( bRes0 ); 01429 cuddDeref( bRes1 ); 01430 01431 cuddCacheInsert1( dd, extraBddSpaceFromMatrixPos, zA, bRes ); 01432 return bRes; 01433 } 01434 }
