diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
| commit | ae4b51351c93983a1285ce1028e3bbd90a6d5721 (patch) | |
| tree | b06797a1771bb1c79124f2ac7d57f1a54c9afc34 /src/aig/mfx/mfxResub.c | |
| parent | f4066b5be3b5473f5c64ab71d1983df6ca7aec76 (diff) | |
| download | abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.gz abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.bz2 abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.zip | |
Cumulative changes in the last few weeks.
Diffstat (limited to 'src/aig/mfx/mfxResub.c')
| -rw-r--r-- | src/aig/mfx/mfxResub.c | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c index 83673661..5a4786d6 100644 --- a/src/aig/mfx/mfxResub.c +++ b/src/aig/mfx/mfxResub.c @@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands ) } p->nSatCexes++; // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! @@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -244,7 +244,7 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 ); if ( RetValue == -1 ) return 0; @@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -390,8 +390,8 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); - pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 ); if ( RetValue == -1 ) return 0; |