diff options
| author | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-14 10:06:00 +0200 |
|---|---|---|
| committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2016-09-14 10:06:00 +0200 |
| commit | e601df9deac339b7404ef366bf10dc0acad8ad3a (patch) | |
| tree | 4a9ce1e8efc1a741ba6fa8bf50a645d650a9065d /src | |
| parent | bb8e1808e6ef6e36a7b81ed78a7e1d7024308737 (diff) | |
| download | abc-e601df9deac339b7404ef366bf10dc0acad8ad3a.tar.gz abc-e601df9deac339b7404ef366bf10dc0acad8ad3a.tar.bz2 abc-e601df9deac339b7404ef366bf10dc0acad8ad3a.zip | |
Some fixes in BMS.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abcExact.c | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index cb578d04..f6233adc 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -2197,19 +2197,19 @@ static int Ses_ManFindNetworkExact( Ses_Man_t * pSes, int nGates ) } // is there a network for a given number of gates -/* return: (2: continue, 1: found, 0: gave up) */ +/* return: (3: impossible, 2: continue, 1: found, 0: gave up) */ static int Ses_ManFindNetworkExactCEGAR( Ses_Man_t * pSes, int nGates, char ** pSol ) { - int fFirst = 0, fRes, iMint, fSat; + int fRes, iMint, fSat; word pTruth[4]; /* debug */ - Abc_DebugErase( pSes->nDebugOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose && !fFirst ); + Abc_DebugErase( pSes->nDebugOffset + ( nGates > 10 ? 5 : 4 ), pSes->fVeryVerbose ); Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose ); /* do #gates and max depth allow for a network? */ if ( !Ses_CheckGatesConsistency( pSes, nGates ) ) - return 0; + return 3; fRes = Ses_ManFindNetworkExact( pSes, nGates ); if ( fRes != 1 ) return fRes; @@ -2256,26 +2256,26 @@ static char * Ses_ManFindMinimumSizeBottomUp( Ses_Man_t * pSes ) memset( pSes->pTtValues, 0, 4 * sizeof( word ) ); + Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose ); + while ( true ) { ++nGates; fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol ); - printf( "fRes = %d\n", fRes ); - if ( fRes == 0 ) { pSes->fHitResLimit = 1; break; } - else if ( fRes == 1 ) + else if ( fRes == 1 || fRes == 3 ) break; } Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose ); - return fRes ? pSol : NULL; + return pSol; } static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) @@ -2285,6 +2285,8 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) pSes->fHitResLimit = 0; + Abc_DebugPrintIntInt( " (%d/%d)", nGates, pSes->nMaxGates, pSes->fVeryVerbose ); + while ( true ) { fRes = Ses_ManFindNetworkExactCEGAR( pSes, nGates, &pSol2 ); @@ -2294,7 +2296,7 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) pSes->fHitResLimit = 1; break; } - else if ( fRes == 2 ) + else if ( fRes == 2 || fRes == 3 ) break; pSol = pSol2; @@ -2305,6 +2307,8 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) --nGates; } + Abc_DebugErase( pSes->nDebugOffset + ( nGates >= 10 ? 5 : 4 ), pSes->fVeryVerbose ); + return pSol; } |