diff options
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 11 | ||||
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 4 | ||||
| -rw-r--r-- | src/proof/pdr/pdrTsim.c | 37 |
3 files changed, 11 insertions, 41 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 5aa689f5..f77bc05f 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -706,7 +706,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) { Counter++; pThis = Pdr_QueueHead( p ); - if ( pThis->iFrame == 0 ) + if ( pThis->iFrame == 0 || (p->pPars->fUseAbs && Pdr_SetIsInit(pThis->pState, -1)) ) return 0; // SAT if ( pThis->iFrame > kMax ) // finished this level return 1; @@ -862,7 +862,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) while ( 1 ) { int fRefined = 0; - if ( p->pPars->fUseAbs && iFrame == 3 ) + if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 2 ) { int i, Prio; assert( p->vAbsFlops == NULL ); @@ -995,7 +995,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } - if ( p->pPars->fVerbose ) + if ( p->pPars->fVerbose && !p->pPars->fUseAbs ) Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) @@ -1043,6 +1043,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart ); } } + if ( fRefined ) + break; if ( p->pTime4Outs ) { abctime timeSince = Abc_Clock() - clkOne; @@ -1059,9 +1061,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) p->timeToStopOne = 0; } } - if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart ); + if ( fRefined ) + continue; // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index e3233a3a..554add9b 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -470,8 +470,8 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p ) Vec_Ptr_t * vCubes; int kStart = Pdr_ManFindInvariantStart( p ); vCubes = Pdr_ManCollectCubes( p, kStart ); - Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", - kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns ); + Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (cex = %d, ave = %.2f)\n", + kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), p->nCexesTotal, 1.0*p->nXsimLits/p->nXsimRuns ); // Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", // kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); Vec_PtrFree( vCubes ); diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 283a0e1d..acbf70f5 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -473,54 +473,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits ); assert( Vec_IntSize(vRes) > 0 ); //p->tTsim += Abc_Clock() - clk; + // move abstracted literals from flops to inputs if ( p->pPars->fUseAbs && p->vAbsFlops ) { - int i, iLit, Used, k = 0, fAllNegs = 1; + int i, iLit, k = 0; Vec_IntForEachEntry( vRes, iLit, i ) { if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop - { Vec_IntWriteEntry( vRes, k++, iLit ); - fAllNegs &= Abc_LitIsCompl(iLit); - } else Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit ); } Vec_IntShrink( vRes, k ); - if ( fAllNegs ) // insert any positive literal - { - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) - { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - if ( Vec_IntEntry(vCiVals, i) ) - { - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - Vec_IntPush( vRes, Abc_Var2Lit(Entry, 0) ); - break; - } - } - // add any flop that is not in the cone - if ( i == Vec_IntSize(vCiObjs) ) - { - Vec_IntForEachEntry( p->vAbsFlops, Used, i ) - { - if ( !Used ) - continue; - if ( Vec_IntFind( vRes, Abc_Var2Lit(i, 1) ) >= 0 ) - continue; - Vec_IntPush( vRes, Abc_Var2Lit(i, 0) ); - //Vec_IntPrint( vRes ); - break; - } - assert( i < Vec_IntSize(p->vAbsFlops) ); - } - } } pRes = Pdr_SetCreate( vRes, vPiLits ); - assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); - //ZH: Disabled assertion because this invariant doesn't hold with down //because of the join operation which can bring in initial states //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); |