diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-21 22:20:03 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-21 22:20:03 -0800 |
commit | 53b1d46b8d19e491679d9374c9758b09e2becf59 (patch) | |
tree | ef523172fc357df19b1c9e46b043674c0f48b4ec /src/proof | |
parent | 96ccd24e6e5e2489d165bc14ac81136255a7b1f8 (diff) | |
download | abc-53b1d46b8d19e491679d9374c9758b09e2becf59.tar.gz abc-53b1d46b8d19e491679d9374c9758b09e2becf59.tar.bz2 abc-53b1d46b8d19e491679d9374c9758b09e2becf59.zip |
Remapping flops in '%pdra.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/pdr/pdrIncr.c | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 6de86c18..3fcd3d31 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -190,7 +190,7 @@ sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal ) SeeAlso [] ***********************************************************************/ -int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) +int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap ) { int i; @@ -199,6 +199,15 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) Vec_VecFree(p->vClauses); p->vClauses = vClauses; + // remap clause literals using mapping (old flop -> new flop) found in array vMap + if ( vMap ) + { + Pdr_Set_t * pSet; int j, k; + Vec_VecForEachEntry( Pdr_Set_t *, vClauses, pSet, i, j ) + for ( k = 0; k < pSet->nLits; k++ ) + pSet->Lits[k] = Abc_Lit2LitV( Vec_IntArray(vMap), pSet->Lits[k] ); + } + for ( i = 0; i < Vec_VecSize(p->vClauses); ++i ) IPdr_ManSetSolver( p, i, Vec_VecSize( p->vClauses ) ); @@ -646,7 +655,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) Pdr_ManStop( p ); p = Pdr_ManStart( pAig, pPars, NULL ); - IPdr_ManRestore( p, vClausesSaved ); + IPdr_ManRestore( p, vClausesSaved, NULL ); pPars->nFrameMax = pPars->nFrameMax << 1; |