Other improvements to &vta and &gla.

4 files changed, 193 insertions, 82 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 245d7d5d..40c74d8a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -212,6 +212,7 @@ struct Gia_ParVta_t_
     int            nRatioMin;     // stop when less than this % of object is abstracted
     int            fUseTermVars;  // use terminal variables
     int            fUseRollback;  // use rollback to the starting number of frames
+    int            fPropFanout;   // propagate fanout implications
     int            fDumpVabs;     // dumps the abstracted model
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag
@@ -698,7 +699,7 @@ extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 extern int                 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf );
 extern int                 Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver );
 /*=== giaAbsGla.c ===========================================================*/
-extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars );
+extern int                 Gia_GlaPerform( Gia_Man_t * p, Gia_ParVta_t * pPars, int fStartVta );
 /*=== giaAbsVta.c ===========================================================*/
 extern void                Gia_VtaSetDefaultParams( Gia_ParVta_t * p );
 extern Vec_Ptr_t *         Gia_VtaAbsToFrames( Vec_Int_t * vAbs );
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 815111b9..53c95650 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -74,6 +74,7 @@ struct Gla_Man_t_
     int            nAbsOld;         // previous abstraction
     // other data
     int            nCexes;          // the number of counter-examples
+    int            nObjAdded;       // total number of objects added
     int            nSatVars;        // the number of SAT variables
     Cnf_Dat_t *    pCnf;            // CNF derived for the nodes
     sat_solver2 *  pSat;            // incremental SAT solver
@@ -83,7 +84,7 @@ struct Gla_Man_t_
     Vec_Int_t *    vObjCounts;      // object counters
     // refinement
     Vec_Int_t *    pvRefis;         // vectors of each object
-    Vec_Int_t *    vPrioSels;       // selected priorities
+//    Vec_Int_t *    vPrioSels;       // selected priorities
     // statistics  
     int            timeInit;
     int            timeSat;
@@ -98,13 +99,13 @@ 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;                                                                  }
+static inline Rfn_Obj_t * Gla_ObjRef( Gla_Man_t * p, Gia_Obj_t * pObj, int f ) { return (Rfn_Obj_t *)Vec_IntGetEntryP( &(p->pvRefis[Gia_ObjId(p->pGia, pObj)]), f ); }
+static inline void        Gla_ObjClearRef( Rfn_Obj_t * p )                     { *((int *)p) = 0;                                                                    }
 
 
 // iterator through abstracted objects
@@ -387,7 +388,7 @@ void Gla_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pGiaObj, Vec_Int_t *
 }
 void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int_t * vCos, Vec_Int_t * vRoAnds )
 {
-    Gla_Obj_t * pObj, * pFanin;
+    Gla_Obj_t * pObj, * pFanin; 
     Gia_Obj_t * pGiaObj;
     int i, k;
 
@@ -409,6 +410,7 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
     Vec_IntUniqify( vPis );
     Vec_IntUniqify( vPPis );
     Vec_IntSort( vCos, 0 );
+    // sorting PIs/PPIs/COs leads to refinements that are more "well-aligned"...
 
     // mark const/PIs/PPIs
     Gia_ManIncrementTravId( p->pGia );
@@ -432,6 +434,67 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
 
 /**Function*************************************************************
 
+  Synopsis    [Drive implications of the given node towards primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRefSetAndPropFanout_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
+{
+    int i, Id = Gia_ObjId(p->pGia, pObj);
+    Rfn_Obj_t * pRef0, * pRef1, * pRef = Gla_ObjRef( p, pObj, f );
+    Gia_Obj_t * pFanout;
+    int k;
+    if ( (int)pRef->Sign != Sign )
+        return;
+    assert( pRef->fVisit == 0 );
+    pRef->fVisit = 1;
+    if ( pRef->fPPi )
+    {
+        assert( (int)pRef->Prio > 0 );
+        for ( i = p->pPars->iFrame; i >= 0; i-- )
+            if ( !Gla_ObjRef(p, pObj, i)->fVisit )
+                Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
+        Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+        return;
+    }
+    if ( (Gia_ObjIsCo(pObj) && f == p->pPars->iFrame) || Gia_ObjIsPo(p->pGia, pObj) )
+        return;
+    if ( Gia_ObjIsRi(p->pGia, pObj) )
+    {
+        pFanout = Gia_ObjRiToRo(p->pGia, pObj);
+        if ( !Gla_ObjRef(p, pFanout, f+1)->fVisit )
+            Gia_ManRefSetAndPropFanout_rec( p, pFanout, f+1, vSelect, Sign );
+        return;
+    }
+    assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
+    Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k )
+    {
+//        Rfn_Obj_t * pRefF = Gla_ObjRef(p, pFanout, f);
+        if ( Gla_ObjRef(p, pFanout, f)->fVisit )
+            continue;
+        if ( Gia_ObjIsCo(pFanout) )
+        {
+            Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
+            continue;
+        } 
+        assert( Gia_ObjIsAnd(pFanout) );
+        pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pFanout), f );
+        pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pFanout), f );
+        if ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRef0->fVisit) ||
+             ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRef1->fVisit) || 
+           ( ((pRef0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRef0->fVisit) && 
+             ((pRef1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRef1->fVisit) ) )
+           Gia_ManRefSetAndPropFanout_rec( p, pFanout, f, vSelect, Sign );
+    }
+}
+ 
+/**Function*************************************************************
+
   Synopsis    [Selects assignments to be refined.]
 
   Description []
@@ -441,23 +504,30 @@ void Gla_ManCollect( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPis, Vec_Int
   SeeAlso     []
 
 ***********************************************************************/
-void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vRes, int Sign )
+void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect, int Sign )
 { 
-    int Id = Gia_ObjId(p->pGia, pObj);
-    Rfn_Obj_t * pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );
+    int i, Id = Gia_ObjId(p->pGia, pObj);
+    Rfn_Obj_t * pRef = Gla_ObjRef( p, pObj, f );
     assert( (int)pRef->Sign == Sign );
     if ( pRef->fVisit )
         return;
-    pRef->fVisit = 1;
+    if ( p->pPars->fPropFanout )
+        Gia_ManRefSetAndPropFanout_rec( p, pObj, f, vSelect, Sign );
+    else
+        pRef->fVisit = 1;
     if ( pRef->fPPi )
     {
         assert( (int)pRef->Prio > 0 );
-        assert( (int)pRef->Prio < Vec_IntSize(p->vPrioSels) );
-        Vec_IntAddToEntry( p->vObjCounts, f, 1 );
-        if ( Vec_IntEntry( p->vPrioSels, pRef->Prio ) == 0 ) // not selected yet
+        if ( p->pPars->fPropFanout )
         {
-            Vec_IntWriteEntry( p->vPrioSels, pRef->Prio, 1 );
-            Vec_IntPush( vRes, Gia_ObjId(p->pGia, pObj) );
+            for ( i = p->pPars->iFrame; i >= 0; i-- )
+                if ( !Gla_ObjRef(p, pObj, i)->fVisit )
+                    Gia_ManRefSetAndPropFanout_rec( p, pObj, i, vSelect, Sign );
+        }
+        else
+        {
+            Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+            Vec_IntAddToEntry( p->vObjCounts, f, 1 );
         }
         return;
     }
@@ -466,19 +536,19 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
     if ( Gia_ObjIsRo(p->pGia, pObj) )
     {
         if ( f > 0 )
-            Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vRes, Sign );
+            Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vSelect, Sign );
         return;
     }
     if ( Gia_ObjIsAnd(pObj) )
     {
-        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 );
+        Rfn_Obj_t * pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
+        Rfn_Obj_t * pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
         if ( pRef->Value == 1 )
         {
             if ( pRef0->Prio > 0 )
-                Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+                Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
             if ( pRef1->Prio > 0 )
-                Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+                Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
         }
         else // select one value
         {
@@ -487,23 +557,23 @@ void Gla_ManRefSelect_rec( Gla_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * v
                 if ( pRef0->Prio <= pRef1->Prio ) // choice
                 {
                     if ( pRef0->Prio > 0 )
-                        Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+                        Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
                 }
                 else
                 {
                     if ( pRef1->Prio > 0 )
-                        Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+                        Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
                 }
             }
             else if ( (pRef0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
             {
                 if ( pRef0->Prio > 0 )
-                    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vRes, Sign );
+                    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(pObj), f, vSelect, Sign );
             }
             else if ( (pRef1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
             {
                 if ( pRef1->Prio > 0 )
-                    Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vRes, Sign );
+                    Gla_ManRefSelect_rec( p, Gia_ObjFanin1(pObj), f, vSelect, Sign );
             }
             else assert( 0 );
         }
@@ -540,14 +610,13 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
                 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_ObjTerSimSetX( pObj );
+        Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
+            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) )
@@ -575,6 +644,7 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
         Gia_ObjTerSimSetC( pObj );
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs refinement.]
@@ -590,7 +660,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
 {
     int fVerify = 1;
     static int Sign = 0;
-    Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vRes = NULL;
+    Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vSelect = NULL;
     Rfn_Obj_t * pRef, * pRef0, * pRef1;
     Gia_Obj_t * pObj;
     int i, f;
@@ -626,7 +696,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
     for ( f = 0; f <= p->pPars->iFrame; f++ )
     {
         // constant
-        pRef = Gla_ObjRef( p, 0, f );  Gla_ObjClearRef( pRef );
+        pRef = Gla_ObjRef( p, Gia_ManConst0(p->pGia), f );  Gla_ObjClearRef( pRef );
         pRef->Value  = 0;
         pRef->Prio   = 0;
         pRef->Sign   = Sign;
@@ -634,7 +704,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
         Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
         {
 //            assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
-            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );   Gla_ObjClearRef( pRef );
+            pRef = Gla_ObjRef( p, pObj, f );   Gla_ObjClearRef( pRef );
             pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
             pRef->Prio  = 0;
             pRef->Sign  = Sign;
@@ -645,7 +715,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
         {
 //            assert( f == p->pPars->iFrame || Gla_ManCheckVar(p, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)], f) );
             assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
-            pRef = Gla_ObjRef( p, Gia_ObjId(p->pGia, pObj), f );   Gla_ObjClearRef( pRef );
+            pRef = Gla_ObjRef( p, pObj, f );   Gla_ObjClearRef( pRef );
             pRef->Value = Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f );
             pRef->Prio  = i+1;
             pRef->fPPi  = 1;
@@ -656,7 +726,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
         Gia_ManForEachObjVec( vRoAnds, 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 = Gla_ObjRef( p, pObj, f );   Gla_ObjClearRef( pRef );
             if ( Gia_ObjIsRo(p->pGia, pObj) )
             {
                 if ( f == 0 )
@@ -667,7 +737,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
                 }
                 else
                 {
-                    pRef0 = Gla_ObjRef( p, Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj)), f-1 );
+                    pRef0 = Gla_ObjRef( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
                     pRef->Value = pRef0->Value;
                     pRef->Prio  = pRef0->Prio;
                     pRef->Sign  = Sign;
@@ -675,8 +745,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
                 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 );
+            pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f );
+            pRef1 = Gla_ObjRef( p, Gia_ObjFanin1(pObj), f );
             pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj)) & (pRef1->Value ^ Gia_ObjFaninC1(pObj));
 
             if ( p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] != ~0 && 
@@ -701,8 +771,8 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
         // 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 = Gla_ObjRef( p, pObj, f );    Gla_ObjClearRef( pRef );
+            pRef0 = Gla_ObjRef( p, Gia_ObjFanin0(pObj), f ); 
             pRef->Value = (pRef0->Value ^ Gia_ObjFaninC0(pObj));
             pRef->Prio  = pRef0->Prio;
             assert( pRef->fVisit == 0 );
@@ -712,7 +782,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
 
     // 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 );
+    pRef = Gla_ObjRef( p, pObj, p->pPars->iFrame );
     if ( pRef->Value != 1 )
         printf( "\nCounter-example verification has failed!!!\n" );
 
@@ -728,27 +798,33 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
     }
 
     // select objects
-    vRes = Vec_IntAlloc( 100 );
-    Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
+    vSelect = Vec_IntAlloc( 100 );
+//    Vec_IntFill( p->vPrioSels, Vec_IntSize(vPPis)+1, 0 );
     Vec_IntFill( p->vObjCounts, p->pPars->iFrame+1, 0 );
-    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vRes, Sign );
+    Gla_ManRefSelect_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), p->pPars->iFrame, vSelect, Sign );
+    Vec_IntUniqify( vSelect );
+
+//    printf( "\nSelected %d.\n", Vec_IntSize(vSelect) );
+
 /*
     for ( f = 0; f < p->pPars->iFrame; f++ )
         printf( "%2d", Vec_IntEntry(p->vObjCounts, f) );
     printf( "\n" );
 */
     if ( fVerify )
-        Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vRes );
+        Gla_ManVerifyUsingTerSim( p, vPis, vPPis, vRoAnds, vCos, vSelect );
 
     // remap them into GLA objects
-    Gia_ManForEachObjVec( vRes, p->pGia, pObj, i )
-        Vec_IntWriteEntry( vRes, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
+    Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i )
+        Vec_IntWriteEntry( vSelect, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
 
     Vec_IntFree( vPis );
     Vec_IntFree( vPPis );
     Vec_IntFree( vRoAnds );
     Vec_IntFree( vCos );
-    return vRes;
+
+    p->nObjAdded += Vec_IntSize(vSelect);
+    return vSelect;
 }
 
 
@@ -888,7 +964,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     p->vAbs  = Vec_IntAlloc( 100 );
     p->vTemp = Vec_IntAlloc( 100 );
     p->vAddedNew = Vec_IntAlloc( 100 );
-    p->vPrioSels = Vec_IntAlloc( 100 );
+//    p->vPrioSels = Vec_IntAlloc( 100 );
     p->vObjCounts = Vec_IntAlloc( 100 );
 
     // internal data
@@ -897,6 +973,8 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     Aig_ManStop( pAig );
     // create working GIA
     p->pGia = Gia_ManDupMapped( pGia0, p->pCnf->vMapping );
+    if ( pPars->fPropFanout )
+        Gia_ManStaticFanoutStart( p->pGia );
 //printf( "Old GIA = %d.  New GIA = %d.\n", Gia_ManObjNum(pGia0), Gia_ManObjNum(p->pGia) );
 
     // derive new gate map
@@ -1051,7 +1129,7 @@ Gla_Man_t * Gla_ManStart2( 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 );
+//    p->vPrioSels = Vec_IntAlloc( 100 );
     // internal data
     pAig = Gia_ManToAigSimple( p->pGia );
     p->pCnf  = Cnf_DeriveOther( pAig, 1 );
@@ -1136,8 +1214,8 @@ void Gla_ManStop( Gla_Man_t * p )
     Gla_Obj_t * pGla;
     int i;
 //    if ( p->pPars->fVerbose )
-        Abc_Print( 1, "SAT solver:  Variables = %d. Clauses = %d. Conflicts = %d. Cexes = %d.\n", 
-            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes );
+        Abc_Print( 1, "SAT solver:  Vars = %d. Clauses = %d. Confs = %d. Cexes = %d. ObjAdded = %d\n", 
+            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->nCexes, p->nObjAdded );
     for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
         ABC_FREE( p->pvRefis[i].pArray );
     Gla_ManForEachObj( p, pGla )
@@ -1145,11 +1223,12 @@ void Gla_ManStop( Gla_Man_t * p )
     Cnf_DataFree( p->pCnf );
     if ( p->pGia0 != NULL )
         Gia_ManStop( p->pGia );
+//    Gia_ManStaticFanoutStart( p->pGia0 );
     sat_solver2_delete( p->pSat );
     Vec_IntFreeP( &p->vObjCounts );
     Vec_IntFreeP( &p->vCla2Obj );
     Vec_IntFreeP( &p->vAddedNew );
-    Vec_IntFreeP( &p->vPrioSels );
+//    Vec_IntFreeP( &p->vPrioSels );
     Vec_IntFreeP( &p->vTemp );
     Vec_IntFreeP( &p->vAbs );
     ABC_FREE( p->pvRefis );
@@ -1563,7 +1642,7 @@ void Gla_ManReportMemory( Gla_Man_t * p )
     double memSat = sat_solver2_memory( p->pSat );
     double memPro = sat_solver2_memory_proof( p->pSat );
     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 memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t);
     double memOth = sizeof(Gla_Man_t);
     for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
         memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
@@ -1625,7 +1704,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
+int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
 {
     extern int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars );
     Gla_Man_t * p;
@@ -1636,30 +1715,41 @@ 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;
-        int nDumpOld        = pPars->fDumpVabs;
-        pPars->nFramesMax   = pPars->nFramesStart;
-        pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
-        pPars->nTimeOut     = 20;
-        pPars->fDumpVabs    = 0;
-        RetValue = Gia_VtaPerformInt( pAig, pPars );
-        pPars->nFramesMax   = nFramesMaxOld;
-        pPars->nFramesStart = nFramesStartOld;
-        pPars->nTimeOut     = nTimeOutOld;
-        pPars->fDumpVabs    = nDumpOld;
-        // create gate classes
-        Vec_IntFreeP( &pAig->vGateClasses );
-        if ( pAig->vObjClasses )
-            pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
-        Vec_IntFreeP( &pAig->vObjClasses );
+        if ( fStartVta )
+        {
+            int nFramesMaxOld   = pPars->nFramesMax;
+            int nFramesStartOld = pPars->nFramesStart;
+            int nTimeOutOld     = pPars->nTimeOut;
+            int nDumpOld        = pPars->fDumpVabs;
+            pPars->nFramesMax   = pPars->nFramesStart;
+            pPars->nFramesStart = Abc_MinInt( pPars->nFramesStart/2 + 1, 3 );
+            pPars->nTimeOut     = 20;
+            pPars->fDumpVabs    = 0;
+            RetValue = Gia_VtaPerformInt( pAig, pPars );
+            pPars->nFramesMax   = nFramesMaxOld;
+            pPars->nFramesStart = nFramesStartOld;
+            pPars->nTimeOut     = nTimeOutOld;
+            pPars->fDumpVabs    = nDumpOld;
+            // create gate classes
+            Vec_IntFreeP( &pAig->vGateClasses );
+            if ( pAig->vObjClasses )
+                pAig->vGateClasses = Gia_VtaConvertToGla( pAig, pAig->vObjClasses );
+            Vec_IntFreeP( &pAig->vObjClasses );
+            // return if VTA solve the problem if could not start
+            if ( RetValue == 0 || pAig->vGateClasses == NULL )
+                return RetValue;
+        }
+        else
+        {
+            pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+            Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+            Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
+        }
     }
-    if ( RetValue == 0 || pAig->vGateClasses == NULL )
-        return RetValue;
     // start the manager
     clk = clock();
     p = Gla_ManStart( pAig, pPars );
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 40e5a45c..c6f5e238 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -126,7 +126,7 @@ static inline int          Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert
 // - the first entry is the number of timeframes (F)
 // - the next (F+1) entries give the beginning position of each timeframe
 // - the following entries give the object IDs
-// invariant:  assert( vec[vec[0]+2] == size(vec) );
+// invariant:  assert( vec[vec[0]+1] == size(vec) );
 
 extern void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame );
 
@@ -1624,6 +1624,18 @@ int Gia_VtaPerformInt( 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->vObjClasses == NULL )
+    {
+        pAig->vObjClasses = Vec_IntAlloc( 5 );
+        Vec_IntPush( pAig->vObjClasses, 1 );
+        Vec_IntPush( pAig->vObjClasses, 3 );
+        Vec_IntPush( pAig->vObjClasses, 4 );
+        Vec_IntPush( pAig->vObjClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) );
+    }
+*/
     // start the manager
     p = Vga_ManStart( pAig, pPars );
     p->pSat->fVerbose = p->pPars->fVerbose;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9167c54c..d1c1e5a9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27382,12 +27382,12 @@ usage:
 int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_ParVta_t Pars, * pPars = &Pars;
-    int c;
+    int c, fStartVta = 0;
     Gia_VtaSetDefaultParams( pPars );
     pPars->nFramesStart = 30;
     pPars->nLearntMax   = 100000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSPCLTRAtrfdavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27483,9 +27483,15 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fUseRollback ^= 1;
             break;
+        case 'f':
+            pPars->fPropFanout ^= 1;
+            break;
         case 'd':
             pPars->fDumpVabs ^= 1;
             break;
+        case 'a':
+            fStartVta ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -27525,14 +27531,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The starting frame should be 1 or larger.\n" );
         return 0;
     }
-    pAbc->Status  = Gia_GlaPerform( pAbc->pGia, pPars );
+    pAbc->Status  = Gia_GlaPerform( pAbc->pGia, pPars, fStartVta );
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-dvh]\n" );
-    Abc_Print( -2, "\t          refines abstracted object map with proof-based abstraction\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLTR num] [-A file] [-fdavh]\n" );
+    Abc_Print( -2, "\t          performs gate-level abstraction of a sequential miter\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
 //    Abc_Print( -2, "\t-P num  : the number of previous frames for UNSAT core [default = %d]\n", pPars->nFramesPast );
@@ -27543,7 +27549,9 @@ usage:
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
 //    Abc_Print( -2, "\t-t      : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
 //    Abc_Print( -2, "\t-r      : toggle using rollback after the starting frames [default = %s]\n", pPars->fUseRollback? "yes": "no" );
+    Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-d      : toggle dumping abstracted model into a file [default = %s]\n", pPars->fDumpVabs? "yes": "no" );
+    Abc_Print( -2, "\t-a      : toggle using VTA to kick start GLA [default = %s]\n", fStartVta? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;