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

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 );