Skip to content

A
abc
Commit 0f49783c by Alan Mishchenko
Options

Compiler warning.

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