Improvements to LMS code.

src/aig/gia/gia.h

@@ -482,6 +482,13 @@ static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 )
 { 
     return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 );
 }
+static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 )  
+{
+    Gia_Obj_t * pObjCo  = Gia_ManCo( p, iCoIndex );
+    assert( Gia_ObjId(p, pObjCo) > Abc_Lit2Var(iLit0) );
+    pObjCo->iDiff0  = Gia_ObjId(p, pObjCo) - Abc_Lit2Var(iLit0);
+    pObjCo->fCompl0 = Abc_LitIsCompl(iLit0);
+}
 
 #define GIA_ZER 1
 #define GIA_ONE 2
@@ -863,6 +870,7 @@ extern int                 Sat_ManTest( Gia_Man_t * pGia, Gia_Obj_t * pObj, int
 extern int                 Gia_ManSeqMarkUsed( Gia_Man_t * p );
 extern int                 Gia_ManCombMarkUsed( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManCleanup( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs );
 extern Gia_Man_t *         Gia_ManSeqCleanup( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
 /*=== giaShrink.c ===========================================================*/

src/aig/gia/giaScl.c

@@ -94,6 +94,32 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
     return Gia_ManDupMarked( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Skip the first outputs during cleanup.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( nOutputs < Gia_ManCoNum(p) );
+    Gia_ManCombMarkUsed( p );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( i < nOutputs )
+            pObj->fMark0 = 1;
+        else
+            break;
+    return Gia_ManDupMarked( p );
+}
+
 
 /**Function*************************************************************
 

src/base/abc/abc.h

@@ -789,7 +789,7 @@ extern ABC_DLL int                Abc_NtkRecVarNum();
 extern ABC_DLL Vec_Int_t *        Abc_NtkRecMemory();
 extern ABC_DLL int                Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
 /*=== abcRec2.c ==========================================================*/
-extern ABC_DLL void               Abc_NtkRecStart2( Gia_Man_t *p, int nVars, int nCuts, int fTrim );
+extern ABC_DLL void               Abc_NtkRecStart2( Gia_Man_t * p, int nVars, int nCuts, int fTrim );
 extern ABC_DLL void               Abc_NtkRecStop2();
 extern ABC_DLL void               Abc_NtkRecAdd2( Abc_Ntk_t * pNtk, int fUseSOPB );
 extern ABC_DLL void               Abc_NtkRecPs2(int fPrintLib);
@@ -799,7 +799,7 @@ extern ABC_DLL int                Abc_NtkRecIsRunning2();
 extern ABC_DLL int                Abc_NtkRecIsInTrimMode2();
 extern ABC_DLL void               Abc_NtkRecFilter2(int nLimit);
 /*=== abcRec3.c ==========================================================*/
-extern ABC_DLL void               Abc_NtkRecStart3( Gia_Man_t *p, int nVars, int nCuts, int fTrim );
+extern ABC_DLL void               Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose );
 extern ABC_DLL void               Abc_NtkRecStop3();
 extern ABC_DLL void               Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB );
 extern ABC_DLL void               Abc_NtkRecPs3(int fPrintLib);

src/base/abci/abc.c

@@ -13056,9 +13056,10 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pGia = NULL;
     int nVars = 6;
     int nCuts = 32;
-    int fTrim = 0;
+    int fFuncOnly = 0;
+    int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCth" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13084,8 +13085,11 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCuts < 1 ) 
                 goto usage;
             break;
-        case 't':
-            fTrim ^= 1;
+        case 'f':
+            fFuncOnly ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -13131,16 +13135,17 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
     }
-    Abc_NtkRecStart3( pGia, nVars, nCuts, fTrim );
+    Abc_NtkRecStart3( pGia, nVars, nCuts, fFuncOnly, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: rec_start3 [-K num] [-C num] [-th]\n" );
+    Abc_Print( -2, "usage: rec_start3 [-K num] [-C num] [-fvh]\n" );
     Abc_Print( -2, "\t         starts recording AIG subgraphs (should be called for\n" );
     Abc_Print( -2, "\t         an empty network or after reading in a previous record)\n" );
     Abc_Print( -2, "\t-K num : the largest number of inputs [default = %d]\n", nVars );
     Abc_Print( -2, "\t-C num : the max number of cuts used at a node (0 < num < 2^12) [default = %d]\n", nCuts );
-    Abc_Print( -2, "\t-t     : toggles the use of trimming [default = %s]\n", fTrim? "yes": "no" );
+    Abc_Print( -2, "\t-f     : toggles recording functions without AIG subgraphs [default = %s]\n", fFuncOnly? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }

src/base/abci/abcRec3.c

@@ -31,6 +31,16 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+/*
+    This LMS manager can be used in two modes:
+    - library constuction
+    - AIG level minimization
+
+    It is not OK to switch from library construction to AIG level minimization
+    without restarting LSM manager.  To restart the LSM manager, GIA has to be written out 
+    (rec_dump3 <file>.aig) and LMS manager started again (rec_start3 <file>.aig).
+*/
+
 typedef struct Lms_Man_t_ Lms_Man_t;
 struct Lms_Man_t_
 {
@@ -39,18 +49,19 @@ struct Lms_Man_t_
     int               nWords;       // the number of TT words
     int               nCuts;        // the max number of cuts to use
     int               fFuncOnly;    // record only functions
-    // internal data
+    int               fLibConstr;   // this manager is used for library construction
+    // internal data for library construction
     Gia_Man_t *       pGia;         // the record
-    Vec_Mem_t *       vTtMem;       // truth tables of primary outputs
-//    Vec_Int_t *       vTruthPo;     // for each semi-canonical class, first PO where this truth table was seen
-    // subgraph attributes (1-to-1 correspondence with POs of Gia)
-    Vec_Int_t *       vTruthIds;    // truth table IDs of this PO
-    Vec_Wrd_t *       vDelays;      // pin-to-pin delays of this PO
-    Vec_Str_t *       vCosts;       // number of AND gates in this PO
-    // sugraph usage statistics
-//    Vec_Int_t *       vFreqs;       // frequencies
+    Vec_Mem_t *       vTtMem;       // truth table memory and hash table
+    Vec_Int_t *       vTruthIds;    // truth table IDs of each PO
+    // internal data for AIG level minimization (allocated the first time it is called)
+    Vec_Int_t *       vTruthPo;     // first PO where this canonicized truth table was seen
+    Vec_Wrd_t *       vDelays;      // pin-to-pin delays of each PO
+    Vec_Str_t *       vAreas;       // number of AND gates in each PO
+    Vec_Int_t *       vFreqs;       // subgraph usage frequencies
     // temporaries
     Vec_Ptr_t *       vNodes;       // the temporary nodes
+    Vec_Ptr_t *       vLabelsP;     // temporary storage for HOP node labels
     Vec_Int_t *       vLabels;      // temporary storage for AIG node labels
     word              pTemp1[1024]; // copy of the truth table
     word              pTemp2[1024]; // copy of the truth table
@@ -64,6 +75,7 @@ struct Lms_Man_t_
     int               nFilterSame;
     int               nAdded;
     int               nAddedFuncs;
+    int               nHoleInTheWall;
     // runtime
     clock_t           timeCollect;
     clock_t           timeCanon;
@@ -72,9 +84,11 @@ struct Lms_Man_t_
     clock_t           timeInsert;
     clock_t           timeOther;
     clock_t           timeTotal;
+
+    clock_t           timeDerive;
 };
 
-static Lms_Man_t * s_pMan = NULL;
+static Lms_Man_t * s_pMan3 = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -91,75 +105,98 @@ static Lms_Man_t * s_pMan = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRecIsRunning3()
-{
-    return s_pMan != NULL;
-}
-Gia_Man_t * Abc_NtkRecGetGia3()
-{
-    return s_pMan->pGia;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Lms_Man_t * Lms_ManStart( int nVars, int nCuts, int fFuncOnly, int fVerbose )
+Lms_Man_t * Lms_ManStart( Gia_Man_t * pGia, int nVars, int nCuts, int fFuncOnly, int fVerbose )
 {
     Lms_Man_t * p;
-    int i;
+    // if GIA is given, use the number of variables from GIA
+    nVars = pGia ? Gia_ManCiNum(pGia) : nVars;
+    assert( nVars >= 6 && nVars <= 16 );
+    // allocate manager
     p = ABC_CALLOC( Lms_Man_t, 1 );
     // parameters
     p->nVars = nVars;
     p->nCuts = nCuts;
     p->nWords = Abc_Truth6WordNum( nVars );
     p->fFuncOnly = fFuncOnly;
-    // GIA
-    p->pGia = Gia_ManStart( 10000 );
-    p->pGia->pName = Abc_UtilStrsav( "record" );
-    for ( i = 0; i < nVars; i++ )
-        Gia_ManAppendCi( p->pGia );
-    // truth tables
+    // internal data for library construction
     p->vTtMem = Vec_MemAlloc( p->nWords, 12 ); // 32 KB/page for 6-var functions
     Vec_MemHashAlloc( p->vTtMem, 10000 );
-//    p->vTruthPo  = Vec_IntAlloc( 1000 );
-    // subgraph attributes
-    p->vTruthIds = Vec_IntAlloc( 1000 );
-    p->vDelays   = Vec_WrdAlloc( 1000 );
-    p->vCosts    = Vec_StrAlloc( 1000 );
-    // sugraph usage statistics
-//    p->vFreqs    = Vec_IntAlloc( 1000 );
+    p->vTruthIds = Vec_IntAlloc( 10000 );
+    if ( pGia == NULL )
+    {
+        int i;
+        p->pGia = Gia_ManStart( 10000 );
+        p->pGia->pName = Abc_UtilStrsav( "record" );
+        for ( i = 0; i < nVars; i++ )
+            Gia_ManAppendCi( p->pGia );
+    }
+    else
+    {
+        Gia_Obj_t * pObj;
+        unsigned * pTruth;
+        int i, Index, Prev = -1;
+        p->pGia = pGia;
+        // populate the manager with subgraphs present in GIA
+        p->nAdded = Gia_ManCoNum( p->pGia );
+        Gia_ManForEachCo( p->pGia, pObj, i )
+        {
+            pTruth = Gia_ObjComputeTruthTable( p->pGia, pObj );
+            Index = Vec_MemHashInsert( p->vTtMem, (word *)pTruth );
+            assert( Index == Prev || Index == Prev + 1 ); // GIA subgraphs should be ordered
+            Vec_IntPush( p->vTruthIds, Index );
+            Prev = Index;
+        }
+    }
     // temporaries
     p->vNodes    = Vec_PtrAlloc( 1000 );
+    p->vLabelsP  = Vec_PtrAlloc( 1000 );
     p->vLabels   = Vec_IntAlloc( 1000 );
     return p;    
 }
 void Lms_ManStop( Lms_Man_t * p )
 {
     // temporaries
-    Vec_IntFree( p->vLabels );
-    Vec_PtrFree( p->vNodes );
-    // subgraph attributes
-    Vec_WrdFree( p->vDelays );
-    Vec_StrFree( p->vCosts );
-//    Vec_IntFree( p->vTruthPo );
-    // sugraph usage statistics
-//    Vec_IntFree( p->vFreqs );
-    // truth tables
-    Vec_IntFree( p->vTruthIds );
+    Vec_IntFreeP( &p->vLabels );
+    Vec_PtrFreeP( &p->vLabelsP );
+    Vec_PtrFreeP( &p->vNodes );
+    // internal data for AIG level minimization
+    Vec_IntFreeP( &p->vTruthPo );
+    Vec_WrdFreeP( &p->vDelays );
+    Vec_StrFreeP( &p->vAreas );
+    Vec_IntFreeP( &p->vFreqs );
+    // internal data for library construction
+    Vec_IntFreeP( &p->vTruthIds );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFree( p->vTtMem );
-    // GIA
     Gia_ManStop( p->pGia );
     ABC_FREE( p );
 }
+void Lms_ManPrint( Lms_Man_t * p )
+{
+//    Gia_ManPrintStats( p->pGia, 0, 0 );
+    printf( "The record has %d classes containing %d AIG subgraphs with %d AND nodes.\n", Vec_MemEntryNum(p->vTtMem), p->nAdded, Gia_ManAndNum(p->pGia) );
+
+    p->nAddedFuncs = Vec_MemEntryNum(p->vTtMem);
+    printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,         !p->nTried? 0 : 100.0*p->nTried/p->nTried );
+    printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,    !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
+    printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund,  !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
+    printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume,  !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
+    printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,   !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
+    printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,   !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
+    printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,    !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
+    printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,         !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
+    printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,    !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
+    printf( "Cuts whose logic structure has a hole       = %10d. (%6.2f %%)\n", p->nHoleInTheWall, !p->nTried? 0 : 100.0*p->nHoleInTheWall/p->nTried );
+
+    p->timeOther = p->timeTotal - p->timeCollect - p->timeCanon - p->timeBuild - p->timeCheck - p->timeInsert;
+    ABC_PRTP( "Runtime: Collect", p->timeCollect, p->timeTotal );
+    ABC_PRTP( "Runtime: Canon  ", p->timeCanon,   p->timeTotal );
+    ABC_PRTP( "Runtime: Build  ", p->timeBuild,   p->timeTotal );
+    ABC_PRTP( "Runtime: Check  ", p->timeCheck,   p->timeTotal );
+    ABC_PRTP( "Runtime: Insert ", p->timeInsert,  p->timeTotal );
+    ABC_PRTP( "Runtime: Other  ", p->timeOther,   p->timeTotal );
+    ABC_PRTP( "Runtime: TOTAL  ", p->timeTotal,   p->timeTotal );
+}
 
 
 /**Function*************************************************************
@@ -173,56 +210,205 @@ void Lms_ManStop( Lms_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fTrim )
+void Abc_NtkRecStart3( Gia_Man_t * p, int nVars, int nCuts, int fFuncOnly, int fVerbose )
 {
-    assert( s_pMan == NULL );
-    if ( p == NULL )
-        s_pMan = Lms_ManStart( nVars, nCuts, 0, 0 );
-    else
-        s_pMan = NULL;
+    assert( s_pMan3 == NULL );
+    s_pMan3 = Lms_ManStart( p, nVars, nCuts, fFuncOnly, fVerbose );
 }
 
 void Abc_NtkRecStop3()
 {
-    assert( s_pMan != NULL );
-    Lms_ManStop( s_pMan );
-    s_pMan = NULL;
+    assert( s_pMan3 != NULL );
+    Lms_ManStop( s_pMan3 );
+    s_pMan3 = NULL;
 }
 
-void Abc_NtkRecPs3(int fPrintLib)
+
+/**Function*************************************************************
+
+  Synopsis    [Compute delay/area profiles of POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int  Lms_DelayGet( word D, int v )           { assert(v >= 0 && v < 16); return (int)((D >> (v << 2)) & 0xF);                    }
+static inline void Lms_DelaySet( word * pD, int v, int d ) { assert(v >= 0 && v < 16); assert(d >= 0 && d < 16); *pD |= ((word)d << (v << 2)); }
+static inline word Lms_DelayInit( int v )                  { assert(v >= 0 && v < 16); return (word)1 << (v << 2);                             }
+static inline word Lms_DelayMax( word D1, word D2, int nVars )
+{
+    int v, Max;
+    word D = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( (Max = Abc_MaxInt(Lms_DelayGet(D1, v), Lms_DelayGet(D2, v))) )
+            Lms_DelaySet( &D, v, Abc_MinInt(Max + 1, 15) );
+    return D;
+}
+static inline word Lms_DelayDecrement( word D1, int nVars )
+{
+    int v;
+    word D = 0;
+    for ( v = 0; v < nVars; v++ )
+        if ( Lms_DelayGet(D1, v) )
+            Lms_DelaySet( &D, v, Lms_DelayGet(D1, v) - 1 );
+    return D;
+}
+static inline int Lms_DelayEqual( word D1, word D2, int nVars ) // returns 1 if D1 has the same delays than D2
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+        if ( Lms_DelayGet(D1, v) != Lms_DelayGet(D2, v) )
+            return 0;
+    return 1;
+}
+static inline int Lms_DelayDom( word D1, word D2, int nVars ) // returns 1 if D1 has the same or smaller delays than D2
+{
+    int v;
+    for ( v = 0; v < nVars; v++ )
+        if ( Lms_DelayGet(D1, v) > Lms_DelayGet(D2, v) )
+            return 0;
+    return 1;
+}
+static inline void Lms_DelayPrint( word D, int nVars )
+{
+    int v;
+    printf( "Delay profile = {" );
+    for ( v = 0; v < nVars; v++ )
+        printf( " %d", Lms_DelayGet(D, v) );
+    printf( " }\n" );
+}
+Vec_Wrd_t * Lms_GiaDelays( Gia_Man_t * p )
 {
-    Lms_Man_t * p = s_pMan;
-
-    printf( "Subgraphs tried                             = %10d. (%6.2f %%)\n", p->nTried,        !p->nTried? 0 : 100.0*p->nTried/p->nTried );
-    printf( "Subgraphs filtered by support size          = %10d. (%6.2f %%)\n", p->nFilterSize,   !p->nTried? 0 : 100.0*p->nFilterSize/p->nTried );
-    printf( "Subgraphs filtered by structural redundancy = %10d. (%6.2f %%)\n", p->nFilterRedund, !p->nTried? 0 : 100.0*p->nFilterRedund/p->nTried );
-    printf( "Subgraphs filtered by volume                = %10d. (%6.2f %%)\n", p->nFilterVolume, !p->nTried? 0 : 100.0*p->nFilterVolume/p->nTried );
-    printf( "Subgraphs filtered by TT redundancy         = %10d. (%6.2f %%)\n", p->nFilterTruth,  !p->nTried? 0 : 100.0*p->nFilterTruth/p->nTried );
-    printf( "Subgraphs filtered by error                 = %10d. (%6.2f %%)\n", p->nFilterError,  !p->nTried? 0 : 100.0*p->nFilterError/p->nTried );
-    printf( "Subgraphs filtered by isomorphism           = %10d. (%6.2f %%)\n", p->nFilterSame,   !p->nTried? 0 : 100.0*p->nFilterSame/p->nTried );
-    printf( "Subgraphs added                             = %10d. (%6.2f %%)\n", p->nAdded,        !p->nTried? 0 : 100.0*p->nAdded/p->nTried );
-    printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,   !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
-
-    p->timeOther = p->timeTotal 
-                        - p->timeCollect 
-                        - p->timeCanon
-                        - p->timeBuild
-                        - p->timeCheck
-                        - p->timeInsert;
+    Vec_Wrd_t * vDelays, * vResult;
+    Gia_Obj_t * pObj;
+    int i;
+    // compute delay profiles of all objects
+    vDelays = Vec_WrdAlloc( Gia_ManObjNum(p) );
+    Vec_WrdPush( vDelays, 0 ); // const 0
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            Vec_WrdPush( vDelays, Lms_DelayMax( Vec_WrdEntry(vDelays, Gia_ObjFaninId0(pObj, i)), Vec_WrdEntry(vDelays, Gia_ObjFaninId1(pObj, i)), Gia_ManCiNum(p) ) );
+        else if ( Gia_ObjIsCo(pObj) )
+            Vec_WrdPush( vDelays, Lms_DelayDecrement( Vec_WrdEntry(vDelays, Gia_ObjFaninId0(pObj, i)), Gia_ManCiNum(p) ) );
+        else if ( Gia_ObjIsCi(pObj) )
+            Vec_WrdPush( vDelays, Lms_DelayInit( Gia_ObjCioId(pObj) ) );
+        else assert( 0 );
+    }
+    // collect delay profiles of COs only
+    vResult = Vec_WrdAlloc( Gia_ManCoNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_WrdPush( vResult, Vec_WrdEntry(vDelays, Gia_ObjId(p, pObj)) );
+    Vec_WrdFree( vDelays );
+    return vResult;
+}
+void Lms_ObjAreaMark_rec( Gia_Obj_t * pObj )
+{
+    if ( pObj->fMark0 || Gia_ObjIsCi(pObj) )
+        return;
+    pObj->fMark0 = 1;
+    Lms_ObjAreaMark_rec( Gia_ObjFanin0(pObj) );
+    Lms_ObjAreaMark_rec( Gia_ObjFanin1(pObj) );
+}
+int  Lms_ObjAreaUnmark_rec( Gia_Obj_t * pObj )
+{
+    if ( !pObj->fMark0 || Gia_ObjIsCi(pObj) )
+        return 0;
+    pObj->fMark0 = 0;
+    return 1 + Lms_ObjAreaUnmark_rec( Gia_ObjFanin0(pObj) ) 
+             + Lms_ObjAreaUnmark_rec( Gia_ObjFanin1(pObj) );
+}
+int Lms_ObjArea( Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsAnd(pObj) );
+    Lms_ObjAreaMark_rec( pObj );
+    return Lms_ObjAreaUnmark_rec( pObj );    
+}
+Vec_Str_t * Lms_GiaAreas( Gia_Man_t * p )
+{
+    Vec_Str_t * vAreas;
+    Gia_Obj_t * pObj;
+    int i;
+    vAreas = Vec_StrAlloc( Gia_ManCoNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Vec_StrPush( vAreas, (char)(Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) ? Lms_ObjArea(Gia_ObjFanin0(pObj)) : 0) );
+    return vAreas;
+}
 
-    ABC_PRTP( "Runtime: Collect", p->timeCollect, p->timeTotal );
-    ABC_PRTP( "Runtime: Canon  ", p->timeCanon,   p->timeTotal );
-    ABC_PRTP( "Runtime: Build  ", p->timeBuild,   p->timeTotal );
-    ABC_PRTP( "Runtime: Check  ", p->timeCheck,   p->timeTotal );
-    ABC_PRTP( "Runtime: Insert ", p->timeInsert,  p->timeTotal );
-    ABC_PRTP( "Runtime: Other  ", p->timeOther,   p->timeTotal );
-    ABC_PRTP( "Runtime: TOTAL  ", p->timeTotal,   p->timeTotal );
+/**Function*************************************************************
+
+  Synopsis    [Prints one GIA subgraph.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Lms_GiaPrintSubgraph_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( !pObj->fMark0 || Gia_ObjIsCi(pObj) )
+        return;
+    pObj->fMark0 = 0;
+    assert( Gia_ObjIsAnd(pObj) );
+    Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin0(pObj) );
+    Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin1(pObj) );
+    Gia_ObjPrint( p, pObj );
 }
+void Lms_GiaPrintSubgraph( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsCo(pObj) );
+    if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
+    {
+        Lms_ObjAreaMark_rec( Gia_ObjFanin0(pObj) );
+        Lms_GiaPrintSubgraph_rec( p, Gia_ObjFanin0(pObj) ); 
+    }
+    else
+        Gia_ObjPrint( p, Gia_ObjFanin0(pObj) );
+    Gia_ObjPrint( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints delay/area profiles of the GIA subgraphs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Lms_GiaProfilesPrint( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Vec_Wrd_t * vDelays;
+    Vec_Str_t * vAreas;
+    vDelays = Lms_GiaDelays( p );
+    vAreas = Lms_GiaAreas( p );
+
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        printf( "%6d : ", i );
+        printf( "A = %2d  ", Vec_StrEntry(vAreas, i) );
+        Lms_DelayPrint( Vec_WrdEntry(vDelays, i), Gia_ManPiNum(p) );
+//        Lms_GiaPrintSubgraph( p, pObj );
+//        printf( "\n" );
+    }
 
+    Vec_WrdFree( vDelays );
+    Vec_StrFree( vAreas );
+    return NULL;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [stretch the truthtable to have more input variables.]
+  Synopsis    [Stretch truthtable to have more input variables.]
 
   Description []
                
@@ -231,7 +417,22 @@ void Abc_NtkRecPs3(int fPrintLib)
   SeeAlso     []
 
 ***********************************************************************/
-static void Abc_TtStretch( word * pInOut, int nVarS, int nVarB )
+static void Abc_TtStretch5( unsigned * pInOut, int nVarS, int nVarB )
+{
+    int w, i, step, nWords;
+    if ( nVarS == nVarB )
+        return;
+    assert( nVarS < nVarB );
+    step = Abc_TruthWordNum(nVarS);
+    nWords = Abc_TruthWordNum(nVarB);
+    if ( step == nWords )
+        return;
+    assert( step < nWords );
+    for ( w = 0; w < nWords; w += step )
+        for ( i = 0; i < step; i++ )
+            pInOut[w + i] = pInOut[i];              
+}
+static void Abc_TtStretch6( word * pInOut, int nVarS, int nVarB )
 {
     int w, i, step, nWords;
     if ( nVarS == nVarB )
@@ -250,7 +451,7 @@ static void Abc_TtStretch( word * pInOut, int nVarS, int nVarB )
 
 /**Function*************************************************************
 
-  Synopsis    [Adds the cut function to the internal storage.]
+  Synopsis    [Evaluates one cut during library construction.]
 
   Description []
                
@@ -261,120 +462,114 @@ static void Abc_TtStretch( word * pInOut, int nVarS, int nVarB )
 ***********************************************************************/
 int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
 {
+    Lms_Man_t * p = s_pMan3;
     char pCanonPerm[16];
     unsigned uCanonPhase;
-    int i, Index, iFanin0, iFanin1;
+    int i, Index, iFanin0, iFanin1, fHole;
     int nLeaves = If_CutLeaveNum(pCut);
-    Vec_Ptr_t * vNodes = s_pMan->vNodes;
-    Gia_Man_t * pGia = s_pMan->pGia;
+    Vec_Ptr_t * vNodes = p->vNodes;
+    Gia_Man_t * pGia = p->pGia;
     Gia_Obj_t * pDriver;
     If_Obj_t * pIfObj;
     unsigned * pTruth;
     clock_t clk;
-    s_pMan->nTried++;
+    p->nTried++;
 
     // skip small cuts
-    assert( s_pMan->nVars == (int)pCut->nLimit );
+    assert( p->nVars == (int)pCut->nLimit );
     if ( nLeaves < 2 )
     {
-        s_pMan->nFilterSize++;
+        p->nFilterSize++;
         return 1;
     }
 
     // collect internal nodes and skip redundant cuts
 clk = clock();
     If_CutTraverse( pIfMan, pRoot, pCut, vNodes );
-s_pMan->timeCollect += clock() - clk;
+p->timeCollect += clock() - clk;
 
     // semi-canonicize truth table
 clk = clock();
     for ( i = 0; i < Abc_MaxInt(nLeaves, 6); i++ )
         pCanonPerm[i] = i;
-    memcpy( s_pMan->pTemp1, If_CutTruthW(pCut), s_pMan->nWords * sizeof(word) );
-//    uCanonPhase = luckyCanonicizer_final_fast( s_pMan->pTemp1, nLeaves, pCanonPerm );
-    uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)s_pMan->pTemp1, (unsigned *)s_pMan->pTemp2, nLeaves, pCanonPerm );
-    if ( nLeaves < 6 )
-        s_pMan->pTemp1[0] = (s_pMan->pTemp1[0] & 0xFFFFFFFF) | (s_pMan->pTemp1[0] << 32);
-    Abc_TtStretch( If_CutTruthW(pCut), nLeaves, s_pMan->nVars );
-s_pMan->timeCanon += clock() - clk;
+    memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
+//    uCanonPhase = luckyCanonicizer_final_fast( p->pTemp1, nLeaves, pCanonPerm );
+    uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
+    Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
+p->timeCanon += clock() - clk;
     // pCanonPerm and uCanonPhase show what was the variable corresponding to each var in the current truth
 
 clk = clock();
     // map cut leaves into elementary variables of GIA
     for ( i = 0; i < nLeaves; i++ )
-    {
-//        printf( "Leaf  " );
-//        If_ObjPrint( If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] ) );
         If_ManObj( pIfMan, pCut->pLeaves[pCanonPerm[i]] )->iCopy = Abc_Var2Lit( Gia_ObjId(pGia, Gia_ManPi(pGia, i)), (uCanonPhase >> i) & 1 );
-    }
     // build internal nodes
-//    printf( "\n" );
+    fHole = 0;
     assert( Vec_PtrSize(vNodes) > 0 );
     Vec_PtrForEachEntryStart( If_Obj_t *, vNodes, pIfObj, i, nLeaves )
     {
-//        If_ObjPrint( pIfObj );
         if ( If_ObjIsCi(pIfObj) )
         {
-//printf( "Seeing PI in %d.\n", Vec_WrdSize(s_pMan->vDelays) );
             pIfObj->iCopy = 0;
+            fHole = 1;
             continue;
         }
         iFanin0 = Abc_LitNotCond( If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj) );
         iFanin1 = Abc_LitNotCond( If_ObjFanin1(pIfObj)->iCopy, If_ObjFaninC1(pIfObj) );
         pIfObj->iCopy = Gia_ManHashAnd( pGia, iFanin0, iFanin1 );
     }
-s_pMan->timeBuild += clock() - clk;
+    p->nHoleInTheWall += fHole;
+p->timeBuild += clock() - clk;
 
     // check if this node is already driving a PO
     pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pIfObj->iCopy));
     if ( pDriver->fMark1 )
     {
-        s_pMan->nFilterSame++;
+        p->nFilterSame++;
         return 1;
     }
 
     // create output
     assert( If_ObjIsAnd(pIfObj) );
     Gia_ManAppendCo( pGia, Abc_LitNotCond( pIfObj->iCopy, (uCanonPhase >> nLeaves) & 1 ) );
+
     // mark the driver
     pDriver = Gia_ManObj(pGia, Abc_Lit2Var(pIfObj->iCopy));
     pDriver->fMark1 = 1;
 
     // verify truth table
 clk = clock();
-    pTruth = Gia_ObjComputeTruthTable( pGia, Gia_ManPo(pGia, Gia_ManPoNum(pGia)-1) );
-    if ( memcmp( s_pMan->pTemp1, pTruth, s_pMan->nWords * sizeof(word) ) != 0 )
+    pTruth = Gia_ObjComputeTruthTable( pGia, Gia_ManCo(pGia, Gia_ManCoNum(pGia)-1) );
+    if ( memcmp( p->pTemp1, pTruth, p->nWords * sizeof(word) ) != 0 )
     {
 /*
         Kit_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
-        Kit_DsdPrintFromTruth( (unsigned *)s_pMan->pTemp1, nLeaves ); printf( "\n" );
+        Kit_DsdPrintFromTruth( (unsigned *)p->pTemp1, nLeaves ); printf( "\n" );
         printf( "Truth table verification has failed.\n" );
 */
-        Vec_IntPush( s_pMan->vTruthIds, -1 ); // truth table IDs
-        Vec_WrdPush( s_pMan->vDelays, 0 );
-        Vec_StrPush( s_pMan->vCosts, 0 );
-        s_pMan->nFilterTruth++;
+        // drive PO with constant
+        Gia_ManPatchCoDriver( pGia, Gia_ManCoNum(pGia)-1, 0 );
+        // save truth table ID
+        Vec_IntPush( p->vTruthIds, -1 );
+        p->nFilterTruth++;
         return 1;
     }
-s_pMan->timeCheck += clock() - clk;
+p->timeCheck += clock() - clk;
 
-    // add the resulting truth table to the hash table 
 clk = clock();
-    s_pMan->nAdded++;
-    Index = Vec_MemHashInsert( s_pMan->vTtMem, s_pMan->pTemp1 );
-    Vec_IntPush( s_pMan->vTruthIds, Index ); // truth table IDs
-    assert( Gia_ManPoNum(pGia) == Vec_IntSize(s_pMan->vTruthIds) );
-    if ( Index == Vec_MemEntryNum(s_pMan->vTtMem) - 1 )
-        s_pMan->nAddedFuncs++;
-    Vec_WrdPush( s_pMan->vDelays, 0 );
-    Vec_StrPush( s_pMan->vCosts, 0 );
-s_pMan->timeInsert += clock() - clk;
+    // add the resulting truth table to the hash table 
+    Index = Vec_MemHashInsert( p->vTtMem, p->pTemp1 );
+    // save truth table ID
+    Vec_IntPush( p->vTruthIds, Index );
+    assert( Gia_ManCoNum(pGia) == Vec_IntSize(p->vTruthIds) );
+    p->nAdded++;
+p->timeInsert += clock() - clk;
     return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Top level procedure for library construction.]
 
   Description []
                
@@ -391,15 +586,17 @@ void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB )
     int clk = clock();
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Performing recoding structures with choices.\n" );
+    // remember that the manager was used for library construction
+    s_pMan3->fLibConstr = 1;
     // create hash table if not available
-    if ( s_pMan->pGia->pHTable == NULL )
-        Gia_ManHashStart( s_pMan->pGia );
+    if ( s_pMan3->pGia->pHTable == NULL )
+        Gia_ManHashStart( s_pMan3->pGia );
 
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-    pPars->nLutSize    =  s_pMan->nVars;
-    pPars->nCutsMax    =  s_pMan->nCuts;
+    pPars->nLutSize    =  s_pMan3->nVars;
+    pPars->nCutsMax    =  s_pMan3->nCuts;
     pPars->DelayTarget = -1;
     pPars->Epsilon     =  (float)0.005;
     pPars->fArea       =  1;
@@ -424,9 +621,371 @@ void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB )
     // perform recording
     pNtkNew = Abc_NtkIf( pNtk, pPars );
     Abc_NtkDelete( pNtkNew );
-s_pMan->timeTotal += clock() - clk;
+s_pMan3->timeTotal += clock() - clk;
+}
+
+ /**Function*************************************************************
+
+  Synopsis    [Returns min AIG level at the output fo the cut using the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int If_CutComputeDelay( If_Man_t * p, If_Cut_t * pCut, char * pCanonPerm, word Delay )
+{
+    If_Obj_t* pLeaf;
+    int nLeaves = If_CutLeaveNum(pCut);
+    int i, delayTemp, delayMax = -ABC_INFINITY;
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        pLeaf = If_ManObj(p, (pCut)->pLeaves[(int)pCanonPerm[i]]);
+        delayTemp = If_ObjCutBest(pLeaf)->Delay + Lms_DelayGet(Delay, i);
+        if(delayTemp > delayMax)
+            delayMax = delayTemp;
+    }
+    return delayMax;
+}
+static inline int If_CutFindBestStruct( If_Man_t * pIfMan, If_Cut_t * pCut, char * pCanonPerm, unsigned * puCanonPhase, int * pBestPo )
+{
+    Lms_Man_t * p = s_pMan3;
+    int i, nLeaves, * pTruthId, iFirstPo, iFirstPoNext, iBestPo;
+    int BestDelay = ABC_INFINITY, BestArea = ABC_INFINITY, Delay, Area;
+    clock_t clk;
+
+    // semicanonicize the function
+clk = clock();
+    nLeaves = If_CutLeaveNum( pCut );
+    for ( i = 0; i < Abc_MaxInt(nLeaves, 6); i++ )
+        pCanonPerm[i] = i;
+    memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
+//    uCanonPhase = luckyCanonicizer_final_fast( p->pTemp1, nLeaves, pCanonPerm );
+    *puCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
+    Abc_TtStretch5( (unsigned *)p->pTemp1, nLeaves, p->nVars );
+p->timeCanon += clock() - clk;
+
+    // get TT ID for the given class
+    pTruthId = Vec_MemHashLookup( p->vTtMem, p->pTemp1 );
+    if ( *pTruthId == -1 )
+        return ABC_INFINITY;
+
+    // note that array p->vTruthPo contains the first PO for the given truth table
+    // other POs belonging to the same equivalence class follow immediately after this one
+    // to iterate through the POs, we need to perform the following steps
+
+    // find the first PO of this class
+    iFirstPo = Vec_IntEntry( p->vTruthPo, *pTruthId );
+    // find the first PO of the next class
+    iFirstPoNext = Vec_IntEntry( p->vTruthPo, *pTruthId+1 );
+    // iterate through the subgraphs of this class
+    iBestPo = -1;
+    for ( i = iFirstPo; i < iFirstPoNext; i++ )
+    {
+        Delay = If_CutComputeDelay( pIfMan, pCut, pCanonPerm, Vec_WrdEntry(p->vDelays, i) );
+        Area  = Vec_StrEntry(p->vAreas, i);
+        if ( iBestPo == -1 || BestDelay > Delay || (BestDelay == Delay && BestArea > Area) )
+        {
+            iBestPo = i;
+            BestDelay = Delay;
+            BestArea = Area;
+        }
+    }
+    if ( pBestPo )
+        *pBestPo = iBestPo;
+    return BestDelay; 
+}
+int If_CutDelayRecCost3( If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pObj )
+{
+    Lms_Man_t * p = s_pMan3;
+    char pCanonPerm[16];
+    unsigned uCanonPhase;
+    // make sure the cut functions match the library
+    assert( p->nVars == (int)pCut->nLimit );
+    // if this assertion fires, it means that LMS manager was used for library construction
+    // in this case, GIA has to be written out and the manager restarted as described above
+    assert( !p->fLibConstr );
+    if ( p->vTruthPo == NULL ) // the first time AIG level minimization is called
+    {
+        // compute the first PO for each semi-canonical form
+        int i, Entry;
+        p->vTruthPo = Vec_IntStartFull( Vec_MemEntryNum(p->vTtMem)+1 );
+        assert( Vec_IntFindMin(p->vTruthIds) >= 0 );
+        assert( Vec_IntFindMax(p->vTruthIds) < Vec_MemEntryNum(p->vTtMem) );
+        Vec_IntForEachEntry( p->vTruthIds, Entry, i )
+            if ( Vec_IntEntry(p->vTruthPo, Entry) == -1 )
+                Vec_IntWriteEntry( p->vTruthPo, Entry, i );
+        Vec_IntWriteEntry( p->vTruthPo, Vec_MemEntryNum(p->vTtMem), Gia_ManCoNum(p->pGia) );
+        // compute delay/area and init frequency
+        assert( p->vDelays == NULL );
+        assert( p->vAreas == NULL );
+        assert( p->vFreqs == NULL );
+        p->vDelays = Lms_GiaDelays( p->pGia );
+        p->vAreas  = Lms_GiaAreas( p->pGia );
+        p->vFreqs  = Vec_IntStart( Gia_ManCoNum(p->pGia) );
+    }
+    // return the delay of the best structure
+    return If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reexpresses the best structure of the cut in the HOP manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj )
+{
+    Lms_Man_t * p = s_pMan3;
+    char pCanonPerm[16];
+    unsigned uCanonPhase;
+    Hop_Obj_t * pFan0, * pFan1, * pHopObj;
+    Gia_Man_t * pGia = p->pGia;
+    Gia_Obj_t * pGiaPo, * pGiaTemp;
+    int i, BestPo, nLeaves = If_CutLeaveNum(pCut);
+    assert( pIfMan->pPars->fCutMin == 1 );
+    assert( nLeaves > 1 );
+
+    // get the best output for this node
+    If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
+    assert( BestPo >= 0 );
+    pGiaPo = Gia_ManCo( pGia, BestPo );
+
+    // collect internal nodes into pGia->vTtNodes
+    if ( pGia->vTtNodes == NULL )
+        pGia->vTtNodes = Vec_IntAlloc( 256 );
+    Gia_ObjCollectInternal( pGia, pGiaPo );
+    // collect HOP nodes for leaves
+    Vec_PtrClear( p->vLabelsP );
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        pHopObj = Hop_IthVar( pMan, pCanonPerm[i] );
+        pHopObj = Hop_NotCond( pHopObj, (uCanonPhase >> i) & 1 );
+        Vec_PtrPush(p->vLabelsP, pHopObj);
+    }
+    // compute HOP nodes for internal nodes
+    Gia_ManForEachObjVec( pGia->vTtNodes, pGia, pGiaTemp, i )
+    {
+        pGiaTemp->fMark0 = 0; // unmark node marked by Gia_ObjCollectInternal()
+
+        if ( Gia_ObjIsAnd(Gia_ObjFanin0(pGiaTemp)) )
+            pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin0(pGiaTemp)) + nLeaves);
+        else
+            pFan0 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjCioId(Gia_ObjFanin0(pGiaTemp)));
+        pFan0 = Hop_NotCond(pFan0, Gia_ObjFaninC0(pGiaTemp));
+
+        if ( Gia_ObjIsAnd(Gia_ObjFanin1(pGiaTemp)) )
+            pFan1 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, Gia_ObjFanin1(pGiaTemp)) + nLeaves);
+        else
+            pFan1 = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjCioId(Gia_ObjFanin1(pGiaTemp)));
+        pFan1 = Hop_NotCond(pFan1, Gia_ObjFaninC1(pGiaTemp));
+
+        pHopObj = Hop_And(pMan, pFan0, pFan1);
+        Vec_PtrPush(p->vLabelsP, pHopObj);
+    }
+    // get the final result
+    assert( Gia_ObjIsAnd(pGiaTemp) );
+    pHopObj = (Hop_Obj_t *)Vec_PtrEntry(p->vLabelsP, Gia_ObjNum(pGia, pGiaTemp) + nLeaves);
+    // complement the result if needed
+    return Hop_NotCond( pHopObj,  pCut->fCompl ^ Gia_ObjFaninC0(pGiaPo) ^ ((uCanonPhase >> nLeaves) & 1) );    
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces GIA to contain only useful COs and internal nodes.]
+
+  Description [During library construction, redundant nodes are added.
+  Some COs are found to be useless because their TT does not match the
+  (semi-canonicized TT) of the cut, etc.  This procedure reduces GIA
+  to contains only useful (non-redundant, non-dominated) COs and the
+  corresponding internal nodes. This procedure replaces GIA by a new GIA
+  and creates new vTruthIds. The COs with the same truth table have
+  adjacent IDs. This procedure does not change the truth tables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// count how many times TT occurs
+Vec_Int_t * Lms_GiaCountTruths( Lms_Man_t * p )
+{
+    Vec_Int_t * vCounts = Vec_IntStart( Vec_MemEntryNum(p->vTtMem) );
+    int i, Entry;
+    Vec_IntForEachEntry( p->vTruthIds, Entry, i )
+        if ( Entry >= 0 )
+            Vec_IntAddToEntry( vCounts, Entry, 1 );
+    return vCounts;
 }
+// collect PO indexes worth visiting
+Vec_Int_t * Lms_GiaCollectUsefulCos( Lms_Man_t * p )
+{
+    Vec_Int_t * vBegins = Vec_IntAlloc( Vec_MemEntryNum(p->vTtMem) );
+    Vec_Int_t * vUseful = Vec_IntStartFull( Gia_ManCoNum(p->pGia) + Vec_MemEntryNum(p->vTtMem) );
+    Vec_Int_t * vCounts = Lms_GiaCountTruths( p );
+    int i, Entry, * pPlace, SumTotal = 0;
+    // mark up the place for POs
+    Vec_IntForEachEntry( vCounts, Entry, i )
+    {
+        assert( Entry > 0 );
+        Vec_IntPush( vBegins, SumTotal );
+        SumTotal += Entry + 1;
+//        printf( "%d ", Entry );
+    }
+    Vec_IntPush( vBegins, SumTotal );
+    // fill out POs in their places
+    Vec_IntFill( vCounts, Vec_IntSize(vCounts), 0 );
+    Vec_IntForEachEntry( p->vTruthIds, Entry, i )
+    {
+        if ( Entry < 0 )
+            continue;
+        pPlace = Vec_IntEntryP( vUseful, Vec_IntEntry(vBegins, Entry) + Vec_IntEntry(vCounts, Entry) );
+        assert( *pPlace == -1 );
+        *pPlace = i;
+        Vec_IntAddToEntry( vCounts, Entry, 1 );
+    }
+    Vec_IntFree( vBegins );
+    Vec_IntFree( vCounts );
+    return vUseful;
+}
+// collect non-dominated COs
+Vec_Int_t * Lms_GiaFindNonRedundantCos( Lms_Man_t * p )
+{
+    Vec_Int_t * vRemain;
+    Vec_Int_t * vUseful;
+    Vec_Wrd_t * vDelays;
+    int i, k, EntryI, EntryK;
+    word D1, D2;
+    vDelays = Lms_GiaDelays( p->pGia );
+    vUseful = Lms_GiaCollectUsefulCos( p );
+    Vec_IntForEachEntry( vUseful, EntryI, i )
+    {
+        if ( EntryI < 0 )
+            continue;
+        D1 = Vec_WrdEntry(vDelays, EntryI);
+        assert( D1 > 0 );
+        Vec_IntForEachEntryStart( vUseful, EntryK, k, i+1 )
+        {
+            if ( EntryK == -1 )
+                break;
+            if ( EntryK == -2 )
+                continue;
+            D2 = Vec_WrdEntry(vDelays, EntryK);
+            assert( D2 > 0 );
+            if ( Lms_DelayDom(D1, D2, Gia_ManCiNum(p->pGia)) ) // D1 dominate D2
+            {
+                Vec_IntWriteEntry( vUseful, k, -2 );
+                continue;
+            }
+            if ( Lms_DelayDom(D2, D1, Gia_ManCiNum(p->pGia)) ) // D2 dominate D1
+            {
+                Vec_IntWriteEntry( vUseful, i, -2 );
+                break;
+            }
+        }
+    }
+
+    vRemain = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntry( vUseful, EntryI, i )
+        if ( EntryI >= 0 )
+            Vec_IntPush( vRemain, EntryI );
+    Vec_IntFree( vUseful );
+    Vec_WrdFree( vDelays );
+    return vRemain;
+}
+// replace GIA and vTruthIds by filtered ones
+void Lms_GiaNormalize( Lms_Man_t * p )
+{
+    Gia_Man_t * pGiaNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vRemain;
+    Vec_Int_t * vTruthIdsNew;
+    int i, Entry, Prev = -1, Next;
+    // collect non-redundant COs
+    vRemain = Lms_GiaFindNonRedundantCos( p );
+    // change these to be useful literals
+    vTruthIdsNew = Vec_IntAlloc( Vec_IntSize(vRemain) );
+    Vec_IntForEachEntry( vRemain, Entry, i )
+    {
+        pObj = Gia_ManCo(p->pGia, Entry);
+        assert( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) );
+        Vec_IntWriteEntry( vRemain, i, Gia_ObjFaninLit0p(p->pGia, pObj) );
+        // create new truth IDs
+        Next = Vec_IntEntry(p->vTruthIds, Gia_ObjCioId(pObj));
+        assert( Prev <= Next );
+        Vec_IntPush( vTruthIdsNew, Next );
+        Prev = Next;
+    }
+    // create a new GIA
+    Gia_ManForEachObj( p->pGia, pObj, i )
+        assert( pObj->fMark0 == 0 );
+    for ( i = 0; i < Gia_ManCoNum(p->pGia); i++ )
+        Gia_ManPatchCoDriver( p->pGia, i, 0 );
+    Vec_IntForEachEntry( vRemain, Entry, i )
+        Gia_ManAppendCo( p->pGia, Entry );
+//    pGiaNew = Gia_ManCleanup( p->pGia );
+    pGiaNew = Gia_ManCleanupOutputs( p->pGia, Gia_ManCoNum(p->pGia) - Vec_IntSize(vRemain) );
+    Gia_ManStop( p->pGia );
+    p->pGia = pGiaNew;
+    Vec_IntFree( vRemain );
+    // update truth IDs
+    Vec_IntFree( p->vTruthIds );
+    p->vTruthIds = vTruthIdsNew;
+//    Vec_IntPrint( vTruthIdsNew );
+}
+
+/**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecPs3(int fPrintLib)
+{
+    Lms_ManPrint( s_pMan3 );
+
+    printf( "Before normalizing\n" );
+    Gia_ManPrintStats( s_pMan3->pGia, 0, 0 );
+
+    Lms_GiaNormalize( s_pMan3 );
+
+    printf( "After normalizing\n" );
+    Gia_ManPrintStats( s_pMan3->pGia, 0, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRecIsRunning3()
+{
+    return s_pMan3 != NULL;
+}
+Gia_Man_t * Abc_NtkRecGetGia3()
+{
+    Lms_GiaNormalize( s_pMan3 );
+    return s_pMan3->pGia;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///