Skip to content

A
abc
Commit 5a4f1fe4 by Alan Mishchenko
Options

Made abstraction and PDR communicate in-memory rather than through a file.

parent fdf5ad34
Showing with 59 additions and 65 deletions
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 =========================================================*/
......
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 );
......
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 )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment