From 8bff9aa1cd118028db47d886254dc4c76c516166 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 17:36:20 -0800 Subject: Adding PDR with abstraction. --- src/aig/gia/giaDup.c | 74 ++++++++++++++++++++++++++ src/base/io/io.c | 2 +- src/proof/pdr/pdrCore.c | 132 ++++++++++++++++++++++++++++------------------- src/proof/pdr/pdrInt.h | 10 ++-- src/proof/pdr/pdrInv.c | 1 + src/proof/pdr/pdrMan.c | 113 +++++++++++++++++++++++++++++++++++----- src/proof/pdr/pdrTsim.c | 36 ++++++++++++- src/sat/bmc/bmc.h | 3 +- src/sat/bmc/bmcCexCare.c | 62 +++++++++++----------- 9 files changed, 330 insertions(+), 103 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index b0ba3472..2a0fe6e3 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -220,6 +220,80 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int k, Flop, Used; + assert( Vec_IntSize(vMapFf2Ppi) == Vec_IntSize(vMapPpi2Ff) + Vec_IntCountEntry(vMapFf2Ppi, -1) ); + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + // create inputs + Gia_ManForEachPi( p, pObj, k ) + pObj->Value = Gia_ManAppendCi(pNew); + Vec_IntForEachEntry( vMapPpi2Ff, Flop, k ) + { + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj->Value = Gia_ManAppendCi(pNew); + } + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + if ( Used >= 0 ) + { + assert( pObj->Value != ~0 ); + continue; + } + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + assert( pObj->Value == ~0 ); + pObj->Value = Gia_ManAppendCi(pNew); + } + Gia_ManForEachCi( p, pObj, k ) + assert( pObj->Value != ~0 ); + // create nodes + Gia_ManForEachPo( p, pObj, k ) + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + if ( Used >= 0 ) + continue; + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj = Gia_ObjRoToRi( p, pObj ); + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + } + // create outputs + Gia_ManForEachPo( p, pObj, k ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + if ( Used >= 0 ) + continue; + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj = Gia_ObjRoToRi( p, pObj ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) - Vec_IntSize(vMapPpi2Ff) ); + assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) + Vec_IntSize(vMapPpi2Ff) ); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) ); + assert( Gia_ManCoNum(pNew) == Gia_ManCoNum(p) - Vec_IntSize(vMapPpi2Ff) ); + return pNew; +} + + /**Function************************************************************* Synopsis [Duplicates AIG while putting objects in the DFS order.] diff --git a/src/base/io/io.c b/src/base/io/io.c index c2cf15d4..2e1ae591 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -2420,7 +2420,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose ); } else - pCare = Bmc_CexCareMinimize( pAig, 0, pCex, fCheckCex, fVerbose ); + pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose ); Aig_ManStop( pAig ); } // output flop values (unaffected by the minimization) diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 74a15e40..47f0ac8b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -420,6 +420,8 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 ) + p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } @@ -778,6 +780,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); + if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 ) + p->nAbsFlops++; Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref @@ -837,29 +841,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_Set_t * pCube = NULL; Aig_Obj_t * pObj; Abc_Cex_t * pCexNew; - int k, RetValue = -1; + int iFrame, RetValue = -1; int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) ); abctime clkStart = Abc_Clock(), clkOne = 0; p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; assert( Vec_PtrSize(p->vSolvers) == 0 ); // in the multi-output mode, mark trivial POs (those fed by const0) as solved if ( p->pPars->fSolveAll ) - Saig_ManForEachPo( p->pAig, pObj, k ) + Saig_ManForEachPo( p->pAig, pObj, iFrame ) if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) ) { - Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat p->pPars->nProveOuts++; if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, k ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } // create the first timeframe p->pPars->timeLastSolved = Abc_Clock(); - Pdr_ManCreateSolver( p, (k = 0) ); + Pdr_ManCreateSolver( p, (iFrame = 0) ); while ( 1 ) { - p->nFrames = k; - assert( k == Vec_PtrSize(p->vSolvers)-1 ); - p->iUseFrame = Abc_MaxInt(k, 1); + if ( p->pPars->fUseAbs && iFrame == 2 ) + { + int i, Prio, Num = Saig_ManPiNum(p->pAig); + assert( p->vAbsFlops == NULL ); + p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); + p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); + p->vMapPpi2Ff = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( p->vPrio, Prio, i ) + if ( Prio >> p->nPrioShift ) + Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); + } + if ( p->pPars->fUseAbs && p->vAbsFlops ) + printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) ); + + p->nFrames = iFrame; + assert( iFrame == Vec_PtrSize(p->vSolvers)-1 ); + p->iUseFrame = Abc_MaxInt(iFrame, 1); Saig_ManForEachPo( p->pAig, pObj, p->iOutCur ) { // skip disproved outputs @@ -876,16 +894,16 @@ 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 ); + pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*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; + pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*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 ); if ( !p->pPars->fNotVerbose ) 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, iFrame, 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 ); @@ -895,8 +913,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Quitting due to callback on fail.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) ) @@ -918,11 +936,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; return -1; } - RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 ); + RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0 ); if ( RetValue == 1 ) break; if ( RetValue == -1 ) @@ -930,9 +948,9 @@ 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 ); + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); 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) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) { Pdr_QueueClean( p ); @@ -940,10 +958,10 @@ 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 ); + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( RetValue == 0 ) @@ -954,9 +972,9 @@ 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 ); + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); 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) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne ) { Pdr_QueueClean( p ); @@ -964,25 +982,33 @@ 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 ); + Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame ); else if ( p->pPars->fVerbose ) - Abc_Print( 1, "Computation cancelled by the callback.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( RetValue == 0 ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; if ( !p->pPars->fSolveAll ) { - p->pAig->pSeqModel = Pdr_ManDeriveCex(p); + Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p); + if ( pCex == NULL ) + { + assert( p->pPars->fUseAbs ); + Pdr_QueueClean( p ); + pCube = NULL; + break; // keep solving + } + p->pAig->pSeqModel = pCex; return 0; // SAT } p->pPars->nFailOuts++; @@ -997,13 +1023,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Quitting due to callback on fail.\n" ); - p->pPars->iFrame = k; + Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( !p->pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n", - nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); + nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) ); if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) ) return 0; // all SAT Pdr_QueueClean( p ); @@ -1025,7 +1051,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) 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 ); + Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame ); } p->timeToStopOne = 0; } @@ -1036,11 +1062,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // open a new timeframe p->nQueLim = p->pPars->nRestLimit; assert( pCube == NULL ); - Pdr_ManSetPropertyOutput( p, k ); - Pdr_ManCreateSolver( p, ++k ); + Pdr_ManSetPropertyOutput( p, iFrame ); + Pdr_ManCreateSolver( p, ++iFrame ); if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } // push clauses into this timeframe @@ -1052,11 +1078,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( !p->pPars->fSilent ) { 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) in frame %d.\n", p->pPars->nTimeOut, iFrame ); else - Abc_Print( 1, "Reached conflict limit (%d).\n", p->pPars->nConfLimit ); + Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame ); } - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } if ( RetValue ) @@ -1067,17 +1093,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) Pdr_ManReportInvariant( p ); if ( !p->pPars->fSilent ) Pdr_ManVerifyInvariant( p ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; // count the number of UNSAT outputs p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' if ( p->pPars->vOutMap ) - for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ ) - if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown + for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ ) + if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown { - Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat + Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat if ( p->pPars->fUseBridge ) - Gia_ManToBridgeResult( stdout, 1, NULL, k ); + Gia_ManToBridgeResult( stdout, 1, NULL, iFrame ); } if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) ) return 1; // UNSAT @@ -1091,44 +1117,44 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // check termination if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) ) { - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } if ( p->timeToStop && Abc_Clock() > p->timeToStop ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached timeout (%d seconds).\n", p->pPars->nTimeOut ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame ); + p->pPars->iFrame = iFrame; return -1; } if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC ) { if ( fPrintClauses ) { - Abc_Print( 1, "*** Clauses after frame %d:\n", k ); + Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame ); Pdr_ManPrintClauses( p, 0 ); } if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) - Abc_Print( 1, "Reached gap timeout (%d seconds).\n", p->pPars->nTimeOutGap ); - p->pPars->iFrame = k; + Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame ); + p->pPars->iFrame = iFrame; return -1; } - if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax ) + if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax ) { if ( p->pPars->fVerbose ) Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart ); if ( !p->pPars->fSilent ) Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax ); - p->pPars->iFrame = k; + p->pPars->iFrame = iFrame; return -1; } } diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index fb671700..2ee4ae09 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -31,6 +31,7 @@ #include "sat/bsat/satSolver.h" #include "pdr.h" #include "misc/hash/hashInt.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_HEADER_START @@ -71,6 +72,7 @@ struct Pdr_Man_t_ // input problem Pdr_Par_t * pPars; // parameters Aig_Man_t * pAig; // user's AIG + Gia_Man_t * pGia; // user's AIG // static CNF representation Cnf_Man_t * pCnfMan; // CNF manager Cnf_Dat_t * pCnf1; // CNF for this AIG @@ -90,7 +92,10 @@ struct Pdr_Man_t_ int * pOrder; // ordering of the lits Vec_Int_t * vActVars; // the counter of activation variables int iUseFrame; // the first used frame - Vec_Int_t * vAbs; // abstraction (mapping abstracted flop ID into its PPIs number) + int nAbsFlops; // the number of flops used + Vec_Int_t * vAbsFlops; // flops currently used + Vec_Int_t * vMapFf2Ppi; + Vec_Int_t * vMapPpi2Ff; // terminary simulation Txs_Man_t * pTxs; // internal use @@ -161,8 +166,6 @@ static inline abctime Pdr_ManTimeLimit( Pdr_Man_t * p ) /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== pdrCex.c ==========================================================*/ -extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); /*=== pdrCnf.c ==========================================================*/ extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj ); extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar ); @@ -183,6 +186,7 @@ extern Vec_Int_t * Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit ); extern void Pdr_ManStop( Pdr_Man_t * p ); extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ); +extern Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ); /*=== pdrSat.c ==========================================================*/ extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ); extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k ); diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index fe759fff..7a8a66d6 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -81,6 +81,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time ) for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%6d", p->nQueMax ); + Abc_Print( 1, "%6d", p->nAbsFlops ); Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); if ( p->pPars->fSolveAll ) Abc_Print( 1, " CEX =%4d", p->pPars->nFailOuts ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index b2df5e01..e2807c92 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "pdrInt.h" -#include "aig/gia/giaAig.h" +#include "sat/bmc/bmc.h" ABC_NAMESPACE_IMPL_START @@ -233,13 +233,6 @@ Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls ) //Vec_IntPrint( vCosts ); return vCosts; } -Vec_Int_t * Pdr_ManDeriveFlopPriorities( Aig_Man_t * pAig, int fMuxCtrls ) -{ - Gia_Man_t * pGia = Gia_ManFromAigSimple(pAig); - Vec_Int_t * vRes = Pdr_ManDeriveFlopPriorities2(pGia, fMuxCtrls); - Gia_ManStop( pGia ); - return vRes; -} /**Function************************************************************* @@ -258,6 +251,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p = ABC_CALLOC( Pdr_Man_t, 1 ); p->pPars = pPars; p->pAig = pAig; + p->pGia = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL; p->vSolvers = Vec_PtrAlloc( 0 ); p->vClauses = Vec_VecAlloc( 0 ); p->pQueue = NULL; @@ -270,7 +264,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio if ( vPrioInit ) p->vPrio = vPrioInit; else if ( pPars->fFlopPrio ) - p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 1); + p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1); else if ( p->pPars->fNewXSim ) p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) ); else @@ -286,8 +280,6 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed p->vRes = Vec_IntAlloc( 100 ); // final result p->pCnfMan = Cnf_ManStart(); - if ( p->vAbs ) - p->vAbs = Vec_IntStart( Aig_ManRegNum(pAig) ); // ternary simulation p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL; // additional AIG data-members @@ -328,6 +320,7 @@ void Pdr_ManStop( Pdr_Man_t * p ) Pdr_Set_t * pCla; sat_solver * pSat; int i, k; + Gia_ManStopP( &p->pGia ); Aig_ManCleanMarkAB( p->pAig ); if ( p->pPars->fVerbose ) { @@ -370,7 +363,9 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_WecFreeP( &p->vVLits ); // CNF manager Cnf_ManStop( p->pCnfMan ); - Vec_IntFreeP( &p->vAbs ); + Vec_IntFreeP( &p->vAbsFlops ); + Vec_IntFreeP( &p->vMapFf2Ppi ); + Vec_IntFreeP( &p->vMapPpi2Ff ); // terminary simulation if ( p->pPars->fNewXSim ) Txs_ManStop( p->pTxs ); @@ -419,7 +414,6 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) nFrames++; // create the counter-example pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); -// pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; pCex->iPo = p->iOutCur; pCex->iFrame = nFrames-1; for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) @@ -428,6 +422,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) Lit = pObl->pState->Lits[i]; if ( lit_sign(Lit) ) continue; + if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away + continue; assert( lit_var(Lit) < pCex->nPis ); Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); } @@ -437,6 +433,97 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) return pCex; } +/**Function************************************************************* + + Synopsis [Derives counter-example when abstraction is used.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p ) +{ + extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi ); + + Gia_Man_t * pAbs; + Abc_Cex_t * pCex, * pCexCare; + Pdr_Obl_t * pObl; + int i, f, Lit, Flop, nFrames = 0; + int nPis = Saig_ManPiNum(p->pAig); + int nFfRefined = 0; + if ( !p->pPars->fUseAbs ) + return Pdr_ManDeriveCex(p); + // restore previous map + Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i ) + { + assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i ); + Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 ); + } + Vec_IntClear( p->vMapPpi2Ff ); + // count the number of frames + for ( pObl = p->pQueue; pObl; pObl = pObl->pNext ) + { + for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) + { + Lit = pObl->pState->Lits[i]; + if ( lit_var(Lit) < nPis ) // PI literal + continue; + Flop = lit_var(Lit) - nPis; + if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal + continue; + Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) ); + Vec_IntPush( p->vMapPpi2Ff, Flop ); + } + nFrames++; + } + if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX + return Pdr_ManDeriveCex(p); + // create the counter-example + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames ); + pCex->iPo = p->iOutCur; + pCex->iFrame = nFrames-1; + for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) + for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) + { + Lit = pObl->pState->Lits[i]; + if ( lit_sign(Lit) ) + continue; + if ( lit_var(Lit) < nPis ) // PI literal + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) ); + else + { + int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis); + assert( iPPI < pCex->nPis ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI ); + } + } + assert( f == nFrames ); + // perform CEX minimization + pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi ); + pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 1, 1 ); + Gia_ManStop( pAbs ); + assert( pCexCare->nPis == pCex->nPis ); + Abc_CexFree( pCex ); + // detect care PPIs + for ( f = 0; f < nFrames; f++ ) + { + for ( i = nPis; i < pCexCare->nPis; i++ ) + if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) ) + { + if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted + Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++; + } + } + Abc_CexFree( pCexCare ); + if ( nFfRefined == 0 ) // no refinement -- this is a real CEX + return Pdr_ManDeriveCex(p); + printf( "CEX-based refinement refined %d flops.\n", nFfRefined ); + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 0bcb6e0c..1cff03c7 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -440,7 +440,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) + if ( Vec_IntEntry(vPrio, Entry) ) continue; Vec_IntClear( vUndo ); if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) @@ -454,7 +454,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) + if ( !Vec_IntEntry(vPrio, Entry) ) continue; Vec_IntClear( vUndo ); if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) @@ -473,7 +473,39 @@ 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, k = 0, fAllNegs = 1; + 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; + } + } + } + } 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) ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 7820ebe6..a3f353c2 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -164,7 +164,8 @@ extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars ); /*=== bmcCexCare.c ==========================================================*/ extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); -extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index 9c0a30d3..cc3e85ea 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -251,9 +251,9 @@ Abc_Cex_t * Bmc_CexCareTotal( Abc_Cex_t ** pCexes, int nCexes ) } return pCexMin; } -Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose ) +Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ) { - int nTryCexes = 4; // belongs to range [1;4] + //int nTryCexes = 4; // belongs to range [1;4] Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL}; int k, f, i, nOnesBest, nOnesCur, Counter = 0; Vec_Int_t * vPriosIn, * vPriosFf; @@ -278,7 +278,7 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, if ( fVerbose ) { printf( "Original : " ); - Bmc_CexPrint( pCex, Gia_ManPiNum(p) - nPPis, 0 ); + Bmc_CexPrint( pCex, nRealPis, 0 ); } vPriosIn = Vec_IntAlloc( pCex->nPis * (pCex->iFrame + 1) ); vPriosFf = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) ); @@ -290,37 +290,37 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, if ( k == 0 ) { for ( f = 0; f <= pCex->iFrame; f++ ) - for ( i = nPPis; i < Gia_ManPiNum(p); i++ ) + for ( i = nRealPis; i < Gia_ManPiNum(p); i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = 0; f <= pCex->iFrame; f++ ) - for ( i = 0; i < nPPis; i++ ) + for ( i = 0; i < nRealPis; i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 1 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis; i < Gia_ManPiNum(p); i++ ) + for ( i = nRealPis; i < Gia_ManPiNum(p); i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = 0; i < nPPis; i++ ) + for ( i = 0; i < nRealPis; i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 2 ) { for ( f = 0; f <= pCex->iFrame; f++ ) - for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- ) + for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = 0; f <= pCex->iFrame; f++ ) - for ( i = nPPis - 1; i >= 0; i-- ) + for ( i = nRealPis - 1; i >= 0; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 3 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- ) + for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis - 1; i >= 0; i-- ) + for ( i = nRealPis - 1; i >= 0; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else assert( 0 ); @@ -328,37 +328,37 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, if ( k == 0 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis; i < Gia_ManPiNum(p); i++ ) + for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = 0; i < nPPis; i++ ) + for ( i = nRealPis - 1; i >= 0; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 1 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis; i < Gia_ManPiNum(p); i++ ) + for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis - 1; i >= 0; i-- ) + for ( i = 0; i < nRealPis; i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 2 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- ) + for ( i = nRealPis; i < Gia_ManPiNum(p); i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = 0; i < nPPis; i++ ) + for ( i = nRealPis - 1; i >= 0; i-- ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else if ( k == 3 ) { for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- ) + for ( i = nRealPis; i < Gia_ManPiNum(p); i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); for ( f = pCex->iFrame; f >= 0; f-- ) - for ( i = nPPis - 1; i >= 0; i-- ) + for ( i = 0; i < nRealPis; i++ ) Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) ); } else assert( 0 ); @@ -377,15 +377,15 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, if ( fVerbose ) { if ( k == 0 ) - printf( "PiUp FrUp: " ); + printf( "PI- PPI-: " ); else if ( k == 1 ) - printf( "PiUp FrDn: " ); + printf( "PI+ PPI-: " ); else if ( k == 2 ) - printf( "PiDn FrUp: " ); + printf( "PI- PPI+: " ); else if ( k == 3 ) - printf( "PiDn FrDn: " ); + printf( "PI+ PPI+: " ); else assert( 0 ); - Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p) - nPPis, 0 ); + Bmc_CexPrint( pCexMin[k], nRealPis, 0 ); } } Vec_IntFree( vPriosIn ); @@ -395,6 +395,8 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, nOnesBest = Abc_CexCountOnes(pCexMin[0]); for ( k = 1; k < nTryCexes; k++ ) { + if ( pCexMin[k] == NULL ) + continue; nOnesCur = Abc_CexCountOnes(pCexMin[k]); if ( nOnesBest > nOnesCur ) { @@ -406,13 +408,13 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, { //Abc_Cex_t * pTotal = Bmc_CexCareTotal( pCexMin, nTryCexes ); printf( "Final : " ); - Bmc_CexPrint( pCexBest, Gia_ManPiNum(p) - nPPis, 0 ); + Bmc_CexPrint( pCexBest, nRealPis, 0 ); //printf( "Total : " ); - //Bmc_CexPrint( pTotal, Gia_ManPiNum(p) - nPPis, 0 ); + //Bmc_CexPrint( pTotal, nRealPis, 0 ); //Abc_CexFreeP( &pTotal ); } for ( k = 0; k < nTryCexes; k++ ) - if ( pCexBest != pCexMin[k] ) + if ( pCexMin[k] && pCexBest != pCexMin[k] ) Abc_CexFreeP( &pCexMin[k] ); // verify and return if ( !Bmc_CexVerify( p, pCex, pCexBest ) ) @@ -421,10 +423,10 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, printf( "Counter-example verification succeeded.\n" ); return pCexBest; } -Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose ) +Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ) { Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); - Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nPPis, pCex, fCheck, fVerbose ); + Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, nTryCexes, fCheck, fVerbose ); Gia_ManStop( pGia ); return pCexMin; } @@ -459,7 +461,7 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in /* { Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, pAbc->pCex, 1, 1 ); + Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, 4, pAbc->pCex, 1, 1 ); Aig_ManStop( pAig ); Abc_CexFree( pCex ); } -- cgit v1.2.3