Performance bug fix in choice generation.

7 files changed, 51 insertions, 27 deletions

diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index c55cbedd..5334aac0 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -392,7 +392,20 @@ Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
 {
     Vec_Ptr_t * vNodes;
     Aig_Obj_t * pObj;
-    int i;
+    int i, Counter = 0;
+
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( Aig_ObjEquiv(p, pObj) == NULL )
+            continue;
+
+        Counter = 0;
+        for ( pObj = Aig_ObjEquiv(p, pObj) ; pObj; pObj = Aig_ObjEquiv(p, pObj) )
+            Counter++;
+        printf( "%d ", Counter );
+    }
+    printf( "\n" );
+
     assert( p->pEquivs != NULL );
     Aig_ManIncrementTravId( p );
     // mark constant and PIs
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 463732a4..a1df0e50 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -299,6 +299,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars )
             for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) )
                 If_ObjSetChoice( If_ManObj(pIfMan, Gia_ObjValue(pObj)), If_ManObj(pIfMan, Gia_ObjValue(pSibl)) );
             If_ManCreateChoice( pIfMan, If_ManObj(pIfMan, Gia_ObjValue(pObj)) );
+            pPars->fExpRed = 0;
         }
 //        assert( If_ObjLevel(pIfObj) == Gia_ObjLevel(pNode) );
     }
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 85555ad2..30e3ad92 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -334,6 +334,7 @@ static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj )       { return &p
 static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj )            { return pObj->pCopy;              }
 static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )             { return pObj->pNtk;               }
 static inline void *      Abc_ObjData( Abc_Obj_t * pObj )            { return pObj->pData;              }
+static inline Abc_Obj_t * Abc_ObjEquiv( Abc_Obj_t * pObj )           { return (Abc_Obj_t *)pObj->pData; }
 static inline Abc_Obj_t * Abc_ObjCopyCond( Abc_Obj_t * pObj )        { return Abc_ObjRegular(pObj)->pCopy? Abc_ObjNotCond(Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj)) : NULL;  }
 
 // setting data members of the network
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dbb75f59..83da1c60 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -864,7 +864,6 @@ Abc_Ntk_t * Abc_NtkAfterTrim( Aig_Man_t * pMan, Abc_Ntk_t * pNtkOld )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
-    Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
     Aig_Obj_t * pObj, * pTemp;
     int i;
@@ -874,32 +873,40 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
     pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     pNtkNew->nConstrs = pMan->nConstrs;
     // transfer the pointers to the basic nodes
+    Aig_ManCleanData( pMan );
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachCi( pMan, pObj, i )
         pObj->pData = Abc_NtkCi(pNtkNew, i);
-
     // rebuild the AIG
-    vNodes = Aig_ManDfsChoices( pMan );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    Aig_ManForEachNode( pMan, pObj, i )
     {
         pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
         if ( (pTemp = Aig_ObjEquiv(pMan, pObj)) )
         {
-            Abc_Obj_t * pAbcRepr, * pAbcObj;
             assert( pTemp->pData != NULL );
-            pAbcRepr = (Abc_Obj_t *)pObj->pData;
-            pAbcObj  = (Abc_Obj_t *)pTemp->pData;
-            pAbcObj->pData  = pAbcRepr->pData;
-            pAbcRepr->pData = pAbcObj;
+            ((Abc_Obj_t *)pObj->pData)->pData = ((Abc_Obj_t *)pTemp->pData);
         }
     }
-//Abc_Print( 1, "Total = %d.  Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
-    Vec_PtrFree( vNodes );
     // connect the PO nodes
     Aig_ManForEachCo( pMan, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
     if ( !Abc_NtkCheck( pNtkNew ) )
         Abc_Print( 1, "Abc_NtkFromDar(): Network check has failed.\n" );
+
+    // verify topological order
+    if ( 0 )
+    {
+        Abc_Obj_t * pNode;
+        Abc_NtkForEachNode( pNtkNew, pNode, i )
+            if ( Abc_AigNodeIsChoice( pNode ) )
+            {
+                int Counter = 0;
+                for ( pNode = Abc_ObjEquiv(pNode); pNode; pNode = Abc_ObjEquiv(pNode) )
+                    Counter++;
+                printf( "%d ", Counter );
+            }
+        printf( "\n" );
+    }
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 76171eee..315507c2 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -184,17 +184,16 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
+static inline If_Obj_t * Abc_ObjIfCopy( Abc_Obj_t * pNode ) { return (If_Obj_t *)pNode->pCopy; } 
 If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
 {
     ProgressBar * pProgress;
     If_Man_t * pIfMan;
-    Abc_Obj_t * pNode, * pFanin, * pPrev;
     Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode, * pPrev;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
-//    vNodes = Abc_NtkFindGoodOrder( pNtk );
-    vNodes = Abc_AigDfs( pNtk, 0, 0 );
 
     // start the mapping manager and set its parameters
     pIfMan = If_ManStart( pPars );
@@ -212,34 +211,37 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     {
         pNode->pCopy = (Abc_Obj_t *)If_ManCreateCi( pIfMan );
         // transfer logic level information
-        ((If_Obj_t *)pNode->pCopy)->Level = pNode->Level;
+        Abc_ObjIfCopy(pNode)->Level = pNode->Level;
     }
 
     // load the AIG into the mapper
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
-//    Abc_AigForEachAnd( pNtk, pNode, i )
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, "Initial" );
         // add the node to the mapper
         pNode->pCopy = (Abc_Obj_t *)If_ManCreateAnd( pIfMan, 
-            If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), 
-            If_NotCond( (If_Obj_t *)Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+            If_NotCond( Abc_ObjIfCopy(Abc_ObjFanin0(pNode)), Abc_ObjFaninC0(pNode) ), 
+            If_NotCond( Abc_ObjIfCopy(Abc_ObjFanin1(pNode)), Abc_ObjFaninC1(pNode) ) );
         // set up the choice node
         if ( Abc_AigNodeIsChoice( pNode ) )
         {
-            for ( pPrev = pNode, pFanin = (Abc_Obj_t *)pNode->pData; pFanin; pPrev = pFanin, pFanin = (Abc_Obj_t *)pFanin->pData )
-                If_ObjSetChoice( (If_Obj_t *)pPrev->pCopy, (If_Obj_t *)pFanin->pCopy );
-            If_ManCreateChoice( pIfMan, (If_Obj_t *)pNode->pCopy );
+            Abc_Obj_t * pEquiv;
+//            int Counter = 0;
+            assert( If_ObjId(Abc_ObjIfCopy(pNode)) > If_ObjId(Abc_ObjIfCopy(Abc_ObjEquiv(pNode))) );
+            for ( pPrev = pNode, pEquiv = Abc_ObjEquiv(pPrev); pEquiv; pPrev = pEquiv, pEquiv = Abc_ObjEquiv(pPrev) )
+                If_ObjSetChoice( Abc_ObjIfCopy(pPrev), Abc_ObjIfCopy(pEquiv) );//, Counter++;
+//            printf( "%d ", Counter );
+            If_ManCreateChoice( pIfMan, Abc_ObjIfCopy(pNode) );
         }
-//printf( "AIG node %2d -> IF node %2d\n", pNode->Id, ((If_Obj_t *)pNode->pCopy)->Id );
     }
     Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
     // set the primary outputs without copying the phase
     Abc_NtkForEachCo( pNtk, pNode, i )
-        pNode->pCopy = (Abc_Obj_t *)If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
+        pNode->pCopy = (Abc_Obj_t *)If_ManCreateCo( pIfMan, If_NotCond( Abc_ObjIfCopy(Abc_ObjFanin0(pNode)), Abc_ObjFaninC0(pNode) ) );
     return pIfMan;
 }
 
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index e75b78f5..fcfe448b 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -412,8 +412,8 @@ void Lms_ManPrintFuncStats( Lms_Man_t * p )
         if ( i == Vec_IntSize(p->vTruthPo) - 1 )
             break;
         Next = Vec_IntEntry( p->vTruthPo, i+1 );
-        Counters[Vec_StrEntry(vSupps, Entry)]++;
-        CountersS[Vec_StrEntry(vSupps, Entry)] += Next - Entry;
+        Counters[(int)Vec_StrEntry(vSupps, Entry)]++;
+        CountersS[(int)Vec_StrEntry(vSupps, Entry)] += Next - Entry;
     }
     for ( i = 0; i <= LMS_VAR_MAX; i++ )
         if ( Counters[i] )
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 2fee88c4..04ff59e4 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -335,7 +335,7 @@ static inline void *     If_ObjCopy( If_Obj_t * pObj )                       { r
 static inline int        If_ObjLevel( If_Obj_t * pObj )                      { return pObj->Level;                   }
 static inline void       If_ObjSetLevel( If_Obj_t * pObj, int Level )        { pObj->Level = Level;                  }
 static inline void       If_ObjSetCopy( If_Obj_t * pObj, void * pCopy )      { pObj->pCopy = pCopy;                  }
-static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { assert( pObj->Id > pEqu->Id ); pObj->pEquiv = pEqu;                  }
+static inline void       If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu;                  }
 
 static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj )                    { return &pObj->CutBest;                }
 static inline unsigned   If_ObjCutSign( unsigned ObjId )                     { return (1 << (ObjId % 31));           }