9 files changed, 488 insertions, 50 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index feee5472..2d633d5c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -418,6 +418,7 @@ static inline int         Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c )  { i
 static inline int         Gia_ObjDiffColors( Gia_Man_t * p, int i, int j )   { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
 static inline int         Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j )  { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
 
+static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id )            { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );}
 static inline int         Gia_ObjNext( Gia_Man_t * p, int Id )               { return p->pNexts[Id];               }
 static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p->pNexts[Id] = Num;                }
 
@@ -535,6 +536,8 @@ extern Gia_Man_t *         Gia_ManRemoveEnables( Gia_Man_t * p );
 /*=== giaEquiv.c ==========================================================*/
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
+extern void                Gia_ManDeriveReprs( Gia_Man_t * p );
+extern int                 Gia_ManEquivCountClasses( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
 extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
@@ -544,6 +547,7 @@ extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int f
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
 extern void                Gia_ManEquivImprove( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
 /*=== giaFanout.c =========================================================*/
 extern void                Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
 extern void                Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -629,6 +633,8 @@ extern Gia_Cex_t *         Gia_ManAllocCounterExample( int nRegs, int nRealPis,
 extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
 extern void                Gia_ManPrintCounterExample( Gia_Cex_t * p );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
+extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern int                 Gia_ManHasDandling( Gia_Man_t * p );
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 601b85af..a4f1ab44 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -45,19 +45,24 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Obj_t * pObj )
+void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    if ( pObj->pData )
+    Aig_Obj_t * pNext;
+    if ( pObj->iData )
         return;
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        pObj->iData = Gia_ManAppendCi( pNew );
-        return;
-    }
     assert( Aig_ObjIsNode(pObj) );
-    Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
-    Gia_ManFromAig_rec( pNew, Aig_ObjFanin1(pObj) );
+    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+    if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
+    {
+        int iObjNew, iNextNew;
+        Gia_ManFromAig_rec( pNew, p, pNext );
+        iObjNew  = Gia_Lit2Var(pObj->iData);
+        iNextNew = Gia_Lit2Var(pNext->iData);
+        if ( pNew->pNexts )
+            pNew->pNexts[iObjNew] = iNextNew;        
+    }
 }
 
 /**Function*************************************************************
@@ -76,26 +81,25 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
-    // add fake POs to all the dangling nodes (choices)
-    Aig_ManForEachNode( p, pObj, i )
-        assert( Aig_ObjRefs(pObj) > 0 );
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    // create room to store equivalences
+    if ( p->pEquivs )
+        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
     Aig_ManForEachPi( p, pObj, i )
-    {
-//        if ( Aig_ObjRefs(pObj) == 0 )
-            pObj->iData = Gia_ManAppendCi( pNew );
-    }
+        pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachPo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachPo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    if ( pNew->pNexts )
+        Gia_ManDeriveReprs( pNew );
     return pNew;
 }
 
@@ -117,7 +121,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Gia_UtilStrsav( p->pName );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
@@ -127,12 +131,12 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     Aig_ManForEachNode( p, pObj, i )
         if ( Aig_ObjRefs(pObj) == 0 )
         {
-            Gia_ManFromAig_rec( pNew, pObj );        
+            Gia_ManFromAig_rec( pNew, p, pObj );        
             Gia_ManAppendCo( pNew, pObj->iData );
         }
     // add logic for the POs
     Aig_ManForEachPo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachPo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
@@ -152,17 +156,27 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
 ***********************************************************************/
 void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
+    Gia_Obj_t * pNext;
     if ( ppNodes[Gia_ObjId(p, pObj)] )
         return;
     if ( Gia_ObjIsCi(pObj) )
-    {
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
-        return;
+    else
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+    }
+    if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
+    {
+        Aig_Obj_t * pObjNew, * pNextNew;
+        Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
+        pObjNew  = ppNodes[Gia_ObjId(p, pObj)];
+        pNextNew = ppNodes[Gia_ObjId(p, pNext)];
+        if ( pNew->pEquivs )
+            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
     }
-    assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
-    Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
-    ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
 }
 
 /**Function*************************************************************
@@ -176,37 +190,31 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
+Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
-
+    assert( !fChoices || (p->pNexts && p->pReprs) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+    // duplicate representation of choice nodes
+    if ( fChoices )
+        pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the PIs
+    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     ppNodes[0] = Aig_ManConst0(pNew);
     Gia_ManForEachCi( p, pObj, i )
-    {
-//        if ( Aig_ObjRefs(pObj) == 0 )
-            ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
-    }
-
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
-/*
-    Gia_ManForEachCo( p, pObj, i )
-        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
-    Gia_ManForEachCo( p, pObj, i )
-        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
-*/
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
@@ -230,7 +238,7 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
     pGia = Gia_ManFromAig( p );
     pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
     Gia_ManStop( pTemp );
-    pMan = Gia_ManToAig( pGia );
+    pMan = Gia_ManToAig( pGia, 0 );
     Gia_ManStop( pGia );
     return pMan;
 }
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 07cf7bae..0c0ee598 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -48,7 +48,7 @@
 /*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
-extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
+extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 8dbc0cab..afe9164f 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -413,7 +413,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
     pName = Gia_FileNameGeneric( pFileName );
     pNew->pName = Gia_UtilStrsav( pName );
-//    pNew->pSpec = Aig_UtilStrsav( pFileName );
+//    pNew->pSpec = Gia_UtilStrsav( pFileName );
     ABC_FREE( pName );
 
     // prepare the array of nodes
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index bd5297e4..63748403 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -387,6 +387,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     {
         if ( pObj->fMark0 )
             continue;
+        pObj->fMark0 = 0;
         if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
@@ -396,14 +397,32 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
         }
         else if ( Gia_ObjIsCo(pObj) )
         {
-            Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
-
+//            Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
             nRis += Gia_ObjIsRi(p, pObj);
         }
     }
     assert( nRos == nRis );
     Gia_ManSetRegNum( pNew, nRos );
+    if ( p->pReprs && p->pNexts )
+    {
+        Gia_Obj_t * pRepr;
+        pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+        for ( i = 0; i < Gia_ManObjNum(p); i++ )
+            Gia_ObjSetRepr( pNew, i, GIA_VOID );
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( !~pObj->Value )
+                continue;
+            pRepr = Gia_ObjReprObj( p, i );
+            if ( pRepr == NULL )
+                continue;
+            assert( ~pRepr->Value );
+            if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) )
+                Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) ); 
+        }
+        pNew->pNexts = Gia_ManDeriveNexts( pNew );
+    }
     return pNew;
 }
 
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index f802e15d..cdee73d0 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -94,7 +94,8 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 {
     unsigned * pNexts, * pTails;
     int i;
-    assert( p->pReprs );
+    assert( p->pReprs != NULL );
+    assert( p->pNexts == NULL );
     pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
     pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
@@ -112,6 +113,37 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Given points to the next objects, derives representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDeriveReprs( Gia_Man_t * p )
+{
+    int i, iObj;
+    assert( p->pReprs == NULL );
+    assert( p->pNexts != NULL );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( p->pNexts[i] == 0 )
+            continue;
+        if ( p->pReprs[i].iRepr != GIA_VOID )
+            continue;
+        // next is set, repr is not set
+        for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
+            p->pReprs[iObj].iRepr = i;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -186,6 +218,25 @@ int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManEquivCountClasses( Gia_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        Counter += Gia_ObjIsHead(p, i);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
 {
     int nLitsReal = Gia_ManEquivCountLitsAll( p );
@@ -966,6 +1017,246 @@ void Gia_ManEquivImprove( Gia_Man_t * p )
 //    p->pNexts = Gia_ManDeriveNexts( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+    if ( Gia_ObjIsCi(pNode) )
+        return 0;
+//    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
+//        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( pNode->fMark0 )
+        return 0;
+    pNode->fMark0 = 1;
+    Vec_PtrPush( vVisited, pNode );
+    // check the children
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
+        return 1;
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
+        return 1;
+    // check equivalent nodes
+    return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    Vec_Ptr_t * vVisited;
+    Gia_Obj_t * pObj;
+    int RetValue, i;
+    assert( !Gia_IsComplement(pOld) );
+    assert( !Gia_IsComplement(pNode) );
+    vVisited = Vec_PtrAlloc( 100 );
+    RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
+    Vec_PtrForEachEntry( vVisited, pObj, i )
+        pObj->fMark0 = 0;
+    Vec_PtrFree( vVisited );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the next entry while making choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
+    {
+        Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
+        return;
+    }
+    Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
+    if ( ~pObj->Value )
+        return;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        if ( Gia_ObjIsConst0(pRepr) )
+        {
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        Gia_ManEquivToChoices_rec( pNew, p, pRepr );
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
+        {
+            assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
+            return;
+        }
+        assert( pRepr->Value < pObj->Value );
+        pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
+        pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
+        {
+            assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
+        {
+            assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
+            Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
+            Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
+        }
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes choices, which contain fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRemoveBadChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, iObj, iPrev, Counter = 0;
+    // mark nodes with fanout
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    // go through the classes and remove 
+    Gia_ManForEachClass( p, i )
+    {
+        for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
+        {
+            if ( !Gia_ManObj(p, iObj)->fMark0 )
+            {
+                iPrev = iObj; 
+                continue;
+            }
+            Gia_ObjSetRepr( p, iObj, GIA_VOID );
+            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
+            Gia_ObjSetNext( p, iObj, 0 );
+            Counter++;
+        } 
+    }
+    // remove the marks
+    Gia_ManCleanMark0( p );
+//    printf( "Removed %d bad choices.\n", Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces AIG using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachRo( p, pObj, i )
+        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+        {
+            assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
+            pObj->Value = pRepr->Value;
+        }
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( i % nSnapshots == 0 )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Gia_ManRemoveBadChoices( pNew );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index f69ac266..7f4da081 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -158,7 +158,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p )
 void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 {
     if ( p->pName )
-        printf( "%8s : ", p->pName );
+        printf( "%-8s : ", p->pName );
     printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
     if ( Gia_ManRegNum(p) )
         printf( "  ff =%7d", Gia_ManRegNum(p) );
@@ -166,6 +166,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
     printf( "  lev =%5d", Gia_ManLevelNum(p) );
     printf( "  cut =%5d", Gia_ManCrossCut(p) );
     printf( "  mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+    if ( Gia_ManHasDandling(p) )
+        printf( "  ch =%5d", Gia_ManEquivCountClasses(p) );
     if ( fSwitch )
     {
         if ( p->pSwitching )
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index cf72104f..5ac8e04a 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -41,12 +41,15 @@
 ***********************************************************************/
 int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
+    if ( pObj == NULL )
+        return 0;
     if ( !pObj->fMark0 )
         return 0;
     pObj->fMark0 = 0;
     assert( Gia_ObjIsAnd(pObj) );
     return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
-             + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) );
+             + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) )
+             + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0);
 }
 
 /**Function*************************************************************
@@ -88,6 +91,7 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
     return Gia_ManDupMarked( p );
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Marks CIs/COs/ANDs unreachable from POs.]
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 5716c1a0..54bc98dd 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -858,6 +858,114 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
     return ConeSize1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter1 = 0, Counter2 = 0;
+    int nFailNoRepr = 0;
+    int nFailHaveRepr = 0;
+    int nChoiceNodes = 0;
+    int nChoices = 0;
+    if ( p->pReprs == NULL || p->pNexts == NULL )
+        return 0;
+    // check if there are any representatives
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+            Counter1++;
+        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+            Counter2++;
+    }
+    if ( Counter1 == 0 )
+    {
+        printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
+        return 0;
+    }
+//    printf( "%d nodes have reprs.\n", Counter1 );
+//    printf( "%d nodes have nexts.\n", Counter2 );
+    // check if there are any internal nodes without fanout
+    // make sure all nodes without fanout have representatives
+    // make sure all nodes with fanout have no representatives
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjRefs(p, pObj) == 0 )
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
+                nFailNoRepr++;
+            else
+                nChoices++;
+        }
+        else
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nFailHaveRepr++;
+            if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nChoiceNodes++;
+        }
+        if ( Gia_ObjReprObj( p, i ) )
+            assert( Gia_ObjRepr(p, i) < i );
+    }
+    if ( nChoices == 0 )
+        return 0;
+    if ( nFailNoRepr )
+    {
+        printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
+//        return 0;
+    }
+    if ( nFailHaveRepr )
+    {
+        printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
+//        return 0;
+    }
+//    printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has dangling nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasDandling( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        Counter += !pObj->fMark0;
+    Gia_ManCleanMark0( p );
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////