Version abc50902

24 files changed, 759 insertions, 667 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 97e5663f..dca80ca5 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -20,7 +20,6 @@
 
 #include "abc.h"
 #include "mainInt.h"
-#include "ft.h"
 #include "fraig.h"
 #include "fxu.h"
 #include "cut.h"
@@ -162,7 +161,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
 
-    Ft_FactorStartMan();
 //    Rwt_Man4ExploreStart();
 //    Map_Var3Print();
 //    Map_Var4Test();
@@ -181,7 +179,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
-    Ft_FactorStopMan();
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
 }
@@ -1707,7 +1704,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
     }
-    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
         return 1;
@@ -1816,7 +1813,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command can only be applied to an AIG.\n" );
         return 1;
     }
-    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    if ( Abc_NtkGetChoiceNum(pNtk) )
     {
         fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
         return 1;
@@ -1957,7 +1954,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pArgvNew = argv + util_optind;
     nArgcNew = argc - util_optind;
-    if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+    if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
 
     // compute the miter
@@ -3858,7 +3855,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pArgvNew = argv + util_optind;
     nArgcNew = argc - util_optind;
-    if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+    if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
 
     // perform equivalence checking
@@ -3943,7 +3940,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pArgvNew = argv + util_optind;
     nArgcNew = argc - util_optind;
-    if ( !Abc_NtkPrepareCommand( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+    if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
         return 1;
 
     // perform equivalence checking
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c779230a..81a1c328 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -476,6 +476,7 @@ extern Abc_Ntk_t *        Abc_NtkFraigRestore();
 extern void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
+extern DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
 extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
 extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
@@ -509,6 +510,13 @@ extern char *             Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pN
 extern char *             Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
 extern void               Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
+extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
+extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
+extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
+extern int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
+extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
@@ -546,7 +554,6 @@ extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NodeMffcCollect( Abc_Obj_t * pNode );
-extern void               Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, int nGain );
 /*=== abcRenode.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
@@ -594,8 +601,6 @@ extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses,
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
 extern Abc_Obj_t *        Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
-extern Abc_Obj_t *        Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm );
-extern int                Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 /*=== abcSweep.c ==========================================================*/
 extern bool               Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
@@ -622,13 +627,6 @@ extern void               Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
 extern int                Abc_NodeReadReverseLevel( Abc_Obj_t * pObj );
 extern int                Abc_NodeReadRequiredLevel( Abc_Obj_t * pObj );
-/*=== abcTravId.c ==========================================================*/
-extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
-extern void               Abc_NodeSetTravId( Abc_Obj_t * pObj, int TravId );
-extern void               Abc_NodeSetTravIdCurrent( Abc_Obj_t * pObj );
-extern void               Abc_NodeSetTravIdPrevious( Abc_Obj_t * pObj );
-extern bool               Abc_NodeIsTravIdCurrent( Abc_Obj_t * pObj );
-extern bool               Abc_NodeIsTravIdPrevious( Abc_Obj_t * pObj );
 /*=== abcUtil.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
@@ -637,28 +635,22 @@ extern int                Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk );
 extern double             Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
 extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
 extern void               Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
-extern int                Abc_NtkCountExors( Abc_Ntk_t * pNtk );
 extern bool               Abc_NodeIsExorType( Abc_Obj_t * pNode );
 extern bool               Abc_NodeIsMuxType( Abc_Obj_t * pNode );
 extern Abc_Obj_t *        Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
-extern int                Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk );
-extern int                Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
+extern int                Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
 extern void               Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
 extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
-extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
-extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
-extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
-extern void               Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb );
-extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
 
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 9b9e9ee2..c5f644d2 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -661,8 +661,8 @@ bool Abc_NtkCompareLatches( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
-    Abc_NtkAlphaOrderSignals( pNtk1, fComb );
-    Abc_NtkAlphaOrderSignals( pNtk2, fComb );
+    Abc_NtkOrderObjsByName( pNtk1, fComb );
+    Abc_NtkOrderObjsByName( pNtk2, fComb );
     if ( !Abc_NtkCompareLatches( pNtk1, pNtk2, fComb ) )
         return 0;
     if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c
index 2316e934..ad411aa5 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abc/abcFpga.c
@@ -53,7 +53,7 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // print a warning about choice nodes
-    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing FPGA mapping with choices.\n" );
 
     // perform FPGA mapping
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 83735e47..ef4746d5 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -267,7 +267,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     Abc_NtkFinalize( pNtk, pNtkNew );
 
     // print a warning about choice nodes
-    printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkCountChoiceNodes( pNtkNew ) );
+    printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
 
     // make sure that everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 44acb699..e5af1829 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -24,7 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static DdNode *    Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins );
 static int         Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFanins, Vec_Str_t * vCube, int fPhase );
 
 ////////////////////////////////////////////////////////////////////////
@@ -61,7 +60,7 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) );
+        pNode->pData = Abc_ConvertSopToBdd( dd, pNode->pData );
         if ( pNode->pData == NULL )
         {
             printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
@@ -89,43 +88,37 @@ int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins )
+DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
 {
-    DdNode * bCube, * bTemp, * bVar, * bRes;
+    DdNode * bSum, * bCube, * bTemp, * bVar;
     char * pCube;
-    int i, c;
-
-    bRes = Cudd_Not(dd->one);   Cudd_Ref( bRes );
-    for ( c = 0; ; c++ )
+    int nVars, Value, v;
+    // start the cover
+    nVars = Abc_SopGetVarNum(pSop);
+    // check the logic function of the node
+    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
+    Abc_SopForEachCube( pSop, nVars, pCube )
     {
-        // get the cube
-        pCube = pSop + c * (nFanins + 3);
-        if ( *pCube == 0 )
-            break;
-        // construct BDD for the cube
-        bCube = dd->one;   Cudd_Ref( bCube );
-        for ( i = 0; i < nFanins; i++ )
+        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
+        Abc_CubeForEachVar( pCube, Value, v )
         {
-            if ( pCube[i] == '0' )
-                bVar = Cudd_Not( dd->vars[i] );
-            else if ( pCube[i] == '1' )
-                bVar = dd->vars[i];
+            if ( Value == '0' )
+                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
+            else if ( Value == '1' )
+                bVar = Cudd_bddIthVar( dd, v );
             else
                 continue;
             bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
             Cudd_RecursiveDeref( dd, bTemp );
         }
-        bRes = Cudd_bddOr( dd, bTemp = bRes, bCube );   Cudd_Ref( bRes );
+        bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   Cudd_Ref( bSum );
         Cudd_RecursiveDeref( dd, bTemp );
         Cudd_RecursiveDeref( dd, bCube );
     }
-    // decide if we need to complement the result
-    pCube = pSop + nFanins + 1;
-    assert( *pCube == '0' || *pCube == '1' );
-    if ( *pCube == '0' )
-        bRes = Cudd_Not(bRes);
-    Cudd_Deref( bRes );
-    return bRes;
+    // complement the result if necessary
+    bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
+    Cudd_Deref( bSum );
+    return bSum;
 }
 
 /**Function*************************************************************
@@ -171,7 +164,7 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( Abc_SopIsComplement(pNode->pData) )
         {
-            bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) );  Cudd_Ref( bFunc );
+            bFunc = Abc_ConvertSopToBdd( dd, pNode->pData );  Cudd_Ref( bFunc );
             pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, 1 );
             Cudd_RecursiveDeref( dd, bFunc );
             assert( !Abc_SopIsComplement(pNode->pData) );
@@ -340,7 +333,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     // verify
     if ( fVerify )
     {
-        bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins );  Cudd_Ref( bFuncNew );
+        bFuncNew = Abc_ConvertSopToBdd( dd, pSop );  Cudd_Ref( bFuncNew );
         if ( bFuncOn == bFuncOnDc )
         {
             if ( bFuncNew != bFuncOn )
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index f847aa40..28853c8d 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     }
 
     // print a warning about choice nodes
-    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing mapping with choices.\n" );
 
     // perform the mapping
@@ -442,7 +442,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
     }
 
     // print a warning about choice nodes
-    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing mapping with choices.\n" );
 
     // perform the mapping
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 088dc855..2bf6461b 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -269,6 +269,233 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pFanin;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames )
+{
+    Vec_Ptr_t * vNames;
+    char Buffer[5];
+    int i;
+
+    vNames = Vec_PtrAlloc( nNames );
+    for ( i = 0; i < nNames; i++ )
+    {
+        if ( nNames < 26 )
+        {
+            Buffer[0] = 'a' + i;
+            Buffer[1] = 0;
+        }
+        else
+        {
+            Buffer[0] = 'a' + i%26;
+            Buffer[1] = '0' + i/26;
+            Buffer[2] = 0;
+        }
+        Vec_PtrPush( vNames, util_strsav(Buffer) );
+    }
+    return vNames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeNames( Vec_Ptr_t * vNames )
+{
+    int i;
+    if ( vNames == NULL )
+        return;
+    for ( i = 0; i < vNames->nSize; i++ )
+        free( vNames->pArray[i] );
+    Vec_PtrFree( vNames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the CI or CO names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos )
+{
+    Abc_Obj_t * pObj;
+    char ** ppNames;
+    int i;
+    if ( fCollectCos )
+    {
+        ppNames = ALLOC( char *, Abc_NtkCoNum(pNtk) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            ppNames[i] = Abc_ObjName(pObj);
+    }
+    else
+    {
+        ppNames = ALLOC( char *, Abc_NtkCiNum(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            ppNames[i] = Abc_ObjName(pObj);
+    }
+    return ppNames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
+{
+    int Diff = strcmp( (char *)(*pp1)->pCopy, (char *)(*pp2)->pCopy );
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders PIs/POs/latches alphabetically.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // temporarily store the names in the copy field
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
+    // order objects alphabetically
+    qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+    qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), 
+        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+    // if the comparison if combinational (latches as PIs/POs), order them too
+    if ( fComb )
+    {
+        qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), 
+            (int (*)(const void *, const void *)) Abc_NodeCompareNames );
+        // add latches to make COs
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+        {
+            Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj );
+            Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj );
+        }
+    }
+    // clean the copy fields
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
+{
+    stmm_table * tObj2NameNew;
+    Abc_Obj_t * pObj;
+    char Buffer[100];
+    char * pNameNew;
+    int Length, i;
+
+    tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "pi%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "po%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    // create new names and add them to the table
+    Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        sprintf( Buffer, "lat%0*d", Length, i );
+        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
+        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
+    }
+    stmm_free_table( pNtk->tObj2Name );
+    pNtk->tObj2Name = tObj2NameNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index f7eb0804..77fbeb38 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -313,7 +313,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes;
     int i, k;
     assert( Abc_NtkIsStrash(pNtk) );
-    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    if ( Abc_NtkGetChoiceNum(pNtk) )
         printf( "Warning: Choice nodes are skipped.\n" );
     // start the network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 4f8b4aeb..41b9288e 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -60,9 +60,9 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else if ( Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
-        if ( Num = Abc_NtkCountChoiceNodes(pNtk) )
+        if ( Num = Abc_NtkGetChoiceNum(pNtk) )
             fprintf( pFile, " (choice = %d)", Num );
-        if ( Num = Abc_NtkCountExors(pNtk) )
+        if ( Num = Abc_NtkGetExorNum(pNtk) )
             fprintf( pFile, " (exor = %d)", Num );
     }
     else if ( Abc_NtkIsSeq(pNtk) )
@@ -332,7 +332,7 @@ void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames )
 ***********************************************************************/
 void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
 {
-    Vec_Int_t * vFactor;
+    Dec_Graph_t * pGraph;
     Vec_Ptr_t * vNamesIn;
     if ( Abc_ObjIsCo(pNode) )
         pNode = Abc_ObjFanin0(pNode);
@@ -347,16 +347,16 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
         return;
     }
     assert( Abc_ObjIsNode(pNode) );
-    vFactor = Ft_Factor( pNode->pData );
+    pGraph = Dec_Factor( pNode->pData );
     if ( fUseRealNames )
     {
         vNamesIn = Abc_NodeGetFaninNames(pNode);
-        Ft_FactorPrint( stdout, vFactor, (char **)vNamesIn->pArray, Abc_ObjName(pNode) );
+        Dec_GraphPrint( stdout, pGraph, (char **)vNamesIn->pArray, Abc_ObjName(pNode) );
         Abc_NodeFreeNames( vNamesIn );
     }
     else
-        Ft_FactorPrint( stdout, vFactor, (char **)NULL, Abc_ObjName(pNode) );
-    Vec_IntFree( vFactor );
+        Dec_GraphPrint( stdout, pGraph, (char **)NULL, Abc_ObjName(pNode) );
+    Dec_GraphFree( pGraph );
 }
 
 
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
index ea662799..766c14f3 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abc/abcReconv.c
@@ -19,7 +19,6 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "ft.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 1524489d..791d2d53 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -34,10 +34,8 @@ struct Abc_ManRef_t_
     int              fVerbose;          // the verbosity flag
     // internal data structures
     DdManager *      dd;                // the BDD manager
-//    Vec_Int_t *      vReqTimes;         // required times for each node
     Vec_Str_t *      vCube;             // temporary
     Vec_Int_t *      vForm;             // temporary
-    Vec_Int_t *      vLevNums;          // temporary
     Vec_Ptr_t *      vVisited;          // temporary
     Vec_Ptr_t *      vLeaves;           // temporary
     // node statistics
@@ -60,7 +58,7 @@ struct Abc_ManRef_t_
 static void           Abc_NtkManRefPrintStats( Abc_ManRef_t * p );
 static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose );
 static void           Abc_NtkManRefStop( Abc_ManRef_t * p );
-static Vec_Int_t *    Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose );
+static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -88,11 +86,11 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     ProgressBar * pProgress;
     Abc_ManRef_t * pManRef;
     Abc_ManCut_t * pManCut;
+    Dec_Graph_t * pFForm;
     Vec_Ptr_t * vFanins;
-    Vec_Int_t * vForm;
     Abc_Obj_t * pNode;
-    int i, nNodes;
     int clk, clkStart = clock();
+    int i, nNodes;
 
     assert( Abc_NtkIsStrash(pNtk) );
     // cleanup the AIG
@@ -109,27 +107,27 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        // stop if all nodes have been tried once
-        if ( i >= nNodes )
-            break;
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // stop if all nodes have been tried once
+        if ( i >= nNodes )
+            break;
         // compute a reconvergence-driven cut
 clk = clock();
         vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
 pManRef->timeCut += clock() - clk;
         // evaluate this cut
 clk = clock();
-        vForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose );
+        pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose );
 pManRef->timeRes += clock() - clk;
-        if ( vForm == NULL )
+        if ( pFForm == NULL )
             continue;
         // acceptable replacement found, update the graph
 clk = clock();
-        Abc_NodeUpdate( pNode, vFanins, vForm, pManRef->nLastGain );
+        Dec_GraphUpdateNetwork( pNode, pFForm, pManRef->nLastGain );
 pManRef->timeNtk += clock() - clk;
-        Vec_IntFree( vForm );
+        Dec_GraphFree( pFForm );
     }
     Extra_ProgressBarStop( pProgress );
 pManRef->timeTotal = clock() - clkStart;
@@ -161,40 +159,33 @@ pManRef->timeTotal = clock() - clkStart;
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose )
+Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
     int fVeryVerbose = 0;
     Abc_Obj_t * pFanin;
-    Vec_Int_t * vForm;
-    DdNode * bNodeFunc, * bNodeDc, * bNodeOn, * bNodeOnDc;
+    Dec_Graph_t * pFForm;
+    DdNode * bNodeFunc;
+    int nNodesSaved, nNodesAdded, i, clk;
     char * pSop;
-    int nBddNodes, nFtNodes, nNodesSaved, nNodesAdded;
-    int i, Required, clk;
 
     p->nNodesConsidered++;
 
-    // get the required level of this node
-    Required = Abc_NodeReadRequiredLevel( pNode );
-
     // get the function of the cut
 clk = clock();
     bNodeFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pNode, vFanins, p->vVisited );  Cudd_Ref( bNodeFunc );
 p->timeBdd += clock() - clk;
-    nBddNodes = Cudd_DagSize(bNodeFunc);
 
     // if don't-care are used, transform the function into ISOP
     if ( fUseDcs )
     {
+        DdNode * bNodeDc, * bNodeOn, * bNodeOnDc;
         int nMints, nMintsDc;
-
 clk = clock();
         // get the don't-cares
         bNodeDc = Abc_NodeConeDcs( p->dd, p->dd->vars + vFanins->nSize, p->dd->vars, p->vLeaves, vFanins, p->vVisited ); Cudd_Ref( bNodeDc );
-
         nMints = (1 << vFanins->nSize);
         nMintsDc = (int)Cudd_CountMinterm( p->dd, bNodeDc, vFanins->nSize );
 //        printf( "Percentage of minterms = %5.2f.\n", 100.0 * nMintsDc / nMints );
-
         // get the ISF
         bNodeOn   = Cudd_bddAnd( p->dd, bNodeFunc, Cudd_Not(bNodeDc) );   Cudd_Ref( bNodeOn );
         bNodeOnDc = Cudd_bddOr ( p->dd, bNodeFunc, bNodeDc );             Cudd_Ref( bNodeOnDc );
@@ -207,58 +198,52 @@ clk = clock();
 p->timeDcs += clock() - clk;
     }
 
-//Extra_bddPrint( p->dd, bNodeFunc ); printf( "\n" );
     // always accept the case of constant node
     if ( Cudd_IsConstant(bNodeFunc) )
     {
         p->nLastGain = Abc_NodeMffcSize( pNode );
         p->nNodesGained += p->nLastGain;
         p->nNodesRefactored++;
-        // get the constant node
-//        pFanin = Abc_ObjNotCond( Abc_AigConst1(pNode->pNtk->pManFunc), Cudd_IsComplement(bNodeFunc) );
-//        Abc_AigReplace( pNode->pNtk->pManFunc, pNode, pFanin );
-//        Cudd_RecursiveDeref( p->dd, bNodeFunc );
-//printf( "Gain = %d.\n", p->nLastGain );
         Cudd_RecursiveDeref( p->dd, bNodeFunc );
-        return Ft_FactorConst( !Cudd_IsComplement(bNodeFunc) );
+        if ( Cudd_IsComplement(bNodeFunc) )
+            return Dec_GraphCreateConst0();
+        return Dec_GraphCreateConst1();
     }
 
     // get the SOP of the cut
 clk = clock();
     pSop = Abc_ConvertBddToSop( NULL, p->dd, bNodeFunc, bNodeFunc, vFanins->nSize, p->vCube, -1 );
 p->timeSop += clock() - clk;
-    Cudd_RecursiveDeref( p->dd, bNodeFunc );
 
     // get the factored form
 clk = clock();
-    vForm = Ft_Factor( pSop );
-p->timeFact += clock() - clk;
-    nFtNodes = Ft_FactorGetNumNodes( vForm );
+    pFForm = Dec_Factor( pSop );
     free( pSop );
-//Ft_FactorPrint( stdout, vForm, NULL, NULL );
+p->timeFact += clock() - clk;
 
     // mark the fanin boundary 
-    // (can mark only essential fanins, belonging to bNodeFunc!!!)
+    // (can mark only essential fanins, belonging to bNodeFunc!)
     Vec_PtrForEachEntry( vFanins, pFanin, i )
         pFanin->vFanouts.nSize++;
-
     // label MFFC with current traversal ID
     Abc_NtkIncrementTravId( pNode->pNtk );
     nNodesSaved = Abc_NodeMffcLabel( pNode );
-
-    // unmark the fanin boundary
+    // unmark the fanin boundary and set the fanins as leaves in the form
     Vec_PtrForEachEntry( vFanins, pFanin, i )
+    {
         pFanin->vFanouts.nSize--;
+        Dec_GraphNode(pFForm, i)->pFunc = pFanin;
+    }
 
     // detect how many new nodes will be added (while taking into account reused nodes)
 clk = clock();
-    nNodesAdded = Abc_NodeStrashDecCount( pNode->pNtk->pManFunc, pNode, vFanins, vForm, 
-        p->vLevNums, nNodesSaved, Required );
+    nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Abc_NodeReadRequiredLevel(pNode) );
 p->timeEval += clock() - clk;
     // quit if there is no improvement
     if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros )
     {
-        Vec_IntFree( vForm );
+        Cudd_RecursiveDeref( p->dd, bNodeFunc );
+        Dec_GraphFree( pFForm );
         return NULL;
     }
 
@@ -272,14 +257,15 @@ p->timeEval += clock() - clk;
     {
         printf( "Node %6s : ",  Abc_ObjName(pNode) );
         printf( "Cone = %2d. ", vFanins->nSize );
-        printf( "BDD = %2d. ",  nBddNodes );
-        printf( "FF = %2d. ",   nFtNodes );
+        printf( "BDD = %2d. ",  Cudd_DagSize(bNodeFunc) );
+        printf( "FF = %2d. ",   1 + Dec_GraphNodeNum(pFForm) );
         printf( "MFFC = %2d. ", nNodesSaved );
         printf( "Add = %2d. ",  nNodesAdded );
         printf( "GAIN = %2d. ", p->nLastGain );
         printf( "\n" );
     }
-    return vForm;
+    Cudd_RecursiveDeref( p->dd, bNodeFunc );
+    return pFForm;
 }
 
 
@@ -300,7 +286,6 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUse
     p = ALLOC( Abc_ManRef_t, 1 );
     memset( p, 0, sizeof(Abc_ManRef_t) );
     p->vCube        = Vec_StrAlloc( 100 );
-    p->vLevNums     = Vec_IntAlloc( 100 );
     p->vVisited     = Vec_PtrAlloc( 100 );
     p->nNodeSizeMax = nNodeSizeMax;
     p->nConeSizeMax = nConeSizeMax;
@@ -328,9 +313,7 @@ Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUse
 void Abc_NtkManRefStop( Abc_ManRef_t * p )
 {
     Extra_StopManager( p->dd );
-//    Vec_IntFree( p->vReqTimes );
     Vec_PtrFree( p->vVisited );
-    Vec_IntFree( p->vLevNums );
     Vec_StrFree( p->vCube    );
     free( p );
 }
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 5cfa23ba..47618bf4 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -221,37 +221,6 @@ int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference )
     return Counter;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Replaces MFFC of the node by the new factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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(pNtk);
-    // create the new structure of nodes
-    assert( vForm->nSize == 1 || Vec_PtrSize(vFanins) < Vec_IntSize(vForm) );
-    pNodeNew = Abc_NodeStrashDec( pNtk->pManFunc, vFanins, vForm );
-    // in some cases, the new node may have a minor redundancy 
-    // (has to do with the precomputed subgraph library)
-    if ( !Abc_AigNodeIsAcyclic( Abc_ObjRegular(pNodeNew), pNode ) )
-        return;
-    // remove the old nodes
-    Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew );
-    // compare the gains
-    nNodesNew = Abc_NtkNodeNum(pNtk);
-    assert( nGain <= nNodesOld - nNodesNew );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index b17e2394..c77c0d70 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     assert( nFaninMax > 1 );
 
     // print a warning about choice nodes
-    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the AIG are removed by renoding.\n" );
 
     // define the boundary
diff --git a/src/base/abc/abcRewrite.c b/src/base/abc/abcRewrite.c
index f28aaa42..75fe1627 100644
--- a/src/base/abc/abcRewrite.c
+++ b/src/base/abc/abcRewrite.c
@@ -20,7 +20,7 @@
 
 #include "abc.h"
 #include "rwr.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -85,13 +85,12 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros );
         if ( nGain > 0 || nGain == 0 && fUseZeros )
         {
-            Vec_Int_t * vForm   = Rwr_ManReadDecs(pManRwr);
-            Vec_Ptr_t * vFanins = Rwr_ManReadFanins(pManRwr);
-            int fCompl          = Rwr_ManReadCompl(pManRwr);
+            Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
+            int fCompl           = Rwr_ManReadCompl(pManRwr);
             // complement the FF if needed
-            if ( fCompl ) Ft_FactorComplement( vForm );
-            Abc_NodeUpdate( pNode, vFanins, vForm, nGain );
-            if ( fCompl ) Ft_FactorComplement( vForm );
+            if ( fCompl ) Dec_GraphComplement( pGraph );
+            Dec_GraphUpdateNetwork( pNode, pGraph, nGain );
+            if ( fCompl ) Dec_GraphComplement( pGraph );
         }
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index a3e522cb..ee59cf43 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -55,7 +55,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode )
     char * pNameOut;
 
     assert( Abc_NtkIsBddLogic(pNode->pNtk) );
-    // create the file names
+    // create the file name
     Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
     // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
@@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
-    // create the file names
+    // create the file name
     Abc_ShowGetFileName( pNtk->pName, FileNameDot );
     // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
@@ -119,7 +119,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Visualizes reconvergence driven cut at the node.]
+  Synopsis    [Visualizes a reconvergence driven cut at the node.]
 
   Description []
                
@@ -158,7 +158,7 @@ void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
     Vec_PtrForEachEntry( vNodesTfo, pTemp, i )
         Vec_PtrPushUnique( vInside, pTemp );
 
-    // create the file names
+    // create the file name
     Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
     // check that the file can be opened
     if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 0a28c3c1..935f1300 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -20,7 +20,7 @@
 
 #include "abc.h"
 #include "extra.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -59,7 +59,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     if ( Abc_NtkIsBddLogic(pNtk) )
         Abc_NtkBddToSop(pNtk);
     // print warning about choice nodes
-    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // perform strashing
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
@@ -188,9 +188,6 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     // consider the case when the graph is an AIG
     if ( Abc_NtkIsStrash(pNode->pNtk) )
     {
-//        Abc_Obj_t * pChild0, * pChild1;
-//        pChild0 = Abc_ObjFanin0(pNode);
-//        pChild1 = Abc_ObjFanin1(pNode);
         if ( Abc_NodeIsConst(pNode) )
             return Abc_AigConst1(pMan);
         return Abc_AigAnd( pMan, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
@@ -202,14 +199,9 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     else
         pSop = pNode->pData;
 
-    // consider the cconstant node
+    // consider the constant node
     if ( Abc_NodeIsConst(pNode) )
-    {
-        // check if the SOP is constant
-        if ( Abc_SopIsConst1(pSop) )
-            return Abc_AigConst1(pMan);
-        return Abc_ObjNot( Abc_AigConst1(pMan) );
-    }
+        return Abc_ObjNotCond( Abc_AigConst1(pMan), Abc_SopIsConst0(pSop) );
 
     // decide when to use factoring
     if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
@@ -273,199 +265,21 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop
 ***********************************************************************/
 Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pSop )
 {
-    Vec_Int_t * vForm;
-    Vec_Ptr_t * vAnds;
-    Abc_Obj_t * pAnd, * pFanin;
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Abc_Obj_t * pAnd;
     int i;
-    // derive the factored form
-    vForm = Ft_Factor( pSop );
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
     // collect the fanins
-    vAnds = Vec_PtrAlloc( 20 );
-    Abc_ObjForEachFanin( pRoot, pFanin, i )
-        Vec_PtrPush( vAnds, pFanin->pCopy );
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
     // perform strashing
-    pAnd = Abc_NodeStrashDec( pMan, vAnds, vForm );
-    Vec_PtrFree( vAnds );
-    Vec_IntFree( vForm );
-    return pAnd;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Strashes the factored form into the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NodeStrashDec( Abc_Aig_t * pMan, Vec_Ptr_t * vFanins, Vec_Int_t * vForm )
-{
-    Abc_Obj_t * pAnd, * pAnd0, * pAnd1;
-    Ft_Node_t * pFtNode;
-    int i, nVars;
-
-    // sanity checks
-    nVars = Ft_FactorGetNumVars( vForm );
-    assert( nVars >= 0 );
-    assert( vForm->nSize > nVars );
-
-    // check for constant function
-    pFtNode = Ft_NodeRead( vForm, 0 );
-    if ( pFtNode->fConst )
-        return Abc_ObjNotCond( Abc_AigConst1(pMan), pFtNode->fCompl );
-    assert( nVars == vFanins->nSize );
-
-    // compute the function of other nodes
-    for ( i = nVars; i < vForm->nSize; i++ )
-    {
-        pFtNode = Ft_NodeRead( vForm, i );
-        pAnd0   = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin0], pFtNode->fCompl0 ); 
-        pAnd1   = Abc_ObjNotCond( vFanins->pArray[pFtNode->iFanin1], pFtNode->fCompl1 ); 
-        pAnd    = Abc_AigAnd( pMan, pAnd0, pAnd1 );
-        Vec_PtrPush( vFanins, pAnd );
-//printf( "Adding " );  Abc_AigPrintNode( pAnd );
-    }
-    assert( vForm->nSize = vFanins->nSize );
-
-    // complement the result if necessary
-    pFtNode = Ft_NodeReadLast( vForm );
-    pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl );
+    pAnd = Dec_GraphToNetwork( pMan, pFForm );
+    Dec_GraphFree( pFForm );
     return pAnd;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of new nodes added when using this factored form,]
-
-  Description [Returns NodeMax + 1 if the number of nodes and levels exceeded 
-  the given limit or the number of levels exceeded the maximum allowed level.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeStrashDecCount( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, Vec_Int_t * vForm, Vec_Int_t * vLevels, int NodeMax, int LevelMax )
-{
-    Abc_Obj_t * pAnd, * pAnd0, * pAnd1, * pTop;
-    Ft_Node_t * pFtNode;
-    int i, nVars, LevelNew, LevelOld, Counter;
-
-    // sanity checks
-    nVars = Ft_FactorGetNumVars( vForm );
-    assert( nVars >= 0 );
-    assert( vForm->nSize > nVars );
-
-    // check for constant function
-    pFtNode = Ft_NodeRead( vForm, 0 );
-    if ( pFtNode->fConst )
-        return 0;
-    assert( nVars == vFanins->nSize ); 
-
-    // set the levels
-    Vec_IntClear( vLevels );
-    Vec_PtrForEachEntry( vFanins, pAnd, i )
-        Vec_IntPush( vLevels, Abc_ObjRegular(pAnd)->Level );
-
-    // compute the function of other nodes
-    Counter = 0;
-    for ( i = nVars; i < vForm->nSize; i++ )
-    {
-        pFtNode = Ft_NodeRead( vForm, i );
-        // check for buffer/inverter
-        if ( pFtNode->iFanin0 == pFtNode->iFanin1 )
-        {
-            assert( vForm->nSize == nVars + 1 );
-            pAnd = Vec_PtrEntry(vFanins, pFtNode->iFanin0);  
-            pAnd = Abc_ObjNotCond( pAnd, pFtNode->fCompl );
-            Vec_PtrPush( vFanins, pAnd );
-            break;
-        }
-
-        pAnd0   = Vec_PtrEntry(vFanins, pFtNode->iFanin0);  
-        pAnd1   = Vec_PtrEntry(vFanins, pFtNode->iFanin1);  
-        if ( pAnd0 && pAnd1 )
-        {
-            pAnd0 = Abc_ObjNotCond( pAnd0, pFtNode->fCompl0 );
-            pAnd1 = Abc_ObjNotCond( pAnd1, pFtNode->fCompl1 );
-            pAnd  = Abc_AigAndLookup( pMan, pAnd0, pAnd1 );
-        }
-        else
-            pAnd = NULL;
-        // count the number of added nodes
-        if ( pAnd == NULL || Abc_NodeIsTravIdCurrent( Abc_ObjRegular(pAnd) ) )
-        {
-            if ( pAnd )
-            {
-//printf( "Reusing labeled " );  Abc_AigPrintNode( pAnd );
-            }
-            Counter++;
-            if ( Counter > NodeMax )
-            {
-                Vec_PtrShrink( vFanins, nVars );
-                return -1;
-            }
-        }
-        else
-        {
-//printf( "Reusing " );  Abc_AigPrintNode( pAnd );
-        }
-
-        // count the number of new levels
-        LevelNew = -1;
-        if ( pAnd )
-        {
-            if ( Abc_ObjRegular(pAnd) == Abc_AigConst1(pMan) )
-                LevelNew = 0;
-            else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd0) )
-                LevelNew = (int)Abc_ObjRegular(pAnd0)->Level;
-            else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) )
-                LevelNew = (int)Abc_ObjRegular(pAnd1)->Level;
-        }
-        if ( LevelNew == -1 )
-            LevelNew = 1 + ABC_MAX( Vec_IntEntry(vLevels, pFtNode->iFanin0), Vec_IntEntry(vLevels, pFtNode->iFanin1) );
-
-//        assert( pAnd == NULL || LevelNew == LevelOld );
-        if ( pAnd ) 
-        {
-            LevelOld = (int)Abc_ObjRegular(pAnd)->Level;
-            if ( LevelNew != LevelOld ) 
-            {
-                int x = 0;
-                Abc_Obj_t * pFanin0, * pFanin1;
-                pFanin0 = Abc_ObjFanin0( Abc_ObjRegular(pAnd) );
-                pFanin1 = Abc_ObjFanin1( Abc_ObjRegular(pAnd) );
-                x = 0;
-            }
-        }
-
-        if ( LevelNew > LevelMax )
-        {
-            Vec_PtrShrink( vFanins, nVars );
-            return -1;
-        }
-        Vec_PtrPush( vFanins, pAnd );
-        Vec_IntPush( vLevels, LevelNew );
-    }
-    assert( vForm->nSize = vFanins->nSize );
-
-    // check if this is the same form
-    pTop = Vec_PtrEntryLast(vFanins);
-    if ( Abc_ObjRegular(pTop) == pRoot )
-    {
-        assert( !Abc_ObjIsComplement(pTop) );
-        Vec_PtrShrink( vFanins, nVars );
-        return -1;
-    }
-    Vec_PtrShrink( vFanins, nVars );
-    return Counter;
-}
-
-
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcTiming.c b/src/base/abc/abcTiming.c
index 032d074c..b8524bd5 100644
--- a/src/base/abc/abcTiming.c
+++ b/src/base/abc/abcTiming.c
@@ -252,7 +252,7 @@ void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk )
         pTime = ppTimes[pObj->Id];
         if ( pTime->Worst != -ABC_INFINITY )
             continue;
-        *pTime = pNtk->pManTime->tArrDef;
+        *pTime = pNtk->pManTime->tReqDef;
     }
     // set the 0 arrival times for latches and constant nodes
     ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
@@ -380,16 +380,16 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
     // set the default timing
     pNtkNew->pManTime->tArrDef = pNtkOld->pManTime->tArrDef;
     pNtkNew->pManTime->tReqDef = pNtkOld->pManTime->tReqDef;
-    // set the PI timing
+    // set the CI timing
     ppTimesOld = (Abc_Time_t **)pNtkOld->pManTime->vArrs->pArray;
     ppTimesNew = (Abc_Time_t **)pNtkNew->pManTime->vArrs->pArray;
-    Abc_NtkForEachPi( pNtkOld, pObj, i )
-        *ppTimesNew[ Abc_NtkPi(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ];
-    // set the PO timing
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        *ppTimesNew[ Abc_NtkCi(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ];
+    // set the CO timing
     ppTimesOld = (Abc_Time_t **)pNtkOld->pManTime->vReqs->pArray;
     ppTimesNew = (Abc_Time_t **)pNtkNew->pManTime->vReqs->pArray;
-    Abc_NtkForEachPo( pNtkOld, pObj, i )
-        *ppTimesNew[ Abc_NtkPo(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ];
+    Abc_NtkForEachCo( pNtkOld, pObj, i )
+        *ppTimesNew[ Abc_NtkCo(pNtkNew,i)->Id ] = *ppTimesOld[ pObj->Id ];
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 2c460301..7a6a705d 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -21,7 +21,7 @@
 #include "abc.h"
 #include "main.h"
 #include "mio.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -118,16 +118,18 @@ int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk )
 {
-    Vec_Int_t * vFactor;
+    Dec_Graph_t * pFactor;
     Abc_Obj_t * pNode;
     int nNodes, i;
     assert( Abc_NtkHasSop(pNtk) );
     nNodes = 0;
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        vFactor = Ft_Factor( pNode->pData );
-        nNodes += Ft_FactorGetNumNodes(vFactor);
-        Vec_IntFree( vFactor );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        pFactor = Dec_Factor( pNode->pData );
+        nNodes += 1 + Dec_GraphNodeNum(pFactor);
+        Dec_GraphFree( pFactor );
     }
     return nNodes;
 }
@@ -224,6 +226,49 @@ double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of exors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += pNode->fExor;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if it is an AIG with choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter;
+    if ( !Abc_NtkIsStrash(pNtk) )
+        return 0;
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += Abc_NodeIsAigChoice( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the maximum number of fanins.]
 
   Description []
@@ -451,26 +496,6 @@ void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
-  Synopsis    [Marks and counts the number of exors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkCountExors( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i, Counter = 0;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        Counter += pNode->fExor;
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Returns 1 if the node is the root of EXOR/NEXOR.]
 
   Description []
@@ -634,29 +659,6 @@ Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_O
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if it is an AIG with choice nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    int i, Counter;
-    if ( !Abc_NtkIsStrash(pNtk) )
-        return 0;
-    Counter = 0;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        Counter += Abc_NodeIsAigChoice( pNode );
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Prepares two network for a two-argument command similar to "verify".]
 
   Description []
@@ -666,7 +668,7 @@ int Abc_NtkCountChoiceNodes( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkPrepareCommand( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, 
+int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, 
     Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 )
 {
     int fCheck = 1;
@@ -837,234 +839,6 @@ int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 )
-{
-    int Diff = strcmp( (char *)(*pp1)->pCopy, (char *)(*pp2)->pCopy );
-    if ( Diff < 0 )
-        return -1;
-    if ( Diff > 0 ) 
-        return 1;
-    return 0; 
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Gets fanin node names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pFanin;
-    int i;
-    vNodes = Vec_PtrAlloc( 100 );
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Gets fanin node names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames )
-{
-    Vec_Ptr_t * vNames;
-    char Buffer[5];
-    int i;
-
-    vNames = Vec_PtrAlloc( nNames );
-    for ( i = 0; i < nNames; i++ )
-    {
-        if ( nNames < 26 )
-        {
-            Buffer[0] = 'a' + i;
-            Buffer[1] = 0;
-        }
-        else
-        {
-            Buffer[0] = 'a' + i%26;
-            Buffer[1] = '0' + i/26;
-            Buffer[2] = 0;
-        }
-        Vec_PtrPush( vNames, util_strsav(Buffer) );
-    }
-    return vNames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Gets fanin node names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeFreeNames( Vec_Ptr_t * vNames )
-{
-    int i;
-    if ( vNames == NULL )
-        return;
-    for ( i = 0; i < vNames->nSize; i++ )
-        free( vNames->pArray[i] );
-    Vec_PtrFree( vNames );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the CI or CO names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos )
-{
-    Abc_Obj_t * pObj;
-    char ** ppNames;
-    int i;
-    if ( fCollectCos )
-    {
-        ppNames = ALLOC( char *, Abc_NtkCoNum(pNtk) );
-        Abc_NtkForEachCo( pNtk, pObj, i )
-            ppNames[i] = Abc_ObjName(pObj);
-    }
-    else
-    {
-        ppNames = ALLOC( char *, Abc_NtkCiNum(pNtk) );
-        Abc_NtkForEachCi( pNtk, pObj, i )
-            ppNames[i] = Abc_ObjName(pObj);
-    }
-    return ppNames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Orders PIs/POs/latches alphabetically.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkAlphaOrderSignals( Abc_Ntk_t * pNtk, int fComb )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    // temporarily store the names in the copy field
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
-    // order objects alphabetically
-    qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), 
-        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-    qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), 
-        (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-    // if the comparison if combinational (latches as PIs/POs), order them too
-    if ( fComb )
-    {
-        qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), 
-            (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-        // add latches to make COs
-        Abc_NtkForEachLatch( pNtk, pObj, i )
-        {
-            Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj );
-            Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj );
-        }
-    }
-    // clean the copy fields
-    Abc_NtkForEachPi( pNtk, pObj, i )
-        pObj->pCopy = NULL;
-    Abc_NtkForEachPo( pNtk, pObj, i )
-        pObj->pCopy = NULL;
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-        pObj->pCopy = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
-{
-    stmm_table * tObj2NameNew;
-    Abc_Obj_t * pObj;
-    char Buffer[100];
-    char * pNameNew;
-    int Length, i;
-
-    tObj2NameNew = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPiNum(pNtk) );
-    Abc_NtkForEachPi( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "pi%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkPoNum(pNtk) );
-    Abc_NtkForEachPo( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "po%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    // create new names and add them to the table
-    Length = Extra_Base10Log( Abc_NtkLatchNum(pNtk) );
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        sprintf( Buffer, "lat%0*d", Length, i );
-        pNameNew = Abc_NtkRegisterName( pNtk, Buffer );
-        stmm_insert( tObj2NameNew, (char *)pObj, pNameNew );
-    }
-    stmm_free_table( pNtk->tObj2Name );
-    pNtk->tObj2Name = tObj2NameNew;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Creates the array of fanout counters.]
 
   Description []
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 7d88e52d..97258c81 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -45,7 +45,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     FILE * pFile;
     Abc_Obj_t * pNode, * pTemp, * pPrev;
     int LevelMin, LevelMax, fHasCos, Level, i;
-    int Limit = 200;
+    int Limit = 300;
 
     if ( vNodes->nSize < 1 )
     {
@@ -109,8 +109,10 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
 //  fprintf( pFile, "ranksep = 0.5;\n" );
 //  fprintf( pFile, "nodesep = 0.5;\n" );
     fprintf( pFile, "center = true;\n" );
+//  fprintf( pFile, "orientation = landscape;\n" );
 //  fprintf( pFile, "edge [fontsize = 10];\n" );
 //  fprintf( pFile, "edge [dir = none];\n" );
+    fprintf( pFile, "edge [dir = back];\n" );
     fprintf( pFile, "\n" );
 
     // labels on the left of the picture
@@ -194,8 +196,9 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         {
             if ( !Abc_ObjIsCo(pNode) )
                 continue;
-            fprintf( pFile, "  Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
-            fprintf( pFile, ", shape = invtriangle" );
+            fprintf( pFile, "  Node%d%s [label = \"%s%s\"", pNode->Id, 
+                (Abc_ObjIsLatch(pNode)? "_in":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_in":"") );
+            fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"invtriangle") );
             if ( pNode->fMarkB )
                 fprintf( pFile, ", style = filled" );
             fprintf( pFile, ", color = coral, fillcolor = coral" );
@@ -240,8 +243,9 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         {
             if ( !Abc_ObjIsCi(pNode) )
                 continue;
-            fprintf( pFile, "  Node%d [label = \"%s\"", pNode->Id, Abc_ObjName(pNode) );
-            fprintf( pFile, ", shape = triangle" );
+            fprintf( pFile, "  Node%d%s [label = \"%s%s\"", pNode->Id, 
+                (Abc_ObjIsLatch(pNode)? "_out":""), Abc_ObjName(pNode), (Abc_ObjIsLatch(pNode)? "_out":"") );
+            fprintf( pFile, ", shape = %s", (Abc_ObjIsLatch(pNode)? "box":"triangle") );
             if ( pNode->fMarkB )
                 fprintf( pFile, ", style = filled" );
             fprintf( pFile, ", color = coral, fillcolor = coral" );
@@ -258,7 +262,8 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
     {
         if ( (int)pNode->Level != LevelMax )
             continue;
-        fprintf( pFile, "title2 -> Node%d [style = invis];\n", pNode->Id );
+        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id, 
+            (Abc_ObjIsLatch(pNode)? "_in":"") );
     }
 
     // generate edges
@@ -269,10 +274,10 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         // generate the edge from this node to the next
         if ( Abc_ObjFanin0(pNode)->fMarkC )
         {
-            fprintf( pFile, "Node%d",  pNode->Id );
+            fprintf( pFile, "Node%d%s",  pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") );
             fprintf( pFile, " -> " );
-            fprintf( pFile, "Node%d",  Abc_ObjFaninId0(pNode) );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" );
+            fprintf( pFile, "Node%d%s",  Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
+            fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
             fprintf( pFile, ";\n" );
         }
         if ( Abc_ObjFaninNum(pNode) == 1 )
@@ -282,8 +287,8 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
         {
             fprintf( pFile, "Node%d",  pNode->Id );
             fprintf( pFile, " -> " );
-            fprintf( pFile, "Node%d",  Abc_ObjFaninId1(pNode) );
-            fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" );
+            fprintf( pFile, "Node%d%s",  Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
+            fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
             fprintf( pFile, ";\n" );
         }
         // generate the edges between the equivalent nodes
@@ -295,7 +300,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow,
                 fprintf( pFile, "Node%d",  pPrev->Id );
                 fprintf( pFile, " -> " );
                 fprintf( pFile, "Node%d",  pTemp->Id );
-                fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" );
+                fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dotted" : "bold" );
                 fprintf( pFile, ";\n" );
                 pPrev = pTemp;
             }
diff --git a/src/base/io/ioWriteDot_old.c b/src/base/io/ioWriteDot_old.c
new file mode 100644
index 00000000..59bbbde3
--- /dev/null
+++ b/src/base/io/ioWriteDot_old.c
@@ -0,0 +1,325 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteDot.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write the graph structure of AIG in DOT.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteDot.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the graph structure of AIG in DOT.]
+
+  Description [Useful for graph visualization using tools such as GraphViz: 
+  http://www.graphviz.org/]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode, * pFanin, * pPrev, * pTemp;
+    int LevelMin, LevelMax, fHasCos, Level, i;
+    int Limit = 200;
+
+    if ( vNodes->nSize < 1 )
+    {
+        printf( "The set has no nodes. DOT file is not written.\n" );
+        return;
+    }
+
+    if ( vNodes->nSize > Limit )
+    {
+        printf( "The set has more than %d nodes. DOT file is not written.\n", Limit );
+        return;
+    }
+
+    // start the output file
+    if ( (pFile = fopen( pFileName, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+        return;
+    }
+
+    // mark the nodes from the set
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        pNode->fMarkC = 1;
+    if ( vNodesShow )
+        Vec_PtrForEachEntry( vNodesShow, pNode, i )
+            pNode->fMarkB = 1;
+
+    // find the largest and the smallest levels
+    LevelMin = 10000;
+    LevelMax = -1;
+    fHasCos  = 0;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsCo(pNode) )
+        {
+            fHasCos = 1;
+            continue;
+        }
+        if ( LevelMin > (int)pNode->Level )
+            LevelMin = pNode->Level;
+        if ( LevelMax < (int)pNode->Level )
+            LevelMax = pNode->Level;
+    }
+
+    // set the level of the CO nodes
+    if ( fHasCos )
+    {
+        LevelMax++;
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( Abc_ObjIsCo(pNode) )
+                pNode->Level = LevelMax;
+        }
+    }
+
+    // write the DOT header
+    fprintf( pFile, "# %s\n",  "AIG generated by ABC" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "digraph AIG {\n" );
+    fprintf( pFile, "size = \"7.5,10\";\n" );
+//  fprintf( pFile, "ranksep = 0.5;\n" );
+//  fprintf( pFile, "nodesep = 0.5;\n" );
+    fprintf( pFile, "center = true;\n" );
+//  fprintf( pFile, "edge [fontsize = 10];\n" );
+//    fprintf( pFile, "edge [dir = back];\n" );
+//  fprintf( pFile, "edge [dir = none];\n" );
+    fprintf( pFile, "\n" );
+
+    // labels on the left of the picture
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  node [shape = plaintext];\n" );
+    fprintf( pFile, "  edge [style = invis];\n" );
+    fprintf( pFile, "  LevelTitle1 [label=\"\"];\n" );
+    fprintf( pFile, "  LevelTitle2 [label=\"\"];\n" );
+    // generate node names with labels
+    for ( Level = LevelMax; Level >= LevelMin; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d", Level );
+        fprintf( pFile, " [label = " );
+        // label name
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "\"" );
+        fprintf( pFile, "];\n" );
+    }
+
+    // genetate the sequence of visible/invisible nodes to mark levels
+    fprintf( pFile, "  LevelTitle1 ->  LevelTitle2 ->" );
+    for ( Level = LevelMax; Level >= LevelMin; Level-- )
+    {
+        // the visible node name
+        fprintf( pFile, "  Level%d",  Level );
+        // the connector
+        if ( Level != LevelMin )
+            fprintf( pFile, " ->" );
+        else
+            fprintf( pFile, ";" );
+    }
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate title box on top
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle1;\n" );
+    fprintf( pFile, "  title1 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=20,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "%s", "AIG generated by ABC" );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "Benchmark \\\"%s\\\". ", pNtk->pName );
+    fprintf( pFile, "Time was %s. ",  Extra_TimeStamp() );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate statistics box
+    fprintf( pFile, "{\n" );
+    fprintf( pFile, "  rank = same;\n" );
+    fprintf( pFile, "  LevelTitle2;\n" );
+    fprintf( pFile, "  title2 [shape=plaintext,\n" );
+    fprintf( pFile, "          fontsize=18,\n" );
+    fprintf( pFile, "          fontname = \"Times-Roman\",\n" );
+    fprintf( pFile, "          label=\"" );
+    fprintf( pFile, "The set contains %d nodes and spans %d levels.", vNodes->nSize, LevelMax - LevelMin );
+    fprintf( pFile, "\\n" );
+    fprintf( pFile, "\"\n" );
+    fprintf( pFile, "         ];\n" );
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+
+    // generate the POs
+    if ( fHasCos )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  LevelMax );
+        // generat the PO nodes
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( !Abc_ObjIsCo(pNode) )
+                continue;
+            fprintf( pFile, "  Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":""), Abc_ObjName(pNode) );
+            fprintf( pFile, ", shape = invtriangle" );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, ", color = coral, fillcolor = coral" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate nodes of each rank
+    for ( Level = LevelMax - fHasCos; Level >= LevelMin && Level > 0; Level-- )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  Level );
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( (int)pNode->Level != Level )
+                continue;
+            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
+            fprintf( pFile, ", shape = ellipse" );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate the PI nodes if any
+    if ( LevelMin == 0 )
+    {
+        fprintf( pFile, "{\n" );
+        fprintf( pFile, "  rank = same;\n" );
+        // the labeling node of this level
+        fprintf( pFile, "  Level%d;\n",  LevelMin );
+        // generat the PO nodes
+        Vec_PtrForEachEntry( vNodes, pNode, i )
+        {
+            if ( !Abc_ObjIsCi(pNode) )
+                continue;
+            fprintf( pFile, "  Node%d%s [label = \"%s\"", pNode->Id, (Abc_ObjIsLatch(pNode)? "Bot":""), Abc_ObjName(pNode) );
+            fprintf( pFile, ", shape = triangle" );
+            if ( pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
+            fprintf( pFile, ", color = coral, fillcolor = coral" );
+            fprintf( pFile, "];\n" );
+        }
+        fprintf( pFile, "}" );
+        fprintf( pFile, "\n" );
+        fprintf( pFile, "\n" );
+    }
+
+    // generate invisible edges from the square down
+    fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( (int)pNode->Level != LevelMax )
+            continue;
+        fprintf( pFile, "title2 -> Node%d%s [style = invis];\n", pNode->Id );
+    }
+
+    // generate edges
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    { 
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
+        // generate the edge from this node to the next
+        pFanin = Abc_ObjFanin0(pNode);
+        if ( pFanin->fMarkC )
+        {
+            fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "Top":"") );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") );
+            fprintf( pFile, " [style = %s]", Abc_ObjFaninC0(pNode)? "dashed" : "bold" );
+            fprintf( pFile, ";\n" );
+        }
+        if ( Abc_ObjFaninNum(pNode) == 1 )
+            continue;
+        // generate the edge from this node to the next
+        pFanin = Abc_ObjFanin1(pNode);
+        if ( pFanin->fMarkC )
+        {
+            fprintf( pFile, "Node%d",  pNode->Id );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d%s",  pFanin->Id, (Abc_ObjIsLatch(pFanin)? "Bot":"") );
+            fprintf( pFile, " [style = %s]", Abc_ObjFaninC1(pNode)? "dashed" : "bold" );
+            fprintf( pFile, ";\n" );
+        }
+        // generate the edges between the equivalent nodes
+        pPrev = pNode;
+        for ( pTemp = pNode->pData; pTemp; pTemp = pTemp->pData )
+        {
+            if ( pTemp->fMarkC )
+            {
+                fprintf( pFile, "Node%d",  pPrev->Id );
+                fprintf( pFile, " -> " );
+                fprintf( pFile, "Node%d",  pTemp->Id );
+                fprintf( pFile, " [style = %s]", (pPrev->fPhase ^ pTemp->fPhase)? "dashed" : "bold" );
+                fprintf( pFile, ";\n" );
+                pPrev = pTemp;
+            }
+        }
+    }
+
+    fprintf( pFile, "}" );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+
+    // unmark the nodes from the set
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        pNode->fMarkC = 0;
+    if ( vNodesShow )
+        Vec_PtrForEachEntry( vNodesShow, pNode, i )
+            pNode->fMarkB = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/main/main.h b/src/base/main/main.h
index da47f154..72eec599 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -102,6 +102,9 @@ extern void            Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void
 extern void            Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib );
 extern void            Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib );
 
+extern void *          Abc_FrameReadManDd          ( Abc_Frame_t * pFrame );
+extern void *          Abc_FrameReadManDec         ( Abc_Frame_t * pFrame );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 2e9d9d41..09a750ea 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -20,6 +20,7 @@
 
 #include "mainInt.h"
 #include "abc.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -58,6 +59,9 @@ Abc_Frame_t * Abc_FrameAllocate()
     // set the starting step
     p->nSteps = 1;
     p->fBatchMode = 0;
+    // initialize decomposition manager
+    p->pManDec = Dec_ManStart();
+    p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     return p;
 }
 
@@ -75,6 +79,8 @@ Abc_Frame_t * Abc_FrameAllocate()
 ***********************************************************************/
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
+    Dec_ManStop( p->pManDec );
+    Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
     free( p );
     p = NULL;
@@ -417,17 +423,20 @@ Abc_Frame_t * Abc_FrameGetGlobalFrame()
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame )                     { return pFrame->pStored;  } 
-int         Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame )                     { return pFrame->nStored;  }
-void        Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk )   { pFrame->pStored  = pNtk;     } 
-void        Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored )        { pFrame->nStored  = nStored;  }
+Abc_Ntk_t * Abc_FrameReadNtkStore       ( Abc_Frame_t * pFrame )                     { return pFrame->pStored;    } 
+int         Abc_FrameReadNtkStoreSize   ( Abc_Frame_t * pFrame )                     { return pFrame->nStored;    }
+void        Abc_FrameSetNtkStore        ( Abc_Frame_t * pFrame, Abc_Ntk_t * pNtk )   { pFrame->pStored  = pNtk;   } 
+void        Abc_FrameSetNtkStoreSize    ( Abc_Frame_t * pFrame, int nStored )        { pFrame->nStored  = nStored;}
 
 void *      Abc_FrameReadLibLut         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibLut;    } 
 void *      Abc_FrameReadLibGen         ( Abc_Frame_t * pFrame )                     { return pFrame->pLibGen;    } 
 void *      Abc_FrameReadLibSuper       ( Abc_Frame_t * pFrame )                     { return pFrame->pLibSuper;  } 
-void        Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibLut   = pLib;   } 
-void        Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibGen   = pLib;   } 
-void        Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibSuper = pLib;   } 
+void        Abc_FrameSetLibLut          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibLut   = pLib;  } 
+void        Abc_FrameSetLibGen          ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibGen   = pLib;  } 
+void        Abc_FrameSetLibSuper        ( Abc_Frame_t * pFrame, void * pLib )        { pFrame->pLibSuper = pLib;  } 
+
+void *      Abc_FrameReadManDd          ( Abc_Frame_t * pFrame )                     { return pFrame->dd;         } 
+void *      Abc_FrameReadManDec         ( Abc_Frame_t * pFrame )                     { return pFrame->pManDec;    } 
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 557c4e2f..95d5b22d 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -66,6 +66,9 @@ struct Abc_Frame_t_
     // temporary storage for structural choices
     Abc_Ntk_t *     pStored;     // the stored networks
     int             nStored;     // the number of stored networks
+    // decomposition package
+    DdManager *     dd;          // temporary BDD package
+    void *          pManDec;     // decomposition manager
 
     void *          pLibLut;     // the current LUT library
     void *          pLibGen;     // the current genlib