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

Fixing undesirable effect of recent refinement code on older code in &gla -n.

This commit is contained in:
Alan Mishchenko 2012-08-11 11:47:22 -07:00
parent 528c8e0bba
commit 5da7102f55
4 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaAbsGla.c
View File

@ -712,7 +712,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
Gia_Obj_t * pObj;
int i;
Gia_GlaPrepareCexAndMap( p, &pCex, &vMap );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 0, 1 );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
{

2
src/aig/gia/giaAbsGla2.c
View File

@ -1224,7 +1224,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
int i, k;
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1, 1 );
// printf( "Refinement %d\n", Vec_IntSize(vVec) );
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )

6
src/aig/gia/giaAbsRef.c
View File

@ -900,10 +900,10 @@ Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
SeeAlso []
***********************************************************************/
Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose )
{
int fVerify = 0;
int fPostProcess = 1;
// int fPostProcess = 1;
Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
Vec_Int_t * vNew;
clock_t clk, clk2 = clock();
@ -953,6 +953,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
}
else
{
/*
vNew = Rnm_ManRefineUnsatCore( p, vSelected );
if ( Vec_IntSize(vNew) > 0 )
{
@ -965,6 +966,7 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
Vec_IntFree( vNew );
// printf( "\nBig refinement.\n" );
}
*/
}
// clean values

2
src/aig/gia/giaAbsRef.h
View File

@ -51,7 +51,7 @@ typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
extern Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia );
extern void Rnm_ManStop( Rnm_Man_t * p, int fProfile );
extern double Rnm_ManMemoryUsage( Rnm_Man_t * p );
extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose );
extern Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose );