Version abc80717

21 files changed, 3825 insertions, 45 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 96aa1c93..93ca298a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -505,6 +505,7 @@ extern int             Aig_ManPoCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
 extern void            Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
 extern void            Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
+extern void            Aig_ManFlipFirstPo( Aig_Man_t * p );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index dae7e42b..a1c3eb01 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -433,6 +433,23 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
     p->nTruePos = Aig_ManPoNum(p) - nRegs;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFlipFirstPo( Aig_Man_t * p )
+{
+    Aig_ObjChild0Flip( Aig_ManPo(p, 0) ); 
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index e3e6bfe1..f1c446fe 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -238,26 +238,26 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable )
+void Cnf_DataWriteIntoFileGz( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
-    FILE * pFile;
+    gzFile pFile;
     int * pLit, * pStop, i;
-    pFile = fopen( pFileName, "w" );
+    pFile = gzopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
         printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
         return;
     }
-    fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
-    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
+    gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
+    gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
     for ( i = 0; i < p->nClauses; i++ )
     {
         for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
-            fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
-        fprintf( pFile, "0\n" );
+            gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
+        gzprintf( pFile, "0\n" );
     }
-    fprintf( pFile, "\n" );
-    fclose( pFile );
+    gzprintf( pFile, "\n" );
+    gzclose( pFile );
 }
 
 /**Function*************************************************************
@@ -273,24 +273,29 @@ void Cnf_DataWriteIntoFile_old( Cnf_Dat_t * p, char * pFileName, int fReadable )
 ***********************************************************************/
 void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
-    gzFile pFile;
+    FILE * pFile;
     int * pLit, * pStop, i;
-    pFile = gzopen( pFileName, "wb" );
+    if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) 
+    {
+        Cnf_DataWriteIntoFileGz( p, pFileName, fReadable );
+        return;
+    }
+    pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
         printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
         return;
     }
-    gzprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
-    gzprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
+    fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
+    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
     for ( i = 0; i < p->nClauses; i++ )
     {
         for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
-            gzprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
-        gzprintf( pFile, "0\n" );
+            fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
+        fprintf( pFile, "0\n" );
     }
-    gzprintf( pFile, "\n" );
-    gzclose( pFile );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 96c0de77..3365ac9a 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -389,11 +389,11 @@ PRT( "Time", clock() - clkTotal );
 clk = clock();
     if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
-        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
+        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth );
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, pParSec->fVeryVerbose, &Depth );
+        RetValue = Saig_Interpolate( pNew, 5000, 0, 1, 0, pParSec->fVeryVerbose, &Depth );
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 105f4c4a..6eb2cc95 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -876,6 +876,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
             p->pNtk->attrWhite = 0;
         else if ( strcmp( pToken, "box" ) == 0 )
             p->pNtk->attrBox = 1;
+        else if ( strcmp( pToken, "logic" ) == 0 )
+            p->pNtk->attrBox = 0;
         else if ( strcmp( pToken, "white" ) == 0 )
             p->pNtk->attrWhite = 1;
         else if ( strcmp( pToken, "comb" ) == 0 )
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index e3d0a061..222130f3 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -24,7 +24,7 @@
 #ifdef __cplusplus
 extern "C" {
 #endif
-
+ 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -86,7 +86,10 @@ struct Nwk_Obj_t_
     Nwk_Man_t *        pMan;           // the manager  
     Hop_Obj_t *        pFunc;          // functionality
     void *             pCopy;          // temporary pointer
-    void *             pNext;          // temporary pointer
+    union {
+        void *         pNext;          // temporary pointer
+        int            iTemp;          // temporary number
+    };
     // node information
     unsigned           Type     :  3;  // object type
     unsigned           fInvert  :  1;  // complemented attribute
diff --git a/src/aig/nwk/nwkMan.c b/src/aig/nwk/nwkMan.c
index d9a41849..252546e8 100644
--- a/src/aig/nwk/nwkMan.c
+++ b/src/aig/nwk/nwkMan.c
@@ -153,7 +153,7 @@ int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
         ParsBest.Nodes = ParsNew.Nodes; 
         ParsBest.nPis  = ParsNew.nPis; 
         ParsBest.nPos  = ParsNew.nPos;
-        // writ the network
+        // write the network
         Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
 //        Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL );
         return 1;
diff --git a/src/aig/nwk/nwkMerge.c b/src/aig/nwk/nwkMerge.c
index 1a5255d3..531bc1c0 100644
--- a/src/aig/nwk/nwkMerge.c
+++ b/src/aig/nwk/nwkMerge.c
@@ -348,6 +348,45 @@ void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Sort pairs by the first vertex in the topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphSortPairs( Nwk_Grf_t * p )
+{
+    int nSize = Vec_IntSize(p->vPairs);
+    int * pIdToPair, i;
+    // allocate storage
+    pIdToPair = ALLOC( int, p->nObjs+1 );
+    for ( i = 0; i <= p->nObjs; i++ )
+        pIdToPair[i] = -1;
+    // create mapping
+    for ( i = 0; i < p->vPairs->nSize; i += 2 )
+    {
+        assert( pIdToPair[ p->vPairs->pArray[i] ] == -1 );
+        pIdToPair[ p->vPairs->pArray[i] ] = p->vPairs->pArray[i+1];
+    }
+    // recreate pairs
+    Vec_IntClear( p->vPairs );
+    for ( i = 0; i <= p->nObjs; i++ )
+        if ( pIdToPair[i] >= 0 )
+        {
+            assert( i < pIdToPair[i] );
+            Vec_IntPush( p->vPairs, i );
+            Vec_IntPush( p->vPairs, pIdToPair[i] );
+        }
+    assert( nSize == Vec_IntSize(p->vPairs) );
+    free( pIdToPair );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Updates the problem after pulling out one edge.]
 
   Description []
@@ -615,6 +654,7 @@ void Nwk_ManGraphSolve( Nwk_Grf_t * p )
         if ( j == NWK_MAX_LIST + 1 )
             break;
     }
+    Nwk_ManGraphSortPairs( p );
 }
 
 /**Function*************************************************************
@@ -982,6 +1022,9 @@ Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars )
         Nwk_ManGraphReportMemoryUsage( p );
     }
     vResult = p->vPairs; p->vPairs = NULL;
+    for ( i = 0; i < vResult->nSize; i += 2 )
+        printf( "(%d,%d) ", vResult->pArray[i], vResult->pArray[i+1] );
+    printf( "\n" );
     Nwk_ManGraphFree( p );
     return vResult;
 }
diff --git a/src/aig/nwk2/module.make b/src/aig/nwk2/module.make
new file mode 100644
index 00000000..226a68ef
--- /dev/null
+++ b/src/aig/nwk2/module.make
@@ -0,0 +1,7 @@
+SRC +=    src/aig/nwk/nwkCheck.c \
+    src/aig/nwk/nwkDfs.c \
+    src/aig/nwk/nwkFanio.c \
+    src/aig/nwk/nwkMan.c \
+    src/aig/nwk/nwkMerge.c \
+    src/aig/nwk/nwkObj.c \
+    src/aig/nwk/nwkUtil.c
diff --git a/src/aig/nwk2/nwk.h b/src/aig/nwk2/nwk.h
new file mode 100644
index 00000000..465bd651
--- /dev/null
+++ b/src/aig/nwk2/nwk.h
@@ -0,0 +1,278 @@
+/**CFile****************************************************************
+
+  FileName    [nwk.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwk.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NWK_H__
+#define __NWK_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+#include "hop.h"
+#include "tim.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Nwk_Man_t_    Nwk_Man_t;
+typedef struct Nwk_Obj_t_    Nwk_Obj_t;
+
+// object types
+typedef enum { 
+    NWK_OBJ_NONE,                      // 0: non-existant object
+    NWK_OBJ_CI,                        // 1: combinational input
+    NWK_OBJ_CO,                        // 2: combinational output
+    NWK_OBJ_NODE,                      // 3: logic node
+    NWK_OBJ_LATCH,                     // 4: register
+    NWK_OBJ_VOID                       // 5: unused object
+} Nwk_Type_t;
+
+struct Nwk_Man_t_
+{
+    // models of this design
+    char *             pName;          // the name of this design
+    char *             pSpec;          // the name of input file
+    // node representation
+    Vec_Ptr_t *        vCis;           // the primary inputs of the extracted part
+    Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
+    Vec_Ptr_t *        vObjs;          // the objects in the topological order
+    int                nObjs[NWK_OBJ_VOID]; // counter of objects of each type
+    int                nFanioPlus;     // the number of extra fanins/fanouts alloc by default
+    // functionality, timing, memory, etc
+    Hop_Man_t *        pManHop;        // the functionality representation
+    Tim_Man_t *        pManTime;       // the timing manager
+//    If_Lib_t *         pLutLib;        // the LUT library
+    Aig_MmFlex_t *     pMemObjs;       // memory for objects
+    Vec_Ptr_t *        vTemp;          // array used for incremental updates
+    int                nTravIds;       // the counter of traversal IDs
+    int                nRealloced;     // the number of realloced nodes
+    // sequential information
+    int                nLatches;       // the total number of latches 
+    int                nTruePis;       // the number of true primary inputs
+    int                nTruePos;       // the number of true primary outputs
+};
+
+struct Nwk_Obj_t_
+{
+    Nwk_Man_t *        pMan;           // the manager  
+    Hop_Obj_t *        pFunc;          // functionality
+    void *             pCopy;          // temporary pointer
+    union {
+        void *         pNext;          // temporary pointer
+        int            iTemp;          // temporary number
+    };
+    // node information
+    unsigned           Type     :  3;  // object type
+    unsigned           fInvert  :  1;  // complemented attribute
+    unsigned           MarkA    :  1;  // temporary mark  
+    unsigned           MarkB    :  1;  // temporary mark
+    unsigned           MarkC    :  1;  // temporary mark
+    unsigned           PioId    : 25;  // number of this node in the PI/PO list
+    int                Id;             // unique ID
+    int                TravId;         // traversal ID
+    // timing information
+    int                Level;          // the topological level
+    float              tArrival;       // the arrival time
+    float              tRequired;      // the required time
+    float              tSlack;         // the slack
+    // fanin/fanout representation
+    int                nFanins;        // the number of fanins
+    int                nFanouts;       // the number of fanouts
+    int                nFanioAlloc;    // the number of allocated fanins/fanouts
+    Nwk_Obj_t **       pFanio;         // fanins/fanouts
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                      INLINED FUNCTIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int         Nwk_ManCiNum( Nwk_Man_t * p )           { return p->nObjs[NWK_OBJ_CI];                } 
+static inline int         Nwk_ManCoNum( Nwk_Man_t * p )           { return p->nObjs[NWK_OBJ_CO];                } 
+static inline int         Nwk_ManNodeNum( Nwk_Man_t * p )         { return p->nObjs[NWK_OBJ_NODE];              } 
+static inline int         Nwk_ManLatchNum( Nwk_Man_t * p )        { return p->nObjs[NWK_OBJ_LATCH];             } 
+static inline int         Nwk_ManObjNumMax( Nwk_Man_t * p )       { return Vec_PtrSize(p->vObjs);               }
+
+static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i )       { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCis, i );          } 
+static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i )       { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCos, i );          } 
+static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i )      { return (Nwk_Obj_t *)Vec_PtrEntry( p->vObjs, i );         } 
+
+static inline int         Nwk_ObjId( Nwk_Obj_t * p )              { return p->Id;                               } 
+static inline int         Nwk_ObjPioNum( Nwk_Obj_t * p )          { return p->PioId;                            } 
+static inline int         Nwk_ObjFaninNum( Nwk_Obj_t * p )        { return p->nFanins;                          } 
+static inline int         Nwk_ObjFanoutNum( Nwk_Obj_t * p )       { return p->nFanouts;                         } 
+
+static inline Nwk_Obj_t * Nwk_ObjFanin0( Nwk_Obj_t * p )          { return p->pFanio[0];                        } 
+static inline Nwk_Obj_t * Nwk_ObjFanout0( Nwk_Obj_t * p )         { return p->pFanio[p->nFanins];               } 
+static inline Nwk_Obj_t * Nwk_ObjFanin( Nwk_Obj_t * p, int i )    { return p->pFanio[i];                        } 
+static inline Nwk_Obj_t * Nwk_ObjFanout( Nwk_Obj_t * p, int i )   { return p->pFanio[p->nFanins+1];             } 
+
+static inline int         Nwk_ObjIsNone( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NONE;             } 
+static inline int         Nwk_ObjIsCi( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CI;               } 
+static inline int         Nwk_ObjIsCo( Nwk_Obj_t * p )            { return p->Type == NWK_OBJ_CO;               } 
+static inline int         Nwk_ObjIsNode( Nwk_Obj_t * p )          { return p->Type == NWK_OBJ_NODE;             } 
+static inline int         Nwk_ObjIsLatch( Nwk_Obj_t * p )         { return p->Type == NWK_OBJ_LATCH;            } 
+static inline int         Nwk_ObjIsPi( Nwk_Obj_t * p )            { return Nwk_ObjIsCi(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCi(p->pMan->pManTime, p->PioId) == -1); } 
+static inline int         Nwk_ObjIsPo( Nwk_Obj_t * p )            { return Nwk_ObjIsCo(p) && (p->pMan->pManTime == NULL || Tim_ManBoxForCo(p->pMan->pManTime, p->PioId) == -1);  }
+static inline int         Nwk_ObjIsLi( Nwk_Obj_t * p )            { return p->pMan->nTruePos && Nwk_ObjIsCo(p) && (int)p->PioId >= p->pMan->nTruePos;       } 
+static inline int         Nwk_ObjIsLo( Nwk_Obj_t * p )            { return p->pMan->nTruePis && Nwk_ObjIsCi(p) && (int)p->PioId >= p->pMan->nTruePis;       } 
+
+static inline float       Nwk_ObjArrival( Nwk_Obj_t * pObj )                 { return pObj->tArrival;           }
+static inline float       Nwk_ObjRequired( Nwk_Obj_t * pObj )                { return pObj->tRequired;          }
+static inline float       Nwk_ObjSlack( Nwk_Obj_t * pObj )                   { return pObj->tSlack;             }
+static inline void        Nwk_ObjSetArrival( Nwk_Obj_t * pObj, float Time )  { pObj->tArrival   = Time;         }
+static inline void        Nwk_ObjSetRequired( Nwk_Obj_t * pObj, float Time ) { pObj->tRequired  = Time;         }
+static inline void        Nwk_ObjSetSlack( Nwk_Obj_t * pObj, float Time )    { pObj->tSlack     = Time;         }
+
+static inline int         Nwk_ObjLevel( Nwk_Obj_t * pObj )                   { return pObj->Level;              }
+static inline void        Nwk_ObjSetLevel( Nwk_Obj_t * pObj, int Level )     { pObj->Level = Level;             }
+
+static inline void        Nwk_ObjSetTravId( Nwk_Obj_t * pObj, int TravId )   { pObj->TravId = TravId;                           }
+static inline void        Nwk_ObjSetTravIdCurrent( Nwk_Obj_t * pObj )        { pObj->TravId = pObj->pMan->nTravIds;             }
+static inline void        Nwk_ObjSetTravIdPrevious( Nwk_Obj_t * pObj )       { pObj->TravId = pObj->pMan->nTravIds - 1;         }
+static inline int         Nwk_ObjIsTravIdCurrent( Nwk_Obj_t * pObj )         { return pObj->TravId == pObj->pMan->nTravIds;     }
+static inline int         Nwk_ObjIsTravIdPrevious( Nwk_Obj_t * pObj )        { return pObj->TravId == pObj->pMan->nTravIds - 1; }
+
+static inline int         Nwk_ManTimeEqual( float f1, float f2, float Eps )  { return (f1 < f2 + Eps) && (f2 < f1 + Eps);  }
+static inline int         Nwk_ManTimeLess( float f1, float f2, float Eps )   { return (f1 < f2 + Eps);                     }
+static inline int         Nwk_ManTimeMore( float f1, float f2, float Eps )   { return (f1 + Eps > f2);                     }
+
+////////////////////////////////////////////////////////////////////////
+///                         ITERATORS                                ///
+////////////////////////////////////////////////////////////////////////
+
+#define Nwk_ManForEachCi( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCis, pObj, i )
+#define Nwk_ManForEachCo( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCos, pObj, i )
+#define Nwk_ManForEachPi( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCis, pObj, i )                                \
+        if ( !Nwk_ObjIsPi(pObj) ) {} else
+#define Nwk_ManForEachPo( p, pObj, i )                                     \
+    Vec_PtrForEachEntry( p->vCos, pObj, i )                                \
+        if ( !Nwk_ObjIsPo(pObj) ) {} else
+#define Nwk_ManForEachObj( p, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( pObj == NULL ) {} else
+#define Nwk_ManForEachNode( p, pObj, i )                                   \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Nwk_ObjIsNode(pObj) ) {} else
+#define Nwk_ManForEachLatch( p, pObj, i )                                  \
+    for ( i = 0; (i < Vec_PtrSize(p->vObjs)) && (((pObj) = Vec_PtrEntry(p->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Nwk_ObjIsLatch(pObj) ) {} else
+
+#define Nwk_ObjForEachFanin( pObj, pFanin, i )                                  \
+    for ( i = 0; (i < (int)(pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
+#define Nwk_ObjForEachFanout( pObj, pFanout, i )                                \
+    for ( i = 0; (i < (int)(pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+
+// sequential iterators
+#define Nwk_ManForEachPiSeq( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vCis, pObj, i, (p)->nTruePis )
+#define Nwk_ManForEachPoSeq( p, pObj, i )                                           \
+    Vec_PtrForEachEntryStop( p->vCos, pObj, i, (p)->nTruePos )
+#define Nwk_ManForEachLoSeq( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCis, i+(p)->nTruePis)), 1); i++ )
+#define Nwk_ManForEachLiSeq( p, pObj, i )                                           \
+    for ( i = 0; (i < (p)->nLatches) && (((pObj) = Vec_PtrEntry(p->vCos, i+(p)->nTruePos)), 1); i++ )
+#define Nwk_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )                               \
+    for ( i = 0; (i < (p)->nLatches) && (((pObjLi) = Nwk_ManCo(p, i+(p)->nTruePos)), 1)        \
+        && (((pObjLo) = Nwk_ManCi(p, i+(p)->nTruePis)), 1); i++ )
+
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== nwkCheck.c ==========================================================*/
+extern int             Nwk_ManCheck( Nwk_Man_t * p );
+/*=== nwkDfs.c ==========================================================*/
+extern int             Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevel( Nwk_Man_t * pNtk );
+extern int             Nwk_ManLevelMax( Nwk_Man_t * pNtk );
+extern Vec_Vec_t *     Nwk_ManLevelize( Nwk_Man_t * pNtk );
+extern Vec_Ptr_t *     Nwk_ManDfs( Nwk_Man_t * pNtk );
+extern Vec_Ptr_t *     Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern Vec_Ptr_t *     Nwk_ManDfsReverse( Nwk_Man_t * pNtk );
+extern Vec_Ptr_t *     Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern void            Nwk_ManSupportSum( Nwk_Man_t * pNtk );
+extern int             Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
+/*=== nwkFanio.c ==========================================================*/
+extern void            Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern void            Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern int             Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern int             Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
+extern void            Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern void            Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern void            Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern void            Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
+extern void            Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
+/*=== nwkMan.c ============================================================*/
+extern Nwk_Man_t *     Nwk_ManAlloc();
+extern void            Nwk_ManFree( Nwk_Man_t * p );
+//extern void            Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
+/*=== nwkObj.c ============================================================*/
+extern Nwk_Obj_t *     Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts );
+extern Nwk_Obj_t *     Nwk_ManCreateCo( Nwk_Man_t * pMan );
+extern Nwk_Obj_t *     Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern Nwk_Obj_t *     Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern Nwk_Obj_t *     Nwk_ManCreateLatch( Nwk_Man_t * pMan );
+extern void            Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
+extern void            Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
+/*=== nwkUtil.c ============================================================*/
+extern void            Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
+extern int             Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
+extern int             Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk );
+extern int             Nwk_ManPiNum( Nwk_Man_t * pNtk );
+extern int             Nwk_ManPoNum( Nwk_Man_t * pNtk );
+extern int             Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
+extern int             Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern int             Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
+extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
+extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
+extern void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
+extern void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/nwk2/nwkCheck.c b/src/aig/nwk2/nwkCheck.c
new file mode 100644
index 00000000..6922e439
--- /dev/null
+++ b/src/aig/nwk2/nwkCheck.c
@@ -0,0 +1,73 @@
+/**CFile****************************************************************
+
+  FileName    [nwkCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [Consistency checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checking the logic network for consistency.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManCheck( Nwk_Man_t * p )
+{
+    Nwk_Obj_t * pObj;
+    int i, k, m;
+    // check if the nodes have duplicated fanins
+    Nwk_ManForEachNode( p, pObj, i )
+    {
+        for ( k = 0; k < pObj->nFanins; k++ )
+            for ( m = k + 1; m < pObj->nFanins; m++ )
+                if ( pObj->pFanio[k] == pObj->pFanio[m] )
+                    printf( "Node %d has duplicated fanin %d.\n", pObj->Id, pObj->pFanio[k]->Id );
+    }
+/*
+    // check if all nodes are in the correct fanin/fanout relationship
+    Nwk_ManForEachObj( p, pObj, i )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+            if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id );
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+            if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )
+                printf( "Nwk_ManCheck(): Object %d has fanout %d which does not have a corresponding fanin.\n", pObj->Id, pNext->Id );
+    }
+*/
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkDfs.c b/src/aig/nwk2/nwkDfs.c
new file mode 100644
index 00000000..c1c77349
--- /dev/null
+++ b/src/aig/nwk2/nwkDfs.c
@@ -0,0 +1,659 @@
+/**CFile****************************************************************
+
+  FileName    [nwkDfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [DFS traversals.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies that the objects are in a topo order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k, iBox, iTerm1, nTerms;
+    Nwk_ManIncrementTravId( pNtk );
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
+        {
+            Nwk_ObjForEachFanin( pObj, pNext, k )
+            {
+                if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                {
+                    printf( "Node %d has fanin %d that is not in a topological order.\n", pObj->Id, pNext->Id );
+                    return 0;
+                }
+            }
+        }
+        else if ( Nwk_ObjIsCi(pObj) )
+        {
+            if ( pNtk->pManTime )
+            {
+                iBox = Tim_ManBoxForCi( pNtk->pManTime, pObj->PioId );
+                if ( iBox >= 0 ) // this is not a true PI
+                {
+                    iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
+                    for ( k = 0; k < nTerms; k++ )
+                    {
+                        pNext = Nwk_ManCo( pNtk, iTerm1 + k );
+                        if ( !Nwk_ObjIsTravIdCurrent(pNext) )
+                        {
+                            printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
+                            return 0;
+                        }
+                    }
+                }
+            }
+        }
+        else
+            assert( 0 );
+        Nwk_ObjSetTravIdCurrent( pObj );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Assumes that white boxes have unit level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLevelBackup( Nwk_Man_t * pNtk )
+{
+    Tim_Man_t * pManTimeUnit;
+    Nwk_Obj_t * pObj, * pFanin;
+    int i, k, LevelMax, Level;
+    assert( Nwk_ManVerifyTopoOrder(pNtk) );
+    // clean the levels
+    Nwk_ManForEachObj( pNtk, pObj, i )
+        Nwk_ObjSetLevel( pObj, 0 );
+    // perform level computation
+    LevelMax = 0;
+    pManTimeUnit = pNtk->pManTime ? Tim_ManDupUnit( pNtk->pManTime ) : NULL;
+    if ( pManTimeUnit )
+        Tim_ManIncrementTravId( pManTimeUnit );
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Nwk_ObjIsCi(pObj) )
+        {
+            Level = pManTimeUnit? (int)Tim_ManGetCiArrival( pManTimeUnit, pObj->PioId ) : 0;
+            Nwk_ObjSetLevel( pObj, Level );
+        }
+        else if ( Nwk_ObjIsCo(pObj) )
+        {
+            Level = Nwk_ObjLevel( Nwk_ObjFanin0(pObj) );
+            if ( pManTimeUnit )
+                Tim_ManSetCoArrival( pManTimeUnit, pObj->PioId, (float)Level );
+            Nwk_ObjSetLevel( pObj, Level );
+            if ( LevelMax < Nwk_ObjLevel(pObj) )
+                LevelMax = Nwk_ObjLevel(pObj);
+        }
+        else if ( Nwk_ObjIsNode(pObj) )
+        {
+            Level = 0;
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+                if ( Level < Nwk_ObjLevel(pFanin) )
+                    Level = Nwk_ObjLevel(pFanin);
+            Nwk_ObjSetLevel( pObj, Level + 1 );
+        }
+        else
+            assert( 0 );
+    }
+    // set the old timing manager
+    if ( pManTimeUnit )
+        Tim_ManStop( pManTimeUnit );
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManLevel_rec( Nwk_Obj_t * pObj )
+{
+    Tim_Man_t * pManTime = pObj->pMan->pManTime;
+    Nwk_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjIsCi(pObj) )
+    {
+        if ( pManTime ) 
+        {
+            iBox = Tim_ManBoxForCi( pManTime, pObj->PioId );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Nwk_ManCo(pObj->pMan, iTerm1 + i);
+                    Nwk_ManLevel_rec( pNext );
+                    if ( LevelMax < Nwk_ObjLevel(pNext) )
+                        LevelMax = Nwk_ObjLevel(pNext);
+                }
+                LevelMax++;
+            }
+        }
+    }
+    else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCo(pObj) )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, i )
+        {
+            Nwk_ManLevel_rec( pNext );
+            if ( LevelMax < Nwk_ObjLevel(pNext) )
+                LevelMax = Nwk_ObjLevel(pNext);
+        }
+        if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFaninNum(pObj) > 0 )
+            LevelMax++;
+    }
+    else
+        assert( 0 );
+    Nwk_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Does not assume that the objects are in a topo order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLevel( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Nwk_ManForEachObj( pNtk, pObj, i )
+        Nwk_ObjSetLevel( pObj, 0 );
+    Nwk_ManIncrementTravId( pNtk );
+    Nwk_ManForEachPo( pNtk, pObj, i )
+    {
+        Nwk_ManLevel_rec( pObj );
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    }
+    Nwk_ManForEachCi( pNtk, pObj, i )
+    {
+        Nwk_ManLevel_rec( pObj );
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    }
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description [Does not assume that the objects are in a topo order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLevelMax( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i, LevelMax = 0;
+    Nwk_ManForEachPo( pNtk, pObj, i )
+        if ( LevelMax < Nwk_ObjLevel(pObj) )
+            LevelMax = Nwk_ObjLevel(pObj);
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of objects in the AIG manager ordered by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, i;
+//    assert( Nwk_ManVerifyLevel(pNtk) );
+    nLevels = Nwk_ManLevelMax( pNtk );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        assert( Nwk_ObjLevel(pObj) <= nLevels );
+        Vec_VecPush( vLevels, Nwk_ObjLevel(pObj), pObj );
+    }
+    return vLevels;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDfs_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        Nwk_ManDfs_rec( pNext, vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Nwk_ManForEachObj( pNtk, pObj, i )
+    {
+        if ( Nwk_ObjIsCi(pObj) )
+        {
+            Nwk_ObjSetTravIdCurrent( pObj );
+            Vec_PtrPush( vNodes, pObj );
+        }
+        else if ( Nwk_ObjIsCo(pObj) )
+            Nwk_ManDfs_rec( pObj, vNodes );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDfsNodes_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjIsCi(pObj) )
+        return;
+    assert( Nwk_ObjIsNode(pObj) );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        Nwk_ManDfsNodes_rec( pNext, vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of internal nodes rooted in the given nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    // set the traversal ID
+    Nwk_ManIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    // go through the PO nodes and call for each of them
+    for ( i = 0; i < nNodes; i++ )
+        if ( Nwk_ObjIsCo(ppNodes[i]) )
+            Nwk_ManDfsNodes_rec( Nwk_ObjFanin0(ppNodes[i]), vNodes );
+        else
+            Nwk_ManDfsNodes_rec( ppNodes[i], vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDfsReverse_rec( Nwk_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms;
+    if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pObj );
+    if ( Nwk_ObjIsCo(pObj) )
+    {
+        if ( pObj->pMan->pManTime )
+        {
+            iBox = Tim_ManBoxForCo( pObj->pMan->pManTime, pObj->PioId );
+            if ( iBox >= 0 ) // this is not a true PO
+            {
+                iTerm1 = Tim_ManBoxOutputFirst( pObj->pMan->pManTime, iBox );
+                nTerms = Tim_ManBoxOutputNum( pObj->pMan->pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Nwk_ManCi(pObj->pMan, iTerm1 + i);
+                    Nwk_ManDfsReverse_rec( pNext, vNodes );
+                }
+            }
+        }
+    }
+    else if ( Nwk_ObjIsNode(pObj) || Nwk_ObjIsCi(pObj) )
+    {
+        Nwk_ObjForEachFanout( pObj, pNext, i )
+            Nwk_ManDfsReverse_rec( pNext, vNodes );
+    }
+    else
+        assert( 0 );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the DFS ordered array of all objects except latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManIncrementTravId( pNtk );
+    vNodes = Vec_PtrAlloc( 100 );
+    Nwk_ManForEachPi( pNtk, pObj, i )
+        Nwk_ManDfsReverse_rec( pObj, vNodes );
+    // add nodes without fanins
+    Nwk_ManForEachNode( pNtk, pObj, i )
+        if ( Nwk_ObjFaninNum(pObj) == 0 && !Nwk_ObjIsTravIdCurrent(pObj) )
+            Vec_PtrPush( vNodes, pObj );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManSupportNodes_rec( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    // if this node is already visited, skip
+    if ( Nwk_ObjIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Nwk_ObjSetTravIdCurrent( pNode );
+    // collect the CI
+    if ( Nwk_ObjIsCi(pNode) )
+    {
+        Vec_PtrPush( vNodes, pNode );
+        return;
+    }
+    assert( Nwk_ObjIsNode( pNode ) );
+    // visit the transitive fanin of the node
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        Nwk_ManSupportNodes_rec( pFanin, vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the set of CI nodes in the support of the given nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    // set the traversal ID
+    Nwk_ManIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    // go through the PO nodes and call for each of them
+    for ( i = 0; i < nNodes; i++ )
+        if ( Nwk_ObjIsCo(ppNodes[i]) )
+            Nwk_ManSupportNodes_rec( Nwk_ObjFanin0(ppNodes[i]), vNodes );
+        else
+            Nwk_ManSupportNodes_rec( ppNodes[i], vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the sum total of supports of all outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManSupportSum( Nwk_Man_t * pNtk )
+{
+    Vec_Ptr_t * vSupp;
+    Nwk_Obj_t * pObj;
+    int i, nTotalSupps = 0;
+    Nwk_ManForEachCo( pNtk, pObj, i )
+    {
+        vSupp = Nwk_ManSupportNodes( pNtk, &pObj, 1 );
+        nTotalSupps += Vec_PtrSize( vSupp );
+        Vec_PtrFree( vSupp );
+    }
+    printf( "Total supports = %d.\n", nTotalSupps );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ObjDeref_rec( Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Nwk_ObjIsCi(pNode) )
+        return 0;
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        assert( pFanin->nFanouts > 0 );
+        if ( --pFanin->nFanouts == 0 )
+            Counter += Nwk_ObjDeref_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ObjRef_rec( Nwk_Obj_t * pNode )
+{
+    Nwk_Obj_t * pFanin;
+    int i, Counter = 1;
+    if ( Nwk_ObjIsCi(pNode) )
+        return 0;
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+    {
+        if ( pFanin->nFanouts++ == 0 )
+            Counter += Nwk_ObjRef_rec( pFanin );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal and boundary nodes in the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjMffcLabel_rec( Nwk_Obj_t * pNode, int fTopmost )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    // add to the new support nodes
+    if ( !fTopmost && (Nwk_ObjIsCi(pNode) || pNode->nFanouts > 0) )
+        return;
+    // skip visited nodes
+    if ( Nwk_ObjIsTravIdCurrent(pNode) )
+        return;
+    Nwk_ObjSetTravIdCurrent(pNode);
+    // recur on the children
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        Nwk_ObjMffcLabel_rec( pFanin, 0 );
+    // collect the internal node
+//    printf( "%d ", pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal nodes of the MFFC limited by cut.]
+
+  Description []
+               
+  SideEffects [Increments the trav ID and marks visited nodes.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode )
+{
+    int Count1, Count2;
+    // dereference the node
+    Count1 = Nwk_ObjDeref_rec( pNode );
+    // collect the nodes inside the MFFC
+    Nwk_ManIncrementTravId( pNode->pMan );
+    Nwk_ObjMffcLabel_rec( pNode, 1 );
+    // reference it back
+    Count2 = Nwk_ObjRef_rec( pNode );
+    assert( Count1 == Count2 );
+    return Count1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkFanio.c b/src/aig/nwk2/nwkFanio.c
new file mode 100644
index 00000000..4068a1a5
--- /dev/null
+++ b/src/aig/nwk2/nwkFanio.c
@@ -0,0 +1,309 @@
+/**CFile****************************************************************
+
+  FileName    [nwkFanio.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [Manipulation of fanins/fanouts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects fanins of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pFanin;
+    int i;
+    Vec_PtrClear(vNodes);
+    Nwk_ObjForEachFanin( pNode, pFanin, i )
+        Vec_PtrPush( vNodes, pFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects fanouts of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Nwk_Obj_t * pFanout;
+    int i;
+    Vec_PtrClear(vNodes);
+    Nwk_ObjForEachFanout( pNode, pFanout, i )
+        Vec_PtrPush( vNodes, pFanout );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the fanin of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
+{  
+    Nwk_Obj_t * pTemp;
+    int i;
+    Nwk_ObjForEachFanin( pObj, pTemp, i )
+        if ( pTemp == pFanin )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of the fanout of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout )
+{  
+    Nwk_Obj_t * pTemp;
+    int i;
+    Nwk_ObjForEachFanout( pObj, pTemp, i )
+        if ( pTemp == pFanout )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node has to be reallocated.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Nwk_ObjReallocIsNeeded( Nwk_Obj_t * pObj )
+{  
+    return pObj->nFanins + pObj->nFanouts == pObj->nFanioAlloc;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Reallocates the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Nwk_Obj_t * Nwk_ManReallocNode( Nwk_Obj_t * pObj )
+{  
+    Nwk_Obj_t ** pFanioOld = pObj->pFanio;
+    assert( Nwk_ObjReallocIsNeeded(pObj) );
+    pObj->pFanio = (Nwk_Obj_t **)Aig_MmFlexEntryFetch( pObj->pMan->pMemObjs, 2 * pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) );
+    memmove( pObj->pFanio, pFanioOld, pObj->nFanioAlloc * sizeof(Nwk_Obj_t *) );
+    pObj->nFanioAlloc *= 2;
+    pObj->pMan->nRealloced++;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
+{
+    int i;
+    assert( pObj->pMan == pFanin->pMan );
+    assert( pObj->Id >= 0 && pFanin->Id >= 0 );
+    if ( Nwk_ObjReallocIsNeeded(pObj) )
+        Nwk_ManReallocNode( pObj );
+    if ( Nwk_ObjReallocIsNeeded(pFanin) )
+        Nwk_ManReallocNode( pFanin );
+    for ( i = pObj->nFanins + pObj->nFanouts; i > pObj->nFanins; i-- )
+        pObj->pFanio[i] = pObj->pFanio[i-1];
+    pObj->pFanio[pObj->nFanins++] = pFanin;
+    pFanin->pFanio[pFanin->nFanins + pFanin->nFanouts++] = pObj;
+    pObj->Level = AIG_MAX( pObj->Level, pFanin->Level + Nwk_ObjIsNode(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin )
+{
+    int i, k, Limit;
+    // remove pFanin from the fanin list of pObj
+    Limit = pObj->nFanins + pObj->nFanouts;
+    for ( k = i = 0; i < Limit; i++ )
+        if ( pObj->pFanio[i] != pFanin )
+            pObj->pFanio[k++] = pObj->pFanio[i];
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanin
+    pObj->nFanins--;
+    // remove pObj from the fanout list of pFanin
+    Limit = pFanin->nFanins + pFanin->nFanouts;
+    for ( k = i = pFanin->nFanins; i < Limit; i++ )
+        if ( pFanin->pFanio[i] != pObj )
+            pFanin->pFanio[k++] = pFanin->pFanio[i];
+    assert( i == k + 1 ); // if it fails, likely because of duplicated fanout
+    pFanin->nFanouts--; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces a fanin of the node.]
+
+  Description [The node is pObj. An old fanin of this node (pFaninOld) has to be
+  replaced by a new fanin (pFaninNew). Assumes that the node and the old fanin 
+  are not complemented. The new fanin can be complemented. In this case, the
+  polarity of the new fanin will change, compared to the polarity of the old fanin.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew )
+{
+    int i, k, iFanin, Limit;
+    assert( pFaninOld != pFaninNew );
+    assert( pObj != pFaninOld );
+    assert( pObj != pFaninNew );
+    assert( pObj->pMan == pFaninOld->pMan );
+    assert( pObj->pMan == pFaninNew->pMan );
+    // update the fanin
+    iFanin = Nwk_ObjFindFanin( pObj, pFaninOld );
+    if ( iFanin == -1 )
+    {
+        printf( "Nwk_ObjPatchFanin(); Error! Node %d is not among", pFaninOld->Id );
+        printf( " the fanins of node %d...\n", pObj->Id );
+        return;
+    }
+    pObj->pFanio[iFanin] = pFaninNew;
+    // remove pObj from the fanout list of pFaninOld
+    Limit = pFaninOld->nFanins + pFaninOld->nFanouts;
+    for ( k = i = pFaninOld->nFanins; i < Limit; i++ )
+        if ( pFaninOld->pFanio[i] != pObj )
+            pFaninOld->pFanio[k++] = pFaninOld->pFanio[i];
+    pFaninOld->nFanouts--;
+    // add pObj to the fanout list of pFaninNew
+    if ( Nwk_ObjReallocIsNeeded(pFaninNew) )
+        Nwk_ManReallocNode( pFaninNew );
+    pFaninNew->pFanio[pFaninNew->nFanins + pFaninNew->nFanouts++] = pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers fanout from the old node to the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo )
+{
+    Vec_Ptr_t * vFanouts = pNodeFrom->pMan->vTemp;
+    Nwk_Obj_t * pTemp;
+    int nFanoutsOld, i;
+    assert( !Nwk_ObjIsCo(pNodeFrom) && !Nwk_ObjIsCo(pNodeTo) );
+    assert( pNodeFrom->pMan == pNodeTo->pMan );
+    assert( pNodeFrom != pNodeTo );
+    assert( Nwk_ObjFanoutNum(pNodeFrom) > 0 );
+    // get the fanouts of the old node
+    nFanoutsOld = Nwk_ObjFanoutNum(pNodeTo);
+    Nwk_ObjCollectFanouts( pNodeFrom, vFanouts );
+    // patch the fanin of each of them
+    Vec_PtrForEachEntry( vFanouts, pTemp, i )
+        Nwk_ObjPatchFanin( pTemp, pNodeFrom, pNodeTo );
+    assert( Nwk_ObjFanoutNum(pNodeFrom) == 0 );
+    assert( Nwk_ObjFanoutNum(pNodeTo) == nFanoutsOld + Vec_PtrSize(vFanouts) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the node by a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew )
+{
+    assert( pNodeOld->pMan == pNodeNew->pMan );
+    assert( pNodeOld != pNodeNew );
+    assert( Nwk_ObjFanoutNum(pNodeOld) > 0 );
+    // transfer the fanouts to the old node
+    Nwk_ObjTransferFanout( pNodeOld, pNodeNew );
+    // remove the old node
+    Nwk_ManDeleteNode_rec( pNodeOld );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkMan.c b/src/aig/nwk2/nwkMan.c
new file mode 100644
index 00000000..962cafd4
--- /dev/null
+++ b/src/aig/nwk2/nwkMan.c
@@ -0,0 +1,239 @@
+/**CFile****************************************************************
+
+  FileName    [nwkMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+ 
+  Synopsis    [Network manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Nwk_ManAlloc()
+{
+    Nwk_Man_t * p;
+    p = ALLOC( Nwk_Man_t, 1 );
+    memset( p, 0, sizeof(Nwk_Man_t) );
+    p->vCis = Vec_PtrAlloc( 1000 );
+    p->vCos = Vec_PtrAlloc( 1000 );
+    p->vObjs = Vec_PtrAlloc( 1000 );
+    p->vTemp = Vec_PtrAlloc( 1000 );
+    p->nFanioPlus = 2;
+    p->pMemObjs = Aig_MmFlexStart();
+    p->pManHop = Hop_ManStart();
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManFree( Nwk_Man_t * p )
+{
+//    printf( "The number of realloced nodes = %d.\n", p->nRealloced );
+    if ( p->pName )    free( p->pName );
+    if ( p->pSpec )    free( p->pSpec );
+    if ( p->vCis )     Vec_PtrFree( p->vCis );
+    if ( p->vCos )     Vec_PtrFree( p->vCos );
+    if ( p->vObjs )    Vec_PtrFree( p->vObjs );
+    if ( p->vTemp )    Vec_PtrFree( p->vTemp );
+    if ( p->pManTime ) Tim_ManStop( p->pManTime );
+    if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pManHop )  Hop_ManStop( p->pManHop );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void Nwk_ManPrintLutSizes( Nwk_Man_t * p, If_Lib_t * pLutLib )
+{
+    Nwk_Obj_t * pObj;
+    int i, Counters[256] = {0};
+    Nwk_ManForEachNode( p, pObj, i )
+        Counters[Nwk_ObjFaninNum(pObj)]++;
+    printf( "LUTs by size: " );
+    for ( i = 0; i <= pLutLib->LutMax; i++ )
+        printf( "%d:%d ", i, Counters[i] );
+}
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [If the network is best, saves it in "best.blif" and returns 1.]
+
+  Description [If the networks are incomparable, saves the new network, 
+  returns its parameters in the internal parameter structure, and returns 1.
+  If the new network is not a logic network, quits without saving and returns 0.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManCompareAndSaveBest( Nwk_Man_t * pNtk, void * pNtl )
+{
+    extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName );
+    extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames );
+    static struct ParStruct {
+        char * pName;  // name of the best saved network
+        int    Depth;  // depth of the best saved network
+        int    Flops;  // flops in the best saved network 
+        int    Nodes;  // nodes in the best saved network
+        int    nPis;   // the number of primary inputs
+        int    nPos;   // the number of primary outputs
+    } ParsNew, ParsBest = { 0 };
+    // free storage for the name
+    if ( pNtk == NULL )
+    {
+        FREE( ParsBest.pName );
+        return 0;
+    }
+    // get the parameters
+    ParsNew.Depth = Nwk_ManLevel( pNtk );
+    ParsNew.Flops = Nwk_ManLatchNum( pNtk );
+    ParsNew.Nodes = Nwk_ManNodeNum( pNtk );
+    ParsNew.nPis  = Nwk_ManPiNum( pNtk );
+    ParsNew.nPos  = Nwk_ManPoNum( pNtk );
+    // reset the parameters if the network has the same name
+    if (  ParsBest.pName == NULL ||
+          strcmp(ParsBest.pName, pNtk->pName) ||
+          ParsBest.Depth >  ParsNew.Depth ||
+         (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops >  ParsNew.Flops) ||
+         (ParsBest.Depth == ParsNew.Depth && ParsBest.Flops == ParsNew.Flops && ParsBest.Nodes >  ParsNew.Nodes) )
+    {
+        FREE( ParsBest.pName );
+        ParsBest.pName = Aig_UtilStrsav( pNtk->pName );
+        ParsBest.Depth = ParsNew.Depth; 
+        ParsBest.Flops = ParsNew.Flops; 
+        ParsBest.Nodes = ParsNew.Nodes; 
+        ParsBest.nPis  = ParsNew.nPis; 
+        ParsBest.nPos  = ParsNew.nPos;
+        // write the network
+//        Ioa_WriteBlifLogic( pNtk, pNtl, "best.blif" );
+//        Nwk_ManDumpBlif( pNtk, "best_map.blif", NULL, NULL );
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Nwk_FileNameGeneric( char * FileName )
+{
+    char * pDot, * pRes;
+    pRes = Aig_UtilStrsav( FileName );
+    if ( (pDot = strrchr( pRes, '.' )) )
+        *pDot = 0;
+    return pRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+/*
+void Nwk_ManPrintStats( Nwk_Man_t * pNtk, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl )
+{
+    extern int Ntl_ManLatchNum( void * p );
+    extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, void * pNtl, char * pFileName );
+    if ( fSaveBest )
+        Nwk_ManCompareAndSaveBest( pNtk, pNtl );
+    if ( fDumpResult )
+    {
+        char Buffer[1000] = {0};
+        char * pNameGen = pNtk->pSpec? Nwk_FileNameGeneric( pNtk->pSpec ) : "nameless_";
+        sprintf( Buffer, "%s_dump.blif", pNameGen );
+        Ioa_WriteBlifLogic( pNtk, pNtl, Buffer );
+//        sprintf( Buffer, "%s_dump_map.blif", pNameGen );
+//        Nwk_ManDumpBlif( pNtk, Buffer, NULL, NULL );
+        if ( pNtk->pSpec ) free( pNameGen );
+    }
+
+    pNtk->pLutLib = pLutLib;
+    printf( "%-15s : ",      pNtk->pName );
+    printf( "pi = %5d  ",    Nwk_ManPiNum(pNtk) );
+    printf( "po = %5d  ",    Nwk_ManPoNum(pNtk) );
+    printf( "ci = %5d  ",    Nwk_ManCiNum(pNtk) );
+    printf( "co = %5d  ",    Nwk_ManCoNum(pNtk) );
+    printf( "lat = %5d  ",   Ntl_ManLatchNum(pNtl) );
+    printf( "node = %5d  ",  Nwk_ManNodeNum(pNtk) );
+    printf( "edge = %5d  ",  Nwk_ManGetTotalFanins(pNtk) );
+    printf( "aig = %6d  ",   Nwk_ManGetAigNodeNum(pNtk) );
+    printf( "lev = %3d  ",   Nwk_ManLevel(pNtk) );
+//    printf( "lev2 = %3d  ",  Nwk_ManLevelBackup(pNtk) );
+    printf( "delay = %5.2f   ", Nwk_ManDelayTraceLut(pNtk) );
+    Nwk_ManPrintLutSizes( pNtk, pLutLib );
+    printf( "\n" );
+//    Nwk_ManDelayTracePrint( pNtk, pLutLib );
+    fflush( stdout );
+}
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkMerge.c b/src/aig/nwk2/nwkMerge.c
new file mode 100644
index 00000000..1a5255d3
--- /dev/null
+++ b/src/aig/nwk2/nwkMerge.c
@@ -0,0 +1,993 @@
+/**CFile****************************************************************
+
+  FileName    [nwkMerge.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [LUT merging algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+#include "nwkMerge.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Grf_t * Nwk_ManGraphAlloc( int nVertsMax )
+{
+    Nwk_Grf_t * p;
+    p = ALLOC( Nwk_Grf_t, 1 );
+    memset( p, 0, sizeof(Nwk_Grf_t) );
+    p->nVertsMax = nVertsMax;
+    p->nEdgeHash = Aig_PrimeCudd( 3 * nVertsMax );
+    p->pEdgeHash = CALLOC( Nwk_Edg_t *, p->nEdgeHash );
+    p->pMemEdges = Aig_MmFixedStart( sizeof(Nwk_Edg_t), p->nEdgeHash );
+    p->vPairs    = Vec_IntAlloc( 1000 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphFree( Nwk_Grf_t * p )
+{
+    if ( p->vPairs )    Vec_IntFree( p->vPairs );
+    if ( p->pMemEdges ) Aig_MmFixedStop( p->pMemEdges, 0 );
+    if ( p->pMemVerts ) Aig_MmFlexStop( p->pMemVerts, 0 );
+    FREE( p->pVerts );
+    FREE( p->pEdgeHash );
+    FREE( p->pMapLut2Id );
+    FREE( p->pMapId2Lut );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the graph for solving the problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p )
+{
+    p->nMemBytes1 = 
+        sizeof(Nwk_Grf_t) +
+        sizeof(void *) * p->nEdgeHash + 
+        sizeof(int) * (p->nObjs + p->nVertsMax) +
+        sizeof(Nwk_Edg_t) * p->nEdges;
+    p->nMemBytes2 = 
+        sizeof(Nwk_Vrt_t) * p->nVerts + 
+        sizeof(int) * 2 * p->nEdges;
+    printf( "Memory usage stats:  Preprocessing = %.2f Mb.  Solving = %.2f Mb.\n",
+        1.0 * p->nMemBytes1 / (1<<20), 1.0 * p->nMemBytes2 / (1<<20) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or adds the edge to the graph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 )
+{
+    Nwk_Edg_t * pEntry;
+    unsigned Key;
+    if ( iLut1 == iLut2 )
+        return;
+    if ( iLut1 > iLut2 )
+    {
+        Key = iLut1;
+        iLut1 = iLut2;
+        iLut2 = Key;
+    }
+    assert( iLut1 < iLut2 );
+    if ( p->nObjs < iLut2 )
+        p->nObjs = iLut2;
+    Key = (unsigned)(741457 * iLut1 + 4256249 * iLut2) % p->nEdgeHash;
+    for ( pEntry = p->pEdgeHash[Key]; pEntry; pEntry = pEntry->pNext )
+        if ( pEntry->iNode1 == iLut1 && pEntry->iNode2 == iLut2 )
+            return;
+    pEntry = (Nwk_Edg_t *)Aig_MmFixedEntryFetch( p->pMemEdges );
+    pEntry->iNode1 = iLut1;
+    pEntry->iNode2 = iLut2;
+    pEntry->pNext = p->pEdgeHash[Key];
+    p->pEdgeHash[Key] = pEntry;
+    p->nEdges++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one entry to the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphListAdd( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex )
+{
+    if ( *pList )
+    {
+        Nwk_Vrt_t * pHead;
+        pHead = p->pVerts[*pList];
+        pVertex->iPrev = 0;
+        pVertex->iNext = pHead->Id;
+        pHead->iPrev = pVertex->Id;
+    }
+    *pList = pVertex->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes one entry from the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphListDelete( Nwk_Grf_t * p, int * pList, Nwk_Vrt_t * pVertex )
+{
+    assert( *pList );
+    if ( pVertex->iPrev )
+    {
+//        assert( p->pVerts[pVertex->iPrev]->iNext == pVertex->Id );
+        p->pVerts[pVertex->iPrev]->iNext = pVertex->iNext;
+    }
+    if ( pVertex->iNext )
+    {
+//        assert( p->pVerts[pVertex->iNext]->iPrev == pVertex->Id );
+        p->pVerts[pVertex->iNext]->iPrev = pVertex->iPrev;
+    }
+    if ( *pList == pVertex->Id )
+        *pList = pVertex->iNext;
+    pVertex->iPrev = pVertex->iNext = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the edge into one of the linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphListInsert( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex )
+{
+    Nwk_Vrt_t * pNext;
+    assert( pVertex->nEdges > 0 );
+
+    if ( pVertex->nEdges == 1 )
+    {
+        pNext = p->pVerts[ pVertex->pEdges[0] ];
+        if ( pNext->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListAdd( p, p->pLists1 + NWK_MAX_LIST, pVertex );
+        else
+            Nwk_ManGraphListAdd( p, p->pLists1 + pNext->nEdges, pVertex );
+    }
+    else
+    {
+        if ( pVertex->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListAdd( p, p->pLists2 + NWK_MAX_LIST, pVertex );
+        else
+            Nwk_ManGraphListAdd( p, p->pLists2 + pVertex->nEdges, pVertex );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts the edge from one of the linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphListExtract( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex )
+{
+    Nwk_Vrt_t * pNext;
+    assert( pVertex->nEdges > 0 );
+
+    if ( pVertex->nEdges == 1 )
+    {
+        pNext = p->pVerts[ pVertex->pEdges[0] ];
+        if ( pNext->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListDelete( p, p->pLists1 + NWK_MAX_LIST, pVertex );
+        else
+            Nwk_ManGraphListDelete( p, p->pLists1 + pNext->nEdges, pVertex );
+    }
+    else
+    {
+        if ( pVertex->nEdges >= NWK_MAX_LIST )
+            Nwk_ManGraphListDelete( p, p->pLists2 + NWK_MAX_LIST, pVertex );
+        else
+            Nwk_ManGraphListDelete( p, p->pLists2 + pVertex->nEdges, pVertex );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the graph for solving the problem.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphPrepare( Nwk_Grf_t * p )
+{
+    Nwk_Edg_t * pEntry;
+    Nwk_Vrt_t * pVertex;
+    int * pnEdges, nBytes, i;
+    // allocate memory for the present objects
+    p->pMapLut2Id = ALLOC( int, p->nObjs+1 );
+    p->pMapId2Lut = ALLOC( int, p->nVertsMax+1 );
+    memset( p->pMapLut2Id, 0xff, sizeof(int) * (p->nObjs+1) );
+    memset( p->pMapId2Lut, 0xff, sizeof(int) * (p->nVertsMax+1) );
+    // mark present objects
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        assert( pEntry->iNode1 <= p->nObjs );
+        assert( pEntry->iNode2 <= p->nObjs );
+        p->pMapLut2Id[ pEntry->iNode1 ] = 0;
+        p->pMapLut2Id[ pEntry->iNode2 ] = 0;
+    }
+    // map objects
+    p->nVerts = 0;
+    for ( i = 0; i <= p->nObjs; i++ )
+    {
+        if ( p->pMapLut2Id[i] == 0 )
+        {
+            p->pMapLut2Id[i] = ++p->nVerts;
+            p->pMapId2Lut[p->nVerts] = i;
+        }
+    }
+    // count the edges and mark present objects
+    pnEdges = CALLOC( int, p->nVerts+1 );
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        // translate into vertices
+        assert( pEntry->iNode1 <= p->nObjs );
+        assert( pEntry->iNode2 <= p->nObjs );
+        pEntry->iNode1 = p->pMapLut2Id[pEntry->iNode1];
+        pEntry->iNode2 = p->pMapLut2Id[pEntry->iNode2];
+        // count the edges
+        assert( pEntry->iNode1 <= p->nVerts );
+        assert( pEntry->iNode2 <= p->nVerts );
+        pnEdges[pEntry->iNode1]++;
+        pnEdges[pEntry->iNode2]++;
+    }
+    // allocate the real graph
+    p->pMemVerts  = Aig_MmFlexStart();
+    p->pVerts = ALLOC( Nwk_Vrt_t *, p->nVerts + 1 );
+    p->pVerts[0] = NULL;
+    for ( i = 1; i <= p->nVerts; i++ )
+    {
+        assert( pnEdges[i] > 0 );
+        nBytes = sizeof(Nwk_Vrt_t) + sizeof(int) * pnEdges[i];
+        p->pVerts[i] = (Nwk_Vrt_t *)Aig_MmFlexEntryFetch( p->pMemVerts, nBytes );
+        memset( p->pVerts[i], 0, nBytes );
+        p->pVerts[i]->Id = i;
+    }
+    // add edges to the real graph
+    Nwk_GraphForEachEdge( p, pEntry, i )
+    {
+        pVertex = p->pVerts[pEntry->iNode1];
+        pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode2;
+        pVertex = p->pVerts[pEntry->iNode2];
+        pVertex->pEdges[ pVertex->nEdges++ ] = pEntry->iNode1;
+    }
+    // put vertices into the data structure
+    for ( i = 1; i <= p->nVerts; i++ )
+    {
+        assert( p->pVerts[i]->nEdges == pnEdges[i] );
+        Nwk_ManGraphListInsert( p, p->pVerts[i] );
+    }
+    // clean up
+    Aig_MmFixedStop( p->pMemEdges, 0 ); p->pMemEdges = NULL;
+    FREE( p->pEdgeHash );
+//    p->nEdgeHash = 0;
+    free( pnEdges );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the problem after pulling out one edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphCheckLists( Nwk_Grf_t * p )
+{
+    Nwk_Vrt_t * pVertex, * pNext;
+    int i, j;
+    assert( p->pLists1[0] == 0 );
+    for ( i = 1; i <= NWK_MAX_LIST; i++ )
+        if ( p->pLists1[i] )
+        {
+            pVertex = p->pVerts[ p->pLists1[i] ];
+            assert( pVertex->nEdges == 1 );
+            pNext = p->pVerts[ pVertex->pEdges[0] ];
+            assert( pNext->nEdges == i || pNext->nEdges > NWK_MAX_LIST );
+        }
+    // find the next vertext to extract
+    assert( p->pLists2[0] == 0 );
+    assert( p->pLists2[1] == 0 );
+    for ( j = 2; j <= NWK_MAX_LIST; j++ )
+        if ( p->pLists2[j] )
+        {
+            pVertex = p->pVerts[ p->pLists2[j] ];
+            assert( pVertex->nEdges == j || pVertex->nEdges > NWK_MAX_LIST );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts the edge from one of the linked lists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Nwk_ManGraphVertexRemoveEdge( Nwk_Vrt_t * pThis, Nwk_Vrt_t * pNext )
+{
+    int k;
+    for ( k = 0; k < pThis->nEdges; k++ )
+        if ( pThis->pEdges[k] == pNext->Id )
+            break;
+    assert( k < pThis->nEdges );
+    pThis->nEdges--;
+    for ( ; k < pThis->nEdges; k++ )
+        pThis->pEdges[k] = pThis->pEdges[k+1];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the problem after pulling out one edge.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphUpdate( Nwk_Grf_t * p, Nwk_Vrt_t * pVertex, Nwk_Vrt_t * pNext )
+{
+    Nwk_Vrt_t * pChanged, * pOther;
+    int i, k;
+//    Nwk_ManGraphCheckLists( p );
+    Nwk_ManGraphListExtract( p, pVertex );
+    Nwk_ManGraphListExtract( p, pNext );
+    // update neihbors of pVertex
+    Nwk_VertexForEachAdjacent( p, pVertex, pChanged, i )
+    {
+        if ( pChanged == pNext )
+            continue;
+        Nwk_ManGraphListExtract( p, pChanged );
+        // move those that use this one
+        if ( pChanged->nEdges > 1 )
+        Nwk_VertexForEachAdjacent( p, pChanged, pOther, k )
+        {
+            if ( pOther == pVertex || pOther->nEdges > 1 )
+                continue;
+            assert( pOther->nEdges == 1 );
+            Nwk_ManGraphListExtract( p, pOther );
+            pChanged->nEdges--;
+            Nwk_ManGraphListInsert( p, pOther );
+            pChanged->nEdges++;
+        }
+        // remove the edge
+        Nwk_ManGraphVertexRemoveEdge( pChanged, pVertex );
+        // add the changed vertex back
+        if ( pChanged->nEdges > 0 )
+            Nwk_ManGraphListInsert( p, pChanged );
+    }
+    // update neihbors of pNext
+    Nwk_VertexForEachAdjacent( p, pNext, pChanged, i )
+    {
+        if ( pChanged == pVertex )
+            continue;
+        Nwk_ManGraphListExtract( p, pChanged );
+        // move those that use this one
+        if ( pChanged->nEdges > 1 )
+        Nwk_VertexForEachAdjacent( p, pChanged, pOther, k )
+        {
+            if ( pOther == pNext || pOther->nEdges > 1 )
+                continue;
+            assert( pOther->nEdges == 1 );
+            Nwk_ManGraphListExtract( p, pOther );
+            pChanged->nEdges--;
+            Nwk_ManGraphListInsert( p, pOther );
+            pChanged->nEdges++;
+        }
+        // remove the edge
+        Nwk_ManGraphVertexRemoveEdge( pChanged, pNext );
+        // add the changed vertex back
+        if ( pChanged->nEdges > 0 )
+            Nwk_ManGraphListInsert( p, pChanged );
+    }
+    // add to the result
+    if ( pVertex->Id < pNext->Id )
+    {
+        Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); 
+        Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); 
+    }
+    else
+    {
+        Vec_IntPush( p->vPairs, p->pMapId2Lut[pNext->Id] ); 
+        Vec_IntPush( p->vPairs, p->pMapId2Lut[pVertex->Id] ); 
+    }
+//    Nwk_ManGraphCheckLists( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of entries in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGraphListLength( Nwk_Grf_t * p, int List )
+{
+    Nwk_Vrt_t * pThis;
+    int fVerbose = 0;
+    int Counter = 0;
+    Nwk_ListForEachVertex( p, List, pThis )
+    {
+        if ( fVerbose && Counter < 20 )
+            printf( "%d ", p->pVerts[pThis->pEdges[0]]->nEdges );
+        Counter++;
+    }
+    if ( fVerbose )
+        printf( "\n" );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the adjacent vertex with the mininum number of edges.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Vrt_t * Nwk_ManGraphListFindMinEdge( Nwk_Grf_t * p, Nwk_Vrt_t * pVert )
+{
+    Nwk_Vrt_t * pThis, * pMinCost = NULL;
+    int k;
+    Nwk_VertexForEachAdjacent( p, pVert, pThis, k )
+    {
+        if ( pMinCost == NULL || pMinCost->nEdges > pThis->nEdges )
+            pMinCost = pThis;
+    }
+    return pMinCost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the best vertext in the list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Vrt_t * Nwk_ManGraphListFindMin( Nwk_Grf_t * p, int List )
+{
+    Nwk_Vrt_t * pThis, * pMinCost = NULL;
+    int k, Counter = 10000, BestCost = 1000000;
+    Nwk_ListForEachVertex( p, List, pThis )
+    {
+        for ( k = 0; k < pThis->nEdges; k++ )
+        {
+            if ( pMinCost == NULL || BestCost > p->pVerts[pThis->pEdges[k]]->nEdges )
+            {
+                BestCost = p->pVerts[pThis->pEdges[k]]->nEdges;
+                pMinCost = pThis;
+            }
+        }
+        if ( --Counter == 0 )
+            break;
+    }
+    return pMinCost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the problem by extracting one edge at a time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManGraphSolve( Nwk_Grf_t * p )
+{
+    Nwk_Vrt_t * pVertex, * pNext;
+    int i, j;
+    Nwk_ManGraphPrepare( p );
+    while ( 1 )
+    {
+        // find the next vertex to extract
+        assert( p->pLists1[0] == 0 );
+        for ( i = 1; i <= NWK_MAX_LIST; i++ )
+            if ( p->pLists1[i] )
+            {
+//                printf( "%d ", i );
+//                printf( "ListA = %2d. Length = %5d.\n", i, Nwk_ManGraphListLength(p,p->pLists1[i]) );
+                pVertex = p->pVerts[ p->pLists1[i] ];
+                assert( pVertex->nEdges == 1 );
+                pNext = p->pVerts[ pVertex->pEdges[0] ];
+                Nwk_ManGraphUpdate( p, pVertex, pNext );
+                break;
+            }
+        if ( i < NWK_MAX_LIST + 1 )
+            continue;
+        // find the next vertex to extract
+        assert( p->pLists2[0] == 0 );
+        assert( p->pLists2[1] == 0 );
+        for ( j = 2; j <= NWK_MAX_LIST; j++ )
+            if ( p->pLists2[j] )
+            {
+//                printf( "***%d ", j );
+//                printf( "ListB = %2d. Length = %5d.\n", j, Nwk_ManGraphListLength(p,p->pLists2[j]) );
+                pVertex = Nwk_ManGraphListFindMin( p, p->pLists2[j] ); 
+                assert( pVertex->nEdges == j || j == NWK_MAX_LIST );
+                pNext = Nwk_ManGraphListFindMinEdge( p, pVertex );
+                Nwk_ManGraphUpdate( p, pVertex, pNext );
+                break;
+            }
+        if ( j == NWK_MAX_LIST + 1 )
+            break;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads graph from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Grf_t * Nwk_ManLutMergeReadGraph( char * pFileName )
+{
+    Nwk_Grf_t * p;
+    FILE * pFile;
+    char Buffer[100];
+    int nNodes, nEdges, iNode1, iNode2;
+    pFile = fopen( pFileName, "r" );
+    fscanf( pFile, "%s %d", Buffer, &nNodes );
+    fscanf( pFile, "%s %d", Buffer, &nEdges );
+    p = Nwk_ManGraphAlloc( nNodes );
+    while ( fscanf( pFile, "%s %d %d", Buffer, &iNode1, &iNode2 ) == 3 )
+        Nwk_ManGraphHashEdge( p, iNode1, iNode2 );
+    assert( p->nEdges == nEdges );
+    fclose( pFile );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the graph coming from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManLutMergeGraphTest( char * pFileName )
+{
+    int nPairs;
+    Nwk_Grf_t * p;
+    int clk = clock();
+    p = Nwk_ManLutMergeReadGraph( pFileName );
+    PRT( "Reading", clock() - clk );
+    clk = clock();
+    Nwk_ManGraphSolve( p );
+    printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
+        p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+    PRT( "Solving", clock() - clk );
+    nPairs = Vec_IntSize(p->vPairs)/2;
+    Nwk_ManGraphReportMemoryUsage( p );
+    Nwk_ManGraphFree( p );
+    return nPairs;
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanins of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkFanins_rec( Nwk_Obj_t * pLut, int nLevMin )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( !Nwk_ObjIsNode(pLut) )
+        return;
+    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pLut );
+    if ( Nwk_ObjLevel(pLut) < nLevMin )
+        return;
+    Nwk_ObjForEachFanin( pLut, pNext, i )
+        Nwk_ManMarkFanins_rec( pNext, nLevMin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanouts of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMarkFanouts_rec( Nwk_Obj_t * pLut, int nLevMax, int nFanMax )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    if ( !Nwk_ObjIsNode(pLut) )
+        return;
+    if ( Nwk_ObjIsTravIdCurrent( pLut ) )
+        return;
+    Nwk_ObjSetTravIdCurrent( pLut );
+    if ( Nwk_ObjLevel(pLut) > nLevMax )
+        return;
+    if ( Nwk_ObjFanoutNum(pLut) > nFanMax )
+        return;
+    Nwk_ObjForEachFanout( pLut, pNext, i )
+        Nwk_ManMarkFanouts_rec( pNext, nLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes around the given set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax )
+{
+    Nwk_Obj_t * pObj, * pNext;
+    int i, k;
+    Vec_PtrClear( vNext );
+    Vec_PtrForEachEntry( vStart, pObj, i )
+    {
+        Nwk_ObjForEachFanin( pObj, pNext, k )
+        {
+            if ( !Nwk_ObjIsNode(pNext) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pNext );
+            Vec_PtrPush( vNext, pNext );
+        }
+        Nwk_ObjForEachFanout( pObj, pNext, k )
+        {
+            if ( !Nwk_ObjIsNode(pNext) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pNext ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pNext );
+            if ( Nwk_ObjFanoutNum(pNext) > nFanMax )
+                continue;
+            Vec_PtrPush( vNext, pNext );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes removes from the given one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCollectNonOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Vec_Ptr_t * vTemp;
+    Nwk_Obj_t * pObj;
+    int i, k;
+    Vec_PtrClear( vCands );
+    if ( pPars->nMaxSuppSize - Nwk_ObjFaninNum(pLut) <= 1 )
+        return;
+
+    // collect nodes removed by this distance
+    assert( pPars->nMaxDistance > 0 );
+    Vec_PtrClear( vStart );
+    Vec_PtrPush( vStart, pLut );
+    Nwk_ManIncrementTravId( pLut->pMan );
+    Nwk_ObjSetTravIdCurrent( pLut );
+    for ( i = 1; i <= pPars->nMaxDistance; i++ )
+    {
+        Nwk_ManCollectCircle( vStart, vNext, pPars->nMaxFanout );
+        vTemp  = vStart;
+        vStart = vNext;
+        vNext  = vTemp;
+        // collect the nodes in vStart
+        Vec_PtrForEachEntry( vStart, pObj, k )
+            Vec_PtrPush( vCands, pObj );
+    }
+
+    // mark the TFI/TFO nodes
+    Nwk_ManIncrementTravId( pLut->pMan );
+    if ( pPars->fUseTfiTfo )
+        Nwk_ObjSetTravIdCurrent( pLut );
+    else
+    {
+        Nwk_ObjSetTravIdPrevious( pLut );
+        Nwk_ManMarkFanins_rec( pLut, Nwk_ObjLevel(pLut) - pPars->nMaxDistance );
+        Nwk_ObjSetTravIdPrevious( pLut );
+        Nwk_ManMarkFanouts_rec( pLut, Nwk_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout );
+    }
+
+    // collect nodes satisfying the following conditions:
+    // - they are close enough in terms of distance
+    // - they are not in the TFI/TFO of the LUT
+    // - they have no more than the given number of fanins
+    // - they have no more than the given diff in delay
+    k = 0;
+    Vec_PtrForEachEntry( vCands, pObj, i )
+    {
+        if ( Nwk_ObjIsTravIdCurrent(pObj) )
+            continue;
+        if ( Nwk_ObjFaninNum(pLut) + Nwk_ObjFaninNum(pObj) > pPars->nMaxSuppSize )
+            continue;
+        if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+             Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+             continue;
+        Vec_PtrWriteEntry( vCands, k++, pObj );
+    }
+    Vec_PtrShrink( vCands, k );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count the total number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManCountTotalFanins( Nwk_Obj_t * pLut, Nwk_Obj_t * pCand )
+{
+    Nwk_Obj_t * pFanin;
+    int i, nCounter = Nwk_ObjFaninNum(pLut);
+    Nwk_ObjForEachFanin( pCand, pFanin, i )
+        nCounter += !pFanin->MarkC;
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects overlapping candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwl_ManCollectOverlapCands( Nwk_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Nwk_Obj_t * pFanin, * pObj;
+    int i, k;
+    // mark fanins of pLut
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->MarkC = 1;
+    // collect the matching fanouts of each fanin of the node
+    Vec_PtrClear( vCands );
+    Nwk_ManIncrementTravId( pLut->pMan );
+    Nwk_ObjSetTravIdCurrent( pLut );
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+    {
+        if ( !Nwk_ObjIsNode(pFanin) )
+            continue;
+        if ( Nwk_ObjFanoutNum(pFanin) > pPars->nMaxFanout )
+            continue;
+        Nwk_ObjForEachFanout( pFanin, pObj, k )
+        {
+            if ( !Nwk_ObjIsNode(pObj) )
+                continue;
+            if ( Nwk_ObjIsTravIdCurrent( pObj ) )
+                continue;
+            Nwk_ObjSetTravIdCurrent( pObj );
+            // check the difference in delay
+            if ( Nwk_ObjLevel(pLut) - Nwk_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+                 Nwk_ObjLevel(pObj) - Nwk_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+                 continue;
+            // check the total number of fanins of the node
+            if ( Nwk_ManCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize )
+                continue;
+            Vec_PtrPush( vCands, pObj );
+        }
+    }
+    // unmark fanins of pLut
+    Nwk_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->MarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs LUT merging with parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Nwk_ManLutMerge( Nwk_Man_t * pNtk, Nwk_LMPars_t * pPars )
+{
+    Nwk_Grf_t * p;
+    Vec_Int_t * vResult;
+    Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
+    Nwk_Obj_t * pLut, * pCand;
+    int i, k, nVertsMax, nCands, clk = clock();
+    // count the number of vertices
+    nVertsMax = 0;
+    Nwk_ManForEachNode( pNtk, pLut, i )
+        nVertsMax += (int)(Nwk_ObjFaninNum(pLut) <= pPars->nMaxLutSize);
+    p = Nwk_ManGraphAlloc( nVertsMax );
+    // create graph
+    vStart  = Vec_PtrAlloc( 1000 );
+    vNext   = Vec_PtrAlloc( 1000 );
+    vCands1 = Vec_PtrAlloc( 1000 );
+    vCands2 = Vec_PtrAlloc( 1000 );
+    nCands  = 0;
+    Nwk_ManForEachNode( pNtk, pLut, i )
+    {
+        if ( Nwk_ObjFaninNum(pLut) > pPars->nMaxLutSize )
+            continue;
+        Nwl_ManCollectOverlapCands( pLut, vCands1, pPars );
+        if ( pPars->fUseDiffSupp )
+            Nwk_ManCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars );
+        if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 )
+            continue;
+        nCands += Vec_PtrSize(vCands1) + Vec_PtrSize(vCands2);
+        // save candidates
+        Vec_PtrForEachEntry( vCands1, pCand, k )
+            Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) );
+        Vec_PtrForEachEntry( vCands2, pCand, k )
+            Nwk_ManGraphHashEdge( p, Nwk_ObjId(pLut), Nwk_ObjId(pCand) );
+        // print statistics about this node
+        if ( pPars->fVeryVerbose )
+        printf( "Node %6d : Fanins = %d. Fanouts = %3d.  Cand1 = %3d. Cand2 = %3d.\n",
+            Nwk_ObjId(pLut), Nwk_ObjFaninNum(pLut), Nwk_ObjFaninNum(pLut), 
+            Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) );
+    }
+    Vec_PtrFree( vStart );
+    Vec_PtrFree( vNext );
+    Vec_PtrFree( vCands1 );
+    Vec_PtrFree( vCands2 );
+    if ( pPars->fVerbose )
+    {
+        printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
+        PRT( "Deriving graph", clock() - clk );
+    }
+    // solve the graph problem
+    clk = clock();
+    Nwk_ManGraphSolve( p );
+    if ( pPars->fVerbose )
+    {
+        printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
+            p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+        PRT( "Solving", clock() - clk );
+        Nwk_ManGraphReportMemoryUsage( p );
+    }
+    vResult = p->vPairs; p->vPairs = NULL;
+    Nwk_ManGraphFree( p );
+    return vResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkMerge.h b/src/aig/nwk2/nwkMerge.h
new file mode 100644
index 00000000..df426681
--- /dev/null
+++ b/src/aig/nwk2/nwkMerge.h
@@ -0,0 +1,149 @@
+/**CFile****************************************************************
+
+  FileName    [nwkMerge.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkMerge.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NWK_MERGE_H__
+#define __NWK_MERGE_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define NWK_MAX_LIST  16
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// the LUT merging parameters
+typedef struct Nwk_LMPars_t_  Nwk_LMPars_t;
+struct Nwk_LMPars_t_
+{
+    int    nMaxLutSize;    // the max LUT size for merging (N=5)
+    int    nMaxSuppSize;   // the max total support size after merging (S=5)
+    int    nMaxDistance;   // the max number of nodes separating LUTs
+    int    nMaxLevelDiff;  // the max difference in levels
+    int    nMaxFanout;     // the max number of fanouts to traverse
+    int    fUseDiffSupp;   // enables the use of nodes with different support
+    int    fUseTfiTfo;     // enables the use of TFO/TFO nodes as candidates
+    int    fVeryVerbose;   // enables additional verbose output
+    int    fVerbose;       // enables verbose output
+};
+
+// edge of the graph
+typedef struct Nwk_Edg_t_  Nwk_Edg_t;
+struct Nwk_Edg_t_
+{
+    int             iNode1;      // the first node
+    int             iNode2;      // the second node
+    Nwk_Edg_t *     pNext;       // the next edge
+};
+
+// vertex of the graph
+typedef struct Nwk_Vrt_t_  Nwk_Vrt_t;
+struct Nwk_Vrt_t_
+{
+    int             Id;          // the vertex number
+    int             iPrev;       // the previous vertex in the list
+    int             iNext;       // the next vertex in the list
+    int             nEdges;      // the number of edges
+    int             pEdges[0];   // the array of edges
+};
+
+// the connectivity graph
+typedef struct Nwk_Grf_t_  Nwk_Grf_t;
+struct Nwk_Grf_t_
+{
+    // preliminary graph representation
+    int             nObjs;       // the number of objects
+    int             nVertsMax;   // the upper bound on the number of vertices
+    int             nEdgeHash;   // an approximate number of edges
+    Nwk_Edg_t **    pEdgeHash;   // hash table for edges
+    Aig_MmFixed_t * pMemEdges;   // memory for edges
+    // graph representation
+    int             nEdges;      // the number of edges
+    int             nVerts;      // the number of vertices
+    Nwk_Vrt_t **    pVerts;      // the array of vertices
+    Aig_MmFlex_t *  pMemVerts;   // memory for vertices
+    // intermediate data
+    int pLists1[NWK_MAX_LIST+1]; // lists of nodes with one edge
+    int pLists2[NWK_MAX_LIST+1]; // lists of nodes with more than one edge
+    // the results of matching
+    Vec_Int_t *     vPairs;      // pairs matched in the graph
+    // object mappings
+    int *           pMapLut2Id;  // LUT numbers into vertex IDs
+    int *           pMapId2Lut;  // vertex IDs into LUT numbers
+    // other things
+    int             nMemBytes1;  // memory usage in bytes
+    int             nMemBytes2;  // memory usage in bytes
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Nwk_GraphForEachEdge( p, pEdge, k )             \
+    for ( k = 0; k < p->nEdgeHash; k++ )                \
+        for ( pEdge = p->pEdgeHash[k]; pEdge; pEdge = pEdge->pNext )
+
+#define Nwk_ListForEachVertex( p, List, pVrt )          \
+    for ( pVrt = List? p->pVerts[List] : NULL;  pVrt;   \
+          pVrt = pVrt->iNext? p->pVerts[pVrt->iNext] : NULL )
+
+#define Nwk_VertexForEachAdjacent( p, pVrt, pNext, k )  \
+    for ( k = 0; (k < pVrt->nEdges) && (((pNext) = p->pVerts[pVrt->pEdges[k]]), 1); k++ )
+
+////////////////////////////////////////////////////////////////////////
+///                      INLINED FUNCTIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         ITERATORS                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== nwkMerge.c ==========================================================*/
+extern Nwk_Grf_t *   Nwk_ManGraphAlloc( int nVertsMax );
+extern void          Nwk_ManGraphFree( Nwk_Grf_t * p );
+extern void          Nwk_ManGraphReportMemoryUsage( Nwk_Grf_t * p );
+extern void          Nwk_ManGraphHashEdge( Nwk_Grf_t * p, int iLut1, int iLut2 );
+extern void          Nwk_ManGraphSolve( Nwk_Grf_t * p );
+extern int           Nwk_ManLutMergeGraphTest( char * pFileName );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/nwk2/nwkObj.c b/src/aig/nwk2/nwkObj.c
new file mode 100644
index 00000000..58587f07
--- /dev/null
+++ b/src/aig/nwk2/nwkObj.c
@@ -0,0 +1,199 @@
+/**CFile****************************************************************
+
+  FileName    [nwkObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [Manipulation of objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkObj.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates an object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Nwk_ManCreateObj( Nwk_Man_t * p, int nFanins, int nFanouts )
+{
+    Nwk_Obj_t * pObj;
+    pObj = (Nwk_Obj_t *)Aig_MmFlexEntryFetch( p->pMemObjs, sizeof(Nwk_Obj_t) + (nFanins + nFanouts + p->nFanioPlus) * sizeof(Nwk_Obj_t *) );
+    memset( pObj, 0, sizeof(Nwk_Obj_t) );
+    pObj->pFanio = (Nwk_Obj_t **)((char *)pObj + sizeof(Nwk_Obj_t));
+    pObj->Id = Vec_PtrSize( p->vObjs );
+    Vec_PtrPush( p->vObjs, pObj );
+    pObj->pMan        = p;
+    pObj->nFanioAlloc = nFanins + nFanouts + p->nFanioPlus;
+    return pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Nwk_ManCreateCi( Nwk_Man_t * p, int nFanouts )
+{
+    Nwk_Obj_t * pObj;
+    pObj = Nwk_ManCreateObj( p, 1, nFanouts );
+    pObj->PioId = Vec_PtrSize( p->vCis );
+    Vec_PtrPush( p->vCis, pObj );
+    pObj->Type = NWK_OBJ_CI;
+    p->nObjs[NWK_OBJ_CI]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Nwk_ManCreateCo( Nwk_Man_t * p )
+{
+    Nwk_Obj_t * pObj;
+    pObj = Nwk_ManCreateObj( p, 1, 1 );
+    pObj->PioId = Vec_PtrSize( p->vCos );
+    Vec_PtrPush( p->vCos, pObj );
+    pObj->Type = NWK_OBJ_CO;
+    p->nObjs[NWK_OBJ_CO]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * p )
+{
+    Nwk_Obj_t * pObj;
+    pObj = Nwk_ManCreateObj( p, 1, 1 );
+    pObj->Type = NWK_OBJ_LATCH;
+    p->nObjs[NWK_OBJ_LATCH]++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Obj_t * Nwk_ManCreateNode( Nwk_Man_t * p, int nFanins, int nFanouts )
+{
+    Nwk_Obj_t * pObj;
+    pObj = Nwk_ManCreateObj( p, nFanins, nFanouts );
+    pObj->Type = NWK_OBJ_NODE;
+    p->nObjs[NWK_OBJ_NODE]++;
+    return pObj;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDeleteNode( Nwk_Obj_t * pObj )
+{
+    Vec_Ptr_t * vNodes = pObj->pMan->vTemp;
+    Nwk_Obj_t * pTemp;
+    int i;
+    assert( Nwk_ObjFanoutNum(pObj) == 0 );
+    // delete fanins
+    Nwk_ObjCollectFanins( pObj, vNodes );
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+        Nwk_ObjDeleteFanin( pObj, pTemp );
+    // remove from the list of objects
+    Vec_PtrWriteEntry( pObj->pMan->vObjs, pObj->Id, NULL );
+    pObj->pMan->nObjs[pObj->Type]--;
+    memset( pObj, 0, sizeof(Nwk_Obj_t) );
+    pObj->Id = -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node and MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Nwk_ObjIsCi(pObj) );
+    assert( Nwk_ObjFanoutNum(pObj) == 0 );
+    vNodes = Vec_PtrAlloc( 100 );
+    Nwk_ObjCollectFanins( pObj, vNodes );
+    Nwk_ManDeleteNode( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Nwk_ObjIsNode(pObj) && Nwk_ObjFanoutNum(pObj) == 0 )
+            Nwk_ManDeleteNode_rec( pObj );
+    Vec_PtrFree( vNodes );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwkUtil.c b/src/aig/nwk2/nwkUtil.c
new file mode 100644
index 00000000..d6daca4e
--- /dev/null
+++ b/src/aig/nwk2/nwkUtil.c
@@ -0,0 +1,515 @@
+/**CFile****************************************************************
+
+  FileName    [nwkUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Logic network representation.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwkUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+#include "kit.h"
+#include <math.h>
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    if ( pNtk->nTravIds >= (1<<26)-1 )
+    {
+        pNtk->nTravIds = 0;
+        Nwk_ManForEachObj( pNtk, pObj, i )
+            pObj->TravId = 0;
+    }
+    pNtk->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the maximum number of fanins of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nFaninsMax = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( nFaninsMax < Nwk_ObjFaninNum(pNode) )
+            nFaninsMax = Nwk_ObjFaninNum(pNode);
+    }
+    return nFaninsMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the total number of all fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nFanins = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+        nFanins += Nwk_ObjFaninNum(pNode);
+    return nFanins;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of true PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPiNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, Counter = 0;
+    Nwk_ManForEachCi( pNtk, pNode, i )
+        Counter += Nwk_ObjIsPi( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of true POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManPoNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, Counter = 0;
+    Nwk_ManForEachCo( pNtk, pNode, i )
+        Counter += Nwk_ObjIsPo( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk )
+{
+    Nwk_Obj_t * pNode;
+    int i, nNodes = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        if ( pNode->pFunc == NULL )
+        {
+            printf( "Nwk_ManGetAigNodeNum(): Local AIG of node %d is not assigned.\n", pNode->Id );
+            continue;
+        }
+        if ( Nwk_ObjFaninNum(pNode) < 2 )
+            continue;
+        nNodes += Hop_DagSize( pNode->pFunc );
+    }
+    return nNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+    int Diff = (*pp1)->Level - (*pp2)->Level;
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
+{
+    int Diff = (*pp1)->Level - (*pp2)->Level;
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ObjPrint( Nwk_Obj_t * pObj )
+{
+    Nwk_Obj_t * pNext;
+    int i;
+    printf( "ObjId = %5d.  ", pObj->Id );
+    if ( Nwk_ObjIsPi(pObj) )
+        printf( "PI" );
+    if ( Nwk_ObjIsPo(pObj) )
+        printf( "PO" );
+    if ( Nwk_ObjIsNode(pObj) )
+        printf( "Node" );
+    printf( "   Fanins = " );
+    Nwk_ObjForEachFanin( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "   Fanouts = " );
+    Nwk_ObjForEachFanout( pObj, pNext, i )
+        printf( "%d ", pNext->Id );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dumps the BLIF file for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Nwk_Obj_t * pObj, * pFanin;
+    Aig_MmFlex_t * pMem;
+    char * pSop = NULL;
+    unsigned * pTruth;
+    int i, k, nDigits;
+    if ( Nwk_ManPoNum(pNtk) == 0 )
+    {
+        printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" );
+        return;
+    }
+    // collect nodes in the DFS order
+    nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) );
+    // write the file 
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" );
+//    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+    fprintf( pFile, ".model %s\n", pNtk->pName );
+    // write PIs
+    fprintf( pFile, ".inputs" );
+    Nwk_ManForEachCi( pNtk, pObj, i )
+        if ( vPiNames )
+            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write POs
+    fprintf( pFile, ".outputs" );
+    Nwk_ManForEachCo( pNtk, pObj, i )
+        if ( vPoNames )
+            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPoNames, i) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+    fprintf( pFile, "\n" );
+    // write nodes
+    pMem = Aig_MmFlexStart();
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    vCover = Vec_IntAlloc( 1 << 16 );
+    vNodes = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
+        // derive SOP for the AIG
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        if ( Hop_IsComplement(pObj->pFunc) )
+            Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+        pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        // write the node
+        fprintf( pFile, ".names" );
+        if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+                if ( vPiNames && Nwk_ObjIsPi(pFanin) )
+                    fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) );
+                else
+                    fprintf( pFile, " n%0*d", nDigits, pFanin->Id );
+        }
+        fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        // write the function
+        fprintf( pFile, "%s", pSop );
+    }
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    Vec_PtrFree( vNodes );
+    Aig_MmFlexStop( pMem, 0 );
+    // write POs
+    Nwk_ManForEachCo( pNtk, pObj, i )
+    {
+        fprintf( pFile, ".names" );
+        if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) )
+            fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) );
+        else
+            fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id );
+        if ( vPoNames )
+            fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) );
+        else
+            fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+        fprintf( pFile, "%d 1\n", !pObj->fInvert );
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the distribution of fanins/fanouts in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
+{
+    char Buffer[100];
+    Nwk_Obj_t * pNode;
+    Vec_Int_t * vFanins, * vFanouts;
+    int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
+    int i, k, nSizeMax;
+
+    // determine the largest fanin and fanout
+    nFaninsMax = nFanoutsMax = 0;
+    nFaninsAll = nFanoutsAll = 0;
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+        nFaninsAll  += nFanins;
+        nFanoutsAll += nFanouts;
+        nFaninsMax   = AIG_MAX( nFaninsMax, nFanins );
+        nFanoutsMax  = AIG_MAX( nFanoutsMax, nFanouts );
+    }
+
+    // allocate storage for fanin/fanout numbers
+    nSizeMax = AIG_MAX( 10 * (Aig_Base10Log(nFaninsMax) + 1), 10 * (Aig_Base10Log(nFanoutsMax) + 1) );
+    vFanins  = Vec_IntStart( nSizeMax );
+    vFanouts = Vec_IntStart( nSizeMax );
+
+    // count the number of fanins and fanouts
+    Nwk_ManForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Nwk_ObjFaninNum(pNode);
+        nFanouts = Nwk_ObjFanoutNum(pNode);
+//        nFanouts = Nwk_NodeMffcSize(pNode);
+
+        if ( nFanins < 10 )
+            Vec_IntAddToEntry( vFanins, nFanins, 1 );
+        else if ( nFanins < 100 )
+            Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
+        else if ( nFanins < 1000 )
+            Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
+        else if ( nFanins < 10000 )
+            Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
+        else if ( nFanins < 100000 )
+            Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
+        else if ( nFanins < 1000000 )
+            Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
+        else if ( nFanins < 10000000 )
+            Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
+
+        if ( nFanouts < 10 )
+            Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
+        else if ( nFanouts < 100 )
+            Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
+        else if ( nFanouts < 1000 )
+            Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
+        else if ( nFanouts < 10000 )
+            Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
+        else if ( nFanouts < 100000 )
+            Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
+        else if ( nFanouts < 1000000 )
+            Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
+        else if ( nFanouts < 10000000 )
+            Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
+    }
+
+    printf( "The distribution of fanins and fanouts in the network:\n" );
+    printf( "         Number   Nodes with fanin  Nodes with fanout\n" );
+    for ( k = 0; k < nSizeMax; k++ )
+    {
+        if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+            continue;
+        if ( k < 10 )
+            printf( "%15d : ", k );
+        else
+        {
+            sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); 
+            printf( "%15s : ", Buffer );
+        }
+        if ( vFanins->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanins->pArray[k] );
+        printf( "    " );
+        if ( vFanouts->pArray[k] == 0 )
+            printf( "              " );
+        else
+            printf( "%12d  ", vFanouts->pArray[k] );
+        printf( "\n" );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vFanouts );
+
+    printf( "Fanins: Max = %d. Ave = %.2f.  Fanouts: Max = %d. Ave =  %.2f.\n", 
+        nFaninsMax,  1.0*nFaninsAll/Nwk_ManNodeNum(pNtk), 
+        nFanoutsMax, 1.0*nFanoutsAll/Nwk_ManNodeNum(pNtk)  );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the temporary marks of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
+{
+    Nwk_Obj_t * pObj;
+    int i;
+    Nwk_ManForEachObj( pMan, pObj, i )
+        pObj->MarkA = pObj->MarkB = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
+{
+    unsigned * pTruth;
+    Vec_Int_t * vTruth;
+    Nwk_Obj_t * pObj, * pFanin, * pObjNew;
+    int uSupp, nSuppSize, i, k, Counter = 0;
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj));
+        if ( nSuppSize == Nwk_ObjFaninNum(pObj) )
+            continue;
+        Counter++;
+        uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) );
+        // create new node with the given support
+        pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) );
+        Nwk_ObjForEachFanin( pObj, pFanin, k )
+            if ( uSupp & (1 << k) )
+                Nwk_ObjAddFanin( pObjNew, pFanin );
+        pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) );
+        if ( fVerbose )
+            printf( "Reducing node %d fanins from %d to %d.\n", 
+                pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) );
+        Nwk_ObjReplace( pObj, pObjNew );
+    }
+    if ( fVerbose && Counter )
+        printf( "Support minimization reduced support of %d nodes.\n", Counter );
+    Vec_IntFree( vTruth );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/nwk2/nwk_.c b/src/aig/nwk2/nwk_.c
new file mode 100644
index 00000000..81cffbbf
--- /dev/null
+++ b/src/aig/nwk2/nwk_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [nwk_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: nwk_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "nwk.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f3bd028a..08275ff3 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -85,7 +85,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index ae8d02ec..527f372d 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -336,6 +336,68 @@ sat_solver * Saig_DeriveSatSolver(
 
 /**Function*************************************************************
 
+  Synopsis    [Checks constainment of two interpolants.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
+{
+    Aig_Man_t * pMiter, * pAigTemp;
+    int RetValue;
+    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
+//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
+//    Aig_ManStop( pAigTemp );
+    RetValue = Fra_FraigMiterStatus( pMiter );
+    if ( RetValue == -1 )
+    {
+        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
+        RetValue = Fra_FraigMiterStatus( pAigTemp );
+        Aig_ManStop( pAigTemp );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+    }
+    assert( RetValue != -1 );
+    Aig_ManStop( pMiter );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks constainment of two interpolants.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
+{
+    Aig_Man_t * pMiter, * pAigTemp;
+    int RetValue;
+    pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
+//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
+//    Aig_ManStop( pAigTemp );
+    RetValue = Fra_FraigMiterStatus( pMiter );
+    if ( RetValue == -1 )
+    {
+        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
+        RetValue = Fra_FraigMiterStatus( pAigTemp );
+        Aig_ManStop( pAigTemp );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+    }
+    assert( RetValue != -1 );
+    Aig_ManStop( pMiter );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs one SAT run with interpolation.]
 
   Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
@@ -345,11 +407,12 @@ sat_solver * Saig_DeriveSatSolver(
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_PerformOneStep( Saig_IntMan_t * p )
+int Saig_PerformOneStep_old( Saig_IntMan_t * p, int fUseIp )
 {
     sat_solver * pSat;
     void * pSatCnf = NULL;
-    Inta_Man_t * pManInter; 
+    Inta_Man_t * pManInterA; 
+    Intb_Man_t * pManInterB; 
     int clk, status, RetValue;
     assert( p->pInterNew == NULL );
 
@@ -380,9 +443,18 @@ p->timeSat += clock() - clk;
 
     // create the resulting manager
 clk = clock();
-    pManInter = Inta_ManAlloc();
-    p->pInterNew = Inta_ManInterpolate( pManInter, pSatCnf, p->vVarsAB, 0 );
-    Inta_ManFree( pManInter );
+    if ( !fUseIp )
+    {
+        pManInterA = Inta_ManAlloc();
+        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+        Inta_ManFree( pManInterA );
+    }
+    else
+    {
+        pManInterB = Intb_ManAlloc();
+        p->pInterNew = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
+        Intb_ManFree( pManInterB );
+    }
 p->timeInt += clock() - clk;
     Sto_ManFree( pSatCnf );
     return RetValue;
@@ -390,7 +462,7 @@ p->timeInt += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Checks constainment of two interpolants.]
+  Synopsis    []
 
   Description []
                
@@ -399,23 +471,192 @@ p->timeInt += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
+Aig_Man_t * Aig_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
 {
-    Aig_Man_t * pMiter, * pAigTemp;
-    int RetValue;
-    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
-//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
-//    Aig_ManStop( pAigTemp );
-    RetValue = Fra_FraigMiterStatus( pMiter );
-    if ( RetValue == -1 )
+    Aig_Man_t * pInterC;
+    assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
+    pInterC = Aig_ManDupSimple( pInter );
+    Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
+    assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
+    return pInterC;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_VerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
+{
+    extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
+    Aig_Man_t * pLower, * pUpper, * pInterC;
+    int RetValue1, RetValue2;
+
+    pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
+    pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
+    Aig_ManFlipFirstPo( pUpper );
+
+    pInterC = Aig_ManDupExpand( pInter, pLower );
+    RetValue1 = Saig_ManCheckContainment( pLower, pInterC );
+    Aig_ManStop( pInterC );
+
+    pInterC = Aig_ManDupExpand( pInter, pUpper );
+    RetValue2 = Saig_ManCheckContainment( pInterC, pUpper );
+    Aig_ManStop( pInterC );
+    
+    if ( RetValue1 && RetValue2 )
+        printf( "Im is correct.\n" );
+    if ( !RetValue1 )
+        printf( "Property A => Im fails.\n" );
+    if ( !RetValue2 )
+        printf( "Property Im => !B fails.\n" );
+
+    Aig_ManStop( pLower );
+    Aig_ManStop( pUpper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_VerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
+{
+    extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
+    Aig_Man_t * pLower, * pUpper, * pInterC;
+    int RetValue1, RetValue2;
+
+    pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
+    pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
+    Aig_ManFlipFirstPo( pUpper );
+
+    pInterC = Aig_ManDupExpand( pInter, pLower );
+//Aig_ManPrintStats( pLower );
+//Aig_ManPrintStats( pUpper );
+//Aig_ManPrintStats( pInterC );
+//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
+    RetValue1 = Saig_ManCheckContainment( pLower, pInterC );
+    Aig_ManStop( pInterC );
+
+    pInterC = Aig_ManDupExpand( pInter, pUpper );
+    RetValue2 = Saig_ManCheckContainment( pInterC, pUpper );
+    Aig_ManStop( pInterC );
+    
+    if ( RetValue1 && RetValue2 )
+        printf( "Ip is correct.\n" );
+    if ( !RetValue1 )
+        printf( "Property A => Ip fails.\n" );
+    if ( !RetValue2 )
+        printf( "Property Ip => !B fails.\n" );
+
+    Aig_ManStop( pLower );
+    Aig_ManStop( pUpper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_PerformOneStep( Saig_IntMan_t * p, int fUseIp )
+{
+    sat_solver * pSat;
+    void * pSatCnf = NULL;
+    Inta_Man_t * pManInterA; 
+    Intb_Man_t * pManInterB; 
+    int clk, status, RetValue;
+    assert( p->pInterNew == NULL );
+
+    // derive the SAT solver
+    pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB );
+//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 );
+    // solve the problem
+clk = clock();
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    p->nConfCur = pSat->stats.conflicts;
+p->timeSat += clock() - clk;
+    if ( status == l_False )
     {
-        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
-        RetValue = Fra_FraigMiterStatus( pAigTemp );
-        Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+        pSatCnf = sat_solver_store_release( pSat );
+        RetValue = 1;
     }
-    assert( RetValue != -1 );
-    Aig_ManStop( pMiter );
+    else if ( status == l_True )
+    {
+        RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+    }
+    sat_solver_delete( pSat );
+    if ( pSatCnf == NULL )
+        return RetValue;
+
+    // create the resulting manager
+clk = clock();
+    if ( !fUseIp )
+    {
+        pManInterA = Inta_ManAlloc();
+        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+        Inta_ManFree( pManInterA );
+    }
+    else
+    {
+        Aig_Man_t * pInterNew2;
+        int RetValue;
+
+        pManInterA = Inta_ManAlloc();
+        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+//        Saig_VerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
+        Inta_ManFree( pManInterA );
+
+        pManInterB = Intb_ManAlloc();
+        pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
+        Saig_VerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
+        Intb_ManFree( pManInterB );
+
+        // check relationship
+        RetValue = Saig_ManCheckEquivalence( pInterNew2, p->pInterNew );
+        if ( RetValue )
+            printf( "Equivalence \"Ip == Im\" holds\n" );
+        else
+        {
+//            printf( "Equivalence \"Ip == Im\" does not hold\n" );
+            RetValue = Saig_ManCheckContainment( pInterNew2, p->pInterNew );
+            if ( RetValue )
+                printf( "Containment \"Ip -> Im\" holds\n" );
+            else
+                printf( "Containment \"Ip -> Im\" does not hold\n" );
+
+            RetValue = Saig_ManCheckContainment( p->pInterNew, pInterNew2 );
+            if ( RetValue )
+                printf( "Containment \"Im -> Ip\" holds\n" );
+            else
+                printf( "Containment \"Im -> Ip\" does not hold\n" );
+        }
+
+        Aig_ManStop( pInterNew2 );
+    }
+p->timeInt += clock() - clk;
+    Sto_ManFree( pSatCnf );
     return RetValue;
 }
 
@@ -497,7 +738,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth )
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUseIp, int fVerbose, int * pDepth )
 {
     Saig_IntMan_t * p;
     Aig_Man_t * pAigTemp;
@@ -578,7 +819,7 @@ p->timeCnf += clock() - clk;
             }
             // perform interplation
             clk = clock();
-            RetValue = Saig_PerformOneStep( p );
+            RetValue = Saig_PerformOneStep( p, fUseIp );
             if ( fVerbose )
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ",