Gate level abstraction (command &gla).

3 files changed, 102 insertions, 42 deletions

diff --git a/abc.rc b/abc.rc
index a0ffbc38..99326c5f 100644
--- a/abc.rc
+++ b/abc.rc
@@ -119,6 +119,7 @@ alias share       "st; multi -m; fx; resyn2"
 alias addinit     "read_init; undc; strash; zero"
 alias blif2aig    "undc; strash; zero"
 alias v2p         "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v"
+alias g2p         "&ps; &gla_derive; &put; w 2.aig; pdr -v"
 
 # resubstitution scripts for the IWLS paper
 alias src_rw      "st; rw -l; rwz -l; rwz -l" 
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 17296cf2..23cd03a6 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -56,8 +56,10 @@ struct Gla_Man_t_
     Gia_Man_t *   pGia;            // AIG manager
     Gia_ParVta_t* pPars;           // parameters
     // internal data
+    Vec_Int_t *   vAbs;            // abstracted objects
     Gla_Obj_t *   pObjs;           // objects
     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
@@ -67,6 +69,7 @@ struct Gla_Man_t_
     Vec_Int_t *   vTemp;           // temporary array
     Vec_Int_t *   vAddedNew;       // temporary array
     // statistics 
+    int           timeInit;
     int           timeSat;
     int           timeUnsat;
     int           timeCex;
@@ -79,9 +82,11 @@ static inline Gla_Obj_t * Gla_ManObj( Gla_Man_t * p, int i )               { ass
 static inline Gia_Obj_t * Gla_ManGiaObj( Gla_Man_t * p, Gla_Obj_t * pObj ) { return Gia_ManObj( p->pGia, pObj->iGiaObj );                                      }
 
 // iterator through abstracted objects
-#define Gla_ManForEachObjAbs( p, pObj )              \
-    for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) if ( !pObj->fAbs ) {} else
-#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i )  \
+#define Gla_ManForEachObj( p, pObj )                       \
+    for ( pObj = p->pObjs + 1; pObj < p->pObjs + p->nObjs; pObj++ ) 
+#define Gla_ManForEachObjAbs( p, pObj, i )                 \
+    for ( i = 0; i < Vec_IntSize(p->vAbs) && ((pObj = Gla_ManObj(p, Vec_IntEntry(p->vAbs, i))),1); i++) 
+#define Gla_ManForEachObjAbsVec( vVec, p, pObj, i )        \
     for ( i = 0; i < Vec_IntSize(vVec) && ((pObj = Gla_ManObj(p, Vec_IntEntry(vVec, i))),1); i++) 
 
 // iterator through fanins of an abstracted object
@@ -283,6 +288,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p = ABC_CALLOC( Gla_Man_t, 1 );
     p->pGia  = pGia;
     p->pPars = pPars;
+    p->vAbs = Vec_IntAlloc( 100 );
     p->vTemp = Vec_IntAlloc( 100 );
     p->vAddedNew = Vec_IntAlloc( 100 );
     // internal data
@@ -325,20 +331,24 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
         if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) )
         {
             Gla_ManCollectFanins( p, pGla, pObj->Value, p->vTemp );
-            pGla->fConst  = Gia_ObjIsConst0(pObj);
             pGla->nFanins = Vec_IntSize( p->vTemp );
             memcpy( pGla->Fanins, Vec_IntArray(p->vTemp), sizeof(int) * Vec_IntSize(p->vTemp) );
             continue;
         }
         assert( Gia_ObjIsRo(p->pGia, pObj) );
-        pGla->nFanins = 1;
+        pGla->nFanins   = 1;
         pGla->Fanins[0] = Gia_ObjFanin0( Gia_ObjRoToRi(p->pGia, pObj) )->Value;
-        pGla->fCompl0  = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
+        pGla->fCompl0   = Gia_ObjFaninC0( Gia_ObjRoToRi(p->pGia, pObj) );
     }
     // abstraction 
     assert( pGia->vGateClasses != NULL );
-    for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
-        pGla->fAbs = (Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 1);
+    Gla_ManForEachObj( p, pGla )
+    {
+        if ( Vec_IntEntry( pGia->vGateClasses, pGla->iGiaObj ) == 0 )
+            continue;
+        pGla->fAbs = 1;
+        Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
+    }
     // other 
     p->vCla2Obj  = Vec_IntAlloc( 1000 );  Vec_IntPush( p->vCla2Obj, -1 );
     p->pSat      = sat_solver2_new();
@@ -360,13 +370,14 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
 void Gla_ManStop( Gla_Man_t * p )
 {
     Gla_Obj_t * pGla;
-    for ( pGla = p->pObjs + 1; pGla < p->pObjs + p->nObjs; pGla++ )
+    Gla_ManForEachObj( p, pGla )
         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 );
     ABC_FREE( p->pObjs );
     ABC_FREE( p );
 }
@@ -385,15 +396,15 @@ void Gla_ManStop( Gla_Man_t * p )
 int Gia_GlaAbsCount( Gla_Man_t * p, int fRo, int fAnd )
 {
     Gla_Obj_t * pObj;
-    int Counter = 0;
+    int i, Counter = 0;
     if ( fRo )
-        Gla_ManForEachObjAbs( p, pObj )
+        Gla_ManForEachObjAbs( p, pObj, i )
             Counter += (pObj->fRo && pObj->fAbs);
     else if ( fAnd )
-        Gla_ManForEachObjAbs( p, pObj )
+        Gla_ManForEachObjAbs( p, pObj, i )
             Counter += (pObj->fAnd && pObj->fAbs);
     else
-        Gla_ManForEachObjAbs( p, pObj )
+        Gla_ManForEachObjAbs( p, pObj, i )
             Counter += (pObj->fAbs);
     return Counter;
 }
@@ -430,9 +441,9 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
     Vec_Int_t * vRes;
     Gla_Obj_t * pObj, * pFanin;
     Gia_Obj_t * pGiaObj;
-    int k;
+    int i, k;
     vRes = Vec_IntStart( Gia_ManObjNum(p->pGia) );
-    Gla_ManForEachObjAbs( p, pObj )
+    Gla_ManForEachObjAbs( p, pObj, i )
     {
         Vec_IntWriteEntry( vRes, pObj->iGiaObj, 1 );
         pGiaObj = Gla_ManGiaObj( p, pObj );
@@ -463,9 +474,9 @@ Vec_Int_t * Gla_ManCollectPPis( Gla_Man_t * p )
 {
     Vec_Int_t * vPPis;
     Gla_Obj_t * pObj, * pFanin;
-    int k;
+    int i, k;
     vPPis = Vec_IntAlloc( 1000 );
-    Gla_ManForEachObjAbs( p, pObj )
+    Gla_ManForEachObjAbs( p, pObj, i )
     {
         assert( pObj->fConst || pObj->fRo || pObj->fAnd );
         Gla_ObjForEachFanin( p, pObj, pFanin, k )
@@ -484,6 +495,35 @@ int Gla_ManCountPPis( Gla_Man_t * p )
     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 )
+        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 )
+            continue;
+        Vec_IntWriteEntry( vPPis, j++, Gla_ObjId(p, pObj) );
+    }
+//    printf( "\n%d -> %d\n", Vec_IntSize(vPPis), j );
+    Vec_IntShrink( vPPis, j );
+}
+
 
 /**Function*************************************************************
 
@@ -514,10 +554,6 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
 {
     Gla_Obj_t * pGlaObj = Gla_ManObj( p, iObj );
     int iVar, iVar1, iVar2;
-    if ( iObj == 4753 )
-    {
-        int s = 0;
-    }
     if ( pGlaObj->fConst )
     {
         iVar = Gla_ManGetVar( p, iObj, iFrame );
@@ -538,9 +574,6 @@ void Gla_ManAddClauses( Gla_Man_t * p, int iObj, int iFrame, Vec_Int_t * vLits )
         else
         {
             iVar1 = Gla_ManGetVar( p, iObj, iFrame );
-//            pGlaObj = Gla_ManObj( p, pGlaObj->Fanins[0] );
-//            assert( pGlaObj->fRo && pGlaObj->nFanins == 1 );
-//            assert( Vec_IntSize(&pGlaObj->vFrames) == 0 );
             iVar2 = Gla_ManGetVar( p, pGlaObj->Fanins[0], iFrame-1 );
             sat_solver2_add_buffer( p->pSat, iVar1, iVar2, pGlaObj->fCompl0, 0 );
             // remember the clause
@@ -576,16 +609,17 @@ void Gia_GlaAddToAbs( Gla_Man_t * p, Vec_Int_t * vAbsAdd, int fCheck )
     Gla_ManForEachObjAbsVec( vAbsAdd, p, pGla, i )
     {
         assert( !fCheck || pGla->fAbs == 0 );
+        if ( pGla->fAbs )
+            continue;
         pGla->fAbs = 1;
-        // remember the change
-        Vec_IntPush( p->vAddedNew, Gla_ObjId(p, pGla) );
-        Vec_IntPush( p->vAddedNew, -1 );
+        Vec_IntPush( p->vAbs, Gla_ObjId(p, pGla) );
     }
 }
 void Gia_GlaAddTimeFrame( Gla_Man_t * p, int f )
 {
     Gla_Obj_t * pObj;
-    Gla_ManForEachObjAbs( p, pObj )
+    int i;
+    Gla_ManForEachObjAbs( p, pObj, i )
         Gla_ManAddClauses( p, Gla_ObjId(p, pObj), f, p->vTemp );
     sat_solver2_simplify( p->pSat );
 }
@@ -602,17 +636,15 @@ void Gla_ManRollBack( Gla_Man_t * p )
     int i, iObj, iFrame;
     Vec_IntForEachEntryDouble( p->vAddedNew, iObj, iFrame, i )
     {
-        if ( iFrame == -1 )
-        {
-            assert( Gla_ManObj(p, iObj)->fAbs == 1 );
-            Gla_ManObj(p, iObj)->fAbs = 0;
-        }
-        else
-        {
-            assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
-            Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
-        }
+        assert( Vec_IntEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame ) > 0 );
+        Vec_IntWriteEntry( &Gla_ManObj(p, iObj)->vFrames, iFrame, 0 );
     }
+    Vec_IntForEachEntryStart( p->vAbs, iObj, i, p->nAbsOld )
+    {
+        assert( Gla_ManObj( p, iObj )->fAbs == 1 );
+        Gla_ManObj( p, iObj )->fAbs = 0;
+    }
+    Vec_IntShrink( p->vAbs, p->nAbsOld );
 }
 
 
@@ -708,6 +740,7 @@ Vec_Int_t * Gla_ManUnsatCore( Gla_Man_t * p, int f, Vec_Int_t * vCla2Obj, sat_so
 void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfls, int nCexes, int Time )
 {
     Abc_Print( 1, "%3d :", nFrames-1 );
+    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Gia_GlaAbsCount(p, 0, 0) / (p->nObjs - Gia_ManPoNum(p->pGia) + Gia_ManCoNum(p->pGia) + 1)) ); 
     Abc_Print( 1, "%6d", Gia_GlaAbsCount(p, 0, 0) );
     Abc_Print( 1, "%5d", Gla_ManCountPPis(p) );
     Abc_Print( 1, "%5d", Gia_GlaAbsCount(p, 1, 0) );
@@ -737,6 +770,7 @@ void Gla_ManReportMemory( Gla_Man_t * p )
     memOth += Vec_IntCap(p->vCla2Obj) * sizeof(int);
     memOth += Vec_IntCap(p->vAddedNew) * 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 );
@@ -791,6 +825,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
 ***********************************************************************/
 int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 {
+    extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
     Gla_Man_t * p;
     Vec_Int_t * vCore, * vPPis;
     Abc_Cex_t * pCex = NULL;
@@ -799,8 +834,30 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     // preconditions
     assert( Gia_ManPoNum(pAig) == 1 );
     assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
+    // compute intial abstraction
+    if ( pAig->vGateClasses == NULL )
+    {
+        int nFramesMaxOld   = pPars->nFramesMax;
+        int nFramesStartOld = pPars->nFramesStart;
+        int nTimeOutOld     = pPars->nTimeOut;
+        pPars->nFramesMax   = pPars->nFramesStart;
+        pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
+        pPars->nTimeOut     = 10;
+        RetValue = Gia_VtaPerformInt( pAig, pPars );
+        pPars->nFramesMax   = nFramesMaxOld;
+        pPars->nFramesStart = nFramesStartOld;
+        pPars->nTimeOut     = nTimeOutOld;
+        // create gate classes
+        Vec_IntFreeP( &pAig->vGateClasses );
+        pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
+        Vec_IntFreeP( &pAig->vObjClasses );
+    }
+    if ( RetValue == 0 )
+        return RetValue;
     // start the manager
+    clk = clock();
     p = Gla_ManStart( pAig, pPars );
+    p->timeInit = clock() - clk;
     p->pSat->fVerbose = p->pPars->fVerbose;
     sat_solver2_set_learntmax( p->pSat, pPars->nLearntMax );
     // set runtime limit
@@ -812,7 +869,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         Abc_Print( 1, "Running variable-timeframe abstraction (VTA) with the following parameters:\n" );
         Abc_Print( 1, "FrameStart = %d  FrameMax = %d  Conf = %d  Timeout = %d. RatioMin = %d %%.\n", 
             p->pPars->nFramesStart, p->pPars->nFramesMax, p->pPars->nConfLimit, p->pPars->nTimeOut, pPars->nRatioMin );
-        Abc_Print( 1, "Frame   Abs  PPI   FF   AND   Confl  Cex   Core    SatVar      Time\n" );
+        Abc_Print( 1, "Frame   %%   Abs  PPI   FF   AND   Confl  Cex   Core    SatVar     Time\n" );
     }
     for ( f = i = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
     {
@@ -824,6 +881,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
 //            sat_solver2_reducedb( p->pSat );
         sat_solver2_bookmark( p->pSat );
         Vec_IntClear( p->vAddedNew );
+        p->nAbsOld = Vec_IntSize( p->vAbs );
 //        nClaOld = Vec_IntSize( p->vCla2Obj );
         // iterate as long as there are counter-examples
         for ( i = 0; ; i++ )
@@ -847,6 +905,7 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             pCex = NULL;
 
             vPPis = Gla_ManCollectPPis( p );
+            Gla_ManExplorePPis( p, vPPis );
             Gia_GlaAddToAbs( p, vPPis, 1 );
             Gia_GlaAddOneSlice( p, f, vPPis );
             Vec_IntFree( vPPis );
@@ -947,15 +1006,14 @@ finish:
         p->pPars->iFrame = pCex->iFrame - 1;
     }
     Abc_PrintTime( 1, "Time", clock() - clk );
-
-    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex;
+    p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
+    ABC_PRTP( "Runtime: Initializing", p->timeInit,   clock() - clk );
     ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  clock() - clk );
     ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    clock() - clk );
     ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    clock() - clk );
     ABC_PRTP( "Runtime: Other       ", p->timeOther,  clock() - clk );
     ABC_PRTP( "Runtime: TOTAL       ", clock() - clk, clock() - clk );
     Gla_ManReportMemory( p );
-
     Gla_ManStop( p );
     fflush( stdout );
     return RetValue;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2b0bd0af..c6784fd6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27372,6 +27372,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_ParVta_t Pars, * pPars = &Pars;
     int c;
     Gia_VtaSetDefaultParams( pPars );
+    pPars->nFramesStart = 20;
     pPars->nLearntMax = 100000;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )