Version abc60812

13 files changed, 1009 insertions, 99 deletions

diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index a36c795b..2409284e 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -110,14 +110,17 @@ struct Ivy_Man_t_
     int              nTravIds;       // the traversal ID
     int              nLevelMax;      // the maximum level
     Vec_Int_t *      vRequired;      // required times
-//    Vec_Ptr_t *      vFanouts;       // representation of the fanouts
     int              fFanout;        // fanout is allocated
     void *           pData;          // the temporary data
     void *           pCopy;          // the temporary data
+    Ivy_Man_t *      pHaig;          // history AIG if present
     // memory management
     Vec_Ptr_t *      vChunks;        // allocated memory pieces
     Vec_Ptr_t *      vPages;         // memory pages used by nodes
     Ivy_Obj_t *      pListFree;      // the list of free nodes 
+    // timing statistics
+    int              time1;
+    int              time2;
 };
 
 
@@ -197,51 +200,54 @@ static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->nO
 static inline int          Ivy_ManHashObjNum( Ivy_Man_t * p )     { return p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]+p->nObjs[IVY_LATCH];     }
 static inline int          Ivy_ManGetCost( Ivy_Man_t * p )        { return p->nObjs[IVY_AND]+3*p->nObjs[IVY_EXOR]+8*p->nObjs[IVY_LATCH]; }
 
-static inline Ivy_Type_t   Ivy_ObjType( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type;               }
-static inline Ivy_Init_t   Ivy_ObjInit( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Init;               }
-static inline int          Ivy_ObjIsConst1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Id == 0;            }
-static inline int          Ivy_ObjIsGhost( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->Id < 0;             }
-static inline int          Ivy_ObjIsNone( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_NONE;   }
-static inline int          Ivy_ObjIsPi( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI;     }
-static inline int          Ivy_ObjIsPo( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO;     }
-static inline int          Ivy_ObjIsCi( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
-static inline int          Ivy_ObjIsCo( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
-static inline int          Ivy_ObjIsAssert( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ASSERT; }
-static inline int          Ivy_ObjIsLatch( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LATCH;  }
-static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND;    }
-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_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_ObjIsMarkA( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA;  }
-static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1;     }
-static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0;     }
+static inline Ivy_Type_t   Ivy_ObjType( Ivy_Obj_t * pObj )        { return pObj->Type;               }
+static inline Ivy_Init_t   Ivy_ObjInit( Ivy_Obj_t * pObj )        { return pObj->Init;               }
+static inline int          Ivy_ObjIsConst1( Ivy_Obj_t * pObj )    { return pObj->Id == 0;            }
+static inline int          Ivy_ObjIsGhost( Ivy_Obj_t * pObj )     { return pObj->Id < 0;             }
+static inline int          Ivy_ObjIsNone( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_NONE;   }
+static inline int          Ivy_ObjIsPi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI;     }
+static inline int          Ivy_ObjIsPo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO;     }
+static inline int          Ivy_ObjIsCi( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PI || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsCo( Ivy_Obj_t * pObj )        { return pObj->Type == IVY_PO || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsAssert( Ivy_Obj_t * pObj )    { return pObj->Type == IVY_ASSERT; }
+static inline int          Ivy_ObjIsLatch( Ivy_Obj_t * pObj )     { return pObj->Type == IVY_LATCH;  }
+static inline int          Ivy_ObjIsAnd( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_AND;    }
+static inline int          Ivy_ObjIsExor( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_EXOR;   }
+static inline int          Ivy_ObjIsBuf( Ivy_Obj_t * pObj )       { return pObj->Type == IVY_BUF;    }
+static inline int          Ivy_ObjIsNode( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
+static inline int          Ivy_ObjIsTerm( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_PI  || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
+static inline int          Ivy_ObjIsHash( Ivy_Obj_t * pObj )      { return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
+static inline int          Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj )  { return pObj->Type == IVY_PO  || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
+
+static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { return pObj->fMarkA;  }
+static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { pObj->fMarkA = 1;     }
+static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { pObj->fMarkA = 0;     }
  
-static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId;                                              }
-static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds;                          }
-static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = p->nTravIds - 1;                      }
-static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds);     }
-static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == p->nTravIds - 1); }
-
-static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { assert( !Ivy_IsComplement(pObj) ); return pObj->Id;                               }
-static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->fPhase;                           }
-static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->fExFan;                           }
-static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj->nRefs;                            }
-static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->nRefs++;                                 }
-static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
-static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
-static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
-static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin0);        }
-static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return Ivy_IsComplement(pObj->pFanin1);        }
-static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin0);             }
-static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Regular(pObj->pFanin1);             }
-static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin0;                          }
-static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->pFanin1;                          }
-static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Level;                            }
-static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
+static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId )                { pObj->TravId = TravId;                               }
+static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { pObj->TravId = p->nTravIds;                          }
+static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )     { pObj->TravId = p->nTravIds - 1;                      }
+static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Man_t * p, Ivy_Obj_t * pObj )       { return (int )((int)pObj->TravId == p->nTravIds);     }
+static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Man_t * p, Ivy_Obj_t * pObj )      { return (int )((int)pObj->TravId == p->nTravIds - 1); }
+
+static inline int          Ivy_ObjId( Ivy_Obj_t * pObj )          { return pObj->Id;                               }
+static inline int          Ivy_ObjTravId( Ivy_Obj_t * pObj )      { return pObj->TravId;                           }
+static inline int          Ivy_ObjPhase( Ivy_Obj_t * pObj )       { return pObj->fPhase;                           }
+static inline int          Ivy_ObjExorFanout( Ivy_Obj_t * pObj )  { return pObj->fExFan;                           }
+static inline int          Ivy_ObjRefs( Ivy_Obj_t * pObj )        { return pObj->nRefs;                            }
+static inline void         Ivy_ObjRefsInc( Ivy_Obj_t * pObj )     { pObj->nRefs++;                                 }
+static inline void         Ivy_ObjRefsDec( Ivy_Obj_t * pObj )     { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
+static inline int          Ivy_ObjFaninId0( Ivy_Obj_t * pObj )    { return pObj->pFanin0? Ivy_ObjId(Ivy_Regular(pObj->pFanin0)) : 0; }
+static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { return pObj->pFanin1? Ivy_ObjId(Ivy_Regular(pObj->pFanin1)) : 0; }
+static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin0);        }
+static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { return Ivy_IsComplement(pObj->pFanin1);        }
+static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin0);             }
+static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { return Ivy_Regular(pObj->pFanin1);             }
+static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { return pObj->pFanin0;                          }
+static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { return pObj->pFanin1;                          }
+static inline Ivy_Obj_t *  Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL;  }
+static inline Ivy_Obj_t *  Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }
+static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { return pObj->Level;                            }
+static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * 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; 
@@ -415,10 +421,19 @@ extern void            Ivy_ObjPatchFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_
 extern void            Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vArray );
 extern Ivy_Obj_t *     Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern int             Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+/*=== ivyHaig.c ==========================================================*/
+extern void            Ivy_ManHaigStart( Ivy_Man_t * p );
+extern void            Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
+extern void            Ivy_ManHaigStop( Ivy_Man_t * p );
+extern void            Ivy_ManHaigPrintStats( Ivy_Man_t * p );
+extern void            Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew );
+extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
 /*=== ivyIsop.c ==========================================================*/
 extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
+extern Ivy_Man_t *     Ivy_ManDup( Ivy_Man_t * p );
 extern void            Ivy_ManStop( Ivy_Man_t * p );
 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
 extern int             Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel );
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
index 0303485a..3e8bd6d2 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -59,6 +59,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
     Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
     Ivy_ManForEachPi( p, pObj, i )
         pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
+    // if HAIG is defined, trasfer the pointers to the PIs/latches
+//    if ( p->pHaig )
+//        Ivy_ManHaigTrasfer( p, pNew );
     // balance the AIG
     vStore = Vec_VecAlloc( 50 );
     Ivy_ManForEachPo( p, pObj, i )
@@ -327,10 +330,18 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, i
     // get the two last nodes
     pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
     pObj2 = Vec_PtrEntry( vSuper, RightBound     );
+    if ( Ivy_Regular(pObj1) == p->pConst1 || Ivy_Regular(pObj2) == p->pConst1 )
+        return;
     // find the first node that can be shared
     for ( i = RightBound; i >= LeftBound; i-- )
     {
         pObj3 = Vec_PtrEntry( vSuper, i );
+        if ( Ivy_Regular(pObj3) == p->pConst1 )
+        {
+            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
+            return;
+        }
         pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
         if ( Ivy_TableLookup( p, pGhost ) )
         {
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 65ba4aac..d918c96c 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -889,7 +889,6 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves
 {
     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
-    Ivy_Man_t * pMan = p;
     Ivy_Obj_t * pLeaf;
     int i, k, iLeaf0, iLeaf1;
 
diff --git a/src/temp/ivy/ivyCutTrav.c b/src/temp/ivy/ivyCutTrav.c
new file mode 100644
index 00000000..ea57c9f5
--- /dev/null
+++ b/src/temp/ivy/ivyCutTrav.c
@@ -0,0 +1,473 @@
+/**CFile****************************************************************
+
+  FileName    [ivyCutTrav.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyCutTrav.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId );
+static void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront );
+static void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, int nLeaves, int nWords, Vec_Int_t * vStore );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes cuts for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Store_t * Ivy_NodeFindCutsTravAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves, int nNodeLimit, 
+                                      Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront, Vec_Int_t * vStore, Vec_Vec_t * vBitCuts )
+{
+    static Ivy_Store_t CutStore, * pCutStore = &CutStore;
+    Vec_Ptr_t * vCuts, * vCuts0, * vCuts1;
+    unsigned * pBitCut;
+    Ivy_Obj_t * pLeaf;
+    Ivy_Cut_t * pCut;
+    int i, k, nWords, nNodes;
+
+    assert( nLeaves <= IVY_CUT_INPUT );
+
+    // find the given number of nodes in the TFI
+    Ivy_NodeComputeVolume( pObj, nNodeLimit - 1, vNodes, vFront );
+    nNodes = Vec_PtrSize(vNodes);
+//    assert( nNodes <= nNodeLimit );
+
+    // make sure vBitCuts has enough room
+    Vec_VecExpand( vBitCuts, nNodes-1 );
+    Vec_VecClear( vBitCuts );
+
+    // prepare the memory manager
+    Vec_IntClear( vStore );
+    Vec_IntGrow( vStore, 64000 );
+
+    // set elementary cuts for the leaves
+    nWords = Extra_BitWordNum( nNodes );
+    Vec_PtrForEachEntry( vFront, pLeaf, i )
+    {
+        assert( Ivy_ObjTravId(pLeaf) < nNodes );
+        // get the new bitcut
+        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
+        // set it as the cut of this leaf
+        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
+    }
+
+    // compute the cuts for each node
+    Vec_PtrForEachEntry( vNodes, pLeaf, i )
+    {
+        // skip the leaves
+        vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pLeaf) );
+        if ( Vec_PtrSize(vCuts) > 0 )
+            continue;
+        // add elementary cut
+        pBitCut = Ivy_NodeCutElementary( vStore, nWords, Ivy_ObjTravId(pLeaf) );
+        // set it as the cut of this leaf
+        Vec_VecPush( vBitCuts, Ivy_ObjTravId(pLeaf), pBitCut );
+        // get the fanin cuts
+        vCuts0 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin0(pLeaf) ) );
+        vCuts1 = Vec_VecEntry( vBitCuts, Ivy_ObjTravId( Ivy_ObjFanin1(pLeaf) ) );
+        assert( Vec_PtrSize(vCuts0) > 0 );
+        assert( Vec_PtrSize(vCuts1) > 0 );
+        // merge the cuts
+        Ivy_NodeFindCutsMerge( vCuts0, vCuts1, vCuts, nLeaves, nWords, vStore );
+    }
+
+    // start the structure
+    pCutStore->nCuts = 0;
+    pCutStore->nCutsMax = IVY_CUT_LIMIT;
+    // collect the cuts of the root node
+    vCuts = Vec_VecEntry( vBitCuts, Ivy_ObjTravId(pObj) );
+    Vec_PtrForEachEntry( vCuts, pBitCut, i )
+    {
+        pCut = pCutStore->pCuts + pCutStore->nCuts++;
+        pCut->nSize = 0;
+        pCut->nSizeMax = nLeaves;
+        pCut->uHash = 0;
+        for ( k = 0; k < nNodes; k++ )
+            if ( Extra_TruthHasBit(pBitCut, k) )
+                pCut->pArray[ pCut->nSize++ ] = Ivy_ObjId( Vec_PtrEntry(vNodes, k) );
+        assert( pCut->nSize <= nLeaves );
+        if ( pCutStore->nCuts == pCutStore->nCutsMax )
+            break;
+    }
+
+    // clean the travIds
+    Vec_PtrForEachEntry( vNodes, pLeaf, i )
+        pLeaf->TravId = 0;
+    return pCutStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates elementary bit-cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_NodeCutElementary( Vec_Int_t * vStore, int nWords, int NodeId )
+{
+    unsigned * pBitCut;
+    pBitCut = Vec_IntFetch( vStore, nWords );
+    memset( pBitCut, 0, 4 * nWords );
+    Extra_TruthSetBit( pBitCut, NodeId );
+    return pBitCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compares the node by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CompareNodesByLevel( Ivy_Obj_t ** ppObj1, Ivy_Obj_t ** ppObj2 )
+{
+    Ivy_Obj_t * pObj1 = *ppObj1;
+    Ivy_Obj_t * pObj2 = *ppObj2;
+    if ( pObj1->Level < pObj2->Level )
+        return -1;
+    if ( pObj1->Level > pObj2->Level )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark all nodes up to the given depth.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolumeTrav1_rec( Ivy_Obj_t * pObj, int Depth )
+{
+    if ( Ivy_ObjIsCi(pObj) || Depth == 0 )
+        return;
+    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin0(pObj), Depth - 1 );
+    Ivy_NodeComputeVolumeTrav1_rec( Ivy_ObjFanin1(pObj), Depth - 1 );
+    pObj->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the marked nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolumeTrav2_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( !pObj->fMarkA )
+        return;
+    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_NodeComputeVolumeTrav2_rec( Ivy_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolume( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
+{
+    Ivy_Obj_t * pTemp, * pFanin;
+    int i, nNodes;
+    // mark nodes up to the given depth
+    Ivy_NodeComputeVolumeTrav1_rec( pObj, 6 );
+    // collect the marked nodes
+    Vec_PtrClear( vFront );
+    Ivy_NodeComputeVolumeTrav2_rec( pObj, vFront );
+    // find the fanins that are not marked
+    Vec_PtrClear( vNodes );
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+    {
+        pFanin = Ivy_ObjFanin0(pTemp);
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+        }
+        pFanin = Ivy_ObjFanin1(pTemp);
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+        }
+    }
+    // remember the number of nodes in the frontier
+    nNodes = Vec_PtrSize( vNodes );
+    // add the remaining nodes
+    Vec_PtrForEachEntry( vFront, pTemp, i )
+        Vec_PtrPush( vNodes, pTemp );
+    // unmark the nodes
+    Vec_PtrForEachEntry( vNodes, pTemp, i )
+    {
+        pTemp->fMarkA = 0;
+        pTemp->TravId = i;
+    }
+    // collect the frontier nodes
+    Vec_PtrClear( vFront );
+    Vec_PtrForEachEntryStop( vNodes, pTemp, i, nNodes )
+        Vec_PtrPush( vFront, pTemp );
+//    printf( "%d ", Vec_PtrSize(vNodes) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComputeVolume2( Ivy_Obj_t * pObj, int nNodeLimit, Vec_Ptr_t * vNodes, Vec_Ptr_t * vFront )
+{
+    Ivy_Obj_t * pLeaf, * pPivot, * pFanin;
+    int LevelMax, i;
+    assert( Ivy_ObjIsNode(pObj) );
+    // clear arrays
+    Vec_PtrClear( vNodes );
+    Vec_PtrClear( vFront );
+    // add the root
+    pObj->fMarkA = 1;
+    Vec_PtrPush( vNodes, pObj );
+    Vec_PtrPush( vFront, pObj );
+    // expand node with maximum level
+    LevelMax = pObj->Level;
+    do {
+        // get the node to expand
+        pPivot = NULL;
+        Vec_PtrForEachEntryReverse( vFront, pLeaf, i )
+        {
+            if ( (int)pLeaf->Level == LevelMax )
+            {
+                pPivot = pLeaf;
+                break;
+            }
+        }
+        // decrease level if we did not find the node
+        if ( pPivot == NULL )
+        {
+            if ( --LevelMax == 0 )
+                break;
+            continue;
+        }
+        // the node to expand is found
+        // remove it from frontier
+        Vec_PtrRemove( vFront, pPivot );
+        // add fanins
+        pFanin = Ivy_ObjFanin0(pPivot); 
+        if ( !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+            Vec_PtrPush( vFront, pFanin );
+        }
+        pFanin = Ivy_ObjFanin1(pPivot); 
+        if ( pFanin && !pFanin->fMarkA )
+        {
+            pFanin->fMarkA = 1;
+            Vec_PtrPush( vNodes, pFanin );
+            Vec_PtrPush( vFront, pFanin );
+        }
+        // quit if we collected enough nodes
+    } while ( Vec_PtrSize(vNodes) < nNodeLimit );
+
+    // sort nodes by level
+    Vec_PtrSort( vNodes, Ivy_CompareNodesByLevel );
+    // make sure the nodes are ordered in the increasing number of levels
+    pFanin = Vec_PtrEntry( vNodes, 0 );
+    pPivot = Vec_PtrEntryLast( vNodes );
+    assert( pFanin->Level <= pPivot->Level );
+
+    // clean the marks and remember node numbers in the TravId
+    Vec_PtrForEachEntry( vNodes, pFanin, i )
+    {
+        pFanin->fMarkA = 0;
+        pFanin->TravId = i;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Extra_TruthOrWords( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nWords )
+{
+    int w;
+    for ( w = nWords-1; w >= 0; w-- )
+        pOut[w] = pIn0[w] | pIn1[w];
+}
+static inline int Extra_TruthIsImplyWords( unsigned * pIn1, unsigned * pIn2, int nWords )
+{
+    int w;
+    for ( w = nWords-1; w >= 0; w-- )
+        if ( pIn1[w] & ~pIn2[w] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two sets of bit-cuts at a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeFindCutsMerge( Vec_Ptr_t * vCuts0, Vec_Ptr_t * vCuts1, Vec_Ptr_t * vCuts, 
+                           int nLeaves, int nWords, Vec_Int_t * vStore )
+{
+    unsigned * pBitCut, * pBitCut0, * pBitCut1, * pBitCutTest;
+    int i, k, c, w, Counter;
+    // iterate through the cut pairs
+    Vec_PtrForEachEntry( vCuts0, pBitCut0, i )
+    Vec_PtrForEachEntry( vCuts1, pBitCut1, k )
+    {
+        // skip infeasible cuts
+        Counter = 0;
+        for ( w = 0; w < nWords; w++ )
+        {
+            Counter += Extra_WordCountOnes( pBitCut0[w] | pBitCut1[w] );
+            if ( Counter > nLeaves )
+                break;
+        }
+        if ( Counter > nLeaves )
+            continue;
+        // the new cut is feasible - create it
+        pBitCutTest = Vec_IntFetch( vStore, nWords );
+        Extra_TruthOrWords( pBitCutTest, pBitCut0, pBitCut1, nWords );
+        // filter contained cuts; try to find containing cut
+        w = 0;
+        Vec_PtrForEachEntry( vCuts, pBitCut, c )
+        {
+            if ( Extra_TruthIsImplyWords( pBitCut, pBitCutTest, nWords ) )
+                break;
+            if ( Extra_TruthIsImplyWords( pBitCutTest, pBitCut, nWords ) )
+                continue;
+            Vec_PtrWriteEntry( vCuts, w++, pBitCut );
+        }
+        if ( c != Vec_PtrSize(vCuts) )
+            continue;
+        Vec_PtrShrink( vCuts, w );
+        // add the cut
+        Vec_PtrPush( vCuts, pBitCutTest );
+    }
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Compute the set of all cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManTestCutsTravAll( Ivy_Man_t * p )
+{
+    Ivy_Store_t * pStore;
+    Ivy_Obj_t * pObj;
+    Vec_Ptr_t * vNodes, * vFront;
+    Vec_Int_t * vStore;
+    Vec_Vec_t * vBitCuts;
+    int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
+    int clk = clock();
+
+    vNodes = Vec_PtrAlloc( 100 );
+    vFront = Vec_PtrAlloc( 100 );
+    vStore = Vec_IntAlloc( 100 );
+    vBitCuts = Vec_VecAlloc( 100 );
+
+    nNodeTotal = nNodeOver = 0;
+    nCutsTotal = -Ivy_ManNodeNum(p);
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( !Ivy_ObjIsNode(pObj) )
+            continue;
+        pStore = Ivy_NodeFindCutsTravAll( p, pObj, 4, 60, vNodes, vFront, vStore, vBitCuts );
+        nCutsCut    = pStore->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 );
+
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vFront );
+    Vec_IntFree( vStore );
+    Vec_VecFree( vBitCuts );
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 7246ec25..314bed8d 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -119,7 +119,7 @@ Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
-    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
+//    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
     *pvLatches = vLatches;
     return vNodes;
 }
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
new file mode 100644
index 00000000..7ce71a60
--- /dev/null
+++ b/src/temp/ivy/ivyHaig.c
@@ -0,0 +1,348 @@
+/**CFile****************************************************************
+
+  FileName    [ivyHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [HAIG management procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyHaig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    HAIGing rules in working AIG:
+    - The node points to the representative of its class
+    - The pointer can be complemented if they have different polarity
+
+    Choice node rules in HAIG:
+    - Equivalent nodes are linked into a ring
+    - Exactly one node in the ring has fanouts (this node is called representative)
+    - Pointer going from a node to the next node in the ring is complemented 
+      if the first node is complemented, compared to the representative node
+    - The representative node always has non-complemented pointer to the next node
+    - New nodes are inserted into the ring before the representative node
+*/
+
+// returns the representative node of the given HAIG node
+static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pTemp;
+    assert( !Ivy_IsComplement(pObj) );
+    // if the node has no equivalent or has fanout, it is representative
+    if ( pObj->pEquiv == NULL || Ivy_ObjRefs(pObj) > 0 )
+        return pObj;
+    // the node belongs to a class and is not a representative
+    // complemented edge (pObj->pEquiv) tells if it is complemented w.r.t. the repr
+    for ( pTemp = Ivy_Regular(pObj->pEquiv); pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+        if ( Ivy_ObjRefs(pTemp) > 0 )
+            break;
+    // return the representative node
+    assert( pTemp != pObj );
+    return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
+}
+
+// counts the number of nodes in the equivalence class
+static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pTemp;
+    int Counter;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjRefs(pObj) > 0 );
+    if ( pObj->pEquiv == NULL )
+        return 1;
+    Counter = 1;
+    assert( !Ivy_IsComplement(pObj->pEquiv) );
+    for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+        Counter++;
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts HAIG for the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigStart( Ivy_Man_t * p )
+{
+    assert( p->pHaig == NULL );
+    p->pHaig = Ivy_ManDup( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers the HAIG to the newly created manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    assert( p->pHaig != NULL );
+    Ivy_ManConst1(pNew)->pEquiv = Ivy_ManConst1(p)->pEquiv;
+    Ivy_ManForEachPi( pNew, pObj, i )
+        pObj->pEquiv = Ivy_ManPi( p, i )->pEquiv;
+    pNew->pHaig = p->pHaig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops HAIG for the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigStop( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    assert( p->pHaig != NULL );
+    Ivy_ManStop( p->pHaig );
+    p->pHaig = NULL;
+    // remove dangling pointers to the HAIG objects
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->pEquiv = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new node in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
+{
+    assert( p->pHaig != NULL );
+    assert( !Ivy_IsComplement(pObj) );
+    if ( Ivy_ObjType(pObj) == IVY_BUF )
+        pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
+    else if ( Ivy_ObjType(pObj) == IVY_LATCH )
+        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+    else if ( Ivy_ObjType(pObj) == IVY_AND )
+        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    else assert( 0 );
+    // make sure the node points to the representative
+    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the pair of equivalent nodes in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew )
+{
+    Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
+    Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
+    int fCompl;
+    assert( p->pHaig != NULL );
+    // get pointers to the classes
+    pObjOldHaig = pObjOld->pEquiv;
+    pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
+    // get regular pointers
+    pObjOldHaigR = Ivy_Regular(pObjOldHaig);
+    pObjNewHaigR = Ivy_Regular(pObjNewHaig);
+    // check if there is phase difference between them
+    fCompl = (Ivy_IsComplement(pObjOldHaig) != Ivy_IsComplement(pObjNewHaig));
+    // if the class is the same, nothing to do
+    if ( pObjOldHaigR == pObjNewHaigR )
+        return;
+    // combine classes
+    // assume the second node does not belong to a class
+    assert( pObjNewHaigR->pEquiv == NULL );
+    // add this node to the class of pObjOldHaig
+    if ( pObjOldHaigR->pEquiv == NULL )
+        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
+    else
+        pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
+    pObjOldHaigR->pEquiv = pObjNewHaigR;
+    // update the class of the new node
+    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of choices and choice nodes in HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
+{
+    Ivy_Obj_t * pObj;
+    int nChoices, nChoiceNodes, Counter, i;
+    assert( p->pHaig != NULL );
+    nChoices = nChoiceNodes = 0;
+    Ivy_ManForEachObj( p->pHaig, pObj, i )
+    {
+        if ( Ivy_ObjIsTerm(pObj) || i == 0 )
+            continue;
+        if ( Ivy_ObjRefs(pObj) == 0 )
+        {
+            assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
+            continue;
+        }
+        Counter = Ivy_HaigObjCountClass( pObj );
+        nChoiceNodes += (int)(Counter > 1);
+        nChoices += Counter - 1;
+    }
+    *pnChoices = nChoices;
+    return nChoiceNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints statistics of the HAIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
+{
+    int nChoices, nChoiceNodes;
+    assert( p->pHaig != NULL );
+    printf( "Original : " );
+    Ivy_ManPrintStats( p );
+    printf( "HAIG     : " );
+    Ivy_ManPrintStats( p->pHaig );
+
+    // print choice node stats
+    nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
+    printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices ); 
+    Ivy_ManHaigSimulate( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Applies the simulation rules.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1 )
+{
+    assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
+    if ( In0 == IVY_INIT_DC || In1 == IVY_INIT_DC )
+        return IVY_INIT_DC;
+    if ( In0 == IVY_INIT_1 && In1 == IVY_INIT_1 )
+        return IVY_INIT_1;
+    return IVY_INIT_0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulate HAIG using modified 3-valued simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManHaigSimulate( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Obj_t * pObj;
+    Ivy_Init_t In0, In1;
+    int i, k, Counter;
+    assert( p->pHaig != NULL );
+    p = p->pHaig;
+    // collect latches and nodes in the DFS order
+    vNodes = Ivy_ManDfsSeq( p, &vLatches );
+    // set the PI values
+    Ivy_ManConst1(p)->Init = IVY_INIT_0;
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->Init = IVY_INIT_0;
+    // set the latch values
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        pObj->Init = IVY_INIT_DC;
+    // perform several rounds of simulation
+    for ( k = 0; k < 5; k++ )
+    {
+        // count the number of non-determinate values
+        Counter = 0;
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            Counter += ( pObj->Init == IVY_INIT_DC );
+        printf( "Iter %d : Non-determinate = %d\n", k, Counter );               
+        // simulate the internal nodes
+        Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        {
+            In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
+            In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
+            pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
+        }
+        // simulate the latches
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            pObj->Level = Ivy_ObjFanin0(pObj)->Init;
+        Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+            pObj->Init = pObj->Level, pObj->Level = 0;
+    }
+    // free arrays
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLatches );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 9839567f..e3b8a5b8 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -70,6 +70,62 @@ Ivy_Man_t * Ivy_ManStart()
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Man_t * pNew;
+    Ivy_Obj_t * pObj;
+    int i;
+    // collect latches and nodes in the DFS order
+    vNodes = Ivy_ManDfsSeq( p, &vLatches );
+    // create the new manager
+    pNew = Ivy_ManStart();
+    // create the PIs
+    Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+    // create the fake PIs for latches
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+    // duplicate internal nodes
+    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+    // add the POs
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) );
+    // transform additional PI nodes into latches and connect them
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+    {
+        assert( !Ivy_ObjFaninC0(pObj) );
+        pObj->pEquiv->Type = IVY_LATCH;
+        pObj->pEquiv->Init = pObj->Init;
+        Ivy_ObjConnect( pNew, pObj->pEquiv, Ivy_ObjChild0Equiv(pObj), NULL );
+    }
+    // shrink the arrays
+    Vec_PtrShrink( pNew->vPis, Ivy_ManPiNum(p) );
+    // update the counters of different objects
+    pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p);
+    pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p);
+    // free arrays
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLatches );
+    // check the resulting network
+    if ( !Ivy_ManCheck(pNew) )
+        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -81,6 +137,8 @@ Ivy_Man_t * Ivy_ManStart()
 ***********************************************************************/
 void Ivy_ManStop( Ivy_Man_t * p )
 {
+    if ( p->time1 ) { PRT( "Update lev  ", p->time1 ); }
+    if ( p->time2 ) { PRT( "Update levR ", p->time2 ); }
 //    Ivy_TableProfile( p );
 //    if ( p->vFanouts )  Ivy_ManStopFanout( p );
     if ( p->vChunks )   Ivy_ManStopMemory( p );
diff --git a/src/temp/ivy/ivyMem.c b/src/temp/ivy/ivyMem.c
index 6ca33541..09c73c49 100644
--- a/src/temp/ivy/ivyMem.c
+++ b/src/temp/ivy/ivyMem.c
@@ -89,7 +89,7 @@ void Ivy_ManAddMemory( Ivy_Man_t * p )
     int i, nBytes;
     assert( sizeof(Ivy_Obj_t) <= 64 );
     assert( p->pListFree == NULL );
-    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
+//    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
     // allocate new memory page
     nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
     pMemory = ALLOC( char, nBytes );
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index f098332d..a7970156 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -294,45 +294,6 @@ int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals,
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Constructs the well-balanced tree of gates.]
-
-  Description [Disregards levels and possible logic sharing.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
-{
-    Ivy_Obj_t * pObj1, * pObj2;
-    if ( nObjs == 1 )
-        return ppObjs[0];
-    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
-    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
-    return Ivy_Oper( p, pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
-    assert( Type == IVY_AND || Type == IVY_EXOR );
-    assert( nArgs > 0 );
-    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 3122c8c8..e8924b5b 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -79,7 +79,6 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     assert( Ivy_TableLookup(p, pGhost) == NULL );
     // get memory for the new object
     pObj = Ivy_ManFetchMemory( p );
-//printf( "Reusing %p.\n", pObj );
     assert( Ivy_ObjIsNone(pObj) );
     pObj->Id = Vec_PtrSize(p->vObjs);
     Vec_PtrPush( p->vObjs, pObj );
@@ -115,6 +114,9 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Ivy_ObjType(pObj)]++;
     p->nCreated++;
+    // if HAIG is defined, create a corresponding node
+    if ( p->pHaig )
+        Ivy_ManHaigCreateObj( p, pObj );
     return pObj;
 }
 
@@ -258,7 +260,6 @@ void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
         // free the node
         Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
         Ivy_ManRecycleMemory( p, pObj );
-//printf( "Recycling after delete %p.\n", pObj );
     }
     else
     {
@@ -312,7 +313,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop )
 ***********************************************************************/
 void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel )
 {
-    int nRefsOld;
+    int nRefsOld;//, clk;
     // the object to be replaced cannot be complemented
     assert( !Ivy_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
@@ -321,12 +322,16 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) );
     // the object cannot be the same
     assert( pObjOld != Ivy_Regular(pObjNew) );
+    // if HAIG is defined, create the choice node
+    if ( p->pHaig )
+        Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew );
     // if the new object is complemented or already used, add the buffer
     if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
         pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) );
     assert( !Ivy_IsComplement(pObjNew) );
     if ( fUpdateLevel )
     {
+//clk = clock();
         // if the new node's arrival time is different, recursively update arrival time of the fanouts
         if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level )
         {
@@ -334,7 +339,9 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
             pObjOld->Level = pObjNew->Level;
             Ivy_ObjUpdateLevel_rec( p, pObjOld );
         }
+//p->time1 += clock() - clk;
         // if the new node's required time has changed, recursively update required time of the fanins
+//clk = clock();
         if ( p->vRequired )
         {
             int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id);
@@ -344,6 +351,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
                 Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew );
             }
         }
+//p->time2 += clock() - clk;
     }
     // delete the old object
     if ( fDeleteOld )
@@ -375,7 +383,6 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in
     // recycle the object that was taken over by pObjOld
     Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL );
     Ivy_ManRecycleMemory( p, pObjNew );
-//printf( "Recycling after patch %p.\n", pObjNew );
     // if the new node is the buffer propagate it
     if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) )
         Vec_PtrPush( p->vBufs, pObjOld );
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
index af216e45..8115ce4f 100644
--- a/src/temp/ivy/ivyOper.c
+++ b/src/temp/ivy/ivyOper.c
@@ -210,6 +210,45 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t *
 
 /**Function*************************************************************
 
+  Synopsis    [Constructs the well-balanced tree of gates.]
+
+  Description [Disregards levels and possible logic sharing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
+    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+    return Ivy_Oper( p, pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Implements the miter.]
 
   Description []
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
index 7cf55b69..11660e42 100644
--- a/src/temp/ivy/ivySeq.c
+++ b/src/temp/ivy/ivySeq.c
@@ -80,10 +80,6 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
         // stop if all nodes have been tried once
         if ( i > nNodes )
             break;
-        if ( i == 8648 )
-        {
-            int x = 0;
-        }
         // for each cut, try to resynthesize it
         nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
         if ( nGain > 0 || nGain == 0 && fUseZeroCost )
diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c
index 91994ca6..ca84ded1 100644
--- a/src/temp/player/playerToAbc.c
+++ b/src/temp/player/playerToAbc.c
@@ -446,7 +446,7 @@ static inline int Abc_NodePlayerCost( int nFanins )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Abc_NtkPlayerCostOne( int nCost, int RankCost )
+static inline int Abc_NtkPlayerCostOneLevel( int nCost, int RankCost )
 {
     return (nCost / RankCost) + ((nCost % RankCost) > 0);
 }
@@ -466,7 +466,8 @@ int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
 {
     Abc_Obj_t * pObj;
     int * pLevelCosts, * pLevelCostsR;
-    int nFanins, nLevels, LevelR, Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR, i; 
+    int Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR;
+    int nFanins, nLevels, LevelR, i; 
     // compute the reverse levels
     Abc_NtkStartReverseLevels( pNtk );
     // compute the costs for each level
@@ -491,17 +492,19 @@ int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose )
     {
         CostTotal    += pLevelCosts[i];
         CostTotalR   += pLevelCostsR[i];
-        nRanksTotal  += Abc_NtkPlayerCostOne( pLevelCosts[i], RankCost );
-        nRanksTotalR += Abc_NtkPlayerCostOne( pLevelCostsR[i], RankCost );
+        nRanksTotal  += Abc_NtkPlayerCostOneLevel( pLevelCosts[i], RankCost );
+        nRanksTotalR += Abc_NtkPlayerCostOneLevel( pLevelCostsR[i], RankCost );
     }
     assert( CostTotal == CostTotalR );
     // print out statistics
     if ( fVerbose )
     {
         for ( i = 1; i <= nLevels; i++ )
+        {
             printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i, 
             pLevelCosts[i], ((double)pLevelCosts[i])/RankCost, 
             pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost );
+        }
         printf( "TOTAL    : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n", 
             CostTotal, nRanksTotal, nRanksTotalR, nLevels );
     }