Version abc60804

34 files changed, 1230 insertions, 383 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7bee7f40..bb8f5658 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4487,22 +4487,26 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPlaMax;
     int RankCost;
     int fFastMode;
+    int fRewriting;
+    int fSynthesis;
     int fVerbose;
-//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fEsop, bool fSop, bool fInvs, bool fVerbose );
+    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax   = 8;
-    nPlaMax   = 128;
-    RankCost  = 96000;
-    fFastMode = 0;
-    fVerbose  = 0;
+    nLutMax    = 8;
+    nPlaMax    = 128;
+    RankCost   = 96000;
+    fFastMode  = 1;
+    fRewriting = 1;
+    fSynthesis = 0;
+    fVerbose   = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4542,6 +4546,12 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             fFastMode ^= 1;
             break;
+        case 'r':
+            fRewriting ^= 1;
+            break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -4570,8 +4580,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fVerbose );
+//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
+    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -4582,12 +4592,14 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-fvh]\n" );
+    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-frsvh]\n" );
     fprintf( pErr, "\t         specilized LUT/PLA decomposition\n" );
     fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax );
     fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax );
     fprintf( pErr, "\t-R num : maximum are of one decomposition rank [default = %d]\n", RankCost );
     fprintf( pErr, "\t-f     : toggle using fast LUT mapping mode [default = %s]\n", fFastMode? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle using one pass of AIG rewriting [default = %s]\n", fRewriting? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle using synthesis by AIG rewriting [default = %s]\n", fSynthesis? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index a3ffcf4e..380b3f8b 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -343,9 +343,11 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 //    Ivy_ManRequiredLevels( pMan );
 
-    Pla_ManFastLutMap( pMan, 8 );
-    Ivy_ManStop( pMan );
+//    Pla_ManFastLutMap( pMan, 8 );
+//    Ivy_ManStop( pMan );
     return NULL;
+
+
 /*
     // convert from the AIG manager
     pNtkAig = Abc_NtkFromAig( pNtk, pMan );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f447516f..b8491d06 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -408,7 +408,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
 int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
 {
 //  nLevelMax = ((nLevelMax)/2)*3;
-    assert( pObj->Level <= nLevelMax );
+    assert( (int)pObj->Level <= nLevelMax );
 //    return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
     return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
 //    return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index a40954bd..d2d731d9 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -647,9 +647,10 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pFanout;
     int i, k, nLevelsCur;
-    assert( Abc_NtkIsStrash(pNtk) );
+//    assert( Abc_NtkIsStrash(pNtk) );
     // remember the maximum number of direct levels
-    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+//    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+    pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk);
     // start the reverse levels
     pNtk->vLevelsR = Vec_IntAlloc( 0 );
     Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index ecf77f70..5c4a0675 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -136,11 +136,11 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
-    extern void Ivy_TruthManStop();
+//    extern void Ivy_TruthManStop();
 //    Abc_HManStop();
     undefine_cube_size();
     Rwt_ManGlobalStop();
-    Ivy_TruthManStop();
+//    Ivy_TruthManStop();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );
diff --git a/src/misc/nm/nmApi.c b/src/misc/nm/nmApi.c
index e44d1ef9..120dbe91 100644
--- a/src/misc/nm/nmApi.c
+++ b/src/misc/nm/nmApi.c
@@ -46,10 +46,10 @@ Nm_Man_t * Nm_ManCreate( int nSize )
     p = ALLOC( Nm_Man_t, 1 );
     memset( p, 0, sizeof(Nm_Man_t) );
     // set the parameters
-    p->nSizeFactor   = 4; // determined how much larger the table should be compared to data in it
-    p->nGrowthFactor = 4; // determined how much the table grows after resizing
+    p->nSizeFactor   = 2; // determined how much larger the table should be compared to data in it
+    p->nGrowthFactor = 3; // determined how much the table grows after resizing
     // allocate and clean the bins
-    p->nBins = Cudd_PrimeNm(p->nSizeFactor*nSize);
+    p->nBins = Cudd_PrimeNm(nSize);
     p->pBinsI2N = ALLOC( Nm_Entry_t *, p->nBins );
     p->pBinsN2I = ALLOC( Nm_Entry_t *, p->nBins );
     memset( p->pBinsI2N, 0, sizeof(Nm_Entry_t *) * p->nBins );
@@ -127,6 +127,7 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, char * pName, char * pSuffix
     nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1;
     nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
     pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize );
+    pEntry->pNextI2N = pEntry->pNextN2I = NULL;
     pEntry->ObjId = ObjId;
     sprintf( pEntry->Name, "%s%s", pName, pSuffix? pSuffix : "" );
     // add the entry to the hash table
diff --git a/src/misc/nm/nmInt.h b/src/misc/nm/nmInt.h
index 43901993..8356a4cb 100644
--- a/src/misc/nm/nmInt.h
+++ b/src/misc/nm/nmInt.h
@@ -45,6 +45,8 @@ typedef struct Nm_Entry_t_ Nm_Entry_t;
 struct Nm_Entry_t_
 {
     int              ObjId;         // object ID
+    Nm_Entry_t *     pNextI2N;      // the next entry in the ID hash table
+    Nm_Entry_t *     pNextN2I;      // the next entry in the name hash table
     char             Name[0];       // name of the object
 };
 
diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c
index 4243244d..4eeaf610 100644
--- a/src/misc/nm/nmTable.c
+++ b/src/misc/nm/nmTable.c
@@ -44,7 +44,7 @@ static unsigned Nm_HashString( char * pName, int TableSize )
     };
     unsigned i, Key = 0;
     for ( i = 0; pName[i] != '\0'; i++ )
-        Key ^= s_Primes[i%10]*pName[i]*pName[i]*pName[i];
+        Key ^= s_Primes[i%10]*pName[i]*pName[i];
     return Key % TableSize;
 }
 
@@ -67,13 +67,16 @@ static void Nm_ManResize( Nm_Man_t * p );
 ***********************************************************************/
 int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry )
 {
-    int i;
+    Nm_Entry_t ** ppSpot;
+//    int i;
     // resize the tables if needed
-    if ( p->nEntries * p->nSizeFactor > p->nBins )
+//    if ( p->nEntries * p->nSizeFactor > p->nBins )
+    if ( p->nEntries > p->nBins * p->nSizeFactor )
     {
 //        Nm_ManPrintTables( p );
         Nm_ManResize( p );
     }
+/*
     // hash it by ID
     for ( i = Nm_HashNumber(pEntry->ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins )
         if ( p->pBinsI2N[i] == pEntry )
@@ -86,6 +89,15 @@ int Nm_ManTableAdd( Nm_Man_t * p, Nm_Entry_t * pEntry )
             return 0;
     assert( p->pBinsN2I[i] == NULL );
     p->pBinsN2I[i] = pEntry;
+*/
+    ppSpot = p->pBinsI2N + Nm_HashNumber(pEntry->ObjId, p->nBins);
+    pEntry->pNextI2N = *ppSpot;
+    *ppSpot = pEntry;
+
+    ppSpot = p->pBinsN2I + Nm_HashString(pEntry->Name, p->nBins);
+    pEntry->pNextN2I = *ppSpot;
+    *ppSpot = pEntry;
+
     // report successfully added entry
     p->nEntries++;
     return 1;
@@ -121,10 +133,16 @@ int Nm_ManTableDelete( Nm_Man_t * p, Nm_Entry_t * pEntry )
 ***********************************************************************/
 Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
 {
-    int i;
+    Nm_Entry_t * pEntry;
+//    int i;
+/*
     for ( i = Nm_HashNumber(ObjId, p->nBins); p->pBinsI2N[i]; i = (i+1) % p->nBins )
         if ( p->pBinsI2N[i]->ObjId == ObjId )
             return p->pBinsI2N[i];
+*/
+    for ( pEntry = p->pBinsI2N[ Nm_HashNumber(ObjId, p->nBins) ]; pEntry; pEntry = pEntry->pNextI2N )
+        if ( pEntry->ObjId == ObjId )
+            return pEntry;
     return NULL;
 }
 
@@ -141,9 +159,10 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
 ***********************************************************************/
 Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond )
 {
-    Nm_Entry_t * pFirst, * pSecond;
-    int i, Counter = 0;
+    Nm_Entry_t * pFirst, * pSecond, * pEntry;
+    int Counter = 0;
     pFirst = pSecond = NULL;
+/*
     for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins )
         if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 )
         {
@@ -158,12 +177,60 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
             Counter++;
     if ( Counter > 100 )
     printf( "%d ", Counter );
+*/
+    for ( pEntry = p->pBinsN2I[ Nm_HashString(pName, p->nBins) ]; pEntry; pEntry = pEntry->pNextN2I )
+        if ( strcmp(pEntry->Name, pName) == 0 )
+        {
+            if ( pFirst == NULL )
+                pFirst = pEntry;
+            else if ( pSecond == NULL )
+                pSecond = pEntry;
+            else
+                assert( 0 ); // name appears more than 2 times
+        }
+
     // save the names
     if ( ppSecond )
         *ppSecond = pSecond;
     return pFirst;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Profiles hash tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nm_ManProfile( Nm_Man_t * p )
+{
+    Nm_Entry_t * pEntry;
+    int Counter, e;
+    printf( "I2N table: " );
+    for ( e = 0; e < p->nBins; e++ )
+    {
+        Counter = 0;
+        for ( pEntry = p->pBinsI2N[e]; pEntry; pEntry = pEntry->pNextI2N )
+            Counter++;
+        printf( "%d ", Counter );
+    }
+    printf( "\n" );
+    printf( "N2I table: " );
+    for ( e = 0; e < p->nBins; e++ )
+    {
+        Counter = 0;
+        for ( pEntry = p->pBinsN2I[e]; pEntry; pEntry = pEntry->pNextN2I )
+            Counter++;
+        printf( "%d ", Counter );
+    }
+    printf( "\n" );
+}
+
+
 
 /**Function*************************************************************
 
@@ -178,8 +245,8 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
 ***********************************************************************/
 void Nm_ManResize( Nm_Man_t * p )
 {
-    Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry;
-    int nBinsNew, Counter, e, i, clk;
+    Nm_Entry_t ** pBinsNewI2N, ** pBinsNewN2I, * pEntry, * pEntry2, ** ppSpot;
+    int nBinsNew, Counter, e, clk;
 
 clk = clock();
     // get the new table size
@@ -192,12 +259,13 @@ clk = clock();
     // rehash the entries from the old table
     Counter = 0;
     for ( e = 0; e < p->nBins; e++ )
+    for ( pEntry = p->pBinsI2N[e], pEntry2 = pEntry? pEntry->pNextI2N : NULL; 
+          pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNextI2N : NULL )
     {
-        pEntry = p->pBinsI2N[e];
-        if ( pEntry == NULL )
-            continue;
-        Counter++;
-
+//        pEntry = p->pBinsI2N[e];
+//        if ( pEntry == NULL )
+//            continue;
+/*
         // hash it by ID
         for ( i = Nm_HashNumber(pEntry->ObjId, nBinsNew); pBinsNewI2N[i]; i = (i+1) % nBinsNew )
             if ( pBinsNewI2N[i] == pEntry )
@@ -210,6 +278,16 @@ clk = clock();
                 assert( 0 );
         assert( pBinsNewN2I[i] == NULL );
         pBinsNewN2I[i] = pEntry;
+*/
+        ppSpot = pBinsNewI2N + Nm_HashNumber(pEntry->ObjId, nBinsNew);
+        pEntry->pNextI2N = *ppSpot;
+        *ppSpot = pEntry;
+
+        ppSpot = pBinsNewN2I + Nm_HashString(pEntry->Name, nBinsNew);
+        pEntry->pNextN2I = *ppSpot;
+        *ppSpot = pEntry;
+
+        Counter++;
     }
     assert( Counter == p->nEntries );
 //    printf( "Increasing the structural table size from %6d to %6d. ", p->nBins, nBinsNew );
@@ -220,10 +298,10 @@ clk = clock();
     p->pBinsI2N = pBinsNewI2N;
     p->pBinsN2I = pBinsNewN2I;
     p->nBins = nBinsNew;
+//    Nm_ManProfile( p );
 }
 
 
-
 /**Function*************************************************************
 
   Synopsis    [Returns the smallest prime larger than the number.]
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 4f193cf2..4a97fc91 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -583,6 +583,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the pointer to the next nWords entries in the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
+{
+    p->nSize += nWords;
+    if ( p->nSize > p->nCap )
+    {
+//         Vec_IntGrow( p, 2 * p->nSize );
+        return NULL;
+    }
+    return ((unsigned *)p->pArray) + p->nSize - nWords;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the last entry and removes it from the list.]
 
   Description []
diff --git a/src/opt/cut/abcCut.c b/src/opt/cut/abcCut.c
new file mode 100644
index 00000000..b4b879a3
--- /dev/null
+++ b/src/opt/cut/abcCut.c
@@ -0,0 +1,491 @@
+/**CFile****************************************************************
+
+  FileName    [abcCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface to cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+#include "seqInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
+static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
+
+
+extern int nTotal, nGood, nEqual;
+
+// temporary
+//Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) { return NULL; }
+Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Int_t * vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
+    int i;
+    Abc_Obj_t * pObj;
+
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
+            Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+    }
+    return vAttrs; 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    ProgressBar * pProgress;
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj, * pNode;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vChoices;
+    int i;
+    int clk = clock();
+
+    extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
+    extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+
+    nTotal = nGood = nEqual = 0;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    p = Cut_ManStart( pParams );
+    // compute node attributes if local or global cuts are requested
+    if ( pParams->fGlobal || pParams->fLocal )
+    {
+        extern Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+        Cut_ManSetNodeAttrs( p, Abc_NtkGetNodeAttributes(pNtk) );
+    }
+    // prepare for cut dropping
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( p, pObj->Id );
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+    vChoices = Vec_IntAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( pParams->fDrop )
+                Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // compute the cuts to the internal node
+        Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree );  
+        // consider dropping the fanins cuts
+        if ( pParams->fDrop )
+        {
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
+        // add cuts due to choices
+        if ( Abc_NodeIsAigChoice(pObj) )
+        {
+            Vec_IntClear( vChoices );
+            for ( pNode = pObj; pNode; pNode = pNode->pData )
+                Vec_IntPush( vChoices, pNode->Id );
+            Cut_NodeUnionCuts( p, vChoices );
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vChoices );
+PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts( p, pNtk, 0 );
+//    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
+
+    // temporary printout of stats
+    if ( nTotal )
+    printf( "Total cuts = %d. Good cuts = %d.  Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cut computation using the oracle.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p )
+{
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vNodes;
+    int i, clk = clock();
+    int fDrop = Cut_OracleReadDrop(p);
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // prepare cut droppping
+    if ( fDrop )
+        Cut_OracleSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_OracleNodeSetTriv( p, pObj->Id );
+
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( fDrop )
+                Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        // compute the cuts to the internal node
+        Cut_OracleComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+                Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        // consider dropping the fanins cuts
+        if ( fDrop )
+        {
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            Cut_OracleTryDroppingCuts( p, Abc_ObjFaninId1(pObj) );
+        }
+    }
+    Vec_PtrFree( vNodes );
+//PRT( "Total", clock() - clk );
+//Abc_NtkPrintCuts_( p, pNtk, 0 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj, * pNode;
+    int i, nIters, fStatus;
+    Vec_Int_t * vChoices;
+    int clk = clock();
+
+    assert( Abc_NtkIsSeq(pNtk) );
+    assert( pParams->fSeq );
+//    assert( Abc_NtkIsDfsOrdered(pNtk) );
+
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    pParams->nCutSet = Abc_NtkCutSetNodeNum( pNtk );
+    p = Cut_ManStart( pParams );
+
+    // set cuts for the constant node and the PIs
+    pObj = Abc_NtkConst1(pNtk);
+    if ( Abc_ObjFanoutNum(pObj) > 0 )
+        Cut_NodeSetTriv( p, pObj->Id );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+    {
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+        Cut_NodeSetTriv( p, pObj->Id );
+    }
+    // label the cutset nodes and set their number in the array
+    // assign the elementary cuts to the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+    {
+        assert( pObj->fMarkC == 0 );
+        pObj->fMarkC = 1;
+        pObj->pCopy = (Abc_Obj_t *)i;
+        Cut_NodeSetTriv( p, pObj->Id );
+//printf( "Setting trivial cut %d.\n", pObj->Id );
+    }
+
+    // process the nodes
+    vChoices = Vec_IntAlloc( 100 );
+    for ( nIters = 0; nIters < 10; nIters++ )
+    {
+//printf( "ITERATION %d:\n", nIters );
+        // compute the cuts for the internal nodes
+        Abc_AigForEachAnd( pNtk, pObj, i )
+        {
+            Abc_NodeGetCutsSeq( p, pObj, nIters==0 );
+            // add cuts due to choices
+            if ( Abc_NodeIsAigChoice(pObj) )
+            {
+                Vec_IntClear( vChoices );
+                for ( pNode = pObj; pNode; pNode = pNode->pData )
+                    Vec_IntPush( vChoices, pNode->Id );
+                Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 );
+            }
+        }
+        // merge the new cuts with the old cuts
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Cut_NodeNewMergeWithOld( p, pObj->Id );
+        // for the cutset, transfer temp cuts to new cuts
+        fStatus = 0;
+        Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+            fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i );
+        if ( fStatus == 0 )
+            break;
+    }
+    Vec_IntFree( vChoices );
+
+    // if the status is not finished, transfer new to old for the cutset
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        Cut_NodeNewMergeWithOld( p, pObj->Id );
+
+    // transfer the old cuts to the new positions
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        Cut_NodeOldTransferToNew( p, pObj->Id );
+
+    // unlabel the cutset nodes
+    Abc_SeqForEachCutsetNode( pNtk, pObj, i )
+        pObj->fMarkC = 0;
+if ( pParams->fVerbose )
+{
+PRT( "Total", clock() - clk );
+printf( "Converged after %d iterations.\n", nIters );
+}
+//Abc_NtkPrintCuts( p, pNtk, 1 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
+{
+    void * pList;
+    if ( pList = Abc_NodeReadCuts( p, pObj ) )
+        return pList;
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree );
+    Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree );
+    return Abc_NodeGetCuts( p, pObj, fDag, fTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
+{
+    Abc_Obj_t * pFanin;
+    int fDagNode, fTriv, TreeCode = 0;
+//    assert( Abc_NtkIsStrash(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+
+
+    // check if the node is a DAG node
+    fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
+    // increment the counter of DAG nodes
+    if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+    // add the trivial cut if the node is a DAG node, or if we compute all cuts
+    fTriv = fDagNode || !fDag;
+    // check if fanins are DAG nodes
+    if ( fTree )
+    {
+        pFanin = Abc_ObjFanin0(pObj);
+        TreeCode |=  (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin));
+        pFanin = Abc_ObjFanin1(pObj);
+        TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
+    }
+
+
+    // changes due to the global/local cut computation
+    {
+        Cut_Params_t * pParams = Cut_ManReadParams(p);
+        if ( pParams->fLocal )
+        {
+            Vec_Int_t * vNodeAttrs = Cut_ManReadNodeAttrs(p);
+            fDagNode = Vec_IntEntry( vNodeAttrs, pObj->Id );
+            if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+//            fTriv = fDagNode || !pParams->fGlobal;
+            fTriv = !Vec_IntEntry( vNodeAttrs, pObj->Id );
+            TreeCode = 0;
+            pFanin = Abc_ObjFanin0(pObj);
+            TreeCode |=  Vec_IntEntry( vNodeAttrs, pFanin->Id );
+            pFanin = Abc_ObjFanin1(pObj);
+            TreeCode |= (Vec_IntEntry( vNodeAttrs, pFanin->Id ) << 1);
+        }
+    }
+    return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv )
+{
+    int CutSetNum;
+    assert( Abc_NtkIsSeq(pObj->pNtk) );
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    fTriv     = pObj->fMarkC ? 0 : fTriv;
+    CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1;
+    Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+        Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj )
+{
+    return Cut_NodeReadCutsNew( p, pObj->Id );  
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj )
+{
+    Cut_NodeFreeCuts( p, pObj->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    int i;
+    printf( "Cuts of the network:\n" );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        pList = Abc_NodeReadCuts( p, pObj );
+        printf( "Node %s:\n", Abc_ObjName(pObj) );
+        Cut_CutPrintList( pList, fSeq );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
+{
+    Cut_Man_t * pMan = p;
+    Cut_Cut_t * pList;
+    Abc_Obj_t * pObj;
+    pObj = Abc_NtkObj( pNtk, 2 * Abc_NtkObjNum(pNtk) / 3 );
+    pList = Abc_NodeReadCuts( p, pObj );
+    printf( "Node %s:\n", Abc_ObjName(pObj) );
+    Cut_CutPrintList( pList, fSeq );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cut60720.zip b/src/opt/cut/cut60720.zip
new file mode 100644
index 00000000..86ad6726
--- /dev/null
+++ b/src/opt/cut/cut60720.zip
diff --git a/src/opt/cut/cut60721.zip b/src/opt/cut/cut60721.zip
new file mode 100644
index 00000000..d55ccfd0
--- /dev/null
+++ b/src/opt/cut/cut60721.zip
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index adff525f..1f93b14b 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -399,11 +399,9 @@ p->timeMerge += clock() - clk;
     // set the list at the node
     Vec_PtrFillExtra( p->vCutsNew, Node + 1, NULL );
     assert( Cut_NodeReadCutsNew(p, Node) == NULL );
-
     /////
-    pList->pNext = NULL;
+//    pList->pNext = NULL;
     /////
-
     Cut_NodeWriteCutsNew( p, Node, pList );
     // filter the cuts
 //clk = clock();
diff --git a/src/sat/msat/msatActivity.c b/src/sat/msat/msatActivity.c
index f808d9bc..23925669 100644
--- a/src/sat/msat/msatActivity.c
+++ b/src/sat/msat/msatActivity.c
@@ -46,7 +46,7 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
         return;
     Var = MSAT_LIT2VAR(Lit);
     if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
-//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pLevel[Var])) > 1e100 )
+//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }
diff --git a/src/sat/msat/msatInt.h b/src/sat/msat/msatInt.h
index 15932c67..7845ec0b 100644
--- a/src/sat/msat/msatInt.h
+++ b/src/sat/msat/msatInt.h
@@ -119,7 +119,7 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
-    int *               pLevels;     // the levels of the variables
+    int *               pActLevels;  // the levels of the variables
     double              dVarInc;     // Amount to bump next variable with.
     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.
diff --git a/src/sat/msat/msatSolverApi.c b/src/sat/msat/msatSolverApi.c
index 8c1542df..9317dcac 100644
--- a/src/sat/msat/msatSolverApi.c
+++ b/src/sat/msat/msatSolverApi.c
@@ -174,11 +174,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pLevels    = ALLOC( int, p->nVarsAlloc );
+    p->pActLevels = ALLOC( int, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
     {
         p->pdActivity[i] = 0;
-        p->pLevels = 0;
+        p->pActLevels[i] = 0;
     }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
@@ -243,7 +243,7 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pLevels    = REALLOC( int, p->pLevels, p->nVarsAlloc );
+    p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
         p->pdActivity[i] = 0;
 
@@ -399,7 +399,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
-    FREE( p->pLevels );
+    FREE( p->pActLevels );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 7fb054f7..a36c795b 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -66,7 +66,7 @@ typedef enum {
 } Ivy_Init_t;
 
 // the AIG node
-struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)
+struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)   // 10 words - 16 words
 {
     int              Id;             // integer ID
     int              TravId;         // traversal ID
@@ -81,6 +81,10 @@ struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)
     Ivy_Obj_t *      pFanin0;        // fanin
     Ivy_Obj_t *      pFanin1;        // fanin
     Ivy_Obj_t *      pFanout;        // fanout
+    Ivy_Obj_t *      pNextFan0;      // next fanout of the first fanin
+    Ivy_Obj_t *      pNextFan1;      // next fanout of the second fanin
+    Ivy_Obj_t *      pPrevFan0;      // prev fanout of the first fanin
+    Ivy_Obj_t *      pPrevFan1;      // prev fanout of the second fanin
     Ivy_Obj_t *      pEquiv;         // equivalent node
 };
 
@@ -106,7 +110,8 @@ struct Ivy_Man_t_
     int              nTravIds;       // the traversal ID
     int              nLevelMax;      // the maximum level
     Vec_Int_t *      vRequired;      // required times
-    Vec_Ptr_t *      vFanouts;       // representation of the fanouts
+//    Vec_Ptr_t *      vFanouts;       // representation of the fanouts
+    int              fFanout;        // fanout is allocated
     void *           pData;          // the temporary data
     void *           pCopy;          // the temporary data
     // memory management
@@ -384,6 +389,7 @@ extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t *
 extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
 /*=== ivyCheck.c ========================================================*/
 extern int             Ivy_ManCheck( Ivy_Man_t * p );
+extern int             Ivy_ManCheckFanouts( Ivy_Man_t * p );
 /*=== ivyCut.c ==========================================================*/
 extern void            Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
 extern Ivy_Store_t *   Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves );
@@ -407,12 +413,10 @@ extern void            Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Ob
 extern void            Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
 extern void            Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew );
 extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
-extern Ivy_Obj_t *     Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 /*=== ivyIsop.c ==========================================================*/
-extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover );
-extern void            Ivy_TruthManStop();
+extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
 extern void            Ivy_ManStop( Ivy_Man_t * p );
@@ -450,6 +454,7 @@ extern Ivy_Obj_t *     Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, I
 extern Ivy_Obj_t *     Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs );
 extern Ivy_Obj_t *     Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init );
 /*=== ivyResyn.c =========================================================*/
+extern Ivy_Man_t *     Ivy_ManResyn0( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
 extern Ivy_Man_t *     Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbose );
 /*=== ivyRewrite.c =========================================================*/
 extern int             Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index 36222f72..ebae64ff 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -115,7 +115,7 @@ int Ivy_ManCheck( Ivy_Man_t * p )
         if ( Ivy_ObjRefs(pObj) == 0 )
             printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
         // check fanouts
-        if ( p->vFanouts && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
+        if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
             printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
     }
     // count the number of nodes in the table
@@ -124,9 +124,95 @@ int Ivy_ManCheck( Ivy_Man_t * p )
         printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
     }
+//    if ( !Ivy_ManCheckFanouts(p) )
+//        return 0;
     if ( !Ivy_ManIsAcyclic(p) )
         return 0;
-    return 1;
+    return 1; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManCheckFanouts( Ivy_Man_t * p )
+{
+    Vec_Ptr_t * vFanouts;
+    Ivy_Obj_t * pObj, * pFanout, * pFanin;
+    int i, k, RetValue = 1;
+    if ( !p->fFanout )
+        return 1;
+    vFanouts = Vec_PtrAlloc( 100 );
+    // make sure every fanin is a fanout
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        pFanin = Ivy_ObjFanin0(pObj);
+        if ( pFanin == NULL )
+            continue;
+        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
+            if ( pFanout == pObj )
+                break;
+        if ( k == Vec_PtrSize(vFanouts) )
+        {
+            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
+            RetValue = 0;
+        }
+
+        pFanin = Ivy_ObjFanin1(pObj);
+        if ( pFanin == NULL )
+            continue;
+        Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k )
+            if ( pFanout == pObj )
+                break;
+        if ( k == Vec_PtrSize(vFanouts) )
+        {
+            printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id );
+            RetValue = 0;
+        }
+        // check that the previous fanout has the same fanin
+        if ( pObj->pPrevFan0 )
+        {
+            if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
+                 Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 
+                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 
+                 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) )
+            {
+                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id );
+                RetValue = 0;
+            }
+        }
+        // check that the previous fanout has the same fanin
+        if ( pObj->pPrevFan1 )
+        {
+            if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
+                 Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 
+                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 
+                 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) )
+            {
+                printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id );
+                RetValue = 0;
+            }
+        }
+    }
+    // make sure every fanout is a fanin
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k )
+            if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj )
+            {
+                printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id );
+                RetValue = 0;
+            }
+    }
+    Vec_PtrFree( vFanouts );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 56f872e9..65ba4aac 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -867,6 +867,24 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore )
   SeeAlso     []
 
 ***********************************************************************/
+static inline Ivy_Obj_t * Ivy_ObjRealFanin( Ivy_Obj_t * pObj )
+{
+    if ( !Ivy_ObjIsBuf(pObj) )
+        return pObj;
+    return Ivy_ObjRealFanin( Ivy_ObjFanin0(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves )
 {
     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
@@ -911,11 +929,14 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
                 continue;
             Ivy_NodeCutHash( pCutNew );
 */
-            iLeaf0 = Ivy_ObjFaninId0(pLeaf);
-            iLeaf1 = Ivy_ObjFaninId1(pLeaf);
+            iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) );
+            iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) );
             if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) )
                 continue;
-            Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
+            if ( iLeaf0 > iLeaf1 )
+                Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 );
+            else
+                Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 );
             Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
             if ( pCutStore->nCuts == IVY_CUT_LIMIT )
                 break;
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 30671baf..7246ec25 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -265,7 +265,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
 {
     if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) )
         return 1;
-    assert( Ivy_ObjIsNode( pNode ) );
+    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
     // make sure the node is not visited
     assert( !Ivy_ObjIsTravIdPrevious(p, pNode) );
     // check if the node is part of the combinational loop
@@ -290,7 +290,7 @@ int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode )
         }
     }
     // check if the fanin is visited
-    if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) 
+    if ( Ivy_ObjIsNode(pNode) && !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) 
     {
         // traverse the fanin's cone searching for the loop
         if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) )
diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c
index 2295516d..3930186a 100644
--- a/src/temp/ivy/ivyFanout.c
+++ b/src/temp/ivy/ivyFanout.c
@@ -24,9 +24,96 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Ivy_FanoutIsArray( void * p )    { return (int )(((unsigned)p) & 01);          }
-static inline Vec_Ptr_t *  Ivy_FanoutGetArray( void * p )   { assert( Ivy_FanoutIsArray(p) );  return (Vec_Ptr_t *)((unsigned)(p) & ~01);  }
-static inline Vec_Ptr_t *  Ivy_FanoutSetArray( void * p )   { assert( !Ivy_FanoutIsArray(p) ); return (Vec_Ptr_t *)((unsigned)(p) ^  01);  }
+// getting hold of the next fanout of the node
+static inline Ivy_Obj_t * Ivy_ObjNextFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    if ( pFanout == NULL )
+        return NULL;
+    if ( Ivy_ObjFanin0(pFanout) == pObj )
+        return pFanout->pNextFan0;
+    assert( Ivy_ObjFanin1(pFanout) == pObj );
+    return pFanout->pNextFan1;
+}
+
+// getting hold of the previous fanout of the node
+static inline Ivy_Obj_t * Ivy_ObjPrevFanout( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    if ( pFanout == NULL )
+        return NULL;
+    if ( Ivy_ObjFanin0(pFanout) == pObj )
+        return pFanout->pPrevFan0;
+    assert( Ivy_ObjFanin1(pFanout) == pObj );
+    return pFanout->pPrevFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    if ( Ivy_ObjFanin0(pFanout) == pObj )
+        return &pFanout->pNextFan0;
+    assert( Ivy_ObjFanin1(pFanout) == pObj );
+    return &pFanout->pNextFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    if ( Ivy_ObjFanin0(pFanout) == pObj )
+        return &pFanout->pPrevFan0;
+    assert( Ivy_ObjFanin1(pFanout) == pObj );
+    return &pFanout->pPrevFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjPrevNextFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    Ivy_Obj_t * pTemp;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    pTemp = Ivy_ObjPrevFanout(pObj, pFanout);
+    if ( pTemp == NULL )
+        return &pObj->pFanout;
+    if ( Ivy_ObjFanin0(pTemp) == pObj )
+        return &pTemp->pNextFan0;
+    assert( Ivy_ObjFanin1(pTemp) == pObj );
+    return &pTemp->pNextFan1;
+}
+
+// getting hold of the place where the next fanout will be attached
+static inline Ivy_Obj_t ** Ivy_ObjNextPrevFanoutPlace( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+{
+    Ivy_Obj_t * pTemp;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_IsComplement(pFanout) );
+    pTemp = Ivy_ObjNextFanout(pObj, pFanout);
+    if ( pTemp == NULL )
+        return NULL;
+    if ( Ivy_ObjFanin0(pTemp) == pObj )
+        return &pTemp->pPrevFan0;
+    assert( Ivy_ObjFanin1(pTemp) == pObj );
+    return &pTemp->pPrevFan1;
+}
+
+// iterator through the fanouts of the node
+#define Ivy_ObjForEachFanoutInt( pObj, pFanout )                 \
+    for ( pFanout = (pObj)->pFanout; pFanout;                    \
+          pFanout = Ivy_ObjNextFanout(pObj, pFanout) )
+
+// safe iterator through the fanouts of the node
+#define Ivy_ObjForEachFanoutIntSafe( pObj, pFanout, pFanout2 )   \
+    for ( pFanout  = (pObj)->pFanout,                            \
+          pFanout2 = Ivy_ObjNextFanout(pObj, pFanout);           \
+          pFanout;                                               \
+          pFanout  = pFanout2,                                   \
+          pFanout2 = Ivy_ObjNextFanout(pObj, pFanout) )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -47,8 +134,8 @@ void Ivy_ManStartFanout( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj;
     int i;
-    assert( p->vFanouts == NULL );
-    p->vFanouts = Vec_PtrStart( Ivy_ManObjIdMax(p) + 1000 );
+    assert( !p->fFanout );
+    p->fFanout = 1;
     Ivy_ManForEachObj( p, pObj, i )
     {
         if ( Ivy_ObjFanin0(pObj) )
@@ -71,14 +158,12 @@ void Ivy_ManStartFanout( Ivy_Man_t * p )
 ***********************************************************************/
 void Ivy_ManStopFanout( Ivy_Man_t * p )
 {
-    void * pTemp;
+    Ivy_Obj_t * pObj;
     int i;
-    assert( p->vFanouts != NULL );
-    Vec_PtrForEachEntry( p->vFanouts, pTemp, i )
-        if ( Ivy_FanoutIsArray(pTemp) )
-            Vec_PtrFree( Ivy_FanoutGetArray(pTemp) );
-    Vec_PtrFree( p->vFanouts );
-    p->vFanouts = NULL;
+    assert( p->fFanout );
+    p->fFanout = 0;
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
 }
 
 /**Function*************************************************************
@@ -92,31 +177,15 @@ void Ivy_ManStopFanout( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout )
 {
-    Vec_Ptr_t * vNodes;
-    void ** ppSpot;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    // get the pointer to the place where fanouts are stored
-    ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
-    // consider several cases
-    if ( *ppSpot == NULL ) // no fanout - add one fanout
-        *ppSpot = pFanout;
-    else if ( Ivy_FanoutIsArray(*ppSpot) ) // array of fanouts - add one fanout
+    assert( p->fFanout );
+    if ( pFanin->pFanout )
     {
-        vNodes = Ivy_FanoutGetArray(*ppSpot);
-        Vec_PtrPush( vNodes, pFanout );
-    }
-    else // only one fanout - create array and put both fanouts into the array
-    {
-        vNodes = Vec_PtrAlloc( 4 );
-        Vec_PtrPush( vNodes, *ppSpot );
-        Vec_PtrPush( vNodes, pFanout );
-        *ppSpot = Ivy_FanoutSetArray( vNodes );
+        *Ivy_ObjNextFanoutPlace(pFanin, pFanout) = pFanin->pFanout;
+        *Ivy_ObjPrevFanoutPlace(pFanin, pFanin->pFanout) = pFanout;
     }
+    pFanin->pFanout = pFanout;
 }
 
 /**Function*************************************************************
@@ -130,30 +199,25 @@ void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
+void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanout )
 {
-    Vec_Ptr_t * vNodes;
-    void ** ppSpot;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
-    if ( *ppSpot == NULL ) // no fanout - should not happen
-    {
-        assert( 0 );
-    }
-    else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - delete the fanout
-    {
-        vNodes = Ivy_FanoutGetArray(*ppSpot);
-        Vec_PtrRemove( vNodes, pFanout );
-    }
-    else // only one fanout - delete the fanout
-    {
-        assert( *ppSpot == pFanout );
-        *ppSpot = NULL;
-    }
-//    printf( " %d", Ivy_ObjFanoutNum(p, pObj) );
+    Ivy_Obj_t ** ppPlace1, ** ppPlace2, ** ppPlaceN;
+    assert( pFanin->pFanout != NULL );
+
+    ppPlace1 = Ivy_ObjNextFanoutPlace(pFanin, pFanout);
+    ppPlaceN = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanout);
+    assert( *ppPlaceN == pFanout );
+    if ( ppPlaceN )
+        *ppPlaceN = *ppPlace1;
+
+    ppPlace2 = Ivy_ObjPrevFanoutPlace(pFanin, pFanout);
+    ppPlaceN = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanout);
+    assert( ppPlaceN == NULL || *ppPlaceN == pFanout );
+    if ( ppPlaceN )
+        *ppPlaceN = *ppPlace2;
+
+    *ppPlace1 = NULL;
+    *ppPlace2 = NULL;
 }
 
 /**Function*************************************************************
@@ -167,32 +231,18 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew )
+void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pFanin, Ivy_Obj_t * pFanoutOld, Ivy_Obj_t * pFanoutNew )
 {
-    Vec_Ptr_t * vNodes;
-    void ** ppSpot;
-    int Index;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    ppSpot = Vec_PtrEntryP( p->vFanouts, pObj->Id );
-    if ( *ppSpot == NULL ) // no fanout - should not happen
-    {
-        assert( 0 );
-    }
-    else if ( Ivy_FanoutIsArray(*ppSpot) ) // the array of fanouts - find and replace the fanout
-    {
-        vNodes = Ivy_FanoutGetArray(*ppSpot);
-        Index = Vec_PtrFind( vNodes, pFanoutOld );
-        assert( Index >= 0 );
-        Vec_PtrWriteEntry( vNodes, Index, pFanoutNew );
-    }
-    else // only one fanout - delete the fanout
-    {
-        assert( *ppSpot == pFanoutOld );
-        *ppSpot = pFanoutNew;
-    }
+    Ivy_Obj_t ** ppPlace;
+    ppPlace = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanoutOld);
+    assert( *ppPlace == pFanoutOld );
+    if ( ppPlace )
+        *ppPlace = pFanoutNew;
+    ppPlace = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanoutOld);
+    assert( ppPlace == NULL || *ppPlace == pFanoutOld );
+    if ( ppPlace )
+        *ppPlace = pFanoutNew;
+    // assuming that pFanoutNew already points to the next fanout
 }
 
 /**Function*************************************************************
@@ -208,52 +258,12 @@ void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanoutOld
 ***********************************************************************/
 void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray )
 {
-    Vec_Ptr_t * vNodes;
-    Ivy_Obj_t * pTemp;
-    int i;
-    assert( p->vFanouts != NULL );
+    Ivy_Obj_t * pFanout;
+    assert( p->fFanout );
     assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
-    // clean the resulting array
     Vec_PtrClear( vArray );
-    if ( vNodes == NULL ) // no fanout - nothing to do
-    {
-    }
-    else if ( Ivy_FanoutIsArray(vNodes) ) // the array of fanouts - copy fanouts
-    {
-        vNodes = Ivy_FanoutGetArray(vNodes);
-        Vec_PtrForEachEntry( vNodes, pTemp, i )
-            Vec_PtrPush( vArray, pTemp );
-    }
-    else // only one fanout - add the fanout
-        Vec_PtrPush( vArray, vNodes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads one fanout.]
-
-  Description [Returns fanout if there is only one fanout.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
-{
-    Vec_Ptr_t * vNodes;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
-    // clean the resulting array
-    if ( vNodes && !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
-        return (Ivy_Obj_t *)vNodes;
-    return NULL;
+    Ivy_ObjForEachFanoutInt( pObj, pFanout )
+        Vec_PtrPush( vArray, pFanout );
 }
 
 /**Function*************************************************************
@@ -269,18 +279,7 @@ Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 ***********************************************************************/
 Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Vec_Ptr_t * vNodes;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
-    // clean the resulting array
-    if ( vNodes == NULL )
-        return NULL;
-    if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
-        return (Ivy_Obj_t *)vNodes;
-    return Vec_PtrEntry( Ivy_FanoutGetArray(vNodes), 0 );
+    return pObj->pFanout;
 }
 
 /**Function*************************************************************
@@ -296,21 +295,13 @@ Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 ***********************************************************************/
 int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Vec_Ptr_t * vNodes;
-    assert( p->vFanouts != NULL );
-    assert( !Ivy_IsComplement(pObj) );
-    // extend the fanout array if needed
-    Vec_PtrFillExtra( p->vFanouts, pObj->Id + 1, NULL );
-    vNodes = Vec_PtrEntry( p->vFanouts, pObj->Id );
-    // clean the resulting array
-    if ( vNodes == NULL )
-        return 0;
-    if ( !Ivy_FanoutIsArray(vNodes) ) // only one fanout - return
-        return 1;
-    return Vec_PtrSize( Ivy_FanoutGetArray(vNodes) );
+    Ivy_Obj_t * pFanout;
+    int Counter = 0;
+    Ivy_ObjForEachFanoutInt( pObj, pFanout )
+        Counter++;
+    return Counter;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c
index 2d0101a7..1a4fce25 100644
--- a/src/temp/ivy/ivyIsop.c
+++ b/src/temp/ivy/ivyIsop.c
@@ -25,6 +25,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// ISOP computation fails if intermediate memory usage exceed this limit
+#define IVY_ISOP_MEM_LIMIT  4096
+
+// intermediate ISOP representation
 typedef struct Ivy_Sop_t_ Ivy_Sop_t;
 struct Ivy_Sop_t_
 {
@@ -32,10 +36,9 @@ struct Ivy_Sop_t_
     int        nCubes;
 };
 
-static Mem_Flex_t * s_Man = NULL;
-
-static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes );
-static unsigned   Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+// static procedures to compute ISOP
+static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
+static unsigned   Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -43,111 +46,60 @@ static unsigned   Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, I
 
 /**Function*************************************************************
 
-  Synopsis    [Deallocates memory used for computing ISOPs from TTs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_TruthManStop()
-{
-    Mem_FlexStop( s_Man, 0 );
-    s_Man = NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes ISOP from TT.]
 
-  Description []
+  Description [Returns the cover in vCover. Uses the rest of array in vCover
+  as an intermediate memory storage. Returns the cover with -1 cubes, if the
+  the computation exceeded the memory limit (IVY_ISOP_MEM_LIMIT words of
+  intermediate data).]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
+int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth )
 {
     Ivy_Sop_t cRes, * pcRes = &cRes;
+    Ivy_Sop_t cRes2, * pcRes2 = &cRes2;
     unsigned * pResult;
-    int i;
+    int RetValue = 0;
     assert( nVars >= 0 && nVars < 16 );
     // if nVars < 5, make sure it does not depend on those vars
-    for ( i = nVars; i < 5; i++ )
-        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
+//    for ( i = nVars; i < 5; i++ )
+//        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
     // prepare memory manager
-    if ( s_Man == NULL )
-        s_Man = Mem_FlexStart();
-    else
-        Mem_FlexRestart( s_Man );
-    // compute ISOP
-    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
-//    Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
-//    Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
-    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
-//printf( "%d ", pcRes->nCubes );
-    // copy the truth table
     Vec_IntClear( vCover );
-    for ( i = 0; i < pcRes->nCubes; i++ )
-        Vec_IntPush( vCover, pcRes->pCubes[i] );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes ISOP from TT.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
-{
-    Ivy_Sop_t cRes, * pcRes = &cRes;
-    unsigned * pResult;
-    int i;
-    assert( nVars >= 0 && nVars < 16 );
-    // if nVars < 5, make sure it does not depend on those vars
-    for ( i = nVars; i < 5; i++ )
-        assert( !Extra_TruthVarInSupport(puTruth, 5, i) );
-    // prepare memory manager
-    if ( s_Man == NULL )
-        s_Man = Mem_FlexStart();
-    else
-        Mem_FlexRestart( s_Man );
-    // compute ISOP
-    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
-//    Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" );
-//    Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" );
-    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-//printf( "%d ", Mem_FlexReadMemUsage(s_Man) );
-//printf( "%d ", pcRes->nCubes );
-    // copy the truth table
-    Vec_IntClear( vCover );
-    for ( i = 0; i < pcRes->nCubes; i++ )
-        Vec_IntPush( vCover, pcRes->pCubes[i] );
-
-    // try other polarity
-    Mem_FlexRestart( s_Man );
-    Extra_TruthNot( puTruth, puTruth, nVars );
-    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes );
-    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
-    Extra_TruthNot( puTruth, puTruth, nVars );
-    if ( Vec_IntSize(vCover) < pcRes->nCubes )
+    Vec_IntGrow( vCover, IVY_ISOP_MEM_LIMIT );
+    // compute ISOP for the direct polarity
+    pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vCover );
+    if ( pcRes->nCubes == -1 )
+    {
+        vCover->nSize = -1;
         return 0;
-
-    // copy the truth table
-    Vec_IntClear( vCover );
-    for ( i = 0; i < pcRes->nCubes; i++ )
-        Vec_IntPush( vCover, pcRes->pCubes[i] );
-    return 1;
+    }
+    assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+    if ( fTryBoth )
+    {
+        // compute ISOP for the complemented polarity
+        Extra_TruthNot( puTruth, puTruth, nVars );
+        pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vCover );
+        if ( pcRes2->nCubes >= 0 )
+        {
+            assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) );
+            if ( pcRes->nCubes > pcRes2->nCubes )
+            {
+                RetValue = 1;
+                pcRes = pcRes2;
+            }
+        }
+        Extra_TruthNot( puTruth, puTruth, nVars );
+    }
+//    printf( "%d ", vCover->nSize );
+    // move the cover representation to the beginning of the memory buffer
+    memmove( vCover->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
+    Vec_IntShrink( vCover, pcRes->nCubes );
+    return RetValue;
 }
 
 /**Function*************************************************************
@@ -161,17 +113,22 @@ int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes )
+unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
 {
     Ivy_Sop_t cRes0, cRes1, cRes2;
     Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
     unsigned * puRes0, * puRes1, * puRes2;
     unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
     int i, k, Var, nWords, nWordsAll;
-    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+//    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
     // allocate room for the resulting truth table
     nWordsAll = Extra_TruthWordNum( nVars );
-    pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll );
+    pTemp = Vec_IntFetch( vStore, nWordsAll );
+    if ( pTemp == NULL )
+    {
+        pcRes->nCubes = -1;
+        return NULL;
+    }
     // check for constants
     if ( Extra_TruthIsConst0( puOn, nVars ) )
     {
@@ -183,7 +140,12 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
     if ( Extra_TruthIsConst1( puOnDc, nVars ) )
     {
         pcRes->nCubes = 1;
-        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
+        if ( pcRes->pCubes == NULL )
+        {
+            pcRes->nCubes = -1;
+            return NULL;
+        }
         pcRes->pCubes[0] = 0;
         Extra_TruthFill( pTemp, nVars );
         return pTemp;
@@ -198,7 +160,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
     // consider a simple case when one-word computation can be used
     if ( Var < 5 )
     {
-        unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes );
+        unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
         for ( i = 0; i < nWordsAll; i++ )
             pTemp[i] = uRes;
         return pTemp;
@@ -211,17 +173,37 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
     pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
     // solve for cofactors
     Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
-    puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 );
+    puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
+    if ( pcRes0->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return NULL;
+    }
     Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
-    puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 );
+    puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
+    if ( pcRes1->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return NULL;
+    }
     Extra_TruthSharp( pTemp0, puOn0, puRes0, Var );
     Extra_TruthSharp( pTemp1, puOn1, puRes1, Var );
     Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var );
     Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
-    puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 );
+    puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
+    if ( pcRes2->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return NULL;
+    }
     // create the resulting cover
     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
-    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
+    if ( pcRes->pCubes == NULL )
+    {
+        pcRes->nCubes = -1;
+        return NULL;
+    }
     k = 0;
     for ( i = 0; i < pcRes0->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
@@ -255,7 +237,7 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes )
+unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes, Vec_Int_t * vStore )
 {
     unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
     Ivy_Sop_t cRes0, cRes1, cRes2;
@@ -273,7 +255,12 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
     if ( uOnDc == 0xFFFFFFFF )
     {
         pcRes->nCubes = 1;
-        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
+        if ( pcRes->pCubes == NULL )
+        {
+            pcRes->nCubes = -1;
+            return 0;
+        }
         pcRes->pCubes[0] = 0;
         return 0xFFFFFFFF;
     }
@@ -292,12 +279,32 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t
     Extra_TruthCofactor0( &uOnDc0, Var + 1, Var );
     Extra_TruthCofactor1( &uOnDc1, Var + 1, Var );
     // solve for cofactors
-    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 );
-    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 );
-    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 );
+    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
+    if ( pcRes0->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return 0;
+    }
+    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
+    if ( pcRes1->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return 0;
+    }
+    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
+    if ( pcRes2->nCubes == -1 )
+    {
+        pcRes->nCubes = -1;
+        return 0;
+    }
     // create the resulting cover
     pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
-    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
+    if ( pcRes->pCubes == NULL )
+    {
+        pcRes->nCubes = -1;
+        return 0;
+    }
     k = 0;
     for ( i = 0; i < pcRes0->nCubes; i++ )
         pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index c5b66ad0..9839567f 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -82,7 +82,7 @@ Ivy_Man_t * Ivy_ManStart()
 void Ivy_ManStop( Ivy_Man_t * p )
 {
 //    Ivy_TableProfile( p );
-    if ( p->vFanouts )  Ivy_ManStopFanout( p );
+//    if ( p->vFanouts )  Ivy_ManStopFanout( p );
     if ( p->vChunks )   Ivy_ManStopMemory( p );
     if ( p->vRequired ) Vec_IntFree( p->vRequired );
     if ( p->vPis )      Vec_PtrFree( p->vPis );
@@ -156,14 +156,14 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel )
 void Ivy_ManPrintStats( Ivy_Man_t * p )
 {
     printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
-    printf( "A = %d. ",       Ivy_ManAndNum(p) );
-    printf( "L = %d. ",       Ivy_ManLatchNum(p) );
+    printf( "A = %7d. ",       Ivy_ManAndNum(p) );
+    printf( "L = %5d. ",       Ivy_ManLatchNum(p) );
 //    printf( "X = %d. ",       Ivy_ManExorNum(p) );
-    printf( "B = %d. ",       Ivy_ManBufNum(p) );
-    printf( "MaxID = %d. ",   Ivy_ManObjIdMax(p) );
+//    printf( "B = %3d. ",       Ivy_ManBufNum(p) );
+    printf( "MaxID = %7d. ",   Ivy_ManObjIdMax(p) );
 //    printf( "Cre = %d. ",     p->nCreated );
 //    printf( "Del = %d. ",     p->nDeleted );
-    printf( "Lev = %d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
+    printf( "Lev = %3d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
     printf( "\n" );
 }
 
@@ -190,7 +190,7 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
     assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) );
     assert( Vec_PtrSize( p->vBufs ) == 0 );
     // create fanouts
-    if ( p->vFanouts == NULL )
+    if ( p->fFanout == 0 )
         Ivy_ManStartFanout( p );
     // collect the POs to be converted into latches
     for ( i = 0; i < nLatches; i++ )
diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c
index 01833f03..6ca33541 100644
--- a/src/temp/ivy/ivyMem.c
+++ b/src/temp/ivy/ivyMem.c
@@ -87,15 +87,15 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
 {
     char * pMemory;
     int i, nBytes;
-    assert( sizeof(Ivy_Obj_t) <= 32 );
+    assert( sizeof(Ivy_Obj_t) <= 64 );
     assert( p->pListFree == NULL );
     assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
     // allocate new memory page
-    nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 32;
+    nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
     pMemory = ALLOC( char, nBytes );
     Vec_PtrPush( p->vChunks, pMemory );
     // align memory at the 32-byte boundary
-    pMemory = pMemory + 32 - (((int)pMemory) & 31);
+    pMemory = pMemory + 64 - (((int)pMemory) & 63);
     // remember the manager in the first entry
     Vec_PtrPush( p->vPages, pMemory );
     // break the memory down into nodes
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 735d79c3..3122c8c8 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -79,6 +79,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     assert( Ivy_TableLookup(p, pGhost) == NULL );
     // get memory for the new object
     pObj = Ivy_ManFetchMemory( p );
+//printf( "Reusing %p.\n", pObj );
     assert( Ivy_ObjIsNone(pObj) );
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
@@ -139,13 +140,13 @@ void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj
     if ( Ivy_ObjFanin0(pObj) != NULL )
     {
         Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
-        if ( p->vFanouts )
+        if ( p->fFanout )
             Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
     }
     if ( Ivy_ObjFanin1(pObj) != NULL )
     {
         Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
-        if ( p->vFanouts )
+        if ( p->fFanout )
             Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
     }
     // add the node to the structural hash table
@@ -168,23 +169,29 @@ void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
     assert( !Ivy_IsComplement(pObj) );
     assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL );
     // remove connections
-    if ( Ivy_ObjFanin0(pObj) != NULL )
+    if ( pObj->pFanin0 != NULL )
     {
         Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
-        if ( p->vFanouts )
+        if ( p->fFanout )
             Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj );
     }
-    if ( Ivy_ObjFanin1(pObj) != NULL )
+    if ( pObj->pFanin1 != NULL )
     {
         Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
-        if ( p->vFanouts )
+        if ( p->fFanout )
             Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj );
     }
+    assert( pObj->pNextFan0 == NULL );
+    assert( pObj->pNextFan1 == NULL );
+    assert( pObj->pPrevFan0 == NULL );
+    assert( pObj->pPrevFan1 == NULL );
     // remove the node from the structural hash table
     Ivy_TableDelete( p, pObj );
     // add the first fanin
     pObj->pFanin0 = NULL;
     pObj->pFanin1 = NULL;
+
+//    Ivy_ManCheckFanouts( p );
 }
 
 /**Function*************************************************************
@@ -205,14 +212,14 @@ void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew
     pFaninOld = Ivy_ObjFanin0(pObj);
     // decrement ref and remove fanout
     Ivy_ObjRefsDec( pFaninOld );
-    if ( p->vFanouts )
+    if ( p->fFanout )
         Ivy_ObjDeleteFanout( p, pFaninOld, pObj );
+    // update the fanin
+    pObj->pFanin0 = pFaninNew;
     // increment ref and add fanout
     Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) );
-    if ( p->vFanouts )
+    if ( p->fFanout )
         Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj );
-    // update the fanin
-    pObj->pFanin0 = pFaninNew;
     // get rid of old fanin
     if ( !Ivy_ObjIsPi(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 )
         Ivy_ObjDelete_rec( p, pFaninOld, 1 );
@@ -243,7 +250,7 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
         Vec_PtrRemove( p->vPis, pObj );
     else if ( Ivy_ObjIsPo(pObj) )
         Vec_PtrRemove( p->vPos, pObj );
-    else if ( p->vFanouts && Ivy_ObjIsBuf(pObj) )
+    else if ( p->fFanout && Ivy_ObjIsBuf(pObj) )
         Vec_PtrRemove( p->vBufs, pObj );
     // clean and recycle the entry
     if ( fFreeTop )
@@ -251,11 +258,14 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
         // free the node
         Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
         Ivy_ManRecycleMemory( p, pObj );
+//printf( "Recycling after delete %p.\n", pObj );
     }
     else
     {
         int nRefsOld = pObj->nRefs;
+        Ivy_Obj_t * pFanout = pObj->pFanout;
         Ivy_ObjClean( pObj );
+        pObj->pFanout = pFanout;
         pObj->nRefs = nRefsOld;
     }
 }
@@ -318,7 +328,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     if ( fUpdateLevel )
     {
         // if the new node's arrival time is different, recursively update arrival time of the fanouts
-        if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
+        if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
         {
             assert( Ivy_ObjIsNode(pObjOld) );
             pObjOld->Level = pObjNew->Level;
@@ -338,16 +348,23 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     // delete the old object
     if ( fDeleteOld )
         Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
-    // make sure object is pointing to itself
+    // make sure object is not pointing to itself
     assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) );
     assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) );
+    // make sure the old node has no fanin fanout pointers
+    if ( p->fFanout )
+    {
+        assert( pObjOld->pFanout != NULL );
+        assert( pObjNew->pFanout == NULL );
+        pObjNew->pFanout = pObjOld->pFanout;
+    }
     // transfer the old object
     assert( Ivy_ObjRefs(pObjNew) == 0 );
     nRefsOld = pObjOld->nRefs;  
     Ivy_ObjOverwrite( pObjOld, pObjNew );
     pObjOld->nRefs = nRefsOld;
     // patch the fanout of the fanins 
-    if ( p->vFanouts )
+    if ( p->fFanout )
     {
         Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld );
         if ( Ivy_ObjFanin1(pObjOld) )
@@ -358,9 +375,12 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     // recycle the object that was taken over by pObjOld
     Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
     Ivy_ManRecycleMemory( p, pObjNew );
+//printf( "Recycling after patch %p.\n", pObjNew );
     // if the new node is the buffer propagate it
-    if ( p->vFanouts && Ivy_ObjIsBuf(pObjOld) )
+    if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
         Vec_PtrPush( p->vBufs, pObjOld );
+//    Ivy_ManCheckFanouts( p );
+//    printf( "\n" );
 }
 
 /**Function*************************************************************
@@ -385,6 +405,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel
             return;
         pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
         Ivy_ObjPatchFanin0( p, pNode, pFanReal0 );
+//        Ivy_ManCheckFanouts( p );
         return;
     }
     if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
index 804bdfb4..b2e4a4dd 100644
--- a/src/temp/ivy/ivyResyn.c
+++ b/src/temp/ivy/ivyResyn.c
@@ -39,6 +39,47 @@
   SeeAlso     []
 
 ***********************************************************************/
+Ivy_Man_t * Ivy_ManResyn0( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
+{
+    int clk;
+    Ivy_Man_t * pTemp;
+
+if ( fVerbose ) { printf( "Original:\n" ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Ivy_ManBalance( pMan, fUpdateLevel );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+//    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
+clk = clock();
+    Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+    Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs several passes of rewriting on the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
     int clk;
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
index 537b64ff..64331579 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -61,7 +61,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
     if ( pManRwt == NULL )
         return 0; 
     // create fanouts
-    if ( fUpdateLevel && p->vFanouts == NULL )
+    if ( fUpdateLevel && p->fFanout == 0 )
         Ivy_ManStartFanout( p );
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 8fd1b63b..7cf55b69 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -64,7 +64,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     if ( pManRwt == NULL )
         return 0; 
     // create fanouts
-    if ( p->vFanouts == NULL )
+    if ( p->fFanout == 0 )
         Ivy_ManStartFanout( p );
     // resynthesize each node once
     nNodes = Ivy_ManObjIdMax(p);
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 77a55a39..a23e76c9 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -381,7 +381,7 @@ void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
     Ivy_Obj_t * pFanout;
     Vec_Ptr_t * vFanouts;
     int i, LevelNew;
-    assert( p->vFanouts );
+    assert( p->fFanout );
     assert( Ivy_ObjIsNode(pObj) );
     vFanouts = Vec_PtrAlloc( 10 );
     Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
@@ -416,7 +416,7 @@ int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
     Ivy_Obj_t * pFanout;
     Vec_Ptr_t * vFanouts;
     int i, Required, LevelNew = 1000000;
-    assert( p->vFanouts && p->vRequired );
+    assert( p->fFanout && p->vRequired );
     vFanouts = Vec_PtrAlloc( 10 );
     Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
     {
diff --git a/src/temp/player/player.h b/src/temp/player/player.h
index b0bb0ec4..0213683f 100644
--- a/src/temp/player/player.h
+++ b/src/temp/player/player.h
@@ -86,13 +86,14 @@ static inline Pla_Obj_t *   Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj )  {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== playerToAbc.c ==============================================================*/
-extern void *        Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
+extern void *        Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
 /*=== playerCore.c =============================================================*/
 extern Pla_Man_t *   Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
 /*=== playerFast.c =============================================================*/
 extern void          Pla_ManFastLutMap( Ivy_Man_t * pAig, int nLimit );
 extern void          Pla_ManFastLutMapStop( Ivy_Man_t * pAig );
 extern void          Pla_ManFastLutMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
+extern void          Pla_ManFastLutMapReverseLevel( Ivy_Man_t * pAig );
 /*=== playerMan.c ==============================================================*/
 extern Pla_Man_t *   Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax );
 extern void          Pla_ManFree( Pla_Man_t * p );
diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c
index 1196d242..78b20718 100644
--- a/src/temp/player/playerMan.c
+++ b/src/temp/player/playerMan.c
@@ -40,7 +40,7 @@
 
 ***********************************************************************/
 Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax )
-{
+{ 
     Pla_Man_t * pMan;
     assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128)  );
     // start the manager
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index fc5e01ea..91994ca6 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -50,9 +50,8 @@ static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose )
+void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose )
 {
-    int fUseRewriting = 0;
     Pla_Man_t * p;
     Ivy_Man_t * pMan, * pManExt;
     Abc_Ntk_t * pNtkNew;
@@ -69,7 +68,15 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
     }
     if ( fVerbose )
         Ivy_ManPrintStats( pMan );
-    if ( fUseRewriting )
+    if ( fRewriting )
+    {
+        // simplify
+        pMan = Ivy_ManResyn0( pManExt = pMan, 1, 0 );
+        Ivy_ManStop( pManExt );
+        if ( fVerbose )
+            Ivy_ManPrintStats( pMan );
+    }
+    if ( fSynthesis )
     {
         // simplify
         pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
@@ -261,9 +268,16 @@ Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t *
             pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
             pObjAbc = Abc_NodeCreateConst0( pNtkNew );  
         }
+        else if ( Extra_TruthIsConst1(puTruth, 8) )
+        {
+            pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
+            pObjAbc = Abc_NodeCreateConst1( pNtkNew );  
+        }
         else
         {
-            int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+            int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
+            if ( vNodes->nSize == -1 )
+                printf( "Ivy_ManToAbc_rec(): Internal error.\n" );
             pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
             if ( fCompl ) Abc_SopComplement(pObjAbc->pData); 
 //            printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) );
@@ -372,9 +386,16 @@ Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj
         pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
         pObjAbc = Abc_NodeCreateConst0( pNtkNew );  
     }
+    else if ( Extra_TruthIsConst1(puTruth, 8) )
+    {
+        pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL );
+        pObjAbc = Abc_NodeCreateConst1( pNtkNew );  
+    }
     else
     {
-        int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes );
+        int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 );
+        if ( vNodes->nSize == -1 )
+            printf( "Ivy_ManToAbcFast_rec(): Internal error.\n" );
         pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes );
         if ( fCompl ) Abc_SopComplement(pObjAbc->pData); 
     }
@@ -444,32 +465,48 @@ static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost )
 int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
 {
     Abc_Obj_t * pObj;
-    int nFanins, nLevels, * pLevelCosts, CostTotal, nRanksTotal, i; 
+    int * pLevelCosts, * pLevelCostsR;
+    int nFanins, nLevels, LevelR, Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR, i; 
+    // compute the reverse levels
+    Abc_NtkStartReverseLevels( pNtk );
     // compute the costs for each level
     nLevels = Abc_NtkGetLevelNum( pNtk );
-    pLevelCosts = ALLOC( int, nLevels + 1 );
-    memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) );
+    pLevelCosts  = ALLOC( int, nLevels + 1 );
+    pLevelCostsR = ALLOC( int, nLevels + 1 );
+    memset( pLevelCosts,  0, sizeof(int) * (nLevels + 1) );
+    memset( pLevelCostsR, 0, sizeof(int) * (nLevels + 1) );
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         nFanins = Abc_ObjFaninNum(pObj);
         if ( nFanins == 0 )
             continue;
-        pLevelCosts[ pObj->Level ] += Abc_NodePlayerCost( nFanins );
+        Cost = Abc_NodePlayerCost( nFanins );
+        LevelR = Vec_IntEntry( pNtk->vLevelsR, pObj->Id );
+        pLevelCosts[ pObj->Level ] += Cost;
+        pLevelCostsR[ LevelR ] += Cost;
     }
     // compute the total cost
-    CostTotal = nRanksTotal = 0;
-    for ( i = 1; i <= nLevels; i++ )
+    CostTotal = CostTotalR = nRanksTotal = nRanksTotalR = 0;
+    for ( i = 0; i <= nLevels; i++ )
     {
-        CostTotal   += pLevelCosts[i];
-        nRanksTotal += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
+        CostTotal    += pLevelCosts[i];
+        CostTotalR   += pLevelCostsR[i];
+        nRanksTotal  += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
+        nRanksTotalR += Abc_NtkPlayerCostOne( pLevelCostsR[i], RankCost );
     }
+    assert( CostTotal == CostTotalR );
     // print out statistics
     if ( fVerbose )
     {
         for ( i = 1; i <= nLevels; i++ )
-            printf( "Level %2d : Cost = %6d. Ranks = %6.3f.\n", i, pLevelCosts[i], ((double)pLevelCosts[i])/RankCost );
-        printf( "TOTAL    : Cost = %6d. Ranks = %3d.\n", CostTotal, nRanksTotal );
+            printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i, 
+            pLevelCosts[i], ((double)pLevelCosts[i])/RankCost, 
+            pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost );
+        printf( "TOTAL    : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n", 
+            CostTotal, nRanksTotal, nRanksTotalR, nLevels );
     }
+    free( pLevelCosts );
+    free( pLevelCostsR );
     return nRanksTotal;
 }
 
diff --git a/src/temp/vec/vecInt.h b/src/temp/vec/vecInt.h
index 9db30af7..4a97fc91 100644
--- a/src/temp/vec/vecInt.h
+++ b/src/temp/vec/vecInt.h
@@ -289,23 +289,6 @@ static inline int Vec_IntEntry( Vec_Int_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int * Vec_IntEntryP( Vec_Int_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray + i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
 {
     assert( i >= 0 && i < p->nSize );
@@ -402,10 +385,7 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
     int i;
     if ( p->nSize >= nSize )
         return;
-    if ( p->nSize < 2 * nSize )
-        Vec_IntGrow( p, 2 * nSize );
-    else
-        Vec_IntGrow( p, p->nSize );
+    Vec_IntGrow( p, nSize );
     for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
     p->nSize = nSize;
@@ -603,6 +583,28 @@ static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the pointer to the next nWords entries in the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
+{
+    p->nSize += nWords;
+    if ( p->nSize > p->nCap )
+    {
+//         Vec_IntGrow( p, 2 * p->nSize );
+        return NULL;
+    }
+    return ((unsigned *)p->pArray) + p->nSize - nWords;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the last entry and removes it from the list.]
 
   Description []
diff --git a/src/temp/vec/vecPtr.h b/src/temp/vec/vecPtr.h
index 96975ff0..07ac0f17 100644
--- a/src/temp/vec/vecPtr.h
+++ b/src/temp/vec/vecPtr.h
@@ -293,6 +293,23 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
 {
     assert( i >= 0 && i < p->nSize );
@@ -371,7 +388,10 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
     int i;
     if ( p->nSize >= nSize )
         return;
-    Vec_PtrGrow( p, nSize );
+    if ( p->nSize < 2 * nSize )
+        Vec_PtrGrow( p, 2 * nSize );
+    else
+        Vec_PtrGrow( p, p->nSize );
     for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
     p->nSize = nSize;
@@ -505,10 +525,18 @@ static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
 static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
 {
     int i;
+    // delete assuming that it is closer to the end
+    for ( i = p->nSize - 1; i >= 0; i-- )
+        if ( p->pArray[i] == Entry )
+            break;
+    assert( i >= 0 );
+/*
+    // delete assuming that it is closer to the beginning
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == Entry )
             break;
     assert( i < p->nSize );
+*/
     for ( i++; i < p->nSize; i++ )
         p->pArray[i-1] = p->pArray[i];
     p->nSize--;