Version abc60701

14 files changed, 2695 insertions, 737 deletions

diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 55ada384..57d8cfd2 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -42,6 +42,11 @@ extern "C" {
 
 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 { 
@@ -102,10 +107,12 @@ struct Ivy_Man_t_
     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
@@ -118,6 +125,26 @@ struct Ivy_Man_t_
 };
 
 
+#define IVY_CUT_LIMIT     256
+#define IVY_CUT_INPUT       6
+
+typedef struct Ivy_Cut_t_ Ivy_Cut_t;
+struct Ivy_Cut_t_
+{
+    short       nSize;
+    short       nSizeMax;
+    int         pArray[IVY_CUT_INPUT];
+    unsigned    uHash;
+};
+
+typedef struct Ivy_Store_t_ Ivy_Store_t;
+struct Ivy_Store_t_
+{
+    int         nCuts;
+    int         nCutsMax;
+    Ivy_Cut_t   pCuts[IVY_CUT_LIMIT]; // storage for cuts
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,14 +160,6 @@ static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i
 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 int          Ivy_FanCreate( int Id, int fCompl )    { return (Id << 1) | fCompl;                  }
-static inline int          Ivy_FanId( int Fan )                   { return Fan >> 1;                            }
-static inline int          Ivy_FanCompl( int Fan )                { return Fan & 1;                             }
-
-static inline int          Ivy_LeafCreate( int Id, int Lat )      { return (Id << 4) | Lat;                     }
-static inline int          Ivy_LeafId( int Leaf )                 { return Leaf >> 4;                           }
-static inline int          Ivy_LeafLat( int Leaf )                { return Leaf & 15;                           }
-
 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));  }
@@ -153,6 +172,19 @@ static inline Ivy_Obj_t *  Ivy_ManPi( Ivy_Man_t * p, int i )      { return p->pO
 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 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) ); }
+
+static inline int          Ivy_LeafCreate( int Id, int Lat )      { return (Id << 4) | Lat;                     }
+static inline int          Ivy_LeafId( int Leaf )                 { return Leaf >> 4;                           }
+static inline int          Ivy_LeafLat( int Leaf )                { return Leaf & 15;                           }
+
 static inline int          Ivy_ManPiNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PI];                    }
 static inline int          Ivy_ManPoNum( Ivy_Man_t * p )          { return p->nObjs[IVY_PO];                    }
 static inline int          Ivy_ManAssertNum( Ivy_Man_t * p )      { return p->nObjs[IVY_ASSERT];                }
@@ -185,9 +217,9 @@ static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { assert( !Ivy
 static inline int          Ivy_ObjIsExor( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR;   }
 static inline int          Ivy_ObjIsBuf( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF;    }
 static inline int          Ivy_ObjIsNode( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
-static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
+static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
 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_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;  }
@@ -227,13 +259,9 @@ static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy
 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_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_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(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 )       { 
     int IdSaved = pObj->Id; 
-    if ( IdSaved == 54 )
-    {
-        int x = 0;
-    }
     memset( pObj, 0, sizeof(Ivy_Obj_t) ); 
     pObj->Id = IdSaved; 
 }
@@ -339,6 +367,8 @@ static inline int          Ivy_ObjFaninNum( Ivy_Obj_t * pObj )
 // 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++ )
@@ -369,6 +399,9 @@ static inline int          Ivy_ObjFaninNum( Ivy_Obj_t * pObj )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== 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 );
 /*=== 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 );
@@ -377,11 +410,13 @@ extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init );
 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 );
-/*=== ivyBalance.c ======================================================*/
-extern int             Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
+extern Ivy_Store_t *   Ivy_NodeFindCutsAll( 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 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 );
 /*=== ivyDsd.c ==========================================================*/
 extern int             Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
 extern void            Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -399,6 +434,7 @@ 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 );
 /*=== 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 );
@@ -415,8 +451,12 @@ 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 );
+/*=== ivyResyn.c =========================================================*/
+extern Ivy_Man_t *     Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel );
 /*=== 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 );
@@ -437,6 +477,8 @@ extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj
 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 bbe69dd9..2e230ed2 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -17,32 +17,18 @@
   Revision    [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #include "ivy.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots );
-
-// this procedure returns 1 if the node cannot be expanded
-static inline int Ivy_NodeStopFanin( Ivy_Obj_t * pNode, int iFanin )
-{
-    if ( iFanin == 0 )
-        return Ivy_ObjFanin0(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) > 1 || Ivy_ObjFaninC0(pNode);
-    else
-        return Ivy_ObjFanin1(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) > 1 || Ivy_ObjFaninC1(pNode);
-}
-
-// this procedure returns 1 if the node cannot be recursively dereferenced
-static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin )
-{
-    if ( iFanin == 0 )
-        return Ivy_ObjFanin0(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) == 0 && !Ivy_ObjFaninC0(pNode);
-    else
-        return Ivy_ObjFanin1(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) == 0 && !Ivy_ObjFaninC1(pNode);
-}
+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_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -59,44 +45,41 @@ static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
+Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
 {
-    Vec_Int_t * vNodes;
-    Vec_Ptr_t * vFront, * vSpots;
-    Ivy_Obj_t * pNode;
-    int i;
-    vSpots = Vec_PtrAlloc( 50 );
-    vFront = Vec_PtrAlloc( 50 );
-    vNodes = Ivy_ManDfs( p );
-    Ivy_ManForEachNodeVec( p, vNodes, pNode, i )
+    Ivy_Man_t * pNew;
+    Ivy_Obj_t * pObj, * pDriver;
+    Vec_Vec_t * vStore;
+    int i, NewNodeId;
+    // clean the old manager
+    Ivy_ManCleanTravId( p );
+    // create the new manager 
+    pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 );
+    // 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) );
+    // balance the AIG
+    vStore = Vec_VecAlloc( 50 );
+    Ivy_ManForEachPo( p, pObj, i )
     {
-        if ( Ivy_ObjIsBuf(pNode) )
-            continue;
-        // fix the fanin buffer problem
-        Ivy_NodeFixBufferFanins( pNode );
-        // skip node if it became a buffer
-        if ( Ivy_ObjIsBuf(pNode) )
-            continue;
-        // skip nodes with one fanout if type of the node is the same as type of the fanout
-        // such nodes will be processed when the fanouts are processed
-        if ( Ivy_ObjRefs(pNode) == 1 && Ivy_ObjIsExor(pNode) == Ivy_ObjExorFanout(pNode) )
-            continue;
-        assert( Ivy_ObjRefs(pNode) > 0 );
-        // do not balance the node if both if its fanins have more than one fanout
-        if ( Ivy_NodeStopFanin(pNode, 0) && Ivy_NodeStopFanin(pNode, 1) )
-             continue;
-        // try balancing this node
-        Ivy_NodeBalance( pNode, fUpdateLevel, vFront, vSpots );
+        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) );
     }
-    Vec_IntFree( vNodes );
-    Vec_PtrFree( vSpots );
-    Vec_PtrFree( vFront );
-    return 1;
+    Vec_VecFree( vStore );
+    if ( i = Ivy_ManCleanup( pNew ) )
+        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    // check the resulting AIG
+    if ( !Ivy_ManCheck(pNew) )
+        printf( "Ivy_ManBalance(): The check has failed.\n" );
+    return pNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Dereferences MFFC of the node.]
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
 
   Description []
                
@@ -105,24 +88,19 @@ int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode )
+int Ivy_NodeCompareLevelsDecrease( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
 {
-    Ivy_Obj_t * pFan;
-    // deref the first fanin
-    pFan = Ivy_ObjFanin0(pNode);
-    Ivy_ObjRefsDec( pFan );
-    if ( Ivy_NodeBalanceDerefFanin(pNode, 0) )
-        Ivy_NodeBalanceDeref_rec( pFan );
-    // deref the second fanin
-    pFan = Ivy_ObjFanin1(pNode);
-    Ivy_ObjRefsDec( pFan );
-    if ( Ivy_NodeBalanceDerefFanin(pNode, 1) )
-        Ivy_NodeBalanceDeref_rec( pFan );
+    int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level;
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Removes nodes inside supergate and determines frontier.]
+  Synopsis    [Returns the ID of new node constructed.]
 
   Description []
                
@@ -131,35 +109,47 @@ void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront )
+int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
 {
-    Ivy_Obj_t * pFanin;
-    // skip visited nodes
-    if ( Vec_PtrFind(vSpots, pNode) >= 0 )
-        return;
-    // collect node
-    Vec_PtrPush( vSpots, pNode );
-    // first fanin
-    pFanin = Ivy_ObjFanin0(pNode);
-    if ( Ivy_ObjRefs(pFanin) == 0 )
-        Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront );
-    else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild0(pNode)) >= 0 )
-        Vec_PtrRemove( vFront, Ivy_ObjChild0(pNode) );
-    else
-        Vec_PtrPushUnique( vFront, Ivy_ObjChild0(pNode) );
-    // second fanin
-    pFanin = Ivy_ObjFanin1(pNode);
-    if ( Ivy_ObjRefs(pFanin) == 0 )
-        Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront );
-    else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild1(pNode)) >= 0 )
-        Vec_PtrRemove( vFront, Ivy_ObjChild1(pNode) );
-    else
-        Vec_PtrPushUnique( vFront, Ivy_ObjChild1(pNode) );
+    Ivy_Obj_t * pObjNew;
+    Vec_Ptr_t * vSuper;
+    int i, NewNodeId;
+    assert( !Ivy_IsComplement(pObjOld) );
+    assert( !Ivy_ObjIsBuf(pObjOld) );
+    // return if the result is known
+    if ( Ivy_ObjIsConst1(pObjOld) )
+        return pObjOld->TravId;
+    if ( pObjOld->TravId )
+        return pObjOld->TravId;
+    assert( Ivy_ObjIsNode(pObjOld) );
+    // get the implication supergate
+    vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level );
+    if ( vSuper->nSize == 0 )
+    { // it means that the supergate contains two nodes in the opposite polarity
+        pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) );
+        return pObjOld->TravId;
+    }
+    if ( vSuper->nSize < 2 )
+        printf( "BUG!\n" );
+    // for each old node, derive the new well-balanced node
+    for ( i = 0; i < vSuper->nSize; i++ )
+    {
+        NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) );
+        vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
+    }
+    // build the supergate
+    pObjNew = Ivy_NodeBalanceBuildSuper( 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 );
+    return pObjOld->TravId;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Comparison procedure for two nodes by level.]
+  Synopsis    [Builds implication supergate.]
 
   Description []
                
@@ -168,89 +158,107 @@ void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
 {
-    int Level1 = Ivy_ObjLevel( *pp1 );
-    int Level2 = Ivy_ObjLevel( *pp2 );
-    if ( Level1 > Level2 )
-        return -1;
-    if ( Level1 < Level2 )
-        return 1;
-    return 0;
+    Ivy_Obj_t * pObj1, * pObj2;
+    int LeftBound;
+    assert( vSuper->nSize > 1 );
+    // sort the new nodes by level in the decreasing order
+    Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease );
+    // balance the nodes
+    while ( vSuper->nSize > 1 )
+    {
+        // 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 );
+        // pull out the last two nodes
+        pObj1 = Vec_PtrPop(vSuper);
+        pObj2 = Vec_PtrPop(vSuper);
+        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) );
+    }
+    return Vec_PtrEntry(vSuper, 0);
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Removes nodes inside supergate and determines frontier.]
+  Synopsis    [Collects the nodes of the supergate.]
 
-  Description [Return 1 if the output needs to be complemented.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots )
+int Ivy_NodeBalanceCone_rec( Ivy_Obj_t * pRoot, Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper )
 {
-    Ivy_Man_t * pMan = Ivy_ObjMan( pNode );
-    Ivy_Obj_t * pObj, * pNext;
-    int i, k, Counter = 0;
-    // dereference the cone
-    Ivy_NodeBalanceDeref_rec( pNode );
-    // collect the frontier and the internal nodes
-    Vec_PtrClear( vFront );
-    Vec_PtrClear( vSpots );
-    Ivy_NodeBalanceCollect_rec( pNode, vSpots, vFront );
-    // remove all the nodes
-    Vec_PtrForEachEntry( vSpots, pObj, i )
-    {
-        // skip the first entry (the node itself)
-        if ( i == 0 ) continue;
-        // collect the free entries
-        Vec_IntPush( pMan->vFree, pObj->Id );
-        Ivy_ObjDelete( pObj, 1 );
-    }
-    // sort nodes by level in decreasing order
-    qsort( (void *)Vec_PtrArray(vFront), Vec_PtrSize(vFront), sizeof(Ivy_Obj_t *), 
-            (int (*)(const void *, const void *))Ivy_BalanceCompareByLevel );
-    // check if there are nodes and their complements
-    Counter = 0;
-    Vec_PtrForEachEntry( vFront, pObj, i )
+    int RetValue1, RetValue2, i;
+    // check if the node is visited
+    if ( Ivy_Regular(pObj)->fMarkB )
     {
-        if ( i == Vec_PtrSize(vFront) - 1 )
-            break;
-        pNext = Vec_PtrEntry( vFront, i+1 );
-        if ( Ivy_Regular(pObj) == Ivy_Regular(pNext) )
-        {
-            assert( pObj == Ivy_Not(pNext) );
-            Vec_PtrWriteEntry( vFront, i, NULL );
-            Vec_PtrWriteEntry( vFront, i+1, NULL );
-            i++;
-            Counter++;
-        }
-    }
-    // if there are no complemented pairs, go ahead and balance
-    if ( Counter == 0 )
+        // check if the node occurs in the same polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == pObj )
+                return 1;
+        // check if the node is present in the opposite polarity
+        for ( i = 0; i < vSuper->nSize; i++ )
+            if ( vSuper->pArray[i] == Ivy_Not(pObj) )
+                return -1;
+        assert( 0 );
         return 0;
-    // if there are complemented pairs and this is AND, create const 0
-    if ( Counter > 0 && Ivy_ObjIsAnd(pNode) )
+    }
+    // if the new node is complemented or a PI, another gate begins
+    if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) )
     {
-        Vec_PtrClear( vFront );
-        Vec_PtrPush( vFront, Ivy_ManConst0(pMan) );
+        Vec_PtrPush( vSuper, pObj );
+        Ivy_Regular(pObj)->fMarkB = 1;
         return 0;
     }
-    assert( Counter > 0 && Ivy_ObjIsExor(pNode) );
-    // remove the pairs
-    k = 0;
-    Vec_PtrForEachEntry( vFront, pObj, i )
-        if ( pObj ) 
-            Vec_PtrWriteEntry( vFront, k++, pObj );
-    Vec_PtrShrink( vFront, k );
-    // add constant zero node if nothing is left
-    if ( Vec_PtrSize(vFront) == 0 )
-        Vec_PtrPush( vFront, Ivy_ManConst0(pMan) );
-    // return 1 if the number of pairs is odd (need to complement the output)
-    return Counter & 1;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    // go through the branches
+    RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper );
+    RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild1(pObj) ), vSuper );
+    if ( RetValue1 == -1 || RetValue2 == -1 )
+        return -1;
+    // return 1 if at least one branch has a duplicate
+    return RetValue1 || RetValue2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+{
+    Vec_Ptr_t * vNodes;
+    int RetValue, i;
+    assert( !Ivy_IsComplement(pObj) );
+    // extend the storage
+    if ( Vec_VecSize( vStore ) <= Level )
+        Vec_VecPush( vStore, Level, 0 );
+    // get the temporary array of nodes
+    vNodes = Vec_VecEntry( vStore, Level );
+    Vec_PtrClear( vNodes );
+    // collect the nodes in the implication supergate
+    RetValue = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes );
+    assert( vNodes->nSize > 1 );
+    // unmark the visited nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Ivy_Regular(pObj)->fMarkB = 0;
+    // if we found the node and its complement in the same implication supergate, 
+    // return empty set of nodes (meaning that we should use constant-0 node)
+    if ( RetValue == -1 )
+        vNodes->nSize = 0;
+    return vNodes;
 }
 
 /**Function*************************************************************
@@ -270,27 +278,27 @@ int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * v
 ***********************************************************************/
 int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
 {
-    Ivy_Obj_t * pNodeRight, * pNodeLeft;
+    Ivy_Obj_t * pObjRight, * pObjLeft;
     int Current;
     // if two or less nodes, pair with the first
     if ( Vec_PtrSize(vSuper) < 3 )
         return 0;
     // set the pointer to the one before the last
     Current = Vec_PtrSize(vSuper) - 2;
-    pNodeRight = Vec_PtrEntry( vSuper, Current );
+    pObjRight = Vec_PtrEntry( vSuper, Current );
     // go through the nodes to the left of this one
     for ( Current--; Current >= 0; Current-- )
     {
         // get the next node on the left
-        pNodeLeft = Vec_PtrEntry( vSuper, Current );
+        pObjLeft = Vec_PtrEntry( vSuper, Current );
         // if the level of this node is different, quit the loop
-        if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->Level )
+        if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level )
             break;
     }
     Current++;    
     // get the node, for which the equality holds
-    pNodeLeft = Vec_PtrEntry( vSuper, Current );
-    assert( Ivy_Regular(pNodeLeft)->Level == Ivy_Regular(pNodeRight)->Level );
+    pObjLeft = Vec_PtrEntry( vSuper, Current );
+    assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level );
     return Current;
 }
 
@@ -306,9 +314,9 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
 {
-    Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost;
+    Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
     int RightBound, i;
     // get the right bound
     RightBound = Vec_PtrSize(vSuper) - 2;
@@ -316,19 +324,19 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
     if ( LeftBound == RightBound )
         return;
     // get the two last nodes
-    pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 );
-    pNode2 = Vec_PtrEntry( vSuper, RightBound     );
+    pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
+    pObj2 = Vec_PtrEntry( vSuper, RightBound     );
     // find the first node that can be shared
     for ( i = RightBound; i >= LeftBound; i-- )
     {
-        pNode3 = Vec_PtrEntry( vSuper, i );
-        pGhost = Ivy_ObjCreateGhost( pNode1, pNode3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
+        pObj3 = Vec_PtrEntry( vSuper, i );
+        pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
         if ( Ivy_TableLookup( pGhost ) )
         {
-            if ( pNode3 == pNode2 )
+            if ( pObj3 == pObj2 )
                 return;
-            Vec_PtrWriteEntry( vSuper, i,          pNode2 );
-            Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
             return;
         }
     }
@@ -336,11 +344,11 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
     // we did not find the node to share, randomize choice
     {
         int Choice = rand() % (RightBound - LeftBound + 1);
-        pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
-        if ( pNode3 == pNode2 )
+        pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
+        if ( pObj3 == pObj2 )
             return;
-        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 );
-        Vec_PtrWriteEntry( vSuper, RightBound,         pNode3 );
+        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
+        Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
     }
 */
 }
@@ -356,61 +364,22 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode )
+void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj )
 {
-    Ivy_Obj_t * pNode1, * pNode2;
+    Ivy_Obj_t * pObj1, * pObj2;
     int i;
-    if ( Vec_PtrPushUnique(vFront, pNode) )
+    if ( Vec_PtrPushUnique(vStore, pObj) )
         return;
     // find the p of the node
-    for ( i = vFront->nSize-1; i > 0; i-- )
+    for ( i = vStore->nSize-1; i > 0; i-- )
     {
-        pNode1 = vFront->pArray[i  ];
-        pNode2 = vFront->pArray[i-1];
-        if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
+        pObj1 = vStore->pArray[i  ];
+        pObj2 = vStore->pArray[i-1];
+        if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level )
             break;
-        vFront->pArray[i  ] = pNode2;
-        vFront->pArray[i-1] = pNode1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Balances one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots )
-{
-    Ivy_Man_t * pMan = Ivy_ObjMan( pNode );
-    Ivy_Obj_t * pFan0, * pFan1, * pNodeNew;
-    int fCompl, LeftBound;
-    // remove internal nodes and derive the frontier
-    fCompl = Ivy_NodeBalancePrepare( pNode, vFront, vSpots );
-    assert( Vec_PtrSize(vFront) > 0 );
-    // balance the nodes
-    while ( Vec_PtrSize(vFront) > 1 )
-    {
-        // find the left bound on the node to be paired
-        LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vFront );
-        // find the node that can be shared (if no such node, randomize choice)
-        Ivy_NodeBalancePermute( pMan, vFront, LeftBound, Ivy_ObjIsExor(pNode) );
-        // pull out the last two nodes
-        pFan0 = Vec_PtrPop(vFront);  assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan0)) );
-        pFan1 = Vec_PtrPop(vFront);  assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan1)) );
-        // create the new node
-        pNodeNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pFan0, pFan1, Ivy_ObjType(pNode), IVY_INIT_NONE) );
-        // add the new node to the frontier
-        Ivy_NodeBalancePushUniqueOrderByLevel( vFront, pNodeNew );
+        vStore->pArray[i  ] = pObj2;
+        vStore->pArray[i-1] = pObj1;
     }
-    assert( Vec_PtrSize(vFront) == 1 );
-    // perform the replacement
-    Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 ); 
 }
 
 
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 57720e17..71a3613c 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -200,180 +200,6 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Comparison for node pointers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
-{
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computing one algebraic cut.]
-
-  Description [Returns 1 if the tree-leaves of this node where traversed 
-  and found to have no external references (and have not been collected). 
-  Returns 0 if the tree-leaves have external references and are collected.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pRoot, Ivy_Type_t Type, Vec_Ptr_t * vFront )
-{
-    int RetValue0, RetValue1;
-    Ivy_Obj_t * pRootR = Ivy_Regular(pRoot);
-    assert( Type != IVY_EXOR || !Ivy_IsComplement(pRoot) );
-    // if the node is a buffer skip through it
-    if ( Ivy_ObjIsBuf(pRootR) )
-        return Ivy_ManFindAlgCut_rec( Ivy_NotCond(Ivy_ObjChild0(pRootR), Ivy_IsComplement(pRoot)), Type, vFront );
-    // if the node is the end of the tree, return
-    if ( Ivy_IsComplement(pRoot) || Ivy_ObjIsCi(pRoot) || Ivy_ObjType(pRoot) != Type )
-    {
-        if ( Ivy_ObjRefs(pRootR) == 1 )
-            return 1;
-        assert( Ivy_ObjRefs(pRootR) > 1 );
-        Vec_PtrPush( vFront, pRoot );
-        return 0;
-    }
-    // branch on the node
-    assert( Ivy_ObjIsNode(pRoot) );
-    RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild0(pRoot), Type, vFront );
-    RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild1(pRoot), Type, vFront );
-    // the case when both have no external referenced
-    if ( RetValue0 && RetValue1 )
-    {
-        if ( Ivy_ObjRefs(pRoot) == 1 )
-            return 1;
-        assert( Ivy_ObjRefs(pRoot) > 1 );
-        Vec_PtrPush( vFront, pRoot );
-        return 0;
-    }
-    // the case when one of them has external references
-    if ( RetValue0 )
-        Vec_PtrPush( vFront, Ivy_ObjChild0(pRoot) );
-    if ( RetValue1 )
-        Vec_PtrPush( vFront, Ivy_ObjChild1(pRoot) );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computing one algebraic cut.]
-
-  Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
-  (c) boundary of different gates. Returns 1 if this is a pure tree.
-  Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront )
-{
-    Ivy_Obj_t * pObj, * pPrev;
-    int RetValue, i, k;
-    assert( !Ivy_IsComplement(pRoot) );
-    // clear the frontier and collect the nodes
-    Vec_PtrClear( vFront );
-    RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront );
-    // return if the node is the root of a tree
-    if ( RetValue == 1 )
-        return 1;
-    // sort the entries to in increasing order
-    Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
-    // remove duplicated
-    k = 1;
-    Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
-    {
-        pPrev = (k == 0 ? NULL : Vec_PtrEntry(vFront, k-1));
-        if ( pObj == pPrev )
-        {
-            if ( Ivy_ObjIsExor(pRoot) )
-                k--;
-            continue;
-        }
-        if ( pObj == Ivy_Not(pPrev) )
-            return -1;
-        Vec_PtrWriteEntry( vFront, k++, pObj );
-    }
-    if ( k == 0 )
-        return -1;
-    Vec_PtrShrink( vFront, k );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManTestCutsAlg( Ivy_Man_t * p )
-{
-    Vec_Ptr_t * vFront;
-    Ivy_Obj_t * pObj, * pTemp;
-    int i, k, RetValue;
-    vFront = Vec_PtrAlloc( 100 );
-    Ivy_ManForEachObj( p, pObj, i )
-    {
-        if ( !Ivy_ObjIsNode(pObj) )
-            continue;
-        if ( Ivy_ObjIsMuxType(pObj) )
-        {
-            printf( "m " );
-            continue;
-        }
-        if ( pObj->Id == 509 )
-        {
-            int y = 0;
-        }
-
-        RetValue = Ivy_ManFindAlgCut( pObj, vFront );
-        if ( Ivy_ObjIsExor(pObj) )
-            printf( "x" );
-        if ( RetValue == -1 )
-            printf( "Const0 " );
-        else if ( RetValue == 1 || Vec_PtrSize(vFront) <= 2 )
-            printf( ". " );
-        else
-            printf( "%d ", Vec_PtrSize(vFront) );
-        
-        printf( "( " );
-        Vec_PtrForEachEntry( vFront, pTemp, k )
-            printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
-        printf( ")\n" );
-
-        if ( Vec_PtrSize(vFront) == 5 )
-        {
-            int x = 0;
-        }
-    }
-    printf( "\n" );
-    Vec_PtrFree( vFront );
-}
-
-
 
 
 /**Function*************************************************************
@@ -639,8 +465,8 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu
 void Ivy_ManTestCutsBool( Ivy_Man_t * p )
 {
     Vec_Ptr_t * vFront, * vVolume, * vLeaves;
-    Ivy_Obj_t * pObj, * pTemp;
-    int i, k, RetValue;
+    Ivy_Obj_t * pObj;//, * pTemp;
+    int i, RetValue;//, k;
     vFront = Vec_PtrAlloc( 100 );
     vVolume = Vec_PtrAlloc( 100 );
     vLeaves = Vec_PtrAlloc( 100 );
@@ -673,6 +499,376 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p )
     Vec_PtrFree( vLeaves );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Find the hash value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut )
+{
+    int i;
+//    for ( i = 1; i < pCut->nSize; i++ )
+//        assert( pCut->pArray[i-1] < pCut->pArray[i] );
+    pCut->uHash = 0;
+    for ( i = 0; i < pCut->nSize; i++ )
+        pCut->uHash |= (1 << (pCut->pArray[i] % 31));
+    return pCut->uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one node to the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ivy_NodeCutShrink( Ivy_Cut_t * pCut, int iOld )
+{
+    int i, k;
+    for ( i = k = 0; i < pCut->nSize; i++ )
+        if ( pCut->pArray[i] != iOld )
+            pCut->pArray[k++] = pCut->pArray[i];
+    assert( k == pCut->nSize - 1 );
+    pCut->nSize--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one node to the cut.]
+
+  Description [Returns 1 if the cuts is still okay.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew )
+{
+    int i;
+    for ( i = 0; i < pCut->nSize; i++ )
+        if ( pCut->pArray[i] == iNew )
+            return 1;
+    // check if there is room
+    if ( pCut->nSize == pCut->nSizeMax )
+        return 0;
+    // add the new one
+    for ( i = pCut->nSize - 1; i >= 0; i-- )
+        if ( pCut->pArray[i] > iNew )
+            pCut->pArray[i+1] = pCut->pArray[i];
+        else
+        {
+            assert( pCut->pArray[i] < iNew );
+            break;
+        }
+    pCut->pArray[i+1] = iNew;
+    pCut->nSize++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the cut exists.]
+
+  Description [Returns 1 if the cut exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCutFindOrAdd( 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->uHash == pCutNew->uHash && pCut->nSize == pCutNew->nSize )
+        {
+            for ( k = 0; k < pCutNew->nSize; k++ )
+                if ( pCut->pArray[k] != pCutNew->pArray[k] )
+                    break;
+            if ( k == pCutNew->nSize )
+                return 1;
+        }
+    }
+    assert( pCutStore->nCuts < pCutStore->nCutsMax );
+    // add the cut
+    pCut = pCutStore->pCuts + pCutStore->nCuts++;
+    *pCut = *pCutNew;
+    return 0;
+}
+
+/**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++ )
+    {
+        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_NodeCutFindOrAddFilter( 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 )
+        {
+            // skip the non-contained cuts
+            if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
+                continue;
+            // 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
+//            --pCutStore->nCuts;
+//            for ( k = i; k < pCutStore->nCuts; k++ )
+//                pCutStore->pCuts[k] = pCutStore->pCuts[k+1];
+//            i--;
+            pCut->nSize = 0;
+        }
+    }
+    assert( pCutStore->nCuts < pCutStore->nCutsMax );
+    // add the cut
+    pCut = pCutStore->pCuts + pCutStore->nCuts++;
+    *pCut = *pCutNew;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeCompactCuts( Ivy_Store_t * pCutStore )
+{
+    Ivy_Cut_t * pCut;
+    int i, k;
+    for ( i = k = 0; i < pCutStore->nCuts; i++ )
+    {
+        pCut = pCutStore->pCuts + i;
+        if ( pCut->nSize == 0 )
+            continue;
+        pCutStore->pCuts[k++] = *pCut;
+    }
+    pCutStore->nCuts = k;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodePrintCut( 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_NodePrintCuts( Ivy_Store_t * pCutStore )
+{
+    int i;
+    printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
+    for ( i = 0; i < pCutStore->nCuts; i++ )
+        Ivy_NodePrintCut( pCutStore->pCuts + i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Store_t * Ivy_NodeFindCutsAll( 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_Obj_t * pLeaf;
+    int i, k;
+
+    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] = pObj->Id;
+    Ivy_NodeCutHash( pCutNew );
+    // add the trivial cut
+    Ivy_NodeCutFindOrAdd( pCutStore, 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_ObjObj( pObj, pCut->pArray[k] );
+            if ( Ivy_ObjIsCi(pLeaf) )
+                continue;
+            *pCutNew = *pCut;
+            Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
+            if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
+                continue;
+            if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
+                continue;
+            Ivy_NodeCutHash( pCutNew );
+            Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
+            if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+                break;
+        }
+        if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+            break;
+    }
+    Ivy_NodeCompactCuts( pCutStore );
+//    Ivy_NodePrintCuts( pCutStore );
+    return pCutStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManTestCutsAll( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
+    int clk = clock();
+    nNodeTotal = nNodeOver = 0;
+    nCutsTotal = -Ivy_ManNodeNum(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        nCutsCut    = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts;
+        nCutsTotal += nCutsCut;
+        nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
+        nNodeTotal++;
+    }
+    printf( "Total cuts = %6d. Trivial = %6d.   Nodes = %6d. Satur = %6d.  ", 
+        nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
+    PRT( "Time", clock() - clk );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 2db80b00..2dc3bac8 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -69,6 +69,9 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
     Vec_Int_t * vNodes;
     Ivy_Obj_t * pObj;
     int i;
+    // 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 )
@@ -107,7 +110,7 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
     // traverse the fanins
     vFanins = Ivy_ObjGetFanins( pObj );
     Vec_IntForEachEntry( vFanins, Fanin, i )
-        Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes );
+        Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes );
     // add the node
     Vec_IntPush( vNodes, pObj->Id );
 } 
@@ -134,7 +137,7 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
     vNodes = Vec_IntAlloc( 10 );
     Ivy_ManForEachPo( p, pObj, i )
     {
-        pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) );
+        pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) );
         Ivy_ManDfsExt_rec( pFanin, vNodes );
     }
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
@@ -145,6 +148,132 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCollectCone_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+    if ( pObj->fMarkA )
+        return;
+    if ( Ivy_ObjIsBuf(pObj) )
+    {
+        Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
+        Vec_PtrPush( vCone, pObj );
+        return;
+    }
+    assert( Ivy_ObjIsNode(pObj) );
+    Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
+    Ivy_ManCollectCone_rec( Ivy_ObjFanin1(pObj), vCone );
+    Vec_PtrPushUnique( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
+{
+    Ivy_Obj_t * pTemp;
+    int i;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    // mark the nodes
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+        Ivy_Regular(pTemp)->fMarkA = 1;
+    assert( pObj->fMarkA == 0 );
+    // collect the cone
+    Vec_PtrClear( vCone );
+    Ivy_ManCollectCone_rec( pObj, vCone );
+    // unmark the nodes
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+        Ivy_Regular(pTemp)->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the nodes by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p )
+{
+    Vec_Vec_t * vNodes;
+    Ivy_Obj_t * pObj;
+    int i;
+    vNodes = Vec_VecAlloc( 100 );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        assert( !Ivy_ObjIsBuf(pObj) );
+        if ( Ivy_ObjIsNode(pObj) )
+            Vec_VecPush( vNodes, pObj->Level, pObj );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes required levels for each node.]
+
+  Description [Assumes topological ordering of the nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    Vec_Int_t * vLevelsR;
+    Vec_Vec_t * vNodes;
+    int i, k, Level, LevelMax;
+    assert( p->vRequired == NULL );
+    // start the required times
+    vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) );
+    // iterate through the nodes in the reverse order
+    vNodes = Ivy_ManLevelize( p );
+    Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
+    {
+        Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj);
+        if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level )
+            Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level );
+        if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level )
+            Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level );
+    }
+    Vec_VecFree( vNodes );
+    // convert it into the required times
+    LevelMax = Ivy_ManReadLevels( p );
+//printf( "max %5d\n",LevelMax );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        Level = Vec_IntEntry( vLevelsR, pObj->Id );
+        Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level );
+//printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level );
+    }
+    p->vRequired = vLevelsR;
+    return vLevelsR;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 04c31f3d..2ff90aa9 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -48,6 +48,7 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
     p = ALLOC( Ivy_Man_t, 1 );
     memset( p, 0, sizeof(Ivy_Man_t) );
     p->nTravIds = 1;
+    p->fCatchExor = 1;
     // AIG nodes
     p->nObjsAlloc = 1 + nPis + nPos + nNodesMax;
 //    p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even
@@ -191,12 +192,13 @@ void Ivy_ManPrintStats( Ivy_Man_t * p )
     {
     printf( "A = %d. ",     Ivy_ManAndNum(p) );
     printf( "X = %d. ",     Ivy_ManExorNum(p) );
-    printf( "B = %d. ",     Ivy_ManBufNum(p) );
+    printf( "B = %4d. ",     Ivy_ManBufNum(p) );
     }
-    printf( "MaxID = %d. ", p->ObjIdNext-1 );
-    printf( "All = %d. ",   p->nObjsAlloc );
+//    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" );
 }
 
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index 059d1500..e2a44e2d 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -24,22 +24,18 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Ivy_Eval_t_ Ivy_Eval_t;
-struct Ivy_Eval_t_
+#define IVY_EVAL_LIMIT    128
+
+typedef struct Ivy_Eva_t_ Ivy_Eva_t;
+struct Ivy_Eva_t_
 {
-    unsigned Mask   :  5;  // the mask of covered nodes
-    unsigned Weight :  3;  // the number of covered nodes
-    unsigned Cost   :  4;  // the number of overlapping nodes
-    unsigned Level  : 12;  // the level of this node
-    unsigned Fan0   :  4;  // the first fanin
-    unsigned Fan1   :  4;  // the second fanin
+    Ivy_Obj_t * pArg;     // the argument node
+    unsigned    Mask;     // the mask of covered nodes
+    int         Weight;   // the number of covered nodes
 };
 
-static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-static void        Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs );
-static int         Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode );
-static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-
+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 );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -47,212 +43,121 @@ static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type
 
 /**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_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
-{
-    Ivy_Obj_t * pObj1, * pObj2;
-    if ( nObjs == 1 )
-        return ppObjs[0];
-    pObj1 = Ivy_Multi_rec( ppObjs,           nObjs/2,         Type );
-    pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type );
-    return Ivy_Oper( pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Constructs a balanced tree while taking sharing into account.]
 
-  Description []
+  Description [Returns 1 if the implementation exists.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
 {
-    static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5};
-    static Ivy_Eval_t pEvals[15+15*14/2];
-    static Ivy_Obj_t * pArgs[16];
-    Ivy_Eval_t * pEva, * pEvaBest;
-    int nArgsNew, nEvals, i, k;
-    Ivy_Obj_t * pTemp;
-
-    // consider the case of one argument
-    assert( nArgs > 0 );
-    if ( nArgs == 1 )
-        return pArgsInit[0];
-    // consider the case of two arguments
-    if ( nArgs == 2 )
-        return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type );
-
-//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" );
-
-    // set the initial ones
-    for ( i = 0; i < nArgs; i++ )
+    static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
+    Ivy_Eva_t * pEval, * pFan0, * pFan1;
+    Ivy_Obj_t * pObj, * pTemp;
+    int nEvals, nEvalsOld, i, k, x, nLeaves;
+    unsigned uMaskAll;
+
+    // consider special cases
+    nLeaves = Vec_PtrSize(vLeaves);
+    assert( nLeaves > 2 );
+    if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT )
+        return 0;
+//    if ( nLeaves == 1 )
+//        return Vec_PtrEntry( vLeaves, 0 );
+//    if ( nLeaves == 2 )
+//        return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type );
+
+    // set the leaf entries
+    uMaskAll = ((1 << nLeaves) - 1);
+    nEvals = 0;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
     {
-        pArgs[i] = pArgsInit[i];
-        pEva = pEvals + i;
-        pEva->Mask   = (1 << i);
-        pEva->Weight = 1;
-        pEva->Cost   = 0; 
-        pEva->Level  = Ivy_Regular(pArgs[i])->Level; 
-        pEva->Fan0   = 0; 
-        pEva->Fan1   = 0; 
+        pEval = pEvals + nEvals;
+        pEval->pArg   = pObj;
+        pEval->Mask   = (1 << nEvals);
+        pEval->Weight = 1;
+        // mark the leaf
+        Ivy_Regular(pObj)->TravId = nEvals;
+        nEvals++;
     }
 
-    // find the available nodes
-    pEvaBest = pEvals;
-    nArgsNew = nArgs;
-    for ( i = 1; i < nArgsNew; i++ )
-    for ( k = 0; k < i; k++ )
-        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) )
-        {
-            pEva = pEvals + nArgsNew;
-            pEva->Mask   = pEvals[k].Mask | pEvals[i].Mask;
-            pEva->Weight = NumBits[pEva->Mask];
-            pEva->Cost   = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; 
-            pEva->Level  = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); 
-            pEva->Fan0   = k; 
-            pEva->Fan1   = i; 
-//            assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) );
-            // compare
-            if ( pEvaBest->Weight < pEva->Weight ||
-                 pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
-                 pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
-                 pEvaBest = pEva;
-            // save the argument
-            pArgs[nArgsNew++] = pTemp;
-            if ( nArgsNew == 15 )
-                goto Outside;
-        }
-Outside:
-
-//    printf( "Best = %d.\n", pEvaBest - pEvals );
-
-    // the case of no common nodes
-    if ( nArgsNew == nArgs )
+    // propagate masks through the cone
+    Vec_PtrForEachEntry( vCone, pObj, i )
     {
-        Ivy_MultiSort( pArgs, nArgs );
-        return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+        pObj->TravId = nEvals + i;
+        if ( Ivy_ObjIsBuf(pObj) )
+            pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask;
+        else
+            pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask;
     }
-    // the case of one common node
-    if ( nArgsNew == nArgs + 1 )
+
+    // set the internal entries
+    Vec_PtrForEachEntry( vCone, pObj, i )
     {
-        assert( pEvaBest - pEvals == nArgs );
-        k = 0;
-        for ( i = 0; i < nArgs; i++ )
-            if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 )
-                pArgs[k++] = pArgs[i];
-        pArgs[k++] = pArgs[nArgs];
-        assert( k == nArgs - 1 );
-        nArgs = k;
-        Ivy_MultiSort( pArgs, nArgs );
-        return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+        if ( i == Vec_PtrSize(vCone) - 1 )
+            break;
+        // skip buffers
+        if ( Ivy_ObjIsBuf(pObj) )
+            continue;
+        // skip nodes without external fanout
+        if ( Ivy_ObjRefs(pObj) == 0 )
+            continue;
+        assert( !Ivy_IsComplement(pObj) );
+        pEval = pEvals + nEvals;
+        pEval->pArg   = pObj;
+        pEval->Mask   = pEvals[pObj->TravId].Mask;
+        pEval->Weight = Extra_WordCountOnes(pEval->Mask);
+        // mark the node
+        pObj->TravId = nEvals;
+        nEvals++;
     }
-    // the case when there is a node that covers everything
-    if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) )
-        return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); 
 
-    // evaluate node pairs
-    nEvals = nArgsNew;
-    for ( i = 1; i < nArgsNew; i++ )
+    // find the available nodes
+    nEvalsOld = nEvals;
+    for ( i = 1; i < nEvals; i++ )
     for ( k = 0; k < i; k++ )
     {
-        pEva = pEvals + nEvals;
-        pEva->Mask   = pEvals[k].Mask | pEvals[i].Mask;
-        pEva->Weight = NumBits[pEva->Mask];
-        pEva->Cost   = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; 
-        pEva->Level  = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); 
-        pEva->Fan0   = k; 
-        pEva->Fan1   = i; 
-        // compare
-        if ( pEvaBest->Weight < pEva->Weight ||
-             pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
-             pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
-             pEvaBest = pEva;
+        pFan0 = pEvals + i;
+        pFan1 = pEvals + k;
+        pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
+        // skip nodes in the cone
+        if ( pTemp == NULL || pTemp->fMarkB )
+            continue;
+        // skip the leaves
+        for ( x = 0; x < nLeaves; x++ )
+            if ( pTemp == Ivy_Regular(vLeaves->pArray[x]) )
+                break;
+        if ( x < nLeaves )
+            continue;
+        pEval = pEvals + nEvals;
+        pEval->pArg   = pTemp;
+        pEval->Mask   = pFan0->Mask | pFan1->Mask;
+        pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight;
         // save the argument
+        pObj->TravId = nEvals;
         nEvals++;
+        // quit if the number of entries exceeded the limit
+        if ( nEvals == IVY_EVAL_LIMIT )
+            goto Outside;
+        // quit if we found an acceptable implementation
+        if ( pEval->Mask == uMaskAll )
+            goto Outside;
     }
-    assert( pEvaBest - pEvals >= nArgsNew );
-
-//    printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 );
-
-    // get the best implementation
-    pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
-
-    // collect those not covered by EvaBest
-    k = 0;
-    for ( i = 0; i < nArgs; i++ )
-        if ( (pEvaBest->Mask & (1 << i)) == 0 )
-            pArgs[k++] = pArgs[i];
-    pArgs[k++] = pTemp;
-    assert( k == nArgs - (int)pEvaBest->Weight + 1 );
-    nArgs = k;
-    Ivy_MultiSort( pArgs, nArgs );
-    return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements multi-input AND/EXOR operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    if ( iNum < nArgs )
-        return pArgs[iNum];
-    pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type );
-    pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type );
-    return Ivy_Oper( pNode0, pNode1, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Selection-sorts the nodes in the decreasing over of level.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
-{
-    Ivy_Obj_t * pTemp;
-    int i, j, iBest;
+Outside:
 
-    for ( i = 0; i < nArgs-1; i++ )
-    {
-        iBest = i;
-        for ( j = i+1; j < nArgs; j++ )
-            if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level )
-                iBest = j;
-        pTemp = pArgs[i]; 
-        pArgs[i] = pArgs[iBest]; 
-        pArgs[iBest] = pTemp;
-    }
+//    Ivy_MultiPrint( pEvals, nLeaves, nEvals );
+    if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) )
+        return 0;
+    assert( Vec_PtrSize( vSols ) > 0 );
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Inserts a new node in the order by levels.]
+  Synopsis    [Computes how many uncovered ones this one covers.]
 
   Description []
                
@@ -261,32 +166,28 @@ void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode )
+void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
 {
-    Ivy_Obj_t * pNode1, * pNode2;
-    int i;
-    // try to find the node in the array
-    for ( i = 0; i < nArgs; i++ )
-        if ( pArray[i] == pNode )
-            return nArgs;
-    // put the node last
-    pArray[nArgs++] = pNode;
-    // find the place to put the new node
-    for ( i = nArgs-1; i > 0; i-- )
+    Ivy_Eva_t * pEval;
+    int i, k;
+    for ( i = nLeaves; i < nEvals; i++ )
     {
-        pNode1 = pArray[i  ];
-        pNode2 = pArray[i-1];
-        if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
-            break;
-        pArray[i  ] = pNode2;
-        pArray[i-1] = pNode1;
+        pEval = pEvals + i;
+        printf( "%2d  (id = %5d)  : |", i-nLeaves, Ivy_ObjId(pEval->pArg) );
+        for ( k = 0; k < nLeaves; k++ )
+        {
+            if ( pEval->Mask & (1 << k) )
+                printf( "+" );
+            else
+                printf( " " );
+        }
+        printf( "|  Lev = %d.\n", Ivy_ObjLevel(pEval->pArg) );
     }
-    return nArgs;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Balances the array recursively.]
+  Synopsis    [Computes how many uncovered ones this one covers.]
 
   Description []
                
@@ -295,129 +196,102 @@ int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFound )
 {
-    Ivy_Obj_t * pNodeNew;
-    // consider the case of one argument
-    assert( nArgs > 0 );
-    if ( nArgs == 1 )
-        return pArgs[0];
-    // consider the case of two arguments
-    if ( nArgs == 2 )
-        return Ivy_Oper( pArgs[0], pArgs[1], Type );
-    // get the last two nodes
-    pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type );
-    // add the new node
-    nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew );
-    return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+    assert( uMask & ~uFound );
+    if ( (uMask & uFound) == 0 )
+        return nMaskOnes;
+    return Extra_WordCountOnes( uMask & ~uFound );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Implements multi-input AND/EXOR operation.]
+  Synopsis    [Finds the cover.]
 
-  Description []
+  Description [Returns 1 if the cover is found.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
 {
-    Ivy_Obj_t * pTemp;
-    int i, k;
-    int nArgsOld = nArgs;
-    for ( i = 0; i < nArgs; i++ )
-        printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level );
-    for ( i = 1; i < nArgs; i++ )
-        for ( k = 0; k < i; k++ )
+    int fVerbose = 0;
+    Ivy_Eva_t * pEval, * pEvalBest;
+    unsigned uMaskAll, uFound, uTemp;
+    int i, k, BestK, WeightBest, WeightCur, LevelBest, LevelCur;
+    uMaskAll = (nLeaves == 32)? (~(unsigned)0) : ((1 << nLeaves) - 1);
+    uFound = 0;
+    // solve the covering problem
+    if ( fVerbose )
+    printf( "Solution:  " );
+    Vec_PtrClear( vSols );
+    for ( i = 0; i < nLimit; i++ )
+    {
+        BestK = -1;
+        for ( k = nEvals - 1; k >= 0; k-- )
         {
-            pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE));
-            if ( pTemp != NULL )
+            pEval = pEvals + k;
+            if ( (pEval->Mask & ~uFound) == 0 )
+                continue;
+            if ( BestK == -1 )
             {
-                printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i );
-                pArgs[nArgs++] = pTemp;
+                BestK      = k;
+                pEvalBest  = pEval;
+                WeightBest = Ivy_MultiWeight( pEvalBest->Mask, pEvalBest->Weight, uFound );
+                LevelBest  = Ivy_ObjLevel( Ivy_Regular(pEvalBest->pArg) );
+                continue;
+            }
+            // compare BestK and the new one (k)
+            WeightCur = Ivy_MultiWeight( pEval->Mask, pEval->Weight, uFound );
+            LevelCur = Ivy_ObjLevel( Ivy_Regular(pEval->pArg) );
+            if ( WeightBest < WeightCur || 
+                (WeightBest == WeightCur && LevelBest > LevelCur) )
+            {
+                BestK      = k;
+                pEvalBest  = pEval;
+                WeightBest = WeightCur;
+                LevelBest  = LevelCur;
             }
         }
-    printf( "     ((%d/%d))    ", nArgsOld, nArgs-nArgsOld );
-    return NULL;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
-    Ivy_Obj_t * pArgsRef[5], * pTemp;
-    int i, k, m, nArgsNew, Counter = 0;
- 
-    
-//Ivy_MultiEval( pArgs, nArgs, Type );  printf( "\n" );
-
-
-    assert( Type == IVY_AND || Type == IVY_EXOR );
-    assert( nArgs > 0 );
-    if ( nArgs == 1 )
-        return pArgs[0];
-
-    // find the nodes with more than one fanout
-    nArgsNew = 0;
-    for ( i = 0; i < nArgs; i++ )
-        if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 )
-            pArgsRef[nArgsNew++] = pArgs[i];
-
-    // go through pairs
-    if ( nArgsNew >= 2 )
-    for ( i = 0; i < nArgsNew; i++ )
-    for ( k = i + 1; k < nArgsNew; k++ )
-        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
-            Counter++;
-//    printf( "%d", Counter );
-            
-    // go through pairs
-    if ( nArgsNew >= 2 )
-    for ( i = 0; i < nArgsNew; i++ )
-    for ( k = i + 1; k < nArgsNew; k++ )
-        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+        assert( BestK != -1 );
+        // if the cost is only 1, take the leaf
+        if ( WeightBest == 1 && BestK >= nLeaves )
         {
-            nArgsNew = 0;
-            for ( m = 0; m < nArgs; m++ )
-                if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] )
-                    pArgs[nArgsNew++] = pArgs[m];
-            pArgs[nArgsNew++] = pTemp;
-            assert( nArgsNew == nArgs - 1 );
-            return Ivy_Multi1( pArgs, nArgsNew, Type );
+            uTemp = (pEvalBest->Mask & ~uFound);
+            for ( k = 0; k < nLeaves; k++ )
+                if ( uTemp & (1 << k) )
+                    break;
+            assert( k < nLeaves );
+            BestK     = k;
+            pEvalBest = pEvals + BestK;
         }
-    return Ivy_Multi_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
-    assert( Type == IVY_AND || Type == IVY_EXOR );
-    assert( nArgs > 0 );
-    return Ivy_Multi_rec( pArgs, nArgs, Type );
+        if ( fVerbose )
+        {
+            if ( BestK < nLeaves )
+                printf( "L(%d) ", BestK );
+            else
+                printf( "%d ", BestK - nLeaves );
+        }
+        // update the found set
+        Vec_PtrPush( vSols, pEvalBest->pArg );
+        uFound |= pEvalBest->Mask;
+        if ( uFound == uMaskAll )
+            break;
+    }
+    if ( uFound == uMaskAll )
+    {
+        if ( fVerbose )
+            printf( "  Found \n\n" );
+        return 1;
+    }
+    else
+    {
+        if ( fVerbose )
+            printf( "  Not found \n\n" );
+        return 0;
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyMulti8.c b/src/temp/ivy/ivyMulti8.c
new file mode 100644
index 00000000..059d1500
--- /dev/null
+++ b/src/temp/ivy/ivyMulti8.c
@@ -0,0 +1,427 @@
+/**CFile****************************************************************
+
+  FileName    [ivyMulti.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Constructing multi-input AND/EXOR gates.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyMulti.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Eval_t_ Ivy_Eval_t;
+struct Ivy_Eval_t_
+{
+    unsigned Mask   :  5;  // the mask of covered nodes
+    unsigned Weight :  3;  // the number of covered nodes
+    unsigned Cost   :  4;  // the number of overlapping nodes
+    unsigned Level  : 12;  // the level of this node
+    unsigned Fan0   :  4;  // the first fanin
+    unsigned Fan1   :  4;  // the second fanin
+};
+
+static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+static void        Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs );
+static int         Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode );
+static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**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_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Ivy_Multi_rec( ppObjs,           nObjs/2,         Type );
+    pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+    return Ivy_Oper( pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs a balanced tree while taking sharing into account.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type )
+{
+    static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5};
+    static Ivy_Eval_t pEvals[15+15*14/2];
+    static Ivy_Obj_t * pArgs[16];
+    Ivy_Eval_t * pEva, * pEvaBest;
+    int nArgsNew, nEvals, i, k;
+    Ivy_Obj_t * pTemp;
+
+    // consider the case of one argument
+    assert( nArgs > 0 );
+    if ( nArgs == 1 )
+        return pArgsInit[0];
+    // consider the case of two arguments
+    if ( nArgs == 2 )
+        return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type );
+
+//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" );
+
+    // set the initial ones
+    for ( i = 0; i < nArgs; i++ )
+    {
+        pArgs[i] = pArgsInit[i];
+        pEva = pEvals + i;
+        pEva->Mask   = (1 << i);
+        pEva->Weight = 1;
+        pEva->Cost   = 0; 
+        pEva->Level  = Ivy_Regular(pArgs[i])->Level; 
+        pEva->Fan0   = 0; 
+        pEva->Fan1   = 0; 
+    }
+
+    // find the available nodes
+    pEvaBest = pEvals;
+    nArgsNew = nArgs;
+    for ( i = 1; i < nArgsNew; i++ )
+    for ( k = 0; k < i; k++ )
+        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) )
+        {
+            pEva = pEvals + nArgsNew;
+            pEva->Mask   = pEvals[k].Mask | pEvals[i].Mask;
+            pEva->Weight = NumBits[pEva->Mask];
+            pEva->Cost   = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; 
+            pEva->Level  = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); 
+            pEva->Fan0   = k; 
+            pEva->Fan1   = i; 
+//            assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) );
+            // compare
+            if ( pEvaBest->Weight < pEva->Weight ||
+                 pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
+                 pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
+                 pEvaBest = pEva;
+            // save the argument
+            pArgs[nArgsNew++] = pTemp;
+            if ( nArgsNew == 15 )
+                goto Outside;
+        }
+Outside:
+
+//    printf( "Best = %d.\n", pEvaBest - pEvals );
+
+    // the case of no common nodes
+    if ( nArgsNew == nArgs )
+    {
+        Ivy_MultiSort( pArgs, nArgs );
+        return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+    }
+    // the case of one common node
+    if ( nArgsNew == nArgs + 1 )
+    {
+        assert( pEvaBest - pEvals == nArgs );
+        k = 0;
+        for ( i = 0; i < nArgs; i++ )
+            if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 )
+                pArgs[k++] = pArgs[i];
+        pArgs[k++] = pArgs[nArgs];
+        assert( k == nArgs - 1 );
+        nArgs = k;
+        Ivy_MultiSort( pArgs, nArgs );
+        return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+    }
+    // the case when there is a node that covers everything
+    if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) )
+        return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type ); 
+
+    // evaluate node pairs
+    nEvals = nArgsNew;
+    for ( i = 1; i < nArgsNew; i++ )
+    for ( k = 0; k < i; k++ )
+    {
+        pEva = pEvals + nEvals;
+        pEva->Mask   = pEvals[k].Mask | pEvals[i].Mask;
+        pEva->Weight = NumBits[pEva->Mask];
+        pEva->Cost   = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask]; 
+        pEva->Level  = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level); 
+        pEva->Fan0   = k; 
+        pEva->Fan1   = i; 
+        // compare
+        if ( pEvaBest->Weight < pEva->Weight ||
+             pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
+             pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
+             pEvaBest = pEva;
+        // save the argument
+        nEvals++;
+    }
+    assert( pEvaBest - pEvals >= nArgsNew );
+
+//    printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 );
+
+    // get the best implementation
+    pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
+
+    // collect those not covered by EvaBest
+    k = 0;
+    for ( i = 0; i < nArgs; i++ )
+        if ( (pEvaBest->Mask & (1 << i)) == 0 )
+            pArgs[k++] = pArgs[i];
+    pArgs[k++] = pTemp;
+    assert( k == nArgs - (int)pEvaBest->Weight + 1 );
+    nArgs = k;
+    Ivy_MultiSort( pArgs, nArgs );
+    return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements multi-input AND/EXOR operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pNode0, * pNode1;
+    if ( iNum < nArgs )
+        return pArgs[iNum];
+    pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type );
+    pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type );
+    return Ivy_Oper( pNode0, pNode1, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selection-sorts the nodes in the decreasing over of level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
+{
+    Ivy_Obj_t * pTemp;
+    int i, j, iBest;
+
+    for ( i = 0; i < nArgs-1; i++ )
+    {
+        iBest = i;
+        for ( j = i+1; j < nArgs; j++ )
+            if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level )
+                iBest = j;
+        pTemp = pArgs[i]; 
+        pArgs[i] = pArgs[iBest]; 
+        pArgs[iBest] = pTemp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts a new node in the order by levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pNode1, * pNode2;
+    int i;
+    // try to find the node in the array
+    for ( i = 0; i < nArgs; i++ )
+        if ( pArray[i] == pNode )
+            return nArgs;
+    // put the node last
+    pArray[nArgs++] = pNode;
+    // find the place to put the new node
+    for ( i = nArgs-1; i > 0; i-- )
+    {
+        pNode1 = pArray[i  ];
+        pNode2 = pArray[i-1];
+        if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
+            break;
+        pArray[i  ] = pNode2;
+        pArray[i-1] = pNode1;
+    }
+    return nArgs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Balances the array recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pNodeNew;
+    // consider the case of one argument
+    assert( nArgs > 0 );
+    if ( nArgs == 1 )
+        return pArgs[0];
+    // consider the case of two arguments
+    if ( nArgs == 2 )
+        return Ivy_Oper( pArgs[0], pArgs[1], Type );
+    // get the last two nodes
+    pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type );
+    // add the new node
+    nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew );
+    return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements multi-input AND/EXOR operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pTemp;
+    int i, k;
+    int nArgsOld = nArgs;
+    for ( i = 0; i < nArgs; i++ )
+        printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level );
+    for ( i = 1; i < nArgs; i++ )
+        for ( k = 0; k < i; k++ )
+        {
+            pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE));
+            if ( pTemp != NULL )
+            {
+                printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i );
+                pArgs[nArgs++] = pTemp;
+            }
+        }
+    printf( "     ((%d/%d))    ", nArgsOld, nArgs-nArgsOld );
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pArgsRef[5], * pTemp;
+    int i, k, m, nArgsNew, Counter = 0;
+ 
+    
+//Ivy_MultiEval( pArgs, nArgs, Type );  printf( "\n" );
+
+
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    if ( nArgs == 1 )
+        return pArgs[0];
+
+    // find the nodes with more than one fanout
+    nArgsNew = 0;
+    for ( i = 0; i < nArgs; i++ )
+        if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 )
+            pArgsRef[nArgsNew++] = pArgs[i];
+
+    // go through pairs
+    if ( nArgsNew >= 2 )
+    for ( i = 0; i < nArgsNew; i++ )
+    for ( k = i + 1; k < nArgsNew; k++ )
+        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+            Counter++;
+//    printf( "%d", Counter );
+            
+    // go through pairs
+    if ( nArgsNew >= 2 )
+    for ( i = 0; i < nArgsNew; i++ )
+    for ( k = i + 1; k < nArgsNew; k++ )
+        if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+        {
+            nArgsNew = 0;
+            for ( m = 0; m < nArgs; m++ )
+                if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] )
+                    pArgs[nArgsNew++] = pArgs[m];
+            pArgs[nArgsNew++] = pTemp;
+            assert( nArgsNew == nArgs - 1 );
+            return Ivy_Multi1( pArgs, nArgsNew, Type );
+        }
+    return Ivy_Multi_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    return Ivy_Multi_rec( pArgs, nArgs, Type );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 5d063525..703218bb 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -51,6 +51,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
     // 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 );
     }
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
index a10ba343..96f78165 100644
--- a/src/temp/ivy/ivyOper.c
+++ b/src/temp/ivy/ivyOper.c
@@ -81,7 +81,7 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
 Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
     Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
-    Ivy_Obj_t * pFan0, * pFan1;
+//    Ivy_Obj_t * pFan0, * pFan1;
     // check trivial cases
     if ( p0 == p1 )
         return p0;
@@ -92,8 +92,8 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
     if ( Ivy_Regular(p1) == pConst1 )
         return p1 == pConst1 ? p0 : Ivy_Not(pConst1);
     // check if it can be an EXOR gate
-    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
-        return Ivy_CanonExor( pFan0, pFan1 );
+//    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
+//        return Ivy_CanonExor( pFan0, pFan1 );
     return Ivy_CanonAnd( p0, p1 );
 }
 
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
new file mode 100644
index 00000000..2d65e7f7
--- /dev/null
+++ b/src/temp/ivy/ivyResyn.c
@@ -0,0 +1,96 @@
+/**CFile****************************************************************
+
+  FileName    [ivyResyn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [AIG rewriting script.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyResyn.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs several passes of rewriting on the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel )
+{
+    int clk, fVerbose = 0;
+    Ivy_Man_t * pTemp;
+
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+clk = clock();
+    pMan = Ivy_ManBalance( pMan, fUpdateLevel );
+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 ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+    Ivy_ManStop( pTemp );
+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 );
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+    Ivy_ManStop( pTemp );
+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 ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+    Ivy_ManStop( pTemp );
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+    return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c
new file mode 100644
index 00000000..234827ff
--- /dev/null
+++ b/src/temp/ivy/ivyRwrAlg.c
@@ -0,0 +1,408 @@
+/**CFile****************************************************************
+
+  FileName    [ivyRwrAlg.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Algebraic AIG rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyRwrAlg.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost );
+static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Algebraic AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
+{
+    Vec_Int_t * vRequired;
+    Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol;
+    Ivy_Obj_t * pObj, * pResult;
+    int i, RetValue, LevelR, nNodesOld;
+    int CountUsed, CountUndo;
+    vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL;
+    vFront    = Vec_PtrAlloc( 100 );
+    vLeaves   = Vec_PtrAlloc( 100 );
+    vCone     = Vec_PtrAlloc( 100 );
+    vSol      = Vec_PtrAlloc( 100 );
+    // go through the nodes in the topological order
+    CountUsed = CountUndo = 0;
+    nNodesOld = Ivy_ManObjIdNext(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        assert( !Ivy_ObjIsBuf(pObj) );
+        if ( i >= nNodesOld )
+            break;
+        // skip no-nodes and MUX roots
+        if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) )
+            continue;
+//        if ( pObj->Id > 297 ) // 296 --- 297 
+//            break;
+        if ( pObj->Id == 297 )
+        {
+            int x = 0;
+        }
+        // get the largest algebraic cut
+        RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone );
+        // the case of a trivial tree cut
+        if ( RetValue == 1 )
+            continue;
+        // the case of constant 0 cone
+        if ( RetValue == -1 )
+        {
+            Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 ); 
+            continue;
+        }
+        assert( Vec_PtrSize(vLeaves) > 2 );
+        // get the required level for this node
+        LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000;
+        // create a new cone
+        pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost );
+        if ( pResult == NULL || pResult == pObj )
+            continue;
+        assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) );
+        if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
+            Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
+        else
+            Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++; 
+    }
+    printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
+    Vec_PtrFree( vFront );
+    Vec_PtrFree( vCone );
+    Vec_PtrFree( vSol );
+    if ( vRequired ) Vec_IntFree( vRequired );
+    if ( i = Ivy_ManCleanup(p) )
+        printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManRewriteAlg(): The check has failed.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Analizes one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost )
+{
+    int fVerbose = 0;
+    Ivy_Obj_t * pTemp;
+    int k, Counter, nMffc, RetValue;
+
+    if ( fVerbose )
+    {
+        if ( Ivy_ObjIsExor(pObj) )
+            printf( "x " );
+        else
+            printf( "  " );
+    }
+
+/*       
+    printf( "%d ", Vec_PtrSize(vFront) );
+    printf( "( " );
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+    printf( ")\n" );
+*/
+    // collect nodes in the cone
+    if ( Ivy_ObjIsExor(pObj) )
+        Ivy_ManCollectCone( pObj, vFront, vCone );
+    else
+        Ivy_ManCollectCone( pObj, vLeaves, vCone );
+
+    // deref nodes in the cone
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+    {
+        Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) );
+        Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) );
+        pTemp->fMarkB = 1;
+    }
+
+    // count the MFFC size
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        Ivy_Regular(pTemp)->fMarkA = 1;
+    nMffc = Ivy_NodeCountMffc( pObj );
+    Vec_PtrForEachEntry( vFront, pTemp, k )
+        Ivy_Regular(pTemp)->fMarkA = 0;
+
+    if ( fVerbose )
+    {
+    Counter = 0;
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+        Counter += (Ivy_ObjRefs(pTemp) > 0);
+    printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d.   Mffc = %d.   Lev = %d.  LevR = %d.\n", 
+        pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR );
+    }
+/*
+    printf( "Leaves:" );
+    Vec_PtrForEachEntry( vLeaves, pTemp, k )
+        printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" );
+    printf( "\n" );
+    printf( "Cone:\n" );
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+        printf( " %5d = %d%s %d%s\n", pTemp->Id,
+            Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "",
+            Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" );
+*/
+
+    RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols );
+
+    // ref nodes in the cone
+    Vec_PtrForEachEntry( vCone, pTemp, k )
+    {
+        Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) );
+        Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) );
+        pTemp->fMarkA = 0;
+        pTemp->fMarkB = 0;
+    }
+
+    if ( !RetValue )
+        return NULL;
+
+    if ( Vec_PtrSize( vSols ) == 1 )
+        return Vec_PtrEntry( vSols, 0 );
+    return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCountMffc_rec( Ivy_Obj_t * pNode )
+{
+    if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA )
+        return 0;
+    assert( pNode->fMarkB );
+    pNode->fMarkA = 1;
+//    printf( "%d ", pNode->Id );
+    if ( Ivy_ObjIsBuf(pNode) )
+        return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) );
+    return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCountMffc( Ivy_Obj_t * pNode )
+{
+    assert( pNode->fMarkB );
+    return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison for node pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Returns 1 if the tree-leaves of this node where traversed 
+  and found to have no external references (and have not been collected). 
+  Returns 0 if the tree-leaves have external references and are collected.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
+{
+    int RetValue0, RetValue1;
+    Ivy_Obj_t * pObjR = Ivy_Regular(pObj);
+    assert( !Ivy_ObjIsBuf(pObjR) );
+    assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) );
+
+    // make sure the node is not visited twice in different polarities
+    if ( Ivy_IsComplement(pObj) )
+    { // if complemented, mark B
+        if ( pObjR->fMarkA )
+            return -1;
+        pObjR->fMarkB = 1;
+    }
+    else
+    { // if non-complicated, mark A
+        if ( pObjR->fMarkB )
+            return -1;
+        pObjR->fMarkA = 1;
+    }
+    Vec_PtrPush( vCone, pObjR );
+
+    // if the node is the end of the tree, return
+    if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type )
+    {
+        if ( Ivy_ObjRefs(pObjR) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pObjR) > 1 );
+        Vec_PtrPush( vFront, pObj );
+        return 0;
+    }
+
+    // branch on the node
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    // what if buffer has more than one fanout???
+    RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone );
+    RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone );
+    if ( RetValue0 == -1 || RetValue1 == -1 )
+        return -1;
+
+    // the case when both have no external references
+    if ( RetValue0 && RetValue1 )
+    {
+        if ( Ivy_ObjRefs(pObj) == 1 )
+            return 1;
+        assert( Ivy_ObjRefs(pObj) > 1 );
+        Vec_PtrPush( vFront, pObj );
+        return 0;
+    }
+    // the case when one of them has external references
+    if ( RetValue0 )
+        Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) );
+    if ( RetValue1 )
+        Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing one algebraic cut.]
+
+  Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
+  (c) boundary of different gates. Returns 1 if this is a pure tree.
+  Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+    Ivy_Obj_t * pObj, * pPrev;
+    int RetValue, i;
+    assert( !Ivy_IsComplement(pRoot) );
+    assert( Ivy_ObjIsNode(pRoot) );
+    // clear the frontier and collect the nodes
+    Vec_PtrClear( vCone );
+    Vec_PtrClear( vFront );
+    Vec_PtrClear( vLeaves );
+    RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone );
+    // clean the marks
+    Vec_PtrForEachEntry( vCone, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+    // quit if the same node is found in both polarities
+    if ( RetValue == -1 )
+        return -1;
+    // return if the node is the root of a tree
+    if ( RetValue == 1 )
+        return 1;
+    // return if the cut is composed of two nodes
+    if ( Vec_PtrSize(vFront) <= 2 )
+        return 1;
+    // sort the entries in increasing order
+    Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
+    // remove duplicates from vFront and save the nodes in vLeaves
+    pPrev = Vec_PtrEntry(vFront, 0);
+    Vec_PtrPush( vLeaves, pPrev );
+    Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
+    {
+        // compare current entry and the previous entry
+        if ( pObj == pPrev )
+        {
+            if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0
+            {
+                // vLeaves are no longer structural support of pRoot!!!
+                Vec_PtrPop(vLeaves);  
+                pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves);
+            }
+            continue;
+        }
+        if ( pObj == Ivy_Not(pPrev) )
+        {
+            assert( Ivy_ObjIsAnd(pRoot) );
+            return -1;
+        }
+        pPrev = pObj;
+        Vec_PtrPush( vLeaves, pObj );
+    }
+    if ( Vec_PtrSize(vLeaves) == 0 )
+        return -1;
+    if ( Vec_PtrSize(vLeaves) <= 2 )
+        return 1;
+    return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
new file mode 100644
index 00000000..243ab261
--- /dev/null
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+  FileName    [ivyRwtPre.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Rewriting based on precomputation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+#include "deco.h"
+#include "rwt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+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, 
+    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 );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose )
+{
+    Rwt_Man_t * pManRwt;
+    Ivy_Obj_t * pNode;
+    int i, nNodes, nGain;
+    int clk, clkStart = clock();
+    // start the rewriting manager
+    pManRwt = Rwt_ManStart( 0 );
+    if ( pManRwt == NULL )
+        return 0;
+    // compute the reverse levels if level update is requested
+    if ( fUpdateLevel )
+        Ivy_ManRequiredLevels( p );
+    // resynthesize each node once
+    nNodes = Ivy_ManObjIdNext( p );
+    Ivy_ManForEachObj( p, pNode, i )
+    {
+        if ( !Ivy_ObjIsNode(pNode) )
+            continue;
+        // fix the fanin buffer problem
+        Ivy_NodeFixBufferFanins( pNode );
+        if ( Ivy_ObjIsBuf(pNode) )
+            continue;
+        // stop if all nodes have been tried once
+        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 );
+        if ( nGain > 0 || nGain == 0 && fUseZeroCost )
+        {
+            Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
+            int fCompl           = Rwt_ManReadCompl(pManRwt);
+/*
+            {
+                Ivy_Obj_t * pObj;
+                int i;
+                printf( "USING: (" );
+                Vec_PtrForEachEntry( Rwt_ManReadLeaves(pManRwt), pObj, i )
+                    printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) );
+                printf( ")   Gain = %d.\n", nGain );
+            }
+            if ( nGain > 0 )
+            { // print stats on the MFFC
+                extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode );
+                printf( "Node %6d : Gain = %4d  ", pNode->Id, nGain );
+                Ivy_NodeMffsConeSuppPrint( pNode );
+            }
+*/
+            // complement the FF if needed
+clk = clock();
+            if ( fCompl ) Dec_GraphComplement( pGraph );
+            Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+            if ( fCompl ) Dec_GraphComplement( pGraph );
+Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+        }
+    }
+Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+    // print stats
+    if ( fVerbose )
+        Rwt_ManPrintStats( pManRwt );
+    // delete the managers
+    Rwt_ManStop( pManRwt );
+    // fix the levels
+    if ( fUpdateLevel )
+        Vec_IntFree( p->vRequired ), p->vRequired = NULL;
+    // check
+    if ( i = Ivy_ManCleanup(p) )
+        printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManRewritePre(): The check has failed.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs rewriting for one node.]
+
+  Description [This procedure considers all the cuts computed for the node
+  and tries to rewrite each of them using the "forest" of different AIG
+  structures precomputed and stored in the RWR manager. 
+  Determines the best rewriting and computes the gain in the number of AIG
+  nodes in the final network. In the end, p->vFanins contains information 
+  about the best cut that can be used for rewriting, while p->pGraph gives 
+  the decomposition dag (represented using decomposition graph data structure).
+  Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost )
+{
+    int fVeryVerbose = 0;
+    Dec_Graph_t * pGraph;
+    Ivy_Store_t * pStore;
+    Ivy_Cut_t * pCut;
+    Ivy_Obj_t * pFanin;
+    unsigned uPhase, uTruthBest, uTruth;
+    char * pPerm;
+    int Required, nNodesSaved, nNodesSaveCur;
+    int i, c, GainCur, GainBest = -1;
+    int clk, clk2;
+
+    p->nNodesConsidered++;
+    // get the required times
+    Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000;
+    // get the node's cuts
+clk = clock();
+    pStore = Ivy_NodeFindCutsAll( pNode, 5 );
+p->timeCut += clock() - clk;
+
+    // go through the cuts
+clk = clock();
+    for ( c = 1; c < pStore->nCuts; c++ )
+    {
+        pCut = pStore->pCuts + c;
+        // consider only 4-input cuts
+        if ( pCut->nSize != 4 )
+            continue;
+        // skip the cuts with buffers
+        for ( i = 0; i < (int)pCut->nSize; i++ )
+            if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, 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
+p->timeTruth += clock() - clk2;
+        pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+        uPhase = p->pPhases[uTruth];
+        // collect fanins with the corresponding permutation/phase
+        Vec_PtrClear( p->vFaninsCur );
+        Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
+        for ( i = 0; i < (int)pCut->nSize; i++ )
+        {
+            pFanin = Ivy_ObjObj( pNode, 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 );
+        }
+clk2 = clock();
+/*
+        printf( "Considering: (" );
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pFanin)) );
+        printf( ")\n" );
+*/
+        // mark the fanin boundary 
+        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 );
+        // unmark the fanin boundary
+        Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+            Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+p->timeMffc += clock() - clk2;
+
+        // evaluate the cut
+clk2 = clock();
+        pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+p->timeEval += clock() - clk2;
+
+        // check if the cut is better than the current best one
+        if ( pGraph != NULL && GainBest < GainCur )
+        {
+            // save this form
+            nNodesSaveCur = nNodesSaved;
+            GainBest  = GainCur;
+            p->pGraph  = pGraph;
+            p->fCompl = ((uPhase & (1<<4)) > 0);
+            uTruthBest = uTruth;
+            // collect fanins in the
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+                Vec_PtrPush( p->vFanins, pFanin );
+        }
+    }
+p->timeRes += clock() - clk;
+
+    if ( GainBest == -1 )
+        return -1;
+
+//    printf( "%d", nNodesSaveCur - GainBest );
+/*
+    if ( GainBest > 0 )
+    {
+        if ( Rwt_CutIsintean( pNode, p->vFanins ) )
+            printf( "b" );
+        else
+        {
+            printf( "Node %d : ", pNode->Id );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+                printf( "%d ", Ivy_Regular(pFanin)->Id );
+            printf( "a" );
+        }
+    }
+*/
+/*
+    if ( GainBest > 0 )
+        if ( p->fCompl )
+            printf( "c" );
+        else
+            printf( "." );
+*/
+
+    // copy the leaves
+    Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+        Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
+
+    p->nScores[p->pMap[uTruthBest]]++;
+    p->nNodesGained += GainBest;
+    if ( fUseZeroCost || GainBest > 0 )
+        p->nNodesRewritten++;
+
+    // report the progress
+    if ( fVeryVerbose && GainBest > 0 )
+    {
+        printf( "Node %6d :   ", Ivy_ObjId(pNode) );
+        printf( "Fanins = %d. ", p->vFanins->nSize );
+        printf( "Save = %d.  ", nNodesSaveCur );
+        printf( "Add = %d.  ",  nNodesSaveCur-GainBest );
+        printf( "GAIN = %d.  ", GainBest );
+        printf( "Cone = %d.  ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+        printf( "Class = %d.  ", p->pMap[uTruthBest] );
+        printf( "\n" );
+    }
+    return GainBest;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [References/references the node and returns MFFC size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
+{
+    Ivy_Obj_t * pNode0, * pNode1;
+    int Counter;
+    // label visited nodes
+    if ( fLabel )
+        Ivy_ObjSetTravIdCurrent( pNode );
+    // skip the CI
+    if ( Ivy_ObjIsCi(pNode) )
+        return 0;
+    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
+    // process the internal node
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    Counter = Ivy_ObjIsNode(pNode);
+    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 );
+    }
+    else
+    {
+        assert( pNode0->nRefs > 0 );
+        assert( 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 );
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the size of MFFC and labels nodes with the current TravId.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeMffcLabel( 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
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    return nConeSize1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth_rec( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+    static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned uTruth0, uTruth1;
+    int i;
+    for ( i = 0; i < nNums; i++ )
+        if ( pObj->Id == pNums[i] )
+            return uMasks[i];
+    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+    uTruth0 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin0(pObj), pNums, nNums );
+    if ( Ivy_ObjFaninC0(pObj) )
+        uTruth0 = ~uTruth0;
+    if ( Ivy_ObjIsBuf(pObj) )
+        return uTruth0;
+    uTruth1 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin1(pObj), pNums, nNums );
+    if ( Ivy_ObjFaninC1(pObj) )
+        uTruth1 = ~uTruth1;
+    return uTruth0 & uTruth1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+    assert( nNums < 6 );
+    return Ivy_NodeGetTruth_rec( pObj, pNums, nNums );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  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 )
+{
+    Vec_Ptr_t * vSubgraphs;
+    Dec_Graph_t * pGraphBest, * pGraphCur;
+    Rwt_Node_t * pNode, * pFanin;
+    int nNodesAdded, GainBest, i, k;
+    // find the matching class of subgraphs
+    vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+    p->nSubgraphs += vSubgraphs->nSize;
+    // determine the best subgraph
+    GainBest = -1;
+    Vec_PtrForEachEntry( vSubgraphs, pNode, i )
+    {
+        // get the current graph
+        pGraphCur = (Dec_Graph_t *)pNode->pNext;
+        // copy the leaves
+        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 );
+        if ( nNodesAdded == -1 )
+            continue;
+        assert( nNodesSaved >= nNodesAdded );
+        // count the gain at this node
+        if ( GainBest < nNodesSaved - nNodesAdded )
+        {
+            GainBest   = nNodesSaved - nNodesAdded;
+            pGraphBest = pGraphCur;
+        }
+    }
+    if ( GainBest == -1 )
+        return NULL;
+    *pGainBest = GainBest;
+    return pGraphBest;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of new nodes added when using this graph.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
+  of the leaves of the graph before calling this procedure. 
+  Returns -1 if the number of nodes and levels exceeded the given limit or 
+  the number of levels exceeded the maximum allowed level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+    Dec_Node_t * pNode, * pNode0, * pNode1;
+    Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
+    int i, Counter, LevelNew, LevelOld;
+    // check for constant function or a literal
+    if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+        return 0;
+    // set the levels of the leaves
+    Dec_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->Level = Ivy_Regular(pNode->pFunc)->Level;
+    // compute the AIG size after adding the internal nodes
+    Counter = 0;
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        // get the children of this node
+        pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+        pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+        // get the AIG nodes corresponding to the children 
+        pAnd0 = pNode0->pFunc; 
+        pAnd1 = pNode1->pFunc; 
+        if ( pAnd0 && pAnd1 )
+        {
+            // 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) );
+            // return -1 if the node is the same as the original root
+            if ( Ivy_Regular(pAnd) == pRoot )
+                return -1;
+        }
+        else
+            pAnd = NULL;
+        // count the number of added nodes
+        if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) )
+        {
+            if ( ++Counter > NodeMax )
+                return -1;
+        }
+        // count the number of new levels
+        LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level );
+        if ( pAnd )
+        {
+            if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) )
+                LevelNew = 0;
+            else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) )
+                LevelNew = (int)Ivy_Regular(pAnd0)->Level;
+            else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd1) )
+                LevelNew = (int)Ivy_Regular(pAnd1)->Level;
+            LevelOld = (int)Ivy_Regular(pAnd)->Level;
+//            assert( LevelNew == LevelOld );
+        }
+        if ( LevelNew > LevelMax )
+            return -1;
+        pNode->pFunc = pAnd;
+        pNode->Level = LevelNew;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+  of the leaves of the graph before calling this procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, 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) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        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 );
+    }
+    // complement the result if necessary
+    return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetwork( 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));
+    // create the new structure of nodes
+    pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph );
+    // remove the old nodes
+//    Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel );
+    Ivy_ObjReplace( pRoot, pRootNew, 1, 0 );
+    // compare the gains
+    nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+    assert( nGain <= nNodesOld - nNodesNew );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 590affd7..3d1ac335 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -362,6 +362,222 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
     return vLatches;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManReadLevels( 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 );
+    }
+    return LevelMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the real fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjReal( 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) );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the cube has exactly one 1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_TruthHasOneOne( unsigned uCube )
+{
+    return (uCube & (uCube - 1)) == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes are distance-1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
+{
+    unsigned uTemp = uCube1 | uCube2;
+    return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if two cubes differ in only one literal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
+{
+    unsigned uTemp = uCube1 ^ uCube2;
+    return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Combines two distance 1 cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 )
+{
+    unsigned uTemp;
+    uTemp = uCube1 | uCube2;
+    uTemp &= (uTemp >> 1) & 0x55555555;
+    assert( Ivy_TruthHasOneOne(uTemp) );
+    uTemp |= (uTemp << 1);
+    return (uCube1 | uCube2) ^ uTemp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Estimates the number of AIG nodes in the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
+{
+    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" );
+        }
+    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-- )
+    {
+        for ( k = 0; k < nRes; k++ )
+            if ( (uCover[i] & uResult[k]) == uResult[k] )
+                break;
+        if ( k != nRes )
+            continue;
+        uResult[nRes++] = uCover[i];
+    }
+    // count the number of literals
+    Counter = 0;
+    for ( i = 0; i < nRes; i++ )
+    {
+        for ( k = 0; k < nVars; k++ )
+            if ( uResult[i] & (3 << (k<<1)) )
+                Counter++;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tests the cover procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthEstimateNodesTest()
+{
+    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) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index beadb8b9..f697910b 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -8,7 +8,8 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyMulti.c \
     src/temp/ivy/ivyObj.c \
     src/temp/ivy/ivyOper.c \
-    src/temp/ivy/ivyRewrite.c \
+    src/temp/ivy/ivyResyn.c \
+    src/temp/ivy/ivyRwrPre.c \
     src/temp/ivy/ivySeq.c \
     src/temp/ivy/ivyTable.c \
     src/temp/ivy/ivyUndo.c \