Supporting edges in delay-optimization in &satlut.

7 files changed, 568 insertions, 151 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 274b9314..8c282a51 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1009,6 +1009,8 @@ static inline int         Gia_ObjCellId( Gia_Man_t * p, int iLit )          { re
 
 #define Gia_ManForEachLut( p, i )                                       \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut(p, i) ) {} else
+#define Gia_ManForEachLutReverse( p, i )                                \
+    for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsLut(p, i) ) {} else
 #define Gia_LutForEachFanin( p, i, iFan, k )                            \
     for ( k = 0; k < Gia_ObjLutSize(p,i) && ((iFan = Gia_ObjLutFanins(p,i)[k]),1); k++ )
 #define Gia_LutForEachFaninObj( p, i, pFanin, k )                       \
@@ -1147,6 +1149,8 @@ extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNo
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern Vec_Vec_t *         Gia_ManLevelize( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManOrderReverse( Gia_Man_t * p );
+extern void                Gia_ManCollectTfi( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes );
+extern void                Gia_ManCollectTfo( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes );
 /*=== giaDup.c ============================================================*/
 extern void                Gia_ManDupRemapLiterals( Vec_Int_t * vLits, Gia_Man_t * p );
 extern void                Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p );
@@ -1206,9 +1210,13 @@ extern Gia_Man_t *         Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax );
 /*=== giaEdge.c ==========================================================*/
 extern void                Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray );
 extern Vec_Int_t *         Gia_ManEdgeToArray( Gia_Man_t * p );
+extern void                Gia_ManConvertPackingToEdges( Gia_Man_t * p );
 extern int                 Gia_ManEvalEdgeDelay( Gia_Man_t * p );
+extern int                 Gia_ManEvalEdgeCount( Gia_Man_t * p );
 extern int                 Gia_ManComputeEdgeDelay( Gia_Man_t * p );
 extern int                 Gia_ManComputeEdgeDelay2( Gia_Man_t * p );
+extern void                Gia_ManUpdateMapping( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Wec_t * vWin );
+extern int                 Gia_ManEvalWindow( Gia_Man_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Wec_t * vWin, Vec_Int_t * vTemp );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 504533e9..a6ea9322 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -762,8 +762,13 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
                 for ( i = 0; i < 2*nPairs; i++ )
                     Vec_IntPush( vPairs, Gia_AigerReadInt(pCur) ),      pCur += 4;
                 assert( pCur == pCurTemp );
-                if ( fVerbose ) printf( "Finished reading extension \"w\".\n" );
-                Gia_ManEdgeFromArray( pNew, vPairs );
+                if ( fSkipStrash )
+                {
+                    Gia_ManEdgeFromArray( pNew, vPairs );
+                    if ( fVerbose ) printf( "Finished reading extension \"w\".\n" );
+                }
+                else
+                    printf( "Cannot read extension \"w\" because AIG is rehashed. Use \"&r -s <file.aig>\".\n" );
                 Vec_IntFree( vPairs );
             }
             else break;
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 0dd0ac8e..60edef81 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -505,6 +505,74 @@ void Gia_ManCollectSeqTest( Gia_Man_t * p )
 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect TFI nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCollectTfi_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes )
+{
+    Gia_Obj_t * pObj;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManCollectTfi_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes );
+    Gia_ManCollectTfi_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes );
+    Vec_IntPush( vNodes, iObj );
+}
+void Gia_ManCollectTfi( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes )
+{
+    int i, iRoot; 
+    Vec_IntClear( vNodes );
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vRoots, iRoot, i )
+        Gia_ManCollectTfi_rec( p, iRoot, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect TFI nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCollectTfo_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes )
+{
+    Gia_Obj_t * pObj; int i, iFan;
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsCo(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i )
+        Gia_ManCollectTfo_rec( p, iFan, vNodes );
+    Vec_IntPush( vNodes, iObj );
+}
+void Gia_ManCollectTfo( Gia_Man_t * p, Vec_Int_t * vRoots, Vec_Int_t * vNodes )
+{
+    int i, iRoot; 
+    Vec_IntClear( vNodes );
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vRoots, iRoot, i )
+        Gia_ManCollectTfo_rec( p, iRoot, vNodes );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaEdge.c b/src/aig/gia/giaEdge.c
index 93624fdf..f67f0b3c 100644
--- a/src/aig/gia/giaEdge.c
+++ b/src/aig/gia/giaEdge.c
@@ -26,17 +26,31 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int Sbm_ObjEdgeCount( int iObj, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
+static inline int Gia_ObjEdgeCount( int iObj, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
 {
     return (Vec_IntEntry(vEdge1, iObj) > 0) + (Vec_IntEntry(vEdge2, iObj) > 0);
 }
-static inline void Sbm_ObjEdgeAdd( int iObj, int iNext, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
+static inline int Gia_ObjEdgeAdd( int iObj, int iNext, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
 {
+    int RetValue = 0;
     if ( Vec_IntEntry(vEdge1, iObj) == 0 )
         Vec_IntWriteEntry(vEdge1, iObj, iNext);
     else if ( Vec_IntEntry(vEdge2, iObj) == 0 )
         Vec_IntWriteEntry(vEdge2, iObj, iNext);
-    else assert( 0 );
+    else RetValue = 1;
+    return RetValue;
+}
+static inline void Gia_ObjEdgeRemove( int iObj, int iNext, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
+{
+    assert( Vec_IntEntry(vEdge1, iObj) == iNext || Vec_IntEntry(vEdge2, iObj) == iNext );
+    if ( Vec_IntEntry(vEdge1, iObj) == iNext )
+        Vec_IntWriteEntry( vEdge1, iObj, Vec_IntEntry(vEdge2, iObj) );
+    Vec_IntWriteEntry( vEdge2, iObj, 0 );
+}
+static inline void Gia_ObjEdgeClean( int iObj, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
+{
+    Vec_IntWriteEntry( vEdge1, iObj, 0 );
+    Vec_IntWriteEntry( vEdge2, iObj, 0 );
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -58,37 +72,86 @@ void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray )
 {
     int i, iObj1, iObj2;
     Vec_IntFreeP( &p->vEdge1 );
-    Vec_IntFreeP( &p->vEdge1 );
+    Vec_IntFreeP( &p->vEdge2 );
     p->vEdge1 = Vec_IntStart( Gia_ManObjNum(p) );
     p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) );
     Vec_IntForEachEntryDouble( vArray, iObj1, iObj2, i )
     {
-        assert( iObj1 != iObj2 );
-        Sbm_ObjEdgeAdd( iObj1, iObj2, p->vEdge1, p->vEdge2 );
-        Sbm_ObjEdgeAdd( iObj2, iObj1, p->vEdge1, p->vEdge2 );
+        assert( iObj1 < iObj2 );
+        Gia_ObjEdgeAdd( iObj1, iObj2, p->vEdge1, p->vEdge2 );
+        Gia_ObjEdgeAdd( iObj2, iObj1, p->vEdge1, p->vEdge2 );
     }
 }
 Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p )
 {
-    int i, Entry;
+    int iObj, iFanin;
     Vec_Int_t * vArray = Vec_IntAlloc( 1000 );
     assert( p->vEdge1 && p->vEdge2 );
     assert( Vec_IntSize(p->vEdge1) == Gia_ManObjNum(p) );
     assert( Vec_IntSize(p->vEdge2) == Gia_ManObjNum(p) );
-    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    for ( iObj = 0; iObj < Gia_ManObjNum(p); iObj++ )
     {
-        Entry = Vec_IntEntry(p->vEdge1, i);
-        if ( Entry && Entry < i )
-            Vec_IntPushTwo( vArray, Entry, i );
-        Entry = Vec_IntEntry(p->vEdge2, i);
-        if ( Entry && Entry < i )
-            Vec_IntPushTwo( vArray, Entry, i );
+        iFanin = Vec_IntEntry( p->vEdge1, iObj );
+        if ( iFanin && iFanin < iObj )
+            Vec_IntPushTwo( vArray, iFanin, iObj );
+        iFanin = Vec_IntEntry( p->vEdge2, iObj );
+        if ( iFanin && iFanin < iObj )
+            Vec_IntPushTwo( vArray, iFanin, iObj );
     }
     return vArray;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Prints mapping statistics.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManConvertPackingToEdges( Gia_Man_t * p )
+{
+    int i, k, Entry, nEntries, nEntries2, nNodes[4], Count = 0;
+    if ( p->vPacking == NULL )
+        return;
+    Vec_IntFreeP( &p->vEdge1 );
+    Vec_IntFreeP( &p->vEdge2 );
+    p->vEdge1 = Vec_IntStart( Gia_ManObjNum(p) );
+    p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) );
+    // iterate through structures
+    nEntries = Vec_IntEntry( p->vPacking, 0 );
+    nEntries2 = 0;
+    Vec_IntForEachEntryStart( p->vPacking, Entry, i, 1 )
+    {
+        assert( Entry > 0 && Entry < 4 );
+        i++;
+        for ( k = 0; k < Entry; k++, i++ )
+            nNodes[k] = Vec_IntEntry(p->vPacking, i);
+        i--;
+        nEntries2++;
+        // create edges
+        if ( Entry == 2 )
+        {
+            Count += Gia_ObjEdgeAdd( nNodes[0], nNodes[1], p->vEdge1, p->vEdge2 );
+            Count += Gia_ObjEdgeAdd( nNodes[1], nNodes[0], p->vEdge1, p->vEdge2 );
+        }
+        else if ( Entry == 3 )
+        {
+            Count += Gia_ObjEdgeAdd( nNodes[0], nNodes[2], p->vEdge1, p->vEdge2 );
+            Count += Gia_ObjEdgeAdd( nNodes[2], nNodes[0], p->vEdge1, p->vEdge2 );
+            Count += Gia_ObjEdgeAdd( nNodes[1], nNodes[2], p->vEdge1, p->vEdge2 );
+            Count += Gia_ObjEdgeAdd( nNodes[2], nNodes[1], p->vEdge1, p->vEdge2 );
+        }
+    }
+    assert( nEntries == nEntries2 );
+    printf( "Skipped %d illegal edges.\n", Count );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Evaluates given edge assignment.]
 
   Description []
@@ -105,13 +168,25 @@ static inline int Gia_ObjHaveEdge( Gia_Man_t * p, int iObj, int iNext )
 static inline int Gia_ObjEvalEdgeDelay( Gia_Man_t * p, int iObj, Vec_Int_t * vDelay )
 {
     int i, iFan, Delay, DelayMax = 0;
-    assert( Gia_ObjIsLut(p, iObj) );
-    assert( Gia_ObjLutSize(p, iObj) <= 4 );
-    Gia_LutForEachFanin( p, iObj, iFan, i )
+    if ( Gia_ManHasMapping(p) && Gia_ObjIsLut(p, iObj) )
     {
-        Delay = Vec_IntEntry(vDelay, iFan) + !Gia_ObjHaveEdge(p, iObj, iFan);
-        DelayMax = Abc_MaxInt( DelayMax, Delay );
+        assert( Gia_ObjLutSize(p, iObj) <= 4 );
+        Gia_LutForEachFanin( p, iObj, iFan, i )
+        {
+            Delay = Vec_IntEntry(vDelay, iFan) + !Gia_ObjHaveEdge(p, iObj, iFan);
+            DelayMax = Abc_MaxInt( DelayMax, Delay );
+        }
+    }
+    else if ( Gia_ObjIsLut2(p, iObj) )
+    {
+        assert( Gia_ObjLutSize2(p, iObj) <= 4 );
+        Gia_LutForEachFanin2( p, iObj, iFan, i )
+        {
+            Delay = Vec_IntEntry(vDelay, iFan) + !Gia_ObjHaveEdge(p, iObj, iFan);
+            DelayMax = Abc_MaxInt( DelayMax, Delay );
+        }
     }
+    else assert( 0 );
     return DelayMax;
 }
 int Gia_ManEvalEdgeDelay( Gia_Man_t * p )
@@ -120,12 +195,21 @@ int Gia_ManEvalEdgeDelay( Gia_Man_t * p )
     assert( p->vEdge1 && p->vEdge2 );
     Vec_IntFreeP( &p->vEdgeDelay );
     p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) );
-    Gia_ManForEachLut( p, iLut )
-        Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+    if ( Gia_ManHasMapping(p) )
+        Gia_ManForEachLut( p, iLut )
+            Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+    else if ( Gia_ManHasMapping2(p) )
+        Gia_ManForEachLut2( p, iLut )
+            Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) );
+    else assert( 0 );
     Gia_ManForEachCoDriverId( p, iLut, k )
         DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) );
     return DelayMax;
 }
+int Gia_ManEvalEdgeCount( Gia_Man_t * p )
+{
+    return (Vec_IntCountPositive(p->vEdge1) + Vec_IntCountPositive(p->vEdge2))/2;
+}
 
 
 /**Function*************************************************************
@@ -141,74 +225,106 @@ int Gia_ManEvalEdgeDelay( Gia_Man_t * p )
 ***********************************************************************/
 int Gia_ObjComputeEdgeDelay( Gia_Man_t * p, int iObj, Vec_Int_t * vDelay, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2 )
 {
-    int i, iFan, Status[4], Delay[4];
+    int i, iFan, Delay, Status1, Status2;
     int DelayMax = 0, nCountMax = 0;
     int iFanMax1 = -1, iFanMax2 = -1;
-    int iMax1 = -1, iMax2 = -1; 
-    assert( Gia_ObjIsLut(p, iObj) );
-    assert( Gia_ObjLutSize(p, iObj) <= 4 );
     Vec_IntWriteEntry(vEdge1, iObj, 0);
     Vec_IntWriteEntry(vEdge2, iObj, 0);
-    Gia_LutForEachFanin( p, iObj, iFan, i )
+    if ( Gia_ManHasMapping(p) && Gia_ObjIsLut(p, iObj) )
     {
-        Status[i] = Sbm_ObjEdgeCount( iFan, vEdge1, vEdge2 );
-        Delay[i]  = Vec_IntEntry( vDelay, iFan ) + 1;
-        if ( DelayMax < Delay[i] )
+        assert( Gia_ObjLutSize(p, iObj) <= 4 );
+        Gia_LutForEachFanin( p, iObj, iFan, i )
         {
-            DelayMax  = Delay[i];
-            iFanMax1  = iFan;
-            iMax1     = i;
-            nCountMax = 1;
+            Delay = Vec_IntEntry( vDelay, iFan ) + 1;
+            if ( DelayMax < Delay )
+            {
+                DelayMax  = Delay;
+                iFanMax1  = iFan;
+                nCountMax = 1;
+            }
+            else if ( DelayMax == Delay )
+            {
+                iFanMax2  = iFan;
+                nCountMax++;
+            }
         }
-        else if ( DelayMax == Delay[i] )
+    }
+    else if ( Gia_ObjIsLut2(p, iObj) )
+    {
+        assert( Gia_ObjLutSize2(p, iObj) <= 4 );
+        Gia_LutForEachFanin2( p, iObj, iFan, i )
         {
-            iFanMax2  = iFan;
-            iMax2     = i;
-            nCountMax++;
+            Delay = Vec_IntEntry( vDelay, iFan ) + 1;
+            if ( DelayMax < Delay )
+            {
+                DelayMax  = Delay;
+                iFanMax1  = iFan;
+                nCountMax = 1;
+            }
+            else if ( DelayMax == Delay )
+            {
+                iFanMax2  = iFan;
+                nCountMax++;
+            }
         }
     }
+    else assert( 0 );
     assert( nCountMax > 0 );
-    if ( nCountMax == 1 && Status[iMax1] <= 1 )
+    if ( DelayMax == 1 )
+    {} // skip first level
+    else if ( nCountMax == 1 )
     {
-        Sbm_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
-        Sbm_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
-        Vec_IntWriteEntry( vDelay, iObj, DelayMax-1 );
-        return 1;
+        Status1 = Gia_ObjEdgeCount( iFanMax1, vEdge1, vEdge2 );
+        if ( Status1 <= 1 )
+        {
+            Gia_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
+            Vec_IntWriteEntry( vDelay, iObj, DelayMax-1 );
+            return DelayMax-1;
+        }
     }
-    if ( nCountMax == 2 && Status[iMax1] <= 1 && Status[iMax2] <= 1 )
+    else if ( nCountMax == 2 )
     {
-        Sbm_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
-        Sbm_ObjEdgeAdd( iFanMax2, iObj, vEdge1, vEdge2 );
-        Sbm_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
-        Sbm_ObjEdgeAdd( iObj, iFanMax2, vEdge1, vEdge2 );
-        Vec_IntWriteEntry( vDelay, iObj, DelayMax-1 );
-        return 2;
+        Status1 = Gia_ObjEdgeCount( iFanMax1, vEdge1, vEdge2 );
+        Status2 = Gia_ObjEdgeCount( iFanMax2, vEdge1, vEdge2 );
+        if ( Status1 <= 1 && Status2 <= 1 )
+        {
+            Gia_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iFanMax2, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax2, vEdge1, vEdge2 );
+            Vec_IntWriteEntry( vDelay, iObj, DelayMax-1 );
+            return DelayMax-1;
+        }
     }
     Vec_IntWriteEntry( vDelay, iObj, DelayMax );
-    return 0;
+    return DelayMax;
 }
 int Gia_ManComputeEdgeDelay( Gia_Man_t * p )
 {
-    int k, iLut, DelayMax = 0, EdgeCount = 0;
+    int k, iLut, DelayMax = 0;
     Vec_IntFreeP( &p->vEdgeDelay );
     Vec_IntFreeP( &p->vEdge1 );
-    Vec_IntFreeP( &p->vEdge1 );
+    Vec_IntFreeP( &p->vEdge2 );
     p->vEdge1 = Vec_IntStart( Gia_ManObjNum(p) );
     p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) );
     p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) );
-    Gia_ManForEachLut( p, iLut )
-        EdgeCount += Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+    if ( Gia_ManHasMapping(p) )
+        Gia_ManForEachLut( p, iLut )
+            Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+    else if ( Gia_ManHasMapping2(p) )
+        Gia_ManForEachLut2( p, iLut )
+            Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+    else assert( 0 );
     Gia_ManForEachCoDriverId( p, iLut, k )
         DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) );
-    assert( 2 * EdgeCount == Vec_IntCountPositive(p->vEdge1) + Vec_IntCountPositive(p->vEdge2) );
-    printf( "The number of edges = %d.  ", EdgeCount );
-    printf( "Delay = %d.\n", DelayMax );
+    //printf( "The number of edges = %d.  Delay = %d.\n", Gia_ManEvalEdgeCount(p), DelayMax );
     return DelayMax;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Finds edge assignment to reduce delay.]
+  Synopsis    [Finds edge assignment.]
 
   Description []
                
@@ -217,9 +333,157 @@ int Gia_ManComputeEdgeDelay( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ObjComputeEdgeDelay2( Gia_Man_t * p, int iObj, Vec_Int_t * vDelay, Vec_Int_t * vEdge1, Vec_Int_t * vEdge2, Vec_Int_t * vFanMax1, Vec_Int_t * vFanMax2, Vec_Int_t * vCountMax )
+{
+    int i, iFan, DelayFanin, Status1, Status2;
+    int DelayMax = 0, nCountMax = 0;
+    int iFanMax1 = -1, iFanMax2 = -1;
+    Vec_IntWriteEntry(vEdge1, iObj, 0);
+    Vec_IntWriteEntry(vEdge2, iObj, 0);
+    // analyze this node
+    DelayMax = Vec_IntEntry( vDelay, iObj );
+    nCountMax = Vec_IntEntry( vCountMax, iObj );
+    if ( DelayMax == 0 )
+    {}
+    else if ( nCountMax == 1 )
+    {
+        iFanMax1 = Vec_IntEntry( vFanMax1, iObj );
+        Status1 = Gia_ObjEdgeCount( iFanMax1, vEdge1, vEdge2 );
+        if ( Status1 <= 1 )
+        {
+            Gia_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
+            DelayMax--;
+        }
+    }
+    else if ( nCountMax == 2 )
+    {
+        iFanMax1 = Vec_IntEntry( vFanMax1, iObj );
+        iFanMax2 = Vec_IntEntry( vFanMax2, iObj );
+        Status1 = Gia_ObjEdgeCount( iFanMax1, vEdge1, vEdge2 );
+        Status2 = Gia_ObjEdgeCount( iFanMax2, vEdge1, vEdge2 );
+        if ( Status1 <= 1 && Status2 <= 1 )
+        {
+            Gia_ObjEdgeAdd( iFanMax1, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iFanMax2, iObj, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax1, vEdge1, vEdge2 );
+            Gia_ObjEdgeAdd( iObj, iFanMax2, vEdge1, vEdge2 );
+            DelayMax--;
+        }
+    }
+    Vec_IntWriteEntry( vDelay, iObj, DelayMax );
+    // computed DelayMax at this point
+    if ( Gia_ManHasMapping(p) && Gia_ObjIsLut(p, iObj) )
+    {
+        Gia_LutForEachFanin( p, iObj, iFan, i )
+        {
+            DelayFanin = Vec_IntEntry( vDelay, iFan );
+            if ( DelayFanin < DelayMax + 1 )
+            {
+                Vec_IntWriteEntry( vDelay, iFan, DelayMax + 1 );
+                Vec_IntWriteEntry( vFanMax1, iFan, iObj );
+                Vec_IntWriteEntry( vCountMax, iFan, 1 );
+            }
+            else if ( DelayFanin == DelayMax + 1 )
+            {
+                Vec_IntWriteEntry( vFanMax2, iFan, iObj );
+                Vec_IntAddToEntry( vCountMax, iFan, 1 );
+            }
+        }
+    }
+    else if ( Gia_ObjIsLut2(p, iObj) )
+    {
+        Gia_LutForEachFanin2( p, iObj, iFan, i )
+        {
+            DelayFanin = Vec_IntEntry( vDelay, iFan );
+            if ( DelayFanin < DelayMax + 1 )
+            {
+                Vec_IntWriteEntry( vDelay, iFan, DelayMax + 1 );
+                Vec_IntWriteEntry( vFanMax1, iFan, iObj );
+                Vec_IntWriteEntry( vCountMax, iFan, 1 );
+            }
+            else if ( DelayFanin == DelayMax + 1 )
+            {
+                Vec_IntWriteEntry( vFanMax2, iFan, iObj );
+                Vec_IntAddToEntry( vCountMax, iFan, 1 );
+            }
+        }
+    }
+    else assert( 0 );
+    return DelayMax;
+}
 int Gia_ManComputeEdgeDelay2( Gia_Man_t * p )
 {
-    return 0;
+    int k, iLut, DelayMax = 0, EdgeCount = 0;
+    Vec_Int_t * vFanMax1 = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vFanMax2 = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vCountMax = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_IntFreeP( &p->vEdgeDelay );
+    Vec_IntFreeP( &p->vEdge1 );
+    Vec_IntFreeP( &p->vEdge2 );
+    p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) );
+    p->vEdge1 = Vec_IntStart( Gia_ManObjNum(p) );
+    p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) );
+//    Gia_ManForEachCoDriverId( p, iLut, k )
+//        Vec_IntWriteEntry( p->vEdgeDelay, iLut, 1 );
+    if ( Gia_ManHasMapping(p) )
+        Gia_ManForEachLutReverse( p, iLut )
+            Gia_ObjComputeEdgeDelay2( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2, vFanMax1, vFanMax2, vCountMax );
+    else if ( Gia_ManHasMapping2(p) )
+        Gia_ManForEachLut2Reverse( p, iLut )
+            Gia_ObjComputeEdgeDelay2( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2, vFanMax1, vFanMax2, vCountMax );
+    else assert( 0 );
+    Gia_ManForEachCiId( p, iLut, k )
+        DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) );
+    Vec_IntFree( vFanMax1 );
+    Vec_IntFree( vFanMax2 );
+    Vec_IntFree( vCountMax );
+    //printf( "The number of edges = %d.  Delay = %d.\n", Gia_ManEvalEdgeCount(p), DelayMax );
+    return DelayMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds edge assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManUpdateMapping( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Wec_t * vWin )
+{
+    int i, iNode;
+    Vec_IntForEachEntry( vNodes, iNode, i )
+        ABC_SWAP( Vec_Int_t, *Vec_WecEntry(p->vMapping2, iNode), *Vec_WecEntry(vWin, i) );
+}
+int Gia_ManEvalWindowInc( Gia_Man_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Wec_t * vWin, Vec_Int_t * vTemp )
+{
+    int i, iLut, Delay, DelayMax = 0;
+    assert( Vec_IntSize(vNodes) == Vec_WecSize(vWin) );
+    Gia_ManUpdateMapping( p, vNodes, vWin );
+    Gia_ManCollectTfo( p, vLeaves, vTemp );
+    Vec_IntReverseOrder( vTemp );
+    Vec_IntForEachEntry( vTemp, iLut, i )
+    {
+        if ( !Gia_ObjIsLut(p, iLut) )
+            continue;
+        Delay = Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 );
+        DelayMax = Abc_MaxInt( DelayMax, Delay );
+    }
+    Gia_ManUpdateMapping( p, vNodes, vWin );
+    return DelayMax;
+}
+int Gia_ManEvalWindow( Gia_Man_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Wec_t * vWin, Vec_Int_t * vTemp )
+{
+    int DelayMax;
+    assert( Vec_IntSize(vNodes) == Vec_WecSize(vWin) );
+    Gia_ManUpdateMapping( p, vNodes, vWin );
+    DelayMax = Gia_ManComputeEdgeDelay( p );
+    Gia_ManUpdateMapping( p, vNodes, vWin );
+    return DelayMax;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaOf.c b/src/aig/gia/giaOf.c
index 2dc8b376..dca13ae6 100644
--- a/src/aig/gia/giaOf.c
+++ b/src/aig/gia/giaOf.c
@@ -1846,6 +1846,8 @@ Gia_Man_t * Of_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
 
     pNew = Of_ManDeriveMapping( p );
     Gia_ManMappingVerify( pNew );
+    if ( pNew->vPacking )
+        Gia_ManConvertPackingToEdges( pNew );
     //Of_ManPrintCuts( p );
     Of_StoDelete( p );
     if ( pCls != pGia )
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index a5359905..9b905753 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -69,10 +69,10 @@ struct Sbl_Man_t_
     Vec_Int_t *    vCutsNum;     // cut counts for each obj
     Vec_Int_t *    vCutsStart;   // starting cuts for each obj
     Vec_Int_t *    vCutsObj;     // object to which this cut belongs
-    Vec_Wrd_t *    vTempI1;       // temporary cuts
-    Vec_Wrd_t *    vTempI2;       // temporary cuts
-    Vec_Wrd_t *    vTempN1;       // temporary cuts
-    Vec_Wrd_t *    vTempN2;       // temporary cuts
+    Vec_Wrd_t *    vTempI1;      // temporary cuts
+    Vec_Wrd_t *    vTempI2;      // temporary cuts
+    Vec_Wrd_t *    vTempN1;      // temporary cuts
+    Vec_Wrd_t *    vTempN2;      // temporary cuts
     Vec_Int_t *    vSolInit;     // initial solution
     Vec_Int_t *    vSolCur;      // current solution
     Vec_Int_t *    vSolBest;     // best solution
@@ -236,7 +236,7 @@ void Sbl_ManStop( Sbl_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Timing computation.]
+  Synopsis    [For each node in the window, create fanins.]
 
   Description []
                
@@ -245,52 +245,70 @@ void Sbl_ManStop( Sbl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins, int * pEdges )
+void Sbl_ManGetCurrentMapping( Sbl_Man_t * p )
 {
-    int k, iFan, DelayMax = -1, Count = 0, iFanMax = -1;
-    *pEdges = -1;
-    Vec_IntForEachEntry( vFanins, iFan, k )
-    {
-        int Delay = Vec_IntEntry(p->vArrs, iFan) + 1;
-        if ( DelayMax < Delay )
-        {
-            DelayMax = Delay;
-            iFanMax = k;
-            Count = 1;
-        }
-        else if ( DelayMax == Delay )
-            Count++;
-    }
-    if ( p->nEdges == 0 )
-        return DelayMax;
-    if ( p->nEdges == 1 )
+    Vec_Int_t * vObj;
+    word CutI1, CutI2, CutN1, CutN2;
+    int i, c, b, iObj;
+    Vec_WecClear( p->vWindow );
+    Vec_WecInit( p->vWindow, Vec_IntSize(p->vAnds) );
+    assert( Vec_IntSize(p->vSolCur) > 0 );
+    Vec_IntForEachEntry( p->vSolCur, c, i )
     {
-        if ( Count == 1 )
-        {
-            *pEdges = iFanMax;
-            return DelayMax - 1;
-        }
-        return DelayMax;
+        CutI1 = Vec_WrdEntry( p->vCutsI1, c );
+        CutI2 = Vec_WrdEntry( p->vCutsI2, c );
+        CutN1 = Vec_WrdEntry( p->vCutsN1, c );
+        CutN2 = Vec_WrdEntry( p->vCutsN2, c );
+        iObj  = Vec_IntEntry( p->vCutsObj, c );
+        //iObj  = Vec_IntEntry( p->vAnds, iObj );
+        vObj  = Vec_WecEntry( p->vWindow, iObj );
+        assert( Vec_IntSize(vObj) == 0 );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutI1 >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutI2 >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, 64+b) );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutN1 >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
+        for ( b = 0; b < 64; b++ )
+            if ( (CutN2 >> b) & 1 )
+                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, 64+b) );
     }
-    assert( 0 );
-    return 0;
 }
-int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart, int * pnEdges )
+
+
+/**Function*************************************************************
+
+  Synopsis    [Timing computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbl_ManComputeDelay( Sbl_Man_t * p, int iLut, Vec_Int_t * vFanins )
+{
+    int k, iFan, Delay = 0;
+    Vec_IntForEachEntry( vFanins, iFan, k )
+        Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vArrs, iFan) + 1 );
+    return Delay;
+}
+int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart )
 {
     Vec_Int_t * vFanins;
-    int DelayMax = DelayStart, Delay;
-    int iLut, iFan, k, Edges, nCountEdges = 0;
+    int DelayMax = DelayStart, Delay, iLut, iFan, k;
     // compute arrival times
     Vec_IntFill( p->vArrs,  Gia_ManObjNum(p->pGia), 0 );
-    Vec_IntFill( p->vEdges, Gia_ManObjNum(p->pGia), -1 );
     Gia_ManForEachLut2( p->pGia, iLut )
     {
         vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
-        Delay = Sbl_ManComputeDelay( p, iLut, vFanins, &Edges );
+        Delay = Sbl_ManComputeDelay( p, iLut, vFanins );
         Vec_IntWriteEntry( p->vArrs,  iLut, Delay );
-        Vec_IntWriteEntry( p->vEdges, iLut, Edges );
         DelayMax = Abc_MaxInt( DelayMax, Delay );
-        nCountEdges += (Edges >= 0);
     }
     // compute required times
     Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY );
@@ -299,23 +317,16 @@ int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart, int * pnEdges )
     Gia_ManForEachLut2Reverse( p->pGia, iLut )
     {
         Delay = Vec_IntEntry(p->vReqs, iLut) - 1;
-        Edges = Vec_IntEntry(p->vEdges, iLut);
-        assert( p->nEdges > 0 || Edges == -1 );
         vFanins = Gia_ObjLutFanins2(p->pGia, iLut);
         Vec_IntForEachEntry( vFanins, iFan, k )
-            if ( k != Edges )
-                Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
-            else
-                Vec_IntDowndateEntry( p->vReqs, iFan, Delay + 1 );
+            Vec_IntDowndateEntry( p->vReqs, iFan, Delay );
     }
-    if ( pnEdges )
-        *pnEdges = nCountEdges;
     return DelayMax;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [For each node in the window, create fanins.]
+  Synopsis    [Given mapping in p->vSolCur, check if mapping meets delay.]
 
   Description []
                
@@ -324,37 +335,24 @@ int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart, int * pnEdges )
   SeeAlso     []
 
 ***********************************************************************/
-void Sbl_ManGetCurrentMapping( Sbl_Man_t * p )
+int Sbl_ManEvaluateMappingEdge( Sbl_Man_t * p, int DelayGlo )
 {
-    Vec_Int_t * vObj;
-    word CutI1, CutI2, CutN1, CutN2;
-    int i, c, b, iObj;
-    Vec_WecClear( p->vWindow );
-    Vec_WecInit( p->vWindow, Vec_IntSize(p->vAnds) );
-    assert( Vec_IntSize(p->vSolCur) > 0 );
-    Vec_IntForEachEntry( p->vSolCur, c, i )
-    {
-        CutI1 = Vec_WrdEntry( p->vCutsI1, c );
-        CutI2 = Vec_WrdEntry( p->vCutsI2, c );
-        CutN1 = Vec_WrdEntry( p->vCutsN1, c );
-        CutN2 = Vec_WrdEntry( p->vCutsN2, c );
-        iObj  = Vec_IntEntry( p->vCutsObj, c );
-        //iObj  = Vec_IntEntry( p->vAnds, iObj );
-        vObj  = Vec_WecEntry( p->vWindow, iObj );
-        assert( Vec_IntSize(vObj) == 0 );
-        for ( b = 0; b < 64; b++ )
-            if ( (CutI1 >> b) & 1 )
-                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
-        for ( b = 0; b < 64; b++ )
-            if ( (CutI2 >> b) & 1 )
-                Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, 64+b) );
-        for ( b = 0; b < 64; b++ )
-            if ( (CutN1 >> b) & 1 )
-                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
-        for ( b = 0; b < 64; b++ )
-            if ( (CutN2 >> b) & 1 )
-                Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, 64+b) );
-    }
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vArray; 
+    int i, DelayMax;
+    Vec_IntClear( p->vPath );
+    // update new timing
+    Sbl_ManGetCurrentMapping( p );
+    // derive new timing
+    DelayMax = Gia_ManEvalWindow( p->pGia, p->vLeaves, p->vAnds, p->vWindow, p->vPolar );
+    p->timeTime += Abc_Clock() - clk;
+    if ( DelayMax <= DelayGlo )
+        return 1;
+    // create critical path composed of all nodes
+    Vec_WecForEachLevel( p->vWindow, vArray, i )
+        if ( Vec_IntSize(vArray) > 0 )
+            Vec_IntPush( p->vPath, i );
+    return 0;
 }
 
 /**Function*************************************************************
@@ -381,18 +379,19 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo )
 {
     abctime clk = Abc_Clock();
     Vec_Int_t * vFanins;
-    int i, iLut = -1, iAnd, Delay, Required, Edges;
+    int i, iLut, iAnd, Delay, Required;
+    if ( p->pGia->vEdge1 )
+        return Sbl_ManEvaluateMappingEdge( p, DelayGlo );
     Vec_IntClear( p->vPath );
     // derive timing
-    Sbl_ManCreateTiming( p, DelayGlo, NULL );
+    Sbl_ManCreateTiming( p, DelayGlo );
     // update new timing
     Sbl_ManGetCurrentMapping( p );
     Vec_IntForEachEntry( p->vAnds, iLut, i )
     {
         vFanins = Vec_WecEntry( p->vWindow, i );
-        Delay   = Sbl_ManComputeDelay( p, iLut, vFanins, &Edges );
+        Delay   = Sbl_ManComputeDelay( p, iLut, vFanins );
         Vec_IntWriteEntry( p->vArrs, iLut, Delay );
-        Vec_IntWriteEntry( p->vEdges, iLut, Edges );
     }
     // compare timing at the root nodes
     Vec_IntForEachEntry( p->vRoots, iLut, i )
@@ -1029,9 +1028,15 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
     // update solution
     if ( Vec_IntSize(p->vSolBest) > 0 && Vec_IntSize(p->vSolBest) < Vec_IntSize(p->vSolInit) )
     {
-        int nDelayCur, nEdgesCur;
-        nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax, &nEdgesCur );
+        int nDelayCur, nEdgesCur = 0;
         Sbl_ManUpdateMapping( p );
+        if ( p->pGia->vEdge1 )
+        {
+            nDelayCur = Gia_ManEvalEdgeDelay( p->pGia );
+            nEdgesCur = Gia_ManEvalEdgeCount( p->pGia );
+        }
+        else
+            nDelayCur = Sbl_ManCreateTiming( p, p->DelayMax );
         printf( "Object %5d : Saved %2d nodes  (Conf =%8d)  Iter =%3d  Delay = %d  Edges = %4d\n", 
             iPivot, Vec_IntSize(p->vSolInit)-Vec_IntSize(p->vSolBest), nConfTotal, nIters, nDelayCur, nEdgesCur );
         p->timeTotal += Abc_Clock() - p->timeStart;
@@ -1066,6 +1071,10 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit,
     p->fReverse     = fReverse;     // reverse windowing
     p->fVeryVerbose = fVeryVerbose; // verbose
     p->fVerbose     = fVerbose | fVeryVerbose;
+    // determine delay limit
+    if ( fDelay && pGia->vEdge1 && p->DelayMax == 0 )
+        p->DelayMax = Gia_ManEvalEdgeDelay( pGia );
+    // iterate through the internal nodes
     Gia_ManComputeOneWinStart( pGia, nNumber, fReverse );
     Gia_ManForEachLut2( pGia, iLut )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c54427da..dd64a9da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -418,6 +418,7 @@ static int Abc_CommandAbc9Mf                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Nf                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Of                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Pack               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Edge               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Unmap              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Struct             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1043,6 +1044,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&nf",           Abc_CommandAbc9Nf,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&of",           Abc_CommandAbc9Of,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&pack",         Abc_CommandAbc9Pack,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&edge",         Abc_CommandAbc9Edge,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&satlut",       Abc_CommandAbc9SatLut,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&unmap",        Abc_CommandAbc9Unmap,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&struct",       Abc_CommandAbc9Struct,       0 );
@@ -34800,7 +34802,8 @@ int Abc_CommandAbc9Pack( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 )
         Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
-    Gia_ManLutPacking( pAbc->pGia, nBlock, DelayRoute, DelayDir, fVerbose );
+    else
+        Gia_ManLutPacking( pAbc->pGia, nBlock, DelayRoute, DelayDir, fVerbose );
     return 0;
 
 usage:
@@ -34825,6 +34828,67 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c, DelayMax = 0, fReverse = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'r':
+                fReverse ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+            default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Empty GIA network.\n" );
+        return 1;
+    }
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Current AIG has no mapping. Run \"&if\".\n" );
+        return 1;
+    }
+    if ( Gia_ManLutSizeMax(pAbc->pGia) > 6 )
+    {
+        Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
+        return 0;
+    }
+    if ( fReverse )
+        DelayMax = Gia_ManComputeEdgeDelay2( pAbc->pGia );
+    else 
+        DelayMax = Gia_ManComputeEdgeDelay( pAbc->pGia );
+    printf( "The number of edges = %d.  Delay = %d.\n", Gia_ManEvalEdgeCount(pAbc->pGia), DelayMax );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &edge [-rvh]\n" );
+    Abc_Print( -2, "\t           find edge assignment of the LUT-mapped network\n" );
+    Abc_Print( -2, "\t-r       : toggles using reverse order [default = %s]\n", fReverse? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : prints the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nImproves, int nBTLimit, int DelayMax, int nEdges, int fDelay, int fReverse, int fVeryVerbose, int fVerbose );
@@ -40558,8 +40622,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    extern void Gia_ManCheckFalseTest( Gia_Man_t * p, int nSlackMax );
 //    extern void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs );
 //    extern void Gia_ManTisTest( Gia_Man_t * pInit );
-//    extern void Gia_Iso3Test( Gia_Man_t * p );
-    extern int Gia_ManEvalEdgeDelay( Gia_Man_t * p );
+    extern void Gia_Iso3Test( Gia_Man_t * p );
 
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "WPFsvh" ) ) != EOF )
@@ -40663,9 +40726,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Jf_ManTestCnf( pAbc->pGia );
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
-//    Gia_Iso3Test( pAbc->pGia );
-    Gia_ManEvalEdgeDelay( pAbc->pGia );
-
+    Gia_Iso3Test( pAbc->pGia );
 //    printf( "\nThis command is currently disabled.\n\n" );
     return 0;
 usage: