From 1cd5f76800590c01b13c7eb606402fb995df2074 Mon Sep 17 00:00:00 2001 From: Mathias Soeken Date: Mon, 6 Mar 2017 16:32:07 +0100 Subject: Fix exact command for multiple-output functions. --- src/base/abci/abcExact.c | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) (limited to 'src') 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 ) -- cgit v1.2.3