Version abc50829

54 files changed, 441 insertions, 417 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index f8871ba9..7c949ee0 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -445,7 +445,7 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Printing factored forms can be done for SOP networks.\n" );
         return 1;
@@ -465,15 +465,11 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
             return 1;
         }
-//        Ft_FactorStartMan();
         Abc_NodePrintFactor( pOut, pNode );
-//        Ft_FactorStopMan();
         return 0;
     }
     // print the nodes
-//    Ft_FactorStartMan();
     Abc_NtkPrintFactor( pOut, pNtk );
-//    Ft_FactorStopMan();
     return 0;
 
 usage:
@@ -508,7 +504,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fProfile = 0;
+    fProfile = 1;
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
     {
@@ -530,7 +526,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !fProfile && !Abc_NtkIsAig(pNtk) )
+    if ( !fProfile && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
@@ -607,7 +603,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command works only for AIGs.\n" );
         return 1;
@@ -664,7 +660,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
         fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
         return 1;
@@ -738,14 +734,14 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Can only collapse a logic network.\n" );
         return 1;
     }
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
     else
     {
@@ -880,7 +876,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         pNtkRes = Abc_NtkBalance( pNtk, fDuplicate );
     }
@@ -992,7 +988,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cannot renode a network that is not an AIG.\n" );
         return 1;
@@ -1065,7 +1061,7 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
         return 1;
@@ -1276,7 +1272,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fGlobal )
     {
         // get the new network
-        if ( !Abc_NtkIsAig(pNtk) )
+        if ( !Abc_NtkIsStrash(pNtk) )
         {
             pNtkNew = Abc_NtkStrash( pNtk, 0 );
             pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
@@ -1305,7 +1301,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else if ( fRecursive )
     {
-        if ( !Abc_NtkIsLogicBdd( pNtk ) )
+        if ( !Abc_NtkIsBddLogic( pNtk ) )
         {
             fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
             return 1;
@@ -1390,7 +1386,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
@@ -1499,7 +1495,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
@@ -1734,7 +1730,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkStrash( pNtk, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
@@ -1802,7 +1798,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
         fprintf( pErr, "Converting to SOP is possible when node functions are BDDs.\n" );
         return 1;
@@ -1862,7 +1858,7 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" );
         return 1;
@@ -1930,16 +1926,15 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
         return 0;
     }
-    if ( !(Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsLogicBdd(pNtk)) )
+    if ( !Abc_NtkIsLogic(pNtk) )
     {
-        fprintf( stdout, "First convert node representation into BDDs or SOPs.\n" );
+        fprintf( stdout, "This command can only be applied to logic network.\n" );
         return 0;
     }
-    if ( Abc_NtkIsLogicSop(pNtk) )
-    {
-//        printf( "Converting node functions from SOP to BDD.\n" );
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+        Abc_NtkUnmap(pNtk);
+    if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkSopToBdd(pNtk);
-    }
 
     if ( Abc_NtkMiterSat( pNtk, fVerbose ) )
         printf( "The miter is satisfiable.\n" );
@@ -2006,7 +2001,7 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "The current network has no latches.\n" );
         return 0;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "This command works only for AIGs.\n" );
         return 0;
@@ -2085,7 +2080,7 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Currently can only be applied to the logic network or an AIG.\n" );
         return 1;
@@ -2280,7 +2275,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cut computation is available only for AIGs.\n" );
         return 1;
@@ -2415,9 +2410,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Can only fraig a logic network.\n" );
+        fprintf( pErr, "Can only fraig a logic network or an AIG.\n" );
         return 1;
     }
 
@@ -2425,7 +2420,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerboseP = pParams->fTryProve;
 
     // get the new network
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
@@ -2750,7 +2745,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Cannot sweep AIGs (use \"fraig\").\n" );
         return 1;
@@ -2848,7 +2843,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
@@ -2948,7 +2943,7 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    if ( !Abc_NtkIsLogicMap(pNtk) )
+    if ( !Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pErr, "Cannot unmap the network that is not mapped.\n" );
         return 1;
@@ -3010,7 +3005,7 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Can only attach gates if the nodes have SOP representations.\n" );
         return 1;
@@ -3073,7 +3068,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Works only for the AIG representation.\n" );
         return 1;
@@ -3148,7 +3143,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
         pNtk = Abc_NtkStrash( pNtk, 0 );
@@ -3241,7 +3236,10 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    printf( "This command is not yet implemented.\n" );
+    return 0;
+
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Works only for AIG.\n" );
         return 1;
@@ -3317,6 +3315,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    printf( "This command is not yet implemented.\n" );
+    return 0;
+
+
     if ( !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pErr, "Works only for sequential AIG.\n" );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 2366aa10..a3f7ddb7 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -43,36 +43,46 @@
 
 // network types
 typedef enum { 
-    ABC_NTK_NONE,          // 0:  unknown
-    ABC_NTK_NETLIST_SOP,   // 1:  netlist with nodes represented using SOPs
-    ABC_NTK_NETLIST_MAP,   // 2:  netlist with nodes represented using gates from the library
-    ABC_NTK_LOGIC_SOP,     // 3:  only SOP logic nodes (similar to SIS network)
-    ABC_NTK_LOGIC_BDD,     // 4:  only BDD logic nodes (similar to BDS network)
-    ABC_NTK_LOGIC_MAP,     // 5:  only mapped logic nodes (similar to mapped SIS network)
-    ABC_NTK_AIG,           // 6:  AIG or FRAIG (two input gates with c-attributes on edges)
-    ABC_NTK_SEQ,           // 7:  sequential AIG (two input gates with c- and latch-attributes on edges)
-    ABC_NTK_OTHER          // 8:  unused
+    ABC_TYPE_NONE,      // 0:  unknown
+    ABC_TYPE_NETLIST,   // 1:  network with PIs/POs, latches, nodes, and nets
+    ABC_TYPE_LOGIC,     // 2:  network with PIs/POs, latches, and nodes
+    ABC_TYPE_STRASH,    // 3:  structurally hashed AIG (two input AND gates with c-attributes on edges)
+    ABC_TYPE_SEQ,       // 4:  sequential AIG (two input AND gates with c- and latch-attributes on edges)
+    ABC_TYPE_OTHER      // 5:  unused
 } Abc_NtkType_t;
 
 // functionality types
 typedef enum { 
-    ABC_FUNC_NONE,         // 0:  unknown
-    ABC_FUNC_SOP,          // 1:  sum-of-products
-    ABC_FUNC_BDD,          // 2:  binary decision diagrams
-    ABC_FUNC_AIG,          // 3:  and-inverter graphs
-    ABC_FUNC_MAP,          // 4:  standard cell library
-    ABC_FUNC_OTHER         // 5:  unused
-} Abc_FuncType_t;
+    ABC_FUNC_NONE,      // 0:  unknown
+    ABC_FUNC_SOP,       // 1:  sum-of-products
+    ABC_FUNC_BDD,       // 2:  binary decision diagrams
+    ABC_FUNC_AIG,       // 3:  and-inverter graphs
+    ABC_FUNC_MAP,       // 4:  standard cell library
+    ABC_FUNC_OTHER      // 5:  unused
+} Abc_NtkFunc_t;
+
+// Supported type/functionality combinations:
+/*------------------------------------------|
+|           |  SOP  |  BDD  |  AIG  |  Map  |
+|-----------|-------|-------|-------|-------|
+|  Netlist  |   x   |       |       |   x   |
+|-----------|-------|-------|-------|-------|
+|  Logic    |   x   |   x   |       |   x   |
+|-----------|-------|-------|-------|-------|
+|  Strash   |       |       |   x   |       |
+|-----------|-------|-------|-------|-------|
+|  Seq      |       |       |   x   |       | 
+--------------------------------------------|*/
 
 // object types
 typedef enum { 
-    ABC_OBJ_NONE,          // 0:  unknown
-    ABC_OBJ_NET,           // 1:  net
-    ABC_OBJ_NODE,          // 2:  node
-    ABC_OBJ_LATCH,         // 3:  latch
-    ABC_OBJ_PI,            // 4:  primary input terminal
-    ABC_OBJ_PO,            // 5:  primary output terminal
-    ABC_OBJ_OTHER          // 6:  unused
+    ABC_OBJ_NONE,       // 0:  unknown
+    ABC_OBJ_NET,        // 1:  net
+    ABC_OBJ_NODE,       // 2:  node
+    ABC_OBJ_LATCH,      // 3:  latch
+    ABC_OBJ_PI,         // 4:  primary input terminal
+    ABC_OBJ_PO,         // 5:  primary output terminal
+    ABC_OBJ_OTHER       // 6:  unused
 } Abc_ObjType_t;
 
 ////////////////////////////////////////////////////////////////////////
@@ -124,7 +134,8 @@ struct Abc_Obj_t_ // 12 words
 struct Abc_Ntk_t_ 
 {
     // general information 
-    Abc_NtkType_t    Type;          // type of the network
+    Abc_NtkType_t    ntkType;       // type of the network
+    Abc_NtkFunc_t    ntkFunc;       // functionality of the network
     char *           pName;         // the network name
     char *           pSpec;         // the name of the spec file if present
     // name representation 
@@ -177,13 +188,31 @@ struct Abc_Ntk_t_
 #define ABC_MAX(a,b)      (((a) > (b))? (a) : (b))
 #define ABC_INFINITY      (10000000)
 
+// checking the network type
+static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pNtk->ntkType == ABC_TYPE_NETLIST; }
+static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )         { return pNtk->ntkType == ABC_TYPE_LOGIC;   }
+static inline bool        Abc_NtkIsStrash( Abc_Ntk_t * pNtk )        { return pNtk->ntkType == ABC_TYPE_STRASH;  }
+static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )           { return pNtk->ntkType == ABC_TYPE_SEQ;     }
+
+static inline bool        Abc_NtkHasSop( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_SOP;    }
+static inline bool        Abc_NtkHasBdd( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_BDD;    }
+static inline bool        Abc_NtkHasAig( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_AIG;    }
+static inline bool        Abc_NtkHasMapping( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_MAP;    }
+
+static inline bool        Abc_NtkIsSopNetlist( Abc_Ntk_t * pNtk )    { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_TYPE_NETLIST;  }
+static inline bool        Abc_NtkIsMappedNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_TYPE_NETLIST;  }
+static inline bool        Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk )   { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_TYPE_LOGIC  ;  }
+static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return pNtk->nLatches == 0;      }
+
 // reading data members of the network
-static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )         { return pNtk->pName;           }
-static inline char *      Abc_NtkSpec( Abc_Ntk_t * pNtk )         { return pNtk->pSpec;           }
-static inline int         Abc_NtkTravId( Abc_Ntk_t * pNtk )       { return pNtk->nTravIds;        }    
-static inline Abc_Ntk_t * Abc_NtkExdc( Abc_Ntk_t * pNtk )         { return pNtk->pExdc;           }
-static inline Abc_Ntk_t * Abc_NtkBackup( Abc_Ntk_t * pNtk )       { return pNtk->pNetBackup;      }
-static inline int         Abc_NtkStep  ( Abc_Ntk_t * pNtk )       { return pNtk->iStep;           }
+static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )            { return pNtk->pName;           }
+static inline char *      Abc_NtkSpec( Abc_Ntk_t * pNtk )            { return pNtk->pSpec;           }
+static inline int         Abc_NtkTravId( Abc_Ntk_t * pNtk )          { return pNtk->nTravIds;        }    
+static inline Abc_Ntk_t * Abc_NtkExdc( Abc_Ntk_t * pNtk )            { return pNtk->pExdc;           }
+static inline Abc_Ntk_t * Abc_NtkBackup( Abc_Ntk_t * pNtk )          { return pNtk->pNetBackup;      }
+static inline int         Abc_NtkStep  ( Abc_Ntk_t * pNtk )          { return pNtk->iStep;           }
 
 // setting data members of the network
 static inline void        Abc_NtkSetName  ( Abc_Ntk_t * pNtk, char * pName )           { pNtk->pName      = pName;      } 
@@ -192,98 +221,83 @@ static inline void        Abc_NtkSetBackup( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNetBa
 static inline void        Abc_NtkSetStep  ( Abc_Ntk_t * pNtk, int iStep )              { pNtk->iStep      = iStep;      }
 
 // getting the number of objects 
-static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )    { return pNtk->vObjs->nSize;         }
-static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )       { return pNtk->nObjs;                }
-static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )       { return pNtk->nNets;                }
-static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )      { return pNtk->nNodes;               }
-static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )     { return pNtk->nLatches;             }
-static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )        { return pNtk->nPis;                 }
-static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )        { return pNtk->nPos;                 }
-static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )        { return pNtk->vCis->nSize;          }
-static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )        { return pNtk->vCos->nSize;          }
+static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )       { return pNtk->vObjs->nSize;         }
+static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjs;                }
+static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nNets;                }
+static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nNodes;               }
+static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return pNtk->nLatches;             }
+static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )           { return pNtk->nPis;                 }
+static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )           { return pNtk->nPos;                 }
+static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return pNtk->vCis->nSize;          }
+static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return pNtk->vCos->nSize;          }
 
 // reading objects
-static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )   { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i];  }
-static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
-static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )    { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
-
-// checking the network type
-static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )    { return pNtk->Type == ABC_NTK_NETLIST_SOP || pNtk->Type == ABC_NTK_NETLIST_MAP;   }
-static inline bool        Abc_NtkIsNetlistSop( Abc_Ntk_t * pNtk ) { return pNtk->Type == ABC_NTK_NETLIST_SOP;   }
-static inline bool        Abc_NtkIsNetlistMap( Abc_Ntk_t * pNtk ) { return pNtk->Type == ABC_NTK_NETLIST_MAP;   }
-static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )      { return pNtk->Type == ABC_NTK_LOGIC_SOP || pNtk->Type == ABC_NTK_LOGIC_BDD || pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsLogicSop( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_SOP; }
-static inline bool        Abc_NtkIsLogicBdd( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_BDD; }
-static inline bool        Abc_NtkIsLogicMap( Abc_Ntk_t * pNtk )   { return pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsAig( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_AIG;       }
-static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_SEQ;       }
-static inline bool        Abc_NtkIsMapped( Abc_Ntk_t * pNtk )     { return pNtk->Type == ABC_NTK_NETLIST_MAP || pNtk->Type == ABC_NTK_LOGIC_MAP; }
-static inline bool        Abc_NtkIsSop( Abc_Ntk_t * pNtk )        { return pNtk->Type == ABC_NTK_NETLIST_SOP || pNtk->Type == ABC_NTK_LOGIC_SOP; }
-static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )       { return Abc_NtkLatchNum(pNtk) == 0;      }
-
+static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { assert( i < Vec_PtrSize(pNtk->vObjs) ); return pNtk->vObjs->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { assert( i < Vec_PtrSize(pNtk->vLats) ); return pNtk->vLats->pArray[i];  }
+static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCiNum(pNtk) ); return pNtk->vCis->pArray[i];      }
+static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkCoNum(pNtk) ); return pNtk->vCos->pArray[i];      }
 
 // reading data members of the object
-static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )         { return pObj->Type;               }
-static inline unsigned    Abc_ObjId( Abc_Obj_t * pObj )           { return pObj->Id;                 }
-static inline int         Abc_ObjTravId( Abc_Obj_t * pObj )       { return pObj->TravId;             }
-static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )     { return &pObj->vFanins;           }
-static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )    { return &pObj->vFanouts;          }
-static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )         { return pObj->pCopy;              }
-static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )          { return pObj->pNtk;               }
-static inline void *      Abc_ObjData( Abc_Obj_t * pObj )         { return pObj->pData;              }
+static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
+static inline unsigned    Abc_ObjId( Abc_Obj_t * pObj )              { return pObj->Id;                 }
+static inline int         Abc_ObjTravId( Abc_Obj_t * pObj )          { return pObj->TravId;             }
+static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj )        { return &pObj->vFanins;           }
+static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )       { return &pObj->vFanouts;          }
+static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )            { return pObj->pCopy;              }
+static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )             { return pObj->pNtk;               }
+static inline void *      Abc_ObjData( Abc_Obj_t * pObj )            { return pObj->pData;              }
 
 // setting data members of the network
-static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )             { pObj->pCopy    =  pCopy;    } 
-static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )                  { pObj->pData    =  pData;    } 
+static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )  { pObj->pCopy    =  pCopy;    } 
+static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData    =  pData;    } 
 
 // working with complemented attributes of objects
-static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )    { return (bool)(((unsigned)p) & 01);           }
-static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )         { return (Abc_Obj_t *)((unsigned)(p) & ~01);  }
-static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )             { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
-static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )  { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
+static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)(((unsigned)p) & 01);           }
+static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((unsigned)(p) & ~01);  }
+static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
+static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
 
 // checking the object type
-static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )       { return pObj->Type == ABC_OBJ_NODE;   }
-static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_NET;    }
-static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )      { return pObj->Type == ABC_OBJ_LATCH;  }
-static inline bool        Abc_ObjIsPi( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PI;     }
-static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PO;     }
-static inline bool        Abc_ObjIsPio( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO;    }
-static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;   }
+static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;    }
+static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_LATCH;  }
+static inline bool        Abc_ObjIsPi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI;     }
+static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO;     }
+static inline bool        Abc_ObjIsPio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO;    }
+static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
 
 // working with fanin/fanout edges
-static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )     { return pObj->vFanins.nSize;      }
-static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )    { return pObj->vFanouts.nSize;     }
-static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
-static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[0].iFan; }
-static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )     { return pObj->vFanins.pArray[1].iFan; }
-static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )      { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
-static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )       { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )    { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
-static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )   { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
-static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl;                               }
-static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].fCompl;                               }
-static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].fCompl;                               }
+static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )        { return pObj->vFanins.nSize;      }
+static inline int         Abc_ObjFanoutNum( Abc_Obj_t * pObj )       { return pObj->vFanouts.nSize;     }
+static inline int         Abc_ObjFaninId( Abc_Obj_t * pObj, int i)   { return pObj->vFanins.pArray[i].iFan; }
+static inline int         Abc_ObjFaninId0( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[0].iFan; }
+static inline int         Abc_ObjFaninId1( Abc_Obj_t * pObj )        { return pObj->vFanins.pArray[1].iFan; }
+static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i )   { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ];   }
+static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan  ];   }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj;     }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj;    }
+static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].fCompl;                               }
+static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].fCompl;                               }
+static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].fCompl;                               }
 static inline bool        Abc_ObjFanoutC( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjFaninC0(pFanout) : Abc_ObjFaninC1(pFanout);  }
-static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats;                                }
-static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[0].nLats;                                }
-static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )      { return pObj->vFanins.pArray[1].nLats;                                }
-static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
-static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )   {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
-static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
-static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
-static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
-static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )       { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
+static inline int         Abc_ObjFaninL( Abc_Obj_t * pObj, int i )   { return pObj->vFanins.pArray[i].nLats;                                }
+static inline int         Abc_ObjFaninL0( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[0].nLats;                                }
+static inline int         Abc_ObjFaninL1( Abc_Obj_t * pObj )         { return pObj->vFanins.pArray[1].nLats;                                }
+static inline int         Abc_ObjFaninLMin( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline int         Abc_ObjFaninLMax( Abc_Obj_t * pObj )       {  assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
+static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i )    { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj )          { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );}
+static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );  }
+static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj )      { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) );  }
 static inline Abc_Obj_t * Abc_ObjFanoutFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) {  assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjChild0(pFanout) : Abc_ObjChild1(pFanout);  }
 static inline void        Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1;                               }
 static inline void        Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1;                              }
@@ -300,9 +314,9 @@ extern int                Abc_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                Abc_ObjFanoutLMax( Abc_Obj_t * pObj );
 
 // checking the node type
-static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )   { assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2;                         }
-static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk) || Abc_NtkIsSeq(pNode->pNtk)); return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
-static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )    { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode)));                   return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
+static inline bool        Abc_NodeIsAigAnd( Abc_Obj_t * pNode )      { assert(Abc_NtkHasAig(pNode->pNtk));           return Abc_ObjFaninNum(pNode) == 2;                         }
+static inline bool        Abc_NodeIsAigChoice( Abc_Obj_t * pNode )   { assert(Abc_NtkHasAig(pNode->pNtk));           return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
+static inline bool        Abc_NodeIsConst( Abc_Obj_t * pNode )       { assert(Abc_ObjIsNode(Abc_ObjRegular(pNode))); return Abc_ObjFaninNum(Abc_ObjRegular(pNode)) == 0;         }
 extern        bool        Abc_NodeIsConst0( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsConst1( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsBuf( Abc_Obj_t * pNode );    
@@ -398,8 +412,8 @@ extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
 extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
 extern void               Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type );
-extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
+extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 2200bea1..f71c0a15 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -294,7 +294,7 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
             Counter++;
     if ( Counter != Abc_NtkNodeNum(pMan->pNtkAig) )
     {
-        printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n", Counter );
+        printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
     }
     return 1;
@@ -315,7 +315,7 @@ int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, LevelsMax;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // perform the traversal
     LevelsMax = 0;
     Abc_NtkForEachCo( pNtk, pNode, i )
@@ -718,12 +718,21 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         // such node does not exist - modify the old fanout node 
         // (this way the change will not propagate all the way to the COs)
         assert( Abc_ObjRegular(pFanin1) != Abc_ObjRegular(pFanin2) );             
+
+        // if the node is in the level structure, remove it
+        if ( pFanout->fMarkA )
+            Abc_AigRemoveFromLevelStructure( pMan->vLevels, pFanout );
+        // if the node is in the level structure, remove it
+        if ( pFanout->fMarkB )
+            Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pFanout );
+
         // remove the old fanout node from the structural hashing table
         Abc_AigAndDelete( pMan, pFanout );
         // remove the fanins of the old fanout
         Abc_ObjRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+
         // schedule the updated fanout for updating direct level
         assert( pFanout->fMarkA == 0 );
         pFanout->fMarkA = 1;
@@ -732,6 +741,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         assert( pFanout->fMarkB == 0 );
         pFanout->fMarkB = 1;
         Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout );
+
         // the fanout has changed, update EXOR status of its fanouts
         Abc_ObjForEachFanout( pFanout, pFanoutFanout, v )
             if ( Abc_NodeIsAigAnd(pFanoutFanout) )
diff --git a/src/base/abc/abcAttach.c b/src/base/abc/abcAttach.c
index 47e911c9..a8e06555 100644
--- a/src/base/abc/abcAttach.c
+++ b/src/base/abc/abcAttach.c
@@ -64,7 +64,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     Mio_Gate_t ** ppGates;
     int nGates, nFanins, i;
 
-    assert( Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsSopLogic(pNtk) );
 
     // check that the library is available
     pGenlib = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
@@ -142,7 +142,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
     // replace SOP representation by the gate representation
     Abc_NtkForEachNode( pNtk, pNode, i )
         pNode->pData = pNode->pCopy, pNode->pCopy = NULL;
-    pNtk->Type = ABC_NTK_LOGIC_MAP;
+    pNtk->ntkFunc = ABC_FUNC_MAP;
     Extra_MmFlexStop( pNtk->pManFunc, 0 );
     pNtk->pManFunc = pGenlib;
 
diff --git a/src/base/abc/abcBalance.c b/src/base/abc/abcBalance.c
index bcf1032b..7deab3ba 100644
--- a/src/base/abc/abcBalance.c
+++ b/src/base/abc/abcBalance.c
@@ -48,9 +48,9 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // perform balancing
-    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // make sure everything is okay
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index e8b00271..25d1c86c 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -57,12 +57,17 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
-    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
         return 0;
     }
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( !Abc_NtkHasSop(pNtk) && !Abc_NtkHasBdd(pNtk) && !Abc_NtkHasAig(pNtk) && !Abc_NtkHasMapping(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Unknown functionality type.\n" );
+        return 0;
+    }
+    if ( Abc_NtkHasMapping(pNtk) )
     {
         if ( pNtk->pManFunc != Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
         {
@@ -110,9 +115,9 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     }
 
     // check the nodes
-    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
     {
-        if ( Abc_NtkIsAig(pNtk) ) 
+        if ( Abc_NtkIsStrash(pNtk) ) 
             Abc_AigCheck( pNtk->pManFunc );
     }
     else
@@ -474,7 +479,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
         return 0;
     }
     // the netlist and SOP logic network should have SOPs
-    if ( Abc_NtkIsNetlistSop(pNtk) || Abc_NtkIsLogicSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         if ( !Abc_SopCheck( pNode->pData, Abc_ObjFaninNum(pNode) ) )
         {
@@ -482,7 +487,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
             return 0;
         }
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         int nSuppSize = Cudd_SupportSize(pNtk->pManFunc, pNode->pData);
         if ( nSuppSize > Abc_ObjFaninNum(pNode) )
@@ -491,7 +496,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
             return 0;
         }
     }
-    else if ( !Abc_NtkIsMapped(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) )
     {
         assert( 0 );
     }
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index 2b2da719..e07636cc 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -49,7 +49,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     DdManager * dd;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
     dd = Abc_NtkGlobalBdds( pNtk, 0 );    
@@ -230,7 +230,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i;
     // start the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make sure the new manager has the same number of inputs
     Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
     // process the POs
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 7de9ea3e..9186ec5a 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -47,12 +47,13 @@ static void          Abc_ObjAdd( Abc_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtk;
     pNtk = ALLOC( Abc_Ntk_t, 1 );
     memset( pNtk, 0, sizeof(Abc_Ntk_t) );
-    pNtk->Type        = Type;
+    pNtk->ntkType     = Type;
+    pNtk->ntkFunc     = Func;
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
     pNtk->vLats       = Vec_PtrAlloc( 100 );
@@ -71,13 +72,13 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
     // get ready to assign the first Obj ID
     pNtk->nTravIds    = 1;
     // start the functionality manager
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNtk->pManFunc = Extra_MmFlexStart();
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    else if ( Abc_NtkHasAig(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
     else
         assert( 0 );
@@ -95,7 +96,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type )
+Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pObjNew;
@@ -103,7 +104,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type )
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkAlloc( Type );
+    pNtkNew = Abc_NtkAlloc( Type, Func );
     // duplicate the name and the spec
     pNtkNew->pName = util_strsav(pNtk->pName);
     pNtkNew->pSpec = util_strsav(pNtk->pSpec);
@@ -190,7 +191,7 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 {
     Abc_Ntk_t * pNtkNew; 
     // allocate the empty network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     // set the specs
     pNtkNew->pName = util_strsav( pName );
     pNtkNew->pSpec = util_strsav( pName );
@@ -244,9 +245,9 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
     if ( pNtk == NULL )
         return NULL;
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->Type );
+    pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc );
     // copy the internal nodes
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         Abc_AigDup( pNtk->pManFunc, pNtkNew->pManFunc );
     else
     {
@@ -286,11 +287,11 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     char Buffer[1000];
     int i, k;
 
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
     assert( Abc_ObjIsCo(pNode) ); 
     
     // start the network
-    pNtkNew = Abc_NtkAlloc( pNtk->Type );
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
     // set the name
     sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) );
     pNtkNew->pName = util_strsav(Buffer);
@@ -307,14 +308,14 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
         }
     }
     // establish connection between the constant nodes
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
 
     // copy the nodes
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         // if it is an AIG, add to the hash table
-        if ( Abc_NtkIsAig(pNtk) )
+        if ( Abc_NtkIsStrash(pNtk) )
         {
             pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
         }
@@ -359,7 +360,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
     
     // start the network
     Abc_NtkCleanCopy( pNtk );
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     pNtkNew->pName = util_strsav(pNtk->pName);
 
     // collect the nodes in the TFI of the output
@@ -425,7 +426,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     }
 
     // dereference the BDDs
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         Abc_NtkForEachNode( pNtk, pObj, i )
             Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
         
@@ -458,13 +459,13 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->pManTime )
         Abc_ManTimeStop( pNtk->pManTime );
     // start the functionality manager
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         Extra_MmFlexStop( pNtk->pManFunc, 0 );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( pNtk->pManFunc );
-    else if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    else if ( Abc_NtkHasAig(pNtk) )
         Abc_AigFree( pNtk->pManFunc );
-    else if ( !Abc_NtkIsMapped(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) )
         assert( 0 );
     free( pNtk );
 }
@@ -637,17 +638,17 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
     pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
-    if ( Abc_ObjIsNode(pObj) ) // copy the function if network is the same type
+    if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
     {
-        if ( pNtkNew->Type == pObj->pNtk->Type || Abc_NtkIsNetlist(pObj->pNtk) || Abc_NtkIsNetlist(pNtkNew) ) 
+        if ( pNtkNew->ntkFunc == pObj->pNtk->ntkFunc ) 
         {
-            if ( Abc_NtkIsSop(pNtkNew) )
+            if ( Abc_NtkHasSop(pNtkNew) )
                 pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
-            else if ( Abc_NtkIsLogicBdd(pNtkNew) )
+            else if ( Abc_NtkHasBdd(pNtkNew) )
                 pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
-            else if ( Abc_NtkIsMapped(pNtkNew) )
+            else if ( Abc_NtkHasMapping(pNtkNew) )
                 pObjNew->pData = pObj->pData;
-            else if ( !Abc_NtkIsAig(pNtkNew) && !Abc_NtkIsSeq(pNtkNew) )
+            else if ( Abc_NtkHasAig(pNtkNew) )
                 assert( 0 );
         }
     }
@@ -675,8 +676,8 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
-    assert( Abc_NtkIsLogicSop(pNtkNew) );
+    assert( Abc_NtkIsStrash(pNtkAig) );
+    assert( Abc_NtkIsSopLogic(pNtkNew) );
     pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pConst1) > 0 )
         pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
@@ -697,8 +698,8 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
 Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )  
 { 
     Abc_Obj_t * pReset, * pConst1;
-    assert( Abc_NtkIsAig(pNtkAig) || Abc_NtkIsSeq(pNtkAig) );
-    assert( Abc_NtkIsLogicSop(pNtkNew) );
+    assert( Abc_NtkIsStrash(pNtkAig) );
+    assert( Abc_NtkIsSopLogic(pNtkNew) );
     pReset = Abc_AigReset(pNtkAig->pManFunc);
     if ( Abc_ObjFanoutNum(pReset) > 0 )
     {
@@ -998,12 +999,13 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
+    assert( !Abc_NtkHasAig(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 0\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero(pNtk->pManFunc), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst0(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1024,14 +1026,14 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
-    if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return Abc_AigConst1(pNtk->pManFunc);
     pNode = Abc_NtkCreateNode( pNtk );   
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne(pNtk->pManFunc), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadConst1(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1055,11 +1057,11 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     Abc_ObjAddFanin( pNode, pFanin );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "0 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar(pNtk->pManFunc,0)), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadInv(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1083,11 +1085,11 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     Abc_ObjAddFanin( pNode, pFanin );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "1 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar(pNtk->pManFunc,0), Cudd_Ref( pNode->pData );
-    else if ( Abc_NtkIsMapped(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
         pNode->pData = Mio_LibraryReadBuf(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()));
     else
         assert( 0 );
@@ -1113,7 +1115,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     pNode = Abc_NtkCreateNode( pNtk );   
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, vFanins->pArray[i] );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         char * pSop;
         pSop = Extra_MmFlexEntryFetch( pNtk->pManFunc, vFanins->nSize + 4 );
@@ -1126,7 +1128,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         assert( i == vFanins->nSize + 4 );
         pNode->pData = pSop;
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         DdManager * dd = pNtk->pManFunc;
         DdNode * bFunc, * bTemp;
@@ -1162,7 +1164,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     pNode = Abc_NtkCreateNode( pNtk );   
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, vFanins->pArray[i] );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
     {
         char * pSop;
         pSop = Extra_MmFlexEntryFetch( pNtk->pManFunc, vFanins->nSize + 4 );
@@ -1175,7 +1177,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
         assert( i == vFanins->nSize + 4 );
         pNode->pData = pSop;
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
     {
         DdManager * dd = pNtk->pManFunc;
         DdNode * bFunc, * bTemp;
@@ -1211,9 +1213,9 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     Abc_ObjAddFanin( pNode, pNodeC );
     Abc_ObjAddFanin( pNode, pNode1 );
     Abc_ObjAddFanin( pNode, pNode0 );
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "11- 1\n0-1 1\n" );
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIte(pNtk->pManFunc,Cudd_bddIthVar(pNtk->pManFunc,0),Cudd_bddIthVar(pNtk->pManFunc,1),Cudd_bddIthVar(pNtk->pManFunc,2)), Cudd_Ref( pNode->pData );
     else
         assert( 0 );
@@ -1260,13 +1262,13 @@ bool Abc_NodeIsConst0( Abc_Obj_t * pNode )
     Abc_Ntk_t * pNtk = pNode->pNtk;
     assert(Abc_ObjIsNode(pNode));      
     assert(Abc_NodeIsConst(pNode));
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst0(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return Abc_ObjNot(pNode) == Abc_AigConst1(pNode->pNtk->pManFunc);
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadConst0(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1288,13 +1290,13 @@ bool Abc_NodeIsConst1( Abc_Obj_t * pNode )
     Abc_Ntk_t * pNtk = pNode->pNtk;
     assert(Abc_ObjIsNode(pNode));      
     assert(Abc_NodeIsConst(pNode));
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsConst1(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return pNode == Abc_AigConst1(pNode->pNtk->pManFunc);
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadConst1(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1317,13 +1319,13 @@ bool Abc_NodeIsBuf( Abc_Obj_t * pNode )
     assert(Abc_ObjIsNode(pNode)); 
     if ( Abc_ObjFaninNum(pNode) != 1 )
         return 0;
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsBuf(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return !Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return 0;
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadBuf(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
@@ -1346,13 +1348,13 @@ bool Abc_NodeIsInv( Abc_Obj_t * pNode )
     assert(Abc_ObjIsNode(pNode)); 
     if ( Abc_ObjFaninNum(pNode) != 1 )
         return 0;
-    if ( Abc_NtkIsSop(pNtk) )
+    if ( Abc_NtkHasSop(pNtk) )
         return Abc_SopIsInv(pNode->pData);
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkHasBdd(pNtk) )
         return Cudd_IsComplement(pNode->pData);
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkHasAig(pNtk) )
         return 0;
-    if ( Abc_NtkIsMapped(pNtk) )
+    if ( Abc_NtkHasMapping(pNtk) )
         return pNode->pData == Mio_LibraryReadInv(Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()));
     assert( 0 );
     return 0;
diff --git a/src/base/abc/abcCut.c b/src/base/abc/abcCut.c
index b7d83af0..f487bd1b 100644
--- a/src/base/abc/abcCut.c
+++ b/src/base/abc/abcCut.c
@@ -49,7 +49,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     int i;
     int clk = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index e5f1bde9..2fbbee37 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -223,7 +223,7 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
     int i;
-    assert( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // set the traversal ID
     Abc_NtkIncrementTravId( pNtk );
     // start the array of nodes
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index e92907e3..d1445e75 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     Abc_Ntk_t * pNtkNew;
     DdManager * dd;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
     dd = Abc_NtkGlobalBdds( pNtk, 0 );    
@@ -112,7 +112,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
         return NULL;
 
     // start the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make sure the new manager has enough inputs
     Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
     // put the results into the new network (save new CO drivers in old CO drivers)
@@ -324,7 +324,7 @@ int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
     Vec_Ptr_t * vNodes;
     int i;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
 
     // make the network minimum base
     Abc_NtkMinimumBase( pNtk );
diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c
index b83c376a..2316e934 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abc/abcFpga.c
@@ -50,7 +50,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     Abc_Ntk_t * pNtkNew;
     Fpga_Man_t * pMan;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // print a warning about choice nodes
     if ( Abc_NtkCountChoiceNodes( pNtk ) )
@@ -105,7 +105,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     Abc_Obj_t * pNode, * pFanin, * pPrev;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the mapping manager and set its parameters
     pMan = Fpga_ManCreate( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), fVerbose );
@@ -174,7 +174,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i, nDupGates;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // make the mapper point to the new network
     Fpga_CutsCleanSign( pMan );
     Fpga_ManCleanData0( pMan );
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 724c3877..bb7d8cfa 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -92,7 +92,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     Abc_Obj_t * pNode, * pConst1, * pReset;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // create the FRAIG manager
     pMan = Fraig_ManCreate( pParams );
@@ -148,7 +148,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;//, * pNodeNew;
     int i;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     // make the mapper point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )
         Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
@@ -249,7 +249,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
-    if ( !Abc_NtkIsLogicSop(pNtk) )
+    if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         printf( "Abc_NtkFraigTrust: Trust mode works for netlists and logic SOP networks.\n" );
         return NULL;
@@ -262,7 +262,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     }
     
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkFraigTrustOne( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
 
@@ -421,9 +421,9 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pStore;
     int nAndsOld;
 
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
     {
-        printf( "Convert netlist into a logic network before adding to storage.\n" );
+        printf( "The netlist need to be converted into a logic network before adding it to storage.\n" );
         return 0;
     }
 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 8ecbd343..f616a258 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -48,7 +48,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     DdManager * dd;
     int nFaninsMax, i;
 
-    assert( Abc_NtkIsLogicSop(pNtk) ); 
+    assert( Abc_NtkIsSopLogic(pNtk) ); 
 
     // start the functionality manager
     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
@@ -74,7 +74,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     pNtk->pManFunc = dd;
 
     // update the network type
-    pNtk->Type = ABC_NTK_LOGIC_BDD;
+    pNtk->ntkFunc = ABC_FUNC_BDD;
     return 1;
 }
 
@@ -152,12 +152,12 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     int RetValue, i;
     Vec_Str_t * vCube;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) ); 
+    assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
     // allocate the new manager
     pNtk->pManFunc = Extra_MmFlexStart();
     // update the network type
-    pNtk->Type = ABC_NTK_LOGIC_SOP;
+    pNtk->ntkFunc = ABC_FUNC_SOP;
 
     // go through the objects
     vCube = Vec_StrAlloc( 100 );
@@ -165,7 +165,6 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-//Extra_bddPrint( dd, bFunc ); printf( "\n" ); printf( "\n" );
         pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
         if ( pNode->pData == NULL )
             return 0;
@@ -375,7 +374,7 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
 ***********************************************************************/
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 )
 {
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); 
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) ); 
     *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
     *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
 }
diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c
index 5721a50b..0c8994e1 100644
--- a/src/base/abc/abcFxu.c
+++ b/src/base/abc/abcFxu.c
@@ -54,9 +54,11 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
     int fCheck = 1;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) );
     // convert nodes to SOPs
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsMappedLogic(pNtk) )
+        Abc_NtkUnmap(pNtk);
+    else if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
     else
     { // to make sure the SOPs are SCC-free
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index 15e5c6af..f847aa40 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -61,7 +61,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     Map_Man_t * pMan;
     int clk;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
     if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
@@ -130,7 +130,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
     Abc_Obj_t * pNode, * pFanin, * pPrev;
     int i;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // start the mapping manager and set its parameters
     pMan = Map_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk), Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk), fVerbose );
@@ -202,7 +202,7 @@ Abc_Ntk_t * Abc_NtkFromMap( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     int i, nDupGates;
 
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_MAP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_MAP );
     // make the mapper point to the new network
     Map_ManCleanData( pMan );
     Abc_NtkForEachCi( pNtk, pNode, i )
@@ -388,11 +388,11 @@ int Abc_NtkUnmap( Abc_Ntk_t * pNtk )
     char * pSop;
     int i;
 
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
     // update the functionality manager
     assert( pNtk->pManFunc == Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
     pNtk->pManFunc = Extra_MmFlexStart();
-    pNtk->Type     = ABC_NTK_LOGIC_SOP;
+    pNtk->ntkFunc  = ABC_FUNC_SOP;
     // update the nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -424,7 +424,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 
     Map_Man_t * pMan;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // check that the library is available
     if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index d2d88ebf..2a018e35 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -45,7 +45,7 @@ int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, Counter;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
         Counter += Abc_NodeMinimumBase( pNode );
@@ -70,7 +70,7 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     DdNode * bTemp;
     int i, nVars;
 
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
     assert( Abc_ObjIsNode(pNode) );
 
     // compute support
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index 7e6d4905..b8bcec4d 100644
--- a/src/base/abc/abcMiter.c
+++ b/src/base/abc/abcMiter.c
@@ -55,8 +55,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
         return NULL;
     // make sure the circuits are strashed 
-    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
-    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
     if ( pNtk1 && pNtk2 )
         pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
@@ -81,11 +81,11 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     char Buffer[100];
     Abc_Ntk_t * pNtkMiter;
 
-    assert( Abc_NtkIsAig(pNtk1) );
-    assert( Abc_NtkIsAig(pNtk2) );
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsStrash(pNtk2) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
     pNtkMiter->pName = util_strsav(Buffer);
 
@@ -317,13 +317,13 @@ Abc_Ntk_t * Abc_NtkMiterOne( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( Out < Abc_NtkCoNum(pNtk) );
     assert( In1 < Abc_NtkCiNum(pNtk) );
     assert( In2 < Abc_NtkCiNum(pNtk) );
 
     // start the new network
-    pNtkMiter = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkMiter = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%s_miter", pNtk->pName, Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
     pNtkMiter->pName = util_strsav(Buffer);
 
@@ -387,7 +387,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
 {
     Abc_Obj_t * pNodePo, * pChild;
     int i;
-    assert( Abc_NtkIsAig(pMiter) );
+    assert( Abc_NtkIsStrash(pMiter) );
     Abc_NtkForEachPo( pMiter, pNodePo, i )
     {
         pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) );
@@ -478,9 +478,9 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     Abc_Obj_t * pLatch, * pLatchNew;
     int i, Counter;
     assert( nFrames > 0 );
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the new network
-    pNtkFrames = Abc_NtkAlloc( ABC_NTK_AIG );
+    pNtkFrames = Abc_NtkAlloc( ABC_TYPE_STRASH, ABC_FUNC_AIG );
     sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
     pNtkFrames->pName = util_strsav(Buffer);
     // create new latches (or their initial values) and remember them in the new latches
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 8e10b391..f7eb0804 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -47,10 +47,10 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
     int i, k;
     assert( Abc_NtkIsNetlist(pNtk) );
     // start the network
-    if ( Abc_NtkIsNetlistSop(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    if ( !Abc_NtkHasMapping(pNtk) )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     else
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_MAP );
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_MAP );
     // duplicate the nodes 
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
@@ -84,8 +84,8 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
-    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) );
-    if ( Abc_NtkIsAig(pNtk) )
+    assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsStrash(pNtk) )
     {
         pNtkTemp = Abc_NtkAigToLogicSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkIsBddLogic(pNtk) )
     {
         Abc_NtkBddToSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
@@ -122,7 +122,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     pNtkTemp = Abc_NtkAigToLogicSopBench( pNtk );
     pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
     Abc_NtkDelete( pNtkTemp );
@@ -152,14 +152,17 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     char * pNameCo;
     int i, k;
 
-    assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsLogic(pNtk) );
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
+    if ( Abc_NtkIsBddLogic(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+
     // start the netlist by creating PI/PO/Latch objects
-    if ( Abc_NtkIsLogicSop(pNtk) )
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST_SOP );
+    if ( Abc_NtkIsSopLogic(pNtk) )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     else
-        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST_MAP );
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_NETLIST, ABC_FUNC_BDD );
     // create the CI nets and remember them in the new CI nodes
     Abc_NtkForEachCi( pNtk, pObj, i )
     {
@@ -233,9 +236,9 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pNodeNew;
     int i, k;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant node
     Abc_NtkDupConst1( pNtk, pNtkNew );
     // duplicate the nodes and create node functions
@@ -281,7 +284,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     // duplicate the EXDC Ntk
     if ( pNtk->pExdc )
     {
-        if ( Abc_NtkIsAig(pNtk->pExdc) )
+        if ( Abc_NtkIsStrash(pNtk->pExdc) )
             pNtkNew->pExdc = Abc_NtkAigToLogicSop( pNtk->pExdc );
         else
             pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
@@ -309,11 +312,11 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pFanin;
     Vec_Ptr_t * vNodes;
     int i, k;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     if ( Abc_NtkCountChoiceNodes(pNtk) )
         printf( "Warning: Choice nodes are skipped.\n" );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant node
     Abc_NtkDupConst1( pNtk, pNtkNew );
     // collect the nodes to be used (marks all nodes with current TravId)
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index dc7a2e7b..337dd43b 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -57,7 +57,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
         fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
     }
-    else if ( Abc_NtkIsAig(pNtk) )
+    else if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
         if ( Num = Abc_NtkCountChoiceNodes(pNtk) )
@@ -70,26 +70,26 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
-    if ( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsNetlistSop(pNtk) )   
+    if ( Abc_NtkHasSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
 //        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
         if ( fFactored )
             fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
-    else if ( Abc_NtkIsLogicBdd(pNtk) )
+    else if ( Abc_NtkHasBdd(pNtk) )
         fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
-    else if ( Abc_NtkIsLogicMap(pNtk) || Abc_NtkIsNetlistMap(pNtk) )
+    else if ( Abc_NtkHasMapping(pNtk) )
     {
         fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
         fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
     }
-    else if ( !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    else if ( !Abc_NtkHasAig(pNtk) )
     {
         assert( 0 );
     }
 
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_AigGetLevelNum(pNtk) );
     else if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lev = %3d", Abc_NtkGetLevelNum(pNtk) );
@@ -180,7 +180,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
             continue;
         }
         // count the number of cases when the constant is equal to the initial value
-        if ( Abc_NtkIsAig(pNtk) )
+        if ( Abc_NtkIsStrash(pNtk) )
         {
             if ( Abc_LatchIsInit1(pLatch) == !Abc_ObjFaninC0(pLatch) )
                 Counter2++;
@@ -314,7 +314,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i;
-    assert( Abc_NtkIsLogicSop(pNtk) );
+    assert( Abc_NtkIsSopLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
         Abc_NodePrintFactor( pFile, pNode );
 }
@@ -369,7 +369,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
     int i, Length;
 
     // print the delay profile
-    if ( fProfile && Abc_NtkIsMapped(pNtk) )
+    if ( fProfile && Abc_NtkHasMapping(pNtk) )
     {
         int nIntervals = 12;
         float DelayMax, DelayCur, DelayDelta;
@@ -407,7 +407,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
         int LevelMax, * pLevelCounts;
         int nOutsSum, nOutsTotal;
 
-        if ( !Abc_NtkIsAig(pNtk) )
+        if ( !Abc_NtkIsStrash(pNtk) )
             Abc_NtkGetLevelNum(pNtk);
 
         LevelMax = 0;
@@ -430,7 +430,7 @@ void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
         free( pLevelCounts );
         return;
     }
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // find the longest name
     Length = 0;
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
index 89a4d871..e02ccba0 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abc/abcReconv.c
@@ -472,7 +472,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
     Vec_Ptr_t * vVec;
     Abc_Obj_t * pNode, * pFanout;
     int i, k, v, LevelMin;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
 
     // assuming that the structure is clean
     Vec_VecForEachLevel( vLevels, vVec, i )
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 95454668..7e387b47 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -94,7 +94,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     int i, nNodes;
     int clk, clkStart = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the managers
     pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 1a8f7966..081ccfaa 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -167,16 +167,17 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t
 ***********************************************************************/
 void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain )
 {
+    Abc_Ntk_t * pNtk = pNode->pNtk;
     Abc_Obj_t * pNodeNew;
     int nNodesNew, nNodesOld;
-    nNodesOld = Abc_NtkNodeNum(pNode->pNtk);
+    nNodesOld = Abc_NtkNodeNum(pNtk);
     // create the new structure of nodes
     assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
-    pNodeNew = Abc_NodeStrashDec( pNode->pNtk->pManFunc, vFanins, vForm );
+    pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm );
     // remove the old nodes
-    Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pNodeNew );
+    Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew );
     // compare the gains
-    nNodesNew = Abc_NtkNodeNum(pNode->pNtk);
+    nNodesNew = Abc_NtkNodeNum(pNtk);
     assert( nGain <= nNodesOld - nNodesNew );
 }
 
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index 8037f642..c45f9763 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -55,7 +55,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( nThresh >= 0 );
     assert( nFaninMax > 1 );
 
@@ -74,7 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
         Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
 
     // perform renoding for this boundary
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     Abc_NtkRenodeInt( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
 
diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c
index 0b573bac..62e506bb 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abc/abcRewrite.c
@@ -55,7 +55,7 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose )
     int i, nNodes, nGain;
     int clk, clkStart = clock();
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the rewriting manager
     pManRwr = Rwr_ManStart( 0 );
     if ( pManRwr == NULL )
diff --git a/src/base/abc/abcSat.c b/src/base/abc/abcSat.c
index fccb7fbc..4fb059e5 100644
--- a/src/base/abc/abcSat.c
+++ b/src/base/abc/abcSat.c
@@ -48,7 +48,7 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
     lbool   status;
     int clk;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
     if ( Abc_NtkPoNum(pNtk) > 1 )
@@ -110,7 +110,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
     char * pSop0, * pSop1;
     int i;
 
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
 
     // start the data structures
     pSat    = solver_new();
diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c
index 2fcbf670..d6b1b8e5 100644
--- a/src/base/abc/abcSeq.c
+++ b/src/base/abc/abcSeq.c
@@ -67,9 +67,9 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pConst, * pFanout, * pFaninNew, * pLatch;
     int i, k, fChange, Counter;
 
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_SEQ );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_SEQ, ABC_FUNC_AIG );
     pManNew = pNtkNew->pManFunc;
 
     // set mapping of the constant nodes
@@ -200,7 +200,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
     int i, k, c;
     assert( Abc_NtkIsSeq(pNtk) );
     // start the network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     // create the constant and reset nodes
     Abc_NtkDupConst1( pNtk, pNtkNew );
     Abc_NtkDupReset( pNtk, pNtkNew );
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 5a6e1828..730aca90 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -60,7 +60,7 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
     char * pProgGsViewName;
     int RetValue;
 
-    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
 
 #ifdef WIN32
     pProgDotName = "dot.exe";
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index bf97c5bf..19394fb3 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -56,16 +56,13 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
     int nNodes;
 
     assert( !Abc_NtkIsNetlist(pNtk) );
-    if ( Abc_NtkIsLogicBdd(pNtk) )
-    {
-//        printf( "Converting node functions from BDD to SOP.\n" );
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
-    }
     // print warning about choice nodes
     if ( Abc_NtkCountChoiceNodes( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // perform strashing
-    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
     Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
@@ -106,13 +103,10 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     Abc_Obj_t * pObj;
     int i;
     // the first network should be an AIG
-    assert( Abc_NtkIsAig(pNtk1) );
-    assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsAig(pNtk2) ); 
-    if ( Abc_NtkIsLogicBdd(pNtk2) )
-    {
-//        printf( "Converting node functions from BDD to SOP.\n" );
+    assert( Abc_NtkIsStrash(pNtk1) );
+    assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
+    if ( Abc_NtkIsBddLogic(pNtk2) )
         Abc_NtkBddToSop(pNtk2);
-    }
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
@@ -192,7 +186,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     assert( Abc_ObjIsNode(pNode) );
 
     // consider the case when the graph is an AIG
-    if ( Abc_NtkIsAig(pNode->pNtk) )
+    if ( Abc_NtkIsStrash(pNode->pNtk) )
     {
 //        Abc_Obj_t * pChild0, * pChild1;
 //        pChild0 = Abc_ObjFanin0(pNode);
@@ -203,7 +197,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     }
 
     // get the SOP of the node
-    if ( Abc_NtkIsLogicMap(pNode->pNtk) )
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
         pSop = Mio_GateReadSop(pNode->pData);
     else
         pSop = pNode->pData;
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 92d354ac..47565241 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -58,7 +58,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     Fraig_Man_t * pMan;
     stmm_table * tEquiv;
 
-    assert( !Abc_NtkIsAig(pNtk) );
+    assert( !Abc_NtkIsStrash(pNtk) );
 
     // derive the AIG
     pNtkAig = Abc_NtkStrash( pNtk, 0 );
@@ -194,7 +194,7 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
     // assign levels to the nodes of the network
     Abc_NtkGetLevelNum( pNtk );
     // merge nodes in the classes
-    if ( Abc_NtkIsLogicMap( pNtk ) )
+    if ( Abc_NtkHasMapping( pNtk ) )
     {
         Abc_NtkDelayTrace( pNtk );
         stmm_foreach_item( tEquiv, gen, (char **)&pList, NULL )
@@ -403,7 +403,7 @@ int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
     }
     Vec_PtrFree( vNodes );
     // if it is an AIG, also mark the constant 1 node
-    if ( Abc_NtkIsAig(pNtk) )
+    if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigConst1(pNtk->pManFunc)->fMarkA = 1;
     // remove the non-marked nodes
     Counter = 0;
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index 9d71ace5..032d074c 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -553,7 +553,7 @@ float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk )
     float tArrivalMax;
     int i;
 
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
 
     Abc_NtkTimePrepare( pNtk );
     vNodes = Abc_NtkDfs( pNtk, 1 );
@@ -647,7 +647,7 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pFanout;
     int i, k, nLevelsCur;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // remember the maximum number of direct levels
     pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
     // start the reverse levels
@@ -701,7 +701,7 @@ void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk )
 void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
     Vec_IntWriteEntry( pNtk->vLevelsR, pObj->Id, LevelR );
@@ -722,7 +722,7 @@ void Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR )
 int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     Vec_IntFillExtra( pNtk->vLevelsR, pObj->Id + 1, 0 );
     return Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
@@ -743,7 +743,7 @@ int Abc_NodeReadReverseLevel( Abc_Obj_t * pObj )
 int Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
-    assert( Abc_NtkIsAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     assert( pNtk->vLevelsR );
     return pNtk->LevelMax + 1 - Vec_IntEntry(pNtk->vLevelsR, pObj->Id);
 }
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
index b5a3a644..04e5c96c 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abc/abcUnreach.c
@@ -282,7 +282,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     int i;
 
     // start the new network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD );
+    pNtkNew = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_BDD );
     // create PIs corresponding to LOs
     Abc_NtkForEachLatch( pNtk, pNode, i )
         pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
@@ -308,13 +308,20 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkForEachCo( pNtk, pNode, i )
         Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
 
-    // copy the CI/CO names
+    // store the PI names of the EXDC network
     Abc_NtkForEachLatch( pNtk, pNode, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
+    // store the PO names of the EXDC network
     Abc_NtkForEachPo( pNtk, pNode, i )
         Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjName(pNode) );
+        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
     Abc_NtkBddToSop( pNtkNew );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 87d57947..7d2ca107 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -72,7 +72,7 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nCubes = 0;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -96,7 +96,7 @@ int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nLits = 0;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -121,16 +121,14 @@ int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk )
     Vec_Int_t * vFactor;
     Abc_Obj_t * pNode;
     int nNodes, i;
-    assert( Abc_NtkIsSop(pNtk) );
+    assert( Abc_NtkHasSop(pNtk) );
     nNodes = 0;
-//    Ft_FactorStartMan();
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         vFactor = Ft_Factor( pNode->pData );
         nNodes += Ft_FactorGetNumNodes(vFactor);
         Vec_IntFree( vFactor );
     }
-//    Ft_FactorStopMan();
     return nNodes;
 }
 
@@ -149,7 +147,7 @@ int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, nNodes = 0;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -175,7 +173,7 @@ int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk )
     DdNode * bCover, * zCover, * bFunc;
     DdManager * dd = pNtk->pManFunc;
     int i, nClauses = 0;
-    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkIsBddLogic(pNtk) );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
@@ -214,7 +212,7 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode;
     double TotalArea;
     int i;
-    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkHasMapping(pNtk) );
     TotalArea = 0.0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -367,9 +365,12 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
         pDriver = Abc_ObjFanin0(pNode);
         if ( Abc_ObjIsCi(pDriver) )
         {
-            // skip the case when the CI deriver has the same name as CO
-            if ( strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
+            // skip the case when the driver is a different node with the same name
+            if ( pDriver != pNode && strcmp(Abc_ObjName(pDriver), Abc_ObjName(pNode)) == 0 )
+            {
+                assert( !Abc_ObjFaninC0(pNode) );
                 continue;
+            }
         }
         else
         {
@@ -385,9 +386,9 @@ int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate )
             if ( Abc_ObjFaninC0(pNode) )
             {
                 // change polarity of the duplicated driver
-                if ( Abc_NtkIsLogicSop(pNtk) )
+                if ( Abc_NtkHasSop(pNtk) )
                     Abc_SopComplement( pDriverNew->pData );
-                else if ( Abc_NtkIsLogicBdd(pNtk) )
+                else if ( Abc_NtkHasBdd(pNtk) )
                     pDriverNew->pData = Cudd_Not( pDriverNew->pData );
                 else
                     assert( 0 );
@@ -643,7 +644,7 @@ int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i, Counter;
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
         return 0;
     Counter = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index bd390002..d9bed264 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/base/abc/abc.c \
     src/base/abc/abcAig.c \
     src/base/abc/abcAttach.c \
+    src/base/abc/abcBalance.c \
     src/base/abc/abcCheck.c \
     src/base/abc/abcCollapse.c \
     src/base/abc/abcCreate.c \
@@ -19,9 +20,10 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcNames.c \
     src/base/abc/abcNetlist.c \
     src/base/abc/abcPrint.c \
+    src/base/abc/abcReconv.c \
+    src/base/abc/abcRefactor.c \
     src/base/abc/abcRefs.c \
     src/base/abc/abcRenode.c \
-    src/base/abc/abcRefactor.c \
     src/base/abc/abcRewrite.c \
     src/base/abc/abcSat.c \
     src/base/abc/abcSeq.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 255791a7..84c330bf 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1300,7 +1300,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
 
     // write out the current network
@@ -1423,7 +1423,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
     fclose( pFile );
 
-    if ( Abc_NtkIsLogicBdd(pNtk) )
+    if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
 
     // write out the current network
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 1fe73690..9ffbc3cf 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -604,7 +604,7 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[util_optind];
 
     // check the network type
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( pAbc->Out, "Currently can only write logic networks, AIGs, and seq AIGs.\n" );
         return 0;
@@ -670,7 +670,7 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
     // get the input file name
     FileName = argv[util_optind];
 
-    if ( !Abc_NtkIsAig(pNtk) )
+    if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pAbc->Out, "The network should be an AIG.\n" );
         return 0;
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index f598c4e5..b5dc2fa8 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -292,12 +292,12 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         }
         pModelName = vTokens->pArray[1];
         // allocate the empty network
-        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+        p->pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
         p->pNtk->pName = util_strsav( pModelName );
         p->pNtk->pSpec = util_strsav( p->pFileName );
     }
     else
-        p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+        p->pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
 
     // read the inputs/outputs
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
@@ -581,8 +581,8 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     // if this is the first line with gate, update the network type
     if ( Abc_NtkNodeNum(p->pNtk) == 0 )
     {
-        assert( p->pNtk->Type = ABC_NTK_NETLIST_SOP );
-        p->pNtk->Type = ABC_NTK_NETLIST_MAP;
+        assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
+        p->pNtk->ntkFunc = ABC_FUNC_MAP;
         Extra_MmFlexStop( p->pNtk->pManFunc, 0 );
         p->pNtk->pManFunc = pGenlib;
     }
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index 936a1c0c..53299a0c 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -271,7 +271,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
     pModelName = vTokens->pArray[1];
 
     // allocate the empty network
-    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST_SOP );
+    pNtk = Abc_NtkAlloc( ABC_TYPE_NETLIST, ABC_FUNC_SOP );
     pNtk->pName = util_strsav( pModelName );
     pNtk->pSpec = util_strsav( p->pFileName );
 
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 7c4a4ab1..df79227d 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -46,7 +46,7 @@ int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
 {
     Abc_Ntk_t * pExdc;
     FILE * pFile;
-    assert( Abc_NtkIsNetlistSop(pNtk) );
+    assert( Abc_NtkIsSopNetlist(pNtk) );
     pFile = fopen( pFileName, "w" );
     if ( pFile == NULL )
     {
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 5c83aad2..5135105f 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -320,7 +320,7 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
 ***********************************************************************/
 void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
 {
-    if ( Abc_NtkIsNetlistMap(pNode->pNtk) )
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
     {
         // write the .gate line
         fprintf( pFile, ".gate" );
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 144ff167..bb216bb6 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -44,9 +44,9 @@ static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
 int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
 {
     solver * pSat;
-    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( stdout, "Io_WriteCnf(): Currently can process logic networks with BDDs.\n" );
+        fprintf( stdout, "Io_WriteCnf(): Currently can only process logic networks with BDDs.\n" );
         return 0;
     }
     if ( Abc_NtkPoNum(pNtk) != 1 )
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 9c78b149..25a68978 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -46,7 +46,7 @@ int Io_WritePla( Abc_Ntk_t * pNtk, char * pFileName )
     Abc_Ntk_t * pExdc;
     FILE * pFile;
 
-    assert( Abc_NtkIsNetlistSop(pNtk) );
+    assert( Abc_NtkIsSopNetlist(pNtk) );
     assert( Abc_NtkGetLevelNum(pNtk) == 1 );
 
     pFile = fopen( pFileName, "w" );
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 899f8166..cb39c481 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -2,6 +2,7 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioRead.c \
     src/base/io/ioReadBench.c \
     src/base/io/ioReadBlif.c \
+    src/base/io/ioReadEdif.c \
     src/base/io/ioReadPla.c \
     src/base/io/ioReadVerilog.c \
     src/base/io/ioUtil.c \
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 38574883..2e9d9d41 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -336,7 +336,7 @@ void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
 {
     Abc_Ntk_t * pNtk;
     for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
-        if ( Abc_NtkIsLogicMap(pNtk) )
+        if ( Abc_NtkHasMapping(pNtk) )
             Abc_NtkUnmap( pNtk );
 }
 
diff --git a/src/bdd/dsd/module.make b/src/bdd/dsd/module.make
index f6418492..f5e6673d 100644
--- a/src/bdd/dsd/module.make
+++ b/src/bdd/dsd/module.make
@@ -1,6 +1,6 @@
-SRC +=    bdd\dsd\dsdApi.c \
-    bdd\dsd\dsdCheck.c \
-    bdd\dsd\dsdLocal.c \
-    bdd\dsd\dsdMan.c \
-    bdd\dsd\dsdProc.c \
-    bdd\dsd\dsdTree.c
+SRC +=    src/bdd/dsd/dsdApi.c \
+    src/bdd/dsd/dsdCheck.c \
+    src/bdd/dsd/dsdLocal.c \
+    src/bdd/dsd/dsdMan.c \
+    src/bdd/dsd/dsdProc.c \
+    src/bdd/dsd/dsdTree.c
diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 703be139..7eb41e0e 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,7 +1,7 @@
-SRC +=    bdd\reo\reoApi.c \
-    bdd\reo\reoCore.c \
-    bdd\reo\reoProfile.c \
-    bdd\reo\reoSift.c \
-    bdd\reo\reoSwap.c \
-    bdd\reo\reoTransfer.c \
-    bdd\reo\reoUnits.c
+SRC +=    src/bdd/reo/reoApi.c \
+    src/bdd/reo/reoCore.c \
+    src/bdd/reo/reoProfile.c \
+    src/bdd/reo/reoSift.c \
+    src/bdd/reo/reoSwap.c \
+    src/bdd/reo/reoTransfer.c \
+    src/bdd/reo/reoUnits.c
diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c
index a43bcdc1..16cbfd5c 100644
--- a/src/map/mapper/mapperCore.c
+++ b/src/map/mapper/mapperCore.c
@@ -69,7 +69,7 @@ int Map_Mapping( Map_Man_t * p )
     Map_MappingTruths( p );
     p->timeTruth = clock() - clk;
     //////////////////////////////////////////////////////////////////////
-PRT( "Truths", clock() - clk );
+//PRT( "Truths", clock() - clk );
 
     //////////////////////////////////////////////////////////////////////
     // compute the minimum-delay mapping
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index d5b0330f..6d771990 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -804,7 +804,7 @@ void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounte
         *ppCounters = pCounters;
     else
         free( pCounters );
-    printf( "The number of 3N-classes = %d.\n", nClasses );
+//    printf( "The number of 3N-classes = %d.\n", nClasses );
 }
 
 /**Function*************************************************************
@@ -870,7 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
         *ppCounters = pCounters;
     else
         free( pCounters );
-    printf( "The number of 4N-classes = %d.\n", nClasses );
+//    printf( "The number of 4N-classes = %d.\n", nClasses );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index f3a0f743..6719ed4d 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -70,7 +70,7 @@ static inline int        Cut_CutReadLeaveNum( Cut_Cut_t * p )  {  return p->nLea
 static inline int *      Cut_CutReadLeaves( Cut_Cut_t * p )    {  return p->pLeaves;   }
 static inline void *     Cut_CutReadData( Cut_Cut_t * p )      {  return p->pData;     }
 
-static inline void *     Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
+static inline void       Cut_CutWriteData( Cut_Cut_t * p, void * pData )  { p->pData = pData;  }
 static inline void       Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth )  { 
     if ( p->nVarsMax == 4 )  { p->uTruth = *puTruth;  return; }
     p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 1c291b33..b9bab47f 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -137,7 +137,6 @@ extern void              Rwr_ManWriteToArray( Rwr_Man_t * p );
 extern void              Rwr_ManLoadFromArray( Rwr_Man_t * p, int fVerbose );
 extern void              Rwr_ManWriteToFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
-extern Vec_Int_t *       Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk );
 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
 
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index dedd86fe..65b2bd6f 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -25,8 +25,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 // precomputed data
+#ifdef _WIN32
 unsigned short s_RwrPracticalClasses[];
 unsigned short s_RwtAigSubgraphs[];
+#else
+static unsigned short s_RwrPracticalClasses[];
+static unsigned short s_RwtAigSubgraphs[];
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -221,30 +226,6 @@ void Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the array of fanout counters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Rwt_NtkFanoutCounters( Abc_Ntk_t * pNtk )
-{
-    Vec_Int_t * vFanNums;
-    Abc_Obj_t * pObj;
-    int i;
-    vFanNums = Vec_IntAlloc( 0 );
-    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        if ( Abc_ObjIsNode( pObj ) )
-            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
-    return vFanNums;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Adds the node to the end of the list.]
 
   Description []
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index eddd7270..242de8e2 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -69,7 +69,7 @@ CSAT_Manager CSAT_InitManager()
     CSAT_Manager_t * mng;
     mng = ALLOC( CSAT_Manager_t, 1 );
     memset( mng, 0, sizeof(CSAT_Manager_t) );
-    mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC_SOP );
+    mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
     mng->pNtk->pName = util_strsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
     mng->vNodes  = Vec_PtrAlloc( 100 );
diff --git a/src/sat/csat/module.make b/src/sat/csat/module.make
new file mode 100644
index 00000000..5b71a03c
--- /dev/null
+++ b/src/sat/csat/module.make
@@ -0,0 +1 @@
+SRC +=  src/sat/csat/csat_apis.c
diff --git a/src/sop/ft/ftFactor.c b/src/sop/ft/ftFactor.c
index d25d0653..19f70e36 100644
--- a/src/sop/ft/ftFactor.c
+++ b/src/sop/ft/ftFactor.c
@@ -319,10 +319,10 @@ Ft_Node_t * Ft_FactorTrivialTree_rec( Vec_Int_t * vForm, Ft_Node_t ** ppNodes, i
         return ppNodes[0];
 
     // split the nodes into two parts
-//    nNodes1 = nNodes/2;
-//    nNodes2 = nNodes - nNodes1;
-    nNodes2 = nNodes/2;
-    nNodes1 = nNodes - nNodes2;
+    nNodes1 = nNodes/2;
+    nNodes2 = nNodes - nNodes1;
+//    nNodes2 = nNodes/2;
+//    nNodes1 = nNodes - nNodes2;
 
     // recursively construct the tree for the parts
     pNode1 = Ft_FactorTrivialTree_rec( vForm, ppNodes,           nNodes1, fAnd );