Updated code for lazy man's synthesis (memory optimization).

4 files changed, 368 insertions, 59 deletions

diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index 61f73705..7167de39 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -109,7 +109,7 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
 void Gia_ManHashAlloc( Gia_Man_t * p )  
 {
     assert( p->pHTable == NULL );
-    p->nHTable = Abc_PrimeCudd( p->nObjsAlloc );
+    p->nHTable = Abc_PrimeCudd( Gia_ManAndNum(p) ? Gia_ManAndNum(p) + 1000 : p->nObjsAlloc );
     p->pHTable = ABC_CALLOC( int, p->nHTable );
 }
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 31f03d80..b8a8afb8 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -52,8 +52,8 @@ Gia_Man_t * Gia_ManStart( int nObjsMax )
     p->pObjs = ABC_CALLOC( Gia_Obj_t, nObjsMax );
     p->pObjs->iDiff0 = p->pObjs->iDiff1 = GIA_NONE;
     p->nObjs = 1;
-    p->vCis  = Vec_IntAlloc( nObjsMax / 10 );
-    p->vCos  = Vec_IntAlloc( nObjsMax / 10 );
+    p->vCis  = Vec_IntAlloc( nObjsMax / 20 );
+    p->vCos  = Vec_IntAlloc( nObjsMax / 20 );
     return p;
 }
 
@@ -414,10 +414,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch )
     if ( Gia_ManRegNum(p) )
         printf( "  ff =%7d", Gia_ManRegNum(p) );
     printf( "  and =%8d", Gia_ManAndNum(p) );
-    printf( "  lev =%5d", Gia_ManLevelNum(p) );
+    printf( "  lev =%5d", Gia_ManLevelNum(p) ); Vec_IntFreeP( &p->vLevels );
     printf( "  cut =%5d", Gia_ManCrossCut(p) );
-    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
-//    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
+//    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
+    printf( "  mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjsAlloc + sizeof(int)*(Vec_IntCap(p->vCis) + Vec_IntCap(p->vCos)))/(1<<20) );
     if ( Gia_ManHasDangling(p) )
         printf( "  ch =%5d", Gia_ManEquivCountClasses(p) );
     if ( fSwitch )
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index ed7beea5..8010d553 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -22,16 +22,19 @@
 #include "map/if/if.h"
 #include "bool/kit/kit.h"
 #include "aig/gia/giaAig.h"
+#include "misc/vec/vecMem.h"
 
 ABC_NAMESPACE_IMPL_START
 
 //#define LibOut
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 #define  IF_BIG_CHAR 120
 #define  REC_EMPTY_ID -1
+
 typedef struct Abc_ManRec_t_2 Abc_ManRec_t2;
 typedef struct Rec_Obj_t_2 Rec_Obj_t2;
 
@@ -54,14 +57,14 @@ struct Rec_Obj_t_2
     char pinToPinDelay[0];      // structure's pin-to-pin delay
 };
 
-
 struct Abc_ManRec_t_2
 {
     Gia_Man_t *       pGia;                     // the record
-    Vec_Ptr_t *       vTtElems;                 // the elementary truth tables
-    Vec_Ptr_t *       vTtNodes;                 // the node truth tables
     Vec_Str_t *       vInputs;                  // the input number of nodes
-    Mem_Fixed_t *     pMmTruth;                 // memory manager for truth tables
+    Vec_Ptr_t *       vTtElems;                 // the elementary truth tables
+//    Vec_Ptr_t *       vTtNodes;                 // the node truth tables
+//    Mem_Fixed_t *     pMmTruth;                 // memory manager for truth tables
+    Vec_Mem_t *       vTtMem;                   // memory for truth tables of primary outputs
     int *             pBins;                    // hash table mapping truth tables into nodes
     int               nBins;                    // the number of allocated bins
     int               nVars;                    // the number of variables
@@ -74,13 +77,11 @@ struct Abc_ManRec_t_2
     char *            pRecObjs;
     int               nRecObjs;
     int               nRecObjsAlloc;
-
     // temporaries
     int *             pBytes;                   // temporary storage for minterms
     int *             pMints;                   // temporary storage for minterm counters
     unsigned *        pTemp1;                   // temporary truth table
     unsigned *        pTemp2;                   // temporary truth table
-
     Vec_Ptr_t *       vNodes;                   // the temporary nodes
     Vec_Ptr_t *       vTtTemps;                 // the truth tables for the internal nodes of the cut
     Vec_Ptr_t *       vLabels;                  // temporary storage for AIG node labels
@@ -129,19 +130,19 @@ static Abc_ManRec_t2 * s_pMan = NULL;
 static inline void Abc_ObjSetMax2( Vec_Str_t * p, Gia_Man_t * pGia, Gia_Obj_t * pObj, char Value )  { Vec_StrWriteEntry(p, Gia_ObjId(pGia, pObj), Value); }
 //static inline void Abc_ObjClearMax( Gia_Obj_t * pObj )          { pObj->Value = (pObj->Value & 0xff); }
 static inline int  Abc_ObjGetMax2( Vec_Str_t * p, Gia_Man_t * pGia, Gia_Obj_t * pObj )              { return Vec_StrEntry(p, Gia_ObjId(pGia, pObj)); }
-
 static inline int   Rec_ObjID(Abc_ManRec_t2 *p, Rec_Obj_t2 * pRecObj)                                  
 {   char * pObj = (char *)pRecObj;
     assert(p->pRecObjs <= pObj && pObj < p->pRecObjs + p->nRecObjs * p->recObjSize); 
     return (pObj - p->pRecObjs)/p->recObjSize;
 }
-
 static inline Rec_Obj_t2 * Rec_Obj(Abc_ManRec_t2 *p, int v)
 {
     assert( v < p->nRecObjs ); 
     return (Rec_Obj_t2 *)(p->pRecObjs + v * p->recObjSize);
 }
 
+static inline unsigned * Rec_MemReadEntry( Abc_ManRec_t2 * p, int i )                    { return (unsigned *)Vec_MemReadEntry( p->vTtMem, i ); }
+static inline void       Rec_MemSetEntry( Abc_ManRec_t2 * p, int i, unsigned * pEntry )  { Vec_MemSetEntry( p->vTtMem, i, (word *)pEntry );     }
 
 /**Function*************************************************************
 
@@ -628,7 +629,8 @@ static int * Abc_NtkRecTableLookup2(Abc_ManRec_t2* p,  int * pBins, int nBins, u
     int * ppSpot,  pEntry;
     ppSpot = pBins + Abc_NtkRecTableHash( pTruth, nVars, nBins, s_Primes );
     for ( pEntry = *ppSpot; pEntry != REC_EMPTY_ID; ppSpot = &(Rec_Obj(p,pEntry)->pCopy), pEntry = Rec_Obj(p,pEntry)->pCopy )
-        if ( Kit_TruthIsEqualWithPhase((unsigned *)Vec_PtrEntry(p->vTtNodes, pEntry), pTruth, nVars) )
+//        if ( Kit_TruthIsEqualWithPhase((unsigned *)Vec_PtrEntry(p->vTtNodes, pEntry), pTruth, nVars) )
+        if ( Kit_TruthIsEqualWithPhase( Rec_MemReadEntry(p, pEntry), pTruth, nVars) )
             return ppSpot;
     return ppSpot;
 }
@@ -651,7 +653,7 @@ static void Abc_NtkRecResizeHash2(Abc_ManRec_t2* p)
     int nBinsNew, Counter, i;
     int clk = clock();
     // get the new table size
-    nBinsNew = Cudd_Prime( 3 * p->nBins ); 
+    nBinsNew = Cudd_Prime( 2 * p->nBins ); 
     printf("Hash table resize from %d to %d.\n", p->nBins, nBinsNew);
     // allocate a new array
     pBinsNew = ABC_ALLOC( int, nBinsNew );
@@ -662,7 +664,8 @@ static void Abc_NtkRecResizeHash2(Abc_ManRec_t2* p)
         for ( pEntry = p->pBins[i]; pEntry != REC_EMPTY_ID;)
         {          
             pTemp = Rec_Obj(p, pEntry)->pCopy;
-            ppSpot = Abc_NtkRecTableLookup2(p, pBinsNew, nBinsNew, (unsigned *)Vec_PtrEntry(p->vTtNodes, pEntry), p->nVars);
+//            ppSpot = Abc_NtkRecTableLookup2(p, pBinsNew, nBinsNew, (unsigned *)Vec_PtrEntry(p->vTtNodes, pEntry), p->nVars);
+            ppSpot = Abc_NtkRecTableLookup2(p, pBinsNew, nBinsNew, Rec_MemReadEntry(p, pEntry), p->nVars);
             assert(*ppSpot == REC_EMPTY_ID);
             *ppSpot = pEntry;
             Rec_Obj(p, pEntry)->pCopy = REC_EMPTY_ID;
@@ -886,7 +889,8 @@ void Abc_NtkRecInsertToLookUpTable2(Abc_ManRec_t2* p, int* ppSpot, Gia_Obj_t* pP
     }
     hasRealloced = Rec_AppendObj(p, &pRecObj);
     if(hasRealloced)
-        ppSpot = Abc_NtkRecTableLookup2(p, p->pBins, p->nBins, (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pPO)), p->nVars );
+//        ppSpot = Abc_NtkRecTableLookup2(p, p->pBins, p->nBins, (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pPO)), p->nVars );
+        ppSpot = Abc_NtkRecTableLookup2(p, p->pBins, p->nBins, Rec_MemReadEntry(p, Gia_ObjCioId(pPO)), p->nVars );
     assert(Rec_ObjID(p, pRecObj) == Gia_ObjCioId(pPO));
     if(fTrim)
     {       
@@ -992,7 +996,7 @@ void Abc_NtkRecInsertToLookUpTable2(Abc_ManRec_t2* p, int* ppSpot, Gia_Obj_t* pP
 }
 
 
-
+/*
 int Abc_NtkRecComputeTruth2( Gia_Obj_t * pObj, Vec_Ptr_t * vTtNodes, int nVars )
 {
     unsigned * pTruth, * pTruth0, * pTruth1;
@@ -1010,13 +1014,13 @@ int Abc_NtkRecComputeTruth2( Gia_Obj_t * pObj, Vec_Ptr_t * vTtNodes, int nVars )
     //RetValue = ((pTruth[0] & 1) == pObj->fPhase);
     return 1;
 }
-
+*/
 void Abc_NtkRecStart2( Gia_Man_t * pGia, int nVars, int nCuts, int fTrim )
 {
     Abc_ManRec_t2 * p;
     Gia_Obj_t * pObj, *pFanin;
     int * ppSpot;
-    unsigned * pTruthDst, *pTruthSrc, *pTruth;
+    unsigned * pTruthSrc, * pTruth;//, * pTruthDst;
     int i, j = 0;
     int clkTotal = clock(), clk, timeInsert;
 
@@ -1044,16 +1048,19 @@ void Abc_NtkRecStart2( Gia_Man_t * pGia, int nVars, int nCuts, int fTrim )
         if ( Gia_ManPiNum(pGia) > nVars )
             printf( "The starting record has %d inputs (warning only).\n", Gia_ManPiNum(pGia) );
     }
-     Gia_ManHashStart( pGia );
+//    Gia_ManHashStart( pGia );
+    // move this to rec_add2, because if the library is never used for adding new structures
+    // structural hashing is not needed
+    if ( pGia->pHTable != NULL )
+        Gia_ManHashStop( pGia );
+
     // create the primary inputs
     for ( i = Gia_ManPiNum(pGia); i < nVars; i++ )
-    {
         Gia_ManAppendCi(pGia);
-    }
 
-    p = ABC_ALLOC( Abc_ManRec_t2, 1 );
+    p = ABC_CALLOC( Abc_ManRec_t2, 1 );
     s_pMan = p;
-    memset( p, 0, sizeof(Abc_ManRec_t2) );
+//    memset( p, 0, sizeof(Abc_ManRec_t2) ); // no need for this if we use ABC_CALLOC
     p->pGia = pGia;
     p->nVars = Gia_ManPiNum(pGia);
     p->nWords = Kit_TruthWordNum( p->nVars );
@@ -1073,13 +1080,13 @@ void Abc_NtkRecStart2( Gia_Man_t * pGia, int nVars, int nCuts, int fTrim )
     p->vTtElems->nCap = p->nVars;
     p->vTtElems->pArray = (void **)Extra_TruthElementary( p->nVars );  
     
-    p->vTtNodes = Vec_PtrAlloc( 1000 );
     p->vInputs = Vec_StrStart( 1 << 16 );
-    p->pMmTruth = Mem_FixedStart( sizeof(unsigned)*p->nWords );
     p->vUselessPos = Vec_IntAlloc(1 << 16);
-
-    for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
-        Vec_PtrPush( p->vTtNodes, Mem_FixedEntryFetch(p->pMmTruth) );
+//    p->vTtNodes = Vec_PtrAlloc( 1000 );
+//    p->pMmTruth = Mem_FixedStart( sizeof(unsigned)*p->nWords );
+//    for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
+//        Vec_PtrPush( p->vTtNodes, Mem_FixedEntryFetch(p->pMmTruth) );
+    p->vTtMem = Vec_MemAlloc( p->nWords/2, 12 ); // 32 KB/page for 6-var functions
 
     // create hash table
     //p->nBins = 50011;
@@ -1091,8 +1098,9 @@ clk = clock();
     Gia_ManForEachPo( pGia, pObj, i )
     {
         pTruthSrc = Gia_ObjComputeTruthTable(pGia, pObj);
-        pTruthDst = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
-        Kit_TruthCopy(pTruthDst, pTruthSrc, p->nVars);
+//        pTruthDst = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
+//        Kit_TruthCopy(pTruthDst, pTruthSrc, p->nVars);
+        Rec_MemSetEntry( p, Gia_ObjCioId(pObj), pTruthSrc );
     }
 p->timeTruth += clock() - clk;  
 
@@ -1106,7 +1114,8 @@ timeInsert = clock();
         // mark the nodes with CO fanout.
         assert(pFanin->fMark1 == 0);
         pFanin->fMark1 = 1;
-        pTruth = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
+//        pTruth = (unsigned *)Vec_PtrEntry( p->vTtNodes, Gia_ObjCioId(pObj) );
+        pTruth = Rec_MemReadEntry( p, Gia_ObjCioId(pObj) );
         // add the resulting truth table to the hash table 
         if(p->nAddedFuncs > 2 * p->nBins)
             Abc_NtkRecResizeHash2(p);
@@ -1163,7 +1172,8 @@ for ( i = 0; i < p->nBins; i++ )
     for ( entry = p->pBins[i]; entry != REC_EMPTY_ID; entry = Rec_Obj(p, entry)->pCopy )
     {
         int tmp = 0;
-        pTruth = (unsigned*)Vec_PtrEntry(p->vTtNodes, entry);
+//        pTruth = (unsigned*)Vec_PtrEntry(p->vTtNodes, entry);
+        pTruth = Rec_MemReadEntry( p, entry );
         /*if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
             continue;*/
         Extra_PrintHex( pFile, pTruth, nVars );
@@ -1449,7 +1459,7 @@ int Abc_NtkRecAddCut2( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     Vec_Ptr_t * vNodes = s_pMan->vNodes;
     unsigned * pInOut = s_pMan->pTemp1;
     unsigned * pTemp = s_pMan->pTemp2;
-    unsigned *pTruthSrc, *pTruthDst;
+    unsigned *pTruthSrc;//, *pTruthDst;
     int objectID = 0;
     int i, RetValue, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = If_CutLeaveNum(pCut);
     unsigned uCanonPhase;
@@ -1581,13 +1591,15 @@ s_pMan->timeBuild += clock() - timeBuild;
     assert(pObj->fMark1 == 0);
     pObj->fMark1 = 1;
 
-    if ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ManPoNum(pAig) )
-    {
-        while ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ObjCioId(pPO) )
-            Vec_PtrPush( s_pMan->vTtNodes, Mem_FixedEntryFetch(s_pMan->pMmTruth) );
-    }
-    pTruthDst = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, Gia_ObjCioId(pPO));
-    Kit_TruthCopy(pTruthDst, pTruthSrc, s_pMan->nVars);
+//    if ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ManPoNum(pAig) )
+//    {
+//        while ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ObjCioId(pPO) )
+//            Vec_PtrPush( s_pMan->vTtNodes, Mem_FixedEntryFetch(s_pMan->pMmTruth) );
+//    }
+
+//    pTruthDst = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, Gia_ObjCioId(pPO));
+//    Kit_TruthCopy(pTruthDst, pTruthSrc, s_pMan->nVars);
+    Rec_MemSetEntry( s_pMan, Gia_ObjCioId(pPO), pTruthSrc );
 
     // add the resulting truth table to the hash table 
     timeInsert = clock();
@@ -1619,7 +1631,11 @@ void Abc_NtkRecAdd2( Abc_Ntk_t * pNtk, int fUseSOPB)
     int clk = clock();
 
     if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing renoding with choices.\n" );
+        printf( "Performing recoding structures with choices.\n" );
+
+    // create hash table if not available
+    if ( s_pMan->pGia->pHTable == NULL )
+        Gia_ManHashStart( s_pMan->pGia );
 
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
@@ -1868,7 +1884,8 @@ int If_CutDelayRecCost2(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
     }
     s_pMan->nFunsFound++; 
     // make sure the truth table is the same
-    pTruthRec = (unsigned*)Vec_PtrEntry( s_pMan->vTtNodes, Rec_ObjID(s_pMan, pCandMin) );
+//    pTruthRec = (unsigned*)Vec_PtrEntry( s_pMan->vTtNodes, Rec_ObjID(s_pMan, pCandMin) );
+    pTruthRec = Rec_MemReadEntry( s_pMan, Rec_ObjID(s_pMan, pCandMin) );
     if ( !Kit_TruthIsEqualWithPhase( pTruthRec, pInOut, nLeaves ) )
     {
         assert( 0 );
@@ -2045,13 +2062,13 @@ void Abc_NtkRecStop2()
     assert( s_pMan != NULL );
 //    Abc_NtkRecDumpTruthTables( s_pMan );
     if ( s_pMan->pGia )
-    {
-        Gia_ManHashStop(s_pMan->pGia);
         Gia_ManStop(s_pMan->pGia);
-    }
 //    Vec_PtrFreeFree( s_pMan->vTtNodes );
-    Mem_FixedStop( s_pMan->pMmTruth, 0 );
-    Vec_PtrFree( s_pMan->vTtNodes );
+
+//    Mem_FixedStop( s_pMan->pMmTruth, 0 );
+//    Vec_PtrFree( s_pMan->vTtNodes );
+    Vec_MemFreeP( &s_pMan->vTtMem );
+
     Vec_StrFree( s_pMan->vInputs );
     Vec_PtrFree( s_pMan->vTtElems );
     ABC_FREE( s_pMan->pBins );
@@ -2162,7 +2179,6 @@ void Abc_NtkRecCutTruthFromLib2( Gia_Man_t * pGia2, Vec_Ptr_t * vNodes, int nLea
     assert ( Kit_TruthSupport(pSims, nInputs) == Kit_BitMask(nLeaves) );
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Adds the cut function to the internal storage.]
@@ -2183,7 +2199,7 @@ void Abc_NtkRecAddFromLib2( Gia_Man_t * pGia2, Gia_Obj_t * pRoot, int nVars )
     Vec_Ptr_t * vNodes = s_pMan->vNodes;
     unsigned * pInOut = s_pMan->pTemp1;
     //unsigned * pTemp = s_pMan->pTemp2;
-    unsigned *pTruthSrc, *pTruthDst;
+    unsigned *pTruthSrc;//, *pTruthDst;
     int objectID;
     int i, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = nVars;
     assert( nInputs <= 16 );
@@ -2241,13 +2257,16 @@ void Abc_NtkRecAddFromLib2( Gia_Man_t * pGia2, Gia_Obj_t * pRoot, int nVars )
     assert(pObj->fMark1 == 0);
     pObj->fMark1 = 1;
 
-    if ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ManPoNum(pGia) )
-    {
-        while ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ObjCioId(pPO) )
-            Vec_PtrPush( s_pMan->vTtNodes, Mem_FixedEntryFetch(s_pMan->pMmTruth) );
-    }
-    pTruthDst = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, Gia_ObjCioId(pPO));
-    Kit_TruthCopy(pTruthDst, pTruthSrc, s_pMan->nVars);
+//    if ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ManPoNum(pGia) )
+//    {
+//        while ( Vec_PtrSize(s_pMan->vTtNodes) <= Gia_ObjCioId(pPO) )
+//            Vec_PtrPush( s_pMan->vTtNodes, Mem_FixedEntryFetch(s_pMan->pMmTruth) );
+//    }
+
+//    pTruthDst = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, Gia_ObjCioId(pPO));
+//    Kit_TruthCopy(pTruthDst, pTruthSrc, s_pMan->nVars);
+    Rec_MemSetEntry( s_pMan, Gia_ObjCioId(pPO), pTruthSrc );
+
     // add the resulting truth table to the hash table 
     Abc_NtkRecInsertToLookUpTable2(s_pMan, ppSpot, pPO, nLeaves, s_pMan->fTrim);
     return;
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
new file mode 100644
index 00000000..229c53a2
--- /dev/null
+++ b/src/misc/vec/vecMem.h
@@ -0,0 +1,290 @@
+/**CFile****************************************************************
+
+  FileName    [vecMem.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable array of memory pieces.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 20, 2012.]
+
+  Revision    [$Id: vecMem.h,v 1.00 2012/07/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__misc__vec__vecMem_h
+#define ABC__misc__vec__vecMem_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+
+ABC_NAMESPACE_HEADER_START
+
+/* 
+   This vector stores pieces of memory of the given size.
+   It is useful for representing truth tables and any other objects
+   of the fixed size.  It is better that Extra_MmFixed because the
+   entry IDs can be used as handles to retrieve memory pieces without 
+   the need for an array of pointers from entry IDs into memory pieces
+   (this can save 8(4) bytes per object on a 64(32)-bit platform).
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Mem_t_       Vec_Mem_t;
+struct Vec_Mem_t_ 
+{
+    int              nEntrySize;  // entry size (in terms of 8-byte words)
+    int              nEntries;    // number of entries currently used
+    int              LogPageSze;  // log2 of page size (in terms of entries)
+    int              PageMask;    // page mask
+    int              nPageAlloc;  // number of pages currently allocated
+    int              iPage;       // the number of a page currently used   
+    word **          ppPages;     // memory pages
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define Vec_MemForEachEntry( vVec, pEntry, i )                                              \
+    for ( i = 0; (i < Vec_MemEntryNum(vVec)) && ((pEntry) = Vec_MemReadEntry(vVec, i)); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a memory vector.]
+
+  Description [Entry size is in terms of 8-byte words. Page size is log2
+  of the number of entries on one page.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Mem_t * Vec_MemAlloc( int nEntrySize, int LogPageSze )
+{
+    Vec_Mem_t * p;
+    p = ABC_CALLOC( Vec_Mem_t, 1 );
+    p->nEntrySize = nEntrySize;
+    p->LogPageSze = LogPageSze;
+    p->PageMask   = (1 << p->LogPageSze) - 1;
+    p->iPage      = -1;
+    return p;
+}
+static inline void Vec_MemFree( Vec_Mem_t * p )
+{
+    int i;
+    for ( i = 0; i <= p->iPage; i++ )
+        ABC_FREE( p->ppPages[i] );
+    ABC_FREE( p->ppPages );
+    ABC_FREE( p );
+}
+static inline void Vec_MemFreeP( Vec_Mem_t ** p )
+{
+    if ( *p == NULL )
+        return;
+    Vec_MemFree( *p );
+    *p = NULL;
+}
+static inline Vec_Mem_t * Vec_MemDup( Vec_Mem_t * pVec )
+{
+    Vec_Mem_t * p = NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the integer array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_MemFill( Vec_Mem_t * pVec, int nEntries )
+{
+}
+static inline void Vec_MemClean( Vec_Mem_t * pVec, int nEntries )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_MemEntrySize( Vec_Mem_t * p )
+{
+    return p->nEntrySize;
+}
+static inline int Vec_MemEntryNum( Vec_Mem_t * p )
+{
+    return p->nEntries;
+}
+static inline int Vec_MemPageSize( Vec_Mem_t * p )
+{
+    return p->LogPageSze;
+}
+static inline int Vec_MemPageNum( Vec_Mem_t * p )
+{
+    return p->iPage+1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline double Vec_MemMemory( Vec_Mem_t * p )
+{
+    return (double)sizeof(word) * p->nEntrySize * (1 << p->LogPageSze) * (p->iPage + 1) + (double)sizeof(word *) * p->nPageAlloc + (double)sizeof(Vec_Mem_t);
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline word * Vec_MemReadEntry( Vec_Mem_t * p, int i )
+{
+    assert( i >= 0 && i < p->nEntries );
+    return p->ppPages[i >> p->LogPageSze] + p->nEntrySize * (i & p->PageMask);
+}
+static inline word * Vec_MemReadEntryLast( Vec_Mem_t * p )
+{
+    assert( p->nEntries > 0 );
+    return Vec_MemReadEntry( p, p->nEntries-1 );
+}
+static inline void Vec_MemWriteEntry( Vec_Mem_t * p, int i, word * pEntry )
+{
+    word * pPlace = Vec_MemReadEntry( p, i );
+    memmove( pPlace, pEntry, sizeof(word) * p->nEntrySize );
+}
+static inline word * Vec_MemGetEntry( Vec_Mem_t * p, int i )
+{
+    assert( i >= 0 );
+    if ( i >= p->nEntries )
+    {
+        int k, iPageNew = (i >> p->LogPageSze);
+        if ( p->iPage < iPageNew )
+        {
+            // realloc page pointers if needed
+            if ( iPageNew >= p->nPageAlloc )
+                p->ppPages = ABC_REALLOC( word *, p->ppPages, (p->nPageAlloc = p->nPageAlloc ? 2 * p->nPageAlloc : iPageNew + 32) );
+            // allocate new pages if needed
+            for ( k = p->iPage + 1; k <= iPageNew; k++ )
+                p->ppPages[k] = ABC_ALLOC( word, p->nEntrySize * (1 << p->LogPageSze) );
+            // update page counter
+            p->iPage = iPageNew;
+        }
+        // update entry counter
+        p->nEntries = i + 1;
+    }
+    return Vec_MemReadEntry( p, i );
+}
+static inline void Vec_MemSetEntry( Vec_Mem_t * p, int i, word * pEntry )
+{
+    word * pPlace = Vec_MemGetEntry( p, i );
+    memmove( pPlace, pEntry, sizeof(word) * p->nEntrySize );
+}
+static inline void Vec_MemPush( Vec_Mem_t * p, word * pEntry )
+{
+    word * pPlace = Vec_MemGetEntry( p, p->nEntries );
+    memmove( pPlace, pEntry, sizeof(word) * p->nEntrySize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_MemShrink( Vec_Mem_t * p, int nEntriesNew )
+{
+    int i, iPageOld = p->iPage;
+    assert( nEntriesNew <= p->nEntries );
+    p->nEntries = nEntriesNew;
+    p->iPage = (nEntriesNew >> p->LogPageSze);
+    for ( i = p->iPage + 1; i <= iPageOld; i++ )
+        ABC_FREE( p->ppPages[i] );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_MemPrint( Vec_Mem_t * vVec )
+{
+    word * pEntry;
+    int i;
+    printf( "Memory vector has %d entries: ", Vec_MemEntryNum(vVec) );
+    Vec_MemForEachEntry( vVec, pEntry, i )
+    {
+        printf( "%3d : ", i );
+        // add printout here
+        printf( "\n" );
+    }
+}
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+