summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaAbsGla2.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/gia/giaAbsGla2.c')
-rw-r--r--src/aig/gia/giaAbsGla2.c11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index afcce09b..6910f334 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -396,7 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
Vec_IntPush( p->vAbs, 0 );
// refinement
p->pRnm = Rnm_ManStart( pGia );
-// p->pRf2 = Rf2_ManStart( pGia );
+ p->pRf2 = Rf2_ManStart( pGia );
// SAT solver and variables
p->vId2Lit = Vec_PtrAlloc( 1000 );
// temporaries
@@ -459,7 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
Vec_IntFree( p->vLits );
Vec_IntFree( p->vIsopMem );
Rnm_ManStop( p->pRnm, p->pPars->fVerbose );
-// Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
+ Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
ABC_FREE( p->pTable );
ABC_FREE( p->pSopSizes );
ABC_FREE( p->pSops[1] );
@@ -1216,7 +1216,7 @@ Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
}
return pCex;
-}
+}
Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
{
Abc_Cex_t * pCex;
@@ -1224,8 +1224,11 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
Gia_Obj_t * pObj;
int i;
Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
- vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
+
// Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
+ vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
+// printf( "Refinement %d\n", Vec_IntSize(vVec) );
+
Abc_CexFree( pCex );
if ( Vec_IntSize(vVec) == 0 )
{