Major restructuring of the code.

74 files changed, 674 insertions, 3788 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 267d4e0b..5fc9bfad 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -18,44 +18,37 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "mainInt.h"
-#include "fraig.h"
-#include "fxu.h"
-#include "cut.h"
-#include "fpga.h"
-#include "if.h"
-#include "sim.h"
-#include "res.h"
-#include "lpk.h"
-#include "giaAig.h"
-#include "dar.h"
-#include "mfs.h"
-#include "mfx.h"
-#include "fra.h"
-#include "saig.h"
-#include "nwkMerge.h"
-#include "int.h"
-#include "dch.h"
-#include "ssw.h"
-#include "cgt.h"
-#include "kit.h"
-#include "amap.h"
-#include "retInt.h"
-#include "cnf.h"
-#include "cec.h"
-#include "pdr.h" 
-
-#include "tim.h"
-#include "llb.h"
-#include "ntlnwk.h"
-#include "mfx.h"
-#include "bbr.h"
-#include "cov.h"
-
-#include "cmd.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/base/main/mainInt.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/opt/fxu/fxu.h"
+#include "src/opt/cut/cut.h"
+#include "src/map/fpga/fpga.h"
+#include "src/map/if/if.h"
+#include "src/opt/sim/sim.h"
+#include "src/opt/res/res.h"
+#include "src/opt/lpk/lpk.h"
+#include "src/aig/gia/giaAig.h"
+#include "src/opt/dar/dar.h"
+#include "src/opt/mfs/mfs.h"
+#include "src/proof/fra/fra.h"
+#include "src/aig/saig/saig.h"
+#include "src/proof/int/int.h"
+#include "src/proof/dch/dch.h"
+#include "src/proof/ssw/ssw.h"
+#include "src/opt/cgt/cgt.h"
+#include "src/bool/kit/kit.h"
+#include "src/map/amap/amap.h"
+#include "src/opt/ret/retInt.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/proof/cec/cec.h"
+#include "src/proof/pdr/pdr.h"
+#include "src/misc/tim/tim.h"
+#include "src/proof/llb/llb.h"
+#include "src/proof/bbr/bbr.h"
+#include "src/map/cov/cov.h"
+#include "src/base/cmd/cmd.h"
 
 #ifdef _WIN32
 //#include <io.h>
@@ -112,7 +105,7 @@ static int Abc_CommandMfs                    ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandRewrite                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRefactor               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -287,44 +280,6 @@ static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandTraceStart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-
-static int Abc_CommandAbc8Read               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8ReadLogic          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Write              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8WriteLogic         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8ReadLut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8PrintLut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Check              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandAbc8Ps                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Pfan               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8If                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8DChoice            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Dch                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Dc2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Bidec              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Strash             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Lutpack            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Lutmin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Balance            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Speedup            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Merge              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Insert             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8ClpLut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandAbc8Fraig              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Scl                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Lcorr              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Ssw                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Scorr              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Sweep              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8Zero               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandAbc8Cec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc8DSec               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-
 static int Abc_CommandAbc9Get                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Put                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Read               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -466,24 +421,6 @@ void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
 ***********************************************************************/
 void Abc_FrameClearDesign()
 {
-    Abc_Frame_t * pAbc;
-
-    pAbc = Abc_FrameGetGlobalFrame();
-    if ( pAbc->pAbc8Ntl )
-    {
-        Ntl_ManFree( pAbc->pAbc8Ntl );
-        pAbc->pAbc8Ntl = NULL;
-    }
-    if ( pAbc->pAbc8Aig )
-    {
-        Aig_ManStop( pAbc->pAbc8Aig );
-        pAbc->pAbc8Aig = NULL;
-    }
-    if ( pAbc->pAbc8Nwk )
-    {
-        Nwk_ManFree( pAbc->pAbc8Nwk );
-        pAbc->pAbc8Nwk = NULL;
-    }
 }
 
 /**Function*************************************************************
@@ -536,18 +473,6 @@ void Abc_CommandUpdate9( Abc_Frame_t * pAbc, Gia_Man_t * pNew )
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
-/*
-    char * pBuff = ABC_ALLOC( char, (1<<29) );
-    int i, clk = clock();
-    for ( i = 0; i < (1<<29); i++ )
-        pBuff[i] = i % 53;
-    if ( pBuff == NULL )
-        printf( "Not allocated. " );
-    else
-        printf( "Allocated %d bytes. ", (1<<29) );
-    Abc_PrintTime( 1, "Time", clock() - clk );
-*/
-
     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 );
@@ -591,7 +516,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
+//    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
 
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
@@ -762,42 +687,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "reconcile",     Abc_CommandReconcile,        1 );
     Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
 
-
-    Cmd_CommandAdd( pAbc, "ABC8",         "*r",            Abc_CommandAbc8Read,         0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*rlogic",       Abc_CommandAbc8ReadLogic,    0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*w",            Abc_CommandAbc8Write,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*wlogic",       Abc_CommandAbc8WriteLogic,   0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*rlut",         Abc_CommandAbc8ReadLut,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*plut",         Abc_CommandAbc8PrintLut,     0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*check",        Abc_CommandAbc8Check,        0 );
-
-    Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*pfan",         Abc_CommandAbc8Pfan,         0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*dch",          Abc_CommandAbc8Dch,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*dc2",          Abc_CommandAbc8Dc2,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*bidec",        Abc_CommandAbc8Bidec,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*st",           Abc_CommandAbc8Strash,       0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*mfs",          Abc_CommandAbc8Mfs,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*lp",           Abc_CommandAbc8Lutpack,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*b",            Abc_CommandAbc8Balance,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*speedup",      Abc_CommandAbc8Speedup,      0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*merge",        Abc_CommandAbc8Merge,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*insert",       Abc_CommandAbc8Insert,       0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*clplut",       Abc_CommandAbc8ClpLut,       0 );
-
-    Cmd_CommandAdd( pAbc, "ABC8",         "*fraig",        Abc_CommandAbc8Fraig,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*scorr",        Abc_CommandAbc8Scorr,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*zero",         Abc_CommandAbc8Zero,         0 );
-
-    Cmd_CommandAdd( pAbc, "ABC8",         "*cec",          Abc_CommandAbc8Cec,          0 );
-    Cmd_CommandAdd( pAbc, "ABC8",         "*dsec",         Abc_CommandAbc8DSec,         0 );
-
     Cmd_CommandAdd( pAbc, "ABC9",         "&get",          Abc_CommandAbc9Get,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&put",          Abc_CommandAbc9Put,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&r",            Abc_CommandAbc9Read,         0 );
@@ -956,11 +845,6 @@ void Abc_End( Abc_Frame_t * pAbc )
 //        extern void Au_TabManPrint();
 //        Au_TabManPrint();
     }
-    {
-        extern void If_LutLibFree( If_Lib_t * pLutLib );
-        if ( Abc_FrameGetGlobalFrame()->pAbc8Lib )
-            If_LutLibFree( (If_Lib_t *)Abc_FrameGetGlobalFrame()->pAbc8Lib );
-    }
 
 //    Dar_LibDumpPriorities();
     {
@@ -4570,6 +4454,7 @@ usage:
     return 1;
 } 
 
+#if 0
 /**Function*************************************************************
 
   Synopsis    []
@@ -4702,7 +4587,7 @@ usage:
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
-
+#endif
 /**Function*************************************************************
 
   Synopsis    []
@@ -21305,3075 +21190,6 @@ usage:
 }
 
 
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pFile;
-    char * pFileName;
-    int c;
-    int fMapped;
-    int fTest;
-
-    // set defaults
-    fMapped = 0;
-    fTest   = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'm':
-            fMapped ^= 1;
-            break;
-        case 't':
-            fTest ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( pFileName, "r" )) == NULL )
-    {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
-        Abc_Print( 1, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-    if ( fTest )
-    {
-        Ntl_Man_t * pTemp = Ntl_ManReadBlif( pFileName, 1 );
-        if ( pTemp )
-        {
-//            Ntl_ManWriteBlif( pTemp, "test_boxes.blif" );
-            Ntl_ManPrintStats( pTemp );
-            Ntl_ManFree( pTemp );
-        }
-        return 0; 
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = Ntl_ManReadBlif( pFileName, 1 );
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Read(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Read(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    if ( fMapped )
-    {
-        pAbc->pAbc8Nwk = Ntl_ManExtractNwk( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, NULL );
-        if ( pAbc->pAbc8Nwk == NULL )
-            Abc_Print( -1, "Abc_CommandAbc8Read(): Warning! Mapped network is not extracted.\n" );
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *r [-mth]\n" );
-    Abc_Print( -2, "\t        reads the design with whiteboxes\n" );
-    Abc_Print( -2, "\t-m    : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
-    Abc_Print( -2, "\t-t    : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8ReadLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pFile;
-    char * pFileName;
-    Nwk_Man_t * pNtkNew;
-    int c;
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    // get the input file name
-    pFileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( pFileName, "r" )) == NULL )
-    {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
-        if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".blif", NULL, NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
-        Abc_Print( 1, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-
-    if ( pAbc->pAbc8Ntl == NULL || pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8ReadLogic(): There is no design or its AIG.\n" );
-        return 1;
-    }
-
-    // read the new logic
-    pNtkNew = Ntl_ManReadNwk( pFileName, pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl) );
-    if ( pNtkNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8ReadLogic(): Procedure has failed.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Nwk != NULL )
-        Nwk_ManFree( pAbc->pAbc8Nwk );
-    pAbc->pAbc8Nwk = pNtkNew;    
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *rlogic [-h]\n" );
-    Abc_Print( -2, "\t        reads the logic part of the design without whiteboxes\n" );
-    Abc_Print( -2, "\t        and sets the new logic as the current mapped network\n" );
-    Abc_Print( -2, "\t        (the logic part should be comb and with the same PIs/POs)\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    char * pFileName;
-    Aig_Man_t * pTemp;
-    Ntl_Man_t * pTemp2;
-    int fAig;
-    int fBlif;
-    int fCollapsed;
-    int c;
-
-    // set defaults
-    fAig = 0;
-    fBlif = 1;
-    fCollapsed = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "abch" ) ) != EOF )
-    { 
-        switch ( c )
-        {
-        case 'a':
-            fAig ^= 1;
-            break;
-        case 'b':
-            fBlif ^= 1;
-            break;
-        case 'c':
-            fCollapsed ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Write(): There is no design to write.\n" );
-        return 1;
-    } 
-    // create the design to write
-    pFileName = argv[globalUtilOptind];
-    if ( fAig )
-    {
-        if ( fCollapsed )
-        {
-            pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0, 0 );
-            if ( fBlif )
-                Saig_ManDumpBlif( pTemp, pFileName );
-            else
-                Ioa_WriteAiger( pTemp, pFileName, 0, 0 );
-            Aig_ManStop( pTemp );
-        }
-        else
-        {
-            if ( pAbc->pAbc8Aig != NULL )
-            {
-                if ( fBlif )
-                {
-                    pTemp2 = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
-                    if ( pTemp2 == NULL )
-                    {
-                        Abc_Print( -1, "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
-                        return 1;
-                    }
-                    Ntl_ManWriteBlif( pTemp2, pFileName );
-                    Ntl_ManFree( pTemp2 );
-                }
-                else
-                    Ioa_WriteAiger( pAbc->pAbc8Aig, pFileName, 0, 0 );
-            }
-            else
-            {
-                Abc_Print( -1, "There is no AIG to write.\n" );
-                return 1;
-            }
-        }
-    }
-    else 
-    {
-        if ( pAbc->pAbc8Nwk != NULL ) 
-        {
-            pTemp2 = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-            if ( pTemp2 == NULL )
-            {
-                Abc_Print( -1, "Abc_CommandAbc8Write():  Inserting mapped network has failed.\n" );
-                return 1;
-            }
-            Ntl_ManWriteBlif( pTemp2, pFileName );
-            Ntl_ManFree( pTemp2 );
-        }
-        else
-        {
-            Abc_Print( -1, "Writing the unmapped netlist.\n" );
-            pTemp2 = pAbc->pAbc8Ntl;
-            Ntl_ManWriteBlif( pTemp2, pFileName );
-        }
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *w [-abch]\n" );
-    Abc_Print( -2, "\t        write the design with whiteboxes\n" );
-    Abc_Print( -2, "\t-a    : toggle writing design or internal AIG [default = %s]\n", fAig? "AIG": "design" );
-    Abc_Print( -2, "\t-b    : toggle writing AIG as BLIF or AIGER [default = %s]\n", fBlif? "BLIF": "AIGER" );
-    Abc_Print( -2, "\t-c    : toggle writing collapsed sequential AIG [default = %s]\n", fCollapsed? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Vec_Ptr_t * vCiNames = NULL, * vCoNames = NULL;
-    char * pFileName;
-    int fAig;
-    int c;
-
-    // set defaults
-    fAig = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'a':
-            fAig ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Write(): There is no design to write.\n" );
-        return 1;
-    }
-    // create the design to write
-    pFileName = argv[globalUtilOptind];
-//    vCiNames = Ntl_ManCollectCiNames( pAbc->pAbc8Ntl );
-//    vCoNames = Ntl_ManCollectCoNames( pAbc->pAbc8Ntl );
-    // the problem is duplicated CO names...
-    if ( fAig )
-    {
-        if ( pAbc->pAbc8Aig != NULL )
-            Aig_ManDumpBlif( pAbc->pAbc8Aig, pFileName, vCiNames, vCoNames );
-        else
-        {
-            Abc_Print( -1, "There is no AIG to write.\n" );
-            return 1;
-        }
-    }
-    else 
-    {
-        if ( pAbc->pAbc8Nwk != NULL ) 
-            Nwk_ManDumpBlif( pAbc->pAbc8Nwk, pFileName, vCiNames, vCoNames );
-        else
-        {
-            Abc_Print( -1, "There is no mapped network to write.\n" );
-            return 1;
-        }
-    }
-    if ( vCiNames )  Vec_PtrFree( vCiNames );
-    if ( vCoNames )  Vec_PtrFree( vCoNames );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *wlogic [-ah]\n" );
-    Abc_Print( -2, "\t        write the logic part of the design without whiteboxes\n" );
-    Abc_Print( -2, "\t-a    : toggle writing mapped network or AIG [default = %s]\n", fAig? "AIG": "network" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Command procedure to read LUT libraries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8ReadLut( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    FILE * pFile;
-    char * FileName;
-    If_Lib_t * pLib;
-    int c;
-    extern If_Lib_t * If_LutLibRead( char * FileName );
-    extern void If_LutLibFree( If_Lib_t * pLutLib );
-
-    // set the defaults
-    Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
-    {
-        switch (c) 
-        {
-            case 'h':
-                goto usage;
-                break;
-            default:
-                goto usage;
-        }
-    }
-
-
-    if ( argc != globalUtilOptind + 1 )
-    {
-        goto usage;
-    }
-
-    // get the input file name
-    FileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
-    {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
-        if ( (FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
-        Abc_Print( 1, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-
-    // set the new network
-    pLib = If_LutLibRead( FileName );
-    if ( pLib == NULL )
-    {
-        Abc_Print( -1, "Reading LUT library has failed.\n" );
-        goto usage;
-    }
-    // replace the current library
-    if ( pAbc->pAbc8Lib != NULL )
-        If_LutLibFree( pAbc->pAbc8Lib );
-    pAbc->pAbc8Lib = pLib;
-    return 0;
-
-usage:
-    Abc_Print( -2, "\nusage: *rlut [-h]\n");
-    Abc_Print( -2, "\t          read the LUT library from the file\n" );  
-    Abc_Print( -2, "\t-h      : print the command usage\n");
-    Abc_Print( -2, "\t                                        \n");
-    Abc_Print( -2, "\t          File format for a LUT library:\n");
-    Abc_Print( -2, "\t          (the default library is shown)\n");
-    Abc_Print( -2, "\t                                        \n");
-    Abc_Print( -2, "\t          # The area/delay of k-variable LUTs:\n");
-    Abc_Print( -2, "\t          # k  area   delay\n");
-    Abc_Print( -2, "\t          1      1      1\n");
-    Abc_Print( -2, "\t          2      2      2\n");
-    Abc_Print( -2, "\t          3      4      3\n");
-    Abc_Print( -2, "\t          4      8      4\n");
-    Abc_Print( -2, "\t          5     16      5\n");
-    Abc_Print( -2, "\t          6     32      6\n");
-    return 1;       /* error exit */
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Command procedure to read LUT libraries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8PrintLut( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    int c;
-    extern void If_LutLibPrint( If_Lib_t * pLutLib );
-
-    // set the defaults
-    Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
-    {
-        switch (c) 
-        {
-            case 'h':
-                goto usage;
-                break;
-            default:
-                goto usage;
-        }
-    }
-
-    if ( argc != globalUtilOptind )
-    {
-        goto usage;
-    }
-
-    // set the new network
-    if ( pAbc->pAbc8Lib == NULL )
-        Abc_Print( -1, "Abc_CommandAbc8PrintLut(): LUT library is not specified.\n" );
-    else
-        If_LutLibPrint( (If_Lib_t *)pAbc->pAbc8Lib );
-    return 0;
-
-usage:
-    Abc_Print( -2, "\nusage: *plut [-h]\n");
-    Abc_Print( -2, "\t          print the current LUT library\n" );  
-    Abc_Print( -2, "\t-h      : print the command usage\n");
-    return 1;       /* error exit */
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Command procedure to read LUT libraries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Check( Abc_Frame_t * pAbc, int argc, char **argv )
-{
-    int c;
-
-    // set the defaults
-    Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "h")) != EOF ) 
-    {
-        switch (c) 
-        {
-            case 'h':
-                goto usage;
-                break;
-            default:
-                goto usage;
-        }
-    }
-
-    if ( argc != globalUtilOptind )
-    {
-        goto usage;
-    }
-
-    // set the new network
-    if ( pAbc->pAbc8Nwk == NULL )
-        Abc_Print( -1, "Abc_CommandAbc8Check(): There is no mapped network.\n" );
-    else
-        Nwk_ManCheck( pAbc->pAbc8Nwk );
-    return 0;
-
-usage:
-    Abc_Print( -2, "\nusage: *check [-h]\n");
-    Abc_Print( -2, "\t          checks if the current mapped network has duplicated fanins\n" );  
-    Abc_Print( -2, "\t-h      : print the command usage\n");
-    return 1;       /* error exit */
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    int c;
-    int fSaveBest;
-    int fDumpResult;
-    int fPower;
-    int fShort;
-    extern If_Lib_t *  If_SetSimpleLutLib( int nLutSize );
-
-    // set defaults
-    fSaveBest = 0;
-    fDumpResult = 0;
-    fPower = 0;
-    fShort = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "bdpsh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'b':
-            fSaveBest ^= 1;
-            break;
-        case 'd':
-            fDumpResult ^= 1;
-            break;
-        case 'p':
-            fPower ^= 1;
-            break;
-        case 's':
-            fShort ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ps(): There is no design to show.\n" );
-        return 1;
-    }
-
-    if ( fShort )
-    {
-        Nwk_ManPrintStatsShort( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk );
-        return 0;
-    }
-    // get the input file name
-    if ( pAbc->pAbc8Ntl )
-    {
-        Abc_Print( -1, "NETLIST: " );
-        Ntl_ManPrintStats( pAbc->pAbc8Ntl );
-    }
-    if ( pAbc->pAbc8Aig )
-    {
-        Abc_Print( -1, "AIG:     " );
-        Aig_ManPrintStats( pAbc->pAbc8Aig );
-    }
-    if ( pAbc->pAbc8Nwk )
-    {
-        if ( pAbc->pAbc8Lib == NULL )
-        {
-            Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
-            pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
-        }
-        Abc_Print( -1, "MAPPED:  " );
-        Nwk_ManPrintStats( pAbc->pAbc8Nwk, pAbc->pAbc8Lib, fSaveBest, fDumpResult, fPower, pAbc->pAbc8Ntl );
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *ps [-bdpsh]\n" );
-    Abc_Print( -2, "\t        prints design statistics\n" );
-    Abc_Print( -2, "\t-b    : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
-    Abc_Print( -2, "\t-d    : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
-    Abc_Print( -2, "\t-p    : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" );
-    Abc_Print( -2, "\t-s    : toggles short printing mode [default = %s]\n", fShort? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Pfan( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    int c;
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Pfan(): There is no mapped network for print fanin/fanout.\n" );
-        return 1;
-    }
-    Nwk_ManPrintFanioNew( pAbc->pAbc8Nwk );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *pfan [-h]\n" );
-    Abc_Print( -2, "\t        prints fanin/fanout stats of the mapped network\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    char Buffer[200];
-    char LutSize[200];
-    If_Par_t Pars, * pPars = &Pars;
-    Nwk_Man_t * pNtkNew;
-    int c;
-
-    if ( pAbc->pAbc8Lib == NULL )
-    {
-//        Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
-        pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
-    }
-
-    // set defaults
-    Nwk_ManSetIfParsDefault( pPars );
-    pPars->pLutLib = pAbc->pAbc8Lib;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'K':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->nLutSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nLutSize < 0 ) 
-                goto usage;
-            // if the LUT size is specified, disable library
-            pPars->pLutLib = NULL; 
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->nCutsMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nCutsMax < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->nFlowIters = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFlowIters < 0 ) 
-                goto usage;
-            break;
-        case 'A':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-A\" should be followed by a positive integer.\n" );
-                goto usage;
-            }
-            pPars->nAreaIters = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nAreaIters < 0 ) 
-                goto usage;
-            break;
-        case 'D':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by a floating point number.\n" );
-                goto usage;
-            }
-            pPars->DelayTarget = (float)atof(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->DelayTarget <= 0.0 ) 
-                goto usage;
-            break;
-        case 'E':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-E\" should be followed by a floating point number.\n" );
-                goto usage;
-            }
-            pPars->Epsilon = (float)atof(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 ) 
-                goto usage;
-            break;
-        case 'q':
-            pPars->fPreprocess ^= 1;
-            break;
-        case 'a':
-            pPars->fArea ^= 1;
-            break;
-        case 'r':
-            pPars->fExpRed ^= 1;
-            break;
-        case 'f':
-            pPars->fFancy ^= 1;
-            break;
-        case 'l':
-            pPars->fLatchPaths ^= 1;
-            break;
-        case 'e':
-            pPars->fEdge ^= 1;
-            break;
-        case 'p':
-            pPars->fPower ^= 1;
-            break;
-        case 'm':
-            pPars->fCutMin ^= 1;
-            break;
-        case 's':
-            pPars->fSeqMap ^= 1;
-            break;
-        case 'd':
-            pPars->fBidec ^= 1;
-            break;
-        case 'b':
-            pPars->fUseBat ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8If(): There is no AIG to map.\n" );
-        return 1;
-    }
-
-    if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
-    {
-        Abc_Print( -1, "Incorrect LUT size (%d).\n", pPars->nLutSize );
-        return 1;
-    }
-
-    if ( pPars->nCutsMax < 1 || pPars->nCutsMax >= (1<<12) )
-    {
-        Abc_Print( -1, "Incorrect number of cuts.\n" );
-        return 1;
-    }
-
-    // enable truth table computation if choices are selected
-    if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) )
-    {
-//        Abc_Print( 0, "Performing LUT mapping with %d choices.\n", c );
-        pPars->fExpRed = 0;
-    }
-
-    if ( pPars->fUseBat )
-    {
-        if ( pPars->nLutSize < 4 || pPars->nLutSize > 6 )
-        {
-            Abc_Print( -1, "This feature only works for {4,5,6}-LUTs.\n" );
-            return 1;
-        }
-        pPars->fCutMin = 1;            
-    }
-
-    // enable truth table computation if cut minimization is selected
-    if ( pPars->fCutMin )
-    {
-        pPars->fTruth = 1;
-        pPars->fExpRed = 0;
-    }
-
-    // complain if truth tables are requested but the cut size is too large
-    if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
-    {
-        Abc_Print( -1, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
-        return 1;
-    }
-
-    pNtkNew = Nwk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
-    if ( pNtkNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8If(): Mapping of the AIG has failed.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Nwk != NULL )
-        Nwk_ManFree( pAbc->pAbc8Nwk );
-    pAbc->pAbc8Nwk = pNtkNew;
-    return 0;
-
-usage:
-    if ( pPars->DelayTarget == -1 ) 
-        sprintf( Buffer, "best possible" );
-    else
-        sprintf( Buffer, "%.2f", pPars->DelayTarget );
-    if ( pPars->nLutSize == -1 ) 
-        sprintf( LutSize, "library" );
-    else
-        sprintf( LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: *if [-KCFA num] [-DE float] [-qarlepmdbvh]\n" );
-    Abc_Print( -2, "\t           performs FPGA technology mapping of the network\n" );
-    Abc_Print( -2, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
-    Abc_Print( -2, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
-    Abc_Print( -2, "\t-F num   : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
-    Abc_Print( -2, "\t-A num   : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
-    Abc_Print( -2, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
-    Abc_Print( -2, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );  
-    Abc_Print( -2, "\t-q       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
-    Abc_Print( -2, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
-//    Abc_Print( -2, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
-    Abc_Print( -2, "\t-r       : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
-    Abc_Print( -2, "\t-l       : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
-    Abc_Print( -2, "\t-e       : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
-    Abc_Print( -2, "\t-p       : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
-    Abc_Print( -2, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
-//    Abc_Print( -2, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
-    Abc_Print( -2, "\t-d       : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
-    Abc_Print( -2, "\t-b       : toggles the use of one special feature [default = %s]\n", pPars->fUseBat? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : prints the command usage\n");
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAigNew;
-    int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
-    int nConfMax, nLevelMax;
-    extern Aig_Man_t * Ntl_ManPerformChoicing( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
-
-    // set defaults
-    fBalance     = 1;
-    fUpdateLevel = 1;
-    fConstruct   = 0;
-    nConfMax     = 1000;
-    nLevelMax    = 0;
-    fVerbose     = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfMax < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nLevelMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nLevelMax < 0 ) 
-                goto usage;
-            break;
-        case 'b':
-            fBalance ^= 1;
-            break;
-        case 'l':
-            fUpdateLevel ^= 1;
-            break;
-        case 'c':
-            fConstruct ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8DChoice(): There is no AIG to synthesize.\n" );
-        return 1;
-    }
-
-    // get the input file name
-    pAigNew = Ntl_ManPerformChoicing( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8DChoice(): Tranformation has failed.\n" );
-        return 1;
-    }
-    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *dchoice [-C num] [-L num] [-blcvh]\n" );
-    Abc_Print( -2, "\t         performs AIG-based synthesis and derives choices\n" );
-    Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
-    Abc_Print( -2, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
-    Abc_Print( -2, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
-    Abc_Print( -2, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
-    Abc_Print( -2, "\t-c     : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Dch_Pars_t Pars, * pPars = &Pars;
-    Aig_Man_t * pAigNew;
-    int c;
-    extern Aig_Man_t * Ntl_ManPerformChoicingNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-
-    // set defaults
-    Dch_ManSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'W':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nWords = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nWords < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBTLimit < 0 ) 
-                goto usage;
-            break;
-        case 'S':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nSatVarMax < 0 ) 
-                goto usage;
-            break;
-        case 's':
-            pPars->fSynthesis ^= 1;
-            break;
-        case 'p':
-            pPars->fPower ^= 1;
-            break;
-        case 't':
-            pPars->fSimulateTfo ^= 1;
-            break;
-        case 'f':
-            pPars->fLightSynth ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Dch(): There is no AIG to synthesize.\n" );
-        return 1;
-    }
-
-    // get the input file name
-    pAigNew = Ntl_ManPerformChoicingNew( pAbc->pAbc8Aig, pPars );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Dch(): Tranformation has failed.\n" );
-        return 1;
-    }
-//    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *dch [-WCS num] [-sptfvh]\n" );
-    Abc_Print( -2, "\t         computes structural choices using a new approach\n" );
-    Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
-    Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
-    Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
-    Abc_Print( -2, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
-    Abc_Print( -2, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
-    Abc_Print( -2, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Dc2( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAigNew;
-    int c;
-    int fBalance;
-    int fUpdateLevel;
-    int fVerbose;
-    int fPower;
-
-    extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
-
-    // set defaults
-    fBalance     = 1;
-    fUpdateLevel = 1;
-    fPower       = 0;
-    fVerbose     = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "blpvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'b':
-            fBalance ^= 1;
-            break;
-        case 'l':
-            fUpdateLevel ^= 1;
-            break;
-        case 'p':
-            fPower ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Dc2(): There is no AIG to synthesize.\n" );
-        return 1;
-    }
-
-    // get the input file name
-    pAigNew = Dar_ManCompress2( pAbc->pAbc8Aig, fBalance, fUpdateLevel, 1, fPower, fVerbose );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Dc2(): Tranformation has failed.\n" );
-        return 1;
-    }
-    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *dc2 [-blpvh]\n" );
-    Abc_Print( -2, "\t        performs AIG-based synthesis without deriving choices\n" );
-    Abc_Print( -2, "\t-b    : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
-    Abc_Print( -2, "\t-l    : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
-    Abc_Print( -2, "\t-p    : toggle power-aware rewriting [default = %s]\n", fPower? "yes": "no" );
-    Abc_Print( -2, "\t-v    : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Bidec( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    int c;
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Bidec(): There is no mapped network to strash.\n" );
-        return 1;
-    }
-    Nwk_ManBidecResyn( pAbc->pAbc8Nwk, 0 );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *bidec [-h]\n" );
-    Abc_Print( -2, "\t        performs bi-decomposition of local functions\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAigNew;
-    int c;
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Strash(): There is no mapped network to strash.\n" );
-        return 1;
-    } 
-
-    pAigNew = Nwk_ManStrash( pAbc->pAbc8Nwk );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Strash(): Tranformation has failed.\n" );
-        return 1;
-    }
-    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *st [-h]\n" );
-    Abc_Print( -2, "\t        performs structural hashing of mapped network\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Mfx_Par_t Pars, * pPars = &Pars;
-    int c;
-//    extern int Mfx_Perform( void * pNtk, Mfx_Par_t * pPars, If_Lib_t * pLutLib );
-
-    // set defaults
-    Mfx_ParsDefault( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraespvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'W':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nWinTfoLevs < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFanoutsMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFanoutsMax < 1 ) 
-                goto usage;
-            break;
-        case 'D':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nDepthMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nDepthMax < 0 ) 
-                goto usage;
-            break;
-        case 'M':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nWinSizeMax < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nGrowthLevel = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBTLimit < 0 ) 
-                goto usage;
-            break;
-        case 'r':
-            pPars->fResub ^= 1;
-            break;
-        case 'a':
-            pPars->fArea ^= 1;
-            break;
-        case 'e':
-            pPars->fMoreEffort ^= 1;
-            break;
-        case 's':
-            pPars->fSwapEdge ^= 1;
-            break;
-        case 'p':
-            pPars->fPower ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Mfs(): There is no mapped network.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Lib == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Mfs(): There is no LUT library.\n" );
-        return 1;
-    }
-    if ( If_LutLibDelaysAreDifferent(pAbc->pAbc8Lib) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Mfs(): Cannot perform don't-care simplication with variable-pin-delay LUT model.\n" );
-        Abc_Print( -1, "The delay model should be fixed-pin-delay, for example, the delay of all pins of all LUTs is 0.4.\n" );
-        return 1;
-    }
-
-
-    // modify the current network
-    if ( !Mfx_Perform( pAbc->pAbc8Nwk, pPars, pAbc->pAbc8Lib ) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Mfs(): Command has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *mfs [-WFDMLC num] [-raespvh]\n" );
-    Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
-    Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
-    Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
-    Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
-    Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
-    Abc_Print( -2, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-    Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
-    Abc_Print( -2, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
-    Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
-    Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
-    Abc_Print( -2, "\t-s       : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
-    Abc_Print( -2, "\t-p       : toggle power-aware optimization [default = %s]\n", pPars->fPower? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Lutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    int c;
-
-    Abc_Print( -1, "This command is temporarily disabled.\n" );
-    return 0;
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lutpack(): There is no mapped network to strash.\n" );
-        return 1;
-    }
-
-    
-    return 0;
-usage:
-/*
-    Abc_Print( -2, "usage: *lp [-h]\n" );
-    Abc_Print( -2, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" );
-    Abc_Print( -2, "\t           performs \"rewriting\" for LUT network;\n" );
-    Abc_Print( -2, "\t           determines LUT size as the max fanin count of a node;\n" );
-    Abc_Print( -2, "\t           if the network is not LUT-mapped, packs it into 6-LUTs\n" );
-    Abc_Print( -2, "\t           (there is another command for resynthesis after LUT mapping, \"imfs\")\n" );
-    Abc_Print( -2, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
-    Abc_Print( -2, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
-    Abc_Print( -2, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
-    Abc_Print( -2, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
-    Abc_Print( -2, "\t-s       : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
-    Abc_Print( -2, "\t-z       : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
-    Abc_Print( -2, "\t-f       : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
-    Abc_Print( -2, "\t-o       : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w       : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : print the command usage\n");
-*/
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAigNew;
-    int c;
-    int fExor;
-    int fUpdateLevel;
-    int fVerbose;
-    extern Aig_Man_t *  Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
-
-    // set defaults
-    fExor        = 0;
-    fUpdateLevel = 1;
-    fVerbose     = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "xlh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'x':
-            fExor ^= 1;
-            break;
-        case 'l':
-            fUpdateLevel ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Balance(): There is no AIG to synthesize.\n" );
-        return 1;
-    }
-
-    // get the input file name
-    pAigNew = Dar_ManBalanceXor( pAbc->pAbc8Aig, fExor, fUpdateLevel, fVerbose );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Balance(): Tranformation has failed.\n" );
-        return 1;
-    }
-    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *b [-xlvh]\n" );
-    Abc_Print( -2, "\t        performs balancing of the AIG\n" );
-    Abc_Print( -2, "\t-x    : toggle using XOR-balancing [default = %s]\n", fExor? "yes": "no" );
-    Abc_Print( -2, "\t-l    : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
-    Abc_Print( -2, "\t-v    : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAigNew;
-    int c;
-    int fUseLutLib = 0;
-    int Percentage = 100;
-    int Degree = 5;
-    int fVerbose = 0;
-    int fVeryVerbose = 0;
-
-    // set defaults
-    fUseLutLib = 0;
-    Percentage = 5;
-    Degree     = 2;
-    fVerbose   = 0;
-    fVeryVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PNlvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            Percentage = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( Percentage < 1 || Percentage > 100 ) 
-                goto usage;
-            break;
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            Degree = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( Degree < 1 || Degree > 5 ) 
-                goto usage;
-            break;
-        case 'l':
-            fUseLutLib ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'w':
-            fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Speedup(): There is no mapped network to strash.\n" );
-        return 1;
-    }
-       
-    pAigNew = Nwk_ManSpeedup( pAbc->pAbc8Nwk, fUseLutLib, Percentage, Degree, fVerbose, fVeryVerbose );
-    if ( pAigNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Speedup(): Tranformation has failed.\n" );
-        return 1;
-    }
-    Aig_ManStop( pAbc->pAbc8Aig );
-    pAbc->pAbc8Aig = pAigNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *speedup [-P num] [-N num] [-lvwh]\n" );
-    Abc_Print( -2, "\t           transforms LUT-mapped network into an AIG with choices;\n" );
-    Abc_Print( -2, "\t           the choices are added to speedup the next round of mapping\n" );
-    Abc_Print( -2, "\t-P <num> : delay delta defining critical path for library model [default = %d%%]\n", Percentage );
-    Abc_Print( -2, "\t-N <num> : the max critical path degree for resynthesis (0 < num < 6) [default = %d]\n", Degree );
-    Abc_Print( -2, "\t-l       : toggle using unit- or LUT-library-delay model [default = %s]\n", fUseLutLib? "lib" : "unit" );
-    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Merge( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Nwk_LMPars_t Pars, * pPars = &Pars;
-    Vec_Int_t * vResult;
-    int c;
-
-    // set defaults
-    memset( pPars, 0, sizeof(Nwk_LMPars_t) );
-    pPars->nMaxLutSize    = 5;   // the max LUT size for merging (N=5)
-    pPars->nMaxSuppSize   = 5;   // the max total support size after merging (S=5)
-    pPars->nMaxDistance   = 3;   // the max number of nodes separating LUTs
-    pPars->nMaxLevelDiff  = 2;   // the max difference in levels
-    pPars->nMaxFanout     = 100; // the max number of fanouts to traverse
-    pPars->fUseDiffSupp   = 0;   // enables the use of nodes with different support
-    pPars->fUseTfiTfo     = 0;   // enables the use of TFO/TFO nodes as candidates
-    pPars->fVeryVerbose   = 0;   // enables additional verbose output
-    pPars->fVerbose       = 1;   // enables verbose output
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFscvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxLutSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxLutSize < 2 ) 
-                goto usage;
-            break;
-        case 'S':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxSuppSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxSuppSize < 2 ) 
-                goto usage;
-            break;
-        case 'D':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxDistance = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxDistance < 2 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxLevelDiff = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxLevelDiff < 2 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxFanout = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxFanout < 2 ) 
-                goto usage;
-            break;
-        case 's':
-            pPars->fUseDiffSupp ^= 1;
-            break;
-        case 'c':
-            pPars->fUseTfiTfo ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Speedup(): There is no mapped network to merge LUTs.\n" );
-        return 1;
-    }
-       
-    vResult = Nwk_ManLutMerge( pAbc->pAbc8Nwk, pPars );
-    Vec_IntFree( vResult );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *merge [-NSDLF num] [-scwvh]\n" );
-    Abc_Print( -2, "\t           creates pairs of topologically-related LUTs\n" );
-    Abc_Print( -2, "\t-N <num> : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize );
-    Abc_Print( -2, "\t-S <num> : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize );
-    Abc_Print( -2, "\t-D <num> : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance );
-    Abc_Print( -2, "\t-L <num> : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff );
-    Abc_Print( -2, "\t-F <num> : the max number of fanouts to stop traversal (0 < num) [default = %d]\n", pPars->nMaxFanout );
-    Abc_Print( -2, "\t-s       : toggle the use of nodes without support overlap [default = %s]\n", pPars->fUseDiffSupp? "yes" : "no" );
-    Abc_Print( -2, "\t-c       : toggle the use of TFI/TFO nodes as candidates [default = %s]\n", pPars->fUseTfiTfo? "yes" : "no" );
-    Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h       : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Insert( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew;
-    int c;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Insert(): There is no design.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Nwk == NULL ) 
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Insert(): There is no network to insert.\n" );
-        return 1;
-    }
-    pNtlNew = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *insert [-h]\n" );
-    Abc_Print( -2, "\t         inserts the mapped network into the netlist\n" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8ClpLut( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew;
-    int c;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Insert(): There is no design.\n" );
-        return 1;
-    }
-    pNtlNew = Ntl_ManDupCollapseLuts( pAbc->pAbc8Ntl );
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *clplut [-h]\n" );
-    Abc_Print( -2, "\t         collapses comb white boxes whose model name begins with \"LUT\"\n" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     [] 
-
-***********************************************************************/
-int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew, * pNtlOld;
-    int c, fVerbose;
-    int nPartSize;
-    int nConfLimit;
-    int nLevelMax;
-    int fUseCSat;
-
-    // set defaults
-    nPartSize    = 0;
-    nConfLimit   = 100;   
-    nLevelMax    = 0;
-    fUseCSat     = 0;
-    fVerbose     = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLcvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nPartSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nPartSize < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
-                goto usage;
-            break;
-         case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nLevelMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nLevelMax < 0 ) 
-                goto usage;
-            break;
-        case 'c':
-            fUseCSat ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Fraig(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-
-    // get the input file name
-    pNtlOld = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-    pNtlNew = Ntl_ManFraig( pNtlOld, nPartSize, nConfLimit, nLevelMax, fUseCSat, fVerbose );
-    if ( pNtlNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Fraig(): Tranformation has failed.\n" );
-        return 1;
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Fraig(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Fraig(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *fraig [-P num] [-C num] [-L num] [-vh]\n" );
-    Abc_Print( -2, "\t         applies SAT sweeping to netlist with white-boxes\n" );
-    Abc_Print( -2, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
-    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-    Abc_Print( -2, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
-//    Abc_Print( -2, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew, * pNtlOld;
-    int c;
-    int fLatchConst;
-    int fLatchEqual;
-    int fVerbose;
-
-    // set defaults
-    fLatchConst = 1;
-    fLatchEqual = 1;
-    fVerbose    = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'c':
-            fLatchConst ^= 1;
-            break;
-        case 'e':
-            fLatchEqual ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scl(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-
-    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scl(): The network is combinational.\n" );
-        return 0;
-    }
-
-    // get the input file name
-    pNtlOld = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-    pNtlNew = Ntl_ManScl( pNtlOld, fLatchConst, fLatchEqual, fVerbose );
-    if ( pNtlNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scl(): Tranformation has failed.\n" );
-        return 1;
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scl(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scl(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *scl [-cevh]\n" );
-    Abc_Print( -2, "\t         performs sequential cleanup of the netlist\n" );
-    Abc_Print( -2, "\t         by removing nodes and latches that do not feed into POs\n" );
-    Abc_Print( -2, "\t-c     : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
-    Abc_Print( -2, "\t-e     : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew, * pNtlOld;
-    int c;
-    int fScorrGia;
-    int fUseCSat;
-    int nFramesP;
-    int nConfMax;
-    int fVerbose;
-
-    // set defaults
-    fScorrGia  = 0;
-    fUseCSat   = 0;
-    nFramesP   = 0;
-    nConfMax   = 10000;
-    fVerbose   = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PCncvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFramesP = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFramesP < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfMax < 0 ) 
-                goto usage;
-            break;
-        case 'n':
-            fScorrGia ^= 1;
-            break;
-        case 'c':
-            fUseCSat ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lcorr(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-
-    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lcorr(): The network is combinational.\n" );
-        return 0;
-    }
- 
-    // get the input file name
-    pNtlOld = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-    pNtlNew = Ntl_ManLcorr( pNtlOld, nConfMax, fScorrGia, fUseCSat, fVerbose );
-    if ( pNtlNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lcorr(): Tranformation has failed.\n" );
-        return 1;
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lcorr(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Lcorr(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *lcorr [-C num] [-ncvh]\n" );
-    Abc_Print( -2, "\t         computes latch correspondence for the netlist\n" );
-//    Abc_Print( -2, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
-    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfMax );
-    Abc_Print( -2, "\t-n     : toggle using new AIG package [default = %s]\n", fScorrGia? "yes": "no" );
-    Abc_Print( -2, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", fUseCSat? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew, * pNtlOld;
-    Fra_Ssw_t Pars, * pPars = &Pars;
-    int c;
-
-    // set defaults
-    pPars->nPartSize   = 0;
-    pPars->nOverSize   = 0;
-    pPars->nFramesP    = 0;
-    pPars->nFramesK    = 1;
-    pPars->nMaxImps    = 5000;
-    pPars->nMaxLevs    = 0;
-    pPars->nMinDomSize = 100;
-    pPars->fUseImps    = 0;
-    pPars->fRewrite    = 0;
-    pPars->fFraiging   = 0;
-    pPars->fLatchCorr  = 0;
-    pPars->fWriteImps  = 0;
-    pPars->fUse1Hot    = 0;
-    pPars->fVerbose    = 0;
-    pPars->TimeLimit   = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILDirfletvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nPartSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nPartSize < 2 ) 
-                goto usage;
-            break;
-        case 'Q':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nOverSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nOverSize < 0 ) 
-                goto usage;
-            break;
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesP = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesP < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesK = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesK <= 0 ) 
-                goto usage;
-            break;
-        case 'I':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxImps = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxImps <= 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxLevs <= 0 ) 
-                goto usage;
-            break;
-        case 'D':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMinDomSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMinDomSize <= 0 ) 
-                goto usage;
-            break;
-        case 'i':
-            pPars->fUseImps ^= 1;
-            break;
-        case 'r':
-            pPars->fRewrite ^= 1;
-            break;
-        case 'f':
-            pPars->fFraiging ^= 1;
-            break;
-        case 'l':
-            pPars->fLatchCorr ^= 1;
-            break;
-        case 'e':
-            pPars->fWriteImps ^= 1;
-            break;
-        case 't':
-            pPars->fUse1Hot ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-
-    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
-
-    if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
-    {
-        Abc_Print( -1, "Currrently can only use one-hotness for simple induction (K=1).\n" );
-        return 0;
-    }
-
-    if ( pPars->nFramesP && pPars->fUse1Hot )
-    {
-        Abc_Print( -1, "Currrently can only use one-hotness without prefix.\n" );
-        return 0;
-    }
-
-    // get the input file name
-    pNtlOld = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-    pNtlNew = Ntl_ManSsw( pNtlOld, pPars );
-    if ( pNtlNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ssw(): Tranformation has failed.\n" );
-        return 1;
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ssw(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ssw(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *ssw [-PQNFLD num] [-lrfetvh]\n" );
-    Abc_Print( -2, "\t         performs sequential sweep using K-step induction on the netlist \n" );
-    Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
-    Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
-    Abc_Print( -2, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
-    Abc_Print( -2, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
-    Abc_Print( -2, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
-    Abc_Print( -2, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
-//    Abc_Print( -2, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
-//    Abc_Print( -2, "\t-i     : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
-    Abc_Print( -2, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
-    Abc_Print( -2, "\t-f     : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
-    Abc_Print( -2, "\t-e     : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
-    Abc_Print( -2, "\t-t     : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew, * pNtlOld;
-    Ssw_Pars_t Pars, * pPars = &Pars;
-    int c;
-
-    // set defaults
-    Ssw_ManSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSDVMpldsncvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nPartSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nPartSize < 2 ) 
-                goto usage;
-            break;
-        case 'Q':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nOverSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nOverSize < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesK = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesK <= 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBTLimit <= 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMaxLevs <= 0 ) 
-                goto usage;
-            break;
-        case 'S':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesAddSim = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesAddSim < 0 ) 
-                goto usage;
-            break;
-        case 'D':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nMinDomSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nMinDomSize < 0 ) 
-                goto usage;
-            break;
-        case 'V':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nSatVarMax2 = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nSatVarMax2 < 0 ) 
-                goto usage;
-            break;
-        case 'M':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nRecycleCalls2 = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nRecycleCalls2 < 0 ) 
-                goto usage;
-            break;
-        case 'p':
-            pPars->fPolarFlip ^= 1;
-            break;
-        case 'l':
-            pPars->fLatchCorr ^= 1;
-            break;
-        case 'd':
-            pPars->fDynamic ^= 1;
-            break;
-        case 's':
-            pPars->fLocalSim ^= 1;
-            break;
-        case 'n':
-            pPars->fScorrGia ^= 1;
-            break;
-        case 'c':
-            pPars->fUseCSat ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
-        return 1;
-    }
-
-    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
-
-    if ( pPars->fDynamic && (pPars->nPartSize || pPars->nOverSize) )
-    {
-        pPars->nPartSize = 0;
-        pPars->nOverSize = 0;
-        Abc_Print( -1, "With dynamic partitioning (-d) enabled, static one (-P <num> -Q <num>) is ignored.\n" );
-    }
-
-    // get the input file name
-    pNtlOld = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-    pNtlNew = Ntl_ManScorr( pNtlOld, pPars );
-    if ( pNtlNew == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scorr(): Tranformation has failed.\n" );
-        return 1;
-    }
-
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scorr(): Reading BLIF has failed.\n" );
-        return 1;
-    }
-    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-    if ( pAbc->pAbc8Aig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Scorr(): AIG extraction has failed.\n" );
-        return 1;
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *scorr [-PQFCLSDVM num] [-pldsncvh]\n" );
-    Abc_Print( -2, "\t         performs sequential sweep using K-step induction\n" );
-    Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
-    Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
-    Abc_Print( -2, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
-    Abc_Print( -2, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
-    Abc_Print( -2, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
-    Abc_Print( -2, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
-    Abc_Print( -2, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
-    Abc_Print( -2, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
-    Abc_Print( -2, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
-    Abc_Print( -2, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
-    Abc_Print( -2, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
-    Abc_Print( -2, "\t-d     : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" );
-    Abc_Print( -2, "\t-n     : toggle using new AIG package [default = %s]\n", pPars->fScorrGia? "yes": "no" );
-    Abc_Print( -2, "\t-c     : toggle using new AIG package and SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlTemp;
-    int Counter;
-    int fMapped;
-    int fVerbose;
-    int c;
-
-    // set defaults
-    fMapped  = 0;
-    fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'm':
-            fMapped ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
-        return 1;
-    }
-
-    // if mapped, insert the network
-    if ( fMapped )
-    {
-        if ( pAbc->pAbc8Nwk == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc8Sweep(): There is no mapped network to sweep.\n" );
-            return 1;
-        }
-        pNtlTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-        if ( pNtlTemp == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc8Sweep():  Inserting mapped network has failed.\n" );
-            return 1;
-        }
-        Abc_FrameClearDesign(); 
-        pAbc->pAbc8Ntl = pNtlTemp;
-    }
- 
-    // sweep the current design
-    Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
-    if ( Counter == 0 && fVerbose )
-        Abc_Print( -1, "The netlist is unchanged by sweep.\n" );
-
-    // if mapped, create new AIG and new mapped network
-    if ( fMapped )
-    {
-        pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-        if ( pAbc->pAbc8Aig == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
-            return 1;
-        }
-        pAbc->pAbc8Nwk = Ntl_ManExtractNwk( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, NULL );
-        if ( pAbc->pAbc8Nwk == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc8Sweep(): Failed to extract the mapped network.\n" );
-            return 1;
-        }
-    }
-    else // remove old AIG/mapped and create new AIG
-    {
-        pNtlTemp = pAbc->pAbc8Ntl; pAbc->pAbc8Ntl = NULL;
-        Abc_FrameClearDesign(); 
-        pAbc->pAbc8Ntl = pNtlTemp;
-        // extract new AIG
-        pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
-        if ( pAbc->pAbc8Aig == NULL )
-        {
-            Abc_Print( -1, "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
-            return 1;
-        }
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *sw [-mvh]\n" );
-    Abc_Print( -2, "\t        performs structural sweep of the netlist\n" );
-    Abc_Print( -2, "\t        removes dangling nodes, registers, and white-boxes\n" );
-    Abc_Print( -2, "\t-m    : inserts mapped network into netlist and sweeps it [default = %s]\n", fMapped? "yes": "no" );
-    Abc_Print( -2, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Zero( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Ntl_Man_t * pNtlNew;
-    int fVerbose;
-    int c;
-
-    // set defaults
-    fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Zero(): There is no design to convert.\n" );
-        return 1;
-    }
-
-    // transform the registers
-    pNtlNew = pAbc->pAbc8Ntl;
-    pAbc->pAbc8Ntl = NULL;
-    Ntl_ManTransformInitValues( pNtlNew );
-
-    // replace the design
-    Abc_FrameClearDesign(); 
-    pAbc->pAbc8Ntl = pNtlNew;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *zero [-h]\n" );
-    Abc_Print( -2, "\t        converts registers to have constant-0 initial value\n" );
-    Abc_Print( -2, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Aig_Man_t * pAig1, * pAig2;
-    Ntl_Man_t * pTemp1, * pTemp2;
-    char ** pArgvNew;
-    int nArgcNew;
-    int c;
-    int fVerbose;
-    int nConfLimit;
-    int fSmart;
-    int nPartSize;
-    extern int         Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
-
-    // set defaults
-    nConfLimit = 100000;   
-    nPartSize  = 100;
-    fSmart     = 0;
-    fVerbose   = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CPsvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
-                goto usage;
-            break;
-        case 'P':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nPartSize = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nPartSize < 0 ) 
-                goto usage;
-            break;
-        case 's':
-            fSmart ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    pArgvNew = argv + globalUtilOptind;
-    nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 0 && nArgcNew != 2 )
-    {
-        Abc_Print( -1, "Currently can only compare current mapped network against the spec, or designs derived from two files.\n" );
-        return 0;
-    }
-    if ( nArgcNew == 2 )
-    {
-        Ntl_ManPrepareCec( pArgvNew[0], pArgvNew[1], &pAig1, &pAig2 );
-        if ( !pAig1 || !pAig2 )
-            return 1;
-        Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
-        Aig_ManStop( pAig1 );
-        Aig_ManStop( pAig2 );
-        return 0;
-    }
-
-    if ( pAbc->pAbc8Ntl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Cec(): There is no design to verify.\n" );
-        return 1;
-    }
-    if ( pAbc->pAbc8Nwk == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc8Cec(): There is no mapped network to verify.\n" );
-        return 1;
-    }
-//    Abc_Print( -1, "Currently *cec works only for two designs given on command line.\n" );
-
-    // insert the mapped network
-    pTemp1 = Ntl_ManDup( pAbc->pAbc8Ntl );
-    pTemp2 = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
-    if ( pTemp2 == NULL )
-    {
-        Ntl_ManFree( pTemp1 );
-        Abc_Print( -1, "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
-        return 1;
-    }
-    Ntl_ManPrepareCecMans( pTemp1, pTemp2, &pAig1, &pAig2 );
-    Ntl_ManFree( pTemp1 );
-    Ntl_ManFree( pTemp2 );
-    if ( !pAig1 || !pAig2 )
-        return 1;
-    Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
-    Aig_ManStop( pAig1 );
-    Aig_ManStop( pAig2 );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *cec [-C num] [-P num] [-svh] <file1> <file2>\n" );
-    Abc_Print( -2, "\t         performs combinational equivalence checking\n" );
-    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
-    Abc_Print( -2, "\t-P num : the partition size for partitioned CEC [default = %d]\n", nPartSize );
-    Abc_Print( -2, "\t-s     : toggle smart and natural output partitioning [default = %s]\n", fSmart? "smart": "natural" );
-    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    Abc_Print( -2, "\tfile1  : (optional) the file with the first network\n");
-    Abc_Print( -2, "\tfile2  : (optional) the file with the second network\n");
-    Abc_Print( -2, "\t         if no files are given, uses the current network and its spec\n");
-    Abc_Print( -2, "\t         if two files are given, compares designs derived from files\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Fra_Sec_t SecPar, * pSecPar = &SecPar;
-    Aig_Man_t * pAig;
-    char ** pArgvNew;
-    int nArgcNew;
-    int c;
-
-    extern void Fra_SecSetDefaultParams( Fra_Sec_t * pSecPar );
-    extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar, Aig_Man_t ** ppResult );
-
-    // set defaults
-    Fra_SecSetDefaultParams( pSecPar );
-    pSecPar->nFramesMax     = 4;
-    pSecPar->fPhaseAbstract = 0;
-    pSecPar->fRetimeFirst   = 0;
-    pSecPar->fRetimeRegs    = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pSecPar->nFramesMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pSecPar->nFramesMax < 0 ) 
-                goto usage;
-            break;
-        case 'a':
-            pSecPar->fPhaseAbstract ^= 1;
-            break;
-        case 'r':
-            pSecPar->fRetimeFirst ^= 1;
-            break;
-        case 'm':
-            pSecPar->fRetimeRegs ^= 1;
-            break;
-        case 'f':
-            pSecPar->fFraiging ^= 1;
-            break;
-        case 'w':
-            pSecPar->fVeryVerbose ^= 1;
-            break;
-        case 'v':
-            pSecPar->fVerbose ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    pArgvNew = argv + globalUtilOptind;
-    nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew != 2 )
-    {
-        Abc_Print( -1, "Only works for two designs written from files specified on the command line.\n" );
-        return 1;
-    }
-
-    pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
-    if ( pAig == NULL )
-        return 0;
-    Fra_FraigSec( pAig, pSecPar, NULL );
-    Aig_ManStop( pAig );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: *dsec [-F num] [-armfwvh] <file1> <file2>\n" );
-    Abc_Print( -2, "\t         performs sequential equivalence checking for two designs\n" );
-    Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
-    Abc_Print( -2, "\t-a     : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" );
-    Abc_Print( -2, "\t-m     : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" );
-    Abc_Print( -2, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    Abc_Print( -2, "\tfile1  : the file with the first design\n");
-    Abc_Print( -2, "\tfile2  : the file with the second design\n");
-//    Abc_Print( -2, "\t         if no files are given, uses the current network and its spec\n");
-//    Abc_Print( -2, "\t         if one file is given, uses the current network and the file\n");
-    return 1;
-}
-
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -24791,7 +21607,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkForEachCi( pNtk, pObj, i ) {
             if (i < Vec_PtrSize(pAbc->pGia->vNamesIn)) {
                 Nm_ManDeleteIdName(pNtk->pManName, pObj->Id);
-                Abc_ObjAssignName( pObj, Vec_PtrEntry(pAbc->pGia->vNamesIn, i), NULL );
+                Abc_ObjAssignName( pObj, (char *)Vec_PtrEntry(pAbc->pGia->vNamesIn, i), NULL );
             }
         }
     }
@@ -28188,14 +25004,14 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     extern void Gia_ManSetIfParsDefault( If_Par_t * pPars );
     extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars );
-    if ( pAbc->pAbc8Lib == NULL )
-    {
-        Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
-        pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
-    }
     // set defaults
     Gia_ManSetIfParsDefault( pPars );
-    pPars->pLutLib = pAbc->pAbc8Lib;
+//    if ( pAbc->pAbc8Lib == NULL )
+//    {
+//        Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
+//        pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
+//    }
+//    pPars->pLutLib = pAbc->pAbc8Lib;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbvh" ) ) != EOF )
     {
diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c
deleted file mode 100644
index 3bfaaa98..00000000
--- a/src/base/abci/abcAbc8.c
+++ /dev/null
@@ -1,280 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [abcAbc8.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Network and node package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: abcAbc8.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "nwk.h"
-#include "mfx.h"
-
-#include "main.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Converts old ABC network into new ABC network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Nwk_Man_t * Abc_NtkToNtkNew( Abc_Ntk_t * pNtk )
-{
-    Vec_Ptr_t * vNodes;
-    Nwk_Man_t * pNtkNew;
-    Nwk_Obj_t * pObjNew;
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k;
-    if ( !Abc_NtkIsLogic(pNtk) )
-    {
-        fprintf( stdout, "This is not a logic network.\n" );
-        return 0;
-    }
-    // convert into the AIG
-    if ( !Abc_NtkToAig(pNtk) )
-    {
-        fprintf( stdout, "Converting to AIGs has failed.\n" );
-        return 0;
-    }
-    assert( Abc_NtkHasAig(pNtk) );
-    // construct the network
-    pNtkNew = Nwk_ManAlloc();
-    pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
-    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec );
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Nwk_ManCreateCi( pNtkNew, Abc_ObjFanoutNum(pObj) );
-    vNodes = Abc_NtkDfs( pNtk, 1 );
-    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
-    {
-        pObjNew = Nwk_ManCreateNode( pNtkNew, Abc_ObjFaninNum(pObj), Abc_ObjFanoutNum(pObj) );
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            Nwk_ObjAddFanin( pObjNew, (Nwk_Obj_t *)pFanin->pCopy );
-        pObjNew->pFunc = Hop_Transfer( (Hop_Man_t *)pNtk->pManFunc, pNtkNew->pManHop, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj) );
-        pObj->pCopy = (Abc_Obj_t *)pObjNew;
-    }
-    Vec_PtrFree( vNodes );
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pObjNew = Nwk_ManCreateCo( pNtkNew );
-        Nwk_ObjAddFanin( pObjNew, (Nwk_Obj_t *)Abc_ObjFanin0(pObj)->pCopy );
-    }
-//    if ( !Nwk_ManCheck( pNtkNew ) )
-//        fprintf( stdout, "Abc_NtkToNtkNew(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Converts new ABC network into old ABC network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromNtkNew( Abc_Ntk_t * pNtkOld, Nwk_Man_t * pNtk )
-{
-    Vec_Ptr_t * vNodes;
-    Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObjNew, * pFaninNew;
-    Nwk_Obj_t * pObj, * pFanin;
-    int i, k;
-    // construct the network
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
-    pNtkNew->pName = Extra_UtilStrsav( pNtk->pName );
-    pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec );
-    Nwk_ManForEachCi( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkCreatePi( pNtkNew );
-        pObj->pCopy = (Nwk_Obj_t *)pObjNew;
-        Abc_ObjAssignName( pObjNew, Abc_ObjName( Abc_NtkCi(pNtkOld, i) ), NULL );
-    }
-    vNodes = Nwk_ManDfs( pNtk );
-    Vec_PtrForEachEntry( Nwk_Obj_t *, vNodes, pObj, i )
-    {
-        if ( !Nwk_ObjIsNode(pObj) )
-            continue;
-        pObjNew = Abc_NtkCreateNode( pNtkNew );
-        Nwk_ObjForEachFanin( pObj, pFanin, k )
-            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pFanin->pCopy );
-        pObjNew->pData = Hop_Transfer( pNtk->pManHop, (Hop_Man_t *)pNtkNew->pManFunc, pObj->pFunc, Nwk_ObjFaninNum(pObj) );
-        pObj->pCopy = (Nwk_Obj_t *)pObjNew;
-    }
-    Vec_PtrFree( vNodes );
-    Nwk_ManForEachCo( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkCreatePo( pNtkNew );
-        if ( pObj->fInvert )
-            pFaninNew = Abc_NtkCreateNodeInv( pNtkNew, (Abc_Obj_t *)Nwk_ObjFanin0(pObj)->pCopy );
-        else
-            pFaninNew = (Abc_Obj_t *)Nwk_ObjFanin0(pObj)->pCopy;
-        Abc_ObjAddFanin( pObjNew, pFaninNew );
-        Abc_ObjAssignName( pObjNew, Abc_ObjName( Abc_NtkCo(pNtkOld, i) ), NULL );
-    }
-    if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkFromNtkNew(): Network check has failed.\n" );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest2( Abc_Ntk_t * pNtk ) 
-{
-    extern void Abc_NtkSupportSum( Abc_Ntk_t * pNtk );
-    Abc_Ntk_t * pNtkNew;
-    Nwk_Man_t * pMan;
-    int clk;
-
-clk = clock();
-    Abc_NtkSupportSum( pNtk );
-ABC_PRT( "Time", clock() - clk );
-
-    pMan = Abc_NtkToNtkNew( pNtk );
-clk = clock();
-    Nwk_ManSupportSum( pMan );
-ABC_PRT( "Time", clock() - clk );
-
-    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
-    Nwk_ManFree( pMan );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest3( Abc_Ntk_t * pNtk ) 
-{
-    extern void Abc_NtkSupportSum( Abc_Ntk_t * pNtk );
-    extern void *          Abc_FrameReadLibLut();                    
-
-    Abc_Ntk_t * pNtkNew;
-    Nwk_Man_t * pMan;
-    int clk;
-
-clk = clock();
-    printf( "%6.2f\n", Abc_NtkDelayTraceLut( pNtk, 1 ) );
-ABC_PRT( "Time", clock() - clk );
-
-    pMan = Abc_NtkToNtkNew( pNtk );
-    pMan->pLutLib = (If_Lib_t *)Abc_FrameReadLibLut();
-clk = clock();
-    printf( "%6.2f\n", Nwk_ManDelayTraceLut( pMan ) );
-ABC_PRT( "Time", clock() - clk );
-
-    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
-    Nwk_ManFree( pMan );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest4( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ) 
-{
-
-    Mfx_Par_t Pars, * pPars = &Pars;
-    Abc_Ntk_t * pNtkNew;
-    Nwk_Man_t * pMan;
-    pMan = Abc_NtkToNtkNew( pNtk );
-
-    Mfx_ParsDefault( pPars );
-    Mfx_Perform( pMan, pPars, pLutLib );
-
-    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
-    Nwk_ManFree( pMan );
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib ) 
-{
-    Vec_Ptr_t * vNodes;
-    extern Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
-    extern Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
-
-    Abc_Ntk_t * pNtkNew;
-    Nwk_Man_t * pMan;
-    pMan = Abc_NtkToNtkNew( pNtk );
-
-    vNodes = Nwk_ManRetimeCutBackward( pMan, Abc_NtkLatchNum(pNtk), 1 );
-//    vNodes = Nwk_ManRetimeCutForward( pMan, Abc_NtkLatchNum(pNtk), 1 );
-    Vec_PtrFree( vNodes );
-
-    pNtkNew = Abc_NtkFromNtkNew( pNtk, pMan );
-    Nwk_ManFree( pMan );
-    return pNtkNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index d1712f4d..6408b54f 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "mio.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/map/mio/mio.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index 02d5fd17..e1e479e3 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index a4fa0451..c46fd4b7 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -18,8 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index bae29e07..fc093420 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "bdc.h"
-#include "kit.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/bdc/bdc.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c
index 25fba5fd..3a8567fe 100644
--- a/src/base/abci/abcBm.c
+++ b/src/base/abci/abcBm.c
@@ -27,10 +27,10 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "sim.h"
-#include "satSolver.h"
+#include "src/base/abc/abc.h"
+#include "src/opt/sim/sim.h"
+#include "src/sat/bsat/satSolver.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
index 21f2d484..6ea4435c 100644
--- a/src/base/abci/abcBmc.c
+++ b/src/base/abci/abcBmc.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "ivy.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/ivy/ivy.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 68c91343..7e80c919 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c
index 533321c5..a477077d 100644
--- a/src/base/abci/abcCascade.c
+++ b/src/base/abci/abcCascade.c
@@ -18,8 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "reo.h"
+#include "src/base/abc/abc.h"
+#include "src/bdd/reo/reo.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -263,7 +264,7 @@ int Abc_ResCofCount( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pChec
     Vec_PtrFree( vCofs );
     if ( pCheck )
     {
-        *pCheck = Abc_ResCheckNonStrict( Pattern, nVars, Extra_Base2Log(Result) );
+        *pCheck = Abc_ResCheckNonStrict( Pattern, nVars, Abc_Base2Log(Result) );
 /*
         if ( *pCheck == 1 && nVars == 4 && Result == 8 )
         {
@@ -290,7 +291,7 @@ int Abc_ResCofCount( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pChec
 int Abc_ResCost( DdManager * dd, DdNode * bFunc, unsigned uMask, int * pnCofs, int * pCheck )
 {
     int nCofs = Abc_ResCofCount( dd, bFunc, uMask, pCheck );
-    int n2Log = Extra_Base2Log( nCofs );
+    int n2Log = Abc_Base2Log( nCofs );
     if ( pnCofs ) *pnCofs = nCofs;
     return 10000 * n2Log + (nCofs - (1 << (n2Log-1))) * (nCofs - (1 << (n2Log-1)));
 }
@@ -360,7 +361,7 @@ void Abc_ResPrint( DdManager * dd, DdNode * bFunc, int nInputs, unsigned uParts[
         CostAll += Cost;
         for ( k = 0; k < nInputs; k++ )
             printf( "%c", (uParts[i] & (1 << k))? 'a' + k : '-' );
-        printf( " %2d %d-%d %6d   ", nCofs, Extra_Base2Log(nCofs), fCheck, Cost );
+        printf( " %2d %d-%d %6d   ", nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
     }
     printf( "%4d\n", CostAll );
 }
@@ -390,7 +391,7 @@ void Abc_ResPrintAllCofs( DdManager * dd, DdNode * bFunc, int nInputs, int nCofM
         for ( k = 0; k < nInputs; k++ )
             printf( "%c", (i & (1 << k))? 'a' + k : '-' );
         printf( "  n=%2d  c=%2d  l=%d-%d   %6d\n", 
-            Extra_WordCountOnes(i), nCofs, Extra_Base2Log(nCofs), fCheck, Cost );
+            Extra_WordCountOnes(i), nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
     }
 }
 
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 07996b9a..69525e2f 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index a08ce490..6116649e 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "cut.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/opt/cut/cut.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4a74ad7e..b032b4e4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -18,22 +18,22 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "giaAig.h"
-#include "dar.h"
-#include "cnf.h"
-#include "fra.h"
-#include "fraig.h"
-#include "int.h"
-#include "dch.h"
-#include "ssw.h"
-#include "cgt.h"
-#include "bbr.h"
-#include "gia.h"
-#include "cec.h"
-#include "csw.h"
-#include "pdr.h" 
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/aig/gia/giaAig.h"
+#include "src/opt/dar/dar.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/proof/fra/fra.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/proof/int/int.h"
+#include "src/proof/dch/dch.h"
+#include "src/proof/ssw/ssw.h"
+#include "src/opt/cgt/cgt.h"
+#include "src/proof/bbr/bbr.h"
+#include "src/aig/gia/gia.h"
+#include "src/proof/cec/cec.h"
+#include "src/opt/csw/csw.h"
+#include "src/proof/pdr/pdr.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -358,7 +358,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         }
 */
         assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
-        nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
+        nDigits = Abc_Base10Log( Abc_NtkLatchNum(pNtkNew) );
         Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
         {
             pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
@@ -1669,7 +1669,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
 
 /*
 #include <signal.h>
-#include "utilMem.h"
+#include "src/misc/util/utilMem.h"
 static void sigfunc( int signo ) 
 {
     if (signo == SIGINT) {
@@ -2160,10 +2160,10 @@ int Abc_NtkDarDemiterDual( Abc_Ntk_t * pNtk, int fVerbose )
     }
     // create new AIG
     ABC_FREE( pPart0->pName );
-    pPart0->pName = Aig_UtilStrsav( "part0" );
+    pPart0->pName = Abc_UtilStrsav( "part0" );
     // create new AIGs
     ABC_FREE( pPart1->pName );
-    pPart1->pName = Aig_UtilStrsav( "part1" );
+    pPart1->pName = Abc_UtilStrsav( "part1" );
     // create file names
     pFileNameGeneric = Extra_FileNameGeneric( pNtk->pSpec );
     sprintf( pFileName0,  "%s%s",  pFileNameGeneric, "_part0.aig" ); 
@@ -3831,8 +3831,8 @@ int Abc_NtkDarReach( Abc_Ntk_t * pNtk, Saig_ParBbr_t * pPars )
 
 ABC_NAMESPACE_IMPL_END
 
-#include "amap.h"
-#include "mio.h"
+#include "src/map/amap/amap.h"
+#include "src/map/mio/mio.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -4095,7 +4095,7 @@ void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose )
             printf( "Primary output :  ", i );
         else
             printf( "Constraint %3d :  ", i-(Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan)) );
-        printf( "ProbOne = %f  ", Aig_Int2Float(Entry) );
+        printf( "ProbOne = %f  ", Abc_Int2Float(Entry) );
         printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
         printf( "\n" );
     }
diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c
index 43ceb63a..baf87944 100644
--- a/src/base/abci/abcDebug.c
+++ b/src/base/abci/abcDebug.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "ioAbc.h"
+#include "src/base/abc/abc.h"
+#include "src/base/io/ioAbc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
index c9c956e4..745dcac0 100644
--- a/src/base/abci/abcDress.c
+++ b/src/base/abci/abcDress.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "ioAbc.h"
+#include "src/base/abc/abc.h"
+#include "src/base/io/ioAbc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcDress2.c b/src/base/abci/abcDress2.c
index 039a4fed..fbaf833a 100644
--- a/src/base/abci/abcDress2.c
+++ b/src/base/abci/abcDress2.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "aig.h"
-#include "dch.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/aig/aig.h"
+#include "src/proof/dch/dch.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -392,8 +392,8 @@ void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, int Tim
         NegAll[1] += Neg[1]; // total negative polarity in network 1
 
         // assuming that the name can be transferred to only one node
-        PairsAll += ABC_MIN(Neg[0] + Pos[0], Neg[1] + Pos[1]);
-        PairsOne += ABC_MIN(Neg[0], Neg[1]) + ABC_MIN(Pos[0], Pos[1]);
+        PairsAll += Abc_MinInt(Neg[0] + Pos[0], Neg[1] + Pos[1]);
+        PairsOne += Abc_MinInt(Neg[0], Neg[1]) + Abc_MinInt(Pos[0], Pos[1]);
     }
     printf( "Total number of equiv classes                = %7d.\n", Vec_PtrSize(vRes) );
     printf( "Participating nodes from both networks       = %7d.\n", NegAll[0]+PosAll[0]+NegAll[1]+PosAll[1] );
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 250cac14..c4086ce7 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "dsd.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
+#include "src/bdd/dsd/dsd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index c8c1d8e1..2e78ad3f 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "espresso.h"
+#include "base/abc/abc.h"
+#include "misc/espresso/espresso.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcExtract.c b/src/base/abci/abcExtract.c
index 8eca34a6..e6b4193b 100644
--- a/src/base/abci/abcExtract.c
+++ b/src/base/abci/abcExtract.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcFlop.c b/src/base/abci/abcFlop.c
index a735f279..6ed411f7 100644
--- a/src/base/abci/abcFlop.c
+++ b/src/base/abci/abcFlop.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 0c45c7d2..4d6b2978 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -18,8 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fpgaInt.h"
+#include "src/base/abc/abc.h"
+#include "src/map/fpga/fpgaInt.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index 46572fa8..1c5693fd 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "ivy.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/ivy/ivy.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 1beab4f4..e1c12b3f 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fraig.h"
-#include "main.h"
+#include "src/base/abc/abc.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -722,7 +722,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
     // no more than 256M for one circuit (128M + 128M)
     nWords1 = 32;
     nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
-    nWordsMin = ABC_MIN( nWords1, nWords2 );
+    nWordsMin = Abc_MinInt( nWords1, nWords2 );
 
     // set parameters for fraiging
     Fraig_ParamsSetDefault( &Params );
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index dbbcb1b1..2470a1d1 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fxu.h"
+#include "src/base/abc/abc.h"
+#include "src/opt/fxu/fxu.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 3299a968..55191021 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -18,8 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -122,7 +121,7 @@ void Abc_GenSorter( char * pFileName, int nVars )
     fprintf( pFile, "\n" );
 
     Counter = 0;
-    nDigits = Extra_Base10Log( (nVars-2)*nVars );
+    nDigits = Abc_Base10Log( (nVars-2)*nVars );
     if ( nVars == 2 )
         fprintf( pFile, ".subckt Comp a=x00 b=x01 x=y00 y=y01\n" );
     else
@@ -427,7 +426,7 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
     int fGenerateFunc = 1;
     FILE * pFile;
     int nVarsLut = (1 << nLutSize);                     // the number of LUT variables
-    int nVarsLog = Extra_Base2Log( nVars + nLuts - 1 ); // the number of encoding vars
+    int nVarsLog = Abc_Base2Log( nVars + nLuts - 1 ); // the number of encoding vars
     int nVarsDeg = (1 << nVarsLog);                     // the number of LUT variables (total)
     int nParsLut = nLuts * (1 << nLutSize);             // the number of LUT params
     int nParsVar = nLuts * nLutSize * nVarsLog;         // the number of var params
@@ -548,12 +547,12 @@ void Abc_GenOneHot( char * pFileName, int nVars )
     fprintf( pFile, "# One-hotness condition for %d vars generated by ABC on %s\n", nVars, Extra_TimeStamp() );
     fprintf( pFile, ".model 1hot_%dvars\n", nVars );
     fprintf( pFile, ".inputs" );
-    nDigitsIn = Extra_Base10Log( nVars );
+    nDigitsIn = Abc_Base10Log( nVars );
     for ( i = 0; i < nVars; i++ )
         fprintf( pFile, " i%0*d", nDigitsIn, i );
     fprintf( pFile, "\n" );
     fprintf( pFile, ".outputs" );
-    nDigitsOut = Extra_Base10Log( nVars * (nVars - 1) / 2 );
+    nDigitsOut = Abc_Base10Log( nVars * (nVars - 1) / 2 );
     for ( i = 0; i < nVars * (nVars - 1) / 2; i++ )
         fprintf( pFile, " o%0*d", nDigitsOut, i );
     fprintf( pFile, "\n" );
@@ -598,12 +597,12 @@ void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t *
     fprintf( pFile, "}\n" );
     fprintf( pFile, ".model 1hot_%dvars_%dregs\n", nPis, nRegs );
     fprintf( pFile, ".inputs" );
-    nDigitsIn = Extra_Base10Log( nPis+nRegs );
+    nDigitsIn = Abc_Base10Log( nPis+nRegs );
     for ( i = 0; i < nPis+nRegs; i++ )
         fprintf( pFile, " i%0*d", nDigitsIn, i );
     fprintf( pFile, "\n" );
     fprintf( pFile, ".outputs" );
-    nDigitsOut = Extra_Base10Log( Counter );
+    nDigitsOut = Abc_Base10Log( Counter );
     for ( i = 0; i < Counter; i++ )
         fprintf( pFile, " o%0*d", nDigitsOut, i );
     fprintf( pFile, "\n" );
@@ -626,7 +625,7 @@ void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t *
 
 ABC_NAMESPACE_IMPL_END
 
-#include "aig.h"
+#include "src/aig/aig/aig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -646,7 +645,7 @@ void Abc_GenRandom( char * pFileName, int nPis )
 {
     FILE * pFile;
     unsigned * pTruth;
-    int i, b, w, nWords = Aig_TruthWordNum( nPis );
+    int i, b, w, nWords = Abc_TruthWordNum( nPis );
     int nDigitsIn;
     Aig_ManRandom( 1 );
     pTruth = ABC_ALLOC( unsigned, nWords );
@@ -656,18 +655,18 @@ void Abc_GenRandom( char * pFileName, int nPis )
     fprintf( pFile, "# Random function with %d inputs generated by ABC on %s\n", nPis, Extra_TimeStamp() );
     fprintf( pFile, ".model rand%d\n", nPis );
     fprintf( pFile, ".inputs" );
-    nDigitsIn = Extra_Base10Log( nPis );
+    nDigitsIn = Abc_Base10Log( nPis );
     for ( i = 0; i < nPis; i++ )
         fprintf( pFile, " i%0*d", nDigitsIn, i );
     fprintf( pFile, "\n" );
     fprintf( pFile, ".outputs f\n" );
     fprintf( pFile, ".names" );
-    nDigitsIn = Extra_Base10Log( nPis );
+    nDigitsIn = Abc_Base10Log( nPis );
     for ( i = 0; i < nPis; i++ )
         fprintf( pFile, " i%0*d", nDigitsIn, i );
     fprintf( pFile, " f\n" );
     for ( i = 0; i < (1<<nPis); i++ )
-        if ( Aig_InfoHasBit(pTruth, i) )
+        if ( Abc_InfoHasBit(pTruth, i) )
         {
             for ( b = nPis-1; b >= 0; b-- )
                 fprintf( pFile, "%d", (i>>b)&1 );
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index b102e04f..073defd0 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 674a4550..ded34d3c 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -18,11 +18,11 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "if.h"
-#include "kit.h"
-#include "aig.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/map/if/if.h"
+#include "src/bool/kit/kit.h"
+#include "src/aig/aig/aig.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcIfMux.c b/src/base/abci/abcIfMux.c
index bf9d6cff..545adafb 100644
--- a/src/base/abci/abcIfMux.c
+++ b/src/base/abci/abcIfMux.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "if.h"
+#include "src/base/abc/abc.h"
+#include "src/map/if/if.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 28ff0ee6..c2637a08 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -18,13 +18,14 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "dec.h"
-#include "fra.h"
-#include "ivy.h"
-#include "fraig.h"
-#include "mio.h"
-#include "aig.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
+#include "src/proof/fra/fra.h"
+#include "src/aig/ivy/ivy.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/map/mio/mio.h"
+#include "src/aig/aig/aig.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcLog.c b/src/base/abci/abcLog.c
index ecccb36b..aa926a41 100644
--- a/src/base/abci/abcLog.c
+++ b/src/base/abci/abcLog.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "gia.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/gia/gia.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -102,7 +102,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nF
     else
     {
         for ( i = 0; i < pCex->nRegs; i++ )
-            fprintf( pFile, "%d", Gia_InfoHasBit(pCex->pData,i) );
+            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
     }
     fprintf( pFile, "\n" );
     // write <TRACE>
@@ -112,7 +112,7 @@ void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nF
     {
         assert( pCex->nBits - pCex->nRegs == pCex->nPis * (pCex->iFrame + 1) );
         for ( i = pCex->nRegs; i < pCex->nBits; i++ )
-            fprintf( pFile, "%d", Gia_InfoHasBit(pCex->pData,i) );
+            fprintf( pFile, "%d", Abc_InfoHasBit(pCex->pData,i) );
     }
     fprintf( pFile, "\n" );
     fclose( pFile );
@@ -211,7 +211,7 @@ int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames )
         assert( Vec_IntSize(vNums) == pCex->nBits );
         for ( c = 0; c < pCex->nBits; c++ )
             if ( Vec_IntEntry(vNums, c) )
-                Gia_InfoSetBit( pCex->pData, c );
+                Abc_InfoSetBit( pCex->pData, c );
         Vec_IntFree( vNums );
         if ( ppCex )
             *ppCex = pCex;
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index 98991e25..1653918f 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "cut.h" 
+#include "src/base/abc/abc.h"
+#include "src/opt/cut/cut.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -175,7 +174,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int
         if ( Abc_ObjFaninNum(pFanin) == 1 )
             pFanin = Abc_ObjFanin0( pFanin );
         // get the new level
-        LevelMax = ABC_MAX( LevelMax, (int)pFanin->Level );
+        LevelMax = Abc_MaxInt( LevelMax, (int)pFanin->Level );
     }
 
     if ( fVerbose )
@@ -516,7 +515,7 @@ int Abc_NodeGetLevel( Abc_Obj_t * pObj )
     int i, Level;
     Level = 0;
     Abc_ObjForEachFanin( pObj, pFanin, i )
-        Level = ABC_MAX( Level, (int)pFanin->Level );
+        Level = Abc_MaxInt( Level, (int)pFanin->Level );
     return Level + 1;
 }
 
@@ -723,7 +722,7 @@ int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
             return 0;
     }
     // the number of cofactors is acceptable
-    nVarsNew = Extra_Base2Log( nClasses );
+    nVarsNew = Abc_Base2Log( nClasses );
     assert( nVarsNew < p->nLutSize );
     // create the remainder truth table
     // for each class of cofactors, multiply cofactor truth table by its code
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 6d62f330..d740777c 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -418,8 +418,8 @@ Abc_Obj_t * Abc_NtkBddCurtis( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t
     DdManager * ddNew = (DdManager *)pNtkNew->pManFunc;
     DdNode * bCof, * bUniq, * bMint, * bTemp, * bFunc, * bBits[10], ** pbCodeVars;
     Abc_Obj_t * pNodeNew = NULL, * pNodeBS[10];
-    int nLutSize = Extra_Base2Log( Vec_PtrSize(vCofs) );
-    int nBits    = Extra_Base2Log( Vec_PtrSize(vUniq) );
+    int nLutSize = Abc_Base2Log( Vec_PtrSize(vCofs) );
+    int nBits    = Abc_Base2Log( Vec_PtrSize(vUniq) );
     int b, c, u, i;
     assert( nBits + 2 <= nLutSize );
     assert( nLutSize < Abc_ObjFaninNum(pNode) );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 578727cc..eeeaf15f 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -18,10 +18,10 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "mio.h"
-#include "mapper.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/map/mio/mio.h"
+#include "src/map/mapper/mapper.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMeasure.c b/src/base/abci/abcMeasure.c
index 5352084f..a366b830 100644
--- a/src/base/abci/abcMeasure.c
+++ b/src/base/abci/abcMeasure.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "kit.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMerge.c b/src/base/abci/abcMerge.c
index d7abece8..917a97da 100644
--- a/src/base/abci/abcMerge.c
+++ b/src/base/abci/abcMerge.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "aig.h"
-#include "nwkMerge.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/aig/aig.h"
+#include "src/opt/nwk/nwkMerge.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index b4510bd0..b88452e8 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
  
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index 429c40c6..0af87d36 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 9cda4608..66734c04 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -18,8 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c
index 299e22d5..c8247b28 100644
--- a/src/base/abci/abcMulti.c
+++ b/src/base/abci/abcMulti.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index 98d27a19..5f612b62 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcNpnSave.c b/src/base/abci/abcNpnSave.c
index 568a3e28..b57d2ef3 100644
--- a/src/base/abci/abcNpnSave.c
+++ b/src/base/abci/abcNpnSave.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "aig.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/aig/aig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -81,7 +80,7 @@ static Npn_Man_t * pNpnMan = NULL;
 void Npn_TruthPermute_rec( char * pStr, int mid, int end )
 {
     static int count = 0;
-    char * pTemp = Aig_UtilStrsav(pStr);
+    char * pTemp = Abc_UtilStrsav(pStr);
     char e;
     int i;
     if ( mid == end ) 
@@ -329,7 +328,7 @@ static inline word Npn_TruthCanon( word t, int nVars, int * pPhase )
                 }
                 else
                 {
-                    if ( ABC_MIN(pSigs[2*v],pSigs[2*v+1]) >= ABC_MIN(pSigs[2*(v+1)],pSigs[2*(v+1)+1]) )
+                    if ( Abc_MinInt(pSigs[2*v],pSigs[2*v+1]) >= Abc_MinInt(pSigs[2*(v+1)],pSigs[2*(v+1)+1]) )
                         continue;
                 }
                 fChange = 1;
@@ -400,7 +399,7 @@ clk = clock();
     pBinsOld = p->pBins;
     nBinsOld = p->nBins;
     // get the new Bins
-    p->nBins = Aig_PrimeCudd( 3 * nBinsOld ); 
+    p->nBins = Abc_PrimeCudd( 3 * nBinsOld ); 
     p->pBins = ABC_CALLOC( int, p->nBins );
     // rehash the entries from the old table
     Counter = 1;
@@ -594,7 +593,7 @@ Npn_Man_t * Npn_ManStart( char * pFileName )
         p->nBufferSize = 1000000;
         p->nBufferSize = 100;
         p->pBuffer     = ABC_ALLOC( Npn_Obj_t, p->nBufferSize );
-        p->nBins       = Aig_PrimeCudd( p->nBufferSize / 2 );
+        p->nBins       = Abc_PrimeCudd( p->nBufferSize / 2 );
         p->pBins       = ABC_CALLOC( int, p->nBins );
         p->nEntries    = 1;
     }
@@ -609,7 +608,7 @@ Npn_Man_t * Npn_ManStart( char * pFileName )
         fclose( pFile );
         p->nBufferSize = 4 * ( Extra_FileSize(pFileName) / 20 );
         p->pBuffer     = ABC_ALLOC( Npn_Obj_t, p->nBufferSize );
-        p->nBins       = Aig_PrimeCudd( p->nBufferSize / 2 );
+        p->nBins       = Abc_PrimeCudd( p->nBufferSize / 2 );
         p->pBins       = ABC_CALLOC( int, p->nBins );
         p->nEntries    = 1;
         Npn_ManRead( p, pFileName );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index e3df605e..a1fab695 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index 50694832..e0f6d6de 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -18,8 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c
index c306d01d..a3f66a63 100644
--- a/src/base/abci/abcOrder.c
+++ b/src/base/abci/abcOrder.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 5df5af62..7ae435d8 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "cmd.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/base/cmd/cmd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -594,7 +594,7 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
         if ( Vec_IntSize(vPartSupp) < 100 )
             Repulse = 1;
         else
-            Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100);
+            Repulse = 1+Abc_Base2Log(Vec_IntSize(vPartSupp)-100);
         Value = Attract/Repulse;
         if ( ValueBest < Value )
         {
diff --git a/src/base/abci/abcPlace.c b/src/base/abci/abcPlace.c
index 06c23e65..7faa5d77 100644
--- a/src/base/abci/abcPlace.c
+++ b/src/base/abci/abcPlace.c
@@ -18,10 +18,10 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "base/abc/abc.h"
 
 // placement includes
-#include "place_base.h"
+#include "phys/place/place_base.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 9e2f48d3..af34029e 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -19,12 +19,13 @@
 ***********************************************************************/
 
 #include <math.h>
-#include "abc.h"
-#include "dec.h"
-#include "main.h"
-#include "mio.h"
-#include "aig.h"
-#include "if.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
+#include "src/base/main/main.h"
+#include "src/map/mio/mio.h"
+#include "src/aig/aig/aig.h"
+#include "src/map/if/if.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -523,7 +524,7 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
         if ( nFanins > vFanins->nSize || nFanouts > vFanouts->nSize )
         {
             nOldSize = vFanins->nSize;
-            nNewSize = ABC_MAX(nFanins, nFanouts) + 10;
+            nNewSize = Abc_MaxInt(nFanins, nFanouts) + 10;
             Vec_IntGrow( vFanins,  nNewSize  );
             Vec_IntGrow( vFanouts, nNewSize );
             for ( k = nOldSize; k < nNewSize; k++ )
@@ -592,12 +593,12 @@ void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk, int fMffc )
             nFanouts = Abc_ObjFanoutNum(pNode);
         nFaninsAll  += nFanins;
         nFanoutsAll += nFanouts;
-        nFaninsMax   = ABC_MAX( nFaninsMax, nFanins );
-        nFanoutsMax  = ABC_MAX( nFanoutsMax, nFanouts );
+        nFaninsMax   = Abc_MaxInt( nFaninsMax, nFanins );
+        nFanoutsMax  = Abc_MaxInt( nFanoutsMax, nFanouts );
     }
 
     // allocate storage for fanin/fanout numbers
-    nSizeMax = ABC_MAX( 10 * (Extra_Base10Log(nFaninsMax) + 1), 10 * (Extra_Base10Log(nFanoutsMax) + 1) );
+    nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) );
     vFanins  = Vec_IntStart( nSizeMax );
     vFanouts = Vec_IntStart( nSizeMax );
 
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 154c5e1c..3a6c42a4 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -18,10 +18,11 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fraig.h"
-#include "math.h"
-#include "extra.h"
+#include <math.h>
+
+#include "src/base/abc/abc.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -254,7 +255,7 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, ABC_INT64_T nInsp
     // no more than 256M for one circuit (128M + 128M)
     nWords1 = 32;
     nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
-    nWordsMin = ABC_MIN( nWords1, nWords2 );
+    nWordsMin = Abc_MinInt( nWords1, nWords2 );
 
     // set the FRAIGing parameters
     Fraig_ParamsSetDefault( pParams );
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index e6395ef3..98cb3eb6 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 262797d2..7185cf8d 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -18,8 +18,7 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index f7bc5186..e1ffa309 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index abb4be4b..e51b15bd 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "if.h"
-#include "kit.h"
+#include "src/base/abc/abc.h"
+#include "src/map/if/if.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -246,7 +246,7 @@ void Rec_ObjSet(Abc_ManRec_t* p, Rec_Obj_t* pRecObj, Abc_Obj_t* pObj, char* newD
     Abc_NodeSetTravIdCurrent(pObj);
     Delay0 = If_CutDelayRecComput_rec(Abc_ObjFanin0(pObj), vCosts);
     Delay1 = If_CutDelayRecComput_rec(Abc_ObjFanin1(pObj), vCosts);
-    Delay = ABC_MAX(Delay0, Delay1) + 1;
+    Delay = Abc_MaxInt(Delay0, Delay1) + 1;
     Vec_StrWriteEntry(vCosts,pObj->Id,Delay);
     return Delay;
  }*/
@@ -299,7 +299,7 @@ char If_CutDepthRecComput_rec(Abc_Obj_t* pObj, int iLeaf)
         return -IF_BIG_CHAR;
     Depth0 = If_CutDepthRecComput_rec(Abc_ObjFanin0(pObj), iLeaf);
     Depth1 = If_CutDepthRecComput_rec(Abc_ObjFanin1(pObj), iLeaf);
-    Depth = ABC_MAX(Depth0, Depth1);
+    Depth = Abc_MaxInt(Depth0, Depth1);
     Depth = (Depth == -IF_BIG_CHAR) ? -IF_BIG_CHAR : Depth + 1;
     assert(Depth <= 127);
     return Depth;
@@ -1064,7 +1064,7 @@ void Abc_NtkRecLibMerge(Abc_Ntk_t* pNtk)
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_ObjSetMax( pObj, i+1 );
     Abc_AigForEachAnd( pNtk, pObj, i )
-        Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+        Abc_ObjSetMax( pObj, Abc_MaxInt( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
 
     // insert the PO nodes into the table
     Abc_NtkForEachPo( pNtk, pObj, i )
@@ -1105,7 +1105,7 @@ void Abc_NtkRecRezieHash(Abc_ManRec_t* p)
     int nBinsNew, Counter, i;
     int clk = clock();
     // get the new table size
-    nBinsNew = Cudd_Prime( 3 * p->nBins ); 
+    nBinsNew = Abc_PrimeCudd( 3 * p->nBins ); 
     printf("Hash table resize from %d to %d.\n", p->nBins, nBinsNew);
     // allocate a new array
     pBinsNew = ABC_ALLOC( Rec_Obj_t *, nBinsNew );
@@ -1242,7 +1242,7 @@ p->timeTruth += clock() - clk;
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_ObjSetMax( pObj, i+1 );
     Abc_AigForEachAnd( pNtk, pObj, i )
-        Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+        Abc_ObjSetMax( pObj, Abc_MaxInt( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
 
     // insert the PO nodes into the table
     timeInsert = clock();
@@ -1308,7 +1308,7 @@ void Abc_NtkRecDumpTruthTables( Abc_ManRec_t * p )
     for ( i = 0; i < p->nBins; i++ )
         for ( pObj = p->pBins[i]; pObj; pObj = pObj->pCopy )
         {
-            pTruth = Vec_PtrEntry(p->vTtNodes, pObj->Id);
+            pTruth = (unsigned *)Vec_PtrEntry(p->vTtNodes, pObj->Id);
             if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
                 continue;
             Extra_PrintHex( pFile, pTruth, nVars );
@@ -1418,7 +1418,7 @@ void Abc_NtkRecPs(int fPrintLib)
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_ObjSetMax( pObj, i+1 );
     Abc_AigForEachAnd( pNtk, pObj, i )
-        Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+        Abc_ObjSetMax( pObj, Abc_MaxInt( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
 if(fPrintLib)
 {
     pFile = fopen( "tt10.txt", "wb" );
@@ -1426,7 +1426,7 @@ for ( i = 0; i < p->nBins; i++ )
     for ( entry = p->pBins[i]; entry; entry = entry->pCopy )
     {
         int tmp = 0;
-        pTruth = Vec_PtrEntry(p->vTtNodes, entry->Id);
+        pTruth = (unsigned *)Vec_PtrEntry(p->vTtNodes, entry->Id);
         /*if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
             continue;*/
         Extra_PrintHex( pFile, pTruth, nVars );
@@ -2416,7 +2416,7 @@ char Abc_NtkRecCurrentDepth_rec(If_Obj_t * pObj, int iLeaf)
         return -IF_BIG_CHAR;
     Depth0 = Abc_NtkRecCurrentDepth_rec(If_ObjFanin0(pObj), iLeaf);
     Depth1 = Abc_NtkRecCurrentDepth_rec(If_ObjFanin1(pObj), iLeaf);
-    Depth = ABC_MAX(Depth0, Depth1);
+    Depth = Abc_MaxInt(Depth0, Depth1);
     Depth = (Depth == -IF_BIG_CHAR) ? -IF_BIG_CHAR : Depth + 1;
     assert(Depth <= 127);
     return Depth;
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index e0cec5cd..4a5be4a2 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3ba171b7..69d84b0c 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "dec.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 848021a0..35cebd9d 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -18,10 +18,11 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "reo.h"
-#include "if.h"
-#include "kit.h"
+#include "src/base/abc/abc.h"
+#include "src/bdd/reo/reo.h"
+#include "src/map/if/if.h"
+#include "src/bool/kit/kit.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index d2e7dcea..5fd041ae 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "reo.h"
+#include "src/base/abc/abc.h"
+#include "src/bdd/reo/reo.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 719d722e..66b1d8e8 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -18,11 +18,11 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "dec.h"
-#include "dsd.h"
-#include "cut.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
+#include "src/opt/cut/cut.h"
+#include "src/misc/extra/extraBdd.h"
+#include "src/bdd/dsd/dsd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -655,7 +655,7 @@ Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst
             // set level
             Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
             Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
-            Dec_GraphNode( pGraph, eNode3.Node )->Level = 1 + ABC_MAX(Level1, Level2);
+            Dec_GraphNode( pGraph, eNode3.Node )->Level = 1 + Abc_MaxInt(Level1, Level2);
             // get the new node if possible
             if ( pNode3 )
             {
@@ -708,7 +708,7 @@ Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst
             // set level
             Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
             Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
-            Dec_GraphNode( pGraph, eNode3.Node )->Level = 2 + ABC_MAX(Level1, Level2);
+            Dec_GraphNode( pGraph, eNode3.Node )->Level = 2 + Abc_MaxInt(Level1, Level2);
             // get the new node if possible
             if ( pNode3 )
             {
@@ -824,7 +824,7 @@ Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst
         Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level;
         Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level;
         Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level;
-        Dec_GraphNode( pGraph, eResult.Node )->Level = 2 + ABC_MAX( ABC_MAX(Level1, Level2), Level3 );
+        Dec_GraphNode( pGraph, eResult.Node )->Level = 2 + Abc_MaxInt( Abc_MaxInt(Level1, Level2), Level3 );
         // get the new node if possible
         if ( pNode4 )
         {
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index aab4d1ce..b03c36aa 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "dec.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1151,7 +1150,7 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
                         break;
                 if ( w == p->nWords )
                 {
-                    LevelMax = ABC_MAX( pObj0->Level, ABC_MAX(pObj1->Level, pObj2->Level) );
+                    LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
                     assert( LevelMax <= Required - 1 );
 
                     pObjMax = NULL;
@@ -1192,7 +1191,7 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
                         break;
                 if ( w == p->nWords )
                 {
-                    LevelMax = ABC_MAX( pObj0->Level, ABC_MAX(pObj1->Level, pObj2->Level) );
+                    LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
                     assert( LevelMax <= Required - 1 );
 
                     pObjMax = NULL;
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 54e19f50..5e2745b9 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -18,10 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "rwr.h"
-#include "dec.h"
+#include "src/base/abc/abc.h"
+#include "src/opt/rwr/rwr.h"
+#include "src/bool/dec/dec.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 3e60ebf9..61c8d085 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -18,10 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fraig.h"
-#include "extra.h"
-#include "sim.h"
+#include "src/base/abc/abc.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/opt/sim/sim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -434,7 +433,7 @@ int Abc_NtkRRWindow( Abc_RRMan_t * p )
     pEdgeFanout = p->pFanout? p->pFanout : p->pNode;
     pEdgeFanin  = p->pFanout? p->pNode : p->pFanin;
     // get the minimum and maximum levels of the window
-    LevelMin = ABC_MAX( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
+    LevelMin = Abc_MaxInt( 0, ((int)p->pFanin->Level) - p->nFaninLevels );
     LevelMax = (int)pEdgeFanout->Level + p->nFanoutLevels;
 
     // start the TFI leaves with the fanin
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index b0c5024a..29f13bda 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -18,10 +18,11 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "cmd.h"
-#include "satSolver.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/base/cmd/cmd.h"
+#include "src/sat/bsat/satSolver.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -590,7 +591,7 @@ int Abc_NtkMiterSatCreateInt( sat_solver * pSat, Abc_Ntk_t * pNtk )
                 continue;
             pPrefVars[nVars++] = (int)pNode->pCopy;
         }
-        nVars = ABC_MIN( nVars, 10 );
+        nVars = Abc_MinInt( nVars, 10 );
         ASat_SolverSetPrefVars( pSat, pPrefVars, nVars );
     }
 */
diff --git a/src/base/abci/abcScorr.c b/src/base/abci/abcScorr.c
index 9687003b..e7683edf 100644
--- a/src/base/abci/abcScorr.c
+++ b/src/base/abci/abcScorr.c
@@ -18,13 +18,13 @@
 
 ***********************************************************************/
  
-#include "abc.h"
-#include "ioAbc.h"
-#include "saig.h"
-#include "ssw.h"
-#include "gia.h"
-#include "cec.h"
-#include "giaAig.h"
+#include "src/base/abc/abc.h"
+#include "src/base/io/ioAbc.h"
+#include "src/aig/saig/saig.h"
+#include "src/proof/ssw/ssw.h"
+#include "src/aig/gia/gia.h"
+#include "src/proof/cec/cec.h"
+#include "src/aig/gia/giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -80,7 +80,7 @@ Vec_Int_t * Abc_NtkMapGiaIntoNameId( Abc_Ntk_t * pNetlist, Aig_Man_t * pAig, Gia
             if ( pGia == NULL )
                 Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
             else
-                Vec_IntWriteEntry( vId2Name, Gia_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
+                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
         }
     }
     // overwrite CO names
@@ -95,7 +95,7 @@ Vec_Int_t * Abc_NtkMapGiaIntoNameId( Abc_Ntk_t * pNetlist, Aig_Man_t * pAig, Gia
             if ( pGia == NULL )
                 Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
             else
-                Vec_IntWriteEntry( vId2Name, Gia_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
+                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
         }
     }
     // overwrite CI names
@@ -110,7 +110,7 @@ Vec_Int_t * Abc_NtkMapGiaIntoNameId( Abc_Ntk_t * pNetlist, Aig_Man_t * pAig, Gia
             if ( pGia == NULL )
                 Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
             else
-                Vec_IntWriteEntry( vId2Name, Gia_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
+                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
         }
     }
     return vId2Name;
diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c
index 8a477c4e..3bcbc205 100644
--- a/src/base/abci/abcSense.c
+++ b/src/base/abci/abcSense.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "fraig.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/proof/fraig/fraig.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcSpeedup.c b/src/base/abci/abcSpeedup.c
index 35a901ad..2c3ebca0 100644
--- a/src/base/abci/abcSpeedup.c
+++ b/src/base/abci/abcSpeedup.c
@@ -18,10 +18,10 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "if.h"
-#include "aig.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/map/if/if.h"
+#include "src/aig/aig/aig.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index e08def57..996c9db0 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -18,9 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "dec.h"
+#include "src/base/abc/abc.h"
+#include "src/bool/dec/dec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -468,7 +467,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCoNum(pNtk) == 1 );
     // get the cutoff level
-    LevelCut = ABC_MAX( 0, Abc_AigLevel(pNtk) - nLevels );
+    LevelCut = Abc_MaxInt( 0, Abc_AigLevel(pNtk) - nLevels );
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 43c99d90..a898f26c 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -18,13 +18,13 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "fraig.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 41abc4db..2a36be14 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
-#include "sim.h"
+#include "src/base/abc/abc.h"
+#include "src/opt/sim/sim.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 79768645..d8334e9d 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -18,9 +18,9 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "mio.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/map/mio/mio.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -139,7 +139,7 @@ void Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float Rise, float Fall )
         pNtk->pManTime = Abc_ManTimeStart();
     pNtk->pManTime->tArrDef.Rise  = Rise;
     pNtk->pManTime->tArrDef.Fall  = Fall;
-    pNtk->pManTime->tArrDef.Worst = ABC_MAX( Rise, Fall );
+    pNtk->pManTime->tArrDef.Worst = Abc_MaxInt( Rise, Fall );
 }
 
 /**Function*************************************************************
@@ -161,7 +161,7 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
         pNtk->pManTime = Abc_ManTimeStart();
     pNtk->pManTime->tReqDef.Rise  = Rise;
     pNtk->pManTime->tReqDef.Fall  = Fall;
-    pNtk->pManTime->tReqDef.Worst = ABC_MAX( Rise, Fall );
+    pNtk->pManTime->tReqDef.Worst = Abc_MaxInt( Rise, Fall );
 }
 
 /**Function*************************************************************
@@ -189,7 +189,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     pTime = (Abc_Time_t *)vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
     pTime->Fall  = Fall;
-    pTime->Worst = ABC_MAX( Rise, Fall );
+    pTime->Worst = Abc_MaxInt( Rise, Fall );
 }
 
 /**Function*************************************************************
@@ -217,7 +217,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     pTime = (Abc_Time_t *)vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
     pTime->Fall  = Fall;
-    pTime->Worst = ABC_MAX( Rise, Fall );
+    pTime->Worst = Abc_MaxInt( Rise, Fall );
 }
 
 /**Function*************************************************************
@@ -625,7 +625,7 @@ void Abc_NodeDelayTraceArrival( Abc_Obj_t * pNode )
         }
         pPin = Mio_PinReadNext(pPin);
     }
-    pTimeOut->Worst = ABC_MAX( pTimeOut->Rise, pTimeOut->Fall );
+    pTimeOut->Worst = Abc_MaxInt( pTimeOut->Rise, pTimeOut->Fall );
 }
 
 
@@ -647,7 +647,7 @@ int Abc_ObjLevelNew( Abc_Obj_t * pObj )
     Abc_Obj_t * pFanin;
     int i, Level = 0;
     Abc_ObjForEachFanin( pObj, pFanin, i )
-        Level = ABC_MAX( Level, Abc_ObjLevel(pFanin) );
+        Level = Abc_MaxInt( Level, Abc_ObjLevel(pFanin) );
     return Level + 1;
 }
 
@@ -669,7 +669,7 @@ int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj )
     Abc_ObjForEachFanout( pObj, pFanout, i )
     {
         LevelCur = Abc_ObjReverseLevel( pFanout );
-        Level = ABC_MAX( Level, LevelCur );
+        Level = Abc_MaxInt( Level, LevelCur );
     }
     return Level + 1;
 }
@@ -827,7 +827,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
                 assert( Abc_ObjLevel(pFanout) >= Lev );
                 Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
 //                Counter++;
-//                CounterMax = ABC_MAX( CounterMax, Counter );
+//                CounterMax = Abc_MaxInt( CounterMax, Counter );
                 pFanout->fMarkA = 1;
             }
         }
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 829a83bd..a56973b6 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index f62ec7fc..72514029 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "extra.h"
+#include "src/base/abc/abc.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 7a9a5239..9b88cb8a 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -18,15 +18,15 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "main.h"
-#include "cmd.h"
-#include "fraig.h"
-#include "sim.h"
-#include "aig.h"
-#include "saig.h"
-#include "gia.h"
-#include "ssw.h"
+#include "src/base/abc/abc.h"
+#include "src/base/main/main.h"
+#include "src/base/cmd/cmd.h"
+#include "src/proof/fraig/fraig.h"
+#include "src/opt/sim/sim.h"
+#include "src/aig/aig/aig.h"
+#include "src/aig/saig/saig.h"
+#include "src/aig/gia/gia.h"
+#include "src/proof/ssw/ssw.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 12ad0e68..23bbbe1a 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "abc.h"
-#include "gia.h"
+#include "src/base/abc/abc.h"
+#include "src/aig/gia/gia.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/fahout_cut.c b/src/base/abci/fahout_cut.c
new file mode 100644
index 00000000..0b4b421f
--- /dev/null
+++ b/src/base/abci/fahout_cut.c
@@ -0,0 +1,357 @@
+/**CFile****************************************************************
+
+  FileName    [abcMerge.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [LUT merging algorithm.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "aig/aig/aig.h"
+#include "aig/nwk/nwkMerge.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanins of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMarkFanins_rec( Abc_Obj_t * pLut, int nLevMin )
+{
+    Abc_Obj_t * pNext;
+    int i;
+    if ( !Abc_ObjIsNode(pLut) )
+        return;
+    if ( Abc_NodeIsTravIdCurrent( pLut ) )
+        return;
+    Abc_NodeSetTravIdCurrent( pLut );
+    if ( Abc_ObjLevel(pLut) < nLevMin )
+        return;
+    Abc_ObjForEachFanin( pLut, pNext, i )
+        Abc_NtkMarkFanins_rec( pNext, nLevMin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the fanouts of the node with the current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMarkFanouts_rec( Abc_Obj_t * pLut, int nLevMax, int nFanMax )
+{
+    Abc_Obj_t * pNext;
+    int i;
+    if ( !Abc_ObjIsNode(pLut) )
+        return;
+    if ( Abc_NodeIsTravIdCurrent( pLut ) )
+        return;
+    Abc_NodeSetTravIdCurrent( pLut );
+    if ( Abc_ObjLevel(pLut) > nLevMax )
+        return;
+    if ( Abc_ObjFanoutNum(pLut) > nFanMax )
+        return;
+    Abc_ObjForEachFanout( pLut, pNext, i )
+        Abc_NtkMarkFanouts_rec( pNext, nLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes around the given set.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax )
+{
+    Abc_Obj_t * pObj, * pNext;
+    int i, k;
+    Vec_PtrClear( vNext );
+    Vec_PtrForEachEntry( Vec_Int_t *, vStart, pObj, i )
+    {
+        Abc_ObjForEachFanin( pObj, pNext, k )
+        {
+            if ( !Abc_ObjIsNode(pNext) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent( pNext ) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNext );
+            Vec_PtrPush( vNext, pNext );
+        }
+        Abc_ObjForEachFanout( pObj, pNext, k )
+        {
+            if ( !Abc_ObjIsNode(pNext) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent( pNext ) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pNext );
+            if ( Abc_ObjFanoutNum(pNext) > nFanMax )
+                continue;
+            Vec_PtrPush( vNext, pNext );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the circle of nodes removes from the given one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCollectNonOverlapCands( Abc_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Vec_Ptr_t * vTemp;
+    Abc_Obj_t * pObj;
+    int i, k;
+    Vec_PtrClear( vCands );
+    if ( pPars->nMaxSuppSize - Abc_ObjFaninNum(pLut) <= 1 )
+        return;
+
+    // collect nodes removed by this distance
+    assert( pPars->nMaxDistance > 0 );
+    Vec_PtrClear( vStart );
+    Vec_PtrPush( vStart, pLut );
+    Abc_NtkIncrementTravId( pLut->pNtk );
+    Abc_NodeSetTravIdCurrent( pLut );
+    for ( i = 1; i <= pPars->nMaxDistance; i++ )
+    {
+        Abc_NtkCollectCircle( vStart, vNext, pPars->nMaxFanout );
+        vTemp  = vStart;
+        vStart = vNext;
+        vNext  = vTemp;
+        // collect the nodes in vStart
+        Vec_PtrForEachEntry( Vec_Int_t *, vStart, pObj, k )
+            Vec_PtrPush( vCands, pObj );
+    }
+
+    // mark the TFI/TFO nodes
+    Abc_NtkIncrementTravId( pLut->pNtk );
+    if ( pPars->fUseTfiTfo )
+        Abc_NodeSetTravIdCurrent( pLut );
+    else
+    {
+        Abc_NodeSetTravIdPrevious( pLut );
+        Abc_NtkMarkFanins_rec( pLut, Abc_ObjLevel(pLut) - pPars->nMaxDistance );
+        Abc_NodeSetTravIdPrevious( pLut );
+        Abc_NtkMarkFanouts_rec( pLut, Abc_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout );
+    }
+
+    // collect nodes satisfying the following conditions:
+    // - they are close enough in terms of distance
+    // - they are not in the TFI/TFO of the LUT
+    // - they have no more than the given number of fanins
+    // - they have no more than the given diff in delay
+    k = 0;
+    Vec_PtrForEachEntry( Vec_Int_t *, vCands, pObj, i )
+    {
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            continue;
+        if ( Abc_ObjFaninNum(pLut) + Abc_ObjFaninNum(pObj) > pPars->nMaxSuppSize )
+            continue;
+        if ( Abc_ObjLevel(pLut) - Abc_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+             Abc_ObjLevel(pObj) - Abc_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+             continue;
+        Vec_PtrWriteEntry( vCands, k++, pObj );
+    }
+    Vec_PtrShrink( vCands, k );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Count the total number of fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountTotalFanins( Abc_Obj_t * pLut, Abc_Obj_t * pCand )
+{
+    Abc_Obj_t * pFanin;
+    int i, nCounter = Abc_ObjFaninNum(pLut);
+    Abc_ObjForEachFanin( pCand, pFanin, i )
+        nCounter += !pFanin->fMarkC;
+    return nCounter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects overlapping candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCollectOverlapCands( Abc_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+    Abc_Obj_t * pFanin, * pObj;
+    int i, k;
+    // mark fanins of pLut
+    Abc_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->fMarkC = 1;
+    // collect the matching fanouts of each fanin of the node
+    Vec_PtrClear( vCands );
+    Abc_NtkIncrementTravId( pLut->pNtk );
+    Abc_NodeSetTravIdCurrent( pLut );
+    Abc_ObjForEachFanin( pLut, pFanin, i )
+    {
+        if ( !Abc_ObjIsNode(pFanin) )
+            continue;
+        if ( Abc_ObjFanoutNum(pFanin) > pPars->nMaxFanout )
+            continue;
+        Abc_ObjForEachFanout( pFanin, pObj, k )
+        {
+            if ( !Abc_ObjIsNode(pObj) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent( pObj ) )
+                continue;
+            Abc_NodeSetTravIdCurrent( pObj );
+            // check the difference in delay
+            if ( Abc_ObjLevel(pLut) - Abc_ObjLevel(pObj) > pPars->nMaxLevelDiff || 
+                 Abc_ObjLevel(pObj) - Abc_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+                 continue;
+            // check the total number of fanins of the node
+            if ( Abc_NtkCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize )
+                continue;
+            Vec_PtrPush( vCands, pObj );
+        }
+    }
+    // unmark fanins of pLut
+    Abc_ObjForEachFanin( pLut, pFanin, i )
+        pFanin->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs LUT merging with parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
+{
+    Nwk_Grf_t * p;
+    Vec_Int_t * vResult;
+    Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
+    Abc_Obj_t * pLut, * pCand;
+    int i, k, nVertsMax, nCands, clk = clock();
+    // count the number of vertices
+    nVertsMax = 0;
+    Abc_NtkForEachNode( pNtk, pLut, i )
+        nVertsMax += (int)(Abc_ObjFaninNum(pLut) <= pPars->nMaxLutSize);
+    p = Nwk_ManGraphAlloc( nVertsMax );
+    // create graph
+    vStart  = Vec_PtrAlloc( 1000 );
+    vNext   = Vec_PtrAlloc( 1000 );
+    vCands1 = Vec_PtrAlloc( 1000 );
+    vCands2 = Vec_PtrAlloc( 1000 );
+    nCands  = 0;
+    Abc_NtkForEachNode( pNtk, pLut, i )
+    {
+        if ( Abc_ObjFaninNum(pLut) > pPars->nMaxLutSize )
+            continue;
+        Abc_NtkCollectOverlapCands( pLut, vCands1, pPars );
+        if ( pPars->fUseDiffSupp )
+            Abc_NtkCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars );
+        if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 )
+            continue;
+        nCands += Vec_PtrSize(vCands1) + Vec_PtrSize(vCands2);
+        // save candidates
+        Vec_PtrForEachEntry( Vec_Int_t *, vCands1, pCand, k )
+            Nwk_ManGraphHashEdge( p, Abc_ObjId(pLut), Abc_ObjId(pCand) );
+        Vec_PtrForEachEntry( Vec_Int_t *, vCands2, pCand, k )
+            Nwk_ManGraphHashEdge( p, Abc_ObjId(pLut), Abc_ObjId(pCand) );
+        // print statistics about this node
+        if ( pPars->fVeryVerbose )
+        printf( "Node %6d : Fanins = %d. Fanouts = %3d.  Cand1 = %3d. Cand2 = %3d.\n",
+            Abc_ObjId(pLut), Abc_ObjFaninNum(pLut), Abc_ObjFaninNum(pLut), 
+            Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) );
+    }
+    Vec_PtrFree( vStart );
+    Vec_PtrFree( vNext );
+    Vec_PtrFree( vCands1 );
+    Vec_PtrFree( vCands2 );
+    if ( pPars->fVerbose )
+    {
+        printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
+        ABC_PRT( "Deriving graph", clock() - clk );
+    }
+    // solve the graph problem
+    clk = clock();
+    Nwk_ManGraphSolve( p );
+    if ( pPars->fVerbose )
+    {
+        printf( "GRAPH: Nodes = %6d. Edges = %6d.  Pairs = %6d.  ", 
+            p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+        ABC_PRT( "Solving", clock() - clk );
+        Nwk_ManGraphReportMemoryUsage( p );
+    }
+    vResult = p->vPairs; p->vPairs = NULL;
+/*
+    for ( i = 0; i < vResult->nSize; i += 2 )
+        printf( "(%d,%d) ", vResult->pArray[i], vResult->pArray[i+1] );
+    printf( "\n" );
+*/
+    Nwk_ManGraphFree( p );
+    return vResult;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 965e0258..8b2ef27b 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -1,5 +1,4 @@
 SRC +=    src/base/abci/abc.c \
-    src/base/abci/abcAbc8.c \
     src/base/abci/abcAttach.c \
     src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \