summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/pdr/pdr.h35
-rw-r--r--src/proof/pdr/pdrCore.c39
2 files changed, 48 insertions, 26 deletions
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-06 17:51:39 +0000