Version abc50831

37 files changed, 3983 insertions, 280 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index 7c949ee0..0d911e79 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -36,8 +36,11 @@ static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowAig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -105,8 +108,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_symm",    Abc_CommandPrintSymms,       0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "show_aig",      Abc_CommandShowAig,          0 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
@@ -297,9 +303,10 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_io [-h]\n" );
+    fprintf( pErr, "usage: print_io [-h] <node>\n" );
     fprintf( pErr, "\t        prints the PIs/POs or fanins/fanouts of a node\n" );
     fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\tnode  : the node to print fanins/fanouts\n");
     return 1;
 }
 
@@ -629,13 +636,85 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fUseBdds;
+    int fNaive;
+    int fVerbose;
+    extern void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseBdds = 1;
+    fNaive   = 0;
+    fVerbose = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'b':
+            fUseBdds ^= 1;
+            break;
+        case 'n':
+            fNaive ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs.\n" );
+        return 1;
+    }
+    Abc_NtkSymmetries( pNtk, fUseBdds, fNaive, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_symm [-nbvh]\n" );
+    fprintf( pErr, "\t         computes symmetries of the PO functions\n" );
+    fprintf( pErr, "\t-b     : enable efficient BDD-based computation [default = %s].\n", fUseBdds? "yes": "no" );  
+    fprintf( pErr, "\t-n     : enable naive BDD-based computation [default = %s].\n", fNaive? "yes": "no" );  
+    fprintf( pErr, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     int c;
-    extern void Abc_NodePrintBdd( Abc_Obj_t * pNode );
+    extern void Abc_NodeShowBdd( Abc_Obj_t * pNode );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -662,7 +741,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
+        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" );
         return 1;
     }
 
@@ -678,7 +757,7 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
         return 1;
     }
-    Abc_NodePrintBdd( pNode );
+    Abc_NodeShowBdd( pNode );
     return 0;
 
 usage:
@@ -693,6 +772,168 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    int nNodeSizeMax;
+    int nConeSizeMax;
+    extern void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nNodeSizeMax = 10;
+    nConeSizeMax = ABC_INFINITY;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nNodeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nConeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Visualizing cuts only works for AIGs.\n" );
+        return 1;
+    }
+    if ( argc != util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+
+    pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+    if ( pNode == NULL )
+    {
+        fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+        return 1;
+    }
+    Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: show_cut [-N num] [-C num] [-h] <node>\n" );
+    fprintf( pErr, "       visualizes the cut of a node using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\t-N num : the max size of the cut to be computed [default = %d]\n", nNodeSizeMax );  
+    fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );  
+    fprintf( pErr, "\tnode   : the node to consider\n");
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Visualizing AIG can only be done for AIGs.\n" );
+        return 1;
+    }
+    Abc_NtkShowAig( pNtk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: show_aig [-h]\n" );
+    fprintf( pErr, "       visualizes the AIG with choices using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -745,7 +986,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
         Abc_NtkDelete( pNtk );
     }
@@ -783,6 +1024,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fAllNodes;
+    int fCleanup;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -790,14 +1032,18 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fAllNodes = 0;
+    fCleanup  = 1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF )
     {
         switch ( c )
         {
         case 'a':
             fAllNodes ^= 1;
             break;
+        case 'c':
+            fCleanup ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -812,7 +1058,7 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes );
+    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes, fCleanup );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Strashing has failed.\n" );
@@ -823,9 +1069,10 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: strash [-ah]\n" );
+    fprintf( pErr, "usage: strash [-ach]\n" );
     fprintf( pErr, "\t        transforms combinational logic into an AIG\n" );
     fprintf( pErr, "\t-a    : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
+    fprintf( pErr, "\t-c    : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -882,7 +1129,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
         if ( pNtkTemp == NULL )
         {
             fprintf( pErr, "Strashing before balancing has failed.\n" );
@@ -1274,7 +1521,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
         // get the new network
         if ( !Abc_NtkIsStrash(pNtk) )
         {
-            pNtkNew = Abc_NtkStrash( pNtk, 0 );
+            pNtkNew = Abc_NtkStrash( pNtk, 0, 0 );
             pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
             Abc_NtkDelete( pNtkNew );
         }
@@ -1732,7 +1979,7 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk, 0 );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -2424,7 +2671,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk, 0 );
+        pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
         Abc_NtkDelete( pNtk );
     }
@@ -2845,7 +3092,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsStrash(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtk, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before mapping has failed.\n" );
@@ -3087,8 +3334,10 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: sc [-h]\n" );
-    fprintf( pErr, "\t        performs superchoicing\n" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\t      performs superchoicing\n" );
+    fprintf( pErr, "\t      (accumulate: \"r file.blif; rsup; b; sc; f -ac; wb file_sc.blif\")\n" );
+    fprintf( pErr, "\t      (map without supergate library: \"r file_sc.blif; ft; map\")\n" );
+    fprintf( pErr, "\t-h  : print the command usage\n");
     return 1;
 }
 
@@ -3146,7 +3395,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk, 0 );
+        pNtk = Abc_NtkStrash( pNtk, 0, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index a3f7ddb7..ab457cc9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -51,7 +51,7 @@ typedef enum {
     ABC_TYPE_OTHER      // 5:  unused
 } Abc_NtkType_t;
 
-// functionality types
+// network functionality
 typedef enum { 
     ABC_FUNC_NONE,      // 0:  unknown
     ABC_FUNC_SOP,       // 1:  sum-of-products
@@ -155,13 +155,16 @@ struct Abc_Ntk_t_
     int              nPos;          // the number of primary outputs
     // the functionality manager 
     void *           pManFunc;      // AIG manager, BDD manager, or memory manager for SOPs
+    // the global functions (BDDs)
+    void *           pManGlob;      // the BDD manager
+    Vec_Ptr_t *      vFuncsGlob;    // the BDDs of CO functions
     // the timing manager (for mapped networks)
     Abc_ManTime_t *  pManTime;      // stores arrival/required times for all nodes
     // the cut manager (for AIGs)
     void *           pManCut;       // stores information about the cuts computed for the nodes
     // level information (for AIGs)
     int              LevelMax;      // maximum number of levels
-    Vec_Int_t *      vLevelsR;       // level in the reverse topological order 
+    Vec_Int_t *      vLevelsR;      // level in the reverse topological order 
     // the external don't-care if given
     Abc_Ntk_t *      pExdc;         // the EXDC network
     // miscellaneous data members
@@ -401,8 +404,11 @@ extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld
 extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
 extern void               Abc_AigPrintNode( Abc_Obj_t * pNode );
+extern bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
+/*=== abcBalance.c ==========================================================*/
+extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcCheck.c ==========================================================*/
 extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
@@ -410,7 +416,7 @@ extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t *
 /*=== abcCollapse.c ==========================================================*/
 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 );
+extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
 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 );
@@ -475,6 +481,7 @@ extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager
 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 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 /*=== abcLatch.c ==========================================================*/
 extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
@@ -519,13 +526,15 @@ extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
 /*=== abcReconv.c ==========================================================*/
-extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax );
+extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
-extern Vec_Ptr_t *        Abc_NtkManCutReadLeaves( Abc_ManCut_t * p );
+extern Vec_Ptr_t *        Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
+extern void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
 extern DdNode *           Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
 extern DdNode *           Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
-extern void               Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult );
+extern Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
 /*=== abcRefs.c ==========================================================*/
 extern int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
 extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
@@ -576,12 +585,11 @@ extern bool               Abc_SopCheck( char * pSop, int nFanins );
 extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
+extern Abc_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 );
-extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcSweep.c ==========================================================*/
 extern bool               Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
 extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
@@ -643,6 +651,7 @@ extern char **            Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollect
 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 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f71c0a15..9588f1e0 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -705,8 +705,10 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         assert( iFanin == 0 || iFanin == 1 );
         // get the new fanin
         pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
+        assert( Abc_ObjRegular(pFanin1) != pFanout );
         // get another fanin
         pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
+        assert( Abc_ObjRegular(pFanin2) != pFanout );
         // check if the node with these fanins exists
         if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
         { // such node exists (it may be a constant)
@@ -732,6 +734,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan )
         Abc_ObjRemoveFanins( pFanout );
         // recreate the old fanout with new fanins and add it to the table
         Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
+        assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) );
 
         // schedule the updated fanout for updating direct level
         assert( pFanout->fMarkA == 0 );
@@ -876,6 +879,7 @@ void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan )
             if ( pNode == NULL )
                 continue;
             assert( Abc_ObjIsNode(pNode) );
+            assert( (int)pNode->Level == i );
             // clean the mark
             assert( pNode->fMarkA == 1 );
             pNode->fMarkA = 0;
@@ -931,6 +935,7 @@ void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan )
             if ( pNode == NULL )
                 continue;
             assert( Abc_ObjIsNode(pNode) );
+            assert( Abc_NodeReadReverseLevel(pNode) == i );
             // clean the mark
             assert( pNode->fMarkB == 1 );
             pNode->fMarkB = 0;
@@ -1113,6 +1118,56 @@ void Abc_AigPrintNode( Abc_Obj_t * pNode )
     printf( "\n" );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the node has a combination loop of depth 1 or 2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot )
+{
+    Abc_Obj_t * pFanin0, * pFanin1;
+    Abc_Obj_t * pChild00, * pChild01;
+    Abc_Obj_t * pChild10, * pChild11;
+    if ( !Abc_NodeIsAigAnd(pNode) )
+        return 1;
+    pFanin0 = Abc_ObjFanin0(pNode);
+    pFanin1 = Abc_ObjFanin1(pNode);
+    if ( pRoot == pFanin0 || pRoot == pFanin1 )
+        return 0;
+    if ( Abc_ObjIsCi(pFanin0) )
+    {
+        pChild00 = NULL;
+        pChild01 = NULL;
+    }
+    else
+    {
+        pChild00 = Abc_ObjFanin0(pFanin0);
+        pChild01 = Abc_ObjFanin1(pFanin0);
+        if ( pRoot == pChild00 || pRoot == pChild01 )
+            return 0;
+    }
+    if ( Abc_ObjIsCi(pFanin1) )
+    {
+        pChild10 = NULL;
+        pChild11 = NULL;
+    }
+    else
+    {
+        pChild10 = Abc_ObjFanin0(pFanin1);
+        pChild11 = Abc_ObjFanin1(pFanin1);
+        if ( pRoot == pChild10 || pRoot == pChild11 )
+            return 0;
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcCollapse.c b/src/base/abc/abcCollapse.c
index e07636cc..a6eda7b3 100644
--- a/src/base/abc/abcCollapse.c
+++ b/src/base/abc/abcCollapse.c
@@ -25,7 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static DdNode *    Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
-static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
 
 ////////////////////////////////////////////////////////////////////////
@@ -47,26 +47,26 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
-    DdManager * dd;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
-    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
-    if ( dd == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
 
     // create the new network
-    pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
-    Abc_NtkFreeGlobalBdds( dd, pNtk );
+    pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
+    Abc_NtkFreeGlobalBdds( pNtk );
     if ( pNtkNew == NULL )
     {
-        Cudd_Quit( dd );
+        Cudd_Quit( pNtk->pManGlob );
+        pNtk->pManGlob = NULL;
         return NULL;
     }
-    Extra_StopManager( dd );
+    Extra_StopManager( pNtk->pManGlob );
+    pNtk->pManGlob = NULL;
 
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
@@ -96,12 +96,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
 {
     int fReorder = 1;
     ProgressBar * pProgress;
+    Vec_Ptr_t * vFuncsGlob;
     Abc_Obj_t * pNode;
     DdNode * bFunc;
     DdManager * dd;
     int i;
 
     // start the manager
+    assert( pNtk->pManGlob == NULL );
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     if ( fReorder )
         Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
@@ -114,6 +116,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
     pNode = Abc_AigConst1( pNtk->pManFunc );
     pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
 
+    vFuncsGlob = Vec_PtrAlloc( 100 );
     if ( fLatchOnly )
     {
         // construct the BDDs
@@ -129,8 +132,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
                 Cudd_Quit( dd );
                 return NULL;
             }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
-            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );   Cudd_Ref( bFunc );
+            Vec_PtrPush( vFuncsGlob, bFunc );
         }
         Extra_ProgressBarStop( pProgress );
     }
@@ -149,8 +152,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
                 Cudd_Quit( dd );
                 return NULL;
             }
-            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
-            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );   Cudd_Ref( bFunc );
+            Vec_PtrPush( vFuncsGlob, bFunc );
         }
         Extra_ProgressBarStop( pProgress );
     }
@@ -168,6 +171,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
         Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
         Cudd_AutodynDisable( dd );
     }
+    pNtk->pManGlob = dd;
+    pNtk->vFuncsGlob = vFuncsGlob;
     return dd;
 }
 
@@ -223,11 +228,12 @@ DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
 {
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
+    DdManager * dd = pNtk->pManGlob;
     int i;
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@@ -238,7 +244,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
     Extra_ProgressBarStop( pProgress );
@@ -281,17 +287,16 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pNode;
+    DdNode * bFunc;
     int i;
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        if ( pNode->pNext == NULL )
-            continue;
-        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-        pNode->pNext = NULL;
-    }
+    assert( pNtk->pManGlob );
+    assert( pNtk->vFuncsGlob );
+    Vec_PtrForEachEntry( pNtk->vFuncsGlob, bFunc, i )
+        Cudd_RecursiveDeref( pNtk->pManGlob, bFunc );
+    Vec_PtrFree( pNtk->vFuncsGlob );
+    pNtk->vFuncsGlob = NULL;
 }
 
 
diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c
index 9186ec5a..d6500803 100644
--- a/src/base/abc/abcCreate.c
+++ b/src/base/abc/abcCreate.c
@@ -818,7 +818,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
     // find the internal node
     if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
     {
-        printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName );
+        printf( "Name \"%s\" is not found among CIs/COs (internal name looks like this: \"[integer]\").\n", pName );
         return NULL;
     }
     Num = atoi( pName + 1 );
diff --git a/src/base/abc/abcDsd.c b/src/base/abc/abcDsd.c
index d1445e75..ccb52ffa 100644
--- a/src/base/abc/abcDsd.c
+++ b/src/base/abc/abcDsd.c
@@ -25,8 +25,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static Abc_Ntk_t *     Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
-static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose );
+static Abc_Ntk_t *     Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
 static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
 
@@ -58,25 +57,25 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
-    DdManager * dd;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
-    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
-    if ( dd == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
         return NULL;
     if ( fVerbose )
-        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
 
     // transform the result of mapping into a BDD network
-    pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort );
+    pNtkNew = Abc_NtkDsdInternal( pNtk, fVerbose, fPrint, fShort );
     if ( pNtkNew == NULL )
     {
-        Cudd_Quit( dd );
+        Cudd_Quit( pNtk->pManGlob );
+        pNtk->pManGlob = NULL;
         return NULL;
     }
-    Extra_StopManager( dd );
+    Extra_StopManager( pNtk->pManGlob );
+    pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
@@ -99,17 +98,33 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
 {
+    DdManager * dd = pNtk->pManGlob;
     Dsd_Manager_t * pManDsd;
     Abc_Ntk_t * pNtkNew;
+    DdNode * bFunc;
     char ** ppNamesCi, ** ppNamesCo;
+    Abc_Obj_t * pObj;
+    int i;
+
+    // complement the global functions
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        bFunc = Vec_PtrEntry(pNtk->vFuncsGlob, i);
+        Vec_PtrWriteEntry(pNtk->vFuncsGlob, i, Cudd_NotCond(bFunc, Abc_ObjFaninC0(pObj)) );
+    }
 
     // perform the decomposition
-    pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
-    Abc_NtkFreeGlobalBdds( dd, pNtk );
+    assert( Vec_PtrSize(pNtk->vFuncsGlob) == Abc_NtkCoNum(pNtk) );
+    pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
+    Dsd_Decompose( pManDsd, (DdNode **)pNtk->vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
+    Abc_NtkFreeGlobalBdds( pNtk );
     if ( pManDsd == NULL )
+    {
+        Cudd_Quit( dd );
         return NULL;
+    }
 
     // start the new network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
@@ -119,6 +134,8 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
     Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
     // finalize the new network
     Abc_NtkFinalize( pNtk, pNtkNew );
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     if ( fPrint )
     {
@@ -136,39 +153,6 @@ Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose,
 
 /**Function*************************************************************
 
-  Synopsis    [Performs DSD by creating the manager and decomposing the functions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose )
-{
-    Dsd_Manager_t * pManDsd;
-    DdNode ** pbFuncsGlo;
-    Abc_Obj_t * pNode;
-    int i;
-
-    // collect global functions into the array
-    pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) );
-//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) );
-    }
-
-    // start the DSD manager and decompose global functions
-    pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
-    Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) );
-    FREE( pbFuncsGlo );
-    return pManDsd;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Constructs the decomposed network.]
 
   Description []
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index bb7d8cfa..83735e47 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -433,7 +433,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     if ( pStore == NULL )
     {
         // start the stored network
-        pStore = Abc_NtkStrash( pNtk, 0 );
+        pStore = Abc_NtkStrash( pNtk, 0, 0 );
         if ( pStore == NULL )
         {
             printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index f616a258..44acb699 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -128,6 +128,57 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop, int nFanins )
     return bRes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Removes complemented SOP covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
+{
+    DdManager * dd;
+    DdNode * bFunc;
+    Vec_Str_t * vCube;
+    Abc_Obj_t * pNode;
+    int nFaninsMax, fFound, i;
+
+    assert( Abc_NtkIsSopLogic(pNtk) );
+
+    // check if there are nodes with complemented SOPs
+    fFound = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_SopIsComplement(pNode->pData) )
+        {
+            fFound = 1;
+            break;
+        }
+    if ( !fFound )
+        return;
+
+    // start the BDD package
+    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
+    if ( nFaninsMax == 0 )
+        printf( "Warning: The network has only constant nodes.\n" );
+    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+
+    // change the cover of negated nodes
+    vCube = Vec_StrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_SopIsComplement(pNode->pData) )
+        {
+            bFunc = Abc_ConvertSopToBdd( dd, pNode->pData, Abc_ObjFaninNum(pNode) );  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) );
+        }
+    Vec_StrFree( vCube );
+    Extra_StopManager( dd );
+}
 
 
 
diff --git a/src/base/abc/abcMiter.c b/src/base/abc/abcMiter.c
index b8bcec4d..a0426dc2 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_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
-    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
+    fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));
+    fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0));
     if ( pNtk1 && pNtk2 )
         pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 337dd43b..c7599f11 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -44,8 +44,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
     int Num;
 
-    fprintf( pFile, "%-15s:",       pNtk->pName );
-    fprintf( pFile, "  i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+    fprintf( pFile, "%-13s:",       pNtk->pName );
+    fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
     if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
diff --git a/src/base/abc/abcReconv.c b/src/base/abc/abcReconv.c
index e02ccba0..ea662799 100644
--- a/src/base/abc/abcReconv.c
+++ b/src/base/abc/abcReconv.c
@@ -30,14 +30,19 @@ struct Abc_ManCut_t_
     // user specified parameters
     int              nNodeSizeMax;  // the limit on the size of the supernode
     int              nConeSizeMax;  // the limit on the size of the containing cone
+    int              nNodeFanStop;  // the limit on the size of the supernode
+    int              nConeFanStop;  // the limit on the size of the containing cone
     // internal parameters
-    Vec_Ptr_t *      vFaninsNode;   // fanins of the supernode
-    Vec_Ptr_t *      vFaninsCone;   // fanins of the containing cone
+    Vec_Ptr_t *      vNodeLeaves;   // fanins of the collapsed node (the cut)
+    Vec_Ptr_t *      vConeLeaves;   // fanins of the containing cone
     Vec_Ptr_t *      vVisited;      // the visited nodes
+    Vec_Vec_t *      vLevels;       // the data structure to compute TFO nodes
+    Vec_Ptr_t *      vNodesTfo;     // the nodes in the TFO of the cut
 };
 
-static int   Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit );
-static void  Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+static int   Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit );
+static int   Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit );
+static void  Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -92,45 +97,142 @@ static inline void Abc_NodesUnmark( Vec_Ptr_t * vVisited )
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Abc_NodesUnmarkBoth( Vec_Ptr_t * vVisited )
+static inline void Abc_NodesUnmarkB( Vec_Ptr_t * vVisited )
 {
     Abc_Obj_t * pNode;
     int i;
     Vec_PtrForEachEntry( vVisited, pNode, i )
-        pNode->fMarkA = pNode->fMarkB = 0;
+        pNode->fMarkB = 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Evaluate the fanin cost.]
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
 
-  Description [Returns the number of fanins that will be brought in.
-  Returns large number if the node cannot be added.]
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
+static inline int Abc_NodeGetLeafCostOne( Abc_Obj_t * pNode, int nFaninLimit )
 {
-    Abc_Obj_t * pFanout;
-    int i;
-    assert( pNode->fMarkA == 1 );  // this node is in the TFI
-    assert( pNode->fMarkB == 1 );  // this node is in the constructed cone
-    // check the PI node
+    int Cost;
+    // make sure the node is in the construction zone
+    assert( pNode->fMarkB == 1 );  
+    // cannot expand over the PI node
+    if ( Abc_ObjIsCi(pNode) )
+        return 999;
+    // get the cost of the cone
+    Cost = (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+    // always accept if the number of leaves does not increase
+    if ( Cost < 2 )
+        return Cost;
+    // skip nodes with many fanouts
+    if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+        return 999;
+    // return the number of nodes that will be on the leaves if this node is removed
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
+
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_NodeGetLeafCostTwo( Abc_Obj_t * pNode, int nFaninLimit, 
+    Abc_Obj_t ** ppLeafToAdd, Abc_Obj_t ** pNodeToMark1, Abc_Obj_t ** pNodeToMark2 )
+{
+    Abc_Obj_t * pFanin0, * pFanin1, * pTemp;
+    Abc_Obj_t * pGrand, * pGrandToAdd;
+    // make sure the node is in the construction zone
+    assert( pNode->fMarkB == 1 );  
+    // cannot expand over the PI node
     if ( Abc_ObjIsCi(pNode) )
         return 999;
     // skip nodes with many fanouts
-    if ( Abc_ObjFanoutNum(pNode) > 5 )
+//    if ( Abc_ObjFanoutNum(pNode) > nFaninLimit )
+//        return 999;
+    // get the children
+    pFanin0 = Abc_ObjFanin0(pNode);
+    pFanin1 = Abc_ObjFanin1(pNode);
+    assert( !pFanin0->fMarkB && !pFanin1->fMarkB );
+    // count the number of unique grandchildren that will be included
+    // return infinite cost if this number if more than 1
+    if ( Abc_ObjIsCi(pFanin0) && Abc_ObjIsCi(pFanin1) )
         return 999;
-    // check the fanouts
-    Abc_ObjForEachFanout( pNode, pFanout, i )
-        if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // the fanout is in the TFI but not in the cone
+    // consider the special case when a non-CI fanin can be dropped
+    if ( !Abc_ObjIsCi(pFanin0) && Abc_ObjFanin0(pFanin0)->fMarkB && Abc_ObjFanin1(pFanin0)->fMarkB )
+    {
+        *ppLeafToAdd  = pFanin1;
+        *pNodeToMark1 = pFanin0;
+        *pNodeToMark2 = NULL;
+        return 1;
+    }
+    if ( !Abc_ObjIsCi(pFanin1) && Abc_ObjFanin0(pFanin1)->fMarkB && Abc_ObjFanin1(pFanin1)->fMarkB )
+    {
+        *ppLeafToAdd  = pFanin0;
+        *pNodeToMark1 = pFanin1;
+        *pNodeToMark2 = NULL;
+        return 1;
+    }
+
+    // make the first node CI if any
+    if ( Abc_ObjIsCi(pFanin1) )
+        pTemp = pFanin0, pFanin0 = pFanin1, pFanin1 = pTemp;
+    // consider the first node
+    pGrandToAdd = NULL;
+    if ( Abc_ObjIsCi(pFanin0) )
+    {
+        *pNodeToMark1 = NULL;
+        pGrandToAdd = pFanin0;
+    }
+    else
+    {
+        *pNodeToMark1 = pFanin0;
+        pGrand = Abc_ObjFanin0(pFanin0);
+        if ( !pGrand->fMarkB )
+        {
+            if ( pGrandToAdd && pGrandToAdd != pGrand )
+                return 999;
+            pGrandToAdd = pGrand;
+        }
+        pGrand = Abc_ObjFanin1(pFanin0);
+        if ( !pGrand->fMarkB )
+        {
+            if ( pGrandToAdd && pGrandToAdd != pGrand )
+                return 999;
+            pGrandToAdd = pGrand;
+        }
+    }
+    // consider the second node
+    *pNodeToMark2 = pFanin1;
+    pGrand = Abc_ObjFanin0(pFanin1);
+    if ( !pGrand->fMarkB )
+    {
+        if ( pGrandToAdd && pGrandToAdd != pGrand )
+            return 999;
+        pGrandToAdd = pGrand;
+    }
+    pGrand = Abc_ObjFanin1(pFanin1);
+    if ( !pGrand->fMarkB )
+    {
+        if ( pGrandToAdd && pGrandToAdd != pGrand )
             return 999;
-    // the fanouts are in the TFI and inside the constructed cone
-    // return the number of fanins that will be on the boundary if this node is added
-    return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+        pGrandToAdd = pGrand;
+    }
+    assert( pGrandToAdd != NULL );
+    *ppLeafToAdd = pGrandToAdd;
+    return 1;
 }
 
 
@@ -153,117 +255,206 @@ Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain
     assert( !Abc_ObjIsComplement(pRoot) );
     assert( Abc_ObjIsNode(pRoot) );
 
-    // mark TFI using fMarkA
+    // start the visited nodes and mark them
     Vec_PtrClear( p->vVisited );
-    Abc_NodesMarkCollect_rec( pRoot, p->vVisited );
-
-    // start the cut 
-    Vec_PtrClear( p->vFaninsNode );
-    Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin0(pRoot) );
-    Vec_PtrPush( p->vFaninsNode, Abc_ObjFanin1(pRoot) );
+    Vec_PtrPush( p->vVisited, pRoot );
+    Vec_PtrPush( p->vVisited, Abc_ObjFanin0(pRoot) );
+    Vec_PtrPush( p->vVisited, Abc_ObjFanin1(pRoot) );
     pRoot->fMarkB = 1;
     Abc_ObjFanin0(pRoot)->fMarkB = 1;
     Abc_ObjFanin1(pRoot)->fMarkB = 1;
 
+    // start the cut 
+    Vec_PtrClear( p->vNodeLeaves );
+    Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin0(pRoot) );
+    Vec_PtrPush( p->vNodeLeaves, Abc_ObjFanin1(pRoot) );
+
     // compute the cut
-    while ( Abc_NodeFindCut_int( p->vFaninsNode, p->nNodeSizeMax ) );
-    assert( Vec_PtrSize(p->vFaninsNode) <= p->nNodeSizeMax );
+    while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vNodeLeaves, p->nNodeSizeMax, p->nNodeFanStop ) );
+    assert( Vec_PtrSize(p->vNodeLeaves) <= p->nNodeSizeMax );
 
     // return if containing cut is not requested
     if ( !fContain )
     {
-        // unmark TFI using fMarkA and fMarkB
-        Abc_NodesUnmarkBoth( p->vVisited );
-        return p->vFaninsNode;
+        // unmark both fMarkA and fMarkB in tbe TFI
+        Abc_NodesUnmarkB( p->vVisited );
+        return p->vNodeLeaves;
     }
 
+//printf( "\n\n\n" );
     // compute the containing cut
     assert( p->nNodeSizeMax < p->nConeSizeMax );
     // copy the current boundary
-    Vec_PtrClear( p->vFaninsCone );
-    Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
-        Vec_PtrPush( p->vFaninsCone, pNode );
+    Vec_PtrClear( p->vConeLeaves );
+    Vec_PtrForEachEntry( p->vNodeLeaves, pNode, i )
+        Vec_PtrPush( p->vConeLeaves, pNode );
     // compute the containing cut
-    while ( Abc_NodeFindCut_int( p->vFaninsCone, p->nConeSizeMax ) );
-    assert( Vec_PtrSize(p->vFaninsCone) <= p->nConeSizeMax );
+    while ( Abc_NodeBuildCutLevelOne_int( p->vVisited, p->vConeLeaves, p->nConeSizeMax, p->nConeFanStop ) );
+    assert( Vec_PtrSize(p->vConeLeaves) <= p->nConeSizeMax );
     // unmark TFI using fMarkA and fMarkB
-    Abc_NodesUnmarkBoth( p->vVisited );
-    return p->vFaninsNode;
+    Abc_NodesUnmarkB( p->vVisited );
+    return p->vNodeLeaves;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Finds a reconvergence-driven cut.]
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
 
-  Description []
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks only at their immediate 
+  predecessors (this is why it is called a one-level construction procedure).]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
+int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nSizeLimit, int nFaninLimit )
 {
     Abc_Obj_t * pNode, * pFaninBest, * pNext;
     int CostBest, CostCur, i;
-//    int fFlagProb = (rand() & 1);
-    int fFlagProb = 1;
     // find the best fanin
     CostBest   = 100;
     pFaninBest = NULL;
-    if ( fFlagProb )
-    {
-        Vec_PtrForEachEntry( vFanins, pNode, i )
-        {
-            CostCur = Abc_NodeGetFaninCost( pNode );
-            if ( CostBest > CostCur )
-            {
-                CostBest   = CostCur;
-                pFaninBest = pNode;
-            }
-        }
-    }
-    else
+//printf( "Evaluating fanins of the cut:\n" );
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
     {
-        Vec_PtrForEachEntry( vFanins, pNode, i )
+        CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
+//printf( "    Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
+        if ( CostBest > CostCur )
         {
-            CostCur = Abc_NodeGetFaninCost( pNode );
-            if ( CostBest >= CostCur )
-            {
-                CostBest   = CostCur;
-                pFaninBest = pNode;
-            }
+            CostBest   = CostCur;
+            pFaninBest = pNode;
         }
+        if ( CostBest == 0 )
+            break;
     }
     if ( pFaninBest == NULL )
         return 0;
+//        return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
     assert( CostBest < 3 );
-    if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+    if ( vLeaves->nSize - 1 + CostBest > nSizeLimit )
         return 0;
+//        return Abc_NodeBuildCutLevelTwo_int( vVisited, vLeaves, nFaninLimit );
+
     assert( Abc_ObjIsNode(pFaninBest) );
     // remove the node from the array
-    Vec_PtrRemove( vFanins, pFaninBest );
+    Vec_PtrRemove( vLeaves, pFaninBest );
+//printf( "Removing fanin %s.\n", Abc_ObjName(pFaninBest) );
+
     // add the left child to the fanins
     pNext = Abc_ObjFanin0(pFaninBest);
     if ( !pNext->fMarkB )
     {
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
         pNext->fMarkB = 1;
-        Vec_PtrPush( vFanins, pNext );
+        Vec_PtrPush( vLeaves, pNext );
+        Vec_PtrPush( vVisited, pNext );
     }
     // add the right child to the fanins
     pNext = Abc_ObjFanin1(pFaninBest);
     if ( !pNext->fMarkB )
     {
+//printf( "Adding fanin %s.\n", Abc_ObjName(pNext) );
         pNext->fMarkB = 1;
-        Vec_PtrPush( vFanins, pNext );
+        Vec_PtrPush( vLeaves, pNext );
+        Vec_PtrPush( vVisited, pNext );
     }
-    assert( vFanins->nSize <= nSizeLimit );
+    assert( vLeaves->nSize <= nSizeLimit );
     // keep doing this
     return 1;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks across two levels of fanins
+  (this is why it is called a two-level construction procedure).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeBuildCutLevelTwo_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int nFaninLimit )
+{
+    Abc_Obj_t * pNode, * pLeafToAdd, * pNodeToMark1, * pNodeToMark2;
+    int CostCur, i;
+    // find the best fanin
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        CostCur = Abc_NodeGetLeafCostTwo( pNode, nFaninLimit, &pLeafToAdd, &pNodeToMark1, &pNodeToMark2 );
+        if ( CostCur < 2 )
+            break;
+    }
+    if ( CostCur > 2 )
+        return 0;
+    // remove the node from the array
+    Vec_PtrRemove( vLeaves, pNode );
+    // add the node to the leaves
+    if ( pLeafToAdd )
+    {
+        assert( !pLeafToAdd->fMarkB );
+        pLeafToAdd->fMarkB = 1;
+        Vec_PtrPush( vLeaves, pLeafToAdd );
+        Vec_PtrPush( vVisited, pLeafToAdd );
+    }
+    // mark the other nodes
+    if ( pNodeToMark1 )
+    {
+        assert( !pNodeToMark1->fMarkB );
+        pNodeToMark1->fMarkB = 1;
+        Vec_PtrPush( vVisited, pNodeToMark1 );
+    }
+    if ( pNodeToMark2 )
+    {
+        assert( !pNodeToMark2->fMarkB );
+        pNodeToMark2->fMarkB = 1;
+        Vec_PtrPush( vVisited, pNodeToMark2 );
+    }
+    // keep doing this
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Get the nodes contained in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited, int fIncludeFanins )
+{
+    Abc_Obj_t * pTemp;
+    int i;
+    // mark the fanins of the cone
+    Abc_NodesMark( vLeaves );
+    // collect the nodes in the DFS order
+    Vec_PtrClear( vVisited );
+    // add the fanins
+    if ( fIncludeFanins )
+        Vec_PtrForEachEntry( vLeaves, pTemp, i )
+            Vec_PtrPush( vVisited, pTemp );
+    // add other nodes
+    for ( i = 0; i < nRoots; i++ )
+        Abc_NodeConeMarkCollect_rec( ppRoots[i], vVisited );
+    // unmark both sets
+    Abc_NodesUnmark( vLeaves );
+    Abc_NodesUnmark( vVisited );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Marks the TFI cone.]
 
   Description []
@@ -273,22 +464,21 @@ int Abc_NodeFindCut_int( Vec_Ptr_t * vFanins, int nSizeLimit )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
 {
     if ( pNode->fMarkA == 1 )
         return;
     // visit transitive fanin 
     if ( Abc_ObjIsNode(pNode) )
     {
-        Abc_NodesMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
-        Abc_NodesMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
     }
     assert( pNode->fMarkA == 0 );
     pNode->fMarkA = 1;
     Vec_PtrPush( vVisited, pNode );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Returns BDD representing the logic function of the cone.]
@@ -300,20 +490,14 @@ void Abc_NodesMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
 {
     DdNode * bFunc0, * bFunc1, * bFunc;
     int i;
-    // mark the fanins of the cone
-    Abc_NodesMark( vFanins );
-    // collect the nodes in the DFS order
-    Vec_PtrClear( vVisited );
-    Abc_NodesMarkCollect_rec( pNode, vVisited );
-    // unmark both sets
-    Abc_NodesUnmark( vFanins );
-    Abc_NodesUnmark( vVisited );
+    // get the nodes in the cut without fanins in the DFS order
+    Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 );
     // set the elementary BDDs
-    Vec_PtrForEachEntry( vFanins, pNode, i )
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)pbVars[i];
     // compute the BDDs for the collected nodes
     Vec_PtrForEachEntry( vVisited, pNode, i )
@@ -347,15 +531,8 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
     DdNode * bFunc0, * bFunc1, * bFunc, * bTrans, * bTemp, * bCube, * bResult;
     Abc_Obj_t * pNode;
     int i;
-    // mark the fanins of the cone
-    Abc_NodesMark( vLeaves );
-    // collect the nodes in the DFS order
-    Vec_PtrClear( vVisited );
-    Vec_PtrForEachEntry( vRoots, pNode, i )
-        Abc_NodesMarkCollect_rec( pNode, vVisited );
-    // unmark both sets
-    Abc_NodesUnmark( vLeaves );
-    Abc_NodesUnmark( vVisited );
+    // get the nodes in the cut without fanins in the DFS order
+    Abc_NodeConeCollect( (Abc_Obj_t **)vRoots->pArray, vRoots->nSize, vLeaves, vVisited, 0 );
     // set the elementary BDDs
     Vec_PtrForEachEntry( vLeaves, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)pbVarsX[i];
@@ -400,16 +577,20 @@ DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
+Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop )
 {
     Abc_ManCut_t * p;
     p = ALLOC( Abc_ManCut_t, 1 );
     memset( p, 0, sizeof(Abc_ManCut_t) );
-    p->vFaninsNode  = Vec_PtrAlloc( 100 );
-    p->vFaninsCone  = Vec_PtrAlloc( 100 );
+    p->vNodeLeaves  = Vec_PtrAlloc( 100 );
+    p->vConeLeaves  = Vec_PtrAlloc( 100 );
     p->vVisited     = Vec_PtrAlloc( 100 );
+    p->vLevels      = Vec_VecAlloc( 100 );
+    p->vNodesTfo     = Vec_PtrAlloc( 100 );
     p->nNodeSizeMax = nNodeSizeMax;
     p->nConeSizeMax = nConeSizeMax;
+    p->nNodeFanStop = nNodeFanStop;
+    p->nConeFanStop = nConeFanStop;
     return p;
 }
 
@@ -426,9 +607,11 @@ Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax )
 ***********************************************************************/
 void Abc_NtkManCutStop( Abc_ManCut_t * p )
 {
-    Vec_PtrFree( p->vFaninsNode );
-    Vec_PtrFree( p->vFaninsCone );
+    Vec_PtrFree( p->vNodeLeaves );
+    Vec_PtrFree( p->vConeLeaves );
     Vec_PtrFree( p->vVisited    );
+    Vec_VecFree( p->vLevels );
+    Vec_PtrFree( p->vNodesTfo );
     free( p );
 }
 
@@ -443,9 +626,25 @@ void Abc_NtkManCutStop( Abc_ManCut_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
+Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
+{
+    return p->vConeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
 {
-    return p->vFaninsCone;
+    return p->vVisited;
 }
 
 
@@ -466,27 +665,27 @@ Vec_Ptr_t * Abc_NtkManCutReadLeaves( Abc_ManCut_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot, 
-    Vec_Ptr_t * vFanins, int LevelMax, Vec_Vec_t * vLevels, Vec_Ptr_t * vResult )
+Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int LevelMax )
 {
+    Abc_Ntk_t * pNtk = pRoot->pNtk;
     Vec_Ptr_t * vVec;
     Abc_Obj_t * pNode, * pFanout;
     int i, k, v, LevelMin;
     assert( Abc_NtkIsStrash(pNtk) );
 
     // assuming that the structure is clean
-    Vec_VecForEachLevel( vLevels, vVec, i )
+    Vec_VecForEachLevel( p->vLevels, vVec, i )
         assert( vVec->nSize == 0 );
 
     // put fanins into the structure while labeling them
     Abc_NtkIncrementTravId( pNtk );
-    LevelMin = ABC_INFINITY;
-    Vec_PtrForEachEntry( vFanins, pNode, i )
+    LevelMin = -1;
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
     {
         if ( pNode->Level > (unsigned)LevelMax )
             continue;
         Abc_NodeSetTravIdCurrent( pNode );
-        Vec_VecPush( vLevels, pNode->Level, pNode );
+        Vec_VecPush( p->vLevels, pNode->Level, pNode );
         if ( LevelMin < (int)pNode->Level )
             LevelMin = pNode->Level;
     }
@@ -497,9 +696,11 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
         Abc_NodeMffcLabel( pRoot );
 
     // go through the levels up
-    Vec_PtrClear( vResult );
-    Vec_VecForEachEntryStartStop( vLevels, pNode, i, k, LevelMin, LevelMax )
+    Vec_PtrClear( p->vNodesTfo );
+    Vec_VecForEachEntryStart( p->vLevels, pNode, i, k, LevelMin )
     {
+        if ( i > LevelMax )
+            break;
         // if the node is not marked, it is not a fanin
         if ( !Abc_NodeIsTravIdCurrent(pNode) )
         {
@@ -508,7 +709,7 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
                  !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
                  continue;
             // save the node in the TFO and label it
-            Vec_PtrPush( vResult, pNode );
+            Vec_PtrPush( p->vNodesTfo, pNode );
             Abc_NodeSetTravIdCurrent( pNode );
         }
         // go through the fanouts and add them to the structure if they meet the conditions
@@ -521,13 +722,18 @@ void Abc_NodeCollectTfoCands( Abc_Ntk_t * pNtk, Abc_Obj_t * pRoot,
             if ( Abc_NodeIsTravIdCurrent(pFanout) )
                 continue;
             // add it to the structure but do not mark it (until tested later)
-            Vec_VecPush( vLevels, pFanout->Level, pFanout );
+            Vec_VecPushUnique( p->vLevels, pFanout->Level, pFanout );
         }
     }
 
     // clear the levelized structure
-    Vec_VecForEachLevelStartStop( vLevels, vVec, i, LevelMin, LevelMax )
+    Vec_VecForEachLevelStart( p->vLevels, vVec, i, LevelMin )
+    {
+        if ( i > LevelMax )
+            break;
         Vec_PtrClear( vVec );
+    }
+    return p->vNodesTfo;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcRefactor.c b/src/base/abc/abcRefactor.c
index 7e387b47..9a413bb1 100644
--- a/src/base/abc/abcRefactor.c
+++ b/src/base/abc/abcRefactor.c
@@ -96,9 +96,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
 
     assert( Abc_NtkIsStrash(pNtk) );
     // start the managers
-    pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax );
+    pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 );
     pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose );
-    pManRef->vLeaves   = Abc_NtkManCutReadLeaves( pManCut );
+    pManRef->vLeaves   = Abc_NtkManCutReadCutLarge( pManCut );
     Abc_NtkStartReverseLevels( pNtk );
 
     // resynthesize each node once
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index 081ccfaa..dfcc3ae5 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -174,6 +174,10 @@ void Abc_NodeUpdate( Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Int_t * vForm,
     // 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
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 730aca90..38840de0 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -18,22 +18,27 @@
 
 ***********************************************************************/
 
-#include "abc.h"
 #ifdef WIN32
-#include "process.h" 
+#include <process.h> 
 #endif
 
+#include "abc.h"
+#include "io.h"
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
- 
+
+static void Abc_ShowFile( char * FileNameDot );
+static void Abc_ShowGetFileName( char * pName, char * pBuffer );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Prints the factored form of one node.]
+  Synopsis    [Visualizes BDD of the node.]
 
   Description []
                
@@ -42,15 +47,152 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodePrintBdd( Abc_Obj_t * pNode )
+void Abc_NodeShowBdd( Abc_Obj_t * pNode )
 {
     FILE * pFile;
     Vec_Ptr_t * vNamesIn;
-    char * FileNameIn;
-    char * FileNameOut;
-    char * FileGeneric;
-    char * pCur, * pNameOut;
     char FileNameDot[200];
+    char * pNameOut;
+
+    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
+    // create the file names
+    Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+
+    // set the node names 
+    vNamesIn = Abc_NodeGetFaninNames( pNode );
+    pNameOut = Abc_ObjName(pNode);
+    Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
+    Abc_NodeFreeFaninNames( vNamesIn );
+    Abc_NtkCleanCopy( pNode->pNtk );
+    fclose( pFile );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Visualizes AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
+{
+    FILE * pFile;
+    Abc_Obj_t * pNode;
+    Vec_Ptr_t * vNodes;
+    char FileNameDot[200];
+    int i;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // create the file names
+    Abc_ShowGetFileName( pNtk->pName, FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+
+    // collect all nodes in the network
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+    // write the DOT file
+    Io_WriteDot( pNtk, vNodes, NULL, FileNameDot );
+    Vec_PtrFree( vNodes );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Visualizes reconvergence driven cut at the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeShowCut( Abc_Obj_t * pNode, int nNodeSizeMax, int nConeSizeMax )
+{
+    FILE * pFile;
+    char FileNameDot[200];
+    Abc_ManCut_t * p;
+    Vec_Ptr_t * vCutSmall;
+    Vec_Ptr_t * vCutLarge;
+    Vec_Ptr_t * vInside;
+    Vec_Ptr_t * vNodesTfo;
+    Abc_Obj_t * pTemp;
+    int i;
+
+    assert( Abc_NtkIsStrash(pNode->pNtk) );
+
+    // start the cut computation manager
+    p = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, ABC_INFINITY );
+    // get the recovergence driven cut
+    vCutSmall = Abc_NodeFindCut( p, pNode, 1 );
+    // get the containing cut
+    vCutLarge = Abc_NtkManCutReadCutLarge( p );
+    // get the array for the inside nodes
+    vInside = Abc_NtkManCutReadVisited( p );
+    // get the inside nodes of the containing cone
+    Abc_NodeConeCollect( &pNode, 1, vCutLarge, vInside, 1 );
+
+    // add the nodes in the TFO 
+    vNodesTfo = Abc_NodeCollectTfoCands( p, pNode, vCutSmall, ABC_INFINITY );
+    Vec_PtrForEachEntry( vNodesTfo, pTemp, i )
+        Vec_PtrPushUnique( vInside, pTemp );
+
+    // create the file names
+    Abc_ShowGetFileName( Abc_ObjName(pNode), FileNameDot );
+    // check that the file can be opened
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    // add the root node to the cone (for visualization)
+    Vec_PtrPush( vCutSmall, pNode );
+    // write the DOT file
+    Io_WriteDot( pNode->pNtk, vInside, vCutSmall, FileNameDot );
+    // stop the cut computation manager
+    Abc_NtkManCutStop( p );
+
+    // visualize the file 
+    Abc_ShowFile( FileNameDot );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Shows the given DOT file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ShowFile( char * FileNameDot )
+{
+    FILE * pFile;
+    char * FileGeneric;
     char FileNamePs[200];
     char CommandDot[1000];
 #ifndef WIN32
@@ -60,8 +202,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
     char * pProgGsViewName;
     int RetValue;
 
-    assert( Abc_NtkIsBddLogic(pNode->pNtk) );
-
 #ifdef WIN32
     pProgDotName = "dot.exe";
     pProgGsViewName = NULL;
@@ -70,34 +210,6 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
     pProgGsViewName = "gv";
 #endif
 
-    FileNameIn  = NULL;
-    FileNameOut = NULL;
-
-    // get the generic file name
-    pNode->pCopy = NULL;
-    FileGeneric = Abc_ObjName(pNode);
-    // get rid of not-alpha-numeric characters
-    for ( pCur = FileGeneric; *pCur; pCur++ )
-        if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) )
-            *pCur = '_';
-    // create the file names
-    sprintf( FileNameDot, "%s.dot", FileGeneric ); 
-    sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
-
-    // write the DOT file
-    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
-    {
-        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
-        return;
-    }
-    // set the node names 
-    vNamesIn = Abc_NodeGetFaninNames( pNode );
-    pNameOut = Abc_ObjName(pNode);
-    Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
-    Abc_NodeFreeFaninNames( vNamesIn );
-    Abc_NtkCleanCopy( pNode->pNtk );
-    fclose( pFile );
-
     // check that the input file is okay
     if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
     {
@@ -106,6 +218,12 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
     }
     fclose( pFile );
 
+    // get the generic file name
+    FileGeneric = Extra_FileNameGeneric( FileNameDot );
+    // create the PostScript file name
+    sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
+    free( FileGeneric );
+
     // generate the DOT file
     sprintf( CommandDot,  "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); 
     RetValue = system( CommandDot );
@@ -146,10 +264,9 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
 #endif
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Derives the DOT file name.]
 
   Description []
                
@@ -158,6 +275,18 @@ void Abc_NodePrintBdd( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_ShowGetFileName( char * pName, char * pBuffer )
+{
+    char * pCur;
+    // creat the file name
+    sprintf( pBuffer, "%s.dot", pName );
+    // get rid of not-alpha-numeric characters
+    for ( pCur = pBuffer; *pCur; pCur++ )
+        if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || 
+               (*pCur >= 'A' && *pCur <= 'Z') || (*pCur == '.')) )
+            *pCur = '_';
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index 19394fb3..0a28c3c1 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -49,7 +49,7 @@ extern char *      Mio_GateReadSop( void * pGate );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
+Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
@@ -68,11 +68,11 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
     // print warning about self-feed latches
     if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
         printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
-    if ( nNodes = Abc_AigCleanup(pNtkAig->pManFunc) )
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
         printf( "Cleanup has removed %d nodes.\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
+        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
     // make sure everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
     {
diff --git a/src/base/abc/abcSweep.c b/src/base/abc/abcSweep.c
index 47565241..61d65ce3 100644
--- a/src/base/abc/abcSweep.c
+++ b/src/base/abc/abcSweep.c
@@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     assert( !Abc_NtkIsStrash(pNtk) );
 
     // derive the AIG
-    pNtkAig = Abc_NtkStrash( pNtk, 0 );
+    pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
     pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );    
diff --git a/src/base/abc/abcSymm.c b/src/base/abc/abcSymm.c
new file mode 100644
index 00000000..8df3a837
--- /dev/null
+++ b/src/base/abc/abcSymm.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+  FileName    [abcSymm.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computation of two-variable symmetries.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcSymm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose );
+static void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [The top level procedure to compute symmetries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSymmetries( Abc_Ntk_t * pNtk, int fUseBdds, int fNaive, int fVerbose )
+{
+    if ( fUseBdds || fNaive )
+        Abc_NtkSymmetriesUsingBdds( pNtk, fNaive, fVerbose );
+    else
+        printf( "This option is currently not implemented.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Symmetry computation using BDDs (both naive and smart).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
+{
+    DdManager * dd;
+    int clk, clkBdd, clkSym;
+
+    // compute the global functions
+clk = clock();
+    dd = Abc_NtkGlobalBdds( pNtk, 0 );
+    Cudd_AutodynDisable( dd );
+    Cudd_zddVarsFromBddVars( dd, 2 );
+clkBdd = clock() - clk;
+    // create the collapsed network
+clk = clock();
+    Ntk_NetworkSymmsBdd( dd, pNtk, fNaive, fVerbose );
+clkSym = clock() - clk;
+    // undo the global functions
+    Abc_NtkFreeGlobalBdds( pNtk );
+    Extra_StopManager( dd );
+    pNtk->pManGlob = NULL;
+
+PRT( "Constructing BDDs", clkBdd );
+PRT( "Computing symms  ", clkSym );
+PRT( "TOTAL            ", clkBdd + clkSym );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Symmetry computation using BDDs (both naive and smart).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
+{
+    Extra_SymmInfo_t * pSymms;
+    Abc_Obj_t * pNode;
+    DdNode * bFunc;
+    int nSymms = 0;
+    int i;
+
+    // compute symmetry info for each PO
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        bFunc = pNtk->vFuncsGlob->pArray[i];
+        if ( Cudd_IsConstant(bFunc) )
+            continue;
+        if ( fNaive )
+            pSymms = Extra_SymmPairsComputeNaive( dd, bFunc );
+        else
+            pSymms = Extra_SymmPairsCompute( dd, bFunc );
+        nSymms += pSymms->nSymms;
+        if ( fVerbose )
+        {
+            printf( "Output %6s (%d): ", Abc_ObjName(pNode), pSymms->nSymms );
+            Ntk_NetworkSymmsPrint( pNtk, pSymms );
+        }
+//Extra_SymmPairsPrint( pSymms );
+        Extra_SymmPairsDissolve( pSymms );
+    }
+    printf( "The total number of symmetries is %d.\n", nSymms );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Printing symmetry groups from the symmetry data structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntk_NetworkSymmsPrint( Abc_Ntk_t * pNtk, Extra_SymmInfo_t * pSymms )
+{
+    char ** pInputNames;
+    int * pVarTaken;
+    int i, k, nVars, nSize, fStart;
+
+    // get variable names
+    nVars = Abc_NtkCiNum(pNtk);
+    pInputNames = Abc_NtkCollectCioNames( pNtk, 0 );
+
+    // alloc the array of marks
+    pVarTaken = ALLOC( int, nVars );
+    memset( pVarTaken, 0, sizeof(int) * nVars );
+
+    // print the groups
+    fStart = 1;
+    nSize = pSymms->nVars;
+    for ( i = 0; i < nSize; i++ )
+    {
+        // skip the variable already considered
+        if ( pVarTaken[i] )
+            continue;
+        // find all the vars symmetric with this one
+        for ( k = 0; k < nSize; k++ )
+        {
+            if ( k == i )
+                continue;
+            if ( pSymms->pSymms[i][k] == 0 )
+                continue;
+            // vars i and k are symmetric
+            assert( pVarTaken[k] == 0 );
+            // there is a new symmetry pair 
+            if ( fStart == 1 )
+            {  // start a new symmetry class
+                fStart = 0;
+                printf( "  { %s", pInputNames[ pSymms->pVars[i] ] );
+                // mark the var as taken
+                pVarTaken[i] = 1;
+            }
+            printf( " %s", pInputNames[ pSymms->pVars[k] ] );
+            // mark the var as taken
+            pVarTaken[k] = 1;
+        }
+        if ( fStart == 0 )
+        {
+            printf( " }" );
+            fStart = 1; 
+        }   
+    }   
+    printf( "\n" );
+
+    free( pInputNames );
+    free( pVarTaken );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcUnreach.c b/src/base/abc/abcUnreach.c
index 04e5c96c..0fe3ec63 100644
--- a/src/base/abc/abcUnreach.c
+++ b/src/base/abc/abcUnreach.c
@@ -91,6 +91,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
     Cudd_RecursiveDeref( dd, bUnreach );
     Extra_StopManager( dd );
+    pNtk->pManGlob = NULL;
 
     // make sure that everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
@@ -135,13 +136,13 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
-        bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext );   Cudd_Ref( bProd );
-        bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );             Cudd_Ref( bRel );
+        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
+        bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );                 Cudd_Ref( bRel );
         Cudd_RecursiveDeref( dd, bTemp ); 
         Cudd_RecursiveDeref( dd, bProd ); 
     }
     // free the global BDDs
-    Abc_NtkFreeGlobalBdds( dd, pNtk );
+    Abc_NtkFreeGlobalBdds( pNtk );
 
     // quantify the PI variables
     bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 7d2ca107..9a2acc32 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1046,6 +1046,29 @@ Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
     return vFanNums;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects all objects into one array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        Vec_PtrPush( vNodes, pNode );
+    return vNodes;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index d9bed264..d3d4091b 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -32,6 +32,7 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcSop.c \
     src/base/abc/abcStrash.c \
     src/base/abc/abcSweep.c \
+    src/base/abc/abcSymm.c \
     src/base/abc/abcTiming.c \
     src/base/abc/abcUnreach.c \
     src/base/abc/abcUtil.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 9ffbc3cf..89703214 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -29,12 +29,16 @@ static int IoCommandRead        ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteDot    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
@@ -58,12 +62,16 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_dot",     IoCommandWriteDot,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_eqn",     IoCommandWriteEqn,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_gml",     IoCommandWriteGml,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
 }
 
@@ -127,7 +135,7 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -199,7 +207,7 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -280,7 +288,7 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -360,7 +368,7 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -406,6 +414,86 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    char * FileName;
+    FILE * pFile;
+    int fCheck;
+    int c;
+
+    fCheck = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pNtk = Io_ReadEqn( FileName, fCheck );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from the equation file has failed.\n" );
+        return 1;
+    }
+
+    pNtk = Abc_NtkNetlistToLogic( pTemp = pNtk );
+    Abc_NtkDelete( pTemp );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Converting to logic network after reading has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         read the network in equation format\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pTemp;
@@ -440,7 +528,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -451,7 +539,7 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
     pNtk = Io_ReadVerilog( FileName, fCheck );
     if ( pNtk == NULL )
     {
-        fprintf( pAbc->Err, "Reading network from Verilog file has failed.\n" );
+        fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
         return 1;
     }
 
@@ -520,7 +608,7 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
-        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".mvpla", NULL ) )
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
             fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
         fprintf( pAbc->Err, "\n" );
         return 1;
@@ -764,6 +852,199 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * FileName;
+    Vec_Ptr_t * vNodes;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
+    {
+        fprintf( stdout, "IoCommandWriteDot(): Currently can only process logic networks with BDDs.\n" );
+        return 0;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    // write the file
+    vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur );
+    Io_WriteDot( pAbc->pNtkCur, vNodes, NULL, FileName );
+    Vec_PtrFree( vNodes );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the AIG into a DOT file\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    char * FileName;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
+        return 0;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    // write the file
+    // get rid of complemented covers if present
+    if ( Abc_NtkIsSopLogic(pNtk) )
+        Abc_NtkLogicMakeDirectSops(pNtk);
+    // derive the netlist
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    if ( pNtkTemp == NULL )
+    {
+        fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
+        return 0;
+    }
+    Io_WriteEqn( pNtkTemp, FileName );
+    Abc_NtkDelete( pNtkTemp );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the current network in the equation format\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * FileName;
+    int c;
+
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pAbc->pNtkCur == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsLogic(pAbc->pNtkCur) && !Abc_NtkIsStrash(pAbc->pNtkCur) )
+    {
+        fprintf( stdout, "IoCommandWriteGml(): Currently can only process logic networks with BDDs.\n" );
+        return 0;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    // write the file
+    Io_WriteGml( pAbc->pNtkCur, FileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         write network using graph representation formal GML\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk, * pNtkTemp;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index d45b7b1b..6bf3a85c 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -53,6 +53,8 @@ extern Abc_Ntk_t *        Io_ReadBlif( char * pFileName, int fCheck );
 extern Abc_Ntk_t *        Io_ReadBench( char * pFileName, int fCheck );
 /*=== abcReadEdif.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadEdif( char * pFileName, int fCheck );
+/*=== abcReadEqn.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadEqn( char * pFileName, int fCheck );
 /*=== abcReadVerilog.c ==========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcReadPla.c ==========================================================*/
@@ -73,6 +75,12 @@ extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ==========================================================*/
 extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteDot.c ==========================================================*/
+extern void               Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName );
+/*=== abcWriteEqn.c ==========================================================*/
+extern void               Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName );
+/*=== abcWriteGml.c ==========================================================*/
+extern void               Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWritePla.c ==========================================================*/
 extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
 
diff --git a/src/base/io/ioRead.c b/src/base/io/ioRead.c
index 75c87a80..acf4deda 100644
--- a/src/base/io/ioRead.c
+++ b/src/base/io/ioRead.c
@@ -53,6 +53,8 @@ Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
         pNtk = Io_ReadEdif( pFileName, fCheck );
     else if ( Extra_FileNameCheckExtension( pFileName, "pla" ) )
         pNtk = Io_ReadPla( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "eqn" ) )
+        pNtk = Io_ReadEqn( pFileName, fCheck );
     else 
     {
         fprintf( stderr, "Unknown file format\n" );
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
new file mode 100644
index 00000000..54890729
--- /dev/null
+++ b/src/base/io/ioReadEqn.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [ioReadEqn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read equation format files.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioReadEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p );
+static void        Io_ReadEqnStrCompact( char * pStr );
+static int         Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName );
+static void        Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the network from a BENCH file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEqn( char * pFileName, int fCheck )
+{
+    Extra_FileReader_t * p;
+    Abc_Ntk_t * pNtk;
+
+    // start the file
+    p = Extra_FileReaderAlloc( pFileName, "#", ";", "=" );
+    if ( p == NULL )
+        return NULL;
+
+    // read the network
+    pNtk = Io_ReadEqnNetwork( p );
+    Extra_FileReaderFree( p );
+    if ( pNtk == NULL )
+        return NULL;
+
+    // make sure that everything is okay with the network structure
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Io_ReadEqn: The network check has failed.\n" );
+        Abc_NtkDelete( pNtk );
+        return NULL;
+    }
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vTokens;
+    Vec_Ptr_t * vCubes, * vLits, * vVars;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    char * pCubesCopy, * pSopCube, * pVarName;
+    int iLine, iNum, i, k;
+    
+    // allocate the empty network
+    pNtk = Abc_NtkStartRead( Extra_FileReaderGetFileName(p) );
+
+    // go through the lines of the file
+    vCubes = Vec_PtrAlloc( 100 );
+    vVars  = Vec_PtrAlloc( 100 );
+    vLits  = Vec_PtrAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
+    for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
+
+        // check if the first token contains anything
+        Io_ReadEqnStrCompact( vTokens->pArray[0] );
+        if ( strlen(vTokens->pArray[0]) == 0 )
+            break;
+
+        // if the number of tokens is different from two, error
+        if ( vTokens->nSize != 2 )
+        {
+            printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
+            Abc_NtkDelete( pNtk );
+            return NULL;
+        }
+
+        // get the type of the line
+        if ( strncmp( vTokens->pArray[0], "INORDER", 7 ) == 0 )
+        {
+            Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
+            Vec_PtrForEachEntry( vVars, pVarName, i )
+                Io_ReadCreatePi( pNtk, pVarName );
+        }
+        else if ( strncmp( vTokens->pArray[0], "OUTORDER", 8 ) == 0 )
+        {
+            Io_ReadEqnStrCutAt( vTokens->pArray[1], " \n\r\t", 0, vVars );
+            Vec_PtrForEachEntry( vVars, pVarName, i )
+                Io_ReadCreatePo( pNtk, pVarName );
+        }
+        else 
+        {
+            // remove spaces
+            pCubesCopy = vTokens->pArray[1];
+            Io_ReadEqnStrCompact( pCubesCopy );
+            // consider the case of the constant node
+            if ( (pCubesCopy[0] == '0' || pCubesCopy[0] == '1') && pCubesCopy[1] == 0 )
+            {
+                pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], NULL, 0 );
+                if ( pCubesCopy[0] == '0' )
+                    pNode->pData = Abc_SopCreateConst0( pNtk->pManFunc );
+                else
+                    pNode->pData = Abc_SopCreateConst1( pNtk->pManFunc );
+                continue;
+            }
+            // determine unique variables
+            pCubesCopy = util_strsav( pCubesCopy );
+            // find the names of the fanins of this node
+            Io_ReadEqnStrCutAt( pCubesCopy, "!*+", 1, vVars );
+            // create the node
+            pNode = Io_ReadCreateNode( pNtk, vTokens->pArray[0], (char **)vVars->pArray, vVars->nSize );
+            // split the string into cubes
+            Io_ReadEqnStrCutAt( vTokens->pArray[1], "+", 0, vCubes );
+            // start the sop
+            pNode->pData = Abc_SopStart( pNtk->pManFunc, vCubes->nSize, vVars->nSize );
+            // read the cubes
+            i = 0;
+            Abc_SopForEachCube( pNode->pData, vVars->nSize, pSopCube )
+            {
+                // split this cube into lits
+                Io_ReadEqnStrCutAt( vCubes->pArray[i], "*", 0, vLits );
+                // read the literals
+                Vec_PtrForEachEntry( vLits, pVarName, k )
+                {
+                    iNum = Io_ReadEqnStrFind( vVars, pVarName + (pVarName[0] == '!') );
+                    assert( iNum >= 0 );
+                    pSopCube[iNum] = '1' - (pVarName[0] == '!');
+                }
+                i++;
+            }
+            assert( i == vCubes->nSize );
+            // remove the cubes
+            free( pCubesCopy );
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vCubes );
+    Vec_PtrFree( vLits );
+    Vec_PtrFree( vVars );
+    Abc_NtkFinalizeRead( pNtk );
+    return pNtk;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Compacts the string by throwing away space-like chars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_ReadEqnStrCompact( char * pStr )
+{
+    char * pCur, * pNew;
+    for ( pNew = pCur = pStr; *pCur; pCur++ )
+        if ( !(*pCur == ' ' || *pCur == '\n' || *pCur == '\r' || *pCur == '\t') )
+            *pNew++ = *pCur;
+    *pNew = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines unique variables in the string.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_ReadEqnStrFind( Vec_Ptr_t * vTokens, char * pName )
+{
+    char * pToken;
+    int i;
+    Vec_PtrForEachEntry( vTokens, pToken, i )
+        if ( strcmp( pToken, pName ) == 0 )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cuts the string into pieces using stop chars.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_ReadEqnStrCutAt( char * pStr, char * pStop, int fUniqueOnly, Vec_Ptr_t * vTokens )
+{
+    char * pToken;
+    Vec_PtrClear( vTokens );
+    for ( pToken = strtok( pStr, pStop ); pToken; pToken = strtok( NULL, pStop ) )
+        if ( !fUniqueOnly || Io_ReadEqnStrFind( vTokens, pToken ) == -1 )
+            Vec_PtrPush( vTokens, pToken );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 5135105f..7d6815b9 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -107,10 +107,7 @@ void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 
   Synopsis    [Write one network.]
 
-  Description [Writes a network composed of PIs, POs, internal nodes,
-  and latches. The following rules are used to print the names of 
-  internal nodes:
-  ]
+  Description []
                
   SideEffects []
 
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index bb216bb6..09824f38 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -6,7 +6,7 @@
 
   PackageName [Command processing package.]
 
-  Synopsis    [Procedures to CNF of the miter cone.]
+  Synopsis    [Procedures to output CNF of the miter cone.]
 
   Author      [Alan Mishchenko]
   
@@ -24,8 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
new file mode 100644
index 00000000..7d88e52d
--- /dev/null
+++ b/src/base/io/ioWriteDot.c
@@ -0,0 +1,322 @@
+/**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, * pTemp, * pPrev;
+    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 stream
+    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 = 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 [label = \"%s\"", pNode->Id, 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 [label = \"%s\"", pNode->Id, 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 [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
+        if ( Abc_ObjFanin0(pNode)->fMarkC )
+        {
+            fprintf( pFile, "Node%d",  pNode->Id );
+            fprintf( pFile, " -> " );
+            fprintf( pFile, "Node%d",  Abc_ObjFaninId0(pNode) );
+            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
+        if ( Abc_ObjFanin1(pNode)->fMarkC )
+        {
+            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, ";\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/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c
new file mode 100644
index 00000000..6c2893b5
--- /dev/null
+++ b/src/base/io/ioWriteEqn.c
@@ -0,0 +1,261 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteEqn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write equation representation of the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteEqn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the logic network in the equation format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteEqn( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+
+    assert( Abc_NtkIsSopNetlist(pNtk) );
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+        printf( "Warning: only combinational portion is being written.\n" );
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteEqn(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "# Equations for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+
+    // write the equations for the network
+    Io_NtkWriteEqnOne( pFile, pNtk );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write one network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteEqnOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // write the PIs
+    fprintf( pFile, "INORDER =" );
+    Io_NtkWriteEqnPis( pFile, pNtk );
+    fprintf( pFile, ";\n" );
+
+    // write the POs
+    fprintf( pFile, "OUTORDER =" );
+    Io_NtkWriteEqnPos( pFile, pNtk );
+    fprintf( pFile, ";\n" );
+
+    // write each internal node
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Io_NtkWriteEqnNode( pFile, pNode );
+    }
+    Extra_ProgressBarStop( pProgress );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteEqnPis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 9;
+    NameCounter = 0;
+
+    Abc_NtkForEachCi( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanout0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteEqnPos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 10;
+    NameCounter = 0;
+
+    Abc_NtkForEachCo( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the node into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteEqnNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    char * pCube;
+    int Value, fFirstLit, i;
+
+    fprintf( pFile, "%s = ", Abc_ObjName(pNode) );
+
+    if ( Abc_SopIsConst0(pNode->pData) )
+    {
+        fprintf( pFile, "0;\n" );
+        return;
+    }
+    if ( Abc_SopIsConst1(pNode->pData) )
+    {
+        fprintf( pFile, "1;\n" );
+        return;
+    }
+
+    NameCounter = 0;
+    LineLength  = strlen(Abc_ObjName(pNode)) + 3;
+    Abc_SopForEachCube( pNode->pData, Abc_ObjFaninNum(pNode), pCube )
+    {
+        if ( pCube != pNode->pData )
+        {
+            fprintf( pFile, " + " );
+            LineLength += 3;
+        }
+
+        // add the cube
+        fFirstLit = 1;
+        Abc_CubeForEachVar( pCube, Value, i )
+        {
+            if ( Value == '-' )
+                continue;
+            pNet = Abc_ObjFanin( pNode, i );
+            // get the line length after this name is written
+            AddedLength = !fFirstLit + (Value == '0') + strlen(Abc_ObjName(pNet));
+            if ( NameCounter && LineLength + AddedLength + 6 > IO_WRITE_LINE_LENGTH )
+            { // write the line extender
+                fprintf( pFile, " \n " );
+                // reset the line length
+                LineLength  = 0;
+                NameCounter = 0;
+            }
+            fprintf( pFile, "%s%s%s", (fFirstLit? "": "*"), ((Value == '0')? "!":""), Abc_ObjName(pNet) );
+            LineLength += AddedLength;
+            NameCounter++;
+            fFirstLit = 0;
+        }
+    }
+    fprintf( pFile, ";\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c
new file mode 100644
index 00000000..ab9f1143
--- /dev/null
+++ b/src/base/io/ioWriteGml.c
@@ -0,0 +1,116 @@
+/**CFile****************************************************************
+
+  FileName    [ioWriteGml.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write the graph structure of AIG in GML.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteGml.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 GML.]
+
+  Description [Useful for graph visualization using tools such as yEd: 
+  http://www.yworks.com/]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteGml( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    FILE * pFile;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k;
+
+    assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk)  );
+
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteGml(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "# GML for \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
+    fprintf( pFile, "graph [\n" );
+
+    // output the POs
+    fprintf( pFile, "\n" );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+        fprintf( pFile, "        graphics [ type \"triangle\" fill \"#00FFFF\" ]\n" );   // blue
+        fprintf( pFile, "    ]\n" );
+    }
+    // output the PIs
+    fprintf( pFile, "\n" );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+        fprintf( pFile, "        graphics [ type \"triangle\" fill \"#00FF00\" ]\n" );   // green
+        fprintf( pFile, "    ]\n" );
+    }
+    // output the latches
+    fprintf( pFile, "\n" );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+        fprintf( pFile, "        graphics [ type \"rectangle\" fill \"#FF0000\" ]\n" );   // red
+        fprintf( pFile, "    ]\n" );
+    }
+    // output the nodes
+    fprintf( pFile, "\n" );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        fprintf( pFile, "    node [ id %5d label \"%s\"\n", pObj->Id, Abc_ObjName(pObj) );
+        fprintf( pFile, "        graphics [ type \"ellipse\" fill \"#CCCCFF\" ]\n" );     // grey
+        fprintf( pFile, "    ]\n" );
+    }
+
+    // output the edges
+    fprintf( pFile, "\n" );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            fprintf( pFile, "    edge [ source %5d   target %5d\n", pObj->Id, pFanin->Id );
+            fprintf( pFile, "        graphics [ type \"line\" arrow \"first\" ]\n" );
+            fprintf( pFile, "    ]\n" );
+        }
+    }
+
+    fprintf( pFile, "]\n" );
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index cb39c481..34582473 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -3,10 +3,14 @@ SRC +=  src/base/io/io.c \
     src/base/io/ioReadBench.c \
     src/base/io/ioReadBlif.c \
     src/base/io/ioReadEdif.c \
+    src/base/io/ioReadEqn.c \
     src/base/io/ioReadPla.c \
     src/base/io/ioReadVerilog.c \
     src/base/io/ioUtil.c \
     src/base/io/ioWriteBench.c \
     src/base/io/ioWriteBlif.c \
     src/base/io/ioWriteCnf.c \
+    src/base/io/ioWriteDot.c \
+    src/base/io/ioWriteEqn.c \
+    src/base/io/ioWriteGml.c \
     src/base/io/ioWritePla.c
diff --git a/src/map/fpga/fpgaCore.c b/src/map/fpga/fpgaCore.c
index b181e997..0fc90228 100644
--- a/src/map/fpga/fpgaCore.c
+++ b/src/map/fpga/fpgaCore.c
@@ -71,7 +71,7 @@ int Fpga_Mapping( Fpga_Man_t * p )
             return 0;
         p->timeRecover = clock() - clk;
     }
-PRT( "Total mapping time", clock() - clkTotal );
+//PRT( "Total mapping time", clock() - clkTotal );
 
     // print the AI-graph used for mapping
     //Fpga_ManShow( p, "test" );
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index d298a204..14a3d950 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -117,6 +117,57 @@ extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
 extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
 
+/*=== extraBddSymm.c =================================================================*/
+
+typedef struct Extra_SymmInfo_t_  Extra_SymmInfo_t;
+struct Extra_SymmInfo_t_ {
+    int nVars;      // the number of variables in the support
+    int nVarsMax;   // the number of variables in the DD manager
+    int nSymms;     // the number of pair-wise symmetries
+    int nNodes;     // the number of nodes in a ZDD (if applicable)
+    int * pVars;    // the list of all variables present in the support
+    char ** pSymms; // the symmetry information
+};
+
+/* computes the classical symmetry information for the function - recursive */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCompute( DdManager * dd, DdNode * bFunc );
+/* computes the classical symmetry information for the function - using naive approach */
+extern Extra_SymmInfo_t *  Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc );
+extern int         Extra_bddCheckVarsSymmetricNaive( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+
+/* allocates the data structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsAllocate( int nVars );
+/* deallocates the data structure */
+extern void        Extra_SymmPairsDissolve( Extra_SymmInfo_t * );
+/* print the contents the data structure */
+extern void        Extra_SymmPairsPrint( Extra_SymmInfo_t * );
+/* converts the ZDD into the Extra_SymmInfo_t structure */
+extern Extra_SymmInfo_t *  Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bVars );
+
+/* computes the classical symmetry information as a ZDD */
+extern DdNode *    Extra_zddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+extern DdNode *     extraZddSymmPairsCompute( DdManager * dd, DdNode * bF, DdNode * bVars );
+/* returns a singleton-set ZDD containing all variables that are symmetric with the given one */
+extern DdNode *    Extra_zddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+extern DdNode *     extraZddGetSymmetricVars( DdManager * dd, DdNode * bF, DdNode * bG, DdNode * bVars );
+/* converts a set of variables into a set of singleton subsets */
+extern DdNode *    Extra_zddGetSingletons( DdManager * dd, DdNode * bVars );
+extern DdNode *     extraZddGetSingletons( DdManager * dd, DdNode * bVars );
+/* filters the set of variables using the support of the function */
+extern DdNode *    Extra_bddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+extern DdNode *     extraBddReduceVarSet( DdManager * dd, DdNode * bVars, DdNode * bF );
+
+/* checks the possibility that the two vars are symmetric */
+extern int         Extra_bddCheckVarsSymmetric( DdManager * dd, DdNode * bF, int iVar1, int iVar2 );
+extern DdNode *     extraBddCheckVarsSymmetric( DdManager * dd, DdNode * bF, DdNode * bVars );
+
+/* build the set of all tuples of K variables out of N from the BDD cube */
+extern DdNode *    Extra_zddTuplesFromBdd( DdManager * dd, int K, DdNode * bVarsN );
+extern DdNode *     extraZddTuplesFromBdd( DdManager * dd, DdNode * bVarsK, DdNode * bVarsN );
+/* selects one subset from a ZDD representing the set of subsets */
+extern DdNode *    Extra_zddSelectOneSubset( DdManager * dd, DdNode * zS );
+extern DdNode *     extraZddSelectOneSubset( DdManager * dd, DdNode * zS );
+
 /*=== extraUtilBitMatrix.c ================================================================*/
 
 typedef struct Extra_BitMat_t_ Extra_BitMat_t;
diff --git a/src/misc/extra/extraUtilBdd.c b/src/misc/extra/extraBddMisc.c
index 38e3345c..373ce5c5 100644
--- a/src/misc/extra/extraUtilBdd.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [extraUtilBdd.c]
+  FileName    [extraBddMisc.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: extraUtilBdd.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+  Revision    [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
diff --git a/src/misc/extra/extraBddSymm.c b/src/misc/extra/extraBddSymm.c
new file mode 100644
index 00000000..474f663f
--- /dev/null
+++ b/src/misc/extra/extraBddSymm.c
@@ -0,0 +1,1469 @@
+/**CFile****************************************************************
+
+  FileName    [extraBddSymm.c]
+
+  PackageName [extra]
+
+  Synopsis    [Efficient methods to compute the information about
+  symmetric variables using the algorithm presented in the paper:
+  A. Mishchenko. Fast Computation of Symmetries in Boolean Functions. 
+  Transactions on CAD, Nov. 2003.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraBddSymm.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+#define DD_GET_SYMM_VARS_TAG          0x0a /* former DD_BDD_XOR_EXIST_ABSTRACT_TAG */
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+/**AutomaticEnd***************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the classical symmetry information for the function.]
+
+  Description [Returns the symmetry information in the form of Extra_SymmInfo_t structure.]
+
+  SideEffects [If the ZDD variables are not derived from BDD variables with
+  multiplicity 2, this function may derive them in a wrong way.]
+
+  SeeAlso     []
+
+******************************************************************************/
+Extra_SymmInfo_t * Extra_SymmPairsCompute( 
+  DdManager * dd,   /* the manager */
+  DdNode * bFunc)   /* the function whose symmetries are computed */
+{
+    DdNode * bSupp;
+    DdNode * zRes;
+    Extra_SymmInfo_t * p;
+
+    bSupp = Cudd_Support( dd, bFunc );                      Cudd_Ref( bSupp );
+    zRes  = Extra_zddSymmPairsCompute( dd, bFunc, bSupp );  Cudd_Ref( zRes );
+
+    p = Extra_SymmPairsCreateFromZdd( dd, zRes, bSupp );
+
+    Cudd_RecursiveDeref( dd, bSupp );
+    Cudd_RecursiveDerefZdd( dd, zRes );
+
+    return p;
+
+} /* end of Extra_SymmPairsCompute */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the classical symmetry information as a ZDD.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_zddSymmPairsCompute( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bF,
+  DdNode * bVars) 
+{
+    DdNode * res;
+    do {
+        dd->reordered = 0;
+        res = extraZddSymmPairsCompute( dd, bF, bVars );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddSymmPairsCompute */
+
+/**Function********************************************************************
+
+  Synopsis    [Returns a singleton-set ZDD containing all variables that are symmetric with the given one.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_zddGetSymmetricVars( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bF,       /* the first function  - originally, the positive cofactor */
+  DdNode * bG,       /* the second fucntion - originally, the negative cofactor */
+  DdNode * bVars)    /* the set of variables, on which F and G depend */
+{
+    DdNode * res;
+    do {
+        dd->reordered = 0;
+        res = extraZddGetSymmetricVars( dd, bF, bG, bVars );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddGetSymmetricVars */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Converts a set of variables into a set of singleton subsets.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_zddGetSingletons( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bVars)    /* the set of variables */
+{
+    DdNode * res;
+    do {
+        dd->reordered = 0;
+        res = extraZddGetSingletons( dd, bVars );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddGetSingletons */
+
+/**Function********************************************************************
+
+  Synopsis    [Filters the set of variables using the support of the function.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddReduceVarSet( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bVars,    /* the set of variables to be reduced */
+  DdNode * bF)       /* the function whose support is used for reduction */
+{
+    DdNode * res;
+    do {
+        dd->reordered = 0;
+        res = extraBddReduceVarSet( dd, bVars, bF );
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_bddReduceVarSet */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Allocates symmetry information structure.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
+{
+    int i;
+    Extra_SymmInfo_t * p;
+
+    // allocate and clean the storage for symmetry info
+    p = ALLOC( Extra_SymmInfo_t, 1 );
+    memset( p, 0, sizeof(Extra_SymmInfo_t) );
+    p->nVars     = nVars;
+    p->pVars     = ALLOC( int, nVars );  
+    p->pSymms    = ALLOC( char *, nVars );  
+    p->pSymms[0] = ALLOC( char  , nVars * nVars );
+    memset( p->pSymms[0], 0, nVars * nVars * sizeof(char) );
+
+    for ( i = 1; i < nVars; i++ )
+        p->pSymms[i] = p->pSymms[i-1] + nVars;
+
+    return p;
+} /* end of Extra_SymmPairsAllocate */
+
+/**Function********************************************************************
+
+  Synopsis    [Delocates symmetry information structure.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_SymmPairsDissolve( Extra_SymmInfo_t * p )
+{
+    free( p->pVars );
+    free( p->pSymms[0] );
+    free( p->pSymms    );
+    free( p );
+} /* end of Extra_SymmPairsDissolve */
+
+/**Function********************************************************************
+
+  Synopsis    [Allocates symmetry information structure.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_SymmPairsPrint( Extra_SymmInfo_t * p )
+{
+    int i, k;
+    printf( "\n" );
+    for ( i = 0; i < p->nVars; i++ )
+    {
+        for ( k = 0; k <= i; k++ )
+            printf( " " );
+        for ( k = i+1; k < p->nVars; k++ )
+            if ( p->pSymms[i][k] )
+                printf( "1" );
+            else
+                printf( "." );
+        printf( "\n" );
+    }
+} /* end of Extra_SymmPairsPrint */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Creates the symmetry information structure from ZDD.]
+
+  Description [ZDD representation of symmetries is the set of cubes, each
+  of which has two variables in the positive polarity. These variables correspond
+  to the symmetric variable pair.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+Extra_SymmInfo_t * Extra_SymmPairsCreateFromZdd( DdManager * dd, DdNode * zPairs, DdNode * bSupp )
+{
+    int i;
+    int nSuppSize;
+    Extra_SymmInfo_t * p;
+    int * pMapVars2Nums;
+    DdNode * bTemp;
+    DdNode * zSet, * zCube, * zTemp;
+    int iVar1, iVar2;
+
+    nSuppSize = Extra_bddSuppSize( dd, bSupp );
+
+    // allocate and clean the storage for symmetry info
+    p = Extra_SymmPairsAllocate( nSuppSize );
+
+    // allocate the storage for the temporary map
+    pMapVars2Nums = ALLOC( int, dd->size );
+    memset( pMapVars2Nums, 0, dd->size * sizeof(int) );
+
+    // assign the variables
+    p->nVarsMax = dd->size;
+//  p->nNodes   = Cudd_DagSize( zPairs );
+    p->nNodes   = 0;
+    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
+    {
+        p->pVars[i] = bTemp->index;
+        pMapVars2Nums[bTemp->index] = i;
+    }
+
+    // write the symmetry info into the structure
+    zSet = zPairs;   Cudd_Ref( zSet );
+    while ( zSet != z0 )
+    {
+        // get the next cube
+        zCube  = Extra_zddSelectOneSubset( dd, zSet );    Cudd_Ref( zCube );
+
+        // add these two variables to the data structure
+        assert( cuddT( cuddT(zCube) ) == z1 );
+        iVar1 = zCube->index/2;
+        iVar2 = cuddT(zCube)->index/2;
+        if ( pMapVars2Nums[iVar1] < pMapVars2Nums[iVar2] )
+            p->pSymms[ pMapVars2Nums[iVar1] ][ pMapVars2Nums[iVar2] ] = 1;
+        else
+            p->pSymms[ pMapVars2Nums[iVar2] ][ pMapVars2Nums[iVar1] ] = 1;
+        // count the symmetric pairs
+        p->nSymms ++;
+
+        // update the cuver and deref the cube
+        zSet = Cudd_zddDiff( dd, zTemp = zSet, zCube );     Cudd_Ref( zSet );
+        Cudd_RecursiveDerefZdd( dd, zTemp );
+        Cudd_RecursiveDerefZdd( dd, zCube );
+
+    } // for each cube 
+    Cudd_RecursiveDerefZdd( dd, zSet );
+
+    FREE( pMapVars2Nums );
+    return p;
+
+} /* end of Extra_SymmPairsCreateFromZdd */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Checks the possibility of two variables being symmetric.]
+
+  Description [Returns 0 if vars are not symmetric. Return 1 if vars can be symmetric.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddCheckVarsSymmetric( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bF,
+  int iVar1,
+  int iVar2) 
+{
+    DdNode * bVars;
+    int Res;
+
+//  return 1;
+
+    assert( iVar1 != iVar2 );
+    assert( iVar1 < dd->size );
+    assert( iVar2 < dd->size );
+
+    bVars = Cudd_bddAnd( dd, dd->vars[iVar1], dd->vars[iVar2] );   Cudd_Ref( bVars );
+
+    Res = (int)( extraBddCheckVarsSymmetric( dd, bF, bVars ) == b1 );
+
+    Cudd_RecursiveDeref( dd, bVars );
+
+    return Res;
+} /* end of Extra_bddCheckVarsSymmetric */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the classical symmetry information for the function.]
+
+  Description [Uses the naive way of comparing cofactors.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+Extra_SymmInfo_t * Extra_SymmPairsComputeNaive( DdManager * dd, DdNode * bFunc )
+{
+    DdNode * bSupp, * bTemp;
+    int nSuppSize;
+    Extra_SymmInfo_t * p;
+    int i, k;
+
+    // compute the support
+    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
+    nSuppSize = Extra_bddSuppSize( dd, bSupp );
+//printf( "Support = %d. ", nSuppSize );
+//Extra_bddPrint( dd, bSupp );
+//printf( "%d ", nSuppSize );
+
+    // allocate the storage for symmetry info
+    p = Extra_SymmPairsAllocate( nSuppSize );
+
+    // assign the variables
+    p->nVarsMax = dd->size;
+    for ( i = 0, bTemp = bSupp; bTemp != b1; bTemp = cuddT(bTemp), i++ )
+        p->pVars[i] = bTemp->index;
+
+    // go through the candidate pairs and check using Idea1
+    for ( i = 0; i < nSuppSize; i++ )
+    for ( k = i+1; k < nSuppSize; k++ )
+    {
+        p->pSymms[k][i] = p->pSymms[i][k] = Extra_bddCheckVarsSymmetricNaive( dd, bFunc, p->pVars[i], p->pVars[k] );
+        if ( p->pSymms[i][k] )
+             p->nSymms++;
+    }
+
+    Cudd_RecursiveDeref( dd, bSupp );
+    return p;
+
+} /* end of Extra_SymmPairsComputeNaive */
+
+/**Function********************************************************************
+
+  Synopsis    [Checks if the two variables are symmetric.]
+
+  Description [Returns 0 if vars are not symmetric. Return 1 if vars are symmetric.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Extra_bddCheckVarsSymmetricNaive( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bF,
+  int iVar1,
+  int iVar2) 
+{
+    DdNode * bCube1, * bCube2;
+    DdNode * bCof01, * bCof10;
+    int Res;
+
+    assert( iVar1 != iVar2 );
+    assert( iVar1 < dd->size );
+    assert( iVar2 < dd->size );
+
+    bCube1 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar1] ), dd->vars[iVar2] );   Cudd_Ref( bCube1 );
+    bCube2 = Cudd_bddAnd( dd, Cudd_Not( dd->vars[iVar2] ), dd->vars[iVar1] );   Cudd_Ref( bCube2 );
+
+    bCof01 = Cudd_Cofactor( dd, bF, bCube1 );  Cudd_Ref( bCof01 );
+    bCof10 = Cudd_Cofactor( dd, bF, bCube2 );  Cudd_Ref( bCof10 );
+
+    Res = (int)( bCof10 == bCof01 );
+
+    Cudd_RecursiveDeref( dd, bCof01 );
+    Cudd_RecursiveDeref( dd, bCof10 );
+    Cudd_RecursiveDeref( dd, bCube1 );
+    Cudd_RecursiveDeref( dd, bCube2 );
+
+    return Res;
+} /* end of Extra_bddCheckVarsSymmetricNaive */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Builds ZDD representing the set of fixed-size variable tuples.]
+
+  Description [Creates ZDD of all combinations of variables in Support that
+  is represented by a BDD.]
+
+  SideEffects [New ZDD variables are created if indices of the variables
+               present in the combination are larger than the currently
+               allocated number of ZDD variables.]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode* Extra_zddTuplesFromBdd( 
+  DdManager * dd,   /* the DD manager */
+  int K,            /* the number of variables in tuples */
+  DdNode * bVarsN)   /* the set of all variables represented as a BDD */
+{
+    DdNode  *zRes;
+    int     autoDynZ;
+
+    autoDynZ = dd->autoDynZ;
+    dd->autoDynZ = 0;
+
+    do {
+        /* transform the numeric arguments (K) into a DdNode* argument;
+         * this allows us to use the standard internal CUDD cache */
+        DdNode *bVarSet = bVarsN, *bVarsK = bVarsN;
+        int     nVars = 0, i;
+
+        /* determine the number of variables in VarSet */
+        while ( bVarSet != b1 )
+        {
+            nVars++;
+            /* make sure that the VarSet is a cube */
+            if ( cuddE( bVarSet ) != b0 )
+                return NULL;
+            bVarSet = cuddT( bVarSet );
+        }
+        /* make sure that the number of variables in VarSet is less or equal 
+           that the number of variables that should be present in the tuples
+        */
+        if ( K > nVars )
+            return NULL;
+
+        /* the second argument in the recursive call stannds for <n>;
+        /* reate the first argument, which stands for <k> 
+         * as when we are talking about the tuple of <k> out of <n> */
+        for ( i = 0; i < nVars-K; i++ )
+            bVarsK = cuddT( bVarsK );
+
+        dd->reordered = 0;
+        zRes = extraZddTuplesFromBdd(dd, bVarsK, bVarsN );
+
+    } while (dd->reordered == 1);
+    dd->autoDynZ = autoDynZ;
+    return zRes;
+
+} /* end of Extra_zddTuplesFromBdd */
+
+/**Function********************************************************************
+
+  Synopsis    [Selects one subset from the set of subsets represented by a ZDD.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode* Extra_zddSelectOneSubset( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * zS)      /* the ZDD */
+{
+    DdNode  *res;
+    do {
+        dd->reordered = 0;
+        res = extraZddSelectOneSubset(dd, zS);
+    } while (dd->reordered == 1);
+    return(res);
+
+} /* end of Extra_zddSelectOneSubset */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a recursive step of Extra_SymmPairsCompute.]
+
+  Description [Returns the set of symmetric variable pairs represented as a set 
+  of two-literal ZDD cubes. Both variables always appear in the positive polarity
+  in the cubes. This function works without building new BDD nodes. Some relatively 
+  small number of ZDD nodes may be built to ensure proper bookkeeping of the 
+  symmetry information.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * 
+extraZddSymmPairsCompute( 
+  DdManager * dd,   /* the manager */
+  DdNode * bFunc,   /* the function whose symmetries are computed */
+  DdNode * bVars )  /* the set of variables on which this function depends */
+{
+    DdNode * zRes;
+    DdNode * bFR = Cudd_Regular(bFunc); 
+
+    if ( cuddIsConstant(bFR) )
+    {
+        int nVars, i;
+
+        // determine how many vars are in the bVars
+        nVars = Extra_bddSuppSize( dd, bVars );
+        if ( nVars < 2 )
+            return z0;
+        else
+        {
+            DdNode * bVarsK;
+
+            // create the BDD bVarsK corresponding to K = 2;
+            bVarsK = bVars;
+            for ( i = 0; i < nVars-2; i++ )
+                bVarsK = cuddT( bVarsK );
+            return extraZddTuplesFromBdd( dd, bVarsK, bVars );
+        }
+    }
+    assert( bVars != b1 );
+
+    if ( zRes = cuddCacheLookup2Zdd(dd, extraZddSymmPairsCompute, bFunc, bVars) )
+        return zRes;
+    else
+    {
+        DdNode * zRes0, * zRes1;
+        DdNode * zTemp, * zPlus, * zSymmVars;             
+        DdNode * bF0, * bF1;             
+        DdNode * bVarsNew;
+        int nVarsExtra;
+        int LevelF;
+
+        // every variable in bF should be also in bVars, therefore LevelF cannot be above LevelV
+        // if LevelF is below LevelV, scroll through the vars in bVars to the same level as F
+        // count how many extra vars are there in bVars
+        nVarsExtra = 0;
+        LevelF = dd->perm[bFR->index];
+        for ( bVarsNew = bVars; LevelF > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) )
+            nVarsExtra++; 
+        // the indexes (level) of variables should be synchronized now
+        assert( bFR->index == bVarsNew->index );
+
+        // cofactor the function
+        if ( bFR != bFunc ) // bFunc is complemented 
+        {
+            bF0 = Cudd_Not( cuddE(bFR) );
+            bF1 = Cudd_Not( cuddT(bFR) );
+        }
+        else
+        {
+            bF0 = cuddE(bFR);
+            bF1 = cuddT(bFR);
+        }
+
+        // solve subproblems
+        zRes0 = extraZddSymmPairsCompute( dd, bF0, cuddT(bVarsNew) );
+        if ( zRes0 == NULL )
+            return NULL;
+        cuddRef( zRes0 );
+
+        // if there is no symmetries in the negative cofactor
+        // there is no need to test the positive cofactor
+        if ( zRes0 == z0 )
+            zRes = zRes0;  // zRes takes reference
+        else
+        {
+            zRes1 = extraZddSymmPairsCompute( dd, bF1, cuddT(bVarsNew) );
+            if ( zRes1 == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes0 );
+                return NULL;
+            }
+            cuddRef( zRes1 );
+
+            // only those variables are pair-wise symmetric 
+            // that are pair-wise symmetric in both cofactors
+            // therefore, intersect the solutions
+            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
+            if ( zRes == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes0 );
+                Cudd_RecursiveDerefZdd( dd, zRes1 );
+                return NULL;
+            }
+            cuddRef( zRes );
+            Cudd_RecursiveDerefZdd( dd, zRes0 );
+            Cudd_RecursiveDerefZdd( dd, zRes1 );
+        }
+
+        // consider the current top-most variable and find all the vars
+        // that are pairwise symmetric with it
+        // these variables are returned as a set of ZDD singletons
+        zSymmVars = extraZddGetSymmetricVars( dd, bF1, bF0, cuddT(bVarsNew) );
+        if ( zSymmVars == NULL )
+        {
+            Cudd_RecursiveDerefZdd( dd, zRes );
+            return NULL;
+        }
+        cuddRef( zSymmVars );
+
+        // attach the topmost variable to the set, to get the variable pairs
+        // use the positive polarity ZDD variable for the purpose
+
+        // there is no need to do so, if zSymmVars is empty
+        if ( zSymmVars == z0 )
+            Cudd_RecursiveDerefZdd( dd, zSymmVars );
+        else
+        {
+            zPlus = cuddZddGetNode( dd, 2*bFR->index, zSymmVars, z0 );
+            if ( zPlus == NULL ) 
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes );
+                Cudd_RecursiveDerefZdd( dd, zSymmVars );
+                return NULL;
+            }
+            cuddRef( zPlus );
+            cuddDeref( zSymmVars );
+
+            // add these variable pairs to the result
+            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
+            if ( zRes == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zTemp );
+                Cudd_RecursiveDerefZdd( dd, zPlus );
+                return NULL;
+            }
+            cuddRef( zRes );
+            Cudd_RecursiveDerefZdd( dd, zTemp );
+            Cudd_RecursiveDerefZdd( dd, zPlus );
+        }
+
+        // only zRes is referenced at this point
+
+        // if we skipped some variables, these variables cannot be symmetric with
+        // any variables that are currently in the support of bF, but they can be 
+        // symmetric with the variables that are in bVars but not in the support of bF
+        if ( nVarsExtra )
+        {
+            // it is possible to improve this step:
+            // (1) there is no need to enter here, if nVarsExtra < 2
+
+            // create the set of topmost nVarsExtra in bVars
+            DdNode * bVarsExtra;
+            int nVars;
+
+            // remove from bVars all the variable that are in the support of bFunc
+            bVarsExtra = extraBddReduceVarSet( dd, bVars, bFunc );  
+            if ( bVarsExtra == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes );
+                return NULL;
+            }
+            cuddRef( bVarsExtra );
+
+            // determine how many vars are in the bVarsExtra
+            nVars = Extra_bddSuppSize( dd, bVarsExtra );
+            if ( nVars < 2 )
+            {
+                Cudd_RecursiveDeref( dd, bVarsExtra );
+            }
+            else
+            {
+                int i;
+                DdNode * bVarsK;
+
+                // create the BDD bVarsK corresponding to K = 2;
+                bVarsK = bVarsExtra;
+                for ( i = 0; i < nVars-2; i++ )
+                    bVarsK = cuddT( bVarsK );
+
+                // create the 2 variable tuples
+                zPlus = extraZddTuplesFromBdd( dd, bVarsK, bVarsExtra );
+                if ( zPlus == NULL )
+                {
+                    Cudd_RecursiveDeref( dd, bVarsExtra );
+                    Cudd_RecursiveDerefZdd( dd, zRes );
+                    return NULL;
+                }
+                cuddRef( zPlus );
+                Cudd_RecursiveDeref( dd, bVarsExtra );
+
+                // add these to the result
+                zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
+                if ( zRes == NULL )
+                {
+                    Cudd_RecursiveDerefZdd( dd, zTemp );
+                    Cudd_RecursiveDerefZdd( dd, zPlus );
+                    return NULL;
+                }
+                cuddRef( zRes );
+                Cudd_RecursiveDerefZdd( dd, zTemp );
+                Cudd_RecursiveDerefZdd( dd, zPlus );
+            }
+        }
+        cuddDeref( zRes );
+
+
+        /* insert the result into cache */
+        cuddCacheInsert2(dd, extraZddSymmPairsCompute, bFunc, bVars, zRes);
+        return zRes;
+    }
+} /* end of extraZddSymmPairsCompute */
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a recursive step of Extra_zddGetSymmetricVars.]
+
+  Description [Returns the set of ZDD singletons, containing those positive
+  ZDD variables that correspond to BDD variables x, for which it is true 
+  that bF(x=0) == bG(x=1).]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraZddGetSymmetricVars( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bF,       /* the first function  - originally, the positive cofactor */
+  DdNode * bG,       /* the second function - originally, the negative cofactor */
+  DdNode * bVars)    /* the set of variables, on which F and G depend */
+{
+    DdNode * zRes;
+    DdNode * bFR = Cudd_Regular(bF); 
+    DdNode * bGR = Cudd_Regular(bG); 
+
+    if ( cuddIsConstant(bFR) && cuddIsConstant(bGR) )
+    {
+        if ( bF == bG )
+            return extraZddGetSingletons( dd, bVars );
+        else 
+            return z0;
+    }
+    assert( bVars != b1 );
+
+    if ( zRes = cuddCacheLookupZdd(dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars) )
+        return zRes;
+    else
+    {
+        DdNode * zRes0, * zRes1;             
+        DdNode * zPlus, * zTemp;
+        DdNode * bF0, * bF1;             
+        DdNode * bG0, * bG1;             
+        DdNode * bVarsNew;
+    
+        int LevelF = cuddI(dd,bFR->index);
+        int LevelG = cuddI(dd,bGR->index);
+        int LevelFG;
+
+        if ( LevelF < LevelG )
+            LevelFG = LevelF;
+        else
+            LevelFG = LevelG;
+
+        // at least one of the arguments is not a constant
+        assert( LevelFG < dd->size );
+
+        // every variable in bF and bG should be also in bVars, therefore LevelFG cannot be above LevelV
+        // if LevelFG is below LevelV, scroll through the vars in bVars to the same level as LevelFG
+        for ( bVarsNew = bVars; LevelFG > dd->perm[bVarsNew->index]; bVarsNew = cuddT(bVarsNew) );
+        assert( LevelFG == dd->perm[bVarsNew->index] );
+
+        // cofactor the functions
+        if ( LevelF == LevelFG )
+        {
+            if ( bFR != bF ) // bF is complemented 
+            {
+                bF0 = Cudd_Not( cuddE(bFR) );
+                bF1 = Cudd_Not( cuddT(bFR) );
+            }
+            else
+            {
+                bF0 = cuddE(bFR);
+                bF1 = cuddT(bFR);
+            }
+        }
+        else 
+            bF0 = bF1 = bF;
+
+        if ( LevelG == LevelFG )
+        {
+            if ( bGR != bG ) // bG is complemented 
+            {
+                bG0 = Cudd_Not( cuddE(bGR) );
+                bG1 = Cudd_Not( cuddT(bGR) );
+            }
+            else
+            {
+                bG0 = cuddE(bGR);
+                bG1 = cuddT(bGR);
+            }
+        }
+        else 
+            bG0 = bG1 = bG;
+
+        // solve subproblems
+        zRes0 = extraZddGetSymmetricVars( dd, bF0, bG0, cuddT(bVarsNew) );
+        if ( zRes0 == NULL ) 
+            return NULL;
+        cuddRef( zRes0 );
+
+        // if there is not symmetries in the negative cofactor
+        // there is no need to test the positive cofactor
+        if ( zRes0 == z0 )
+            zRes = zRes0;  // zRes takes reference
+        else
+        {
+            zRes1 = extraZddGetSymmetricVars( dd, bF1, bG1, cuddT(bVarsNew) );
+            if ( zRes1 == NULL ) 
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes0 );
+                return NULL;
+            }
+            cuddRef( zRes1 );
+
+            // only those variables should belong to the resulting set 
+            // for which the property is true for both cofactors
+            zRes = cuddZddIntersect( dd, zRes0, zRes1 );
+            if ( zRes == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes0 );
+                Cudd_RecursiveDerefZdd( dd, zRes1 );
+                return NULL;
+            }
+            cuddRef( zRes );
+            Cudd_RecursiveDerefZdd( dd, zRes0 );
+            Cudd_RecursiveDerefZdd( dd, zRes1 );
+        }
+
+        // add one more singleton if the property is true for this variable
+        if ( bF0 == bG1 )
+        {
+            zPlus = cuddZddGetNode( dd, 2*bVarsNew->index, z1, z0 );
+            if ( zPlus == NULL ) 
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes );
+                return NULL;
+            }
+            cuddRef( zPlus );
+
+            // add these variable pairs to the result
+            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
+            if ( zRes == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zTemp );
+                Cudd_RecursiveDerefZdd( dd, zPlus );
+                return NULL;
+            }
+            cuddRef( zRes );
+            Cudd_RecursiveDerefZdd( dd, zTemp );
+            Cudd_RecursiveDerefZdd( dd, zPlus );
+        }
+
+        if ( bF == bG && bVars != bVarsNew )
+        { 
+            // if the functions are equal, so are their cofactors
+            // add those variables from V that are above F and G 
+
+            DdNode * bVarsExtra;
+
+            assert( LevelFG > dd->perm[bVars->index] );
+
+            // create the BDD of the extra variables
+            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsNew );
+            if ( bVarsExtra == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zRes );
+                return NULL;
+            }
+            cuddRef( bVarsExtra );
+
+            zPlus = extraZddGetSingletons( dd, bVarsExtra );
+            if ( zPlus == NULL )
+            {
+                Cudd_RecursiveDeref( dd, bVarsExtra );
+                Cudd_RecursiveDerefZdd( dd, zRes );
+                return NULL;
+            }
+            cuddRef( zPlus );
+            Cudd_RecursiveDeref( dd, bVarsExtra );
+
+            // add these to the result
+            zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
+            if ( zRes == NULL )
+            {
+                Cudd_RecursiveDerefZdd( dd, zTemp );
+                Cudd_RecursiveDerefZdd( dd, zPlus );
+                return NULL;
+            }
+            cuddRef( zRes );
+            Cudd_RecursiveDerefZdd( dd, zTemp );
+            Cudd_RecursiveDerefZdd( dd, zPlus );
+        }
+        cuddDeref( zRes );
+
+        cuddCacheInsert( dd, DD_GET_SYMM_VARS_TAG, bF, bG, bVars, zRes );
+        return zRes;
+    }
+}   /* end of extraZddGetSymmetricVars */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a recursive step of Extra_zddGetSingletons.]
+
+  Description [Returns the set of ZDD singletons, containing those positive 
+  polarity ZDD variables that correspond to the BDD variables in bVars.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraZddGetSingletons( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bVars)    /* the set of variables */
+{
+    DdNode * zRes;
+
+    if ( bVars == b1 )
+//    if ( bVars == b0 )  // bug fixed by Jin Zhang, Jan 23, 2004
+        return z1;
+
+    if ( zRes = cuddCacheLookup1Zdd(dd, extraZddGetSingletons, bVars) )
+        return zRes;
+    else
+    {
+        DdNode * zTemp, * zPlus;          
+
+        // solve subproblem
+        zRes = extraZddGetSingletons( dd, cuddT(bVars) );
+        if ( zRes == NULL ) 
+            return NULL;
+        cuddRef( zRes );
+        
+        zPlus = cuddZddGetNode( dd, 2*bVars->index, z1, z0 );
+        if ( zPlus == NULL ) 
+        {
+            Cudd_RecursiveDerefZdd( dd, zRes );
+            return NULL;
+        }
+        cuddRef( zPlus );
+
+        // add these to the result
+        zRes = cuddZddUnion( dd, zTemp = zRes, zPlus );
+        if ( zRes == NULL )
+        {
+            Cudd_RecursiveDerefZdd( dd, zTemp );
+            Cudd_RecursiveDerefZdd( dd, zPlus );
+            return NULL;
+        }
+        cuddRef( zRes );
+        Cudd_RecursiveDerefZdd( dd, zTemp );
+        Cudd_RecursiveDerefZdd( dd, zPlus );
+        cuddDeref( zRes );
+
+        cuddCacheInsert1( dd, extraZddGetSingletons, bVars, zRes );
+        return zRes;
+    }
+}   /* end of extraZddGetSingletons */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs a recursive step of Extra_bddReduceVarSet.]
+
+  Description [Returns the set of all variables in the given set that are not in the 
+  support of the given function.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraBddReduceVarSet( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bVars,    /* the set of variables to be reduced */
+  DdNode * bF)       /* the function whose support is used for reduction */
+{
+    DdNode * bRes;
+    DdNode * bFR = Cudd_Regular(bF);
+
+    if ( cuddIsConstant(bFR) || bVars == b1 )
+        return bVars;
+
+    if ( bRes = cuddCacheLookup2(dd, extraBddReduceVarSet, bVars, bF) )
+        return bRes;
+    else
+    {
+        DdNode * bF0, * bF1;             
+        DdNode * bVarsThis, * bVarsLower, * bTemp;
+        int LevelF;
+
+        // if LevelF is below LevelV, scroll through the vars in bVars 
+        LevelF = dd->perm[bFR->index];
+        for ( bVarsThis = bVars; LevelF > cuddI(dd,bVarsThis->index); bVarsThis = cuddT(bVarsThis) );
+        // scroll also through the current var, because it should be not be added
+        if ( LevelF == cuddI(dd,bVarsThis->index) )
+            bVarsLower = cuddT(bVarsThis);
+        else
+            bVarsLower = bVarsThis;
+
+        // cofactor the function
+        if ( bFR != bF ) // bFunc is complemented 
+        {
+            bF0 = Cudd_Not( cuddE(bFR) );
+            bF1 = Cudd_Not( cuddT(bFR) );
+        }
+        else
+        {
+            bF0 = cuddE(bFR);
+            bF1 = cuddT(bFR);
+        }
+
+        // solve subproblems
+        bRes = extraBddReduceVarSet( dd, bVarsLower, bF0 );
+        if ( bRes == NULL ) 
+            return NULL;
+        cuddRef( bRes );
+
+        bRes = extraBddReduceVarSet( dd, bTemp = bRes, bF1 );
+        if ( bRes == NULL ) 
+        {
+            Cudd_RecursiveDeref( dd, bTemp );
+            return NULL;
+        }
+        cuddRef( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+
+        // the current var should not be added
+        // add the skipped vars
+        if ( bVarsThis != bVars )
+        {
+            DdNode * bVarsExtra;
+
+            // extract the skipped variables
+            bVarsExtra = cuddBddExistAbstractRecur( dd, bVars, bVarsThis );
+            if ( bVarsExtra == NULL )
+            {
+                Cudd_RecursiveDeref( dd, bRes );
+                return NULL;
+            }
+            cuddRef( bVarsExtra );
+
+            // add these variables
+            bRes = cuddBddAndRecur( dd, bTemp = bRes, bVarsExtra );
+            if ( bRes == NULL ) 
+            {
+                Cudd_RecursiveDeref( dd, bTemp );
+                Cudd_RecursiveDeref( dd, bVarsExtra );
+                return NULL;
+            }
+            cuddRef( bRes );
+            Cudd_RecursiveDeref( dd, bTemp );
+            Cudd_RecursiveDeref( dd, bVarsExtra );
+        }
+        cuddDeref( bRes );
+
+        cuddCacheInsert2( dd, extraBddReduceVarSet, bVars, bF, bRes );
+        return bRes;
+    }
+}   /* end of extraBddReduceVarSet */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Extra_bddCheckVarsSymmetric().]
+
+  Description [Returns b0 if the variables are not symmetric. Returns b1 if the
+  variables can be symmetric. The variables are represented in the form of a 
+  two-variable cube. In case the cube contains one variable (below Var1 level),
+  the cube's pointer is complemented if the variable Var1 occurred on the 
+  current path; otherwise, the cube's pointer is regular. Uses additional 
+  complemented bit (Hash_Not) to mark the result if in the BDD rooted that this
+  node there is a branch passing though the node labeled with Var2.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraBddCheckVarsSymmetric( 
+  DdManager * dd,    /* the DD manager */
+  DdNode * bF,
+  DdNode * bVars) 
+{
+    DdNode * bRes;
+
+    if ( bF == b0 )
+        return b1;
+
+    assert( bVars != b1 );
+    
+    if ( bRes = cuddCacheLookup2(dd, extraBddCheckVarsSymmetric, bF, bVars) )
+        return bRes;
+    else
+    {
+        DdNode * bRes0, * bRes1;
+        DdNode * bF0, * bF1;             
+        DdNode * bFR = Cudd_Regular(bF);
+        int LevelF = cuddI(dd,bFR->index);
+
+        DdNode * bVarsR = Cudd_Regular(bVars);
+        int fVar1Pres;
+        int iLev1;
+        int iLev2;
+
+        if ( bVarsR != bVars ) // cube's pointer is complemented
+        {
+            assert( cuddT(bVarsR) == b1 );
+            fVar1Pres = 1;                    // the first var is present on the path
+            iLev1 = -1;                       // we are already below the first var level
+            iLev2 = dd->perm[bVarsR->index];  // the level of the second var
+        }
+        else  // cube's pointer is NOT complemented
+        {
+            fVar1Pres = 0;                    // the first var is absent on the path
+            if ( cuddT(bVars) == b1 )
+            {
+                iLev1 = -1;                             // we are already below the first var level 
+                iLev2 = dd->perm[bVars->index];         // the level of the second var
+            }
+            else
+            {
+                assert( cuddT(cuddT(bVars)) == b1 );
+                iLev1 = dd->perm[bVars->index];         // the level of the first var 
+                iLev2 = dd->perm[cuddT(bVars)->index];  // the level of the second var
+            }
+        }
+
+        // cofactor the function
+        // the cofactors are needed only if we are above the second level
+        if ( LevelF < iLev2 )
+        {
+            if ( bFR != bF ) // bFunc is complemented 
+            {
+                bF0 = Cudd_Not( cuddE(bFR) );
+                bF1 = Cudd_Not( cuddT(bFR) );
+            }
+            else
+            {
+                bF0 = cuddE(bFR);
+                bF1 = cuddT(bFR);
+            }
+        }
+        else
+            bF0 = bF1 = NULL;
+
+        // consider five cases:
+        // (1) F is above iLev1
+        // (2) F is on the level iLev1
+        // (3) F is between iLev1 and iLev2
+        // (4) F is on the level iLev2
+        // (5) F is below iLev2
+
+        // (1) F is above iLev1
+        if ( LevelF < iLev1 )
+        {
+            // the returned result cannot have the hash attribute
+            // because we still did not reach the level of Var1;
+            // the attribute never travels above the level of Var1
+            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
+//          assert( !Hash_IsComplement( bRes0 ) );
+            assert( bRes0 != z0 );
+            if ( bRes0 == b0 )
+                bRes = b0;
+            else
+                bRes = extraBddCheckVarsSymmetric( dd, bF1, bVars );
+//          assert( !Hash_IsComplement( bRes ) );
+            assert( bRes != z0 );
+        }
+        // (2) F is on the level iLev1
+        else if ( LevelF == iLev1 )
+        {
+            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, Cudd_Not( cuddT(bVars) ) );
+            if ( bRes0 == b0 )
+                bRes = b0;
+            else
+            {
+                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, Cudd_Not( cuddT(bVars) ) );
+                if ( bRes1 == b0 )
+                    bRes = b0;
+                else
+                {
+//                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
+                    if ( bRes0 == z0 || bRes1 == z0 )
+                        bRes = b1;
+                    else
+                        bRes = b0;
+                }
+            }
+        }
+        // (3) F is between iLev1 and iLev2
+        else if ( LevelF < iLev2 )
+        {
+            bRes0 = extraBddCheckVarsSymmetric( dd, bF0, bVars );
+            if ( bRes0 == b0 )
+                bRes = b0;
+            else
+            {
+                bRes1 = extraBddCheckVarsSymmetric( dd, bF1, bVars );
+                if ( bRes1 == b0 )
+                    bRes = b0;
+                else
+                {
+//                  if ( Hash_IsComplement( bRes0 ) || Hash_IsComplement( bRes1 ) )
+//                      bRes = Hash_Not( b1 );
+                    if ( bRes0 == z0 || bRes1 == z0 )
+                        bRes = z0;
+                    else
+                        bRes = b1;
+                }
+            }
+        }
+        // (4) F is on the level iLev2
+        else if ( LevelF == iLev2 )
+        {
+            // this is the only place where the hash attribute (Hash_Not) can be added 
+            // to the result; it can be added only if the path came through the node
+            // lebeled with Var1; therefore, the hash attribute cannot be returned
+            // to the caller function
+            if ( fVar1Pres )
+//              bRes = Hash_Not( b1 );
+                bRes = z0;
+            else 
+                bRes = b0;
+        }
+        // (5) F is below iLev2
+        else // if ( LevelF > iLev2 )
+        {
+            // it is possible that the path goes through the node labeled by Var1
+            // and still everything is okay; we do not label with Hash_Not here
+            // because the path does not go through node labeled by Var2
+            bRes = b1;
+        }
+
+        cuddCacheInsert2(dd, extraBddCheckVarsSymmetric, bF, bVars, bRes);
+        return bRes;
+    }
+} /* end of extraBddCheckVarsSymmetric */
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_zddTupleFromBdd().]
+
+  Description [Generates in a bottom-up fashion ZDD for all combinations
+               composed of k variables out of variables belonging to Support.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode* extraZddTuplesFromBdd( 
+  DdManager * dd,   /* the DD manager */
+  DdNode * bVarsK,   /* the number of variables in tuples */
+  DdNode * bVarsN)   /* the set of all variables */
+{
+    DdNode *zRes, *zRes0, *zRes1;
+    statLine(dd); 
+
+    /* terminal cases */
+/*  if ( k < 0 || k > n )
+ *      return dd->zero;
+ *  if ( n == 0 )
+ *      return dd->one; 
+ */
+    if ( cuddI( dd, bVarsK->index ) < cuddI( dd, bVarsN->index ) )
+        return z0;
+    if ( bVarsN == b1 )
+        return z1;
+
+    /* check cache */
+    zRes = cuddCacheLookup2Zdd(dd, extraZddTuplesFromBdd, bVarsK, bVarsN);
+    if (zRes)
+        return(zRes);
+
+    /* ZDD in which this variable is 0 */
+/*  zRes0 = extraZddTuplesFromBdd( dd, k,     n-1 ); */
+    zRes0 = extraZddTuplesFromBdd( dd, bVarsK, cuddT(bVarsN) );
+    if ( zRes0 == NULL ) 
+        return NULL;
+    cuddRef( zRes0 );
+
+    /* ZDD in which this variable is 1 */
+/*  zRes1 = extraZddTuplesFromBdd( dd, k-1,          n-1 ); */
+    if ( bVarsK == b1 )
+    {
+        zRes1 = z0;
+        cuddRef( zRes1 );
+    }
+    else
+    {
+        zRes1 = extraZddTuplesFromBdd( dd, cuddT(bVarsK), cuddT(bVarsN) );
+        if ( zRes1 == NULL ) 
+        {
+            Cudd_RecursiveDerefZdd( dd, zRes0 );
+            return NULL;
+        }
+        cuddRef( zRes1 );
+    }
+
+    /* compose Res0 and Res1 with the given ZDD variable */
+    zRes = cuddZddGetNode( dd, 2*bVarsN->index, zRes1, zRes0 );
+    if ( zRes == NULL ) 
+    {
+        Cudd_RecursiveDerefZdd( dd, zRes0 );
+        Cudd_RecursiveDerefZdd( dd, zRes1 );
+        return NULL;
+    }
+    cuddDeref( zRes0 );
+    cuddDeref( zRes1 );
+
+    /* insert the result into cache */
+    cuddCacheInsert2(dd, extraZddTuplesFromBdd, bVarsK, bVarsN, zRes);
+    return zRes;
+
+} /* end of extraZddTuplesFromBdd */
+
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the recursive step of Extra_zddSelectOneSubset.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * extraZddSelectOneSubset( 
+  DdManager * dd, 
+  DdNode * zS )
+// selects one subset from the ZDD zS
+// returns z0 if and only if zS is an empty set of cubes
+{
+    DdNode * zRes;
+
+    if ( zS == z0 )    return z0;
+    if ( zS == z1 )    return z1;
+    
+    // check cache
+    if ( zRes = cuddCacheLookup1Zdd( dd, extraZddSelectOneSubset, zS ) )
+        return zRes;
+    else
+    {
+        DdNode * zS0, * zS1, * zTemp; 
+
+        zS0 = cuddE(zS);
+        zS1 = cuddT(zS);
+
+        if ( zS0 != z0 )
+        {
+            zRes = extraZddSelectOneSubset( dd, zS0 );
+            if ( zRes == NULL )
+                return NULL;
+        }
+        else // if ( zS0 == z0 )
+        {
+            assert( zS1 != z0 );
+            zRes = extraZddSelectOneSubset( dd, zS1 );
+            if ( zRes == NULL )
+                return NULL;
+            cuddRef( zRes );
+
+            zRes = cuddZddGetNode( dd, zS->index, zTemp = zRes, z0 );
+            if ( zRes == NULL ) 
+            {
+                Cudd_RecursiveDerefZdd( dd, zTemp );
+                return NULL;
+            }
+            cuddDeref( zTemp );
+        }
+
+        // insert the result into cache
+        cuddCacheInsert1( dd, extraZddSelectOneSubset, zS, zRes );
+        return zRes;
+    }       
+} /* end of extraZddSelectOneSubset */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/extraUtilReader.c b/src/misc/extra/extraUtilReader.c
index 2dc597bf..042dfaca 100644
--- a/src/misc/extra/extraUtilReader.c
+++ b/src/misc/extra/extraUtilReader.c
@@ -321,6 +321,7 @@ void * Extra_FileReaderGetTokens_int( Extra_FileReader_t * p )
     // through EXTRA_OFFSET_SIZE chars till the end of the buffer
     if ( p->pBufferStop == p->pBufferEnd ) // end of file
     {
+        *pChar = 0;
         p->fStop = 1;
         return p->vTokens;
     }
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 3098a23c..6cbf5d2c 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/misc/extra/extraUtilBdd.c \
+SRC +=    src/misc/extra/extraBddMisc.c \
+    src/misc/extra/extraBddSymm.c \
     src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilCanon.c \
     src/misc/extra/extraUtilFile.c \
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index bb911bfe..af7ca571 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -52,7 +52,7 @@ struct Vec_Vec_t_
 #define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
     for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
-    for ( i = LevelStart; (i < Vec_PtrSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
+    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
     for ( i = LevelStart; (i <= LevelStop) && (((vVec) = Vec_VecEntry(vGlob, i)), 1); i++ )
 #define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
@@ -234,6 +234,25 @@ static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
     Vec_PtrPush( p->pArray[Level], Entry );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+        Vec_VecPush( p, Level, Entry );
+    else
+        Vec_PtrPushUnique( p->pArray[Level], Entry );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////