Merge

9 files changed, 901 insertions, 357 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b3efa455..35d80047 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -117,6 +117,7 @@ struct Gia_Man_t_
     int *          pReprsOld;     // representatives (for CIs and ANDs)
     Gia_Rpr_t *    pReprs;        // representatives (for CIs and ANDs)
     int *          pNexts;        // next nodes in the equivalence classes
+    int *          pSibls;        // next nodes in the choice nodes
     int *          pIso;          // pairs of structurally isomorphic nodes
     int            nTerLoop;      // the state where loop begins  
     int            nTerStates;    // the total number of ternary states
@@ -481,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
@@ -570,6 +578,8 @@ static inline void        Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ a
 static inline void        Gia_ObjUnsetRepr( Gia_Man_t * p, int Id )          { p->pReprs[Id].iRepr = GIA_VOID;                                            }
 static inline int         Gia_ObjHasRepr( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr != GIA_VOID;                                    }
 static inline int         Gia_ObjReprSelf( Gia_Man_t * p, int Id )           { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id;                    }
+static inline int         Gia_ObjSibl( Gia_Man_t * p, int Id )               { return p->pSibls ? p->pSibls[Id] : 0;                                      }
+static inline Gia_Obj_t * Gia_ObjSiblObj( Gia_Man_t * p, int Id )            { return (p->pSibls && p->pSibls[Id]) ? Gia_ManObj(p, p->pSibls[Id]) : NULL; }
 
 static inline int         Gia_ObjProved( Gia_Man_t * p, int Id )             { return p->pReprs[Id].fProved;       }
 static inline void        Gia_ObjSetProved( Gia_Man_t * p, int Id )          { p->pReprs[Id].fProved = 1;          }
@@ -697,6 +707,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 ============================================================*/
@@ -807,7 +818,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 );
@@ -823,12 +841,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 );
@@ -857,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 ===========================================================*/
@@ -906,7 +920,7 @@ extern int                 Gia_ManLevelNum( Gia_Man_t * p );
 extern void                Gia_ManCreateValueRefs( Gia_Man_t * p );
 extern void                Gia_ManCreateRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
-extern int                 Gia_ManCrossCut( Gia_Man_t * p );
+extern int                 Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
 extern int                 Gia_ManIsNormalized( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );
@@ -920,6 +934,7 @@ extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ManPrint( Gia_Man_t * p );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
+extern void                Gia_ManMarkFanoutDrivers( Gia_Man_t * p );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 224d3bda..5dcc6038 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -42,7 +42,7 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Derives combinational miter of the two AIGs.]
+  Synopsis    [Duplicates AIG in the DFS order.]
 
   Description []
                
@@ -70,6 +70,34 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
             pNew->pNexts[iObjNew] = iNextNew;        
     }
 }
+Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Gia_ManStart( Aig_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
+    // create room to store equivalences
+    if ( p->pEquivs )
+        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->iData = 1;
+    Aig_ManForEachCi( p, pObj, i )
+        pObj->iData = Gia_ManAppendCi( pNew );
+    // add logic for the POs
+    Aig_ManForEachCo( p, pObj, i )
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+    Aig_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    if ( pNew->pNexts )
+        Gia_ManDeriveReprs( pNew );
+    return pNew;
+}
 
 /**Function*************************************************************
 
@@ -82,19 +110,38 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
+void Gia_ManFromAigChoices_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj == NULL || pObj->iData )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
+    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+    if ( Aig_ObjEquiv(p, pObj) )
+    {
+        int iObjNew, iNextNew;
+        iObjNew  = Abc_Lit2Var(pObj->iData);
+        iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
+        assert( iObjNew > iNextNew );
+        assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
+        pNew->pSibls[iObjNew] = iNextNew;        
+    }
+}
+Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
 {
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
+    assert( p->pEquivs != NULL );
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
-    if ( p->pEquivs )
-        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
+    pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
@@ -102,12 +149,11 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
         pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachCo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    if ( pNew->pNexts )
-        Gia_ManDeriveReprs( pNew );
+    assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
     return pNew;
 }
 
@@ -195,7 +241,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives combinational miter of the two AIGs.]
+  Synopsis    [Duplicates AIG in the DFS order.]
 
   Description []
                
@@ -228,18 +274,6 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
             pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
     }
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates AIG in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
 {
     Aig_Man_t * pNew;
@@ -541,7 +575,8 @@ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars )
     Aig_Man_t * pNew;
     pNew = Gia_ManToAig( p, 0 );
     pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
-    pGia = Gia_ManFromAig( pNew );
+//    pGia = Gia_ManFromAig( pNew );
+    pGia = Gia_ManFromAigChoices( pNew );
     Aig_ManStop( pNew );
     return pGia;
 }
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index b72f6415..6498ec52 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -51,6 +51,7 @@ ABC_NAMESPACE_HEADER_START
 
 /*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
+extern Gia_Man_t *         Gia_ManFromAigChoices( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSimple( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
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/giaFront.c b/src/aig/gia/giaFront.c
index 322da785..fc99cfe9 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -103,13 +103,54 @@ void Gia_ManFrontTransform( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManCrossCutSimple( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nCutCur = 0, nCutMax = 0;
+    Gia_ManCreateValueRefs( p );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( pObj->Value )
+            nCutCur++;
+        if ( nCutMax < nCutCur )
+            nCutMax = nCutCur;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+                nCutCur--;
+            if ( --Gia_ObjFanin1(pObj)->Value == 0 )
+                nCutCur--;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            if ( --Gia_ObjFanin0(pObj)->Value == 0 )
+                nCutCur--;
+        }
+    }
+//    Gia_ManForEachObj( p, pObj, i )
+//        assert( pObj->Value == 0 );
+    return nCutMax;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Determine the frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj, * pFanin0New, * pFanin1New, * pObjNew;
     char * pFront;    // places used for the frontier
     int i, iLit, nCrossCut = 0, nCrossCutMax = 0;
-    int nCrossCutMaxInit = Gia_ManCrossCut( p );
+    int nCrossCutMaxInit = Gia_ManCrossCutSimple( p );
     int iFront = 0;//, clk = clock(); 
     // set references for all objects
     Gia_ManCreateValueRefs( p );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 13e4f429..deab1a60 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
 
@@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+extern int Abc_RecToGia2( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_t * pIfObj, Vec_Int_t * vLeaves, int fHash );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,44 +48,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 +98,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 +117,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 +136,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 +155,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 +187,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 +211,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 +250,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 +318,47 @@ 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, int fHash )
 {
-    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 = -1;
+    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 ); 
+        if ( fHash )
+            iRes  = Gia_ManHashAnd( pNew, iRes0, iRes1 );
+        else
+            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 fHash )
+{
+    int iResult;
+    Vec_Wrd_t * vArray;
+    vArray  = If_CutDelaySopArray( p, pCut );
+    iResult = Gia_ManNodeIfSopToGiaInt( pNew, vArray, If_CutLeaveNum(pCut), vLeaves, fHash );
+//    Vec_WrdFree( vArray );
+    return iResult;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Assigns levels.]
+  Synopsis    [Recursively derives the local AIG for the cut.]
 
   Description []
                
@@ -422,22 +367,74 @@ 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, int fHash )
 {
-    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, fHash );
+        if ( iFunc0 == ~0 )
+            continue;
+        iFunc1 = Gia_ManNodeIfToGia_rec( pNew, pIfMan, pTemp->pFanin1, vVisited, fHash );
+        if ( iFunc1 == ~0 )
+            continue;
+        // both branches are solved
+        if ( fHash )
+            iFunc = Gia_ManHashAnd( pNew, Abc_LitNotCond(iFunc0, pTemp->fCompl0), Abc_LitNotCond(iFunc1, pTemp->fCompl1) ); 
+        else
+            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, int fHash )
+{
+    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, fHash ); 
+    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 +443,212 @@ 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;
+    int fHash = 0;
+    Gia_Man_t * pNew;
+    If_Obj_t * pIfObj, * pIfLeaf;
+    If_Cut_t * pCutBest;
+    Vec_Int_t * vLeaves;
+    Vec_Int_t * vCover;
     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
+    vCover = Vec_IntAlloc( 1 << 16 );
+    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->pLutStruct )
+                pIfObj->iCopy = Kit_TruthToGia( pNew, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, vLeaves, fHash );
+            else if ( pIfMan->pPars->fDelayOpt )
+                pIfObj->iCopy = Gia_ManNodeIfSopToGia( pNew, pIfMan, pCutBest, vLeaves, fHash );
+            else if ( pIfMan->pPars->fUserRecLib )
+                pIfObj->iCopy = Abc_RecToGia2( pNew, pIfMan, pCutBest, pIfObj, vLeaves, fHash );
+            else
+                pIfObj->iCopy = Gia_ManNodeIfToGia( pNew, pIfMan, pIfObj, vLeaves, fHash );
+            // complement the node if the TT was used and the cut was complemented
+            if ( pIfMan->pPars->pLutStruct )
+                pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+            // count entries in the mapping array
+            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( vCover );
     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 )
+    if ( 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 )
+        if ( pIfObj->nRefs == 0 && !If_ObjIsTerm(pIfObj) )
             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] );
+        if ( If_ObjIsAnd(pIfObj) )
+        { 
+            GiaId = Abc_Lit2Var( pIfObj->iCopy );
+            if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, GiaId)) ) // skip trivial node
+                continue;
+            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 )
+            {
+                int FaninId = Abc_Lit2Var(pIfLeaf->iCopy);
+                if ( pTruth && Abc_LitIsCompl(pIfLeaf->iCopy) )
+                    Kit_TruthChangePhase( pTruth, If_CutLeaveNum(pCutBest), k );
+                if ( !Gia_ManObj(pNew, FaninId)->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 = ((word)pTruth[0] << 32) | (word)pTruth[0];
+                            If_CluSwapVars( &Truth, 6, NULL, NULL, k, If_CutLeaveNum(pCutBest)-1 );
+                            pTruth[0] = (Truth & 0xFFFFFFFF);
+                        }
+                    }
+                    pNew->pMapping[iOffset-k-1]--;
+                    continue;
+                }
+                assert( FaninId < GiaId );
+                pNew->pMapping[iOffset++] = FaninId;
+            }
+            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 f78ea847..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
 
@@ -107,6 +108,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pReprsOld );
     ABC_FREE( p->pReprs );
     ABC_FREE( p->pNexts );
+    ABC_FREE( p->pSibls );
     ABC_FREE( p->pRefs );
 //    ABC_FREE( p->pNodeRefs );
     ABC_FREE( p->pHTable );
@@ -260,6 +262,36 @@ void Gia_ManPrintTents( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManPrintChoiceStats( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, nEquivs = 0, nChoices = 0;
+    Gia_ManMarkFanoutDrivers( p );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjSibl(p, i) )
+            continue;
+        nEquivs++;
+        if ( pObj->fMark0 )
+            nChoices++;
+        assert( !Gia_ObjSiblObj(p, i)->fMark0 );
+        assert( Gia_ObjIsAnd(Gia_ObjSiblObj(p, i)) );
+    }
+    Abc_Print( 1, "Choice stats: Equivs =%7d. Choices =%7d.\n", nEquivs, nChoices );
+    Gia_ManCleanMark0( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats for the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
 {
     if ( p->pName )
@@ -271,7 +303,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
         printf( "  ff =%7d", Gia_ManRegNum(p) );
     printf( "  and =%8d", Gia_ManAndNum(p) );
     printf( "  lev =%5d", Gia_ManLevelNum(p) ); Vec_IntFreeP( &p->vLevels );
-    printf( "  cut =%5d", Gia_ManCrossCut(p) );
+    printf( "  cut = %d(%d)", Gia_ManCrossCut(p, 0), Gia_ManCrossCut(p, 1) );
 //    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
     printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
     if ( Gia_ManHasDangling(p) )
@@ -289,6 +321,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
 //    Gia_ManSatExperiment( p );
     if ( p->pReprs && p->pNexts )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
+    if ( p->pSibls )
+        Gia_ManPrintChoiceStats( p );
     if ( p->pMapping )
         Gia_ManPrintMappingStats( p );
     if ( p->pPlacement )
@@ -427,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/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index 0aa255db..9b4c1c3e 100644
--- a/src/aig/gia/giaScl.c
+++ b/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*************************************************************
 
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index da713aa0..8389a9b0 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -550,12 +550,59 @@ int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManCrossCut( Gia_Man_t * p )
+void Gia_ManDfsForCrossCut_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
 {
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+        return;
+    }
+    if ( Gia_ObjIsCo(pObj) )
+    {
+        Gia_ObjFanin0(pObj)->Value++;
+        Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
+        Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ObjFanin0(pObj)->Value++;
+    Gia_ObjFanin1(pObj)->Value++;
+    Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin0(pObj), vNodes );
+    Gia_ManDfsForCrossCut_rec( p, Gia_ObjFanin1(pObj), vNodes );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+Vec_Int_t * Gia_ManDfsForCrossCut( Gia_Man_t * p, int fReverse )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManCleanValue( p );
+    vNodes = Vec_IntAlloc( Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    if ( fReverse )
+    {
+        Gia_ManForEachCoReverse( p, pObj, i )
+            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
+    }
+    else
+    {
+        Gia_ManForEachCo( p, pObj, i )
+            if ( !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+                Gia_ManDfsForCrossCut_rec( p, pObj, vNodes );
+    }
+    return vNodes;
+}
+int Gia_ManCrossCut( Gia_Man_t * p, int fReverse )
+{
+    Vec_Int_t * vNodes;
     Gia_Obj_t * pObj;
     int i, nCutCur = 0, nCutMax = 0;
-    Gia_ManCreateValueRefs( p );
-    Gia_ManForEachObj( p, pObj, i )
+    vNodes = Gia_ManDfsForCrossCut( p, fReverse );
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
     {
         if ( pObj->Value )
             nCutCur++;
@@ -574,8 +621,9 @@ int Gia_ManCrossCut( Gia_Man_t * p )
                 nCutCur--;
         }
     }
-//    Gia_ManForEachObj( p, pObj, i )
-//        assert( pObj->Value == 0 );
+    Vec_IntFree( vNodes );
+    Gia_ManForEachObj( p, pObj, i )
+        assert( pObj->Value == 0 );
     return nCutMax;
 }
 
@@ -1195,6 +1243,31 @@ int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Marks nodes that appear as faninis of other nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMarkFanoutDrivers( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManCleanMark0( p );
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////