Adding support of XOR/MUX in GIA.

7 files changed, 341 insertions, 48 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a7ab5c75..c184950e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -89,8 +89,6 @@ struct Gia_Obj_t_
 // Value is currently used to store several types of information
 // - pointer to the next node in the hash table during structural hashing
 // - pointer to the node copy during duplication 
-// - traversal ID of the node during traversal
-// - reference counter of the node (will not be used in the future)
 
 // new AIG manager
 typedef struct Gia_Man_t_ Gia_Man_t;
@@ -103,6 +101,9 @@ struct Gia_Man_t_
     int            nObjs;         // number of objects
     int            nObjsAlloc;    // number of allocated objects
     Gia_Obj_t *    pObjs;         // the array of objects
+    unsigned *     pMuxes;        // control signals of MUXes
+    int            nXors;         // the number of XORs
+    int            nMuxes;        // the number of MUXes 
     Vec_Int_t *    vCis;          // the vector of CIs (PIs + LOs)
     Vec_Int_t *    vCos;          // the vector of COs (POs + LIs)
     int *          pHTable;       // hash table
@@ -302,6 +303,8 @@ static inline int          Gia_ManPoNum( Gia_Man_t * p )       { return Vec_IntS
 static inline int          Gia_ManRegNum( Gia_Man_t * p )      { return p->nRegs;                                                          }
 static inline int          Gia_ManObjNum( Gia_Man_t * p )      { return p->nObjs;                                                          }
 static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1;        }
+static inline int          Gia_ManXorNum( Gia_Man_t * p )      { return p->nXors;                                                          }
+static inline int          Gia_ManMuxNum( Gia_Man_t * p )      { return p->nMuxes;                                                         }
 static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                                }
 static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;                                                       }
 static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
@@ -317,23 +320,25 @@ static inline Gia_Obj_t *  Gia_ManPo( Gia_Man_t * p, int v )   { assert( v < Gia
 static inline Gia_Obj_t *  Gia_ManRo( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); }
 static inline Gia_Obj_t *  Gia_ManRi( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); }
 
+static inline int          Gia_ObjId( Gia_Man_t * p, Gia_Obj_t * pObj )        { assert( p->pObjs <= pObj && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
+static inline int          Gia_ObjCioId( Gia_Obj_t * pObj )                    { assert( pObj->fTerm ); return pObj->iDiff1;                 }
+static inline void         Gia_ObjSetCioId( Gia_Obj_t * pObj, int v )          { assert( pObj->fTerm ); pObj->iDiff1 = v;                    }
+static inline int          Gia_ObjValue( Gia_Obj_t * pObj )                    { return pObj->Value;                                         }
+static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          { pObj->Value = i;                                            }
+static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
+static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
+
 static inline int          Gia_ObjIsTerm( Gia_Obj_t * pObj )                   { return pObj->fTerm;                             } 
 static inline int          Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj )            { return!pObj->fTerm;                             } 
 static inline int          Gia_ObjIsCi( Gia_Obj_t * pObj )                     { return pObj->fTerm && pObj->iDiff0 == GIA_NONE; } 
 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, Gia_Obj_t * pObj )     { return p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)] > 0;    } 
 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; } 
 static inline int          Gia_ManObjIsConst0( Gia_Man_t * p, Gia_Obj_t * pObj){ return pObj == p->pObjs;                        } 
 
-static inline int          Gia_ObjId( Gia_Man_t * p, Gia_Obj_t * pObj )        { assert( p->pObjs <= pObj && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
-static inline int          Gia_ObjCioId( Gia_Obj_t * pObj )                    { assert( Gia_ObjIsTerm(pObj) ); return pObj->iDiff1;         }
-static inline void         Gia_ObjSetCioId( Gia_Obj_t * pObj, int v )          { assert( Gia_ObjIsTerm(pObj) ); pObj->iDiff1 = v;            }
-static inline int          Gia_ObjValue( Gia_Obj_t * pObj )                    { return pObj->Value;                                         }
-static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          { pObj->Value = i;                                            }
-static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
-static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
-
 static inline int          Gia_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); }
 static inline Gia_Obj_t *  Gia_Lit2Obj( Gia_Man_t * p, int iLit )              { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit));  }
 
@@ -353,18 +358,25 @@ static inline int          Gia_ObjDiff0( Gia_Obj_t * pObj )                    {
 static inline int          Gia_ObjDiff1( Gia_Obj_t * pObj )                    { return pObj->iDiff1;         }
 static inline int          Gia_ObjFaninC0( Gia_Obj_t * pObj )                  { return pObj->fCompl0;        }
 static inline int          Gia_ObjFaninC1( Gia_Obj_t * pObj )                  { return pObj->fCompl1;        }
+static inline int          Gia_ObjFaninC2( Gia_Man_t * p, Gia_Obj_t * pObj )   { return p->pMuxes && Abc_LitIsCompl(p->pMuxes[Gia_ObjId(p, pObj)]);  }
 static inline Gia_Obj_t *  Gia_ObjFanin0( Gia_Obj_t * pObj )                   { return pObj - pObj->iDiff0;  }
 static inline Gia_Obj_t *  Gia_ObjFanin1( Gia_Obj_t * pObj )                   { return pObj - pObj->iDiff1;  }
+static inline Gia_Obj_t *  Gia_ObjFanin2( Gia_Man_t * p, Gia_Obj_t * pObj )    { return p->pMuxes ? Gia_ManObj(p, Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)])) : NULL;  }
 static inline Gia_Obj_t *  Gia_ObjChild0( Gia_Obj_t * pObj )                   { return Gia_NotCond( Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj) ); }
 static inline Gia_Obj_t *  Gia_ObjChild1( Gia_Obj_t * pObj )                   { return Gia_NotCond( Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj) ); }
+static inline Gia_Obj_t *  Gia_ObjChild2( Gia_Man_t * p, Gia_Obj_t * pObj )    { return Gia_NotCond( Gia_ObjFanin2(p, pObj), Gia_ObjFaninC2(p, pObj) ); }
 static inline int          Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId )      { return ObjId - pObj->iDiff0;    }
 static inline int          Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId )      { return ObjId - pObj->iDiff1;    }
+static inline int          Gia_ObjFaninId2( Gia_Man_t * p, int ObjId )         { return (p->pMuxes && p->pMuxes[ObjId]) ? Abc_Lit2Var(p->pMuxes[ObjId]) : -1; }
 static inline int          Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) );              }
 static inline int          Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) );              }
+static inline int          Gia_ObjFaninId2p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? Abc_Lit2Var(p->pMuxes[Gia_ObjId(p, pObj)]) : -1; }
 static inline int          Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
 static inline int          Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
+static inline int          Gia_ObjFaninLit2( Gia_Man_t * p, int ObjId )        { return (p->pMuxes && p->pMuxes[ObjId]) ? p->pMuxes[ObjId] : -1;           }
 static inline int          Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );    }
 static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) );    }
+static inline int          Gia_ObjFaninLit2p( Gia_Man_t * p, Gia_Obj_t * pObj) { return (p->pMuxes && p->pMuxes[Gia_ObjId(p, pObj)]) ? p->pMuxes[Gia_ObjId(p, pObj)] : -1;    }
 static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1;          }
 static inline int          Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
 
@@ -372,9 +384,11 @@ static inline int          Gia_ManPoIsConst0( Gia_Man_t * p, int iPoIndex )    {
 static inline int          Gia_ManPoIsConst1( Gia_Man_t * p, int iPoIndex )    { return Gia_ManIsConst1Lit( Gia_ObjFaninLit0p(p, Gia_ManPo(p, iPoIndex)) ); }
 
 static inline Gia_Obj_t *  Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) );                              }
+static inline int          Gia_ObjLitCopy( Gia_Man_t * p, int iLit )           { return Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(iLit))->Value, Abc_LitIsCompl(iLit));     }
 
 static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
 static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
+static inline int          Gia_ObjFanin2Copy( Gia_Man_t * p, Gia_Obj_t * pObj ){ return Abc_LitNotCond(Gia_ObjFanin2(p, pObj)->Value, Gia_ObjFaninC2(p, pObj)); }
 
 static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
 static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
@@ -446,6 +460,11 @@ static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
         assert( p->nObjsAlloc > 0 );
         p->pObjs = ABC_REALLOC( Gia_Obj_t, p->pObjs, 2 * p->nObjsAlloc );
         memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gia_Obj_t) * p->nObjsAlloc );
+        if ( p->pMuxes )
+        {
+            p->pMuxes = ABC_REALLOC( unsigned, p->pMuxes, 2 * p->nObjsAlloc );
+            memset( p->pMuxes + p->nObjsAlloc, 0, sizeof(unsigned) * p->nObjsAlloc );
+        }
         p->nObjsAlloc *= 2;
     }
     return Gia_ManObj( p, p->nObjs++ );
@@ -464,7 +483,7 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
     assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
     assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
-    assert( iLit0 != iLit1 );
+    assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
     if ( iLit0 < iLit1 )
     {
         pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
@@ -494,6 +513,42 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     }
     return Gia_ObjId( p, pObj ) << 1;
 }
+static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 )  
+{ 
+    Gia_Obj_t * pObj = Gia_ManAppendObj( p );
+    assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
+    assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
+    assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
+    assert( !Abc_LitIsCompl(iLit0) );
+    assert( !Abc_LitIsCompl(iLit1) );
+    assert( Abc_Lit2Var(iLit0) > Abc_Lit2Var(iLit1) );
+    pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
+    pObj->fCompl0 = Abc_LitIsCompl(iLit0);
+    pObj->iDiff1  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
+    pObj->fCompl1 = Abc_LitIsCompl(iLit1);
+    p->nXors++;
+    return Gia_ObjId( p, pObj ) << 1;
+}
+static inline int Gia_ManAppendMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )  
+{ 
+    Gia_Obj_t * pObj = Gia_ManAppendObj( p );
+    assert( p->pMuxes != NULL );
+    assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
+    assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
+    assert( iLitC >= 0 && Abc_Lit2Var(iLitC) < Gia_ManObjNum(p) );
+    assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
+    assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit0) );
+    assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit1) );
+    assert( Abc_Lit2Var(iLit0) < Abc_Lit2Var(iLit1) );
+    assert( !Abc_LitIsCompl(iLit1) );
+    pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
+    pObj->fCompl0 = Abc_LitIsCompl(iLit0);
+    pObj->iDiff1  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
+    pObj->fCompl1 = Abc_LitIsCompl(iLit1);
+    p->pMuxes[Gia_ObjId(p, pObj)] = iLitC;
+    p->nMuxes++;
+    return Gia_ObjId( p, pObj ) << 1;
+}
 static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )  
 { 
     Gia_Obj_t * pObj;
@@ -913,7 +968,9 @@ extern void                Gia_ManFrontTest( Gia_Man_t * p );
 /*=== giaHash.c ===========================================================*/
 extern void                Gia_ManHashAlloc( Gia_Man_t * p ); 
 extern void                Gia_ManHashStart( Gia_Man_t * p ); 
-extern void                Gia_ManHashStop( Gia_Man_t * p );  
+extern void                Gia_ManHashStop( Gia_Man_t * p );
+extern int                 Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 );
+extern int                 Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 );
 extern int                 Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ); 
 extern int                 Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 ); 
 extern int                 Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ); 
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 11b56eda..fd5996c9 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1014,6 +1014,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     unsigned char * pBuffer;
     unsigned uLit0, uLit1, uLit;
 //    assert( Gia_ManIsNormalized(pInit) );
+    assert( pInit->nXors == 0 && pInit->nMuxes == 0 );
 
     if ( Gia_ManCoNum(pInit) == 0 )
     {
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 15d77dea..2c7fd59b 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -752,6 +752,8 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     int i, nRos = 0, nRis = 0;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    if ( p->pMuxes )
+        pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
     pNew->nConstrs = p->nConstrs;
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
@@ -762,7 +764,14 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
             continue;
         pObj->fMark0 = 0;
         if ( Gia_ObjIsAnd(pObj) )
-            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        {
+            if ( Gia_ObjIsXor(pObj) )
+                pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+            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) );
+        }
         else if ( Gia_ObjIsCi(pObj) )
         {
             pObj->Value = Gia_ManAppendCi( pNew );
@@ -2350,6 +2359,132 @@ Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAn
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA with MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC;
+    int i;
+    assert( p->pMuxes == NULL );
+    // start the new manager
+    pNew = Gia_ManStart( 5000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
+    // create constant
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManHashStart( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjIsMuxType(pObj) )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan0)), Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan1)) );
+        else
+        {
+            pFanC = Gia_ObjRecognizeMux( pObj, &pFan1, &pFan0 );
+            pObj->Value = Gia_ManHashMuxReal( pNew, Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFanC)), Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan1)), Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan0)) );
+        }
+    }
+    Gia_ManHashStop( pNew );
+    // create ROs
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // perform cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives GIA without MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pMuxes != NULL );
+    // start the new manager
+    pNew = Gia_ManStart( 5000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // create constant
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Gia_ManHashStart( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjIsMux(p, pObj) )
+            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) );
+        else 
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
+    Gia_ManHashStop( pNew );
+    // create ROs
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // perform cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Test these procedures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew, * pNew2;
+    pNew = Gia_ManDupMuxes( p );
+    pNew2 = Gia_ManDupNoMuxes( pNew );
+    Gia_ManPrintStats( p, 0, 0, 0 );
+    Gia_ManPrintStats( pNew, 0, 0, 0 );
+    Gia_ManPrintStats( pNew2, 0, 0, 0 );
+    Gia_ManStop( pNew );
+//    Gia_ManStop( pNew2 );
+    return pNew2;
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index f0204089..b256b165 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Hashing the node.]
+  Synopsis    [Returns the place where this node is stored (or should be stored).]
 
   Description []
                
@@ -42,35 +42,25 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_ManHashOne( int iLit0, int iLit1, int TableSize ) 
+static inline int Gia_ManHashOne( int iLit0, int iLit1, int iLitC, int TableSize ) 
 {
-    unsigned Key = 0;
-    assert( iLit0 < iLit1 );
-    Key ^= Abc_Lit2Var(iLit0) * 7937;
-    Key ^= Abc_Lit2Var(iLit1) * 2971;
-    Key ^= Abc_LitIsCompl(iLit0) * 911;
-    Key ^= Abc_LitIsCompl(iLit1) * 353;
+    unsigned Key = iLitC * 2011;
+    Key += Abc_Lit2Var(iLit0) * 7937;
+    Key += Abc_Lit2Var(iLit1) * 2971;
+    Key += Abc_LitIsCompl(iLit0) * 911;
+    Key += Abc_LitIsCompl(iLit1) * 353;
     return (int)(Key % TableSize);
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the place where this node is stored (or should be stored).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
+static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1, int iLitC )
 {
     Gia_Obj_t * pThis;
-    int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, p->nHTable );
+    int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, iLitC, p->nHTable );
+    assert( p->pMuxes || iLit0 < iLit1 );
+    assert( iLit0 < iLit1 || (!Abc_LitIsCompl(iLit0) && !Abc_LitIsCompl(iLit1)) );
+    assert( iLitC == -1 || !Abc_LitIsCompl(iLit1) );
     for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis; 
           pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL )
-              if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 )
+              if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 && (p->pMuxes == NULL || Gia_ObjFaninLit2p(p, pThis) == iLitC) )
                   break;
     return pPlace;
 }
@@ -92,7 +82,7 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
     int iLit1 = Gia_ObjToLit( p, p1 );
     if ( iLit0 > iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
-    return *Gia_ManHashFind( p, iLit0, iLit1 );
+    return *Gia_ManHashFind( p, iLit0, iLit1, -1 );
 }
 
 /**Function*************************************************************
@@ -132,7 +122,7 @@ void Gia_ManHashStart( Gia_Man_t * p )
     Gia_ManCleanValue( p );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
+        pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i), Gia_ObjFaninLit2(p, i) );
         assert( *pPlace == 0 );
         *pPlace = Abc_Var2Lit( i, 0 );
     }
@@ -186,7 +176,7 @@ void Gia_ManHashResize( Gia_Man_t * p )
           iNext = (pThis? pThis->Value : 0)  )
     {
         pThis->Value = 0;
-        pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis) );
+        pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis), Gia_ObjFaninLit2p(p, pThis) );
         assert( *pPlace == 0 ); // should not be there
         *pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 );
         assert( *pPlace != 0 );
@@ -463,7 +453,104 @@ static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_O
 
 /**Function*************************************************************
 
-  Synopsis    [Rehashes AIG with mapping.]
+  Synopsis    [Hashes XOR gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )  
+{ 
+    int fCompl = 0;
+    assert( p->fAddStrash == 0 );
+    if ( iLit0 < 2 )
+        return iLit0 ? Abc_LitNot(iLit1) : iLit1;
+    if ( iLit1 < 2 )
+        return iLit1 ? Abc_LitNot(iLit0) : iLit0;
+    if ( iLit0 == iLit1 )
+        return 0;
+    if ( iLit0 == Abc_LitNot(iLit1) )
+        return 1;
+    if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
+        Gia_ManHashResize( p );
+    if ( iLit0 < iLit1 )
+        iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
+    if ( Abc_LitIsCompl(iLit0) )
+        iLit0 = Abc_LitNot(iLit0), fCompl ^= 1;
+    if ( Abc_LitIsCompl(iLit1) )
+        iLit1 = Abc_LitNot(iLit1), fCompl ^= 1;
+    {
+        int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
+        if ( *pPlace )
+        {
+            p->nHashHit++;
+            return Abc_LitNotCond( *pPlace, fCompl );
+        }
+        p->nHashMiss++;
+        if ( p->nObjs < p->nObjsAlloc )
+            *pPlace = Gia_ManAppendXorReal( p, iLit0, iLit1 );
+        else
+        {
+            int iNode = Gia_ManAppendXorReal( p, iLit0, iLit1 );
+            pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
+            assert( *pPlace == 0 );
+            *pPlace = iNode;
+        }
+        return Abc_LitNotCond( *pPlace, fCompl );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashes MUX gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )  
+{
+    int fCompl = 0;
+    assert( p->fAddStrash == 0 );
+    assert( iLit0 > 1 && iLit1 > 1 && iLitC > 1 );
+    if ( iLit0 == iLit1 )
+        return iLit0;
+    if ( Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) )
+        return Gia_ManHashXorReal( p, iLitC, iLit0 );
+    if ( iLit0 > iLit1 )
+        iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1, iLitC = Abc_LitNot(iLitC);
+    if ( Abc_LitIsCompl(iLit1) )
+        iLit0 = Abc_LitNot(iLit0), iLit1 = Abc_LitNot(iLit1), fCompl = 1;
+    {
+        int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
+        if ( *pPlace )
+        {
+            p->nHashHit++;
+            return Abc_LitNotCond( *pPlace, fCompl );
+        }
+        p->nHashMiss++;
+        if ( p->nObjs < p->nObjsAlloc )
+            *pPlace = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
+        else
+        {
+            int iNode = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
+            pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
+            assert( *pPlace == 0 );
+            *pPlace = iNode;
+        }
+        return Abc_LitNotCond( *pPlace, fCompl );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashes AND gate.]
 
   Description []
                
@@ -493,7 +580,7 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     if ( iLit0 > iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
     {
-        int * pPlace = Gia_ManHashFind( p, iLit0, iLit1 );
+        int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
         if ( *pPlace )
         {
             p->nHashHit++;
@@ -505,7 +592,7 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
         else
         {
             int iNode = Gia_ManAppendAnd( p, iLit0, iLit1 );
-            pPlace = Gia_ManHashFind( p, iLit0, iLit1 );
+            pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
             assert( *pPlace == 0 );
             return *pPlace = iNode;
         }
@@ -518,7 +605,7 @@ int Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Rehashes AIG with mapping.]
+  Synopsis    []
 
   Description []
                
@@ -540,7 +627,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
     if ( iLit0 > iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
     {
-        int * pPlace = Gia_ManHashFind( p, iLit0, iLit1 );
+        int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
         if ( *pPlace ) 
             return *pPlace;
         return -1;
@@ -549,7 +636,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Rehashes AIG with mapping.]
+  Synopsis    []
 
   Description []
                
@@ -568,7 +655,7 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Rehashes AIG with mapping.]
+  Synopsis    []
 
   Description []
                
@@ -586,7 +673,7 @@ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
 
 /**Function*************************************************************
 
-  Synopsis    [Rehashes AIG with mapping.]
+  Synopsis    [Rehashes AIG.]
 
   Description []
                
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 823941a8..8670993d 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -120,6 +120,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pRefs );
 //    ABC_FREE( p->pNodeRefs );
     ABC_FREE( p->pHTable );
+    ABC_FREE( p->pMuxes );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pSpec );
     ABC_FREE( p->pName );
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index 9b4c1c3e..727ffa90 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -52,7 +52,8 @@ int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
     assert( Gia_ObjIsAnd(pObj) );
     return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
              + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) )
-             + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0);
+             + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0)
+             + (p->pMuxes ? Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin2(p, pObj) ) : 0);
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index cb97e0bf..a076beb9 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1120,6 +1120,15 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
         printf( "RI( %4d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
 //    else if ( Gia_ObjIsBuf(pObj) )
 //        printf( "BUF( %d%s )", Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
+    else if ( Gia_ObjIsXor(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, pObj) )
+        printf( "MUX( %4d%s, %4d%s, %4d%s )", 
+            Gia_ObjFaninId2p(p, pObj), (Gia_ObjFaninC2(p, pObj)? "\'" : " "), 
+            Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " "), 
+            Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " ") );
     else
         printf( "AND( %4d%s, %4d%s )", 
             Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), 
@@ -1156,6 +1165,8 @@ void Gia_ManPrint( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i;
+    printf( "GIA manage has %d ANDs, %d XORs, %d MUXes.\n", 
+        Gia_ManAndNum(p) - Gia_ManXorNum(p) - Gia_ManMuxNum(p), Gia_ManXorNum(p), Gia_ManMuxNum(p) ); 
     Gia_ManForEachObj( p, pObj, i )
         Gia_ObjPrint( p, pObj );
 }