diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-01 08:00:04 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-01 08:00:04 +0700 |
| commit | dbe2b466d79fb550275c4334697ea600acd66036 (patch) | |
| tree | ea063fabf4dc3e14ca6c37c3bf511f5c103ad4d9 | |
| parent | 519b03e8e89c1fd07343d6883ea2c77d259a79e1 (diff) | |
| download | abc-dbe2b466d79fb550275c4334697ea600acd66036.tar.gz abc-dbe2b466d79fb550275c4334697ea600acd66036.tar.bz2 abc-dbe2b466d79fb550275c4334697ea600acd66036.zip | |
Added handling of exceeding conflict limit in PushClasses.
| -rw-r--r-- | src/sat/pdr/pdrCore.c | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c index 3567fde6..04caba1e 100644 --- a/src/sat/pdr/pdrCore.c +++ b/src/sat/pdr/pdrCore.c @@ -127,7 +127,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) { Pdr_Set_t * pTemp, * pCubeK, * pCubeK1; Vec_Ptr_t * vArrayK, * vArrayK1; - int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1; + int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; int Counter = 0; int clk = clock(); Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax ) @@ -150,7 +150,10 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) } // check if the clause can be moved to the next frame - if ( !Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ) ) + RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ); + if ( RetValue2 == -1 ) + return -1; + if ( !RetValue2 ) continue; { @@ -590,7 +593,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintClauses( p, 0 ); } // push clauses into this timeframe - if ( Pdr_ManPushClauses( p ) ) + RetValue = Pdr_ManPushClauses( p ); + if ( RetValue == -1 ) + { + if ( p->pPars->fVerbose ) + Pdr_ManPrintProgress( p, 1, clock() - clkStart ); + printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + p->pPars->iFrame = k; + return -1; + } + if ( RetValue ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, clock() - clkStart ); |