Version abc50817

29 files changed, 3369 insertions, 618 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index f52df69f..ca18265d 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -45,7 +45,9 @@ static int Abc_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFastExtract  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandRewrite      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRefactor     ( 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 );
@@ -55,6 +57,7 @@ static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSplit        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -110,7 +113,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "res",           Abc_CommandRes,              1 );
+
+    Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
@@ -120,6 +125,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "split",         Abc_CommandSplit,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -142,6 +148,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
 
     Ft_FactorStartMan();
+//    Rwt_ManExploreStart();
 }
 
 /**Function*************************************************************
@@ -159,6 +166,7 @@ void Abc_End()
 {
     Ft_FactorStopMan();
     Abc_NtkFraigStoreClean();
+//    Rwt_ManExplorePrint();
 }
 
 /**Function*************************************************************
@@ -517,7 +525,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !fProfile && !Abc_NtkIsAig(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
@@ -1309,23 +1317,109 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    Abc_ManRes_t * p;
-    extern int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p );
+    bool fVerbose;
+
+    {
+        Abc_ManRwr_t * p;
+        int fFlag = 0;
+
+        if ( fFlag )
+            p = Abc_NtkManRwrStart( NULL );
+        else
+            p = Abc_NtkManRwrStart( "data.aaa" );
+
+        Abc_NtkManRwrStop( p );
+        return 0;
+    }
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    p = Abc_NtkManResStart();
-    p->fVerbose     =  0;
-    p->nNodeSizeMax = 10;
-    p->nConeSizeMax = 10;
+    fVerbose     =  0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        return 1;
+    }
+    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    {
+        fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+        return 1;
+    }
+
+    // modify the current network
+    if ( !Abc_NtkRewrite( pNtk ) )
+    {
+        fprintf( pErr, "Rewriting has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: rewrite [-vh]\n" );
+    fprintf( pErr, "\t         performs technology-independent rewriting of the AIG\n" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    Abc_ManRef_t * p;
+    bool fVerbose;
+    int nNodeSizeMax;
+    int nConeSizeMax;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    p = Abc_NtkManRefStart();
+    fVerbose     =  0;
+    nNodeSizeMax = 10;
+    nConeSizeMax = 10;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF )
     {
@@ -1337,9 +1431,9 @@ int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
                 goto usage;
             }
-            p->nNodeSizeMax = atoi(argv[util_optind]);
+            nNodeSizeMax = atoi(argv[util_optind]);
             util_optind++;
-            if ( p->nNodeSizeMax < 0 ) 
+            if ( nNodeSizeMax < 0 ) 
                 goto usage;
             break;
         case 'c':
@@ -1348,13 +1442,13 @@ int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" );
                 goto usage;
             }
-            p->nConeSizeMax = atoi(argv[util_optind]);
+            nConeSizeMax = atoi(argv[util_optind]);
             util_optind++;
-            if ( p->nConeSizeMax < 0 ) 
+            if ( nConeSizeMax < 0 ) 
                 goto usage;
             break;
         case 'v':
-            p->fVerbose ^= 1;
+            fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -1366,32 +1460,36 @@ int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtk == NULL )
     {
         fprintf( pErr, "Empty network.\n" );
-        Abc_NtkManResStop( p );
+        Abc_NtkManRefStop( p );
         return 1;
     }
     if ( !Abc_NtkIsAig(pNtk) )
     {
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
-        Abc_NtkManResStop( p );
+        Abc_NtkManRefStop( p );
         return 1;
     }
     if ( Abc_NtkCountChoiceNodes(pNtk) )
     {
         fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
-        Abc_NtkManResStop( p );
+        Abc_NtkManRefStop( p );
         return 1;
     }
 
     // modify the current network
-    Abc_NtkAigResynthesize( pNtk, p );
+    if ( !Abc_NtkRefactor( pNtk, p ) )
+    {
+        fprintf( pErr, "Refactoring has failed.\n" );
+        return 1;
+    }
     return 0;
 
 usage:
-    fprintf( pErr, "usage: res [-n num] [-c num] [-vh]\n" );
-    fprintf( pErr, "\t         performs technology-independent resynthesis of the AIG\n" );
-    fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", p->nNodeSizeMax );  
-    fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", p->nConeSizeMax );  
-    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", p->fVerbose? "yes": "no" );
+    fprintf( pErr, "usage: refactor [-n num] [-c num] [-vh]\n" );
+    fprintf( pErr, "\t         performs technology-independent refactoring of the AIG\n" );
+    fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );  
+    fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax );  
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -2001,6 +2099,56 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    Abc_NtkShortNames( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: short_names [-h]\n" );
+    fprintf( pErr, "\t         replaces PI/PO/latch names by short char strings\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6acded6e..b6d15951 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -88,7 +88,9 @@ typedef struct Abc_Obj_t_     Abc_Obj_t;
 typedef struct Abc_Ntk_t_     Abc_Ntk_t;
 typedef struct Abc_Aig_t_     Abc_Aig_t;
 typedef struct Abc_ManTime_t_ Abc_ManTime_t;
-typedef struct Abc_ManRes_t_  Abc_ManRes_t;
+typedef struct Abc_ManCut_t_  Abc_ManCut_t;
+typedef struct Abc_ManRef_t_  Abc_ManRef_t;
+typedef struct Abc_ManRwr_t_  Abc_ManRwr_t;
 typedef struct Abc_Time_t_    Abc_Time_t;
 
 struct Abc_Time_t_
@@ -102,8 +104,8 @@ struct Abc_Obj_t_ // 12 words
 {
     // high-level information
     unsigned         Type    :  4;  // the object type
-    unsigned         Unused  :  2;  // currently unused
-    unsigned         Id      : 26;  // the ID of the object
+    unsigned         fExor   :  1;  // marks AIG node that is a root of EXOR
+    unsigned         Id      : 27;  // the ID of the object
     // internal information
     unsigned         fMarkA  :  1;  // the multipurpose mark
     unsigned         fMarkB  :  1;  // the multipurpose mark
@@ -163,30 +165,6 @@ struct Abc_Ntk_t_
     Extra_MmStep_t * pMmStep;       // memory manager for arrays
 };
 
-struct Abc_ManRes_t_
-{
-    // user specified parameters
-    int              nNodeSizeMax;  // the limit on the size of the supernode
-    int              nConeSizeMax;  // the limit on the size of the containing cone
-    int              fVerbose;      // the verbosity flag
-    // internal parameters
-    DdManager *      dd;            // the BDD manager
-    DdNode *         bCubeX;        // the cube of PI variables
-    Abc_Obj_t *      pNode;         // the node currently considered
-    Vec_Ptr_t *      vFaninsNode;   // fanins of the supernode
-    Vec_Ptr_t *      vInsideNode;   // inside of the supernode
-    Vec_Ptr_t *      vFaninsCone;   // fanins of the containing cone
-    Vec_Ptr_t *      vInsideCone;   // inside of the containing cone
-    Vec_Ptr_t *      vVisited;      // the visited nodes
-    Vec_Str_t *      vCube;         // temporary cube for generating covers
-    Vec_Int_t *      vForm;         // the factored form (temporary)
-    // runtime statistics
-    int              time1;
-    int              time2;
-    int              time3;
-    int              time4;
-};
-
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
@@ -287,6 +265,7 @@ static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj-
 static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
 static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
 static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )   { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
 static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                               }
 static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                               }
 static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                               }
@@ -363,24 +342,18 @@ static inline bool        Abc_LatchIsInitDc( Abc_Obj_t * pLatch )   { assert(Abc
         if ( pObj = Abc_NtkLatch(pNtk, i) )
 // inputs and outputs
 #define Abc_NtkForEachPi( pNtk, pPi, i )                                 \
-    for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ )                           \
-        if ( pPi = Abc_NtkPi(pNtk, i) )
+    for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ )
 #define Abc_NtkForEachPo( pNtk, pPo, i )                                 \
-    for ( i = 0; i < Abc_NtkPoNum(pNtk); i++ )                           \
-        if ( pPo = Abc_NtkPo(pNtk, i) )
-#define Abc_NtkForEachCi( pNtk, pPi, i )                                 \
-    for ( i = 0; i < Abc_NtkCiNum(pNtk); i++ )                           \
-        if ( pPi = Abc_NtkCi(pNtk, i) )
-#define Abc_NtkForEachCo( pNtk, pPo, i )                                 \
-    for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ )                           \
-        if ( pPo = Abc_NtkCo(pNtk, i) )
+    for ( i = 0; (i < Abc_NtkPoNum(pNtk)) && (((pPo) = Abc_NtkPo(pNtk, i)), 1); i++ )
+#define Abc_NtkForEachCi( pNtk, pCi, i )                                 \
+    for ( i = 0; (i < Abc_NtkCiNum(pNtk)) && (((pCi) = Abc_NtkCi(pNtk, i)), 1); i++ )
+#define Abc_NtkForEachCo( pNtk, pCo, i )                                 \
+    for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i)), 1); i++ )
 // fanin and fanouts
 #define Abc_ObjForEachFanin( pObj, pFanin, i )                           \
-    for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )                        \
-        if ( pFanin = Abc_ObjFanin(pObj, i) )
+    for ( i = 0; (i < Abc_ObjFaninNum(pObj)) && (((pFanin) = Abc_ObjFanin(pObj, i)), 1); i++ )
 #define Abc_ObjForEachFanout( pObj, pFanout, i )                         \
-    for ( i = 0; i < Abc_ObjFanoutNum(pObj); i++ )                       \
-        if ( pFanout = Abc_ObjFanout(pObj, i) )
+    for ( i = 0; (i < Abc_ObjFanoutNum(pObj)) && (((pFanout) = Abc_ObjFanout(pObj, i)), 1); i++ )
 // cubes and literals
 #define Abc_SopForEachCube( pSop, nFanins, pCube )                       \
     for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
@@ -398,6 +371,7 @@ extern Abc_Aig_t *        Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew );
 extern void               Abc_AigFree( Abc_Aig_t * pMan );
 extern int                Abc_AigCleanup( Abc_Aig_t * pMan );
 extern bool               Abc_AigCheck( Abc_Aig_t * pMan );
+extern int                Abc_AigGetLevelNum( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_AigConst1( Abc_Aig_t * pMan );
 extern Abc_Obj_t *        Abc_AigReset( Abc_Aig_t * pMan );
 extern Abc_Obj_t *        Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
@@ -405,6 +379,7 @@ extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t
 extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
 extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew );
+extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
 extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
 /*=== abcAttach.c ==========================================================*/
@@ -451,8 +426,9 @@ extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcDfs.c ==========================================================*/
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll );
-extern Vec_Ptr_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
+extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
 extern int                Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
 /*=== abcFanio.c ==========================================================*/
@@ -517,15 +493,34 @@ extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode );
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
+/*=== abcReconv.c ==========================================================*/
+extern Abc_ManCut_t *     Abc_NtkManCutStart();
+extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
+extern void               Abc_NodeFindCut( Abc_ManCut_t * p );
+extern DdNode *           Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+extern void               Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult );
 /*=== abcRefs.c ==========================================================*/
 extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
-extern int                Abc_NodeMffcRemove( Abc_Obj_t * pNode );
+extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 /*=== abcRenode.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcRes.c ==========================================================*/
-extern Abc_ManRes_t *     Abc_NtkManResStart();
-extern void               Abc_NtkManResStop( Abc_ManRes_t * p );
+extern int                Abc_NtkRewrite( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p );
+/*=== abcResRef.c ==========================================================*/
+extern Abc_ManRef_t *     Abc_NtkManRefStart();
+extern void               Abc_NtkManRefStop( Abc_ManRef_t * p );
+extern bool               Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode );
+extern Vec_Int_t *        Abc_NtkManRefResult( Abc_ManRef_t * p ); 
+/*=== abcResRwr.c ==========================================================*/
+extern Abc_ManRwr_t *     Abc_NtkManRwrStart( char * pFileName );
+extern void               Abc_NtkManRwrStop( Abc_ManRwr_t * p );
+extern void               Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk );
+extern void               Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode );
+extern int                Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode );
+extern Vec_Int_t *        Abc_NtkManRwrDecs( Abc_ManRwr_t * p );
+extern Vec_Ptr_t *        Abc_NtkManRwrFanins( Abc_ManRwr_t * p );
 /*=== abcSat.c ==========================================================*/
 extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
@@ -565,6 +560,7 @@ extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_In
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_Obj_t *        Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcSweep.c ==========================================================*/
@@ -607,6 +603,8 @@ extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
 extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
 extern void               Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
+extern int                Abc_NtkCountExors( Abc_Ntk_t * pNtk );
+extern bool               Abc_NodeIsExorType( Abc_Obj_t * pNode );
 extern bool               Abc_NodeIsMuxType( Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
 extern int                Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk );
@@ -619,6 +617,7 @@ extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
 extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
 extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
 extern void               Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
+extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 7e4cf33f..2f123dd3 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -23,18 +23,20 @@
 /*
     AIG is an And-Inv Graph with structural hashing.
     It is always structurally hashed. It means that at any time:
+    - for each AND gate, there are no other AND gates with the same children
     - the constants are propagated
     - there is no single-input nodes (inverters/buffers)
-    - for each AND gate, there are no other AND gates with the same children.
+    - there are no dangling nodes (the nodes without fanout)
+    - the level of each AND gate reflects the levels of this fanins
+    - the EXOR-status of each node is up-to-date
     The operations that are performed on AIG:
     - building new nodes (Abc_AigAnd)
-    - elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc)
-    - propagation of constants (Abc_AigReplace)
-    - variable substitution (Abc_AigReplace)
-
+    - performing elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc)
+    - replacing one node by another (Abc_AigReplace)
+    - propagating constants (Abc_AigReplace)
     When AIG is duplicated, the new graph is struturally hashed too.
     If this repeated hashing leads to fewer nodes, it means the original
-    AIG was not strictly hashed (using the three criteria above).
+    AIG was not strictly hashed (one of the conditions above is violated).
 */
 
 ////////////////////////////////////////////////////////////////////////
@@ -54,6 +56,7 @@ struct Abc_Aig_t_
     Vec_Ptr_t *       vStackDelete;      // the nodes to be deleted
     Vec_Ptr_t *       vStackReplaceOld;  // the nodes to be replaced
     Vec_Ptr_t *       vStackReplaceNew;  // the nodes to be used for replacement
+    Vec_Vec_t *       vLevels;           // the nodes to be updated
 };
 
 // iterators through the entries in the linked lists of nodes
@@ -81,6 +84,7 @@ static void        Abc_AigResize( Abc_Aig_t * pMan );
 // incremental AIG procedures
 static void        Abc_AigReplace_int( Abc_Aig_t * pMan );
 static void        Abc_AigDelete_int( Abc_Aig_t * pMan );
+static void        Abc_AigUpdateLevel_int( Abc_Aig_t * pMan );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -111,6 +115,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan->vStackDelete     = Vec_PtrAlloc( 100 );
     pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
     pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
+    pMan->vLevels          = Vec_VecAlloc( 100 );
     // save the current network
     pMan->pNtkAig = pNtkAig;
     // allocate constant nodes
@@ -193,6 +198,7 @@ void Abc_AigFree( Abc_Aig_t * pMan )
     assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
     assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
     // free the table
+    Vec_VecFree( pMan->vLevels );
     Vec_PtrFree( pMan->vStackDelete );
     Vec_PtrFree( pMan->vStackReplaceOld );
     Vec_PtrFree( pMan->vStackReplaceNew );
@@ -268,12 +274,11 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
             printf( "Abc_AigCheck: The AIG has non-standard nodes.\n" );
             return 0;
         }
+        if ( pObj->Level != 1 + ABC_MAX( Abc_ObjFanin0(pObj)->Level, Abc_ObjFanin1(pObj)->Level ) )
+            printf( "Abc_AigCheck: Node \"%s\" has level that does not agree with the fanin levels.\n", Abc_ObjName(pObj) );
         pAnd = Abc_AigAndLookup( pMan, Abc_ObjChild0(pObj), Abc_ObjChild1(pObj) );
         if ( pAnd != pObj )
-        {
             printf( "Abc_AigCheck: Node \"%s\" is not in the structural hashing table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
     }
     // count the number of nodes in the table
     Counter = 0;
@@ -290,6 +295,30 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, LevelsMax;
+    assert( Abc_NtkIsAig(pNtk) );
+    // perform the traversal
+    LevelsMax = 0;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        if ( LevelsMax < (int)Abc_ObjFanin0(pNode)->Level )
+            LevelsMax = (int)Abc_ObjFanin0(pNode)->Level;
+    return LevelsMax;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Read the constant 1 node.]
 
   Description []
@@ -349,6 +378,7 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     Abc_ObjAddFanin( pAnd, p1 );
     // set the level of the new node
     pAnd->Level      = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level ); 
+    pAnd->fExor      = Abc_NodeIsExorType(pAnd);
     // add the node to the corresponding linked list in the table
     Key = Abc_HashKey2( p0, p1, pMan->nBins );
     pAnd->pNext      = pMan->pBins[Key];
@@ -612,6 +642,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
         Abc_AigReplace_int( pMan );
     while ( Vec_PtrSize(pMan->vStackDelete) )
         Abc_AigDelete_int( pMan );
+    Abc_AigUpdateLevel_int( pMan );
 }
 
 /**Function*************************************************************
@@ -627,8 +658,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
 ***********************************************************************/
 void Abc_AigReplace_int( Abc_Aig_t * pMan )
 {
-    Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew;
-    int k, iFanin;
+    Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout;
+    int k, v, iFanin;
     // get the pair of nodes to replace
     assert( Vec_PtrSize(pMan->vStackReplaceOld) > 0 );
     pOld = Vec_PtrPop( pMan->vStackReplaceOld );
@@ -668,6 +699,12 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         Abc_ObjRemoveFanins( pFanout );
         // update the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+        // schedule the updated node for updating level
+        Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
+        // the node has changed, update EXOR status of the fanouts
+        Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
+            if ( Abc_NodeIsAigAnd(pFanoutFanout) )
+                pFanoutFanout->fExor = Abc_NodeIsExorType(pFanoutFanout);
     }
     // schedule deletion of the old node
     if ( Abc_NodeIsAigAnd(pOld) && pOld->fMarkA == 0 )
@@ -688,6 +725,25 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld )
+{
+    assert( Vec_PtrSize(pMan->vStackDelete) == 0 );
+    Vec_PtrPush( pMan->vStackDelete, pOld );
+    while ( Vec_PtrSize(pMan->vStackDelete) )
+        Abc_AigDelete_int( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs internal deletion step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_AigDelete_int( Abc_Aig_t * pMan )
 {
     Abc_Obj_t * pNode, * pFanin;
@@ -717,6 +773,52 @@ void Abc_AigDelete_int( Abc_Aig_t * pMan )
     Abc_NtkDeleteObj( pNode );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Updates the level of the node after it has changed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
+{
+    Abc_Obj_t * pNode, * pFanout;
+    Vec_Ptr_t * vVec;
+    unsigned LevelNew;
+    int i, k, v;
+
+    // go through the nodes and update the level of their fanouts
+    Vec_VecForEachLevel( pMan->vLevels, vVec, i )
+    {
+        if ( Vec_PtrSize(vVec) == 0 )
+            continue;
+        Vec_PtrForEachEntry( vVec, pNode, k )
+        {
+            assert( Abc_ObjIsNode(pNode) );
+            Abc_ObjForEachFanout( pNode, pFanout, v )
+            {
+                if ( Abc_ObjIsCo(pFanout) )
+                    continue;
+                // get the new level of this fanout
+                LevelNew = 1 + ABC_MAX( Abc_ObjFanin0(pFanout)->Level, Abc_ObjFanin1(pFanout)->Level );
+                if ( pFanout->Level == LevelNew ) // no change
+                    continue;
+                // update the fanout level
+                pFanout->Level = LevelNew;
+                // add the fanout to be updated
+                Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout );
+            }
+        }
+        Vec_PtrClear( vVec );
+    }
+}
+
+
+
 
 
 
@@ -775,6 +877,7 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
     return 0;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index f46dbb60..ead24663 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -395,7 +395,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
             Value = 0;
         }
     }
-/*
+
     // make sure fanins are not duplicated
     for ( i = 0; i < pObj->vFanins.nSize; i++ )
         for ( k = i + 1; k < pObj->vFanins.nSize; k++ )
@@ -412,7 +412,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj )
                 printf( "Warning: Node %s has", Abc_ObjName(pObj) );
                 printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) );
             }
-*/
+
     return Value;
 }
 
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 6313a1c5..40fbf799 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -26,7 +26,8 @@
 
 static void     Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 static void     Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-static void     Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels );
+static void     Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void     Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels );
 static int      Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode );
 static bool     Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode );
 
@@ -49,23 +50,23 @@ static bool     Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode );
 Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll )
 {
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode;
+    Abc_Obj_t * pObj;
     int i;
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
     vNodes = Vec_PtrAlloc( 100 );
-    Abc_NtkForEachCo( pNtk, pNode, i )
+    Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        Abc_NodeSetTravIdCurrent( pNode );
-        Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode)), vNodes );
+        Abc_NodeSetTravIdCurrent( pObj );
+        Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)), vNodes );
     }
     // collect dangling nodes if asked to
     if ( fCollectAll )
     {
-        Abc_NtkForEachNode( pNtk, pNode, i )
-            if ( !Abc_NodeIsTravIdCurrent(pNode) )
-                Abc_NtkDfs_rec( pNode, vNodes );
+        Abc_NtkForEachNode( pNtk, pObj, i )
+            if ( !Abc_NodeIsTravIdCurrent(pObj) )
+                Abc_NtkDfs_rec( pObj, vNodes );
     }
     return vNodes;
 }
@@ -138,6 +139,75 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the reverse DFS ordered array of logic nodes.]
+
+  Description [Collects only the internal nodes, leaving CIs and CO.
+  However it marks with the current TravId both CIs and COs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k;
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( pObj );
+        pObj = Abc_ObjFanout0Ntk(pObj);
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            Abc_NtkDfsReverse_rec( pFanout, vNodes );
+    }
+    // add constant nodes in the end
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( Abc_NodeIsConst(pObj) )
+            Vec_PtrPush( vNodes, pObj );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( !Abc_ObjIsNet(pNode) );
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // skip the CI
+    if ( Abc_ObjIsCo(pNode) )
+        return;
+    assert( Abc_ObjIsNode( pNode ) );
+    // visit the transitive fanin of the node
+    pNode = Abc_ObjFanout0Ntk(pNode);
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        Abc_NtkDfsReverse_rec( pFanout, vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Returns the DFS ordered array of logic nodes.]
 
   Description [Collects only the internal nodes, leaving CIs and CO.
@@ -220,20 +290,21 @@ void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi )
+Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi )
 {
-    Vec_Ptr_t * vLevels;
+    Vec_Vec_t * vLevels;
     Abc_Obj_t * pFanout;
     int i;
     assert( fTfi == 0 );
     assert( !Abc_NtkIsNetlist(pNode->pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNode->pNtk );
-    vLevels = Vec_PtrAlloc( 100 );
+    vLevels = Vec_VecAlloc( 100 );
     if ( Abc_ObjIsNode(pNode) )
         Abc_DfsLevelizedTfo_rec( pNode, vLevels );
     else
     {
+        assert( Abc_ObjIsCi(pNode) );
         Abc_NodeSetTravIdCurrent( pNode );
         Abc_ObjForEachFanout( pNode, pFanout, i )
             Abc_DfsLevelizedTfo_rec( pFanout, vLevels );
@@ -252,7 +323,7 @@ Vec_Ptr_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels )
+void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels )
 {
     Abc_Obj_t * pFanout;
     int i;
@@ -266,14 +337,7 @@ void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLevels )
         return;
     assert( Abc_ObjIsNode(pNode) );
     // add the node to the structure
-    if ( vLevels->nSize <= (int)pNode->Level )
-    {
-        Vec_PtrGrow( vLevels, pNode->Level + 1 );
-        for ( i = vLevels->nSize; i <= (int)pNode->Level; i++ )
-            vLevels->pArray[i] = Vec_PtrAlloc( 16 );
-        vLevels->nSize = pNode->Level + 1;
-    }
-    Vec_PtrPush( vLevels->pArray[pNode->Level], pNode );
+    Vec_VecPush( vLevels, pNode->Level, pNode );
     // visit the TFO
     Abc_ObjForEachFanout( pNode, pFanout, i )
         Abc_DfsLevelizedTfo_rec( pFanout, vLevels );
@@ -373,7 +437,7 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
     Abc_NtkIncrementTravId( pNtk );   
     // pNode->TravId == pNet->nTravIds      means "pNode is on the path"
     // pNode->TravId == pNet->nTravIds - 1  means "pNode is visited but is not on the path"
-    // pNode->TravId < pNet->nTravIds - 1   means "pNode is not visited"
+    // pNode->TravId <  pNet->nTravIds - 1  means "pNode is not visited"
     // traverse the network to detect cycles
     fAcyclic = 1;
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -381,12 +445,12 @@ bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk )
         pNode = Abc_ObjFanin0Ntk(Abc_ObjFanin0(pNode));
         if ( Abc_NodeIsTravIdPrevious(pNode) )
             continue;
-        // traverse the output logic cone to detect the combinational loops
-        if ( ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) ) == 0 ) 
-        { // stop as soon as the first loop is detected
-            fprintf( stdout, " (the output node)\n" );
-            break;
-        }
+        // traverse the output logic cone
+        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pNode) )
+            continue;
+        // stop as soon as the first loop is detected
+        fprintf( stdout, " (cone of CO \"%s\")\n", Abc_ObjName(pNode) );
+        break;
     }
     return fAcyclic;
 }
@@ -408,7 +472,6 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int fAcyclic, i;
     assert( !Abc_ObjIsNet(pNode) );
-    // skip the PI
     if ( Abc_ObjIsCi(pNode) )
         return 1;
     assert( Abc_ObjIsNode( pNode ) );
@@ -433,14 +496,12 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
         // check if the fanin is visited
         if ( Abc_NodeIsTravIdPrevious(pFanin) ) 
             continue;
-        // traverse searching for the loop
-        fAcyclic = Abc_NtkIsAcyclic_rec( pFanin );
+        // traverse the fanin's cone searching for the loop
+        if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
+            continue;
         // return as soon as the loop is detected
-        if ( fAcyclic == 0 ) 
-        {
-            fprintf( stdout, "  <--  %s", Abc_ObjName(pNode) );
-            return 0;
-        }
+        fprintf( stdout, " <-- %s", Abc_ObjName(pNode) );
+        return 0;
     }
     // mark this node as a visited node
     Abc_NodeSetTravIdPrevious( pNode );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index a040758e..dd3fa033 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -195,7 +195,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode )
 {
-    int fVerify = 1;
+    int fVerify = 0;
     char * pSop;
     DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
     int nCubes, nCubes0, nCubes1, fPhase;
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index e85b02d7..dc7a2e7b 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -42,6 +42,8 @@
 ***********************************************************************/
 void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
+    int Num;
+
     fprintf( pFile, "%-15s:",       pNtk->pName );
     fprintf( pFile, "  i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
@@ -58,7 +60,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else if ( Abc_NtkIsAig(pNtk) )
     {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
-        fprintf( pFile, "  choice = %5d", Abc_NtkCountChoiceNodes(pNtk) );
+        if ( Num = Abc_NtkCountChoiceNodes(pNtk) )
+            fprintf( pFile, " (choice = %d)", Num );
+        if ( Num = Abc_NtkCountExors(pNtk) )
+            fprintf( pFile, " (exor = %d)", Num );
     }
     else if ( Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
@@ -84,7 +89,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         assert( 0 );
     }
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkIsAig(pNtk) )
+        fprintf( pFile, "  lev = %3d", Abc_AigGetLevelNum(pNtk) );
+    else if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
 
     fprintf( pFile, "\n" );
@@ -360,14 +367,49 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
 {
     Abc_Obj_t * pNode;
     int i, Length;
-    assert( Abc_NtkIsAig(pNtk) );
 
     // print the delay profile
-    if ( fProfile )
+    if ( fProfile && Abc_NtkIsMapped(pNtk) )
+    {
+        int nIntervals = 12;
+        float DelayMax, DelayCur, DelayDelta;
+        int * pLevelCounts;
+        int DelayInt, nOutsSum, nOutsTotal;
+
+        // get the max delay and delta
+        DelayMax   = Abc_NtkDelayTrace( pNtk );
+        DelayDelta = DelayMax/nIntervals;
+        // collect outputs by delay
+        pLevelCounts = ALLOC( int, nIntervals );
+        memset( pLevelCounts, 0, sizeof(int) * nIntervals );
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            DelayCur  = Abc_NodeReadArrival( Abc_ObjFanin0(pNode) )->Worst;
+            DelayInt  = (int)(DelayCur / DelayDelta);
+            if ( DelayInt >= nIntervals )
+                DelayInt = nIntervals - 1;
+            pLevelCounts[DelayInt]++;
+        }
+
+        nOutsSum   = 0;
+        nOutsTotal = Abc_NtkCoNum(pNtk);
+        for ( i = 0; i < nIntervals; i++ )
+        {
+            nOutsSum += pLevelCounts[i];
+            printf( "[%8.2f - %8.2f] :   COs = %4d.   %5.1f %%\n", 
+                DelayDelta * i, DelayDelta * (i+1), pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal );
+        }
+        free( pLevelCounts );
+        return;
+    }
+    else if ( fProfile )
     {
         int LevelMax, * pLevelCounts;
         int nOutsSum, nOutsTotal;
 
+        if ( !Abc_NtkIsAig(pNtk) )
+            Abc_NtkGetLevelNum(pNtk);
+
         LevelMax = 0;
         Abc_NtkForEachCo( pNtk, pNode, i )
             if ( LevelMax < (int)Abc_ObjFanin0(pNode)->Level )
@@ -385,8 +427,10 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
                 nOutsSum += pLevelCounts[i];
                 printf( "Level = %4d.  COs = %4d.   %5.1f %%\n", i, pLevelCounts[i], 100.0 * nOutsSum/nOutsTotal );
             }
+        free( pLevelCounts );
         return;
     }
+    assert( Abc_NtkIsAig(pNtk) );
 
     // find the longest name
     Length = 0;
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
new file mode 100644
index 00000000..7f4588a2
--- /dev/null
+++ b/src/base/abc/abcReconv.c
@@ -0,0 +1,435 @@
+/**CFile****************************************************************
+
+  FileName    [abcRes.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Reconvergence=driven cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ft.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Abc_ManCut_t_
+{
+    // user specified parameters
+    int              nNodeSizeMax;  // the limit on the size of the supernode
+    int              nConeSizeMax;  // the limit on the size of the containing cone
+    // internal parameters
+    Abc_Obj_t *      pNode;         // the node currently considered
+    Vec_Ptr_t *      vFaninsNode;   // fanins of the supernode
+    Vec_Ptr_t *      vInsideNode;   // inside of the supernode
+    Vec_Ptr_t *      vFaninsCone;   // fanins of the containing cone
+    Vec_Ptr_t *      vInsideCone;   // inside of the containing cone
+    Vec_Ptr_t *      vVisited;      // the visited nodes
+};
+
+static int           Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit );
+static int           Abc_NodeGetFaninCost( Abc_Obj_t * pNode );
+static void          Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+static void          Abc_NodeConeMark( Vec_Ptr_t * vVisited );
+static void          Abc_NodeConeUnmark( Vec_Ptr_t * vVisited );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFindCut( Abc_ManCut_t * p )
+{
+    Abc_Obj_t * pNode = p->pNode;
+    int i;
+
+    // mark TFI using fMarkA
+    Vec_PtrClear( p->vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, p->vVisited );
+
+    // start the reconvergence-driven node
+    Vec_PtrClear( p->vInsideNode );
+    Vec_PtrClear( p->vFaninsNode );
+    Vec_PtrPush( p->vFaninsNode, pNode );
+    pNode->fMarkB = 1;
+
+    // compute reconvergence-driven node
+    while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) );
+
+    // compute reconvergence-driven cone
+    Vec_PtrClear( p->vInsideCone );
+    Vec_PtrClear( p->vFaninsCone );
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // copy the node into the cone
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            Vec_PtrPush( p->vInsideCone, pNode );
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            Vec_PtrPush( p->vFaninsCone, pNode );
+        // compute reconvergence-driven cone
+        while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) );
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideCone, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsCone, pNode, i )
+            pNode->fMarkB = 0;
+    }
+    else
+    {
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            pNode->fMarkB = 0;
+    }
+
+    // unmark TFI using fMarkA
+    Abc_NodeConeUnmark( p->vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit )
+{
+    Abc_Obj_t * pNode, * pFaninBest, * pNext;
+    int CostBest, CostCur, i;
+    // find the best fanin
+    CostBest   = 100;
+    pFaninBest = NULL;
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+    {
+        CostCur = Abc_NodeGetFaninCost( pNode );
+        if ( CostBest > CostCur )
+        {
+            CostBest   = CostCur;
+            pFaninBest = pNode;
+        }
+    }
+    if ( pFaninBest == NULL )
+        return 0;
+    assert( CostBest < 3 );
+    if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+        return 0;
+    assert( Abc_ObjIsNode(pFaninBest) );
+    // remove the node from the array
+    Vec_PtrRemove( vFanins, pFaninBest );
+    // add the node to the set
+    Vec_PtrPush( vInside, pFaninBest );
+    // add the left child to the fanins
+    pNext = Abc_ObjFanin0(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    // add the right child to the fanins
+    pNext = Abc_ObjFanin1(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    assert( vFanins->nSize <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the fanin cost.]
+
+  Description [Returns the number of fanins that will be brought in.
+  Returns large number if the node cannot be added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( pNode->fMarkA == 1 );  // this node is in the TFI
+    assert( pNode->fMarkB == 1 );  // this node is in the constructed cone
+    // check the PI node
+    if ( !Abc_ObjIsNode(pNode) )
+        return 999;
+    // check the fanouts
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set
+            return 999;
+    // the fanouts are in the TFI and inside the constructed cone
+    // return the number of fanins that will be on the boundary if this node is added
+    return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    if ( pNode->fMarkA == 1 )
+        return;
+    // visit transitive fanin 
+    if ( Abc_ObjIsNode(pNode) )
+    {
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+    }
+    assert( pNode->fMarkA == 0 );
+    pNode->fMarkA = 1;
+    Vec_PtrPush( vVisited, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns BDD representing the logic function of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    int i;
+    // mark the fanins of the cone
+    Abc_NodeConeMark( vFanins );
+    // collect the nodes in the DFS order
+    Vec_PtrClear( vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, vVisited );
+    // unmark both sets
+    Abc_NodeConeUnmark( vFanins );
+    Abc_NodeConeUnmark( vVisited );
+    // set the elementary BDDs
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)pbVars[i];
+    // compute the BDDs for the collected nodes
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+    {
+        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+    }
+    Cudd_Ref( bFunc );
+    // dereference the intermediate ones
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManCut_t * Abc_NtkManCutStart()
+{
+    Abc_ManCut_t * p;
+    p = ALLOC( Abc_ManCut_t, 1 );
+    memset( p, 0, sizeof(Abc_ManCut_t) );
+    p->vFaninsNode = Vec_PtrAlloc( 100 );
+    p->vInsideNode = Vec_PtrAlloc( 100 );
+    p->vFaninsCone = Vec_PtrAlloc( 100 );
+    p->vInsideCone = Vec_PtrAlloc( 100 );
+    p->vVisited    = Vec_PtrAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManCutStop( Abc_ManCut_t * p )
+{
+    Vec_PtrFree( p->vFaninsNode );
+    Vec_PtrFree( p->vInsideNode );
+    Vec_PtrFree( p->vFaninsCone );
+    Vec_PtrFree( p->vInsideCone );
+    Vec_PtrFree( p->vVisited    );
+    free( p );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the TFO of the cut in the topological order.]
+
+  Description [TFO of the cut is defined as a set of nodes, for which the cut
+  is a cut, that is, every path from the collected nodes to the CIs goes through 
+  a node in the cut. The nodes are collected if their level does not exceed
+  the given number (LevelMax). The nodes are returned in the topological order.
+  If the root node is given, its MFFC is marked, so that the collected nodes
+  do not contain any nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, 
+    Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult )
+{
+    Vec_Ptr_t * vVec;
+    Abc_Obj_t * pNode, * pFanout;
+    int i, k, v, LevelMin;
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // assuming that the structure is clean
+    Vec_VecForEachLevel( vLevels, vVec, i )
+        assert( vVec->nSize == 0 );
+
+    // put fanins into the structure while labeling them
+    Abc_NtkIncrementTravId( pNtk );
+    LevelMin = ABC_INFINITY;
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+    {
+        if ( pNode->Level > (unsigned)LevelMax )
+            continue;
+        Abc_NodeSetTravIdCurrent( pNode );
+        Vec_VecPush( vLevels, pNode->Level, pNode );
+        if ( LevelMin < (int)pNode->Level )
+            LevelMin = pNode->Level;
+    }
+    assert( LevelMin >= 0 );
+
+    // mark MFFC 
+    if ( pRoot )
+        Abc_NodeMffcLabel( pRoot );
+
+    // go through the levels up
+    Vec_PtrClear( vResult );
+    Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax )
+    {
+        // if the node is not marked, it is not a fanin
+        if ( !Abc_NodeIsTravIdCurrent(pNode) )
+        {
+            // check if it belongs to the TFO
+            if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) || 
+                 !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
+                 continue;
+            // save the node in the TFO and label it
+            Vec_PtrPush( vResult, pNode );
+            Abc_NodeSetTravIdCurrent( pNode );
+        }
+        // go through the fanouts and add them to the structure if they meet the conditions
+        Abc_ObjForEachFanout( pNode, pFanout, v )
+        {
+            // skip if fanout is a CO or its level exceeds
+            if ( Abc_ObjIsCo(pFanout) || pFanout->Level > (unsigned)LevelMax )
+                continue;
+            // skip if it is already added or if it is in MFFC
+            if ( Abc_NodeIsTravIdCurrent(pFanout) )
+                continue;
+            // add it to the structure but do not mark it (until tested later)
+            Vec_VecPush( vLevels, pFanout->Level, pFanout );
+        }
+    }
+
+    // clear the levelized structure
+    Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax )
+        Vec_PtrClear( vVec );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index eee0530a..96e8a3b2 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference );
+static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -47,7 +47,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
     nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference
-    nConeSize2 = Abc_NodeRefDeref( pNode, 0, 1 ); // reference
+    nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0 ); // reference
     assert( nConeSize1 == nConeSize2 );
     assert( nConeSize1 > 0 );
     return nConeSize1;
@@ -55,7 +55,7 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure returns the size of the MFFC of the node.]
+  Synopsis    [Lavels MFFC with the current traversal ID.]
 
   Description []
                
@@ -64,11 +64,16 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeMffcRemove( Abc_Obj_t * pNode )
+int Abc_NodeMffcLabel( Abc_Obj_t * pNode )
 {
+    int nConeSize1, nConeSize2;
     assert( !Abc_ObjIsComplement( pNode ) );
     assert( Abc_ObjIsNode( pNode ) );
-    return Abc_NodeRefDeref( pNode, 1, 0 ); // dereference
+    nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference
+    nConeSize2 = Abc_NodeRefDeref( pNode, 1, 1 ); // reference
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    return nConeSize1;
 }
 
 /**Function*************************************************************
@@ -82,10 +87,12 @@ int Abc_NodeMffcRemove( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference )
+int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel )
 {
     Abc_Obj_t * pNode0, * pNode1;
     int Counter;
+    if ( fLabel )
+        Abc_NodeSetTravIdCurrent( pNode );
     if ( Abc_ObjIsCi(pNode) )
         return 0;
     pNode0 = Abc_ObjFanin( pNode, 0 );
@@ -94,34 +101,18 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference )
     if ( fReference )
     {
         if ( pNode0->vFanouts.nSize++ == 0 )
-        {
-            Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference );
-            if ( fFanouts )  
-                Abc_ObjAddFanin( pNode, pNode0 );
-        }
+            Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel );
         if ( pNode1->vFanouts.nSize++ == 0 )
-        {
-            Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference );
-            if ( fFanouts )  
-                Abc_ObjAddFanin( pNode, pNode1 );
-        }
+            Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel );
     }
     else
     {
         assert( pNode0->vFanouts.nSize > 0 );
         assert( pNode1->vFanouts.nSize > 0 );
         if ( --pNode0->vFanouts.nSize == 0 )
-        {
-            Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference );
-            if ( fFanouts )  
-                Abc_ObjDeleteFanin( pNode, pNode0 );
-        }
+            Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel );
         if ( --pNode1->vFanouts.nSize == 0 )
-        {
-            Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference );
-            if ( fFanouts )  
-                Abc_ObjDeleteFanin( pNode, pNode1 );
-        }
+            Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel );
     }
     return Counter;
 }
diff --git a/src/base/abc/abcRes.c b/src/base/abc/abcRes.c
index 221b6f87..7ab60376 100644
--- a/src/base/abc/abcRes.c
+++ b/src/base/abc/abcRes.c
@@ -24,21 +24,8 @@
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
-static void        Abc_NodeResyn( Abc_ManRes_t * p );
 
-static void        Abc_NodeFindCut( Abc_ManRes_t * p );
-static int         Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit );
-static int         Abc_NodeGetFaninCost( Abc_Obj_t * pNode );
-static void        Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
-static void        Abc_NodeConeMark( Vec_Ptr_t * vVisited );
-static void        Abc_NodeConeUnmark( Vec_Ptr_t * vVisited );
-
-static Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p );
-static DdNode *    Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
-
-static int         Abc_NodeDecide( Abc_ManRes_t * p );
-static void        Abc_NodeUpdate( Abc_ManRes_t * p );
+static void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -46,422 +33,76 @@ static void        Abc_NodeUpdate( Abc_ManRes_t * p );
 
 /**Function*************************************************************
 
-  Synopsis    [Performs incremental resynthesis of the AIG.]
+  Synopsis    [Performs incremental rewriting of the AIG.]
 
-  Description [Starting from each node, computes a reconvergence-driven cut, 
-  derives BDD of the cut function, constructs ISOP, factors the cover, 
-  and replaces the current implementation of the MFFC of the cut by the 
-  new factored form if the number of AIG nodes is reduced. Returns the
-  number of AIG nodes saved.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p )
+int Abc_NtkRewrite( Abc_Ntk_t * pNtk )
 {
     int fCheck = 1;
     ProgressBar * pProgress;
+    Abc_ManRwr_t * p;
     Abc_Obj_t * pNode;
-    int i, Counter, Approx;
+    int i, nNodes, nGain;
 
     assert( Abc_NtkIsAig(pNtk) );
+    // start the rewriting manager
+    p = Abc_NtkManRwrStart( "data.aaa" );
+    Abc_NtkManRwrStartCuts( p, pNtk );
 
-    // start the BDD manager
-    p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_zddVarsFromBddVars( p->dd, 2 );
-    p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size );   Cudd_Ref( p->bCubeX );
-
-    // remember the number of nodes
-    Counter = Abc_NtkNodeNum( pNtk );
-    // resynthesize each node
-    pProgress = Extra_ProgressBarStart( stdout, 100 );
+    // resynthesize each node once
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        Approx = (int)(100.0 * i / Abc_NtkObjNumMax(pNtk) );
-        Extra_ProgressBarUpdate( pProgress, Approx, NULL );
-        p->pNode = pNode;
-        Abc_NodeResyn( p );
+        Extra_ProgressBarUpdate( pProgress, nNodes, NULL );
+        // compute the cuts of the node
+        Abc_NodeRwrComputeCuts( p, pNode );
+        // for each cut, try to resynthesize it
+        if ( (nGain = Abc_NodeRwrRewrite( p, pNode )) >= 0 )
+            Abc_NodeUpdate( pNode, Abc_NtkManRwrFanins(p), Abc_NtkManRwrDecs(p), nGain );
+        // check the improvement
+        if ( i == nNodes )
+            break;
     }
     Extra_ProgressBarStop( pProgress );
-    Abc_NtkManResStop( p );
 
+    // delete the manager
+    Abc_NtkManRwrStop( p );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtk ) )
     {
-        printf( "Abc_NtkAigResynthesize: The network check has failed.\n" );
-        return -1;
-    }
-    return Abc_NtkNodeNum(pNtk) - Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs resynthesis of one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeResyn( Abc_ManRes_t * p )
-{
-    int RetValue;
-    int clk;
-
-    assert( Abc_ObjIsNode(p->pNode) );
-
-clk = clock();
-    // detect the cut
-    Abc_NodeFindCut( p );
-p->time1 += clock() - clk;
-
-    // refactor the cut
-clk = clock();
-    p->vForm = Abc_NodeRefactor( p );
-p->time2 += clock() - clk;
-
-    // accept or reject the factored form
-clk = clock();
-    RetValue = Abc_NodeDecide( p );
-p->time3 += clock() - clk;
-
-    // modify the network
-clk = clock();
-    if ( RetValue )
-        Abc_NodeUpdate( p );
-p->time4 += clock() - clk;
-
-    // cleanup
-    Vec_IntFree( p->vForm );
-    p->vForm = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finds a reconvergence-driven cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeFindCut( Abc_ManRes_t * p )
-{
-    Abc_Obj_t * pNode = p->pNode;
-    int i;
-
-    // mark TFI using fMarkA
-    Vec_PtrClear( p->vVisited );
-    Abc_NodeConeMarkCollect_rec( pNode, p->vVisited );
-
-    // start the reconvergence-driven node
-    Vec_PtrClear( p->vInsideNode );
-    Vec_PtrClear( p->vFaninsNode );
-    Vec_PtrPush( p->vFaninsNode, pNode );
-    pNode->fMarkB = 1;
-
-    // compute reconvergence-driven node
-    while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) );
-
-    // compute reconvergence-driven cone
-    Vec_PtrClear( p->vInsideCone );
-    Vec_PtrClear( p->vFaninsCone );
-    if ( p->nConeSizeMax > p->nNodeSizeMax )
-    {
-        // copy the node into the cone
-        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
-            Vec_PtrPush( p->vInsideCone, pNode );
-        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
-            Vec_PtrPush( p->vFaninsCone, pNode );
-        // compute reconvergence-driven cone
-        while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) );
-        // unmark the nodes of the sets
-        Vec_PtrForEachEntry( p->vInsideCone, pNode, i )
-            pNode->fMarkB = 0;
-        Vec_PtrForEachEntry( p->vFaninsCone, pNode, i )
-            pNode->fMarkB = 0;
-    }
-    else
-    {
-        // unmark the nodes of the sets
-        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
-            pNode->fMarkB = 0;
-        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
-            pNode->fMarkB = 0;
-    }
-
-    // unmark TFI using fMarkA
-    Abc_NodeConeUnmark( p->vVisited );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finds a reconvergence-driven cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit )
-{
-    Abc_Obj_t * pNode, * pFaninBest, * pNext;
-    int CostBest, CostCur, i;
-    // find the best fanin
-    CostBest   = 100;
-    pFaninBest = NULL;
-    Vec_PtrForEachEntry( vFanins, pNode, i )
-    {
-        CostCur = Abc_NodeGetFaninCost( pNode );
-        if ( CostBest > CostCur )
-        {
-            CostBest   = CostCur;
-            pFaninBest = pNode;
-        }
-    }
-    if ( pFaninBest == NULL )
-        return 0;
-    assert( CostBest < 3 );
-    if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+        printf( "Abc_NtkRewrite: The network check has failed.\n" );
         return 0;
-    assert( Abc_ObjIsNode(pFaninBest) );
-    // remove the node from the array
-    Vec_PtrRemove( vFanins, pFaninBest );
-    // add the node to the set
-    Vec_PtrPush( vInside, pFaninBest );
-    // add the left child to the fanins
-    pNext = Abc_ObjFanin0(pFaninBest);
-    if ( !pNext->fMarkB )
-    {
-        pNext->fMarkB = 1;
-        Vec_PtrPush( vFanins, pNext );
-    }
-    // add the right child to the fanins
-    pNext = Abc_ObjFanin1(pFaninBest);
-    if ( !pNext->fMarkB )
-    {
-        pNext->fMarkB = 1;
-        Vec_PtrPush( vFanins, pNext );
     }
-    assert( vFanins->nSize <= nSizeLimit );
-    // keep doing this
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Evaluate the fanin cost.]
-
-  Description [Returns the number of fanins that will be brought in.
-  Returns large number if the node cannot be added.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanout;
-    int i;
-    assert( pNode->fMarkA == 1 );  // this node is in the TFI
-    assert( pNode->fMarkB == 1 );  // this node is in the constructed cone
-    // check the PI node
-    if ( !Abc_ObjIsNode(pNode) )
-        return 999;
-    // check the fanouts
-    Abc_ObjForEachFanout( pNode, pFanout, i )
-        if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set
-            return 999;
-    // the fanouts are in the TFI and inside the constructed cone
-    // return the number of fanins that will be on the boundary if this node is added
-    return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the TFI cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
-{
-    if ( pNode->fMarkA == 1 )
-        return;
-    // visit transitive fanin 
-    if ( Abc_ObjIsNode(pNode) )
-    {
-        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
-        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
-    }
-    assert( pNode->fMarkA == 0 );
-    pNode->fMarkA = 1;
-    Vec_PtrPush( vVisited, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the TFI cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeConeMark( Vec_Ptr_t * vVisited )
-{
-    int i;
-    for ( i = 0; i < vVisited->nSize; i++ )
-        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the TFI cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited )
-{
-    int i;
-    for ( i = 0; i < vVisited->nSize; i++ )
-        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the factored form of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p )
-{
-    Vec_Int_t * vForm;
-    DdManager * dd = p->dd;
-    DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc;
-    char * pSop;
-    int nFanins;
-
-    assert( p->vFaninsNode->nSize < p->nNodeSizeMax );
-    assert( p->vFaninsCone->nSize < p->nConeSizeMax );
-
-    // get the function of the node
-    bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited );  
-    Cudd_Ref( bFuncNode );
-    nFanins = p->vFaninsNode->nSize;
-    if ( p->nConeSizeMax > p->nNodeSizeMax )
-    {
-        // get the function of the cone
-        bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited );  
-        Cudd_Ref( bFuncCone );
-        // get the care set
-        bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX );   Cudd_Ref( bCare );
-        Cudd_RecursiveDeref( dd, bFuncCone );
-        // compute the on-set and off-set of the function of the node
-        bFuncOn   = Cudd_bddAnd( dd, bFuncNode, bCare );                Cudd_Ref( bFuncOn );
-        bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare );      Cudd_Ref( bFuncOnDc );
-        bFuncOnDc = Cudd_Not( bFuncOnDc );
-        Cudd_RecursiveDeref( dd, bCare );
-        // get the cover
-        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 );
-        Cudd_RecursiveDeref( dd, bFuncOn );
-        Cudd_RecursiveDeref( dd, bFuncOnDc );
-    }
-    else
-    {
-        // get the cover
-        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 );
-    }
-    Cudd_RecursiveDeref( dd, bFuncNode );
-    // derive the factored form
-    vForm = Ft_Factor( pSop );
-    free( pSop );
-    return vForm;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns BDD representing the logic function of the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
-{
-    DdNode * bFunc0, * bFunc1, * bFunc;
-    int i;
-    // mark the fanins of the cone
-    Abc_NodeConeMark( vFanins );
-    // collect the nodes in the DFS order
-    Vec_PtrClear( vVisited );
-    Abc_NodeConeMarkCollect_rec( pNode, vVisited );
-    // unmark both sets
-    Abc_NodeConeUnmark( vFanins );
-    Abc_NodeConeUnmark( vVisited );
-    // set the elementary BDDs
-    Vec_PtrForEachEntry( vFanins, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)pbVars[i];
-    // compute the BDDs for the collected nodes
-    Vec_PtrForEachEntry( vVisited, pNode, i )
-    {
-        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
-        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
-        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
-        pNode->pCopy = (Abc_Obj_t *)bFunc;
-    }
-    Cudd_Ref( bFunc );
-    // dereference the intermediate ones
-    Vec_PtrForEachEntry( vVisited, pNode, i )
-        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
-    Cudd_Deref( bFunc );
-    return bFunc;
-}
-
 
 /**Function*************************************************************
 
-  Synopsis    [Decides whether to accept the given factored form.]
+  Synopsis    [Performs incremental resynthesis of the AIG.]
 
-  Description []
+  Description [Starting from each node, computes a reconvergence-driven cut, 
+  derives BDD of the cut function, constructs ISOP, factors the cover, 
+  and replaces the current implementation of the MFFC of the cut by the 
+  new factored form if the number of AIG nodes is reduced. Returns the
+  number of AIG nodes saved.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int  Abc_NodeDecide( Abc_ManRes_t * p )
+int Abc_NtkRefactor( Abc_Ntk_t * pNtk, Abc_ManRef_t * p )
 {
-    return 0;
+    int fCheck = 1;
+    return 1;
 }
 
 /**Function*************************************************************
@@ -475,60 +116,21 @@ int  Abc_NodeDecide( Abc_ManRes_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeUpdate( Abc_ManRes_t * p )
-{
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_ManRes_t * Abc_NtkManResStart()
+void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain )
 {
-    Abc_ManRes_t * p;
-    p = ALLOC( Abc_ManRes_t, 1 );
-    p->vFaninsNode = Vec_PtrAlloc( 100 );
-    p->vInsideNode = Vec_PtrAlloc( 100 );
-    p->vFaninsCone = Vec_PtrAlloc( 100 );
-    p->vInsideCone = Vec_PtrAlloc( 100 );
-    p->vVisited    = Vec_PtrAlloc( 100 );
-    p->vCube       = Vec_StrAlloc( 100 );
-    return p;
+    Abc_Obj_t * pNodeNew;
+    int nNodesNew, nNodesOld;
+    nNodesOld = Abc_NtkNodeNum(pNode->pNtk);
+    // create the new structure of nodes
+    assert( Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
+    pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm );
+    // remove the old nodes
+    Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew );
+    // compare the gains
+    nNodesNew = Abc_NtkNodeNum(pNode->pNtk);
+    assert( nGain <= nNodesOld - nNodesNew );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Stops the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkManResStop( Abc_ManRes_t * p )
-{
-    if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX );
-    if ( p->dd )     Extra_StopManager( p->dd );
-    Vec_PtrFree( p->vFaninsNode );
-    Vec_PtrFree( p->vInsideNode );
-    Vec_PtrFree( p->vFaninsCone );
-    Vec_PtrFree( p->vInsideCone );
-    Vec_PtrFree( p->vVisited    );
-    Vec_StrFree( p->vCube       );
-    free( p );
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcResRef.c b/src/base/abc/abcResRef.c
new file mode 100644
index 00000000..fb806ad8
--- /dev/null
+++ b/src/base/abc/abcResRef.c
@@ -0,0 +1,192 @@
+/**CFile****************************************************************
+
+  FileName    [abcResRef.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Resynthesis based on refactoring.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcResRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+struct Abc_ManRef_t_
+{
+    // user specified parameters
+    int              nNodeSizeMax;  // the limit on the size of the supernode
+    int              nConeSizeMax;  // the limit on the size of the containing cone
+    int              fVerbose;      // the verbosity flag
+    // the node currently processed
+    Abc_Obj_t *      pNode;         // the node currently considered
+    // internal parameters
+    DdManager *      dd;            // the BDD manager
+    DdNode *         bCubeX;        // the cube of PI variables
+    Vec_Str_t *      vCube;         // temporary cube for generating covers
+    Vec_Int_t *      vForm;         // the factored form (temporary)
+    // runtime statistics
+    int              time1;
+    int              time2;
+    int              time3;
+    int              time4;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes the node using refactoring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the factored form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p )
+{
+    Vec_Int_t * vForm;
+    DdManager * dd = p->dd;
+    DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc;
+    char * pSop;
+    int nFanins;
+
+    assert( p->vFaninsNode->nSize < p->nNodeSizeMax );
+    assert( p->vFaninsCone->nSize < p->nConeSizeMax );
+
+    // get the function of the node
+    bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited );  
+    Cudd_Ref( bFuncNode );
+    nFanins = p->vFaninsNode->nSize;
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // get the function of the cone
+        bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited );  
+        Cudd_Ref( bFuncCone );
+        // get the care set
+        bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX );   Cudd_Ref( bCare );
+        Cudd_RecursiveDeref( dd, bFuncCone );
+        // compute the on-set and off-set of the function of the node
+        bFuncOn   = Cudd_bddAnd( dd, bFuncNode, bCare );                Cudd_Ref( bFuncOn );
+        bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare );      Cudd_Ref( bFuncOnDc );
+        bFuncOnDc = Cudd_Not( bFuncOnDc );
+        Cudd_RecursiveDeref( dd, bCare );
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 );
+        Cudd_RecursiveDeref( dd, bFuncOn );
+        Cudd_RecursiveDeref( dd, bFuncOnDc );
+    }
+    else
+    {
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 );
+    }
+    Cudd_RecursiveDeref( dd, bFuncNode );
+    // derive the factored form
+    vForm = Ft_Factor( pSop );
+    free( pSop );
+    return vForm;
+}
+*/
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManRef_t * Abc_NtkManRefStart()
+{
+    Abc_ManRef_t * p;
+    p = ALLOC( Abc_ManRef_t, 1 );
+    memset( p, 0, sizeof(Abc_ManRef_t) );
+    p->vCube       = Vec_StrAlloc( 100 );
+    
+
+    // start the BDD manager
+    p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_zddVarsFromBddVars( p->dd, 2 );
+    p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size );   Cudd_Ref( p->bCubeX );
+
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManRefStop( Abc_ManRef_t * p )
+{
+    if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX );
+    if ( p->dd )     Extra_StopManager( p->dd );
+    Vec_StrFree( p->vCube       );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkManRefResult( Abc_ManRef_t * p )
+{
+    return p->vForm;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index ad732d2a..e9fed474 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -31,6 +31,7 @@ static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig,
 static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Abc_Obj_t * Abc_NodeStrashFactor2( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 
 static void        Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate );
 static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, bool fDuplicate );
@@ -179,7 +180,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
 
     // decide when to use factoring
     if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
-        return Abc_NodeStrashFactor( pMan, pNode, pSop );
+        return Abc_NodeStrashFactor2( pMan, pNode, pSop );
     return Abc_NodeStrashSop( pMan, pNode, pSop );
 }
 
@@ -289,6 +290,81 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS
 
 /**Function*************************************************************
 
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeStrashFactor2( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pSop )
+{
+    Vec_Int_t * vForm;
+    Vec_Ptr_t * vAnds;
+    Abc_Obj_t * pAnd, * pFanin;
+    int i;
+    // derive the factored form
+    vForm = Ft_Factor( pSop );
+    // collect the fanins
+    vAnds = Vec_PtrAlloc( 20 );
+    Abc_ObjForEachFanin( pRoot, pFanin, i )
+        Vec_PtrPush( vAnds, pFanin->pCopy );
+    // perform strashing
+    pAnd = Abc_NodeStrashDec( pMan, vAnds, vForm );
+    Vec_PtrFree( vAnds );
+    Vec_IntFree( vForm );
+    return pAnd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm )
+{
+    Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
+    Ft_Node_t * pFtNode;
+    int i, nVars;
+
+    // sanity checks
+    nVars = Ft_FactorGetNumVars( vForm );
+    assert( nVars >= 0 );
+    assert( vForm->nSize > nVars );
+    assert( nVars == vFanins->nSize );
+
+    // check for constant function
+    pFtNode = Ft_NodeRead( vForm, 0 );
+    if ( pFtNode->fConst )
+        return Abc_ObjNotCond( Abc_AigConst1(pMan), pFtNode->fCompl );
+
+    // compute the function of other nodes
+    for ( i = nVars; i < vForm->nSize; i++ )
+    {
+        pFtNode = Ft_NodeRead( vForm, i );
+        pAnd0   = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin0], pFtNode->fCompl0 ); 
+        pAnd1   = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin1], pFtNode->fCompl1 ); 
+        pAnd    = Abc_AigAnd( pMan, pAnd0, pAnd1 );
+        Vec_PtrPush( vFanins, pAnd );
+    }
+    assert( vForm->nSize = vFanins->nSize );
+
+    // complement the result if necessary
+    pFtNode = Ft_NodeReadLast( vForm );
+    pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl );
+    return pAnd;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Appends the second network to the first.]
 
   Description [Modifies the first network by adding the logic of the second. 
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 48fd2f66..d62cec11 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -447,9 +447,62 @@ void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Marks and counts the number of exors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountExors( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += pNode->fExor;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node is the root of EXOR/NEXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NodeIsExorType( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pNode0, * pNode1;
+    // check that the node is regular
+    assert( !Abc_ObjIsComplement(pNode) );
+    // if the node is not AND, this is not EXOR
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return 0;
+    // if the children are not complemented, this is not EXOR
+    if ( !Abc_ObjFaninC0(pNode) || !Abc_ObjFaninC1(pNode) )
+        return 0;
+    // get children
+    pNode0 = Abc_ObjFanin0(pNode);
+    pNode1 = Abc_ObjFanin1(pNode);
+    // if the children are not ANDs, this is not EXOR
+    if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 )
+        return 0;
+    // otherwise, the node is EXOR iff its grand-children are the same
+    return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1)) &&
+           (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1));
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
 
-  Description [The node can be complemented.]
+  Description []
                
   SideEffects []
 
@@ -920,6 +973,54 @@ void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb )
         pObj->pCopy = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
+{
+    stmm_table * tObj2NameNew;
+    Abc_Obj_t * pObj;
+    char Buffer[100];
+    char * pNameNew;
+    int Length, i;
+
+    tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "pi%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "po%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "lat%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    stmm_free_table( pNtk->tObj2Name );
+    pNtk->tObj2Name = tObj2NameNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index e72b9134..0014d48f 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -88,6 +88,9 @@ PRT( "Time", p->timeMatch );
 }
     //////////////////////////////////////////////////////////////////////
 
+    if ( !p->fAreaRecovery )
+        return 1;
+
     //////////////////////////////////////////////////////////////////////
     // perform area recovery using area flow
     clk = clock();
diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c
index a39200bb..1f3c8074 100644
--- a/src/map/mapper/mapperCut.c
+++ b/src/map/mapper/mapperCut.c
@@ -926,7 +926,7 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     Map_Cut_t * pCut;
     int Place, i;
 //    int clk;
-/*
+
     // check the cut
     Place = Map_CutTableLookup( p, ppNodes, nNodes );
     if ( Place == -1 )
@@ -934,7 +934,6 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
     assert( nNodes > 0 );
     // create the new cut
 //clk = clock();
-*/
     pCut = Map_CutAlloc( pMan );
 //pMan->time1 += clock() - clk;
     pCut->nLeaves = nNodes;
@@ -944,15 +943,12 @@ Map_Cut_t * Map_CutTableConsider( Map_Man_t * pMan, Map_CutTable_t * p, Map_Node
         pCut->ppLeaves[i] = ppNodes[i];
 //        pCut->fLevel += ppNodes[i]->Level;
     }
-/*
 //    pCut->fLevel /= nNodes;
     // add the cut to the table
     assert( p->pBins[Place] == NULL );
     p->pBins[Place] = pCut;
     // add the cut to the new list
     p->pCuts[ p->nCuts++ ] = Place;
-*/
-
     return pCut;
 }
 
diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c
index 5530f8cb..f9b280fe 100644
--- a/src/map/mapper/mapperLib.c
+++ b/src/map/mapper/mapperLib.c
@@ -140,10 +140,13 @@ void Map_SuperLibFree( Map_SuperLib_t * p )
     {
 //        if ( s_pLib == p->pGenlib )
 //            s_pLib = NULL;
-        if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib )
-            Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL);
+//        if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == p->pGenlib )
+//            Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL);
 //        Mio_LibraryDelete( p->pGenlib );
+
+        assert( p->pGenlib == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
         Mio_LibraryDelete( p->pGenlib );
+        Abc_FrameSetLibGen(Abc_FrameGetGlobalFrame(), NULL);
     }
     if ( p->tTableC )
         Map_SuperTableFree( p->tTableC );
diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c
index 67ef029b..f79dac01 100644
--- a/src/map/mapper/mapperTruth.c
+++ b/src/map/mapper/mapperTruth.c
@@ -98,6 +98,9 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
         return;
     Map_TruthsCutOne( p, pCut, uTruth );
 
+//assert( pCut->nLeaves < 5 );
+//Rwt_ManExploreCount( uTruth[0] & 0xFFFF );
+
     // compute the canonical form for the positive phase
     Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
     pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 34b0bfa2..48c4b3c3 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -31,8 +31,9 @@
 
 #include "vecFan.h"
 #include "vecInt.h"
-#include "vecPtr.h"
 #include "vecStr.h"
+#include "vecPtr.h"
+#include "vecVec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index e7584feb..ed78c8c2 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -48,16 +48,12 @@ struct Vec_Ptr_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+// iterators through entries
 #define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
     for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-
 #define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start )                                   \
     for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
 
-#define Vec_PtrForEachEntryByLevel( vVec, pEntry, i, k )                                     \
-    for ( i = 0; i < Vec_PtrSize(vVec); i++ )                                                \
-        Vec_PtrForEachEntry( ((Vec_Ptr_t *)Vec_PtrEntry(vVec, i)), pEntry, k ) 
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
new file mode 100644
index 00000000..4ee62080
--- /dev/null
+++ b/src/misc/vec/vecVec.h
@@ -0,0 +1,218 @@
+/**CFile****************************************************************
+
+  FileName    [vecVec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable vector of resizable vectors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_VEC_H__
+#define __VEC_VEC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Vec_t_       Vec_Vec_t;
+struct Vec_Vec_t_ 
+{
+    int         nSize;
+    int         nCap;
+    void **     pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+// iterators through levels 
+#define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
+    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
+    for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
+    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+
+// iteratores through entries
+#define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
+    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart )                           \
+    for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop )            \
+    for ( i = LevelStart; i <= LevelStop; i++ )                                               \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
+{
+    Vec_Vec_t * p;
+    p = ALLOC( Vec_Vec_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSize( Vec_Vec_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_VecEntry( Vec_Vec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecFree( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrFree( vVec );
+    Vec_PtrFree( (Vec_Ptr_t *)p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector of vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSizeSize( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i, Counter = 0;
+    Vec_VecForEachLevel( p, vVec, i )
+        Counter += vVec->nSize;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecClear( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrClear( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+    {
+        int i;
+        Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+        for ( i = p->nSize; i < Level + 1; i++ )
+            p->pArray[i] = Vec_PtrAlloc( 0 );
+        p->nSize = Level + 1;
+    }
+    Vec_PtrPush( p->pArray[Level], Entry );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
new file mode 100644
index 00000000..19fc34c4
--- /dev/null
+++ b/src/opt/rwr/rwr.h
@@ -0,0 +1,131 @@
+/**CFile****************************************************************
+
+  FileName    [rwr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __RWR_H__
+#define __RWR_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+#define RWR_LIMIT  1048576/4  // ((1 << 20) 
+
+typedef struct Rwr_Node_t_  Rwr_Node_t;
+struct Rwr_Node_t_ // 24 bytes
+{
+    int                Id;               // ID 
+    int                TravId;           // traversal ID
+    unsigned           uTruth : 16;      // truth table
+    unsigned           Volume :  8;      // volume
+    unsigned           Level  :  5;      // level
+    unsigned           fMark  :  1;      // mark
+    unsigned           fUsed  :  1;      // mark
+    unsigned           fExor  :  1;      // mark
+    Rwr_Node_t *       p0;               // first child
+    Rwr_Node_t *       p1;               // second child
+    Rwr_Node_t *       pNext;            // next in the table
+};
+
+typedef struct Rwr_Cut_t_  Rwr_Cut_t;
+struct Rwr_Cut_t_ // 24 bytes
+{
+    unsigned           nLeaves : 3;      // the number of leaves
+    unsigned           fTime  :  1;      // set to 1 if meets the required times
+    unsigned           fGain  :  1;      // set to 1 if does not increase nodes
+    unsigned           Volume : 11;      // the gain in the number of nodes
+    unsigned           uTruth : 16;      // the truth table
+    Abc_Obj_t *        ppLeaves[4];      // the leaves
+    Rwr_Cut_t *        pNext;            // the next cut in the list
+};
+
+struct Abc_ManRwr_t_
+{
+    // internal lookups
+    int                nFuncs;           // the number of four var functions
+    unsigned short *   puCanons;         // canonical forms
+    char *             puPhases;         // canonical phases
+    char *             pPractical;       // practical classes
+    unsigned short     puPerms[256][16]; // permutations for three var functions
+    // node space
+    Vec_Ptr_t *        vForest;          // all the nodes
+    Rwr_Node_t **      pTable;           // the hash table of nodes by their canonical form
+    Extra_MmFixed_t *  pMmNode;          // memory for nodes and cuts
+    int                nTravIds;         // the counter of traversal IDs
+    int                nConsidered;      // the number of nodes considered
+    int                nAdded;           // the number of nodes added to lists
+    int                nClasses;         // the number of NN classes
+    // intermediate data
+    Vec_Int_t *        vFanNums;         // the number of fanouts of each node (used to free cuts)
+    Vec_Int_t *        vReqTimes;        // the required times for each node (used for delay-driven evalution)
+    // the result of resynthesis
+    Vec_Int_t *        vForm;            // the decomposition tree (temporary)
+    Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
+    Vec_Ptr_t *        vTfo;             // the TFO node array (temporary)
+    Vec_Vec_t *        vLevels;          // the levelized structure (temporary)
+    int                nGainMax;
+    // runtime statistics
+    int                time1;
+    int                time2;
+    int                time3;
+    int                time4;
+};
+
+// manipulation of complemented attributes
+static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned)p) & 01);           }
+static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned)(p) & ~01);  }
+static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned)(p) ^  01);  }
+static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned)(p) ^ (c));  }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== rwrLib.c ==========================================================*/
+extern void                Rwr_ManPrecompute( Abc_ManRwr_t * p );
+extern void                Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName );
+extern void                Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName );
+extern void                Rwr_ManPrint( Abc_ManRwr_t * p );
+extern Rwr_Node_t *        Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth );
+/*=== rwrMan.c ==========================================================*/
+extern unsigned short      Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase );
+/*=== rwrUtil.c ==========================================================*/
+extern Vec_Int_t *         Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
+extern Vec_Int_t *         Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c
new file mode 100644
index 00000000..88ea3cdb
--- /dev/null
+++ b/src/opt/rwr/rwrCut.c
@@ -0,0 +1,256 @@
+/**CFile****************************************************************
+
+  FileName    [rwrCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p );
+static Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode );
+static Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns elementary cuts to the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManRwrStartCuts( Abc_ManRwr_t * p, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // set the trivial cuts
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)Rwr_CutCreateTriv( p, pNode );
+    // precompute the required times for all internal nodes
+    p->vFanNums = Rwt_NtkFanoutCounters( pNtk );
+    // save the fanout counters for all internal nodes
+    p->vReqTimes = Rwt_NtkRequiredLevels( pNtk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeRwrComputeCuts( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+    Rwr_Cut_t * pCuts0, * pCuts1, * pTemp0, * pTemp1, * pCut;
+    Rwr_Cut_t * pList = NULL, ** ppPlace = &pList; // linked list of cuts
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Abc_NodeIsConst(pNode) )
+        return;
+    // create the elementary cut
+    pCut = Rwr_CutCreateTriv( p, pNode );
+    // add it to the linked list
+    *ppPlace = pCut;  ppPlace  = &pCut->pNext;
+    // create cuts by merging pairwise
+    pCuts0 = (Rwr_Cut_t *)Abc_ObjFanin0(pNode)->pCopy;
+    pCuts1 = (Rwr_Cut_t *)Abc_ObjFanin1(pNode)->pCopy;
+    assert( pCuts0 && pCuts1 );
+    for ( pTemp0 = pCuts0; pTemp0; pTemp0 = pTemp0->pNext )
+    for ( pTemp1 = pCuts1; pTemp1; pTemp1 = pTemp1->pNext )
+    {
+        pCut = Rwr_CutsMerge( p, pTemp0, pTemp1, Abc_ObjFaninC0(pNode), Abc_ObjFaninC1(pNode) );
+        if ( pCut == NULL )
+            continue;
+        // add it to the linked list
+        *ppPlace = pCut;  ppPlace  = &pCut->pNext;
+    }
+    // set the linked list
+    pNode->pCopy = (Abc_Obj_t *)pList;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutsMerge( Abc_ManRwr_t * p, Rwr_Cut_t * pCut0, Rwr_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    Abc_Obj_t * ppNodes[4], * pNodeTemp;
+    Rwr_Cut_t * pCut;
+    unsigned uPhase, uTruth0, uTruth1;
+    int i, k, min, nTotal;
+
+    // solve the most typical case: both cuts are four input
+    if ( pCut0->nLeaves == 4 && pCut1->nLeaves == 4 )
+    {
+        for ( i = 0; i < 4; i++ )
+            if ( pCut0->ppLeaves[i] != pCut1->ppLeaves[i] )
+                return NULL;
+        // create the cut
+        pCut = Rwr_CutAlloc( p );
+        pCut->nLeaves = 4;
+        for ( i = 0; i < 4; i++ )
+            pCut->ppLeaves[i] = pCut0->ppLeaves[i];
+        pCut->uTruth = (fCompl0? ~pCut0->uTruth : pCut0->uTruth) & (fCompl1? ~pCut1->uTruth : pCut1->uTruth) & 0xFFFF;
+        return pCut;
+    }
+
+    // create the set of new nodes
+    // count the number of unique entries in pCut1
+    nTotal = pCut0->nLeaves;
+    for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+    {
+        // try to find this entry among the leaves of pCut0
+        for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+            if ( pCut1->ppLeaves[i] == pCut0->ppLeaves[k] )
+                break;
+        if ( k < (int)pCut0->nLeaves ) // found
+            continue;
+        // we found a new entry to add
+        if ( nTotal == 4 )
+            return NULL;
+        ppNodes[nTotal++] = pCut1->ppLeaves[i];
+    }
+    // we know that the feasible cut exists
+
+    // add the starting entries
+    for ( k = 0; k < (int)pCut0->nLeaves; k++ )
+        ppNodes[k] = pCut0->ppLeaves[k];
+
+    // selection-sort the entries
+    for ( i = 0; i < nTotal - 1; i++ )
+    {
+        min = i;
+        for ( k = i+1; k < nTotal; k++ )
+            if ( ppNodes[k]->Id < ppNodes[min]->Id )
+                min = k;
+        pNodeTemp    = ppNodes[i];
+        ppNodes[i]   = ppNodes[min];
+        ppNodes[min] = pNodeTemp;
+    }
+
+    // find the mapping from the old nodes to the new
+    if ( pCut0->nLeaves == 4 )
+        uTruth0 = pCut0->uTruth;
+    else
+    {
+        uPhase = 0;
+        for ( i = 0; i < (int)pCut0->nLeaves; i++ )
+        {
+            for ( k = 0; k < nTotal; k++ )
+                if ( pCut0->ppLeaves[i] == ppNodes[k] )
+                    break;
+            uPhase |= (1 << k);
+        }
+        assert( uPhase < 16 );
+        assert( pCut0->uTruth < 256 );
+        uTruth0 = p->puPerms[pCut0->uTruth][uPhase];
+    }
+
+    // find the mapping from the old nodes to the new
+    if ( pCut1->nLeaves == 4 )
+        uTruth1 = pCut1->uTruth;
+    else
+    {
+        uPhase = 0;
+        for ( i = 0; i < (int)pCut1->nLeaves; i++ )
+        {
+            for ( k = 0; k < nTotal; k++ )
+                if ( pCut1->ppLeaves[i] == ppNodes[k] )
+                    break;
+            uPhase |= (1 << k);
+        }
+        assert( uPhase < 16 );
+        assert( pCut1->uTruth < 256 );
+        uTruth1 = p->puPerms[pCut1->uTruth][uPhase];
+    }
+
+    // create the cut
+    pCut = Rwr_CutAlloc( p );
+    pCut->nLeaves = nTotal;
+    for ( i = 0; i < nTotal; i++ )
+        pCut->ppLeaves[i] = ppNodes[i];
+    pCut->uTruth = (fCompl0? ~uTruth0 : uTruth0) & (fCompl1? ~uTruth1 : uTruth1) & 0xFFFF;
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutAlloc( Abc_ManRwr_t * p )
+{
+    Rwr_Cut_t * pCut;
+    pCut = (Rwr_Cut_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+    memset( pCut, 0, sizeof(Rwr_Cut_t) );
+    return pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Start the cut computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Cut_t * Rwr_CutCreateTriv( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+    Rwr_Cut_t * pCut;
+    pCut = Rwr_CutAlloc( p );
+    pCut->nLeaves = 1;
+    pCut->ppLeaves[0] = pNode;
+    pCut->uTruth = 0xAAAA;
+    return pCut;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
new file mode 100644
index 00000000..ecf03f4f
--- /dev/null
+++ b/src/opt/rwr/rwrEva.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+  FileName    [rwrDec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Evaluation and decomposition procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrDec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut );
+static void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs rewriting for one node.]
+
+  Description [This procedure considers all the cuts computed for the node
+  and tries to rewrite each of them using the "forest" of different AIG
+  structures precomputed and stored in the RWR manager. 
+  Determines the best rewriting and computes the gain in the number of AIG
+  nodes in the final network. In the end, p->vFanins contains information 
+  about the best cut that can be used for rewriting, while p->vForm gives 
+  the decomposition tree (represented using factored form data structure).
+  Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRwrRewrite( Abc_ManRwr_t * p, Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t Vector = {0,0,0}, * vFanins = &Vector;
+    Rwr_Cut_t * pCut, * pCutBest;
+    int BestGain = -1;
+    int i, Required = Vec_IntEntry( p->vReqTimes, pNode->Id );
+
+    // go through the cuts
+    for ( pCut = (Rwr_Cut_t *)pNode->pCopy, pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+    {
+        // collect the TFO
+        vFanins->nSize  = pCut->nLeaves;
+        vFanins->pArray = pCut->ppLeaves;
+        Abc_NodeCollectTfoCands( pNode->pNtk, pNode, vFanins, Required, p->vLevels, p->vTfo );
+        // evaluate the cut
+        Rwr_CutEvaluate( p, pCut );
+        // check if the cut is the best
+        if ( pCut->fTime && pCut->fGain )
+        {
+            pCutBest = pCut;
+            BestGain = pCut->Volume;
+        }
+    }
+    if ( BestGain == -1 )
+        return -1;
+    // we found a good cut
+
+    // prepare the fanins
+    Vec_PtrClear( p->vFanins );
+    for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+        Vec_PtrPush( p->vFanins, pCutBest->ppLeaves[i] );
+    // collect the TFO again
+    Abc_NodeCollectTfoCands( pNode->pNtk, pNode, p->vFanins, Required, p->vLevels, p->vTfo );
+    // perform the decomposition
+    Rwr_CutDecompose( p, pCutBest, p->vForm );
+    // the best fanins are in p->vFanins, the result of decomposition is in p->vForm
+    return BestGain;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_CutEvaluate( Abc_ManRwr_t * p, Rwr_Cut_t * pCut )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_CutDecompose( Abc_ManRwr_t * p, Rwr_Cut_t * pCut, Vec_Int_t * vForm )
+{
+}
+
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
new file mode 100644
index 00000000..37eabf5b
--- /dev/null
+++ b/src/opt/rwr/rwrExp.c
@@ -0,0 +1,179 @@
+/**CFile****************************************************************
+
+  FileName    [rwrExp.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Computation of practically used NN-classes of 4-input cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrExp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_ManRwrExp_t_ Abc_ManRwrExp_t;
+struct Abc_ManRwrExp_t_
+{
+    // internal lookups
+    int                nFuncs;           // the number of four-var functions
+    unsigned short *   puCanons;         // canonical forms
+    int *              pnCounts;         // the counters of functions in each class
+    int                nConsidered;      // the number of nodes considered
+    int                nClasses;         // the number of NN classes
+};
+
+static Abc_ManRwrExp_t * s_pManRwrExp = NULL;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_ManExploreStart()
+{
+    Abc_ManRwrExp_t * p;
+    unsigned uTruth;
+    int i, k, nClasses;
+    int clk = clock();
+
+    p = ALLOC( Abc_ManRwrExp_t, 1 );
+    memset( p, 0, sizeof(Abc_ManRwrExp_t) );
+    // canonical forms
+    p->nFuncs    = (1<<16);
+    p->puCanons  = ALLOC( unsigned short, p->nFuncs );
+    memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
+    // counters
+    p->pnCounts  = ALLOC( int, p->nFuncs );
+    memset( p->pnCounts, 0, sizeof(int) * p->nFuncs );
+
+    // initialize the canonical forms
+    nClasses = 1;
+    for ( i = 1; i < p->nFuncs-1; i++ )
+    {
+        if ( p->puCanons[i] )
+            continue;
+        nClasses++;
+        for ( k = 0; k < 32; k++ )
+        {
+            uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
+            if ( p->puCanons[uTruth] == 0 )
+                p->puCanons[uTruth] = (unsigned short)i;
+            else
+                assert( p->puCanons[uTruth] == (unsigned short)i );
+        }
+    }
+    // set info for constant 1
+    p->puCanons[p->nFuncs-1] = 0;
+    printf( "The number of NN-canonical forms = %d.\n", nClasses );
+    s_pManRwrExp = p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_ManExploreCount( unsigned uTruth )
+{
+    assert( uTruth < (1<<16) );
+    s_pManRwrExp->pnCounts[ s_pManRwrExp->puCanons[uTruth] ]++;    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects stats about 4-var functions appearing in netlists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwt_ManExplorePrint()
+{
+    FILE * pFile;
+    int i, CountMax, CountWrite, nCuts, nClasses;
+    int * pDistrib;
+    int * pReprs;
+    // find the max number of occurences
+    nCuts = nClasses = 0;
+    CountMax = 0;
+    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+    {
+        if ( CountMax < s_pManRwrExp->pnCounts[i] )
+            CountMax = s_pManRwrExp->pnCounts[i];
+        nCuts += s_pManRwrExp->pnCounts[i];
+        if ( s_pManRwrExp->pnCounts[i] > 0 )
+            nClasses++;
+    }
+    printf( "Number of cuts considered       = %8d.\n", nCuts );
+    printf( "Classes occurring at least once = %8d.\n", nClasses );
+    // print the distribution of classes
+    pDistrib = ALLOC( int, CountMax + 1 );
+    pReprs   = ALLOC( int, CountMax + 1 );
+    memset( pDistrib, 0, sizeof(int)*(CountMax + 1) );
+    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+    {
+        pDistrib[ s_pManRwrExp->pnCounts[i] ]++;
+        pReprs[ s_pManRwrExp->pnCounts[i] ] = i;
+    }
+
+    printf( "Occurence = %6d.  Num classes = %4d.  \n", 0, 2288-nClasses );
+    for ( i = 1; i <= CountMax; i++ )
+        if ( pDistrib[i] )
+        {
+            printf( "Occurence = %6d.  Num classes = %4d.  Repr = ", i, pDistrib[i] );
+            Extra_PrintBinary( stdout, (unsigned*)&(pReprs[i]), 16 ); 
+            printf( "\n" );
+        }
+    free( pDistrib );
+    free( pReprs );
+    // write into a file all classes above limit (5)
+    CountWrite = 0;
+    pFile = fopen( "nnclass_stats.txt", "w" );
+    for ( i = 0; i < s_pManRwrExp->nFuncs; i++ )
+        if ( s_pManRwrExp->pnCounts[i] > 5 )
+        {
+            fprintf( pFile, "%d ", i );
+            CountWrite++;
+        }
+    fclose( pFile );
+    printf( "%d classes written into file \"%s\".\n", CountWrite, "nnclass_stats.txt" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
new file mode 100644
index 00000000..91604244
--- /dev/null
+++ b/src/opt/rwr/rwrLib.c
@@ -0,0 +1,670 @@
+/**CFile****************************************************************
+
+  FileName    [rwrLib.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Rwr_Node_t *        Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static Rwr_Node_t *        Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static int                 Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 );
+
+static void                Rwr_ManIncTravId_int( Abc_ManRwr_t * p );
+static inline void         Rwr_ManIncTravId( Abc_ManRwr_t * p )     { if ( p->nTravIds++ == 0x8FFFFFFF ) Rwr_ManIncTravId_int( p ); }
+
+static void                Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Precomputes the forest in the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPrecompute( Abc_ManRwr_t * p )
+{
+    Rwr_Node_t * p0, * p1;
+    int i, k, Level, Volume;
+    int LevelOld = -1;
+    int nNodes;
+
+    Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
+    Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
+    {
+        if ( LevelOld < (int)p0->Level )
+        {
+            LevelOld = p0->Level;
+            printf( "Starting level %d  (at %d nodes).\n", LevelOld+1, i );
+            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
+                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+        }
+
+        if ( k == i )
+            break;
+//        if ( p0->Level + p1->Level > 6 ) // hard
+//            break;
+
+        if ( p0->Level + p1->Level > 5 ) // easy 
+            break;
+
+//        if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
+//            break;
+
+        // compute the level and volume of the new nodes
+        Level  = 1 + ABC_MAX( p0->Level, p1->Level );
+        Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
+        // try four different nodes
+        Rwr_ManTryNode( p,         p0 ,         p1 , 0, Level, Volume );
+        Rwr_ManTryNode( p, Rwr_Not(p0),         p1 , 0, Level, Volume );
+        Rwr_ManTryNode( p,         p0 , Rwr_Not(p1), 0, Level, Volume );
+        Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
+        // try EXOR
+        Rwr_ManTryNode( p,         p0 ,         p1 , 1, Level, Volume + 1 );
+        // report the progress
+        if ( p->nConsidered % 50000000 == 0 )
+            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
+                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+        // quit after some time
+        if ( p->vForest->nSize == RWR_LIMIT + 5 )
+        {
+            printf( "Considered = %5d M.   Found = %8d.   Classes = %6d.   Trying %7d.\n", 
+                p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+            goto save;
+        }
+    }
+save :
+
+    // mark the relevant ones
+    Rwr_ManIncTravId( p );
+    k = 5;
+    nNodes = 0;
+    Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+        if ( p0->uTruth == p->puCanons[p0->uTruth] )
+        {
+            Rwr_MarkUsed_rec( p, p0 );
+            nNodes++;
+        }
+
+    // compact the array by throwing away non-canonical
+    k = 5;
+    Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+        if ( p0->fUsed )
+        {
+            p->vForest->pArray[k] = p0;
+            p0->Id = k;
+            k++;
+        }
+    p->vForest->nSize = k;
+    printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes to file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManWriteToFile( Abc_ManRwr_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Rwr_Node_t * pNode;
+    unsigned * pBuffer;
+    int i, nEntries, clk = clock();
+    // prepare the buffer
+    nEntries = p->vForest->nSize - 5;
+    pBuffer = ALLOC( unsigned, nEntries * 2 );
+    for ( i = 0; i < nEntries; i++ )
+    {
+        pNode = p->vForest->pArray[i+5];
+        pBuffer[2*i + 0] = (Rwr_Regular(pNode->p0)->Id << 1) | Rwr_IsComplement(pNode->p0);
+        pBuffer[2*i + 1] = (Rwr_Regular(pNode->p1)->Id << 1) | Rwr_IsComplement(pNode->p1);
+        // save EXOR flag
+        pBuffer[2*i + 0] = (pBuffer[2*i + 0] << 1) | pNode->fExor;
+
+    }
+    pFile = fopen( pFileName, "wb" );
+    fwrite( &nEntries, sizeof(int), 1, pFile );
+    fwrite( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
+    free( pBuffer );
+    fclose( pFile );
+    printf( "The number of nodes saved = %d.   ", nEntries );  PRT( "Saving", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads data from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManLoadFromFile( Abc_ManRwr_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Rwr_Node_t * p0, * p1;
+    unsigned * pBuffer;
+    int Level, Volume, nEntries, fExor;
+    int i, clk = clock();
+
+    // load the data
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Rwr_ManLoadFromFile: Cannot open file \"%s\".\n", pFileName );
+        return;
+    }
+    fread( &nEntries, sizeof(int), 1, pFile );
+    pBuffer = ALLOC( unsigned, nEntries * 2 );
+    fread( pBuffer, sizeof(unsigned), nEntries * 2, pFile );
+    fclose( pFile );
+    // reconstruct the forest
+    for ( i = 0; i < nEntries; i++ )
+    {
+        // get EXOR flag
+        fExor = (pBuffer[2*i + 0] & 1);
+        pBuffer[2*i + 0] = (pBuffer[2*i + 0] >> 1);
+        // get the nodes
+        p0 = p->vForest->pArray[pBuffer[2*i + 0] >> 1];
+        p1 = p->vForest->pArray[pBuffer[2*i + 1] >> 1];
+        // compute the level and volume of the new nodes
+        Level  = 1 + ABC_MAX( p0->Level, p1->Level );
+        Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
+        // set the complemented attributes
+        p0 = Rwr_NotCond( p0, (pBuffer[2*i + 0] & 1) );
+        p1 = Rwr_NotCond( p1, (pBuffer[2*i + 1] & 1) );
+        // add the node
+//        Rwr_ManTryNode( p, p0, p1, Level, Volume );
+        Rwr_ManAddNode( p, p0, p1, fExor, Level, Volume + fExor );
+    }
+    free( pBuffer );
+    printf( "The number of classes = %d. Canonical nodes = %d.\n", p->nClasses, p->nAdded );
+    printf( "The number of nodes loaded = %d.   ", nEntries );  PRT( "Loading", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManIncTravId_int( Abc_ManRwr_t * p )
+{
+    Rwr_Node_t * pNode;
+    int i;
+    Vec_PtrForEachEntry( p->vForest, pNode, i )
+        pNode->TravId = 0;
+    p->nTravIds = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_MarkUsed_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+{
+    if ( pNode->fUsed || pNode->TravId == p->nTravIds )
+        return;
+    pNode->TravId = p->nTravIds;
+    pNode->fUsed = 1;
+    Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
+    Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_Trav_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+{
+    if ( pNode->fMark || pNode->TravId == p->nTravIds )
+        return;
+    pNode->TravId = p->nTravIds;
+    (*pVolume)++;
+    if ( pNode->fExor )
+        (*pVolume)++;
+    Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
+    Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_Trav2_rec( Abc_ManRwr_t * p, Rwr_Node_t * pNode, int * pVolume )
+{
+    if ( pNode->fMark || pNode->TravId == p->nTravIds )
+        return;
+    pNode->TravId = p->nTravIds;
+    (*pVolume)++;
+    Rwr_Trav2_rec( p, Rwr_Regular(pNode->p0), pVolume );
+    Rwr_Trav2_rec( p, Rwr_Regular(pNode->p1), pVolume );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwr_ManNodeVolume( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
+{
+    int Volume = 0;
+    Rwr_ManIncTravId( p );
+    Rwr_Trav_rec( p, p0, &Volume );
+    Rwr_Trav_rec( p, p1, &Volume );
+    return Volume;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManTryNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+    Rwr_Node_t * pOld, * pNew, ** ppPlace;
+    unsigned uTruth, uCanon;
+    // compute truth table, level, volume
+    p->nConsidered++;
+    if ( fExor )
+    {
+//        printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
+        uTruth = (p0->uTruth ^ p1->uTruth);
+    }
+    else
+        uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
+                 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+    uCanon = p->puCanons[uTruth];
+    // skip non-practical classes
+    if ( Level > 2 && p->pPractical[uCanon] == 0 )
+        return NULL;
+    // enumerate through the nodes with the same canonical form
+    ppPlace = p->pTable + uCanon;
+    for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
+    {
+        if ( pOld->Level <  (unsigned)Level && pOld->Volume < (unsigned)Volume )
+            return NULL;
+        if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
+            return NULL;
+//        if ( pOld->Level <  (unsigned)Level && pOld->Volume == (unsigned)Volume )
+//            return NULL;
+    }
+//    if ( fExor )
+//        printf( "Adding EXOR of %d and %d.\n", p0->Id, p1->Id );
+    // create the new node
+    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+    pNew->Id     = p->vForest->nSize;
+    pNew->TravId = 0;
+    pNew->uTruth = uTruth;
+    pNew->Level  = Level;
+    pNew->Volume = Volume;
+    pNew->fMark  = 0;
+    pNew->fUsed  = 0;
+    pNew->fExor  = fExor;
+    pNew->p0     = p0;
+    pNew->p1     = p1;
+    pNew->pNext  = NULL;
+    Vec_PtrPush( p->vForest, pNew );
+    *ppPlace     = pNew;
+    if ( p->pTable[uCanon] == pNew )
+        p->nClasses++;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddNode( Abc_ManRwr_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+    Rwr_Node_t * pOld, * pNew;
+    unsigned uTruth, uCanon;
+    // compute truth table, leve, volume
+    p->nConsidered++;
+    if ( fExor )
+        uTruth = (p0->uTruth ^ p1->uTruth);
+    else
+        uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 
+                 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+    uCanon = p->puCanons[uTruth];
+    // skip non-practical classes
+//    if ( p->pPractical[uCanon] == 0 )
+//        return NULL;
+    // create the new node
+    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+    pNew->Id     = p->vForest->nSize;
+    pNew->TravId = 0;
+    pNew->uTruth = uTruth;
+    pNew->Level  = Level;
+    pNew->Volume = Volume;
+    pNew->fMark  = 0;
+    pNew->fUsed  = 0;
+    pNew->fExor  = fExor;
+    pNew->p0     = p0;
+    pNew->p1     = p1;
+    pNew->pNext  = NULL;
+    Vec_PtrPush( p->vForest, pNew );
+    // do not add if the node is not essential
+    if ( uTruth != uCanon )
+        return pNew;
+
+    // add to the list
+    p->nAdded++;
+    pOld = p->pTable[uCanon];
+    if ( pOld == NULL )
+        p->nClasses++;
+    pNew->pNext = pOld;
+    p->pTable[uCanon] = pNew;
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddVar( Abc_ManRwr_t * p, unsigned uTruth )
+{
+    Rwr_Node_t * pNew;
+    pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+    pNew->Id     = p->vForest->nSize;
+    pNew->TravId = 0;
+    pNew->uTruth = uTruth;
+    pNew->Level  = 0;
+    pNew->Volume = 0;
+    pNew->fMark  = 1;
+    pNew->fUsed  = 1;
+    pNew->fExor  = 0;
+    pNew->p0     = NULL;
+    pNew->p1     = NULL;    pNew->pNext  = NULL;
+    Vec_PtrPush( p->vForest, pNew );
+    assert( p->pTable[p->puCanons[uTruth]] == NULL );
+    p->pTable[p->puCanons[uTruth]] = pNew;
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one rwr node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_NodePrint_rec( FILE * pFile, Rwr_Node_t * pNode )
+{
+    assert( !Rwr_IsComplement(pNode) );
+
+    if ( pNode->Id == 0 )
+    {
+        fprintf( pFile, "Const1" );
+        return;
+    }
+
+    if ( pNode->Id < 5 )
+    {
+        fprintf( pFile, "%c", 'a' + pNode->Id - 1 );
+        return;
+    }
+
+    if ( Rwr_IsComplement(pNode->p0) )
+    {
+        if ( Rwr_Regular(pNode->p0)->Id < 5 )
+        {
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+            fprintf( pFile, "\'" );
+        }
+        else
+        {
+            fprintf( pFile, "(" );
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+            fprintf( pFile, ")\'" );
+        }
+    }
+    else
+    {
+        if ( Rwr_Regular(pNode->p0)->Id < 5 )
+        {
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+        }
+        else
+        {
+            fprintf( pFile, "(" );
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p0) );
+            fprintf( pFile, ")" );
+        }
+    }
+
+    if ( pNode->fExor )
+        fprintf( pFile, "+" );
+
+    if ( Rwr_IsComplement(pNode->p1) )
+    {
+        if ( Rwr_Regular(pNode->p1)->Id < 5 )
+        {
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+            fprintf( pFile, "\'" );
+        }
+        else
+        {
+            fprintf( pFile, "(" );
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+            fprintf( pFile, ")\'" );
+        }
+    }
+    else
+    {
+        if ( Rwr_Regular(pNode->p1)->Id < 5 )
+        {
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+        }
+        else
+        {
+            fprintf( pFile, "(" );
+            Rwr_NodePrint_rec( pFile, Rwr_Regular(pNode->p1) );
+            fprintf( pFile, ")" );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one rwr node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_NodePrint( FILE * pFile, Abc_ManRwr_t * p, Rwr_Node_t * pNode )
+{
+    unsigned uTruth;
+    fprintf( pFile, "%5d :", pNode->Id );
+    fprintf( pFile, " tt=", pNode->Id );
+    uTruth = pNode->uTruth;
+    Extra_PrintBinary( pFile, &uTruth, 16 );
+    fprintf( pFile, " cn=", pNode->Id );
+    uTruth = p->puCanons[pNode->uTruth];
+    Extra_PrintBinary( pFile, &uTruth, 16 );
+    fprintf( pFile, " lev=%d", pNode->Level );
+    fprintf( pFile, " vol=%d", pNode->Volume );
+    fprintf( pFile, "  " );
+    Rwr_NodePrint_rec( pFile, pNode );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one rwr node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rwr_ManPrint( Abc_ManRwr_t * p )
+{
+/*
+    Rwr_Node_t * pNode;
+    unsigned uTruth;
+    int Limit = 4;
+    int i;
+
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        if ( p->pTable[i] == NULL )
+            continue;
+        if ( Limit-- == 0 )
+            break;
+        printf( "\nClass " );
+        uTruth = i;
+        Extra_PrintBinary( stdout, &uTruth, 16 );
+        printf( "\n" );
+        for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+            if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+                Rwr_NodePrint( p, pNode );
+    }
+*/
+    FILE * pFile;
+    Rwr_Node_t * pNode;
+    unsigned uTruth;
+    int Limit = 4;
+    int Counter;
+    int i;
+
+    pFile = fopen( "graph_lib.txt", "w" );
+
+    Counter = 0;
+    for ( i = 0; i < p->nFuncs; i++ )
+    {
+        if ( p->pTable[i] == NULL )
+            continue;
+//        if ( Limit-- == 0 )
+//            break;
+        fprintf( pFile, "\nClass %3d  ", Counter++ );
+
+        // count the volume of the bush
+        {
+            int Volume = 0;
+            int nFuncs = 0;
+            Rwr_ManIncTravId( p );
+            for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+                if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+                {
+                    nFuncs++;
+                    Rwr_Trav2_rec( p, pNode, &Volume );
+                }
+            fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume );
+        }
+
+        uTruth = i;
+        Extra_PrintBinary( pFile, &uTruth, 16 );
+        fprintf( pFile, "\n" );
+
+        for ( pNode = p->pTable[i]; pNode; pNode = pNode->pNext )
+            if ( pNode->uTruth == p->puCanons[pNode->uTruth] )
+                Rwr_NodePrint( pFile, p, pNode );
+    }
+
+    fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
new file mode 100644
index 00000000..46752696
--- /dev/null
+++ b/src/opt/rwr/rwrMan.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+  FileName    [rwrMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the following information was derived by computing all 4-input cuts of IWLS, MCNC, and ISCAS benchmarks
+#define RWR_NUM_CLASSES  775
+static int s_PracticalClasses[RWR_NUM_CLASSES] = {
+    0, 1, 3, 5, 6, 7, 15, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 51, 53, 54, 55, 60, 61, 63, 85, 86, 
+    87, 90, 91, 95, 102, 103, 105, 107, 111, 119, 123, 125, 126, 127, 255, 257, 258, 259, 260, 261, 262, 263, 264, 265, 
+    266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 281, 282, 284, 286, 287, 288, 289, 290, 291, 293, 297, 
+    298, 299, 300, 302, 303, 304, 305, 306, 307, 308, 310, 311, 312, 313, 315, 316, 317, 319, 320, 321, 323, 324, 325, 329, 
+    332, 334, 335, 336, 337, 338, 340, 341, 342, 343, 345, 347, 349, 351, 352, 357, 358, 359, 361, 367, 368, 369, 371, 
+    373, 375, 379, 381, 383, 384, 385, 386, 388, 389, 392, 393, 395, 397, 399, 400, 404, 408, 409, 416, 417, 419, 420, 
+    421, 424, 425, 426, 427, 431, 433, 443, 448, 449, 451, 453, 456, 457, 459, 460, 461, 462, 463, 465, 476, 477, 480, 
+    481, 483, 489, 492, 493, 494, 495, 496, 497, 499, 500, 501, 506, 507, 508, 509, 510, 771, 773, 774, 775, 780, 781, 
+    783, 785, 786, 787, 788, 790, 791, 792, 796, 797, 799, 816, 817, 819, 820, 821, 834, 835, 836, 837, 838, 839, 840, 
+    844, 847, 848, 849, 850, 851, 852, 853, 854, 855, 856, 859, 860, 861, 863, 864, 867, 870, 871, 876, 878, 880, 883, 
+    884, 885, 887, 967, 973, 975, 979, 984, 988, 989, 990, 1009, 1011, 1012, 1013, 1020, 1285, 1286, 1287, 1290, 1291, 
+    1295, 1297, 1298, 1300, 1301, 1303, 1307, 1308, 1309, 1311, 1314, 1316, 1317, 1318, 1319, 1322, 1325, 1327, 1329, 
+    1330, 1331, 1332, 1333, 1334, 1335, 1336, 1338, 1340, 1341, 1360, 1361, 1363, 1365, 1367, 1380, 1381, 1382, 1383, 
+    1390, 1392, 1395, 1397, 1399, 1440, 1445, 1447, 1450, 1451, 1455, 1458, 1461, 1463, 1467, 1525, 1530, 1542, 1543, 
+    1545, 1547, 1551, 1553, 1554, 1558, 1559, 1561, 1567, 1569, 1570, 1572, 1574, 1576, 1587, 1588, 1590, 1591, 1596, 
+    1618, 1620, 1621, 1623, 1624, 1632, 1638, 1641, 1647, 1654, 1655, 1680, 1686, 1687, 1689, 1695, 1718, 1776, 1782, 
+    1785, 1799, 1803, 1805, 1806, 1807, 1811, 1813, 1815, 1823, 1826, 1831, 1843, 1844, 1847, 1859, 1860, 1863, 1875, 
+    1877, 1879, 1895, 1902, 1904, 1911, 1912, 1927, 1928, 1933, 1935, 1945, 1956, 1957, 1959, 1962, 1964, 1965, 1975, 
+    1979, 1987, 1991, 1995, 1996, 2000, 2002, 2007, 2013, 2023, 2032, 2040, 3855, 3857, 3859, 3861, 3864, 3866, 3867, 
+    3868, 3869, 3870, 3891, 3892, 3893, 3900, 3921, 3925, 3942, 3945, 3956, 3960, 4080, 4369, 4370, 4371, 4372, 4373, 
+    4374, 4375, 4376, 4377, 4378, 4379, 4380, 4381, 4382, 4386, 4387, 4388, 4389, 4391, 4392, 4394, 4396, 4403, 4405, 
+    4408, 4409, 4411, 4420, 4421, 4422, 4423, 4424, 4426, 4428, 4437, 4439, 4445, 4488, 4494, 4505, 4507, 4509, 4522, 
+    4524, 4525, 4526, 4539, 4540, 4542, 4556, 4557, 4573, 4574, 4590, 4626, 4627, 4629, 4630, 4631, 4632, 4634, 4638, 
+    4641, 4643, 4648, 4659, 4680, 4695, 4698, 4702, 4713, 4731, 4740, 4758, 4766, 4773, 4791, 4812, 4830, 4845, 4883, 
+    4885, 4887, 4888, 4891, 4892, 4899, 4903, 4913, 4914, 4915, 4934, 4940, 4945, 4947, 4949, 4951, 4972, 5005, 5011, 
+    5017, 5019, 5029, 5043, 5049, 5058, 5059, 5060, 5068, 5075, 5079, 5083, 5084, 5100, 5140, 5141, 5142, 5143, 5148, 
+    5160, 5171, 5174, 5180, 5182, 5185, 5186, 5187, 5189, 5205, 5207, 5214, 5238, 5245, 5246, 5250, 5270, 5278, 5290, 
+    5310, 5315, 5335, 5355, 5397, 5399, 5401, 5402, 5405, 5413, 5414, 5415, 5418, 5427, 5429, 5445, 5457, 5460, 5461, 
+    5463, 5469, 5482, 5522, 5525, 5533, 5540, 5546, 5557, 5565, 5571, 5580, 5589, 5593, 5605, 5610, 5654, 5673, 5692, 
+    5698, 5729, 5734, 5782, 5790, 5796, 5814, 5826, 5846, 5911, 5931, 5965, 6001, 6066, 6120, 6168, 6174, 6180, 6206, 
+    6210, 6229, 6234, 6270, 6273, 6279, 6363, 6375, 6425, 6427, 6438, 6446, 6451, 6457, 6478, 6482, 6485, 6489, 6502, 
+    6545, 6553, 6564, 6570, 6594, 6617, 6630, 6682, 6683, 6685, 6686, 6693, 6709, 6741, 6746, 6817, 6821, 6826, 6833, 
+    6849, 6885, 6939, 6940, 6951, 6963, 6969, 6990, 6997, 7065, 7077, 7089, 7140, 7196, 7212, 7219, 7220, 7228, 7230, 
+    7251, 7324, 7356, 7361, 7363, 7372, 7377, 7395, 7453, 7470, 7475, 7495, 7509, 7513, 7526, 7619, 7633, 7650, 7710, 
+    7725, 7731, 7740, 7755, 7770, 7800, 7815, 7830, 7845, 7860, 7890, 7905, 13107, 13109, 13110, 13116, 13141, 13146, 
+    13161, 13164, 13621, 13622, 13626, 13651, 13653, 13658, 13669, 13670, 13763, 13765, 13770, 13878, 13881, 13884, 
+    13910, 13923, 13926, 13932, 13971, 13974, 13980, 14022, 14025, 15420, 15445, 15450, 15462, 15465, 15555, 21845, 
+    21846, 21850, 21865, 21866, 21930, 22102, 22105, 22106, 22117, 22118, 22122, 22165, 22166, 22169, 22170, 22181, 
+    22182, 22185, 23130, 23142, 23145, 23205, 26214, 26217, 26985, 27030 
+};
+
+static unsigned short      Rwr_FunctionPerm( unsigned uTruth, int Phase );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManRwr_t * Abc_NtkManRwrStart( char * pFileName )
+{
+    Abc_ManRwr_t * p;
+    unsigned uTruth;
+    int i, k, nClasses;
+    int clk = clock();
+
+    p = ALLOC( Abc_ManRwr_t, 1 );
+    memset( p, 0, sizeof(Abc_ManRwr_t) );
+    // canonical forms
+    p->nFuncs    = (1<<16);
+    p->puCanons  = ALLOC( unsigned short, p->nFuncs );
+    memset( p->puCanons, 0, sizeof(unsigned short) * p->nFuncs );
+    // permutations
+    p->puPhases  = ALLOC( char, p->nFuncs );
+    memset( p->puPhases, 0, sizeof(char) * p->nFuncs );
+    // hash table
+    p->pTable  = ALLOC( Rwr_Node_t *, p->nFuncs );
+    memset( p->pTable, 0, sizeof(Rwr_Node_t *) * p->nFuncs );
+    // practical classes
+    p->pPractical  = ALLOC( char, p->nFuncs );
+    memset( p->pPractical, 0, sizeof(char) * p->nFuncs );
+    // other stuff
+    p->vForest  = Vec_PtrAlloc( 100 );
+    p->vForm    = Vec_IntAlloc( 50 );
+    p->vFanins  = Vec_PtrAlloc( 50 );
+    p->vTfo     = Vec_PtrAlloc( 50 );
+    p->vLevels  = Vec_VecAlloc( 50 );
+    p->pMmNode  = Extra_MmFixedStart( sizeof(Rwr_Node_t) );
+    p->nTravIds = 1;
+    assert( sizeof(Rwr_Node_t) == sizeof(Rwr_Cut_t) );
+
+    // initialize the canonical forms
+    nClasses = 1;
+    for ( i = 1; i < p->nFuncs-1; i++ )
+    {
+        if ( p->puCanons[i] )
+            continue;
+        nClasses++;
+        for ( k = 0; k < 32; k++ )
+        {
+            uTruth = Rwr_FunctionPhase( (unsigned)i, (unsigned)k );
+            if ( p->puCanons[uTruth] == 0 )
+            {
+                p->puCanons[uTruth] = (unsigned short)i;
+                p->puPhases[uTruth] = (char)k;
+            }
+            else
+                assert( p->puCanons[uTruth] == (unsigned short)i );
+        }
+    }
+    // set info for constant 1
+    p->puCanons[p->nFuncs-1] = 0;
+    p->puPhases[p->nFuncs-1] = 16;
+    printf( "The number of NN-canonical forms = %d.\n", nClasses );
+
+    // initialize permutations
+    for ( i = 0; i < 256; i++ )
+        for ( k = 0; k < 16; k++ )
+            p->puPerms[i][k] = Rwr_FunctionPerm( i, k );
+
+    // initialize practical classes
+    for ( i = 0; i < RWR_NUM_CLASSES; i++ )
+        p->pPractical[ s_PracticalClasses[i] ] = 1;
+
+    // initialize forest
+    Rwr_ManAddVar( p, 0xFFFF ); // constant 1
+    Rwr_ManAddVar( p, 0xAAAA ); // var A
+    Rwr_ManAddVar( p, 0xCCCC ); // var B
+    Rwr_ManAddVar( p, 0xF0F0 ); // var C
+    Rwr_ManAddVar( p, 0xFF00 ); // var D
+    p->nClasses = 5;
+PRT( "Manager startup time", clock() - clk ); 
+
+    // create the nodes
+    if ( pFileName == NULL )
+    {   // precompute
+        Rwr_ManPrecompute( p );
+        Rwr_ManWriteToFile( p, "data.aaa" );
+    }
+    else
+    {   // load previously saved nodes
+        Rwr_ManLoadFromFile( p, pFileName );
+    }
+    Rwr_ManPrint( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManRwrStop( Abc_ManRwr_t * p )
+{
+    if ( p->vFanNums )  Vec_IntFree( p->vFanNums );
+    if ( p->vReqTimes ) Vec_IntFree( p->vReqTimes );
+    Vec_IntFree( p->vForm );
+    Vec_PtrFree( p->vFanins );
+    Vec_PtrFree( p->vTfo );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vForest );
+    Extra_MmFixedStop( p->pMmNode,   0 );
+    free( p->pPractical );
+    free( p->puCanons );
+    free( p->puPhases );
+    free( p->pTable );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkManRwrDecs( Abc_ManRwr_t * p )
+{
+    return p->vForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManRwrFanins( Abc_ManRwr_t * p )
+{
+    return p->vFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a phase of the 4-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned short Rwr_FunctionPhase( unsigned uTruth, unsigned uPhase )
+{
+    static unsigned uMasks0[4] = { 0x5555, 0x3333, 0x0F0F, 0x00FF };
+    static unsigned uMasks1[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
+    int v, Shift;
+    for ( v = 0, Shift = 1; v < 4; v++, Shift <<= 1 )
+        if ( uPhase & Shift )
+            uTruth = (((uTruth & uMasks0[v]) << Shift) | ((uTruth & uMasks1[v]) >> Shift));
+    if ( uPhase & 16 )
+        uTruth = ~uTruth & 0xFFFF;
+    return uTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes a phase of the 3-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned short Rwr_FunctionPerm( unsigned uTruth, int Phase )
+{
+    static int Perm[16][4] = {
+        { 0, 1, 2, 3 }, // 0000  - skip
+        { 0, 1, 2, 3 }, // 0001  - skip
+        { 1, 0, 2, 3 }, // 0010
+        { 0, 1, 2, 3 }, // 0011  - skip
+        { 2, 1, 0, 3 }, // 0100
+        { 0, 2, 1, 3 }, // 0101
+        { 2, 0, 1, 3 }, // 0110
+        { 0, 1, 2, 3 }, // 0111  - skip
+        { 3, 1, 2, 0 }, // 1000
+        { 0, 3, 2, 1 }, // 1001
+        { 3, 0, 2, 1 }, // 1010
+        { 0, 1, 3, 2 }, // 1011
+        { 2, 3, 0, 1 }, // 1100
+        { 0, 3, 1, 2 }, // 1101
+        { 3, 0, 1, 2 }, // 1110
+        { 0, 1, 2, 3 }  // 1111  - skip
+    };
+    int i, k, iRes;
+    unsigned uTruthRes;
+    assert( Phase < 16 );
+    uTruthRes = 0;
+    for ( i = 0; i < 16; i++ )
+        if ( uTruth & (1 << i) )
+        {
+            for ( iRes = 0, k = 0; k < 4; k++ )
+                if ( i & (1 << k) )
+                    iRes |= (1 << Perm[Phase][k]);
+            uTruthRes |= (1 << iRes);
+        }
+    return uTruthRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
new file mode 100644
index 00000000..ae8665ef
--- /dev/null
+++ b/src/opt/rwr/rwrUtil.c
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [rwrUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting package.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rwrUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the array of fanout counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vFanNums;
+    Abc_Obj_t * pObj;
+    int i;
+    vFanNums = Vec_IntAlloc( 0 );
+    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( Abc_ObjIsNode( pObj ) )
+            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
+    return vFanNums;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the array of required times.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rwt_NtkRequiredLevels( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vReqTimes;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pFanout;
+    int i, k, nLevelsMax, nLevelsCur;
+    // start the required times
+    vReqTimes = Vec_IntAlloc( 0 );
+    Vec_IntFill( vReqTimes, Abc_NtkObjNumMax(pNtk), ABC_INFINITY );
+    // compute levels in reverse topological order
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_IntWriteEntry( vReqTimes, pObj->Id, 0 );
+    vNodes = Abc_NtkDfsReverse( pNtk );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        nLevelsCur = 0;
+        Abc_ObjForEachFanout( pObj, pFanout, k )
+            if ( nLevelsCur < Vec_IntEntry(vReqTimes, pFanout->Id) )
+                nLevelsCur = Vec_IntEntry(vReqTimes, pFanout->Id);
+        Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsCur + 1 );
+    }
+    Vec_PtrFree( vNodes );
+    // convert levels into required times: RetTime = NumLevels + 1 - Level
+    nLevelsMax = Abc_AigGetLevelNum(pNtk) + 1;
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Vec_IntWriteEntry( vReqTimes, pObj->Id, nLevelsMax - Vec_IntEntry(vReqTimes, pObj->Id) );
+//    Abc_NtkForEachNode( pNtk, pObj, i )
+//        printf( "(%d,%d)", pObj->Level, Vec_IntEntry(vReqTimes, pObj->Id) );
+//    printf( "\n" );
+    return vReqTimes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/sim/simSupp.c b/src/sat/sim/simSupp.c
index 3ae1d3ab..570e8dc6 100644
--- a/src/sat/sim/simSupp.c
+++ b/src/sat/sim/simSupp.c
@@ -136,7 +136,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
 {
     Sim_Pat_t * pPat;
     Vec_Int_t * vTargets;
-    Vec_Ptr_t * vNodesByLevel;
+    Vec_Vec_t * vNodesByLevel;
     Abc_Obj_t * pNodeCi, * pNode;
     int i, k, v, Output, LuckyPat, fType0, fType1;
     int Counter = 0;
@@ -147,7 +147,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
     // complement the simulation info of the selected CI
     Sim_UtilFlipSimInfo( p, pNodeCi );
     // simulate the levelized structure of nodes
-    Vec_PtrForEachEntryByLevel( vNodesByLevel, pNode, i, k )
+    Vec_VecForEachEntry( vNodesByLevel, pNode, i, k )
     {
         fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
         fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
@@ -213,7 +213,7 @@ int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, bool fUseTargets )
             }
         }
     }
-    Vec_PtrFreeFree( vNodesByLevel );
+    Vec_VecFree( vNodesByLevel );
     return Counter;
 }
 
diff --git a/src/sop/ft/ft.h b/src/sop/ft/ft.h
index 81e1a2dc..c4eab09f 100644
--- a/src/sop/ft/ft.h
+++ b/src/sop/ft/ft.h
@@ -52,16 +52,17 @@ struct Ft_Node_t_
 };
 
 /*
-    The factored form of a SOP is an array (Vec_Int_t) of entries Ft_Node_t.
+    The factored form of an SOP is an array (Vec_Int_t) of entries of type Ft_Node_t.
     If the SOP has n input variables (some of them may not be in the true support)
-    the first n entries of the factored form array have 0s. This representation 
-    makes it each to translate the factored form into an AIG.
-
-    The node structure contains fanins of the node and their complemented attributes 
-    (using AIG semantics). The elementary variable (buffer or interver) are 
-    represented as a node with the same fanins. For example: x' = AND( x', x' ).
-    The constant node cannot be represented. Constant functions should be detected
-    before calling the factoring procedure.
+    the first n entries of the factored form array are zeros. The other entries of the array
+    represent the internal AND nodes of the factored form, and possibly the constant node.
+    This representation makes it easy to translate the factored form into an AIG.
+    The factored AND nodes contains fanins of the node and their complemented attributes 
+    (using AIG semantics). The elementary variable (buffer or interver) are represented 
+    as a node with the same fanins. For example: x' = AND( x', x' ).
+    The constant node is represented a special node with the constant flag set. 
+    If the constant node and the elementary variable are present, no other internal 
+    AND nodes are allowed in the factored form.
 */
 
 // working with complemented attributes of objects