summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/abs.h4
-rw-r--r--src/proof/abs/absGla.c24
-rw-r--r--src/proof/abs/absPth.c96
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 )
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-22 09:33:22 +0000