Skip to content

A
abc
Commit 96e1de43 by Alan Mishchenko
Options

Bug fix in equivalence class handling (another try).

parent bb437893
Showing with 5 additions and 2 deletions
src/aig/gia/giaMini.c
...@@ -769,8 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap ) ...@@ -769,8 +769,8 @@ Vec_Int_t * Gia_ManMapEquivAfterScorr( Gia_Man_t * p, Vec_Int_t * vMap )
{ {
if ( iObjLit == -1 ) if ( iObjLit == -1 )
continue; continue;
if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) ) // if ( Gia_ObjHasRepr(p, Abc_Lit2Var(iObjLit)) && !Gia_ObjProved(p, Abc_Lit2Var(iObjLit)) )
continue; // continue;
iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) ); iReprGia = Gia_ObjReprSelf( p, Abc_Lit2Var(iObjLit) );
iReprMini = Vec_IntEntry( vGia2Mini, iReprGia ); iReprMini = Vec_IntEntry( vGia2Mini, iReprGia );
if ( iReprMini == -1 ) if ( iReprMini == -1 )
......
src/proof/cec/cecSatG2.c
...@@ -1862,6 +1862,9 @@ finalize: ...@@ -1862,6 +1862,9 @@ finalize:
pMan->nSatUndec, pMan->nSatUndec,
pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) ); pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
Cec4_ManDestroy( pMan ); Cec4_ManDestroy( pMan );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjHasRepr(p, i) && !Gia_ObjProved(p, i) )
Gia_ObjSetRepr(p, i, GIA_VOID);
//Gia_ManStaticFanoutStop( p ); //Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 ); //Gia_ManEquivPrintClasses( p, 1, 0 );
if ( ppNew && *ppNew == NULL ) if ( ppNew && *ppNew == NULL )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment