Performance balancing command &b.

9 files changed, 434 insertions, 17 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 848b2c8a..4f4985d4 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3599,6 +3599,10 @@ SOURCE=.\src\aig\gia\giaAigerExt.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaBalance.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaBidec.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d312f437..c6d75b4b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -178,6 +178,9 @@ struct Gia_Man_t_
     Vec_Int_t *    vTtNodes;      // internal nodes
     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
 };
 
 
@@ -371,7 +374,9 @@ static inline int          Gia_ObjIsCi( Gia_Obj_t * pObj )                     {
 static inline int          Gia_ObjIsCo( Gia_Obj_t * pObj )                     { return pObj->fTerm && pObj->iDiff0 != GIA_NONE; } 
 static inline int          Gia_ObjIsAnd( Gia_Obj_t * pObj )                    { return!pObj->fTerm && pObj->iDiff0 != GIA_NONE; } 
 static inline int          Gia_ObjIsXor( Gia_Obj_t * pObj )                    { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 < pObj->iDiff1; } 
-static inline int          Gia_ObjIsMux( Gia_Man_t * p, int iObj )             { return p->pMuxes && p->pMuxes[iObj] > 0;        } 
+static inline int          Gia_ObjIsMuxId( Gia_Man_t * p, int iObj )           { return p->pMuxes && p->pMuxes[iObj] > 0;        } 
+static inline int          Gia_ObjIsMux( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_ObjIsMuxId( p, Gia_ObjId(p, pObj) ); } 
+static inline int          Gia_ObjIsAndReal( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsAnd(pObj) && pObj->iDiff0 > pObj->iDiff1 && !Gia_ObjIsMux(p, pObj); } 
 static inline int          Gia_ObjIsBuf( Gia_Obj_t * pObj )                    { return pObj->iDiff0 == pObj->iDiff1 && pObj->iDiff0 != GIA_NONE; } 
 static inline int          Gia_ObjIsCand( Gia_Obj_t * pObj )                   { return Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj); } 
 static inline int          Gia_ObjIsConst0( Gia_Obj_t * pObj )                 { return pObj->iDiff0 == GIA_NONE && pObj->iDiff1 == GIA_NONE;     } 
@@ -445,6 +450,9 @@ static inline void         Gia_ObjSetLevelId( Gia_Man_t * p, int Id, int l )   {
 static inline void         Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l )  { Gia_ObjSetLevelId( p, Gia_ObjId(p,pObj), l );       }
 static inline void         Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj )  { assert( Gia_ObjIsCo(pObj)  ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) );                                                }
 static inline void         Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
+static inline void         Gia_ObjSetXorLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsXor(pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
+static inline void         Gia_ObjSetMuxLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsMux(p,pObj) ); Gia_ObjSetLevel( p, pObj, 2+Abc_MaxInt( Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))), Gia_ObjLevel(p,Gia_ObjFanin2(p,pObj))) ); }
+static inline void         Gia_ObjSetGateLevel( Gia_Man_t * p, Gia_Obj_t * pObj ){ if ( Gia_ObjIsMux(p,pObj) ) Gia_ObjSetMuxLevel(p, pObj); else if ( Gia_ObjIsXor(pObj) ) Gia_ObjSetXorLevel(p, pObj); else if ( Gia_ObjIsAnd(pObj) ) Gia_ObjSetAndLevel(p, pObj); }
 
 static inline int          Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj )       { return (int)(unsigned char)Vec_StrGetEntry(p->vTtNums, Gia_ObjId(p,pObj));                  }
 static inline void         Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 && n < 254 ); Vec_StrSetEntry(p->vTtNums, Gia_ObjId(p,pObj), (char)n);   }
@@ -499,6 +507,7 @@ static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
         int nObjNew = Abc_MinInt( 2 * p->nObjsAlloc, (1 << 29) );
         if ( p->nObjs == (1 << 29) )
             printf( "Hard limit on the number of nodes (2^29) is reached. Quitting...\n" ), exit(1);
+        assert( p->nObjs < nObjNew );
         if ( p->fVerbose )
             printf("Extending GIA object storage: %d -> %d.\n", p->nObjsAlloc, nObjNew );
         assert( p->nObjsAlloc > 0 );
@@ -887,7 +896,7 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 #define Gia_ManForEachAndReverse( p, pObj, i )                          \
     for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )  if ( !Gia_ObjIsAnd(pObj) ) {} else
 #define Gia_ManForEachMux( p, pObj, i )                                 \
-    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsMux(p, i) ) {} else
+    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsMuxId(p, i) ) {} else
 #define Gia_ManForEachCi( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
@@ -920,6 +929,7 @@ 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 );
+extern Gia_Man_t *         Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, 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
new file mode 100644
index 00000000..34d807c8
--- /dev/null
+++ b/src/aig/gia/giaBalance.c
@@ -0,0 +1,328 @@
+/**CFile****************************************************************
+
+  FileName    [giaBalance.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [AIG balancing.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaBalance.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Simplify multi-input AND/XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManSimplifyXor( Vec_Int_t * vSuper )
+{
+    int i, k = 0, Prev = -1, This, fCompl = 0;
+    Vec_IntForEachEntry( vSuper, This, i )
+    {
+        if ( This == 0 )
+            continue;
+        if ( This == 1 )
+            fCompl ^= 1; 
+        else if ( Prev != This )
+            Vec_IntWriteEntry( vSuper, k++, This ), Prev = This;
+        else
+            Prev = -1, k--;
+    }
+    Vec_IntShrink( vSuper, k );
+    if ( !fCompl )
+        return;
+    if ( Vec_IntSize( vSuper ) == 0 )
+        Vec_IntPush( vSuper, 1 );
+    else
+        Vec_IntWriteEntry( vSuper, 0, Abc_LitNot(Vec_IntEntry(vSuper, 0)) );
+}
+void Gia_ManSimplifyAnd( Vec_Int_t * vSuper )
+{
+    int i, k = 0, Prev = -1, This;
+    Vec_IntForEachEntry( vSuper, This, i )
+    {
+        if ( This == 0 )
+            { Vec_IntClear( vSuper ); 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_IntShrink( vSuper, k );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect multi-input AND/XOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 )
+    {
+        Vec_IntPush( p->vSuper, Gia_ObjToLit(p, pObj) );
+        return;
+    }
+    assert( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) );
+    Gia_ManSuperCollectXor_rec( p, Gia_ObjFanin0(pObj) );
+    Gia_ManSuperCollectXor_rec( p, Gia_ObjFanin1(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 )
+    {
+        Vec_IntPush( p->vSuper, Gia_ObjToLit(p, pObj) );
+        return;
+    }
+    Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild0(pObj) );
+    Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild1(pObj) );
+}
+void Gia_ManSuperCollect( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    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) );
+        Vec_IntSort( p->vSuper, 0 );
+        Gia_ManSimplifyXor( p->vSuper );
+    }
+    else if ( Gia_ObjIsAndReal(p, pObj) )
+    {
+        Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild0(pObj) );
+        Gia_ManSuperCollectAnd_rec( p, Gia_ObjChild1(pObj) );
+        Vec_IntSort( p->vSuper, 0 );
+        Gia_ManSimplifyAnd( p->vSuper );
+    }
+    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCreateGate( Gia_Man_t * pNew, Vec_Int_t * vSuper, Gia_Obj_t * pObj )
+{
+    int iLit0 = Vec_IntPop(vSuper);
+    int iLit1 = Vec_IntPop(vSuper);
+    int iLit, i;
+    if ( Gia_ObjIsXor(pObj) )
+        iLit = Gia_ManHashXorReal( pNew, iLit0, iLit1 );
+    else
+        iLit = Gia_ManHashAnd( pNew, iLit0, iLit1 );
+    Vec_IntPush( vSuper, iLit );
+    Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(iLit)) );
+    // shift to the corrent location
+    for ( i = Vec_IntSize(vSuper)-1; i > 0; i-- )
+    {
+        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) )
+            break;
+        Vec_IntWriteEntry( vSuper, i,   iLit2 );
+        Vec_IntWriteEntry( vSuper, i-1, iLit1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManBalance_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int i, iLit, iBeg, iEnd;
+    if ( ~pObj->Value )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    // handle MUX
+    if ( Gia_ObjIsMux(p, pObj) )
+    {
+        Gia_ManBalance_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManBalance_rec( pNew, p, Gia_ObjFanin1(pObj) );
+        Gia_ManBalance_rec( pNew, p, Gia_ObjFanin2(p, pObj) );
+        pObj->Value = Gia_ManHashMuxReal( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
+        Gia_ObjSetGateLevel( pNew, Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value)) );
+        return;
+    }
+    // find supergate
+    Gia_ManSuperCollect( p, pObj );
+    if ( Vec_IntSize(p->vSuper) == 0 )
+    {
+        pObj->Value = 0;
+        return;
+    }
+    // save entries
+    iBeg = Vec_IntSize( p->vStore );
+    Vec_IntAppend( p->vStore, p->vSuper );
+    iEnd = Vec_IntSize( p->vStore );
+    // call recursively
+    Vec_IntForEachEntryStartStop( p->vStore, iLit, i, iBeg, iEnd )
+    {
+        Gia_Obj_t * pTemp = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+        Gia_ManBalance_rec( pNew, p, pTemp );
+        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 );
+    Vec_IntShrink( p->vStore, iBeg );
+}
+Gia_Man_t * Gia_ManBalanceInt( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    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 );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
+    pNew->vLevels = Vec_IntStart( pNew->nObjsAlloc );
+    // create constant and inputs
+    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 )
+    {
+        Gia_ManBalance_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    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 );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, 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 = Gia_ManBalanceInt( pNew );
+    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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index fd430ff2..3cef3f5b 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -928,7 +928,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
         {
             if ( Gia_ObjIsXor(pObj) )
                 pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-            else if ( Gia_ObjIsMux(p, i) )
+            else if ( Gia_ObjIsMux(p, pObj) )
                 pObj->Value = Gia_ManAppendMuxReal( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
             else
                 pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index fea76107..085dca77 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -113,7 +113,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
     Gia_ManHashStart( pNew );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        if ( Gia_ObjIsMux(p, i) )
+        if ( Gia_ObjIsMuxId(p, i) )
             pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
         else if ( Gia_ObjIsXor(pObj) )
             pObj->Value = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -170,7 +170,7 @@ Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
 int Gia_MuxRef_rec( Gia_Man_t * p, int iObj )
 {
     Gia_Obj_t * pObj;
-    if ( !Gia_ObjIsMux(p, iObj) )
+    if ( !Gia_ObjIsMuxId(p, iObj) )
         return 0;
     pObj = Gia_ManObj( p, iObj );
     if ( Gia_ObjRefInc(p, pObj) )
@@ -182,7 +182,7 @@ int Gia_MuxRef_rec( Gia_Man_t * p, int iObj )
 int Gia_MuxRef( Gia_Man_t * p, int iObj )
 {
     Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
-    assert( Gia_ObjIsMux(p, iObj) );
+    assert( Gia_ObjIsMuxId(p, iObj) );
     return Gia_MuxRef_rec( p, Gia_ObjFaninId0p(p, pObj) ) + 
            Gia_MuxRef_rec( p, Gia_ObjFaninId1p(p, pObj) ) + 
            Gia_MuxRef_rec( p, Gia_ObjFaninId2p(p, pObj) ) + 1;
@@ -190,7 +190,7 @@ int Gia_MuxRef( Gia_Man_t * p, int iObj )
 int Gia_MuxDeref_rec( Gia_Man_t * p, int iObj )
 {
     Gia_Obj_t * pObj;
-    if ( !Gia_ObjIsMux(p, iObj) )
+    if ( !Gia_ObjIsMuxId(p, iObj) )
         return 0;
     pObj = Gia_ManObj( p, iObj );
     if ( Gia_ObjRefDec(p, pObj) )
@@ -202,7 +202,7 @@ int Gia_MuxDeref_rec( Gia_Man_t * p, int iObj )
 int Gia_MuxDeref( Gia_Man_t * p, int iObj )
 {
     Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
-    assert( Gia_ObjIsMux(p, iObj) );
+    assert( Gia_ObjIsMuxId(p, iObj) );
     return Gia_MuxDeref_rec( p, Gia_ObjFaninId0p(p, pObj) ) + 
            Gia_MuxDeref_rec( p, Gia_ObjFaninId1p(p, pObj) ) + 
            Gia_MuxDeref_rec( p, Gia_ObjFaninId2p(p, pObj) ) + 1;
@@ -210,7 +210,7 @@ int Gia_MuxDeref( Gia_Man_t * p, int iObj )
 int Gia_MuxMffcSize( Gia_Man_t * p, int iObj )
 {
     int Count1, Count2;
-    if ( !Gia_ObjIsMux(p, iObj) )
+    if ( !Gia_ObjIsMuxId(p, iObj) )
         return 0;
     Count1 = Gia_MuxDeref( p, iObj );
     Count2 = Gia_MuxRef( p, iObj );
@@ -232,10 +232,10 @@ int Gia_MuxMffcSize( Gia_Man_t * p, int iObj )
 void Gia_MuxStructPrint_rec( Gia_Man_t * p, int iObj, int fFirst )
 {
     Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
-    if ( !fFirst && (!Gia_ObjIsMux(p, iObj) || Gia_ObjRefNumId(p, iObj) > 0) )
+    if ( !fFirst && (!Gia_ObjIsMuxId(p, iObj) || Gia_ObjRefNumId(p, iObj) > 0) )
         return;
     printf( " [(%s", Gia_ObjFaninC2(p, pObj)? "!": "" );
-    if ( !Gia_ObjIsMux(p, Gia_ObjFaninId2p(p, pObj)) )
+    if ( !Gia_ObjIsMuxId(p, Gia_ObjFaninId2p(p, pObj)) )
         printf( "%d", Gia_ObjFaninId2p(p, pObj) );
     else
         Gia_MuxStructPrint_rec( p, Gia_ObjFaninId2p(p, pObj), 0 );
@@ -248,7 +248,7 @@ void Gia_MuxStructPrint_rec( Gia_Man_t * p, int iObj, int fFirst )
 void Gia_MuxStructPrint( Gia_Man_t * p, int iObj )
 {
     int Count1, Count2;
-    assert( Gia_ObjIsMux(p, iObj) );
+    assert( Gia_ObjIsMuxId(p, iObj) );
     Count1 = Gia_MuxDeref( p, iObj );
     Gia_MuxStructPrint_rec( p, iObj, 1 );
     Count2 = Gia_MuxRef( p, iObj );
@@ -287,7 +287,7 @@ void Gia_ManMuxProfiling( Gia_Man_t * p )
         Total++;
         nRefs = Gia_ObjRefNumId(pNew, i);
         assert( nRefs > 0 );
-        if ( nRefs > 1 || !Gia_ObjIsMux(pNew, Vec_IntEntry(vFans, i)) )
+        if ( nRefs > 1 || !Gia_ObjIsMuxId(pNew, Vec_IntEntry(vFans, i)) )
         {
             Roots++;
             Size = Gia_MuxMffcSize(pNew, i);
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index cf1aa762..760d7068 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -557,7 +557,7 @@ void Gia_ManCreateRefs( Gia_Man_t * p )
         {
             Gia_ObjRefFanin0Inc( p, pObj );
             Gia_ObjRefFanin1Inc( p, pObj );
-            if ( Gia_ObjIsMux(p, i) )
+            if ( Gia_ObjIsMuxId(p, i) )
                 Gia_ObjRefFanin2Inc( p, pObj );
         }
         else if ( Gia_ObjIsCo(pObj) )
@@ -1128,7 +1128,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
         printf( "XOR( %4d%s, %4d%s )", 
             Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), 
             Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") );
-    else if ( Gia_ObjIsMux(p, Gia_ObjId(p, pObj)) )
+    else if ( Gia_ObjIsMuxId(p, Gia_ObjId(p, pObj)) )
         printf( "MUX( %4d%s, %4d%s, %4d%s )", 
             Gia_ObjFaninId2p(p, pObj), (Gia_ObjFaninC2(p, pObj)? "\'" : " "), 
             Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " "), 
@@ -1482,7 +1482,7 @@ Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p )
                 Vec_IntWriteEntry(vFans, Gia_ObjFaninId0p(p, pObj), i);
             if ( Vec_IntEntry(vFans, Gia_ObjFaninId1p(p, pObj)) == 0 )
                 Vec_IntWriteEntry(vFans, Gia_ObjFaninId1p(p, pObj), i);
-            if ( Gia_ObjIsMux(p, i) && Vec_IntEntry(vFans, Gia_ObjFaninId2p(p, pObj)) == 0 )
+            if ( Gia_ObjIsMuxId(p, i) && Vec_IntEntry(vFans, Gia_ObjFaninId2p(p, pObj)) == 0 )
                 Vec_IntWriteEntry(vFans, Gia_ObjFaninId2p(p, pObj), i);
         }
         else if ( Gia_ObjIsCo(pObj) )
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index e28c9ad1..1bac1d4b 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \
     src/aig/gia/giaAigerExt.c \
+    src/aig/gia/giaBalance.c \
     src/aig/gia/giaBidec.c \
     src/aig/gia/giaCCof.c \
     src/aig/gia/giaCex.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e6d492c1..0b1c6b23 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -350,6 +350,7 @@ static int Abc_CommandAbc9Enable             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Dc2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bidec              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Shrink             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Balance            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Miter              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Miter2             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Append             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -908,6 +909,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&dc2",          Abc_CommandAbc9Dc2,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bidec",        Abc_CommandAbc9Bidec,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&shrink",       Abc_CommandAbc9Shrink,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&b",            Abc_CommandAbc9Balance,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&miter",        Abc_CommandAbc9Miter,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&miter2",       Abc_CommandAbc9Miter2,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&append",       Abc_CommandAbc9Append,       0 );
@@ -27405,6 +27407,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+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;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nlavh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by a char string.\n" );
+                goto usage;
+            }
+            nFanoutMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFanoutMax < 0 )
+                goto usage;
+            break;
+        case 'l':
+            fKeepLevel ^= 1;
+            break;
+        case 'a':
+            fSimpleAnd ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Balance(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManHasMapping(pAbc->pGia) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Balance(): The current AIG is mapped.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManBalance( pAbc->pGia, fSimpleAnd, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &b [-avh]\n" );
+    Abc_Print( -2, "\t         performs AIG balancing to reduce delay\n" );
+    Abc_Print( -2, "\t-a     : toggle using AND instead of AND/XOR/MUX [default = %s]\n", fSimpleAnd? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pFile;
diff --git a/src/map/mpm/mpmAbc.c b/src/map/mpm/mpmAbc.c
index 23643d06..43a23a66 100644
--- a/src/map/mpm/mpmAbc.c
+++ b/src/map/mpm/mpmAbc.c
@@ -91,7 +91,7 @@ Mig_Man_t * Mig_ManCreate( void * pGia )
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
-        if ( Gia_ObjIsMux(p, i) )
+        if ( Gia_ObjIsMuxId(p, i) )
             pObj->Value = Mig_ManAppendMux( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin2Copy(p, pObj) );
         else if ( Gia_ObjIsXor(pObj) )
             pObj->Value = Mig_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );