diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-16 00:26:18 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-16 00:26:18 -0700 |
commit | 5a4f1fe44c94ee48e707246898db1ac2d66231e9 (patch) | |
tree | 7ba98a541dde0696eb9b816a35ac8ff32369dc9c /src/proof/abs/absPth.c | |
parent | fdf5ad34339c3ca9bdcac8a409dea832469fc6da (diff) | |
download | abc-5a4f1fe44c94ee48e707246898db1ac2d66231e9.tar.gz abc-5a4f1fe44c94ee48e707246898db1ac2d66231e9.tar.bz2 abc-5a4f1fe44c94ee48e707246898db1ac2d66231e9.zip |
Made abstraction and PDR communicate in-memory rather than through a file.
Diffstat (limited to 'src/proof/abs/absPth.c')
-rw-r--r-- | src/proof/abs/absPth.c | 96 |
1 files changed, 45 insertions, 51 deletions
diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index 73f76822..fb10eb81 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -18,16 +18,14 @@ ***********************************************************************/ -#include "aig/ioa/ioa.h" +#include "abs.h" #include "proof/pdr/pdr.h" +// to compile on Linux, add -lpthread to LIBS in Makefile + // uncomment this line to enable pthreads //#define ABC_USE_PTHREADS -// to compile on Linux, modify Makefile as follows: -// add -pthread to OPTFLAGS -// add -lpthread to LIBS - #ifdef ABC_USE_PTHREADS #ifdef WIN32 @@ -47,18 +45,18 @@ ABC_NAMESPACE_IMPL_START #ifndef ABC_USE_PTHREADS -void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {} -void Gia_Ga2ProveCancel( int fVerbose ) {} -int Gia_Ga2ProveCheck( int fVerbose ) { return 0; } +void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ) {} +void Gia_GlaProveCancel( int fVerbose ) {} +int Gia_GlaProveCheck( int fVerbose ) { return 0; } #else // pthreads are used // information given to the thread typedef struct Abs_ThData_t_ { - char * pFileName; - int fVerbose; - int RunId; + Aig_Man_t * pAig; + int fVerbose; + int RunId; } Abs_ThData_t; // mutext to control access to shared variables @@ -101,66 +99,62 @@ void * Abs_ProverThread( void * pArg ) { Abs_ThData_t * pThData = (Abs_ThData_t *)pArg; Pdr_Par_t Pars, * pPars = &Pars; - Aig_Man_t * pAig, * pTemp; int RetValue, status; - pAig = Ioa_ReadAiger( pThData->pFileName, 0 ); - if ( pAig == NULL ) - Abc_Print( 1, "\nCannot open file \"%s\".\n", pThData->pFileName ); - else + // call PDR + Pdr_ManSetDefaultParams( pPars ); + pPars->fSilent = 1; + pPars->RunId = pThData->RunId; + pPars->pFuncStop = Abs_CallBackToStop; + RetValue = Pdr_ManSolve( pThData->pAig, pPars, NULL ); +// RetValue = Pdr_ManSolve_test( pAig, pPars, NULL ); + // update the result + if ( RetValue == 1 ) + { + status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); + g_fAbstractionProved = 1; + status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); + } + // quit this thread + if ( pThData->fVerbose ) { - // synthesize abstraction - pAig = Aig_ManScl( pTemp = pAig, 1, 1, 0, -1, -1, 0, 0 ); - Aig_ManStop( pTemp ); - // call PDR - Pdr_ManSetDefaultParams( pPars ); - pPars->fSilent = 1; - pPars->RunId = pThData->RunId; - pPars->pFuncStop = Abs_CallBackToStop; - RetValue = Pdr_ManSolve( pAig, pPars, NULL ); -// RetValue = Pdr_ManSolve_test( pAig, pPars, NULL ); - // update the result if ( RetValue == 1 ) - { - status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); - g_fAbstractionProved = 1; - status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); - } - // free memory - Aig_ManStop( pAig ); - // quit this thread - if ( pThData->fVerbose ) - { - if ( RetValue == 1 ) - Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId ); - else if ( RetValue == 0 ) - Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId ); - else if ( RetValue == -1 ) - Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId ); - else assert( 0 ); - } + Abc_Print( 1, "\nProved abstraction %d.\n", pThData->RunId ); + else if ( RetValue == 0 ) + Abc_Print( 1, "\nDisproved abstraction %d.\n", pThData->RunId ); + else if ( RetValue == -1 ) + Abc_Print( 1, "\nCancelled abstraction %d.\n", pThData->RunId ); + else assert( 0 ); } - ABC_FREE( pThData->pFileName ); + // free memory + Aig_ManStop( pThData->pAig ); ABC_FREE( pThData ); // quit this thread pthread_exit( NULL ); assert(0); return NULL; } -void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) +void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose ) { Abs_ThData_t * pThData; + Gia_Man_t * pAbs; + Aig_Man_t * pAig; pthread_t ProverThread; int status; - assert( pFileName != NULL ); // disable verbosity fVerbose = 0; + // create abstraction + assert( pGia->vGateClasses != NULL ); + pAbs = Gia_ManDupAbsGates( pGia, pGia->vGateClasses ); + Gia_ManCleanValue( pGia ); + pAig = Gia_ManToAigSimple( pAbs ); + Gia_ManStop( pAbs ); // reset the proof status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); g_fAbstractionProved = 0; status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); // collect thread data pThData = ABC_CALLOC( Abs_ThData_t, 1 ); - pThData->pFileName = Abc_UtilStrsav( (void *)pFileName ); + pThData->pAig = pAig; pThData->fVerbose = fVerbose; status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); pThData->RunId = ++g_nRunIds; @@ -170,14 +164,14 @@ void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) status = pthread_create( &ProverThread, NULL, Abs_ProverThread, pThData ); assert( status == 0 ); } -void Gia_Ga2ProveCancel( int fVerbose ) +void Gia_GlaProveCancel( int fVerbose ) { int status; status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); g_nRunIds++; status = pthread_mutex_unlock(&g_mutex); assert( status == 0 ); } -int Gia_Ga2ProveCheck( int fVerbose ) +int Gia_GlaProveCheck( int fVerbose ) { int status; if ( g_fAbstractionProved == 0 ) |