Version abc80327

9 files changed, 239 insertions, 178 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1d5195c7..7dce5154 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -582,6 +582,7 @@ extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
+extern Vec_Vec_t *        Abc_NtkLevelize( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLevel( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
@@ -612,7 +613,6 @@ extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern unsigned *         Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst );
 extern int                Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern int                Abc_NtkToBdd( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 4c6a7fb0..c82faa15 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -978,6 +978,32 @@ int Abc_NtkLevelReverse_rec( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, i;
+    nLevels = Abc_NtkLevel( pNtk );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        assert( (int)pObj->Level <= nLevels );
+        Vec_VecPush( vLevels, pObj->Level, pObj );
+    }
+    return vLevels;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the number of logic levels not counting PIs/POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkLevel( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index f3297d8f..e99cc88b 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -785,159 +785,6 @@ DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot )
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Construct BDDs and mark AIG nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_ConvertAigToTruth_rec1( Hop_Obj_t * pObj )
-{
-    int Counter = 0;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return 0;
-    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin0(pObj) ); 
-    Counter += Abc_ConvertAigToTruth_rec1( Hop_ObjFanin1(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-    return Counter + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes truth table of the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_ConvertAigToTruth_rec2( Hop_Obj_t * pObj, Vec_Int_t * vTruth, int nWords )
-{
-    unsigned * pTruth, * pTruth0, * pTruth1;
-    int i;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
-        return pObj->pData;
-    // compute the truth tables of the fanins
-    pTruth0 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin0(pObj), vTruth, nWords );
-    pTruth1 = Abc_ConvertAigToTruth_rec2( Hop_ObjFanin1(pObj), vTruth, nWords );
-    // creat the truth table of the node
-    pTruth  = Vec_IntFetch( vTruth, nWords );
-    if ( Hop_ObjIsExor(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] ^ pTruth1[i];
-    else if ( !Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] & pTruth1[i];
-    else if ( !Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = pTruth0[i] & ~pTruth1[i];
-    else if ( Hop_ObjFaninC0(pObj) && !Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = ~pTruth0[i] & pTruth1[i];
-    else // if ( Hop_ObjFaninC0(pObj) && Hop_ObjFaninC1(pObj) )
-        for ( i = 0; i < nWords; i++ )
-            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
-    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjClearMarkA( pObj );
-    pObj->pData = pTruth;
-    return pTruth;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes truth table of the node.]
-
-  Description [Assumes that the structural support is no more than 8 inputs.
-  Uses array vTruth to store temporary truth tables. The returned pointer should 
-  be used immediately.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Abc_ConvertAigToTruth( Hop_Man_t * p, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, int fMsbFirst )
-{
-    static unsigned uTruths[8][8] = { // elementary truth tables
-        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
-        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
-        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
-        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
-        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
-        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
-        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
-        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
-    };
-    Hop_Obj_t * pObj;
-    unsigned * pTruth, * pTruth2;
-    int i, nWords, nNodes;
-    Vec_Ptr_t * vTtElems;
-
-    // if the number of variables is more than 8, allocate truth tables
-    if ( nVars > 8 )
-        vTtElems = Vec_PtrAllocTruthTables( nVars );
-    else
-        vTtElems = NULL;
-
-    // clear the data fields and set marks
-    nNodes = Abc_ConvertAigToTruth_rec1( pRoot );
-    // prepare memory
-    nWords = Hop_TruthWordNum( nVars );
-    Vec_IntClear( vTruth );
-    Vec_IntGrow( vTruth, nWords * (nNodes+1) );
-    pTruth = Vec_IntFetch( vTruth, nWords );
-    // check the case of a constant
-    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
-    {
-        assert( nNodes == 0 );
-        if ( Hop_IsComplement(pRoot) )
-            Extra_TruthClear( pTruth, nVars );
-        else
-            Extra_TruthFill( pTruth, nVars );
-        return pTruth;
-    }
-    // set elementary truth tables at the leaves
-    assert( nVars <= Hop_ManPiNum(p) );
-//    assert( Hop_ManPiNum(p) <= 8 ); 
-    if ( fMsbFirst )
-    {
-        Hop_ManForEachPi( p, pObj, i )
-        {
-            if ( vTtElems )
-                pObj->pData = Vec_PtrEntry(vTtElems, nVars-1-i);
-            else               
-                pObj->pData = (void *)uTruths[nVars-1-i];
-        }
-    }
-    else
-    {
-        Hop_ManForEachPi( p, pObj, i )
-        {
-            if ( vTtElems )
-                pObj->pData = Vec_PtrEntry(vTtElems, i);
-            else               
-                pObj->pData = (void *)uTruths[i];
-        }
-    }
-    // clear the marks and compute the truth table
-    pTruth2 = Abc_ConvertAigToTruth_rec2( pRoot, vTruth, nWords );
-    // copy the result
-    Extra_TruthCopy( pTruth, pTruth2, nVars );
-    if ( vTtElems )
-        Vec_PtrFree( vTtElems );
-    return pTruth;
-}
-
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d9c68bc4..65403609 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -205,6 +205,8 @@ static int Abc_CommandAbc8Write      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Ps         ( 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_CommandAbc8ReadLut    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8PrintLut   ( 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 );
@@ -431,6 +433,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*ps",           Abc_CommandAbc8Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*if",           Abc_CommandAbc8If,           0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*dchoice",      Abc_CommandAbc8DChoice,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*read_lut",     Abc_CommandAbc8ReadLut,      0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*print_lut",    Abc_CommandAbc8PrintLut,     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 );
@@ -473,6 +477,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
 void Abc_End()
 {
     Abc_FrameClearDesign(); 
+    {
+        extern void If_LutLibFree( void * pLutLib );
+        if ( Abc_FrameGetGlobalFrame()->pAbc8Lib )
+            If_LutLibFree( Abc_FrameGetGlobalFrame()->pAbc8Lib );
+    }
 
 //    Dar_LibDumpPriorities();
     {
@@ -1754,7 +1763,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Currently works only for up to 16 inputs.\n" );
             return 1;
         }
-        pTruth = Abc_ConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManFunc, Hop_Regular(pObj->pData), Abc_ObjFaninNum(pObj), vMemory, 0 );
         if ( Hop_IsComplement(pObj->pData) )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
         Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
@@ -3387,7 +3396,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nDivMax      =  250;
     pPars->nWinSizeMax  =  300;
     pPars->nGrowthLevel =    0;
-    pPars->nBTLimit     =10000;
+    pPars->nBTLimit     = 5000;
     pPars->fResub       =    1;
     pPars->fArea        =    0;
     pPars->fMoreEffort  =    0;
@@ -7073,7 +7082,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+//    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 
@@ -8111,10 +8120,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int fBalance, fVerbose, fUpdateLevel, c;
+    int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
     int nConfMax, nLevelMax;
 
-    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -8123,11 +8132,12 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fBalance     = 1;
     fUpdateLevel = 1;
+    fConstruct   = 0;
     nConfMax     = 1000;
     nLevelMax    = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8159,6 +8169,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fUpdateLevel ^= 1;
             break;
+        case 'c':
+            fConstruct ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8178,7 +8191,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command works only for strashed networks.\n" );
         return 1;
     }
-    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
+    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8189,12 +8202,13 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" );
+    fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blcvh]\n" );
     fprintf( pErr, "\t         performs partitioned choicing using a new AIG package\n" );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
     fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -14751,6 +14765,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     int c;
     extern void Ioa_WriteBlif( void * p, char * pFileName );
+    extern int Ntl_ManInsertNtk( void * p, void * pNtk );
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -14772,6 +14787,17 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the input file name
     pFileName = argv[globalUtilOptind];
+    if ( pAbc->pAbc8Ntk != NULL )
+    {
+        if ( !Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Ntk ) )
+        {
+            printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
+            return 1;
+        }
+        printf( "Writing the mapped design.\n" );
+    }
+    else
+        printf( "Writing the original design.\n" );
     Ioa_WriteBlif( pAbc->pAbc8Ntl, pFileName );
     return 0;
 
@@ -14797,6 +14823,7 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
     extern void Ntl_ManPrintStats( void * p );
+    extern void Ntk_ManPrintStats( void * p, void * pLutLib );
 
     // set defaults
     Extra_UtilGetoptReset();
@@ -14821,6 +14848,8 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         Ntl_ManPrintStats( pAbc->pAbc8Ntl );
     if ( pAbc->pAbc8Aig )
         Aig_ManPrintStats( pAbc->pAbc8Aig );
+    if ( pAbc->pAbc8Ntk )
+        Ntk_ManPrintStats( pAbc->pAbc8Ntk, pAbc->pAbc8Lib );
     return 0;
 
 usage:
@@ -14843,11 +14872,26 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    If_Par_t Pars, * pPars = &Pars;
+    void * pNtkNew;
     int c;
     extern int Ntl_ManInsertTest( void * p, Aig_Man_t * pAig );
     extern int Ntl_ManInsertTestIf( void * p, Aig_Man_t * pAig );
+    extern void * Ntk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
+    extern Tim_Man_t * Ntl_ManReadTimeMan( void * p );
+    extern void * If_SetSimpleLutLib( int nLutSize );
+    extern void Ntk_ManSetIfParsDefault( If_Par_t * pPars );
+    extern void Ntk_ManFree( void * );
+
+    if ( pAbc->pAbc8Lib == NULL )
+    {
+        printf( "LUT library is not given. Using defaul 6-LUT library.\n" );
+        pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
+    }
 
     // set defaults
+    Ntk_ManSetIfParsDefault( pPars );
+    pPars->pLutLib = pAbc->pAbc8Lib;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
     {
@@ -14864,7 +14908,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Write(): There is no AIG to map.\n" );
         return 1;
     }
-
+/*
     // get the input file name
     if ( !Ntl_ManInsertTestIf( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
 //    if ( !Ntl_ManInsertTest( pAbc->pAbc8Ntl, pAbc->pAbc8Aig ) )
@@ -14872,6 +14916,16 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Write(): Tranformation of the netlist has failed.\n" );
         return 1;
     }
+*/
+    pNtkNew = Ntk_MappingIf( pAbc->pAbc8Aig, Ntl_ManReadTimeMan(pAbc->pAbc8Ntl), pPars );
+    if ( pNtkNew == NULL )
+    {
+        printf( "Abc_CommandAbc8If(): Mapping of the AIG has failed.\n" );
+        return 1;
+    }
+    if ( pAbc->pAbc8Ntk != NULL )
+        Ntk_ManFree( pAbc->pAbc8Ntk );
+    pAbc->pAbc8Ntk = pNtkNew;
     return 0;
 
 usage:
@@ -14937,6 +14991,138 @@ usage:
 
 /**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;
+    void * pLib;
+    int c;
+    extern void * If_LutLibRead( char * FileName );
+    extern void If_LutLibFree( void * 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 )
+    {
+        fprintf( stdout, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".lut", NULL, NULL, NULL, NULL ) )
+            fprintf( stdout, "Did you mean \"%s\"?", FileName );
+        fprintf( stdout, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pLib = If_LutLibRead( FileName );
+    if ( pLib == NULL )
+    {
+        fprintf( stdout, "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:
+    fprintf( stdout, "\nusage: *read_lut [-h]\n");
+    fprintf( stdout, "\t          read the LUT library from the file\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    fprintf( stdout, "\t                                        \n");
+    fprintf( stdout, "\t          File format for a LUT library:\n");
+    fprintf( stdout, "\t          (the default library is shown)\n");
+    fprintf( stdout, "\t                                        \n");
+    fprintf( stdout, "\t          # The area/delay of k-variable LUTs:\n");
+    fprintf( stdout, "\t          # k  area   delay\n");
+    fprintf( stdout, "\t          1      1      1\n");
+    fprintf( stdout, "\t          2      2      2\n");
+    fprintf( stdout, "\t          3      4      3\n");
+    fprintf( stdout, "\t          4      8      4\n");
+    fprintf( stdout, "\t          5     16      5\n");
+    fprintf( stdout, "\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( void * 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 )
+        printf( "LUT library is not specified.\n" );
+    else
+        If_LutLibPrint( pAbc->pAbc8Lib );
+    return 0;
+
+usage:
+    fprintf( stdout, "\nusage: *print_lut [-h]\n");
+    fprintf( stdout, "\t          print the current LUT library\n" );  
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;       /* error exit */
+}
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index ad332314..bb114578 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -19,15 +19,13 @@
 ***********************************************************************/
 
 #include "abc.h"
-
 #include "bdc.h"
-#include "bdcInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -48,24 +46,25 @@ Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pR
 {
     unsigned * pTruth;
     Bdc_Fun_t * pFunc;
-    int i;
+    int nNodes, i;
     assert( nVars <= 16 );
     // derive truth table
-    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
     if ( Hop_IsComplement(pRoot) )
         Extra_TruthNot( pTruth, pTruth, nVars );
     // decompose truth table
     Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
     // convert back into HOP
-    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+    Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
     for ( i = 0; i < nVars; i++ )
-        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
-    for ( i = nVars + 1; i < p->nNodes; i++ )
+        Bdc_FuncSetCopy( Bdc_ManFunc( p, i+1 ), Hop_ManPi( pHop, i ) );
+    nNodes = Bdc_ManNodeNum(p);
+    for ( i = nVars + 1; i < nNodes; i++ )
     {
-        pFunc = Bdc_FunWithId( p, i );
-        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+        pFunc = Bdc_ManFunc( p, i );
+        Bdc_FuncSetCopy( pFunc, Hop_And( pHop, Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
     }
-    return Bdc_FunCopyHop(p->pRoot);
+    return Bdc_FunCopyHop( Bdc_ManRoot(p) );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 94b6c52b..dd8f8221 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -769,7 +769,7 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
@@ -777,7 +777,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
     pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
+    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
     Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
     Aig_ManStop( pMan );
@@ -1432,6 +1432,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
 ***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
+/*
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 1 );
     if ( pMan == NULL )
@@ -1442,6 +1443,7 @@ void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
     pMan->vFlopNums = NULL;
     Aig_ManHaigRecord( pMan );
     Aig_ManStop( pMan );
+*/
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 744d9c95..c1e0faf0 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -383,7 +383,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
         extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
         int nVars = Abc_NtkRecVarNum();
         Vec_Int_t * vMemory = Abc_NtkRecMemory();
-        unsigned * pTruth = Abc_ConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
+        unsigned * pTruth = Hop_ManConvertAigToTruth( pMan, Hop_Regular(pRoot), nVars, vMemory, 0 );
         assert( Extra_TruthSupportSize(pTruth, nVars) == Abc_ObjFaninNum(pNodeOld) ); // should be swept
         if ( Hop_IsComplement(pRoot) )
             Extra_TruthNot( pTruth, pTruth, nVars );
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index 4b766a47..df4a6259 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -258,7 +258,7 @@ int Io_WriteBenchLutOneNode( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vTruth
     nFanins = Abc_ObjFaninNum(pNode);
     assert( nFanins <= 8 );
     // compute the truth table
-    pTruth = Abc_ConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
+    pTruth = Hop_ManConvertAigToTruth( pNode->pNtk->pManFunc, Hop_Regular(pNode->pData), nFanins, vTruth, 0 );
     if ( Hop_IsComplement(pNode->pData) )
         Extra_TruthNot( pTruth, pTruth, nFanins );
     // consider simple cases
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 0261d7da..7196b952 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -78,6 +78,7 @@ struct Abc_Frame_t_
     void *          pAbc8Ntl;    // the current design
     void *          pAbc8Ntk;    // the current mapped network
     void *          pAbc8Aig;    // the current AIG
+    void *          pAbc8Lib;    // the current LUT library
 };
 
 ////////////////////////////////////////////////////////////////////////