diff options
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
-rw-r--r-- | src/proof/pdr/pdrCore.c | 74 |
1 files changed, 5 insertions, 69 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 6ebceedf..fe023617 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -139,11 +139,8 @@ int Pdr_ManPushClauses( Pdr_Man_t * p ) int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1; int Counter = 0; abctime clk = Abc_Clock(); - assert( p->iUseFrame > 0 ); - Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax ) - { Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare ); vArrayK1 = Vec_VecEntry( p->vClauses, k+1 ); @@ -457,9 +454,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) pThis = Pdr_QueuePop( p ); assert( pThis->iFrame > 0 ); assert( !Pdr_SetIsInit(pThis->pState, -1) ); - p->iUseFrame = Abc_MinInt( p->iUseFrame, pThis->iFrame ); - clk = Abc_Clock(); if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) ) { @@ -493,38 +488,27 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) if ( RetValue ) // cube is blocked inductively in this frame { assert( pCubeMin != NULL ); - // k is the last frame where pCubeMin holds k = pThis->iFrame; - // check other frames assert( pPred == NULL ); for ( k = pThis->iFrame; k < kMax; k++ ) - { - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ); - if ( RetValue == -1 ) - { - Pdr_OblDeref( pThis ); - return -1; - } if ( !RetValue ) break; - } - // add new clause if ( p->pPars->fVeryVerbose ) { - Abc_Print( 1, "Adding cube " ); - Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL ); - Abc_Print( 1, " to frame %d.\n", k ); + Abc_Print( 1, "Adding cube " ); + Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL ); + Abc_Print( 1, " to frame %d.\n", k ); } // set priority flops for ( i = 0; i < pCubeMin->nLits; i++ ) @@ -533,7 +517,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); } - Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref p->nCubes++; // add clause @@ -541,7 +524,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) Pdr_ManSolverAddClause( p, i, pCubeMin ); // schedule proof obligation if ( (k < kMax || p->pPars->fReuseProofOblig) && !p->pPars->fShortest ) - { pThis->iFrame = k+1; pThis->prio = Prio--; @@ -558,7 +540,6 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) assert( pPred != NULL ); pThis->prio = Prio--; Pdr_QueuePush( p, pThis ); - pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) ); Pdr_QueuePush( p, pThis ); } @@ -592,7 +573,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) int fPrintClauses = 0; Pdr_Set_t * pCube = NULL; Aig_Obj_t * pObj; - Abc_Cex_t * pCexNew; int k, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); @@ -604,11 +584,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManCreateSolver( p, (k = 0) ); while ( 1 ) { - p->nFrames = k; assert( k == Vec_PtrSize(p->vSolvers)-1 ); p->iUseFrame = ABC_INFINITY; - Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs @@ -626,24 +604,18 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( !p->pPars->fSolveAll ) { pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ); - p->pAig->pSeqModel = pCexNew; return 0; // SAT } pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1; - p->pPars->nFailOuts++; if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); - if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { if ( p->pPars->fVerbose ) @@ -684,29 +656,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( p->timeToStop && Abc_Clock() > p->timeToStop ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); - else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); - else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) - { - Pdr_QueueClean( p ); - pCube = NULL; - break; // keep solving - } - else 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; @@ -730,9 +690,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) break; // keep solving } else 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; @@ -748,23 +706,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); p->pPars->iFrame = k; - if ( !p->pPars->fSolveAll ) { p->pAig->pSeqModel = Pdr_ManDeriveCex(p); return 0; // SAT } p->pPars->nFailOuts++; - pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1; - if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); - if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); - Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) ) { @@ -797,13 +749,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) { p->pPars->nDropOuts++; if ( p->pPars->vOutMap ) - Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); if ( !p->pPars->fNotVerbose ) - Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur ); } - p->timeToStopOne = 0; } } @@ -851,24 +800,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->vOutMap ) for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ ) if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown - { Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat - if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, k ); - } - if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) - return 1; // UNSAT - if ( p->pPars->nFailOuts > 0 ) - return 0; // SAT - return -1; } if ( p->pPars->fVerbose ) @@ -939,9 +879,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) int k, RetValue; abctime clk = Abc_Clock(); if ( pPars->nTimeOutOne && !pPars->fSolveAll ) - pPars->nTimeOutOne = 0; - if ( pPars->nTimeOutOne ) pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0); if ( pPars->fVerbose ) @@ -978,10 +916,8 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) for ( k = 0; k < Saig_ManPoNum(pAig); k++ ) if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec - - if ( pPars->fUseBridge ){ - Gia_ManToBridgeAbort( stdout, 7, "timeout" ); } - + if ( pPars->fUseBridge ) + Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" ); return RetValue; } |