Version abc90804

committer: Baruch Sterin <baruchs@gmail.com>

3 files changed, 27 insertions, 8 deletions

diff --git a/src/map/amap/amapGraph.c b/src/map/amap/amapGraph.c
index 0e9fd85c..6f269301 100644
--- a/src/map/amap/amapGraph.c
+++ b/src/map/amap/amapGraph.c
@@ -115,6 +115,7 @@ Amap_Obj_t * Amap_ManCreatePo( Amap_Man_t * p, Amap_Obj_t * pFan0 )
     pObj->Level  = Amap_Regular(pFan0)->Level;
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    assert( p->nLevelMax < 4094 ); // 2^12-2
     p->nObjs[AMAP_OBJ_PO]++;
     return pObj;
 }
@@ -142,6 +143,7 @@ Amap_Obj_t * Amap_ManCreateAnd( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
     pObj->Level  = 1 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    assert( p->nLevelMax < 4094 ); // 2^12-2
     p->nObjs[AMAP_OBJ_AND]++;
     return pObj;
 }
@@ -168,6 +170,7 @@ Amap_Obj_t * Amap_ManCreateXor( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
     pObj->Level  = 2 + ABC_MAX( Amap_Regular(pFan0)->Level, Amap_Regular(pFan1)->Level );
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    assert( p->nLevelMax < 4094 ); // 2^12-2
     p->nObjs[AMAP_OBJ_XOR]++;
     return pObj;
 }
@@ -197,6 +200,7 @@ Amap_Obj_t * Amap_ManCreateMux( Amap_Man_t * p, Amap_Obj_t * pFan0, Amap_Obj_t *
     pObj->Level  = 2 + ABC_MAX( pObj->Level, Amap_Regular(pFanC)->Level );
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    assert( p->nLevelMax < 4094 ); // 2^12-2
     p->nObjs[AMAP_OBJ_MUX]++;
     return pObj;
 }
@@ -227,6 +231,7 @@ void Amap_ManCreateChoice( Amap_Man_t * p, Amap_Obj_t * pObj )
     // mark the largest level
     if ( p->nLevelMax < (int)pObj->Level )
         p->nLevelMax = (int)pObj->Level;
+    assert( p->nLevelMax < 4094 ); // 2^12-2
 }
 
 /**Function*************************************************************
diff --git a/src/map/amap/amapInt.h b/src/map/amap/amapInt.h
index dec7e799..d6d5d68b 100644
--- a/src/map/amap/amapInt.h
+++ b/src/map/amap/amapInt.h
@@ -200,8 +200,8 @@ struct Amap_Obj_t_
     unsigned           fPhase   :  1;
     unsigned           fRepr    :  1;
     unsigned           fPolar   :  1;  // pCutBest->fInv ^ pSetBest->fInv
-    unsigned           Level    : 20;
-    unsigned           nCuts    : 12;
+    unsigned           Level    : 12;  // 20  (July 16, 2009)
+    unsigned           nCuts    : 20;  // 12  (July 16, 2009)
     int                nRefs;
     int                Equiv;
     int                Fan[3];
diff --git a/src/map/amap/amapMerge.c b/src/map/amap/amapMerge.c
index 1a6e3804..23d8384b 100644
--- a/src/map/amap/amapMerge.c
+++ b/src/map/amap/amapMerge.c
@@ -170,9 +170,10 @@ Amap_Cut_t * Amap_ManCutCreate3( Amap_Man_t * p,
 ***********************************************************************/
 void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
 {
+    int nMaxCuts = 500;
     int * pBuffer;
     Amap_Cut_t * pNext, * pCut;
-    int i, nWords, Entry, nCuts;
+    int i, nWords, Entry, nCuts, nCuts2;
     assert( pNode->pData == NULL );
     // count memory needed
     nCuts = 1;
@@ -182,7 +183,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
         for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
         {
             nCuts++;
-            nWords += pCut->nFans + 1;
+            if ( nCuts < nMaxCuts )
+                nWords += pCut->nFans + 1;
         }
     }
     p->nBytesUsed += 4*nWords;
@@ -194,17 +196,23 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
     pNext->fInv  = 0;
     pNext->nFans = 1;
     pNext->Fans[0] = Amap_Var2Lit(pNode->Id, 0);
-    pNext = (Amap_Cut_t *)(pBuffer + 2);
+    pNext  = (Amap_Cut_t *)(pBuffer + 2);
     // add other cuts
+    nCuts2 = 1;
     Vec_IntForEachEntry( p->vTemp, Entry, i )
     {
         for ( pCut = p->ppCutsTemp[Entry]; pCut; pCut = *Amap_ManCutNextP(pCut) )
         {
-            memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) );
-            pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1);
+            nCuts2++;
+            if ( nCuts2 < nMaxCuts )
+            {
+                memcpy( pNext, pCut, sizeof(int) * (pCut->nFans + 1) );
+                pNext = (Amap_Cut_t *)((int *)pNext + pCut->nFans + 1);
+            }
         }
         p->ppCutsTemp[Entry] = NULL;
     }
+    assert( nCuts == nCuts2 );
     assert( (int *)pNext - pBuffer == nWords );
     // restore the storage
     Vec_IntClear( p->vTemp );
@@ -213,7 +221,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
         if ( p->ppCutsTemp[i] != NULL )
             printf( "Amap_ManCutSaveStored(): Error!\n" );
     pNode->pData = (Amap_Cut_t *)pBuffer;
-    pNode->nCuts = nCuts;
+    pNode->nCuts = ABC_MIN( nCuts, nMaxCuts-1 );
+    assert( nCuts < (1<<20) );
 //    printf("%d ", nCuts );
     // verify cuts
     pCut = NULL;
@@ -221,6 +230,8 @@ void Amap_ManCutSaveStored( Amap_Man_t * p, Amap_Obj_t * pNode )
 //        for ( i = 0, pNext = (Amap_Cut_t *)pNode->pData; i < (int)pNode->nCuts; 
 //        i++, pNext = Amap_ManCutNext(pNext) )
     {
+        if ( i == nMaxCuts )
+            break;
         assert( pCut == NULL || pCut->iMat <= pNext->iMat );
         pCut = pNext;
     }
@@ -311,8 +322,11 @@ void Amap_ManMergeNodeChoice( Amap_Man_t * p, Amap_Obj_t * pNode )
     for ( pTemp = pNode; pTemp; pTemp = Amap_ObjChoice(p, pTemp) )
     {
         Amap_NodeForEachCut( pTemp, pCut, c )
+        {
+            if (!pCut) break;   // mikelee added; abort when pCut is NULL
             if ( pCut->iMat )
                 Amap_ManCutStore( p, pCut, pNode->fPhase ^ pTemp->fPhase );
+        }
         pTemp->pData = NULL;
     }
     Amap_ManCutSaveStored( p, pNode );