diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/abs/abs.h | 4 | ||||
-rw-r--r-- | src/proof/abs/absGla.c | 24 | ||||
-rw-r--r-- | src/proof/abs/absPth.c | 96 |
3 files changed, 59 insertions, 65 deletions
diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index eeeda583..e7ab9e7d 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -99,6 +99,10 @@ extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars ); extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta ); /*=== absIter.c =========================================================*/ extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); +/*=== absPth.c =========================================================*/ +extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ); +extern void Gia_GlaProveCancel( int fVerbose ); +extern int Gia_GlaProveCheck( int fVerbose ); /*=== absVta.c =========================================================*/ extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars ); /*=== absUtil.c =========================================================*/ diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index b026c6e3..76b6c231 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -126,11 +126,6 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) } -// calling pthreads -extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ); -extern void Gia_Ga2ProveCancel( int fVerbose ); -extern int Gia_Ga2ProveCheck( int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1449,7 +1444,7 @@ char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs ) void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) { char * pFileName; - assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver ); + assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs ); if ( p->pPars->fDumpMabs ) { pFileName = Ga2_GlaGetFileName(p, 0); @@ -1460,7 +1455,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) p->pGia->vGateClasses = Ga2_ManAbsTranslate( p ); Gia_WriteAiger( p->pGia, pFileName, 0, 0 ); } - if ( p->pPars->fDumpVabs || p->pPars->fCallProver ) + else if ( p->pPars->fDumpVabs ) { Vec_Int_t * vGateClasses; Gia_Man_t * pAbs; @@ -1475,6 +1470,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) Gia_ManStop( pAbs ); Vec_IntFreeP( &vGateClasses ); } + else assert( 0 ); } /**Function************************************************************* @@ -1564,7 +1560,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %% RatioMax = %d %%\n", pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMax ); Abc_Print( 1, "LrnStart = %d LrnDelta = %d LrnRatio = %d %% Skip = %d SimpleCNF = %d Dump = %d\n", - pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs|pPars->fCallProver ); + pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs ); if ( pPars->fDumpVabs || pPars->fDumpMabs ) Abc_Print( 1, "%s will be dumped into file \"%s\".\n", pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map", @@ -1642,7 +1638,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) } if ( iFrameTryToProve >= 0 ) { - Gia_Ga2ProveCancel( pPars->fVerbose ); + Gia_GlaProveCancel( pPars->fVerbose ); iFrameTryToProve = -1; } @@ -1762,7 +1758,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) if ( pPars->fVerbose ) Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 ); // check if abstraction was proved - if ( Gia_Ga2ProveCheck( pPars->fVerbose ) ) + if ( Gia_GlaProveCheck( pPars->fVerbose ) ) { RetValue = 1; goto finish; @@ -1785,7 +1781,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim ) { // dump the model into file - if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver ) + if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs ) { char Command[1000]; Abc_FrameSetStatus( -1 ); @@ -1800,9 +1796,9 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) { // cancel old one if it is proving if ( iFrameTryToProve >= 0 ) - Gia_Ga2ProveCancel( pPars->fVerbose ); + Gia_GlaProveCancel( pPars->fVerbose ); // prove new one - Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose ); + Gia_GlaProveAbsracted( pAig, pPars->fVerbose ); iFrameTryToProve = f; } // speak to the bridge @@ -1832,7 +1828,7 @@ finish: Prf_ManStopP( &p->pSat->pPrf2 ); // cancel old one if it is proving if ( iFrameTryToProve >= 0 ) - Gia_Ga2ProveCancel( pPars->fVerbose ); + Gia_GlaProveCancel( pPars->fVerbose ); // analize the results if ( RetValue == 1 ) Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d. ", p->pPars->iFrameProved+1, iFrameTryToProve ); 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 ) |