summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c20
-rw-r--r--src/proof/pdr/pdrInt.h3
-rw-r--r--src/proof/pdr/pdrInv.c22
-rw-r--r--src/proof/pdr/pdrUtil.c4
5 files changed, 35 insertions, 15 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 4f0f769e..d245b467 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -44,6 +44,7 @@ struct Pdr_Par_t_
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
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 025ada06..9ba5dc2d 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -50,6 +50,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->nFrameMax = 5000; // limit on number of timeframes
pPars->nTimeOut = 0; // timeout in seconds
pPars->nConfLimit = 100000; // limit on SAT solver conflicts
+ pPars->nRestLimit = 0; // limit on the number of proof-obligations
pPars->fTwoRounds = 0; // use two rounds for generalization
pPars->fMonoCnf = 0; // monolythic CNF
pPars->fDumpInv = 0; // dump inductive invariant
@@ -429,6 +430,12 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
pThis = Pdr_QueueHead( p );
if ( pThis->iFrame == 0 )
return 0; // SAT
+ if ( p->nQueLim && p->nQueCur >= p->nQueLim )
+ {
+ p->nQueLim = p->nQueLim * 11 / 10;
+ Pdr_QueueStop( p );
+ return 1; // restart
+ }
pThis = Pdr_QueuePop( p );
assert( pThis->iFrame > 0 );
assert( !Pdr_SetIsInit(pThis->pState, -1) );
@@ -584,12 +591,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->iFrame = k;
return 0; // SAT
}
+ if ( p->pPars->fVerbose )
+ Pdr_ManPrintProgress( p, 0, clock() - clkStart );
}
else
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
// open a new timeframe
+ p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, k );
Pdr_ManCreateSolver( p, ++k );
@@ -619,7 +629,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
- clkStart = clock();
+// clkStart = clock();
}
// check the timeout
@@ -696,6 +706,14 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
***********************************************************************/
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
{
+// printf( "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
+ printf( "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ",
+ pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
+ if ( pPars->iOutput >= 0 )
+ printf( "Output = %d. ", pPars->iOutput );
+ printf( "MonoCNF = %s. SkipGen = %s.\n",
+ pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+
/*
Vec_Int_t * vPrioInit = NULL;
int RetValue, nTimeOut;
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index baf4ca02..0a90f9d1 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -107,6 +107,9 @@ struct Pdr_Man_t_
int nCasesSU;
int nCasesUS;
int nCasesUU;
+ int nQueCur;
+ int nQueMax;
+ int nQueLim;
// runtime
int timeStart;
int timeToStop;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index 30d1145d..92bd6d00 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -46,7 +46,6 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
{
- static int PastSize;
Vec_Ptr_t * vVec;
int i, ThisSize, Length, LengthStart;
if ( Vec_PtrSize(p->vSolvers) < 2 )
@@ -56,9 +55,9 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Vec_VecForEachLevel( p->vClauses, vVec, i )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
// determine the starting point
- LengthStart = Abc_MaxInt( 0, Length - 70 );
+ LengthStart = Abc_MaxInt( 0, Length - 60 );
printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
- ThisSize = 6;
+ ThisSize = 5;
if ( LengthStart > 0 )
{
printf( " ..." );
@@ -76,18 +75,13 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
Length += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
ThisSize += 1 + Abc_Base10Log(Vec_PtrSize(vVec)+1);
}
+ for ( i = ThisSize; i < 70; i++ )
+ printf( " " );
+ printf( "%6d", p->nQueMax );
+ printf(" %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
+ printf("%s", fClose ? "\n":"\r" );
if ( fClose )
- {
- for ( i = 0; i < PastSize - ThisSize; i++ )
- printf( " " );
- printf( "\n" );
- }
- else
- {
- printf( "\r" );
- PastSize = ThisSize;
- }
-// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
+ p->nQueMax = 0;
}
/**Function*************************************************************
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 17383425..c0570988 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -500,6 +500,7 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
return NULL;
p->pQueue = p->pQueue->pLink;
Pdr_OblDeref( pRes );
+ p->nQueCur--;
return pRes;
}
@@ -518,6 +519,8 @@ void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
{
Pdr_Obl_t * pTemp, ** ppPrev;
p->nObligs++;
+ p->nQueCur++;
+ p->nQueMax = Abc_MaxInt( p->nQueMax, p->nQueCur );
Pdr_OblRef( pObl );
if ( p->pQueue == NULL )
{
@@ -569,6 +572,7 @@ void Pdr_QueueStop( Pdr_Man_t * p )
Pdr_OblDeref( pObl );
}
p->pQueue = NULL;
+ p->nQueCur = 0;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-28 09:40:09 +0000