Integrating time manager into choice computation.

5 files changed, 212 insertions, 64 deletions

diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index b4c61d15..9d87db92 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -582,6 +582,7 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     if ( pEquivNew )
     {
+        assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
         if ( pNew->pEquivs )
             pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pEquivNew);        
         if ( pNew->pReprs )
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2980cb4a..c17fae5f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -570,6 +570,7 @@ static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
 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 )   { assert( Num == GIA_VOID || Num < Id ); p->pReprs[Id].iRepr = Num;          }
+static inline void        Gia_ObjSetReprRev( Gia_Man_t * p, int Id, int Num ){ assert( Num == GIA_VOID || Num > Id ); 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_ObjHasRepr( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr != GIA_VOID;                                    }
 static inline int         Gia_ObjReprSelf( Gia_Man_t * p, int Id )           { return Gia_ObjHasRepr(p, Id) ? Gia_ObjRepr(p, Id) : Id;                    }
@@ -590,8 +591,8 @@ static inline int         Gia_ObjDiffColors( Gia_Man_t * p, int i, int j )   { r
 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;                }
+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;                                              }
 
 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;  }
@@ -758,6 +759,7 @@ extern int                 Gia_ManEquivCountLitsAll( 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 void                Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
 extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
 extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
@@ -914,9 +916,11 @@ extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern void                Gia_ManPrint( Gia_Man_t * p );
 extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
 extern void                Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern unsigned *          Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern int                 Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 );
 
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index a1d9dd97..d598b511 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -926,7 +926,8 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
     Tim_Man_t * pTime = p->pManTime;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
-    int i, k, curCi, curCo, curNo, nodeId;
+    int i, k, curCi, curCo, curNo, nodeLim;
+//Gia_ManPrint( p );
     assert( pTime != NULL );
     assert( Gia_ManIsNormalized(p) );
     Gia_ManFillValue( p );
@@ -939,24 +940,24 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
         Gia_ManPi(p, k)->Value = Gia_ManAppendCi(pNew);
     curCi = Tim_ManPiNum(pTime);
     curCo = 0;
-    curNo = Gia_ManPiNum(p);
+    curNo = Gia_ManPiNum(p)+1;
     for ( i = 0; i < Tim_ManBoxNum(pTime); i++ )
     {
         // find the latest node feeding into inputs of this box
-        nodeId = -1;
+        nodeLim = -1;
         for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
         {
             pObj = Gia_ManPo( p, curCo + k );
-            nodeId = Abc_MaxInt( nodeId, Gia_ObjFaninId0p(p, pObj) );
+            nodeLim = Abc_MaxInt( nodeLim, Gia_ObjFaninId0p(p, pObj)+1 );
         }
         // copy nodes up to the given node
-        for ( k = curNo; k <= nodeId; k++ )
+        for ( k = curNo; k < nodeLim; k++ )
         {
             pObj = Gia_ManObj( p, k );
             assert( Gia_ObjIsAnd(pObj) );
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         }
-        curNo = Abc_MaxInt( curNo, nodeId + 1 );
+        curNo = Abc_MaxInt( curNo, nodeLim );
         // copy COs
         for ( k = 0; k < Tim_ManBoxInputNum(pTime, i); k++ )
         {
@@ -972,6 +973,16 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
         }
         curCi += Tim_ManBoxOutputNum(pTime, i);
     }
+    // copy remaining nodes
+    nodeLim = Gia_ManObjNum(p) - Gia_ManPoNum(p);
+    for ( k = curNo; k < nodeLim; k++ )
+    {
+        pObj = Gia_ManObj( p, k );
+        assert( Gia_ObjIsAnd(pObj) );
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
+    curNo = Abc_MaxInt( curNo, nodeLim );
+    curNo += Gia_ManPoNum(p);
     // copy primary outputs
     for ( k = 0; k < Tim_ManPoNum(pTime); k++ )
     {
@@ -981,9 +992,10 @@ Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
     curCo += Tim_ManPoNum(pTime);
     assert( curCi == Gia_ManPiNum(p) );
     assert( curCo == Gia_ManPoNum(p) );
-    assert( curNo == Gia_ManAndNum(p) );
+    assert( curNo == Gia_ManObjNum(p) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     Gia_ManDupRemapEquiv( pNew, p );
+//Gia_ManPrint( pNew );
     // pass the timing manager
     pNew->pManTime = pTime;  p->pManTime = NULL;
     return pNew;
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 62afe26c..9ccb91fe 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -156,52 +156,6 @@ void Gia_ManDeriveReprs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
-{
-    int Ent, nLits = 1;
-    Gia_ClassForEachObj1( p, i, Ent )
-    {
-        assert( Gia_ObjRepr(p, Ent) == i );
-        nLits++;
-    }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
-{
-    int Ent;
-    printf( "Class %4d :  Num = %2d  {", Counter, Gia_ManEquivCountOne(p, i) );
-    Gia_ClassForEachObj( p, i, Ent )
-    {
-        printf(" %d", Ent );
-        if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
-            printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
-    }
-    printf( " }\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
 {
     int i, nLits = 0;
@@ -324,6 +278,28 @@ int Gia_ManEquivCountLits( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManEquivCountOne( Gia_Man_t * p, int i )
+{
+    int Ent, nLits = 1;
+    Gia_ClassForEachObj1( p, i, Ent )
+    {
+        assert( Gia_ObjRepr(p, Ent) == i );
+        nLits++;
+    }
+    return nLits;
+}
+void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter )
+{
+    int Ent;
+    printf( "Class %4d :  Num = %2d  {", Counter, Gia_ManEquivCountOne(p, i) );
+    Gia_ClassForEachObj( p, i, Ent )
+    {
+        printf(" %d", Ent );
+        if ( p->pReprs[Ent].fColorA || p->pReprs[Ent].fColorB )
+            printf(" <%d%d>", p->pReprs[Ent].fColorA, p->pReprs[Ent].fColorB );
+    }
+    printf( " }\n" );
+}
 void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
 {
     int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
@@ -342,13 +318,10 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
     printf( "cst =%8d  cls =%7d  lit =%8d  unused =%8d  proof =%6d  mem =%5.2f MB\n", 
         Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
-//    printf( "cst =%8d  cls =%7d  lit =%8d\n", 
-//        Counter0, Counter, nLits );
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
-        int Ent;
-
+//        int Ent;
         printf( "Const0 = " );
         Gia_ManForEachConst( p, i )
             printf( "%d ", i );
@@ -356,7 +329,7 @@ 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 )
@@ -368,7 +341,103 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
                 }
                 printf( "\n" );
             }
+*/
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reverse the order of nodes in equiv classes.]
+
+  Description [If the flag is 1, assumed current increasing order ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
+{
+    Vec_Int_t * vCollected;
+    Vec_Int_t * vClass;
+    int i, k, iRepr, iNode, iPrev;
+    // collect classes
+    vCollected = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, iRepr )
+    {
+        Vec_IntPush( vCollected, iRepr );
+
+        // check classes
+        if ( !fNowIncreasing )
+        {
+            iPrev = iRepr;
+            Gia_ClassForEachObj1( p, iRepr, iNode )
+            {
+                if ( iPrev < iNode )
+                {
+                    printf( "Class %d : ", iRepr );
+                    Gia_ClassForEachObj( p, iRepr, iNode )
+                        printf( " %d", iNode );
+                    printf( "\n" );
+                    break;
+                }
+                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 )
+    {
+        Vec_IntClear( vClass );
+        Vec_IntPush( vClass, iRepr );
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+        {
+            if ( fNowIncreasing )
+                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 );
+        // reverse the class
+        iPrev = 0;
+        iRepr = Vec_IntEntryLast( vClass );
+        Vec_IntForEachEntry( vClass, iNode, k )
+        {
+            if ( fNowIncreasing )
+                Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
+            else
+                Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
+            Gia_ObjSetNext( p, iNode, iPrev );
+            iPrev = iNode;
+        }
     }
+    Vec_IntFree( vCollected );
+    Vec_IntFree( vClass );
+    // verify
+    Gia_ManForEachClass( p, iRepr )
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+            if ( fNowIncreasing )
+                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
+            else
+                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 43ef3e08..499f9293 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -993,8 +993,22 @@ int Gia_ManHasChoices( Gia_Man_t * p )
 void Gia_ManVerifyChoices( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
-    int i, fProb = 0;
+    int i, iRepr, iNode, fProb = 0;
     assert( p->pReprs );
+
+    // mark nodes 
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachClass( p, iRepr )
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+        {
+            if ( Gia_ObjIsHead(p, iNode) )
+                printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
+            if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
+                printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
+            Gia_ManObj( p, iNode )->fMark0 = 1;
+        }
+    Gia_ManCleanMark0(p);
+
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( Gia_ObjIsAnd(pObj) )
@@ -1010,8 +1024,8 @@ void Gia_ManVerifyChoices( Gia_Man_t * p )
                 printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
         }
     }
-//    if ( !fProb )
-//        printf( "GIA with choices is correct.\n" );
+    if ( !fProb )
+        printf( "GIA with choices is correct.\n" );
 }
 
 /**Function*************************************************************
@@ -1135,7 +1149,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
         pObj = Gia_Not(pObj);
     }
     assert( !Gia_IsComplement(pObj) );
-    printf( "Node %4d : ", Gia_ObjId(p, pObj) );
+    printf( "Obj %4d : ", Gia_ObjId(p, pObj) );
     if ( Gia_ObjIsConst0(pObj) )
         printf( "constant 0" );
     else if ( Gia_ObjIsPi(p, pObj) )
@@ -1180,6 +1194,13 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
     }
 */
 }
+void Gia_ManPrint( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        Gia_ObjPrint( p, pObj );
+}
 
 /**Function*************************************************************
 
@@ -1419,6 +1440,47 @@ void Gia_ObjComputeTruthTableTest( Gia_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the manager are structural identical.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManCompare( Gia_Man_t * p1, Gia_Man_t * p2 )
+{
+    Gia_Obj_t * pObj1, * pObj2;
+    int i;
+    if ( Gia_ManObjNum(p1) != Gia_ManObjNum(p2) )
+    {
+        printf( "AIGs have different number of objects.\n" );
+        return 0;
+    }
+    Gia_ManCleanValue( p1 );
+    Gia_ManCleanValue( p2 );
+    Gia_ManForEachObj( p1, pObj1, i )
+    {
+        pObj2 = Gia_ManObj( p2, i );
+        if ( memcmp( pObj1, pObj2, sizeof(Gia_Obj_t) ) )
+        {
+            printf( "Objects %d are different.\n", i );
+            return 0;
+        }
+        if ( p1->pReprs && p2->pReprs )
+        {
+            if ( memcmp( &p1->pReprs[i], &p2->pReprs[i], sizeof(Gia_Rpr_t) ) )
+            {
+                printf( "Representatives of objects %d are different.\n", i );
+                return 0;
+            }
+        }
+    }
+    return 1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///