Version abc60723

22 files changed, 2172 insertions, 1486 deletions

diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 57d8cfd2..8c5f130b 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -44,23 +44,17 @@ typedef struct Ivy_Man_t_            Ivy_Man_t;
 typedef struct Ivy_Obj_t_            Ivy_Obj_t;
 typedef int                          Ivy_Edge_t;
 
-// constant edges
-#define IVY_CONST0                   1
-#define IVY_CONST1                   0
-
 // object types
 typedef enum { 
-    IVY_NONE,                        // 0: unused node
+    IVY_NONE,                        // 0: non-existant object
     IVY_PI,                          // 1: primary input (and constant 1 node)
     IVY_PO,                          // 2: primary output
     IVY_ASSERT,                      // 3: assertion
     IVY_LATCH,                       // 4: sequential element
-    IVY_AND,                         // 5: internal AND node
-    IVY_EXOR,                        // 6: internal EXOR node
-    IVY_BUF,                         // 7: internal buffer (temporary)
-    IVY_ANDM,                        // 8: multi-input AND (logic network only)
-    IVY_EXORM,                       // 9: multi-input EXOR (logic network only)
-    IVY_LUT                          // 10: multi-input LUT (logic network only)
+    IVY_AND,                         // 5: AND node
+    IVY_EXOR,                        // 6: EXOR node
+    IVY_BUF,                         // 7: buffer (temporary)
+    IVY_VOID                         // 8: unused object
 } Ivy_Type_t;
 
 // latch initial values
@@ -72,56 +66,51 @@ typedef enum {
 } Ivy_Init_t;
 
 // the AIG node
-struct Ivy_Obj_t_  // 6 words
+struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)
 {
     int              Id;             // integer ID
     int              TravId;         // traversal ID
-    int              Fanin0;         // fanin ID
-    int              Fanin1;         // fanin ID
-    int              nRefs;          // reference counter
     unsigned         Type    :  4;   // object type
     unsigned         fPhase  :  1;   // value under 000...0 pattern
     unsigned         fMarkA  :  1;   // multipurpose mask
     unsigned         fMarkB  :  1;   // multipurpose mask
     unsigned         fExFan  :  1;   // set to 1 if last fanout added is EXOR
-    unsigned         fComp0  :  1;   // complemented attribute
-    unsigned         fComp1  :  1;   // complemented attribute
     unsigned         Init    :  2;   // latch initial value
-    unsigned         LevelR  :  8;   // reverse logic level
-    unsigned         Level   : 12;   // logic level
+    unsigned         Level   : 22;   // logic level
+    int              nRefs;          // reference counter
+    Ivy_Obj_t *      pFanin0;        // fanin
+    Ivy_Obj_t *      pFanin1;        // fanin
 };
 
 // the AIG manager
 struct Ivy_Man_t_
 {
     // AIG nodes
-    int              nObjs[12];      // the number of objects by type
+    Vec_Ptr_t *      vPis;           // the array of PIs
+    Vec_Ptr_t *      vPos;           // the array of POs
+    Vec_Ptr_t *      vBufs;          // the array of buffers
+    Vec_Ptr_t *      vObjs;          // the array of objects
+    Ivy_Obj_t *      pConst1;        // the constant 1 node
+    Ivy_Obj_t        Ghost;          // the ghost node
+    // AIG node counters
+    int              nObjs[IVY_VOID];// the number of objects by type
     int              nCreated;       // the number of created objects
     int              nDeleted;       // the number of deleted objects
-    int              ObjIdNext;      // the next free obj ID to assign
-    int              nObjsAlloc;     // the allocated number of nodes
-    Ivy_Obj_t *      pObjs;          // the array of all nodes
-    Vec_Int_t *      vPis;           // the array of PIs
-    Vec_Int_t *      vPos;           // the array of POs
     // stuctural hash table
     int *            pTable;         // structural hash table
     int              nTableSize;     // structural hash table size
     // various data members
     int              fCatchExor;     // set to 1 to detect EXORs
-    int              fExtended;      // set to 1 in extended mode
     int              nTravIds;       // the traversal ID
     int              nLevelMax;      // the maximum level
-    void *           pData;          // the temporary data
     Vec_Int_t *      vRequired;      // required times
-    // truth table of the 8-LUTs
-    unsigned *       pMemory;        // memory for truth tables
-    Vec_Int_t *      vTruths;        // offset for truth table of each node
-    // storage for the undo operation
-    Vec_Int_t *      vFree;          // storage for all deleted entries
-    Ivy_Obj_t *      pUndos;         // description of recently deleted nodes
-    int              nUndos;         // the number of recently deleted nodes
-    int              nUndosAlloc;    // the number of allocated cells
-    int              fRecording;     // shows that recording goes on
+    Vec_Ptr_t *      vFanouts;       // representation of the fanouts
+    void *           pData;          // the temporary data
+    void *           pCopy;          // the temporary data
+    // memory management
+    Vec_Ptr_t *      vChunks;        // allocated memory pieces
+    Vec_Ptr_t *      vPages;         // memory pages used by nodes
+    Ivy_Obj_t *      pListFree;      // the list of free nodes 
 };
 
 
@@ -141,7 +130,9 @@ typedef struct Ivy_Store_t_ Ivy_Store_t;
 struct Ivy_Store_t_
 {
     int         nCuts;
+    int         nCutsM;
     int         nCutsMax;
+    int         fSatur;
     Ivy_Cut_t   pCuts[IVY_CUT_LIMIT]; // storage for cuts
 };
 
@@ -149,35 +140,33 @@ struct Ivy_Store_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-#define IVY_SANDBOX_SIZE   1
-
 #define IVY_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define IVY_MAX(a,b)       (((a) > (b))? (a) : (b))
 
-static inline int          Ivy_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);       }
-static inline int          Ivy_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
-static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;   }
-static inline void         Ivy_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));               }
-static inline void         Ivy_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));               }
-
-static inline Ivy_Obj_t *  Ivy_Regular( Ivy_Obj_t * p )           { return (Ivy_Obj_t *)((unsigned)(p) & ~01);  }
-static inline Ivy_Obj_t *  Ivy_Not( Ivy_Obj_t * p )               { return (Ivy_Obj_t *)((unsigned)(p) ^  01);  }
-static inline Ivy_Obj_t *  Ivy_NotCond( Ivy_Obj_t * p, int c )    { return (Ivy_Obj_t *)((unsigned)(p) ^ (c));  }
-static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int )(((unsigned)p) & 01);          }
-
-static inline Ivy_Obj_t *  Ivy_ManConst0( Ivy_Man_t * p )         { return Ivy_Not(p->pObjs);                   }
-static inline Ivy_Obj_t *  Ivy_ManConst1( Ivy_Man_t * p )         { return p->pObjs;                            }
-static inline Ivy_Obj_t *  Ivy_ManGhost( Ivy_Man_t * p )          { return p->pObjs - IVY_SANDBOX_SIZE;         }
-static inline Ivy_Obj_t *  Ivy_ManPi( Ivy_Man_t * p, int i )      { return p->pObjs + Vec_IntEntry(p->vPis,i);  }
-static inline Ivy_Obj_t *  Ivy_ManPo( Ivy_Man_t * p, int i )      { return p->pObjs + Vec_IntEntry(p->vPos,i);  }
-static inline Ivy_Obj_t *  Ivy_ManObj( Ivy_Man_t * p, int i )     { return p->pObjs + i;                        }
-
-static inline Ivy_Edge_t   Ivy_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;                  }
-static inline int          Ivy_EdgeId( Ivy_Edge_t Edge )                   { return Edge >> 1;                           }
-static inline int          Ivy_EdgeIsComplement( Ivy_Edge_t Edge )         { return Edge & 1;                            }
-static inline Ivy_Edge_t   Ivy_EdgeRegular( Ivy_Edge_t Edge )              { return (Edge >> 1) << 1;                    }
-static inline Ivy_Edge_t   Ivy_EdgeNot( Ivy_Edge_t Edge )                  { return Edge ^ 1;                            }
-static inline Ivy_Edge_t   Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond )   { return Edge ^ fCond;                        }
+static inline int          Ivy_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);           }
+static inline int          Ivy_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }
+static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
+static inline void         Ivy_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
+static inline void         Ivy_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
+
+static inline Ivy_Obj_t *  Ivy_Regular( Ivy_Obj_t * p )           { return (Ivy_Obj_t *)((unsigned)(p) & ~01);      }
+static inline Ivy_Obj_t *  Ivy_Not( Ivy_Obj_t * p )               { return (Ivy_Obj_t *)((unsigned)(p) ^  01);      }
+static inline Ivy_Obj_t *  Ivy_NotCond( Ivy_Obj_t * p, int c )    { return (Ivy_Obj_t *)((unsigned)(p) ^ (c));      }
+static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int )(((unsigned)p) & 01);              }
+
+static inline Ivy_Obj_t *  Ivy_ManConst0( Ivy_Man_t * p )         { return Ivy_Not(p->pConst1);                     }
+static inline Ivy_Obj_t *  Ivy_ManConst1( Ivy_Man_t * p )         { return p->pConst1;                              }
+static inline Ivy_Obj_t *  Ivy_ManGhost( Ivy_Man_t * p )          { return &p->Ghost;                               }
+static inline Ivy_Obj_t *  Ivy_ManPi( Ivy_Man_t * p, int i )      { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
+static inline Ivy_Obj_t *  Ivy_ManPo( Ivy_Man_t * p, int i )      { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i);   }
+static inline Ivy_Obj_t *  Ivy_ManObj( Ivy_Man_t * p, int i )     { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i);  }
+
+static inline Ivy_Edge_t   Ivy_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;             }
+static inline int          Ivy_EdgeId( Ivy_Edge_t Edge )                   { return Edge >> 1;                      }
+static inline int          Ivy_EdgeIsComplement( Ivy_Edge_t Edge )         { return Edge & 1;                       }
+static inline Ivy_Edge_t   Ivy_EdgeRegular( Ivy_Edge_t Edge )              { return (Edge >> 1) << 1;               }
+static inline Ivy_Edge_t   Ivy_EdgeNot( Ivy_Edge_t Edge )                  { return Edge ^ 1;                       }
+static inline Ivy_Edge_t   Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond )   { return Edge ^ fCond;                   }
 static inline Ivy_Edge_t   Ivy_EdgeFromNode( Ivy_Obj_t * pNode )           { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) );          }
 static inline Ivy_Obj_t *  Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
 
@@ -192,13 +181,9 @@ static inline int          Ivy_ManLatchNum( Ivy_Man_t * p )       { return p->nO
 static inline int          Ivy_ManAndNum( Ivy_Man_t * p )         { return p->nObjs[IVY_AND];                   }
 static inline int          Ivy_ManExorNum( Ivy_Man_t * p )        { return p->nObjs[IVY_EXOR];                  }
 static inline int          Ivy_ManBufNum( Ivy_Man_t * p )         { return p->nObjs[IVY_BUF];                   }
-static inline int          Ivy_ManAndMultiNum( Ivy_Man_t * p )    { return p->nObjs[IVY_ANDM];                  }
-static inline int          Ivy_ManExorMultiNum( Ivy_Man_t * p )   { return p->nObjs[IVY_EXORM];                 }
-static inline int          Ivy_ManLutNum( Ivy_Man_t * p )         { return p->nObjs[IVY_LUT];                   }
 static inline int          Ivy_ManObjNum( Ivy_Man_t * p )         { return p->nCreated - p->nDeleted;           }
-static inline int          Ivy_ManObjIdNext( Ivy_Man_t * p )      { return p->ObjIdNext;                        }
-static inline int          Ivy_ManObjAllocNum( Ivy_Man_t * p )    { return p->nObjsAlloc;                       }
-static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->fExtended? p->nObjs[IVY_ANDM]+p->nObjs[IVY_EXORM]+p->nObjs[IVY_LUT] : p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]; }
+static inline int          Ivy_ManObjIdMax( Ivy_Man_t * p )       { return Vec_PtrSize(p->vObjs)-1;             }
+static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR];}
 static inline int          Ivy_ManHashObjNum( Ivy_Man_t * p )     { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH];     }
 static inline int          Ivy_ManGetCost( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }
 
@@ -221,27 +206,15 @@ static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { assert( !Ivy
 static inline int          Ivy_ObjIsHash( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
 static inline int          Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
 
-static inline int          Ivy_ObjIsAndMulti( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM;   }
-static inline int          Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM;  }
-static inline int          Ivy_ObjIsLut( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LUT;    }
-static inline int          Ivy_ObjIsNodeExt( Ivy_Obj_t * pObj )   { assert( !Ivy_IsComplement(pObj) ); return pObj->Type >= IVY_ANDM;   }
-
 static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA;  }
 static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1;     }
 static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0;     }
-
-static inline Ivy_Man_t *  Ivy_ObjMan( Ivy_Obj_t * pObj )         { assert( !Ivy_IsComplement(pObj) ); return *((Ivy_Man_t **)(pObj - pObj->Id - IVY_SANDBOX_SIZE - 1)); }
-static inline Ivy_Obj_t *  Ivy_ObjConst0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Not(pObj - pObj->Id);           }
-static inline Ivy_Obj_t *  Ivy_ObjConst1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id;                    }
-static inline Ivy_Obj_t *  Ivy_ObjGhost( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id - IVY_SANDBOX_SIZE; }
-static inline Ivy_Obj_t *  Ivy_ObjObj( Ivy_Obj_t * pObj, int n )  { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + n;                }
-static inline Ivy_Obj_t *  Ivy_ObjNext( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + pObj->TravId;     }
  
 static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId;                                              }
-static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds;                          }
-static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds - 1;                      }
-static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds);     }
-static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds - 1); }
+static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds;                          }
+static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds - 1;                      }
+static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds);     }
+static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds - 1); }
 
 static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { assert( !Ivy_IsComplement(pObj) ); return pObj->Id;                               }
 static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase;                           }
@@ -249,69 +222,53 @@ static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { assert( !Ivy
 static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs;                            }
 static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++;                                 }
 static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
-static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin0;                           }
-static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin1;                           }
-static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp0;                           }
-static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp1;                           }
-static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin0);         }
-static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin1);         }
-static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin0(pObj), Ivy_ObjFaninC0(pObj) );   }
-static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) );   }
-static inline int          Ivy_ObjLevelR( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR;                           }
+static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
+static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
+static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin0);        }
+static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin1);        }
+static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin0);             }
+static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin1);             }
+static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0;                          }
+static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1;                          }
 static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Level;                            }
 static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
-static inline void         Ivy_ObjClean( Ivy_Obj_t * pObj )       { 
+static inline void         Ivy_ObjClean( Ivy_Obj_t * pObj )       
+{ 
     int IdSaved = pObj->Id; 
     memset( pObj, 0, sizeof(Ivy_Obj_t) ); 
     pObj->Id = IdSaved; 
 }
-static inline void         Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData )   { int IdSaved = pBase->Id; memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); pBase->Id = IdSaved;         }
+static inline void         Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData )   
+{ 
+    int IdSaved = pBase->Id; 
+    memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); 
+    pBase->Id = IdSaved;         
+}
 static inline int          Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )    
 { 
-    if ( Ivy_ObjFaninId0(pObj) == Ivy_ObjId(pFanin) ) return 0; 
-    if ( Ivy_ObjFaninId1(pObj) == Ivy_ObjId(pFanin) ) return 1; 
+    if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; 
+    if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; 
     assert(0); return -1; 
 }
 static inline int          Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )    
 { 
-    if ( Ivy_ObjFaninId0(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC0(pObj); 
-    if ( Ivy_ObjFaninId1(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC1(pObj); 
+    if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); 
+    if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); 
     assert(0); return -1; 
 }
 
 // create the ghost of the new node
-static inline Ivy_Obj_t *  Ivy_ObjCreateGhost( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )    
+static inline Ivy_Obj_t *  Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )    
 {
-    Ivy_Obj_t * pGhost;
-    int Temp;
-    pGhost = Ivy_ObjGhost(Ivy_Regular(p0));
+    Ivy_Obj_t * pGhost, * pTemp;
+    pGhost = Ivy_ManGhost(p);
     pGhost->Type = Type;
     pGhost->Init = Init;
-    pGhost->fComp0 = Ivy_IsComplement(p0);
-    pGhost->fComp1 = Ivy_IsComplement(p1);
-    pGhost->Fanin0 = Ivy_ObjId(Ivy_Regular(p0));
-    pGhost->Fanin1 = Ivy_ObjId(Ivy_Regular(p1));
-    if ( pGhost->Fanin0 < pGhost->Fanin1 )
-    {
-        Temp = pGhost->Fanin0, pGhost->Fanin0 = pGhost->Fanin1, pGhost->Fanin1 = Temp;
-        Temp = pGhost->fComp0, pGhost->fComp0 = pGhost->fComp1, pGhost->fComp1 = Temp;
-    }
-    assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 );
-    return pGhost;
-}
-
-// create the ghost of the new node
-static inline Ivy_Obj_t *  Ivy_ObjCreateGhost2( Ivy_Man_t * p, Ivy_Obj_t * pObjDead )    
-{
-    Ivy_Obj_t * pGhost;
-    pGhost = Ivy_ManGhost(p);
-    pGhost->Type   = pObjDead->Type;
-    pGhost->Init   = pObjDead->Init;
-    pGhost->fComp0 = pObjDead->fComp0;
-    pGhost->fComp1 = pObjDead->fComp1;
-    pGhost->Fanin0 = pObjDead->Fanin0;
-    pGhost->Fanin1 = pObjDead->Fanin1;
-    assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 );
+    pGhost->pFanin0 = p0;
+    pGhost->pFanin1 = p1;
+    assert( Type == IVY_PI || Ivy_ObjFanin0(pGhost) != Ivy_ObjFanin1(pGhost) );
+    if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) )
+        pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp;
     return pGhost;
 }
 
@@ -352,48 +309,58 @@ static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB )
     return IVY_INIT_0;
 }
 
-// extended fanins
-static inline Vec_Int_t *  Ivy_ObjGetFanins( Ivy_Obj_t * pObj )                      { assert(Ivy_ObjMan(pObj)->fExtended); return (Vec_Int_t *)*(((int*)pObj)+2);            }
-static inline void         Ivy_ObjSetFanins( Ivy_Obj_t * pObj, Vec_Int_t * vFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); assert(Ivy_ObjGetFanins(pObj)==NULL); *(Vec_Int_t **)(((int*)pObj)+2) = vFanins; }
-static inline void         Ivy_ObjStartFanins( Ivy_Obj_t * pObj, int nFanins )       { assert(Ivy_ObjMan(pObj)->fExtended); Ivy_ObjSetFanins( pObj, Vec_IntAlloc(nFanins) );  }
-static inline void         Ivy_ObjAddFanin( Ivy_Obj_t * pObj, int Fanin )            { assert(Ivy_ObjMan(pObj)->fExtended); Vec_IntPush( Ivy_ObjGetFanins(pObj), Fanin );     }
-static inline int          Ivy_ObjReadFanin( Ivy_Obj_t * pObj, int i )               { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntEntry( Ivy_ObjGetFanins(pObj), i ); }
-static inline int          Ivy_ObjFaninNum( Ivy_Obj_t * pObj )                       { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntSize( Ivy_ObjGetFanins(pObj) );     }
+// internal memory manager
+static inline Ivy_Obj_t * Ivy_ManFetchMemory( Ivy_Man_t * p )  
+{ 
+    extern void Ivy_ManAddMemory( Ivy_Man_t * p );
+    Ivy_Obj_t * pTemp;
+    if ( p->pListFree == NULL )
+        Ivy_ManAddMemory( p );
+    pTemp = p->pListFree;
+    p->pListFree = *((Ivy_Obj_t **)pTemp);
+    memset( pTemp, 0, sizeof(Ivy_Obj_t) ); 
+    return pTemp;
+}
+static inline void Ivy_ManRecycleMemory( Ivy_Man_t * p, Ivy_Obj_t * pEntry )
+{
+    pEntry->Type = IVY_NONE; // distinquishes dead node from live node
+    *((Ivy_Obj_t **)pEntry) = p->pListFree;
+    p->pListFree = pEntry;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
 ////////////////////////////////////////////////////////////////////////
 
-// iterator over all objects, including those currently not used
-#define Ivy_ManForEachObj( p, pObj, i )                                                  \
-    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )
-#define Ivy_ManForEachObjReverse( p, pObj, i )                                           \
-    for ( i = p->ObjIdNext - 1, pObj = p->pObjs + i; i >= 0; i--, pObj-- )
 // iterator over the primary inputs
-#define Ivy_ManForEachPi( p, pObj, i )                                                   \
-    for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ )
+#define Ivy_ManForEachPi( p, pObj, i )                                          \
+    Vec_PtrForEachEntry( p->vPis, pObj, i )
 // iterator over the primary outputs
-#define Ivy_ManForEachPo( p, pObj, i )                                                   \
-    for ( i = 0; i < Vec_IntSize(p->vPos) && ((pObj) = Ivy_ManPo(p, i)); i++ )
+#define Ivy_ManForEachPo( p, pObj, i )                                          \
+    Vec_PtrForEachEntry( p->vPos, pObj, i )
+// iterator over all objects, including those currently not used
+#define Ivy_ManForEachObj( p, pObj, i )                                         \
+    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
 // iterator over the combinational inputs
-#define Ivy_ManForEachCi( p, pObj, i )                                                   \
-    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )                        \
-        if ( !Ivy_ObjIsCi(pObj) ) {} else
+#define Ivy_ManForEachCi( p, pObj, i )                                          \
+    Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else
 // iterator over the combinational outputs
-#define Ivy_ManForEachCo( p, pObj, i )                                                   \
-    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )                        \
-        if ( !Ivy_ObjIsCo(pObj) ) {} else
+#define Ivy_ManForEachCo( p, pObj, i )                                          \
+    Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else
 // iterator over logic nodes (AND and EXOR gates)
-#define Ivy_ManForEachNode( p, pObj, i )                                                 \
-    for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ )                      \
-        if ( !Ivy_ObjIsNode(pObj) ) {} else
+#define Ivy_ManForEachNode( p, pObj, i )                                        \
+    Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else
 // iterator over logic latches
-#define Ivy_ManForEachLatch( p, pObj, i )                                                \
-    for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ )                      \
-        if ( !Ivy_ObjIsLatch(pObj) ) {} else
+#define Ivy_ManForEachLatch( p, pObj, i )                                       \
+    Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else
 // iterator over the nodes whose IDs are stored in the array
-#define Ivy_ManForEachNodeVec( p, vIds, pObj, i )                                        \
+#define Ivy_ManForEachNodeVec( p, vIds, pObj, i )                               \
     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
+// iterator over the fanouts of an object
+#define Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, i )                     \
+    for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray);                        \
+          i < Vec_PtrSize(vArray) && ((pFanout) = Vec_PtrEntry(vArray,i)); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -401,19 +368,19 @@ static inline int          Ivy_ObjFaninNum( Ivy_Obj_t * pObj )
 
 /*=== ivyBalance.c ========================================================*/
 extern Ivy_Man_t *     Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
-extern Ivy_Obj_t *     Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel );
+extern Ivy_Obj_t *     Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel );
 /*=== ivyCanon.c ========================================================*/
-extern Ivy_Obj_t *     Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
-extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
-extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init );
+extern Ivy_Obj_t *     Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+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 );
 /*=== ivyCut.c ==========================================================*/
-extern void            Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
-extern Ivy_Store_t *   Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves );
+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 );
 /*=== ivyDfs.c ==========================================================*/
 extern Vec_Int_t *     Ivy_ManDfs( Ivy_Man_t * p );
-extern Vec_Int_t *     Ivy_ManDfsExt( Ivy_Man_t * p );
+extern Vec_Int_t *     Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches );
 extern void            Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
 extern Vec_Vec_t *     Ivy_ManLevelize( Ivy_Man_t * p );
 extern Vec_Int_t *     Ivy_ManRequiredLevels( Ivy_Man_t * p );
@@ -423,61 +390,76 @@ extern void            Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
 extern unsigned        Ivy_TruthDsdCompute( Vec_Int_t * vTree );
 extern void            Ivy_TruthDsdComputePrint( unsigned uTruth );
 extern Ivy_Obj_t *     Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree );
+/*=== ivyFanout.c ==========================================================*/
+extern void            Ivy_ManStartFanout( Ivy_Man_t * p );
+extern void            Ivy_ManStopFanout( Ivy_Man_t * p );
+extern void            Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout );
+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 );
 /*=== ivyMan.c ==========================================================*/
-extern Ivy_Man_t *     Ivy_ManStart( int nPis, int nPos, int nNodesMax );
+extern Ivy_Man_t *     Ivy_ManStart();
 extern void            Ivy_ManStop( Ivy_Man_t * p );
-extern void            Ivy_ManGrow( Ivy_Man_t * p );
 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
+extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p );
 extern void            Ivy_ManPrintStats( Ivy_Man_t * p );
+extern void            Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits );
+/*=== ivyMem.c ==========================================================*/
+extern void            Ivy_ManStartMemory( Ivy_Man_t * p );
+extern void            Ivy_ManStopMemory( Ivy_Man_t * p );
 /*=== ivyMulti.c ==========================================================*/
-extern Ivy_Obj_t *     Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-extern Ivy_Obj_t *     Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-extern Ivy_Obj_t *     Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
-extern Ivy_Obj_t *     Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-extern int             Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol );
+extern Ivy_Obj_t *     Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_Multi1( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_MultiBalance_rec( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern int             Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol );
 /*=== ivyObj.c ==========================================================*/
-extern Ivy_Obj_t *     Ivy_ObjCreate( Ivy_Obj_t * pGhost );
-extern Ivy_Obj_t *     Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type );
-extern void            Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin );
-extern void            Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop );
-extern void            Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop );
-extern void            Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop );
-extern void            Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode );
+extern Ivy_Obj_t *     Ivy_ObjCreatePi( Ivy_Man_t * p );
+extern Ivy_Obj_t *     Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver );
+extern Ivy_Obj_t *     Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost );
+extern void            Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 );
+extern void            Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew );
+extern void            Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
+extern void            Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop );
+extern void            Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop );
+extern void            Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode );
 /*=== ivyOper.c =========================================================*/
-extern Ivy_Obj_t *     Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
-extern Ivy_Obj_t *     Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
-extern Ivy_Obj_t *     Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
-extern Ivy_Obj_t *     Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
-extern Ivy_Obj_t *     Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
-extern Ivy_Obj_t *     Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
-extern Ivy_Obj_t *     Ivy_Miter( Vec_Ptr_t * vPairs );
+extern Ivy_Obj_t *     Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
+extern Ivy_Obj_t *     Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
+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_ManResyn( Ivy_Man_t * p, int fUpdateLevel );
+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 );
 extern int             Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
 extern int             Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
 /*=== ivyTable.c ========================================================*/
-extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Obj_t * pObj );
-extern void            Ivy_TableInsert( Ivy_Obj_t * pObj );
-extern void            Ivy_TableDelete( Ivy_Obj_t * pObj );
-extern void            Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew );
+extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew );
 extern int             Ivy_TableCountEntries( Ivy_Man_t * p );
-extern void            Ivy_TableResize( Ivy_Man_t * p );
-/*=== ivyUndo.c =========================================================*/
-extern void            Ivy_ManUndoStart( Ivy_Man_t * p );
-extern void            Ivy_ManUndoStop( Ivy_Man_t * p );
-extern void            Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj );
-extern void            Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot );
+extern void            Ivy_TableProfile( Ivy_Man_t * p );
 /*=== ivyUtil.c =========================================================*/
 extern void            Ivy_ManIncrementTravId( Ivy_Man_t * p );
 extern void            Ivy_ManCleanTravId( Ivy_Man_t * p );
+extern unsigned *      Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
+extern Vec_Int_t *     Ivy_ManLatches( Ivy_Man_t * p );
+extern int             Ivy_ManLevels( Ivy_Man_t * p );
+extern void            Ivy_ManResetLevels( Ivy_Man_t * p );
+extern void            Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew );
 extern int             Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
 extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
-extern unsigned *      Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
-extern Ivy_Obj_t *     Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin );
-extern Vec_Int_t *     Ivy_ManLatches( Ivy_Man_t * p );
-extern int             Ivy_ManReadLevels( Ivy_Man_t * p );
 extern Ivy_Obj_t *     Ivy_ObjReal( Ivy_Obj_t * pObj );
 
 #ifdef __cplusplus
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
index 2e230ed2..0303485a 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -27,7 +27,7 @@
 static int         Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
 static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
 static int         Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor );
+static void        Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
 static void        Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj );
 
 ////////////////////////////////////////////////////////////////////////
@@ -54,11 +54,11 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
     // clean the old manager
     Ivy_ManCleanTravId( p );
     // create the new manager 
-    pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 );
+    pNew = Ivy_ManStart();
     // map the nodes
     Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
     Ivy_ManForEachPi( p, pObj, i )
-        pObj->TravId = Ivy_EdgeFromNode( Ivy_ManPi(pNew, i) );
+        pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
     // balance the AIG
     vStore = Vec_VecAlloc( 50 );
     Ivy_ManForEachPo( p, pObj, i )
@@ -66,7 +66,7 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
         pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
         NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
         NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
-        Ivy_ObjConnect( Ivy_ManPo(pNew, i), Ivy_EdgeToNode(pNew, NewNodeId) );
+        Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
     }
     Vec_VecFree( vStore );
     if ( i = Ivy_ManCleanup( pNew ) )
@@ -139,11 +139,12 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto
         vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
     }
     // build the supergate
-    pObjNew = Ivy_NodeBalanceBuildSuper( vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
+    pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
     vSuper->nSize = 0;
     // make sure the balanced node is not assigned
     assert( pObjOld->TravId == 0 );
     pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
+//    assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level );
     return pObjOld->TravId;
 }
 
@@ -158,7 +159,7 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
+Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
 {
     Ivy_Obj_t * pObj1, * pObj2;
     int LeftBound;
@@ -171,11 +172,11 @@ Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int
         // find the left bound on the node to be paired
         LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
         // find the node that can be shared (if no such node, randomize choice)
-        Ivy_NodeBalancePermute( vSuper, LeftBound, Type == IVY_EXOR );
+        Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
         // pull out the last two nodes
         pObj1 = Vec_PtrPop(vSuper);
         pObj2 = Vec_PtrPop(vSuper);
-        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) );
+        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
     }
     return Vec_PtrEntry(vSuper, 0);
 }
@@ -314,7 +315,7 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
 {
     Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
     int RightBound, i;
@@ -330,8 +331,8 @@ void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
     for ( i = RightBound; i >= LeftBound; i-- )
     {
         pObj3 = Vec_PtrEntry( vSuper, i );
-        pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
-        if ( Ivy_TableLookup( pGhost ) )
+        pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
+        if ( Ivy_TableLookup( p, pGhost ) )
         {
             if ( pObj3 == pObj2 )
                 return;
diff --git a/src/temp/ivy/ivyCanon.c b/src/temp/ivy/ivyCanon.c
index c6f43d15..5768b87e 100644
--- a/src/temp/ivy/ivyCanon.c
+++ b/src/temp/ivy/ivyCanon.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
+static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,7 +41,7 @@ static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
+Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
 {
     Ivy_Obj_t * pResult, * pLat0, * pLat1;
     Ivy_Init_t Init, Init0, Init1;
@@ -53,9 +53,9 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
     // consider the case when the pair is canonical
     if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) )
     {
-        if ( pResult = Ivy_TableLookup( pGhost ) )
+        if ( pResult = Ivy_TableLookup( p, pGhost ) )
             return pResult;
-        return Ivy_ObjCreate( pGhost );
+        return Ivy_ObjCreate( p, pGhost );
     }
     /// remember the latches
     pLat0 = Ivy_ObjFanin0(pGhost);
@@ -64,16 +64,13 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
     Type = Ivy_ObjType(pGhost);
     fCompl0 = Ivy_ObjFaninC0(pGhost);
     fCompl1 = Ivy_ObjFaninC1(pGhost);
-    // modify the fanins to be latch fanins
-    pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0);
-    pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1);
     // call recursively
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pResult = Ivy_Oper( p, Ivy_NotCond(Ivy_ObjFanin0(pLat0), fCompl0), Ivy_NotCond(Ivy_ObjFanin0(pLat1), fCompl1), Type );
     // build latch on top of this
     Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 );
     Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 );
     Init  = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1);
-    return Ivy_CanonLatch( pResult, Init );
+    return Ivy_Latch( p, pResult, Init );
 }
 
 /**Function*************************************************************
@@ -87,11 +84,11 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
 {
     Ivy_Obj_t * pGhost, * pResult;
-    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( p, pGhost );
     return pResult;
 }
 
@@ -106,14 +103,14 @@ Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
 {
     Ivy_Obj_t * pGhost, * pResult;
     int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1);
     pObj0 = Ivy_Regular(pObj0);
     pObj1 = Ivy_Regular(pObj1);
-    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( p, pGhost );
     return Ivy_NotCond( pResult, fCompl );
 }
 
@@ -128,15 +125,15 @@ Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
+Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init )
 {
     Ivy_Obj_t * pGhost, * pResult;
     int fCompl = Ivy_IsComplement(pObj);
     pObj = Ivy_Regular(pObj);
-    pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
-    pResult = Ivy_TableLookup( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
+    pResult = Ivy_TableLookup( p, pGhost );
     if ( pResult == NULL )
-        pResult = Ivy_ObjCreate( pGhost );
+        pResult = Ivy_ObjCreate( p, pGhost );
     return Ivy_NotCond( pResult, fCompl );
 }
 
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
index c39eac12..4331c07e 100644
--- a/src/temp/ivy/ivyCheck.c
+++ b/src/temp/ivy/ivyCheck.c
@@ -39,15 +39,18 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManCheck( Ivy_Man_t * pMan )
+int Ivy_ManCheck( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj, * pObj2;
     int i;
-    Ivy_ManForEachObj( pMan, pObj, i )
+    Ivy_ManForEachObj( p, pObj, i )
     {
         // skip deleted nodes
-        if ( Ivy_ObjIsNone(pObj) )
-            continue;
+        if ( Ivy_ObjId(pObj) != i )
+        {
+            printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
+            return 0;
+        }
         // consider the constant node and PIs
         if ( i == 0 || Ivy_ObjIsPi(pObj) )
         {
@@ -69,44 +72,54 @@ int Ivy_ManCheck( Ivy_Man_t * pMan )
         }
         if ( Ivy_ObjIsBuf(pObj) )
         {
+            if ( Ivy_ObjFanin1(pObj) )
+            {
+                printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
+                return 0;
+            }
             continue;
         }
         if ( Ivy_ObjIsLatch(pObj) )
         {
-            if ( Ivy_ObjFaninId1(pObj) != 0 )
+            if ( Ivy_ObjFanin1(pObj) )
             {
                 printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
                 return 0;
             }
-            if ( Ivy_ObjInit(pObj) == 0 )
+            if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
             {
                 printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
                 return 0;
             }
-            pObj2 = Ivy_TableLookup( pObj );
+            pObj2 = Ivy_TableLookup( p, pObj );
             if ( pObj2 != pObj )
                 printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
                 continue;
         }
         // consider the AND node
-        if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) )
+        if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
         {
-            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id );
+            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
             return 0;
         }
-        if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) )
+        if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
         {
             printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
             return 0;
         }
 //        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
-//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
-        pObj2 = Ivy_TableLookup( pObj );
+//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
+        pObj2 = Ivy_TableLookup( p, pObj );
         if ( pObj2 != pObj )
             printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
+        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) )
+            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
-    if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) )
+    if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
     {
         printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 71a3613c..7d1ec63a 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -175,7 +175,7 @@ printf( "%d", Counter );
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize )
+void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize )
 {
     assert( !Ivy_IsComplement(pRoot) );
     assert( Ivy_ObjIsNode(pRoot) );
@@ -194,7 +194,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
     Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
 
     // compute the cut
-    while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) );
+    while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) );
     assert( Vec_IntSize(vFront) <= nSize );
 }
 
@@ -213,7 +213,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
+int Ivy_ManFindBoolCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
 {
     int RetValue0, RetValue1;
     if ( pObj == pPivot )
@@ -231,15 +231,15 @@ int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * v
 
     if ( Ivy_ObjIsBuf(pObj) )
     {
-        RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+        RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
         if ( !RetValue0 )
             return 0;
         Vec_PtrPushUnique( vVolume, pObj );
         return 1;
     }
     assert( Ivy_ObjIsNode(pObj) );
-    RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
-    RetValue1 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
+    RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+    RetValue1 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
     if ( !RetValue0 && !RetValue1 )
         return 0;
     // add new leaves
@@ -296,7 +296,7 @@ int Ivy_ManFindBoolCutCost( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
+int Ivy_ManFindBoolCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
 {
     Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot;
     int RetValue, LevelLimit, Lev, k;
@@ -405,7 +405,7 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu
     // cut exists, collect all the nodes on the shortest path to the pivot
     Vec_PtrClear( vLeaves );
     Vec_PtrClear( vVolume );
-    RetValue = Ivy_ManFindBoolCut_rec( pRoot, vLeaves, vVolume, pPivot );
+    RetValue = Ivy_ManFindBoolCut_rec( p, pRoot, vLeaves, vVolume, pPivot );
     assert( RetValue == 1 );
     // unmark the nodes on the frontier (including the pivot)
     Vec_PtrForEachEntry( vFront, pObj, k )
@@ -481,7 +481,7 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p )
         }
         if ( Ivy_ObjIsExor(pObj) )
             printf( "x" );
-        RetValue = Ivy_ManFindBoolCut( pObj, vFront, vVolume, vLeaves );
+        RetValue = Ivy_ManFindBoolCut( p, pObj, vFront, vVolume, vLeaves );
         if ( RetValue == 0 )
             printf( "- " );
         else
@@ -783,11 +783,11 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves )
+Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves )
 {
     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
-    Ivy_Man_t * pMan = Ivy_ObjMan(pObj);
+    Ivy_Man_t * pMan = p;
     Ivy_Obj_t * pLeaf;
     int i, k;
 
@@ -815,7 +815,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves )
             continue;
         for ( k = 0; k < pCut->nSize; k++ )
         {
-            pLeaf = Ivy_ObjObj( pObj, pCut->pArray[k] );
+            pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
             if ( Ivy_ObjIsCi(pLeaf) )
                 continue;
             *pCutNew = *pCut;
@@ -859,7 +859,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
     {
         if ( !Ivy_ObjIsNode(pObj) )
             continue;
-        nCutsCut    = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts;
+        nCutsCut    = Ivy_NodeFindCutsAll( p, pObj, 5 )->nCuts;
         nCutsTotal += nCutsCut;
         nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
         nNodeTotal++;
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 2dc3bac8..fb938c42 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -69,17 +69,14 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
     Vec_Int_t * vNodes;
     Ivy_Obj_t * pObj;
     int i;
+    assert( Ivy_ManLatchNum(p) == 0 );
     // make sure the nodes are not marked
     Ivy_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
     // collect the nodes
     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
-    if ( Ivy_ManLatchNum(p) > 0 )
-        Ivy_ManForEachCo( p, pObj, i )
-            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
-    else
-        Ivy_ManForEachPo( p, pObj, i )
-            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
     // unmark the collected nodes
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
@@ -90,34 +87,7 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
-{
-    Vec_Int_t * vFanins;
-    int i, Fanin;
-    if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) )
-        return;
-    // mark the node as visited
-    Ivy_ObjSetMarkA(pObj);
-    // traverse the fanins
-    vFanins = Ivy_ObjGetFanins( pObj );
-    Vec_IntForEachEntry( vFanins, Fanin, i )
-        Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes );
-    // add the node
-    Vec_IntPush( vNodes, pObj->Id );
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the DFS order.]
+  Synopsis    [Collects AND/EXOR nodes in the DFS order from CIs to COs.]
 
   Description []
                
@@ -126,25 +96,31 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
+Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
 {
-    Vec_Int_t * vNodes;
-    Ivy_Obj_t * pObj, * pFanin;
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Obj_t * pObj;
     int i;
-    assert( p->fExtended ); 
-    assert( Ivy_ManLatchNum(p) == 0 ); 
-    // make sure network does not have buffers
-    vNodes = Vec_IntAlloc( 10 );
+    assert( Ivy_ManLatchNum(p) > 0 );
+    // make sure the nodes are not marked
+    Ivy_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    // collect the latches
+    vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
+    Ivy_ManForEachLatch( p, pObj, i )
+        Vec_IntPush( vLatches, pObj->Id );
+    // collect the nodes
+    vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
     Ivy_ManForEachPo( p, pObj, i )
-    {
-        pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) );
-        Ivy_ManDfsExt_rec( pFanin, vNodes );
-    }
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    // unmark the collected nodes
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
-    // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes
-//    assert( p->nNodes == Vec_PtrSize(vNodes) );
+    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
+    *pvLatches = vLatches;
     return vNodes;
 }
 
@@ -249,7 +225,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
     int i, k, Level, LevelMax;
     assert( p->vRequired == NULL );
     // start the required times
-    vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) );
+    vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 );
     // iterate through the nodes in the reverse order
     vNodes = Ivy_ManLevelize( p );
     Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
@@ -262,7 +238,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
     }
     Vec_VecFree( vNodes );
     // convert it into the required times
-    LevelMax = Ivy_ManReadLevels( p );
+    LevelMax = Ivy_ManLevels( p );
 //printf( "max %5d\n",LevelMax );
     Ivy_ManForEachObj( p, pObj, i )
     {
diff --git a/src/temp/ivy/ivyDsd.c b/src/temp/ivy/ivyDsd.c
index 5dfdd30f..3b8a2e68 100644
--- a/src/temp/ivy/ivyDsd.c
+++ b/src/temp/ivy/ivyDsd.c
@@ -608,7 +608,7 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod
 
 //        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
 
-        pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
+        pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
         return Ivy_NotCond( pResult, Node.fCompl );
     }
     assert( Node.fCompl == 0 );
@@ -626,9 +626,9 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod
         pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
         pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
         if ( Node.Type == IVY_DEC_MUX )
-            return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] );
+            return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
         else
-            return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] );
+            return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
     }
     assert( 0 );
     return 0;
diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c
new file mode 100644
index 00000000..5911e051
--- /dev/null
+++ b/src/temp/ivy/ivyFanout.c
@@ -0,0 +1,317 @@
+/**CFile****************************************************************
+
+  FileName    [ivyFanout.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Representation of the fanouts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyFanout.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        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);  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the fanout representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( Ivy_ObjFanin0(pObj) )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
+        if ( Ivy_ObjFanin1(pObj) )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fanout representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStopFanout( Ivy_Man_t * p )
+{
+    void * pTemp;
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Add the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjAddFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, 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
+    {
+        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 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, 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;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the fanout of pOld to be pFanoutNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, 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;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts iteration through the fanouts.]
+
+  Description [Copies the currently available fanouts into the array.]
+               
+  SideEffects [Can be used while the fanouts are being removed.]
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads one fanout.]
+
+  Description [Returns fanout if there is only one fanout.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads one fanout.]
+
+  Description [Returns fanout if there is only one fanout.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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) );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c
new file mode 100644
index 00000000..f53e513d
--- /dev/null
+++ b/src/temp/ivy/ivyIsop.c
@@ -0,0 +1,241 @@
+/**CFile****************************************************************
+
+  FileName    [ivyIsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Computing irredundant SOP using truth table.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Sop_t_ Ivy_Sop_t;
+struct Ivy_Sop_t_
+{
+    unsigned * pCubes;
+    int        nCubes;
+};
+
+static Mem_Flex_t * s_Man = NULL;
+
+static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthManStart()
+{
+    s_Man = Mem_FlexStart();
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthManStop()
+{
+    Mem_FlexStop( s_Man, 0 );
+    s_Man = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP for 5 variables or less.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes )
+{
+    Ivy_Sop_t cRes0, cRes1, cRes2;
+    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
+    unsigned * puRes0, * puRes1, * puRes2;
+    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1;
+    int i, k, Var, nWords;
+    assert( nVars > 5 );
+    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+    if ( Extra_TruthIsConst0( puOn, nVars ) )
+    {
+        pcRes->nCubes = 0;
+        pcRes->pCubes = NULL;
+        return puOn;
+    }
+    if ( Extra_TruthIsConst1( puOnDc, nVars ) )
+    {
+        pcRes->nCubes = 1;
+        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes[0] = 0;
+        return puOnDc;
+    }
+    // find the topmost var
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || 
+             Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
+             break;
+    assert( Var >= 0 );
+    if ( Var < 5 )
+    {
+        unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes );
+        return puRes;
+    }
+    nWords = Extra_TruthWordNum( Var+1 );
+    // cofactor
+    puOn0 = puOn;
+    puOn1 = puOn + nWords;
+    puOnDc0 = puOnDc;
+    puOnDc1 = puOnDc + nWords;
+    // intermediate copies
+    pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+    pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+    // solve for cofactors
+    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 );
+    puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 );
+    Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 );
+    puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 );
+    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 );
+    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 );
+    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 );
+    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 );
+    puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 );
+    // create the resulting cover
+    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
+    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    k = 0;
+    for ( i = 0; i < pcRes0->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes2->pCubes[i];
+    assert( k == pcRes->nCubes );
+    // create the resulting truth table
+    Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 );
+    Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 );
+    return pTemp0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP for 5 variables or less.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes )
+{
+    unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    Ivy_Sop_t cRes0, cRes1, cRes2;
+    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
+    unsigned uRes0, uRes1, uRes2;
+    unsigned uOn0, uOn1, uOnDc0, uOnDc1;
+    int i, k, Var;
+    assert( nVars <= 5 );
+    assert( uOn & ~uOnDc == 0 );
+    if ( Extra_TruthIsConst0( uOn == 0 )
+    {
+        pcRes->nCubes = 0;
+        pcRes->pCubes = NULL;
+        return 0;
+    }
+    if ( uOnDc == 0xFFFFFFFF )
+    {
+        pcRes->nCubes = 1;
+        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes[0] = 0;
+        return 0xFFFFFFFF;
+    }
+    // find the topmost var
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || 
+             Extra_TruthVarInSupport( &uOnDc, 5, Var ) )
+             break;
+    assert( Var >= 0 );
+    // cofactor
+    uOn0 = uOn1 = uOn;
+    uOnDc0 = uOnDc1 = uOnDc;
+    Extra_TruthCofactor0( &uOn0, 5, Var );
+    Extra_TruthCofactor1( &uOn1, 5, Var );
+    Extra_TruthCofactor0( &uOnDc0, 5, Var );
+    Extra_TruthCofactor1( &uOnDc1, 5, Var );
+    // solve for cofactors
+    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 );
+    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 );
+    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 );
+    // create the resulting cover
+    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
+    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    k = 0;
+    for ( i = 0; i < pcRes0->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes2->pCubes[i];
+    assert( k == pcRes->nCubes );
+    return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 2ff90aa9..d1aca8a6 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -39,53 +39,32 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
+Ivy_Man_t * Ivy_ManStart()
 {
     Ivy_Man_t * p;
-    Ivy_Obj_t * pObj;
-    int i, nTotalSize;
     // start the manager
     p = ALLOC( Ivy_Man_t, 1 );
     memset( p, 0, sizeof(Ivy_Man_t) );
+    // perform initializations
+    p->Ghost.Id = -1;
     p->nTravIds = 1;
     p->fCatchExor = 1;
-    // AIG nodes
-    p->nObjsAlloc = 1 + nPis + nPos + nNodesMax;
-//    p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even
-    nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1;
-    p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize );
-    memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize );
-    // temporary storage for deleted entries
-    p->vFree  = Vec_IntAlloc( 100 );
-    // set the node IDs
-    for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ )
-        pObj->Id = i - IVY_SANDBOX_SIZE - 1;
-    // remember the manager in the first entry
-    *((Ivy_Man_t **)p->pObjs) = p; 
-    p->pObjs += IVY_SANDBOX_SIZE + 1;
+    // allocate arrays for nodes
+    p->vPis = Vec_PtrAlloc( 100 );
+    p->vPos = Vec_PtrAlloc( 100 );
+    p->vBufs = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 100 );
+    // prepare the internal memory manager
+    Ivy_ManStartMemory( p );
     // create the constant node
+    p->pConst1 = Ivy_ManFetchMemory( p );
+    p->pConst1->fPhase = 1;
+    Vec_PtrPush( p->vObjs, p->pConst1 );
     p->nCreated = 1;
-    p->ObjIdNext = 1;
-    Ivy_ManConst1(p)->fPhase = 1;
-    // create PIs
-    pObj = Ivy_ManGhost(p);
-    pObj->Type = IVY_PI;
-    p->vPis = Vec_IntAlloc( 100 );
-    for ( i = 0; i < nPis; i++ )
-        Ivy_ObjCreate( pObj );
-    // create POs
-    pObj->Type = IVY_PO;
-    p->vPos = Vec_IntAlloc( 100 );
-    for ( i = 0; i < nPos; i++ )
-        Ivy_ObjCreate( pObj );
     // start the table
-    p->nTableSize = p->nObjsAlloc*5/2+13;
+    p->nTableSize = 10007;
     p->pTable = ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
-    // allocate undo storage
-    p->nUndosAlloc = 100;
-    p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc );
-    memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc );
     return p;
 }
 
@@ -102,22 +81,15 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
 ***********************************************************************/
 void Ivy_ManStop( Ivy_Man_t * p )
 {
-    if ( p->fExtended )
-    {
-        Ivy_Obj_t * pObj;
-        int i;
-        Ivy_ManForEachObj( p, pObj, i )
-            if ( Ivy_ObjGetFanins(pObj) )
-                Vec_IntFree( Ivy_ObjGetFanins(pObj) );
-    }
-    if ( p->vFree )   Vec_IntFree( p->vFree );
-    if ( p->vTruths ) Vec_IntFree( p->vTruths );
-    if ( p->vPis )    Vec_IntFree( p->vPis );
-    if ( p->vPos )    Vec_IntFree( p->vPos );
-    FREE( p->pMemory );
-    free( p->pObjs - IVY_SANDBOX_SIZE - 1 );
+//    Ivy_TableProfile( 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 );
+    if ( p->vPos )      Vec_PtrFree( p->vPos );
+    if ( p->vBufs )     Vec_PtrFree( p->vBufs );
+    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
     free( p->pTable );
-    free( p->pUndos );
     free( p );
 }
 
@@ -132,18 +104,15 @@ void Ivy_ManStop( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManGrow( Ivy_Man_t * p )
+int Ivy_ManCleanup( Ivy_Man_t * p )
 {
-    int i;
-    assert( p->ObjIdNext == p->nObjsAlloc );
-    if ( p->ObjIdNext != p->nObjsAlloc )
-        return;
-//    printf( "Ivy_ObjCreate(): Reallocing the node array.\n" );
-    p->nObjsAlloc = 2 * p->nObjsAlloc;
-    p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1;
-    memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 );
-    for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ )
-        Ivy_ManObj( p, i )->Id = i;
+    Ivy_Obj_t * pNode;
+    int i, nNodesOld;
+    nNodesOld = Ivy_ManNodeNum(p);
+    Ivy_ManForEachNode( p, pNode, i )
+        if ( Ivy_ObjRefs(pNode) == 0 )
+            Ivy_ObjDelete_rec( p, pNode, 1 );
+    return nNodesOld - Ivy_ManNodeNum(p);
 }
 
 /**Function*************************************************************
@@ -157,15 +126,19 @@ void Ivy_ManGrow( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManCleanup( Ivy_Man_t * p )
+int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pNode;
-    int i, nNodesOld;
-    nNodesOld = Ivy_ManNodeNum(p);
-    Ivy_ManForEachNode( p, pNode, i )
-        if ( Ivy_ObjRefs(pNode) == 0 )
-            Ivy_ObjDelete_rec( pNode, 1 );
-    return nNodesOld - Ivy_ManNodeNum(p);
+    int nSteps;
+    for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
+    {
+        pNode = Vec_PtrEntryLast(p->vBufs);
+        while ( Ivy_ObjIsBuf(pNode) )
+            pNode = Ivy_ObjReadFirstFanout( p, pNode );
+        Ivy_NodeFixBufferFanins( p, pNode );
+    }
+//    printf( "Number of steps = %d\n", nSteps );
+    return nSteps;
 }
 
 /**Function*************************************************************
@@ -182,24 +155,71 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
 void Ivy_ManPrintStats( Ivy_Man_t * p )
 {
     printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
-    if ( p->fExtended )
-    {
-    printf( "Am = %d. ",    Ivy_ManAndMultiNum(p) );
-    printf( "Xm = %d. ",    Ivy_ManExorMultiNum(p) );
-    printf( "Lut = %d. ",   Ivy_ManLutNum(p) );
-    }
-    else
+    printf( "A = %d. ",       Ivy_ManAndNum(p) );
+    printf( "L = %d. ",       Ivy_ManLatchNum(p) );
+//    printf( "X = %d. ",       Ivy_ManExorNum(p) );
+    printf( "B = %d. ",       Ivy_ManBufNum(p) );
+    printf( "MaxID = %d. ",   Ivy_ManObjIdMax(p) );
+//    printf( "Cre = %d. ",     p->nCreated );
+//    printf( "Del = %d. ",     p->nDeleted );
+    printf( "Lev = %d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a combinational AIG manager into a sequential one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
+{
+    Ivy_Obj_t * pObj, * pLatch;
+    Ivy_Init_t Init;
+    int i;
+    if ( nLatches == 0 )
+        return;
+    assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) );
+    assert( Ivy_ManPiNum(p) == Vec_PtrSize(p->vPis) );
+    assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) );
+    assert( Vec_PtrSize( p->vBufs ) == 0 );
+    // create fanouts
+    if ( p->vFanouts == NULL )
+        Ivy_ManStartFanout( p );
+    // collect the POs to be converted into latches
+    for ( i = 0; i < nLatches; i++ )
     {
-    printf( "A = %d. ",     Ivy_ManAndNum(p) );
-    printf( "X = %d. ",     Ivy_ManExorNum(p) );
-    printf( "B = %4d. ",     Ivy_ManBufNum(p) );
+        // get the latch value
+        Init = pInits? pInits[i] : IVY_INIT_0;
+        // create latch
+        pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i );
+        pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init );
+        Ivy_ObjDisconnect( p, pObj );
+        // convert the corresponding PI to a buffer and connect it to the latch
+        pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i );
+        pObj->Type = IVY_BUF;
+        Ivy_ObjConnect( p, pObj, pLatch, NULL );
+        // save the buffer
+        Vec_PtrPush( p->vBufs, pObj );
     }
-//    printf( "MaxID = %d. ", p->ObjIdNext-1 );
-//    printf( "All = %d. ",   p->nObjsAlloc );
-    printf( "Cre = %d. ",   p->nCreated );
-    printf( "Del = %d. ",   p->nDeleted );
-    printf( "Lev = %d. ",   Ivy_ManReadLevels(p) );
-    printf( "\n" );
+    // shrink the arrays
+    Vec_PtrShrink( p->vPis, Ivy_ManPiNum(p) - nLatches );
+    Vec_PtrShrink( p->vPos, Ivy_ManPoNum(p) - nLatches );
+    // update the counters of different objects
+    p->nObjs[IVY_PI] -= nLatches;
+    p->nObjs[IVY_PO] -= nLatches;
+    p->nObjs[IVY_BUF] += nLatches;
+    p->nDeleted -= 2 * nLatches;
+    // perform hashing by propagating the buffers
+    Ivy_ManPropagateBuffers( p );
+    // check the resulting network
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c
new file mode 100644
index 00000000..01833f03
--- /dev/null
+++ b/src/temp/ivy/ivyMem.c
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+  FileName    [ivyMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Memory management for the AIG nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// memory management
+#define IVY_PAGE_SIZE      12        // page size containing 2^IVY_PAGE_SIZE nodes
+#define IVY_PAGE_MASK    4095        // page bitmask (2^IVY_PAGE_SIZE)-1
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStartMemory( Ivy_Man_t * p )
+{
+    p->vChunks = Vec_PtrAlloc( 128 );
+    p->vPages = Vec_PtrAlloc( 128 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStopMemory( Ivy_Man_t * p )
+{
+    void * pMemory;
+    int i;
+    Vec_PtrForEachEntry( p->vChunks, pMemory, i )
+        free( pMemory );
+    Vec_PtrFree( p->vChunks );
+    Vec_PtrFree( p->vPages );
+    p->pListFree = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates additional memory for the nodes.]
+
+  Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. 
+  Records the pointer to the AIG manager in the -1 entry.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManAddMemory( Ivy_Man_t * p )
+{
+    char * pMemory;
+    int i, nBytes;
+    assert( sizeof(Ivy_Obj_t) <= 32 );
+    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;
+    pMemory = ALLOC( char, nBytes );
+    Vec_PtrPush( p->vChunks, pMemory );
+    // align memory at the 32-byte boundary
+    pMemory = pMemory + 32 - (((int)pMemory) & 31);
+    // remember the manager in the first entry
+    Vec_PtrPush( p->vPages, pMemory );
+    // break the memory down into nodes
+    p->pListFree = (Ivy_Obj_t *)pMemory;
+    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
+    {
+        *((char **)pMemory) = pMemory + sizeof(Ivy_Obj_t);
+        pMemory += sizeof(Ivy_Obj_t);
+    }
+    *((char **)pMemory) = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index e2a44e2d..f098332d 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -34,8 +34,8 @@ struct Ivy_Eva_t_
     int         Weight;   // the number of covered nodes
 };
 
-static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
-static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
+static void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
+static int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -52,7 +52,7 @@ static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLim
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
+int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
 {
     static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
     Ivy_Eva_t * pEval, * pFan0, * pFan1;
@@ -122,7 +122,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int
     {
         pFan0 = pEvals + i;
         pFan1 = pEvals + k;
-        pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
+        pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
         // skip nodes in the cone
         if ( pTemp == NULL || pTemp->fMarkB )
             continue;
@@ -149,7 +149,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int
 Outside:
 
 //    Ivy_MultiPrint( pEvals, nLeaves, nEvals );
-    if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) )
+    if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) )
         return 0;
     assert( Vec_PtrSize( vSols ) > 0 );
     return 1;
@@ -166,7 +166,7 @@ Outside:
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
+void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
 {
     Ivy_Eva_t * pEval;
     int i, k;
@@ -215,7 +215,7 @@ static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFoun
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
+int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
 {
     int fVerbose = 0;
     Ivy_Eva_t * pEval, * pEvalBest;
@@ -294,6 +294,45 @@ int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Constructs the well-balanced tree of gates.]
+
+  Description [Disregards levels and possible logic sharing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
+    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+    return Ivy_Oper( p, pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 703218bb..de67c560 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -39,36 +39,54 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
+Ivy_Obj_t * Ivy_ObjCreatePi( Ivy_Man_t * p )
+{
+    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, NULL, NULL, IVY_PI, IVY_INIT_NONE) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreatePo( Ivy_Man_t * p, Ivy_Obj_t * pDriver )
+{
+    return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pDriver, NULL, IVY_PO, IVY_INIT_NONE) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
 {
-    Ivy_Man_t * p = Ivy_ObjMan(pGhost);
     Ivy_Obj_t * pObj;
     assert( !Ivy_IsComplement(pGhost) );
     assert( Ivy_ObjIsGhost(pGhost) );
-
-    assert( Ivy_TableLookup(pGhost) == NULL );
-
-    // realloc the node array
-    if ( p->ObjIdNext == p->nObjsAlloc )
-    {
-        printf( "AIG manager is being resized. In the current release, it is not allowed!\n" );
-        Ivy_ManGrow( p );
-        pGhost = Ivy_ManGhost( p );
-    }
+    assert( Ivy_TableLookup(p, pGhost) == NULL );
     // get memory for the new object
-    if ( Vec_IntSize(p->vFree) > 0 )
-        pObj = p->pObjs + Vec_IntPop(p->vFree);
-    else
-        pObj = p->pObjs + p->ObjIdNext++;
-    assert( pObj->Id == pObj - p->pObjs );
+    pObj = Ivy_ManFetchMemory( p );
     assert( Ivy_ObjIsNone(pObj) );
+    pObj->Id = Vec_PtrSize(p->vObjs);
+    Vec_PtrPush( p->vObjs, pObj );
     // add basic info (fanins, compls, type, init)
-    Ivy_ObjOverwrite( pObj, pGhost );
-    // increment references of the fanins
-    Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
-    Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
-    // add the node to the structural hash table
-    Ivy_TableInsert( pObj );
+    pObj->Type = pGhost->Type;
+    pObj->Init = pGhost->Init;
+    // add connections
+    Ivy_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
     // compute level
     if ( Ivy_ObjIsNode(pObj) )
         pObj->Level = Ivy_ObjLevelNew(pObj);
@@ -86,9 +104,13 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
     }
     // add PIs/POs to the arrays
     if ( Ivy_ObjIsPi(pObj) )
-        Vec_IntPush( p->vPis, pObj->Id );
+        Vec_PtrPush( p->vPis, pObj );
     else if ( Ivy_ObjIsPo(pObj) )
-        Vec_IntPush( p->vPos, pObj->Id );
+        Vec_PtrPush( p->vPos, pObj );
+//    else if ( Ivy_ObjIsBuf(pObj) )
+//        Vec_PtrPush( p->vBufs, pObj );
+    if ( p->vRequired && Vec_IntSize(p->vRequired) <= pObj->Id )
+        Vec_IntFillExtra( p->vRequired, 2 * Vec_IntSize(p->vRequired), 1000000 );
     // update node counters of the manager
     p->nObjs[Ivy_ObjType(pObj)]++;
     p->nCreated++;
@@ -97,7 +119,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
 
 /**Function*************************************************************
 
-  Synopsis    [Create the new node assuming it does not exist.]
+  Synopsis    [Connect the object to the fanin.]
 
   Description []
                
@@ -106,22 +128,28 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type )
+void Ivy_ObjConnect( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFan0, Ivy_Obj_t * pFan1 )
 {
-    Ivy_Obj_t * pObj;
-    assert( Type == IVY_ANDM || Type == IVY_EXORM || Type == IVY_LUT ); 
-    // realloc the node array
-    if ( p->ObjIdNext == p->nObjsAlloc )
-        Ivy_ManGrow( p );
-    // create the new node
-    pObj = p->pObjs + p->ObjIdNext;
-    assert( pObj->Id == p->ObjIdNext );
-    p->ObjIdNext++;
-    pObj->Type = Type;
-    // update node counters of the manager
-    p->nObjs[Type]++;
-    p->nCreated++;
-    return pObj;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || pFan1 != NULL );
+    // add the first fanin
+    pObj->pFanin0 = pFan0;
+    pObj->pFanin1 = pFan1;
+    // increment references of the fanins and add their fanouts
+    if ( Ivy_ObjFanin0(pObj) != NULL )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
+        if ( p->vFanouts )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj );
+    }
+    if ( Ivy_ObjFanin1(pObj) != NULL )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
+        if ( p->vFanouts )
+            Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj );
+    }
+    // add the node to the structural hash table
+    Ivy_TableInsert( p, pObj );
 }
 
 /**Function*************************************************************
@@ -135,18 +163,59 @@ Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )
+void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
     assert( !Ivy_IsComplement(pObj) );
-    assert( Ivy_ObjIsOneFanin(pObj) );
-    assert( Ivy_ObjFaninId0(pObj) == 0 );
+    assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL );
+    // remove connections
+    if ( Ivy_ObjFanin0(pObj) != NULL )
+    {
+        Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
+        if ( p->vFanouts )
+            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj );
+    }
+    if ( Ivy_ObjFanin1(pObj) != NULL )
+    {
+        Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
+        if ( p->vFanouts )
+            Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj );
+    }
+    // remove the node from the structural hash table
+    Ivy_TableDelete( p, pObj );
     // add the first fanin
-    pObj->fComp0 = Ivy_IsComplement(pFanin);
-    pObj->Fanin0 = Ivy_Regular(pFanin)->Id;
-    // increment references of the fanins
-    Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
-    // add the node to the structural hash table
-    Ivy_TableInsert( pObj );
+    pObj->pFanin0 = NULL;
+    pObj->pFanin1 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the first fanin of the node by the new fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew )
+{
+    Ivy_Obj_t * pFaninOld;
+    assert( !Ivy_IsComplement(pObj) );
+    pFaninOld = Ivy_ObjFanin0(pObj);
+    // decrement ref and remove fanout
+    Ivy_ObjRefsDec( pFaninOld );
+    if ( p->vFanouts )
+        Ivy_ObjDeleteFanout( p, pFaninOld, pObj );
+    // increment ref and add fanout
+    Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) );
+    if ( p->vFanouts )
+        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 );
 }
 
 /**Function*************************************************************
@@ -160,33 +229,35 @@ void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop )
+void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
 {
-    Ivy_Man_t * p;
     assert( !Ivy_IsComplement(pObj) );
-    assert( Ivy_ObjRefs(pObj) == 0 );
-    // remove connections
-    Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
-    Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
-    // remove the node from the structural hash table
-    Ivy_TableDelete( pObj );
+    assert( Ivy_ObjRefs(pObj) == 0 || !fFreeTop );
     // update node counters of the manager
-    p = Ivy_ObjMan(pObj);
     p->nObjs[pObj->Type]--;
     p->nDeleted++;
+    // remove connections
+    Ivy_ObjDisconnect( p, pObj );
     // remove PIs/POs from the arrays
     if ( Ivy_ObjIsPi(pObj) )
-        Vec_IntRemove( p->vPis, pObj->Id );
+        Vec_PtrRemove( p->vPis, pObj );
     else if ( Ivy_ObjIsPo(pObj) )
-        Vec_IntRemove( p->vPos, pObj->Id );
-    // recorde the deleted node
-    if ( p->fRecording )
-        Ivy_ManUndoRecord( p, pObj );
-    // clean the node's memory
-    Ivy_ObjClean( pObj );
-    // remember the entry
+        Vec_PtrRemove( p->vPos, pObj );
+    else if ( p->vFanouts && Ivy_ObjIsBuf(pObj) )
+        Vec_PtrRemove( p->vBufs, pObj );
+    // clean and recycle the entry
     if ( fFreeTop )
-        Vec_IntPush( p->vFree, pObj->Id );
+    {
+        // free the node
+        Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+        Ivy_ManRecycleMemory( p, pObj );
+    }
+    else
+    {
+        int nRefsOld = pObj->nRefs;
+        Ivy_ObjClean( pObj );
+        pObj->nRefs = nRefsOld;
+    }
 }
 
 /**Function*************************************************************
@@ -200,20 +271,20 @@ void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop )
+void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
 {
     Ivy_Obj_t * pFanin0, * pFanin1;
     assert( !Ivy_IsComplement(pObj) );
-    assert( !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsNone(pObj) );
+    assert( !Ivy_ObjIsNone(pObj) );
     if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) )
         return;
     pFanin0 = Ivy_ObjFanin0(pObj);
     pFanin1 = Ivy_ObjFanin1(pObj);
-    Ivy_ObjDelete( pObj, fFreeTop );
-    if ( !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 )
-        Ivy_ObjDelete_rec( pFanin0, 1 );
-    if ( !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 )
-        Ivy_ObjDelete_rec( pFanin1, 1 );
+    Ivy_ObjDelete( p, pObj, fFreeTop );
+    if ( pFanin0 && !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 )
+        Ivy_ObjDelete_rec( p, pFanin0, 1 );
+    if ( pFanin1 && !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 )
+        Ivy_ObjDelete_rec( p, pFanin1, 1 );
 }
 
 /**Function*************************************************************
@@ -229,66 +300,61 @@ void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop )
+void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop )
 {
     int nRefsOld;
     // the object to be replaced cannot be complemented
     assert( !Ivy_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
-    assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsTerm(pObjOld) );
+    assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsPi(pObjOld) );
     // the object to be used cannot be a PO or assert
-    assert( !Ivy_ObjIsPo(Ivy_Regular(pObjNew)) );
+    assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
     // the object cannot be the same
     assert( pObjOld != Ivy_Regular(pObjNew) );
     // if the new object is complemented or already used, add the buffer
-    if ( Ivy_IsComplement(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
-        pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pObjNew, Ivy_ObjConst1(pObjOld), IVY_BUF, IVY_INIT_NONE) );
+    if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+        pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
     assert( !Ivy_IsComplement(pObjNew) );
-    // remember the reference counter
-    nRefsOld = pObjOld->nRefs;  
-    pObjOld->nRefs = 0;
+    // 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 )
+    {
+        assert( Ivy_ObjIsNode(pObjOld) );
+        pObjOld->Level = pObjNew->Level;
+        Ivy_ObjUpdateLevel_rec( p, pObjOld );
+    }
+    // if the new node's required time has changed, recursively update required time of the fanins
+    if ( p->vRequired )
+    {
+        int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
+        if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) )
+        {
+            Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew );
+            Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
+        }
+    }
     // delete the old object
     if ( fDeleteOld )
-        Ivy_ObjDelete_rec( pObjOld, fFreeTop );
+        Ivy_ObjDelete_rec( p, pObjOld, fFreeTop );
     // transfer the old object
     assert( Ivy_ObjRefs(pObjNew) == 0 );
+    nRefsOld = pObjOld->nRefs;  
     Ivy_ObjOverwrite( pObjOld, pObjNew );
     pObjOld->nRefs = nRefsOld;
-    // update the hash table
-    Ivy_TableUpdate( pObjNew, pObjOld->Id );
-    // create the object that was taken over by pObjOld
-    Ivy_ObjClean( pObjNew );
-    // remember the entry
-    Vec_IntPush( Ivy_ObjMan(pObjOld)->vFree, pObjNew->Id );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the first real fanins (not a buffer/inverter).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin )
-{
-    if ( iFanin == 0 )
+    // patch the fanout of the fanins 
+    if ( p->vFanouts )
     {
-        if ( Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) )
-            return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin0(pNode), 0), Ivy_ObjFaninC0(pNode) );
-        else
-            return Ivy_ObjChild0(pNode);
-    }
-    else
-    {
-        if ( Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
-            return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin1(pNode), 0), Ivy_ObjFaninC1(pNode) );
-        else
-            return Ivy_ObjChild1(pNode);
+        Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld );
+        if ( Ivy_ObjFanin1(pObjOld) )
+        Ivy_ObjPatchFanout( p, Ivy_ObjFanin1(pObjOld), pObjNew, pObjOld );
     }
+    // update the hash table
+    Ivy_TableUpdate( p, pObjNew, pObjOld->Id );
+    // recycle the object that was taken over by pObjOld
+    Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
+    Ivy_ManRecycleMemory( p, pObjNew );
+    // if the new node is the buffer propagate it
+    if ( p->vFanouts && Ivy_ObjIsBuf(pObjOld) )
+        Vec_PtrPush( p->vBufs, pObjOld );
 }
 
 /**Function*************************************************************
@@ -304,19 +370,31 @@ Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode )
+void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode )
 {
     Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
-    assert( Ivy_ObjIsNode(pNode) );
+    if ( Ivy_ObjIsPo(pNode) )
+    {
+        if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) )
+            return;
+        pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
+        Ivy_ObjPatchFanin0( p, pNode, pFanReal0 );
+        return;
+    }
     if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
         return;
     // get the real fanins
-    pFanReal0 = Ivy_NodeRealFanin_rec( pNode, 0 );
-    pFanReal1 = Ivy_NodeRealFanin_rec( pNode, 1 );
+    pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) );
+    pFanReal1 = Ivy_ObjReal( Ivy_ObjChild1(pNode) );
     // get the new node
-    pResult = Ivy_Oper( pFanReal0, pFanReal1, Ivy_ObjType(pNode) );
+    if ( Ivy_ObjIsNode(pNode) )
+        pResult = Ivy_Oper( p, pFanReal0, pFanReal1, Ivy_ObjType(pNode) );
+    else if ( Ivy_ObjIsLatch(pNode) )
+        pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) );
+    else 
+        assert( 0 );
     // perform the replacement
-    Ivy_ObjReplace( pNode, pResult, 1, 0 ); 
+    Ivy_ObjReplace( p, pNode, pResult, 1, 0 ); 
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
index 96f78165..af216e45 100644
--- a/src/temp/ivy/ivyOper.c
+++ b/src/temp/ivy/ivyOper.c
@@ -57,12 +57,12 @@ static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
+Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
 {
     if ( Type == IVY_AND )
-        return Ivy_And( p0, p1 );
+        return Ivy_And( p, p0, p1 );
     if ( Type == IVY_EXOR )
-        return Ivy_Exor( p0, p1 );
+        return Ivy_Exor( p, p0, p1 );
     assert( 0 );
     return NULL;
 }
@@ -78,23 +78,22 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
 //    Ivy_Obj_t * pFan0, * pFan1;
     // check trivial cases
     if ( p0 == p1 )
         return p0;
     if ( p0 == Ivy_Not(p1) )
-        return Ivy_Not(pConst1);
-    if ( Ivy_Regular(p0) == pConst1 )
-        return p0 == pConst1 ? p1 : Ivy_Not(pConst1);
-    if ( Ivy_Regular(p1) == pConst1 )
-        return p1 == pConst1 ? p0 : Ivy_Not(pConst1);
+        return Ivy_Not(p->pConst1);
+    if ( Ivy_Regular(p0) == p->pConst1 )
+        return p0 == p->pConst1 ? p1 : Ivy_Not(p->pConst1);
+    if ( Ivy_Regular(p1) == p->pConst1 )
+        return p1 == p->pConst1 ? p0 : Ivy_Not(p->pConst1);
     // check if it can be an EXOR gate
 //    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
 //        return Ivy_CanonExor( pFan0, pFan1 );
-    return Ivy_CanonAnd( p0, p1 );
+    return Ivy_CanonAnd( p, p0, p1 );
 }
 
 /**Function*************************************************************
@@ -108,36 +107,22 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
+/*
     // check trivial cases
     if ( p0 == p1 )
-        return Ivy_Not(pConst1);
+        return Ivy_Not(p->pConst1);
     if ( p0 == Ivy_Not(p1) )
-        return pConst1;
-    if ( Ivy_Regular(p0) == pConst1 )
-        return Ivy_NotCond( p1, p0 == pConst1 );
-    if ( Ivy_Regular(p1) == pConst1 )
-        return Ivy_NotCond( p0, p1 == pConst1 );
+        return p->pConst1;
+    if ( Ivy_Regular(p0) == p->pConst1 )
+        return Ivy_NotCond( p1, p0 == p->pConst1 );
+    if ( Ivy_Regular(p1) == p->pConst1 )
+        return Ivy_NotCond( p0, p1 == p->pConst1 );
     // check the table
-    return Ivy_CanonExor( p0, p1 );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
-{
-    return Ivy_CanonLatch( pObj, Init );
+    return Ivy_CanonExor( p, p0, p1 );
+*/
+    return Ivy_Or( p, Ivy_And(p, p0, Ivy_Not(p1)), Ivy_And(p, Ivy_Not(p0), p1) );
 }
 
 /**Function*************************************************************
@@ -151,9 +136,9 @@ Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) );
+    return Ivy_Not( Ivy_And( p, Ivy_Not(p0), Ivy_Not(p1) ) );
 }
 
 /**Function*************************************************************
@@ -167,43 +152,42 @@ Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
+Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
     Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
     // consider trivial cases
     if ( p0 == Ivy_Not(p1) )
-        return Ivy_Exor( pC, p0 );
+        return Ivy_Exor( p, pC, p0 );
     // other cases can be added
     // implement the first MUX (F = C * x1 + C' * x0)
-    pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          p1, IVY_AND, IVY_INIT_NONE) );
-    pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
+    pTempA1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          p1, IVY_AND, IVY_INIT_NONE) );
+    pTempA2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
     if ( pTempA1 && pTempA2 )
     {
-        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
+        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
         if ( pTemp ) return Ivy_Not(pTemp);
     }
     Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
     // implement the second MUX (F' = C * x1' + C' * x0')
-    pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
-    pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
+    pTempB1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
+    pTempB2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
     if ( pTempB1 && pTempB2 )
     {
-        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
+        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
         if ( pTemp ) return pTemp;
     }
     Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
     // compare and decide which one to implement
     if ( Count0 >= Count1 )
     {
-        pTempA1 = pTempA1? pTempA1 : Ivy_And(pC,          p1);
-        pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0);
-        return Ivy_Or( pTempA1, pTempA2 );
+        pTempA1 = pTempA1? pTempA1 : Ivy_And(p, pC,          p1);
+        pTempA2 = pTempA2? pTempA2 : Ivy_And(p, Ivy_Not(pC), p0);
+        return Ivy_Or( p, pTempA1, pTempA2 );
     }
-    pTempB1 = pTempB1? pTempB1 : Ivy_And(pC,          Ivy_Not(p1));
-    pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0));
-    return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) );
+    pTempB1 = pTempB1? pTempB1 : Ivy_And(p, pC,          Ivy_Not(p1));
+    pTempB2 = pTempB2? pTempB2 : Ivy_And(p, Ivy_Not(pC), Ivy_Not(p0));
+    return Ivy_Not( Ivy_Or( p, pTempB1, pTempB2 ) );
 
 //    return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) );
 }
@@ -219,9 +203,9 @@ Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
+Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
 {
-    return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) );
+    return Ivy_Or( p, Ivy_Or(p, Ivy_And(p, pA, pB), Ivy_And(p, pA, pC)), Ivy_And(p, pB, pC) );
 }
 
 /**Function*************************************************************
@@ -235,16 +219,32 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs )
+Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs )
 {
     int i;
     assert( vPairs->nSize > 0 );
     assert( vPairs->nSize % 2 == 0 );
     // go through the cubes of the node's SOP
     for ( i = 0; i < vPairs->nSize; i += 2 )
-        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) );
+        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
     vPairs->nSize = vPairs->nSize/2;
-    return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
+    return Ivy_Not( Ivy_Multi_rec( p, (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init )
+{
+    return Ivy_CanonLatch( p, pObj, Init );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
index 2d65e7f7..804bdfb4 100644
--- a/src/temp/ivy/ivyResyn.c
+++ b/src/temp/ivy/ivyResyn.c
@@ -39,50 +39,59 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel )
+Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    int clk, fVerbose = 0;
+    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 );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
-if ( fVerbose ) Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+    Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 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 );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 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;
diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c
deleted file mode 100644
index 031db9bc..00000000
--- a/src/temp/ivy/ivyRewrite.c
+++ /dev/null
@@ -1,365 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyRewrite.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [AIG rewriting.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static unsigned    Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront );
-static void        Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone );
-static int         Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs Boolean rewriting of sequential AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
-{
-    Vec_Int_t * vNodes, * vFront, * vInside, * vTree;
-    Ivy_Obj_t * pNode, * pNodeNew, * pTemp;
-    int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs;
-    int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock();
-    unsigned uTruth;
-
-    nInputs  = 4;
-    vTree    = Vec_IntAlloc( 8 );
-    vFront   = Vec_IntAlloc( 8 );
-    vInside  = Vec_IntAlloc( 50 );
-    vNodes   = Ivy_ManDfs( p );
-    Ivy_ManForEachNodeVec( p, vNodes, pNode, i )
-    {
-        if ( Ivy_ObjIsBuf(pNode) )
-            continue;
-        // fix the fanin buffer problem
-        Ivy_NodeFixBufferFanins( pNode );
-        if ( Ivy_ObjIsBuf(pNode) )
-            continue;
-
-        // find one sequential cut rooted at this node
-clk = clock();
-        Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs );
-clkCut += clock() - clk;
-        // compute the truth table of the cut
-clk = clock();
-        uTruth = Ivy_ManSeqFindTruth( pNode, vFront );
-clkTru += clock() - clk;
-        // decompose the truth table
-clk = clock();
-        RetValue = Ivy_TruthDsd( uTruth, vTree );
-clkDsd += clock() - clk;
-        if ( !RetValue )
-            continue; // DSD does not exist
-//        Ivy_TruthDsdPrint( stdout, vTree );
-
-clk = clock();
-        // remember the cost of the current network
-        nCostOld = Ivy_ManGetCost(p);
-        // increment references of the cut variables
-        Vec_IntForEachEntry( vFront, Entry, k )
-        {
-            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
-            Ivy_ObjRefsInc( pTemp );
-        }
-        // dereference and record undo
-        nRefsSaved = pNode->nRefs; pNode->nRefs = 0;
-        Ivy_ManUndoStart( p );
-        Ivy_ObjDelete_rec( pNode, 0 );
-        Ivy_ManUndoStop( p );
-        pNode->nRefs = nRefsSaved;
-
-        // get the intermediate cost
-        nCostInt = Ivy_ManGetCost(p);
-
-//        printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt );
-
-        // construct the new logic cone
-        pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree );
-        // remember the cost
-        nCostNew = Ivy_ManGetCost(p);
-
-//        printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew );
-//        nCostNew = nCostNew;
-
-/*
-        if ( Ivy_Regular(pNodeNew)->nRefs == 0 )
-            Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 );
-        // get the intermediate cost
-        nCostInt2 = Ivy_ManGetCost(p);
-        assert( nCostInt == nCostInt2 );
-
-        Ivy_ManUndoPerform( p, pNode );
-        pNode->nRefs = nRefsSaved;
-
-        Vec_IntForEachEntry( vFront, Entry, k )
-        {
-//            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
-            pTemp = Ivy_ManObj(p, Entry);
-            Ivy_ObjRefsDec( pTemp );
-        }
-clkUpd += clock() - clk;
-        continue;
-*/
-
-        // detect the case when they are exactly the same
-//        if ( pNodeNew == pNode )
-//            continue;
-
-        // compare the costs
-        if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost )
-        { // accept the change
-//            printf( "NODES GAINED = %d\n", nCostOld - nCostNew );
-
-            Ivy_ObjReplace( pNode, pNodeNew, 0, 1 );
-            pNode->nRefs = nRefsSaved;
-        }
-        else
-        { // reject change
-//            printf( "Rejected\n" );
-
-            if ( Ivy_Regular(pNodeNew)->nRefs == 0 )
-                Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 );
-
-            // get the intermediate cost
-            nCostInt2 = Ivy_ManGetCost(p);
-            assert( nCostInt == nCostInt2 );
-
-            // reconstruct the old node
-            Ivy_ManUndoPerform( p, pNode );
-            pNode->nRefs = nRefsSaved;
-        }
-        // decrement references of the cut variables
-        Vec_IntForEachEntry( vFront, Entry, k )
-        {
-//            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
-            pTemp = Ivy_ManObj(p, Entry);
-            if ( Ivy_ObjIsNone(pTemp) )
-                continue;
-            Ivy_ObjRefsDec( pTemp );
-            if ( Ivy_ObjRefs(pTemp) == 0 )
-                Ivy_ObjDelete_rec( pTemp, 1 );
-        }
-
-clkUpd += clock() - clk;
-    }
-
-PRT( "Cut    ", clkCut );
-PRT( "Truth  ", clkTru );
-PRT( "DSD    ", clkDsd );
-PRT( "Update ", clkUpd );
-PRT( "TOTAL  ", clock() - clkStart );
-
-    Vec_IntFree( vTree  );
-    Vec_IntFree( vFront );
-    Vec_IntFree( vInside );
-    Vec_IntFree( vNodes );
-
-    if ( !Ivy_ManCheck(p) )
-    {
-        printf( "Ivy_ManSeqRewrite(): The check has failed.\n" );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth table of the sequential cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront )
-{
-    static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
-    unsigned uTruth0, uTruth1;
-    Ivy_Obj_t * pNode;
-    int nLatches, Number;
-    // consider the case of a constant
-    if ( Node == 0 )
-        return ~((unsigned)0);
-    // try to find this node in the frontier
-    Number = Vec_IntFind( vFront, Node );
-    if ( Number >= 0 )
-        return uMasks[Number];
-    // get the node
-    pNode = Ivy_ManObj( p, Ivy_LeafId(Node) );
-    assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) );
-    // get the number of latches
-    nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode);
-    // expand the first fanin
-    uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront );
-    if ( Ivy_ObjFaninC0(pNode) )
-        uTruth0 = ~uTruth0;
-    // quit if this is the one fanin node
-    if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
-        return uTruth0;
-    assert( Ivy_ObjIsNode(pNode) );
-    // expand the second fanin
-    uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront );
-    if ( Ivy_ObjFaninC1(pNode) )
-        uTruth1 = ~uTruth1;
-    // return the truth table
-    return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the truth table of the sequential cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront )
-{
-    assert( Ivy_ObjIsNode(pNode) );
-    return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively dereferences the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone )
-{
-    Ivy_Obj_t * pFan;
-    assert( !Ivy_IsComplement(pNode) );
-    assert( !Ivy_ObjIsNone(pNode) );
-    if ( Ivy_ObjIsPi(pNode) )
-        return;
-    // deref the first fanin
-    pFan = Ivy_ObjFanin0(pNode);
-    Ivy_ObjRefsDec( pFan );
-    if ( Ivy_ObjRefs( pFan ) == 0 )
-        Ivy_ManSeqDeref_rec( pFan, vCone );
-    // deref the second fanin
-    pFan = Ivy_ObjFanin1(pNode);
-    Ivy_ObjRefsDec( pFan );
-    if ( Ivy_ObjRefs( pFan ) == 0 )
-        Ivy_ManSeqDeref_rec( pFan, vCone );
-    // save the node
-    Vec_IntPush( vCone, pNode->Id );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively references the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode )
-{
-    Ivy_Obj_t * pFan;
-    assert( !Ivy_IsComplement(pNode) );
-    assert( !Ivy_ObjIsNone(pNode) );
-    if ( Ivy_ObjIsPi(pNode) )
-        return;
-    // ref the first fanin
-    pFan = Ivy_ObjFanin0(pNode);
-    if ( Ivy_ObjRefs( pFan ) == 0 )
-        Ivy_ManSeqRef_rec( pFan );
-    Ivy_ObjRefsInc( pFan );
-    // ref the second fanin
-    pFan = Ivy_ObjFanin1(pNode);
-    if ( Ivy_ObjRefs( pFan ) == 0 )
-        Ivy_ManSeqRef_rec( pFan );
-    Ivy_ObjRefsInc( pFan );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collect MFFC of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone )
-{
-    Vec_IntClear( vCone );
-    Ivy_ManSeqDeref_rec( pNode, vCone );
-    Ivy_ManSeqRef_rec( pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the cost of the logic cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone )
-{
-    Ivy_Obj_t * pObj;
-    int i, Cost = 0;
-    Ivy_ManForEachNodeVec( p, vCone, pObj, i )
-    {
-        if ( Ivy_ObjIsAnd(pObj) )
-            Cost += 1;
-        else if ( Ivy_ObjIsExor(pObj) )
-            Cost += 2;
-    }
-    return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
index 243ab261..d2a1697e 100644
--- a/src/temp/ivy/ivyRwrPre.c
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -27,13 +27,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums );
-static int Ivy_NodeMffcLabel( Ivy_Obj_t * pObj );
-static int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
-static Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, 
+static int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+static int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
+static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, 
     Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth );
 
-static int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
-static void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+static int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+static void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -58,29 +58,30 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
     int clk, clkStart = clock();
     // start the rewriting manager
     pManRwt = Rwt_ManStart( 0 );
+    p->pData = pManRwt;
     if ( pManRwt == NULL )
-        return 0;
+        return 0; 
+    // create fanouts
+    if ( fUpdateLevel && p->vFanouts == NULL )
+        Ivy_ManStartFanout( p );
     // compute the reverse levels if level update is requested
     if ( fUpdateLevel )
         Ivy_ManRequiredLevels( p );
+    // set the number of levels
+//    p->nLevelMax = Ivy_ManLevels( p );
     // resynthesize each node once
-    nNodes = Ivy_ManObjIdNext( p );
-    Ivy_ManForEachObj( p, pNode, i )
+    nNodes = Ivy_ManObjIdMax(p);
+    Ivy_ManForEachNode( p, pNode, i )
     {
-        if ( !Ivy_ObjIsNode(pNode) )
-            continue;
         // fix the fanin buffer problem
-        Ivy_NodeFixBufferFanins( pNode );
+        Ivy_NodeFixBufferFanins( p, pNode );
         if ( Ivy_ObjIsBuf(pNode) )
             continue;
         // stop if all nodes have been tried once
-        if ( i >= nNodes )
+        if ( i > nNodes )
             break;
-        // skip the nodes with many fanouts
-//        if ( Ivy_ObjRefs(pNode) > 1000 )
-//            continue;
         // for each cut, try to resynthesize it
-        nGain = Rwt_NodeRewrite( pManRwt, pNode, fUpdateLevel, fUseZeroCost );
+        nGain = Ivy_NodeRewrite( p, pManRwt, pNode, fUpdateLevel, fUseZeroCost );
         if ( nGain > 0 || nGain == 0 && fUseZeroCost )
         {
             Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
@@ -104,7 +105,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
             // complement the FF if needed
 clk = clock();
             if ( fCompl ) Dec_GraphComplement( pGraph );
-            Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+            Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain );
             if ( fCompl ) Dec_GraphComplement( pGraph );
 Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
         }
@@ -115,9 +116,12 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
         Rwt_ManPrintStats( pManRwt );
     // delete the managers
     Rwt_ManStop( pManRwt );
+    p->pData = NULL;
     // fix the levels
     if ( fUpdateLevel )
         Vec_IntFree( p->vRequired ), p->vRequired = NULL;
+//    else
+//        Ivy_ManResetLevels( p );
     // check
     if ( i = Ivy_ManCleanup(p) )
         printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
@@ -144,7 +148,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
   SeeAlso     []
 
 ***********************************************************************/
-int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost )
+int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost )
 {
     int fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
@@ -159,10 +163,10 @@ int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUs
 
     p->nNodesConsidered++;
     // get the required times
-    Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000;
+    Required = fUpdateLevel? Vec_IntEntry( pMan->vRequired, pNode->Id ) : 1000000;
     // get the node's cuts
 clk = clock();
-    pStore = Ivy_NodeFindCutsAll( pNode, 5 );
+    pStore = Ivy_NodeFindCutsAll( pMan, pNode, 5 );
 p->timeCut += clock() - clk;
 
     // go through the cuts
@@ -175,14 +179,10 @@ clk = clock();
             continue;
         // skip the cuts with buffers
         for ( i = 0; i < (int)pCut->nSize; i++ )
-            if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, pCut->pArray[i]) ) )
+            if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, pCut->pArray[i]) ) )
                 break;
         if ( i != pCut->nSize )
             continue;
-
-//        if ( pNode->Id == 82 )
-//            Ivy_NodePrintCut( pCut );
-
         // get the fanin permutation
 clk2 = clock();
         uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize );  // truth table
@@ -194,7 +194,7 @@ p->timeTruth += clock() - clk2;
         Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
         for ( i = 0; i < (int)pCut->nSize; i++ )
         {
-            pFanin = Ivy_ObjObj( pNode, pCut->pArray[pPerm[i]] );
+            pFanin = Ivy_ManObj( pMan, pCut->pArray[pPerm[i]] );
             assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) );
             pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
             Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
@@ -210,8 +210,8 @@ clk2 = clock();
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
         // label MFFC with current ID
-        Ivy_ManIncrementTravId( Ivy_ObjMan(pNode) );
-        nNodesSaved = Ivy_NodeMffcLabel( pNode );
+        Ivy_ManIncrementTravId( pMan );
+        nNodesSaved = Ivy_NodeMffcLabel( pMan, pNode );
         // unmark the fanin boundary
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
@@ -219,7 +219,7 @@ p->timeMffc += clock() - clk2;
 
         // evaluate the cut
 clk2 = clock();
-        pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+        pGraph = Rwt_CutEvaluate( pMan, p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
 p->timeEval += clock() - clk2;
 
         // check if the cut is better than the current best one
@@ -301,13 +301,13 @@ p->timeRes += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
+int Ivy_NodeRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel )
 {
     Ivy_Obj_t * pNode0, * pNode1;
     int Counter;
     // label visited nodes
     if ( fLabel )
-        Ivy_ObjSetTravIdCurrent( pNode );
+        Ivy_ObjSetTravIdCurrent( p, pNode );
     // skip the CI
     if ( Ivy_ObjIsCi(pNode) )
         return 0;
@@ -319,18 +319,18 @@ int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
     if ( fReference )
     {
         if ( pNode0->nRefs++ == 0 )
-            Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
-        if ( Ivy_ObjIsNode(pNode) && pNode1->nRefs++ == 0 )
-            Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+            Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
+        if ( pNode1 && pNode1->nRefs++ == 0 )
+            Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
     }
     else
     {
         assert( pNode0->nRefs > 0 );
-        assert( pNode1->nRefs > 0 );
+        assert( pNode1 == NULL || pNode1->nRefs > 0 );
         if ( --pNode0->nRefs == 0 )
-            Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
-        if ( Ivy_ObjIsNode(pNode) && --pNode1->nRefs == 0 )
-            Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+            Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel );
+        if ( pNode1 && --pNode1->nRefs == 0 )
+            Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel );
     }
     return Counter;
 }
@@ -346,13 +346,13 @@ int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_NodeMffcLabel( Ivy_Obj_t * pNode )
+int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode )
 {
     int nConeSize1, nConeSize2;
     assert( !Ivy_IsComplement( pNode ) );
     assert( Ivy_ObjIsNode( pNode ) );
-    nConeSize1 = Ivy_NodeRefDeref( pNode, 0, 1 ); // dereference
-    nConeSize2 = Ivy_NodeRefDeref( pNode, 1, 0 ); // reference
+    nConeSize1 = Ivy_NodeRefDeref( p, pNode, 0, 1 ); // dereference
+    nConeSize2 = Ivy_NodeRefDeref( p, pNode, 1, 0 ); // reference
     assert( nConeSize1 == nConeSize2 );
     assert( nConeSize1 > 0 );
     return nConeSize1;
@@ -418,7 +418,7 @@ unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
   SeeAlso     []
 
 ***********************************************************************/
-Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
+Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
 {
     Vec_Ptr_t * vSubgraphs;
     Dec_Graph_t * pGraphBest, * pGraphCur;
@@ -437,7 +437,7 @@ Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCu
         Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
             Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
         // detect how many unlabeled nodes will be reused
-        nNodesAdded = Ivy_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax );
+        nNodesAdded = Ivy_GraphToNetworkCount( pMan, pRoot, pGraphCur, nNodesSaved, LevelMax );
         if ( nNodesAdded == -1 )
             continue;
         assert( nNodesSaved >= nNodesAdded );
@@ -469,7 +469,7 @@ Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCu
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
 {
     Dec_Node_t * pNode, * pNode0, * pNode1;
     Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
@@ -495,7 +495,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
             // if they are both present, find the resulting node
             pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
             pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
-            pAnd  = Ivy_TableLookup( Ivy_ObjCreateGhost(pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
+            pAnd  = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
             // return -1 if the node is the same as the original root
             if ( Ivy_Regular(pAnd) == pRoot )
                 return -1;
@@ -503,7 +503,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
         else
             pAnd = NULL;
         // count the number of added nodes
-        if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) )
+        if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) )
         {
             if ( ++Counter > NodeMax )
                 return -1;
@@ -512,7 +512,7 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
         LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level );
         if ( pAnd )
         {
-            if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) )
+            if ( Ivy_Regular(pAnd) == p->pConst1 )
                 LevelNew = 0;
             else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) )
                 LevelNew = (int)Ivy_Regular(pAnd0)->Level;
@@ -541,14 +541,14 @@ int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * p, Dec_Graph_t * pGraph )
 {
     Ivy_Obj_t * pAnd0, * pAnd1;
     Dec_Node_t * pNode;
     int i;
     // check for constant function
     if ( Dec_GraphIsConst(pGraph) )
-        return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+        return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) );
     // check for a literal
     if ( Dec_GraphIsVar(pGraph) )
         return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
@@ -557,7 +557,7 @@ Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
     {
         pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
         pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
-        pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+        pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 );
     }
     // complement the result if necessary
     return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
@@ -574,18 +574,96 @@ Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
+void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
 {
     Ivy_Obj_t * pRootNew;
-    int nNodesNew, nNodesOld;
-    nNodesOld = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+    int nNodesNew, nNodesOld, Required;
+    Required = fUpdateLevel? Vec_IntEntry( p->vRequired, pRoot->Id ) : 1000000;
+    nNodesOld = Ivy_ManNodeNum(p);
     // create the new structure of nodes
-    pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph );
+    pRootNew = Ivy_GraphToNetwork( p, pGraph );
+    assert( (int)Ivy_Regular(pRootNew)->Level <= Required );
+//    if ( Ivy_Regular(pRootNew)->Level == Required )
+//        printf( "Difference %d.\n", Ivy_Regular(pRootNew)->Level - Required );
     // remove the old nodes
 //    Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel );
-    Ivy_ObjReplace( pRoot, pRootNew, 1, 0 );
+/*
+    if ( Ivy_IsComplement(pRootNew) )
+        printf( "c" );
+    else
+        printf( "d" );
+    if ( Ivy_ObjRefs(Ivy_Regular(pRootNew)) > 0 )
+        printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
+    printf( " " );
+*/
+    Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0 );
+    // compare the gains
+    nNodesNew = Ivy_ManNodeNum(p);
+    assert( nGain <= nNodesOld - nNodesNew );
+    // propagate the buffer
+    Ivy_ManPropagateBuffers( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetwork3( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
+{
+    Ivy_Obj_t * pRootNew, * pFanin;
+    int nNodesNew, nNodesOld, i, nRefsOld;
+    nNodesOld = Ivy_ManNodeNum(p);
+
+//printf( "Before = %d. ", Ivy_ManNodeNum(p) );
+    // mark the cut
+    Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i )
+        Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
+    // deref the old cone
+    nRefsOld = pRoot->nRefs;  
+    pRoot->nRefs = 0;
+    Ivy_ObjDelete_rec( p, pRoot, 0 );
+    pRoot->nRefs = nRefsOld;
+    // unmark the cut
+    Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i )
+        Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+//printf( "Deref = %d. ", Ivy_ManNodeNum(p) );
+ 
+    // create the new structure of nodes
+    pRootNew = Ivy_GraphToNetwork( p, pGraph );
+//printf( "Create = %d. ", Ivy_ManNodeNum(p) );
+    // remove the old nodes
+//    Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel );
+/*
+    if ( Ivy_IsComplement(pRootNew) )
+        printf( "c" );
+    else
+        printf( "d" );
+    if ( Ivy_ObjRefs(Ivy_Regular(pRootNew)) > 0 )
+        printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) );
+    printf( " " );
+*/
+    Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0 );
+//printf( "Replace = %d. ", Ivy_ManNodeNum(p) );
+
+    // delete remaining dangling nodes
+    Vec_PtrForEachEntry( ((Rwt_Man_t *)p->pData)->vFanins, pFanin, i )
+    {
+        pFanin = Ivy_Regular(pFanin);
+        if ( !Ivy_ObjIsNone(pFanin) && Ivy_ObjRefs(pFanin) == 0 )
+            Ivy_ObjDelete_rec( p, pFanin, 1 );
+    }
+//printf( "Deref = %d. ", Ivy_ManNodeNum(p) );
+//printf( "\n" );
+
     // compare the gains
-    nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+    nNodesNew = Ivy_ManNodeNum(p);
     assert( nGain <= nNodesOld - nNodesNew );
 }
 
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index d8fbdd9b..1cfa8c4b 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -24,13 +24,33 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Converts a combinational AIG manager into a sequential one.]
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives new cut.]
 
   Description []
                
@@ -39,59 +59,360 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches )
+static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 )
 {
-    Vec_Int_t * vNodes;
-    Ivy_Obj_t * pObj, * pObjNew, * pFan0, * pFan1;
-    int i, fChanges;
-    assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) );
-    // change POs into buffers
-    assert( Ivy_ManPoNum(p) == Vec_IntSize(p->vPos) );
-    for ( i = Ivy_ManPoNum(p) - nLatches; i < Vec_IntSize(p->vPos); i++ )
+    unsigned uHash = 0;
+    int i, k;
+    assert( pCut->nSize > 0 );
+    assert( IdNew0 < IdNew1 );
+    for ( i = k = 0; i < pCut->nSize; i++ )
     {
-        pObj = Ivy_ManPo(p, i);
-        pObj->Type = IVY_BUF;
+        if ( pCut->pArray[i] == IdOld )
+            continue;
+        if ( IdNew0 >= 0 )
+        {
+            if ( IdNew0 <= pCut->pArray[i] )
+            {
+                if ( IdNew0 < pCut->pArray[i] )
+                {
+                    if ( k == pCut->nSizeMax )
+                        return 0;
+                    pCutNew->pArray[ k++ ] = IdNew0;
+                    uHash |= Ivy_CutHashValue( IdNew0 );
+                }
+                IdNew0 = -1;
+            }
+        }
+        if ( IdNew1 >= 0 )
+        {
+            if ( IdNew1 <= pCut->pArray[i] )
+            {
+                if ( IdNew1 < pCut->pArray[i] )
+                {
+                    if ( k == pCut->nSizeMax )
+                        return 0;
+                    pCutNew->pArray[ k++ ] = IdNew1;
+                    uHash |= Ivy_CutHashValue( IdNew1 );
+                }
+                IdNew1 = -1;
+            }
+        }
+        if ( k == pCut->nSizeMax )
+            return 0;
+        pCutNew->pArray[ k++ ] = pCut->pArray[i];
+        uHash |= Ivy_CutHashValue( pCut->pArray[i] );
     }
-    // change PIs into latches and connect them to the corresponding POs
-    assert( Ivy_ManPiNum(p) == Vec_IntSize(p->vPis) );
-    for ( i = Ivy_ManPiNum(p) - nLatches; i < Vec_IntSize(p->vPis); i++ )
+    if ( IdNew0 >= 0 )
     {
-        pObj = Ivy_ManPi(p, i);
-        pObj->Type = IVY_LATCH;
-        Ivy_ObjConnect( pObj, Ivy_ManPo(p, Ivy_ManPoNum(p) - Ivy_ManPiNum(p)) );
+        if ( k == pCut->nSizeMax )
+            return 0;
+        pCutNew->pArray[ k++ ] = IdNew0;
+        uHash |= Ivy_CutHashValue( IdNew0 );
     }
-    // shrink the array
-    Vec_IntShrink( p->vPis, Ivy_ManPiNum(p) - nLatches );
-    Vec_IntShrink( p->vPos, Ivy_ManPoNum(p) - nLatches );
-    // update the counters of different objects
-    p->nObjs[IVY_PI] -= nLatches;
-    p->nObjs[IVY_PO] -= nLatches;
-    p->nObjs[IVY_BUF] += nLatches;
-    p->nObjs[IVY_LATCH] += nLatches;
-    // perform structural hashing while there are changes
-    fChanges = 1;
-    while ( fChanges )
+    if ( IdNew1 >= 0 )
     {
-        fChanges = 0;
-        vNodes = Ivy_ManDfs( p );
-        Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        if ( k == pCut->nSizeMax )
+            return 0;
+        pCutNew->pArray[ k++ ] = IdNew1;
+        uHash |= Ivy_CutHashValue( IdNew1 );
+    }
+    pCutNew->nSize = k;
+    pCutNew->uHash = uHash;
+    assert( pCutNew->nSize <= pCut->nSizeMax );
+    for ( i = 1; i < pCutNew->nSize; i++ )
+        assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_CutCheckDominance( Ivy_Cut_t * pDom, Ivy_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < pDom->nSize; i++ )
+    {
+        assert( i==0 || pDom->pArray[i-1] < pDom->pArray[i] );
+        for ( k = 0; k < pCut->nSize; k++ )
+            if ( pDom->pArray[i] == pCut->pArray[k] )
+                break;
+        if ( k == pCut->nSize ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the cut exists.]
+
+  Description [Returns 1 if the cut exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CutFindOrAddFilter( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew )
+{
+    Ivy_Cut_t * pCut;
+    int i, k;
+    assert( pCutNew->uHash );
+    // try to find the cut
+    for ( i = 0; i < pCutStore->nCuts; i++ )
+    {
+        pCut = pCutStore->pCuts + i;
+        if ( pCut->nSize == 0 )
+            continue;
+        if ( pCut->nSize == pCutNew->nSize )
+        {
+            if ( pCut->uHash == pCutNew->uHash )
+            {
+                for ( k = 0; k < pCutNew->nSize; k++ )
+                    if ( pCut->pArray[k] != pCutNew->pArray[k] )
+                        break;
+                if ( k == pCutNew->nSize )
+                    return 1;
+            }
+            continue;
+        }
+        if ( pCut->nSize < pCutNew->nSize )
         {
-            if ( Ivy_ObjIsBuf(pObj) )
+            // skip the non-contained cuts
+            if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
                 continue;
-            pFan0 = Ivy_NodeRealFanin_rec( pObj, 0 );
-            pFan1 = Ivy_NodeRealFanin_rec( pObj, 1 );
-            if ( Ivy_ObjIsAnd(pObj) )
-                pObjNew = Ivy_And(pFan0, pFan1);
-            else if ( Ivy_ObjIsExor(pObj) )
-                pObjNew = Ivy_Exor(pFan0, pFan1);
-            else assert( 0 );
-            if ( pObjNew == pObj )
+            // check containment seriously
+            if ( Ivy_CutCheckDominance( pCut, pCutNew ) )
+                return 1;
+            continue;
+        }
+        // check potential containment of other cut
+
+        // skip the non-contained cuts
+        if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash )
+            continue;
+        // check containment seriously
+        if ( Ivy_CutCheckDominance( pCutNew, pCut ) )
+        {
+            // remove the current cut
+            pCut->nSize = 0;
+        }
+    }
+    assert( pCutStore->nCuts < pCutStore->nCutsMax );
+    // add the cut
+    pCut = pCutStore->pCuts + pCutStore->nCuts++;
+    *pCut = *pCutNew;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compresses the cut representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_CutCompactAll( Ivy_Store_t * pCutStore )
+{
+    Ivy_Cut_t * pCut;
+    int i, k;
+    pCutStore->nCutsM = 0;
+    for ( i = k = 0; i < pCutStore->nCuts; i++ )
+    {
+        pCut = pCutStore->pCuts + i;
+        if ( pCut->nSize == 0 )
+            continue;
+        if ( pCut->nSize < pCut->nSizeMax )
+            pCutStore->nCutsM++;
+        pCutStore->pCuts[k++] = *pCut;
+    }
+    pCutStore->nCuts = k;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_CutPrintForNode( Ivy_Cut_t * pCut )
+{
+    int i;
+    assert( pCut->nSize > 0 );
+    printf( "%d : {", pCut->nSize );
+    for ( i = 0; i < pCut->nSize; i++ )
+        printf( " %d", pCut->pArray[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore )
+{
+    int i;
+    printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
+    for ( i = 0; i < pCutStore->nCuts; i++ )
+        Ivy_CutPrintForNode( pCutStore->pCuts + i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin )
+{
+    assert( !Ivy_IsComplement(pFanin) );
+    if ( !Ivy_ObjIsLatch(pFanin) )
+        return Ivy_LeafCreate( pFanin->Id, 0 );
+    return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves )
+{
+    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
+    Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
+    Ivy_Man_t * pMan = p;
+    Ivy_Obj_t * pLeaf;
+    int i, k, Temp, nLats, iLeaf0, iLeaf1;
+
+    assert( nLeaves <= IVY_CUT_INPUT );
+
+    // start the structure
+    pCutStore->nCuts = 0;
+    pCutStore->nCutsMax = IVY_CUT_LIMIT;
+    // start the trivial cut
+    pCutNew->uHash = 0;
+    pCutNew->nSize = 1;
+    pCutNew->nSizeMax = nLeaves;
+    pCutNew->pArray[0] = Ivy_LeafCreate( pObj->Id, 0 );
+    pCutNew->uHash = Ivy_CutHashValue( pCutNew->pArray[0] );
+    // add the trivial cut
+    pCutStore->pCuts[pCutStore->nCuts++] = *pCutNew;
+    assert( pCutStore->nCuts == 1 );
+
+    // explore the cuts
+    for ( i = 0; i < pCutStore->nCuts; i++ )
+    {
+        // expand this cut
+        pCut = pCutStore->pCuts + i;
+        if ( pCut->nSize == 0 )
+            continue;
+        for ( k = 0; k < pCut->nSize; k++ )
+        {
+            pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) );
+            if ( Ivy_ObjIsCi(pLeaf) )
                 continue;
-            Ivy_ObjReplace( pObj, pObjNew, 1, 1 );
-            fChanges = 1;
+            assert( Ivy_ObjIsNode(pLeaf) );
+            nLats = Ivy_LeafLat(pCut->pArray[k]);
+            // get the fanins fanins
+            iLeaf0 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) );
+            iLeaf1 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) );
+            if ( iLeaf0 > iLeaf1 )
+                Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp;
+            // create the new cut
+            if ( !Ivy_CutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ) )
+                continue;
+            // add the cut
+            Ivy_CutFindOrAddFilter( pCutStore, pCutNew );
+            if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+                break;
         }
-        Vec_IntFree( vNodes );
+        if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+            break;
+    }
+    if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+        pCutStore->fSatur = 1;
+    else
+        pCutStore->fSatur = 0;
+//    printf( "%d ", pCutStore->nCuts );
+    Ivy_CutCompactAll( pCutStore );
+//    printf( "%d \n", pCutStore->nCuts );
+//    Ivy_CutPrintForNodes( pCutStore );
+    return pCutStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs )
+{
+    Ivy_Store_t * pStore;
+    Ivy_Obj_t * pObj;
+    int i, nCutsTotal, nCutsTotalM, nNodeTotal, nNodeOver;
+    int clk = clock();
+    if ( nInputs > IVY_CUT_INPUT )
+    {
+        printf( "Cannot compute cuts for more than %d inputs.\n", IVY_CUT_INPUT );
+        return;
+    }
+    nNodeTotal = nNodeOver = 0;
+    nCutsTotal = nCutsTotalM = -Ivy_ManNodeNum(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        pStore = Ivy_CutComputeForNode( p, pObj, nInputs );
+        nCutsTotal  += pStore->nCuts;
+        nCutsTotalM += pStore->nCutsM;
+        nNodeOver   += pStore->fSatur;
+        nNodeTotal++;
     }
+    printf( "All = %6d. Minus = %6d. Triv = %6d.   Node = %6d. Satur = %6d.  ", 
+        nCutsTotal, nCutsTotalM, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
+    PRT( "Time", clock() - clk );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
index 815caa29..f2617699 100644
--- a/src/temp/ivy/ivyTable.c
+++ b/src/temp/ivy/ivyTable.c
@@ -12,7 +12,7 @@
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - May 11, 2006.]
+  Date        [Ver. 1.0. Started - May 11, 2006. ]
 
   Revision    [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
@@ -37,22 +37,23 @@ static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize )
 }
 
 // returns the place where this node is stored (or should be stored)
-static int * Ivy_TableFind( Ivy_Obj_t * pObj )
+static int * Ivy_TableFind( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     int i;
     assert( Ivy_ObjIsHash(pObj) );
-    p = Ivy_ObjMan(pObj);
     for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
         if ( p->pTable[i] == pObj->Id )
             break;
     return p->pTable + i;
 }
 
+static void         Ivy_TableResize( Ivy_Man_t * p );
+static unsigned int Cudd_PrimeAig( unsigned int  p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Checks if node with the given attributes is in the hash table.]
@@ -64,27 +65,25 @@ static int * Ivy_TableFind( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj )
+Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     Ivy_Obj_t * pEntry;
     int i;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return NULL;
     assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
-    assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) );
-    p = Ivy_ObjMan(pObj);
+    assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) );
+//    if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
+//        return NULL;
     for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
     {
-        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
-        if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && 
-             Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && 
-             Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && 
-             Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && 
+        pEntry = Ivy_ManObj( p, p->pTable[i] );
+        if ( Ivy_ObjChild0(pEntry) == Ivy_ObjChild0(pObj) && 
+             Ivy_ObjChild1(pEntry) == Ivy_ObjChild1(pObj) && 
              Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && 
              Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) )
-            return Ivy_ObjObj( pObj, p->pTable[i] );
+            return pEntry;
     }
     return NULL;
 }
@@ -100,13 +99,18 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableInsert( Ivy_Obj_t * pObj )
+void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
     int * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    if ( (pObj->Id & 63) == 0 )
+    {
+        if ( p->nTableSize < 2 * Ivy_ManHashObjNum(p) )
+            Ivy_TableResize( p );
+    }
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == 0 );
     *pPlace = pObj->Id;
 }
@@ -122,25 +126,23 @@ void Ivy_TableInsert( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableDelete( Ivy_Obj_t * pObj )
+void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     Ivy_Obj_t * pEntry;
     int i, * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == pObj->Id ); // node should be in the table
     *pPlace = 0;
     // rehash the adjacent entries
-    p = Ivy_ObjMan(pObj);
     i = pPlace - p->pTable;
     for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
     {
-        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
+        pEntry = Ivy_ManObj( p, p->pTable[i] );
         p->pTable[i] = 0;
-        Ivy_TableInsert( pEntry );
+        Ivy_TableInsert( p, pEntry );
     }
 }
 
@@ -157,13 +159,13 @@ void Ivy_TableDelete( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew )
+void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew )
 {
     int * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == pObj->Id ); // node should be in the table
     *pPlace = ObjIdNew;
 }
@@ -202,13 +204,12 @@ void Ivy_TableResize( Ivy_Man_t * p )
 {
     int * pTableOld, * pPlace;
     int nTableSizeOld, Counter, e, clk;
-    assert( 0 );
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
     // get the new table
-    p->nTableSize = p->nObjsAlloc*5/2+13; 
+    p->nTableSize = Cudd_PrimeAig( 5 * Ivy_ManHashObjNum(p) ); 
     p->pTable = ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
     // rehash the entries from the old table
@@ -219,17 +220,79 @@ clk = clock();
             continue;
         Counter++;
         // get the place where this entry goes in the table table
-        pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) );
+        pPlace = Ivy_TableFind( p, Ivy_ManObj(p, pTableOld[e]) );
         assert( *pPlace == 0 ); // should not be in the table
         *pPlace = pTableOld[e];
     }
     assert( Counter == Ivy_ManHashObjNum(p) );
-//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
 //    PRT( "Time", clock() - clk );
     // replace the table and the parameters
-    free( p->pTable );
+    free( pTableOld );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Ivy_TableProfile( Ivy_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+    {
+        if ( p->pTable[i] )
+            Counter++;
+        else if ( Counter )
+        {
+            printf( "%d ", Counter );
+            Counter = 0;
+        }
+    }
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Returns the next prime &gt;= p.]
+
+  Description [Copied from CUDD, for stand-aloneness.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+unsigned int Cudd_PrimeAig( unsigned int  p)
+{
+    int i,pn;
+
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyUndo.c b/src/temp/ivy/ivyUndo.c
deleted file mode 100644
index 6612bf42..00000000
--- a/src/temp/ivy/ivyUndo.c
+++ /dev/null
@@ -1,165 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivyUndo.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Recording the results of recent deletion of logic cone.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoStart( Ivy_Man_t * p )
-{
-    p->fRecording = 1;
-    p->nUndos = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoStop( Ivy_Man_t * p )
-{
-    p->fRecording = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj )
-{
-    Ivy_Obj_t * pObjUndo;
-    if ( p->nUndos >= p->nUndosAlloc )
-    {
-        printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" );
-        return;
-    }
-    pObjUndo = p->pUndos + p->nUndos++;
-    // required data for Ivy_ObjCreateGhost()
-    pObjUndo->Type    = pObj->Type;
-    pObjUndo->Init    = pObj->Init;
-    pObjUndo->Fanin0  = pObj->Fanin0;
-    pObjUndo->Fanin1  = pObj->Fanin1;
-    pObjUndo->fComp0  = pObj->fComp0;
-    pObjUndo->fComp1  = pObj->fComp1;
-    // additional data
-    pObjUndo->Id      = pObj->Id;
-    pObjUndo->nRefs   = pObj->nRefs;
-    pObjUndo->Level   = pObj->Level;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Vec_IntPutLast( Vec_Int_t * vFree, int Last )
-{
-    int Place, i;
-    // find the entry
-    Place = Vec_IntFind( vFree, Last );
-    if ( Place == -1 )
-        return 0;
-    // shift entries by one
-    assert( vFree->pArray[Place] == Last );
-    for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ )
-        vFree->pArray[i] = vFree->pArray[i+1];
-    // put the entry in the end
-    vFree->pArray[i] = Last;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot )
-{
-    Ivy_Obj_t * pObjUndo, * pObjNew;
-    int i;
-    assert( p->nUndos > 0 );
-    assert( p->fRecording == 0 );
-    for ( i = p->nUndos - 1; i >= 0; i-- )
-    {
-        // get the undo object
-        pObjUndo = p->pUndos + i;
-        // if this is the last object
-        if ( i == 0 )
-            Vec_IntPush( p->vFree, pRoot->Id );
-        else
-            Vec_IntPutLast( p->vFree, pObjUndo->Id );
-        // create the new object
-        pObjNew  = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) );
-        pObjNew->nRefs = pObjUndo->nRefs;
-        pObjNew->Level = pObjUndo->Level;
-        // make sure the object is created in the same place as before
-        assert( pObjNew->Id == pObjUndo->Id );
-    }
-    p->nUndos = 0;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 3d1ac335..3b77bf41 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -68,136 +68,6 @@ void Ivy_ManCleanTravId( Ivy_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    // check that the node is regular
-    assert( !Ivy_IsComplement(pNode) );
-    // if the node is not AND, this is not MUX
-    if ( !Ivy_ObjIsAnd(pNode) )
-        return 0;
-    // if the children are not complemented, this is not MUX
-    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
-        return 0;
-    // get children
-    pNode0 = Ivy_ObjFanin0(pNode);
-    pNode1 = Ivy_ObjFanin1(pNode);
-    // if the children are not ANDs, this is not MUX
-    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
-        return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
-    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
-           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
-           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
-           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
-
-  Description [If the node is a MUX, returns the control variable C.
-  Assigns nodes T and E to be the then and else variables of the MUX. 
-  Node C is never complemented. Nodes T and E can be complemented.
-  This function also recognizes EXOR/NEXOR gates as MUXes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    assert( !Ivy_IsComplement(pNode) );
-    assert( Ivy_ObjIsMuxType(pNode) );
-    // get children
-    pNode0 = Ivy_ObjFanin0(pNode);
-    pNode1 = Ivy_ObjFanin1(pNode);
-    // find the control variable
-//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
-    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Ivy_ObjFaninC0(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            return Ivy_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            return Ivy_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
-    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Ivy_ObjFaninC0(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            return Ivy_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            return Ivy_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
-    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Ivy_ObjFaninC1(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            return Ivy_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            return Ivy_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
-    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Ivy_ObjFaninC1(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            return Ivy_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            return Ivy_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    assert( 0 ); // this is not MUX
-    return NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes truth table of the cut.]
 
   Description []
@@ -207,14 +77,14 @@ Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Ob
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
+void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
 {
     if ( pNode->fMarkA )
         return;
     pNode->fMarkA = 1;
     assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) );
-    Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes );
-    Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes );
+    Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes );
+    Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes );
     Vec_IntPush( vNodes, pNode->Id );
 }
 
@@ -230,7 +100,7 @@ void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
 {
     int i, Leaf;
     // collect and mark the leaves
@@ -238,13 +108,13 @@ void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNod
     Vec_IntForEachEntry( vLeaves, Leaf, i )
     {
         Vec_IntPush( vNodes, Leaf );
-        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1;
+        Ivy_ManObj(p, Leaf)->fMarkA = 1;
     }
     // collect and mark the nodes
-    Ivy_ManCollectCut_rec( pRoot, vNodes );
+    Ivy_ManCollectCut_rec( p, pRoot, vNodes );
     // clean the nodes
     Vec_IntForEachEntry( vNodes, Leaf, i )
-        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0;
+        Ivy_ManObj(p, Leaf)->fMarkA = 0;
 }
 
 /**Function*************************************************************
@@ -274,7 +144,7 @@ unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
+void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
 {
     unsigned * pTruth, * pTruth0, * pTruth1;
     int i;
@@ -310,7 +180,7 @@ void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
+unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
 {
     static unsigned uTruths[8][8] = { // elementary truth tables
         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
@@ -324,10 +194,10 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t *
     };
     int i, Leaf;
     // collect the cut
-    Ivy_ManCollectCut( pRoot, vLeaves, vNodes );
+    Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes );
     // set the node numbers
     Vec_IntForEachEntry( vNodes, Leaf, i )
-        Ivy_ObjObj(pRoot, Leaf)->TravId = i;
+        Ivy_ManObj(p, Leaf)->TravId = i;
     // alloc enough memory
     Vec_IntClear( vTruth );
     Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
@@ -336,7 +206,7 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t *
         memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
     // compute truths for other nodes
     Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
-        Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 );
+        Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 );
     return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
 }
 
@@ -373,21 +243,18 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManReadLevels( Ivy_Man_t * p )
+int Ivy_ManLevels( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj;
     int i, LevelMax = 0;
     Ivy_ManForEachPo( p, pObj, i )
-    {
-        pObj = Ivy_ObjFanin0(pObj);
-        LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
-    }
+        LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
     return LevelMax;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the real fanin.]
+  Synopsis    [Collect the latches.]
 
   Description []
                
@@ -396,20 +263,42 @@ int Ivy_ManReadLevels( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
+int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
 {
-    Ivy_Obj_t * pFanin;
-    if ( !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
-        return pObj;
-    pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
-    return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
+    if ( pObj->Level || Ivy_ObjIsCi(pObj) )
+        return pObj->Level;
+    if ( Ivy_ObjIsBuf(pObj) )
+        return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+    Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) );
+    return pObj->Level = Ivy_ObjLevelNew( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect the latches.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManResetLevels( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->Level = 0;
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the cube has exactly one 1.]
+  Synopsis    [Recursively updates fanout levels.]
 
   Description []
                
@@ -418,14 +307,33 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthHasOneOne( unsigned uCube )
+void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    return (uCube & (uCube - 1)) == 0;
+    Ivy_Obj_t * pFanout;
+    Vec_Ptr_t * vFanouts;
+    int i, LevelNew;
+    assert( p->vFanouts );
+    assert( Ivy_ObjIsNode(pObj) );
+    vFanouts = Vec_PtrAlloc( 10 );
+    Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
+    {
+        if ( Ivy_ObjIsCo(pFanout) )
+        {
+//            assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax );
+            continue;
+        }
+        LevelNew = Ivy_ObjLevelNew( pFanout );
+        if ( (int)pFanout->Level == LevelNew )
+            continue;
+        pFanout->Level = LevelNew;
+        Ivy_ObjUpdateLevel_rec( p, pFanout );
+    }
+    Vec_PtrFree( vFanouts );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if two cubes are distance-1.]
+  Synopsis    [Compute the new required level.]
 
   Description []
                
@@ -434,15 +342,25 @@ static inline int Ivy_TruthHasOneOne( unsigned uCube )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
+int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    unsigned uTemp = uCube1 | uCube2;
-    return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 );
+    Ivy_Obj_t * pFanout;
+    Vec_Ptr_t * vFanouts;
+    int i, Required, LevelNew = 1000000;
+    assert( p->vFanouts && p->vRequired );
+    vFanouts = Vec_PtrAlloc( 10 );
+    Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
+    {
+        Required = Vec_IntEntry(p->vRequired, pFanout->Id);
+        LevelNew = IVY_MIN( LevelNew, Required );
+    }
+    Vec_PtrFree( vFanouts );
+    return LevelNew - 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if two cubes differ in only one literal.]
+  Synopsis    [Recursively updates fanout levels.]
 
   Description []
                
@@ -451,15 +369,33 @@ static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
+void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew )
 {
-    unsigned uTemp = uCube1 ^ uCube2;
-    return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 );
+    Ivy_Obj_t * pFanin;
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+        return;
+    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+    // process the first fanin
+    pFanin = Ivy_ObjFanin0(pObj);
+    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
+    {
+        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
+        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
+    }
+    if ( Ivy_ObjIsBuf(pObj) )
+        return;
+    // process the second fanin
+    pFanin = Ivy_ObjFanin1(pObj);
+    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
+    {
+        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
+        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Combines two distance 1 cubes.]
+  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
 
   Description []
                
@@ -468,95 +404,128 @@ static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
   SeeAlso     []
 
 ***********************************************************************/
-static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 )
+int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
 {
-    unsigned uTemp;
-    uTemp = uCube1 | uCube2;
-    uTemp &= (uTemp >> 1) & 0x55555555;
-    assert( Ivy_TruthHasOneOne(uTemp) );
-    uTemp |= (uTemp << 1);
-    return (uCube1 | uCube2) ^ uTemp;
+    Ivy_Obj_t * pNode0, * pNode1;
+    // check that the node is regular
+    assert( !Ivy_IsComplement(pNode) );
+    // if the node is not AND, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode) )
+        return 0;
+    // if the children are not complemented, this is not MUX
+    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
+        return 0;
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // if the children are not ANDs, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
+        return 0;
+    // otherwise the node is MUX iff it has a pair of equal grandchildren
+    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
+           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Estimates the number of AIG nodes in the truth table.]
+  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
 
-  Description []
+  Description [If the node is a MUX, returns the control variable C.
+  Assigns nodes T and E to be the then and else variables of the MUX. 
+  Node C is never complemented. Nodes T and E can be complemented.
+  This function also recognizes EXOR/NEXOR gates as MUXes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
+Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
 {
-    static unsigned short uResult[256];
-    static unsigned short uCover[81*81];
-    static char pVarCount[81*81];
-    int nMints, uCube, uCubeNew, i, k, c, nCubes, nRes, Counter;
-    assert( nVars <= 8 );
-    // create the cover
-    nCubes = 0;
-    nMints = (1 << nVars);
-    for ( i = 0; i < nMints; i++ )
-        if ( pTruth[i/32] & (1 << (i & 31)) )
-        {
-            uCube = 0;
-            for ( k = 0; k < nVars; k++ )
-                if ( i & (1 << k) )
-                    uCube |= (1 << ((k<<1)+1));
-                else
-                    uCube |= (1 << ((k<<1)+0));
-            uCover[nCubes] = uCube;
-            pVarCount[nCubes] = nVars;
-            nCubes++;
-//            Extra_PrintBinary( stdout, &uCube, 8 ); printf( "\n" );
+    Ivy_Obj_t * pNode0, * pNode1;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( Ivy_ObjIsMuxType(pNode) );
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // find the control variable
+//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
+    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
         }
-    assert( nCubes <= 256 );
-    // reduce the cover by building larger cubes
-    for ( i = 1; i < nCubes; i++ )
-        for ( k = 0; k < i; k++ )
-            if ( pVarCount[i] && pVarCount[i] == pVarCount[k] && Ivy_TruthCubesDist1(uCover[i], uCover[k]) )
-            {
-                uCubeNew = Ivy_TruthCubesMerge(uCover[i], uCover[k]);
-                for ( c = i; c < nCubes; c++ )
-                    if ( uCubeNew == uCover[c] )
-                        break;
-                if ( c != nCubes )
-                    continue;
-                uCover[nCubes] = uCubeNew;
-                pVarCount[nCubes] = pVarCount[i] - 1;
-                nCubes++;
-                assert( nCubes < 81*81 );
-//                Extra_PrintBinary( stdout, &uCubeNew, 8 ); printf( "\n" );
-//                c = c;
-            }
-    // compact the cover
-    nRes = 0;
-    for ( i = nCubes -1; i >= 0; i-- )
+    }
+//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
     {
-        for ( k = 0; k < nRes; k++ )
-            if ( (uCover[i] & uResult[k]) == uResult[k] )
-                break;
-        if ( k != nRes )
-            continue;
-        uResult[nRes++] = uCover[i];
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
+        }
+    }
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
     }
-    // count the number of literals
-    Counter = 0;
-    for ( i = 0; i < nRes; i++ )
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
     {
-        for ( k = 0; k < nVars; k++ )
-            if ( uResult[i] & (3 << (k<<1)) )
-                Counter++;
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
     }
-    return Counter;
+    assert( 0 ); // this is not MUX
+    return NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Tests the cover procedure.]
+  Synopsis    [Returns the real fanin.]
 
   Description []
                
@@ -565,17 +534,13 @@ int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TruthEstimateNodesTest()
+Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
 {
-    unsigned uTruth[8];
-    int i;
-    for ( i = 0; i < 8; i++ )
-        uTruth[i] = ~(unsigned)0;
-    uTruth[3] ^= (1 << 13);
-//    uTruth[4] = 0xFFFFF;
-//    uTruth[0] = 0xFF;
-//    uTruth[0] ^= (1 << 3);
-    printf( "Number = %d.\n", Ivy_TruthEstimateNodes(uTruth, 8) );
+    Ivy_Obj_t * pFanin;
+    if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
+        return pObj;
+    pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
+    return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index f697910b..a8f6a824 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -4,7 +4,9 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyCut.c \
     src/temp/ivy/ivyDfs.c \
     src/temp/ivy/ivyDsd.c \
+    src/temp/ivy/ivyFanout.c \
     src/temp/ivy/ivyMan.c \
+    src/temp/ivy/ivyMem.c \
     src/temp/ivy/ivyMulti.c \
     src/temp/ivy/ivyObj.c \
     src/temp/ivy/ivyOper.c \
@@ -12,5 +14,4 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyRwrPre.c \
     src/temp/ivy/ivySeq.c \
     src/temp/ivy/ivyTable.c \
-    src/temp/ivy/ivyUndo.c \
     src/temp/ivy/ivyUtil.c