wlcPth.c

Go to the documentation of this file.

 
#include "wlc.h"
#include "sat/bmc/bmc.h"
 
#ifdef ABC_USE_PTHREADS
 
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
 
#endif
 
ABC_NAMESPACE_IMPL_START 

 
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           Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames, int RunId );
 
static volatile int  g_nRunIds = 0;             // the number of the last prover instance
int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
int Wla_GetGlobalRunId() { return g_nRunIds; }
 
#ifndef ABC_USE_PTHREADS
 
void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId ) {}
void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex ) {}
 
#else // pthreads are used
 
// information given to the thread
typedef struct Bmc3_ThData_t_
{
    Wla_Man_t *  pWla;
    Aig_Man_t *  pAig;
    Abc_Cex_t ** ppCex;
    int          RunId;
    int          fVerbose;
} Bmc3_ThData_t;
 
// mutext to control access to shared variables
extern pthread_mutex_t g_mutex;
 
void Wla_ManJoinThread( Wla_Man_t * pWla, int RunId )
{
    int status;
    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( *(pthread_t *)(pWla->pThread), NULL );
    assert( status == 0 );
    ABC_FREE( pWla->pThread );
    pWla->pThread = NULL;
}
    
void * Wla_Bmc3Thread ( void * pArg )
{
    int status;
    int RetValue = -1;
    int nFramesNoChangeLim = 10;
    Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
    Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
    Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
    Saig_ParBmcSetDefaultParams( pBmcPars );
    pBmcPars->pFuncStop = Wla_CallBackToStop;
    pBmcPars->RunId = pData->RunId;
 
    if ( pData->pWla->pPars->fShrinkAbs )
        pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
 
    RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
 
    if ( RetValue == 0 )
    {
        assert( pAbcNtk->pSeqModel );
        *(pData->ppCex) = pAbcNtk->pSeqModel;
        pAbcNtk->pSeqModel = NULL;
 
        if ( pData->fVerbose )
            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 if ( RetValue == -1 )
    {
        if ( pData->RunId < g_nRunIds && pData->fVerbose )
            Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
 
        if ( pData->pWla->nIters > 1 && pData->RunId == g_nRunIds )
        {
            RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim, pData->RunId );
            pData->pWla->iCexFrame += nFramesNoChangeLim; 
            
            if ( RetValue == 1 )
            {
                pData->pWla->fNewAbs = 1;
                status = pthread_mutex_lock(&g_mutex);  assert( status == 0 );
                ++g_nRunIds;
                status = pthread_mutex_unlock(&g_mutex);  assert( status == 0 );
            }
        }
    }
 
    // free memory
    Abc_NtkDelete( pAbcNtk );
    Aig_ManStop( pData->pAig );
    ABC_FREE( pData );
 
    // quit this thread
    pthread_exit( NULL );
    assert(0);
    return NULL;
}
 
void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppCex )
{
    int status;
    Bmc3_ThData_t * pData;
 
    assert( pWla->pThread == NULL );
    pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 );
 
    pData = ABC_CALLOC( Bmc3_ThData_t, 1 );
    pData->pWla = pWla;
    pData->pAig = pAig;
    pData->ppCex = ppCex;
    pData->RunId = g_nRunIds;
    pData->fVerbose = pWla->pPars->fVerbose;
 
    status = pthread_create( (pthread_t *)pWla->pThread, NULL, Wla_Bmc3Thread, pData );
    assert( status == 0 );
}
 
#endif // pthreads are used

 
 
ABC_NAMESPACE_IMPL_END