diff options
Diffstat (limited to 'src/aig/saig/saigBmc3.c')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 453ea918..508a46c1 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1098,6 +1098,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Gia_ManBmc_t * p; Aig_Obj_t * pObj; int RetValue = -1, fFirst = 1; + int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) printf( "Performing BMC with constraints...\n" ); @@ -1119,6 +1120,19 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); for ( f = 0; f < pPars->nFramesMax; f++ ) { + // stop BMC after exploring all reachable states + if ( Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) ) + { + Saig_Bmc3ManStop( p ); + return pPars->nFailOuts ? 0 : 1; + } + // stop BMC if all targets are solved + if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) + { + Saig_Bmc3ManStop( p ); + return 0; + } + // consider the next timeframe pPars->iFrame = f; // resize the array Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 ); @@ -1158,8 +1172,10 @@ clkOther += clock() - clk2; return 1; } } + if ( pPars->nStart && f < pPars->nStart ) + continue; // solve SAT - clk = clock(); + clk = clock(); Saig_ManForEachPo( pAig, pObj, i ) { if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) @@ -1176,15 +1192,17 @@ clkOther += clock() - clk2; if ( Lit == 1 ) { Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); - printf( "Output %d is trivially SAT in frame %d.\n", i, f ); if ( !pPars->fSolveAll ) { + printf( "Output %d is trivially SAT in frame %d.\n", i, f ); ABC_FREE( pAig->pSeqModel ); pAig->pSeqModel = pCex; Saig_Bmc3ManStop( p ); return 0; } pPars->nFailOuts++; + printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); @@ -1231,7 +1249,8 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", i, f ); + printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); |