Integrating GIA with LUT mapping.

14 files changed, 962 insertions, 362 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4473921c..07bdff94 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -700,6 +700,7 @@ extern int                 Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, i
 extern void                Gia_ManVerifyChoices( Gia_Man_t * p );
 extern void                Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern int                 Gia_ManChoiceLevel( Gia_Man_t * p );
 /*=== giaCsatOld.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
@@ -810,7 +811,14 @@ extern Gia_Man_t *         Gia_ManRehash( Gia_Man_t * p, int fAddStrash );
 extern void                Gia_ManHashProfile( Gia_Man_t * p );
 extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
 /*=== giaIf.c ===========================================================*/
-extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
+extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );
+extern int                 Gia_ManLutSizeMax( Gia_Man_t * p );
+extern int                 Gia_ManLutNum( Gia_Man_t * p );
+extern int                 Gia_ManLutLevel( Gia_Man_t * p );
+extern void                Gia_ManSetRefsMapped( Gia_Man_t * p );
+extern void                Gia_ManSetIfParsDefault( void * pIfPars );
+extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 /*=== giaIso.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fDualOut, int fVerbose );
@@ -826,12 +834,7 @@ extern void                Gia_ManPrintStatsShort( Gia_Man_t * p );
 extern void                Gia_ManPrintMiterStatus( Gia_Man_t * p ); 
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
-/*=== giaMap.c ===========================================================*/
-extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
-extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );
-extern int                 Gia_ManLutSizeMax( Gia_Man_t * p );
-extern int                 Gia_ManLutNum( Gia_Man_t * p );
-extern int                 Gia_ManLutLevel( Gia_Man_t * p );
+extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
 /*=== giaMem.c ===========================================================*/
 extern Gia_MmFixed_t *     Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
 extern void                Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c
index 85f0a372..ca2acb28 100644
--- a/src/aig/gia/giaChoice.c
+++ b/src/aig/gia/giaChoice.c
@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "giaAig.h"
+#include "misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -261,6 +262,108 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Gia_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Gia_ObjSetTravIdCurrent( p, pObj );
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Gia_ManCo( p, iTerm1 + i );
+                    Gia_ManChoiceLevel_rec( p, pNext );
+                    if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                        LevelMax = Gia_ObjLevel(p, pNext);
+                }
+                LevelMax++;
+            }
+        }
+//        Abc_Print( 1, "%d ", pObj->Level );
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+    {
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+    }
+    else if ( Gia_ObjIsAnd(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        pNext = Gia_ObjFanin1(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( p->pSibls && (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
+        {
+            Gia_ManChoiceLevel_rec( p, pNext );
+            if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                LevelMax = Gia_ObjLevel(p, pNext);
+        }
+    }
+    else if ( !Gia_ObjIsConst0(pObj) )
+        assert( 0 );
+    Gia_ObjSetLevel( p, pObj, LevelMax );
+}
+int Gia_ManChoiceLevel( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, LevelMax = 0;
+//    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+    }
+    // account for dangling boxes
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+//        Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
+    }
+//    Abc_Print( 1, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+        assert( Gia_ObjLevel(p, pObj) > 0 );
+//    printf( "Max level %d\n", LevelMax );
+    return LevelMax;
+} 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 13e4f429..ae015116 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -21,7 +21,7 @@
 #include "gia.h"
 #include "aig/aig/aig.h"
 #include "map/if/if.h"
-#include "opt/dar/dar.h"
+#include "bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -45,44 +45,48 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSetIfParsDefault( If_Par_t * pPars )
+void Gia_ManSetIfParsDefault( void * pp )
 {
+    If_Par_t * pPars = (If_Par_t *)pp;
 //    extern void * Abc_FrameReadLibLut();
+    If_Par_t * p = (If_Par_t *)pPars;
     // set defaults
-    memset( pPars, 0, sizeof(If_Par_t) );
+    memset( p, 0, sizeof(If_Par_t) );
     // user-controlable paramters
-//    pPars->nLutSize    = -1;
-    pPars->nLutSize    =  6;
-    pPars->nCutsMax    =  8;
-    pPars->nFlowIters  =  1;
-    pPars->nAreaIters  =  2;
-    pPars->DelayTarget = -1;
-    pPars->Epsilon     =  (float)0.005;
-    pPars->fPreprocess =  1;
-    pPars->fArea       =  0;
-    pPars->fFancy      =  0;
-    pPars->fExpRed     =  1; ////
-    pPars->fLatchPaths =  0;
-    pPars->fEdge       =  1;
-    pPars->fPower      =  0;
-    pPars->fCutMin     =  0;
-    pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  0;
+    p->nLutSize    = -1;
+//    p->nLutSize    =  6;
+    p->nCutsMax    =  8;
+    p->nFlowIters  =  1;
+    p->nAreaIters  =  2;
+    p->DelayTarget = -1;
+    p->Epsilon     =  (float)0.005;
+    p->fPreprocess =  1;
+    p->fArea       =  0;
+    p->fFancy      =  0;
+    p->fExpRed     =  0; ////
+    p->fLatchPaths =  0;
+    p->fEdge       =  1;
+    p->fPower      =  0;
+    p->fCutMin     =  0;
+    p->fSeqMap     =  0;
+    p->fVerbose    =  0;
+    p->pLutStruct  =  NULL;
     // internal parameters
-    pPars->fTruth      =  0;
-    pPars->nLatchesCi  =  0;
-    pPars->nLatchesCo  =  0;
-    pPars->fLiftLeaves =  0;
-//    pPars->pLutLib     =  Abc_FrameReadLibLut();
-    pPars->pLutLib     =  NULL;
-    pPars->pTimesArr   =  NULL; 
-    pPars->pTimesArr   =  NULL;   
-    pPars->pFuncCost   =  NULL;   
+    p->fTruth      =  0;
+    p->nLatchesCi  =  0;
+    p->nLatchesCo  =  0;
+    p->fLiftLeaves =  0;
+    p->fUseCoAttrs =  1;   // use CO attributes
+    p->pLutLib     =  NULL;
+    p->pTimesArr   =  NULL; 
+    p->pTimesArr   =  NULL;   
+    p->pFuncCost   =  NULL;   
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Load the network into FPGA manager.]
+  Synopsis    [Prints mapping statistics.]
 
   Description []
                
@@ -91,97 +95,17 @@ void Gia_ManSetIfParsDefault( If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
+int Gia_ManLutFaninCount( Gia_Man_t * p )
 {
-//    extern Vec_Int_t * SGia_ManComputeSwitchProbs( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
-//    Vec_Int_t * vSwitching = NULL, * vSwitching2 = NULL;
-//    float * pSwitching, * pSwitching2;
-    If_Man_t * pIfMan;
-    If_Obj_t * pIfObj;
-    Gia_Obj_t * pNode;
-    int i;//, clk = clock();
-    Gia_ManLevelNum( p );
-//    assert( p->pReprs == NULL );
-/*
-    // set the number of registers (switch activity will be combinational)
-    Gia_ManSetRegNum( p, 0 );
-    if ( pPars->fPower )
-    {
-        vSwitching  = SGia_ManComputeSwitchProbs( p, 48, 16, 0 );
-        if ( pPars->fVerbose )
-        {
-            ABC_PRT( "Computing switching activity", clock() - clk );
-        }
-        pSwitching  = (float *)vSwitching->pArray;
-        vSwitching2 = Vec_IntStart( Gia_ManObjNumMax(p) );
-        pSwitching2 = (float *)vSwitching2->pArray;
-    }
-*/
-    // start the mapping manager and set its parameters
-    pIfMan = If_ManStart( pPars );
-//    pIfMan->vSwitching = vSwitching2;
-    // load the AIG into the mapper
-    Gia_ManCreateRefs( p );
-    Gia_ManForEachObj( p, pNode, i )
-    {
-        if ( Gia_ObjIsAnd(pNode) )
-            pIfObj = If_ManCreateAnd( pIfMan, 
-                If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ), 
-                If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId1(pNode, i)), Gia_ObjFaninC1(pNode) ) );
-        else if ( Gia_ObjIsCi(pNode) )
-        {
-            pIfObj = If_ManCreateCi( pIfMan );
-            If_ObjSetLevel( pIfObj, Gia_ObjLevel(p,pNode) );
-//            Abc_Print( 1, "pi=%d ", pIfObj->Level );
-            if ( pIfMan->nLevelMax < (int)pIfObj->Level )
-                pIfMan->nLevelMax = (int)pIfObj->Level;
-        }
-        else if ( Gia_ObjIsCo(pNode) )
-        {
-            pIfObj = If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Vec_PtrEntry(vAigToIf, Gia_ObjFaninId0(pNode, i)), Gia_ObjFaninC0(pNode) ) );
-//            Abc_Print( 1, "po=%d ", pIfObj->Level );
-        }
-        else if ( Gia_ObjIsConst0(pNode) )
-            pIfObj = If_Not(If_ManConst1( pIfMan ));
-        else // add the node to the mapper
-            assert( 0 );
-        // save the result
-        assert( Vec_PtrEntry(vAigToIf, i) == NULL );
-        Vec_PtrWriteEntry( vAigToIf, i, pIfObj );
-//        if ( vSwitching2 )
-//            pSwitching2[pIfObj->Id] = pSwitching[pNode->Id];    
-        // set up the choice node
-/*
-//        if ( p->pReprs && p->pNexts && Gia_ObjIsHead( p, i ) )
-        if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefNumId(p, i) )
-        {
-            int iPrev, iFanin;
-            pIfMan->nChoices++;
-            for ( iPrev = i, iFanin = Gia_ObjNext(p, i); iFanin; iPrev = iFanin, iFanin = Gia_ObjNext(p, iFanin) )
-                If_ObjSetChoice( Vec_PtrEntry(vAigToIf,iPrev), Vec_PtrEntry(vAigToIf,iFanin) );
-            If_ManCreateChoice( pIfMan, Vec_PtrEntry(vAigToIf,i) );
-        }
-*/
-/*        // set up the choice node
-        if ( Gia_ObjIsChoice( p, pNode ) )
-        {
-            pIfMan->nChoices++;
-            for ( pPrev = pNode, pFanin = Gia_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Gia_ObjEquiv(p, pFanin) )
-                If_ObjSetChoice( pPrev->pData, pFanin->pData );
-            If_ManCreateChoice( pIfMan, pNode->pData );
-        }
-//        assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
-*/
-    }
-//    if ( vSwitching )
-//        Vec_IntFree( vSwitching );
-    return pIfMan;
+    int i, Counter = 0;
+    Gia_ManForEachLut( p, i )
+        Counter += Gia_ObjLutSize(p, i);
+    return Counter;
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Prints mapping statistics.]
 
   Description []
                
@@ -190,60 +114,17 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
   SeeAlso     []
 
 ***********************************************************************/
-int * Gia_ManFromIf( If_Man_t * pIfMan, Gia_Man_t * p, Vec_Ptr_t * vAigToIf )
+int Gia_ManLutSizeMax( Gia_Man_t * p )
 {
-    int * pMapping, iOffset;
-    Vec_Ptr_t * vIfToAig;
-    Gia_Obj_t * pObj, * pObjRepr;
-    If_Obj_t * pIfObj;
-    If_Cut_t * pCutBest;
-    int i, k, j, nLeaves, * ppLeaves;
-    int nItems = 0;
-    assert( Gia_ManCiNum(p) == If_ManCiNum(pIfMan) );
-    assert( Gia_ManCoNum(p) == If_ManCoNum(pIfMan) );
-    assert( Gia_ManAndNum(p) == If_ManAndNum(pIfMan) );
-    // create mapping of IF to AIG
-    vIfToAig = Vec_PtrStart( If_ManObjNum(pIfMan) );
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        pIfObj = (If_Obj_t *)Vec_PtrEntry( vAigToIf, i );
-        Vec_PtrWriteEntry( vIfToAig, pIfObj->Id, pObj );
-        if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
-            continue;
-        nItems += 2 + If_CutLeaveNum( If_ObjCutBest(pIfObj) );
-    }
-    // construct the network
-    pMapping = ABC_CALLOC( int, Gia_ManObjNum(p) + nItems );
-    iOffset = Gia_ManObjNum(p);
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        pIfObj = (If_Obj_t *)Vec_PtrEntry( vAigToIf, i );
-        if ( !Gia_ObjIsAnd(pObj) || pIfObj->nRefs == 0 )
-            continue;
-        pCutBest = If_ObjCutBest( pIfObj );
-        nLeaves  = If_CutLeaveNum( pCutBest ); 
-        ppLeaves = If_CutLeaves( pCutBest );
-        // create node
-        k = iOffset;
-        pMapping[k++] = nLeaves;
-        for ( j = 0; j < nLeaves; j++ )
-        {
-            pObjRepr = (Gia_Obj_t *)Vec_PtrEntry( vIfToAig, ppLeaves[j] );
-            pMapping[k++] = Gia_ObjId( p, pObjRepr );
-        }
-        pMapping[k++] = i;
-        pMapping[i] = iOffset;
-        iOffset = k;
-    }
-    assert( iOffset <= Gia_ManObjNum(p) + nItems );
-    Vec_PtrFree( vIfToAig );
-//    pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
-    return pMapping;
+    int i, nSizeMax = -1;
+    Gia_ManForEachLut( p, i )
+        nSizeMax = Abc_MaxInt( nSizeMax, Gia_ObjLutSize(p, i) );
+    return nSizeMax;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Interface with the FPGA mapping package.]
+  Synopsis    [Prints mapping statistics.]
 
   Description []
                
@@ -252,39 +133,14 @@ int * Gia_ManFromIf( If_Man_t * pIfMan, Gia_Man_t * p, Vec_Ptr_t * vAigToIf )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars )
+int Gia_ManLutNum( Gia_Man_t * p )
 {
-    If_Man_t * pIfMan;
-    Vec_Ptr_t * vAigToIf;
-    // set the arrival times
-    pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
-    memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
-    // translate into the mapper
-    vAigToIf = Vec_PtrStart( Gia_ManObjNum(p) );
-    pIfMan = Gia_ManToIf( p, pPars, vAigToIf );    
-    if ( pIfMan == NULL )
-    {
-        Vec_PtrFree( vAigToIf );
-        return 0;
-    }
-//    pIfMan->pManTim = Tim_ManDup( pManTime, 0 );
-    if ( !If_ManPerformMapping( pIfMan ) )
-    {
-        Vec_PtrFree( vAigToIf );
-        If_ManStop( pIfMan );
-        return 0;
-    }
-    // transform the result of mapping into the new network
-    ABC_FREE( p->pMapping );
-    p->pMapping = Gia_ManFromIf( pIfMan, p, vAigToIf );
-//    if ( pPars->fBidec && pPars->nLutSize <= 8 )
-//        Gia_ManBidecResyn( pNtk, 0 );
-    If_ManStop( pIfMan );
-    Vec_PtrFree( vAigToIf );
-    return 1;
+    int i, Counter = 0;
+    Gia_ManForEachLut( p, i )
+        Counter ++;
+    return Counter;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Prints mapping statistics.]
@@ -296,35 +152,30 @@ int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintMappingStats( Gia_Man_t * p )
+int Gia_ManLutLevel( Gia_Man_t * p )
 {
-    int * pLevels;
-    int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
-    if ( !p->pMapping )
-        return;
-    pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    Gia_Obj_t * pObj;
+    int i, k, iFan, Level;
+    int * pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachLut( p, i )
     {
-        nLuts++;
-        nFanins += Gia_ObjLutSize(p, i);
-        nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
+        Level = 0;
         Gia_LutForEachFanin( p, i, iFan, k )
-            pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
-        pLevels[i]++;
-        LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
+            if ( Level < pLevels[iFan] )
+                Level = pLevels[iFan];
+        pLevels[i] = Level + 1;
     }
+    Level = 0;
+    Gia_ManForEachCo( p, pObj, k )
+        if ( Level < pLevels[Gia_ObjFaninId0p(p, pObj)] )
+            Level = pLevels[Gia_ObjFaninId0p(p, pObj)];
     ABC_FREE( pLevels );
-    Abc_Print( 1, "mapping (K=%d)  :  ", nLutSize );
-    Abc_Print( 1, "lut =%7d  ", nLuts );
-    Abc_Print( 1, "edge =%8d  ", nFanins );
-    Abc_Print( 1, "lev =%5d  ", LevelMax );
-    Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
-    Abc_Print( 1, "\n" );
+    return Level;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prints mapping statistics.]
+  Synopsis    [Assigns levels.]
 
   Description []
                
@@ -333,12 +184,17 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManLutFaninCount( Gia_Man_t * p )
+void Gia_ManSetRefsMapped( Gia_Man_t * p )  
 {
-    int i, Counter = 0;
+    Gia_Obj_t * pObj;
+    int i, k, iFan;
+    ABC_FREE( p->pRefs );
+    p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ObjRefInc( p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachLut( p, i )
-        Counter += Gia_ObjLutSize(p, i);
-    return Counter;
+        Gia_LutForEachFanin( p, i, iFan, k )
+            Gia_ObjRefInc( p, Gia_ManObj(p, iFan) );
 }
 
 /**Function*************************************************************
@@ -352,17 +208,37 @@ int Gia_ManLutFaninCount( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManLutSizeMax( Gia_Man_t * p )
+void Gia_ManPrintMappingStats( Gia_Man_t * p )
 {
-    int i, nSizeMax = -1;
+    int * pLevels;
+    int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
+    if ( !p->pMapping )
+        return;
+    pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachLut( p, i )
-        nSizeMax = Abc_MaxInt( nSizeMax, Gia_ObjLutSize(p, i) );
-    return nSizeMax;
+    {
+        nLuts++;
+        nFanins += Gia_ObjLutSize(p, i);
+        nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
+        Gia_LutForEachFanin( p, i, iFan, k )
+            pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
+        pLevels[i]++;
+        LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
+    }
+    ABC_FREE( pLevels );
+    Abc_Print( 1, "mapping (K=%d)  :  ", nLutSize );
+    Abc_Print( 1, "lut =%7d  ", nLuts );
+    Abc_Print( 1, "edge =%8d  ", nFanins );
+    Abc_Print( 1, "lev =%5d  ", LevelMax );
+    Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
+    Abc_Print( 1, "\n" );
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Prints mapping statistics.]
+  Synopsis    [Converts GIA into IF manager.]
 
   Description []
                
@@ -371,17 +247,66 @@ int Gia_ManLutSizeMax( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManLutNum( Gia_Man_t * p )
+static inline If_Obj_t * If_ManFanin0Copy( If_Man_t * pIfMan, Gia_Obj_t * pObj ) { return If_NotCond( If_ManObj(pIfMan, Gia_ObjValue(Gia_ObjFanin0(pObj))), Gia_ObjFaninC0(pObj) ); }
+static inline If_Obj_t * If_ManFanin1Copy( If_Man_t * pIfMan, Gia_Obj_t * pObj ) { return If_NotCond( If_ManObj(pIfMan, Gia_ObjValue(Gia_ObjFanin1(pObj))), Gia_ObjFaninC1(pObj) ); }
+If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars )
 {
-    int i, Counter = 0;
-    Gia_ManForEachLut( p, i )
-        Counter ++;
-    return Counter;
+    If_Man_t * pIfMan;
+    If_Obj_t * pIfObj;
+    Gia_Obj_t * pObj;
+    int i;
+    // create levels with choices
+    Gia_ManChoiceLevel( p );
+    // mark representative nodes
+    Gia_ManMarkFanoutDrivers( p );
+    // start the mapping manager and set its parameters
+    pIfMan = If_ManStart( pPars );
+    pIfMan->pName = Abc_UtilStrsav( Gia_ManName(p) );
+    // print warning about excessive memory usage
+    if ( 1.0 * Gia_ManObjNum(p) * pIfMan->nObjBytes / (1<<30) > 1.0 )
+        printf( "Warning: The mapper will allocate %.1f GB for to represent the subject graph with %d AIG nodes.\n", 
+            1.0 * Gia_ManObjNum(p) * pIfMan->nObjBytes / (1<<30), Gia_ManObjNum(p) );
+    // load the AIG into the mapper
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = If_ObjId( If_ManConst1(pIfMan) );
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pIfObj = If_ManCreateAnd( pIfMan, If_ManFanin0Copy(pIfMan, pObj), If_ManFanin1Copy(pIfMan, pObj) );
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pIfObj = If_ManCreateCi( pIfMan );
+            If_ObjSetLevel( pIfObj, Gia_ObjLevel(p, pObj) );
+//            Abc_Print( 1, "pi%d=%d\n ", If_ObjId(pIfObj), If_ObjLevel(pIfObj) );
+            if ( pIfMan->nLevelMax < (int)pIfObj->Level )
+                pIfMan->nLevelMax = (int)pIfObj->Level;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            pIfObj = If_ManCreateCo( pIfMan, If_NotCond( If_ManFanin0Copy(pIfMan, pObj), Gia_ObjIsConst0(Gia_ObjFanin0(pObj))) );
+//            Abc_Print( 1, "po%d=%d\n ", If_ObjId(pIfObj), If_ObjLevel(pIfObj) );
+        }
+        else assert( 0 );
+        assert( i == If_ObjId(pIfObj) );
+        Gia_ObjSetValue( pObj, If_ObjId(pIfObj) );
+        // set up the choice node
+        if ( Gia_ObjSibl(p, i) && pObj->fMark0 )
+        {
+            Gia_Obj_t * pSibl, * pPrev;
+            for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) )
+                If_ObjSetChoice( If_ManObj(pIfMan, Gia_ObjValue(pObj)), If_ManObj(pIfMan, Gia_ObjValue(pSibl)) );
+            If_ManCreateChoice( pIfMan, If_ManObj(pIfMan, Gia_ObjValue(pObj)) );
+        }
+//        assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
+    }
+    Gia_ManCleanMark0( p );
+    return pIfMan;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Prints mapping statistics.]
+  Synopsis    [Derives node's AIG after SOP balancing]
 
   Description []
                
@@ -390,30 +315,45 @@ int Gia_ManLutNum( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManLutLevel( Gia_Man_t * p )
+int Gia_ManNodeIfSopToGiaInt( Gia_Man_t * pNew, Vec_Wrd_t * vAnds, int nVars, Vec_Int_t * vLeaves )
 {
-    Gia_Obj_t * pObj;
-    int i, k, iFan, Level;
-    int * pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
-    Gia_ManForEachLut( p, i )
+    Vec_Int_t * vResults;
+    int iRes0, iRes1, iRes;
+    If_And_t This;
+    word Entry;
+    int i;
+    if ( Vec_WrdSize(vAnds) == 0 )
+        return 0;
+    if ( Vec_WrdSize(vAnds) == 1 && Vec_WrdEntry(vAnds,0) == 0 )
+        return 1;
+    vResults = Vec_IntAlloc( Vec_WrdSize(vAnds) );
+    for ( i = 0; i < nVars; i++ )
+        Vec_IntPush( vResults, Vec_IntEntry(vLeaves, i) );
+    Vec_WrdForEachEntryStart( vAnds, Entry, i, nVars )
     {
-        Level = 0;
-        Gia_LutForEachFanin( p, i, iFan, k )
-            if ( Level < pLevels[iFan] )
-                Level = pLevels[iFan];
-        pLevels[i] = Level + 1;
+        This  = If_WrdToAnd( Entry );
+        iRes0 = Abc_LitNotCond( Vec_IntEntry(vResults, This.iFan0), This.fCompl0 ); 
+        iRes1 = Abc_LitNotCond( Vec_IntEntry(vResults, This.iFan1), This.fCompl1 ); 
+        iRes  = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+//        iRes  = Gia_ManAppendAnd( pNew, iRes0, iRes1 );
+        Vec_IntPush( vResults, iRes );
     }
-    Level = 0;
-    Gia_ManForEachCo( p, pObj, k )
-        if ( Level < pLevels[Gia_ObjFaninId0p(p, pObj)] )
-            Level = pLevels[Gia_ObjFaninId0p(p, pObj)];
-    ABC_FREE( pLevels );
-    return Level;
+    Vec_IntFree( vResults );
+    return Abc_LitNotCond( iRes, This.fCompl );
+}
+int Gia_ManNodeIfSopToGia( Gia_Man_t * pNew, If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vLeaves )
+{
+    int iResult;
+    Vec_Wrd_t * vArray;
+    vArray  = If_CutDelaySopArray( p, pCut );
+    iResult = Gia_ManNodeIfSopToGiaInt( pNew, vArray, If_CutLeaveNum(pCut), vLeaves );
+//    Vec_WrdFree( vArray );
+    return iResult;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns levels.]
+  Synopsis    [Recursively derives the local AIG for the cut.]
 
   Description []
                
@@ -422,22 +362,72 @@ int Gia_ManLutLevel( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSetRefsMapped( Gia_Man_t * p )  
+int Gia_ManNodeIfToGia_rec( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
 {
-    Gia_Obj_t * pObj;
-    int i, k, iFan;
-    ABC_FREE( p->pRefs );
-    p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
-    Gia_ManForEachCo( p, pObj, i )
-        Gia_ObjRefInc( p, Gia_ObjFanin0(pObj) );
-    Gia_ManForEachLut( p, i )
-        Gia_LutForEachFanin( p, i, iFan, k )
-            Gia_ObjRefInc( p, Gia_ManObj(p, iFan) );
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    int iFunc, iFunc0, iFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutDataInt(pCut) )
+        return If_CutDataInt(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetDataInt( pCut, ~0 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutDataInt(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        iFunc0 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin0, vVisited );
+        if ( iFunc0 == ~0 )
+            continue;
+        iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited );
+        if ( iFunc1 == ~0 )
+            continue;
+        // both branches are solved
+        iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
+//        iFunc = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            iFunc = Abc_LitNot(iFunc);
+        If_CutSetDataInt( pCut, iFunc );
+        break;
+    }
+    return If_CutDataInt(pCut);
+}
+int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vLeaves )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pLeaf;
+    int i, iRes;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    assert( pCut->nLeaves > 1 );
+    // set the leaf variables
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetDataInt( If_ObjCutBest(pLeaf), Vec_IntEntry(vLeaves, i) );
+    // recursively compute the function while collecting visited cuts
+    Vec_PtrClear( pIfMan->vTemp );
+    iRes = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pIfObj, pIfMan->vTemp ); 
+    if ( iRes == ~0 )
+    {
+        Abc_Print( -1, "Gia_ManNodeIfToGia(): Computing local AIG has failed.\n" );
+        return ~0;
+    }
+    // clean the cuts
+    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
+        If_CutSetDataInt( If_ObjCutBest(pLeaf), 0 );
+    Vec_PtrForEachEntry( If_Cut_t *, pIfMan->vTemp, pCut, i )
+        If_CutSetDataInt( pCut, 0 );
+    return iRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prints NPN class statistics.]
+  Synopsis    [Converts IF into GIA manager.]
 
   Description []
                
@@ -446,83 +436,196 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintNpnClasses( Gia_Man_t * p )
+Gia_Man_t * Gia_ManFromIf( If_Man_t * pIfMan )
 {
-    extern char ** Kit_DsdNpn4ClassNames();
-    char ** pNames = Kit_DsdNpn4ClassNames();
-    Vec_Int_t * vLeaves, * vTruth, * vVisited;
-    int * pLutClass, ClassCounts[222] = {0};
-    int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
+    Gia_Man_t * pNew;
+    If_Obj_t * pIfObj, * pIfLeaf;
+    If_Cut_t * pCutBest;
+    Vec_Int_t * vLeaves;
     unsigned * pTruth;
-    assert( p->pMapping != NULL );
-    assert(  Gia_ManLutSizeMax( p ) <= 4 );
-    vLeaves   = Vec_IntAlloc( 100 );
-    vVisited  = Vec_IntAlloc( 100 );
-    vTruth    = Vec_IntAlloc( (1<<16) );
-    pLutClass = ABC_CALLOC( int, Gia_ManObjNum(p) );
-    Gia_ManCleanTruth( p );
-    Gia_ManForEachLut( p, i )
+    int Counter, iOffset, nItems = 0;
+    int i, k, w, GiaId;
+    // create new manager
+    pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
+    Gia_ManHashAlloc( pNew );
+    // iterate through nodes used in the mapping
+    vLeaves = Vec_IntAlloc( 16 );
+    If_ManCleanCutData( pIfMan );
+    If_ManForEachObj( pIfMan, pIfObj, i )
     {
-        if ( Gia_ObjLutSize(p,i) > 4 )
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
             continue;
-        Vec_IntClear( vLeaves );
-        Gia_LutForEachFanin( p, i, iFan, k )
-            Vec_IntPush( vLeaves, iFan );
-        for ( ; k < 4; k++ )
-            Vec_IntPush( vLeaves, 0 );
-        pTruth = Gia_ManConvertAigToTruth( p, Gia_ManObj(p, i), vLeaves, vTruth, vVisited );
-        Class = Dar_LibReturnClass( *pTruth );
-        ClassCounts[ Class ]++;
-        pLutClass[i] = Class;
+        if ( If_ObjIsAnd(pIfObj) )
+        {
+            pCutBest = If_ObjCutBest( pIfObj );
+            // collect leaves of the best cut
+            Vec_IntClear( vLeaves );
+            If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
+                Vec_IntPush( vLeaves, pIfLeaf->iCopy );
+            // get the functionality
+            if ( pIfMan->pPars->fDelayOpt )
+                pIfObj->iCopy = Gia_ManNodeIfSopToGia( pNew, pIfMan, pCutBest, vLeaves );
+            else
+                pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves );
+            nItems += 2 + If_CutLeaveNum( pCutBest );
+        }
+        else if ( If_ObjIsCi(pIfObj) )
+            pIfObj->iCopy = Gia_ManAppendCi(pNew);
+        else if ( If_ObjIsCo(pIfObj) )
+            pIfObj->iCopy = Gia_ManAppendCo( pNew, Abc_LitNotCond(If_ObjFanin0(pIfObj)->iCopy, If_ObjFaninC0(pIfObj)) );
+        else if ( If_ObjIsConst1(pIfObj) )
+        {
+            pIfObj->iCopy = 1;
+            nItems += 2; 
+        }
+        else assert( 0 );
     }
     Vec_IntFree( vLeaves );
-    Vec_IntFree( vTruth );
-    Vec_IntFree( vVisited );
-    Vec_IntFreeP( &p->vTruths );
-    nTotal = 0;
-    for ( i = 0; i < 222; i++ )
-        nTotal += ClassCounts[i];
-    Abc_Print( 1, "NPN CLASS STATISTICS (for %d LUT4 present in the current mapping):\n", nTotal );
-    OtherClasses = 0;
-    for ( i = 0; i < 222; i++ )
+    Gia_ManHashStop( pNew );
+
+    // GIA after mapping with choices may end up with dangling nodes
+    // which participate as leaves of some cuts used in the mapping
+    // such nodes are marked here and skipped when mapping is derived
+    Counter = Gia_ManMarkDangling(pNew);
+    if ( pIfMan->pPars->fVerbose && Counter )
+        printf( "GIA after mapping has %d dangling nodes.\n", Counter );
+
+    // create mapping
+    iOffset = Gia_ManObjNum(pNew);
+    pNew->pMapping = ABC_CALLOC( int, iOffset + nItems );
+    assert( pNew->vTruths == NULL );
+    if ( pIfMan->pPars->pLutStruct )
+        pNew->vTruths = Vec_IntAlloc( 1000 );
+    If_ManForEachObj( pIfMan, pIfObj, i )
     {
-        if ( ClassCounts[i] == 0 )
-            continue;
-        if ( 100.0 * ClassCounts[i] / (nTotal+1) < 0.1 ) // do not show anything below 0.1 percent
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
             continue;
-        OtherClasses += ClassCounts[i];
-        Abc_Print( 1, "Class %3d :  Count = %6d   (%7.2f %%)   %s\n", 
-            i, ClassCounts[i], 100.0 * ClassCounts[i] / (nTotal+1), pNames[i] );
+        if ( If_ObjIsAnd(pIfObj) )
+        {
+            GiaId = Abc_Lit2Var( pIfObj->iCopy );
+            assert( Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) );
+            if ( !Gia_ManObj(pNew, GiaId)->fMark0 ) // skip dangling node
+                continue;
+            // get the best cut
+            pCutBest = If_ObjCutBest( pIfObj );
+            // copy the truth tables
+            pTruth = NULL;
+            if ( pNew->vTruths )
+            { 
+                // copy truth table
+                for ( w = 0; w < pIfMan->nTruthWords; w++ )
+                    Vec_IntPush( pNew->vTruths, If_CutTruth(pCutBest)[w] );
+                pTruth = (unsigned *)(Vec_IntArray(pNew->vTruths) + Vec_IntSize(pNew->vTruths) - pIfMan->nTruthWords);
+                // complement 
+                if ( pCutBest->fCompl ^ Abc_LitIsCompl(pIfObj->iCopy) )
+                    for ( w = 0; w < pIfMan->nTruthWords; w++ )
+                        pTruth[w] = ~pTruth[w];
+            }
+            // create node
+            pNew->pMapping[GiaId]     = iOffset;
+            pNew->pMapping[iOffset++] = If_CutLeaveNum(pCutBest);
+            If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
+            {
+                GiaId = Abc_Lit2Var(pIfLeaf->iCopy);
+                if ( pTruth && Abc_LitIsCompl(pIfLeaf->iCopy) )
+                    Kit_TruthChangePhase( pTruth, If_CutLeaveNum(pCutBest), k );
+                if ( !Gia_ManObj(pNew, GiaId)->fMark0 ) // skip dangling node
+                {
+                    // update truth table
+                    if ( pTruth )
+                    {
+                        extern void If_CluSwapVars( word * pTruth, int nVars, int * V2P, int * P2V, int iVar, int jVar );
+                        if ( If_CutLeaveNum(pCutBest) >= 6 )
+                            If_CluSwapVars( (word*)pTruth, If_CutLeaveNum(pCutBest), NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
+                        else
+                        {
+                            word Truth = (pTruth[0] << 32) | pTruth[0];
+                            If_CluSwapVars( &Truth, 6, NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
+                            pTruth[0] = (Truth & 0xFFFFFFFF);
+                        }
+                    }
+                    pNew->pMapping[iOffset-k-1]--;
+                    continue;
+                }
+                pNew->pMapping[iOffset++] = GiaId;
+            }
+            pNew->pMapping[iOffset++] = GiaId;
+        }
+        else if ( If_ObjIsConst1(pIfObj) )
+        {
+            // create node
+            pNew->pMapping[0] = iOffset;
+            pNew->pMapping[iOffset++] = 0;
+            pNew->pMapping[iOffset++] = 0;
+/*
+            if ( pNew->vTruths )
+            {
+                printf( "%d ", nLeaves );
+                for ( w = 0; w < pIfMan->nTruthWords; w++ )
+                    Vec_IntPush( pNew->vTruths, 0 );
+            }
+*/
+        }
     }
-    OtherClasses = nTotal - OtherClasses;
-    Abc_Print( 1, "Other     :  Count = %6d   (%7.2f %%)\n", 
-        OtherClasses, 100.0 * OtherClasses / (nTotal+1) );
-    // count the number of LUTs that have MUX function and two fanins with MUX functions
-    OtherClasses = OtherClasses2 = 0;
-    ABC_FREE( p->pRefs );
-    Gia_ManSetRefsMapped( p );
-    Gia_ManForEachLut( p, i )
+    Gia_ManCleanMark0( pNew );
+//    assert( iOffset == Gia_ManObjNum(pNew) + nItems );
+    if ( pIfMan->pManTim )
+        pNew->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    // verify that COs have mapping
     {
-        if ( pLutClass[i] != 109 )
-            continue;
-        Counter = Counter2 = 0;
-        Gia_LutForEachFanin( p, i, iFan, k )
+        Gia_Obj_t * pObj;
+        Gia_ManForEachCo( pNew, pObj, i )
         {
-            Counter  += (pLutClass[iFan] == 109);
-            Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
+            if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
+                assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
         }
-        OtherClasses  += (Counter > 1);
-        OtherClasses2 += (Counter2 > 1);
-//            Abc_Print( 1, "%d -- ", pLutClass[i] );
-//            Gia_LutForEachFanin( p, i, iFan, k )
-//                Abc_Print( 1, "%d ", pLutClass[iFan] );
-//            Abc_Print( 1, "\n" );
     }
-    ABC_FREE( p->pRefs );
-    Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d  (%7.2f %%)  MFFC = %6d  (%7.2f %%)\n", 
-        OtherClasses,  100.0 * OtherClasses  / (nTotal+1),
-        OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
-    ABC_FREE( pLutClass );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interface of LUT mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
+{
+    Gia_Man_t * pNew;
+    If_Man_t * pIfMan;
+    If_Par_t * pPars = (If_Par_t *)pp;
+    // set the arrival times
+    assert( pPars->pTimesArr == NULL );
+    pPars->pTimesArr = ABC_ALLOC( float, Gia_ManCiNum(p) );
+    memset( pPars->pTimesArr, 0, sizeof(float) * Gia_ManCiNum(p) );
+    // translate into the mapper
+    pIfMan = Gia_ManToIf( p, pPars );    
+    if ( pIfMan == NULL )
+        return NULL;
+    if ( p->pManTime )
+        pIfMan->pManTim = Tim_ManDup( p->pManTime, 0 );
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+    // transform the result of mapping into the new network
+    pNew = Gia_ManFromIf( pIfMan );
+    If_ManStop( pIfMan );
+    // transfer name
+    assert( pNew->pName == NULL );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // unmap in case of SOP balancing
+//    if ( pIfMan->pPars->fDelayOpt )
+//        Vec_IntFreeP( &pNew->vMapping );
+    return pNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index f82e7952..0ae484fc 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -21,6 +21,7 @@
 #include "gia.h"
 #include "misc/tim/tim.h"
 #include "proof/abs/abs.h"
+#include "opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -277,6 +278,7 @@ void Gia_ManPrintChoiceStats( Gia_Man_t * p )
         assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
     }
     Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
+    Gia_ManCleanMark0( p );
 }
 
 /**Function*************************************************************
@@ -459,6 +461,96 @@ void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints NPN class statistics.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintNpnClasses( Gia_Man_t * p )
+{
+    extern char ** Kit_DsdNpn4ClassNames();
+    char ** pNames = Kit_DsdNpn4ClassNames();
+    Vec_Int_t * vLeaves, * vTruth, * vVisited;
+    int * pLutClass, ClassCounts[222] = {0};
+    int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
+    unsigned * pTruth;
+    assert( p->pMapping != NULL );
+    assert(  Gia_ManLutSizeMax( p ) <= 4 );
+    vLeaves   = Vec_IntAlloc( 100 );
+    vVisited  = Vec_IntAlloc( 100 );
+    vTruth    = Vec_IntAlloc( (1<<16) );
+    pLutClass = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    Gia_ManCleanTruth( p );
+    Gia_ManForEachLut( p, i )
+    {
+        if ( Gia_ObjLutSize(p,i) > 4 )
+            continue;
+        Vec_IntClear( vLeaves );
+        Gia_LutForEachFanin( p, i, iFan, k )
+            Vec_IntPush( vLeaves, iFan );
+        for ( ; k < 4; k++ )
+            Vec_IntPush( vLeaves, 0 );
+        pTruth = Gia_ManConvertAigToTruth( p, Gia_ManObj(p, i), vLeaves, vTruth, vVisited );
+        Class = Dar_LibReturnClass( *pTruth );
+        ClassCounts[ Class ]++;
+        pLutClass[i] = Class;
+    }
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vTruth );
+    Vec_IntFree( vVisited );
+    Vec_IntFreeP( &p->vTruths );
+    nTotal = 0;
+    for ( i = 0; i < 222; i++ )
+        nTotal += ClassCounts[i];
+    Abc_Print( 1, "NPN CLASS STATISTICS (for %d LUT4 present in the current mapping):\n", nTotal );
+    OtherClasses = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        if ( ClassCounts[i] == 0 )
+            continue;
+        if ( 100.0 * ClassCounts[i] / (nTotal+1) < 0.1 ) // do not show anything below 0.1 percent
+            continue;
+        OtherClasses += ClassCounts[i];
+        Abc_Print( 1, "Class %3d :  Count = %6d   (%7.2f %%)   %s\n", 
+            i, ClassCounts[i], 100.0 * ClassCounts[i] / (nTotal+1), pNames[i] );
+    }
+    OtherClasses = nTotal - OtherClasses;
+    Abc_Print( 1, "Other     :  Count = %6d   (%7.2f %%)\n", 
+        OtherClasses, 100.0 * OtherClasses / (nTotal+1) );
+    // count the number of LUTs that have MUX function and two fanins with MUX functions
+    OtherClasses = OtherClasses2 = 0;
+    ABC_FREE( p->pRefs );
+    Gia_ManSetRefsMapped( p );
+    Gia_ManForEachLut( p, i )
+    {
+        if ( pLutClass[i] != 109 )
+            continue;
+        Counter = Counter2 = 0;
+        Gia_LutForEachFanin( p, i, iFan, k )
+        {
+            Counter  += (pLutClass[iFan] == 109);
+            Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1);
+        }
+        OtherClasses  += (Counter > 1);
+        OtherClasses2 += (Counter2 > 1);
+//            Abc_Print( 1, "%d -- ", pLutClass[i] );
+//            Gia_LutForEachFanin( p, i, iFan, k )
+//                Abc_Print( 1, "%d ", pLutClass[iFan] );
+//            Abc_Print( 1, "\n" );
+    }
+    ABC_FREE( p->pRefs );
+    Abc_Print( 1, "Approximate number of 4:1 MUX structures: All = %6d  (%7.2f %%)  MFFC = %6d  (%7.2f %%)\n", 
+        OtherClasses,  100.0 * OtherClasses  / (nTotal+1),
+        OtherClasses2, 100.0 * OtherClasses2 / (nTotal+1) );
+    ABC_FREE( pLutClass );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index bc3399e0..6dc06f19 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -377,12 +377,12 @@ int Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
         }
         if ( Abc_ObjFaninNum(pObj) != 1 )
         {
-            fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: A PO \"%s\" does not have one fanin (but %d).\n", Abc_ObjName(pObj), Abc_ObjFaninNum(pObj) );
             return 0;
         }
         if ( Abc_ObjFanoutNum(pObj) > 0 )
         {
-            fprintf( stdout, "NetworkCheck: A PO \"%s\" has fanouts.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: A PO \"%s\" has %d fanout(s).\n", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
             return 0;
         }
         pObj->pCopy = (Abc_Obj_t *)1;
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 5fb22d79..2669ae0c 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -87,20 +87,13 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     assert( !Abc_ObjIsComplement(pObj) );
     assert( pObj->pNtk == pFaninR->pNtk );
     assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
+    assert( !Abc_ObjIsPi(pObj) && !Abc_ObjIsPo(pFanin) );    // fanin of PI or fanout of PO
+    assert( !Abc_ObjIsCo(pObj) || !Abc_ObjFaninNum(pObj) );  // CO with two fanins
+    assert( !Abc_ObjIsNet(pObj) || !Abc_ObjFaninNum(pObj) ); // net with two fanins
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pObj->vFanins,     pFaninR->Id );
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
-    if ( Abc_ObjIsNet(pObj) && Abc_ObjFaninNum(pObj) > 1 )
-    {
-        printf( "Abc_ObjAddFanin(): Error! Creating net \"%s\" with two fanins.\n", Abc_ObjName(pObj) );
-    }
-/*
-    if ( Abc_ObjIsCo(pFanin) )
-    {
-        printf( "Abc_ObjAddFanin(): Error! Creating fanout of a CO.\n", Abc_ObjName(pFanin) );
-    }
-*/
 }
 
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 46ae90a4..84f6ade2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14392,7 +14392,7 @@ usage:
     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-u       : toggles the use of MUXes along with LUTs [default = %s]\n", fLutMux? "yes": "no" );
-    Abc_Print( -2, "\t-g       : toggles global delay optimization [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
+    Abc_Print( -2, "\t-g       : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
     Abc_Print( -2, "\t-y       : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
     Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
     Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
@@ -22697,7 +22697,12 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( Gia_ManHasDangling(pAbc->pGia) == 0 )
+    if ( pAbc->pGia->pMapping )
+    {
+        extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p );
+        pNtk = Abc_NtkFromMappedGia( pAbc->pGia );
+    }
+    else if ( Gia_ManHasDangling(pAbc->pGia) == 0 )
     {
         pMan = Gia_ManToAig( pAbc->pGia, 0 );
         pNtk = Abc_NtkFromAigPhase( pMan );
@@ -26210,20 +26215,18 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[200];
     char LutSize[200];
+    Gia_Man_t * pNew;
     If_Par_t Pars, * pPars = &Pars;
     int c;
-    extern void Gia_ManSetIfParsDefault( If_Par_t * pPars );
-    extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars );
     // set defaults
     Gia_ManSetIfParsDefault( pPars );
-//    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;
+    if ( pAbc->pLibLut == NULL )
+    {
+        Abc_Print( -1, "LUT library is not given. Using default LUT library.\n" );
+        pAbc->pLibLut = If_SetSimpleLutLib( 6 );
+    }
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrsdbvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbgyojikcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26273,6 +26276,17 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nAreaIters < 0 ) 
                 goto usage;
             break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by a positive integer no less than 3.\n" );
+                goto usage;
+            }
+            pPars->nGateSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nGateSize < 2 ) 
+                goto usage;
+            break;
         case 'D':
             if ( globalUtilOptind >= argc )
             {
@@ -26295,6 +26309,31 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 ) 
                 goto usage;
             break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->WireDelay = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->WireDelay < 0.0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
+                goto usage;
+            }
+            pPars->pLutStruct = argv[globalUtilOptind];
+            globalUtilOptind++;
+            if ( strlen(pPars->pLutStruct) != 2 && strlen(pPars->pLutStruct) != 3 ) 
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by a 2- or 3-char string (e.g. \"44\" or \"555\").\n" );
+                goto usage;
+            }
+            break;
         case 'q':
             pPars->fPreprocess ^= 1;
             break;
@@ -26328,6 +26367,27 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fUseBat ^= 1;
             break;
+        case 'g':
+            pPars->fDelayOpt ^= 1;
+            break;
+        case 'y':
+            pPars->fUserRecLib ^= 1;
+            break;
+        case 'o':
+            pPars->fUseBuffs ^= 1;
+            break;
+        case 'j':
+            pPars->fEnableCheck07 ^= 1;
+            break;
+        case 'i':
+            pPars->fEnableCheck08 ^= 1;
+            break;
+        case 'k':
+            pPars->fEnableCheck10 ^= 1;
+            break;
+        case 'c':
+            pPars->fEnableRealPos ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26336,12 +26396,27 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9If(): There is no AIG to map.\n" );
+        Abc_Print( -1, "Empty GIA network.\n" );
         return 1;
     }
 
+    if ( pPars->nLutSize == -1 )
+    {
+        if ( pPars->pLutLib == NULL )
+        {
+            Abc_Print( -1, "The LUT library is not given.\n" );
+            return 1;
+        }
+        // get LUT size from the library
+        pPars->nLutSize = pPars->pLutLib->LutMax;
+        // if variable pin delay, force truth table computation
+//        if ( pPars->pLutLib->fVarPinDelays )
+//            pPars->fTruth = 1;
+    }
+
     if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
     {
         Abc_Print( -1, "Incorrect LUT size (%d).\n", pPars->nLutSize );
@@ -26355,9 +26430,10 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // enable truth table computation if choices are selected
-    if ( (c = Gia_ManCountChoiceNodes( pAbc->pGia )) )
+    if ( Gia_ManHasChoices(pAbc->pGia) )
     {
-        Abc_Print( 0, "Performing LUT mapping with %d choices.\n", c );
+        if ( !Abc_FrameReadFlag("silentmode") )
+            Abc_Print( 0, "Performing LUT mapping with choices.\n" );
         pPars->fExpRed = 0;
     }
 
@@ -26371,12 +26447,86 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->fCutMin = 1;            
     }
 
+    if ( pPars->fEnableCheck07 + pPars->fEnableCheck08 + pPars->fEnableCheck10 + (pPars->pLutStruct != NULL) > 1 )
+    {
+        Abc_Print( -1, "Only one additional check can be performed at the same time.\n" );
+        return 1;
+    }
+    if ( pPars->fEnableCheck07 )
+    {
+        if ( pPars->nLutSize < 6 || pPars->nLutSize > 7 )
+        {
+            Abc_Print( -1, "This feature only works for {6,7}-LUTs.\n" );
+            return 1;
+        }
+        pPars->pFuncCell = If_CutPerformCheck07;
+        pPars->fCutMin = 1;            
+    }
+    if ( pPars->fEnableCheck08 )
+    {
+        if ( pPars->nLutSize < 6 || pPars->nLutSize > 8 )
+        {
+            Abc_Print( -1, "This feature only works for {6,7,8}-LUTs.\n" );
+            return 1;
+        }
+        pPars->pFuncCell = If_CutPerformCheck08;
+        pPars->fCutMin = 1;            
+    }
+    if ( pPars->fEnableCheck10 )
+    {
+        if ( pPars->nLutSize < 6 || pPars->nLutSize > 10 )
+        {
+            Abc_Print( -1, "This feature only works for {6,7,8,9,10}-LUTs.\n" );
+            return 1;
+        }
+        pPars->pFuncCell = If_CutPerformCheck10;
+        pPars->fCutMin = 1;            
+    }
+    if ( pPars->pLutStruct )
+    {
+        if ( pPars->nLutSize < 6 || pPars->nLutSize > 16 )
+        {
+            Abc_Print( -1, "This feature only works for [6;16]-LUTs.\n" );
+            return 1;
+        }
+        pPars->pFuncCell = If_CutPerformCheck16;
+        pPars->fCutMin = 1;            
+    }
+
     // enable truth table computation if cut minimization is selected
     if ( pPars->fCutMin )
     {
         pPars->fTruth = 1;
         pPars->fExpRed = 0;
     }
+    // modify the subgraph recording
+    if ( pPars->fUserRecLib )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fExpRed     =  0;
+        pPars->fUsePerm    =  1;
+        pPars->pLutLib     =  NULL;
+    }
+    // modify for global delay optimization
+    if ( pPars->fDelayOpt )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fExpRed     =  0;
+        pPars->fUsePerm    =  1;
+        pPars->pLutLib     =  NULL;
+    }
+    // modify for global delay optimization
+    if ( pPars->nGateSize > 0 )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fExpRed     =  0;
+        pPars->fUsePerm    =  1;
+        pPars->pLutLib     =  NULL;
+        pPars->nLutSize    =  pPars->nGateSize; 
+    }
 
     // complain if truth tables are requested but the cut size is too large
     if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
@@ -26385,11 +26535,14 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( !Gia_MappingIf( pAbc->pGia, pPars ) )
+    // perform mapping
+    pNew = Gia_ManPerformMapping( pAbc->pGia, pPars );
+    if ( pNew == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9If(): Mapping of the AIG has failed.\n" );
         return 1;
     }
+    Abc_CommandUpdate9( pAbc, pNew );
     return 0;
 
 usage:
@@ -26401,14 +26554,17 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    Abc_Print( -2, "usage: &if [-KCFA num] [-DE float] [-qarlepmdbvh]\n" );
+    Abc_Print( -2, "usage: &if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbgyojikcvh]\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-G num   : the max AND/OR gate size for mapping (0 = unused) [default = %d]\n", pPars->nGateSize );
     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-W float : sets wire delay between adjects LUTs [default = %f]\n", pPars->WireDelay );  
+    Abc_Print( -2, "\t-S str   : string representing the LUT structure [default = %s]\n", pPars->pLutStruct ? pPars->pLutStruct : "not used" );  
     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" );
@@ -26417,9 +26573,16 @@ usage:
     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-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-g       : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" );
+    Abc_Print( -2, "\t-y       : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
+    Abc_Print( -2, "\t-o       : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
+    Abc_Print( -2, "\t-j       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
+    Abc_Print( -2, "\t-i       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck08? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck10? "yes": "no" );
+    Abc_Print( -2, "\t-c       : toggles enabling additional feature [default = %s]\n", pPars->fEnableRealPos? "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;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 6072a9db..dbb75f59 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -620,6 +620,150 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
     return pNtkNew;
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_ObjHopFromGia_rec( Hop_Man_t * pHopMan, Gia_Man_t * p, int Id, Vec_Ptr_t * vCopies )
+{
+    Gia_Obj_t * pObj;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    if ( Gia_ObjIsTravIdCurrentId(p, Id) )
+        return (Hop_Obj_t *)Vec_PtrEntry( vCopies, Id );
+    Gia_ObjSetTravIdCurrentId(p, Id);
+    pObj = Gia_ManObj(p, Id);
+    assert( Gia_ObjIsAnd(pObj) );
+    // compute the functions of the children
+    gFunc0 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId0(pObj, Id), vCopies );
+    gFunc1 = Abc_ObjHopFromGia_rec( pHopMan, p, Gia_ObjFaninId1(pObj, Id), vCopies );
+    // get the function of the cut
+    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, Gia_ObjFaninC0(pObj)), Hop_NotCond(gFunc1, Gia_ObjFaninC1(pObj)) );  
+    Vec_PtrWriteEntry( vCopies, Id, gFunc );
+    return gFunc;
+}
+Hop_Obj_t * Abc_ObjHopFromGia( Hop_Man_t * pHopMan, Gia_Man_t * p, int GiaId, Vec_Ptr_t * vCopies )
+{
+    int k, iFan;
+    assert( Gia_ObjIsLut(p, GiaId) );
+    assert( Gia_ObjLutSize(p, GiaId) > 0 );
+    Gia_ManIncrementTravId( p );
+    Gia_LutForEachFanin( p, GiaId, iFan, k )
+    {
+        Gia_ObjSetTravIdCurrentId(p, iFan);
+        Vec_PtrWriteEntry( vCopies, iFan, Hop_IthVar(pHopMan, k) );
+    }
+    return Abc_ObjHopFromGia_rec( pHopMan, p, GiaId, vCopies );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the mapped GIA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
+{
+    int fVerbose = 0;
+    int fDuplicate = 0;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObjNew, * pObjNewLi, * pObjNewLo, * pConst0 = NULL;
+    Gia_Obj_t * pObj, * pObjLi, * pObjLo;
+    Vec_Ptr_t * vReflect;
+    int i, k, iFan, nDupGates; 
+    assert( p->pMapping != NULL );
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(p->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(p->pSpec);
+    Gia_ManFillValue( p );
+    // create constant
+    pConst0 = Abc_NtkCreateNodeConst0( pNtkNew );
+    Gia_ManConst0(p)->Value = Abc_ObjId(pConst0);
+    // create PIs
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->Value = Abc_ObjId( Abc_NtkCreatePi( pNtkNew ) );
+    // create POs
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Abc_ObjId( Abc_NtkCreatePo( pNtkNew ) );
+    // create as many latches as there are registers in the manager
+    Gia_ManForEachRiRo( p, pObjLi, pObjLo, i )
+    {
+        pObjNew = Abc_NtkCreateLatch( pNtkNew );
+        pObjNewLi = Abc_NtkCreateBi( pNtkNew );
+        pObjNewLo = Abc_NtkCreateBo( pNtkNew );
+        Abc_ObjAddFanin( pObjNew, pObjNewLi );
+        Abc_ObjAddFanin( pObjNewLo, pObjNew );
+        pObjLi->Value = Abc_ObjId( pObjNewLi );
+        pObjLo->Value = Abc_ObjId( pObjNewLo );
+        Abc_LatchSetInit0( pObjNew );
+    }
+    // rebuild the AIG
+    vReflect = Vec_PtrStart( Gia_ManObjNum(p) );
+    Gia_ManForEachLut( p, i )
+    {
+        pObj = Gia_ManObj(p, i);
+        assert( pObj->Value == ~0 );
+        if ( Gia_ObjLutSize(p, i) == 0 )
+        {
+            pObj->Value = Abc_ObjId(pConst0);
+            continue;
+        }
+        pObjNew = Abc_NtkCreateNode( pNtkNew );
+        Gia_LutForEachFanin( p, i, iFan, k )
+            Abc_ObjAddFanin( pObjNew, Abc_NtkObj(pNtkNew, Gia_ObjValue(Gia_ManObj(p, iFan))) );
+        pObjNew->pData = Abc_ObjHopFromGia( pNtkNew->pManFunc, p, i, vReflect );
+        pObj->Value = Abc_ObjId( pObjNew );
+    }
+    Vec_PtrFree( vReflect );
+    // connect the PO nodes
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        pObjNew = Abc_NtkObj( pNtkNew, Gia_ObjValue(Gia_ObjFanin0(pObj)) );
+        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), Abc_ObjNotCond( pObjNew, Gia_ObjFaninC0(pObj) ) );
+    }
+    // create names
+    Abc_NtkAddDummyPiNames( pNtkNew );
+    Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyBoxNames( pNtkNew );
+
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, fDuplicate );
+    if ( fVerbose && nDupGates && !Abc_FrameReadFlag("silentmode") )
+    {
+        if ( !fDuplicate )
+            printf( "Added %d buffers/inverters to decouple the CO drivers.\n", nDupGates );
+        else
+            printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+    }
+    // remove const node if it is not used
+    if ( Abc_ObjFanoutNum(pConst0) == 0 )
+        Abc_NtkDeleteObj( pConst0 );
+
+    assert( Gia_ManPiNum(p) == Abc_NtkPiNum(pNtkNew) );
+    assert( Gia_ManPoNum(p) == Abc_NtkPoNum(pNtkNew) );
+    assert( Gia_ManRegNum(p) == Abc_NtkLatchNum(pNtkNew) );
+
+    // check the resulting AIG
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        Abc_Print( 1, "Abc_NtkFromMappedGia(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 362f0e46..46c1374b 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -228,7 +228,6 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
         {
-            pIfMan->nChoices++;
             for ( pPrev = pNode, pFanin = (Abc_Obj_t *)pNode->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 4db982f0..f30a13e5 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -111,7 +111,7 @@ struct Abc_Frame_t_
     void *          pAbc85Ntl2;
     void *          pAbc85Best;
     void *          pAbc85Delay;
-    If_Lib_t *      pAbc85Lib;
+//    If_Lib_t *      pAbc85Lib;
 
     EXT_ABC_FRAME   // plugin for external functionality
 };
diff --git a/src/map/if/if.h b/src/map/if/if.h
index f74a59da..24910d75 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -333,7 +333,7 @@ static inline void *     If_ObjCopy( If_Obj_t * pObj )                       { r
 static inline int        If_ObjLevel( If_Obj_t * pObj )                      { return pObj->Level;                   }
 static inline void       If_ObjSetLevel( If_Obj_t * pObj, int Level )        { pObj->Level = Level;                  }
 static inline void       If_ObjSetCopy( If_Obj_t * pObj, void * pCopy )      { pObj->pCopy = pCopy;                  }
-static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu;                  }
+static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { assert( pObj->Id > pEqu->Id ); pObj->pEquiv = pEqu;                  }
 
 static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return &pObj->CutBest;                }
 static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { return (1 << (ObjId % 31));           }
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 3028e370..6946afa1 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -337,6 +337,7 @@ void If_ManCreateChoice( If_Man_t * p, If_Obj_t * pObj )
     // mark the largest level
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    p->nChoices++;
 }
 
 /**Function*************************************************************
diff --git a/src/opt/nwk/nwkMap.c b/src/opt/nwk/nwkMap.c
index e80c4c93..e8be5a2d 100644
--- a/src/opt/nwk/nwkMap.c
+++ b/src/opt/nwk/nwkMap.c
@@ -163,7 +163,6 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
         // set up the choice node
         if ( Aig_ObjIsChoice( p, pNode ) )
         {
-            pIfMan->nChoices++;
             for ( pPrev = pNode, pFanin = Aig_ObjEquiv(p, pNode); pFanin; pPrev = pFanin, pFanin = Aig_ObjEquiv(p, pFanin) )
                 If_ObjSetChoice( (If_Obj_t *)pPrev->pData, (If_Obj_t *)pFanin->pData );
             If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pData );
diff --git a/src/proof/llb/llb4Map.c b/src/proof/llb/llb4Map.c
index 51f1fec6..4b46f308 100644
--- a/src/proof/llb/llb4Map.c
+++ b/src/proof/llb/llb4Map.c
@@ -48,7 +48,7 @@ Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
 {
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
     extern If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
-    extern void        Gia_ManSetIfParsDefault( If_Par_t * pPars );
+    extern void        Gia_ManSetIfParsDefault( void * pPars );
     If_Par_t Pars, * pPars = &Pars;
     If_Man_t * pIfMan;
     If_Obj_t * pAnd;