luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding PDR with abstraction.

This commit is contained in:
Alan Mishchenko 2017-02-10 17:36:20 -08:00
parent fce2b16a60
commit 8bff9aa1cd
9 changed files with 330 additions and 103 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

74
src/aig/gia/giaDup.c
View File

@ -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.]

2
src/base/io/io.c
View File

@ -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)

132
src/proof/pdr/pdrCore.c
View File

@ -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;
}
}

10
src/proof/pdr/pdrInt.h
View File

@ -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 );

1
src/proof/pdr/pdrInv.c
View File

@ -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 );

113
src/proof/pdr/pdrMan.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////

36
src/proof/pdr/pdrTsim.c
View File

@ -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) );

3
src/sat/bmc/bmc.h
View File

@ -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 );

62
src/sat/bmc/bmcCexCare.c
View File

@ -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 );
}