diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-01 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-03-01 08:01:00 -0800 |
| commit | 320c429bc46728c1faddfc561c166810aa134a04 (patch) | |
| tree | c773cc96431cd38ae35484dae7d7d17a79671ac2 /src/aig/fra/fraInd.c | |
| parent | f65983c2c0810cfb933f696952325a81d2378987 (diff) | |
| download | abc-320c429bc46728c1faddfc561c166810aa134a04.tar.gz abc-320c429bc46728c1faddfc561c166810aa134a04.tar.bz2 abc-320c429bc46728c1faddfc561c166810aa134a04.zip | |
Version abc80301
Diffstat (limited to 'src/aig/fra/fraInd.c')
| -rw-r--r-- | src/aig/fra/fraInd.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 0715524e..7e0d080c 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -253,6 +253,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) int * pMapBack; int i, nCountPis, nCountRegs; int nClasses, nPartSize, fVerbose; + int clk = clock(); // save parameters nPartSize = pPars->nPartSize; pPars->nPartSize = 0; @@ -281,6 +282,9 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) Vec_PtrForEachEntry( vResult, vPart, i ) { pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack ); + // create the projection of 1-hot registers + if ( pAig->vOnehots ) + pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose ); // run SSW pNew = Fra_FraigInduction( pTemp, pPars ); nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); @@ -299,6 +303,10 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) Vec_VecFree( (Vec_Vec_t *)vResult ); pPars->nPartSize = nPartSize; pPars->fVerbose = fVerbose; + if ( fVerbose ) + { + PRT( "Total time", clock() - clk ); + } return pNew; } @@ -485,6 +493,8 @@ p->timeTrav += clock() - clk2; // add one-hotness clauses if ( p->pPars->fUse1Hot ) Fra_OneHotAssume( p, p->vOneHots ); +// if ( p->pManAig->vOnehots ) +// Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots ); // report the intermediate results if ( pPars->fVerbose ) |