Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

9 files changed, 181 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 571a6ef8..af92acc9 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -82,7 +82,7 @@ struct Gia_Obj_t_
 
     unsigned       Value;         // application-specific value
 };
-// Value is currently use to store several types of information
+// 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
@@ -135,6 +135,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
+    int *          pTravIds;      // separate traversal ID representation
 };
 
 
@@ -309,13 +310,22 @@ static inline void         Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){
 static inline void         Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj));  }
 static inline void         Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj));  }
 
-static inline void         Gia_ManResetTravId( Gia_Man_t * p )                             { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1;  }
-static inline void         Gia_ManIncrementTravId( Gia_Man_t * p )                         { p->nTravIds++;                                 }
-static inline void         Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId )                { pObj->Value = TravId;                          }
-static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )      { pObj->Value = p->nTravIds;                     }
-static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )     { pObj->Value = p->nTravIds - 1;                 }
-static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )       { return ((int)pObj->Value == p->nTravIds);      }
-static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )      { return ((int)pObj->Value == p->nTravIds - 1);  }
+static inline void         Gia_ManResetTravId( Gia_Man_t * p )                              { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1;  }
+static inline void         Gia_ManIncrementTravId( Gia_Man_t * p )                          { p->nTravIds++;                                 }
+static inline void         Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId )                 { pObj->Value = TravId;                          }
+static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )       { pObj->Value = p->nTravIds;                     }
+static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )      { pObj->Value = p->nTravIds - 1;                 }
+static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )        { return ((int)pObj->Value == p->nTravIds);      }
+static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )       { return ((int)pObj->Value == p->nTravIds - 1);  }
+
+static inline void         Gia_ManResetTravIdArray( Gia_Man_t * p )                         { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1;  }
+static inline void         Gia_ManIncrementTravIdArray( Gia_Man_t * p )                     { p->nTravIds++;                                                    }
+static inline void         Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj )  { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds;                    }
+static inline void         Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1;                }
+static inline int          Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj )   { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds);          }
+static inline int          Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj )  { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1);      }
+static inline void         Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id )          { p->pTravIds[Id] = p->nTravIds;                 }
+static inline int          Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id )           { return (p->pTravIds[Id] == p->nTravIds);       }
 
 // AIG construction
 extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -402,6 +412,7 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
 static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr );                  }
 static inline int         Gia_ObjRepr( Gia_Man_t * p, int Id )               { return p->pReprs[Id].iRepr;         }
 static inline void        Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num )   { p->pReprs[Id].iRepr = Num;          }
+static inline void        Gia_ObjUnsetRepr( Gia_Man_t * p, int Id )          { p->pReprs[Id].iRepr = GIA_VOID;     }
 
 static inline int         Gia_ObjProved( Gia_Man_t * p, int Id )             { return p->pReprs[Id].fProved;       }
 static inline void        Gia_ObjSetProved( Gia_Man_t * p, int Id )          { p->pReprs[Id].fProved = 1;          }
@@ -423,12 +434,15 @@ static inline int         Gia_ObjNext( Gia_Man_t * p, int Id )               { r
 static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p->pNexts[Id] = Num;                }
 
 static inline int         Gia_ObjIsConst( Gia_Man_t * p, int Id )            { return Gia_ObjRepr(p, Id) == 0;                                   }
+static inline int         Gia_ObjIsUsed( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsHead( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsNone( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
 static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;                  }
 static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;                   }
 static inline int         Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k )  { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0;  }
 static inline int         Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k);                     }
+static inline int         Gia_ClassIsPair( Gia_Man_t * p, int i )            { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0;     }
+static inline void        Gia_ClassUndoPair( Gia_Man_t * p, int i )          { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0);       }
 
 #define Gia_ManForEachConst( p, i )                            \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
@@ -466,7 +480,9 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
 #define Gia_ManForEachObjReverse( p, pObj, i )                          \
     for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
-    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )  if ( !Gia_ObjIsAnd(pObj) ) {} else
+    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsAnd(pObj) ) {} else
+#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_ManForEachCi( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
@@ -498,6 +514,8 @@ extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+/*=== giaCTas.c ============================================================*/
+extern Vec_Int_t *         Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
@@ -508,6 +526,7 @@ extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int n
 extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes );
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
+extern Vec_Vec_t *         Gia_ManLevelize( Gia_Man_t * p );
 /*=== giaDup.c ============================================================*/
 extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
@@ -620,6 +639,7 @@ extern void                Gia_ManCheckMark1( Gia_Man_t * p );
 extern void                Gia_ManCleanValue( Gia_Man_t * p );
 extern void                Gia_ManFillValue( Gia_Man_t * p );
 extern void                Gia_ManSetPhase( Gia_Man_t * p );
+extern void                Gia_ManCleanPhase( Gia_Man_t * p );
 extern int                 Gia_ManLevelNum( Gia_Man_t * p );
 extern void                Gia_ManSetRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
@@ -636,6 +656,14 @@ 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 );
+/*=== giaUtil.c ===========================================================*/
+typedef struct Tas_Man_t_  Tas_Man_t;
+extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
+extern void                Tas_ManStop( Tas_Man_t * p );
+extern Vec_Int_t *         Tas_ReadModel( Tas_Man_t * p );
+extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
+extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 4b3692e4..07e74e34 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -271,6 +271,47 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t ** ppNodes;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pNexts == NULL && p->pReprs == NULL );
+    assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Gia_ManAndNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+    // create the PIs
+    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    ppNodes[0] = Aig_ManConst0(pNew);
+    Gia_ManForEachCi( p, pObj, i )
+        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) );        
+        if ( i % nOutDelta != 0 )
+            continue;
+        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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
 {
     Aig_Man_t * pMan;
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 507e5143..0e29bf06 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -50,6 +50,7 @@ extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSimple( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
+extern Aig_Man_t *         Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta );
 extern void                Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
  
 #ifdef __cplusplus
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index e005dfc2..644ccda5 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -1020,6 +1020,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     // solve for each output
     Gia_ManForEachCo( pAig, pRoot, i )
     {
+//        printf( "\n" );
+
         Vec_IntClear( vCex );
         if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
         {
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 8a3aef92..bcc1748f 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -264,6 +264,33 @@ int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Levelizes the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, Level, i;
+    nLevels = Gia_ManLevelNum( p );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Level = Gia_ObjLevel( p, pObj );
+        assert( Level <= nLevels );
+        Vec_VecPush( vLevels, Level, pObj );
+    }
+    return vLevels;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 041be0f5..8458268c 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -277,6 +277,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
+        int Ent;
+/*
         printf( "Const0 = " );
         Gia_ManForEachConst( p, i )
             printf( "%d ", i );
@@ -284,6 +286,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
         Counter = 0;
         Gia_ManForEachClass( p, i )
             Gia_ManEquivPrintOne( p, i, ++Counter );
+*/
+        Gia_ManLevelNum( p );
+        Gia_ManForEachClass( p, i )
+            if ( i % 100 == 0 )
+            {
+//                printf( "%d ", Gia_ManEquivCountOne(p, i) );
+                Gia_ClassForEachObj( p, i, Ent )
+                {
+                    printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
+                }
+                printf( "\n" );
+            }
     }
 }
 
@@ -370,6 +384,15 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
         printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+    // check if there are any equivalences defined
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjReprObj(p, i) != NULL )
+            break;
+    if ( i == Gia_ManObjNum(p) )
+    {
+        printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
+        return NULL;
+    }
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
@@ -720,6 +743,16 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
         printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+    // check if there are any equivalences defined
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjReprObj(p, i) != NULL )
+            break;
+    if ( i == Gia_ManObjNum(p) )
+    {
+        printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
+        return NULL;
+    }
+
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 7f4da081..37afde13 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -70,6 +70,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pTravIds );
     ABC_FREE( p->pPlacement );
     ABC_FREE( p->pSwitching );
     ABC_FREE( p->pCexSeq );
@@ -203,10 +204,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 void Gia_ManPrintStatsShort( Gia_Man_t * p )
 {
     printf( "i/o =%7d/%7d  ", Gia_ManPiNum(p), Gia_ManPoNum(p) );
-//    printf( "ff =%7d  ", Gia_ManRegNum(p) );
+    printf( "ff =%7d  ", Gia_ManRegNum(p) );
     printf( "and =%8d  ", Gia_ManAndNum(p) );
     printf( "lev =%5d  ", Gia_ManLevelNum(p) );
-    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+//    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
     printf( "\n" );
 }
  
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 54bc98dd..938c6363 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -317,6 +317,25 @@ void Gia_ManSetPhase( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets phases of the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCleanPhase( Gia_Man_t * p )  
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fPhase = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Assigns levels.]
 
   Description []
@@ -883,17 +902,32 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
             Counter1++;
+        }
+//        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+//            Counter2++;
+    }
+//    printf( "\n" );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+//        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+//            Counter1++;
         if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
             Counter2++;
+        }
     }
+//    printf( "\n" );
     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 );
+    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
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 6f70f7d3..79bfa2fb 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -4,6 +4,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaCof.c \
     src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \
+    src/aig/gia/giaCTas.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
     src/aig/gia/giaEmbed.c \