Integrating time manager into choice computation.

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 )

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;                    }
@@ -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;

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;

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*************************************************************

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                                ///

src/base/cmd/cmdHist.c

@@ -48,7 +48,7 @@ ABC_NAMESPACE_IMPL_START
 void Cmd_HistoryAddCommand(    Abc_Frame_t * p, const char * command )
 {
     int nLastLooked =  10;  // do not add history if the same entry appears among the last entries
-    int nLastSaved  = 100;  // when saving a file, save no more than this number of last entries
+    int nLastSaved  = 500;  // when saving a file, save no more than this number of last entries
 
     char Buffer[ABC_MAX_STR];
     int Len = strlen(command);
@@ -57,9 +57,11 @@ void Cmd_HistoryAddCommand(    Abc_Frame_t * p, const char * command )
         Buffer[Len-1] = 0;
     if ( strlen(Buffer) > 3 &&
          strncmp(Buffer,"set",3) && 
+         strncmp(Buffer,"time",4) && 
          strncmp(Buffer,"quit",4) && 
          strncmp(Buffer,"source",6) && 
-         strncmp(Buffer,"history",7) && strncmp(Buffer,"hi ", 3) && strcmp(Buffer,"hi") )
+         strncmp(Buffer,"history",7) && strncmp(Buffer,"hi ", 3) && strcmp(Buffer,"hi") &&
+         Buffer[strlen(Buffer)-1] != '?' )
     {
         char * pStr = NULL;
         int i, Start = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory) - nLastLooked );

src/misc/tim/timBox.c

@@ -189,10 +189,14 @@ int Tim_ManBoxOutputNum( Tim_Man_t * p, int iBox )
 ***********************************************************************/
 float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox )
 {
+    float * pTable;
     Tim_Box_t * pBox = (Tim_Box_t *)Vec_PtrEntry( p->vBoxes, iBox );
     if ( pBox->iDelayTable < 0 )
         return NULL;
-    return (float *)Vec_PtrEntry( p->vDelayTables, pBox->iDelayTable );
+    pTable = (float *)Vec_PtrEntry( p->vDelayTables, pBox->iDelayTable );
+    assert( (int)pTable[1] == pBox->nInputs );
+    assert( (int)pTable[2] == pBox->nOutputs );
+    return pTable;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/misc/tim/timDump.c

@@ -63,6 +63,7 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
     // save number of boxes
     Vec_StrPutI_ne( vStr, Tim_ManBoxNum(p) );
     // for each box, save num_inputs, num_outputs, and delay table ID
+    if ( Tim_ManBoxNum(p) > 0 )
     Tim_ManForEachBox( p, pBox, i )
     {
         Vec_StrPutI_ne( vStr, Tim_ManBoxInputNum(p, pBox->iBox) );
@@ -72,7 +73,8 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
     // save the number of delay tables
     Vec_StrPutI_ne( vStr, Tim_ManDelayTableNum(p) );
     // save the delay tables
-    Vec_PtrForEachEntry( float *, p->vDelayTables, pDelayTable, i )
+    if ( Tim_ManDelayTableNum(p) > 0 )
+    Tim_ManForEachTable( p, pDelayTable, i )
     {
         assert( (int)pDelayTable[0] == i );
         // save table ID and dimensions (inputs x outputs)
@@ -126,6 +128,7 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
     // start boxes
     nBoxes = Vec_StrGetI_ne( p, &iStr );
     assert( pMan->vBoxes == NULL );
+    if ( nBoxes > 0 )
         pMan->vBoxes = Vec_PtrAlloc( nBoxes );
     // create boxes
     curPi = nPis;
@@ -145,9 +148,9 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
     // create delay tables
     nTables = Vec_StrGetI_ne( p, &iStr );
     assert( pMan->vDelayTables == NULL );
+    if ( nTables > 0 )
         pMan->vDelayTables = Vec_PtrAlloc( nTables );
     // read delay tables
-    assert( Vec_PtrSize(pMan->vDelayTables) == 0 );
     for ( i = 0; i < nTables; i++ )
     {
         // read table ID and dimensions
@@ -167,7 +170,7 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
         assert( Vec_PtrSize(pMan->vDelayTables) == TableId );
         Vec_PtrPush( pMan->vDelayTables, pDelayTable );
     }
-    assert( Vec_PtrSize(pMan->vDelayTables) == nTables );
+    assert( Tim_ManDelayTableNum(pMan) == nTables );
 //    Tim_ManPrint( pMan );
     return pMan;
 }

src/misc/tim/timInt.h

@@ -128,6 +128,9 @@ static inline Tim_Obj_t * Tim_ManBoxOutput( Tim_Man_t * p, Tim_Box_t * pBox, int
 #define Tim_ManBoxForEachOutput( p, pBox, pObj, i )                     \
     for ( i = 0; (i < (pBox)->nOutputs) && ((pObj) = Tim_ManBoxOutput(p, pBox, i)); i++ )
 
+#define Tim_ManForEachTable( p, pTable, i )                             \
+    Vec_PtrForEachEntry( float *, p->vDelayTables, pTable, i )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     SEQUENTIAL ITERATORS                         ///
 ////////////////////////////////////////////////////////////////////////

src/misc/tim/timMan.c

@@ -112,8 +112,10 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
         Tim_ManInitPoRequiredAll( p, (float)TIM_ETERNITY );
     }
     // duplicate delay tables
+    if ( Tim_ManDelayTableNum(p) > 0 )
+    {
         pNew->vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vDelayTables) );
-    Vec_PtrForEachEntry( float *, p->vDelayTables, pDelayTable, i )
+        Tim_ManForEachTable( p, pDelayTable, i )
         {
             assert( i == (int)pDelayTable[0] );
             nInputs   = (int)pDelayTable[1];
@@ -127,10 +129,15 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
             assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
             Vec_PtrPush( pNew->vDelayTables, pDelayTableNew );
         }
+    }
     // duplicate boxes
+    if ( Tim_ManBoxNum(p) > 0 )
+    {
+        pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
         Tim_ManForEachBox( p, pBox, i )
            Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs, 
                 pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable );
+    }
     return pNew;
 }
 
@@ -147,15 +154,8 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
 ***********************************************************************/
 void Tim_ManStop( Tim_Man_t * p )
 {
-    float * pTable;
-    int i;
-    if ( p->vDelayTables )
-    {
-        Vec_PtrForEachEntry( float *, p->vDelayTables, pTable, i )
-            ABC_FREE( pTable );
-        Vec_PtrFree( p->vDelayTables );
-    }
-    Vec_PtrFree( p->vBoxes );
+    Vec_PtrFreeFree( p->vDelayTables );
+    Vec_PtrFreeP( &p->vBoxes );
     Mem_FlexStop( p->pMemObj, 0 );
     ABC_FREE( p->pCis );
     ABC_FREE( p->pCos );
@@ -185,7 +185,7 @@ void Tim_ManPrint( Tim_Man_t * p )
     Tim_Box_t * pBox;
     Tim_Obj_t * pObj, * pPrev;
     float * pTable;
-    int i, k;
+    int i, j, k, TableX, TableY;
     printf( "TIMING INFORMATION:\n" );
 
     // print CI info
@@ -211,40 +211,48 @@ void Tim_ManPrint( Tim_Man_t * p )
             printf( "PO%5d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
 
     // print box info
+    if ( Tim_ManBoxNum(p) > 0 )
     Tim_ManForEachBox( p, pBox, i )
     {
-        printf( "*** Box %3d :  Ins = %d. Outs = %d.\n", i, pBox->nInputs, pBox->nOutputs );
-        printf( "Delay table:\n" );
-        pTable = Tim_ManBoxDelayTable( p, pBox->iBox );
-        for ( i = 0; i < pBox->nOutputs; i++, printf( "\n" ) )
-            for ( k = 0; k < pBox->nInputs; k++ )
-                if ( pTable[3+i*pBox->nInputs+k] == -ABC_INFINITY )
-                    printf( "%5s", "-" );
-                else
-                    printf( "%5.0f", pTable[3+i*pBox->nInputs+k] );
-        printf( "\n" );
+        printf( "*** Box %5d :  Ins = %4d. Outs = %4d. DelayTable = %4d\n", i, pBox->nInputs, pBox->nOutputs, pBox->iDelayTable );
 
         // print box inputs
         pPrev = Tim_ManBoxInput( p, pBox, 0 );
-        Tim_ManBoxForEachInput( p, pBox, pObj, i )
+        Tim_ManBoxForEachInput( p, pBox, pObj, k )
             if ( pPrev->timeArr != pObj->timeArr || pPrev->timeReq != pObj->timeReq )
                 break;
-        if ( i == Tim_ManBoxInputNum(p, pBox->iBox) )
+        if ( k == Tim_ManBoxInputNum(p, pBox->iBox) )
             printf( "Box inputs  :  arr = %5.3f  req = %5.3f\n", pPrev->timeArr, pPrev->timeReq );
         else
-            Tim_ManBoxForEachInput( p, pBox, pObj, i )
-                printf( "box-inp%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+            Tim_ManBoxForEachInput( p, pBox, pObj, k )
+                printf( "box-in%4d :  arr = %5.3f  req = %5.3f\n", k, pObj->timeArr, pObj->timeReq );
 
         // print box outputs
         pPrev = Tim_ManBoxOutput( p, pBox, 0 );
-        Tim_ManBoxForEachOutput( p, pBox, pObj, i )
+        Tim_ManBoxForEachOutput( p, pBox, pObj, k )
             if ( pPrev->timeArr != pObj->timeArr || pPrev->timeReq != pObj->timeReq )
                 break;
-        if ( i == Tim_ManBoxOutputNum(p, pBox->iBox) )
+        if ( k == Tim_ManBoxOutputNum(p, pBox->iBox) )
             printf( "Box outputs :  arr = %5.3f  req = %5.3f\n", pPrev->timeArr, pPrev->timeReq );
         else
-            Tim_ManBoxForEachOutput( p, pBox, pObj, i )
-                printf( "box-out%3d :  arr = %5.3f  req = %5.3f\n", i, pObj->timeArr, pObj->timeReq );
+            Tim_ManBoxForEachOutput( p, pBox, pObj, k )
+                printf( "box-out%3d :  arr = %5.3f  req = %5.3f\n", k, pObj->timeArr, pObj->timeReq );
+    }
+
+    // print delay tables
+    if ( Tim_ManDelayTableNum(p) > 0 )
+    Tim_ManForEachTable( p, pTable, i )
+    {
+        printf( "Delay table %d:\n", i );
+        assert( i == (int)pTable[0] );
+        TableX = (int)pTable[1];
+        TableY = (int)pTable[2];
+        for ( j = 0; j < TableY; j++, printf( "\n" ) )
+            for ( k = 0; k < TableX; k++ )
+                if ( pTable[3+j*TableX+k] == -ABC_INFINITY )
+                    printf( "%5s", "-" );
+                else
+                    printf( "%5.0f", pTable[3+j*TableX+k] );
     }
     printf( "\n" );
 }
@@ -270,20 +278,25 @@ int Tim_ManCoNum( Tim_Man_t * p )
 }
 int Tim_ManPiNum( Tim_Man_t * p )
 {
+    if ( Tim_ManBoxNum(p) == 0 )
+        return Tim_ManCiNum(p);
     return Tim_ManBoxOutputFirst(p, 0);
 }
 int Tim_ManPoNum( Tim_Man_t * p )
 {
-    int iLastBoxId = Tim_ManBoxNum(p) - 1;
+    int iLastBoxId;
+    if ( Tim_ManBoxNum(p) == 0 )
+        return Tim_ManCoNum(p);
+    iLastBoxId = Tim_ManBoxNum(p) - 1;
     return Tim_ManCoNum(p) - (Tim_ManBoxInputFirst(p, iLastBoxId) + Tim_ManBoxInputNum(p, iLastBoxId));
 }
 int Tim_ManBoxNum( Tim_Man_t * p )
 {
-    return Vec_PtrSize(p->vBoxes);
+    return p->vBoxes ? Vec_PtrSize(p->vBoxes) : 0;
 }
 int Tim_ManDelayTableNum( Tim_Man_t * p )
 {
-    return Vec_PtrSize(p->vDelayTables);
+    return p->vDelayTables ? Vec_PtrSize(p->vDelayTables) : 0;
 }
 
 /**Function*************************************************************

src/proof/dch/dchChoice.c

@@ -103,68 +103,6 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    // check the trivial cases
-    if ( pObj == NULL )
-        return 0;
-    if ( Aig_ObjIsCi(pObj) )
-        return 0;
-    if ( pObj->fMarkA )
-        return 1;
-    // skip the visited node
-    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
-        return 0;
-    Aig_ObjSetTravIdCurrent( p, pObj );
-    // check the children
-    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
-        return 1;
-    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
-        return 1;
-    // check equivalent nodes
-    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
-{
-    Aig_Obj_t * pTemp;
-    int RetValue;
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_IsComplement(pRepr) );
-    // mark nodes of the choice node
-    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
-        pTemp->fMarkA = 1;
-    // traverse the new node
-    Aig_ManIncrementTravId( p );
-    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
-    // unmark nodes of the choice node
-    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
-        pTemp->fMarkA = 0;
-    return RetValue;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Returns representatives of fanin in approapriate polarity.]
 
   Description []
@@ -190,146 +128,6 @@ static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the TFI of the node.]
-
-  Description [Returns 1 if there is a CI not marked with previous ID.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int RetValue;
-    if ( pObj == NULL )
-        return 0;
-    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
-        return 0;
-    if ( Aig_ObjIsCi(pObj) )
-    {
-        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
-        Aig_ObjSetTravIdCurrent( p, pObj );
-        return RetValue;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    Aig_ObjSetTravIdCurrent( p, pObj );
-    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
-    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
-//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
-    return (RetValue > 0);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the AIG with choices from representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
-{
-    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
-    // get the new node
-    pObj->pData = Aig_And( pAigNew, 
-        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
-        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
-    pRepr = Aig_ObjRepr( pAigOld, pObj );
-    if ( pRepr == NULL )
-        return;
-    // get the corresponding new nodes
-    pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
-    pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
-    if ( pObjNew == pReprNew )
-        return;
-    // skip the earlier nodes
-    if ( pReprNew->Id > pObjNew->Id )
-        return;
-    assert( pReprNew->Id < pObjNew->Id );
-    // set the representatives
-    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
-    // skip used nodes
-    if ( pObjNew->nRefs > 0 )
-        return;
-    assert( pObjNew->nRefs == 0 );
-    // update new nodes of the object
-    if ( !Aig_ObjIsNode(pRepr) )
-        return;
-    // skip choices with combinational loops
-    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
-        return;
-    // don't add choice if structural support of pObjNew and pReprNew differ
-    if ( fSkipRedSupps )
-    {
-        int fSkipChoice = 0;
-        // mark support of the representative node (pReprNew)
-        Aig_ManIncrementTravId( pAigNew );
-        Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
-        // detect if the new node (pObjNew) depends on any additional variables
-        Aig_ManIncrementTravId( pAigNew );
-        if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
-            fSkipChoice = 1;//, printf( "1" );
-        // detect if the representative node (pReprNew) depends on any additional variables
-        Aig_ManIncrementTravId( pAigNew );
-        if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
-            fSkipChoice = 1;//, printf( "2" );
-        // skip the choice if this is what is happening
-        if ( fSkipChoice )
-            return;
-    }
-    // add choice
-    pAigNew->pEquivs[pObjNew->Id]  = pAigNew->pEquivs[pReprNew->Id];
-    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the AIG with choices from representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
-{
-    Aig_Man_t * pChoices, * pTemp;
-    Aig_Obj_t * pObj;
-    int i;
-    // start recording equivalences
-    pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
-    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
-    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
-    // map constants and PIs
-    Aig_ManCleanData( pAig );
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
-    Aig_ManForEachCi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreateCi( pChoices );
-    // construct choices for the internal nodes
-    assert( pAig->pReprs != NULL );
-    Aig_ManForEachNode( pAig, pObj, i )
-        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, 0 );
-    Aig_ManForEachCo( pAig, pObj, i )
-        Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
-    Dch_DeriveChoiceCountEquivs( pChoices );
-    // there is no need for cleanup
-    ABC_FREE( pChoices->pReprs );
-    pChoices = Aig_ManDupDfs( pTemp = pChoices );
-    Aig_ManStop( pTemp );
-    return pChoices;
-}
-
-
-
-
-/**Function*************************************************************
-
   Synopsis    [Checks for combinational loops in the AIG.]
 
   Description [Returns 1 if combinational loop is detected.]
@@ -413,18 +211,6 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
     Aig_ObjSetTravIdPrevious( p, pNode );
     return 1;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Checks for combinational loops in the AIG.]
-
-  Description [Returns 1 if there is no combinational loops.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
 {
     Aig_Obj_t * pNode;
@@ -487,6 +273,124 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Verify correctness of choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_CheckChoices( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, fProb = 0;
+    Aig_ManCleanMarkA( p );
+    Aig_ManForEachNode( p, pObj, i )
+        if ( p->pEquivs[i] != NULL )
+        {
+            if ( pObj->fMarkA == 1 )
+                printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
+            pObj->fMarkA = 1;
+            // consider the last one
+            pObj = p->pEquivs[i];
+            if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
+            {
+                if ( pObj->fMarkA == 1 )
+                    printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
+                pObj->fMarkA = 1;
+            }
+        }
+    Aig_ManCleanMarkA( p );
+    if ( !fProb )
+        printf( "Verification of choice AIG succeeded.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI of the node.]
+
+  Description [Returns 1 if there is a CI not marked with previous ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int RetValue;
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    if ( Aig_ObjIsCi(pObj) )
+    {
+        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
+        Aig_ObjSetTravIdCurrent( p, pObj );
+        return RetValue;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
+    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
+//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+    return (RetValue > 0);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the choice node of pRepr is in the TFI of pObj.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    // check the trivial cases
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsCi(pObj) )
+        return 0;
+    if ( pObj->fMarkA )
+        return 1;
+    // skip the visited node
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    // check the children
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin0(pObj) ) )
+        return 1;
+    if ( Dch_ObjCheckTfi_rec( p, Aig_ObjFanin1(pObj) ) )
+        return 1;
+    // check equivalent nodes
+    return Dch_ObjCheckTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+}
+int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pTemp;
+    int RetValue;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pRepr) );
+    // mark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 1;
+    // traverse the new node
+    Aig_ManIncrementTravId( p );
+    RetValue = Dch_ObjCheckTfi_rec( p, pObj );
+    // unmark nodes of the choice node
+    for ( pTemp = pRepr; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
+        pTemp->fMarkA = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Derives the AIG with choices from representatives.]
 
   Description []
@@ -496,11 +400,71 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
+{
+    Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    // get the new node
+    assert( pObj->pData == NULL );
+    pObj->pData = Aig_And( pAigNew, 
+        Aig_ObjChild0CopyRepr(pAigNew, pObj), 
+        Aig_ObjChild1CopyRepr(pAigNew, pObj) );
+    pRepr = Aig_ObjRepr( pAigOld, pObj );
+    if ( pRepr == NULL )
+        return;
+    assert( pRepr->Id < pObj->Id );
+    // get the corresponding new nodes
+    pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
+    pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
+    if ( pObjNew == pReprNew )
+        return;
+    // skip the earlier nodes
+    if ( pReprNew->Id > pObjNew->Id )
+        return;
+    assert( pReprNew->Id < pObjNew->Id );
+    // set the representatives
+    Aig_ObjSetRepr( pAigNew, pObjNew, pReprNew );
+    // skip used nodes
+    if ( pObjNew->nRefs > 0 )
+        return;
+    assert( pObjNew->nRefs == 0 );
+    // update new nodes of the object
+    if ( !Aig_ObjIsNode(pRepr) )
+        return;
+    // skip choices with combinational loops
+    if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
+        return;
+    // don't add choice if structural support of pObjNew and pReprNew differ
+    if ( fSkipRedSupps )
+    {
+        int fSkipChoice = 0;
+        // mark support of the representative node (pReprNew)
+        Aig_ManIncrementTravId( pAigNew );
+        Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
+        // detect if the new node (pObjNew) depends on any additional variables
+        Aig_ManIncrementTravId( pAigNew );
+        if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
+            fSkipChoice = 1;//, printf( "1" );
+        // detect if the representative node (pReprNew) depends on any additional variables
+        Aig_ManIncrementTravId( pAigNew );
+        if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
+            fSkipChoice = 1;//, printf( "2" );
+        // skip the choice if this is what is happening
+        if ( fSkipChoice )
+            return;
+    }
+    // add choice
+    pAigNew->pEquivs[pObjNew->Id]  = pAigNew->pEquivs[pReprNew->Id];
+    pAigNew->pEquivs[pReprNew->Id] = pObjNew;
+}
 Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
 {
     Aig_Man_t * pChoices;
     Aig_Obj_t * pObj;
     int i;
+    // make sure reprsentative nodes do not have representatives
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( pAig->pReprs[i] != NULL && pAig->pReprs[pAig->pReprs[i]->Id] != NULL )
+            printf( "Node %d: repr %d has repr %d.\n", i, Aig_ObjId(pAig->pReprs[i]), Aig_ObjId(pAig->pReprs[pAig->pReprs[i]->Id]) );
     // start recording equivalences
     pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
@@ -518,6 +482,7 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
         Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
     Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
+//Dch_CheckChoices( pChoices );
     return pChoices;
 }