Version abc60419

14 files changed, 1386 insertions, 171 deletions

diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 7eb62416..0d75eb76 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -743,7 +743,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool
     if ( fUpdateLevel )
     {
         Abc_AigUpdateLevel_int( pMan );
-        Abc_AigUpdateLevelR_int( pMan );
+        if ( pMan->pNtkAig->vLevelsR ) 
+            Abc_AigUpdateLevelR_int( pMan );
     }
 }
 
@@ -819,9 +820,12 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
             pFanout->fMarkA = 1;
             Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
             // schedule the updated fanout for updating reverse level
-            assert( pFanout->fMarkB == 0 );
-            pFanout->fMarkB = 1;
-            Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
+            if ( pMan->pNtkAig->vLevelsR ) 
+            {
+                assert( pFanout->fMarkB == 0 );
+                pFanout->fMarkB = 1;
+                Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
+            }
         }
 
         // the fanout has changed, update EXOR status of its fanouts
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 68518ef0..4be253d1 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -235,7 +235,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
-        assert( Abc_NtkPoNum(pObj->pNtk) == 1 );
+        assert( Abc_NtkPoNum(pObj->pNtk) > 0 );
         Vec_PtrRemove( pObj->pNtk->vCos, pObj );
         pObj->pNtk->nPos--;
         // add the name to the table
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 697c3b32..201a1208 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -69,6 +69,7 @@ static int Abc_CommandRr           ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDemiter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrPos        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -178,6 +179,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
@@ -2866,8 +2868,8 @@ int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: rr [-W NM] [-fvh]\n" );
-    fprintf( pErr, "\t         performs redundancy removal in the current network\n" );
-    fprintf( pErr, "\t-W NM  : window size as the number of TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels );
+    fprintf( pErr, "\t         removes combinational redundancies in the current network\n" );
+    fprintf( pErr, "\t-W NM  : window size: TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels );
     fprintf( pErr, "\t-f     : toggle RR w.r.t. fanouts [default = %s]\n", fUseFanouts? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -3027,10 +3029,10 @@ usage:
 int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
     int fComb;
     int c;
-    extern Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk );
+    extern int Abc_NtkDemiter( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3062,17 +3064,16 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->fExor )
+    if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
     {
         fprintf( pErr, "The miter's PO is not an EXOR.\n" );
         return 1;
     }
 
     // get the new network
-    pNtkRes = Abc_NtkDemiter( pNtk );
-    if ( pNtkRes == NULL )
+    if ( !Abc_NtkDemiter( pNtk ) )
     {
-        fprintf( pErr, "Miter computation has failed.\n" );
+        fprintf( pErr, "Demitering has failed.\n" );
         return 1;
     }
     // replace the current network
@@ -3098,6 +3099,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    int fComb;
+    int c;
+    extern int Abc_NtkOrPos( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fComb ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "The network is not strashed.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+    {
+        fprintf( pErr, "The network already has one PO.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pErr, "The miter has latches. ORing is not performed.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkOrPos( pNtk ) )
+    {
+        fprintf( pErr, "ORing the POs has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+//    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: orpos [-h]\n" );
+    fprintf( pErr, "\t        creates single-output miter by ORing the POs of the current network\n" );
+//    fprintf( pErr, "\t-c    : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4540,15 +4614,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cut_CellDumpToFile();
 //    else
 //        Cut_CellPrecompute();
-//        Cut_CellLoad();
-
+        Cut_CellLoad();
+/*
         {
             Abc_Ntk_t * pNtkRes;
             extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
             pNtkRes = Abc_NtkTopmost( pNtk, nLevels );
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
-
+*/
     return 0;
 
 usage:
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 2f54dcee..c22532e9 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -704,6 +704,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     Fraig_Params_t Params;
     Abc_Ntk_t * pStore, * pFraig;
     int nWords1, nWords2, nWordsMin;
+    int clk = clock();
 
     // get the stored network
     pStore = Abc_FrameReadNtkStore();
@@ -740,6 +741,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 //    Fraig_ManReportChoices( p );
     // transform it into FRAIG
     pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
+PRT( "Total fraiging time", clock() - clk );
     if ( pFraig == NULL )
         return NULL;
     Abc_NtkDelete( pStore );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 76ec8a7e..490cf0c6 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -957,7 +957,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the timeframes of the network.]
+  Synopsis    [Splits the miter into two logic cones combined by an EXOR]
 
   Description []
 
@@ -966,7 +966,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
+int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNodeC, * pNodeA, * pNodeB, * pNode;
     Abc_Obj_t * pPoNew;
@@ -975,22 +975,33 @@ Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
-    assert( Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->fExor );
+    if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
+    {
+        printf( "The root of the miter is not an EXOR gate.\n" );
+        return 0;
+    }
     pNodeC = Abc_NodeRecognizeMux( Abc_ObjFanin0(Abc_NtkPo(pNtk,0)), &pNodeA, &pNodeB );
     assert( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) );
+    if ( Abc_ObjFaninC0(Abc_NtkPo(pNtk,0)) )
+    {
+        pNodeA = Abc_ObjNot(pNodeA);
+        pNodeB = Abc_ObjNot(pNodeB);
+    }
 
+    // add the PO corresponding to control input
     pPoNew = Abc_NtkCreatePo( pNtk );
     Abc_ObjAddFanin( pPoNew, pNodeC );
     Abc_NtkLogicStoreName( pPoNew, "addOut1" );
 
+    // add the PO corresponding to other input
     pPoNew = Abc_NtkCreatePo( pNtk );
-    Abc_ObjAddFanin( pPoNew, Abc_ObjRegular(pNodeA) );
+    Abc_ObjAddFanin( pPoNew, pNodeB );
     Abc_NtkLogicStoreName( pPoNew, "addOut2" );
 
     // mark the nodes in the first cone
-    pNodeA = Abc_ObjRegular(pNodeA);
+    pNodeB = Abc_ObjRegular(pNodeB);
     vNodes1 = Abc_NtkDfsNodes( pNtk, &pNodeC, 1 );
-    vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeA, 1 );
+    vNodes2 = Abc_NtkDfsNodes( pNtk, &pNodeB, 1 );
 
     Vec_PtrForEachEntry( vNodes1, pNode, i )
         pNode->fMarkA = 1;
@@ -1003,9 +1014,45 @@ Abc_Ntk_t * Abc_NtkDemiter( Abc_Ntk_t * pNtk )
     printf( "First cone = %6d.  Second cone = %6d.  Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
     Vec_PtrFree( vNodes1 );
     Vec_PtrFree( vNodes2 );
+    return 1;
+}
 
+/**Function*************************************************************
 
-    return pNtk;
+  Synopsis    [ORs the outputs.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkOrPos( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pMiter;
+    int i;
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    // OR the POs
+    pMiter = Abc_ObjNot( Abc_NtkConst1(pNtk) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pMiter = Abc_AigOr( pNtk->pManFunc, pMiter, Abc_ObjChild0(pNode) );
+    // remove the POs and their names
+    for ( i = Abc_NtkPoNum(pNtk) - 1; i >= 0; i-- )
+        Abc_NtkDeleteObj( Abc_NtkPo(pNtk, i) );
+    assert( Abc_NtkPoNum(pNtk) == 0 );
+    // create the new PO
+    pNode = Abc_NtkCreatePo( pNtk );
+    Abc_ObjAddFanin( pNode, pMiter );
+    Abc_NtkLogicStoreName( pNode, "miter" );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkOrPos: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index eec9e305..d7b270bf 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -70,10 +70,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
             fprintf( pFile, " (choice = %d)", Num );
         if ( Num = Abc_NtkGetExorNum(pNtk) )
             fprintf( pFile, " (exor = %d)", Num );
-        if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
-            fprintf( pFile, " (mux = %d)", Num2-Num );
-        if ( Num2 )
-            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
+//        if ( Num2 = Abc_NtkGetMuxNum(pNtk) )
+//            fprintf( pFile, " (mux = %d)", Num2-Num );
+//        if ( Num2 )
+//            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
     }
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
@@ -109,12 +109,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     {
         FILE * pTable;
         pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s  ",  pNtk->pName );
-        fprintf( pTable, "%4d ", Abc_NtkPiNum(pNtk) );
-        fprintf( pTable, "%4d ", Abc_NtkPoNum(pNtk) );
-//        fprintf( pTable, "%4d ", Abc_NtkLatchNum(pNtk) );
-        fprintf( pTable, "%6d ", Abc_NtkNodeNum(pNtk) );
-        fprintf( pTable, "%6d ", Abc_AigGetLevelNum(pNtk) );
+        fprintf( pTable, "%s ",  pNtk->pName );
+        fprintf( pTable, "%d ", Abc_NtkPiNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
+        fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 3a6a29c9..a9c61e1a 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "sim.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -47,21 +48,34 @@ struct Abc_RRMan_t_
     // the miter 
     Abc_Ntk_t *      pMiter;           // the miter derived from the window
     Prove_Params_t * pParams;          // the miter proving parameters
+    // statistical variables
+    int              nNodesOld;        // the old number of nodes
+    int              nLevelsOld;       // the old number of levels
+    int              nEdgesTried;      // the number of nodes tried
+    int              nEdgesRemoved;    // the number of nodes proved
+    int              timeWindow;       // the time to construct the window
+    int              timeMiter;        // the time to construct the miter
+    int              timeProve;        // the time to prove the miter
+    int              timeUpdate;       // the network update time
+    int              timeTotal;        // the total runtime
 };
 
 static Abc_RRMan_t * Abc_RRManStart();
 static void          Abc_RRManStop( Abc_RRMan_t * p );
+static void          Abc_RRManPrintStats( Abc_RRMan_t * p );
 static void          Abc_RRManClean( Abc_RRMan_t * p );
 static int           Abc_NtkRRProve( Abc_RRMan_t * p );
 static int           Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout );
 static int           Abc_NtkRRWindow( Abc_RRMan_t * p );
 
-static int           Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit );
-static int           Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout );
+static int           Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit );
+static int           Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout );
 static int           Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit );
-static void          Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static void          Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit );
 static Abc_Ntk_t *   Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots );
 
+static void          Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk );
+static void          Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -83,14 +97,18 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     ProgressBar * pProgress;
     Abc_RRMan_t * p;
     Abc_Obj_t * pNode, * pFanin, * pFanout;
-    int i, k, m, nNodes;
+    int i, k, m, nNodes, RetValue, clk, clkTotal = clock();
     // start the manager
     p = Abc_RRManStart( nFaninLevels, nFanoutLevels );
-    p->pNtk = pNtk;
+    p->pNtk          = pNtk;
     p->nFaninLevels  = nFaninLevels;
     p->nFanoutLevels = nFanoutLevels;
+    p->nNodesOld     = Abc_NtkNodeNum(pNtk);
+    p->nLevelsOld    = Abc_AigGetLevelNum(pNtk);
     // go through the nodes
+    Abc_NtkCleanCopy(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
+    Abc_NtkRRSimulateStart(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -109,36 +127,87 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
         {
             Abc_ObjForEachFanin( pNode, pFanin, k )
             {
+                // skip the nodes with only one fanout (tree nodes)
+                if ( Abc_ObjFanoutNum(pFanin) == 1 )
+                    continue;
+/*
+                if ( pFanin->Id == 228 && pNode->Id == 2649 )
+                {
+                    int k = 0;
+                }
+*/
+                p->nEdgesTried++;
                 Abc_RRManClean( p );
                 p->pNode   = pNode;
                 p->pFanin  = pFanin;
                 p->pFanout = NULL;
-                if ( !Abc_NtkRRWindow( p ) )
+
+                clk = clock();
+                RetValue = Abc_NtkRRWindow( p );
+                p->timeWindow += clock() - clk;
+                if ( !RetValue )
                     continue;
-                if ( !Abc_NtkRRProve( p ) )
+/*
+                if ( pFanin->Id == 228 && pNode->Id == 2649 )
+                {
+                    Abc_NtkShowAig( p->pWnd, 0 );
+                }
+*/
+                clk = clock();
+                RetValue = Abc_NtkRRProve( p );
+                p->timeMiter += clock() - clk;
+                if ( !RetValue )
                     continue;
+//printf( "%d -> %d (%d)\n", pFanin->Id, pNode->Id, k );
+
+                clk = clock();
                 Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
+                p->timeUpdate += clock() - clk;
+
+                p->nEdgesRemoved++;
                 break;
             }
             continue;
         }
         // use the fanouts
-        Abc_ObjForEachFanout( pNode, pFanout, m )
         Abc_ObjForEachFanin( pNode, pFanin, k )
+        Abc_ObjForEachFanout( pNode, pFanout, m )
         {
+            // skip the nodes with only one fanout (tree nodes)
+//            if ( Abc_ObjFanoutNum(pFanin) == 1 && Abc_ObjFanoutNum(pNode) == 1 )
+//                continue;
+
+            p->nEdgesTried++;
             Abc_RRManClean( p );
             p->pNode   = pNode;
             p->pFanin  = pFanin;
             p->pFanout = pFanout;
-            if ( !Abc_NtkRRWindow( p ) )
+
+            clk = clock();
+            RetValue = Abc_NtkRRWindow( p );
+            p->timeWindow += clock() - clk;
+            if ( !RetValue )
                 continue;
-            if ( !Abc_NtkRRProve( p ) )
+
+            clk = clock();
+            RetValue = Abc_NtkRRProve( p );
+            p->timeMiter += clock() - clk;
+            if ( !RetValue )
                 continue;
+
+            clk = clock();
             Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout );
+            p->timeUpdate += clock() - clk;
+
+            p->nEdgesRemoved++;
             break;
         }
     }
+    Abc_NtkRRSimulateStop(pNtk);
     Extra_ProgressBarStop( pProgress );
+    p->timeTotal = clock() - clkTotal;
+    if ( fVerbose )
+        Abc_RRManPrintStats( p );
     Abc_RRManStop( p );
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
@@ -204,6 +273,33 @@ void Abc_RRManStop( Abc_RRMan_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stop the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RRManPrintStats( Abc_RRMan_t * p )
+{
+    double Ratio = 100.0*(p->nNodesOld  - Abc_NtkNodeNum(p->pNtk))/p->nNodesOld;
+    printf( "Redundancy removal statistics:\n" );
+    printf( "Edges tried     = %6d.\n", p->nEdgesTried );
+    printf( "Edges removed   = %6d. (%5.2f %%)\n", p->nEdgesRemoved, 100.0*p->nEdgesRemoved/p->nEdgesTried );
+    printf( "Node gain       = %6d. (%5.2f %%)\n", p->nNodesOld  - Abc_NtkNodeNum(p->pNtk), Ratio );
+    printf( "Level gain      = %6d.\n", p->nLevelsOld - Abc_AigGetLevelNum(p->pNtk) );
+    PRT( "Windowing      ", p->timeWindow );
+    PRT( "Miter          ", p->timeMiter );
+    PRT( "    Construct  ", p->timeMiter - p->timeProve );
+    PRT( "    Prove      ", p->timeProve );
+    PRT( "Update         ", p->timeUpdate );
+    PRT( "TOTAL          ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Clean the manager.]
 
   Description []
@@ -243,11 +339,17 @@ void Abc_RRManClean( Abc_RRMan_t * p )
 int Abc_NtkRRProve( Abc_RRMan_t * p )
 {
     Abc_Ntk_t * pWndCopy;
-    int RetValue;
+    int RetValue, clk;
+//    Abc_NtkShowAig( p->pWnd, 0 );
     pWndCopy = Abc_NtkDup( p->pWnd );
-    Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy, p->pFanin->pCopy, p->pFanout? p->pFanout->pCopy : NULL );
+    Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
+    if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
+        Abc_NtkReassignIds(pWndCopy);
     p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 );
+    Abc_NtkDelete( pWndCopy );
+clk = clock();
     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
+p->timeProve += clock() - clk;
     if ( RetValue == 1 )
         return 1;
     return 0;
@@ -257,7 +359,9 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
 
   Synopsis    [Updates the network after redundancy removal.]
 
-  Description []
+  Description [This procedure assumes that non-control value of the fanin
+  was proved redundant. It is okay to concentrate on non-control values
+  because the control values can be seen as redundancy of the fanout edge.]
                
   SideEffects []
 
@@ -280,7 +384,7 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
     // replace
     if ( pFanout == NULL )
     {
-        Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew, 0 );
+        Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew, 1 );
         return 1;
     }
     // find the fanout after redundancy removal
@@ -290,7 +394,7 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
         pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) );
     else assert( 0 );
     // replace
-    Abc_AigReplace( pNtk->pManFunc, pFanout, pFanoutNew, 0 );
+    Abc_AigReplace( pNtk->pManFunc, pFanout, pFanoutNew, 1 );
     return 1;
 }
 
@@ -310,59 +414,50 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
 ***********************************************************************/
 int Abc_NtkRRWindow( Abc_RRMan_t * p )
 {
-    Abc_Obj_t * pObj, * pFanout, * pEdgeFanin, * pEdgeFanout;
-    int i, k;
+    Abc_Obj_t * pObj, * pEdgeFanin, * pEdgeFanout;
+    int i, LevelMin, LevelMax, RetValue;
 
     // get the edge
     pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
     pEdgeFanin  = p->pFanout? p->pNode : p->pFanin;
+    // get the minimum and maximum levels of the window
+    LevelMin = ABC_MAX( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
+    LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels;
 
     // start the TFI leaves with the fanin
     Abc_NtkIncrementTravId( p->pNtk );
     Abc_NodeSetTravIdCurrent( p->pFanin );
     Vec_PtrPush( p->vFaninLeaves, p->pFanin );
     // mark the TFI cone and collect the leaves down to the given level
-    while ( Abc_NtkRRTfi_int(p->vFaninLeaves, p->pFanin->Level - p->nFaninLevels) );
+    while ( Abc_NtkRRTfi_int(p->vFaninLeaves, LevelMin) );
 
-    // collect the TFO cone of the leaves
+    // mark the leaves with the new TravId
     Abc_NtkIncrementTravId( p->pNtk );
     Vec_PtrForEachEntry( p->vFaninLeaves, pObj, i )
-    {
-        Abc_ObjForEachFanout( pObj, pFanout, k )
-        {
-            if ( !Abc_ObjIsNode(pFanout) )
-                continue;
-            if ( pFanout->Level > pEdgeFanout->Level + p->nFanoutLevels )
-                continue;
-            if ( Abc_NodeIsTravIdCurrent(pFanout) )
-                continue;
-            Abc_NodeSetTravIdCurrent( pFanout );
-            Vec_PtrPush( p->vFanoutRoots, pFanout );
-        }
-    }
-    // mark the TFO cone and collect the leaves up to the given level (while skipping the edge)
-    while ( Abc_NtkRRTfo_int(p->vFanoutRoots, pEdgeFanout->Level + p->nFanoutLevels, pEdgeFanin, pEdgeFanout) );
-    // unmark the nodes
-    Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
-        pObj->fMarkA = 0;
+        Abc_NodeSetTravIdCurrent( pObj );
+    // traverse the TFO cone of the leaves (while skipping the edge)
+    // (a) mark the nodes in the cone using the current TravId
+    // (b) collect the nodes that have external fanouts into p->vFanoutRoots
+    while ( Abc_NtkRRTfo_int(p->vFaninLeaves, p->vFanoutRoots, LevelMax, pEdgeFanin, pEdgeFanout) );
 
-    // mark the current roots
-    Abc_NtkIncrementTravId( p->pNtk );
+    // mark the fanout roots
     Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
-        Abc_NodeSetTravIdCurrent( pObj );
+        pObj->fMarkA = 1;
     // collect roots reachable from the fanout (p->vRoots)
-    if ( !Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, pEdgeFanout->Level + p->nFanoutLevels + 5 ) )
+    RetValue = Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, LevelMax + 1 );
+    // unmark the fanout roots
+    Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i )
+        pObj->fMarkA = 0;
+
+    // return if the window is infeasible
+    if ( RetValue == 0 )
         return 0;
 
     // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves)
     // using the previous marks coming from the TFO cone
+    Abc_NtkIncrementTravId( p->pNtk );
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
-        Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone );
-    // unmark the nodes
-    Vec_PtrForEachEntry( p->vCone, pObj, i )
-        pObj->fMarkA = 0;
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 0;
+        Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone, LevelMin );
 
     // create a new network
     p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots );
@@ -380,21 +475,22 @@ int Abc_NtkRRWindow( Abc_RRMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit )
+int Abc_NtkRRTfi_int( Vec_Ptr_t * vLeaves, int LevelLimit )
 {
     Abc_Obj_t * pObj, * pNext;
     int i, k, LevelMax, nSize;
+    assert( LevelLimit >= 0 );
     // find the maximum level of leaves
     LevelMax = 0;
-    Vec_PtrForEachEntry( vFaninLeaves, pObj, i )
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
         if ( LevelMax < (int)pObj->Level )
             LevelMax = pObj->Level;
     // if the nodes are all PIs, LevelMax == 0
-    if ( LevelMax == 0 || LevelMax <= LevelLimit )
+    if ( LevelMax <= LevelLimit )
         return 0;
     // expand the nodes with the minimum level
-    nSize = Vec_PtrSize(vFaninLeaves);
-    Vec_PtrForEachEntryStop( vFaninLeaves, pObj, i, nSize )
+    nSize = Vec_PtrSize(vLeaves);
+    Vec_PtrForEachEntryStop( vLeaves, pObj, i, nSize )
     {
         if ( LevelMax != (int)pObj->Level )
             continue;
@@ -403,18 +499,20 @@ int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit )
             if ( Abc_NodeIsTravIdCurrent(pNext) )
                 continue;
             Abc_NodeSetTravIdCurrent( pNext );
-            Vec_PtrPush( vFaninLeaves, pNext );
+            Vec_PtrPush( vLeaves, pNext );
         }
     }
     // remove old nodes (cannot remove a PI)
     k = 0;
-    Vec_PtrForEachEntry( vFaninLeaves, pObj, i )
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
     {
         if ( LevelMax == (int)pObj->Level )
             continue;
-        Vec_PtrWriteEntry( vFaninLeaves, k++, pObj );
+        Vec_PtrWriteEntry( vLeaves, k++, pObj );
     }
-    Vec_PtrShrink( vFaninLeaves, k );
+    Vec_PtrShrink( vLeaves, k );
+    if ( Vec_PtrSize(vLeaves) > 2000 )
+        return 0;
     return 1;
 }
 
@@ -429,60 +527,56 @@ int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout )
+int Abc_NtkRRTfo_int( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout )
 {
     Abc_Obj_t * pObj, * pNext;
-    int i, k, LevelMin, nSize;
-    // find the minimum level of roots
+    int i, k, LevelMin, nSize, fObjIsRoot;
+    // find the minimum level of leaves
     LevelMin = ABC_INFINITY;
-    Vec_PtrForEachEntry( vFanoutRoots, pObj, i )
-        if ( Abc_ObjIsNode(pObj) && !pObj->fMarkA && LevelMin > (int)pObj->Level )
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        if ( LevelMin > (int)pObj->Level )
             LevelMin = pObj->Level;
-    // if the nodes are all POs, LevelMin == ABC_INFINITY
-    if ( LevelMin == ABC_INFINITY || LevelMin > LevelLimit )
+    // if the minimum level exceed the limit, we are done
+    if ( LevelMin > LevelLimit )
         return 0;
     // expand the nodes with the minimum level
-    nSize = Vec_PtrSize(vFanoutRoots);
-    Vec_PtrForEachEntryStop( vFanoutRoots, pObj, i, nSize )
+    nSize = Vec_PtrSize(vLeaves);
+    Vec_PtrForEachEntryStop( vLeaves, pObj, i, nSize )
     {
         if ( LevelMin != (int)pObj->Level )
             continue;
+        fObjIsRoot = 0;
         Abc_ObjForEachFanout( pObj, pNext, k )
         {
-            if ( !Abc_ObjIsNode(pNext) || pNext->Level > (unsigned)LevelLimit )
+            // check if the fanout is outside of the cone
+            if ( Abc_ObjIsCo(pNext) || pNext->Level > (unsigned)LevelLimit )
             {
-                pObj->fMarkA = 1;
+                fObjIsRoot = 1;
                 continue;
             }
+            // skip the edge under check
             if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
                 continue;
+            // skip the visited fanouts
             if ( Abc_NodeIsTravIdCurrent(pNext) )
                 continue;
             Abc_NodeSetTravIdCurrent( pNext );
-            Vec_PtrPush( vFanoutRoots, pNext );
+            Vec_PtrPush( vLeaves, pNext );
         }
+        if ( fObjIsRoot )
+            Vec_PtrPush( vRoots, pObj );
     }
     // remove old nodes
     k = 0;
-    Vec_PtrForEachEntry( vFanoutRoots, pObj, i )
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
     {
         if ( LevelMin == (int)pObj->Level )
-        {
-            // check if the node has external fanouts
-            Abc_ObjForEachFanout( pObj, pNext, k )
-            {
-                if ( pObj == pEdgeFanin && pNext == pEdgeFanout )
-                    continue;
-                if ( !Abc_NodeIsTravIdCurrent(pNext) )
-                    break;
-            }
-            // if external fanout is found, do not remove the node
-            if ( pNext )
-                continue;
-        }
-        Vec_PtrWriteEntry( vFanoutRoots, k++, pObj );
+            continue;
+        Vec_PtrWriteEntry( vLeaves, k++, pObj );
     }
-    Vec_PtrShrink( vFanoutRoots, k );
+    Vec_PtrShrink( vLeaves, k );
+    if ( Vec_PtrSize(vLeaves) > 2000 )
+        return 0;
     return 1;
 }
 
@@ -490,7 +584,8 @@ int Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdg
 
   Synopsis    [Collects the roots in the TFO of the node.]
 
-  Description []
+  Description [Note that this procedure can be improved by
+  marking and skipping the visited nodes.]
                
   SideEffects []
 
@@ -501,14 +596,18 @@ int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit )
 {
     Abc_Obj_t * pFanout;
     int i;
+    // if we encountered a node outside of the TFO cone of the fanins, quit
     if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit )
         return 0;
-    if ( Abc_NodeIsTravIdCurrent(pNode) )
+    // if we encountered a node on the boundary, add it to the roots
+    if ( pNode->fMarkA )
     {
         Vec_PtrPushUnique( vRoots, pNode );
         return 1;
     }
+    // mark the node with the current TravId (needed to have all internal nodes marked)
     Abc_NodeSetTravIdCurrent( pNode );
+    // traverse the fanouts
     Abc_ObjForEachFanout( pNode, pFanout, i )
         if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) )
             return 0;
@@ -517,7 +616,7 @@ int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Collects the leaves and cone of the roots.]
 
   Description []
                
@@ -526,22 +625,26 @@ int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, int LevelLimit )
 {
     Abc_Obj_t * pFanin;
     int i;
     // skip visited nodes
-    if ( pNode->fMarkA )
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
         return;
-    pNode->fMarkA = 1;
-    // add the node if it was not visited in the previus run
-    if ( !Abc_NodeIsTravIdPrevious(pNode) )
+    // add node to leaves if it is not in TFI cone of the leaves (marked before) or below the limit
+    if ( !Abc_NodeIsTravIdPrevious(pNode) || (int)pNode->Level <= LevelLimit )
     {
+        Abc_NodeSetTravIdCurrent( pNode );
         Vec_PtrPush( vLeaves, pNode );
         return;
     }
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // call for the node's fanins
     Abc_ObjForEachFanin( pNode, pFanin, i )
-        Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone );
+        Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone, LevelLimit );
+    // add the node to the cone in topological order
     Vec_PtrPush( vCone, pNode );
 }
 
@@ -560,6 +663,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj;
+    int fCheck = 1;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
@@ -581,12 +685,15 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
             Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) );
     // create the POs
     Vec_PtrForEachEntry( vRoots, pObj, i )
+    {
+        assert( !Abc_ObjIsComplement(pObj->pCopy) );
         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy );
+    }
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkNew );
     Abc_NtkAddDummyPoNames( pNtkNew );
     // check
-    if ( !Abc_NtkCheck( pNtkNew ) )
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkWindow: The network check has failed.\n" );
         return NULL;
@@ -594,6 +701,288 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
     return pNtkNew;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Starts simulation to detect non-redundant edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRRSimulateStart( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    unsigned uData, uData0, uData1;
+    int i;
+    Abc_NtkConst1(pNtk)->pData = (void *)~((unsigned)0);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pData = (void *)SIM_RANDOM_UNSIGNED;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
+        uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
+        uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
+        assert( pObj->pData == NULL );
+        pObj->pData = (void *)uData;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops simulation to detect non-redundant edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRRSimulateStop( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pData = NULL;
+}
+
+
+
+
+
+
+
+static void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes );
+static void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField );
+static void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField );
+
+/**Function*************************************************************
+
+  Synopsis    [Simulation to detect non-redundant edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Abc_NtkRRSimulate( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes, * vField;
+    Vec_Str_t * vTargets;
+    Abc_Obj_t * pObj;
+    unsigned uData, uData0, uData1;
+    int PrevCi, Phase, i, k;
+
+    // start the candidates
+    vTargets = Vec_StrStart( Abc_NtkObjNumMax(pNtk) + 1 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        Phase = ((Abc_ObjFanoutNum(Abc_ObjFanin1(pObj)) > 1) << 1);
+        Phase |= (Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) > 1);
+        Vec_StrWriteEntry( vTargets, pObj->Id, (char)Phase );
+    }
+
+    // simulate patters and store them in copy
+    Abc_NtkConst1(pNtk)->pCopy = (Abc_Obj_t *)~((unsigned)0);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)SIM_RANDOM_UNSIGNED;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( i == 0 ) continue;
+        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
+        uData1 = (unsigned)Abc_ObjFanin1(pObj)->pData;
+        uData  = Abc_ObjFaninC0(pObj)? ~uData0 : uData0;
+        uData &= Abc_ObjFaninC1(pObj)? ~uData1 : uData1;
+        pObj->pCopy = (Abc_Obj_t *)uData;
+    }
+    // store the result in data
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        uData0 = (unsigned)Abc_ObjFanin0(pObj)->pData;
+        if ( Abc_ObjFaninC0(pObj) )
+            pObj->pData = (void *)~uData0;
+        else
+            pObj->pData = (void *)uData0;
+    }
+
+    // refine the candidates
+    for ( PrevCi = 0; PrevCi < Abc_NtkCiNum(pNtk); PrevCi = i )
+    {
+        vNodes = Vec_PtrAlloc( 10 );
+        Abc_NtkIncrementTravId( pNtk );
+        for ( i = PrevCi; i < Abc_NtkCiNum(pNtk); i++ )
+        {
+            Sim_TraverseNodes_rec( Abc_NtkCi(pNtk, i), vTargets, vNodes );
+            if ( Vec_PtrSize(vNodes) > 128 )
+                break;
+        }
+        // collect the marked nodes in the topological order
+        vField = Vec_PtrAlloc( 10 );
+        Abc_NtkIncrementTravId( pNtk );
+        Abc_NtkForEachCo( pNtk, pObj, k )
+            Sim_CollectNodes_rec( pObj, vField );
+
+        // simulate these nodes
+        Sim_SimulateCollected( vTargets, vNodes, vField );
+        // prepare for the next loop
+        Vec_PtrFree( vNodes );
+    }
+
+    // clean
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pData = NULL;
+    return vTargets;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes starting from the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_TraverseNodes_rec( Abc_Obj_t * pRoot, Vec_Str_t * vTargets, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    char Entry;
+    int k;
+    if ( Abc_NodeIsTravIdCurrent(pRoot) )
+        return;
+    Abc_NodeSetTravIdCurrent( pRoot );
+    // save the reached targets
+    Entry = Vec_StrEntry(vTargets, pRoot->Id);
+    if ( Entry & 1 )
+        Vec_PtrPush( vNodes, Abc_ObjNot(pRoot) );
+    if ( Entry & 2 )
+        Vec_PtrPush( vNodes, pRoot );
+    // explore the fanouts
+    Abc_ObjForEachFanout( pRoot, pFanout, k )
+        Sim_TraverseNodes_rec( pFanout, vTargets, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes starting from the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_CollectNodes_rec( Abc_Obj_t * pRoot, Vec_Ptr_t * vField )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_NodeIsTravIdCurrent(pRoot) )
+        return;
+    if ( !Abc_NodeIsTravIdPrevious(pRoot) )
+        return;
+    Abc_NodeSetTravIdCurrent( pRoot );
+    Abc_ObjForEachFanin( pRoot, pFanin, i )
+        Sim_CollectNodes_rec( pFanin, vField );
+    if ( !Abc_ObjIsCo(pRoot) )
+        pRoot->pData = (void *)Vec_PtrSize(vField);
+    Vec_PtrPush( vField, pRoot );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulate the given nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sim_SimulateCollected( Vec_Str_t * vTargets, Vec_Ptr_t * vNodes, Vec_Ptr_t * vField )
+{
+    Abc_Obj_t * pObj, * pFanin0, * pFanin1, * pDisproved;
+    Vec_Ptr_t * vSims;
+    unsigned * pUnsigned, * pUnsignedF;
+    int i, k, Phase, fCompl;
+    // get simulation info
+    vSims = Sim_UtilInfoAlloc( Vec_PtrSize(vField), Vec_PtrSize(vNodes), 0 );
+    // simulate the nodes
+    Vec_PtrForEachEntry( vField, pObj, i )
+    {
+        if ( Abc_ObjIsCi(pObj) )
+        {
+            pUnsigned = Vec_PtrEntry( vSims, i );
+            for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
+                pUnsigned[k] = (unsigned)pObj->pCopy;
+            continue;
+        }
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            pUnsigned  = Vec_PtrEntry( vSims, i );
+            pUnsignedF = Vec_PtrEntry( vSims, (int)Abc_ObjFanin0(pObj)->pData );
+            if ( Abc_ObjFaninC0(pObj) )
+                for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
+                    pUnsigned[k] = ~pUnsignedF[k];
+            else
+                for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
+                    pUnsigned[k] = pUnsignedF[k];
+            // update targets
+            for ( k = 0; k < Vec_PtrSize(vNodes); k++ )
+            {
+                if ( pUnsigned[k] == (unsigned)pObj->pData )
+                    continue;
+                pDisproved = Vec_PtrEntry( vNodes, k );
+                fCompl = Abc_ObjIsComplement(pDisproved);
+                pDisproved = Abc_ObjRegular(pDisproved);
+                Phase = Vec_StrEntry( vTargets, pDisproved->Id );
+                if ( fCompl )
+                    Phase = (Phase & 2);
+                else
+                    Phase = (Phase & 1);
+                Vec_StrWriteEntry( vTargets, pDisproved->Id, (char)Phase );
+            }
+            continue;
+        }
+        // simulate the node
+        pFanin0 = Abc_ObjFanin0(pObj);
+        pFanin1 = Abc_ObjFanin1(pObj);
+    }
+}
+
+
+
+/*
+                {
+                    unsigned uData;
+                    if ( pFanin == Abc_ObjFanin0(pNode) )
+                    {
+                        uData = (unsigned)Abc_ObjFanin1(pNode)->pData;
+                        uData = Abc_ObjFaninC1(pNode)? ~uData : uData;
+                    }
+                    else if ( pFanin == Abc_ObjFanin1(pNode) )
+                    {
+                        uData = (unsigned)Abc_ObjFanin0(pNode)->pData;
+                        uData = Abc_ObjFaninC0(pNode)? ~uData : uData;
+                    }
+                    uData ^= (unsigned)pNode->pData;
+//                    Extra_PrintBinary( stdout, &uData, 32 ); printf( "\n" );
+                    if ( Extra_WordCountOnes(uData) > 8 )
+                        continue;
+                }
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 93fe2b90..ac012516 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -168,6 +168,14 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
     pAbc->TimeTotal += pAbc->TimeCommand;
     fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n",
         (float)pAbc->TimeCommand / CLOCKS_PER_SEC, (float)pAbc->TimeTotal / CLOCKS_PER_SEC );
+/*
+    {
+        FILE * pTable;
+        pTable = fopen( "runtimes.txt", "a+" );
+        fprintf( pTable, "%4.2f\n", (float)pAbc->TimeCommand / CLOCKS_PER_SEC );
+        fclose( pTable );
+    }
+*/
     pAbc->TimeCommand = 0;
     return 0;
 
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 9d74a782..f6d92af7 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -212,6 +212,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     // read the model name
     if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
         pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
+    else if ( strcmp( p->vTokens->pArray[0], ".exdc" ) != 0 ) 
+    {
+        printf( "%s: File parsing skipped after line %d (\"%s\").\n", p->pFileName, 
+            Extra_FileReaderGetLineNumber(p->pReader, 0), p->vTokens->pArray[0] );
+        return NULL;
+    }
 
     // read the inputs/outputs
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
new file mode 100644
index 00000000..75467d4d
--- /dev/null
+++ b/src/base/io/ioWriteVer.c
@@ -0,0 +1,497 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteVerilog.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to output a special subset of Verilog.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteVerilog.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+#include "main.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
+static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+
+    if ( !(Abc_NtkIsNetlist(pNtk) && (Abc_NtkHasMapping(pNtk) || Io_WriteVerilogCheckNtk(pNtk))) )
+    {
+        printf( "Io_WriteVerilog(): Can produce Verilog for a subset of logic networks.\n" );
+        printf( "The network should be either an AIG or a network after technology mapping.\n" );
+        printf( "The current network is not in the subset; the output files is not written.\n" );
+        return;
+    }
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // write the equations for the network
+    Io_WriteVerilogInt( pFile, pNtk );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes verilog.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    // write inputs and outputs
+    fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "module %s ( gclk,\n   ", Abc_NtkName(pNtk) );
+    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    fprintf( pFile, ",\n   " );
+    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    fprintf( pFile, "  );\n" );
+    // write inputs, outputs, registers, and wires
+    fprintf( pFile, "  input gclk," );
+    Io_WriteVerilogPis( pFile, pNtk, 10 );
+    fprintf( pFile, ";\n" );
+    fprintf( pFile, "  output" );
+    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    fprintf( pFile, ";\n" );
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+    fprintf( pFile, "  reg" );
+    Io_WriteVerilogRegs( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    }
+    fprintf( pFile, "  wire" );
+    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    fprintf( pFile, ";\n" );
+    // write registers
+    Io_WriteVerilogLatches( pFile, pNtk );
+    // write the nodes
+    if ( Abc_NtkHasMapping(pNtk) )
+        Io_WriteVerilogGates( pFile, pNtk );
+    else
+        Io_WriteVerilogNodes( pFile, pNtk );
+    // finalize the file
+    fprintf( pFile, "endmodule\n\n" );
+    fclose( pFile );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachPi( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanout0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPiNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachPo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Abc_ObjName(pNet), (i==Abc_NtkPoNum(pNtk)-1)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the wires.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of wires
+    nNodes = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        nNodes++;
+    }
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachNode( pNtk, pTerm, i )
+    {
+        if ( i == 0 ) 
+            continue;
+        pNet = Abc_ObjFanout0(pTerm);
+        if ( Abc_ObjIsCo(Abc_ObjFanout0(pNet)) )
+            continue;
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the regs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i, Counter, nNodes;
+
+    // count the number of latches
+    nNodes = Abc_NtkLatchNum(pNtk);
+
+    // write the wires
+    Counter = 0;
+    LineLength  = Start;
+    NameCounter = 0;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pNet = Abc_ObjFanout0(pLatch);
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
+            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
+            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Mio_Gate_t * pGate;
+    Mio_Pin_t * pGatePin;
+    Abc_Obj_t * pObj;
+    int i, k, Counter, nDigits, nFanins;
+
+    Counter = 1;
+    nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        pGate = pObj->pData;
+        nFanins = Abc_ObjFaninNum(pObj);
+        fprintf( pFile, "  %s g%0*d", Mio_GateReadName(pGate), nDigits, Counter++ );
+        fprintf( pFile, "(.%s (%s),", Mio_GateReadOutName(pGate), Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        for ( pGatePin = Mio_GateReadPins(pGate), k = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), k++ )
+            fprintf( pFile, " .%s (%s)%s", Mio_PinReadName(pGatePin), Io_WriteVerilogGetName(Abc_ObjFanin(pObj,k)), k==nFanins-1? "":"," );
+        fprintf( pFile, ");\n" );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFanins;
+    char * pName;
+
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        assert( Abc_SopGetCubeNum(pObj->pData) == 1 );
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            continue;
+        }
+        if ( nFanins == 1 )
+        {
+            pName = Abc_SopIsInv(pObj->pData)? "not" : "and";
+            fprintf( pFile, "  %s(%s, ", pName, Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+            fprintf( pFile, "%s);\n", Io_WriteVerilogGetName(Abc_ObjFanin0(pObj)) );
+            continue;
+        }
+        pName = Abc_SopIsComplement(pObj->pData)? "or" : "and";
+        fprintf( pFile, "  %s(%s, ", pName, Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : ", ") );
+        fprintf( pFile, ");\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+{
+    Abc_Obj_t * pFanin;
+    int i, Counter = 2;
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+    }
+    for ( ; i < nInMax; i++ )
+    {
+        if ( Counter++ % 4 == 0 )
+            fprintf( pFile, "\n   " );
+        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+    }
+    fprintf( pFile, ");\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        if ( Abc_SopGetCubeNum(pObj->pData) > 1 )
+        {
+            printf( "Node %s contains a cover with more than one cube.\n", Abc_ObjName(pObj) );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the name for writing the Verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+{
+    static char Buffer[20];
+    char * pName;
+    pName = Abc_ObjName(pObj);
+    if ( pName[0] != '[' )
+        return pName;
+    // replace the brackets; as a result, the length of the name does not change
+    strcpy( Buffer, pName );
+    Buffer[0] = 'x';
+    Buffer[strlen(Buffer)-1] = 'x';
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerAux.c
index f56da052..f0814c84 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerAux.c
@@ -24,14 +24,14 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
-static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
-static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
-static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
+static void Io_WriteVerilogAuxInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogAuxPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
+static void Io_WriteVerilogAuxNodes( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogAuxArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
+static int Io_WriteVerilogAuxCheckNtk( Abc_Ntk_t * pNtk );
+static char * Io_WriteVerilogAuxGetName( Abc_Obj_t * pObj );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,30 +48,30 @@ static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilogAux( Abc_Ntk_t * pNtk, char * pFileName )
 {
     FILE * pFile;
 
-    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogCheckNtk(pNtk) )
+    if ( !Abc_NtkIsSopNetlist(pNtk) || !Io_WriteVerilogAuxCheckNtk(pNtk) )
     {
-        printf( "Io_WriteVerilog(): Can write Verilog for a very special subset of logic networks.\n" );
+        printf( "Io_WriteVerilogAux(): Can write Verilog for a very special subset of logic networks.\n" );
         printf( "The current network is not in the subset; writing Verilog is not performed.\n" );
         return;
     }
 
     if ( Abc_NtkLatchNum(pNtk) > 0 )
-        printf( "Io_WriteVerilog(): Warning: only combinational portion is being written.\n" );
+        printf( "Io_WriteVerilogAux(): Warning: only combinational portion is being written.\n" );
 
     // start the output stream
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
-        fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", pFileName );
+        fprintf( stdout, "Io_WriteVerilogAux(): Cannot open the output file \"%s\".\n", pFileName );
         return;
     }
 
     // write the equations for the network
-    Io_WriteVerilogInt( pFile, pNtk );
+    Io_WriteVerilogAuxInt( pFile, pNtk );
     fprintf( pFile, "\n" );
     fclose( pFile );
 }
@@ -87,27 +87,27 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogAuxInt( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     // write inputs and outputs
     fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
     fprintf( pFile, "module %s (\n   ", Abc_NtkName(pNtk) );
-    Io_WriteVerilogPis( pFile, pNtk, 3 );
+    Io_WriteVerilogAuxPis( pFile, pNtk, 3 );
     fprintf( pFile, ",\n   " );
-    Io_WriteVerilogPos( pFile, pNtk, 3 );
+    Io_WriteVerilogAuxPos( pFile, pNtk, 3 );
     fprintf( pFile, "  );\n" );
     // write inputs, outputs and wires
     fprintf( pFile, "  input" );
-    Io_WriteVerilogPis( pFile, pNtk, 5 );
+    Io_WriteVerilogAuxPis( pFile, pNtk, 5 );
     fprintf( pFile, ";\n" );
     fprintf( pFile, "  output" );
-    Io_WriteVerilogPos( pFile, pNtk, 5 );
+    Io_WriteVerilogAuxPos( pFile, pNtk, 5 );
     fprintf( pFile, ";\n" );
     fprintf( pFile, "  wire" );
-    Io_WriteVerilogWires( pFile, pNtk, 4 );
+    Io_WriteVerilogAuxWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
     // write the nodes
-    Io_WriteVerilogNodes( pFile, pNtk );
+    Io_WriteVerilogAuxNodes( pFile, pNtk );
     // finalize the file
     fprintf( pFile, "endmodule\n\n" );
     fclose( pFile );
@@ -124,7 +124,7 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -163,7 +163,7 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -202,7 +202,7 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
+void Io_WriteVerilogAuxWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
 {
     Abc_Obj_t * pTerm, * pNet;
     int LineLength;
@@ -243,7 +243,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
             LineLength  = 3;
             NameCounter = 0;
         }
-        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        fprintf( pFile, " %s%s", Io_WriteVerilogAuxGetName(pNet), (Counter==nNodes)? "" : "," );
         LineLength += AddedLength;
         NameCounter++;
     }
@@ -260,7 +260,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogAuxNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i, nCubes, nFanins, Counter, nDigits, fPadZeros;
@@ -284,62 +284,62 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
         if ( nCubes == 0 )
         {
             fprintf( pFile, "  ts_gnd g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 0, fPadZeros );
         }
         else if ( nCubes == 1 && nFanins == 0 )
         {
             fprintf( pFile, "  ts_vdd g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 0, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 0, fPadZeros );
         }
         else if ( nFanins == 1 && Abc_SopIsInv(pObj->pData) )
         {
             fprintf( pFile, "  ts_inv g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 1, fPadZeros );
         }
         else if ( nFanins == 1 )
         {
             fprintf( pFile, "  ts_buf g%0*d ", nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 1, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 1, fPadZeros );
         }
         else if ( nFanins <= 4 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 4, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 4, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 4, fPadZeros );
         }
         else if ( nFanins <= 6 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 6, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 6, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 6, fPadZeros );
         }
         else if ( nFanins == 7 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 7, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 7, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 7, fPadZeros );
         }
         else if ( nFanins == 8 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 8, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 8, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 8, fPadZeros );
         }
         else if ( nFanins <= 16 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 16, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 16, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 16, fPadZeros );
         }
         else if ( nFanins <= 32 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 32, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 32, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 32, fPadZeros );
         }
         else if ( nFanins <= 64 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 64, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 64, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 64, fPadZeros );
         }
         else if ( nFanins <= 128 )
         {
             fprintf( pFile, "  %s%d g%0*d ", pName, 128, nDigits, Counter++ );
-            Io_WriteVerilogArgs( pFile, pObj, 128, fPadZeros );
+            Io_WriteVerilogAuxArgs( pFile, pObj, 128, fPadZeros );
         }
     }
 }
@@ -355,16 +355,16 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+void Io_WriteVerilogAuxArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
 {
     Abc_Obj_t * pFanin;
     int i, Counter = 2;
-    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+    fprintf( pFile, "(.z (%s)", Io_WriteVerilogAuxGetName(Abc_ObjFanout0(pObj)) );
     Abc_ObjForEachFanin( pObj, pFanin, i )
     {
         if ( Counter++ % 4 == 0 )
             fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
+        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogAuxGetName(Abc_ObjFanin(pObj,i)) );
     }
     for ( ; i < nInMax; i++ )
     {
@@ -386,7 +386,7 @@ void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZe
   SeeAlso     []
 
 ***********************************************************************/
-int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
+int Io_WriteVerilogAuxCheckNtk( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     char * pSop;
@@ -423,7 +423,7 @@ int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_WriteVerilogGetName( Abc_Obj_t * pObj )
+char * Io_WriteVerilogAuxGetName( Abc_Obj_t * pObj )
 {
     static char Buffer[20];
     char * pName;
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 8693c8eb..2d5e4b9e 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -17,4 +17,5 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioWriteGml.c \
     src/base/io/ioWriteList.c \
     src/base/io/ioWritePla.c \
-    src/base/io/ioWriteVerilog.c
+    src/base/io/ioWriteVer.c \
+    src/base/io/ioWriteVerAux.c
diff --git a/src/opt/cut/cutExpand.c b/src/opt/cut/cutExpand.c
new file mode 100644
index 00000000..d389ef7a
--- /dev/null
+++ b/src/opt/cut/cutExpand.c
@@ -0,0 +1,184 @@
+/**CFile****************************************************************
+
+  FileName    [cutExpand.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [K-feasible cut computation package.]
+
+  Synopsis    [Computes the truth table of the cut after expansion.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cutExpand.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define CUT_CELL_MVAR  9
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
+    {
+        if ( k == (int)pCut1->nLeaves )
+            break;
+        if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
+            continue;
+        assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the composition of cuts.]
+
+  Description [Inputs are: 
+  - a factor cut (truth table is stored inside)
+  - a node in the factor cut
+  - a tree cut to be substituted (truth table is stored inside)
+  - the resulting cut (truth table will be filled in).
+  Note that all cuts, including the resulting one, should be already 
+  computed and the nodes should be stored in the ascending order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cut_TruthCompose( Cut_Cut_t * pCutF, int Node, Cut_Cut_t * pCutT, Cut_Cut_t * pCutRes )
+{
+    static unsigned uCof0[1<<(CUT_CELL_MVAR-5)];
+    static unsigned uCof1[1<<(CUT_CELL_MVAR-5)];
+    static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
+    unsigned * pIn, * pOut, * pTemp;
+    unsigned uPhase;
+    int NodeIndex, i, k;
+
+    // sanity checks
+    assert( pCutF->nVarsMax == pCutT->nVarsMax );
+    assert( pCutF->nVarsMax == pCutRes->nVarsMax );
+    assert( pCutF->nVarsMax <= CUT_CELL_MVAR );
+    // the factor cut (pCutF) should have its nodes sorted in the ascending order
+    assert( pCutF->nLeaves <= pCutF->nVarsMax );
+    for ( i = 0; i < (int)pCutF->nLeaves - 1; i++ )
+        assert( pCutF->pLeaves[i] < pCutF->pLeaves[i+1] );
+    // the tree cut (pCutT) should have its nodes sorted in the ascending order
+    assert( pCutT->nLeaves <= pCutT->nVarsMax );
+    for ( i = 0; i < (int)pCutT->nLeaves - 1; i++ )
+        assert( pCutT->pLeaves[i] < pCutT->pLeaves[i+1] );
+    // the resulting cut (pCutRes) should have its nodes sorted in the ascending order
+    assert( pCutRes->nLeaves <= pCutRes->nVarsMax );
+    for ( i = 0; i < (int)pCutRes->nLeaves - 1; i++ )
+        assert( pCutRes->pLeaves[i] < pCutRes->pLeaves[i+1] );
+    // make sure that every node in pCutF (except Node) appears in pCutRes
+    for ( i = 0; i < (int)pCutF->nLeaves; i++ )
+    {
+        if ( pCutF->pLeaves[i] == Node )
+            continue;
+        for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
+            if ( pCutF->pLeaves[i] == pCutRes->pLeaves[k] )
+                break;
+        assert( k < (int)pCutRes->nLeaves ); // node i from pCutF is not found in pCutRes!!!
+    }
+    // make sure that every node in pCutT appears in pCutRes
+    for ( i = 0; i < (int)pCutT->nLeaves; i++ )
+    {
+        for ( k = 0; k < (int)pCutRes->nLeaves; k++ )
+            if ( pCutT->pLeaves[i] == pCutRes->pLeaves[k] )
+                break;
+        assert( k < (int)pCutRes->nLeaves ); // node i from pCutT is not found in pCutRes!!!
+    }
+
+
+    // find the index of the given node in the factor cut
+    NodeIndex = -1;
+    for ( NodeIndex = 0; NodeIndex < (int)pCutF->nLeaves; NodeIndex++ )
+        if ( pCutF->pLeaves[NodeIndex] == Node )
+            break;
+    assert( NodeIndex >= 0 );  // Node should be in pCutF
+
+    // copy the truth table
+    Extra_TruthCopy( uTemp, Cut_CutReadTruth(pCutF), pCutF->nLeaves );
+
+    // bubble-move the NodeIndex variable to be the last one (the most significant one)
+    pIn = uTemp; pOut = uCof0; // uCof0 is used for temporary storage here
+    for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
+    {
+        Extra_TruthSwapAdjacentVars( pOut, pIn, pCutF->nLeaves, i );
+        pTemp = pIn; pIn = pOut; pOut = pTemp;
+    }
+    if ( (pCutF->nLeaves - 1 - NodeIndex) & 1 )
+        Extra_TruthCopy( pOut, pIn, pCutF->nLeaves );
+    // the result of stretching is in uTemp
+
+    // cofactor the factor cut with respect to the node
+    Extra_TruthCopy( uCof0, uTemp, pCutF->nLeaves );
+    Extra_TruthCofactor0( uCof0, pCutF->nLeaves, pCutF->nLeaves-1 );
+    Extra_TruthCopy( uCof1, uTemp, pCutF->nLeaves );
+    Extra_TruthCofactor1( uCof1, pCutF->nLeaves, pCutF->nLeaves-1 );
+
+    // temporarily shrink the factor cut's variables by removing Node 
+    for ( i = NodeIndex; i < (int)pCutF->nLeaves - 1; i++ )
+        pCutF->pLeaves[i] = pCutF->pLeaves[i+1];
+    pCutF->nLeaves--;
+
+    // spread out the cofactors' truth tables to the same var order as the resulting cut
+    uPhase = Cut_TruthPhase(pCutRes, pCutF);
+    assert( Extra_WordCountOnes(uPhase) == (int)pCutF->nLeaves );
+    Extra_TruthStretch( uTemp, uCof0, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
+    Extra_TruthCopy( uCof0, uTemp, pCutF->nVarsMax );
+    Extra_TruthStretch( uTemp, uCof1, pCutF->nLeaves, pCutF->nVarsMax, uPhase );
+    Extra_TruthCopy( uCof1, uTemp, pCutF->nVarsMax );
+
+    // spread out the tree cut's truth table to the same var order as the resulting cut
+    uPhase = Cut_TruthPhase(pCutRes, pCutT); 
+    assert( Extra_WordCountOnes(uPhase) == (int)pCutT->nLeaves );
+    Extra_TruthStretch( uTemp, Cut_CutReadTruth(pCutT), pCutT->nLeaves, pCutT->nVarsMax, uPhase );
+
+    // create the resulting truth table
+    pTemp = Cut_CutReadTruth(pCutRes);
+    for ( i = Extra_TruthWordNum(pCutRes->nLeaves)-1; i >= 0; i-- )
+        pTemp[i] = (uCof0[i] & ~uTemp[i]) | (uCof1[i] & uTemp[i]);
+
+    // undo the removal of the node from the cut
+    for ( i = (int)pCutF->nLeaves - 1; i >= NodeIndex; --i )
+        pCutF->pLeaves[i+1] = pCutF->pLeaves[i];
+    pCutF->pLeaves[NodeIndex] = Node;
+    pCutF->nLeaves++;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index dd52b694..693978d6 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -203,6 +203,11 @@ void Cut_CellLoad()
 */
         // add to the table
         p->nTotal++;
+
+//        Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars ); printf( "\n" );
+//        if ( p->nTotal == 500 )
+//            break;
+
         if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
             p->nGood++;
     }