luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix in equivalence class handling (another try).

This commit is contained in:
Alan Mishchenko 2023-05-17 10:34:14 -07:00
parent 3d35624be6
commit 5a9a902044
3 changed files with 24 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/proof/cec/cecChoice.c
View File

@ -412,33 +412,11 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
SeeAlso []
***********************************************************************/
void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
{
int i, iObj, iPrev, Counter = 0;
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
{
Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
}
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose );
Aig_Man_t * pAig;
Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
Gia_ManRemoveWrongChoices( pGia );
pGia = Gia_ManEquivToChoices( pGia, 3 );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
@ -450,7 +428,6 @@ Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose )
Aig_Man_t * pAig;
Gia_Man_t * pNew = Cec5_ManSimulateTest3( pGia, nConfs, fVerbose );
Gia_ManStop( pNew );
Gia_ManRemoveWrongChoices( pGia );
pGia = Gia_ManEquivToChoices( pGia, 3 );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );

25
src/proof/cec/cecSatG2.c
View File

@ -1729,6 +1729,27 @@ Gia_Obj_t * Cec4_ManFindRepr( Gia_Man_t * p, Cec4_Man_t * pMan, int iObj )
pMan->timeResimLoc += Abc_Clock() - clk;
return NULL;
}
void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
{
int i, iObj, iPrev, Counter = 0;
Gia_ManForEachClass( p, i )
{
for ( iPrev = i, iObj = Gia_ObjNext(p, i); -1 < iObj; iObj = Gia_ObjNext(p, iPrev) )
{
Gia_Obj_t * pRepr = Gia_ObjReprObj(p, iObj);
if( !Gia_ObjFailed(p,iObj) && Abc_Lit2Var(Gia_ManObj(p,iObj)->Value) == Abc_Lit2Var(pRepr->Value) )
{
iPrev = iObj;
continue;
}
Gia_ObjSetRepr( p, iObj, GIA_VOID );
Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
Gia_ObjSetNext( p, iObj, 0 );
Counter++;
}
}
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
{
Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars );
@ -1862,13 +1883,11 @@ finalize:
pMan->nSatUndec,
pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
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_ManEquivPrintClasses( p, 1, 0 );
if ( ppNew && *ppNew == NULL )
*ppNew = Gia_ManDup(p);
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )

2
src/proof/cec/cecSatG3.c
View File

@ -1871,6 +1871,7 @@ void Cec5_ManExtend( Cec5_Man_t * pMan, CbsP_Man_t * pCbs ){
int Cec5_ManSweepNodeCbs( Cec5_Man_t * p, CbsP_Man_t * pCbs, int iObj, int iRepr, int fTagFail );
int Cec5_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly, int fCbs, int approxLim, int subBatchSz, int adaRecycle )
{
extern void Gia_ManRemoveWrongChoices( Gia_Man_t * p );
Gia_Obj_t * pObj, * pRepr;
CbsP_Man_t * pCbs = NULL;
int i, fSimulate = 1;
@ -2119,6 +2120,7 @@ finalize:
CbsP_ManStop(pCbs);
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );
Gia_ManRemoveWrongChoices( p );
return p->pCexSeq ? 0 : 1;
}
Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle )