Restructured the code to post-process object used during refinement in &gla.

10 files changed, 343 insertions, 311 deletions

diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h
index e7ab9e7d..11eda38c 100644
--- a/src/proof/abs/abs.h
+++ b/src/proof/abs/abs.h
@@ -61,6 +61,7 @@ struct Abs_Par_t_
     int                  fUseRollback;       // use rollback to the starting number of frames
     int                  fPropFanout;        // propagate fanout implications
     int                  fAddLayer;          // refinement strategy by adding layers
+    int                  fNewRefine;         // uses new refinement heuristics
     int                  fUseSkip;           // skip proving intermediate timeframes
     int                  fUseSimple;         // use simple CNF construction
     int                  fSkipHash;          // skip hashing CNF while unrolling
@@ -81,6 +82,13 @@ struct Abs_Par_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )          { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                         }
+static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                     }
+static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                                }
+static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )           { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);            }
+static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )          { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);            }
+static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )          { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;       }
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -114,6 +122,7 @@ extern Vec_Int_t *       Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
 extern int               Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
 extern int               Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
 
+
 /*=== absOldCex.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
 extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c
index 247137bd..94215575 100644
--- a/src/proof/abs/absDup.c
+++ b/src/proof/abs/absDup.c
@@ -53,7 +53,7 @@ void Gia_ManDupAbsFlops_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs abstraction of the AIG to preserve the included flops.]
+  Synopsis    [Extractes a flop-level abstraction given a flop map.]
 
   Description []
                
@@ -207,7 +207,7 @@ void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs abstraction of the AIG to preserve the included gates.]
+  Synopsis    [Extractes a gate-level abstraction given a gate map.]
 
   Description [The array contains 1 for those objects (const, RO, AND)
   that are included in the abstraction; 0, otherwise.]
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 76b6c231..260a649c 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -78,13 +78,6 @@ struct Ga2_Man_t_
     clock_t        timeOther;
 };
 
-static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )       { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                    }
-static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                }
-static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                           }
-static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )        { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);       }
-static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )       { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);       }
-static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )       { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;  }
-
 static inline int         Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj )           { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj));                                                  }
 static inline void        Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i);                                                 }
 
@@ -1329,7 +1322,7 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
     }
     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, 1 );
+    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
 //    printf( "Refinement %d\n", Vec_IntSize(vVec) );
     Abc_CexFree( pCex );
     if ( Vec_IntSize(vVec) == 0 )
@@ -1644,6 +1637,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
 
                     // perform refinement
                     clk2 = clock();
+                    Rnm_ManSetRefId( p->pRnm, c );
                     vPPis = Ga2_ManRefine( p );
                     p->timeCex += clock() - clk2;
                     if ( vPPis == NULL )
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 5ee69739..4ab956f7 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -503,7 +503,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, 0, 1 );
+    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
     Abc_CexFree( pCex );
     if ( Vec_IntSize(vVec) == 0 )
     {
diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c
index 3aea96ee..64e1f55c 100644
--- a/src/proof/abs/absRef.c
+++ b/src/proof/abs/absRef.c
@@ -73,80 +73,20 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
-struct Rnm_Obj_t_
-{
-    unsigned       Value     :  1;  // binary value
-    unsigned       fVisit    :  1;  // visited object
-    unsigned       fVisit0   :  1;  // visited object
-    unsigned       fPPi      :  1;  // PPI object
-    unsigned       Prio      : 24;  // priority (0 - highest)
-};
-
-struct Rnm_Man_t_
-{
-    // user data
-    Gia_Man_t *    pGia;            // working AIG manager (it is completely owned by this package)
-    Abc_Cex_t *    pCex;            // counter-example
-    Vec_Int_t *    vMap;            // mapping of CEX inputs into objects (PI + PPI, in any order)
-    int            fPropFanout;     // propagate fanouts
-    int            fVerbose;        // verbose flag
-    // traversing data
-    Vec_Int_t *    vObjs;           // internal objects used in value propagation
-    Vec_Str_t *    vCounts;         // fanin counters
-    Vec_Int_t *    vFanins;         // fanins
-    // SAT solver
-    sat_solver2 *  pSat;            // incremental SAT solver
-    Vec_Int_t *    vSatVars;        // SAT variables
-    Vec_Int_t *    vSat2Ids;        // mapping of SAT variables into object IDs
-    Vec_Int_t *    vIsopMem;        // memory for ISOP computation
-    // internal data
-    Rnm_Obj_t *    pObjs;           // refinement objects
-    int            nObjs;           // the number of used objects
-    int            nObjsAlloc;      // the number of allocated objects
-    int            nObjsFrame;      // the number of used objects in each frame
-    int            nCalls;          // total number of calls
-    int            nRefines;        // total refined objects
-    int            nVisited;        // visited during justification
-    // statistics  
-    clock_t        timeFwd;         // forward propagation
-    clock_t        timeBwd;         // backward propagation
-    clock_t        timeVer;         // ternary simulation
-    clock_t        timeTotal;       // other time
-};
-
-// accessing the refinement object
-static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )  
-{ 
-    assert( Gia_ObjIsConst0(pObj) || pObj->Value );
-    assert( (int)pObj->Value < p->nObjsFrame );
-    assert( f >= 0 && f <= p->pCex->iFrame ); 
-    return p->pObjs + f * p->nObjsFrame + pObj->Value;  
-}
-
-static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )          { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                         }
-static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                     }
-static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                                }
-static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )           { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);            }
-static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )          { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);            }
-static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )          { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;       }
-
-static inline int         Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj )           { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) );                                                  }
-static inline void        Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c );                                           }
-static inline int         Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj )      { int c = Rnm_ObjCount(p, pObj); if ( c < 16 )  Rnm_ObjSetCount(p, pObj, c+1); return c;                        }
-
+/*
 static inline int         Rnm_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj )          { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) );                                                 }
 static inline void        Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c );                                                }
 static inline int         Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj)  { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); }
-
+*/
 extern void               Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId );
-
 extern Vec_Int_t *        Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0 
+
 /**Function*************************************************************
 
   Synopsis    [Performs UNSAT-core-based refinement.]
@@ -308,6 +248,7 @@ Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs )
     return vCoreFinal;
 }
 
+#endif
 
 /**Function*************************************************************
 
@@ -329,9 +270,9 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
     p->vObjs = Vec_IntAlloc( 100 );
     p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
     p->vFanins = Vec_IntAlloc( 1000 );
-    p->vSatVars = Vec_IntAlloc( 0 );
-    p->vSat2Ids = Vec_IntAlloc( 1000 );
-    p->vIsopMem  = Vec_IntAlloc( 0 );
+//    p->vSatVars = Vec_IntAlloc( 0 );
+//    p->vSat2Ids = Vec_IntAlloc( 1000 );
+//    p->vIsopMem  = Vec_IntAlloc( 0 );
     p->nObjsAlloc = 10000;
     p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
     if ( p->pGia->vFanout == NULL )
@@ -364,9 +305,9 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
     Gia_ManCleanMark1(p->pGia);
     Gia_ManStaticFanoutStop(p->pGia);
 //    Gia_ManSetPhase(p->pGia);
-    Vec_IntFree( p->vIsopMem );
-    Vec_IntFree( p->vSatVars );
-    Vec_IntFree( p->vSat2Ids );
+//    Vec_IntFree( p->vIsopMem );
+//    Vec_IntFree( p->vSatVars );
+//    Vec_IntFree( p->vSat2Ids );
     Vec_StrFree( p->vCounts );
     Vec_IntFree( p->vFanins );
     Vec_IntFree( p->vObjs );
@@ -533,9 +474,9 @@ void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_I
     int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
     assert( pRnm->fVisit == 0 );
     pRnm->fVisit = 1;
-    if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
+    if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
     {
-        Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+        Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
         p->nVisited++;
     }
     if ( pRnm->fPPi )
@@ -591,9 +532,9 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe
     else
     {
         pRnm->fVisit = 1;
-        if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
+        if ( Rnm_ManObj( p, pObj, 0 )->fVisitJ == 0 )
         {
-            Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+            Rnm_ManObj( p, pObj, 0 )->fVisitJ = 1;
             p->nVisited++;
         }
     }
@@ -720,177 +661,6 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap
 
 /**Function*************************************************************
 
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vSelected )
-{
-    Gia_Obj_t * pObj;
-    int i, Counter = 0;
-    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
-    {
-        if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
-        {
-            if ( Vec_IntFind(vSelected, Gia_ObjId(p->pGia, pObj)) >= 0 )
-                printf( "1" ), Counter++;
-            else
-                printf( "0" );
-        }
-        else
-            printf( "-" );
-    }
-    printf( " %3d\n", Counter );
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Perform structural analysis.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vSelect )
-{
-    Vec_Int_t * vLeaves;
-    Gia_Obj_t * pObj, * pFanin;
-    int i, k;
-    // clean labels
-    Gia_ManForEachObj( p, pObj, i )
-        pObj->fMark0 = pObj->fMark1 = 0;
-    // label frontier
-    Gia_ManForEachObjVec( vFront, p, pObj, i )
-        pObj->fMark0 = 1, pObj->fMark1 = 0;
-    // label objects
-    Gia_ManForEachObjVec( vInter, p, pObj, i )
-        pObj->fMark1 = 0, pObj->fMark1 = 1;
-    // label selected
-    Gia_ManForEachObjVec( vSelect, p, pObj, i )
-        pObj->fMark1 = 1, pObj->fMark1 = 1;
-    // explore selected
-    printf( "\n" );
-    Gia_ManForEachObjVec( vSelect, p, pObj, i )
-    {
-        printf( "Selected %6d : ", Gia_ObjId(p, pObj) );
-        printf( "\n" );
-        vLeaves = Ga2_ObjLeaves( p, pObj );
-        Gia_ManForEachObjVec( vLeaves, p, pFanin, k )
-        {
-            printf( "    " );
-            printf( "%6d ", Gia_ObjId(p, pFanin) );
-            if ( pFanin->fMark0 && pFanin->fMark1 )
-                printf( "select" );
-            else if ( pFanin->fMark0 && !pFanin->fMark1 )
-                printf( "front" );
-            else if ( !pFanin->fMark0 &&  pFanin->fMark1 )
-                printf( "internal" );
-            else if ( !pFanin->fMark0 && !pFanin->fMark1 )
-                printf( "new" );
-            printf( "\n" );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Finds essential objects.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect )
-{
-    Vec_Int_t * vNew, * vLeaves;
-    Gia_Obj_t * pObj, * pFanin;
-    int i, k, RetValue;//, Counters[3] = {0};
-/*
-    // check that selected are not visited
-    Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
-        assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 1 );
-    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
-        if ( Vec_IntFind(vSelect, Gia_ObjId(p->pGia, pObj)) == -1 )
-            assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 );
-*/
-
-    // verify
-//    Gia_ManForEachObj( p->pGia, pObj, i )
-//        assert( Rnm_ObjCount(p, pObj) == 0 );
-
-    // increment fanin counters
-    Vec_IntClear( p->vFanins );
-    Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
-    {
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-            if ( Rnm_ObjAddToCount(p, pFanin) == 0 )
-                Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
-    }
-
-    // find selected objects, which create potential constraints
-    // - flop objects
-    // - objects whose fanin belongs to the justified area
-    // - objects whose fanins overlap
-    // (these do not guantee reconvergence, but may potentially have it)
-    // (other objects cannot have reconvergence, even if they are added)
-    vNew = Vec_IntAlloc( 100 );
-    Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
-    {
-        if ( Gia_ObjIsRo(p->pGia, pObj) )
-        {
-            Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
-            continue;
-        }
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-        {
-            if ( Gia_ObjIsConst0(pFanin)
-                 || (pFanin->Value && Rnm_ManObj(p, pFanin, 0)->fVisit0 == 1)
-                 || Rnm_ObjCount(p, pFanin) > 1
-               )
-            {
-                Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) );
-                break;
-            }
-        }
-//        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-//        {
-//            Counters[1] += (pFanin->Value && Rnm_ManObj( p, pFanin, 0 )->fVisit0 == 1);
-//            Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
-//        }
-    }
-    RetValue = Vec_IntUniqify( vNew );
-    assert( RetValue == 0 );
-
-//    printf( "\n*** Select = %5d. New = %5d.   Flops = %5d.  Visited = %5d.  Fanins = %5d.\n", 
-//        Vec_IntSize(vSelect), Vec_IntSize(vNew), Counters[0], Counters[1], Counters[2] );
-
-    // clear fanin counters
-    Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
-        Rnm_ObjSetCount( p, pObj, 0 );
-    return vNew;
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Computes the refinement for a given counter-example.]
 
   Description []
@@ -900,12 +670,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 fPostProcess, int fVerbose )
+Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose )
 {
     int fVerify = 0;
-//    int fPostProcess = 1;
-    Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
-    Vec_Int_t * vNew;
+    Vec_Int_t * vGoodPPis, * vNewPPis;
     clock_t clk, clk2 = clock();
     int RetValue;
     p->nCalls++;
@@ -925,71 +693,50 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
     memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
     // propagate priorities
     clk = clock();
+    vGoodPPis = Vec_IntAlloc( 100 );
     if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
     {
         p->timeFwd += clock() - clk;
         // select refinement
         clk = clock();
         p->nVisited = 0;
-        Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected );
-        RetValue = Vec_IntUniqify( vSelected );
+        Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vGoodPPis );
+        RetValue = Vec_IntUniqify( vGoodPPis );
 //        assert( RetValue == 0 );
         p->timeBwd += clock() - clk;
     }
-
-    if ( fPostProcess )
-    {
-        vNew = Ga2_FilterSelected( p, vSelected );
-        if ( Vec_IntSize(vNew) > 0 )
-        {
-            Vec_IntFree( vSelected );
-            vSelected = vNew;
-        }
-        else
-        {
-            Vec_IntFree( vNew );
-    //        printf( "\nBig refinement.\n" );
-        }
-    }
-    else
+    // at this point array vGoodPPis contains the set of important PPIs
+    if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement 
     {
-/*
-        vNew = Rnm_ManRefineUnsatCore( p, vSelected );
-        if ( Vec_IntSize(vNew) > 0 )
-        {
-            Vec_IntFree( vSelected );
-            vSelected = vNew;
-//            Vec_IntFree( vNew );
-        }
-        else
-        {
-            Vec_IntFree( vNew );
-    //        printf( "\nBig refinement.\n" );
-        }
-*/
+        // filter selected set
+        if ( !fNewRefinement )  // default 
+            vNewPPis = Rnm_ManFilterSelected( p, vGoodPPis );
+        else // this is enabled when &gla is called with -r (&gla -r)
+            vNewPPis = Rnm_ManFilterSelectedNew( p, vGoodPPis );
+
+        // replace the PPI array if necessary
+        if ( Vec_IntSize(vNewPPis) > 0 ) // something to select, replace current refinement 
+            Vec_IntFree( vGoodPPis ), vGoodPPis = vNewPPis;
+        else // if there is nothing to select, do not change the current refinement array
+            Vec_IntFree( vNewPPis );
     }
 
     // clean values
     Rnm_ManCleanValues( p );
 
     // verify (empty) refinement
+    // (only works when post-processing is not applied)
     if ( fVerify )
     {
         clk = clock();
-        Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
+        Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vGoodPPis );
         p->timeVer += clock() - clk;
     }
 
-//    printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) );
-//    Rnm_ManPrintSelected( p, vSelected );
-        
-//    Ga2_StructAnalize( p->pGia, vMap, p->vObjs, vSelected );
-//    printf( "\nObjects = %5d.  Visited = %5d.\n", Vec_IntSize(p->vObjs), p->nVisited );
-
-//    Vec_IntReverseOrder( vSelected );
+//    Vec_IntReverseOrder( vGoodPPis );
     p->timeTotal += clock() - clk2;
-    p->nRefines += Vec_IntSize(vSelected);
-    return vSelected;
+    p->nRefines += Vec_IntSize(vGoodPPis);
+    return vGoodPPis;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absRef.h b/src/proof/abs/absRef.h
index ca46c776..9bae40a3 100644
--- a/src/proof/abs/absRef.h
+++ b/src/proof/abs/absRef.h
@@ -37,28 +37,90 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
+struct Rnm_Obj_t_
+{
+    unsigned        Value     :  1;  // binary value
+    unsigned        fVisit    :  1;  // visited object
+    unsigned        fVisitJ   :  1;  // justified visited object
+    unsigned        fPPi      :  1;  // PPI object
+    unsigned        Prio      : 24;  // priority (0 - highest)
+};
+
+typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
+struct Rnm_Man_t_
+{
+    // user data
+    Gia_Man_t *     pGia;            // working AIG manager (it is completely owned by this package)
+    Abc_Cex_t *     pCex;            // counter-example
+    Vec_Int_t *     vMap;            // mapping of CEX inputs into objects (PI + PPI, in any order)
+    int             fPropFanout;     // propagate fanouts
+    int             fVerbose;        // verbose flag
+    int             nRefId;          // refinement ID
+    // traversing data
+    Vec_Int_t *     vObjs;           // internal objects used in value propagation
+    // filtering of selected objects
+    Vec_Str_t *     vCounts;         // fanin counters
+    Vec_Int_t *     vFanins;         // fanins
+/*
+    // SAT solver
+    sat_solver2 *   pSat;            // incremental SAT solver
+    Vec_Int_t *     vSatVars;        // SAT variables
+    Vec_Int_t *     vSat2Ids;        // mapping of SAT variables into object IDs
+    Vec_Int_t *     vIsopMem;        // memory for ISOP computation
+*/
+    // internal data
+    Rnm_Obj_t *     pObjs;           // refinement objects
+    int             nObjs;           // the number of used objects
+    int             nObjsAlloc;      // the number of allocated objects
+    int             nObjsFrame;      // the number of used objects in each frame
+    int             nCalls;          // total number of calls
+    int             nRefines;        // total refined objects
+    int             nVisited;        // visited during justification
+    // statistics  
+    clock_t         timeFwd;         // forward propagation
+    clock_t         timeBwd;         // backward propagation
+    clock_t         timeVer;         // ternary simulation
+    clock_t         timeTotal;       // other time
+};
+
+// accessing the refinement object
+static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )  
+{ 
+    assert( Gia_ObjIsConst0(pObj) || pObj->Value );
+    assert( (int)pObj->Value < p->nObjsFrame );
+    assert( f >= 0 && f <= p->pCex->iFrame ); 
+    return p->pObjs + f * p->nObjsFrame + pObj->Value;  
+}
+static inline void  Rnm_ManSetRefId( Rnm_Man_t * p, int RefId )               { p->nRefId = RefId; }
+
+static inline int   Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj )           { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) );                           }
+static inline void  Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c );                    }
+static inline int   Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj )      { int c = Rnm_ObjCount(p, pObj); if ( c < 16 )  Rnm_ObjSetCount(p, pObj, c+1); return c; }
+
+static inline int   Rnm_ObjIsJust( Rnm_Man_t * p, Gia_Obj_t * pObj )          { return Gia_ObjIsConst0(pObj) || (pObj->Value && Rnm_ManObj(p, pObj, 0)->fVisitJ);      }
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== giaAbsRef.c ===========================================================*/
+/*=== absRef.c ===========================================================*/
 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 fPostProcess, int fVerbose );
-
+extern Vec_Int_t *  Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose );
+/*=== absRefSelected.c ===========================================================*/
+extern Vec_Int_t *  Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
+extern Vec_Int_t *  Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
 
 
 ABC_NAMESPACE_HEADER_END
 
-
-
 #endif
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absRef2.c b/src/proof/abs/absRefJ.c
index 7fb26e5a..aa5ea7bb 100644
--- a/src/proof/abs/absRef2.c
+++ b/src/proof/abs/absRefJ.c
@@ -6,7 +6,7 @@
 
   PackageName [Abstraction package.]
 
-  Synopsis    [Refinement manager.]
+  Synopsis    [Refinement manager to compute all justifying subsets.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/proof/abs/absRef2.h b/src/proof/abs/absRefJ.h
index df7774c0..0c56d2dd 100644
--- a/src/proof/abs/absRef2.h
+++ b/src/proof/abs/absRefJ.h
@@ -6,7 +6,7 @@
 
   PackageName [Abstraction package.]
 
-  Synopsis    [Refinement manager.]
+  Synopsis    [Refinement manager to compute all justifying subsets.]
 
   Author      [Alan Mishchenko]
   
diff --git a/src/proof/abs/absRefSelect.c b/src/proof/abs/absRefSelect.c
new file mode 100644
index 00000000..871eb79b
--- /dev/null
+++ b/src/proof/abs/absRefSelect.c
@@ -0,0 +1,220 @@
+/**CFile****************************************************************
+
+  FileName    [absRefSelect.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Abstraction package.]
+
+  Synopsis    [Post-processes the set of selected refinement objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: absRefSelect.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#include "abs.h"
+#include "absRef.h"
+
+ABC_NAMESPACE_IMPL_START 
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        if ( Gia_ObjIsPi(p->pGia, pObj) ) 
+            printf( "-" );
+        else if ( Vec_IntFind(vNewPPis, Gia_ObjId(p->pGia, pObj)) >= 0 )// this is PPI
+            printf( "1" ), Counter++;
+        else
+            printf( "0" );
+    printf( " %3d\n", Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform structural analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
+{
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k;
+    // clean labels
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = pObj->fMark1 = 0;
+    // label frontier
+    Gia_ManForEachObjVec( vFront, p, pObj, i )
+        pObj->fMark0 = 1, pObj->fMark1 = 0;
+    // label objects
+    Gia_ManForEachObjVec( vInter, p, pObj, i )
+        pObj->fMark1 = 0, pObj->fMark1 = 1;
+    // label selected
+    Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
+        pObj->fMark1 = 1, pObj->fMark1 = 1;
+    // explore selected
+    Gia_ManForEachObjVec( vNewPPis, p, pObj, i )
+    {
+        printf( "Selected PPI %3d : ", i+1 );
+        printf( "%6d ",  Gia_ObjId(p, pObj) );
+        printf( "\n" );
+        vLeaves = Ga2_ObjLeaves( p, pObj );
+        Gia_ManForEachObjVec( vLeaves, p, pFanin, k )
+        {
+            printf( "    " );
+            printf( "%6d ", Gia_ObjId(p, pFanin) );
+            if ( pFanin->fMark0 && pFanin->fMark1 )
+                printf( "selected PPI" );
+            else if ( pFanin->fMark0 && !pFanin->fMark1 )
+                printf( "frontier (original PI or PPI)" );
+            else if ( !pFanin->fMark0 &&  pFanin->fMark1 )
+                printf( "abstracted node" );
+            else if ( !pFanin->fMark0 && !pFanin->fMark1 )
+                printf( "free variable" );
+            printf( "\n" );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Postprocessing the set of PPIs using structural analysis.]
+
+  Description [The following sets are used:
+  The set of all PI+PPI is in p->vMap.
+  The set of all abstracted objects is in p->vObjs;
+  The set of important PPIs is in vOldPPis.
+  The new set of selected PPIs is in vNewPPis.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
+{
+   int fVerbose = 0;
+    Vec_Int_t * vNewPPis, * vLeaves;
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k, RetValue, Counters[3] = {0};
+
+    // (0) make sure fanin counters are 0 at the beginning
+//    Gia_ManForEachObj( p->pGia, pObj, i )
+//        assert( Rnm_ObjCount(p, pObj) == 0 );
+
+    // (1) increment PPI fanin counters
+    Vec_IntClear( p->vFanins );
+    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
+    {
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+            if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) // fanin counter is 0 -- save it
+                Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
+    }
+
+    // (3) select objects with reconvergence, which create potential constraints
+    // - flop objects
+    // - objects whose fanin belongs to the justified area
+    // - objects whose fanins overlap
+    // (these do not guantee reconvergence, but may potentially have it)
+    // (other objects cannot have reconvergence, even if they are added)
+    vNewPPis = Vec_IntAlloc( 100 );
+    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
+    {
+        if ( Gia_ObjIsRo(p->pGia, pObj) )
+        {
+            if ( fVerbose )
+                Counters[0]++;
+            Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+            continue;
+        }
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+        {
+            if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
+            {
+                if ( fVerbose )
+                    Counters[1] += Rnm_ObjIsJust(p, pFanin);
+                if ( fVerbose )
+                    Counters[2] += (Rnm_ObjCount(p, pFanin) > 1);
+                Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+                break;
+            }
+        }
+    }
+    RetValue = Vec_IntUniqify( vNewPPis );
+    assert( RetValue == 0 );
+
+    // (4) clear fanin counters
+    // this is important for counters to be correctly set in the future iterations -- see step (0)
+    Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
+        Rnm_ObjSetCount( p, pObj, 0 );
+
+    // visualize
+    if ( fVerbose )
+        printf( "*** Refinement %3d : PI+PPI =%4d. Old =%4d. New =%4d.   FF =%4d. Just =%4d. Shared =%4d.\n", 
+            p->nRefId, Vec_IntSize(p->vMap), Vec_IntSize(vOldPPis), Vec_IntSize(vNewPPis), Counters[0], Counters[1], Counters[2] );
+
+//    Rnm_ManPrintSelected( p, vNewPPis );
+//    Ga2_StructAnalize( p->pGia, p->vMap, p->vObjs, vNewPPis );
+    return vNewPPis;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Improved postprocessing the set of PPIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
+{
+    Vec_Int_t * vNewPPis;
+    vNewPPis = Vec_IntDup( vOldPPis );
+    return vNewPPis;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/abs/module.make b/src/proof/abs/module.make
index 4e652afd..4dd463e2 100644
--- a/src/proof/abs/module.make
+++ b/src/proof/abs/module.make
@@ -10,6 +10,6 @@ SRC +=    src/proof/abs/abs.c \
     src/proof/abs/absOut.c \
     src/proof/abs/absPth.c \
     src/proof/abs/absRef.c \
-    src/proof/abs/absRef2.c \
+    src/proof/abs/absRefSelect.c \
     src/proof/abs/absVta.c \
     src/proof/abs/absUtil.c