summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAbsGla2.c15
-rw-r--r--src/aig/gia/giaAbsPth.c102
-rw-r--r--src/base/abci/abcDar.c21
-rw-r--r--src/proof/pdr/pdr.h35
-rw-r--r--src/proof/pdr/pdrCore.c39
5 files changed, 166 insertions, 46 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
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 85377956..8278fa16 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2577,15 +2577,18 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
else
RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
// output the result
- if ( RetValue == 1 )
- Abc_Print( 1, "Property proved. " );
- else if ( RetValue == 0 )
- Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
- else if ( RetValue == -1 )
- Abc_Print( 1, "Property UNDECIDED. " );
- else
- assert( 0 );
-ABC_PRT( "Time", clock() - clk );
+ if ( !pPars->fSilent )
+ {
+ if ( RetValue == 1 )
+ Abc_Print( 1, "Property proved. " );
+ else if ( RetValue == 0 )
+ Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
+ else if ( RetValue == -1 )
+ Abc_Print( 1, "Property UNDECIDED. " );
+ else
+ assert( 0 );
+ ABC_PRT( "Time", clock() - clk );
+ }
if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index d245b467..491477dd 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -40,20 +40,23 @@ ABC_NAMESPACE_HEADER_START
typedef struct Pdr_Par_t_ Pdr_Par_t;
struct Pdr_Par_t_
{
- int iOutput; // zero-based number of primary output to solve
- int nRecycle; // limit on vars for recycling
- int nFrameMax; // limit on frame count
- int nConfLimit; // limit on SAT solver conflicts
- int nRestLimit; // limit on the number of proof-obligations
- int nTimeOut; // timeout in seconds
- int fTwoRounds; // use two rounds for generalization
- int fMonoCnf; // monolythic CNF
- int fDumpInv; // dump inductive invariant
- int fShortest; // forces bug traces to be shortest
- int fSkipGeneral; // skips expensive generalization step
- int fVerbose; // verbose output
- int fVeryVerbose; // very verbose output
- int iFrame; // explored up to this frame
+ int iOutput; // zero-based number of primary output to solve
+ int nRecycle; // limit on vars for recycling
+ int nFrameMax; // limit on frame count
+ int nConfLimit; // limit on SAT solver conflicts
+ int nRestLimit; // limit on the number of proof-obligations
+ int nTimeOut; // timeout in seconds
+ int fTwoRounds; // use two rounds for generalization
+ int fMonoCnf; // monolythic CNF
+ int fDumpInv; // dump inductive invariant
+ int fShortest; // forces bug traces to be shortest
+ int fSkipGeneral; // skips expensive generalization step
+ int fVerbose; // verbose output`
+ int fVeryVerbose; // very verbose output
+ int fSilent; // totally silent execution
+ int iFrame; // explored up to this frame
+ int RunId; // PDR id in this run
+ int(*pFuncStop)(int); // callback to terminate
};
////////////////////////////////////////////////////////////////////////
@@ -65,8 +68,8 @@ struct Pdr_Par_t_
////////////////////////////////////////////////////////////////////////
/*=== pdrCore.c ==========================================================*/
-extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
+extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 765894e3..5cb05143 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -528,7 +528,9 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
Pdr_QueuePush( p, pThis );
}
- // check the timeout
+ // check termination
+ if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+ return -1;
if ( p->timeToStop && clock() > p->timeToStop )
return -1;
}
@@ -565,7 +567,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ if ( p->pPars->nConfLimit )
+ Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ else if ( p->pPars->fVerbose )
+ Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
return -1;
}
@@ -576,7 +581,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ if ( p->pPars->nConfLimit )
+ Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ else if ( p->pPars->fVerbose )
+ Abc_Print( 1, "Computation cancelled by the callback.\n" );
p->pPars->iFrame = k;
return -1;
}
@@ -615,7 +623,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
+ if ( !p->pPars->fSilent )
+ Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
p->pPars->iFrame = k;
return -1;
}
@@ -623,8 +632,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Pdr_ManReportInvariant( p );
- Pdr_ManVerifyInvariant( p );
+ if ( !p->pPars->fSilent )
+ Pdr_ManReportInvariant( p );
+ if ( !p->pPars->fSilent )
+ Pdr_ManVerifyInvariant( p );
p->pPars->iFrame = k;
return 1; // UNSAT
}
@@ -633,7 +644,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
// clkStart = clock();
}
- // check the timeout
+ // check termination
+ if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
+ {
+ p->pPars->iFrame = k;
+ return -1;
+ }
if ( p->timeToStop && clock() > p->timeToStop )
{
if ( fPrintClauses )
@@ -643,7 +659,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
+ if ( !p->pPars->fSilent )
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
p->pPars->iFrame = k;
return -1;
}
@@ -651,7 +668,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
- Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
+ if ( !p->pPars->fSilent )
+ Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = k;
return -1;
}
@@ -677,7 +695,8 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
clock_t clk = clock();
p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
RetValue = Pdr_ManSolveInt( p );
- *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+ if ( ppCex )
+ *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
if ( p->pPars->fDumpInv )
Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
// if ( *ppCex && pPars->fVerbose )
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 15:15:49 +0000