diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsGla.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAbsRef.c | 6 | ||||
-rw-r--r-- | src/aig/gia/giaAbsRef.h | 2 |
4 files changed, 7 insertions, 5 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 160e47e1..508dd218 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -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 ) { diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c index f3fcbbd0..5e1873f0 100644 --- a/src/aig/gia/giaAbsGla2.c +++ b/src/aig/gia/giaAbsGla2.c @@ -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 ) diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c index 473afc92..8a5aedc5 100644 --- a/src/aig/gia/giaAbsRef.c +++ b/src/aig/gia/giaAbsRef.c @@ -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 diff --git a/src/aig/gia/giaAbsRef.h b/src/aig/gia/giaAbsRef.h index 26992dac..e44245be 100644 --- a/src/aig/gia/giaAbsRef.h +++ b/src/aig/gia/giaAbsRef.h @@ -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 ); |