diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 13:31:29 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-14 13:31:29 -0700 |
commit | 3b14c7b490cf0cdd93f47f9697c700b19cdda895 (patch) | |
tree | e30f5e754d5304d879d357a6730dfa24cec30133 /src/aig/gia | |
parent | 19c28cae94cd2fe94d7cc7d9542d0fbacd9be95b (diff) | |
download | abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.tar.gz abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.tar.bz2 abc-3b14c7b490cf0cdd93f47f9697c700b19cdda895.zip |
Prepared &gla to try abstracting and proving concurrently.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 15 | ||||
-rw-r--r-- | src/aig/gia/giaAbsPth.c | 102 |
2 files changed, 106 insertions, 11 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index 55f79ac7..24ea351a 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -129,6 +129,7 @@ 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 void Gia_Ga2ProveFinish( int fVerbose ); extern int Gia_Ga2ProveCheck( int fVerbose ); //////////////////////////////////////////////////////////////////////// @@ -1434,8 +1435,8 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) if ( p->pPars->fDumpMabs ) { pFileName = Ga2_GlaGetFileName(p, 0); - if ( fVerbose ) - Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); +// if ( fVerbose ) +// Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName ); // dump abstraction map Vec_IntFreeP( &p->pGia->vGateClasses ); p->pGia->vGateClasses = Ga2_ManAbsTranslate( p ); @@ -1446,8 +1447,8 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose ) Vec_Int_t * vGateClasses; Gia_Man_t * pAbs; pFileName = Ga2_GlaGetFileName(p, 1); - if ( fVerbose ) - Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); +// if ( fVerbose ) +// Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName ); // dump absracted model vGateClasses = Ga2_ManAbsTranslate( p ); pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses ); @@ -1545,7 +1546,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_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->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs|pPars->fCallProver ); if ( pPars->fDumpVabs || pPars->fDumpMabs ) Abc_Print( 1, "%s will be dumped into file \"%s\".\n", pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map", @@ -1810,6 +1811,10 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) } finish: Prf_ManStopP( &p->pSat->pPrf2 ); + // cancel old one if it is proving + if ( iFrameTryProve >= 0 ) + Gia_Ga2ProveCancel( pPars->fVerbose ); + Gia_Ga2ProveFinish( 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, iFrameTryProve ); diff --git a/src/aig/gia/giaAbsPth.c b/src/aig/gia/giaAbsPth.c index 31f63674..c69f3891 100644 --- a/src/aig/gia/giaAbsPth.c +++ b/src/aig/gia/giaAbsPth.c @@ -18,10 +18,11 @@ ***********************************************************************/ -#include "gia.h" +#include "aig/ioa/ioa.h" +#include "proof/pdr/pdr.h" // comment this out to disable pthreads -//#define ABC_USE_PTHREADS +#define ABC_USE_PTHREADS #ifdef ABC_USE_PTHREADS @@ -34,7 +35,7 @@ #endif -ABC_NAMESPACE_IMPL_START +ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -59,21 +60,110 @@ ABC_NAMESPACE_IMPL_START void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {} void Gia_Ga2ProveCancel( int fVerbose ) {} +void Gia_Ga2ProveFinish( int fVerbose ) {} int Gia_Ga2ProveCheck( int fVerbose ) { return 0; } #else // pthreads are used +// information given to the thread +typedef struct Abs_Pair_t_ +{ + char * pFileName; + int fVerbose; + int RunId; +} Abs_Pair_t; + +// the last valid thread +static int g_nRunIds = 0; +int Abs_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; } + + +int Pdr_ManSolve_test( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex ) +{ + char * p = ABC_ALLOC( char, 111 ); + while ( 1 ) + { + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + break; + } + ABC_FREE( p ); + return -1; +} + +static int g_fAbstractionProved = 0; +void * Abs_ProverThread( void * pArg ) +{ + Abs_Pair_t * pPair = (Abs_Pair_t *)pArg; + Pdr_Par_t Pars, * pPars = &Pars; + Aig_Man_t * pAig, * pTemp; + int RetValue; + pAig = Ioa_ReadAiger( pPair->pFileName, 0 ); + if ( pAig == NULL ) + Abc_Print( 1, "\nCannot open file \"%s\".\n", pPair->pFileName ); + else + { + // 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 = pPair->RunId; + pPars->pFuncStop = Abs_CallBackToStop; + RetValue = Pdr_ManSolve( pAig, pPars, NULL ); +// RetValue = Pdr_ManSolve_test( pAig, pPars, NULL ); + // update the result + g_fAbstractionProved = (RetValue == 1); + // free memory + Aig_ManStop( pAig ); + // quit this thread + if ( pPair->fVerbose ) + { + if ( RetValue == 1 ) + Abc_Print( 1, "\nProved abstraction %d.\n", pPair->RunId ); + else if ( RetValue == 0 ) + Abc_Print( 1, "\nDisproved abstraction %d.\n", pPair->RunId ); + else if ( RetValue == -1 ) + Abc_Print( 1, "\nCancelled abstraction %d.\n", pPair->RunId ); + else assert( 0 ); + } + } + ABC_FREE( pPair->pFileName ); + ABC_FREE( pPair ); + // quit this thread + pthread_exit( NULL ); + assert(0); + return NULL; +} void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) { - Abc_Print( 1, "Trying to prove abstraction.\n" ); + Abs_Pair_t * pPair; + pthread_t ProverThread; + int RetValue; + assert( pFileName != NULL ); + g_fAbstractionProved = 0; + // disable verbosity + fVerbose = 0; + // create thread + pPair = ABC_CALLOC( Abs_Pair_t, 1 ); + pPair->pFileName = Abc_UtilStrsav( (void *)pFileName ); + pPair->fVerbose = fVerbose; + pPair->RunId = ++g_nRunIds; + if ( fVerbose ) Abc_Print( 1, "\nTrying to prove abstraction %d.\n", pPair->RunId ); + RetValue = pthread_create( &ProverThread, NULL, Abs_ProverThread, pPair ); + assert( RetValue == 0 ); } void Gia_Ga2ProveCancel( int fVerbose ) { - Abc_Print( 1, "Canceling attempt to prove abstraction.\n" ); + g_nRunIds++; +} +void Gia_Ga2ProveFinish( int fVerbose ) +{ + g_fAbstractionProved = 0; } int Gia_Ga2ProveCheck( int fVerbose ) { - return 0; + return g_fAbstractionProved; } #endif |