diff options
author | Mathias Soeken <mathias.soeken@epfl.ch> | 2017-03-06 16:32:07 +0100 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@epfl.ch> | 2017-03-06 16:32:07 +0100 |
commit | 1cd5f76800590c01b13c7eb606402fb995df2074 (patch) | |
tree | 44886cd21745e2127f0f542fa4bc4d48389c4135 | |
parent | d971505402e34887b54a40bf8e98fedf7fc1ce01 (diff) | |
download | abc-1cd5f76800590c01b13c7eb606402fb995df2074.tar.gz abc-1cd5f76800590c01b13c7eb606402fb995df2074.tar.bz2 abc-1cd5f76800590c01b13c7eb606402fb995df2074.zip |
Fix exact command for multiple-output functions.
-rw-r--r-- | src/base/abci/abcExact.c | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 2064873a..c9cb4e32 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1921,7 +1921,7 @@ static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes ) for ( h = 0; h < pSes->nSpecFunc; ++h ) { printf( " func %d: ", h + 1 ); - Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars ); + Abc_TtPrintHexRev( stdout, &pSes->pSpec[h << 2], pSes->nSpecVars ); printf( "\n" ); } @@ -2357,6 +2357,29 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates ) static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes ) { char * pSol = NULL; + int i = pSes->nStartGates + 1, fRes; + + /* if more than one function, no CEGAR */ + if ( pSes->nSpecFunc > 1 ) + { + while ( true ) + { + if ( pSes->fVerbose ) + { + printf( "try with %d gates\n", i ); + } + + memset( pSes->pTtValues, ~0, 4 * sizeof( word ) ); + fRes = Ses_ManFindNetworkExact( pSes, i++ ); + if ( fRes == 2 ) continue; + if ( fRes == 0 ) break; + + pSol = Ses_ManExtractSolution( pSes ); + break; + } + + return pSol; + } /* do the arrival times allow for a network? */ if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile ) |