Version abc80130

14 files changed, 0 insertions, 3498 deletions

diff --git a/src/aig/hop/cudd2.c b/src/aig/hop/cudd2.c
deleted file mode 100644
index 28d13ce0..00000000
--- a/src/aig/hop/cudd2.c
+++ /dev/null
@@ -1,355 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cudd2.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Recording AIGs for the BDD operations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - October 3, 2006.]
-
-  Revision    [$Id: cudd2.c,v 1.00 2006/10/03 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-#include "st.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Aig_CuddMan_t_        Aig_CuddMan_t;
-struct Aig_CuddMan_t_
-{
-    Aig_Man_t *  pAig;   // internal AIG package
-    st_table *   pTable; // hash table mapping BDD nodes into AIG nodes
-};
-
-// static Cudd AIG manager used in this experiment
-static Aig_CuddMan_t * s_pCuddMan = NULL;
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start AIG recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
-{
-    int v;
-    // start the BDD-to-AIG manager when the first BDD manager is allocated
-    if ( s_pCuddMan != NULL )
-        return;
-    s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
-    s_pCuddMan->pAig = Aig_ManStart();
-    s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
-    for ( v = 0; v < (int)numVars; v++ )
-        Aig_ObjCreatePi( s_pCuddMan->pAig );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops AIG recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_Quit( void * pCudd )
-{
-    assert( s_pCuddMan != NULL );
-    Aig_ManDumpBlif( s_pCuddMan->pAig, "aig_temp.blif" );
-    Aig_ManStop( s_pCuddMan->pAig );
-    st_free_table( s_pCuddMan->pTable );
-    free( s_pCuddMan );
-    s_pCuddMan = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fetches AIG node corresponding to the BDD node from the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Aig_Obj_t * Cudd2_GetArg( void * pArg )
-{
-    Aig_Obj_t * pNode;
-    assert( s_pCuddMan != NULL );
-    if ( !st_lookup( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), (char **)&pNode ) )
-    {
-        printf( "Cudd2_GetArg(): An argument BDD is not in the hash table.\n" );
-        return NULL;
-    }
-    return Aig_NotCond( pNode, Aig_IsComplement(pArg) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the AIG node corresponding to the BDD node into the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
-{
-    assert( s_pCuddMan != NULL );
-    if ( st_is_member( s_pCuddMan->pTable, (char *)Aig_Regular(pResult) ) )
-        return;
-    pNode = Aig_NotCond( pNode,  Aig_IsComplement(pResult) );
-    st_insert( s_pCuddMan->pTable, (char *)Aig_Regular(pResult), (char *)pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Registers constant 1 node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddOne( void * pCudd, void * pResult )
-{
-    Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds elementary variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddIthVar( void * pCudd, int iVar, void * pResult )
-{
-    int v;
-    assert( s_pCuddMan != NULL );
-    for ( v = Aig_ManPiNum(s_pCuddMan->pAig); v <= iVar; v++ )
-        Aig_ObjCreatePi( s_pCuddMan->pAig );
-    Cudd2_SetArg( Aig_ManPi(s_pCuddMan->pAig, iVar), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddAnd( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, pNode1 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddOr( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddNand( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, pArg0, pArg1, Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddNor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddAnd( pCudd, Aig_Not(pArg0), Aig_Not(pArg1), pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddXor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddXnor( void * pCudd, void * pArg0, void * pArg1, void * pResult )
-{
-    Cudd2_bddXor( pCudd, pArg0, pArg1, Aig_Not(pResult) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddIte( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode2, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode2 = Cudd2_GetArg( pArg2 );
-    pNode  = Aig_Mux( s_pCuddMan->pAig, pNode0, pNode1, pNode2 );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BDD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Compose( s_pCuddMan->pAig, pNode0, pNode1, v );
-    Cudd2_SetArg( pNode, pResult );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Should be called after each containment check.]
-
-  Description [Result should be 1 if Cudd2_bddLeq returned 1.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddLeq( void * pCudd, void * pArg0, void * pArg1, int Result )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_And( s_pCuddMan->pAig, pNode0, Aig_Not(pNode1) );
-    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Should be called after each equality check.]
-
-  Description [Result should be 1 if they are equal.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_bddEqual( void * pCudd, void * pArg0, void * pArg1, int Result )
-{
-    Aig_Obj_t * pNode0, * pNode1, * pNode;
-    pNode0 = Cudd2_GetArg( pArg0 );
-    pNode1 = Cudd2_GetArg( pArg1 );
-    pNode  = Aig_Exor( s_pCuddMan->pAig, pNode0, pNode1 );
-    Aig_ObjCreatePo( s_pCuddMan->pAig, pNode );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/cudd2.h b/src/aig/hop/cudd2.h
deleted file mode 100644
index 69711c11..00000000
--- a/src/aig/hop/cudd2.h
+++ /dev/null
@@ -1,82 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cudd2.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - October 3, 2006.]
-
-  Revision    [$Id: cudd2.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __CUDD2_H__
-#define __CUDD2_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
-// HA: Added for printing messages
-#ifndef MSG 
-#define MSG(msg) (printf("%s = \n",(msg)));
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////
-///                             ITERATORS                            ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-extern void Cudd2_Init      ( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd );
-extern void Cudd2_Quit      ( void * pCudd );
-extern void Cudd2_bddOne    ( void * pCudd, void * pResult );
-extern void Cudd2_bddIthVar ( void * pCudd, int iVar, void * pResult );
-extern void Cudd2_bddAnd    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddOr     ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddNand   ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddNor    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddXor    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddXnor   ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
-extern void Cudd2_bddIte    ( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult );
-extern void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult );
-extern void Cudd2_bddLeq    ( void * pCudd, void * pArg0, void * pArg1, int Result );
-extern void Cudd2_bddEqual  ( void * pCudd, void * pArg0, void * pArg1, int Result );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
deleted file mode 100644
index af1d9cd3..00000000
--- a/src/aig/hop/hop.h
+++ /dev/null
@@ -1,347 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hop.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hop.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __HOP_H__
-#define __HOP_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-
-#include "vec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Hop_Man_t_            Hop_Man_t;
-typedef struct Hop_Obj_t_            Hop_Obj_t;
-typedef int                          Hop_Edge_t;
-
-// object types
-typedef enum { 
-    AIG_NONE,                        // 0: non-existent object
-    AIG_CONST1,                      // 1: constant 1 
-    AIG_PI,                          // 2: primary input
-    AIG_PO,                          // 3: primary output
-    AIG_AND,                         // 4: AND node
-    AIG_EXOR,                        // 5: EXOR node
-    AIG_VOID                         // 6: unused object
-} Hop_Type_t;
-
-// the AIG node
-struct Hop_Obj_t_  // 6 words
-{
-    void *           pData;          // misc
-    Hop_Obj_t *      pNext;          // strashing table
-    Hop_Obj_t *      pFanin0;        // fanin
-    Hop_Obj_t *      pFanin1;        // fanin
-    unsigned int     Type    :  3;   // object type
-    unsigned int     fPhase  :  1;   // value under 000...0 pattern
-    unsigned int     fMarkA  :  1;   // multipurpose mask
-    unsigned int     fMarkB  :  1;   // multipurpose mask
-    unsigned int     nRefs   : 26;   // reference count (level)
-    int              Id;             // unique ID of the node
-};
-
-// the AIG manager
-struct Hop_Man_t_
-{
-    // AIG nodes
-    Vec_Ptr_t *      vPis;           // the array of PIs
-    Vec_Ptr_t *      vPos;           // the array of POs
-    Vec_Ptr_t *      vObjs;          // the array of all nodes (optional)
-    Hop_Obj_t *      pConst1;        // the constant 1 node
-    Hop_Obj_t        Ghost;          // the ghost node
-    // AIG node counters
-    int              nObjs[AIG_VOID];// the number of objects by type
-    int              nCreated;       // the number of created objects
-    int              nDeleted;       // the number of deleted objects
-    // stuctural hash table
-    Hop_Obj_t **     pTable;         // structural hash table
-    int              nTableSize;     // structural hash table size
-    // various data members
-    void *           pData;          // the temporary data
-    int              nTravIds;       // the current traversal ID
-    int              fRefCount;      // enables reference counting
-    int              fCatchExor;     // enables EXOR nodes
-    // memory management
-    Vec_Ptr_t *      vChunks;        // allocated memory pieces
-    Vec_Ptr_t *      vPages;         // memory pages used by nodes
-    Hop_Obj_t *      pListFree;      // the list of free nodes 
-    // timing statistics
-    int              time1;
-    int              time2;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
-#define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
-
-#ifndef PRT
-#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-#endif
-
-static inline int          Hop_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);           }
-static inline int          Hop_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }
-static inline int          Hop_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
-static inline void         Hop_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
-static inline void         Hop_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
-static inline int          Hop_Base2Log( unsigned n )             { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
-static inline int          Hop_Base10Log( unsigned n )            { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
-
-static inline Hop_Obj_t *  Hop_Regular( Hop_Obj_t * p )           { return (Hop_Obj_t *)((unsigned long)(p) & ~01); }
-static inline Hop_Obj_t *  Hop_Not( Hop_Obj_t * p )               { return (Hop_Obj_t *)((unsigned long)(p) ^  01); }
-static inline Hop_Obj_t *  Hop_NotCond( Hop_Obj_t * p, int c )    { return (Hop_Obj_t *)((unsigned long)(p) ^ (c)); }
-static inline int          Hop_IsComplement( Hop_Obj_t * p )      { return (int)((unsigned long)(p) & 01);          }
-
-static inline Hop_Obj_t *  Hop_ManConst0( Hop_Man_t * p )         { return Hop_Not(p->pConst1);                     }
-static inline Hop_Obj_t *  Hop_ManConst1( Hop_Man_t * p )         { return p->pConst1;                              }
-static inline Hop_Obj_t *  Hop_ManGhost( Hop_Man_t * p )          { return &p->Ghost;                               }
-static inline Hop_Obj_t *  Hop_ManPi( Hop_Man_t * p, int i )      { return (Hop_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
-static inline Hop_Obj_t *  Hop_ManPo( Hop_Man_t * p, int i )      { return (Hop_Obj_t *)Vec_PtrEntry(p->vPos, i);   }
-static inline Hop_Obj_t *  Hop_ManObj( Hop_Man_t * p, int i )     { return p->vObjs ? (Hop_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL;  }
-
-static inline Hop_Edge_t   Hop_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;             }
-static inline int          Hop_EdgeId( Hop_Edge_t Edge )                   { return Edge >> 1;                      }
-static inline int          Hop_EdgeIsComplement( Hop_Edge_t Edge )         { return Edge & 1;                       }
-static inline Hop_Edge_t   Hop_EdgeRegular( Hop_Edge_t Edge )              { return (Edge >> 1) << 1;               }
-static inline Hop_Edge_t   Hop_EdgeNot( Hop_Edge_t Edge )                  { return Edge ^ 1;                       }
-static inline Hop_Edge_t   Hop_EdgeNotCond( Hop_Edge_t Edge, int fCond )   { return Edge ^ fCond;                   }
-
-static inline int          Hop_ManPiNum( Hop_Man_t * p )          { return p->nObjs[AIG_PI];                    }
-static inline int          Hop_ManPoNum( Hop_Man_t * p )          { return p->nObjs[AIG_PO];                    }
-static inline int          Hop_ManAndNum( Hop_Man_t * p )         { return p->nObjs[AIG_AND];                   }
-static inline int          Hop_ManExorNum( Hop_Man_t * p )        { return p->nObjs[AIG_EXOR];                  }
-static inline int          Hop_ManNodeNum( Hop_Man_t * p )        { return p->nObjs[AIG_AND]+p->nObjs[AIG_EXOR];}
-static inline int          Hop_ManGetCost( Hop_Man_t * p )        { return p->nObjs[AIG_AND]+3*p->nObjs[AIG_EXOR]; }
-static inline int          Hop_ManObjNum( Hop_Man_t * p )         { return p->nCreated - p->nDeleted;           }
-
-static inline Hop_Type_t   Hop_ObjType( Hop_Obj_t * pObj )        { return (Hop_Type_t)pObj->Type;               }
-static inline int          Hop_ObjIsNone( Hop_Obj_t * pObj )      { return pObj->Type == AIG_NONE;   }
-static inline int          Hop_ObjIsConst1( Hop_Obj_t * pObj )    { assert(!Hop_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }
-static inline int          Hop_ObjIsPi( Hop_Obj_t * pObj )        { return pObj->Type == AIG_PI;     }
-static inline int          Hop_ObjIsPo( Hop_Obj_t * pObj )        { return pObj->Type == AIG_PO;     }
-static inline int          Hop_ObjIsAnd( Hop_Obj_t * pObj )       { return pObj->Type == AIG_AND;    }
-static inline int          Hop_ObjIsExor( Hop_Obj_t * pObj )      { return pObj->Type == AIG_EXOR;   }
-static inline int          Hop_ObjIsNode( Hop_Obj_t * pObj )      { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }
-static inline int          Hop_ObjIsTerm( Hop_Obj_t * pObj )      { return pObj->Type == AIG_PI  || pObj->Type == AIG_PO || pObj->Type == AIG_CONST1; }
-static inline int          Hop_ObjIsHash( Hop_Obj_t * pObj )      { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }
-
-static inline int          Hop_ObjIsMarkA( Hop_Obj_t * pObj )     { return pObj->fMarkA;  }
-static inline void         Hop_ObjSetMarkA( Hop_Obj_t * pObj )    { pObj->fMarkA = 1;     }
-static inline void         Hop_ObjClearMarkA( Hop_Obj_t * pObj )  { pObj->fMarkA = 0;     }
- 
-static inline void         Hop_ObjSetTravId( Hop_Obj_t * pObj, int TravId )                { pObj->pData = (void *)TravId;                       }
-static inline void         Hop_ObjSetTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )      { pObj->pData = (void *)p->nTravIds;                  }
-static inline void         Hop_ObjSetTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )     { pObj->pData = (void *)(p->nTravIds - 1);            }
-static inline int          Hop_ObjIsTravIdCurrent( Hop_Man_t * p, Hop_Obj_t * pObj )       { return (int )((int)pObj->pData == p->nTravIds);     }
-static inline int          Hop_ObjIsTravIdPrevious( Hop_Man_t * p, Hop_Obj_t * pObj )      { return (int )((int)pObj->pData == p->nTravIds - 1); }
-
-static inline int          Hop_ObjTravId( Hop_Obj_t * pObj )      { return (int)pObj->pData;                       }
-static inline int          Hop_ObjPhase( Hop_Obj_t * pObj )       { return pObj->fPhase;                           }
-static inline int          Hop_ObjRefs( Hop_Obj_t * pObj )        { return pObj->nRefs;                            }
-static inline void         Hop_ObjRef( Hop_Obj_t * pObj )         { pObj->nRefs++;                                 }
-static inline void         Hop_ObjDeref( Hop_Obj_t * pObj )       { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
-static inline void         Hop_ObjClearRef( Hop_Obj_t * pObj )    { pObj->nRefs = 0;                               }
-static inline int          Hop_ObjFaninC0( Hop_Obj_t * pObj )     { return Hop_IsComplement(pObj->pFanin0);        }
-static inline int          Hop_ObjFaninC1( Hop_Obj_t * pObj )     { return Hop_IsComplement(pObj->pFanin1);        }
-static inline Hop_Obj_t *  Hop_ObjFanin0( Hop_Obj_t * pObj )      { return Hop_Regular(pObj->pFanin0);             }
-static inline Hop_Obj_t *  Hop_ObjFanin1( Hop_Obj_t * pObj )      { return Hop_Regular(pObj->pFanin1);             }
-static inline Hop_Obj_t *  Hop_ObjChild0( Hop_Obj_t * pObj )      { return pObj->pFanin0;                          }
-static inline Hop_Obj_t *  Hop_ObjChild1( Hop_Obj_t * pObj )      { return pObj->pFanin1;                          }
-static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin0(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin0(pObj)->pData, Hop_ObjFaninC0(pObj)) : NULL;  }
-static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
-static inline int          Hop_ObjLevel( Hop_Obj_t * pObj )       { return pObj->nRefs;                            }
-static inline int          Hop_ObjLevelNew( Hop_Obj_t * pObj )    { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }
-static inline int          Hop_ObjFaninPhase( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
-static inline void         Hop_ObjClean( Hop_Obj_t * pObj )       { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
-static inline int          Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )    
-{ 
-    if ( Hop_ObjFanin0(pObj) == pFanin ) return 0; 
-    if ( Hop_ObjFanin1(pObj) == pFanin ) return 1; 
-    assert(0); return -1; 
-}
-static inline int          Hop_ObjFanoutC( Hop_Obj_t * pObj, Hop_Obj_t * pFanout )    
-{ 
-    if ( Hop_ObjFanin0(pFanout) == pObj ) return Hop_ObjFaninC0(pObj); 
-    if ( Hop_ObjFanin1(pFanout) == pObj ) return Hop_ObjFaninC1(pObj); 
-    assert(0); return -1; 
-}
-
-// create the ghost of the new node
-static inline Hop_Obj_t *  Hop_ObjCreateGhost( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type )    
-{
-    Hop_Obj_t * pGhost;
-    assert( Type != AIG_AND || !Hop_ObjIsConst1(Hop_Regular(p0)) );
-    assert( p1 == NULL || !Hop_ObjIsConst1(Hop_Regular(p1)) );
-    assert( Type == AIG_PI || Hop_Regular(p0) != Hop_Regular(p1) );
-    pGhost = Hop_ManGhost(p);
-    pGhost->Type = Type;
-    if ( Hop_Regular(p0)->Id < Hop_Regular(p1)->Id )
-    {
-        pGhost->pFanin0 = p0;
-        pGhost->pFanin1 = p1;
-    }
-    else
-    {
-        pGhost->pFanin0 = p1;
-        pGhost->pFanin1 = p0;
-    }
-    return pGhost;
-}
-
-// internal memory manager
-static inline Hop_Obj_t * Hop_ManFetchMemory( Hop_Man_t * p )  
-{ 
-    extern void Hop_ManAddMemory( Hop_Man_t * p );
-    Hop_Obj_t * pTemp;
-    if ( p->pListFree == NULL )
-        Hop_ManAddMemory( p );
-    pTemp = p->pListFree;
-    p->pListFree = *((Hop_Obj_t **)pTemp);
-    memset( pTemp, 0, sizeof(Hop_Obj_t) ); 
-    if ( p->vObjs )
-    {
-        assert( p->nCreated == Vec_PtrSize(p->vObjs) );
-        Vec_PtrPush( p->vObjs, pTemp );
-    }
-    pTemp->Id = p->nCreated++;
-    return pTemp;
-}
-static inline void Hop_ManRecycleMemory( Hop_Man_t * p, Hop_Obj_t * pEntry )
-{
-    pEntry->Type = AIG_NONE; // distinquishes dead node from live node
-    *((Hop_Obj_t **)pEntry) = p->pListFree;
-    p->pListFree = pEntry;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                             ITERATORS                            ///
-////////////////////////////////////////////////////////////////////////
-
-// iterator over the primary inputs
-#define Hop_ManForEachPi( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPis, pObj, i )
-// iterator over the primary outputs
-#define Hop_ManForEachPo( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPos, pObj, i )
-// iterator over all objects, including those currently not used
-#define Hop_ManForEachNode( p, pObj, i )                                        \
-    for ( i = 0; i < p->nTableSize; i++ )                                       \
-        if ( ((pObj) = p->pTable[i]) == NULL ) {} else
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== hopBalance.c ========================================================*/
-extern Hop_Man_t *     Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel );
-extern Hop_Obj_t *     Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel );
-/*=== hopCheck.c ========================================================*/
-extern int             Hop_ManCheck( Hop_Man_t * p );
-/*=== hopDfs.c ==========================================================*/
-extern Vec_Ptr_t *     Hop_ManDfs( Hop_Man_t * p );
-extern Vec_Ptr_t *     Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode );
-extern int             Hop_ManCountLevels( Hop_Man_t * p );
-extern void            Hop_ManCreateRefs( Hop_Man_t * p );
-extern int             Hop_DagSize( Hop_Obj_t * pObj );
-extern void            Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
-extern Hop_Obj_t *     Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
-extern Hop_Obj_t *     Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
-/*=== hopMan.c ==========================================================*/
-extern Hop_Man_t *     Hop_ManStart();
-extern Hop_Man_t *     Hop_ManDup( Hop_Man_t * p );
-extern void            Hop_ManStop( Hop_Man_t * p );
-extern int             Hop_ManCleanup( Hop_Man_t * p );
-extern void            Hop_ManPrintStats( Hop_Man_t * p );
-/*=== hopMem.c ==========================================================*/
-extern void            Hop_ManStartMemory( Hop_Man_t * p );
-extern void            Hop_ManStopMemory( Hop_Man_t * p );
-/*=== hopObj.c ==========================================================*/
-extern Hop_Obj_t *     Hop_ObjCreatePi( Hop_Man_t * p );
-extern Hop_Obj_t *     Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver );
-extern Hop_Obj_t *     Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost );
-extern void            Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj_t * pFan1 );
-extern void            Hop_ObjDisconnect( Hop_Man_t * p, Hop_Obj_t * pObj );
-extern void            Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
-extern void            Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj );
-extern Hop_Obj_t *     Hop_ObjRepr( Hop_Obj_t * pObj );
-extern void            Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew );
-/*=== hopOper.c =========================================================*/
-extern Hop_Obj_t *     Hop_IthVar( Hop_Man_t * p, int i );
-extern Hop_Obj_t *     Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type );
-extern Hop_Obj_t *     Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 );
-extern Hop_Obj_t *     Hop_Or( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 );
-extern Hop_Obj_t *     Hop_Exor( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 );
-extern Hop_Obj_t *     Hop_Mux( Hop_Man_t * p, Hop_Obj_t * pC, Hop_Obj_t * p1, Hop_Obj_t * p0 );
-extern Hop_Obj_t *     Hop_Maj( Hop_Man_t * p, Hop_Obj_t * pA, Hop_Obj_t * pB, Hop_Obj_t * pC );
-extern Hop_Obj_t *     Hop_Miter( Hop_Man_t * p, Vec_Ptr_t * vPairs );
-extern Hop_Obj_t *     Hop_CreateAnd( Hop_Man_t * p, int nVars );
-extern Hop_Obj_t *     Hop_CreateOr( Hop_Man_t * p, int nVars );
-extern Hop_Obj_t *     Hop_CreateExor( Hop_Man_t * p, int nVars );
-/*=== hopTable.c ========================================================*/
-extern Hop_Obj_t *     Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost );
-extern void            Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj );
-extern void            Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj );
-extern int             Hop_TableCountEntries( Hop_Man_t * p );
-extern void            Hop_TableProfile( Hop_Man_t * p );
-/*=== hopUtil.c =========================================================*/
-extern void            Hop_ManIncrementTravId( Hop_Man_t * p );
-extern void            Hop_ManCleanData( Hop_Man_t * p );
-extern void            Hop_ObjCleanData_rec( Hop_Obj_t * pObj );
-extern void            Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSuper );
-extern int             Hop_ObjIsMuxType( Hop_Obj_t * pObj );
-extern int             Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
-extern Hop_Obj_t *     Hop_ObjRecognizeMux( Hop_Obj_t * pObj, Hop_Obj_t ** ppObjT, Hop_Obj_t ** ppObjE );
-extern void            Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
-extern void            Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
-extern void            Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig );
-extern void            Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig );
-extern void            Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/hop/hopBalance.c b/src/aig/hop/hopBalance.c
deleted file mode 100644
index 73c90685..00000000
--- a/src/aig/hop/hopBalance.c
+++ /dev/null
@@ -1,391 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopBalance.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Algebraic AIG balancing.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
-static Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
-static int         Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
-static void        Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs algebraic balancing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel )
-{
-    Hop_Man_t * pNew;
-    Hop_Obj_t * pObj, * pObjNew;
-    Vec_Vec_t * vStore;
-    int i;
-    // create the new manager 
-    pNew = Hop_ManStart();
-    pNew->fRefCount = 0;
-    // map the PI nodes
-    Hop_ManCleanData( p );
-    Hop_ManConst1(p)->pData = Hop_ManConst1(pNew);
-    Hop_ManForEachPi( p, pObj, i )
-        pObj->pData = Hop_ObjCreatePi(pNew);
-    // balance the AIG
-    vStore = Vec_VecAlloc( 50 );
-    Hop_ManForEachPo( p, pObj, i )
-    {
-        pObjNew = Hop_NodeBalance_rec( pNew, Hop_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
-        Hop_ObjCreatePo( pNew, Hop_NotCond( pObjNew, Hop_ObjFaninC0(pObj) ) );
-    }
-    Vec_VecFree( vStore );
-    // remove dangling nodes
-//    Hop_ManCreateRefs( pNew );
-//    if ( i = Hop_ManCleanup( pNew ) )
-//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
-    // check the resulting AIG
-    if ( !Hop_ManCheck(pNew) )
-        printf( "Hop_ManBalance(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the new node constructed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_NodeBalance_rec( Hop_Man_t * pNew, Hop_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
-{
-    Hop_Obj_t * pObjNew;
-    Vec_Ptr_t * vSuper;
-    int i;
-    assert( !Hop_IsComplement(pObjOld) );
-    // return if the result is known
-    if ( pObjOld->pData )
-        return pObjOld->pData;
-    assert( Hop_ObjIsNode(pObjOld) );
-    // get the implication supergate
-    vSuper = Hop_NodeBalanceCone( pObjOld, vStore, Level );
-    // check if supergate contains two nodes in the opposite polarity
-    if ( vSuper->nSize == 0 )
-        return pObjOld->pData = Hop_ManConst0(pNew);
-    if ( Vec_PtrSize(vSuper) < 2 )
-        printf( "BUG!\n" );
-    // for each old node, derive the new well-balanced node
-    for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
-    {
-        pObjNew = Hop_NodeBalance_rec( pNew, Hop_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
-        vSuper->pArray[i] = Hop_NotCond( pObjNew, Hop_IsComplement(vSuper->pArray[i]) );
-    }
-    // build the supergate
-    pObjNew = Hop_NodeBalanceBuildSuper( pNew, vSuper, Hop_ObjType(pObjOld), fUpdateLevel );
-    // make sure the balanced node is not assigned
-//    assert( pObjOld->Level >= Hop_Regular(pObjNew)->Level );
-    assert( pObjOld->pData == NULL );
-    return pObjOld->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_NodeBalanceCone_rec( Hop_Obj_t * pRoot, Hop_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    int RetValue1, RetValue2, i;
-    // check if the node is visited
-    if ( Hop_Regular(pObj)->fMarkB )
-    {
-        // check if the node occurs in the same polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == pObj )
-                return 1;
-        // check if the node is present in the opposite polarity
-        for ( i = 0; i < vSuper->nSize; i++ )
-            if ( vSuper->pArray[i] == Hop_Not(pObj) )
-                return -1;
-        assert( 0 );
-        return 0;
-    }
-    // if the new node is complemented or a PI, another gate begins
-    if ( pObj != pRoot && (Hop_IsComplement(pObj) || Hop_ObjType(pObj) != Hop_ObjType(pRoot) || Hop_ObjRefs(pObj) > 1) )
-    {
-        Vec_PtrPush( vSuper, pObj );
-        Hop_Regular(pObj)->fMarkB = 1;
-        return 0;
-    }
-    assert( !Hop_IsComplement(pObj) );
-    assert( Hop_ObjIsNode(pObj) );
-    // go through the branches
-    RetValue1 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild0(pObj), vSuper );
-    RetValue2 = Hop_NodeBalanceCone_rec( pRoot, Hop_ObjChild1(pObj), vSuper );
-    if ( RetValue1 == -1 || RetValue2 == -1 )
-        return -1;
-    // return 1 if at least one branch has a duplicate
-    return RetValue1 || RetValue2;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Hop_NodeBalanceCone( Hop_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
-{
-    Vec_Ptr_t * vNodes;
-    int RetValue, i;
-    assert( !Hop_IsComplement(pObj) );
-    // extend the storage
-    if ( Vec_VecSize( vStore ) <= Level )
-        Vec_VecPush( vStore, Level, 0 );
-    // get the temporary array of nodes
-    vNodes = Vec_VecEntry( vStore, Level );
-    Vec_PtrClear( vNodes );
-    // collect the nodes in the implication supergate
-    RetValue = Hop_NodeBalanceCone_rec( pObj, pObj, vNodes );
-    assert( vNodes->nSize > 1 );
-    // unmark the visited nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Hop_Regular(pObj)->fMarkB = 0;
-    // if we found the node and its complement in the same implication supergate, 
-    // return empty set of nodes (meaning that we should use constant-0 node)
-    if ( RetValue == -1 )
-        vNodes->nSize = 0;
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_NodeCompareLevelsDecrease( Hop_Obj_t ** pp1, Hop_Obj_t ** pp2 )
-{
-    int Diff = Hop_ObjLevel(Hop_Regular(*pp1)) - Hop_ObjLevel(Hop_Regular(*pp2));
-    if ( Diff > 0 )
-        return -1;
-    if ( Diff < 0 ) 
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Builds implication supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel )
-{
-    Hop_Obj_t * pObj1, * pObj2;
-    int LeftBound;
-    assert( vSuper->nSize > 1 );
-    // sort the new nodes by level in the decreasing order
-    Vec_PtrSort( vSuper, Hop_NodeCompareLevelsDecrease );
-    // balance the nodes
-    while ( vSuper->nSize > 1 )
-    {
-        // find the left bound on the node to be paired
-        LeftBound = (!fUpdateLevel)? 0 : Hop_NodeBalanceFindLeft( vSuper );
-        // find the node that can be shared (if no such node, randomize choice)
-        Hop_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR );
-        // pull out the last two nodes
-        pObj1 = Vec_PtrPop(vSuper);
-        pObj2 = Vec_PtrPop(vSuper);
-        Hop_NodeBalancePushUniqueOrderByLevel( vSuper, Hop_Oper(p, pObj1, pObj2, Type) );
-    }
-    return Vec_PtrEntry(vSuper, 0);
-}
-
-/**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 Hop_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
-{
-    Hop_Obj_t * pObjRight, * pObjLeft;
-    int Current;
-    // if two or less nodes, pair with the first
-    if ( Vec_PtrSize(vSuper) < 3 )
-        return 0;
-    // set the pointer to the one before the last
-    Current = Vec_PtrSize(vSuper) - 2;
-    pObjRight = Vec_PtrEntry( vSuper, Current );
-    // go through the nodes to the left of this one
-    for ( Current--; Current >= 0; Current-- )
-    {
-        // get the next node on the left
-        pObjLeft = Vec_PtrEntry( vSuper, Current );
-        // if the level of this node is different, quit the loop
-        if ( Hop_ObjLevel(Hop_Regular(pObjLeft)) != Hop_ObjLevel(Hop_Regular(pObjRight)) )
-            break;
-    }
-    Current++;    
-    // get the node, for which the equality holds
-    pObjLeft = Vec_PtrEntry( vSuper, Current );
-    assert( Hop_ObjLevel(Hop_Regular(pObjLeft)) == Hop_ObjLevel(Hop_Regular(pObjRight)) );
-    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 Hop_NodeBalancePermute( Hop_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
-{
-    Hop_Obj_t * pObj1, * pObj2, * pObj3, * 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
-    pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
-    pObj2 = Vec_PtrEntry( vSuper, RightBound     );
-    if ( Hop_Regular(pObj1) == p->pConst1 || Hop_Regular(pObj2) == p->pConst1 )
-        return;
-    // find the first node that can be shared
-    for ( i = RightBound; i >= LeftBound; i-- )
-    {
-        pObj3 = Vec_PtrEntry( vSuper, i );
-        if ( Hop_Regular(pObj3) == p->pConst1 )
-        {
-            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
-            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
-            return;
-        }
-        pGhost = Hop_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_EXOR : AIG_AND );
-        if ( Hop_TableLookup( p, pGhost ) )
-        {
-            if ( pObj3 == pObj2 )
-                return;
-            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
-            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
-            return;
-        }
-    }
-/*
-    // we did not find the node to share, randomize choice
-    {
-        int Choice = rand() % (RightBound - LeftBound + 1);
-        pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
-        if ( pObj3 == pObj2 )
-            return;
-        Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
-        Vec_PtrWriteEntry( vSuper, RightBound,         pObj3 );
-    }
-*/
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts a new node in the order by levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Hop_Obj_t * pObj )
-{
-    Hop_Obj_t * pObj1, * pObj2;
-    int i;
-    if ( Vec_PtrPushUnique(vStore, pObj) )
-        return;
-    // find the p of the node
-    for ( i = vStore->nSize-1; i > 0; i-- )
-    {
-        pObj1 = vStore->pArray[i  ];
-        pObj2 = vStore->pArray[i-1];
-        if ( Hop_ObjLevel(Hop_Regular(pObj1)) <= Hop_ObjLevel(Hop_Regular(pObj2)) )
-            break;
-        vStore->pArray[i  ] = pObj2;
-        vStore->pArray[i-1] = pObj1;
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopCheck.c b/src/aig/hop/hopCheck.c
deleted file mode 100644
index 9120906f..00000000
--- a/src/aig/hop/hopCheck.c
+++ /dev/null
@@ -1,110 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopCheck.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [AIG checking procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the consistency of the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ManCheck( Hop_Man_t * p )
-{
-    Hop_Obj_t * pObj, * pObj2;
-    int i;
-    // check primary inputs
-    Hop_ManForEachPi( p, pObj, i )
-    {
-        if ( Hop_ObjFanin0(pObj) || Hop_ObjFanin1(pObj) )
-        {
-            printf( "Hop_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
-            return 0;
-        }
-    }
-    // check primary outputs
-    Hop_ManForEachPo( p, pObj, i )
-    {
-        if ( !Hop_ObjFanin0(pObj) )
-        {
-            printf( "Hop_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
-            return 0;
-        }
-        if ( Hop_ObjFanin1(pObj) )
-        {
-            printf( "Hop_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
-            return 0;
-        }
-    }
-    // check internal nodes
-    Hop_ManForEachNode( p, pObj, i )
-    {
-        if ( !Hop_ObjFanin0(pObj) || !Hop_ObjFanin1(pObj) )
-        {
-            printf( "Hop_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
-            return 0;
-        }
-        if ( Hop_ObjFanin0(pObj)->Id >= Hop_ObjFanin1(pObj)->Id )
-        {
-            printf( "Hop_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
-            return 0;
-        }
-        pObj2 = Hop_TableLookup( p, pObj );
-        if ( pObj2 != pObj )
-        {
-            printf( "Hop_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
-            return 0;
-        }
-    }
-    // count the total number of nodes
-    if ( Hop_ManObjNum(p) != 1 + Hop_ManPiNum(p) + Hop_ManPoNum(p) + Hop_ManAndNum(p) + Hop_ManExorNum(p) )
-    {
-        printf( "Hop_ManCheck: The number of created nodes is wrong.\n" );
-        return 0;
-    }
-    // count the number of nodes in the table
-    if ( Hop_TableCountEntries(p) != Hop_ManAndNum(p) + Hop_ManExorNum(p) )
-    {
-        printf( "Hop_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
-        return 0;
-    }
-//    if ( !Hop_ManIsAcyclic(p) )
-//        return 0;
-    return 1; 
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c
deleted file mode 100644
index 49e5f221..00000000
--- a/src/aig/hop/hopDfs.c
+++ /dev/null
@@ -1,399 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopDfs.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [DFS traversal procedures.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManDfs_rec( Hop_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return;
-    Hop_ManDfs_rec( Hop_ObjFanin0(pObj), vNodes );
-    Hop_ManDfs_rec( Hop_ObjFanin1(pObj), vNodes );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA(pObj);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Hop_Obj_t * pObj;
-    int i;
-    vNodes = Vec_PtrAlloc( Hop_ManNodeNum(p) );
-    Hop_ManForEachNode( p, pObj, i )
-        Hop_ManDfs_rec( pObj, vNodes );
-    Hop_ManForEachNode( p, pObj, i )
-        Hop_ObjClearMarkA(pObj);
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode )
-{
-    Vec_Ptr_t * vNodes;
-    Hop_Obj_t * pObj;
-    int i;
-    assert( !Hop_IsComplement(pNode) );
-    vNodes = Vec_PtrAlloc( 16 );
-    Hop_ManDfs_rec( pNode, vNodes );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Hop_ObjClearMarkA(pObj);
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the max number of levels in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ManCountLevels( Hop_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Hop_Obj_t * pObj;
-    int i, LevelsMax, Level0, Level1;
-    // initialize the levels
-    Hop_ManConst1(p)->pData = NULL;
-    Hop_ManForEachPi( p, pObj, i )
-        pObj->pData = NULL;
-    // compute levels in a DFS order
-    vNodes = Hop_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        Level0 = (int)Hop_ObjFanin0(pObj)->pData;
-        Level1 = (int)Hop_ObjFanin1(pObj)->pData;
-        pObj->pData = (void *)(1 + Hop_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
-    }
-    Vec_PtrFree( vNodes );
-    // get levels of the POs
-    LevelsMax = 0;
-    Hop_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, (int)Hop_ObjFanin0(pObj)->pData );
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates correct reference counters at each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManCreateRefs( Hop_Man_t * p )
-{
-    Hop_Obj_t * pObj;
-    int i;
-    if ( p->fRefCount )
-        return;
-    p->fRefCount = 1;
-    // clear refs
-    Hop_ObjClearRef( Hop_ManConst1(p) );
-    Hop_ManForEachPi( p, pObj, i )
-        Hop_ObjClearRef( pObj );
-    Hop_ManForEachNode( p, pObj, i )
-        Hop_ObjClearRef( pObj );
-    Hop_ManForEachPo( p, pObj, i )
-        Hop_ObjClearRef( pObj );
-    // set refs
-    Hop_ManForEachNode( p, pObj, i )
-    {
-        Hop_ObjRef( Hop_ObjFanin0(pObj) );
-        Hop_ObjRef( Hop_ObjFanin1(pObj) );
-    }
-    Hop_ManForEachPo( p, pObj, i )
-        Hop_ObjRef( Hop_ObjFanin0(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ConeMark_rec( Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return;
-    Hop_ConeMark_rec( Hop_ObjFanin0(pObj) );
-    Hop_ConeMark_rec( Hop_ObjFanin1(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ConeCleanAndMark_rec( Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return;
-    Hop_ConeCleanAndMark_rec( Hop_ObjFanin0(pObj) );
-    Hop_ConeCleanAndMark_rec( Hop_ObjFanin1(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-    pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ConeCountAndMark_rec( Hop_Obj_t * pObj )
-{
-    int Counter;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return 0;
-    Counter = 1 + Hop_ConeCountAndMark_rec( Hop_ObjFanin0(pObj) ) + 
-        Hop_ConeCountAndMark_rec( Hop_ObjFanin1(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ConeUnmark_rec( Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || !Hop_ObjIsMarkA(pObj) )
-        return;
-    Hop_ConeUnmark_rec( Hop_ObjFanin0(pObj) ); 
-    Hop_ConeUnmark_rec( Hop_ObjFanin1(pObj) );
-    assert( Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjClearMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_DagSize( Hop_Obj_t * pObj )
-{
-    int Counter;
-    Counter = Hop_ConeCountAndMark_rec( Hop_Regular(pObj) );
-    Hop_ConeUnmark_rec( Hop_Regular(pObj) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_Transfer_rec( Hop_Man_t * pDest, Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
-        return;
-    Hop_Transfer_rec( pDest, Hop_ObjFanin0(pObj) ); 
-    Hop_Transfer_rec( pDest, Hop_ObjFanin1(pObj) );
-    pObj->pData = Hop_And( pDest, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pRoot, int nVars )
-{
-    Hop_Obj_t * pObj;
-    int i;
-    // solve simple cases
-    if ( pSour == pDest )
-        return pRoot;
-    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
-        return Hop_NotCond( Hop_ManConst1(pDest), Hop_IsComplement(pRoot) );
-    // set the PI mapping
-    Hop_ManForEachPi( pSour, pObj, i )
-    {
-        if ( i == nVars )
-           break;
-        pObj->pData = Hop_IthVar(pDest, i);
-    }
-    // transfer and set markings
-    Hop_Transfer_rec( pDest, Hop_Regular(pRoot) );
-    // clear the markings
-    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
-    return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_Compose_rec( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFunc, Hop_Obj_t * pVar )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( Hop_ObjIsMarkA(pObj) )
-        return;
-    if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
-    {
-        pObj->pData = pObj == pVar ? pFunc : pObj;
-        return;
-    }
-    Hop_Compose_rec( p, Hop_ObjFanin0(pObj), pFunc, pVar ); 
-    Hop_Compose_rec( p, Hop_ObjFanin1(pObj), pFunc, pVar );
-    pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
-    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
-    Hop_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar )
-{
-    // quit if the PI variable is not defined
-    if ( iVar >= Hop_ManPiNum(p) )
-    {
-        printf( "Hop_Compose(): The PI variable %d is not defined.\n", iVar );
-        return NULL;
-    }
-    // recursively perform composition
-    Hop_Compose_rec( p, Hop_Regular(pRoot), pFunc, Hop_ManPi(p, iVar) );
-    // clear the markings
-    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
-    return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopMan.c b/src/aig/hop/hopMan.c
deleted file mode 100644
index 99f5d316..00000000
--- a/src/aig/hop/hopMan.c
+++ /dev/null
@@ -1,164 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [AIG manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Man_t * Hop_ManStart()
-{
-    Hop_Man_t * p;
-    // start the manager
-    p = ALLOC( Hop_Man_t, 1 );
-    memset( p, 0, sizeof(Hop_Man_t) );
-    // perform initializations
-    p->nTravIds = 1;
-    p->fRefCount = 1;
-    p->fCatchExor = 0;
-    // allocate arrays for nodes
-    p->vPis = Vec_PtrAlloc( 100 );
-    p->vPos = Vec_PtrAlloc( 100 );
-    // prepare the internal memory manager
-    Hop_ManStartMemory( p );
-    // create the constant node
-    p->pConst1 = Hop_ManFetchMemory( p );
-    p->pConst1->Type = AIG_CONST1;
-    p->pConst1->fPhase = 1;
-    p->nCreated = 1;
-    // start the table
-//    p->nTableSize = 107;
-    p->nTableSize = 10007;
-    p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManStop( Hop_Man_t * p )
-{
-    Hop_Obj_t * pObj;
-    int i;
-    // make sure the nodes have clean marks
-    pObj = Hop_ManConst1(p);
-    assert( !pObj->fMarkA && !pObj->fMarkB );
-    Hop_ManForEachPi( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    Hop_ManForEachPo( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    Hop_ManForEachNode( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    // print time
-    if ( p->time1 ) { PRT( "time1", p->time1 ); }
-    if ( p->time2 ) { PRT( "time2", p->time2 ); }
-//    Hop_TableProfile( p );
-    if ( p->vChunks )  Hop_ManStopMemory( p );
-    if ( p->vPis )     Vec_PtrFree( p->vPis );
-    if ( p->vPos )     Vec_PtrFree( p->vPos );
-    if ( p->vObjs )    Vec_PtrFree( p->vObjs );
-    free( p->pTable );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ManCleanup( Hop_Man_t * p )
-{
-    Vec_Ptr_t * vObjs;
-    Hop_Obj_t * pNode;
-    int i, nNodesOld;
-    assert( p->fRefCount );
-    nNodesOld = Hop_ManNodeNum(p);
-    // collect roots of dangling nodes
-    vObjs = Vec_PtrAlloc( 100 );
-    Hop_ManForEachNode( p, pNode, i )
-        if ( Hop_ObjRefs(pNode) == 0 )
-            Vec_PtrPush( vObjs, pNode );
-    // recursively remove dangling nodes
-    Vec_PtrForEachEntry( vObjs, pNode, i )
-        Hop_ObjDelete_rec( p, pNode );
-    Vec_PtrFree( vObjs );
-    return nNodesOld - Hop_ManNodeNum(p);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManPrintStats( Hop_Man_t * p )
-{
-    printf( "PI/PO = %d/%d. ", Hop_ManPiNum(p), Hop_ManPoNum(p) );
-    printf( "A = %7d. ",       Hop_ManAndNum(p) );
-    printf( "X = %5d. ",       Hop_ManExorNum(p) );
-    printf( "Cre = %7d. ",     p->nCreated );
-    printf( "Del = %7d. ",     p->nDeleted );
-    printf( "Lev = %3d. ",     Hop_ManCountLevels(p) );
-    printf( "\n" );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopMem.c b/src/aig/hop/hopMem.c
deleted file mode 100644
index 0665470a..00000000
--- a/src/aig/hop/hopMem.c
+++ /dev/null
@@ -1,115 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopMem.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Memory management for the AIG nodes.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// memory management
-#define IVY_PAGE_SIZE      12        // page size containing 2^IVY_PAGE_SIZE nodes
-#define IVY_PAGE_MASK    4095        // page bitmask (2^IVY_PAGE_SIZE)-1
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the internal memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManStartMemory( Hop_Man_t * p )
-{
-    p->vChunks = Vec_PtrAlloc( 128 );
-    p->vPages = Vec_PtrAlloc( 128 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the internal memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManStopMemory( Hop_Man_t * p )
-{
-    void * pMemory;
-    int i;
-    Vec_PtrForEachEntry( p->vChunks, pMemory, i )
-        free( pMemory );
-    Vec_PtrFree( p->vChunks );
-    Vec_PtrFree( p->vPages );
-    p->pListFree = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates additional memory for the nodes.]
-
-  Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. 
-  Records the pointer to the AIG manager in the -1 entry.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManAddMemory( Hop_Man_t * p )
-{
-    char * pMemory;
-    int i, nBytes;
-    assert( sizeof(Hop_Obj_t) <= 64 );
-    assert( p->pListFree == NULL );
-//    assert( (Hop_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
-    // allocate new memory page
-    nBytes = sizeof(Hop_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
-    pMemory = ALLOC( char, nBytes );
-    Vec_PtrPush( p->vChunks, pMemory );
-    // align memory at the 32-byte boundary
-    pMemory = pMemory + 64 - (((int)pMemory) & 63);
-    // remember the manager in the first entry
-    Vec_PtrPush( p->vPages, pMemory );
-    // break the memory down into nodes
-    p->pListFree = (Hop_Obj_t *)pMemory;
-    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
-    {
-        *((char **)pMemory) = pMemory + sizeof(Hop_Obj_t);
-        pMemory += sizeof(Hop_Obj_t);
-    }
-    *((char **)pMemory) = NULL;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c
deleted file mode 100644
index c8e70dd3..00000000
--- a/src/aig/hop/hopObj.c
+++ /dev/null
@@ -1,271 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopObj.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Adding/removing objects.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates primary input.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p )
-{
-    Hop_Obj_t * pObj;
-    pObj = Hop_ManFetchMemory( p );
-    pObj->Type = AIG_PI;
-    Vec_PtrPush( p->vPis, pObj );
-    p->nObjs[AIG_PI]++;
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates primary output with the given driver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
-{
-    Hop_Obj_t * pObj;
-    pObj = Hop_ManFetchMemory( p );
-    pObj->Type = AIG_PO;
-    Vec_PtrPush( p->vPos, pObj );
-    // add connections
-    pObj->pFanin0 = pDriver;
-    if ( p->fRefCount )
-        Hop_ObjRef( Hop_Regular(pDriver) );
-    else
-        pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
-    // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pDriver);
-    // update node counters of the manager
-    p->nObjs[AIG_PO]++;
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create the new node assuming it does not exist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost )
-{
-    Hop_Obj_t * pObj;
-    assert( !Hop_IsComplement(pGhost) );
-    assert( Hop_ObjIsNode(pGhost) );
-    assert( pGhost == &p->Ghost );
-    // get memory for the new object
-    pObj = Hop_ManFetchMemory( p );
-    pObj->Type = pGhost->Type;
-    // add connections
-    Hop_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
-    // update node counters of the manager
-    p->nObjs[Hop_ObjType(pObj)]++;
-    assert( pObj->pData == NULL );
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connect the object to the fanin.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj_t * pFan1 )
-{
-    assert( !Hop_IsComplement(pObj) );
-    assert( Hop_ObjIsNode(pObj) );
-    // add the first fanin
-    pObj->pFanin0 = pFan0;
-    pObj->pFanin1 = pFan1;
-    // increment references of the fanins and add their fanouts
-    if ( p->fRefCount )
-    {
-        if ( pFan0 != NULL )
-            Hop_ObjRef( Hop_ObjFanin0(pObj) );
-        if ( pFan1 != NULL )
-            Hop_ObjRef( Hop_ObjFanin1(pObj) );
-    }
-    else
-        pObj->nRefs = Hop_ObjLevelNew( pObj );
-    // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
-    // add the node to the structural hash table
-    Hop_TableInsert( p, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connect the object to the fanin.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjDisconnect( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    assert( Hop_ObjIsNode(pObj) );
-    // remove connections
-    if ( pObj->pFanin0 != NULL )
-        Hop_ObjDeref(Hop_ObjFanin0(pObj));
-    if ( pObj->pFanin1 != NULL )
-        Hop_ObjDeref(Hop_ObjFanin1(pObj));
-    // remove the node from the structural hash table
-    Hop_TableDelete( p, pObj );
-    // add the first fanin
-    pObj->pFanin0 = NULL;
-    pObj->pFanin1 = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    assert( !Hop_ObjIsTerm(pObj) );
-    assert( Hop_ObjRefs(pObj) == 0 );
-    // update node counters of the manager
-    p->nObjs[pObj->Type]--;
-    p->nDeleted++;
-    // remove connections
-    Hop_ObjDisconnect( p, pObj );
-    // remove PIs/POs from the arrays
-    if ( Hop_ObjIsPi(pObj) )
-        Vec_PtrRemove( p->vPis, pObj );
-    // free the node
-    Hop_ManRecycleMemory( p, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the MFFC of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    Hop_Obj_t * pFanin0, * pFanin1;
-    assert( !Hop_IsComplement(pObj) );
-    if ( Hop_ObjIsConst1(pObj) || Hop_ObjIsPi(pObj) )
-        return;
-    assert( Hop_ObjIsNode(pObj) );
-    pFanin0 = Hop_ObjFanin0(pObj);
-    pFanin1 = Hop_ObjFanin1(pObj);
-    Hop_ObjDelete( p, pObj );
-    if ( pFanin0 && !Hop_ObjIsNone(pFanin0) && Hop_ObjRefs(pFanin0) == 0 )
-        Hop_ObjDelete_rec( p, pFanin0 );
-    if ( pFanin1 && !Hop_ObjIsNone(pFanin1) && Hop_ObjRefs(pFanin1) == 0 )
-        Hop_ObjDelete_rec( p, pFanin1 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the representative of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    if ( pObj->pData == NULL || pObj->pData == pObj )
-        return pObj;
-    return Hop_ObjRepr( pObj->pData );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets an equivalence relation between the nodes.]
-
-  Description [Makes the representative of pNew point to the representaive of pOld.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew )
-{
-    Hop_Obj_t * pOldRepr;
-    Hop_Obj_t * pNewRepr;
-    assert( pOld != NULL && pNew != NULL );
-    pOldRepr = Hop_ObjRepr(pOld);
-    pNewRepr = Hop_ObjRepr(pNew);
-    if ( pNewRepr != pOldRepr )
-        pNewRepr->pData = pOldRepr;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopOper.c b/src/aig/hop/hopOper.c
deleted file mode 100644
index a31ca0f2..00000000
--- a/src/aig/hop/hopOper.c
+++ /dev/null
@@ -1,373 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopOper.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [AIG operations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: hopOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// procedure to detect an EXOR gate
-static inline int Hop_ObjIsExorType( Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 )
-{
-    if ( !Hop_IsComplement(p0) || !Hop_IsComplement(p1) )
-        return 0;
-    p0 = Hop_Regular(p0);
-    p1 = Hop_Regular(p1);
-    if ( !Hop_ObjIsAnd(p0) || !Hop_ObjIsAnd(p1) )
-        return 0;
-    if ( Hop_ObjFanin0(p0) != Hop_ObjFanin0(p1) || Hop_ObjFanin1(p0) != Hop_ObjFanin1(p1) )
-        return 0;
-    if ( Hop_ObjFaninC0(p0) == Hop_ObjFaninC0(p1) || Hop_ObjFaninC1(p0) == Hop_ObjFaninC1(p1) )
-        return 0;
-    *ppFan0 = Hop_ObjChild0(p0);
-    *ppFan1 = Hop_ObjChild1(p0);
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns i-th elementary variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i )
-{
-    int v;
-    for ( v = Hop_ManPiNum(p); v <= i; v++ )
-        Hop_ObjCreatePi( p );
-    assert( i < Vec_PtrSize(p->vPis) );
-    return Hop_ManPi( p, i );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform one operation.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type )
-{
-    if ( Type == AIG_AND )
-        return Hop_And( p, p0, p1 );
-    if ( Type == AIG_EXOR )
-        return Hop_Exor( p, p0, p1 );
-    assert( 0 );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 )
-{
-    Hop_Obj_t * pGhost, * pResult;
-//    Hop_Obj_t * pFan0, * pFan1;
-    // check trivial cases
-    if ( p0 == p1 )
-        return p0;
-    if ( p0 == Hop_Not(p1) )
-        return Hop_Not(p->pConst1);
-    if ( Hop_Regular(p0) == p->pConst1 )
-        return p0 == p->pConst1 ? p1 : Hop_Not(p->pConst1);
-    if ( Hop_Regular(p1) == p->pConst1 )
-        return p1 == p->pConst1 ? p0 : Hop_Not(p->pConst1);
-    // check if it can be an EXOR gate
-//    if ( Hop_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
-//        return Hop_Exor( p, pFan0, pFan1 );
-    // check the table
-    pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_AND );
-    if ( pResult = Hop_TableLookup( p, pGhost ) )
-        return pResult;
-    return Hop_ObjCreate( p, pGhost );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Exor( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 )
-{
-/*
-    Hop_Obj_t * pGhost, * pResult;
-    // check trivial cases
-    if ( p0 == p1 )
-        return Hop_Not(p->pConst1);
-    if ( p0 == Hop_Not(p1) )
-        return p->pConst1;
-    if ( Hop_Regular(p0) == p->pConst1 )
-        return Hop_NotCond( p1, p0 == p->pConst1 );
-    if ( Hop_Regular(p1) == p->pConst1 )
-        return Hop_NotCond( p0, p1 == p->pConst1 );
-    // check the table
-    pGhost = Hop_ObjCreateGhost( p, p0, p1, AIG_EXOR );
-    if ( pResult = Hop_TableLookup( p, pGhost ) )
-        return pResult;
-    return Hop_ObjCreate( p, pGhost );
-*/
-    return Hop_Or( p, Hop_And(p, p0, Hop_Not(p1)), Hop_And(p, Hop_Not(p0), p1) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements Boolean OR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Or( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 )
-{
-    return Hop_Not( Hop_And( p, Hop_Not(p0), Hop_Not(p1) ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements ITE operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Mux( Hop_Man_t * p, Hop_Obj_t * pC, Hop_Obj_t * p1, Hop_Obj_t * p0 )
-{
-/*    
-    Hop_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
-    int Count0, Count1;
-    // consider trivial cases
-    if ( p0 == Hop_Not(p1) )
-        return Hop_Exor( p, pC, p0 );
-    // other cases can be added
-    // implement the first MUX (F = C * x1 + C' * x0)
-
-    // check for constants here!!!
-
-    pTempA1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC,          p1, AIG_AND) );
-    pTempA2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), p0, AIG_AND) );
-    if ( pTempA1 && pTempA2 )
-    {
-        pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempA1), Hop_Not(pTempA2), AIG_AND) );
-        if ( pTemp ) return Hop_Not(pTemp);
-    }
-    Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
-    // implement the second MUX (F' = C * x1' + C' * x0')
-    pTempB1 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, pC,          Hop_Not(p1), AIG_AND) );
-    pTempB2 = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pC), Hop_Not(p0), AIG_AND) );
-    if ( pTempB1 && pTempB2 )
-    {
-        pTemp = Hop_TableLookup( p, Hop_ObjCreateGhost(p, Hop_Not(pTempB1), Hop_Not(pTempB2), AIG_AND) );
-        if ( pTemp ) return pTemp;
-    }
-    Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
-    // compare and decide which one to implement
-    if ( Count0 >= Count1 )
-    {
-        pTempA1 = pTempA1? pTempA1 : Hop_And(p, pC,          p1);
-        pTempA2 = pTempA2? pTempA2 : Hop_And(p, Hop_Not(pC), p0);
-        return Hop_Or( p, pTempA1, pTempA2 );
-    }
-    pTempB1 = pTempB1? pTempB1 : Hop_And(p, pC,          Hop_Not(p1));
-    pTempB2 = pTempB2? pTempB2 : Hop_And(p, Hop_Not(pC), Hop_Not(p0));
-    return Hop_Not( Hop_Or( p, pTempB1, pTempB2 ) );
-*/
-    return Hop_Or( p, Hop_And(p, pC, p1), Hop_And(p, Hop_Not(pC), p0) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements ITE operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Maj( Hop_Man_t * p, Hop_Obj_t * pA, Hop_Obj_t * pB, Hop_Obj_t * pC )
-{
-    return Hop_Or( p, Hop_Or(p, Hop_And(p, pA, pB), Hop_And(p, pA, pC)), Hop_And(p, pB, pC) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Constructs the well-balanced tree of gates.]
-
-  Description [Disregards levels and possible logic sharing.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Multi_rec( Hop_Man_t * p, Hop_Obj_t ** ppObjs, int nObjs, Hop_Type_t Type )
-{
-    Hop_Obj_t * pObj1, * pObj2;
-    if ( nObjs == 1 )
-        return ppObjs[0];
-    pObj1 = Hop_Multi_rec( p, ppObjs,           nObjs/2,         Type );
-    pObj2 = Hop_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
-    return Hop_Oper( p, pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Multi( Hop_Man_t * p, Hop_Obj_t ** pArgs, int nArgs, Hop_Type_t Type )
-{
-    assert( Type == AIG_AND || Type == AIG_EXOR );
-    assert( nArgs > 0 );
-    return Hop_Multi_rec( p, pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_Miter( Hop_Man_t * p, Vec_Ptr_t * vPairs )
-{
-    int i;
-    assert( vPairs->nSize > 0 );
-    assert( vPairs->nSize % 2 == 0 );
-    // go through the cubes of the node's SOP
-    for ( i = 0; i < vPairs->nSize; i += 2 )
-        vPairs->pArray[i/2] = Hop_Not( Hop_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
-    vPairs->nSize = vPairs->nSize/2;
-    return Hop_Not( Hop_Multi_rec( p, (Hop_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_AND ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_CreateAnd( Hop_Man_t * p, int nVars )
-{
-    Hop_Obj_t * pFunc;
-    int i;
-    pFunc = Hop_ManConst1( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Hop_And( p, pFunc, Hop_IthVar(p, i) );
-    return pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_CreateOr( Hop_Man_t * p, int nVars )
-{
-    Hop_Obj_t * pFunc;
-    int i;
-    pFunc = Hop_ManConst0( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Hop_Or( p, pFunc, Hop_IthVar(p, i) );
-    return pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_CreateExor( Hop_Man_t * p, int nVars )
-{
-    Hop_Obj_t * pFunc;
-    int i;
-    pFunc = Hop_ManConst0( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Hop_Exor( p, pFunc, Hop_IthVar(p, i) );
-    return pFunc;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopTable.c b/src/aig/hop/hopTable.c
deleted file mode 100644
index 76390054..00000000
--- a/src/aig/hop/hopTable.c
+++ /dev/null
@@ -1,262 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopTable.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic And-Inverter Graph package.]
-
-  Synopsis    [Structural hashing table.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006. ]
-
-  Revision    [$Id: hopTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// hashing the node
-static unsigned long Hop_Hash( Hop_Obj_t * pObj, int TableSize ) 
-{
-    unsigned long Key = Hop_ObjIsExor(pObj) * 1699;
-    Key ^= Hop_ObjFanin0(pObj)->Id * 7937;
-    Key ^= Hop_ObjFanin1(pObj)->Id * 2971;
-    Key ^= Hop_ObjFaninC0(pObj) * 911;
-    Key ^= Hop_ObjFaninC1(pObj) * 353;
-    return Key % TableSize;
-}
-
-// returns the place where this node is stored (or should be stored)
-static Hop_Obj_t ** Hop_TableFind( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    Hop_Obj_t ** ppEntry;
-    assert( Hop_ObjChild0(pObj) && Hop_ObjChild1(pObj) );
-    assert( Hop_ObjFanin0(pObj)->Id < Hop_ObjFanin1(pObj)->Id );
-    for ( ppEntry = p->pTable + Hop_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
-        if ( *ppEntry == pObj )
-            return ppEntry;
-    assert( *ppEntry == NULL );
-    return ppEntry;
-}
-
-static void         Hop_TableResize( Hop_Man_t * p );
-static unsigned int Cudd_PrimeAig( unsigned int  p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
- 
-/**Function*************************************************************
-
-  Synopsis    [Checks if a node with the given attributes is in the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost )
-{
-    Hop_Obj_t * pEntry;
-    assert( !Hop_IsComplement(pGhost) );
-    assert( Hop_ObjChild0(pGhost) && Hop_ObjChild1(pGhost) );
-    assert( Hop_ObjFanin0(pGhost)->Id < Hop_ObjFanin1(pGhost)->Id );
-    if ( p->fRefCount && (!Hop_ObjRefs(Hop_ObjFanin0(pGhost)) || !Hop_ObjRefs(Hop_ObjFanin1(pGhost))) )
-        return NULL;
-    for ( pEntry = p->pTable[Hop_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
-    {
-        if ( Hop_ObjChild0(pEntry) == Hop_ObjChild0(pGhost) && 
-             Hop_ObjChild1(pEntry) == Hop_ObjChild1(pGhost) && 
-             Hop_ObjType(pEntry) == Hop_ObjType(pGhost) )
-            return pEntry;
-    }
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the new node to the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    Hop_Obj_t ** ppPlace;
-    assert( !Hop_IsComplement(pObj) );
-    assert( Hop_TableLookup(p, pObj) == NULL );
-    if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Hop_ManNodeNum(p) )
-        Hop_TableResize( p );
-    ppPlace = Hop_TableFind( p, pObj );
-    assert( *ppPlace == NULL );
-    *ppPlace = pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the node from the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj )
-{
-    Hop_Obj_t ** ppPlace;
-    assert( !Hop_IsComplement(pObj) );
-    ppPlace = Hop_TableFind( p, pObj );
-    assert( *ppPlace == pObj ); // node should be in the table
-    // remove the node
-    *ppPlace = pObj->pNext;
-    pObj->pNext = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of nodes in the table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_TableCountEntries( Hop_Man_t * p )
-{
-    Hop_Obj_t * pEntry;
-    int i, Counter = 0;
-    for ( i = 0; i < p->nTableSize; i++ )
-        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
-            Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the table.]
-
-  Description [Typically this procedure should not be called.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_TableResize( Hop_Man_t * p )
-{
-    Hop_Obj_t * pEntry, * pNext;
-    Hop_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, nEntries, i, clk;
-clk = clock();
-    // save the old table
-    pTableOld = p->pTable;
-    nTableSizeOld = p->nTableSize;
-    // get the new table
-    p->nTableSize = Cudd_PrimeAig( 2 * Hop_ManNodeNum(p) ); 
-    p->pTable = ALLOC( Hop_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Hop_Obj_t *) * p->nTableSize );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( i = 0; i < nTableSizeOld; i++ )
-    for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
-    {
-        // get the place where this entry goes in the table 
-        ppPlace = Hop_TableFind( p, pEntry );
-        assert( *ppPlace == NULL ); // should not be there
-        // add the entry to the list
-        *ppPlace = pEntry;
-        pEntry->pNext = NULL;
-        Counter++;
-    }
-    nEntries = Hop_ManNodeNum(p);
-    assert( Counter == nEntries );
-//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
-//    PRT( "Time", clock() - clk );
-    // replace the table and the parameters
-    free( pTableOld );
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Profiles the hash table.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void Hop_TableProfile( Hop_Man_t * p )
-{
-    Hop_Obj_t * pEntry;
-    int i, Counter;
-    for ( i = 0; i < p->nTableSize; i++ )
-    {
-        Counter = 0;
-        for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
-            Counter++;
-        if ( Counter ) 
-            printf( "%d ", Counter );
-    }
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime &gt;= p.]
-
-  Description [Copied from CUDD, for stand-aloneness.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-unsigned int Cudd_PrimeAig( unsigned int  p)
-{
-    int i,pn;
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
deleted file mode 100644
index 87fdb15e..00000000
--- a/src/aig/hop/hopUtil.c
+++ /dev/null
@@ -1,572 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [hopUtil.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: hopUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "hop.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Increments the current traversal ID of the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManIncrementTravId( Hop_Man_t * p )
-{
-    if ( p->nTravIds >= (1<<30)-1 )
-        Hop_ManCleanData( p );
-    p->nTravIds++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the data pointers for the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManCleanData( Hop_Man_t * p )
-{
-    Hop_Obj_t * pObj;
-    int i;
-    p->nTravIds = 1;
-    Hop_ManConst1(p)->pData = NULL;
-    Hop_ManForEachPi( p, pObj, i )
-        pObj->pData = NULL;
-    Hop_ManForEachPo( p, pObj, i )
-        pObj->pData = NULL;
-    Hop_ManForEachNode( p, pObj, i )
-        pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively cleans the data pointers in the cone of the node.]
-
-  Description [Applicable to small AIGs only because no caching is performed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjCleanData_rec( Hop_Obj_t * pObj )
-{
-    assert( !Hop_IsComplement(pObj) );
-    assert( !Hop_ObjIsPo(pObj) );
-    if ( Hop_ObjIsAnd(pObj) )
-    {
-        Hop_ObjCleanData_rec( Hop_ObjFanin0(pObj) );
-        Hop_ObjCleanData_rec( Hop_ObjFanin1(pObj) );
-    }
-    pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detects multi-input gate rooted at this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjCollectMulti_rec( Hop_Obj_t * pRoot, Hop_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    if ( pRoot != pObj && (Hop_IsComplement(pObj) || Hop_ObjIsPi(pObj) || Hop_ObjType(pRoot) != Hop_ObjType(pObj)) )
-    {
-        Vec_PtrPushUnique(vSuper, pObj);
-        return;
-    }
-    Hop_ObjCollectMulti_rec( pRoot, Hop_ObjChild0(pObj), vSuper );
-    Hop_ObjCollectMulti_rec( pRoot, Hop_ObjChild1(pObj), vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detects multi-input gate rooted at this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjCollectMulti( Hop_Obj_t * pRoot, Vec_Ptr_t * vSuper )
-{
-    assert( !Hop_IsComplement(pRoot) );
-    Vec_PtrClear( vSuper );
-    Hop_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ObjIsMuxType( Hop_Obj_t * pNode )
-{
-    Hop_Obj_t * pNode0, * pNode1;
-    // check that the node is regular
-    assert( !Hop_IsComplement(pNode) );
-    // if the node is not AND, this is not MUX
-    if ( !Hop_ObjIsAnd(pNode) )
-        return 0;
-    // if the children are not complemented, this is not MUX
-    if ( !Hop_ObjFaninC0(pNode) || !Hop_ObjFaninC1(pNode) )
-        return 0;
-    // get children
-    pNode0 = Hop_ObjFanin0(pNode);
-    pNode1 = Hop_ObjFanin1(pNode);
-    // if the children are not ANDs, this is not MUX
-    if ( !Hop_ObjIsAnd(pNode0) || !Hop_ObjIsAnd(pNode1) )
-        return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
-    return (Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1))) || 
-           (Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1))) ||
-           (Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1))) ||
-           (Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1)));
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recognizes what nodes are inputs of the EXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 )
-{
-    Hop_Obj_t * p0, * p1;
-    assert( !Hop_IsComplement(pObj) );
-    if ( !Hop_ObjIsNode(pObj) )
-        return 0;
-    if ( Hop_ObjIsExor(pObj) )
-    {
-        *ppFan0 = Hop_ObjChild0(pObj);
-        *ppFan1 = Hop_ObjChild1(pObj);
-        return 1;
-    }
-    assert( Hop_ObjIsAnd(pObj) );
-    p0 = Hop_ObjChild0(pObj);
-    p1 = Hop_ObjChild1(pObj);
-    if ( !Hop_IsComplement(p0) || !Hop_IsComplement(p1) )
-        return 0;
-    p0 = Hop_Regular(p0);
-    p1 = Hop_Regular(p1);
-    if ( !Hop_ObjIsAnd(p0) || !Hop_ObjIsAnd(p1) )
-        return 0;
-    if ( Hop_ObjFanin0(p0) != Hop_ObjFanin0(p1) || Hop_ObjFanin1(p0) != Hop_ObjFanin1(p1) )
-        return 0;
-    if ( Hop_ObjFaninC0(p0) == Hop_ObjFaninC0(p1) || Hop_ObjFaninC1(p0) == Hop_ObjFaninC1(p1) )
-        return 0;
-    *ppFan0 = Hop_ObjChild0(p0);
-    *ppFan1 = Hop_ObjChild1(p0);
-    return 1;
-}
-
-/**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     []
-
-***********************************************************************/
-Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pNode, Hop_Obj_t ** ppNodeT, Hop_Obj_t ** ppNodeE )
-{
-    Hop_Obj_t * pNode0, * pNode1;
-    assert( !Hop_IsComplement(pNode) );
-    assert( Hop_ObjIsMuxType(pNode) );
-    // get children
-    pNode0 = Hop_ObjFanin0(pNode);
-    pNode1 = Hop_ObjFanin1(pNode);
-
-    // find the control variable
-    if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Hop_ObjFaninC1(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
-            return Hop_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
-            return Hop_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Hop_ObjFaninC0(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
-            return Hop_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
-            return Hop_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-    else if ( Hop_ObjFanin0(pNode0) == Hop_ObjFanin1(pNode1) && (Hop_ObjFaninC0(pNode0) ^ Hop_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Hop_ObjFaninC0(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
-            return Hop_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Hop_Not(Hop_ObjChild0(pNode1));//pNode2->p1);
-            return Hop_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-    else if ( Hop_ObjFanin1(pNode0) == Hop_ObjFanin0(pNode1) && (Hop_ObjFaninC1(pNode0) ^ Hop_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Hop_ObjFaninC1(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
-            return Hop_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Hop_Not(Hop_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Hop_Not(Hop_ObjChild1(pNode1));//pNode2->p2);
-            return Hop_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    assert( 0 ); // this is not MUX
-    return NULL;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints Eqn formula for the AIG rooted at this node.]
-
-  Description [The formula is in terms of PIs, which should have
-  their names assigned in pObj->pData fields.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
-{
-    Vec_Ptr_t * vSuper;
-    Hop_Obj_t * pFanin;
-    int fCompl, i;
-    // store the complemented attribute
-    fCompl = Hop_IsComplement(pObj);
-    pObj = Hop_Regular(pObj);
-    // constant case
-    if ( Hop_ObjIsConst1(pObj) )
-    {
-        fprintf( pFile, "%d", !fCompl );
-        return;
-    }
-    // PI case
-    if ( Hop_ObjIsPi(pObj) )
-    {
-        fprintf( pFile, "%s%s", fCompl? "!" : "", pObj->pData );
-        return;
-    }
-    // AND case
-    Vec_VecExpand( vLevels, Level );
-    vSuper = Vec_VecEntry(vLevels, Level);
-    Hop_ObjCollectMulti( pObj, vSuper );
-    fprintf( pFile, "%s", (Level==0? "" : "(") );
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        Hop_ObjPrintEqn( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
-        if ( i < Vec_PtrSize(vSuper) - 1 )
-            fprintf( pFile, " %s ", fCompl? "+" : "*" );
-    }
-    fprintf( pFile, "%s", (Level==0? "" : ")") );
-    return;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints Verilog formula for the AIG rooted at this node.]
-
-  Description [The formula is in terms of PIs, which should have
-  their names assigned in pObj->pData fields.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
-{
-    Vec_Ptr_t * vSuper;
-    Hop_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
-    int fCompl, i;
-    // store the complemented attribute
-    fCompl = Hop_IsComplement(pObj);
-    pObj = Hop_Regular(pObj);
-    // constant case
-    if ( Hop_ObjIsConst1(pObj) )
-    {
-        fprintf( pFile, "1\'b%d", !fCompl );
-        return;
-    }
-    // PI case
-    if ( Hop_ObjIsPi(pObj) )
-    {
-        fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData );
-        return;
-    }
-    // EXOR case
-    if ( Hop_ObjIsExor(pObj) )
-    {
-        Vec_VecExpand( vLevels, Level );
-        vSuper = Vec_VecEntry( vLevels, Level );
-        Hop_ObjCollectMulti( pObj, vSuper );
-        fprintf( pFile, "%s", (Level==0? "" : "(") );
-        Vec_PtrForEachEntry( vSuper, pFanin, i )
-        {
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
-            if ( i < Vec_PtrSize(vSuper) - 1 )
-                fprintf( pFile, " ^ " );
-        }
-        fprintf( pFile, "%s", (Level==0? "" : ")") );
-        return;
-    }
-    // MUX case
-    if ( Hop_ObjIsMuxType(pObj) )
-    {
-        if ( Hop_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
-        {
-            fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
-            fprintf( pFile, " ^ " );
-            Hop_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
-            fprintf( pFile, "%s", (Level==0? "" : ")") );
-        }
-        else 
-        {
-            pFaninC = Hop_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
-            fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Hop_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
-            fprintf( pFile, " ? " );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin1, fCompl), vLevels, Level+1 );
-            fprintf( pFile, " : " );
-            Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin0, fCompl), vLevels, Level+1 );
-            fprintf( pFile, "%s", (Level==0? "" : ")") );
-        }
-        return;
-    }
-    // AND case
-    Vec_VecExpand( vLevels, Level );
-    vSuper = Vec_VecEntry(vLevels, Level);
-    Hop_ObjCollectMulti( pObj, vSuper );
-    fprintf( pFile, "%s", (Level==0? "" : "(") );
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        Hop_ObjPrintVerilog( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
-        if ( i < Vec_PtrSize(vSuper) - 1 )
-            fprintf( pFile, " %s ", fCompl? "|" : "&" );
-    }
-    fprintf( pFile, "%s", (Level==0? "" : ")") );
-    return;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints node in HAIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig )
-{
-    assert( !Hop_IsComplement(pObj) );
-    printf( "Node %p : ", pObj );
-    if ( Hop_ObjIsConst1(pObj) )
-        printf( "constant 1" );
-    else if ( Hop_ObjIsPi(pObj) )
-        printf( "PI" );
-    else
-        printf( "AND( %p%s, %p%s )", 
-            Hop_ObjFanin0(pObj), (Hop_ObjFaninC0(pObj)? "\'" : " "), 
-            Hop_ObjFanin1(pObj), (Hop_ObjFaninC1(pObj)? "\'" : " ") );
-    printf( " (refs = %3d)", Hop_ObjRefs(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints node in HAIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig )
-{
-    Vec_Ptr_t * vNodes;
-    Hop_Obj_t * pObj;
-    int i;
-    printf( "PIs: " );
-    Hop_ManForEachPi( p, pObj, i )
-        printf( " %p", pObj );
-    printf( "\n" );
-    vNodes = Hop_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Hop_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the AIG into the BLIF file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName )
-{
-    FILE * pFile;
-    Vec_Ptr_t * vNodes;
-    Hop_Obj_t * pObj, * pConst1 = NULL;
-    int i, nDigits, Counter = 0;
-    if ( Hop_ManPoNum(p) == 0 )
-    {
-        printf( "Hop_ManDumpBlif(): AIG manager does not have POs.\n" );
-        return;
-    }
-    // collect nodes in the DFS order
-    vNodes = Hop_ManDfs( p );
-    // assign IDs to objects
-    Hop_ManConst1(p)->pData = (void *)Counter++;
-    Hop_ManForEachPi( p, pObj, i )
-        pObj->pData = (void *)Counter++;
-    Hop_ManForEachPo( p, pObj, i )
-        pObj->pData = (void *)Counter++;
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = (void *)Counter++;
-    nDigits = Hop_Base10Log( Counter );
-    // write the file
-    pFile = fopen( pFileName, "w" );
-    fprintf( pFile, "# BLIF file written by procedure Hop_ManDumpBlif() in ABC\n" );
-    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
-    fprintf( pFile, ".model test\n" );
-    // write PIs
-    fprintf( pFile, ".inputs" );
-    Hop_ManForEachPi( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
-    fprintf( pFile, "\n" );
-    // write POs
-    fprintf( pFile, ".outputs" );
-    Hop_ManForEachPo( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
-    fprintf( pFile, "\n" );
-    // write nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", 
-            nDigits, (int)Hop_ObjFanin0(pObj)->pData, 
-            nDigits, (int)Hop_ObjFanin1(pObj)->pData, 
-            nDigits, (int)pObj->pData );
-        fprintf( pFile, "%d%d 1\n", !Hop_ObjFaninC0(pObj), !Hop_ObjFaninC1(pObj) );
-    }
-    // write POs
-    Hop_ManForEachPo( p, pObj, i )
-    {
-        fprintf( pFile, ".names n%0*d n%0*d\n", 
-            nDigits, (int)Hop_ObjFanin0(pObj)->pData, 
-            nDigits, (int)pObj->pData );
-        fprintf( pFile, "%d 1\n", !Hop_ObjFaninC0(pObj) );
-        if ( Hop_ObjIsConst1(Hop_ObjFanin0(pObj)) )
-            pConst1 = Hop_ManConst1(p);
-    }
-    if ( pConst1 )
-        fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData );
-    fprintf( pFile, ".end\n\n" );
-    fclose( pFile );
-    Vec_PtrFree( vNodes );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/hop/hop_.c b/src/aig/hop/hop_.c
deleted file mode 100644
index 468413fa..00000000
--- a/src/aig/hop/hop_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ivy_.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Minimalistic 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/aig/hop/module.make b/src/aig/hop/module.make
deleted file mode 100644
index b06d91fd..00000000
--- a/src/aig/hop/module.make
+++ /dev/null
@@ -1,9 +0,0 @@
-SRC +=    src/aig/hop/hopBalance.c \
-    src/aig/hop/hopCheck.c \
-    src/aig/hop/hopDfs.c \
-    src/aig/hop/hopMan.c \
-    src/aig/hop/hopMem.c \
-    src/aig/hop/hopObj.c \
-    src/aig/hop/hopOper.c \
-    src/aig/hop/hopTable.c \
-    src/aig/hop/hopUtil.c