Testing GIA with time manager.

5 files changed, 19 insertions, 28 deletions

diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index e1eab364..98025ae3 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -315,7 +315,6 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
 ***********************************************************************/
 void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    int fHaig = 0;
     int fShowFanouts = 0;
     Aig_Obj_t * pTemp;
     if ( pObj == NULL )
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c17fae5f..ef87c5d5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -281,6 +281,7 @@ static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs
 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;                                                         } 
+static inline int          Gia_ManWithChoices( Gia_Man_t * p ) { return p->pReprs != NULL;                                                 } 
 
 static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                                          }
 static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                                         }
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 0873602d..7940c790 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1266,7 +1266,7 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
         Gia_ClassForEachObj( p, iRepr, iNode )
             nItems++;
     }
-    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
+    pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) );
     // write constant class
     iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) );
 //printf( "\nRepr = %d ", 0 );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 9ccb91fe..b9557600 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -366,7 +366,7 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
     Gia_ManForEachClass( p, iRepr )
     {
         Vec_IntPush( vCollected, iRepr );
-
+/*
         // check classes
         if ( !fNowIncreasing )
         {
@@ -384,20 +384,8 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
                 iPrev = iNode;
             }
         }
+*/
     }
-
-    iRepr = 129720;
-    printf( "Class %d : ", iRepr );
-    Gia_ClassForEachObj( p, iRepr, iNode )
-        printf( " %d", iNode );
-    printf( "\n" );
-
-    iRepr = 129737;
-    printf( "Class %d : ", iRepr );
-    Gia_ClassForEachObj( p, iRepr, iNode )
-        printf( " %d", iNode );
-    printf( "\n" );
-
     // correct each class
     vClass = Vec_IntAlloc( 100 );
     Vec_IntForEachEntry( vCollected, iRepr, i )
@@ -408,14 +396,14 @@ void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
         {
             if ( fNowIncreasing )
                 assert( iRepr < iNode );
-            else
-                assert( iRepr > iNode );
+//            else
+//                assert( iRepr > iNode );
             Vec_IntPush( vClass, iNode );
         }
-//        if ( !fNowIncreasing )
-//            Vec_IntSort( vClass, 1 );
-        if ( iRepr == 129720 || iRepr == 129737 )
-            Vec_IntPrint( vClass );
+        if ( !fNowIncreasing )
+            Vec_IntSort( vClass, 1 );
+//        if ( iRepr == 129720 || iRepr == 129737 )
+//            Vec_IntPrint( vClass );
         // reverse the class
         iPrev = 0;
         iRepr = Vec_IntEntryLast( vClass );
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 2d25b002..1e991b38 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -64,11 +64,12 @@ typedef enum {
 // the AIG node
 struct Hop_Obj_t_  // 6 words
 {
-    void *           pData;          // misc
-    union {                         
+    union { 
+        void *       pData;          // misc
+        int          iData; };       // misc
+    union { 
         Hop_Obj_t *  pNext;          // strashing table
-        int          PioNum;         // the number of PI/PO
-    };
+        int          PioNum; };      // the number of PI/PO
     Hop_Obj_t *      pFanin0;        // fanin
     Hop_Obj_t *      pFanin1;        // fanin
     unsigned int     Type    :  3;   // object type
@@ -182,8 +183,10 @@ static inline Hop_Obj_t *  Hop_ObjFanin0( Hop_Obj_t * pObj )      { return Hop_R
 static inline Hop_Obj_t *  Hop_ObjFanin1( Hop_Obj_t * pObj )      { return Hop_Regular(pObj->pFanin1);             }
 static inline Hop_Obj_t *  Hop_ObjChild0( Hop_Obj_t * pObj )      { return pObj->pFanin0;                          }
 static inline Hop_Obj_t *  Hop_ObjChild1( Hop_Obj_t * pObj )      { return pObj->pFanin1;                          }
-static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }
-static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
+static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj )  { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }
+static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj )  { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
+static inline int          Hop_ObjChild0CopyI( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Abc_LitNotCond(Hop_ObjFanin0(pObj)->iData, Hop_ObjFaninC0(pObj)) : -1;              }
+static inline int          Hop_ObjChild1CopyI( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Abc_LitNotCond(Hop_ObjFanin1(pObj)->iData, Hop_ObjFaninC1(pObj)) : -1;              }
 static inline int          Hop_ObjLevel( Hop_Obj_t * pObj )       { return pObj->nRefs;                            }
 static inline int          Hop_ObjLevelNew( Hop_Obj_t * pObj )    { return 1 + Hop_ObjIsExor(pObj) + Abc_MaxInt(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }
 static inline int          Hop_ObjPhaseCompl( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }