diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-12-09 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-12-09 08:01:00 -0800 |
commit | b9abf9c00c02feb52a2c796199343acebe20d8ef (patch) | |
tree | de4ad845520c09f876309d89a60e13831360ad70 /src/opt/kit/kitBdd.c | |
parent | 4cf99cae95c629b31d6d89c5dcea2eeb17654c85 (diff) | |
download | abc-b9abf9c00c02feb52a2c796199343acebe20d8ef.tar.gz abc-b9abf9c00c02feb52a2c796199343acebe20d8ef.tar.bz2 abc-b9abf9c00c02feb52a2c796199343acebe20d8ef.zip |
Version abc61209
Diffstat (limited to 'src/opt/kit/kitBdd.c')
-rw-r--r-- | src/opt/kit/kitBdd.c | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/opt/kit/kitBdd.c b/src/opt/kit/kitBdd.c index ed978740..9c8d4f7a 100644 --- a/src/opt/kit/kitBdd.c +++ b/src/opt/kit/kitBdd.c @@ -135,26 +135,26 @@ DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph ) SeeAlso [] ***********************************************************************/ -DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal ) +DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop ) { DdNode * bF0, * bF1, * bF; - if ( nVars == 0 ) + int Var; + if ( nVars <= 5 ) { - if ( pTruth[iBit>>5] & (1 << iBit&31) ) - return b1; - return b0; - } - if ( nVars == 5 ) - { - if ( pTruth[iBit>>5] == 0xFFFFFFFF ) - return b1; - if ( pTruth[iBit>>5] == 0 ) + unsigned uTruth, uMask; + uMask = ((~(unsigned)0) >> (32 - (1<<nVars))); + uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask; + if ( uTruth == 0 ) return b0; + if ( uTruth == uMask ) + return b1; } + // find the variable to use + Var = fMSBonTop? nVarsTotal-nVars : nVars-1; // other special cases can be added - bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal ); Cudd_Ref( bF0 ); - bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal ); Cudd_Ref( bF1 ); - bF = Cudd_bddIte( dd, dd->vars[nVarsTotal-nVars], bF1, bF0 ); Cudd_Ref( bF ); + bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit, nVars-1, nVarsTotal, fMSBonTop ); Cudd_Ref( bF0 ); + bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop ); Cudd_Ref( bF1 ); + bF = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 ); Cudd_Ref( bF ); Cudd_RecursiveDeref( dd, bF0 ); Cudd_RecursiveDeref( dd, bF1 ); Cudd_Deref( bF ); @@ -176,9 +176,9 @@ DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nV SeeAlso [] ***********************************************************************/ -DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars ) +DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop ) { - return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars ); + return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop ); } /**Function************************************************************* |