Version abc51005

18 files changed, 2127 insertions, 76 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ca9f1dfa..cde9c16b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32,6 +32,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintExdc    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintLatch   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -39,6 +40,7 @@ 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_CommandPrintKMap    ( 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 );
@@ -61,12 +63,16 @@ static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReorder      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -93,6 +99,7 @@ static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -114,7 +121,10 @@ static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
+//    Abc_NtkBddImplicationTest();
+
     Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 ); 
+    Cmd_CommandAdd( pAbc, "Printing",     "print_exdc",    Abc_CommandPrintExdc,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
@@ -122,6 +132,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     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",     "print_kmap",    Abc_CommandPrintKMap,        0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
@@ -139,17 +150,21 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
 
-    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
+//    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "one_output",    Abc_CommandOneOutput,        1 );
     Cmd_CommandAdd( pAbc, "Various",      "one_node",      Abc_CommandOneNode,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
@@ -176,6 +191,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "seq_sweep",     Abc_CommandSeqSweep,         1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
@@ -248,7 +264,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pNtk == NULL )
     {
-        fprintf( Abc_FrameReadErr(pAbc), "Empty network\n" );
+        fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
         return 1;
     }
     Abc_NtkPrintStats( pOut, pNtk, fFactor );
@@ -256,7 +272,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: print_stats [-fh]\n" );
-    fprintf( pErr, "\t        prints the network statistics and\n" );
+    fprintf( pErr, "\t        prints the network statistics\n" );
     fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -273,6 +289,98 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    double Percentage;
+    bool fShort;
+    int c;
+    int fPrintDc;
+
+    extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    fShort  = 1;
+    fPrintDc = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "sdh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fShort ^= 1;
+            break;
+        case 'd':
+            fPrintDc ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
+        return 1;
+    }
+    if ( pNtk->pExdc == NULL )
+    {
+        fprintf( Abc_FrameReadErr(pAbc), "Network has no EXDC.\n" );
+        return 1;
+    }
+
+    if ( fPrintDc )
+    {
+        if ( !Abc_NtkIsStrash(pNtk->pExdc) )
+        {
+            pNtkTemp = Abc_NtkStrash(pNtk->pExdc, 0, 0);
+            Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtkTemp, 0) ) );
+            Abc_NtkDelete( pNtkTemp );
+        }
+        else
+            Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtk->pExdc, 0) ) );
+
+        printf( "EXDC network statistics: " );
+        printf( "(" );
+        if ( Percentage > 0.05 && Percentage < 99.95 )
+            printf( "%.2f", Percentage );
+        else if ( Percentage > 0.000005 && Percentage < 99.999995 )
+            printf( "%.6f", Percentage );
+        else
+            printf( "%f", Percentage );
+        printf( " %% don't-cares)\n" );
+    }
+    else
+        printf( "EXDC network statistics: \n" );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0 );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_exdc [-dh]\n" );
+    fprintf( pErr, "\t        prints the EXDC network statistics\n" );
+    fprintf( pErr, "\t-d    : toggles printing don't-care percentage [default = %s]\n", fPrintDc? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -754,6 +862,94 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    int fUseRealNames;
+
+    extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseRealNames = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'n':
+            fUseRealNames ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
+        return 1;
+    }
+    if ( argc > util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+    if ( argc == util_optind )
+    {
+        pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+        if ( !Abc_ObjIsNode(pNode) )
+        {
+            fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) );
+            return 1;
+        }
+    }
+    else
+    {
+        pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+        if ( pNode == NULL )
+        {
+            fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+            return 1;
+        }
+    }
+    Abc_NodePrintKMap( pNode, fUseRealNames );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_kmap [-nh] <node>\n" );
+    fprintf( pErr, "          shows the truth table of the node\n" );
+    fprintf( pErr, "\t-n    : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\tnode  : the node to consider (default = the driver of the first PO)\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -787,21 +983,32 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" );
+        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
         return 1;
     }
 
-    if ( argc != util_optind + 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 )
+    if ( argc == util_optind )
     {
-        fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
-        return 1;
+        pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+        if ( !Abc_ObjIsNode(pNode) )
+        {
+            fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) );
+            return 1;
+        }
+    }
+    else
+    {
+        pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+        if ( pNode == NULL )
+        {
+            fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+            return 1;
+        }
     }
     Abc_NodeShowBdd( pNode );
     return 0;
@@ -813,7 +1020,7 @@ usage:
     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, "\tnode  : the node to consider\n");
+    fprintf( pErr, "\tnode  : the node to consider [default = the driver of the first PO]\n");
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1423,7 +1630,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (unmap it first).\n" );
+        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (run \"unmap\").\n" );
         return 1;
     }
     // modify the current network
@@ -1666,7 +1873,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_NtkIsBddLogic( pNtk ) )
         {
-            fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
+            fprintf( pErr, "This command is only applicable to logic BDD networks (run \"bdd\").\n" );
             return 1;
         }
         fprintf( stdout, "Performing simple non-recursive DSD of local functions.\n" );
@@ -2233,7 +2440,6 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    // get the new network
     if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" );
@@ -2264,6 +2470,69 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+    extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Variable reordering is possible when node functions are BDDs (run \"bdd\").\n" );
+        return 1;
+    }
+    Abc_NtkBddReorder( pNtk, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: reorder [-vh]\n" );
+    fprintf( pErr, "\t         reorders local functions of the nodes using sifting\n" );
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2559,7 +2828,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Cannot find CO node \"%s\".\n", argv[util_optind] );
             return 1;
         }
-        pNtkRes = Abc_NtkSplitOutput( pNtk, pNode, fUseAllCis );
+        pNtkRes = Abc_NtkCreateOutput( pNtk, pNode, fUseAllCis );
     }
     else
     {
@@ -2573,7 +2842,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) );
             return 1;
         }
-        pNtkRes = Abc_NtkSplitOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis );
+        pNtkRes = Abc_NtkCreateOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis );
     }
     if ( pNtkRes == NULL )
     {
@@ -2654,7 +2923,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkSplitNode( pNtk, pNode );
+    pNtkRes = Abc_NtkCreateFromNode( pNtk, pNode );
 //    pNtkRes = Abc_NtkDeriveFromBdd( pNtk->pManFunc, pNode->pData, NULL, NULL );
     if ( pNtkRes == NULL )
     {
@@ -2735,6 +3004,210 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( pNtk->pExdc == NULL )
+    {
+        fprintf( pErr, "The network has no EXDC.\n" );
+        return 1;
+    }
+
+    Abc_NtkDelete( pNtk->pExdc );
+    pNtk->pExdc = NULL;
+
+    // replace the current network
+    pNtkRes = Abc_NtkDup( pNtk );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_free [-h]\n" );
+    fprintf( pErr, "\t         frees the EXDC network of the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( pNtk->pExdc == NULL )
+    {
+        fprintf( pErr, "The network has no EXDC.\n" );
+        return 1;
+    }
+
+    // replace the current network
+    pNtkRes = Abc_NtkDup( pNtk->pExdc );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_get [-h]\n" );
+    fprintf( pErr, "\t         replaces the current network by the EXDC of the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
+    char * FileName;
+    int c;
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    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
+    pNtkNew = Io_Read( FileName, 1 );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+        return 1;
+    }
+
+    // replace the EXDC
+    if ( pNtk->pExdc )
+    {
+        Abc_NtkDelete( pNtk->pExdc );
+        pNtk->pExdc = NULL;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    pNtkRes->pExdc = pNtkNew;
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_set [-h] <file>\n" );
+    fprintf( pErr, "\t         sets the network from file as EXDC for the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : file with the new EXDC network\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
@@ -3038,6 +3511,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fAllNodes;
+    int fExdc;
     int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -3045,6 +3519,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fExdc     = 0;
     fAllNodes = 0;
     memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = 2048; // the number of words of random simulation info
@@ -3059,7 +3534,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerbose   =  0;   // the verbosiness flag
     pParams->fVerboseP  =  0;   // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "RDBrscpvaeh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3115,6 +3590,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fAllNodes ^= 1;
             break;
+        case 'e':
+            fExdc ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -3138,11 +3616,11 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -3170,6 +3648,7 @@ usage:
     fprintf( pErr, "\t-c     : toggle accumulation of choices [default = %s]\n",              pParams->fChoicing? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle proving the final miter [default = %s]\n",              pParams->fTryProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->fVerbose?  "yes": "no" );
+    fprintf( pErr, "\t-e     : toggle functional sweeping using EXDC [default = %s]\n",       fExdc? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -3430,7 +3909,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int fUseInv;
+    int fExdc;
     int fVerbose;
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3438,15 +3919,19 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fUseInv   = 1;
+    fExdc     = 0;
     fVerbose  = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ivh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "ievh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'i':
             fUseInv ^= 1;
             break;
+        case 'e':
+            fExdc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3473,7 +3958,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fVerbose ) )
+    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) )
     {
         fprintf( pErr, "Sweeping has failed.\n" );
         return 1;
@@ -3481,9 +3966,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fraig_sweep [-vh]\n" );
+    fprintf( pErr, "usage: fraig_sweep [-evh]\n" );
     fprintf( pErr, "\t        performs technology-dependent sweep\n" );
-//    fprintf( pErr, "\t-i    : toggle using inverter for complemented nodes [default = %s]\n", fUseInv? "yes": "no" );
+    fprintf( pErr, "\t-e    : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-v    : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -3513,6 +3998,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int c;
     extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3603,7 +4089,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     if ( fSweep )
-        Abc_NtkFraigSweep( pNtkRes, 0, 0 );
+        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 );
 
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -4517,6 +5003,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
+return 0;
 
     // get the new network
     pNtkRes = Abc_NtkFpgaSeq( pNtk, fVerbose );
@@ -4588,6 +5075,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
+return 0;
 
     // get the new network
     pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose );
@@ -4608,6 +5096,109 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nFrames;
+    int fExdc;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames  = 1;
+    fExdc    = 1;
+    fVerbose = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'e':
+            fExdc ^= 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_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for combinational networks (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Works only for structurally hashed networks (run \"strash\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" );
+    fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
+    fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index c612a1ce..9b5f7d5b 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -52,6 +52,8 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
     Abc_NtkFinalize( pNtk, pNtkAig );
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 8c2f5bd3..9de61389 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -69,6 +69,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 5b317994..7e81c579 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -76,6 +76,9 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     Extra_StopManager( pNtk->pManGlob );
     pNtk->pManGlob = NULL;
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index ea97826a..161607b5 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -88,6 +88,9 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 5657fe38..421cdfed 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -26,12 +26,16 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t *   Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t *   Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
-
-static int           Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
-static void          Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
+static Abc_Ntk_t *    Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Ntk_t *    Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Obj_t *    Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
+static void           Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
+extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
+static void           Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+
+static int            Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
+static void           Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *    Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -48,19 +52,27 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
+Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
     Fraig_Man_t * pMan;
+    // check if EXDC is present
+    if ( fExdc && pNtk->pExdc == NULL )
+        fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
     // perform fraiging
-    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); 
+    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
     // prove the miter if asked to
     if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
     // reconstruct FRAIG in the new network
-    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+    if ( fExdc ) 
+        pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
+    else
+        pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
     Fraig_ManFree( pMan );
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -82,14 +94,13 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
+void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
+    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     Fraig_Man_t * pMan;
     ProgressBar * pProgress;
-    Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1;
-    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
+    Abc_Obj_t * pNode;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -97,11 +108,12 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
     // create the FRAIG manager
     pMan = Fraig_ManCreate( pParams );
 
-    // create PIs and remember them in the old nodes
+    // map the constant node
     Abc_NtkCleanCopy( pNtk );
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // create PIs and remember them in the old nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
-    pConst1 = Abc_AigConst1( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -109,21 +121,22 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
         pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         if ( !fInternal )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( pNode == pConst1 )
-            pNodeFraig = Fraig_ManReadConst1(pMan);
-        else
-            pNodeFraig = Fraig_NodeAnd( pMan, 
+        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
                 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
-        assert( pNode->pCopy == NULL );
-        pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
     }
     if ( !fInternal )
         Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
+    // use EXDC to change the mapping of nodes into FRAIG nodes
+    if ( fExdc )
+        Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
+
     // set the primary outputs
     Abc_NtkForEachCo( pNtk, pNode, i )
         Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
@@ -132,7 +145,123 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms FRAIG into what looks like a strashed network.]
+  Synopsis    [Derives EXDC node for the given network.]
+
+  Description [Assumes that EXDCs of all POs are the same.
+  Returns the EXDC of the first PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
+{
+    Abc_Ntk_t * pNtkStrash;
+    Abc_Obj_t * pObj;
+    Fraig_Node_t * gResult;
+    char ** ppNames;
+    int i, k;
+    // strash the EXDC network
+    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0 );
+    Abc_NtkCleanCopy( pNtkStrash );
+    Abc_AigConst1(pNtkStrash->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // set the mapping of the PI nodes
+    ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
+    Abc_NtkForEachCi( pNtkStrash, pObj, i )
+    {
+        for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
+            if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
+            {
+                pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
+                break;
+            }
+        assert( pObj->pCopy != NULL );
+    }
+    free( ppNames );
+    // build FRAIG for each node
+    Abc_AigForEachAnd( pNtkStrash, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
+                Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ),
+                Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ) );
+    // get the EXDC to be returned
+    pObj = Abc_NtkPo( pNtkStrash, 0 );
+    gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Abc_NtkDelete( pNtkStrash );
+    return gResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Changes mapping of the old nodes into FRAIG nodes using EXDC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Fraig_Node_t * gNodeNew, * gNodeExdc;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Abc_Obj_t * pNode, * pNodeBest;
+    Abc_Obj_t * pClass, ** ppSlot;
+    Vec_Ptr_t * vNexts;
+    int i;
+
+    // get the global don't-cares
+    assert( pNtk->pExdc );
+    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
+
+    // save the next pointers
+    vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );
+
+    // find the classes of AIG nodes which have FRAIG nodes assigned
+    Abc_NtkCleanNext( pNtk );
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
+                *ppSlot = NULL;
+            pNode->pNext = *ppSlot;
+            *ppSlot = pNode;
+        }
+
+    // for reach non-trival class, find the node with minimum level, and replace other nodes by it
+    Abc_AigSetNodePhases( pNtk );
+    stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
+    {
+        if ( pClass->pNext == NULL )
+            continue;
+        // find the node with minimum level
+        pNodeBest = pClass;
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            if ( pNodeBest->Level > pNode->Level )
+                 pNodeBest = pNode;
+        // remap the class nodes
+        for ( pNode = pClass; pNode; pNode = pNode->pNext )
+            pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
+    }
+    stmm_free_table( tTable );
+
+    // restore the next pointers
+    Abc_NtkCleanNext( pNtk );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pNext = Vec_PtrEntry( vNexts, pNode->Id );
+    Vec_PtrFree( vNexts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network with choices.]
 
   Description []
                
@@ -229,6 +358,110 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
     return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network without choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    stmm_table * tTable;
+    Vec_Ptr_t * vNodeReprs;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pRepr, ** ppSlot;
+    int i;
+
+    // map the nodes into their lowest level representives
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+        *ppSlot = pNode;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+            *ppSlot = pNode;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+                *ppSlot = pNode;
+            else if ( (*ppSlot)->Level > pNode->Level )
+                *ppSlot = pNode;
+        }
+    // save representatives for each node
+    vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {           
+            if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
+                assert( 0 );
+            if ( pNode != pRepr )
+                Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
+        }
+    stmm_free_table( tTable );
+
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+
+    // perform strashing
+    Abc_AigSetNodePhases( pNtk );
+    Abc_NtkIncrementTravId( pNtk );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodeReprs );
+
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms into AIG one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
+{
+    Abc_Obj_t * pRepr;
+    // skip the PIs and constants
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    assert( Abc_ObjIsNode( pNode ) );
+    // get the node's representative
+    if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) )
+    {
+        Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
+        pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
+        return;
+    }
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
+    pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+}
 
 
 
@@ -507,7 +740,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 
 //    Fraig_ManReportChoices( p );
     // transform it into FRAIG
-    pFraig = Abc_NtkFraig( pStore, &Params, 1 );
+    pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
     if ( pFraig == NULL )
         return NULL;
     Abc_NtkDelete( pStore );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 7e83b4f0..0f727006 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -113,6 +113,9 @@ clk = clock();
         return NULL;
     Map_ManFree( pMan );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index c5a9f5f3..0017a9de 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -31,6 +31,10 @@ static void        Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter,
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes );
 
+// to be exported 
+typedef void (*AddFrameMapping)( Abc_Obj_t*, Abc_Obj_t*, int, void*);
+extern Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg );
+static void        Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -598,6 +602,178 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the timeframes of the network.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
+{
+    char Buffer[100];
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkFrames;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pLatch, * pLatchNew;
+    int i, Counter;
+    assert( nFrames > 0 );
+    assert( Abc_NtkIsStrash(pNtk) );   
+    // start the new network
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
+    pNtkFrames->pName = util_strsav(Buffer);
+    // create new latches (or their initial values) and remember them in the new latches
+    if ( !fInitial )
+    {
+        Abc_NtkForEachLatch( pNtk, pLatch, i ) {
+            Abc_NtkDupObj( pNtkFrames, pLatch );
+            if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
+        }
+    }
+    else
+    {
+        Counter = 0;
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
+            {
+                pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
+                Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) );
+                Counter++;
+            }
+            else {
+                pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
+            }
+ 
+            if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
+        }
+        if ( Counter )
+            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
+    }
+    
+    // create the timeframes
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, nFrames );
+    for ( i = 0; i < nFrames; i++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Abc_NtkAddFrame2( pNtkFrames, pNtk, i, vNodes, addFrameMapping, arg );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    
+    // connect the new latches to the outputs of the last frame
+    if ( !fInitial )
+    {
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            pLatchNew = Abc_NtkLatch(pNtkFrames, i);
+            Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
+
+            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
+            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
+            Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
+        }
+    }
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pNext = NULL;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+    
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkFrames ) )
+    {
+        printf( "Abc_NtkFrames: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkFrames );
+        return NULL;
+    }
+    return pNtkFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one time frame to the new network.]
+
+  Description [Assumes that the latches of the old network point
+  to the outputs of the previous frame of the new network (pLatch->pCopy). 
+  In the end, updates the latches of the old network to point to the 
+  outputs of the current frame of the new network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg )
+{
+    char Buffer[10];
+    Abc_Obj_t * pNode, * pNodeNew, * pLatch;
+    Abc_Obj_t * pConst1, * pConst1New;
+    int i;
+    // get the constant nodes
+    pConst1    = Abc_AigConst1( pNtk->pManFunc );
+    pConst1New = Abc_AigConst1( pNtkFrames->pManFunc );
+    // create the prefix to be added to the node names
+    sprintf( Buffer, "_%02d", iFrame );
+    // add the new PI nodes
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
+        Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // add the internal nodes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( pNode == pConst1 )
+            pNodeNew = pConst1New;
+        else
+            pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+        pNode->pCopy = pNodeNew;
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // add the new POs
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
+        Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) );
+        Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // transfer the implementation of the latch drivers to the latches
+
+    // it is important that these two steps are performed it two loops
+    // and not in the same loop
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+        pLatch->pNext = Abc_ObjChild0Copy(pLatch);
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+        pLatch->pCopy = pLatch->pNext;
+
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+    {
+        if (addFrameMapping) {
+            // don't give Mike complemented pointers because he doesn't like it
+            if (Abc_ObjIsComplement(pLatch->pCopy)) {            
+                pNodeNew = Abc_NtkCreateNode( pNtkFrames );
+                Abc_ObjAddFanin( pNodeNew, pLatch->pCopy );
+                assert(Abc_ObjFaninNum(pNodeNew) == 1);
+                pNodeNew->Level = 1 + Abc_ObjRegular(pLatch->pCopy)->Level;
+
+                pLatch->pNext = pNodeNew;
+                pLatch->pCopy = pNodeNew;
+            }
+            addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg);
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 8aee5014..d88e5370 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -394,6 +394,159 @@ void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
     pNtk->vFuncsGlob = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the BDD of the logic cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNodeR;
+    DdManager * dd;
+    DdNode * bFunc;
+    double Result;
+    int i;
+    pNodeR = Abc_ObjRegular(pNode);
+    assert( Abc_NtkIsStrash(pNodeR->pNtk) );
+    Abc_NtkCleanCopy( pNodeR->pNtk );
+    // get the CIs in the support of the node
+    vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
+    // start the manager
+    dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    // assign elementary BDDs for the CIs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
+    // build the BDD of the cone
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR );  Cudd_Ref( bFunc );
+    bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
+    // count minterms
+    Result = Cudd_CountMinterm( dd, bFunc, dd->size );
+    // get the percentagle
+    Result *= 100.0;
+    for ( i = 0; i < dd->size; i++ )
+        Result /= 2;
+    // clean up
+    Cudd_Quit( dd );
+    Vec_PtrFree( vNodes );
+    return Result;
+}
+
+
+
+#include "reo.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDD of the local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    DdNode * bFunc;
+    int * pOrder, i;
+    // create the temporary array for the variable order
+    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
+    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+        pOrder[i] = -1;
+    // reorder the BDD
+    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
+    pNode->pData = bFunc;
+    // update the fanin order
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ].iFan;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pNode->vFanins.pArray[i].iFan = pOrder[i];
+    free( pOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs of the local functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    reo_man * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjFaninNum(pNode) < 3 )
+            continue;
+        if ( fVerbose )
+            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
+        if ( fVerbose )
+            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
+        Abc_NodeBddReorder( p, pNode );
+        if ( fVerbose )
+            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
+    }
+    Extra_ReorderQuit( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Experiment with BDD-based representation of implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddImplicationTest()
+{
+    DdManager * dd;
+    DdNode * bImp, * bSum, * bTemp;
+    int nVars = 200;
+    int nImps = 200;
+    int i, clk;
+clk = clock();
+    dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
+    bSum = b0;   Cudd_Ref( bSum );
+    for ( i = 0; i < nImps; i++ )
+    {
+        printf( "." );
+        bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] );  Cudd_Ref( bImp );
+        bSum = Cudd_bddOr( dd, bTemp = bSum, bImp );     Cudd_Ref( bSum );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bImp );
+    }
+    printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
+    printf( "The BDD after  = %d.\n", Cudd_DagSize(bSum) );
+PRT( "Time", clock() - clk );
+    Cudd_RecursiveDeref( dd, bSum );
+    Cudd_Quit( dd );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c
index 5142d66b..5a115410 100644
--- a/src/base/abci/abcPga.c
+++ b/src/base/abci/abcPga.c
@@ -75,6 +75,9 @@ Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2e9c3cc8..aff31f4c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -499,6 +499,33 @@ void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode )
     fprintf( pFile, "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
+{
+    Vec_Ptr_t * vNamesIn;
+    if ( fUseRealNames )
+    {
+        vNamesIn = Abc_NodeGetFaninNames(pNode);
+        Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), 
+            Abc_ObjFaninNum(pNode), NULL, 0, (char **)vNamesIn->pArray );
+        Abc_NodeFreeNames( vNamesIn );
+    }
+    else
+        Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), 
+            Abc_ObjFaninNum(pNode), NULL, 0, NULL );
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 3871b52c..672fd376 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -91,6 +91,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     }
 //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 8059f222..93f534ce 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -71,7 +71,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
         printf( "Cleanup has removed %d nodes.\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index fa840937..62cd5b55 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -25,10 +25,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static stmm_table *   Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
+static void           Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
-static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
-static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
+static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
+static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
@@ -52,7 +53,7 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
+bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig;
@@ -63,11 +64,24 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 
     // derive the AIG
     pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
+
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
-    pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );    
+    pMan = Abc_NtkToFraig( pNtkAig, &Params, 0, 0 );   
+    // cannot use EXDC with FRAIG because it can create classes of equivalent FRAIG nodes
+    // with representative nodes that do not correspond to the nodes with the current network
+
+    // update FRAIG using EXDC
+    if ( fExdc )
+    {
+        if ( pNtk->pExdc == NULL )
+            printf( "Warning: Networks has no EXDC.\n" );
+        else
+            Abc_NtkFraigSweepUsingExdc( pMan, pNtk );
+    }
+
     // collect the classes of equivalent nets
-    tEquiv = Abc_NtkFraigEquiv( pMan, pNtk, fUseInv, fVerbose );
+    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose );
 
     // transform the network into the equivalent one
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
@@ -90,6 +104,47 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Sweep the network using EXDC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Fraig_Node_t * gNodeExdc, * gNode, * gNodeRes;
+    Abc_Obj_t * pNode, * pNodeAig;
+    int i;
+    extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkExdc );
+
+    assert( pNtk->pExdc );
+    // derive FRAIG node representing don't-cares in the EXDC network
+    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
+    // update the node pointers
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip the constant input nodes
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
+        // get the strashed node
+        pNodeAig = pNode->pCopy;
+        // skip the dangling nodes
+        if ( pNodeAig == NULL )
+            continue;
+        // get the FRAIG node
+        gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) );
+        // perform ANDing with EXDC
+        gNodeRes = Fraig_NodeAnd( pMan, gNode, Fraig_Not(gNodeExdc) );
+        // write the node back
+        Abc_ObjRegular(pNodeAig)->pCopy = (Abc_Obj_t *)Fraig_NotCond( gNodeRes, Abc_ObjIsComplement(pNodeAig) );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects equivalence classses of node in the network.]
 
   Description []
@@ -99,7 +154,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
+stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
 {
     Abc_Obj_t * pList, * pNode, * pNodeAig;
     Fraig_Node_t * gNode;
@@ -113,14 +168,14 @@ stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv,
     tStrash2Net = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
     Abc_NtkForEachNode( pNtk, pNode, c )
     {
+        // skip the constant input nodes
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         // get the strashed node
         pNodeAig = pNode->pCopy;
         // skip the dangling nodes
         if ( pNodeAig == NULL )
             continue;
-        // skip the constant input nodes
-        if ( Abc_ObjFaninNum(pNode) == 0 )
-            continue;
         // skip the nodes that fanout into POs
         if ( Abc_NodeHasUniqueCoFanout(pNode) )
             continue;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 182d688d..e932d076 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -87,6 +87,8 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     // allocate ZDD variables
     Cudd_zddVarsFromBddVars( dd, 2 );
     // create the EXDC network representing the unreachable states
+    if ( pNtk->pExdc )
+        Abc_NtkDelete( pNtk->pExdc );
     pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
     Cudd_RecursiveDeref( dd, bUnreach );
     Extra_StopManager( dd );
@@ -283,9 +285,13 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
 
     // start the new network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtkNew->pName = util_strsav("exdc");
+    pNtkNew->pSpec = NULL;
+
     // create PIs corresponding to LOs
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) );
+    // cannot ADD POs here because pLatch->pCopy point to the PIs
 
     // create a new node
     pNodeNew = Abc_NtkCreateNode(pNtkNew);
@@ -304,21 +310,22 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     free( pPermute );
     Abc_NodeMinimumBase( pNodeNew );
 
-    // make the new node drive all the COs
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-
-    // store the PI names of the EXDC network
+    // for each CO, create PO (skip POs equal to CIs because of name conflict)
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
-    // store the PO names of the EXDC network
+        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") );
+
+    // link to the POs of the network 
     Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
 
-    // make the network minimum base
-    Abc_NtkMinimumBase( pNtkNew );
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
 
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
new file mode 100644
index 00000000..d0179514
--- /dev/null
+++ b/src/base/abci/abcVanEijk.c
@@ -0,0 +1,789 @@
+/**CFile****************************************************************
+
+  FileName    [abcVanEijk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implementation of van Eijk's method for finding
+  signal correspondence: C. A. J. van Eijk. "Sequential equivalence 
+  checking based on structural similarities", IEEE Trans. CAD, 
+  vol. 19(7), July 2000, pp. 814-819.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 2, 2005.]
+
+  Revision    [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Vec_Ptr_t *    Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+static Vec_Ptr_t *    Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames );
+static Vec_Ptr_t *    Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame );
+static int            Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses );
+static void           Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses );
+static int            Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses );
+static void           Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses );
+static Abc_Ntk_t *    Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
+static void           Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
+static Fraig_Man_t *  Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
+static Abc_Ntk_t *    Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses );
+
+////////////////////////////////////////////////////////////////////////
+///                     INLINED FUNCTIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// sets the correspondence of the node in the frame
+static inline void        Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) 
+{
+    Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); 
+}
+// returns the correspondence of the node in the frame
+static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) 
+{
+    return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); 
+}
+// returns the hash value of the node in the frame
+static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) 
+{
+    return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy );  
+}
+// returns the representative node of the class to which the node belongs
+static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) 
+{
+    if ( pNode->pNext == NULL )
+        return NULL;
+    while ( pNode->pNext )   
+        pNode = pNode->pNext;
+    return pNode;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives classes of sequentially equivalent nodes.]
+
+  Description [Performs sequential sweep by combining the equivalent
+  nodes. Adds EXDC network to the current network to record the subset
+  of unreachable states computed by identifying the equivalent nodes.]
+               
+  SideEffects []
+ 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose )
+{
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkSingle;
+    Vec_Ptr_t * vClasses;
+    Abc_Ntk_t * pNtkNew;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // FRAIG the network to get rid of combinational equivalences
+    Fraig_ParamsSetDefaultFull( &Params );
+    pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+    Abc_AigSetNodePhases( pNtkSingle );
+
+    // get the equivalence classes
+    vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose );
+    if ( Vec_PtrSize(vClasses) > 0 )
+    {
+        // transform the network by merging nodes in the equivalence classes
+        pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 );
+//        pNtkNew = Abc_NtkDup( pNtkSingle );  
+        // derive the EXDC network if asked
+        if ( fExdc )
+            pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses );
+    }
+    else
+        pNtkNew = Abc_NtkDup( pNtkSingle );  
+    Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses );
+    Vec_PtrFree( vClasses );
+
+    Abc_NtkDelete( pNtkSingle );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the classes of sequentially equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose )
+{
+    Fraig_Man_t * pFraig;
+    Abc_Ntk_t * pNtkMulti;
+    Vec_Ptr_t * vCorresp, * vClasses;
+    int nIter, RetValue;
+
+    if ( fVerbose )
+        printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) );
+
+    // get the AIG of the base case
+    vCorresp = Vec_PtrAlloc( 100 );
+    Abc_NtkCleanNext(pNtkSingle);
+    pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 );
+    if ( fVerbose )
+        printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) );
+
+    // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
+    pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 );
+    Fraig_ManFree( pFraig );
+
+    // find initial equivalence classes
+    vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames );
+    if ( fVerbose )
+        printf( "The number of classes in the base case    = %5d.  Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
+    Abc_NtkDelete( pNtkMulti );
+
+    // refine the classes using iterative FRAIGing
+    for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ )
+    {
+        // derive the network with equivalence classes
+        Abc_NtkVanEijkClassesOrder( vClasses );
+        pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 );
+        // simulate with classes (TO DO)
+
+        // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
+        pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 );
+        Fraig_ManFree( pFraig );
+
+        // refine the classes
+        RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses );
+        Abc_NtkDelete( pNtkMulti );
+        if ( fVerbose )
+            printf( "The number of classes after %2d iterations = %5d.  Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
+        // quit if there is no change
+        if ( RetValue == 0 )
+            break;
+    }
+    Vec_PtrFree( vCorresp );
+
+    if ( fVerbose )
+    {
+        Abc_Obj_t * pObj, * pClass;
+        int i, Counter;
+        printf( "The classes are: " );
+        Vec_PtrForEachEntry( vClasses, pClass, i )
+        {
+            Counter = 0;
+            for ( pObj = pClass; pObj; pObj = pObj->pNext )
+                Counter++;
+            printf( " %d", Counter );
+        }
+        printf( "\n" );
+    }
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the equivalence classes of nodes using the base case.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames )
+{
+    Vec_Ptr_t * vClasses;
+    int i, RetValue;
+    // derive the classes for the last frame
+    vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 );
+    // refine the classes using other timeframes
+    for ( i = 0; i < nFrames - 1; i++ )
+    {
+        if ( Vec_PtrSize(vClasses) == 0 )
+            break;
+        RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses );
+//        if ( RetValue )
+//            printf( " yes%s", (i==nFrames-2 ? "\n":"") );
+//        else
+//            printf( " no%s", (i==nFrames-2 ? "\n":"") );
+    }
+    return vClasses;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the equivalence classes of nodes.]
+
+  Description [Original network (pNtk) is mapped into the unfolded frames 
+  using given array of nodes (vCorresp). Each node in the unfolded frames 
+  is mapped into a FRAIG node (pNode->pCopy). This procedure uses next 
+  pointers (pNode->pNext) to combine the nodes into equivalence classes.
+  Each class is represented by its representative node with the minimum level.
+  Only the last frame is considered.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame )
+{
+    Abc_Obj_t * pNode, * pKey, ** ppSlot;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Ptr_t * vClasses;
+    int i;
+    // start the table hashing FRAIG nodes into classes of original network nodes
+    tTable = stmm_init_table( st_ptrcmp, st_ptrhash );
+    // create the table
+    Abc_NtkCleanNext( pNtk );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( Abc_ObjIsPo(pNode) )
+            continue;
+        pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame );
+        if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) )
+            *ppSlot = NULL;
+        pNode->pNext = *ppSlot;
+        *ppSlot = pNode;
+    }
+    // collect only non-trivial classes
+    vClasses = Vec_PtrAlloc( 100 );
+    stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode )
+        if ( pNode->pNext )
+            Vec_PtrPush( vClasses, pNode );
+    stmm_free_table( tTable );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes using one frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pHeadSame, ** ppTailSame;
+    Abc_Obj_t * pHeadDiff, ** ppTailDiff;
+    Abc_Obj_t * pNode, * pClass, * pKey;
+    int i, k, fChange = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+//        assert( pClass->pNext );
+        pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame );
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey )
+                break;
+        if ( pNode == NULL )
+            continue;
+        fChange = 1;
+        // create two classes
+        pHeadSame = NULL; ppTailSame = &pHeadSame;
+        pHeadDiff = NULL; ppTailDiff = &pHeadDiff;
+        for ( pNode = pClass; pNode; pNode = pNode->pNext )
+            if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey )
+                *ppTailDiff = pNode, ppTailDiff = &pNode->pNext;
+            else
+                *ppTailSame = pNode, ppTailSame = &pNode->pNext;
+        *ppTailSame = NULL;
+        *ppTailDiff = NULL;
+        assert( pHeadSame && pHeadDiff );
+        // put the updated class back
+        Vec_PtrWriteEntry( vClasses, i, pHeadSame );
+        // append the new class to be processed later
+        Vec_PtrPush( vClasses, pHeadDiff );
+    }
+    // remove trivial classes
+    k = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        if ( pClass->pNext )
+            Vec_PtrWriteEntry( vClasses, k++, pClass );
+    Vec_PtrShrink( vClasses, k );
+    return fChange;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders nodes in the equivalence classes.]
+
+  Description [Finds a min-level representative of each class and puts it last.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin;
+    int i;
+    // go through the classes
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        pPrevMin = NULL;
+        pNodeMin = pClass;
+        for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext )
+            if ( pNodeMin->Level >= pNode->Level )
+            {
+                pPrevMin = pPrev;
+                pNodeMin = pNode;
+            }
+        if ( pNodeMin->pNext == NULL ) // already last
+            continue;
+        // update the class
+        if ( pNodeMin == pClass )
+            Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext );
+        else
+            pPrevMin->pNext = pNodeMin->pNext;
+        // attach the min node
+        assert( pPrev->pNext == NULL );
+        pPrev->pNext = pNodeMin;
+        pNodeMin->pNext = NULL;
+    }
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        assert( pClass->pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts pairs of equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) 
+{
+    Abc_Obj_t * pClass, * pNode;
+    int i, nPairs = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            nPairs++;
+    }
+    return nPairs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sanity check for the class representation.]
+
+  Description [Checks that pNode->pNext is only used in the classes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pClass, * pObj;
+    int i;
+    Abc_NtkCleanCopy( pNtkSingle );
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        for ( pObj = pClass; pObj; pObj = pObj->pNext )
+            if ( pObj->pNext )
+                pObj->pCopy = (Abc_Obj_t *)1;
+    Abc_NtkForEachObj( pNtkSingle, pObj, i )
+        assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) );
+    Abc_NtkCleanCopy( pNtkSingle );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pRepr;
+    // skip CI and const
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    assert( Abc_ObjIsNode( pNode ) );
+    // check if the node belongs to the class
+    if ( pRepr = Abc_NodeVanEijkRepr(pNode) )
+        Abc_NtkVanEijkDfs_rec( pRepr, vNodes );
+    else
+    {
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes );
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes );
+    }
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds DFS ordering of nodes using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes );
+    return vNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the timeframes of the network.]
+
+  Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkFrames;
+    Abc_Obj_t * pLatch, * pLatchNew;
+    Vec_Ptr_t * vOrder;
+    int i;
+    assert( nFrames > 0 );
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+    // clean the array of connections
+    if ( vCorresp )
+        Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
+    // start the new network
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    if ( fShortNames )
+    {
+        pNtkFrames->pName = util_strsav(pNtk->pName);
+        pNtkFrames->pSpec = util_strsav(pNtk->pSpec);
+    }
+    else
+    {
+        sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast );
+        pNtkFrames->pName = util_strsav(Buffer);
+    }
+    // map the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkFrames->pManFunc);
+    // create new latches and remember them in the new latches
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Abc_NtkDupObj( pNtkFrames, pLatch );
+    // collect nodes in such a way each class representative goes first
+    vOrder = Abc_NtkVanEijkDfs( pNtk );
+    // create the timeframes
+    for ( i = 0; i < nFrames; i++ )
+        Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames );
+    Vec_PtrFree( vOrder );
+    // add one more timeframe without class info
+    if ( fAddLast )
+        Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames );
+    // connect the new latches to the outputs of the last frame
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pLatchNew = Abc_NtkLatch(pNtkFrames, i);
+        Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
+        Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
+        Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
+        Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
+        pLatch->pNext = NULL;
+    }
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkFrames ) )
+        printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" );
+    return pNtkFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one time frame to the new network.]
+
+  Description [If the ordering of nodes is given, uses it. Otherwise, 
+  uses the DSF order of the nodes in the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames )
+{
+    char Buffer[10];
+    Abc_Obj_t * pNode, * pLatch, * pRepr;
+    Vec_Ptr_t * vTemp;
+    int i;
+    // create the prefix to be added to the node names
+    sprintf( Buffer, "_%02d", iFrame );
+    // add the new PI nodes
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePi(pNtkFrames);       
+        if ( fShortNames )
+            Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
+        else         
+            Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer );
+    }
+    // remember the CI mapping 
+    if ( vCorresp )
+    {
+        pNode = Abc_AigConst1(pNtk->pManFunc);
+        Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        Abc_NtkForEachCi( pNtk, pNode, i )
+            Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+    }
+    // go through the nodes in the given order or in the natural order
+    if ( vOrder )
+    {
+        // add the internal nodes
+        Vec_PtrForEachEntry( vOrder, pNode, i )
+        {
+            if ( pRepr = Abc_NodeVanEijkRepr(pNode) )
+                pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase );
+            else
+                pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+            assert( Abc_ObjRegular(pNode->pCopy) != NULL );
+            if ( vCorresp )
+                Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        }
+    }
+    else
+    {
+        // add the internal nodes
+        Abc_AigForEachAnd( pNtk, pNode, i )
+        {
+            pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+            assert( Abc_ObjRegular(pNode->pCopy) != NULL );
+            if ( vCorresp )
+                Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        }
+    }
+    // add the new POs
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePo(pNtkFrames);       
+        Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
+        if ( fShortNames )
+            Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
+        else         
+            Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer );
+    }
+    // transfer the implementation of the latch drivers to the latches
+    vTemp = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pCopy = Vec_PtrEntry( vTemp, i );
+    Vec_PtrFree( vTemp );
+
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fraigs the network with or without initialization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
+{
+    Fraig_Man_t * pMan;
+    Fraig_Params_t Params;
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i;
+    assert( Abc_NtkIsStrash(pMulti) );
+    // create the FRAIG manager
+    Fraig_ParamsSetDefaultFull( &Params );
+    pMan = Fraig_ManCreate( &Params );
+    // clean the copy fields in the old network
+    Abc_NtkCleanCopy( pMulti );
+    // map the constant nodes
+    Abc_AigConst1(pMulti->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    if ( fInit )
+    {
+        // map the PI nodes
+        Abc_NtkForEachPi( pMulti, pNode, i )
+            pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
+        // map the latches
+        Abc_NtkForEachLatch( pMulti, pNode, i )
+           pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) );
+    }
+    else
+    {
+        // map the CI nodes
+        Abc_NtkForEachCi( pMulti, pNode, i )
+            pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
+    }
+    // perform fraiging
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) );
+    Abc_AigForEachAnd( pMulti, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
+                Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
+                Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pMan;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create EXDC from the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
+    Abc_Obj_t * pMiter, * pTotal;
+    Vec_Ptr_t * vCone;
+    int i, k;
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew->pName = util_strsav("exdc");
+    pNtkNew->pSpec = NULL;
+
+    // map the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+    // for each CI, create PI
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) );
+    // cannot add latches here because pLatch->pCopy pointers are used
+
+    // create the cones for each pair of nodes in an equivalence class
+    pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) );
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        // get the cone for the representative node
+        pRepr = Abc_NodeVanEijkRepr( pClass );
+        if ( Abc_ObjFaninNum(pRepr) == 2 )
+        {
+            vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pRepr );
+        }
+        // go through the node pairs (representative is last in the list)
+        for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext )
+        {
+            // get the cone for the node
+            assert( Abc_ObjFaninNum(pNode) == 2 );
+            vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pNode );
+            // complement if there is phase difference
+            pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase );
+            // add the miter
+            pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy );
+        }
+        // add the miter to the final
+        pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
+    }
+
+    // for each CO, create PO (skip POs equal to CIs because of name conflict)
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") );
+
+    // link to the POs of the network
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_ObjAddFanin( pObj->pCopy, pTotal );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, pTotal );
+
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
+
+    // check the result
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 2d5493ea..08a54e80 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -60,12 +60,12 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
         return;
     }
     if ( RetValue == 1 )
@@ -127,18 +127,18 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
         return;
     }
     if ( RetValue == 1 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
+        Abc_NtkDelete( pMiter );
         return;
     }
 
@@ -146,7 +146,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
     // analyze the result
@@ -315,7 +315,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    pMan = Abc_NtkToFraig( pFrames, &Params, 0 ); 
+    pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
     // analyze the result
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 0123e213..4466cf99 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -22,4 +22,5 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcSymm.c \
     src/base/abci/abcTiming.c \
     src/base/abci/abcUnreach.c \
+    src/base/abci/abcVanEijk.c \
     src/base/abci/abcVerify.c