Changed a few things in the refinement package of &gla.

4 files changed, 118 insertions, 24 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dc86ccb2..254359c2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28364,7 +28364,7 @@ usage:
     Abc_Print( -2, "\t-T num  : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-R num  : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
     Abc_Print( -2, "\t-P num  : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
-    Abc_Print( -2, "\t-B num  : the number of stable frames to dump abstraction or call prover (0<=num<=100) [default = %d]\n", pPars->nFramesNoChangeLim );
+    Abc_Print( -2, "\t-B num  : the number of stable frames to call prover or dump abstraction [default = %d]\n", pPars->nFramesNoChangeLim );
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 260a649c..fe024710 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -59,6 +59,7 @@ struct Ga2_Man_t_
     int            nSatVars;     // the number of SAT variables
     int            nCexes;       // the number of counter-examples
     int            nObjAdded;    // objs added during refinement
+    int            nPdrCalls;    // count the number of concurrent calls
     // hash table
     int *          pTable;
     int            nTable;
@@ -463,8 +464,8 @@ void Ga2_ManStop( Ga2_Man_t * p )
             sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), 
             p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
     if ( p->pPars->fVerbose )
-    Abc_Print( 1, "Hash hits = %d.  Hash misses = %d.  Hash overs = %d.\n", 
-        p->nHashHit, p->nHashMiss, p->nHashOver );
+    Abc_Print( 1, "Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  Concurrent calls = %d.\n", 
+        p->nHashHit, p->nHashMiss, p->nHashOver, p->nPdrCalls );
 
     if( p->pSat ) sat_solver2_delete( p->pSat );
     Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
@@ -1794,6 +1795,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
                     // prove new one
                     Gia_GlaProveAbsracted( pAig, pPars->fVerbose );
                     iFrameTryToProve = f;
+                    p->nPdrCalls++;
                 }
                 // speak to the bridge
                 if ( Abc_FrameIsBridgeMode() )
diff --git a/src/proof/abs/absRef.c b/src/proof/abs/absRef.c
index 64e1f55c..f72d86e2 100644
--- a/src/proof/abs/absRef.c
+++ b/src/proof/abs/absRef.c
@@ -672,7 +672,7 @@ 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 fNewRefinement, int fVerbose )
 {
-    int fVerify = 0;
+    int fVerify = 1;
     Vec_Int_t * vGoodPPis, * vNewPPis;
     clock_t clk, clk2 = clock();
     int RetValue;
@@ -705,6 +705,16 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
 //        assert( RetValue == 0 );
         p->timeBwd += clock() - clk;
     }
+
+    // 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, vGoodPPis );
+        p->timeVer += clock() - clk;
+    }
+
     // at this point array vGoodPPis contains the set of important PPIs
     if ( Vec_IntSize(vGoodPPis) > 0 ) // spurious CEX resulting in a non-trivial refinement 
     {
@@ -722,17 +732,10 @@ Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
     }
 
     // clean values
+    // we cannot do this before, because we need to remember what objects
+    // belong to the abstraction when we do Rnm_ManFilterSelected()
     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, vGoodPPis );
-        p->timeVer += clock() - clk;
-    }
-
 //    Vec_IntReverseOrder( vGoodPPis );
     p->timeTotal += clock() - clk2;
     p->nRefines += Vec_IntSize(vGoodPPis);
diff --git a/src/proof/abs/absRefSelect.c b/src/proof/abs/absRefSelect.c
index 871eb79b..1832d42c 100644
--- a/src/proof/abs/absRefSelect.c
+++ b/src/proof/abs/absRefSelect.c
@@ -69,7 +69,7 @@ void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vNewPPis )
 ***********************************************************************/
 void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vNewPPis )
 {
-    Vec_Int_t * vLeaves;
+    Vec_Int_t * vFanins;
     Gia_Obj_t * pObj, * pFanin;
     int i, k;
     // clean labels
@@ -90,8 +90,8 @@ void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, V
         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 )
+        vFanins = Ga2_ObjLeaves( p, pObj );
+        Gia_ManForEachObjVec( vFanins, p, pFanin, k )
         {
             printf( "    " );
             printf( "%6d ", Gia_ObjId(p, pFanin) );
@@ -125,8 +125,8 @@ void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, V
 ***********************************************************************/
 Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
 {
-   int fVerbose = 0;
-    Vec_Int_t * vNewPPis, * vLeaves;
+    int fVerbose = 0;
+    Vec_Int_t * vNewPPis, * vFanins;
     Gia_Obj_t * pObj, * pFanin;
     int i, k, RetValue, Counters[3] = {0};
 
@@ -138,8 +138,8 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
     Vec_IntClear( p->vFanins );
     Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
     {
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vFanins, 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) );
     }
@@ -160,8 +160,8 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
             Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
             continue;
         }
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
         {
             if ( Rnm_ObjIsJust(p, pFanin) || Rnm_ObjCount(p, pFanin) > 1 )
             {
@@ -206,8 +206,97 @@ Vec_Int_t * Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
 ***********************************************************************/
 Vec_Int_t * Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis )
 {
-    Vec_Int_t * vNewPPis;
-    vNewPPis = Vec_IntDup( vOldPPis );
+    static int Counter = 0;
+    int fVerbose = 0;
+    Vec_Int_t * vNewPPis, * vFanins, * vFanins2;
+    Gia_Obj_t * pObj, * pFanin, * pFanin2;
+    int i, k, k2, RetValue, Counters[3] = {0};
+
+    // return full set of PPIs once in a while
+    if ( ++Counter % 9 == 0 )
+        return Vec_IntDup( vOldPPis );
+    return Rnm_ManFilterSelected( p, vOldPPis );
+
+    // (0) make sure fanin counters are 0 at the beginning
+//    Gia_ManForEachObj( p->pGia, pObj, i )
+//        assert( Rnm_ObjCount(p, pObj) == 0 );
+
+    // (1) increment two levels of PPI fanin counters
+    Vec_IntClear( p->vFanins );
+    Gia_ManForEachObjVec( vOldPPis, p->pGia, pObj, i )
+    {
+        // go through the fanins
+        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
+        {
+            Rnm_ObjAddToCount(p, pFanin);
+            if ( Rnm_ObjIsJust(p, pFanin) )   // included in the abstraction
+                Rnm_ObjAddToCount(p, pFanin); // count it second time!
+            Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) );
+
+            // go through the fanins of the fanins
+            vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
+            Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
+            {
+                Rnm_ObjAddToCount(p, pFanin2);
+                if ( Rnm_ObjIsJust(p, pFanin2) )   // included in the abstraction
+                    Rnm_ObjAddToCount(p, pFanin2); // count it second time!
+                Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin2) );
+            }
+        }
+    }
+
+    // (3) select objects with reconvergence, which create potential constraints
+    // - flop objects - yes
+    // - objects whose fanin (or fanins' fanin) belongs to the justified area - yes
+    // - objects whose fanins (or fanins' fanin) overlap - yes
+    // (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;
+        } 
+        // go through the first fanins
+        vFanins = Ga2_ObjLeaves( p->pGia, pObj );
+        Gia_ManForEachObjVec( vFanins, p->pGia, pFanin, k )
+        {
+            if ( Rnm_ObjCount(p, pFanin) > 1 )
+                Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+            continue;
+
+            // go through the fanins of the fanins
+            vFanins2 = Ga2_ObjLeaves( p->pGia, pFanin );
+            Gia_ManForEachObjVec( vFanins2, p->pGia, pFanin2, k2 )
+            {
+                if ( Rnm_ObjCount(p, pFanin2) > 1 )
+                {
+//                    Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pFanin) );
+                    Vec_IntPush( vNewPPis, Gia_ObjId(p->pGia, pObj) );
+                }
+            }
+        }
+    }
+    RetValue = Vec_IntUniqify( vNewPPis );
+//    assert( RetValue == 0 ); // we will have duplicated entries here!
+
+    // (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;
 }