Other improvements to &vta and &gla.

3 files changed, 738 insertions, 80 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b3584f14..e24ecd26 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -515,6 +515,66 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
     return GIA_ONE;
 }
 
+
+static inline void Gia_ObjTerSimSetC( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 0;    }
+static inline void Gia_ObjTerSimSet0( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 0;    }
+static inline void Gia_ObjTerSimSet1( Gia_Obj_t * pObj ) { pObj->fMark0 = 0; pObj->fMark1 = 1;    }
+static inline void Gia_ObjTerSimSetX( Gia_Obj_t * pObj ) { pObj->fMark0 = 1; pObj->fMark1 = 1;    }
+
+static inline int  Gia_ObjTerSimGetC( Gia_Obj_t * pObj ) { return !pObj->fMark0 && !pObj->fMark1; }
+static inline int  Gia_ObjTerSimGet0( Gia_Obj_t * pObj ) { return  pObj->fMark0 && !pObj->fMark1; }
+static inline int  Gia_ObjTerSimGet1( Gia_Obj_t * pObj ) { return !pObj->fMark0 &&  pObj->fMark1; }
+static inline int  Gia_ObjTerSimGetX( Gia_Obj_t * pObj ) { return  pObj->fMark0 &&  pObj->fMark1; }
+
+static inline int  Gia_ObjTerSimGet0Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
+static inline int  Gia_ObjTerSimGet1Fanin0( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj)); }
+
+static inline int  Gia_ObjTerSimGet0Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
+static inline int  Gia_ObjTerSimGet1Fanin1( Gia_Obj_t * pObj ) { return (Gia_ObjTerSimGet0(Gia_ObjFanin1(pObj)) && Gia_ObjFaninC1(pObj)) || (Gia_ObjTerSimGet1(Gia_ObjFanin1(pObj)) && !Gia_ObjFaninC1(pObj)); }
+
+static inline void Gia_ObjTerSimAnd( Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
+    assert( !Gia_ObjTerSimGetC( Gia_ObjFanin1(pObj) ) );
+    if ( Gia_ObjTerSimGet0Fanin0(pObj) || Gia_ObjTerSimGet0Fanin1(pObj) )
+        Gia_ObjTerSimSet0( pObj );
+    else if ( Gia_ObjTerSimGet1Fanin0(pObj) && Gia_ObjTerSimGet1Fanin1(pObj) )
+        Gia_ObjTerSimSet1( pObj );
+    else 
+        Gia_ObjTerSimSetX( pObj );
+}
+static inline void Gia_ObjTerSimCo( Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsCo(pObj) );
+    assert( !Gia_ObjTerSimGetC( Gia_ObjFanin0(pObj) ) );
+    if ( Gia_ObjTerSimGet0Fanin0(pObj) )
+        Gia_ObjTerSimSet0( pObj );
+    else if ( Gia_ObjTerSimGet1Fanin0(pObj) )
+        Gia_ObjTerSimSet1( pObj );
+    else 
+        Gia_ObjTerSimSetX( pObj );
+}
+static inline void Gia_ObjTerSimRo( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pTemp = Gia_ObjRoToRi(p, pObj);
+    assert( Gia_ObjIsRo(p, pObj) );
+    assert( !Gia_ObjTerSimGetC( pTemp ) );
+    pObj->fMark0 = pTemp->fMark0;
+    pObj->fMark1 = pTemp->fMark1;
+}
+
+static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
+{
+    if ( Gia_ObjTerSimGet0(pObj) )
+        printf( "0" );
+    else if ( Gia_ObjTerSimGet1(pObj) )
+        printf( "1" );
+    else if ( Gia_ObjTerSimGetX(pObj) )
+        printf( "X" );
+}
+
+
 static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr );                  }
 static inline int         Gia_ObjRepr( Gia_Man_t * p, int Id )               { return p->pReprs[Id].iRepr;                                                }
 static inline void        Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num )   { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num;          }
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 6f3731a1..a9ac56b6 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -26,61 +26,84 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Gla_Obj_t_ Gla_Obj_t; // object
+typedef struct Rfn_Obj_t_ Rfn_Obj_t; // refinement object
+struct Rfn_Obj_t_
+{
+    unsigned       Value     :  1;  // value
+    unsigned       fVisit    :  1;  // visited
+    unsigned       fPPi      :  1;  // PPI
+    unsigned       Prio      : 28;  // priority
+};
+
+typedef struct Gla_Obj_t_ Gla_Obj_t; // abstraction object
 struct Gla_Obj_t_
 {
-    int           iGiaObj;         // corresponding GIA obj
-    unsigned      fAbs      :  1;  // belongs to abstraction
-    unsigned      fCompl0   :  1;  // compl bit of the first fanin
-//    unsigned      fCompl1   :  1;  // compl bit of the second fanin
-    unsigned      fConst    :  1;  // object attribute
-    unsigned      fPi       :  1;  // object attribute
-    unsigned      fPo       :  1;  // object attribute
-    unsigned      fRo       :  1;  // object attribute
-    unsigned      fRi       :  1;  // object attribute
-    unsigned      fAnd      :  1;  // object attribute
-    unsigned      nFanins   : 24;  // fanin count
-    int           Fanins[4];       // fanins
-    Vec_Int_t     vFrames;         // variables in each timeframe
+    int            iGiaObj;         // corresponding GIA obj
+    unsigned       fAbs      :  1;  // belongs to abstraction
+    unsigned       fCompl0   :  1;  // compl bit of the first fanin
+    unsigned       fConst    :  1;  // object attribute
+    unsigned       fPi       :  1;  // object attribute
+    unsigned       fPo       :  1;  // object attribute
+    unsigned       fRo       :  1;  // object attribute
+    unsigned       fRi       :  1;  // object attribute
+    unsigned       fAnd      :  1;  // object attribute
+    unsigned       fMark     :  1;  // nearby object
+    unsigned       nFanins   : 23;  // fanin count
+    int            Fanins[4];       // fanins
+    Vec_Int_t      vFrames;         // variables in each timeframe
 };
 
 typedef struct Gla_Man_t_ Gla_Man_t; // manager
 struct Gla_Man_t_
 {
     // user data
-    Gia_Man_t *   pGia;            // AIG manager
-    Gia_ParVta_t* pPars;           // parameters
+    Gia_Man_t *    pGia;            // AIG manager
+    Gia_ParVta_t*  pPars;           // parameters
     // internal data
-    Vec_Int_t *   vAbs;            // abstracted objects
-    Gla_Obj_t *   pObjRoot;        // the primary output
-    Gla_Obj_t *   pObjs;           // objects
-    int           nObjs;           // the number of objects
-    int           nAbsOld;         // previous abstraction
+    Vec_Int_t *    vAbs;            // abstracted objects
+    Gla_Obj_t *    pObjRoot;        // the primary output
+    Gla_Obj_t *    pObjs;           // objects
+    unsigned *     pObj2Obj;        // mapping of GIA obj into GLA obj
+    int            nObjs;           // the number of objects
+    int            nAbsOld;         // previous abstraction
     // other data
-    int           nCexes;          // the number of counter-examples
-    int           nSatVars;        // the number of SAT variables
-    Cnf_Dat_t *   pCnf;            // CNF derived for the nodes
-    sat_solver2 * pSat;            // incremental SAT solver
-    Vec_Int_t *   vCla2Obj;        // mapping of clauses into GLA objs
-    Vec_Int_t *   vTemp;           // temporary array
-    Vec_Int_t *   vAddedNew;       // temporary array
-    // statistics 
-    int           timeInit;
-    int           timeSat;
-    int           timeUnsat;
-    int           timeCex;
-    int           timeOther;
+    int            nCexes;          // the number of counter-examples
+    int            nSatVars;        // the number of SAT variables
+    Cnf_Dat_t *    pCnf;            // CNF derived for the nodes
+    sat_solver2 *  pSat;            // incremental SAT solver
+    Vec_Int_t *    vCla2Obj;        // mapping of clauses into GLA objs
+    Vec_Int_t *    vTemp;           // temporary array
+    Vec_Int_t *    vAddedNew;       // temporary array
+    Vec_Int_t *    vPrevCore;       // previous core
+    // refinement
+    Vec_Int_t *    pvRefis;         // vectors of each object
+    Vec_Int_t *    vPrioSels;       // selected priorities
+    // statistics  
+    int            timeInit;
+    int            timeSat;
+    int            timeUnsat;
+    int            timeCex;
+    int            timeOther;
 };
 
+// declarations
+static Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis );
+static int         Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame );
+static int         Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame );
+
 // object procedures
-static inline int         Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj )     { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;  }
-static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i )               { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                 }
-static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj );                                      }
+static inline int         Gla_ObjId( Gla_Man_t * p, Gla_Obj_t * pObj )      { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs;   }
+static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i )                { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL;                  }
+static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj )  { return Gia_ManObj( p->pGia, pObj->iGiaObj );                                       }
+static inline int         Gla_ObjSatValue( Gla_Man_t * p, int iGia, int f ) { return Gla_ManCheckVar(p, p->pObj2Obj[iGia], f) ? sat_solver2_var_value( p->pSat, Gla_ManGetVar(p, p->pObj2Obj[iGia], f) ) : 0;  }
+
+static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, int iObj, int f )      {  return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[iObj]), f );                   }
+static inline void        Gla_ObjClearRef( Rfn_Obj_t * p )                  {  *((int *)p) = 0;                                                                  }
+
 
 // iterator through abstracted objects
 #define Gla_ManForEachObj( p, pObj )                       \
@@ -91,7 +114,7 @@ static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { ret
     for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++) 
 
 // iterator through fanins of an abstracted object
-#define Gla_ObjForEachFanin( p, pObj, pFanin, i )    \
+#define Gla_ObjForEachFanin( p, pObj, pFanin, i )          \
     for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
@@ -240,6 +263,398 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives counter-example using current assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
+{
+    Abc_Cex_t * pCex;
+    Gia_Obj_t * pObj;
+    int i, f;
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
+    pCex->iPo = 0;
+    pCex->iFrame = p->pPars->iFrame;
+    Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+    {
+        assert( Gia_ObjIsPi(p->pGia, pObj) );
+        for ( f = 0; f <= pCex->iFrame; f++ )
+            if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal objects in a topo order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManRefCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRoAnds, Vec_Int_t * vCos )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsRo(p, pObj) )
+    {
+        Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
+        Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gla_ManRefCollect_rec( p, Gia_ObjFanin0(pObj), vRoAnds, vCos );
+    Gla_ManRefCollect_rec( p, Gia_ObjFanin1(pObj), vRoAnds, vCos );
+    Vec_IntPush( vRoAnds, Gia_ObjId(p, pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects assignments to be refined.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes )
+{
+    Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
+    if ( pRef->fVisit )
+        return;
+    pRef->fVisit = 1;
+    if ( pRef->fPPi )
+    {
+        assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
+        if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
+        {
+            Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 );
+            Vec_IntPush( vRes, Gia_ObjId(p->pGia, pObj) );
+        }
+        return;
+    }
+    if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
+        return;
+    if ( Gia_ObjIsRo(p->pGia, pObj) )
+    {
+        if ( f > 0 )
+            Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( pRef->Value == 1 )
+    {
+        Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
+        Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
+    }
+    else // select one value
+    {
+        Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
+        Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
+        int fSel0 = Vec_IntEntry( p->vPrioSels, pRef0->Prio );
+        int fSel1 = Vec_IntEntry( p->vPrioSels, pRef1->Prio );
+
+        if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
+        {
+            if ( !fSel0 && !fSel1 )
+            {
+                if ( pRef0->Prio <= pRef1->Prio ) // choice
+                    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
+                else
+                    Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
+            }
+        }
+        else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
+        {
+            if ( !fSel0 )
+                Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes );
+        }
+        else 
+        {
+            if ( !fSel1 )
+                Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs refinement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
+{
+    int fVerify = 0;
+    Vec_Int_t * vPis, * vPPis, * vRoAnds, * vCos, * vRes = NULL;
+    Rfn_Obj_t * pRef, * pRef0, * pRef1;
+    Gia_Obj_t * pObj;
+    Gla_Obj_t * pGla;
+    int i, f;
+
+    // compute PIs and pseudo-PIs
+    vPis = Vec_IntAlloc( 100 );
+    vPPis = Gla_ManCollectPPis( p, vPis );
+
+    // remap into GIA
+    Gla_ManForEachObjAbsVec( vPis, p, pGla, i )
+        Vec_IntWriteEntry( vPis, i, pGla->iGiaObj );
+    Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
+        Vec_IntWriteEntry( vPPis, i, pGla->iGiaObj );
+
+    // prepare boundary objects
+    Gia_ManIncrementTravId( p->pGia );
+    Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
+    Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+        Gia_ObjSetTravIdCurrent( p->pGia, pObj );
+    Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
+        Gia_ObjSetTravIdCurrent( p->pGia, pObj );
+
+    // collect internal objects
+    vCos = Vec_IntAlloc( 1000 );  
+    vRoAnds = Vec_IntAlloc( 1000 );
+    Vec_IntPush( vCos, Gia_ObjId(p->pGia, Gia_ManPo(p->pGia, 0)) );
+    Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
+        Gla_ManRefCollect_rec( p->pGia, Gia_ObjFanin0(pObj), vRoAnds, vCos );
+
+    // propagate values
+    for ( f = 0; f <= p->pPars->iFrame; f++ )
+    {
+        // constant
+        pRef = Gla_ObjRef( p, 0, f );  Gla_ObjClearRef( pRef );
+        pRef->Value  = 0;
+        pRef->Prio   = 0;
+        // primary input
+        Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+        {
+            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );   Gla_ObjClearRef( pRef );
+            pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
+            pRef->Prio = 0;
+        }
+        // primary input
+        Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
+        {
+            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
+            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );   Gla_ObjClearRef( pRef );
+            pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
+            pRef->Prio  = i+1;
+            pRef->fPPi  = 1;
+        }
+        // internal nodes
+        Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
+        {
+            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );   Gla_ObjClearRef( pRef );
+            if ( Gia_ObjIsRo(p->pGia, pObj) )
+            {
+                if ( f == 0 )
+                {
+                    pRef->Value = 0;
+                    pRef->Prio  = 0;
+                }
+                else
+                {
+                    pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 );
+                    pRef->Value = pRef0->Value;
+                    pRef->Prio  = pRef0->Prio;
+                }
+                continue;
+            }
+            assert( Gia_ObjIsAnd(pObj) );
+            pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
+            pRef1 = Gla_ObjRef( p, Gia_ObjFaninId1p(p->pGia, pObj), f );
+            pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
+//                if ( p->pCnf->pObj2Count[Gia_ObjId(p->pGia, pObj)] >= 0 )
+//                    assert( (int)pRef->Value == Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) );
+            if ( pRef->Value == 1 )
+                pRef->Prio  = Abc_MaxInt( pRef0->Prio, pRef1->Prio );
+            else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
+                pRef->Prio  = Abc_MinInt( pRef0->Prio, pRef1->Prio ); // choice
+            else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
+                pRef->Prio  = pRef0->Prio;
+            else 
+                pRef->Prio  = pRef1->Prio;
+        }
+        // output nodes
+        Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
+        {
+            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );    Gla_ObjClearRef( pRef );
+            pRef0 = Gla_ObjRef( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); 
+            pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
+            pRef->Prio  = pRef0->Prio;
+        }
+    }
+    // make sure the output value is 1
+    pObj = Gia_ManPo( p->pGia, 0 );
+    pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), p->pPars->iFrame );
+    assert( pRef->Value == 1 );
+
+    // check the CEX
+    if ( pRef->Prio == 0 )
+    {
+        p->pGia->pCexSeq = Gla_ManDeriveCex( p, vPis );
+        Vec_IntFree( vPis );
+        Vec_IntFree( vPPis );
+        Vec_IntFree( vRoAnds );
+        Vec_IntFree( vCos );
+        return 0;
+    }
+
+    // select objects
+    vRes = Vec_IntAlloc( 100 );
+    Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
+    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes );
+
+    if ( fVerify )
+    {
+        Gia_ManForEachObj( p->pGia, pObj, i )
+            assert( Gia_ObjTerSimGetC(pObj) );
+        for ( f = 0; f <= p->pPars->iFrame; f++ )
+        {
+            Gia_ObjTerSimSet0( Gia_ManConst0(p->pGia) );
+            Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+            {
+                if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
+                    Gia_ObjTerSimSet1( pObj );
+                else
+                    Gia_ObjTerSimSet0( pObj );
+            }
+            Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
+            {
+                if ( Vec_IntEntry(p->vPrioSels, i+1) == 0 ) // not selected
+                    Gia_ObjTerSimSetX( pObj );
+                else if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
+                    Gia_ObjTerSimSet1( pObj );
+                else
+                    Gia_ObjTerSimSet0( pObj );
+            }
+            Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
+            {
+                if ( Gia_ObjIsAnd(pObj) )
+                    Gia_ObjTerSimAnd( pObj );
+                else if ( f == 0 )
+                    Gia_ObjTerSimSet0( pObj );
+                else
+                    Gia_ObjTerSimRo( p->pGia, pObj );
+            }
+            Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
+                Gia_ObjTerSimCo( pObj );
+        }
+        pObj = Gia_ManPo( p->pGia, 0 );
+        if ( !Gia_ObjTerSimGet1(pObj) )
+            printf( "Refinement verification has failed!!!" );
+        // clear
+        Gia_ObjTerSimSetC( Gia_ManConst0(p->pGia) );
+        Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
+            Gia_ObjTerSimSetC( pObj );
+        Gia_ManForEachObjVec( vPPis, p->pGia, pObj, i )
+            Gia_ObjTerSimSetC( pObj );
+        Gia_ManForEachObjVec( vRoAnds, p->pGia, pObj, i )
+            Gia_ObjTerSimSetC( pObj );
+        Gia_ManForEachObjVec( vCos, p->pGia, pObj, i )
+            Gia_ObjTerSimSetC( pObj );
+    }
+
+    // remap them into GLA objects
+    Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
+        Vec_IntWriteEntry( vRes, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
+
+    Vec_IntFree( vPis );
+    Vec_IntFree( vPPis );
+    Vec_IntFree( vRoAnds );
+    Vec_IntFree( vCos );
+    return vRes;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Selects items that are new in the current abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gla_ManRegionStart( Gla_Man_t * p, Vec_Int_t * vCore )
+{
+    Vec_Int_t * vRes;
+    Gla_Obj_t * pGla;
+    int i;
+    vRes = Vec_IntAlloc( 100 );
+    Gla_ManForEachObjAbsVec( vCore, p, pGla, i )
+        if ( !pGla->fAbs )
+            Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds adjacent to previous core among select (or all if NULL).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gla_ManRegionFilter( Gla_Man_t * p, Vec_Int_t * vSelected, Vec_Int_t * vPrevCore )
+{
+    Vec_Int_t * vRes;
+    Gla_Obj_t * pGla, * pFanin;
+    int i, k;
+    // mark fanins of previous core
+    Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
+    {
+        assert( pGla->fMark == 0 );
+        Gla_ObjForEachFanin( p, pGla, pFanin, k )
+            pFanin->fMark = 1;
+    }
+    // select those not marked and included in the abstraction
+    vRes = Vec_IntAlloc( 100 );
+    if ( vSelected == NULL )
+    {
+        Gla_ManForEachObj( p, pGla )
+            if ( !pGla->fAbs && pGla->fMark )
+                Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
+    }
+    else
+    {
+        Gla_ManForEachObjAbsVec( vSelected, p, pGla, i )
+            if ( !pGla->fAbs && pGla->fMark )
+                Vec_IntPush( vRes, Gla_ObjId(p, pGla) );
+    }
+    // unmark fanins of previous core
+    Gla_ManForEachObjAbsVec( vPrevCore, p, pGla, i )
+        Gla_ObjForEachFanin( p, pGla, pFanin, k )
+            pFanin->fMark = 0;
+    return vRes;
+}
+
 
 
 /**Function*************************************************************
@@ -292,6 +707,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->vAbs = Vec_IntAlloc( 100 );
     p->vTemp = Vec_IntAlloc( 100 );
     p->vAddedNew = Vec_IntAlloc( 100 );
+    p->vPrioSels = Vec_IntAlloc( 100 );
     // internal data
     pAig = Gia_ManToAigSimple( p->pGia );
     p->pCnf  = Cnf_DeriveOther( pAig );
@@ -311,16 +727,18 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         assert( ~pObj->Value );
         pLits[i] = toLitCond( pObj->Value, lit_sign(pLits[i]) );
     }
-    // create objects
-    p->pObjs = ABC_CALLOC( Gla_Obj_t, p->nObjs );
+    // create objects 
+    p->pObjs    = ABC_CALLOC( Gla_Obj_t, p->nObjs );
+    p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
+    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
     Gia_ManForEachObj( p->pGia, pObj, i )
     {
+        p->pObj2Obj[i] = pObj->Value;
         if ( !~pObj->Value )
             continue;
         pGla = Gla_ManObj( p, pObj->Value );
         pGla->iGiaObj = i;
         pGla->fCompl0 = Gia_ObjFaninC0(pObj);
-//        pGla->fCompl1 = Gia_ObjFaninC1(pObj);
         pGla->fConst  = Gia_ObjIsConst0(pObj);
         pGla->fPi     = Gia_ObjIsPi(p->pGia, pObj);
         pGla->fPo     = Gia_ObjIsPo(p->pGia, pObj);
@@ -379,10 +797,14 @@ void Gla_ManStop( Gla_Man_t * p )
         ABC_FREE( pGla->vFrames.pArray );
     Cnf_DataFree( p->pCnf );
     sat_solver2_delete( p->pSat );
-    Vec_IntFree( p->vCla2Obj );
-    Vec_IntFree( p->vAddedNew );
-    Vec_IntFree( p->vTemp );
-    Vec_IntFree( p->vAbs );
+    Vec_IntFreeP( &p->vCla2Obj );
+    Vec_IntFreeP( &p->vPrevCore );
+    Vec_IntFreeP( &p->vAddedNew );
+    Vec_IntFreeP( &p->vPrioSels );
+    Vec_IntFreeP( &p->vTemp );
+    Vec_IntFreeP( &p->vAbs );
+    ABC_FREE( p->pvRefis );
+    ABC_FREE( p->pObj2Obj );
     ABC_FREE( p->pObjs );
     ABC_FREE( p );
 }
@@ -475,53 +897,53 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
+Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p, Vec_Int_t * vPis )
 {
     Vec_Int_t * vPPis;
     Gla_Obj_t * pObj, * pFanin;
     int i, k;
     vPPis = Vec_IntAlloc( 1000 );
+    if ( vPis )
+        Vec_IntClear( vPis );
     Gla_ManForEachObjAbs( p, pObj, i )
     {
         assert( pObj->fConst || pObj->fRo || pObj->fAnd );
         Gla_ObjForEachFanin( p, pObj, pFanin, k )
             if ( !pFanin->fPi && !pFanin->fAbs )
                 Vec_IntPush( vPPis, pObj->Fanins[k] );
+            else if ( vPis && pFanin->fPi && !pFanin->fAbs )
+                Vec_IntPush( vPis, pObj->Fanins[k] );
     }
     Vec_IntUniqify( vPPis );
     Vec_IntReverseOrder( vPPis );
+    if ( vPis )
+        Vec_IntUniqify( vPis );
     return vPPis;
 }
 int Gla_ManCountPPis( Gla_Man_t * p )
 {
-    Vec_Int_t * vPPis = Gla_ManCollectPPis( p );
+    Vec_Int_t * vPPis = Gla_ManCollectPPis( p, NULL );
     int RetValue = Vec_IntSize( vPPis );
     Vec_IntFree( vPPis );
     return RetValue;
 }
 
+
 void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
 {
     static int Round = 0;
     Gla_Obj_t * pObj, * pFanin;
     int i, j, k, Count;
-    if ( (Round++ % 3) == 0 )
+    if ( (Round++ % 5) == 0 )
         return;
-//    printf( "\n" );
     j = 0;
     Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
     {
         assert( pObj->fAbs == 0 );
-//        printf( "%6d ", Gla_ObjId(p, pObj) );
-//        printf( "Fanins=%d ", pObj->nFanins );
-//        Gla_ObjForEachFanin( p, pObj, pFanin, k )
-//            printf( "%d", pFanin->fAbs );
-//        printf( "\n" );
-
         Count = 0;
         Gla_ObjForEachFanin( p, pObj, pFanin, k )
             Count += pFanin->fAbs;
-        if ( Count == 0 )
+        if ( Count == 0 || ((Round & 1) && Count == 1) )
             continue;
         Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
     }
@@ -529,6 +951,99 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
     Vec_IntShrink( vPPis, j );
 }
 
+// add those having more than one shared fanin
+
+
+void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis )
+{
+    static int Round = 0;
+    Vec_Int_t * vTemp;
+    Gla_Obj_t * pGla, * pFanin;
+    int i, k, Entry, Count;
+    if ( p->vPrevCore == NULL )
+        return;
+    if ( (Round++ % 10) == 0 )
+    {
+        p->vPrevCore = Gla_ManRegionFilter( p, vPPis, vTemp = p->vPrevCore );
+        Vec_IntFree( vTemp );
+    }
+    else
+    {
+        p->vPrevCore = Gla_ManRegionFilter( p, NULL, vTemp = p->vPrevCore );
+        Vec_IntFree( vTemp );
+        // save a copy
+        vTemp = Vec_IntDup( vPPis );
+        // udpate
+        Vec_IntClear( vPPis );
+        Vec_IntForEachEntry( p->vPrevCore, Entry, i )
+            Vec_IntPush( vPPis, Entry );
+
+
+        // mark those included as abstracted
+        Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
+        {
+            assert( pGla->fAbs == 0 );
+            pGla->fAbs = 1;
+        }
+        // add those not included but to close to abstracted
+        Gla_ManForEachObjAbsVec( vTemp, p, pGla, i )
+        {
+            if ( pGla->fAbs )
+                continue;
+            Count = 0;
+            Gla_ObjForEachFanin( p, pGla, pFanin, k )
+                Count += pFanin->fAbs;
+            if ( Count == 0 || Count == 1 )
+                continue;
+            Vec_IntPush( vPPis, Gla_ObjId(p, pGla) );
+        }
+        // unmark those included
+        Gla_ManForEachObjAbsVec( vPPis, p, pGla, i )
+            pGla->fAbs = 0;
+
+
+        // cleanup
+        Vec_IntFree( vTemp );
+    }
+}
+
+/*
+void Gla_ManExplorePPis2( Gla_Man_t * p, Vec_Int_t * vPPis, int iIter )
+{
+    Gla_Obj_t * pObj, * pFanin;
+    int i, j, k;
+    if ( iIter > 10 )
+    {
+        Gla_ManForEachObj( p, pObj )
+            pObj->fMark = 0;
+        return;
+    }
+    j = 0;
+    Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
+    {
+        assert( pObj->fAbs == 0 );
+        if ( pObj->fMark == 0 )
+        {
+            Gla_ObjForEachFanin( p, pObj, pFanin, k )
+                if ( pObj->fMark )
+                    break;
+            if ( k == (int)pObj->nFanins )
+                continue;
+        }
+        Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
+    }
+//    printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
+    Vec_IntShrink( vPPis, j );
+
+    // update
+    Gla_ManForEachObj( p, pObj )
+        pObj->fMark = 0;
+    Gla_ManForEachObjAbsVec( vPPis, p, pObj, i )
+        Gla_ObjForEachFanin( p, pObj, pFanin, k )
+            pFanin->fMark = 1;
+}
+*/
+
 
 /**Function*************************************************************
 
@@ -541,6 +1056,13 @@ void Gla_ManExplorePPis( Gla_Man_t * p, Vec_Int_t * vPPis )
   SeeAlso     []
 
 ***********************************************************************/
+int Gla_ManCheckVar( Gla_Man_t * p, int iObj, int iFrame )
+{
+    Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
+    int iVar = Vec_IntGetEntry( &pGla->vFrames, iFrame );
+    assert( !pGla->fPo && !pGla->fRi );
+    return (iVar > 0);
+}
 int Gla_ManGetVar( Gla_Man_t * p, int iObj, int iFrame )
 {
     Gla_Obj_t * pGla = Gla_ManObj( p, iObj );
@@ -772,25 +1294,31 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
 void Gla_ManReportMemory( Gla_Man_t * p )
 {
     Gla_Obj_t * pGla;
+    int i;
     double memTot = 0;
     double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
     double memSat = sat_solver2_memory( p->pSat );
     double memPro = sat_solver2_memory_proof( p->pSat );
-    double memMap = p->nObjs * sizeof(Gla_Obj_t);
+    double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
+    double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t) + Vec_IntCap(p->vPrioSels) * sizeof(int);
     double memOth = sizeof(Gla_Man_t);
     for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
         memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
+    for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
+        memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
     memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
     memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
+    memOth += (p->vPrevCore ? Vec_IntCap(p->vPrevCore) : 0) * sizeof(int);
     memOth += Vec_IntCap(p->vTemp) * sizeof(int);
     memOth += Vec_IntCap(p->vAbs) * sizeof(int);
-    memTot = memAig + memSat + memPro + memMap + memOth;
-    ABC_PRMP( "Memory: AIG  ", memAig, memTot );
-    ABC_PRMP( "Memory: SAT  ", memSat, memTot );
-    ABC_PRMP( "Memory: Proof", memPro, memTot );
-    ABC_PRMP( "Memory: Map  ", memMap, memTot );
-    ABC_PRMP( "Memory: Other", memOth, memTot );
-    ABC_PRMP( "Memory: TOTAL", memTot, memTot );
+    memTot = memAig + memSat + memPro + memMap + memRef + memOth;
+    ABC_PRMP( "Memory: AIG   ", memAig, memTot );
+    ABC_PRMP( "Memory: SAT   ", memSat, memTot );
+    ABC_PRMP( "Memory: Proof ", memPro, memTot );
+    ABC_PRMP( "Memory: Map   ", memMap, memTot );
+    ABC_PRMP( "Memory: Refine", memRef, memTot );
+    ABC_PRMP( "Memory: Other ", memOth, memTot );
+    ABC_PRMP( "Memory: TOTAL ", memTot, memTot );
 }
 
 
@@ -920,11 +1448,17 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             p->nCexes++;
             // perform the refinement
             clk2 = clock();
-//            pCex = Vta_ManRefineAbstraction( p, f );
-            pCex = NULL;
-
-            vPPis = Gla_ManCollectPPis( p );
+/*
+            vPPis = Gla_ManRefinement( p );
+            if ( vPPis == NULL )
+            {
+                pCex = p->pGia->pCexSeq; p->pGia->pCexSeq = NULL;
+                break;
+            }
+*/
+            vPPis = Gla_ManCollectPPis( p, NULL );
             Gla_ManExplorePPis( p, vPPis );
+
             Gia_GlaAddToAbs( p, vPPis, 1 );
             Gia_GlaAddOneSlice( p, f, vPPis );
             Vec_IntFree( vPPis );
@@ -952,6 +1486,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             Gla_ManRollBack( p );
             Vec_IntShrink( p->vCla2Obj, (int)p->pSat->stats.clauses+1 );
             // load this timeframe
+            Vec_IntFreeP( &p->vPrevCore );
+            p->vPrevCore = Gla_ManRegionStart( p, vCore );
             Gia_GlaAddToAbs( p, vCore, 0 );
             Gia_GlaAddOneSlice( p, f, vCore );
             Vec_IntFree( vCore );
@@ -965,6 +1501,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 break;
             if ( Status == 0 )
             {
+                assert( 0 );
     //            Vta_ManSatVerify( p );
                 // make sure, there was no initial abstraction (otherwise, it was invalid)
                 assert( pAig->vObjClasses == NULL && f < p->pPars->nFramesStart );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 9a9dc56f..44169f23 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -532,8 +532,8 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p
 {
     *ppThis0 = NULL;
     *ppThis1 = NULL;
-    if ( !pThis->fAdded )
-        return;
+//    if ( !pThis->fAdded )
+//        return;
     assert( !Gia_ObjIsPi(p->pGia, pObj) );
     if ( Gia_ObjIsConst0(pObj) || (Gia_ObjIsCi(pObj) && pThis->iFrame == 0) )
         return;
@@ -541,13 +541,13 @@ static inline void Vta_ObjPreds( Vta_Man_t * p, Vta_Obj_t * pThis, Gia_Obj_t * p
     {
         *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame );
         *ppThis1 = Vga_ManFind( p, Gia_ObjFaninId1p(p->pGia, pObj), pThis->iFrame );
-        assert( *ppThis0 && *ppThis1 );
+//        assert( *ppThis0 && *ppThis1 );
         return;
     }
     assert( Gia_ObjIsRo(p->pGia, pObj) && pThis->iFrame > 0 );
     pObj = Gia_ObjRoToRi( p->pGia, pObj );
     *ppThis0 = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), pThis->iFrame-1 );
-    assert( *ppThis0 );
+//    assert( *ppThis0 );
 }
 
 /**Function*************************************************************
@@ -569,9 +569,12 @@ void Vta_ManCollectNodes_rec( Vta_Man_t * p, Vta_Obj_t * pThis, Vec_Int_t * vOrd
         return;
     pThis->fVisit = 1;
     pObj = Gia_ManObj( p->pGia, pThis->iObj );
-    Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
-    if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
-    if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
+    if ( pThis->fAdded )
+    {
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        if ( pThis0 ) Vta_ManCollectNodes_rec( p, pThis0, vOrder );
+        if ( pThis1 ) Vta_ManCollectNodes_rec( p, pThis1, vOrder );
+    }
     Vec_IntPush( vOrder, Vta_ObjId(p, pThis) );
 }
 Vec_Int_t * Vta_ManCollectNodes( Vta_Man_t * p, int f )
@@ -728,6 +731,41 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         if ( pThis1 ) 
             pThis1->Prio = Abc_MinInt( pThis1->Prio, pThis->Prio + 1 );
     }
+
+/*
+    // update priorities according to reconvergest counters
+    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+    {
+        Vta_Obj_t * pThis0, * pThis1;
+        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        pThis->Prio += 10000000;
+        if ( pThis0 )
+            pThis->Prio -= 1000000 * pThis0->fAdded;
+        if ( pThis1 )
+            pThis->Prio -= 1000000 * pThis1->fAdded;
+    }
+    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
+    {
+        Vta_Obj_t * pThis0, * pThis1;
+        Gia_Obj_t * pObj = Gia_ManObj( p->pGia, pThis->iObj );
+        Vta_ObjPreds( p, pThis, pObj, &pThis0, &pThis1 );
+        pThis->Prio += 10000000;
+        if ( pThis0 )
+            pThis->Prio -= 1000000 * pThis0->fAdded;
+        if ( pThis1 )
+            pThis->Prio -= 1000000 * pThis1->fAdded;
+    }
+*/
+
+/*
+    // update priorities according to reconvergest counters
+    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+        pThis->Prio = pThis->iObj;
+    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUnused, pThis, i )
+        pThis->Prio = pThis->iObj;
+*/
+
     // objects with equal distance should receive priority based on number
     // those objects whose prototypes have been added in other timeframes
     // should have higher priority than the current object
@@ -747,9 +785,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pThis->Prio = Counter++;
 //    Abc_Print( 1, "Used %d  Unused %d\n", Vec_PtrSize(vTermsUsed), Vec_PtrSize(vTermsUnused) );
 
-    Vec_PtrFree( vTermsUsed );
-    Vec_PtrFree( vTermsUnused );
-
 
     // propagate in the direct order
     Vta_ManForEachObjObjVec( vOrder, p, pThis, pObj, i )
@@ -885,6 +920,33 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
             assert( 0 );
     }
 
+    // mark those currently included
+    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+    {
+        assert( pThis->fVisit == 0 );
+        pThis->fVisit = 1;
+    }
+    // add used terms, which have close relationship
+    Counter = Vec_IntSize(vTermsToAdd);
+    Vec_PtrForEachEntry( Vta_Obj_t *, vTermsUsed, pThis, i )
+    {
+        if ( pThis->fVisit )
+            continue;
+//        Vta_ObjPreds( p, pThis, Gia_ManObj(p->pGia, pThis->iObj), &pThis0, &pThis1 );
+//        if ( (pThis0 && (pThis0->fAdded || pThis0->fVisit)) || (pThis1 && (pThis1->fAdded || pThis1->fVisit)) )
+            Vec_IntPush( vTermsToAdd, Vta_ObjId(p, pThis) );
+    }
+    // remove those currenty included
+    Vta_ManForEachObjVec( vTermsToAdd, p, pThis, i )
+        pThis->fVisit = 0;
+//    printf( "\n%d -> %d\n", Counter, Vec_IntSize(vTermsToAdd) );
+//Vec_IntReverseOrder( vTermsToAdd );
+//Vec_IntSort( vTermsToAdd, 1 );
+
+    // cleanup
+    Vec_PtrFree( vTermsUsed );
+    Vec_PtrFree( vTermsUnused );
+
 
     if ( fVerify )
     {
@@ -955,7 +1017,6 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
         pCex = Vga_ManDeriveCex( p );
     else
     {
-//        int nObjOld = p->nObjs;
         Vta_ManForEachObjObjVec( vTermsToAdd, p, pThis, pObj, i )
             if ( !Gia_ObjIsPi(p->pGia, pObj) )
                 Vga_ManAddClausesOne( p, pThis->iObj, pThis->iFrame );