Version abc60804

13 files changed, 472 insertions, 300 deletions

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 )
     {