Improved abstraction refinement.

4 files changed, 491 insertions, 44 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 6910f334..d8a18930 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -20,7 +20,7 @@
 
 #include "gia.h"
 #include "giaAbsRef.h"
-#include "giaAbsRef2.h"
+//#include "giaAbsRef2.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver2.h"
 #include "base/main/main.h"
@@ -52,7 +52,7 @@ struct Ga2_Man_t_
     int            nMarked;      // total number of marked nodes and flops
     // refinement
     Rnm_Man_t *    pRnm;         // refinement manager
-    Rf2_Man_t *    pRf2;         // refinement manager
+//    Rf2_Man_t *    pRf2;         // refinement manager
     // SAT solver and variables
     Vec_Ptr_t *    vId2Lit;      // mapping, for each timeframe, of object ID into SAT literal
     sat_solver2 *  pSat;         // incremental SAT solver
@@ -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] );
@@ -1224,11 +1224,9 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
- 
-//    Rf2_ManRefine( p->pRf2, 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 )
     {
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c
index 5b7bcee2..21a87c33 100644
--- a/src/aig/gia/giaAbsRef.c
+++ b/src/aig/gia/giaAbsRef.c
@@ -77,6 +77,7 @@ 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)
 };
@@ -91,6 +92,8 @@ struct Rnm_Man_t_
     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
     // internal data
     Rnm_Obj_t *    pObjs;           // refinement objects
     int            nObjs;           // the number of used objects
@@ -98,6 +101,7 @@ struct Rnm_Man_t_
     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
@@ -114,6 +118,17 @@ static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )
     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;  }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -136,6 +151,8 @@ Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
     p = ABC_CALLOC( Rnm_Man_t, 1 );
     p->pGia = pGia;
     p->vObjs = Vec_IntAlloc( 100 );
+    p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) );
+    p->vFanins = Vec_IntAlloc( 100 );
     p->nObjsAlloc = 10000;
     p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
     if ( p->pGia->vFanout == NULL )
@@ -168,6 +185,8 @@ void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
     Gia_ManCleanMark1(p->pGia);
     Gia_ManStaticFanoutStop(p->pGia);
 //    Gia_ManSetPhase(p->pGia);
+    Vec_StrFree( p->vCounts );
+    Vec_IntFree( p->vFanins );
     Vec_IntFree( p->vObjs );
     ABC_FREE( p->pObjs );
     ABC_FREE( p );
@@ -332,6 +351,11 @@ 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 )
+    {
+        Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+        p->nVisited++;
+    }
     if ( pRnm->fPPi )
     {
         assert( (int)pRnm->Prio > 0 );
@@ -383,7 +407,14 @@ void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSe
     if ( p->fPropFanout )
         Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect );
     else
+    {
         pRnm->fVisit = 1;
+        if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 )
+        {
+            Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1;
+            p->nVisited++;
+        }
+    }
     if ( pRnm->fPPi )
     {
         assert( (int)pRnm->Prio > 0 );
@@ -507,6 +538,177 @@ 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 []
@@ -518,8 +720,11 @@ void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap
 ***********************************************************************/
 Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
 {
+    int fVerify = 0;
     Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
+    Vec_Int_t * vNew;
     clock_t clk, clk2 = clock();
+    int RetValue;
     p->nCalls++;
 //    Gia_ManCleanValue( p->pGia );
     // initialize
@@ -542,17 +747,43 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
         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 );
+//        assert( RetValue == 0 );
         p->timeBwd += clock() - clk;
     }
+
+    vNew = Ga2_FilterSelected( p, vSelected );
+    if ( Vec_IntSize(vNew) > 0 )
+    {
+        Vec_IntFree( vSelected );
+        vSelected = vNew;
+    }
+    else
+    {
+        Vec_IntFree( vNew );
+//        printf( "\nBig refinement.\n" );
+    }
+
     // clean values
     Rnm_ManCleanValues( p );
+
     // verify (empty) refinement
-    clk = clock();
-    Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
-    Vec_IntUniqify( vSelected );
+    if ( fVerify )
+    {
+        clk = clock();
+        Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
+        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 );
-    p->timeVer += clock() - clk;
     p->timeTotal += clock() - clk2;
     p->nRefines += Vec_IntSize(vSelected);
     return vSelected;
diff --git a/src/aig/gia/giaAbsRef2.c b/src/aig/gia/giaAbsRef2.c
index 03f1d9a2..e5bf3b0f 100644
--- a/src/aig/gia/giaAbsRef2.c
+++ b/src/aig/gia/giaAbsRef2.c
@@ -93,7 +93,8 @@ struct Rf2_Man_t_
     Vec_Int_t *    vObjs;           // internal objects used in value propagation
     Vec_Int_t *    vFanins;         // fanins of the PPI nodes
     Vec_Int_t *    pvVecs;          // vectors of integers for each object
-    Vec_Vec_t *    vNod2Ppi;        // for each node, the set of PPIs to include
+    Vec_Vec_t *    vGrp2Ppi;        // for each node, the set of PPIs to include
+    int            nMapWords;
     // internal data
     Rf2_Obj_t *    pObjs;           // refinement objects
     int            nObjs;           // the number of used objects
@@ -122,6 +123,76 @@ static inline Vec_Int_t * Rf2_ObjVec( Rf2_Man_t * p, Gia_Obj_t * pObj )
     return p->pvVecs + Gia_ObjId(p->pGia, pObj);
 }
 
+
+static inline unsigned * Rf2_ObjA( Rf2_Man_t * p, Gia_Obj_t * pObj )  
+{
+    return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj));
+}
+static inline unsigned * Rf2_ObjN( Rf2_Man_t * p, Gia_Obj_t * pObj )  
+{
+    return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords;
+}
+static inline void Rf2_ObjClear( Rf2_Man_t * p, Gia_Obj_t * pObj )  
+{
+    Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 );
+}
+static inline void Rf2_ObjStart( Rf2_Man_t * p, Gia_Obj_t * pObj, int i )  
+{
+    Vec_Int_t * vVec = Rf2_ObjVec(p, pObj);
+    int w;
+    Vec_IntClear( vVec );
+    for ( w = 0; w < p->nMapWords; w++ )
+        Vec_IntPush( vVec, 0 );
+    for ( w = 0; w < p->nMapWords; w++ )
+        Vec_IntPush( vVec, ~0 );
+    Abc_InfoSetBit( Rf2_ObjA(p, pObj), i );
+    Abc_InfoXorBit( Rf2_ObjN(p, pObj), i );
+}
+static inline void Rf2_ObjCopy( Rf2_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  
+{
+    assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
+    memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords );
+}
+static inline void Rf2_ObjDeriveAnd( Rf2_Man_t * p, Gia_Obj_t * pObj, int One )  
+{
+    unsigned * pInfo, * pInfo0, * pInfo1;
+    int i;
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( One == (int)pObj->fMark0 );
+    assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) );
+    assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) );
+    assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
+
+    pInfo  = Rf2_ObjA( p, pObj );
+    pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) );
+    pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) );
+    for ( i = 0; i < p->nMapWords; i++ )
+        pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]);
+
+    pInfo  = Rf2_ObjN( p, pObj );
+    pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) );
+    pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) );
+    for ( i = 0; i < p->nMapWords; i++ )
+        pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]);
+}
+static inline void Rf2_ObjPrint( Rf2_Man_t * p, Gia_Obj_t * pRoot )  
+{
+    Gia_Obj_t * pObj;
+    unsigned * pInfo;
+    int i;
+    pInfo  = Rf2_ObjA( p, pRoot );
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        if ( !Gia_ObjIsPi(p->pGia, pObj) )
+            printf( "%d", Abc_InfoHasBit(pInfo, i) );
+    printf( "\n" );
+    pInfo  = Rf2_ObjN( p, pRoot );
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        if ( !Gia_ObjIsPi(p->pGia, pObj) )
+            printf( "%d", !Abc_InfoHasBit(pInfo, i) );
+    printf( "\n" );
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -146,7 +217,7 @@ Rf2_Man_t * Rf2_ManStart( Gia_Man_t * pGia )
     p->vObjs = Vec_IntAlloc( 1000 );
     p->vFanins = Vec_IntAlloc( 1000 );
     p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) );
-    p->vNod2Ppi = Vec_VecStart( 100 );
+    p->vGrp2Ppi = Vec_VecStart( 100 );
     Gia_ManCleanMark0(pGia);
     Gia_ManCleanMark1(pGia);
     return p;
@@ -171,7 +242,7 @@ void Rf2_ManStop( Rf2_Man_t * p, int fProfile )
     }
     Vec_IntFree( p->vObjs );
     Vec_IntFree( p->vFanins );
-    Vec_VecFree( p->vNod2Ppi );
+    Vec_VecFree( p->vGrp2Ppi );
     ABC_FREE( p->pvVecs );
     ABC_FREE( p );
 }
@@ -471,9 +542,14 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
   SeeAlso     []
 
 ***********************************************************************/
-int Rf2_ManCountPis( Rf2_Man_t * p )
+static inline int Rf2_ManCountPpis( Rf2_Man_t * p )
 {
-    return 0;
+    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
+            Counter++;
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -487,9 +563,40 @@ int Rf2_ManCountPis( Rf2_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
+static inline void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
 {
+    int i, k, Entry;
+    Vec_IntForEachEntry( p, Entry, i )
+    {
+        for ( k = 0; k < Num; k++ )
+            printf( "%c", '0' + ((Entry>>k) & 1) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sort, make dup- and containment-free, and filter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
+{
+//    int Start = Vec_IntSize(p);
+    int Start = 0;
     int i, j, k, Entry, Entry2;
+//    printf( "%d", Vec_IntSize(p) );
+    if ( Start > 5 )
+    {
+        printf( "Before: \n" );
+        Rf2_ManPrintVector( p, 31 );
+    }
+
     k = 0;
     Vec_IntForEachEntry( p, Entry, i )
         if ( Gia_WordCountOnes((unsigned)Entry) <= Limit )
@@ -506,11 +613,18 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
             Vec_IntWriteEntry( p, k++, Entry );
     }
     Vec_IntShrink( p, k );            
+//    printf( "->%d ", Vec_IntSize(p) );
+    if ( Start > 5 )
+    {
+        printf( "After: \n" );
+        Rf2_ManPrintVector( p, 31 );
+        k = 0;
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Sort, make dup- and containment-free, and filter.]
+  Synopsis    [Assigns a unique justifification ID for each PPI.]
 
   Description []
                
@@ -519,18 +633,23 @@ void Rf2_ManProcessVector( Vec_Int_t * p, int Limit )
   SeeAlso     []
 
 ***********************************************************************/
-void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
+int Rf2_ManAssignJustIds( Rf2_Man_t * p )
 {
-    extern void Extra_PrintBinary( FILE * pFile, unsigned * p, int nBits );
-    int i, Entry;
-    printf( "Justification containing %d subsets.\n", Vec_IntSize(p) );
-    Vec_IntForEachEntry( p, Entry, i )
-        Extra_PrintBinary( stdout, (unsigned *)&Entry, Num ), printf( "\n" );
+    Gia_Obj_t * pObj;
+    int nPpis = Rf2_ManCountPpis( p );
+    int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
+    int i, k = 0;
+    Vec_VecClear( p->vGrp2Ppi );
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
+            Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i );
+    printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize );
+    return (k-1)/nGroupSize+1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns a unique justifification ID for each PPI.]
+  Synopsis    [Sort, make dup- and containment-free, and filter.]
 
   Description []
                
@@ -539,15 +658,31 @@ void Rf2_ManPrintVector( Vec_Int_t * p, int Num )
   SeeAlso     []
 
 ***********************************************************************/
-void Rf2_ManAssignJustIds( Rf2_Man_t * p )
+static inline void Rf2_ManPrintVectorSpecial( Rf2_Man_t * p, Vec_Int_t * vVec )
 {
     Gia_Obj_t * pObj;
-    int i, k = 0;
-    Vec_VecClear( p->vNod2Ppi );
-    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
-        if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
-            Vec_VecPushInt( p->vNod2Ppi, k++, i );
-    printf( "Considering %d PPIs with unique justification IDs.\n", k );
+    int nPpis = Rf2_ManCountPpis( p );
+    int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
+    int s, i, k, Entry, Counter;
+
+    Vec_IntForEachEntry( vVec, Entry, s )
+    {
+        k = 0;
+        Counter = 0;
+        Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        {
+            if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
+            {
+                if ( (Entry >> (k++ / nGroupSize)) & 1 )
+                    printf( "1" ), Counter++;
+                else
+                    printf( "0" );
+            }
+            else
+                printf( "-" );
+        }
+        printf( " %3d \n", Counter );
+    }
 }
 
 /**Function*************************************************************
@@ -581,7 +716,7 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
             Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
         }
         // assign justification sets for PPis
-        Vec_VecForEachLevelInt( p->vNod2Ppi, vVec, i )
+        Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i )
             Vec_IntForEachEntry( vVec, Entry, k )
             {
                 assert( i < 31 );
@@ -615,11 +750,11 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
                 continue;
             }
             assert( Gia_ObjIsAnd(pObj) );
+            vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
+            vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
             if ( pObj->fMark0 == 1 )
             {
-                vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
-                vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
                 Vec_IntForEachEntry( vVec0, Entry, k )
                     Vec_IntForEachEntry( vVec1, Entry2, j )
                         Vec_IntPush( vVec, Entry | Entry2 );
@@ -645,6 +780,77 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs justification propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rf2_ManBounds( Rf2_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int f, i, iBit = p->pCex->nRegs;
+    // init constant
+    pObj = Gia_ManConst0(p->pGia);
+    pObj->fMark0 = 0;
+    Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) );
+    // iterate through the timeframes
+    for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
+    {
+        // initialize frontier values and init justification sets
+        Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        {
+            assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
+            pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
+            Rf2_ObjStart( p, pObj, i );
+        }
+        // propagate internal nodes
+        Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
+        {
+            pObj->fMark0 = 0;
+            Rf2_ObjClear( p, pObj );
+            if ( Gia_ObjIsRo(p->pGia, pObj) )
+            {
+                if ( f == 0 )
+                {
+                    Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i );
+                    continue;
+                }
+                pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
+                Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) );
+                continue;
+            }
+            if ( Gia_ObjIsCo(pObj) )
+            {
+                pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
+                Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
+                continue;
+            }
+            assert( Gia_ObjIsAnd(pObj) );
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+            if ( pObj->fMark0 == 1 )
+                Rf2_ObjDeriveAnd( p, pObj, 1 );
+            else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
+                Rf2_ObjDeriveAnd( p, pObj, 0 );
+            else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
+                Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
+            else 
+                Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) );
+        }
+    }
+    assert( iBit == p->pCex->nBits );
+    if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
+        printf( "Output value is incorrect.\n" );
+
+    printf( "Bounds: \n" );
+    Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the refinement for a given counter-example.]
 
   Description []
@@ -657,8 +863,10 @@ Vec_Int_t * Rf2_ManPropagate( Rf2_Man_t * p, int Limit )
 Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
 {
     Vec_Int_t * vJusts;
-    Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
+//    Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
+    Vec_Int_t * vSelected = NULL;
     clock_t clk, clk2 = clock();
+    int nGroups;
     p->nCalls++;
     // initialize
     p->pCex = pCex;
@@ -670,15 +878,23 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
     // collect reconvergence points
 //    Rf2_ManGatherFanins( p, 2 );
     // propagate justification IDs
-    Rf2_ManAssignJustIds( p );
-    vJusts = Rf2_ManPropagate( p, 100 );
-    Rf2_ManPrintVector( vJusts, Rf2_ManCountPis(p) );
+    nGroups = Rf2_ManAssignJustIds( p );
+    vJusts = Rf2_ManPropagate( p, 32 );
+
+//    printf( "\n" );
+//    Rf2_ManPrintVector( vJusts, nGroups );
+    Rf2_ManPrintVectorSpecial( p, vJusts );
     if ( Vec_IntSize(vJusts) == 0 )
     {
         printf( "Empty set of justifying subsets.\n" );
         return NULL;
     }
+
+//    p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const
+//    Rf2_ManBounds( p );
+
     // select the result
+//    Abc_PrintTime( 1, "Time", clock() - clk2 );
 
     // verify (empty) refinement
     clk = clock();
@@ -687,7 +903,7 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
 //    Vec_IntReverseOrder( vSelected );
     p->timeVer += clock() - clk;
     p->timeTotal += clock() - clk2;
-    p->nRefines += Vec_IntSize(vSelected);
+//    p->nRefines += Vec_IntSize(vSelected);
     return vSelected;
 }
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 6988c8ea..a7722866 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1170,23 +1170,25 @@ static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
 
   Synopsis    [Leaves only unique entries.]
 
-  Description []
+  Description [Returns the number of duplicated entried found.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntUniqify( Vec_Int_t * p )
+static inline int Vec_IntUniqify( Vec_Int_t * p )
 {
-    int i, k;
+    int i, k, RetValue;
     if ( p->nSize < 2 )
-        return;
+        return 0;
     Vec_IntSort( p, 0 );
     for ( i = k = 1; i < p->nSize; i++ )
         if ( p->pArray[i] != p->pArray[i-1] )
             p->pArray[k++] = p->pArray[i];
+    RetValue = p->nSize - k;
     p->nSize = k;
+    return RetValue;
 }
 
 /**Function*************************************************************