Supporting edges in delay-optimization in &satlut.

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 );

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" );
+                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;

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                                ///
 ////////////////////////////////////////////////////////////////////////

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 )

src/aig/gia/giaSatLut.c

@@ -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 )
-    {
-        if ( Count == 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 )
     {
-            *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 );
     }
-    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 )
     {

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,6 +34802,7 @@ 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) );
+    else
         Gia_ManLutPacking( pAbc->pGia, nBlock, DelayRoute, DelayDir, fVerbose );
     return 0;
 
@@ -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: