Version abc60611

author: Alan Mishchenko <alanmi@berkeley.edu> 2006-06-11 08:01:00 -0700
committer: Alan Mishchenko <alanmi@berkeley.edu> 2006-06-11 08:01:00 -0700
commit: 3db1557f45b03875a0a0b8adddcc15c4565895d2 (patch)
tree: 2896d20ddcb85ae4aa7245ca28bc585f567fea54 /src/temp/ivy
parent: 7d0921330b1f4e789901b4c2450920e7c412f95f (diff)
download: abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.gz
abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.bz2
abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.zip
18 files changed, 4827 insertions, 0 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
new file mode 100644
index 00000000..55ada384
--- /dev/null
+++ b/src/temp/ivy/ivy.h
@@ -0,0 +1,450 @@
+/**CFile****************************************************************
+
+  FileName    [ivy.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __IVY_H__
+#define __IVY_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Man_t_            Ivy_Man_t;
+typedef struct Ivy_Obj_t_            Ivy_Obj_t;
+
+// object types
+typedef enum { 
+    IVY_NONE,                        // 0: unused node
+    IVY_PI,                          // 1: primary input (and constant 1 node)
+    IVY_PO,                          // 2: primary output
+    IVY_ASSERT,                      // 3: assertion
+    IVY_LATCH,                       // 4: sequential element
+    IVY_AND,                         // 5: internal AND node
+    IVY_EXOR,                        // 6: internal EXOR node
+    IVY_BUF,                         // 7: internal buffer (temporary)
+    IVY_ANDM,                        // 8: multi-input AND (logic network only)
+    IVY_EXORM,                       // 9: multi-input EXOR (logic network only)
+    IVY_LUT                          // 10: multi-input LUT (logic network only)
+} Ivy_Type_t;
+
+// latch initial values
+typedef enum { 
+    IVY_INIT_NONE,                   // 0: not a latch
+    IVY_INIT_0,                      // 1: zero
+    IVY_INIT_1,                      // 2: one
+    IVY_INIT_DC                      // 3: don't-care
+} Ivy_Init_t;
+
+// the AIG node
+struct Ivy_Obj_t_  // 6 words
+{
+    int              Id;             // integer ID
+    int              TravId;         // traversal ID
+    int              Fanin0;         // fanin ID
+    int              Fanin1;         // fanin ID
+    int              nRefs;          // reference counter
+    unsigned         Type    :  4;   // object type
+    unsigned         fPhase  :  1;   // value under 000...0 pattern
+    unsigned         fMarkA  :  1;   // multipurpose mask
+    unsigned         fMarkB  :  1;   // multipurpose mask
+    unsigned         fExFan  :  1;   // set to 1 if last fanout added is EXOR
+    unsigned         fComp0  :  1;   // complemented attribute
+    unsigned         fComp1  :  1;   // complemented attribute
+    unsigned         Init    :  2;   // latch initial value
+    unsigned         LevelR  :  8;   // reverse logic level
+    unsigned         Level   : 12;   // logic level
+};
+
+// the AIG manager
+struct Ivy_Man_t_
+{
+    // AIG nodes
+    int              nObjs[12];      // the number of objects by type
+    int              nCreated;       // the number of created objects
+    int              nDeleted;       // the number of deleted objects
+    int              ObjIdNext;      // the next free obj ID to assign
+    int              nObjsAlloc;     // the allocated number of nodes
+    Ivy_Obj_t *      pObjs;          // the array of all nodes
+    Vec_Int_t *      vPis;           // the array of PIs
+    Vec_Int_t *      vPos;           // the array of POs
+    // stuctural hash table
+    int *            pTable;         // structural hash table
+    int              nTableSize;     // structural hash table size
+    // various data members
+    int              fExtended;      // set to 1 in extended mode
+    int              nTravIds;       // the traversal ID
+    int              nLevelMax;      // the maximum level
+    void *           pData;          // the temporary data
+    // truth table of the 8-LUTs
+    unsigned *       pMemory;        // memory for truth tables
+    Vec_Int_t *      vTruths;        // offset for truth table of each node
+    // storage for the undo operation
+    Vec_Int_t *      vFree;          // storage for all deleted entries
+    Ivy_Obj_t *      pUndos;         // description of recently deleted nodes
+    int              nUndos;         // the number of recently deleted nodes
+    int              nUndosAlloc;    // the number of allocated cells
+    int              fRecording;     // shows that recording goes on
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#define IVY_SANDBOX_SIZE   1
+
+#define IVY_MIN(a,b)       (((a) < (b))? (a) : (b))
+#define IVY_MAX(a,b)       (((a) > (b))? (a) : (b))
+
+static inline int          Ivy_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);       }
+static inline int          Ivy_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int          Ivy_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;   }
+static inline void         Ivy_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));               }
+static inline void         Ivy_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));               }
+
+static inline 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));  }
+static inline int          Ivy_IsComplement( Ivy_Obj_t * p )      { return (int )(((unsigned)p) & 01);          }
+
+static inline Ivy_Obj_t *  Ivy_ManConst0( Ivy_Man_t * p )         { return Ivy_Not(p->pObjs);                   }
+static inline Ivy_Obj_t *  Ivy_ManConst1( Ivy_Man_t * p )         { return p->pObjs;                            }
+static inline Ivy_Obj_t *  Ivy_ManGhost( Ivy_Man_t * p )          { return p->pObjs - IVY_SANDBOX_SIZE;         }
+static inline Ivy_Obj_t *  Ivy_ManPi( Ivy_Man_t * p, int i )      { return p->pObjs + Vec_IntEntry(p->vPis,i);  }
+static inline Ivy_Obj_t *  Ivy_ManPo( Ivy_Man_t * p, int i )      { return p->pObjs + Vec_IntEntry(p->vPos,i);  }
+static inline Ivy_Obj_t *  Ivy_ManObj( Ivy_Man_t * p, int i )     { return p->pObjs + i;                        }
+
+static inline 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];                }
+static inline int          Ivy_ManLatchNum( Ivy_Man_t * p )       { return p->nObjs[IVY_LATCH];                 }
+static inline int          Ivy_ManAndNum( Ivy_Man_t * p )         { return p->nObjs[IVY_AND];                   }
+static inline int          Ivy_ManExorNum( Ivy_Man_t * p )        { return p->nObjs[IVY_EXOR];                  }
+static inline int          Ivy_ManBufNum( Ivy_Man_t * p )         { return p->nObjs[IVY_BUF];                   }
+static inline int          Ivy_ManAndMultiNum( Ivy_Man_t * p )    { return p->nObjs[IVY_ANDM];                  }
+static inline int          Ivy_ManExorMultiNum( Ivy_Man_t * p )   { return p->nObjs[IVY_EXORM];                 }
+static inline int          Ivy_ManLutNum( Ivy_Man_t * p )         { return p->nObjs[IVY_LUT];                   }
+static inline int          Ivy_ManObjNum( Ivy_Man_t * p )         { return p->nCreated - p->nDeleted;           }
+static inline int          Ivy_ManObjIdNext( Ivy_Man_t * p )      { return p->ObjIdNext;                        }
+static inline int          Ivy_ManObjAllocNum( Ivy_Man_t * p )    { return p->nObjsAlloc;                       }
+static inline int          Ivy_ManNodeNum( Ivy_Man_t * p )        { return p->fExtended? p->nObjs[IVY_ANDM]+p->nObjs[IVY_EXORM]+p->nObjs[IVY_LUT] : p->nObjs[IVY_AND]+p->nObjs[IVY_EXOR]; }
+static inline int          Ivy_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_ObjIsAndMulti( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM;   }
+static inline int          Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM;  }
+static inline int          Ivy_ObjIsLut( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_LUT;    }
+static inline int          Ivy_ObjIsNodeExt( Ivy_Obj_t * pObj )   { assert( !Ivy_IsComplement(pObj) ); return pObj->Type >= IVY_ANDM;   }
+
+static inline int          Ivy_ObjIsMarkA( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fMarkA;  }
+static inline void         Ivy_ObjSetMarkA( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 1;     }
+static inline void         Ivy_ObjClearMarkA( Ivy_Obj_t * pObj )  { assert( !Ivy_IsComplement(pObj) ); pObj->fMarkA = 0;     }
+
+static inline Ivy_Man_t *  Ivy_ObjMan( Ivy_Obj_t * pObj )         { assert( !Ivy_IsComplement(pObj) ); return *((Ivy_Man_t **)(pObj - pObj->Id - IVY_SANDBOX_SIZE - 1)); }
+static inline Ivy_Obj_t *  Ivy_ObjConst0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_Not(pObj - pObj->Id);           }
+static inline Ivy_Obj_t *  Ivy_ObjConst1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id;                    }
+static inline Ivy_Obj_t *  Ivy_ObjGhost( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id - IVY_SANDBOX_SIZE; }
+static inline Ivy_Obj_t *  Ivy_ObjObj( Ivy_Obj_t * pObj, int n )  { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + n;                }
+static inline Ivy_Obj_t *  Ivy_ObjNext( Ivy_Obj_t * pObj )        { assert( !Ivy_IsComplement(pObj) ); return pObj - pObj->Id + pObj->TravId;     }
+ 
+static inline void         Ivy_ObjSetTravId( Ivy_Obj_t * pObj, int TravId ) { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = TravId;                                              }
+static inline void         Ivy_ObjSetTravIdCurrent( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds;                          }
+static inline void         Ivy_ObjSetTravIdPrevious( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); pObj->TravId = Ivy_ObjMan(pObj)->nTravIds - 1;                      }
+static inline int          Ivy_ObjIsTravIdCurrent( Ivy_Obj_t * pObj )       { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds);     }
+static inline int          Ivy_ObjIsTravIdPrevious( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return (int )((int)pObj->TravId == Ivy_ObjMan(pObj)->nTravIds - 1); }
+
+static inline 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->Fanin0;                           }
+static inline int          Ivy_ObjFaninId1( Ivy_Obj_t * pObj )    { assert( !Ivy_IsComplement(pObj) ); return pObj->Fanin1;                           }
+static inline int          Ivy_ObjFaninC0( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp0;                           }
+static inline int          Ivy_ObjFaninC1( Ivy_Obj_t * pObj )     { assert( !Ivy_IsComplement(pObj) ); return pObj->fComp1;                           }
+static inline Ivy_Obj_t *  Ivy_ObjFanin0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin0);         }
+static inline Ivy_Obj_t *  Ivy_ObjFanin1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjObj(pObj, pObj->Fanin1);         }
+static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin0(pObj), Ivy_ObjFaninC0(pObj) );   }
+static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) );   }
+static inline int          Ivy_ObjLevelR( Ivy_Obj_t * pObj )      { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR;                           }
+static inline int          Ivy_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 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; 
+}
+static inline void         Ivy_ObjOverwrite( Ivy_Obj_t * pBase, Ivy_Obj_t * pData )   { int IdSaved = pBase->Id; memcpy( pBase, pData, sizeof(Ivy_Obj_t) ); pBase->Id = IdSaved;         }
+static inline int          Ivy_ObjWhatFanin( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )    
+{ 
+    if ( Ivy_ObjFaninId0(pObj) == Ivy_ObjId(pFanin) ) return 0; 
+    if ( Ivy_ObjFaninId1(pObj) == Ivy_ObjId(pFanin) ) return 1; 
+    assert(0); return -1; 
+}
+static inline int          Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout )    
+{ 
+    if ( Ivy_ObjFaninId0(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC0(pObj); 
+    if ( Ivy_ObjFaninId1(pFanout) == Ivy_ObjId(pObj) ) return Ivy_ObjFaninC1(pObj); 
+    assert(0); return -1; 
+}
+
+// create the ghost of the new node
+static inline Ivy_Obj_t *  Ivy_ObjCreateGhost( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init )    
+{
+    Ivy_Obj_t * pGhost;
+    int Temp;
+    pGhost = Ivy_ObjGhost(Ivy_Regular(p0));
+    pGhost->Type = Type;
+    pGhost->Init = Init;
+    pGhost->fComp0 = Ivy_IsComplement(p0);
+    pGhost->fComp1 = Ivy_IsComplement(p1);
+    pGhost->Fanin0 = Ivy_ObjId(Ivy_Regular(p0));
+    pGhost->Fanin1 = Ivy_ObjId(Ivy_Regular(p1));
+    if ( pGhost->Fanin0 < pGhost->Fanin1 )
+    {
+        Temp = pGhost->Fanin0, pGhost->Fanin0 = pGhost->Fanin1, pGhost->Fanin1 = Temp;
+        Temp = pGhost->fComp0, pGhost->fComp0 = pGhost->fComp1, pGhost->fComp1 = Temp;
+    }
+    assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 );
+    return pGhost;
+}
+
+// create the ghost of the new node
+static inline Ivy_Obj_t *  Ivy_ObjCreateGhost2( Ivy_Man_t * p, Ivy_Obj_t * pObjDead )    
+{
+    Ivy_Obj_t * pGhost;
+    pGhost = Ivy_ManGhost(p);
+    pGhost->Type   = pObjDead->Type;
+    pGhost->Init   = pObjDead->Init;
+    pGhost->fComp0 = pObjDead->fComp0;
+    pGhost->fComp1 = pObjDead->fComp1;
+    pGhost->Fanin0 = pObjDead->Fanin0;
+    pGhost->Fanin1 = pObjDead->Fanin1;
+    assert( Ivy_ObjIsOneFanin(pGhost) || pGhost->Fanin0 > pGhost->Fanin1 );
+    return pGhost;
+}
+
+// get the complemented initial state
+static Ivy_Init_t Ivy_InitNotCond( Ivy_Init_t Init, int fCompl )
+{
+    assert( Init != IVY_INIT_NONE );
+    if ( fCompl == 0 )
+        return Init;
+    if ( Init == IVY_INIT_0 )
+        return IVY_INIT_1;
+    if ( Init == IVY_INIT_1 )
+        return IVY_INIT_0;
+    return IVY_INIT_DC;
+}
+
+// get the initial state after forward retiming over AND gate
+static Ivy_Init_t Ivy_InitAnd( Ivy_Init_t InitA, Ivy_Init_t InitB )
+{
+    assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
+    if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 )
+        return IVY_INIT_0;
+    if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
+        return IVY_INIT_DC;
+    return IVY_INIT_1;
+}
+
+// get the initial state after forward retiming over EXOR gate
+static Ivy_Init_t Ivy_InitExor( Ivy_Init_t InitA, Ivy_Init_t InitB )
+{
+    assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE );
+    if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC )
+        return IVY_INIT_DC;
+    if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 )
+        return IVY_INIT_1;
+    if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 )
+        return IVY_INIT_1;
+    return IVY_INIT_0;
+}
+
+// extended fanins
+static inline Vec_Int_t *  Ivy_ObjGetFanins( Ivy_Obj_t * pObj )                      { assert(Ivy_ObjMan(pObj)->fExtended); return (Vec_Int_t *)*(((int*)pObj)+2);            }
+static inline void         Ivy_ObjSetFanins( Ivy_Obj_t * pObj, Vec_Int_t * vFanins ) { assert(Ivy_ObjMan(pObj)->fExtended); assert(Ivy_ObjGetFanins(pObj)==NULL); *(Vec_Int_t **)(((int*)pObj)+2) = vFanins; }
+static inline void         Ivy_ObjStartFanins( Ivy_Obj_t * pObj, int nFanins )       { assert(Ivy_ObjMan(pObj)->fExtended); Ivy_ObjSetFanins( pObj, Vec_IntAlloc(nFanins) );  }
+static inline void         Ivy_ObjAddFanin( Ivy_Obj_t * pObj, int Fanin )            { assert(Ivy_ObjMan(pObj)->fExtended); Vec_IntPush( Ivy_ObjGetFanins(pObj), Fanin );     }
+static inline int          Ivy_ObjReadFanin( Ivy_Obj_t * pObj, int i )               { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntEntry( Ivy_ObjGetFanins(pObj), i ); }
+static inline int          Ivy_ObjFaninNum( Ivy_Obj_t * pObj )                       { assert(Ivy_ObjMan(pObj)->fExtended); return Vec_IntSize( Ivy_ObjGetFanins(pObj) );     }
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over all objects, including those currently not used
+#define Ivy_ManForEachObj( p, pObj, i )                                                  \
+    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )
+// 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++ )
+// iterator over the primary outputs
+#define Ivy_ManForEachPo( p, pObj, i )                                                   \
+    for ( i = 0; i < Vec_IntSize(p->vPos) && ((pObj) = Ivy_ManPo(p, i)); i++ )
+// iterator over the combinational inputs
+#define Ivy_ManForEachCi( p, pObj, i )                                                   \
+    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )                        \
+        if ( !Ivy_ObjIsCi(pObj) ) {} else
+// iterator over the combinational outputs
+#define Ivy_ManForEachCo( p, pObj, i )                                                   \
+    for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )                        \
+        if ( !Ivy_ObjIsCo(pObj) ) {} else
+// iterator over logic nodes (AND and EXOR gates)
+#define Ivy_ManForEachNode( p, pObj, i )                                                 \
+    for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ )                      \
+        if ( !Ivy_ObjIsNode(pObj) ) {} else
+// iterator over logic latches
+#define Ivy_ManForEachLatch( p, pObj, i )                                                \
+    for ( i = 1, pObj = p->pObjs+i; i < p->ObjIdNext; i++, pObj++ )                      \
+        if ( !Ivy_ObjIsLatch(pObj) ) {} else
+// iterator over the nodes whose IDs are stored in the array
+#define Ivy_ManForEachNodeVec( p, vIds, pObj, i )                                        \
+    for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== ivyCanon.c ========================================================*/
+extern Ivy_Obj_t *     Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init );
+/*=== ivyCheck.c ========================================================*/
+extern int             Ivy_ManCheck( Ivy_Man_t * p );
+/*=== ivyCut.c ==========================================================*/
+extern void            Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
+/*=== ivyBalance.c ======================================================*/
+extern int             Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
+/*=== ivyDfs.c ==========================================================*/
+extern Vec_Int_t *     Ivy_ManDfs( Ivy_Man_t * p );
+extern Vec_Int_t *     Ivy_ManDfsExt( 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 );
+extern unsigned        Ivy_TruthDsdCompute( Vec_Int_t * vTree );
+extern void            Ivy_TruthDsdComputePrint( unsigned uTruth );
+extern Ivy_Obj_t *     Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree );
+/*=== ivyMan.c ==========================================================*/
+extern Ivy_Man_t *     Ivy_ManStart( int nPis, int nPos, int nNodesMax );
+extern void            Ivy_ManStop( Ivy_Man_t * p );
+extern void            Ivy_ManGrow( Ivy_Man_t * p );
+extern int             Ivy_ManCleanup( Ivy_Man_t * p );
+extern void            Ivy_ManPrintStats( Ivy_Man_t * p );
+/*=== ivyMulti.c ==========================================================*/
+extern Ivy_Obj_t *     Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+/*=== ivyObj.c ==========================================================*/
+extern Ivy_Obj_t *     Ivy_ObjCreate( Ivy_Obj_t * pGhost );
+extern Ivy_Obj_t *     Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type );
+extern void            Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin );
+extern void            Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop );
+extern void            Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop );
+extern void            Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop );
+extern void            Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode );
+/*=== ivyOper.c =========================================================*/
+extern Ivy_Obj_t *     Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type );
+extern Ivy_Obj_t *     Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
+extern Ivy_Obj_t *     Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
+extern Ivy_Obj_t *     Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
+extern Ivy_Obj_t *     Ivy_Miter( Vec_Ptr_t * vPairs );
+/*=== ivyRewrite.c =========================================================*/
+extern int             Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
+/*=== ivyTable.c ========================================================*/
+extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Obj_t * pObj );
+extern void            Ivy_TableInsert( Ivy_Obj_t * pObj );
+extern void            Ivy_TableDelete( Ivy_Obj_t * pObj );
+extern void            Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew );
+extern int             Ivy_TableCountEntries( Ivy_Man_t * p );
+extern void            Ivy_TableResize( Ivy_Man_t * p );
+/*=== ivyUndo.c =========================================================*/
+extern void            Ivy_ManUndoStart( Ivy_Man_t * p );
+extern void            Ivy_ManUndoStop( Ivy_Man_t * p );
+extern void            Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj );
+extern void            Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot );
+/*=== ivyUtil.c =========================================================*/
+extern void            Ivy_ManIncrementTravId( Ivy_Man_t * p );
+extern void            Ivy_ManCleanTravId( Ivy_Man_t * p );
+extern int             Ivy_ObjIsMuxType( Ivy_Obj_t * pObj );
+extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObjT, Ivy_Obj_t ** ppObjE );
+extern unsigned *      Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
+extern Ivy_Obj_t *     Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin );
+extern Vec_Int_t *     Ivy_ManLatches( Ivy_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
new file mode 100644
index 00000000..bbe69dd9
--- /dev/null
+++ b/src/temp/ivy/ivyBalance.c
@@ -0,0 +1,421 @@
+/**CFile****************************************************************
+
+  FileName    [ivyBalance.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Algebraic AIG balancing.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  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);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs algebraic balancing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int 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 )
+    {
+        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 );
+    }
+    Vec_IntFree( vNodes );
+    Vec_PtrFree( vSpots );
+    Vec_PtrFree( vFront );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode )
+{
+    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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes nodes inside supergate and determines frontier.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront )
+{
+    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) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Comparison procedure for two nodes by level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+    int Level1 = Ivy_ObjLevel( *pp1 );
+    int Level2 = Ivy_ObjLevel( *pp2 );
+    if ( Level1 > Level2 )
+        return -1;
+    if ( Level1 < Level2 )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes nodes inside supergate and determines frontier.]
+
+  Description [Return 1 if the output needs to be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots )
+{
+    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 )
+    {
+        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 )
+        return 0;
+    // if there are complemented pairs and this is AND, create const 0
+    if ( Counter > 0 && Ivy_ObjIsAnd(pNode) )
+    {
+        Vec_PtrClear( vFront );
+        Vec_PtrPush( vFront, Ivy_ManConst0(pMan) );
+        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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the left bound on the next candidate to be paired.]
+
+  Description [The nodes in the array are in the decreasing order of levels. 
+  The last node in the array has the smallest level. By default it would be paired 
+  with the next node on the left. However, it may be possible to pair it with some
+  other node on the left, in such a way that the new node is shared. This procedure
+  finds the index of the left-most node, which can be paired with the last node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
+{
+    Ivy_Obj_t * pNodeRight, * pNodeLeft;
+    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 );
+    // 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 );
+        // if the level of this node is different, quit the loop
+        if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->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 );
+    return Current;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Moves closer to the end the node that is best for sharing.]
+
+  Description [If there is no node with sharing, randomly chooses one of 
+  the legal nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+{
+    Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost;
+    int RightBound, i;
+    // get the right bound
+    RightBound = Vec_PtrSize(vSuper) - 2;
+    assert( LeftBound <= RightBound );
+    if ( LeftBound == RightBound )
+        return;
+    // get the two last nodes
+    pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 );
+    pNode2 = 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 );
+        if ( Ivy_TableLookup( pGhost ) )
+        {
+            if ( pNode3 == pNode2 )
+                return;
+            Vec_PtrWriteEntry( vSuper, i,          pNode2 );
+            Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
+            return;
+        }
+    }
+/*
+    // 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 )
+            return;
+        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 );
+        Vec_PtrWriteEntry( vSuper, RightBound,         pNode3 );
+    }
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts a new node in the order by levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pNode1, * pNode2;
+    int i;
+    if ( Vec_PtrPushUnique(vFront, pNode) )
+        return;
+    // find the p of the node
+    for ( i = vFront->nSize-1; i > 0; i-- )
+    {
+        pNode1 = vFront->pArray[i  ];
+        pNode2 = vFront->pArray[i-1];
+        if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->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 );
+    }
+    assert( Vec_PtrSize(vFront) == 1 );
+    // perform the replacement
+    Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 ); 
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyCanon.c b/src/temp/ivy/ivyCanon.c
new file mode 100644
index 00000000..c6f43d15
--- /dev/null
+++ b/src/temp/ivy/ivyCanon.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+  FileName    [ivyCanon.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Finding canonical form of objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyCanon.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
+{
+    Ivy_Obj_t * pResult, * pLat0, * pLat1;
+    Ivy_Init_t Init, Init0, Init1;
+    int fCompl0, fCompl1;
+    Ivy_Type_t Type;
+    assert( Ivy_ObjIsNode(pGhost) );
+    assert( Ivy_ObjIsAnd(pGhost) || (!Ivy_ObjFaninC0(pGhost) && !Ivy_ObjFaninC1(pGhost)) );
+    assert( Ivy_ObjFaninId0(pGhost) != 0 && Ivy_ObjFaninId1(pGhost) != 0 );
+    // consider the case when the pair is canonical
+    if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) )
+    {
+        if ( pResult = Ivy_TableLookup( pGhost ) )
+            return pResult;
+        return Ivy_ObjCreate( pGhost );
+    }
+    /// remember the latches
+    pLat0 = Ivy_ObjFanin0(pGhost);
+    pLat1 = Ivy_ObjFanin1(pGhost);
+    // remember type and compls
+    Type = Ivy_ObjType(pGhost);
+    fCompl0 = Ivy_ObjFaninC0(pGhost);
+    fCompl1 = Ivy_ObjFaninC1(pGhost);
+    // modify the fanins to be latch fanins
+    pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0);
+    pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1);
+    // call recursively
+    pResult = Ivy_CanonPair_rec( pGhost );
+    // build latch on top of this
+    Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 );
+    Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 );
+    Init  = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1);
+    return Ivy_CanonLatch( pResult, Init );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+    Ivy_Obj_t * pGhost, * pResult;
+    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( pGhost );
+    return pResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+    Ivy_Obj_t * pGhost, * pResult;
+    int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1);
+    pObj0 = Ivy_Regular(pObj0);
+    pObj1 = Ivy_Regular(pObj1);
+    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( pGhost );
+    return Ivy_NotCond( pResult, fCompl );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the canonical form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
+{
+    Ivy_Obj_t * pGhost, * pResult;
+    int fCompl = Ivy_IsComplement(pObj);
+    pObj = Ivy_Regular(pObj);
+    pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
+    pResult = Ivy_TableLookup( pGhost );
+    if ( pResult == NULL )
+        pResult = Ivy_ObjCreate( pGhost );
+    return Ivy_NotCond( pResult, fCompl );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c
new file mode 100644
index 00000000..c39eac12
--- /dev/null
+++ b/src/temp/ivy/ivyCheck.c
@@ -0,0 +1,121 @@
+/**CFile****************************************************************
+
+  FileName    [ivyCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [AIG checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the consistency of the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManCheck( Ivy_Man_t * pMan )
+{
+    Ivy_Obj_t * pObj, * pObj2;
+    int i;
+    Ivy_ManForEachObj( pMan, pObj, i )
+    {
+        // skip deleted nodes
+        if ( Ivy_ObjIsNone(pObj) )
+            continue;
+        // consider the constant node and PIs
+        if ( i == 0 || Ivy_ObjIsPi(pObj) )
+        {
+            if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) )
+            {
+                printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        if ( Ivy_ObjIsPo(pObj) )
+        {
+            if ( Ivy_ObjFaninId1(pObj) )
+            {
+                printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id );
+                return 0;
+            }
+            continue;
+        }
+        if ( Ivy_ObjIsBuf(pObj) )
+        {
+            continue;
+        }
+        if ( Ivy_ObjIsLatch(pObj) )
+        {
+            if ( Ivy_ObjFaninId1(pObj) != 0 )
+            {
+                printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
+                return 0;
+            }
+            if ( Ivy_ObjInit(pObj) == 0 )
+            {
+                printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
+                return 0;
+            }
+            pObj2 = Ivy_TableLookup( pObj );
+            if ( pObj2 != pObj )
+                printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
+                continue;
+        }
+        // consider the AND node
+        if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) )
+        {
+            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id );
+            return 0;
+        }
+        if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) )
+        {
+            printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
+            return 0;
+        }
+//        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
+//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
+        pObj2 = Ivy_TableLookup( pObj );
+        if ( pObj2 != pObj )
+            printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
+    }
+    // count the number of nodes in the table
+    if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) )
+    {
+        printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
new file mode 100644
index 00000000..a8fd148b
--- /dev/null
+++ b/src/temp/ivy/ivyCut.c
@@ -0,0 +1,205 @@
+/**CFile****************************************************************
+
+  FileName    [ivyCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Computes reconvergence driven sequential cut.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyCut.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
+
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Ivy_NodeGetLeafCostOne( Ivy_Man_t * p, int Leaf, Vec_Int_t * vInside )
+{
+    Ivy_Obj_t * pNode;
+    int nLatches, FaninLeaf, Cost;
+    // make sure leaf is not a contant node
+    assert( Leaf > 0 ); 
+    // get the node
+    pNode = Ivy_ManObj( p, Ivy_LeafId(Leaf) );
+    // cannot expand over the PI node
+    if ( Ivy_ObjIsPi(pNode) || Ivy_ObjIsConst1(pNode) )
+        return 999;
+    // get the number of latches
+    nLatches = Ivy_LeafLat(Leaf) + Ivy_ObjIsLatch(pNode);
+    if ( nLatches > 15 )
+        return 999;
+    // get the first fanin
+    FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches );
+    Cost = FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1);
+    // quit if this is the one fanin node
+    if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
+        return Cost;
+    assert( Ivy_ObjIsNode(pNode) );
+    // get the second fanin
+    FaninLeaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches );
+    Cost += FaninLeaf && (Vec_IntFind(vInside, FaninLeaf) == -1);
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks only at their immediate 
+  predecessors (this is why it is called a one-level construction procedure).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManSeqFindCut_int( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSizeLimit )
+{
+    Ivy_Obj_t * pNode;
+    int CostBest, CostCur, Leaf, LeafBest, Next, nLatches, i;
+    int LeavesBest[10];
+    int Counter;
+
+    // add random selection of the best fanin!!!
+
+    // find the best fanin
+    CostBest = 99;
+    LeafBest = -1;
+    Counter = -1;
+//printf( "Evaluating fanins of the cut:\n" );
+    Vec_IntForEachEntry( vFront, Leaf, i )
+    {
+        CostCur = Ivy_NodeGetLeafCostOne( p, Leaf, vInside );
+//printf( "    Fanin %s has cost %d.\n", Ivy_ObjName(pNode), CostCur );
+        if ( CostBest > CostCur )
+        {
+            CostBest = CostCur;
+            LeafBest = Leaf;
+            LeavesBest[0] = Leaf;
+            Counter = 1;
+        }
+        else if ( CostBest == CostCur )
+            LeavesBest[Counter++] = Leaf;
+
+        if ( CostBest <= 1 ) // can be if ( CostBest <= 1 )
+            break;
+    }
+    if ( CostBest == 99 )
+        return 0;
+//        return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit );
+
+    assert( CostBest < 3 );
+    if ( Vec_IntSize(vFront) - 1 + CostBest > nSizeLimit )
+        return 0;
+//        return Ivy_NodeBuildCutLevelTwo_int( vInside, vFront, nFaninLimit );
+
+    assert( Counter > 0 );
+printf( "%d", Counter );
+
+    LeafBest = LeavesBest[rand() % Counter];
+
+    // remove the node from the array
+    assert( LeafBest >= 0 );
+    Vec_IntRemove( vFront, LeafBest );
+//printf( "Removing fanin %s.\n", Ivy_ObjName(pNode) );
+
+    // get the node and its latches
+    pNode = Ivy_ManObj( p, Ivy_LeafId(LeafBest) );
+    nLatches = Ivy_LeafLat(LeafBest) + Ivy_ObjIsLatch(pNode);
+    assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) );
+
+    // add the left child to the fanins
+    Next = Ivy_LeafCreate( Ivy_ObjFaninId0(pNode), nLatches );
+    if ( Next && Vec_IntFind(vInside, Next) == -1 )
+    {
+//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) );
+        Vec_IntPush( vFront, Next );
+        Vec_IntPush( vInside, Next );
+    }
+
+    // quit if this is the one fanin node
+    if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
+        return 1;
+    assert( Ivy_ObjIsNode(pNode) );
+
+    // add the right child to the fanins
+    Next = Ivy_LeafCreate( Ivy_ObjFaninId1(pNode), nLatches );
+    if ( Next && Vec_IntFind(vInside, Next) == -1 )
+    {
+//printf( "Adding fanin %s.\n", Ivy_ObjName(pNext) );
+        Vec_IntPush( vFront, Next );
+        Vec_IntPush( vInside, Next );
+    }
+    assert( Vec_IntSize(vFront) <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes one sequential cut of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize )
+{
+    assert( !Ivy_IsComplement(pRoot) );
+    assert( Ivy_ObjIsNode(pRoot) );
+    assert( Ivy_ObjFaninId0(pRoot) );
+    assert( Ivy_ObjFaninId1(pRoot) );
+
+    // start the cut 
+    Vec_IntClear( vFront );
+    Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
+    Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
+
+    // start the visited nodes
+    Vec_IntClear( vInside );
+    Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) );
+    Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) );
+    Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
+
+    // compute the cut
+    while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) );
+    assert( Vec_IntSize(vFront) <= nSize );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
new file mode 100644
index 00000000..2db80b00
--- /dev/null
+++ b/src/temp/ivy/ivyDfs.c
@@ -0,0 +1,152 @@
+/**CFile****************************************************************
+
+  FileName    [ivyDfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [DFS collection procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManDfs_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
+{
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+        return;
+    if ( Ivy_ObjIsMarkA(pObj) )
+        return;
+    Ivy_ObjSetMarkA(pObj);
+    assert( Ivy_ObjIsBuf(pObj) || Ivy_ObjIsAnd(pObj) || Ivy_ObjIsExor(pObj) );
+    Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    if ( !Ivy_ObjIsBuf(pObj) )
+        Ivy_ManDfs_rec( Ivy_ObjFanin1(pObj), vNodes );
+    Vec_IntPush( vNodes, pObj->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects AND/EXOR nodes in the DFS order from CIs to COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Ivy_Obj_t * pObj;
+    int i;
+    // collect the nodes
+    vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
+    if ( Ivy_ManLatchNum(p) > 0 )
+        Ivy_ManForEachCo( p, pObj, i )
+            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    else
+        Ivy_ManForEachPo( p, pObj, i )
+            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    // unmark the collected nodes
+    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) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
+{
+    Vec_Int_t * vFanins;
+    int i, Fanin;
+    if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) )
+        return;
+    // mark the node as visited
+    Ivy_ObjSetMarkA(pObj);
+    // traverse the fanins
+    vFanins = Ivy_ObjGetFanins( pObj );
+    Vec_IntForEachEntry( vFanins, Fanin, i )
+        Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes );
+    // add the node
+    Vec_IntPush( vNodes, pObj->Id );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
+{
+    Vec_Int_t * vNodes;
+    Ivy_Obj_t * pObj, * pFanin;
+    int i;
+    assert( p->fExtended ); 
+    assert( Ivy_ManLatchNum(p) == 0 ); 
+    // make sure network does not have buffers
+    vNodes = Vec_IntAlloc( 10 );
+    Ivy_ManForEachPo( p, pObj, i )
+    {
+        pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) );
+        Ivy_ManDfsExt_rec( pFanin, vNodes );
+    }
+    Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        Ivy_ObjClearMarkA(pObj);
+    // make sure network does not have dangling nodes
+    // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes
+//    assert( p->nNodes == Vec_PtrSize(vNodes) );
+    return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyDsd.c b/src/temp/ivy/ivyDsd.c
new file mode 100644
index 00000000..5dfdd30f
--- /dev/null
+++ b/src/temp/ivy/ivyDsd.c
@@ -0,0 +1,819 @@
+/**CFile****************************************************************
+
+  FileName    [ivyDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Disjoint-support decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// decomposition types
+typedef enum { 
+    IVY_DEC_PI,             // 0: var
+    IVY_DEC_CONST1,         // 1: CONST1
+    IVY_DEC_BUF,            // 2: BUF
+    IVY_DEC_AND,            // 3: AND
+    IVY_DEC_EXOR,           // 4: EXOR
+    IVY_DEC_MUX,            // 5: MUX
+    IVY_DEC_MAJ,            // 6: MAJ
+    IVY_DEC_PRIME           // 7: undecomposable
+} Ivy_DecType_t;
+
+typedef struct Ivy_Dec_t_ Ivy_Dec_t;
+struct Ivy_Dec_t_
+{
+    unsigned  Type   : 4;   // the node type (PI, CONST1, AND, EXOR, MUX, PRIME)
+    unsigned  fCompl : 1;   // shows if node is complemented (root node only)
+    unsigned  nFans  : 3;   // the number of fanins
+    unsigned  Fan0   : 4;   // fanin 0
+    unsigned  Fan1   : 4;   // fanin 1 
+    unsigned  Fan2   : 4;   // fanin 2
+    unsigned  Fan3   : 4;   // fanin 3 
+    unsigned  Fan4   : 4;   // fanin 4 
+    unsigned  Fan5   : 4;   // fanin 5
+};
+
+static inline int        Ivy_DecToInt( Ivy_Dec_t Node )     { return *((int *)&Node);       }
+static inline Ivy_Dec_t  Ivy_IntToDec( int Node )           { return *((Ivy_Dec_t *)&Node); }
+static inline void       Ivy_DecClear( Ivy_Dec_t * pNode )  { *((int *)pNode) = 0;          }
+
+
+static unsigned s_Masks[6][2] = {
+    { 0x55555555, 0xAAAAAAAA },
+    { 0x33333333, 0xCCCCCCCC },
+    { 0x0F0F0F0F, 0xF0F0F0F0 },
+    { 0x00FF00FF, 0xFF00FF00 },
+    { 0x0000FFFF, 0xFFFF0000 },
+    { 0x00000000, 0xFFFFFFFF }
+};
+
+static inline int        Ivy_TruthWordCountOnes( unsigned uWord )
+{
+    uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+    uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+    uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+    uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+    return  (uWord & 0x0000FFFF) + (uWord>>16);
+}
+
+static inline int        Ivy_TruthCofactorIsConst( unsigned uTruth, int Var, int Cof, int Const )
+{
+    if ( Const == 0 )
+        return (uTruth & s_Masks[Var][Cof]) == 0;
+    else
+        return (uTruth & s_Masks[Var][Cof]) == s_Masks[Var][Cof];
+}
+
+static inline int        Ivy_TruthCofactorIsOne( unsigned uTruth, int Var )
+{
+    return (uTruth & s_Masks[Var][0]) == 0;
+}
+
+static inline unsigned   Ivy_TruthCofactor( unsigned uTruth, int Var )
+{
+    unsigned uCofactor = uTruth & s_Masks[Var >> 1][(Var & 1) == 0];
+    int Shift = (1 << (Var >> 1));
+    if ( Var & 1 )
+        return uCofactor | (uCofactor << Shift);
+    return uCofactor | (uCofactor >> Shift);
+}
+
+static inline unsigned   Ivy_TruthCofactor2( unsigned uTruth, int Var0, int Var1 )
+{
+    return Ivy_TruthCofactor( Ivy_TruthCofactor(uTruth, Var0), Var1 );
+}
+
+// returns 1 if the truth table depends on this var (var is regular interger var)
+static inline int        Ivy_TruthDepends( unsigned uTruth, int Var )
+{
+    return Ivy_TruthCofactor(uTruth, Var << 1) != Ivy_TruthCofactor(uTruth, (Var << 1) | 1);
+}
+
+static inline void       Ivy_DecSetVar( Ivy_Dec_t * pNode, int iNum, unsigned Var )
+{
+    assert( iNum >= 0 && iNum <= 5 );
+    switch( iNum )
+    {
+        case 0: pNode->Fan0 = Var; break;
+        case 1: pNode->Fan1 = Var; break;
+        case 2: pNode->Fan2 = Var; break;
+        case 3: pNode->Fan3 = Var; break;
+        case 4: pNode->Fan4 = Var; break;
+        case 5: pNode->Fan5 = Var; break;
+    }
+}
+
+static inline unsigned   Ivy_DecGetVar( Ivy_Dec_t * pNode, int iNum )
+{
+    assert( iNum >= 0 && iNum <= 5 );
+    switch( iNum )
+    {
+        case 0: return pNode->Fan0;
+        case 1: return pNode->Fan1;
+        case 2: return pNode->Fan2;
+        case 3: return pNode->Fan3;
+        case 4: return pNode->Fan4;
+        case 5: return pNode->Fan5;
+    }
+    return ~0;
+}
+
+static int   Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree );
+static int   Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree );
+
+//int nTruthDsd;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes DSD of truth table of 5 variables or less.]
+
+  Description [Returns 1 if the function is a constant or is fully 
+  DSD decomposable using AND/EXOR/MUX gates.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree )
+{
+    Ivy_Dec_t Node;
+    int i, RetValue;
+    // set the PI variables
+    Vec_IntClear( vTree );
+    for ( i = 0; i < 5; i++ )
+        Vec_IntPush( vTree, 0 );
+    // check if it is a constant
+    if ( uTruth == 0 || ~uTruth == 0 )
+    {
+        Ivy_DecClear( &Node );
+        Node.Type = IVY_DEC_CONST1;
+        Node.fCompl = (uTruth == 0);
+        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+        return 1;
+    }
+    // perform the decomposition
+    RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
+    if ( RetValue == -1 )
+        return 0;
+    // get the topmost node
+    if ( (RetValue >> 1) < 5 )
+    { // add buffer
+        Ivy_DecClear( &Node );
+        Node.Type = IVY_DEC_BUF;
+        Node.fCompl = (RetValue & 1);
+        Node.Fan0 = ((RetValue >> 1) << 1);
+        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+    }
+    else if ( RetValue & 1 )
+    { // check if the topmost node has to be complemented
+        Node = Ivy_IntToDec( Vec_IntPop(vTree) );
+        assert( Node.fCompl == 0 );
+        Node.fCompl = (RetValue & 1);
+        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+    }
+    if ( uTruth != Ivy_TruthDsdCompute(vTree) )
+        printf( "Verification failed.\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes DSD of truth table.]
+
+  Description [Returns the number of topmost decomposition node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_TruthDecompose_rec( unsigned uTruth, Vec_Int_t * vTree )
+{
+    Ivy_Dec_t Node;
+    int Supp[5], Vars0[5], Vars1[5], Vars2[5], * pVars;
+    int nSupp, Count0, Count1, Count2, nVars, RetValue, fCompl, i;
+    unsigned uTruthCof, uCof0, uCof1;
+
+    // get constant confactors
+    Count0 = Count1 = Count2 = nSupp = 0;
+    for ( i = 0; i < 5; i++ )
+    {
+        if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 0) )
+            Vars0[Count0++] = (i << 1) | 0;
+        else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 0) )
+            Vars0[Count0++] = (i << 1) | 1;
+        else if ( Ivy_TruthCofactorIsConst(uTruth, i, 0, 1) )
+            Vars1[Count1++] = (i << 1) | 0;
+        else if ( Ivy_TruthCofactorIsConst(uTruth, i, 1, 1) )
+            Vars1[Count1++] = (i << 1) | 1;
+        else
+        {
+            uCof0 = Ivy_TruthCofactor( uTruth, (i << 1) | 1 );
+            uCof1 = Ivy_TruthCofactor( uTruth, (i << 1) | 0 );
+            if ( uCof0 == ~uCof1 )
+                Vars2[Count2++] = (i << 1) | 0;
+            else if ( uCof0 != uCof1 )
+                Supp[nSupp++] = i;
+        }
+    }
+    assert( Count0 == 0 || Count1 == 0 );
+    assert( Count0 == 0 || Count2 == 0 );
+    assert( Count1 == 0 || Count2 == 0 );
+
+    // consider the case of a single variable
+    if ( Count0 == 1 && nSupp == 0 )
+        return Vars0[0];
+
+    // consider more complex decompositions
+    if ( Count0 == 0 && Count1 == 0 && Count2 == 0 )
+        return Ivy_TruthRecognizeMuxMaj( uTruth, Supp, nSupp, vTree );
+
+    // extract the nodes
+    Ivy_DecClear( &Node );
+    if ( Count0 > 0 )
+        nVars = Count0, pVars = Vars0, Node.Type = IVY_DEC_AND,  fCompl = 0;
+    else if ( Count1 > 0 )
+        nVars = Count1, pVars = Vars1, Node.Type = IVY_DEC_AND,  fCompl = 1, uTruth = ~uTruth;
+    else if ( Count2 > 0 )
+        nVars = Count2, pVars = Vars2, Node.Type = IVY_DEC_EXOR, fCompl = 0;
+    else 
+        assert( 0 );
+    Node.nFans = nVars+(nSupp>0);
+
+    // compute cofactor
+    uTruthCof = uTruth;
+    for ( i = 0; i < nVars; i++ )
+    {
+        uTruthCof = Ivy_TruthCofactor( uTruthCof, pVars[i] );
+        Ivy_DecSetVar( &Node, i, pVars[i] );
+    }
+
+    if ( Node.Type == IVY_DEC_EXOR )
+        fCompl ^= ((Node.nFans & 1) == 0);
+
+    if ( nSupp > 0 )
+    {
+        assert( uTruthCof != 0 && ~uTruthCof != 0 );
+        // call recursively
+        RetValue = Ivy_TruthDecompose_rec( uTruthCof, vTree );
+        // quit if non-decomposable
+        if ( RetValue == -1 )
+            return -1;
+        // remove the complement from the child if the node is EXOR
+        if ( Node.Type == IVY_DEC_EXOR && (RetValue & 1) )
+        {
+            fCompl ^= 1;
+            RetValue ^= 1;
+        }
+        // set the new decomposition
+        Ivy_DecSetVar( &Node, nVars, RetValue );
+    }
+    else if ( Node.Type == IVY_DEC_EXOR )
+        fCompl ^= (uTruthCof == 0);
+
+    Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+    return ((Vec_IntSize(vTree)-1) << 1) | fCompl;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns a non-negative number if the truth table is a MUX.]
+
+  Description [If the truth table is a MUX, returns the variable as follows:
+  first, control variable; second, positive cofactor; third, negative cofactor.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_TruthRecognizeMuxMaj( unsigned uTruth, int * pSupp, int nSupp, Vec_Int_t * vTree )
+{
+    Ivy_Dec_t Node;
+    int i, k, RetValue0, RetValue1;
+    unsigned uCof0, uCof1, Num;
+    char Count[3];
+    assert( nSupp >= 3 );
+    // start the node
+    Ivy_DecClear( &Node );
+    Node.Type = IVY_DEC_MUX;
+    Node.nFans = 3;
+    // try each of the variables
+    for ( i = 0; i < nSupp; i++ )
+    {
+        // get the cofactors with respect to these variables
+        uCof0 = Ivy_TruthCofactor( uTruth, (pSupp[i] << 1) | 1 );
+        uCof1 = Ivy_TruthCofactor( uTruth,  pSupp[i] << 1 );
+        // go through all other variables and make sure 
+        // each of them belongs to the support of one cofactor
+        for ( k = 0; k < nSupp; k++ )
+        {
+            if ( k == i )
+                continue;
+            if ( Ivy_TruthDepends(uCof0, pSupp[k]) && Ivy_TruthDepends(uCof1, pSupp[k]) )
+                break;
+        }
+        if ( k < nSupp )
+            continue;
+        // MUX decomposition exists
+        RetValue0 = Ivy_TruthDecompose_rec( uCof0, vTree );
+        if ( RetValue0 == -1 )
+            break;
+        RetValue1 = Ivy_TruthDecompose_rec( uCof1, vTree );
+        if ( RetValue1 == -1 )
+            break;
+        // both of them exist; create the node
+        Ivy_DecSetVar( &Node, 0, pSupp[i] << 1 );
+        Ivy_DecSetVar( &Node, 1, RetValue1 );
+        Ivy_DecSetVar( &Node, 2, RetValue0 );
+        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+        return ((Vec_IntSize(vTree)-1) << 1) | 0;
+    }
+    // check majority gate
+    if ( nSupp > 3 )
+        return -1;
+    if ( Ivy_TruthWordCountOnes(uTruth) != 16 )
+        return -1;
+    // this is a majority gate; determine polarity
+    Node.Type = IVY_DEC_MAJ;
+    Count[0] = Count[1] = Count[2] = 0;
+    for ( i = 0; i < 8; i++ )
+    {
+        Num = 0;
+        for ( k = 0; k < 3; k++ )
+            if ( i & (1 << k) )
+                Num |= (1 << pSupp[k]);
+        assert( Num < 32 );
+        if ( (uTruth & (1 << Num)) == 0 )
+            continue;
+        for ( k = 0; k < 3; k++ )
+            if ( i & (1 << k) )
+                Count[k]++;
+    }
+    assert( Count[0] == 1 || Count[0] == 3 );
+    assert( Count[1] == 1 || Count[1] == 3 );
+    assert( Count[2] == 1 || Count[2] == 3 );
+    Ivy_DecSetVar( &Node, 0, (pSupp[0] << 1)|(Count[0] == 1) );
+    Ivy_DecSetVar( &Node, 1, (pSupp[1] << 1)|(Count[1] == 1) );
+    Ivy_DecSetVar( &Node, 2, (pSupp[2] << 1)|(Count[2] == 1) );
+    Vec_IntPush( vTree, Ivy_DecToInt(Node) );
+    return ((Vec_IntSize(vTree)-1) << 1) | 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of decomposition tree for verification.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_TruthDsdCompute_rec( int iNode, Vec_Int_t * vTree )
+{
+    unsigned uTruthChild, uTruthTotal;
+    int Var, i;
+    // get the node
+    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
+    // compute the node function
+    if ( Node.Type == IVY_DEC_CONST1 )
+        return s_Masks[5][ !Node.fCompl ];
+    if ( Node.Type == IVY_DEC_PI )
+        return s_Masks[iNode][ !Node.fCompl ];
+    if ( Node.Type == IVY_DEC_BUF )
+    {
+        uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree );
+        return Node.fCompl? ~uTruthTotal : uTruthTotal;
+    }
+    if ( Node.Type == IVY_DEC_AND )
+    {
+        uTruthTotal = s_Masks[5][1];
+        for ( i = 0; i < (int)Node.nFans; i++ )
+        {
+            Var = Ivy_DecGetVar( &Node, i );
+            uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
+            uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild;
+        }
+        return Node.fCompl? ~uTruthTotal : uTruthTotal;
+    }
+    if ( Node.Type == IVY_DEC_EXOR )
+    {
+        uTruthTotal = 0;
+        for ( i = 0; i < (int)Node.nFans; i++ )
+        {
+            Var = Ivy_DecGetVar( &Node, i );
+            uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
+            assert( (Var & 1) == 0 );
+        }
+        return Node.fCompl? ~uTruthTotal : uTruthTotal;
+    }
+    assert( Node.fCompl == 0 );
+    if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
+    {
+        unsigned uTruthChildC, uTruthChild1, uTruthChild0;
+        int VarC, Var1, Var0;
+        VarC = Ivy_DecGetVar( &Node, 0 );
+        Var1 = Ivy_DecGetVar( &Node, 1 );
+        Var0 = Ivy_DecGetVar( &Node, 2 );
+        uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree );
+        uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree );
+        uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree );
+        assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
+        uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC;
+        uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1;
+        uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0;
+        if ( Node.Type == IVY_DEC_MUX )
+            return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0);
+        else
+            return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0);
+    }
+    assert( 0 );
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of decomposition tree for verification.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_TruthDsdCompute( Vec_Int_t * vTree )
+{
+    return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decomposition tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthDsdPrint_rec( FILE * pFile, int iNode, Vec_Int_t * vTree )
+{
+    int Var, i;
+    // get the node
+    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
+    // compute the node function
+    if ( Node.Type == IVY_DEC_CONST1 )
+        fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") );
+    else if ( Node.Type == IVY_DEC_PI )
+        fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") );
+    else if ( Node.Type == IVY_DEC_BUF )
+    {
+        Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree );
+        fprintf( pFile, "%s", (Node.fCompl? "\'" : "") );
+    }
+    else if ( Node.Type == IVY_DEC_AND )
+    {
+        fprintf( pFile, "AND(" );
+        for ( i = 0; i < (int)Node.nFans; i++ )
+        {
+            Var = Ivy_DecGetVar( &Node, i );
+            Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
+            fprintf( pFile, "%s", (Var & 1)? "\'" : "" );
+            if ( i != (int)Node.nFans-1 )
+                fprintf( pFile, "," );
+        }
+        fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
+    }
+    else if ( Node.Type == IVY_DEC_EXOR )
+    {
+        fprintf( pFile, "EXOR(" );
+        for ( i = 0; i < (int)Node.nFans; i++ )
+        {
+            Var = Ivy_DecGetVar( &Node, i );
+            Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
+            if ( i != (int)Node.nFans-1 )
+                fprintf( pFile, "," );
+            assert( (Var & 1) == 0 );
+        }
+        fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
+    }
+    else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
+    {
+        int VarC, Var1, Var0;
+        assert( Node.fCompl == 0 );
+        VarC = Ivy_DecGetVar( &Node, 0 );
+        Var1 = Ivy_DecGetVar( &Node, 1 );
+        Var0 = Ivy_DecGetVar( &Node, 2 );
+        fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" );
+        Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree );
+        fprintf( pFile, "%s", (VarC & 1)? "\'" : "" );
+        fprintf( pFile, "," );
+        Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree );
+        fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" );
+        fprintf( pFile, "," );
+        Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree );
+        fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" );
+        fprintf( pFile, ")" );
+    }
+    else assert( 0 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the decomposition tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree )
+{
+    fprintf( pFile, "F = " );
+    Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implement DSD in the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNode, Vec_Int_t * vTree )
+{
+    Ivy_Obj_t * pResult, * pChild, * pNodes[16];
+    int Var, i;
+    // get the node
+    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
+    // compute the node function
+    if ( Node.Type == IVY_DEC_CONST1 )
+        return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl );
+    if ( Node.Type == IVY_DEC_PI )
+    {
+        pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) );
+        return Ivy_NotCond( pResult, Node.fCompl );
+    }
+    if ( Node.Type == IVY_DEC_BUF )
+    {
+        pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree );
+        return Ivy_NotCond( pResult, Node.fCompl );
+    }
+    if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR )
+    {
+        for ( i = 0; i < (int)Node.nFans; i++ )
+        {
+            Var = Ivy_DecGetVar( &Node, i );
+            assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 );
+            pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree );
+            pChild = Ivy_NotCond( pChild, (Var & 1) );
+            pNodes[i] = pChild;
+        }
+
+//        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
+
+        pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
+        return Ivy_NotCond( pResult, Node.fCompl );
+    }
+    assert( Node.fCompl == 0 );
+    if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
+    {
+        int VarC, Var1, Var0;
+        VarC = Ivy_DecGetVar( &Node, 0 );
+        Var1 = Ivy_DecGetVar( &Node, 1 );
+        Var0 = Ivy_DecGetVar( &Node, 2 );
+        pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree );
+        pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree );
+        pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree );
+        assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
+        pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) );
+        pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
+        pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
+        if ( Node.Type == IVY_DEC_MUX )
+            return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] );
+        else
+            return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] );
+    }
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implement DSD in the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ManDsdConstruct( Ivy_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vTree )
+{
+    int Entry, i;
+    // implement latches on the frontier (TEMPORARY!!!)
+    Vec_IntForEachEntry( vFront, Entry, i )
+        Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
+    // recursively construct the tree
+    return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthDsdComputePrint( unsigned uTruth )
+{
+    static Vec_Int_t * vTree = NULL;
+    if ( vTree == NULL )
+        vTree = Vec_IntAlloc( 12 );
+    if ( Ivy_TruthDsd( uTruth, vTree ) )
+        Ivy_TruthDsdPrint( stdout, vTree );
+    else
+        printf( "Undecomposable\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthTestOne( unsigned uTruth )
+{
+    static int Counter = 0;
+    static Vec_Int_t * vTree = NULL;
+    // decompose
+    if ( vTree == NULL )
+        vTree = Vec_IntAlloc( 12 );
+
+    if ( !Ivy_TruthDsd( uTruth, vTree ) )
+    {
+//        printf( "Undecomposable\n" );
+    }
+    else
+    {
+//        nTruthDsd++;
+        printf( "%5d : ", Counter++ );
+        Extra_PrintBinary( stdout, &uTruth, 32 );
+        printf( "  " );
+        Ivy_TruthDsdPrint( stdout, vTree );
+        if ( uTruth != Ivy_TruthDsdCompute(vTree) )
+            printf( "Verification failed.\n" );
+    }
+//    Vec_IntFree( vTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthTest()
+{
+    FILE * pFile;
+    char Buffer[100];
+    unsigned uTruth;
+    int i;
+
+    pFile = fopen( "npn4.txt", "r" );
+    for ( i = 0; i < 222; i++ )
+//    pFile = fopen( "npn5.txt", "r" );
+//    for ( i = 0; i < 616126; i++ )
+    {
+        fscanf( pFile, "%s", Buffer );
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
+//        Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
+        uTruth |= (uTruth << 16);
+//        uTruth = ~uTruth;
+        Ivy_TruthTestOne( uTruth );
+    }
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthTest3()
+{
+    FILE * pFile;
+    char Buffer[100];
+    unsigned uTruth;
+    int i;
+
+    pFile = fopen( "npn3.txt", "r" );
+    for ( i = 0; i < 14; i++ )
+    {
+        fscanf( pFile, "%s", Buffer );
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 3 );
+        uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24);
+        Ivy_TruthTestOne( uTruth );
+    }
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthTest5()
+{
+    FILE * pFile;
+    char Buffer[100];
+    unsigned uTruth;
+    int i;
+
+//    pFile = fopen( "npn4.txt", "r" );
+//    for ( i = 0; i < 222; i++ )
+    pFile = fopen( "npn5.txt", "r" );
+    for ( i = 0; i < 616126; i++ )
+    {
+        fscanf( pFile, "%s", Buffer );
+//        Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 );
+        Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
+//        uTruth |= (uTruth << 16);
+//        uTruth = ~uTruth;
+        Ivy_TruthTestOne( uTruth );
+    }
+    fclose( pFile );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
new file mode 100644
index 00000000..04c31f3d
--- /dev/null
+++ b/src/temp/ivy/ivyMan.c
@@ -0,0 +1,207 @@
+/**CFile****************************************************************
+
+  FileName    [ivyMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [AIG manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
+{
+    Ivy_Man_t * p;
+    Ivy_Obj_t * pObj;
+    int i, nTotalSize;
+    // start the manager
+    p = ALLOC( Ivy_Man_t, 1 );
+    memset( p, 0, sizeof(Ivy_Man_t) );
+    p->nTravIds = 1;
+    // AIG nodes
+    p->nObjsAlloc = 1 + nPis + nPos + nNodesMax;
+//    p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even
+    nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1;
+    p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize );
+    memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize );
+    // temporary storage for deleted entries
+    p->vFree  = Vec_IntAlloc( 100 );
+    // set the node IDs
+    for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ )
+        pObj->Id = i - IVY_SANDBOX_SIZE - 1;
+    // remember the manager in the first entry
+    *((Ivy_Man_t **)p->pObjs) = p; 
+    p->pObjs += IVY_SANDBOX_SIZE + 1;
+    // create the constant node
+    p->nCreated = 1;
+    p->ObjIdNext = 1;
+    Ivy_ManConst1(p)->fPhase = 1;
+    // create PIs
+    pObj = Ivy_ManGhost(p);
+    pObj->Type = IVY_PI;
+    p->vPis = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nPis; i++ )
+        Ivy_ObjCreate( pObj );
+    // create POs
+    pObj->Type = IVY_PO;
+    p->vPos = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nPos; i++ )
+        Ivy_ObjCreate( pObj );
+    // start the table
+    p->nTableSize = p->nObjsAlloc*5/2+13;
+    p->pTable = ALLOC( int, p->nTableSize );
+    memset( p->pTable, 0, sizeof(int) * p->nTableSize );
+    // allocate undo storage
+    p->nUndosAlloc = 100;
+    p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc );
+    memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStop( Ivy_Man_t * p )
+{
+    if ( p->fExtended )
+    {
+        Ivy_Obj_t * pObj;
+        int i;
+        Ivy_ManForEachObj( p, pObj, i )
+            if ( Ivy_ObjGetFanins(pObj) )
+                Vec_IntFree( Ivy_ObjGetFanins(pObj) );
+    }
+    if ( p->vFree )   Vec_IntFree( p->vFree );
+    if ( p->vTruths ) Vec_IntFree( p->vTruths );
+    if ( p->vPis )    Vec_IntFree( p->vPis );
+    if ( p->vPos )    Vec_IntFree( p->vPos );
+    FREE( p->pMemory );
+    free( p->pObjs - IVY_SANDBOX_SIZE - 1 );
+    free( p->pTable );
+    free( p->pUndos );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManGrow( Ivy_Man_t * p )
+{
+    int i;
+    assert( p->ObjIdNext == p->nObjsAlloc );
+    if ( p->ObjIdNext != p->nObjsAlloc )
+        return;
+//    printf( "Ivy_ObjCreate(): Reallocing the node array.\n" );
+    p->nObjsAlloc = 2 * p->nObjsAlloc;
+    p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1;
+    memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 );
+    for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ )
+        Ivy_ManObj( p, i )->Id = i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManCleanup( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pNode;
+    int i, nNodesOld;
+    nNodesOld = Ivy_ManNodeNum(p);
+    Ivy_ManForEachNode( p, pNode, i )
+        if ( Ivy_ObjRefs(pNode) == 0 )
+            Ivy_ObjDelete_rec( pNode, 1 );
+    return nNodesOld - Ivy_ManNodeNum(p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManPrintStats( Ivy_Man_t * p )
+{
+    printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
+    if ( p->fExtended )
+    {
+    printf( "Am = %d. ",    Ivy_ManAndMultiNum(p) );
+    printf( "Xm = %d. ",    Ivy_ManExorMultiNum(p) );
+    printf( "Lut = %d. ",   Ivy_ManLutNum(p) );
+    }
+    else
+    {
+    printf( "A = %d. ",     Ivy_ManAndNum(p) );
+    printf( "X = %d. ",     Ivy_ManExorNum(p) );
+    printf( "B = %d. ",     Ivy_ManBufNum(p) );
+    }
+    printf( "MaxID = %d. ", p->ObjIdNext-1 );
+    printf( "All = %d. ",   p->nObjsAlloc );
+    printf( "Cre = %d. ",   p->nCreated );
+    printf( "Del = %d. ",   p->nDeleted );
+    printf( "\n" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
new file mode 100644
index 00000000..059d1500
--- /dev/null
+++ b/src/temp/ivy/ivyMulti.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
new file mode 100644
index 00000000..5d063525
--- /dev/null
+++ b/src/temp/ivy/ivyObj.c
@@ -0,0 +1,325 @@
+/**CFile****************************************************************
+
+  FileName    [ivyObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Adding/removing objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
+{
+    Ivy_Man_t * p = Ivy_ObjMan(pGhost);
+    Ivy_Obj_t * pObj;
+    assert( !Ivy_IsComplement(pGhost) );
+    assert( Ivy_ObjIsGhost(pGhost) );
+
+    assert( Ivy_TableLookup(pGhost) == NULL );
+
+    // realloc the node array
+    if ( p->ObjIdNext == p->nObjsAlloc )
+    {
+        Ivy_ManGrow( p );
+        pGhost = Ivy_ManGhost( p );
+    }
+    // get memory for the new object
+    if ( Vec_IntSize(p->vFree) > 0 )
+        pObj = p->pObjs + Vec_IntPop(p->vFree);
+    else
+        pObj = p->pObjs + p->ObjIdNext++;
+    assert( pObj->Id == pObj - p->pObjs );
+    assert( Ivy_ObjIsNone(pObj) );
+    // add basic info (fanins, compls, type, init)
+    Ivy_ObjOverwrite( pObj, pGhost );
+    // increment references of the fanins
+    Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
+    Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) );
+    // add the node to the structural hash table
+    Ivy_TableInsert( pObj );
+    // compute level
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->Level = Ivy_ObjLevelNew(pObj);
+    else if ( Ivy_ObjIsLatch(pObj) )
+        pObj->Level = 0;
+    else if ( Ivy_ObjIsOneFanin(pObj) )
+        pObj->Level = Ivy_ObjFanin0(pObj)->Level;
+    else if ( !Ivy_ObjIsPi(pObj) )
+        assert( 0 );
+    // mark the fanins in a special way if the node is EXOR
+    if ( Ivy_ObjIsExor(pObj) )
+    {
+        Ivy_ObjFanin0(pObj)->fExFan = 1;
+        Ivy_ObjFanin1(pObj)->fExFan = 1;
+    }
+    // add PIs/POs to the arrays
+    if ( Ivy_ObjIsPi(pObj) )
+        Vec_IntPush( p->vPis, pObj->Id );
+    else if ( Ivy_ObjIsPo(pObj) )
+        Vec_IntPush( p->vPos, pObj->Id );
+    // update node counters of the manager
+    p->nObjs[Ivy_ObjType(pObj)]++;
+    p->nCreated++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj;
+    assert( Type == IVY_ANDM || Type == IVY_EXORM || Type == IVY_LUT ); 
+    // realloc the node array
+    if ( p->ObjIdNext == p->nObjsAlloc )
+        Ivy_ManGrow( p );
+    // create the new node
+    pObj = p->pObjs + p->ObjIdNext;
+    assert( pObj->Id == p->ObjIdNext );
+    p->ObjIdNext++;
+    pObj->Type = Type;
+    // update node counters of the manager
+    p->nObjs[Type]++;
+    p->nCreated++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjConnect( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanin )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjIsOneFanin(pObj) );
+    assert( Ivy_ObjFaninId0(pObj) == 0 );
+    // add the first fanin
+    pObj->fComp0 = Ivy_IsComplement(pFanin);
+    pObj->Fanin0 = Ivy_Regular(pFanin)->Id;
+    // increment references of the fanins
+    Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) );
+    // add the node to the structural hash table
+    Ivy_TableInsert( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDelete( Ivy_Obj_t * pObj, int fFreeTop )
+{
+    Ivy_Man_t * p;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( Ivy_ObjRefs(pObj) == 0 );
+    // remove connections
+    Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj));
+    Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj));
+    // remove the node from the structural hash table
+    Ivy_TableDelete( pObj );
+    // update node counters of the manager
+    p = Ivy_ObjMan(pObj);
+    p->nObjs[pObj->Type]--;
+    p->nDeleted++;
+    // remove PIs/POs from the arrays
+    if ( Ivy_ObjIsPi(pObj) )
+        Vec_IntRemove( p->vPis, pObj->Id );
+    else if ( Ivy_ObjIsPo(pObj) )
+        Vec_IntRemove( p->vPos, pObj->Id );
+    // recorde the deleted node
+    if ( p->fRecording )
+        Ivy_ManUndoRecord( p, pObj );
+    // clean the node's memory
+    Ivy_ObjClean( pObj );
+    // remember the entry
+    if ( fFreeTop )
+        Vec_IntPush( p->vFree, pObj->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjDelete_rec( Ivy_Obj_t * pObj, int fFreeTop )
+{
+    Ivy_Obj_t * pFanin0, * pFanin1;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsNone(pObj) );
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) )
+        return;
+    pFanin0 = Ivy_ObjFanin0(pObj);
+    pFanin1 = Ivy_ObjFanin1(pObj);
+    Ivy_ObjDelete( pObj, fFreeTop );
+    if ( !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 )
+        Ivy_ObjDelete_rec( pFanin0, 1 );
+    if ( !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 )
+        Ivy_ObjDelete_rec( pFanin1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces one object by another.]
+
+  Description [Both objects are currently in the manager. The new object
+  (pObjNew) should be used instead of the old object (pObjOld). If the 
+  new object is complemented or used, the buffer is added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ObjReplace( Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop )
+{
+    int nRefsOld;
+    // the object to be replaced cannot be complemented
+    assert( !Ivy_IsComplement(pObjOld) );
+    // the object to be replaced cannot be a terminal
+    assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsTerm(pObjOld) );
+    // the object to be used cannot be a PO or assert
+    assert( !Ivy_ObjIsPo(Ivy_Regular(pObjNew)) );
+    // the object cannot be the same
+    assert( pObjOld != Ivy_Regular(pObjNew) );
+    // if the new object is complemented or already used, add the buffer
+    if ( Ivy_IsComplement(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+        pObjNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pObjNew, Ivy_ObjConst1(pObjOld), IVY_BUF, IVY_INIT_NONE) );
+    assert( !Ivy_IsComplement(pObjNew) );
+    // remember the reference counter
+    nRefsOld = pObjOld->nRefs;  
+    pObjOld->nRefs = 0;
+    // delete the old object
+    if ( fDeleteOld )
+        Ivy_ObjDelete_rec( pObjOld, fFreeTop );
+    // transfer the old object
+    assert( Ivy_ObjRefs(pObjNew) == 0 );
+    Ivy_ObjOverwrite( pObjOld, pObjNew );
+    pObjOld->nRefs = nRefsOld;
+    // update the hash table
+    Ivy_TableUpdate( pObjNew, pObjOld->Id );
+    // create the object that was taken over by pObjOld
+    Ivy_ObjClean( pObjNew );
+    // remember the entry
+    Vec_IntPush( Ivy_ObjMan(pObjOld)->vFree, pObjNew->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the first real fanins (not a buffer/inverter).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin )
+{
+    if ( iFanin == 0 )
+    {
+        if ( Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) )
+            return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin0(pNode), 0), Ivy_ObjFaninC0(pNode) );
+        else
+            return Ivy_ObjChild0(pNode);
+    }
+    else
+    {
+        if ( Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
+            return Ivy_NotCond( Ivy_NodeRealFanin_rec(Ivy_ObjFanin1(pNode), 0), Ivy_ObjFaninC1(pNode) );
+        else
+            return Ivy_ObjChild1(pNode);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fixes buffer fanins.]
+
+  Description [This situation happens because NodeReplace is a lazy
+  procedure, which does not propagate the change to the fanouts but
+  instead records the change in the form of a buf/inv node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeFixBufferFanins( Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult;
+    assert( Ivy_ObjIsNode(pNode) );
+    if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) )
+        return;
+    // get the real fanins
+    pFanReal0 = Ivy_NodeRealFanin_rec( pNode, 0 );
+    pFanReal1 = Ivy_NodeRealFanin_rec( pNode, 1 );
+    // get the new node
+    pResult = Ivy_Oper( pFanReal0, pFanReal1, Ivy_ObjType(pNode) );
+    // perform the replacement
+    Ivy_ObjReplace( pNode, pResult, 1, 0 ); 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
new file mode 100644
index 00000000..a10ba343
--- /dev/null
+++ b/src/temp/ivy/ivyOper.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+  FileName    [ivyOper.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [AIG operations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// procedure to detect an EXOR gate
+static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t ** ppFan0, Ivy_Obj_t ** ppFan1 )
+{
+    if ( !Ivy_IsComplement(p0) || !Ivy_IsComplement(p1) )
+        return 0;
+    p0 = Ivy_Regular(p0);
+    p1 = Ivy_Regular(p1);
+    if ( !Ivy_ObjIsAnd(p0) || !Ivy_ObjIsAnd(p1) )
+        return 0;
+    if ( Ivy_ObjFanin0(p0) != Ivy_ObjFanin0(p1) || Ivy_ObjFanin1(p0) != Ivy_ObjFanin1(p1) )
+        return 0;
+    if ( Ivy_ObjFaninC0(p0) == Ivy_ObjFaninC0(p1) || Ivy_ObjFaninC1(p0) == Ivy_ObjFaninC1(p1) )
+        return 0;
+    *ppFan0 = Ivy_ObjChild0(p0);
+    *ppFan1 = Ivy_ObjChild1(p0);
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Perform one operation.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
+{
+    if ( Type == IVY_AND )
+        return Ivy_And( p0, p1 );
+    if ( Type == IVY_EXOR )
+        return Ivy_Exor( p0, p1 );
+    assert( 0 );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    // check trivial cases
+    if ( p0 == p1 )
+        return p0;
+    if ( p0 == Ivy_Not(p1) )
+        return Ivy_Not(pConst1);
+    if ( Ivy_Regular(p0) == pConst1 )
+        return p0 == pConst1 ? p1 : Ivy_Not(pConst1);
+    if ( Ivy_Regular(p1) == pConst1 )
+        return p1 == pConst1 ? p0 : Ivy_Not(pConst1);
+    // check if it can be an EXOR gate
+    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
+        return Ivy_CanonExor( pFan0, pFan1 );
+    return Ivy_CanonAnd( p0, p1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description [The argument nodes can be complemented.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+{
+    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
+    // check trivial cases
+    if ( p0 == p1 )
+        return Ivy_Not(pConst1);
+    if ( p0 == Ivy_Not(p1) )
+        return pConst1;
+    if ( Ivy_Regular(p0) == pConst1 )
+        return Ivy_NotCond( p1, p0 == pConst1 );
+    if ( Ivy_Regular(p1) == pConst1 )
+        return Ivy_NotCond( p0, p1 == pConst1 );
+    // check the table
+    return Ivy_CanonExor( p0, p1 );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
+{
+    return Ivy_CanonLatch( pObj, Init );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements Boolean OR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+{
+    return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements ITE operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
+{
+    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
+    Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
+    int Count0, Count1;
+    // consider trivial cases
+    if ( p0 == Ivy_Not(p1) )
+        return Ivy_Exor( pC, p0 );
+    // other cases can be added
+    // implement the first MUX (F = C * x1 + C' * x0)
+    pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          p1, IVY_AND, IVY_INIT_NONE) );
+    pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
+    if ( pTempA1 && pTempA2 )
+    {
+        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
+        if ( pTemp ) return Ivy_Not(pTemp);
+    }
+    Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
+    // implement the second MUX (F' = C * x1' + C' * x0')
+    pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
+    pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
+    if ( pTempB1 && pTempB2 )
+    {
+        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
+        if ( pTemp ) return pTemp;
+    }
+    Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
+    // compare and decide which one to implement
+    if ( Count0 >= Count1 )
+    {
+        pTempA1 = pTempA1? pTempA1 : Ivy_And(pC,          p1);
+        pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0);
+        return Ivy_Or( pTempA1, pTempA2 );
+    }
+    pTempB1 = pTempB1? pTempB1 : Ivy_And(pC,          Ivy_Not(p1));
+    pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0));
+    return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) );
+
+//    return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements ITE operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
+{
+    return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs )
+{
+    int i;
+    assert( vPairs->nSize > 0 );
+    assert( vPairs->nSize % 2 == 0 );
+    // go through the cubes of the node's SOP
+    for ( i = 0; i < vPairs->nSize; i += 2 )
+        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) );
+    vPairs->nSize = vPairs->nSize/2;
+    return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c
new file mode 100644
index 00000000..031db9bc
--- /dev/null
+++ b/src/temp/ivy/ivyRewrite.c
@@ -0,0 +1,365 @@
+/**CFile****************************************************************
+
+  FileName    [ivyRewrite.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [AIG rewriting.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned    Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront );
+static void        Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone );
+static int         Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs Boolean rewriting of sequential AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
+{
+    Vec_Int_t * vNodes, * vFront, * vInside, * vTree;
+    Ivy_Obj_t * pNode, * pNodeNew, * pTemp;
+    int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs;
+    int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock();
+    unsigned uTruth;
+
+    nInputs  = 4;
+    vTree    = Vec_IntAlloc( 8 );
+    vFront   = Vec_IntAlloc( 8 );
+    vInside  = Vec_IntAlloc( 50 );
+    vNodes   = Ivy_ManDfs( p );
+    Ivy_ManForEachNodeVec( p, vNodes, pNode, i )
+    {
+        if ( Ivy_ObjIsBuf(pNode) )
+            continue;
+        // fix the fanin buffer problem
+        Ivy_NodeFixBufferFanins( pNode );
+        if ( Ivy_ObjIsBuf(pNode) )
+            continue;
+
+        // find one sequential cut rooted at this node
+clk = clock();
+        Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs );
+clkCut += clock() - clk;
+        // compute the truth table of the cut
+clk = clock();
+        uTruth = Ivy_ManSeqFindTruth( pNode, vFront );
+clkTru += clock() - clk;
+        // decompose the truth table
+clk = clock();
+        RetValue = Ivy_TruthDsd( uTruth, vTree );
+clkDsd += clock() - clk;
+        if ( !RetValue )
+            continue; // DSD does not exist
+//        Ivy_TruthDsdPrint( stdout, vTree );
+
+clk = clock();
+        // remember the cost of the current network
+        nCostOld = Ivy_ManGetCost(p);
+        // increment references of the cut variables
+        Vec_IntForEachEntry( vFront, Entry, k )
+        {
+            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
+            Ivy_ObjRefsInc( pTemp );
+        }
+        // dereference and record undo
+        nRefsSaved = pNode->nRefs; pNode->nRefs = 0;
+        Ivy_ManUndoStart( p );
+        Ivy_ObjDelete_rec( pNode, 0 );
+        Ivy_ManUndoStop( p );
+        pNode->nRefs = nRefsSaved;
+
+        // get the intermediate cost
+        nCostInt = Ivy_ManGetCost(p);
+
+//        printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt );
+
+        // construct the new logic cone
+        pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree );
+        // remember the cost
+        nCostNew = Ivy_ManGetCost(p);
+
+//        printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew );
+//        nCostNew = nCostNew;
+
+/*
+        if ( Ivy_Regular(pNodeNew)->nRefs == 0 )
+            Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 );
+        // get the intermediate cost
+        nCostInt2 = Ivy_ManGetCost(p);
+        assert( nCostInt == nCostInt2 );
+
+        Ivy_ManUndoPerform( p, pNode );
+        pNode->nRefs = nRefsSaved;
+
+        Vec_IntForEachEntry( vFront, Entry, k )
+        {
+//            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
+            pTemp = Ivy_ManObj(p, Entry);
+            Ivy_ObjRefsDec( pTemp );
+        }
+clkUpd += clock() - clk;
+        continue;
+*/
+
+        // detect the case when they are exactly the same
+//        if ( pNodeNew == pNode )
+//            continue;
+
+        // compare the costs
+        if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost )
+        { // accept the change
+//            printf( "NODES GAINED = %d\n", nCostOld - nCostNew );
+
+            Ivy_ObjReplace( pNode, pNodeNew, 0, 1 );
+            pNode->nRefs = nRefsSaved;
+        }
+        else
+        { // reject change
+//            printf( "Rejected\n" );
+
+            if ( Ivy_Regular(pNodeNew)->nRefs == 0 )
+                Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 );
+
+            // get the intermediate cost
+            nCostInt2 = Ivy_ManGetCost(p);
+            assert( nCostInt == nCostInt2 );
+
+            // reconstruct the old node
+            Ivy_ManUndoPerform( p, pNode );
+            pNode->nRefs = nRefsSaved;
+        }
+        // decrement references of the cut variables
+        Vec_IntForEachEntry( vFront, Entry, k )
+        {
+//            pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry));
+            pTemp = Ivy_ManObj(p, Entry);
+            if ( Ivy_ObjIsNone(pTemp) )
+                continue;
+            Ivy_ObjRefsDec( pTemp );
+            if ( Ivy_ObjRefs(pTemp) == 0 )
+                Ivy_ObjDelete_rec( pTemp, 1 );
+        }
+
+clkUpd += clock() - clk;
+    }
+
+PRT( "Cut    ", clkCut );
+PRT( "Truth  ", clkTru );
+PRT( "DSD    ", clkDsd );
+PRT( "Update ", clkUpd );
+PRT( "TOTAL  ", clock() - clkStart );
+
+    Vec_IntFree( vTree  );
+    Vec_IntFree( vFront );
+    Vec_IntFree( vInside );
+    Vec_IntFree( vNodes );
+
+    if ( !Ivy_ManCheck(p) )
+    {
+        printf( "Ivy_ManSeqRewrite(): The check has failed.\n" );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the sequential cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront )
+{
+    static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    unsigned uTruth0, uTruth1;
+    Ivy_Obj_t * pNode;
+    int nLatches, Number;
+    // consider the case of a constant
+    if ( Node == 0 )
+        return ~((unsigned)0);
+    // try to find this node in the frontier
+    Number = Vec_IntFind( vFront, Node );
+    if ( Number >= 0 )
+        return uMasks[Number];
+    // get the node
+    pNode = Ivy_ManObj( p, Ivy_LeafId(Node) );
+    assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) );
+    // get the number of latches
+    nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode);
+    // expand the first fanin
+    uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront );
+    if ( Ivy_ObjFaninC0(pNode) )
+        uTruth0 = ~uTruth0;
+    // quit if this is the one fanin node
+    if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) )
+        return uTruth0;
+    assert( Ivy_ObjIsNode(pNode) );
+    // expand the second fanin
+    uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront );
+    if ( Ivy_ObjFaninC1(pNode) )
+        uTruth1 = ~uTruth1;
+    // return the truth table
+    return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the truth table of the sequential cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront )
+{
+    assert( Ivy_ObjIsNode(pNode) );
+    return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively dereferences the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone )
+{
+    Ivy_Obj_t * pFan;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( !Ivy_ObjIsNone(pNode) );
+    if ( Ivy_ObjIsPi(pNode) )
+        return;
+    // deref the first fanin
+    pFan = Ivy_ObjFanin0(pNode);
+    Ivy_ObjRefsDec( pFan );
+    if ( Ivy_ObjRefs( pFan ) == 0 )
+        Ivy_ManSeqDeref_rec( pFan, vCone );
+    // deref the second fanin
+    pFan = Ivy_ObjFanin1(pNode);
+    Ivy_ObjRefsDec( pFan );
+    if ( Ivy_ObjRefs( pFan ) == 0 )
+        Ivy_ManSeqDeref_rec( pFan, vCone );
+    // save the node
+    Vec_IntPush( vCone, pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively references the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pFan;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( !Ivy_ObjIsNone(pNode) );
+    if ( Ivy_ObjIsPi(pNode) )
+        return;
+    // ref the first fanin
+    pFan = Ivy_ObjFanin0(pNode);
+    if ( Ivy_ObjRefs( pFan ) == 0 )
+        Ivy_ManSeqRef_rec( pFan );
+    Ivy_ObjRefsInc( pFan );
+    // ref the second fanin
+    pFan = Ivy_ObjFanin1(pNode);
+    if ( Ivy_ObjRefs( pFan ) == 0 )
+        Ivy_ManSeqRef_rec( pFan );
+    Ivy_ObjRefsInc( pFan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone )
+{
+    Vec_IntClear( vCone );
+    Ivy_ManSeqDeref_rec( pNode, vCone );
+    Ivy_ManSeqRef_rec( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cost of the logic cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone )
+{
+    Ivy_Obj_t * pObj;
+    int i, Cost = 0;
+    Ivy_ManForEachNodeVec( p, vCone, pObj, i )
+    {
+        if ( Ivy_ObjIsAnd(pObj) )
+            Cost += 1;
+        else if ( Ivy_ObjIsExor(pObj) )
+            Cost += 2;
+    }
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c
new file mode 100644
index 00000000..d8fbdd9b
--- /dev/null
+++ b/src/temp/ivy/ivySeq.c
@@ -0,0 +1,101 @@
+/**CFile****************************************************************
+
+  FileName    [ivySeq.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: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a combinational AIG manager into a sequential one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches )
+{
+    Vec_Int_t * vNodes;
+    Ivy_Obj_t * pObj, * pObjNew, * pFan0, * pFan1;
+    int i, fChanges;
+    assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) );
+    // change POs into buffers
+    assert( Ivy_ManPoNum(p) == Vec_IntSize(p->vPos) );
+    for ( i = Ivy_ManPoNum(p) - nLatches; i < Vec_IntSize(p->vPos); i++ )
+    {
+        pObj = Ivy_ManPo(p, i);
+        pObj->Type = IVY_BUF;
+    }
+    // change PIs into latches and connect them to the corresponding POs
+    assert( Ivy_ManPiNum(p) == Vec_IntSize(p->vPis) );
+    for ( i = Ivy_ManPiNum(p) - nLatches; i < Vec_IntSize(p->vPis); i++ )
+    {
+        pObj = Ivy_ManPi(p, i);
+        pObj->Type = IVY_LATCH;
+        Ivy_ObjConnect( pObj, Ivy_ManPo(p, Ivy_ManPoNum(p) - Ivy_ManPiNum(p)) );
+    }
+    // shrink the array
+    Vec_IntShrink( p->vPis, Ivy_ManPiNum(p) - nLatches );
+    Vec_IntShrink( p->vPos, Ivy_ManPoNum(p) - nLatches );
+    // update the counters of different objects
+    p->nObjs[IVY_PI] -= nLatches;
+    p->nObjs[IVY_PO] -= nLatches;
+    p->nObjs[IVY_BUF] += nLatches;
+    p->nObjs[IVY_LATCH] += nLatches;
+    // perform structural hashing while there are changes
+    fChanges = 1;
+    while ( fChanges )
+    {
+        fChanges = 0;
+        vNodes = Ivy_ManDfs( p );
+        Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+        {
+            if ( Ivy_ObjIsBuf(pObj) )
+                continue;
+            pFan0 = Ivy_NodeRealFanin_rec( pObj, 0 );
+            pFan1 = Ivy_NodeRealFanin_rec( pObj, 1 );
+            if ( Ivy_ObjIsAnd(pObj) )
+                pObjNew = Ivy_And(pFan0, pFan1);
+            else if ( Ivy_ObjIsExor(pObj) )
+                pObjNew = Ivy_Exor(pFan0, pFan1);
+            else assert( 0 );
+            if ( pObjNew == pObj )
+                continue;
+            Ivy_ObjReplace( pObj, pObjNew, 1, 1 );
+            fChanges = 1;
+        }
+        Vec_IntFree( vNodes );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c
new file mode 100644
index 00000000..815caa29
--- /dev/null
+++ b/src/temp/ivy/ivyTable.c
@@ -0,0 +1,237 @@
+/**CFile****************************************************************
+
+  FileName    [ivyTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Structural hashing table.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// hashing the node
+static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize ) 
+{
+    unsigned Key = Ivy_ObjIsExor(pObj) * 1699;
+    Key ^= Ivy_ObjFaninId0(pObj) * 7937;
+    Key ^= Ivy_ObjFaninId1(pObj) * 2971;
+    Key ^= Ivy_ObjFaninC0(pObj) * 911;
+    Key ^= Ivy_ObjFaninC1(pObj) * 353;
+    Key ^= Ivy_ObjInit(pObj) * 911;
+    return Key % TableSize;
+}
+
+// returns the place where this node is stored (or should be stored)
+static int * Ivy_TableFind( Ivy_Obj_t * pObj )
+{
+    Ivy_Man_t * p;
+    int i;
+    assert( Ivy_ObjIsHash(pObj) );
+    p = Ivy_ObjMan(pObj);
+    for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
+        if ( p->pTable[i] == pObj->Id )
+            break;
+    return p->pTable + i;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if node with the given attributes is in the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj )
+{
+    Ivy_Man_t * p;
+    Ivy_Obj_t * pEntry;
+    int i;
+    assert( !Ivy_IsComplement(pObj) );
+    if ( !Ivy_ObjIsHash(pObj) )
+        return NULL;
+    assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
+    assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) );
+    p = Ivy_ObjMan(pObj);
+    for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
+    {
+        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
+        if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && 
+             Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && 
+             Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && 
+             Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && 
+             Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && 
+             Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) )
+            return Ivy_ObjObj( pObj, p->pTable[i] );
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the node to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TableInsert( Ivy_Obj_t * pObj )
+{
+    int * pPlace;
+    assert( !Ivy_IsComplement(pObj) );
+    if ( !Ivy_ObjIsHash(pObj) )
+        return;
+    pPlace = Ivy_TableFind( pObj );
+    assert( *pPlace == 0 );
+    *pPlace = pObj->Id;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TableDelete( Ivy_Obj_t * pObj )
+{
+    Ivy_Man_t * p;
+    Ivy_Obj_t * pEntry;
+    int i, * pPlace;
+    assert( !Ivy_IsComplement(pObj) );
+    if ( !Ivy_ObjIsHash(pObj) )
+        return;
+    pPlace = Ivy_TableFind( pObj );
+    assert( *pPlace == pObj->Id ); // node should be in the table
+    *pPlace = 0;
+    // rehash the adjacent entries
+    p = Ivy_ObjMan(pObj);
+    i = pPlace - p->pTable;
+    for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
+    {
+        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
+        p->pTable[i] = 0;
+        Ivy_TableInsert( pEntry );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the table to point to the new node.]
+
+  Description [If the old node (pObj) is in the table, updates the table
+  to point to an object with different ID (ObjIdNew). The table should
+  not contain an object with ObjIdNew (this is currently not checked).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew )
+{
+    int * pPlace;
+    assert( !Ivy_IsComplement(pObj) );
+    if ( !Ivy_ObjIsHash(pObj) )
+        return;
+    pPlace = Ivy_TableFind( pObj );
+    assert( *pPlace == pObj->Id ); // node should be in the table
+    *pPlace = ObjIdNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of nodes in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_TableCountEntries( Ivy_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+        Counter += (p->pTable[i] != 0);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description [Typically this procedure should not be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TableResize( Ivy_Man_t * p )
+{
+    int * pTableOld, * pPlace;
+    int nTableSizeOld, Counter, e, clk;
+    assert( 0 );
+clk = clock();
+    // save the old table
+    pTableOld = p->pTable;
+    nTableSizeOld = p->nTableSize;
+    // get the new table
+    p->nTableSize = p->nObjsAlloc*5/2+13; 
+    p->pTable = ALLOC( int, p->nTableSize );
+    memset( p->pTable, 0, sizeof(int) * p->nTableSize );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( e = 0; e < nTableSizeOld; e++ )
+    {
+        if ( pTableOld[e] == 0 )
+            continue;
+        Counter++;
+        // get the place where this entry goes in the table table
+        pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) );
+        assert( *pPlace == 0 ); // should not be in the table
+        *pPlace = pTableOld[e];
+    }
+    assert( Counter == Ivy_ManHashObjNum(p) );
+//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( p->pTable );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyUndo.c b/src/temp/ivy/ivyUndo.c
new file mode 100644
index 00000000..6612bf42
--- /dev/null
+++ b/src/temp/ivy/ivyUndo.c
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+  FileName    [ivyUndo.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Recording the results of recent deletion of logic cone.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManUndoStart( Ivy_Man_t * p )
+{
+    p->fRecording = 1;
+    p->nUndos = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManUndoStop( Ivy_Man_t * p )
+{
+    p->fRecording = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj )
+{
+    Ivy_Obj_t * pObjUndo;
+    if ( p->nUndos >= p->nUndosAlloc )
+    {
+        printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" );
+        return;
+    }
+    pObjUndo = p->pUndos + p->nUndos++;
+    // required data for Ivy_ObjCreateGhost()
+    pObjUndo->Type    = pObj->Type;
+    pObjUndo->Init    = pObj->Init;
+    pObjUndo->Fanin0  = pObj->Fanin0;
+    pObjUndo->Fanin1  = pObj->Fanin1;
+    pObjUndo->fComp0  = pObj->fComp0;
+    pObjUndo->fComp1  = pObj->fComp1;
+    // additional data
+    pObjUndo->Id      = pObj->Id;
+    pObjUndo->nRefs   = pObj->nRefs;
+    pObjUndo->Level   = pObj->Level;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Vec_IntPutLast( Vec_Int_t * vFree, int Last )
+{
+    int Place, i;
+    // find the entry
+    Place = Vec_IntFind( vFree, Last );
+    if ( Place == -1 )
+        return 0;
+    // shift entries by one
+    assert( vFree->pArray[Place] == Last );
+    for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ )
+        vFree->pArray[i] = vFree->pArray[i+1];
+    // put the entry in the end
+    vFree->pArray[i] = Last;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot )
+{
+    Ivy_Obj_t * pObjUndo, * pObjNew;
+    int i;
+    assert( p->nUndos > 0 );
+    assert( p->fRecording == 0 );
+    for ( i = p->nUndos - 1; i >= 0; i-- )
+    {
+        // get the undo object
+        pObjUndo = p->pUndos + i;
+        // if this is the last object
+        if ( i == 0 )
+            Vec_IntPush( p->vFree, pRoot->Id );
+        else
+            Vec_IntPutLast( p->vFree, pObjUndo->Id );
+        // create the new object
+        pObjNew  = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) );
+        pObjNew->nRefs = pObjUndo->nRefs;
+        pObjNew->Level = pObjUndo->Level;
+        // make sure the object is created in the same place as before
+        assert( pObjNew->Id == pObjUndo->Id );
+    }
+    p->nUndos = 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
new file mode 100644
index 00000000..590affd7
--- /dev/null
+++ b/src/temp/ivy/ivyUtil.c
@@ -0,0 +1,369 @@
+/**CFile****************************************************************
+
+  FileName    [ivyUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Various procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the current traversal ID of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManIncrementTravId( Ivy_Man_t * p )
+{
+    if ( p->nTravIds >= (1<<30)-1 - 1000 )
+        Ivy_ManCleanTravId( p );
+    p->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the DFS ordering of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCleanTravId( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    p->nTravIds = 1;
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->TravId = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pNode0, * pNode1;
+    // check that the node is regular
+    assert( !Ivy_IsComplement(pNode) );
+    // if the node is not AND, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode) )
+        return 0;
+    // if the children are not complemented, this is not MUX
+    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
+        return 0;
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // if the children are not ANDs, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
+        return 0;
+    // otherwise the node is MUX iff it has a pair of equal grandchildren
+    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
+           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
+
+  Description [If the node is a MUX, returns the control variable C.
+  Assigns nodes T and E to be the then and else variables of the MUX. 
+  Node C is never complemented. Nodes T and E can be complemented.
+  This function also recognizes EXOR/NEXOR gates as MUXes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
+{
+    Ivy_Obj_t * pNode0, * pNode1;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( Ivy_ObjIsMuxType(pNode) );
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // find the control variable
+//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
+    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
+        }
+    }
+//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
+        }
+    }
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
+    }
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
+    }
+    assert( 0 ); // this is not MUX
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
+{
+    if ( pNode->fMarkA )
+        return;
+    pNode->fMarkA = 1;
+    assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) );
+    Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes );
+    Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes );
+    Vec_IntPush( vNodes, pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description [Does not modify the array of leaves. Uses array vTruth to store 
+  temporary truth tables. The returned pointer should be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+{
+    int i, Leaf;
+    // collect and mark the leaves
+    Vec_IntClear( vNodes );
+    Vec_IntForEachEntry( vLeaves, Leaf, i )
+    {
+        Vec_IntPush( vNodes, Leaf );
+        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1;
+    }
+    // collect and mark the nodes
+    Ivy_ManCollectCut_rec( pRoot, vNodes );
+    // clean the nodes
+    Vec_IntForEachEntry( vNodes, Leaf, i )
+        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the pointer to the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
+{
+   return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    int i;
+    pTruth  = Ivy_ObjGetTruthStore( pNode->TravId, vTruth );
+    pTruth0 = Ivy_ObjGetTruthStore( Ivy_ObjFanin0(pNode)->TravId, vTruth );
+    pTruth1 = Ivy_ObjGetTruthStore( Ivy_ObjFanin1(pNode)->TravId, vTruth );
+    if ( Ivy_ObjIsExor(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] ^ pTruth1[i];
+    else if ( !Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Ivy_ObjFaninC0(pNode) && !Ivy_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Ivy_ObjFaninC0(pNode) && Ivy_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description [Does not modify the array of leaves. Uses array vTruth to store 
+  temporary truth tables. The returned pointer should be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
+{
+    static unsigned uTruths[8][8] = { // elementary truth tables
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
+    };
+    int i, Leaf;
+    // collect the cut
+    Ivy_ManCollectCut( pRoot, vLeaves, vNodes );
+    // set the node numbers
+    Vec_IntForEachEntry( vNodes, Leaf, i )
+        Ivy_ObjObj(pRoot, Leaf)->TravId = i;
+    // alloc enough memory
+    Vec_IntClear( vTruth );
+    Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
+    // set the elementary truth tables
+    Vec_IntForEachEntry( vLeaves, Leaf, i )
+        memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
+    // compute truths for other nodes
+    Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
+        Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 );
+    return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect the latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
+{
+    Vec_Int_t * vLatches;
+    Ivy_Obj_t * pObj;
+    int i;
+    vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
+    Ivy_ManForEachLatch( p, pObj, i )
+        Vec_IntPush( vLatches, pObj->Id );
+    return vLatches;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivy_.c b/src/temp/ivy/ivy_.c
new file mode 100644
index 00000000..65689689
--- /dev/null
+++ b/src/temp/ivy/ivy_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [ivy_.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: ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
new file mode 100644
index 00000000..d59a3fa3
--- /dev/null
+++ b/src/temp/ivy/module.make
@@ -0,0 +1,14 @@
+SRC +=    src/temp/ivy/ivyBalance.c \
+    src/temp/ivy/ivyCanon.c \
+    src/temp/ivy/ivyCheck.c \
+    src/temp/ivy/ivyCut.c \
+    src/temp/ivy/ivyDfs.c \
+    src/temp/ivy/ivyDsd.c \
+    src/temp/ivy/ivyMan.c \
+    src/temp/ivy/ivyObj.c \
+    src/temp/ivy/ivyOper.c \
+    src/temp/ivy/ivyRewrite.c \
+    src/temp/ivy/ivySeq.c \
+    src/temp/ivy/ivyTable.c \
+    src/temp/ivy/ivyUndo.c \
+    src/temp/ivy/ivyUtil.c
author	Alan Mishchenko <alanmi@berkeley.edu>	2006-06-11 08:01:00 -0700
committer	Alan Mishchenko <alanmi@berkeley.edu>	2006-06-11 08:01:00 -0700
commit	3db1557f45b03875a0a0b8adddcc15c4565895d2 (patch)
tree	2896d20ddcb85ae4aa7245ca28bc585f567fea54 /src/temp/ivy
parent	7d0921330b1f4e789901b4c2450920e7c412f95f (diff)
download	abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.gz abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.bz2 abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.zip