diff options
Diffstat (limited to 'src/base/wlc')
-rw-r--r-- | src/base/wlc/wlcAbs.c | 90 |
1 files changed, 60 insertions, 30 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 29f66ee3..b58ef5b5 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -48,6 +48,9 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu extern int IPdr_ManCheckCombUnsat( Pdr_Man_t * p ); extern int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ); extern void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ); +extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig ); +extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp ); +extern int Abs_CallBackToStop( int RunId ); typedef struct Int_Pair_t_ Int_Pair_t; struct Int_Pair_t_ @@ -89,6 +92,7 @@ typedef struct Bmc3_ThData_t_ // mutext to control access to shared variables extern pthread_mutex_t g_mutex; static volatile int g_nRunIds = 0; // the number of the last prover instance +static int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) { @@ -1322,28 +1326,35 @@ int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig ) return RetValue; } -int Bmc3_test( Aig_Man_t * pAig, int RunId, Abc_Cex_t ** ppCex ) -{ - char * p = ABC_ALLOC( char, 111 ); - while ( 1 ) - { - if ( RunId < g_nRunIds ) - break; - } - ABC_FREE( p ); - return -1; -} - void * Wla_Bmc3Thread ( void * pArg ) { + int status; int RetValue = -1; Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg; - RetValue = Bmc3_test( pData->pAig, pData->RunId, pData->ppCex ); + Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig ); + Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars; + Saig_ParBmcSetDefaultParams( pBmcPars ); + + RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 ); - if ( RetValue == -1 ) - Abc_Print( 1, "Cancelled bmc3 %d.\n", pData->RunId ); + if ( RetValue == 0 ) + { + assert( pAbcNtk->pSeqModel ); + *(pData->ppCex) = pAbcNtk->pSeqModel; + pAbcNtk->pSeqModel = NULL; + Abc_Print( 1, "BMC3 found CEX. RunId=%d.\n", pData->RunId ); + + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } + else + { + Abc_Print( 1, "BMC3 got cancelled. RunId=%d.\n", pData->RunId ); + } // free memory + Abc_NtkDelete( pAbcNtk ); Aig_ManStop( pData->pAig ); ABC_FREE( pData ); @@ -1353,17 +1364,15 @@ void * Wla_Bmc3Thread ( void * pArg ) return NULL; } -void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig ) +void Wla_ManConcurrentBmc3( pthread_t * pThread, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) { int status; Bmc3_ThData_t * pData; pData = ABC_CALLOC( Bmc3_ThData_t, 1 ); pData->pAig = pAig; - pData->ppCex = NULL; - status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); - pData->RunId = ++g_nRunIds; - status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + pData->ppCex = ppCex; + pData->RunId = g_nRunIds; status = pthread_create( pThread, NULL, Wla_Bmc3Thread, pData ); assert( status == 0 ); @@ -1373,8 +1382,11 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; Pdr_Man_t * pPdr; + Abc_Cex_t * pBmcCex = NULL; + pthread_t * pBmc3Thread = NULL; int RetValue = -1; int status; + int RunId = g_nRunIds; if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { @@ -1394,15 +1406,11 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) if ( pWla->pPars->fUseBmc3 ) { - pthread_t Bmc3Thread; + pWla->pPdrPars->RunId = g_nRunIds; + pWla->pPdrPars->pFuncStop = Wla_CallBackToStop; - Wla_ManConcurrentBmc3( &Bmc3Thread, Aig_ManDupSimple(pAig) ); - status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); - ++g_nRunIds; - status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); - - status = pthread_join( Bmc3Thread, NULL ); - assert( status == 0 ); + pBmc3Thread = ABC_CALLOC( pthread_t, 1 ); + Wla_ManConcurrentBmc3( pBmc3Thread, Aig_ManDupSimple( pAig ), &pBmcCex ); } clk = Abc_Clock(); @@ -1418,8 +1426,30 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 ); Pdr_ManStop( pPdr ); - pWla->pCex = pAig->pSeqModel; - pAig->pSeqModel = NULL; + + if ( pWla->pPars->fUseBmc3 ) + { + if ( RunId == g_nRunIds ) + { + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + ++g_nRunIds; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } + + status = pthread_join( *pBmc3Thread, NULL ); + assert( status == 0 ); + ABC_FREE( pBmc3Thread ); + } + + if ( pBmcCex ) + { + pWla->pCex = pBmcCex ; + } + else + { + pWla->pCex = pAig->pSeqModel; + pAig->pSeqModel = NULL; + } // consider outcomes if ( pWla->pCex == NULL ) |