diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-21 16:40:56 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-21 16:40:56 -0700 |
| commit | bfe7333f4105442a7df530c68ed1cf1b7da7edda (patch) | |
| tree | 295068e63d3e63b94e401ebef9ce85c341f5d72a /src/proof/cec/cecSolve.c | |
| parent | aa3d8a65b43d8fb526721b8f40d8296b9c2db7a7 (diff) | |
| download | abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.tar.gz abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.tar.bz2 abc-bfe7333f4105442a7df530c68ed1cf1b7da7edda.zip | |
Adding new command 'dump_equiv'.
Diffstat (limited to 'src/proof/cec/cecSolve.c')
| -rw-r--r-- | src/proof/cec/cecSolve.c | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index e3db0b93..f75914e4 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -673,7 +673,7 @@ p->timeSatUndec += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ -void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) { Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; @@ -706,6 +706,16 @@ clk2 = Abc_Clock(); status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); pObj->fMark0 = (status == 0); pObj->fMark1 = (status == 1); + if ( status == 1 && vIdsOrig ) + { + int iObj1 = Vec_IntEntry(vMiterPairs, 2*i); + int iObj2 = Vec_IntEntry(vMiterPairs, 2*i+1); + int OrigId1 = Vec_IntEntry(vIdsOrig, iObj1); + int OrigId2 = Vec_IntEntry(vIdsOrig, iObj2); + assert( OrigId1 >= 0 && OrigId2 >= 0 ); + Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 ); + } + /* if ( status == -1 ) { |