New logic sharing extraction.

7 files changed, 626 insertions, 76 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 4f4985d4..3ec36358 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2791,6 +2791,10 @@ SOURCE=.\src\misc\vec\vecHash.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\vec\vecHsh.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\vec\vecInt.h
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c6d75b4b..d4e83f58 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -179,8 +179,8 @@ struct Gia_Man_t_
     Vec_Ptr_t *    vTtInputs;     // truth tables for constant and primary inputs
     Vec_Wrd_t *    vTtMemory;     // truth tables for internal nodes
     // balancing
-    Vec_Int_t *    vStore;        // node storage  
     Vec_Int_t *    vSuper;        // supergate
+    Vec_Int_t *    vStore;        // node storage  
 };
 
 
@@ -929,7 +929,9 @@ extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int
 extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );
 extern Vec_Str_t *         Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
 extern void                Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName );
+/*=== giaBalance.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
+extern Gia_Man_t *         Gia_ManMultiExtract( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 34d807c8..521a8457 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "gia.h"
+#include "misc/vec/vecHash.h"
+#include "misc/vec/vecQue.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -57,11 +59,9 @@ void Gia_ManSimplifyXor( Vec_Int_t * vSuper )
             Prev = -1, k--;
     }
     Vec_IntShrink( vSuper, k );
-    if ( !fCompl )
-        return;
     if ( Vec_IntSize( vSuper ) == 0 )
-        Vec_IntPush( vSuper, 1 );
-    else
+        Vec_IntPush( vSuper, fCompl );
+    else if ( fCompl )
         Vec_IntWriteEntry( vSuper, 0, Abc_LitNot(Vec_IntEntry(vSuper, 0)) );
 }
 void Gia_ManSimplifyAnd( Vec_Int_t * vSuper )
@@ -70,15 +70,17 @@ void Gia_ManSimplifyAnd( Vec_Int_t * vSuper )
     Vec_IntForEachEntry( vSuper, This, i )
     {
         if ( This == 0 )
-            { Vec_IntClear( vSuper ); return; }
+            { Vec_IntFill(vSuper, 1, 0); return; }
         if ( This == 1 )
             continue;
         if ( Prev == -1 || Abc_Lit2Var(Prev) != Abc_Lit2Var(This) )
             Vec_IntWriteEntry( vSuper, k++, This ), Prev = This;
         else if ( Prev != This )
-            { Vec_IntClear( vSuper ); return; }
+            { Vec_IntFill(vSuper, 1, 0); return; }
     }
     Vec_IntShrink( vSuper, k );
+    if ( Vec_IntSize( vSuper ) == 0 )
+        Vec_IntPush( vSuper, 1 );
 }
 
 /**Function*************************************************************
@@ -95,7 +97,7 @@ void Gia_ManSimplifyAnd( Vec_Int_t * vSuper )
 void Gia_ManSuperCollectXor_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     assert( !Gia_IsComplement(pObj) );
-    if ( !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(p, pObj) > 1 || Vec_IntSize(p->vSuper) > 10000 )
+    if ( !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(p, pObj) > 1 || Vec_IntSize(p->vSuper) > 100 )
     {
         Vec_IntPush( p->vSuper, Gia_ObjToLit(p, pObj) );
         return;
@@ -106,7 +108,7 @@ void Gia_ManSuperCollectXor_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 }
 void Gia_ManSuperCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
-    if ( Gia_IsComplement(pObj) || !Gia_ObjIsAndReal(p, pObj) || Gia_ObjRefNum(p, pObj) > 1 || Vec_IntSize(p->vSuper) > 10000 )
+    if ( Gia_IsComplement(pObj) || !Gia_ObjIsAndReal(p, pObj) || Gia_ObjRefNum(p, pObj) > 1 || Vec_IntSize(p->vSuper) > 100 )
     {
         Vec_IntPush( p->vSuper, Gia_ObjToLit(p, pObj) );
         return;
@@ -116,23 +118,36 @@ void Gia_ManSuperCollectAnd_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 }
 void Gia_ManSuperCollect( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
-    Vec_IntClear( p->vSuper );
+//    int nSize;
+    if ( p->vSuper == NULL )
+        p->vSuper = Vec_IntAlloc( 1000 );
+    else
+        Vec_IntClear( p->vSuper );
     if ( Gia_ObjIsXor(pObj) )
     {
         assert( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) );
         Gia_ManSuperCollectXor_rec( p, Gia_ObjFanin0(pObj) );
         Gia_ManSuperCollectXor_rec( p, Gia_ObjFanin1(pObj) );
+//        nSize = Vec_IntSize(vSuper);
         Vec_IntSort( p->vSuper, 0 );
         Gia_ManSimplifyXor( p->vSuper );
+//        if ( nSize != Vec_IntSize(vSuper) )
+//            printf( "X %d->%d  ", nSize, Vec_IntSize(vSuper) );
     }
     else if ( Gia_ObjIsAndReal(p, pObj) )
     {
         Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild0(pObj) );
         Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild1(pObj) );
+//        nSize = Vec_IntSize(vSuper);
         Vec_IntSort( p->vSuper, 0 );
         Gia_ManSimplifyAnd( p->vSuper );
+//        if ( nSize != Vec_IntSize(vSuper) )
+//            printf( "A %d->%d  ", nSize, Vec_IntSize(vSuper) );
     }
     else assert( 0 );
+//    if ( nSize > 10 )
+//        printf( "%d ", nSize );
+    assert( Vec_IntSize(p->vSuper) > 0 );
 }
 
 /**Function*************************************************************
@@ -146,15 +161,17 @@ void Gia_ManSuperCollect( Gia_Man_t * p, Gia_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCreateGate( Gia_Man_t * pNew, Vec_Int_t * vSuper, Gia_Obj_t * pObj )
+void Gia_ManCreateGate( Gia_Man_t * pNew, Gia_Obj_t * pObj, Vec_Int_t * vSuper )
 {
     int iLit0 = Vec_IntPop(vSuper);
     int iLit1 = Vec_IntPop(vSuper);
     int iLit, i;
-    if ( Gia_ObjIsXor(pObj) )
-        iLit = Gia_ManHashXorReal( pNew, iLit0, iLit1 );
-    else
+    if ( !Gia_ObjIsXor(pObj) )
         iLit = Gia_ManHashAnd( pNew, iLit0, iLit1 );
+    else if ( pNew->pMuxes )
+        iLit = Gia_ManHashXorReal( pNew, iLit0, iLit1 );
+    else 
+        iLit = Gia_ManHashXor( pNew, iLit0, iLit1 );
     Vec_IntPush( vSuper, iLit );
     Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(iLit)) );
     // shift to the corrent location
@@ -162,14 +179,48 @@ void Gia_ManCreateGate( Gia_Man_t * pNew, Vec_Int_t * vSuper, Gia_Obj_t * pObj )
     {
         int iLit1 = Vec_IntEntry(vSuper, i);
         int iLit2 = Vec_IntEntry(vSuper, i-1);
-        Gia_Obj_t * pNode1 = Gia_ManObj( pNew, Abc_Lit2Var(iLit1) );
-        Gia_Obj_t * pNode2 = Gia_ManObj( pNew, Abc_Lit2Var(iLit2) );
-        if ( Gia_ObjLevel(pNew, pNode1) <= Gia_ObjLevel(pNew, pNode2) )
+        if ( Gia_ObjLevelId(pNew, Abc_Lit2Var(iLit1)) <= Gia_ObjLevelId(pNew, Abc_Lit2Var(iLit2)) )
             break;
         Vec_IntWriteEntry( vSuper, i,   iLit2 );
         Vec_IntWriteEntry( vSuper, i-1, iLit1 );
     }
 }
+int Gia_ManBalanceGate( Gia_Man_t * pNew, Gia_Obj_t * pObj, Vec_Int_t * vSuper, int * pLits, int nLits )
+{
+    if ( nLits == 2 )
+    {
+        Vec_IntClear( vSuper );
+        Vec_IntPush( vSuper, pLits[0] );
+        Vec_IntPush( vSuper, pLits[1] );
+        Gia_ManCreateGate( pNew, pObj, vSuper );
+    }
+    else if ( nLits > 2 )
+    {
+        int i, * pArray, * pPerm;
+        // collect levels
+        Vec_IntClear( vSuper );
+        for ( i = 0; i < nLits; i++ )
+            Vec_IntPush( vSuper, Gia_ObjLevelId(pNew, Abc_Lit2Var(pLits[i])) );
+        // sort by level
+        Vec_IntGrow( vSuper, 4 * nLits );        
+        pArray = Vec_IntArray( vSuper );
+        pPerm = pArray + nLits;
+        Abc_QuickSortCostData( pArray, nLits, 1, (word *)(pArray + 2 * nLits), pPerm );
+        // collect in the increasing order of level
+        for ( i = 0; i < nLits; i++ )
+            Vec_IntWriteEntry( vSuper, i, pLits[pPerm[i]] );
+        Vec_IntShrink( vSuper, nLits );
+//        Vec_IntForEachEntry( vSuper, iLit, i )
+//            printf( "%d ", Gia_ObjLevel(pNew, Gia_ManObj( pNew, Abc_Lit2Var(iLit) )) );
+//        printf( "\n" );
+        // perform incremental extraction
+        while ( Vec_IntSize(vSuper) > 1 )
+            Gia_ManCreateGate( pNew, pObj, vSuper );
+    }
+    // consider trivial case
+    assert( Vec_IntSize(vSuper) == 1 );
+    return Vec_IntEntry(vSuper, 0);
+}
 
 /**Function*************************************************************
 
@@ -200,12 +251,9 @@ void Gia_ManBalance_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     }
     // find supergate
     Gia_ManSuperCollect( p, pObj );
-    if ( Vec_IntSize(p->vSuper) == 0 )
-    {
-        pObj->Value = 0;
-        return;
-    }
     // save entries
+    if ( p->vStore == NULL )
+        p->vStore = Vec_IntAlloc( 1000 );
     iBeg = Vec_IntSize( p->vStore );
     Vec_IntAppend( p->vStore, p->vSuper );
     iEnd = Vec_IntSize( p->vStore );
@@ -217,42 +265,8 @@ void Gia_ManBalance_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
         Vec_IntWriteEntry( p->vStore, i, Abc_LitNotCond(pTemp->Value, Abc_LitIsCompl(iLit)) );
     }
     assert( Vec_IntSize(p->vStore) == iEnd );
-    // extract entries
-    Vec_IntClear( p->vSuper );
-    Vec_IntForEachEntryStartStop( p->vStore, iLit, i, iBeg, iEnd )
-        Vec_IntPush( p->vSuper, iLit );
     // consider general case
-    if ( Vec_IntSize(p->vSuper) > 2 )
-    {
-        // replace entries by their level
-        int nSize, * pArray, * pPerm;
-        Vec_IntForEachEntry( p->vSuper, iLit, i )
-        {
-            Gia_Obj_t * pTemp = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
-            Vec_IntWriteEntry( p->vSuper, i, Gia_ObjLevel(pNew, pTemp) );
-        }
-        // allocate space
-        nSize = Vec_IntSize( p->vSuper );
-        Vec_IntGrow( p->vSuper, 4 * nSize );        
-        pArray = Vec_IntArray( p->vSuper );
-        pPerm = pArray + nSize;
-        Abc_QuickSortCostData( pArray, nSize, 1, (word *)(pArray + 2 * nSize), pPerm );
-        // collect entries in the increasing order of level
-        for ( i = 0; i < nSize; i++ )
-            Vec_IntWriteEntry( p->vSuper, i, Vec_IntEntry(p->vStore, iBeg + pPerm[i]) );
-        Vec_IntShrink( p->vSuper, nSize );
-        // perform incremental extraction
-//        Vec_IntForEachEntry( p->vSuper, iLit, i )
-//            printf( "%d ", Gia_ObjLevel(pNew, Gia_ManObj( pNew, Abc_Lit2Var(iLit) )) );
-//        printf( "\n" );
-        while ( Vec_IntSize(p->vSuper) > 1 )
-            Gia_ManCreateGate( pNew, p->vSuper, pObj );
-    }
-    // consider trivial case
-    else if ( Vec_IntSize(p->vSuper) == 2 )
-        Gia_ManCreateGate( pNew, p->vSuper, pObj );
-    assert( Vec_IntSize(p->vSuper) == 1 );
-    pObj->Value = Vec_IntEntry( p->vSuper, 0 );
+    pObj->Value = Gia_ManBalanceGate( pNew, pObj, p->vSuper, Vec_IntEntryP(p->vStore, iBeg), iEnd-iBeg );
     Vec_IntShrink( p->vStore, iBeg );
 }
 Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p )
@@ -262,9 +276,6 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p )
     int i;
     Gia_ManFillValue( p );
     Gia_ManCreateRefs( p ); 
-    assert( p->vStore == NULL );
-    p->vStore = Vec_IntAlloc( 1000 );
-    p->vSuper = Vec_IntAlloc( 1000 );
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
@@ -284,8 +295,6 @@ Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p )
     }
     assert( Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) );
     Gia_ManHashStop( pNew );
-    Vec_IntFree( p->vStore );
-    Vec_IntFree( p->vSuper );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     // perform cleanup
     pNew = Gia_ManCleanup( pTemp = pNew );
@@ -319,6 +328,511 @@ Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose )
     return pNew2;
 }
 
+
+
+
+
+
+// operation manager
+typedef struct Dam_Man_t_ Dam_Man_t;
+struct Dam_Man_t_
+{
+    Gia_Man_t *      pGia;      // user's AIG
+    Vec_Int_t *      vNod2Set;  // node ID into fanin set
+    Vec_Int_t *      vDiv2Nod;  // div ID into fanin set
+    Vec_Int_t *      vSetStore; // stored multisets
+    Vec_Int_t *      vNodStore; // stored divisors
+    Vec_Flt_t *      vCounts;   // occur counts
+    Vec_Que_t *      vQue;      // pairs by count
+    Hash_IntMan_t *  vHash;     // pair hash table
+    abctime          clkStart;  // starting the clock
+    int              nAnds;     // total AND node count
+    int              nDivs;     // extracted divisor count
+};
+
+static inline int    Dam_ObjHand( Dam_Man_t * p, int i )     { return i < Vec_IntSize(p->vNod2Set) ? Vec_IntEntry(p->vNod2Set, i) : 0;                      }
+static inline int *  Dam_ObjSet( Dam_Man_t * p, int i )      { int h = Dam_ObjHand(p, i); if ( h == 0 ) return NULL; return Vec_IntEntryP(p->vSetStore, h); }
+
+static inline int    Dam_DivHand( Dam_Man_t * p, int d )     { return d < Vec_IntSize(p->vDiv2Nod) ? Vec_IntEntry(p->vDiv2Nod, d) : 0;                      }
+static inline int *  Dam_DivSet( Dam_Man_t * p, int d )      { int h = Dam_DivHand(p, d); if ( h == 0 ) return NULL; return Vec_IntEntryP(p->vNodStore, h); }
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dam_Man_t * Dam_ManAlloc( Gia_Man_t * pGia )
+{
+    Dam_Man_t * p;
+    p = ABC_CALLOC( Dam_Man_t, 1 );
+    p->clkStart = Abc_Clock();
+    p->pGia = pGia;
+    return p;
+}
+void Dam_ManFree( Dam_Man_t * p )
+{   
+    Vec_IntFreeP( &p->vNod2Set );
+    Vec_IntFreeP( &p->vDiv2Nod );
+    Vec_IntFreeP( &p->vSetStore );
+    Vec_IntFreeP( &p->vNodStore );
+    Vec_FltFreeP( &p->vCounts );
+    Vec_QueFreeP( &p->vQue );
+    Hash_IntManStop( p->vHash );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect initial multi-input gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dam_ManCollectSets_rec( Dam_Man_t * p, int Id )
+{
+    Gia_Obj_t * pObj;
+    int i, iBeg, iEnd, iLit;
+    if ( Dam_ObjHand(p, Id) || Id == 0 )
+        return;
+    pObj = Gia_ManObj(p->pGia, Id);
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    if ( Gia_ObjIsMux(p->pGia, pObj) )
+    {
+        Dam_ManCollectSets_rec( p, Gia_ObjFaninId0(pObj, Id) );
+        Dam_ManCollectSets_rec( p, Gia_ObjFaninId1(pObj, Id) );
+        Dam_ManCollectSets_rec( p, Gia_ObjFaninId2(p->pGia, Id) );
+        p->nAnds += 3;
+        return;
+    }
+    Gia_ManSuperCollect( p->pGia, pObj );
+    Vec_IntWriteEntry( p->vNod2Set, Id, Vec_IntSize(p->vSetStore) );
+    Vec_IntPush( p->vSetStore, Vec_IntSize(p->pGia->vSuper) );
+    p->nAnds += (1 + 2 * Gia_ObjIsXor(pObj)) * (Vec_IntSize(p->pGia->vSuper) - 1);
+    // save entries
+    iBeg = Vec_IntSize( p->vSetStore );
+    Vec_IntAppend( p->vSetStore, p->pGia->vSuper );
+    iEnd = Vec_IntSize( p->vSetStore );
+    // call recursively
+    Vec_IntForEachEntryStartStop( p->vSetStore, iLit, i, iBeg, iEnd )
+        Dam_ManCollectSets_rec( p, Abc_Lit2Var(iLit) );
+}
+void Dam_ManCollectSets( Dam_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManCreateRefs( p->pGia ); 
+    p->vNod2Set  = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    p->vSetStore = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );
+    Vec_IntPush( p->vSetStore, -1 );
+    Gia_ManForEachCo( p->pGia, pObj, i )
+        Dam_ManCollectSets_rec( p, Gia_ObjFaninId0p(p->pGia, pObj) );
+    ABC_FREE( p->pGia->pRefs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dam_ManCreateMultiRefs( Dam_Man_t * p, Vec_Int_t ** pvRefsAnd, Vec_Int_t ** pvRefsXor )  
+{
+    Vec_Int_t * vRefsAnd, * vRefsXor;
+    Gia_Obj_t * pObj;
+    int i, k, * pSet;
+    vRefsAnd = Vec_IntStart( 2 * Gia_ManObjNum(p->pGia) );
+    vRefsXor = Vec_IntStart( Gia_ManObjNum(p->pGia) );
+    Gia_ManForEachAnd( p->pGia, pObj, i )
+    {
+        if ( !Dam_ObjHand(p, i) )
+            continue;
+        pSet = Dam_ObjSet(p, i);
+        if ( Gia_ObjIsXor(pObj) )
+            for ( k = 1; k <= pSet[0]; k++ )
+            {
+                assert( !Abc_LitIsCompl(pSet[k]) );
+                Vec_IntAddToEntry( vRefsXor, Abc_Lit2Var(pSet[k]), 1 );
+            }
+        else if ( Gia_ObjIsAndReal(p->pGia, pObj) )
+            for ( k = 1; k <= pSet[0]; k++ )
+                Vec_IntAddToEntry( vRefsAnd, pSet[k], 1 );
+        else assert( 0 );
+    }
+    *pvRefsAnd = vRefsAnd;
+    *pvRefsXor = vRefsXor;
+}
+void Dam_ManCreatePairs( Dam_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    Hash_IntMan_t * vHash;
+    Vec_Int_t * vRefsAnd, * vRefsXor, * vSuper, * vDivs, * vRemap;
+    int i, j, k, Num, FanK, FanJ, nRefs, iNode, iDiv, * pSet;
+    int nPairsAll = 0, nPairsTried = 0, nPairsUsed = 0, nPairsXor = 0;
+    int nDivsAll = 0, nDivsUsed = 0, nDivsXor = 0;
+    Dam_ManCollectSets( p );
+    vSuper = p->pGia->vSuper;
+    vDivs  = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );
+    vHash  = Hash_IntManStart( Gia_ManObjNum(p->pGia) );
+    Dam_ManCreateMultiRefs( p, &vRefsAnd, &vRefsXor );
+    Gia_ManForEachAnd( p->pGia, pObj, i )
+    {
+        if ( !Dam_ObjHand(p, i) )
+            continue;
+        pSet = Dam_ObjSet(p, i);
+        nPairsAll += pSet[0] * (pSet[0] - 1) / 2;
+        Vec_IntClear(vSuper);
+        if ( Gia_ObjIsXor(pObj) )
+        {
+            for ( k = 1; k <= pSet[0]; k++ )
+                if ( Vec_IntEntry(vRefsXor, Abc_Lit2Var(pSet[k])) > 1 )
+                    Vec_IntPush( vSuper, pSet[k] );
+        }
+        else if ( Gia_ObjIsAndReal(p->pGia, pObj) )
+        {
+            for ( k = 1; k <= pSet[0]; k++ )
+                if ( Vec_IntEntry(vRefsAnd, pSet[k]) > 1 )
+                    Vec_IntPush( vSuper, pSet[k] );
+        }
+        else assert( 0 );
+        if ( Vec_IntSize(vSuper) < 2 )
+            continue;
+        // enumerate pairs
+        nPairsTried += Vec_IntSize(vSuper) * (Vec_IntSize(vSuper) - 1) / 2;
+        Vec_IntPush( vDivs, -i ); // remember node
+        Vec_IntForEachEntry( vSuper, FanK, k )
+        Vec_IntForEachEntryStart( vSuper, FanJ, j, k+1 )
+        {
+            if ( (FanK > FanJ) ^ Gia_ObjIsXor(pObj) )
+                Num = Hash_Int2ManInsert( vHash, FanJ, FanK, 0 );
+            else
+                Num = Hash_Int2ManInsert( vHash, FanK, FanJ, 0 );
+            if ( Hash_Int2ObjInc( vHash, Num ) == 1 )
+            {
+                nDivsUsed++;
+                nDivsXor += Gia_ObjIsXor(pObj);
+            }
+            Vec_IntPush( vDivs, Num ); // remember devisor
+        }
+    }
+    Vec_IntFree( vRefsAnd );
+    Vec_IntFree( vRefsXor );
+    // remove entries that appear only once
+    p->vHash     = Hash_IntManStart( 2 * nDivsUsed );
+    p->vCounts   = Vec_FltAlloc( 2 * nDivsUsed );           Vec_FltPush( p->vCounts, ABC_INFINITY );
+    p->vQue      = Vec_QueAlloc( Vec_FltCap(p->vCounts) );
+    Vec_QueSetCosts( p->vQue, Vec_FltArrayP(p->vCounts) );
+    // mapping div to node
+    p->vDiv2Nod  = Vec_IntAlloc( 2 * nDivsUsed );           Vec_IntPush( p->vDiv2Nod, ABC_INFINITY );
+    p->vNodStore = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );  Vec_IntPush( p->vNodStore, -1 );
+    nDivsAll     = Hash_IntManEntryNum(vHash);
+    vRemap       = Vec_IntStartFull( nDivsAll+1 );
+    for ( i = 1; i <= nDivsAll; i++ )
+    {
+        nRefs = Hash_IntObjData2(vHash, i);
+        if ( nRefs < 2 )
+            continue;
+        nPairsUsed += nRefs;
+        if ( Hash_IntObjData0(vHash, i) > Hash_IntObjData1(vHash, i) )
+            nPairsXor += nRefs; 
+        Num = Hash_Int2ManInsert( p->vHash, Hash_IntObjData0(vHash, i), Hash_IntObjData1(vHash, i), 0 );
+        assert( Num == Hash_IntManEntryNum(p->vHash) );
+        assert( Num == Vec_FltSize(p->vCounts) );
+        Vec_FltPush( p->vCounts, nRefs );
+        Vec_QuePush( p->vQue, Num );
+        // remember divisors
+        assert( Num == Vec_IntSize(p->vDiv2Nod) );
+        Vec_IntPush( p->vDiv2Nod, Vec_IntSize(p->vNodStore) );
+        Vec_IntPush( p->vNodStore, 0 );
+        Vec_IntFillExtra( p->vNodStore, Vec_IntSize(p->vNodStore) + nRefs, -1 );
+        // remember entry
+        Vec_IntWriteEntry( vRemap, i, Num );
+    }
+    assert( Vec_FltSize(p->vCounts) == Hash_IntManEntryNum(p->vHash)+1 );
+    assert( Vec_IntSize(p->vDiv2Nod) == nDivsUsed+1 );
+    Hash_IntManStop( vHash );
+    // fill in the divisors
+    iNode = -1;
+    Vec_IntForEachEntry( vDivs, iDiv, i )
+    {
+        if ( iDiv < 0 )
+        {
+            iNode = -iDiv;
+            continue;
+        }
+        Num = Vec_IntEntry( vRemap, iDiv );
+        if ( Num == -1 )
+            continue;
+        pSet = Dam_DivSet( p, Num );
+        assert( pSet[0] < Vec_FltEntry(p->vCounts, Num) );
+        pSet[++pSet[0]] = iNode;
+    }
+    Vec_IntFree( vRemap );
+    Vec_IntFree( vDivs );
+    // make sure divisors are added correctly
+    for ( i = 1; i <= nDivsUsed; i++ )
+        assert( Dam_DivSet(p, i)[0] == Vec_FltEntry(p->vCounts, i) );
+
+    // print stats
+    printf( "Pairs:" );
+    printf( "  Total =%9d (%6.2f %%)", nPairsAll,   100.0 * nPairsAll   / Abc_MaxInt(nPairsAll, 1) );
+    printf( "  Tried =%9d (%6.2f %%)", nPairsTried, 100.0 * nPairsTried / Abc_MaxInt(nPairsAll, 1) );
+    printf( "  Used =%9d (%6.2f %%)",  nPairsUsed,  100.0 * nPairsUsed  / Abc_MaxInt(nPairsAll, 1) );
+    printf( "  Xor =%9d (%6.2f %%)",   nPairsXor,   100.0 * nPairsXor   / Abc_MaxInt(nPairsAll, 1) );
+    printf( "\n" );
+    printf( "Div:  " );
+    printf( "  Total =%9d (%6.2f %%)", nDivsAll,    100.0 * nDivsAll    / Abc_MaxInt(nDivsAll, 1) );
+    printf( "  Tried =%9d (%6.2f %%)", nDivsAll,    100.0 * nDivsAll    / Abc_MaxInt(nDivsAll, 1) );
+    printf( "  Used =%9d (%6.2f %%)",  nDivsUsed,   100.0 * nDivsUsed   / Abc_MaxInt(nDivsAll, 1) );
+    printf( "  Xor =%9d (%6.2f %%)",   nDivsXor,    100.0 * nDivsXor    / Abc_MaxInt(nDivsAll, 1) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dam_ManMultiAig_rec( Dam_Man_t * pMan, Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int i, * pSet;
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    pSet = Dam_ObjSet(pMan, Gia_ObjId(p, pObj));
+    if ( pSet == NULL )
+    {
+        Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin0(pObj) );
+        Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin1(pObj) );
+        if ( Gia_ObjIsMux(p, pObj) )
+        {
+            Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin2(p, pObj) );
+            pObj->Value = Gia_ManHashMuxReal( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
+        }
+        else if ( Gia_ObjIsXor(pObj) )
+            pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else 
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value)) );
+        return;
+    }
+    assert( Gia_ObjIsXor(pObj) || Gia_ObjIsAndReal(p, pObj) );
+    // call recursively
+    for ( i = 1; i <= pSet[0]; i++ )
+    {
+        Gia_Obj_t * pTemp = Gia_ManObj( p, Abc_Lit2Var(pSet[i]) );
+        Dam_ManMultiAig_rec( pMan, pNew, p, pTemp );
+        pSet[i] = Abc_LitNotCond( pTemp->Value, Abc_LitIsCompl(pSet[i]) );
+    }
+    // create balanced gate
+    pObj->Value = Gia_ManBalanceGate( pNew, pObj, p->vSuper, pSet + 1, pSet[0] );
+}
+Gia_Man_t * Dam_ManMultiAig( Dam_Man_t * pMan )
+{
+    Gia_Man_t * p = pMan->pGia;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    // start the new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
+    pNew->vLevels = Vec_IntStart( pNew->nObjsAlloc );
+    // create constant and inputs
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManHashStart( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Dam_ManMultiAig_rec( pMan, pNew, p, Gia_ObjFanin0(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    assert( Gia_ManObjNum(pNew) <= Gia_ManObjNum(p) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // perform cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the data-structure after extracting one divisor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dam_PrintDiv( Dam_Man_t * p, int iDiv )
+{
+    if ( iDiv == 0 )
+        printf( "Final statistics after extracting %6d divisors:         ", p->nDivs );
+    else
+    {
+        int iData0 = Hash_IntObjData0(p->vHash, iDiv);
+        int iData1 = Hash_IntObjData1(p->vHash, iDiv);
+        printf( "%4d : ",       p->nDivs+1 );
+        printf( "Div %7d : ",   iDiv );
+        printf( "Weight %5d  ", (int)Vec_FltEntry(p->vCounts, iDiv) );
+        printf( "%s(",          iData0 < iData1 ? "AND" : "XOR" );
+        printf( "%7d ",         iData0 );
+        printf( "%7d )   ",     iData1 );
+    }
+    printf( "Divs =%8d  ",  Hash_IntManEntryNum(p->vHash) );
+    printf( "Ands =%7d  ",  p->nAnds );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
+}
+void Dam_PrintQue( Dam_Man_t * p )
+{
+    int i;
+    printf( "Divisor queue: \n" );
+    for ( i = 1; i <= Hash_IntManEntryNum(p->vHash); i++ )
+    {
+        int iLit0 = Hash_IntObjData0(p->vHash, i);
+        int iLit1 = Hash_IntObjData1(p->vHash, i);
+        printf( "Div %7d : ",   i );
+        printf( "Weight %5d  ", (int)Vec_FltEntry(p->vCounts, i) );
+        printf( "F = %c%c ",    Abc_LitIsCompl(iLit0) ? '!': ' ', 'a' + Abc_Lit2Var(iLit0)-1 );
+        printf( "%c ",          (Hash_IntObjData0(p->vHash, i) < Hash_IntObjData1(p->vHash, i)) ? '*':'+' );
+        printf( "%c%c   ",      Abc_LitIsCompl(iLit1) ? '!': ' ', 'a' + Abc_Lit2Var(iLit1)-1 );
+        printf( "\n" );
+    }
+}
+void Dam_ManUpdateNode( Dam_Man_t * p, int iObj, int iLit0, int iLit1, int iLitNew )
+{
+    int i, k, c, Num, iLit, iLit2;
+    int * pSet = Dam_ObjSet( p, iObj );
+    for ( k = i = 1; i <= pSet[0]; i++ )
+    {
+        if ( iLit0 == pSet[i] || iLit1 == pSet[i] )
+            continue;
+        pSet[k++] = iLit = pSet[i];
+        // reduce weights of the divisors
+        for ( c = 0; c < 2; c++ )
+        {
+            iLit2 = c ? iLit1 : iLit0;
+            if ( (iLit > iLit2) ^ (iLit0 > iLit1) )
+                Num = *Hash_Int2ManLookup( p->vHash, iLit2, iLit );
+            else
+                Num = *Hash_Int2ManLookup( p->vHash, iLit, iLit2 );
+            if ( Num > 0 )
+            {
+                Vec_FltAddToEntry( p->vCounts, Num, -1 );
+                Vec_QueUpdate( p->vQue, Num );
+            }
+        }
+    }
+    pSet[k] = iLitNew;
+    pSet[0] = k;
+    // add new divisors
+    for ( i = 1; i < pSet[0]; i++ )
+    {
+    }
+
+}
+void Dam_ManUpdate( Dam_Man_t * p, int iDiv )
+{
+    int iLit0 = Hash_IntObjData0(p->vHash, iDiv);
+    int iLit1 = Hash_IntObjData1(p->vHash, iDiv);
+    int i, iLitNew, * pNods = Dam_DivSet( p, iDiv );
+    int fThisIsXor = (iLit0 > iLit1);
+//    Dam_PrintQue( p );
+    if ( fThisIsXor )
+        iLitNew = Gia_ManAppendXorReal( p->pGia, iLit0, iLit1 );
+    else
+        iLitNew = Gia_ManAppendAnd( p->pGia, iLit0, iLit1 );
+    // replace entries
+    assert( pNods[0] >= 2 );
+    for ( i = 1; i <= pNods[0]; i++ )
+        Dam_ManUpdateNode( p, pNods[i], iLit0, iLit1, iLitNew );
+    // update reference counters of AND/XOR nodes
+
+    // update costs
+    Vec_FltWriteEntry( p->vCounts, iDiv, 0 );
+    p->nAnds -= (1 + 2 * fThisIsXor) * (pNods[0] - 1);
+    p->nDivs++;
+//    Dam_PrintQue( p );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Perform extraction for multi-input AND/XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Dam_ManMultiExtractInt( Gia_Man_t * p, int nNewNodesMax, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    Dam_Man_t * pMan;
+    int i, iDiv;
+//    nNewNodesMax = 1;
+    pMan = Dam_ManAlloc( p );
+    Dam_ManCreatePairs( pMan );
+    for ( i = 0; i < nNewNodesMax && Vec_QueTopCost(pMan->vQue) > 1; i++ )
+    {
+        iDiv = Vec_QuePop(pMan->vQue);
+        if ( fVerbose )
+            Dam_PrintDiv( pMan, iDiv );
+        Dam_ManUpdate( pMan, iDiv );
+    }
+    if ( fVerbose )
+        Dam_PrintDiv( pMan, 0 );
+    pNew = Dam_ManMultiAig( pMan );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - pMan->clkStart );
+    Dam_ManFree( pMan );
+    return pNew;
+}
+Gia_Man_t * Gia_ManMultiExtract( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose )
+{
+    Gia_Man_t * pNew, * pNew1, * pNew2;
+    if ( fVerbose )     Gia_ManPrintStats( p, NULL );
+    pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p );
+    if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
+    pNew1 = Dam_ManMultiExtractInt( pNew, nNewNodesMax, fVerbose );
+    if ( fVerbose )     Gia_ManPrintStats( pNew1, NULL );
+    Gia_ManStop( pNew );
+    pNew2 = Gia_ManDupNoMuxes( pNew1 );
+    if ( fVerbose )     Gia_ManPrintStats( pNew2, NULL );
+    Gia_ManStop( pNew1 );
+    return pNew2;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index ae17c176..eb89a9cd 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -518,6 +518,12 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
 {
     int fCompl = 0;
     assert( p->fAddStrash == 0 );
+    if ( iLitC < 2 )
+        return iLitC ? iLit1 : iLit0;
+    if ( iLit0 < 2 )
+        return iLit0 ? Gia_ManHashOr(p, Abc_LitNot(iLitC), iLit1) : Gia_ManHashAnd(p, iLitC, iLit1);
+    if ( iLit1 < 2 )
+        return iLit1 ? Gia_ManHashOr(p, iLitC, iLit0) : Gia_ManHashAnd(p, Abc_LitNot(iLitC), iLit0);
     assert( iLit0 > 1 && iLit1 > 1 && iLitC > 1 );
     if ( iLit0 == iLit1 )
         return iLit0;
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 53035506..5df2faa5 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -77,6 +77,8 @@ void Gia_ManStop( Gia_Man_t * p )
     assert( p->pManTime == NULL );
     Vec_PtrFreeFree( p->vNamesIn );
     Vec_PtrFreeFree( p->vNamesOut );
+    Vec_IntFreeP( &p->vSuper );
+    Vec_IntFreeP( &p->vStore );
     Vec_IntFreeP( &p->vClassNew );
     Vec_IntFreeP( &p->vClassOld );
     Vec_WrdFreeP( &p->vSims );
@@ -335,13 +337,19 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
         Abc_Print( 1, "(c=%d)", Gia_ManConstrNum(p) );
     if ( Gia_ManRegNum(p) )
         Abc_Print( 1, "  ff =%7d", Gia_ManRegNum(p) );
-    Abc_Print( 1, "  and =%8d", Gia_ManAndNum(p) );
+    Abc_Print( 1, "  %s =%8d", p->pMuxes? "nod" : "and", Gia_ManAndNum(p) );
     Abc_Print( 1, "  lev =%5d", Gia_ManLevelNum(p) ); Vec_IntFreeP( &p->vLevels );
     if ( pPars && pPars->fCut )
         Abc_Print( 1, "  cut = %d(%d)", Gia_ManCrossCut(p, 0), Gia_ManCrossCut(p, 1) );
     Abc_Print( 1, "  mem =%5.2f MB", Gia_ManMemory(p)/(1<<20) );
     if ( Gia_ManHasDangling(p) )
         Abc_Print( 1, "  ch =%5d", Gia_ManEquivCountClasses(p) );
+    if ( p->pMuxes )
+    {
+        Abc_Print( 1, "  and =%5d", Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p) );
+        Abc_Print( 1, "  xor =%5d", Gia_ManXorNum(p) );
+        Abc_Print( 1, "  mux =%5d", Gia_ManMuxNum(p) );
+    }
     if ( pPars && pPars->fSwitch )
     {
         if ( p->pSwitching )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 760d7068..9628312a 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1008,13 +1008,19 @@ int Gia_ManHasDangling( Gia_Man_t * p )
     Gia_ManForEachObj( p, pObj, i )
     {
         pObj->fMark0 = 0;
-        if ( Gia_ObjIsAnd(pObj) )
+        if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+        else if ( Gia_ObjIsMux(p, pObj) )
         {
             Gia_ObjFanin0(pObj)->fMark0 = 1;
             Gia_ObjFanin1(pObj)->fMark0 = 1;
+            Gia_ObjFanin2(p, pObj)->fMark0 = 1;
         }
-        else if ( Gia_ObjIsCo(pObj) )
+        else if ( Gia_ObjIsAnd(pObj) )
+        {
             Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
     }
     Gia_ManForEachAnd( p, pObj, i )
         Counter += !pObj->fMark0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0b1c6b23..6bac9542 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27410,12 +27410,13 @@ usage:
 int Abc_CommandAbc9Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
-    int c,fVerbose = 0;
-    int fSimpleAnd = 0;
-    int fKeepLevel = 0;
-    int nFanoutMax = 50;
+    int nNewNodesMax = ABC_INFINITY;
+    int fMultiExt    = 0;
+    int fSimpleAnd   = 0;
+    int fKeepLevel   = 0;
+    int c, fVerbose  = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nlavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nealvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -27425,17 +27426,20 @@ int Abc_CommandAbc9Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-N\" should be followed by a char string.\n" );
                 goto usage;
             }
-            nFanoutMax = atoi(argv[globalUtilOptind]);
+            nNewNodesMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFanoutMax < 0 )
+            if ( nNewNodesMax < 0 )
                 goto usage;
             break;
-        case 'l':
-            fKeepLevel ^= 1;
+        case 'e':
+            fMultiExt ^= 1;
             break;
         case 'a':
             fSimpleAnd ^= 1;
             break;
+        case 'l':
+            fKeepLevel ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -27455,14 +27459,20 @@ int Abc_CommandAbc9Balance( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Balance(): The current AIG is mapped.\n" );
         return 1;
     }
-    pTemp = Gia_ManBalance( pAbc->pGia, fSimpleAnd, fVerbose );
+    if ( fMultiExt )
+        pTemp = Gia_ManMultiExtract( pAbc->pGia, fSimpleAnd, nNewNodesMax, fVerbose );
+    else
+        pTemp = Gia_ManBalance( pAbc->pGia, fSimpleAnd, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &b [-avh]\n" );
+    Abc_Print( -2, "usage: &b [-N num] [-ealvh]\n" );
     Abc_Print( -2, "\t         performs AIG balancing to reduce delay\n" );
+    Abc_Print( -2, "\t-N num : the max fanout count to skip a divisor [default = %d]\n", nNewNodesMax );
+    Abc_Print( -2, "\t-e     : toggle extacting shared logic while balancing [default = %s]\n", fMultiExt? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle using AND instead of AND/XOR/MUX [default = %s]\n", fSimpleAnd? "yes": "no" );
+    Abc_Print( -2, "\t-l     : toggle level update during shrinking [default = %s]\n", fKeepLevel? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;