diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 18:53:39 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-10 18:53:39 -0800 |
commit | dd96bb7477fc568ef8fc8d86d330af22c8fa2f26 (patch) | |
tree | 33744ec4f77423b3d117fd0788bd9062583f6365 /src/proof/pdr/pdrTsim.c | |
parent | 5d717256d3b856d8f29c4a5e442af624f0b0bb69 (diff) | |
download | abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.gz abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.tar.bz2 abc-dd96bb7477fc568ef8fc8d86d330af22c8fa2f26.zip |
Adding PDR with abstraction.
Diffstat (limited to 'src/proof/pdr/pdrTsim.c')
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 1cff03c7..283a0e1d 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -476,7 +476,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); // move abstracted literals from flops to inputs if ( p->pPars->fUseAbs && p->vAbsFlops ) { - int i, iLit, k = 0, fAllNegs = 1; + int i, iLit, Used, k = 0, fAllNegs = 1; Vec_IntForEachEntry( vRes, iLit, i ) { if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop @@ -501,6 +501,21 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); 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 ); |