Version abc61122

21 files changed, 0 insertions, 7061 deletions

diff --git a/src/temp/aig_free/aig.h b/src/temp/aig_free/aig.h
deleted file mode 100644
index 0dfc3f11..00000000
--- a/src/temp/aig_free/aig.h
+++ /dev/null
@@ -1,321 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aig.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: aig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __AIG_H__
-#define __AIG_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 Aig_Man_t_            Aig_Man_t;
-typedef struct Aig_Obj_t_            Aig_Obj_t;
-typedef int                          Aig_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
-} Aig_Type_t;
-
-// the AIG node
-struct Aig_Obj_t_  // 4 words
-{
-    void *           pData;          // misc
-    Aig_Obj_t *      pFanin0;        // fanin
-    Aig_Obj_t *      pFanin1;        // fanin
-    unsigned long    Type    :  3;   // object type
-    unsigned long    fPhase  :  1;   // value under 000...0 pattern
-    unsigned long    fMarkA  :  1;   // multipurpose mask
-    unsigned long    fMarkB  :  1;   // multipurpose mask
-    unsigned long    nRefs   : 26;   // reference count (level)
-};
-
-// the AIG manager
-struct Aig_Man_t_
-{
-    // AIG nodes
-    Vec_Ptr_t *      vPis;           // the array of PIs
-    Vec_Ptr_t *      vPos;           // the array of POs
-    Aig_Obj_t *      pConst1;        // the constant 1 node
-    Aig_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
-    Aig_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
-    Aig_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          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);           }
-static inline int          Aig_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }
-static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
-static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
-static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
-
-static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned long)(p) & ~01);      }
-static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned long)(p) ^  01);      }
-static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((unsigned long)(p) ^ (c));      }
-static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int )(((unsigned long)p) & 01);              }
-
-static inline Aig_Obj_t *  Aig_ManConst0( Aig_Man_t * p )         { return Aig_Not(p->pConst1);                     }
-static inline Aig_Obj_t *  Aig_ManConst1( Aig_Man_t * p )         { return p->pConst1;                              }
-static inline Aig_Obj_t *  Aig_ManGhost( Aig_Man_t * p )          { return &p->Ghost;                               }
-static inline Aig_Obj_t *  Aig_ManPi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i);   }
-
-static inline Aig_Edge_t   Aig_EdgeCreate( int Id, int fCompl )            { return (Id << 1) | fCompl;             }
-static inline int          Aig_EdgeId( Aig_Edge_t Edge )                   { return Edge >> 1;                      }
-static inline int          Aig_EdgeIsComplement( Aig_Edge_t Edge )         { return Edge & 1;                       }
-static inline Aig_Edge_t   Aig_EdgeRegular( Aig_Edge_t Edge )              { return (Edge >> 1) << 1;               }
-static inline Aig_Edge_t   Aig_EdgeNot( Aig_Edge_t Edge )                  { return Edge ^ 1;                       }
-static inline Aig_Edge_t   Aig_EdgeNotCond( Aig_Edge_t Edge, int fCond )   { return Edge ^ fCond;                   }
-
-static inline int          Aig_ManPiNum( Aig_Man_t * p )          { return p->nObjs[AIG_PI];                    }
-static inline int          Aig_ManPoNum( Aig_Man_t * p )          { return p->nObjs[AIG_PO];                    }
-static inline int          Aig_ManAndNum( Aig_Man_t * p )         { return p->nObjs[AIG_AND];                   }
-static inline int          Aig_ManExorNum( Aig_Man_t * p )        { return p->nObjs[AIG_EXOR];                  }
-static inline int          Aig_ManNodeNum( Aig_Man_t * p )        { return p->nObjs[AIG_AND]+p->nObjs[AIG_EXOR];}
-static inline int          Aig_ManGetCost( Aig_Man_t * p )        { return p->nObjs[AIG_AND]+3*p->nObjs[AIG_EXOR]; }
-static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nCreated - p->nDeleted;           }
-
-static inline Aig_Type_t   Aig_ObjType( Aig_Obj_t * pObj )        { return pObj->Type;               }
-static inline int          Aig_ObjIsNone( Aig_Obj_t * pObj )      { return pObj->Type == AIG_NONE;   }
-static inline int          Aig_ObjIsConst1( Aig_Obj_t * pObj )    { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_CONST1; }
-static inline int          Aig_ObjIsPi( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PI;     }
-static inline int          Aig_ObjIsPo( Aig_Obj_t * pObj )        { return pObj->Type == AIG_PO;     }
-static inline int          Aig_ObjIsAnd( Aig_Obj_t * pObj )       { return pObj->Type == AIG_AND;    }
-static inline int          Aig_ObjIsExor( Aig_Obj_t * pObj )      { return pObj->Type == AIG_EXOR;   }
-static inline int          Aig_ObjIsNode( Aig_Obj_t * pObj )      { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }
-static inline int          Aig_ObjIsTerm( Aig_Obj_t * pObj )      { return pObj->Type == AIG_PI  || pObj->Type == AIG_PO || pObj->Type == AIG_CONST1; }
-static inline int          Aig_ObjIsHash( Aig_Obj_t * pObj )      { return pObj->Type == AIG_AND || pObj->Type == AIG_EXOR;   }
-
-static inline int          Aig_ObjIsMarkA( Aig_Obj_t * pObj )     { return pObj->fMarkA;  }
-static inline void         Aig_ObjSetMarkA( Aig_Obj_t * pObj )    { pObj->fMarkA = 1;     }
-static inline void         Aig_ObjClearMarkA( Aig_Obj_t * pObj )  { pObj->fMarkA = 0;     }
- 
-static inline void         Aig_ObjSetTravId( Aig_Obj_t * pObj, int TravId )                { pObj->pData = (void *)TravId;                       }
-static inline void         Aig_ObjSetTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj )      { pObj->pData = (void *)p->nTravIds;                  }
-static inline void         Aig_ObjSetTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj )     { pObj->pData = (void *)(p->nTravIds - 1);            }
-static inline int          Aig_ObjIsTravIdCurrent( Aig_Man_t * p, Aig_Obj_t * pObj )       { return (int )((int)pObj->pData == p->nTravIds);     }
-static inline int          Aig_ObjIsTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * pObj )      { return (int )((int)pObj->pData == p->nTravIds - 1); }
-
-static inline int          Aig_ObjTravId( Aig_Obj_t * pObj )      { return (int)pObj->pData;                       }
-static inline int          Aig_ObjPhase( Aig_Obj_t * pObj )       { return pObj->fPhase;                           }
-static inline int          Aig_ObjRefs( Aig_Obj_t * pObj )        { return pObj->nRefs;                            }
-static inline void         Aig_ObjRef( Aig_Obj_t * pObj )         { pObj->nRefs++;                                 }
-static inline void         Aig_ObjDeref( Aig_Obj_t * pObj )       { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
-static inline void         Aig_ObjClearRef( Aig_Obj_t * pObj )    { pObj->nRefs = 0;                               }
-static inline int          Aig_ObjFaninC0( Aig_Obj_t * pObj )     { return Aig_IsComplement(pObj->pFanin0);        }
-static inline int          Aig_ObjFaninC1( Aig_Obj_t * pObj )     { return Aig_IsComplement(pObj->pFanin1);        }
-static inline Aig_Obj_t *  Aig_ObjFanin0( Aig_Obj_t * pObj )      { return Aig_Regular(pObj->pFanin0);             }
-static inline Aig_Obj_t *  Aig_ObjFanin1( Aig_Obj_t * pObj )      { return Aig_Regular(pObj->pFanin1);             }
-static inline Aig_Obj_t *  Aig_ObjChild0( Aig_Obj_t * pObj )      { return pObj->pFanin0;                          }
-static inline Aig_Obj_t *  Aig_ObjChild1( Aig_Obj_t * pObj )      { return pObj->pFanin1;                          }
-static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
-static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->nRefs;                            }
-static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->nRefs, Aig_ObjFanin1(pObj)->nRefs);       }
-static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) ); }
-static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
-{ 
-    if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
-    if ( Aig_ObjFanin1(pObj) == pFanin ) return 1; 
-    assert(0); return -1; 
-}
-static inline int          Aig_ObjFanoutC( Aig_Obj_t * pObj, Aig_Obj_t * pFanout )    
-{ 
-    if ( Aig_ObjFanin0(pFanout) == pObj ) return Aig_ObjFaninC0(pObj); 
-    if ( Aig_ObjFanin1(pFanout) == pObj ) return Aig_ObjFaninC1(pObj); 
-    assert(0); return -1; 
-}
-
-// create the ghost of the new node
-static inline Aig_Obj_t *  Aig_ObjCreateGhost( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type )    
-{
-    Aig_Obj_t * pGhost;
-    assert( Type != AIG_AND || !Aig_ObjIsConst1(Aig_Regular(p0)) );
-    assert( p1 == NULL || !Aig_ObjIsConst1(Aig_Regular(p1)) );
-    assert( Type == AIG_PI || Aig_Regular(p0) != Aig_Regular(p1) );
-    pGhost = Aig_ManGhost(p);
-    pGhost->Type = Type;
-    pGhost->pFanin0 = p0 < p1? p0 : p1;
-    pGhost->pFanin1 = p0 < p1? p1 : p0;
-    return pGhost;
-}
-
-// internal memory manager
-static inline Aig_Obj_t * Aig_ManFetchMemory( Aig_Man_t * p )  
-{ 
-    extern void Aig_ManAddMemory( Aig_Man_t * p );
-    Aig_Obj_t * pTemp;
-    if ( p->pListFree == NULL )
-        Aig_ManAddMemory( p );
-    pTemp = p->pListFree;
-    p->pListFree = *((Aig_Obj_t **)pTemp);
-    memset( pTemp, 0, sizeof(Aig_Obj_t) ); 
-    return pTemp;
-}
-static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
-{
-    pEntry->Type = AIG_NONE; // distinquishes dead node from live node
-    *((Aig_Obj_t **)pEntry) = p->pListFree;
-    p->pListFree = pEntry;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                             ITERATORS                            ///
-////////////////////////////////////////////////////////////////////////
-
-// iterator over the primary inputs
-#define Aig_ManForEachPi( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPis, pObj, i )
-// iterator over the primary outputs
-#define Aig_ManForEachPo( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPos, pObj, i )
-// iterator over all objects, including those currently not used
-#define Aig_ManForEachNode( p, pObj, i )                                        \
-    for ( i = 0; i < p->nTableSize; i++ )                                       \
-        if ( ((pObj) = p->pTable[i]) == NULL ) {} else
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== aigBalance.c ========================================================*/
-extern Aig_Man_t *     Aig_ManBalance( Aig_Man_t * p, int fUpdateLevel );
-extern Aig_Obj_t *     Aig_NodeBalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel );
-/*=== aigCheck.c ========================================================*/
-extern int             Aig_ManCheck( Aig_Man_t * p );
-/*=== aigDfs.c ==========================================================*/
-extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
-extern Vec_Ptr_t *     Aig_ManDfsNode( Aig_Man_t * p, Aig_Obj_t * pNode );
-extern int             Aig_ManCountLevels( Aig_Man_t * p );
-extern void            Aig_ManCreateRefs( Aig_Man_t * p );
-extern int             Aig_DagSize( Aig_Obj_t * pObj );
-extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
-extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
-extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
-/*=== aigMan.c ==========================================================*/
-extern Aig_Man_t *     Aig_ManStart();
-extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p );
-extern void            Aig_ManStop( Aig_Man_t * p );
-extern int             Aig_ManCleanup( Aig_Man_t * p );
-extern void            Aig_ManPrintStats( Aig_Man_t * p );
-/*=== aigMem.c ==========================================================*/
-extern void            Aig_ManStartMemory( Aig_Man_t * p );
-extern void            Aig_ManStopMemory( Aig_Man_t * p );
-/*=== aigObj.c ==========================================================*/
-extern Aig_Obj_t *     Aig_ObjCreatePi( Aig_Man_t * p );
-extern Aig_Obj_t *     Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );
-extern Aig_Obj_t *     Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost );
-extern void            Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj_t * pFan1 );
-extern void            Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern void            Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern void            Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj );
-/*=== aigOper.c =========================================================*/
-extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
-extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
-extern Aig_Obj_t *     Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
-extern Aig_Obj_t *     Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
-extern Aig_Obj_t *     Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
-extern Aig_Obj_t *     Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
-extern Aig_Obj_t *     Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC );
-extern Aig_Obj_t *     Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs );
-extern Aig_Obj_t *     Aig_CreateAnd( Aig_Man_t * p, int nVars );
-extern Aig_Obj_t *     Aig_CreateOr( Aig_Man_t * p, int nVars );
-extern Aig_Obj_t *     Aig_CreateExor( Aig_Man_t * p, int nVars );
-/*=== aigTable.c ========================================================*/
-extern Aig_Obj_t *     Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
-extern void            Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
-extern int             Aig_TableCountEntries( Aig_Man_t * p );
-extern void            Aig_TableProfile( Aig_Man_t * p );
-/*=== aigUtil.c =========================================================*/
-extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
-extern void            Aig_ManCleanData( Aig_Man_t * p );
-extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
-extern int             Aig_ObjIsMuxType( Aig_Obj_t * pObj );
-extern int             Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
-extern Aig_Obj_t *     Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
-extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
-extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
-extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
-extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/aig_free/aigBalance.c b/src/temp/aig_free/aigBalance.c
deleted file mode 100644
index 1abc672d..00000000
--- a/src/temp/aig_free/aigBalance.c
+++ /dev/null
@@ -1,391 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigBalance.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: aigBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static Aig_Obj_t * Aig_NodeBalance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
-static Vec_Ptr_t * Aig_NodeBalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
-static int         Aig_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Aig_NodeBalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
-static void        Aig_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs algebraic balancing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManBalance( Aig_Man_t * p, int fUpdateLevel )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    Vec_Vec_t * vStore;
-    int i;
-    // create the new manager 
-    pNew = Aig_ManStart();
-    pNew->fRefCount = 0;
-    // map the PI nodes
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi(pNew);
-    // balance the AIG
-    vStore = Vec_VecAlloc( 50 );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        pObjNew = Aig_NodeBalance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
-        Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) );
-    }
-    Vec_VecFree( vStore );
-    // remove dangling nodes
-//    Aig_ManCreateRefs( pNew );
-//    if ( i = Aig_ManCleanup( pNew ) )
-//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
-    // check the resulting AIG
-    if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManBalance(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the new node constructed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_NodeBalance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
-{
-    Aig_Obj_t * pObjNew;
-    Vec_Ptr_t * vSuper;
-    int i;
-    assert( !Aig_IsComplement(pObjOld) );
-    // return if the result is known
-    if ( pObjOld->pData )
-        return pObjOld->pData;
-    assert( Aig_ObjIsNode(pObjOld) );
-    // get the implication supergate
-    vSuper = Aig_NodeBalanceCone( pObjOld, vStore, Level );
-    // check if supergate contains two nodes in the opposite polarity
-    if ( vSuper->nSize == 0 )
-        return pObjOld->pData = Aig_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 = Aig_NodeBalance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
-        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
-    }
-    // build the supergate
-    pObjNew = Aig_NodeBalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
-    // make sure the balanced node is not assigned
-//    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
-    assert( pObjOld->pData == NULL );
-    return pObjOld->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the nodes of the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeBalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    int RetValue1, RetValue2, i;
-    // check if the node is visited
-    if ( Aig_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] == Aig_Not(pObj) )
-                return -1;
-        assert( 0 );
-        return 0;
-    }
-    // if the new node is complemented or a PI, another gate begins
-    if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) )
-    {
-        Vec_PtrPush( vSuper, pObj );
-        Aig_Regular(pObj)->fMarkB = 1;
-        return 0;
-    }
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    // go through the branches
-    RetValue1 = Aig_NodeBalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
-    RetValue2 = Aig_NodeBalanceCone_rec( pRoot, Aig_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 * Aig_NodeBalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
-{
-    Vec_Ptr_t * vNodes;
-    int RetValue, i;
-    assert( !Aig_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 = Aig_NodeBalanceCone_rec( pObj, pObj, vNodes );
-    assert( vNodes->nSize > 1 );
-    // unmark the visited nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_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 Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
-{
-    int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2));
-    if ( Diff > 0 )
-        return -1;
-    if ( Diff < 0 ) 
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Builds implication supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_NodeBalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    int LeftBound;
-    assert( vSuper->nSize > 1 );
-    // sort the new nodes by level in the decreasing order
-    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
-    // balance the nodes
-    while ( vSuper->nSize > 1 )
-    {
-        // find the left bound on the node to be paired
-        LeftBound = (!fUpdateLevel)? 0 : Aig_NodeBalanceFindLeft( vSuper );
-        // find the node that can be shared (if no such node, randomize choice)
-        Aig_NodeBalancePermute( p, vSuper, LeftBound, Type == AIG_EXOR );
-        // pull out the last two nodes
-        pObj1 = Vec_PtrPop(vSuper);
-        pObj2 = Vec_PtrPop(vSuper);
-        Aig_NodeBalancePushUniqueOrderByLevel( vSuper, Aig_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 Aig_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
-{
-    Aig_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 ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
-            break;
-    }
-    Current++;    
-    // get the node, for which the equality holds
-    pObjLeft = Vec_PtrEntry( vSuper, Current );
-    assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_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 Aig_NodeBalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
-{
-    Aig_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 ( Aig_Regular(pObj1) == p->pConst1 || Aig_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 ( Aig_Regular(pObj3) == p->pConst1 )
-        {
-            Vec_PtrWriteEntry( vSuper, i,          pObj2 );
-            Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
-            return;
-        }
-        pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_EXOR : AIG_AND );
-        if ( Aig_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 Aig_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
-{
-    Aig_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 ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
-            break;
-        vStore->pArray[i  ] = pObj2;
-        vStore->pArray[i-1] = pObj1;
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigCheck.c b/src/temp/aig_free/aigCheck.c
deleted file mode 100644
index 61e4cf78..00000000
--- a/src/temp/aig_free/aigCheck.c
+++ /dev/null
@@ -1,110 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigCheck.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: aigCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Checks the consistency of the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManCheck( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObj2;
-    int i;
-    // check primary inputs
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        if ( Aig_ObjFanin0(pObj) || Aig_ObjFanin1(pObj) )
-        {
-            printf( "Aig_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
-            return 0;
-        }
-    }
-    // check primary outputs
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        if ( !Aig_ObjFanin0(pObj) )
-        {
-            printf( "Aig_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
-            return 0;
-        }
-        if ( Aig_ObjFanin1(pObj) )
-        {
-            printf( "Aig_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
-            return 0;
-        }
-    }
-    // check internal nodes
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        if ( !Aig_ObjFanin0(pObj) || !Aig_ObjFanin1(pObj) )
-        {
-            printf( "Aig_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
-            return 0;
-        }
-        if ( Aig_ObjFanin0(pObj) >= Aig_ObjFanin1(pObj) )
-        {
-            printf( "Aig_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
-            return 0;
-        }
-        pObj2 = Aig_TableLookup( p, pObj );
-        if ( pObj2 != pObj )
-        {
-            printf( "Aig_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
-            return 0;
-        }
-    }
-    // count the total number of nodes
-    if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
-    {
-        printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
-        return 0;
-    }
-    // count the number of nodes in the table
-    if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
-    {
-        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
-        return 0;
-    }
-//    if ( !Aig_ManIsAcyclic(p) )
-//        return 0;
-    return 1; 
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigDfs.c b/src/temp/aig_free/aigDfs.c
deleted file mode 100644
index c004cab0..00000000
--- a/src/temp/aig_free/aigDfs.c
+++ /dev/null
@@ -1,399 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigDfs.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: aigDfs.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDfs_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ManDfs_rec( Aig_ObjFanin0(pObj), vNodes );
-    Aig_ManDfs_rec( Aig_ObjFanin1(pObj), vNodes );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA(pObj);
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
-    Aig_ManForEachNode( p, pObj, i )
-        Aig_ManDfs_rec( pObj, vNodes );
-    Aig_ManForEachNode( p, pObj, i )
-        Aig_ObjClearMarkA(pObj);
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsNode( Aig_Man_t * p, Aig_Obj_t * pNode )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    assert( !Aig_IsComplement(pNode) );
-    vNodes = Vec_PtrAlloc( 16 );
-    Aig_ManDfs_rec( pNode, vNodes );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_ObjClearMarkA(pObj);
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the max number of levels in the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManCountLevels( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i, LevelsMax, Level0, Level1;
-    // initialize the levels
-    Aig_ManConst1(p)->pData = NULL;
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = NULL;
-    // compute levels in a DFS order
-    vNodes = Aig_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-    {
-        Level0 = (int)Aig_ObjFanin0(pObj)->pData;
-        Level1 = (int)Aig_ObjFanin1(pObj)->pData;
-        pObj->pData = (void *)(1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1));
-    }
-    Vec_PtrFree( vNodes );
-    // get levels of the POs
-    LevelsMax = 0;
-    Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->pData );
-    return LevelsMax;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates correct reference counters at each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManCreateRefs( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    if ( p->fRefCount )
-        return;
-    p->fRefCount = 1;
-    // clear refs
-    Aig_ObjClearRef( Aig_ManConst1(p) );
-    Aig_ManForEachPi( p, pObj, i )
-        Aig_ObjClearRef( pObj );
-    Aig_ManForEachNode( p, pObj, i )
-        Aig_ObjClearRef( pObj );
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjClearRef( pObj );
-    // set refs
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        Aig_ObjRef( Aig_ObjFanin0(pObj) );
-        Aig_ObjRef( Aig_ObjFanin1(pObj) );
-    }
-    Aig_ManForEachPo( p, pObj, i )
-        Aig_ObjRef( Aig_ObjFanin0(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeMark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeMark_rec( Aig_ObjFanin0(pObj) );
-    Aig_ConeMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeCleanAndMark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeCleanAndMark_rec( Aig_ObjFanin0(pObj) );
-    Aig_ConeCleanAndMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-    pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ConeCountAndMark_rec( Aig_Obj_t * pObj )
-{
-    int Counter;
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return 0;
-    Counter = 1 + Aig_ConeCountAndMark_rec( Aig_ObjFanin0(pObj) ) + 
-        Aig_ConeCountAndMark_rec( Aig_ObjFanin1(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ConeUnmark_rec( Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || !Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_ConeUnmark_rec( Aig_ObjFanin0(pObj) ); 
-    Aig_ConeUnmark_rec( Aig_ObjFanin1(pObj) );
-    assert( Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjClearMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of AIG nodes rooted at this cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_DagSize( Aig_Obj_t * pObj )
-{
-    int Counter;
-    Counter = Aig_ConeCountAndMark_rec( Aig_Regular(pObj) );
-    Aig_ConeUnmark_rec( Aig_Regular(pObj) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_Transfer_rec( Aig_Man_t * pDest, Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) || Aig_ObjIsMarkA(pObj) )
-        return;
-    Aig_Transfer_rec( pDest, Aig_ObjFanin0(pObj) ); 
-    Aig_Transfer_rec( pDest, Aig_ObjFanin1(pObj) );
-    pObj->pData = Aig_And( pDest, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the AIG from one manager into another.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoot, int nVars )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // solve simple cases
-    if ( pSour == pDest )
-        return pRoot;
-    if ( Aig_ObjIsConst1( Aig_Regular(pRoot) ) )
-        return Aig_NotCond( Aig_ManConst1(pDest), Aig_IsComplement(pRoot) );
-    // set the PI mapping
-    Aig_ManForEachPi( pSour, pObj, i )
-    {
-        if ( i == nVars )
-           break;
-        pObj->pData = Aig_IthVar(pDest, i);
-    }
-    // transfer and set markings
-    Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
-    // clear the markings
-    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_Compose_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFunc, Aig_Obj_t * pVar )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsMarkA(pObj) )
-        return;
-    if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
-    {
-        pObj->pData = pObj == pVar ? pFunc : pObj;
-        return;
-    }
-    Aig_Compose_rec( p, Aig_ObjFanin0(pObj), pFunc, pVar ); 
-    Aig_Compose_rec( p, Aig_ObjFanin1(pObj), pFunc, pVar );
-    pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    assert( !Aig_ObjIsMarkA(pObj) ); // loop detection
-    Aig_ObjSetMarkA( pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar )
-{
-    // quit if the PI variable is not defined
-    if ( iVar >= Aig_ManPiNum(p) )
-    {
-        printf( "Aig_Compose(): The PI variable %d is not defined.\n", iVar );
-        return NULL;
-    }
-    // recursively perform composition
-    Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) );
-    // clear the markings
-    Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigMan.c b/src/temp/aig_free/aigMan.c
deleted file mode 100644
index bb39712f..00000000
--- a/src/temp/aig_free/aigMan.c
+++ /dev/null
@@ -1,162 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigMan.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: aig_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManStart()
-{
-    Aig_Man_t * p;
-    // start the manager
-    p = ALLOC( Aig_Man_t, 1 );
-    memset( p, 0, sizeof(Aig_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
-    Aig_ManStartMemory( p );
-    // create the constant node
-    p->pConst1 = Aig_ManFetchMemory( p );
-    p->pConst1->Type = AIG_CONST1;
-    p->pConst1->fPhase = 1;
-    p->nCreated = 1;
-    // start the table
-    p->nTableSize = 10007;
-    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManStop( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // make sure the nodes have clean marks
-    pObj = Aig_ManConst1(p);
-    assert( !pObj->fMarkA && !pObj->fMarkB );
-    Aig_ManForEachPi( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    Aig_ManForEachPo( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    Aig_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 ); }
-//    Aig_TableProfile( p );
-    if ( p->vChunks )   Aig_ManStopMemory( p );
-    if ( p->vPis )      Vec_PtrFree( p->vPis );
-    if ( p->vPos )      Vec_PtrFree( p->vPos );
-    free( p->pTable );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManCleanup( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pNode;
-    int i, nNodesOld;
-    assert( p->fRefCount );
-    nNodesOld = Aig_ManNodeNum(p);
-    // collect roots of dangling nodes
-    vNodes = Vec_PtrAlloc( 100 );
-    Aig_ManForEachNode( p, pNode, i )
-        if ( Aig_ObjRefs(pNode) == 0 )
-            Vec_PtrPush( vNodes, pNode );
-    // recursively remove dangling nodes
-    Vec_PtrForEachEntry( vNodes, pNode, i )
-        Aig_ObjDelete_rec( p, pNode );
-    Vec_PtrFree( vNodes );
-    return nNodesOld - Aig_ManNodeNum(p);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManPrintStats( Aig_Man_t * p )
-{
-    printf( "PI/PO = %d/%d. ", Aig_ManPiNum(p), Aig_ManPoNum(p) );
-    printf( "A = %7d. ",       Aig_ManAndNum(p) );
-    printf( "X = %5d. ",       Aig_ManExorNum(p) );
-    printf( "Cre = %7d. ",     p->nCreated );
-    printf( "Del = %7d. ",     p->nDeleted );
-    printf( "Lev = %3d. ",     Aig_ManCountLevels(p) );
-    printf( "\n" );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigMem.c b/src/temp/aig_free/aigMem.c
deleted file mode 100644
index 1be78a88..00000000
--- a/src/temp/aig_free/aigMem.c
+++ /dev/null
@@ -1,115 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigMem.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: aigMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.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 Aig_ManStartMemory( Aig_Man_t * p )
-{
-    p->vChunks = Vec_PtrAlloc( 128 );
-    p->vPages = Vec_PtrAlloc( 128 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the internal memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManStopMemory( Aig_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 Aig_ManAddMemory( Aig_Man_t * p )
-{
-    char * pMemory;
-    int i, nBytes;
-    assert( sizeof(Aig_Obj_t) <= 64 );
-    assert( p->pListFree == NULL );
-//    assert( (Aig_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
-    // allocate new memory page
-    nBytes = sizeof(Aig_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 = (Aig_Obj_t *)pMemory;
-    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
-    {
-        *((char **)pMemory) = pMemory + sizeof(Aig_Obj_t);
-        pMemory += sizeof(Aig_Obj_t);
-    }
-    *((char **)pMemory) = NULL;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigObj.c b/src/temp/aig_free/aigObj.c
deleted file mode 100644
index 51ce6008..00000000
--- a/src/temp/aig_free/aigObj.c
+++ /dev/null
@@ -1,228 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigObj.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: aigObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates primary input.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    pObj = Aig_ManFetchMemory( p );
-    pObj->Type = AIG_PI;
-    Vec_PtrPush( p->vPis, pObj );
-    p->nObjs[AIG_PI]++;
-    p->nCreated++;
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates primary output with the given driver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
-{
-    Aig_Obj_t * pObj;
-    pObj = Aig_ManFetchMemory( p );
-    pObj->Type = AIG_PO;
-    Vec_PtrPush( p->vPos, pObj );
-    // add connections
-    pObj->pFanin0 = pDriver;
-    if ( p->fRefCount )
-        Aig_ObjRef( Aig_Regular(pDriver) );
-    else
-        pObj->nRefs = Aig_ObjLevel( Aig_Regular(pDriver) );
-    // update node counters of the manager
-    p->nObjs[AIG_PO]++;
-    p->nCreated++;
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create the new node assuming it does not exist.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
-{
-    Aig_Obj_t * pObj;
-    assert( !Aig_IsComplement(pGhost) );
-    assert( Aig_ObjIsNode(pGhost) );
-    assert( pGhost == &p->Ghost );
-    // get memory for the new object
-    pObj = Aig_ManFetchMemory( p );
-    pObj->Type = pGhost->Type;
-    // add connections
-    Aig_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
-    // update node counters of the manager
-    p->nObjs[Aig_ObjType(pObj)]++;
-    p->nCreated++;
-    return pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connect the object to the fanin.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj_t * pFan1 )
-{
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_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 )
-            Aig_ObjRef( Aig_ObjFanin0(pObj) );
-        if ( pFan1 != NULL )
-            Aig_ObjRef( Aig_ObjFanin1(pObj) );
-    }
-    else
-        pObj->nRefs = Aig_ObjLevelNew( pObj );
-    // add the node to the structural hash table
-    Aig_TableInsert( p, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Connect the object to the fanin.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    // remove connections
-    if ( pObj->pFanin0 != NULL )
-        Aig_ObjDeref(Aig_ObjFanin0(pObj));
-    if ( pObj->pFanin1 != NULL )
-        Aig_ObjDeref(Aig_ObjFanin1(pObj));
-    // remove the node from the structural hash table
-    Aig_TableDelete( p, pObj );
-    // add the first fanin
-    pObj->pFanin0 = NULL;
-    pObj->pFanin1 = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsTerm(pObj) );
-    assert( Aig_ObjRefs(pObj) == 0 );
-    // update node counters of the manager
-    p->nObjs[pObj->Type]--;
-    p->nDeleted++;
-    // remove connections
-    Aig_ObjDisconnect( p, pObj );
-    // remove PIs/POs from the arrays
-    if ( Aig_ObjIsPi(pObj) )
-        Vec_PtrRemove( p->vPis, pObj );
-    // free the node
-    Aig_ManRecycleMemory( p, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the MFFC of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pFanin0, * pFanin1;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
-        return;
-    assert( Aig_ObjIsNode(pObj) );
-    pFanin0 = Aig_ObjFanin0(pObj);
-    pFanin1 = Aig_ObjFanin1(pObj);
-    Aig_ObjDelete( p, pObj );
-    if ( pFanin0 && !Aig_ObjIsNone(pFanin0) && Aig_ObjRefs(pFanin0) == 0 )
-        Aig_ObjDelete_rec( p, pFanin0 );
-    if ( pFanin1 && !Aig_ObjIsNone(pFanin1) && Aig_ObjRefs(pFanin1) == 0 )
-        Aig_ObjDelete_rec( p, pFanin1 );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigOper.c b/src/temp/aig_free/aigOper.c
deleted file mode 100644
index 9985093e..00000000
--- a/src/temp/aig_free/aigOper.c
+++ /dev/null
@@ -1,373 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigOper.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: aigOper.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// procedure to detect an EXOR gate
-static inline int Aig_ObjIsExorType( Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
-{
-    if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
-        return 0;
-    p0 = Aig_Regular(p0);
-    p1 = Aig_Regular(p1);
-    if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
-        return 0;
-    if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
-        return 0;
-    if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
-        return 0;
-    *ppFan0 = Aig_ObjChild0(p0);
-    *ppFan1 = Aig_ObjChild1(p0);
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns i-th elementary variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i )
-{
-    int v;
-    for ( v = Aig_ManPiNum(p); v <= i; v++ )
-        Aig_ObjCreatePi( p );
-    assert( i < Vec_PtrSize(p->vPis) );
-    return Aig_ManPi( p, i );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform one operation.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type )
-{
-    if ( Type == AIG_AND )
-        return Aig_And( p, p0, p1 );
-    if ( Type == AIG_EXOR )
-        return Aig_Exor( p, p0, p1 );
-    assert( 0 );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
-{
-    Aig_Obj_t * pGhost, * pResult;
-//    Aig_Obj_t * pFan0, * pFan1;
-    // check trivial cases
-    if ( p0 == p1 )
-        return p0;
-    if ( p0 == Aig_Not(p1) )
-        return Aig_Not(p->pConst1);
-    if ( Aig_Regular(p0) == p->pConst1 )
-        return p0 == p->pConst1 ? p1 : Aig_Not(p->pConst1);
-    if ( Aig_Regular(p1) == p->pConst1 )
-        return p1 == p->pConst1 ? p0 : Aig_Not(p->pConst1);
-    // check if it can be an EXOR gate
-//    if ( Aig_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
-//        return Aig_Exor( p, pFan0, pFan1 );
-    // check the table
-    pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_AND );
-    if ( pResult = Aig_TableLookup( p, pGhost ) )
-        return pResult;
-    return Aig_ObjCreate( p, pGhost );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description [The argument nodes can be complemented.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
-{
-/*
-    Aig_Obj_t * pGhost, * pResult;
-    // check trivial cases
-    if ( p0 == p1 )
-        return Aig_Not(p->pConst1);
-    if ( p0 == Aig_Not(p1) )
-        return p->pConst1;
-    if ( Aig_Regular(p0) == p->pConst1 )
-        return Aig_NotCond( p1, p0 == p->pConst1 );
-    if ( Aig_Regular(p1) == p->pConst1 )
-        return Aig_NotCond( p0, p1 == p->pConst1 );
-    // check the table
-    pGhost = Aig_ObjCreateGhost( p, p0, p1, AIG_EXOR );
-    if ( pResult = Aig_TableLookup( p, pGhost ) )
-        return pResult;
-    return Aig_ObjCreate( p, pGhost );
-*/
-    return Aig_Or( p, Aig_And(p, p0, Aig_Not(p1)), Aig_And(p, Aig_Not(p0), p1) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements Boolean OR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
-{
-    return Aig_Not( Aig_And( p, Aig_Not(p0), Aig_Not(p1) ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements ITE operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
-{
-/*    
-    Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
-    int Count0, Count1;
-    // consider trivial cases
-    if ( p0 == Aig_Not(p1) )
-        return Aig_Exor( p, pC, p0 );
-    // other cases can be added
-    // implement the first MUX (F = C * x1 + C' * x0)
-
-    // check for constants here!!!
-
-    pTempA1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          p1, AIG_AND) );
-    pTempA2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), p0, AIG_AND) );
-    if ( pTempA1 && pTempA2 )
-    {
-        pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempA1), Aig_Not(pTempA2), AIG_AND) );
-        if ( pTemp ) return Aig_Not(pTemp);
-    }
-    Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
-    // implement the second MUX (F' = C * x1' + C' * x0')
-    pTempB1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          Aig_Not(p1), AIG_AND) );
-    pTempB2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), Aig_Not(p0), AIG_AND) );
-    if ( pTempB1 && pTempB2 )
-    {
-        pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempB1), Aig_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 : Aig_And(p, pC,          p1);
-        pTempA2 = pTempA2? pTempA2 : Aig_And(p, Aig_Not(pC), p0);
-        return Aig_Or( p, pTempA1, pTempA2 );
-    }
-    pTempB1 = pTempB1? pTempB1 : Aig_And(p, pC,          Aig_Not(p1));
-    pTempB2 = pTempB2? pTempB2 : Aig_And(p, Aig_Not(pC), Aig_Not(p0));
-    return Aig_Not( Aig_Or( p, pTempB1, pTempB2 ) );
-*/
-    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements ITE operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC )
-{
-    return Aig_Or( p, Aig_Or(p, Aig_And(p, pA, pB), Aig_And(p, pA, pC)), Aig_And(p, pB, pC) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Constructs the well-balanced tree of gates.]
-
-  Description [Disregards levels and possible logic sharing.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Multi_rec( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Aig_Type_t Type )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    if ( nObjs == 1 )
-        return ppObjs[0];
-    pObj1 = Aig_Multi_rec( p, ppObjs,           nObjs/2,         Type );
-    pObj2 = Aig_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
-    return Aig_Oper( p, pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Old code.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type )
-{
-    assert( Type == AIG_AND || Type == AIG_EXOR );
-    assert( nArgs > 0 );
-    return Aig_Multi_rec( p, pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Implements the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_Miter( Aig_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] = Aig_Not( Aig_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
-    vPairs->nSize = vPairs->nSize/2;
-    return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_AND ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_CreateAnd( Aig_Man_t * p, int nVars )
-{
-    Aig_Obj_t * pFunc;
-    int i;
-    pFunc = Aig_ManConst1( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Aig_And( p, pFunc, Aig_IthVar(p, i) );
-    return pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_CreateOr( Aig_Man_t * p, int nVars )
-{
-    Aig_Obj_t * pFunc;
-    int i;
-    pFunc = Aig_ManConst0( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Aig_Or( p, pFunc, Aig_IthVar(p, i) );
-    return pFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AND function with nVars inputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars )
-{
-    Aig_Obj_t * pFunc;
-    int i;
-    pFunc = Aig_ManConst0( p );
-    for ( i = 0; i < nVars; i++ )
-        pFunc = Aig_Exor( p, pFunc, Aig_IthVar(p, i) );
-    return pFunc;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigTable.c b/src/temp/aig_free/aigTable.c
deleted file mode 100644
index 338faa45..00000000
--- a/src/temp/aig_free/aigTable.c
+++ /dev/null
@@ -1,266 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigTable.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: aigTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// hashing the node
-static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) 
-{
-    unsigned long Key = Aig_ObjIsExor(pObj) * 1699;
-    Key ^= (long)Aig_ObjFanin0(pObj) * 7937;
-    Key ^= (long)Aig_ObjFanin1(pObj) * 2971;
-    Key ^= Aig_ObjFaninC0(pObj) * 911;
-    Key ^= Aig_ObjFaninC1(pObj) * 353;
-    return Key % TableSize;
-}
-
-// returns the place where this node is stored (or should be stored)
-static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int i;
-    assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
-    assert( Aig_ObjChild0(pObj) <  Aig_ObjChild1(pObj) );
-    for ( i = Aig_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
-        if ( p->pTable[i] == pObj )
-            break;
-    return p->pTable + i;
-}
-
-static void         Aig_TableResize( Aig_Man_t * p );
-static unsigned int Cudd_PrimeAig( unsigned int  p );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
- 
-/**Function*************************************************************
-
-  Synopsis    [Checks if node with the given attributes is in the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
-{
-    int i;
-    assert( !Aig_IsComplement(pGhost) );
-    assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
-    assert( Aig_ObjChild0(pGhost) <  Aig_ObjChild1(pGhost) );
-    if ( p->fRefCount && (!Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost))) )
-        return NULL;
-    for ( i = Aig_Hash(pGhost, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
-    {
-        if ( Aig_ObjChild0(p->pTable[i]) == Aig_ObjChild0(pGhost) && 
-             Aig_ObjChild1(p->pTable[i]) == Aig_ObjChild1(pGhost) && 
-             Aig_ObjType(p->pTable[i]) == Aig_ObjType(pGhost) )
-            return p->pTable[i];
-    }
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds the new node to the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t ** ppPlace;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_TableLookup(p, pObj) == NULL );
-    if ( p->nTableSize < 2 * Aig_ManNodeNum(p) )
-        Aig_TableResize( p );
-    ppPlace = Aig_TableFind( p, pObj );
-    assert( *ppPlace == NULL );
-    *ppPlace = pObj;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the node from the hash table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    Aig_Obj_t * pEntry, ** ppPlace;
-    int i;
-    assert( !Aig_IsComplement(pObj) );
-    ppPlace = Aig_TableFind( p, pObj );
-    assert( *ppPlace == pObj ); // node should be in the table
-    *ppPlace = NULL;
-    // rehash the adjacent entries
-    i = ppPlace - p->pTable;
-    for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
-    {
-        pEntry = p->pTable[i];
-        p->pTable[i] = 0;
-        Aig_TableInsert( p, pEntry );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of nodes in the table.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_TableCountEntries( Aig_Man_t * p )
-{
-    int i, Counter = 0;
-    for ( i = 0; i < p->nTableSize; i++ )
-        Counter += (p->pTable[i] != NULL);
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the table.]
-
-  Description [Typically this procedure should not be called.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_TableResize( Aig_Man_t * p )
-{
-    Aig_Obj_t ** pTableOld, ** ppPlace;
-    int nTableSizeOld, Counter, nEntries, e, clk;
-clk = clock();
-    // save the old table
-    pTableOld = p->pTable;
-    nTableSizeOld = p->nTableSize;
-    // get the new table
-    p->nTableSize = Cudd_PrimeAig( 5 * Aig_ManNodeNum(p) ); 
-    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
-    // rehash the entries from the old table
-    Counter = 0;
-    for ( e = 0; e < nTableSizeOld; e++ )
-    {
-        if ( pTableOld[e] == 0 )
-            continue;
-        Counter++;
-        // get the place where this entry goes in the table table
-        ppPlace = Aig_TableFind( p, pTableOld[e] );
-        assert( *ppPlace == NULL ); // should not be in the table
-        *ppPlace = pTableOld[e];
-    }
-    nEntries = Aig_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 Aig_TableProfile( Aig_Man_t * p )
-{
-    int i, Counter = 0;
-    for ( i = 0; i < p->nTableSize; i++ )
-    {
-        if ( p->pTable[i] )
-            Counter++;
-        else if ( Counter )
-        {
-            printf( "%d ", Counter );
-            Counter = 0;
-        }
-    }
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime &gt;= p.]
-
-  Description [Copied from CUDD, for stand-aloneness.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-unsigned int Cudd_PrimeAig( unsigned int  p)
-{
-    int i,pn;
-
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/aigUtil.c b/src/temp/aig_free/aigUtil.c
deleted file mode 100644
index 623de32b..00000000
--- a/src/temp/aig_free/aigUtil.c
+++ /dev/null
@@ -1,513 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigUtil.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: aigUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-
-int Extra_Base10Log( unsigned Num )
-{
-    int Res;
-    assert( Num >= 0 );
-    if ( Num == 0 ) return 0;
-    if ( Num == 1 ) return 1;
-    for ( Res = 0, Num--;  Num;  Num /= 10,  Res++ );
-    return Res;
-} /* end of Extra_Base2Log */
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Increments the current traversal ID of the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManIncrementTravId( Aig_Man_t * p )
-{
-    if ( p->nTravIds >= (1<<30)-1 )
-        Aig_ManCleanData( p );
-    p->nTravIds++;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the DFS ordering of the nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManCleanData( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    p->nTravIds = 1;
-    Aig_ManConst1(p)->pData = NULL;
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = NULL;
-    Aig_ManForEachPo( p, pObj, i )
-        pObj->pData = NULL;
-    Aig_ManForEachNode( p, pObj, i )
-        pObj->pData = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detects multi-input gate rooted at this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
-    {
-        Vec_PtrPushUnique(vSuper, pObj);
-        return;
-    }
-    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
-    Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Detects multi-input gate rooted at this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
-{
-    assert( !Aig_IsComplement(pRoot) );
-    Vec_PtrClear( vSuper );
-    Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
-{
-    Aig_Obj_t * pNode0, * pNode1;
-    // check that the node is regular
-    assert( !Aig_IsComplement(pNode) );
-    // if the node is not AND, this is not MUX
-    if ( !Aig_ObjIsAnd(pNode) )
-        return 0;
-    // if the children are not complemented, this is not MUX
-    if ( !Aig_ObjFaninC0(pNode) || !Aig_ObjFaninC1(pNode) )
-        return 0;
-    // get children
-    pNode0 = Aig_ObjFanin0(pNode);
-    pNode1 = Aig_ObjFanin1(pNode);
-    // if the children are not ANDs, this is not MUX
-    if ( !Aig_ObjIsAnd(pNode0) || !Aig_ObjIsAnd(pNode1) )
-        return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
-    return (Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1))) || 
-           (Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1))) ||
-           (Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1))) ||
-           (Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recognizes what nodes are inputs of the EXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
-{
-    Aig_Obj_t * p0, * p1;
-    assert( !Aig_IsComplement(pObj) );
-    if ( !Aig_ObjIsNode(pObj) )
-        return 0;
-    if ( Aig_ObjIsExor(pObj) )
-    {
-        *ppFan0 = Aig_ObjChild0(pObj);
-        *ppFan1 = Aig_ObjChild1(pObj);
-        return 1;
-    }
-    assert( Aig_ObjIsAnd(pObj) );
-    p0 = Aig_ObjChild0(pObj);
-    p1 = Aig_ObjChild1(pObj);
-    if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
-        return 0;
-    p0 = Aig_Regular(p0);
-    p1 = Aig_Regular(p1);
-    if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
-        return 0;
-    if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
-        return 0;
-    if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
-        return 0;
-    *ppFan0 = Aig_ObjChild0(p0);
-    *ppFan1 = Aig_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     []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Obj_t ** ppNodeE )
-{
-    Aig_Obj_t * pNode0, * pNode1;
-    assert( !Aig_IsComplement(pNode) );
-    assert( Aig_ObjIsMuxType(pNode) );
-    // get children
-    pNode0 = Aig_ObjFanin0(pNode);
-    pNode1 = Aig_ObjFanin1(pNode);
-
-    // find the control variable
-    if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Aig_ObjFaninC1(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
-            return Aig_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
-            return Aig_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Aig_ObjFaninC0(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
-            return Aig_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
-            return Aig_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-    else if ( Aig_ObjFanin0(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC0(pNode0) ^ Aig_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Aig_ObjFaninC0(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
-            return Aig_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode1));//pNode2->p1);
-            return Aig_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-    else if ( Aig_ObjFanin1(pNode0) == Aig_ObjFanin0(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Aig_ObjFaninC1(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
-            return Aig_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Aig_Not(Aig_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Aig_Not(Aig_ObjChild1(pNode1));//pNode2->p2);
-            return Aig_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    assert( 0 ); // this is not MUX
-    return NULL;
-}
-
-
-/**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 Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
-{
-    Vec_Ptr_t * vSuper;
-    Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
-    int fCompl, i;
-    // store the complemented attribute
-    fCompl = Aig_IsComplement(pObj);
-    pObj = Aig_Regular(pObj);
-    // constant case
-    if ( Aig_ObjIsConst1(pObj) )
-    {
-        fprintf( pFile, "%d", !fCompl );
-        return;
-    }
-    // PI case
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData );
-        return;
-    }
-    // EXOR case
-    if ( Aig_ObjIsExor(pObj) )
-    {
-        Vec_VecExpand( vLevels, Level );
-        vSuper = Vec_VecEntry( vLevels, Level );
-        Aig_ObjCollectMulti( pObj, vSuper );
-        fprintf( pFile, "%s", (Level==0? "" : "(") );
-        Vec_PtrForEachEntry( vSuper, pFanin, i )
-        {
-            Aig_ObjPrintVerilog( pFile, Aig_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 ( Aig_ObjIsMuxType(pObj) )
-    {
-        if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
-        {
-            fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
-            fprintf( pFile, " ^ " );
-            Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
-            fprintf( pFile, "%s", (Level==0? "" : ")") );
-        }
-        else 
-        {
-            pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
-            fprintf( pFile, "%s", (Level==0? "" : "(") );
-            Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
-            fprintf( pFile, " ? " );
-            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
-            fprintf( pFile, " : " );
-            Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
-            fprintf( pFile, "%s", (Level==0? "" : ")") );
-        }
-        return;
-    }
-    // AND case
-    Vec_VecExpand( vLevels, Level );
-    vSuper = Vec_VecEntry(vLevels, Level);
-    Aig_ObjCollectMulti( pObj, vSuper );
-    fprintf( pFile, "%s", (Level==0? "" : "(") );
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        Aig_ObjPrintVerilog( pFile, Aig_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 Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
-{
-    assert( !Aig_IsComplement(pObj) );
-    printf( "Node %p : ", pObj );
-    if ( Aig_ObjIsConst1(pObj) )
-        printf( "constant 1" );
-    else if ( Aig_ObjIsPi(pObj) )
-        printf( "PI" );
-    else
-        printf( "AND( %p%s, %p%s )", 
-            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), 
-            Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") );
-    printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints node in HAIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    printf( "PIs: " );
-    Aig_ManForEachPi( p, pObj, i )
-        printf( " %p", pObj );
-    printf( "\n" );
-    vNodes = Aig_ManDfs( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the AIG into the BLIF file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
-{
-    FILE * pFile;
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj, * pConst1 = NULL;
-    int i, nDigits, Counter = 0;
-    if ( Aig_ManPoNum(p) == 0 )
-    {
-        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
-        return;
-    }
-    // collect nodes in the DFS order
-    vNodes = Aig_ManDfs( p );
-    // assign IDs to objects
-    Aig_ManConst1(p)->pData = (void *)Counter++;
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = (void *)Counter++;
-    Aig_ManForEachPo( p, pObj, i )
-        pObj->pData = (void *)Counter++;
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = (void *)Counter++;
-    nDigits = Extra_Base10Log( Counter );
-    // write the file
-    pFile = fopen( pFileName, "w" );
-    fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif() in ABC\n" );
-    fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
-    fprintf( pFile, ".model test\n" );
-    // write PIs
-    fprintf( pFile, ".inputs" );
-    Aig_ManForEachPi( p, pObj, i )
-        fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData );
-    fprintf( pFile, "\n" );
-    // write POs
-    fprintf( pFile, ".outputs" );
-    Aig_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)Aig_ObjFanin0(pObj)->pData, 
-            nDigits, (int)Aig_ObjFanin1(pObj)->pData, 
-            nDigits, (int)pObj->pData );
-        fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
-    }
-    // write POs
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        fprintf( pFile, ".names n%0*d n%0*d\n", 
-            nDigits, (int)Aig_ObjFanin0(pObj)->pData, 
-            nDigits, (int)pObj->pData );
-        fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
-        if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
-            pConst1 = Aig_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/temp/aig_free/cudd2.c b/src/temp/aig_free/cudd2.c
deleted file mode 100644
index f95d3fd0..00000000
--- a/src/temp/aig_free/cudd2.c
+++ /dev/null
@@ -1,375 +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 "aig.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;
-    assert( s_pCuddMan == NULL );
-    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    [Creates equivalent of BDD.ONE and BDD.ReadZero.]
-
-  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 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Should be called each time a BDD node is dereferenced.]
-
-  Description [Removes mapping of a BDD node into an AIG node when the BDD
-  node is dereferenced.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cudd2_RecursiveDeref( void * pCudd, void * pArg )
-{
-    assert( s_pCuddMan != NULL );
-    assert( st_is_member(s_pCuddMan->pTable, (char *)Aig_Regular(pArg)) );
-    st_delete( s_pCuddMan->pTable, (char *)Aig_Regular(pArg), NULL );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/temp/aig_free/cudd2.h b/src/temp/aig_free/cudd2.h
deleted file mode 100644
index c80ec5ed..00000000
--- a/src/temp/aig_free/cudd2.h
+++ /dev/null
@@ -1,83 +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/temp/aig_free/st.c b/src/temp/aig_free/st.c
deleted file mode 100644
index 5024e08d..00000000
--- a/src/temp/aig_free/st.c
+++ /dev/null
@@ -1,626 +0,0 @@
-/*
- * Revision Control Information
- *
- * /projects/hsis/CVS/utilities/st/st.c,v
- * serdar
- * 1.1
- * 1993/07/29 01:00:13
- *
- */
-#include <stdio.h>
-
-#include <stdlib.h>
-//#include "extra.h"
-#include "st.h"
-
-#ifndef ABS
-#  define ABS(a)            ((a) < 0 ? -(a) : (a))
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
-
-#define ST_NUMCMP(x,y) ((x) != (y))
-#define ST_NUMHASH(x,size) (ABS((long)x)%(size))
-#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size)
-#define EQUAL(func, x, y) \
-    ((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\
-      (ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0))
-
-
-#define do_hash(key, table)\
-    ((table->hash == st_ptrhash) ? ST_PTRHASH((key),(table)->num_bins) :\
-     (table->hash == st_numhash) ? ST_NUMHASH((key), (table)->num_bins) :\
-     (*table->hash)((key), (table)->num_bins))
-
-static int rehash();
-int st_numhash(), st_ptrhash(), st_numcmp(), st_ptrcmp();
-
-st_table *
-st_init_table_with_params(compare, hash, size, density, grow_factor,
-              reorder_flag)
-int (*compare)();
-int (*hash)();
-int size;
-int density;
-double grow_factor;
-int reorder_flag;
-{
-    int i;
-    st_table *new;
-
-    new = ALLOC(st_table, 1);
-    if (new == NULL) {
-    return NULL;
-    }
-    new->compare = compare;
-    new->hash = hash;
-    new->num_entries = 0;
-    new->max_density = density;
-    new->grow_factor = grow_factor;
-    new->reorder_flag = reorder_flag;
-    if (size <= 0) {
-    size = 1;
-    }
-    new->num_bins = size;
-    new->bins = ALLOC(st_table_entry *, size);
-    if (new->bins == NULL) {
-    FREE(new);
-    return NULL;
-    }
-    for(i = 0; i < size; i++) {
-    new->bins[i] = 0;
-    }
-    return new;
-}
-
-st_table *
-st_init_table(compare, hash)
-int (*compare)();
-int (*hash)();
-{
-    return st_init_table_with_params(compare, hash, ST_DEFAULT_INIT_TABLE_SIZE,
-                     ST_DEFAULT_MAX_DENSITY,
-                     ST_DEFAULT_GROW_FACTOR,
-                     ST_DEFAULT_REORDER_FLAG);
-}
-                
-void
-st_free_table(table)
-st_table *table;
-{
-    register st_table_entry *ptr, *next;
-    int i;
-
-    for(i = 0; i < table->num_bins ; i++) {
-    ptr = table->bins[i];
-    while (ptr != NULL) {
-        next = ptr->next;
-        FREE(ptr);
-        ptr = next;
-    }
-    }
-    FREE(table->bins);
-    FREE(table);
-}
-
-#define PTR_NOT_EQUAL(table, ptr, user_key)\
-(ptr != NULL && !EQUAL(table->compare, user_key, (ptr)->key))
-
-#define FIND_ENTRY(table, hash_val, key, ptr, last) \
-    (last) = &(table)->bins[hash_val];\
-    (ptr) = *(last);\
-    while (PTR_NOT_EQUAL((table), (ptr), (key))) {\
-    (last) = &(ptr)->next; (ptr) = *(last);\
-    }\
-    if ((ptr) != NULL && (table)->reorder_flag) {\
-    *(last) = (ptr)->next;\
-    (ptr)->next = (table)->bins[hash_val];\
-    (table)->bins[hash_val] = (ptr);\
-    }
-
-int
-st_lookup(table, key, value)
-st_table *table;
-register char *key;
-char **value;
-{
-    int hash_val;
-    register st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr, last);
-    
-    if (ptr == NULL) {
-    return 0;
-    } else {
-    if (value != NULL) {
-        *value = ptr->record; 
-    }
-    return 1;
-    }
-}
-
-int
-st_lookup_int(table, key, value)
-st_table *table;
-register char *key;
-int *value;
-{
-    int hash_val;
-    register st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr, last);
-    
-    if (ptr == NULL) {
-    return 0;
-    } else {
-    if (value != 0) {
-        *value = (long) ptr->record;
-    }
-    return 1;
-    }
-}
-
-/* This macro does not check if memory allocation fails. Use at you own risk */
-#define ADD_DIRECT(table, key, value, hash_val, new)\
-{\
-    if (table->num_entries/table->num_bins >= table->max_density) {\
-    rehash(table);\
-    hash_val = do_hash(key,table);\
-    }\
-    \
-    new = ALLOC(st_table_entry, 1);\
-    \
-    new->key = key;\
-    new->record = value;\
-    new->next = table->bins[hash_val];\
-    table->bins[hash_val] = new;\
-    table->num_entries++;\
-}
-
-int
-st_insert(table, key, value)
-register st_table *table;
-register char *key;
-char *value;
-{
-    int hash_val;
-    st_table_entry *new;
-    register st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr, last);
-
-    if (ptr == NULL) {
-    if (table->num_entries/table->num_bins >= table->max_density) {
-        if (rehash(table) == ST_OUT_OF_MEM) {
-        return ST_OUT_OF_MEM;
-        }
-        hash_val = do_hash(key, table);
-    }
-    new = ALLOC(st_table_entry, 1);
-    if (new == NULL) {
-        return ST_OUT_OF_MEM;
-    }
-    new->key = key;
-    new->record = value;
-    new->next = table->bins[hash_val];
-    table->bins[hash_val] = new;
-    table->num_entries++;
-    return 0;
-    } else {
-    ptr->record = value;
-    return 1;
-    }
-}
-
-int
-st_add_direct(table, key, value)
-st_table *table;
-char *key;
-char *value;
-{
-    int hash_val;
-    st_table_entry *new;
-    
-    hash_val = do_hash(key, table);
-    if (table->num_entries / table->num_bins >= table->max_density) {
-    if (rehash(table) == ST_OUT_OF_MEM) {
-        return ST_OUT_OF_MEM;
-    }
-    }
-    hash_val = do_hash(key, table);
-    new = ALLOC(st_table_entry, 1);
-    if (new == NULL) {
-    return ST_OUT_OF_MEM;
-    }
-    new->key = key;
-    new->record = value;
-    new->next = table->bins[hash_val];
-    table->bins[hash_val] = new;
-    table->num_entries++;
-    return 1;
-}
-
-int
-st_find_or_add(table, key, slot)
-st_table *table;
-char *key;
-char ***slot;
-{
-    int hash_val;
-    st_table_entry *new, *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr, last);
-
-    if (ptr == NULL) {
-    if (table->num_entries / table->num_bins >= table->max_density) {
-        if (rehash(table) == ST_OUT_OF_MEM) {
-        return ST_OUT_OF_MEM;
-        }
-        hash_val = do_hash(key, table);
-    }
-    new = ALLOC(st_table_entry, 1);
-    if (new == NULL) {
-        return ST_OUT_OF_MEM;
-    }
-    new->key = key;
-    new->record = (char *) 0;
-    new->next = table->bins[hash_val];
-    table->bins[hash_val] = new;
-    table->num_entries++;
-    if (slot != NULL) *slot = &new->record;
-    return 0;
-    } else {
-    if (slot != NULL) *slot = &ptr->record;
-    return 1;
-    }
-}
-
-int
-st_find(table, key, slot)
-st_table *table;
-char *key;
-char ***slot;
-{
-    int hash_val;
-    st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr, last);
-
-    if (ptr == NULL) {
-    return 0;
-    } else {
-    if (slot != NULL) {
-        *slot = &ptr->record;
-    }
-    return 1;
-    }
-}
-
-static int
-rehash(table)
-register st_table *table;
-{
-    register st_table_entry *ptr, *next, **old_bins;
-    int             i, old_num_bins, hash_val, old_num_entries;
-
-    /* save old values */
-    old_bins = table->bins;
-    old_num_bins = table->num_bins;
-    old_num_entries = table->num_entries;
-
-    /* rehash */
-    table->num_bins = (int)(table->grow_factor * old_num_bins);
-    if (table->num_bins % 2 == 0) {
-    table->num_bins += 1;
-    }
-    table->num_entries = 0;
-    table->bins = ALLOC(st_table_entry *, table->num_bins);
-    if (table->bins == NULL) {
-    table->bins = old_bins;
-    table->num_bins = old_num_bins;
-    table->num_entries = old_num_entries;
-    return ST_OUT_OF_MEM;
-    }
-    /* initialize */
-    for (i = 0; i < table->num_bins; i++) {
-    table->bins[i] = 0;
-    }
-
-    /* copy data over */
-    for (i = 0; i < old_num_bins; i++) {
-    ptr = old_bins[i];
-    while (ptr != NULL) {
-        next = ptr->next;
-        hash_val = do_hash(ptr->key, table);
-        ptr->next = table->bins[hash_val];
-        table->bins[hash_val] = ptr;
-        table->num_entries++;
-        ptr = next;
-    }
-    }
-    FREE(old_bins);
-
-    return 1;
-}
-
-st_table *
-st_copy(old_table)
-st_table *old_table;
-{
-    st_table *new_table;
-    st_table_entry *ptr, *newptr, *next, *new;
-    int i, j, num_bins = old_table->num_bins;
-
-    new_table = ALLOC(st_table, 1);
-    if (new_table == NULL) {
-    return NULL;
-    }
-    
-    *new_table = *old_table;
-    new_table->bins = ALLOC(st_table_entry *, num_bins);
-    if (new_table->bins == NULL) {
-    FREE(new_table);
-    return NULL;
-    }
-    for(i = 0; i < num_bins ; i++) {
-    new_table->bins[i] = NULL;
-    ptr = old_table->bins[i];
-    while (ptr != NULL) {
-        new = ALLOC(st_table_entry, 1);
-        if (new == NULL) {
-        for (j = 0; j <= i; j++) {
-            newptr = new_table->bins[j];
-            while (newptr != NULL) {
-            next = newptr->next;
-            FREE(newptr);
-            newptr = next;
-            }
-        }
-        FREE(new_table->bins);
-        FREE(new_table);
-        return NULL;
-        }
-        *new = *ptr;
-        new->next = new_table->bins[i];
-        new_table->bins[i] = new;
-        ptr = ptr->next;
-    }
-    }
-    return new_table;
-}
-
-int
-st_delete(table, keyp, value)
-register st_table *table;
-register char **keyp;
-char **value;
-{
-    int hash_val;
-    char *key = *keyp;
-    register st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr ,last);
-    
-    if (ptr == NULL) {
-    return 0;
-    }
-
-    *last = ptr->next;
-    if (value != NULL) *value = ptr->record;
-    *keyp = ptr->key;
-    FREE(ptr);
-    table->num_entries--;
-    return 1;
-}
-
-int
-st_delete_int(table, keyp, value)
-register st_table *table;
-register long *keyp;
-char **value;
-{
-    int hash_val;
-    char *key = (char *) *keyp;
-    register st_table_entry *ptr, **last;
-
-    hash_val = do_hash(key, table);
-
-    FIND_ENTRY(table, hash_val, key, ptr ,last);
-
-    if (ptr == NULL) {
-        return 0;
-    }
-
-    *last = ptr->next;
-    if (value != NULL) *value = ptr->record;
-    *keyp = (long) ptr->key;
-    FREE(ptr);
-    table->num_entries--;
-    return 1;
-}
-
-int
-st_foreach(table, func, arg)
-st_table *table;
-enum st_retval (*func)();
-char *arg;
-{
-    st_table_entry *ptr, **last;
-    enum st_retval retval;
-    int i;
-
-    for(i = 0; i < table->num_bins; i++) {
-    last = &table->bins[i]; ptr = *last;
-    while (ptr != NULL) {
-        retval = (*func)(ptr->key, ptr->record, arg);
-        switch (retval) {
-        case ST_CONTINUE:
-        last = &ptr->next; ptr = *last;
-        break;
-        case ST_STOP:
-        return 0;
-        case ST_DELETE:
-        *last = ptr->next;
-        table->num_entries--;    /* cstevens@ic */
-        FREE(ptr);
-        ptr = *last;
-        }
-    }
-    }
-    return 1;
-}
-
-int
-st_strhash(string, modulus)
-register char *string;
-int modulus;
-{
-    register int val = 0;
-    register int c;
-    
-    while ((c = *string++) != '\0') {
-    val = val*997 + c;
-    }
-
-    return ((val < 0) ? -val : val)%modulus;
-}
-
-int
-st_numhash(x, size)
-char *x;
-int size;
-{
-    return ST_NUMHASH(x, size);
-}
-
-int
-st_ptrhash(x, size)
-char *x;
-int size;
-{
-    return ST_PTRHASH(x, size);
-}
-
-int
-st_numcmp(x, y)
-char *x;
-char *y;
-{
-    return ST_NUMCMP(x, y);
-}
-
-int
-st_ptrcmp(x, y)
-char *x;
-char *y;
-{
-    return ST_NUMCMP(x, y);
-}
-
-st_generator *
-st_init_gen(table)
-st_table *table;
-{
-    st_generator *gen;
-
-    gen = ALLOC(st_generator, 1);
-    if (gen == NULL) {
-    return NULL;
-    }
-    gen->table = table;
-    gen->entry = NULL;
-    gen->index = 0;
-    return gen;
-}
-
-
-int 
-st_gen(gen, key_p, value_p)
-st_generator *gen;
-char **key_p;
-char **value_p;
-{
-    register int i;
-
-    if (gen->entry == NULL) {
-    /* try to find next entry */
-    for(i = gen->index; i < gen->table->num_bins; i++) {
-        if (gen->table->bins[i] != NULL) {
-        gen->index = i+1;
-        gen->entry = gen->table->bins[i];
-        break;
-        }
-    }
-    if (gen->entry == NULL) {
-        return 0;        /* that's all folks ! */
-    }
-    }
-    *key_p = gen->entry->key;
-    if (value_p != 0) {
-    *value_p = gen->entry->record;
-    }
-    gen->entry = gen->entry->next;
-    return 1;
-}
-
-
-int 
-st_gen_int(gen, key_p, value_p)
-st_generator *gen;
-char **key_p;
-long *value_p;
-{
-    register int i;
-
-    if (gen->entry == NULL) {
-    /* try to find next entry */
-    for(i = gen->index; i < gen->table->num_bins; i++) {
-        if (gen->table->bins[i] != NULL) {
-        gen->index = i+1;
-        gen->entry = gen->table->bins[i];
-        break;
-        }
-    }
-    if (gen->entry == NULL) {
-        return 0;        /* that's all folks ! */
-    }
-    }
-    *key_p = gen->entry->key;
-    if (value_p != 0) {
-       *value_p = (long) gen->entry->record;
-    }
-    gen->entry = gen->entry->next;
-    return 1;
-}
-
-
-void
-st_free_gen(gen)
-st_generator *gen;
-{
-    FREE(gen);
-}
diff --git a/src/temp/aig_free/st.h b/src/temp/aig_free/st.h
deleted file mode 100644
index b15f3c83..00000000
--- a/src/temp/aig_free/st.h
+++ /dev/null
@@ -1,96 +0,0 @@
-/*
- * Revision Control Information
- *
- * /projects/hsis/CVS/utilities/st/st.h,v
- * serdar
- * 1.1
- * 1993/07/29 01:00:21
- *
- */
-/* LINTLIBRARY */
-
-/* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
-
-#ifndef ST_INCLUDED
-#define ST_INCLUDED
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-typedef struct st_table_entry st_table_entry;
-struct st_table_entry {
-    char *key;
-    char *record;
-    st_table_entry *next;
-};
-
-typedef struct st_table st_table;
-struct st_table {
-    int (*compare)();
-    int (*hash)();
-    int num_bins;
-    int num_entries;
-    int max_density;
-    int reorder_flag;
-    double grow_factor;
-    st_table_entry **bins;
-};
-
-typedef struct st_generator st_generator;
-struct st_generator {
-    st_table *table;
-    st_table_entry *entry;
-    int index;
-};
-
-#define st_is_member(table,key) st_lookup(table,key,(char **) 0)
-#define st_count(table) ((table)->num_entries)
-
-enum st_retval {ST_CONTINUE, ST_STOP, ST_DELETE};
-
-typedef enum st_retval (*ST_PFSR)();
-typedef int (*ST_PFI)();
-
-extern st_table *st_init_table_with_params (ST_PFI, ST_PFI, int, int, double, int);
-extern st_table *st_init_table (ST_PFI, ST_PFI); 
-extern void st_free_table (st_table *);
-extern int st_lookup (st_table *, char *, char **);
-extern int st_lookup_int (st_table *, char *, int *);
-extern int st_insert (st_table *, char *, char *);
-extern int st_add_direct (st_table *, char *, char *);
-extern int st_find_or_add (st_table *, char *, char ***);
-extern int st_find (st_table *, char *, char ***);
-extern st_table *st_copy (st_table *);
-extern int st_delete (st_table *, char **, char **);
-extern int st_delete_int (st_table *, long *, char **);
-extern int st_foreach (st_table *, ST_PFSR, char *);
-extern int st_strhash (char *, int);
-extern int st_numhash (char *, int);
-extern int st_ptrhash (char *, int);
-extern int st_numcmp (char *, char *);
-extern int st_ptrcmp (char *, char *);
-extern st_generator *st_init_gen (st_table *);
-extern int st_gen (st_generator *, char **, char **);
-extern int st_gen_int (st_generator *, char **, long *);
-extern void st_free_gen (st_generator *);
-
-
-#define ST_DEFAULT_MAX_DENSITY 5
-#define ST_DEFAULT_INIT_TABLE_SIZE 11
-#define ST_DEFAULT_GROW_FACTOR 2.0
-#define ST_DEFAULT_REORDER_FLAG 0
-
-#define st_foreach_item(table, gen, key, value) \
-    for(gen=st_init_gen(table); st_gen(gen,key,value) || (st_free_gen(gen),0);)
-
-#define st_foreach_item_int(table, gen, key, value) \
-    for(gen=st_init_gen(table); st_gen_int(gen,key,value) || (st_free_gen(gen),0);)
-
-#define ST_OUT_OF_MEM -10000
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif /* ST_INCLUDED */
diff --git a/src/temp/aig_free/subdir.mk b/src/temp/aig_free/subdir.mk
deleted file mode 100644
index 1867f777..00000000
--- a/src/temp/aig_free/subdir.mk
+++ /dev/null
@@ -1,87 +0,0 @@
-################################################################################
-# Automatically-generated file. Do not edit!
-################################################################################
-
-INCPATHS = -I$(ROOT)/aig-alan
-
-# Add inputs and outputs from these tool invocations to the build variables 
-PURE_C_SRCS += \
-${addprefix $(ROOT)/aig-alan/, \
-aigBalance.c \
-aigCheck.c \
-aigDfs.c \
-aigMan.c \
-aigMem.c \
-aigObj.c \
-aigOper.c \
-aigTable.c \
-aigUtil.c \
-cudd2.c \
-st.c \
-}
-
-C_SRCS += $(PURE_C_SRCS)
-
-
-PURE_C_OBJS += \
-${addprefix $(ROOT)/obj/aig-alan/, \
-aigBalance.o \
-aigCheck.o \
-aigDfs.o \
-aigMan.o \
-aigMem.o \
-aigObj.o \
-aigOper.o \
-aigTable.o \
-aigUtil.o \
-cudd2.o \
-st.o \
-}
-
-OBJS += $(PURE_C_OBJS) 
-
-PURE_C_DEPS += \
-${addprefix $(ROOT)/obj/aig-alan, \
-aigBalance.d \
-aigCheck.d \
-aigDfs.d \
-aigMan.d \
-aigMem.d \
-aigObj.d \
-aigOper.d \
-aigTable.d \
-aigUtil.d \
-cudd2.d \
-st.d \
-}
-
-DEPS += $(PURE_C_DEPS)
-
-
-OCAML_OBJS += 
-
-
-DEPEND_SRCS += 
-
-# Each subdirectory must supply rules for building sources it contributes
-$(ROOT)/obj/aig-alan/%.o: $(ROOT)/aig-alan/%.c
-	@echo 'Building file: $<'
-	@echo 'Invoking: GCC C Compiler: $(CC)'
-	@echo $(CC) $(GPCC_OPTS) $(INCPATHS)  -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $<
-	@$(CC)  $(GPCC_OPTS)  $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $< && \
-	echo -n $(@:%.o=%.d) $(dir $@) > $(@:%.o=%.d) && \
-	$(CC) -MM -MG -P -w  $(GPCC_OPTS) $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0  $< >> $(@:%.o=%.d)
-	@echo 'Finished building: $<'
-	@echo ' '
-
-$(ROOT)/obj/aig-alan/%.o: $(ROOT)/aig-alan/%.cpp
-	@echo 'Building file: $<'
-	@echo 'Invoking: G++ C Compiler: $(GPCC)'
-	@echo $(GPPCC) $(GPCC_OPTS) $(INCPATHS)  -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $<
-	@$(GPPCC)  $(GPCC_OPTS)  $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $< && \
-	echo -n $(@:%.o=%.d) $(dir $@) > $(@:%.o=%.d) && \
-	$(GPPCC) -MM -MG -P -w  $(GPCC_OPTS) $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0  $< >> $(@:%.o=%.d)
-	@echo 'Finished building: $<'
-	@echo ' '
-
-
diff --git a/src/temp/aig_free/vec.h b/src/temp/aig_free/vec.h
deleted file mode 100644
index 61737d3a..00000000
--- a/src/temp/aig_free/vec.h
+++ /dev/null
@@ -1,82 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vec.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_H__
-#define __VEC_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef _WIN32
-#define inline __inline // compatible with MS VS 6.0
-#endif
-
-#ifndef ALLOC
-#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
-#endif
-
-#ifndef FREE
-#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
-#endif
-
-#ifndef REALLOC
-#define REALLOC(type, obj, num)    \
-        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
-         ((type *) malloc(sizeof(type) * (num))))
-#endif
-
-
-#include "vecInt.h"
-#include "vecFlt.h"
-#include "vecStr.h"
-#include "vecPtr.h"
-#include "vecVec.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/aig_free/vecFlt.h b/src/temp/aig_free/vecFlt.h
deleted file mode 100644
index 6d92d824..00000000
--- a/src/temp/aig_free/vecFlt.h
+++ /dev/null
@@ -1,667 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecFlt.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Resizable arrays of floats.]
-
-  Author      [Aaron P. Hurst]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_FLT_H__
-#define __VEC_FLT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-//#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Vec_Flt_t_       Vec_Flt_t;
-struct Vec_Flt_t_ 
-{
-    int              nCap;
-    int              nSize;
-    float *          pArray;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#define Vec_FltForEachEntry( vVec, Entry, i )                                               \
-    for ( i = 0; (i < Vec_FltSize(vVec)) && (((Entry) = Vec_FltEntry(vVec, i)), 1); i++ )
-#define Vec_FltForEachEntryStart( vVec, Entry, i, Start )                                   \
-    for ( i = Start; (i < Vec_FltSize(vVec)) && (((Entry) = Vec_FltEntry(vVec, i)), 1); i++ )
-#define Vec_FltForEachEntryStartStop( vVec, Entry, i, Start, Stop )                         \
-    for ( i = Start; (i < Stop) && (((Entry) = Vec_FltEntry(vVec, i)), 1); i++ )
-#define Vec_FltForEachEntryReverse( vVec, pEntry, i )                                       \
-    for ( i = Vec_FltSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_FltEntry(vVec, i)), 1); i-- )
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltAlloc( int nCap )
-{
-    Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
-    if ( nCap > 0 && nCap < 16 )
-        nCap = 16;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( float, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given size and cleans it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltStart( int nSize )
-{
-    Vec_Flt_t * p;
-    p = Vec_FltAlloc( nSize );
-    p->nSize = nSize;
-    memset( p->pArray, 0, sizeof(float) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from a float array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltAllocArray( float * pArray, int nSize )
-{
-    Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = pArray;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from a float array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltAllocArrayCopy( float * pArray, int nSize )
-{
-    Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = ALLOC( float, nSize );
-    memcpy( p->pArray, pArray, sizeof(float) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the float array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltDup( Vec_Flt_t * pVec )
-{
-    Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( float, p->nCap ) : NULL;
-    memcpy( p->pArray, pVec->pArray, sizeof(float) * pVec->nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the array into another vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Flt_t * Vec_FltDupArray( Vec_Flt_t * pVec )
-{
-    Vec_Flt_t * p;
-    p = ALLOC( Vec_Flt_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = pVec->pArray;
-    pVec->nSize  = 0;
-    pVec->nCap   = 0;
-    pVec->pArray = NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltFree( Vec_Flt_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline float * Vec_FltReleaseArray( Vec_Flt_t * p )
-{
-    float * pArray = p->pArray;
-    p->nCap = 0;
-    p->nSize = 0;
-    p->pArray = NULL;
-    return pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline float * Vec_FltArray( Vec_Flt_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltSize( Vec_Flt_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline float Vec_FltEntry( Vec_Flt_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltWriteEntry( Vec_Flt_t * p, int i, float Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltAddToEntry( Vec_Flt_t * p, int i, float Addition )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] += Addition;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline float Vec_FltEntryLast( Vec_Flt_t * p )
-{
-    return p->pArray[p->nSize-1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltGrow( Vec_Flt_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( float, p->pArray, nCapMin ); 
-    p->nCap   = nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltFill( Vec_Flt_t * p, int nSize, float Entry )
-{
-    int i;
-    Vec_FltGrow( p, nSize );
-    for ( i = 0; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltFillExtra( Vec_Flt_t * p, int nSize, float Entry )
-{
-    int i;
-    if ( p->nSize >= nSize )
-        return;
-    Vec_FltGrow( p, nSize );
-    for ( i = p->nSize; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltShrink( Vec_Flt_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltClear( Vec_Flt_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltPush( Vec_Flt_t * p, float Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_FltGrow( p, 16 );
-        else
-            Vec_FltGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-// HA: Commented as proposed by Alan M. 
-// static inline void Vec_FltPushMem( Extra_MmStep_t * pMemMan, Vec_Flt_t * p, float Entry )
-// {
-//     if ( p->nSize == p->nCap )
-//     {
-//         float * pArray;
-//         int i;
-
-//         if ( p->nSize == 0 )
-//             p->nCap = 1;
-//         pArray = (float *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
-// //        pArray = ALLOC( float, p->nCap * 2 );
-//         if ( p->pArray )
-//         {
-//             for ( i = 0; i < p->nSize; i++ )
-//                 pArray[i] = p->pArray[i];
-//             Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
-// //            free( p->pArray );
-//         }
-//         p->nCap *= 2;
-//         p->pArray = pArray;
-//     }
-//     p->pArray[p->nSize++] = Entry;
-// }
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltPushOrder( Vec_Flt_t * p, float Entry )
-{
-    int i;
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_FltGrow( p, 16 );
-        else
-            Vec_FltGrow( p, 2 * p->nCap );
-    }
-    p->nSize++;
-    for ( i = p->nSize-2; i >= 0; i-- )
-        if ( p->pArray[i] > Entry )
-            p->pArray[i+1] = p->pArray[i];
-        else
-            break;
-    p->pArray[i+1] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltPushUnique( Vec_Flt_t * p, float Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return 1;
-    Vec_FltPush( p, Entry );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the last entry and removes it from the list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline float Vec_FltPop( Vec_Flt_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find entry.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltFind( Vec_Flt_t * p, float Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return i;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltRemove( Vec_Flt_t * p, float Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            break;
-    if ( i == p->nSize )
-        return 0;
-    assert( i < p->nSize );
-    for ( i++; i < p->nSize; i++ )
-        p->pArray[i-1] = p->pArray[i];
-    p->nSize--;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two floats.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltSortCompare1( float * pp1, float * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two floats.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_FltSortCompare2( float * pp1, float * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 > *pp2 )
-        return -1;
-    if ( *pp1 < *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_FltSort( Vec_Flt_t * p, int fReverse )
-{
-    if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(float), 
-                (int (*)(const void *, const void *)) Vec_FltSortCompare2 );
-    else
-        qsort( (void *)p->pArray, p->nSize, sizeof(float), 
-                (int (*)(const void *, const void *)) Vec_FltSortCompare1 );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-#endif
-
diff --git a/src/temp/aig_free/vecInt.h b/src/temp/aig_free/vecInt.h
deleted file mode 100644
index 77bf5849..00000000
--- a/src/temp/aig_free/vecInt.h
+++ /dev/null
@@ -1,781 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecInt.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Resizable arrays of integers.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_INT_H__
-#define __VEC_INT_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-//HA: Commented as advised by Alan
-//#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Vec_Int_t_       Vec_Int_t;
-struct Vec_Int_t_ 
-{
-    int              nCap;
-    int              nSize;
-    int *            pArray;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#define Vec_IntForEachEntry( vVec, Entry, i )                                               \
-    for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
-#define Vec_IntForEachEntryStart( vVec, Entry, i, Start )                                   \
-    for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
-#define Vec_IntForEachEntryStartStop( vVec, Entry, i, Start, Stop )                         \
-    for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
-#define Vec_IntForEachEntryReverse( vVec, pEntry, i )                                       \
-    for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntAlloc( int nCap )
-{
-    Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
-    if ( nCap > 0 && nCap < 16 )
-        nCap = 16;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given size and cleans it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntStart( int nSize )
-{
-    Vec_Int_t * p;
-    p = Vec_IntAlloc( nSize );
-    p->nSize = nSize;
-    memset( p->pArray, 0, sizeof(int) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntAllocArray( int * pArray, int nSize )
-{
-    Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = pArray;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntAllocArrayCopy( int * pArray, int nSize )
-{
-    Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = ALLOC( int, nSize );
-    memcpy( p->pArray, pArray, sizeof(int) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the integer array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntDup( Vec_Int_t * pVec )
-{
-    Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( int, p->nCap ) : NULL;
-    memcpy( p->pArray, pVec->pArray, sizeof(int) * pVec->nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the array into another vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
-{
-    Vec_Int_t * p;
-    p = ALLOC( Vec_Int_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = pVec->pArray;
-    pVec->nSize  = 0;
-    pVec->nCap   = 0;
-    pVec->pArray = NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntFree( Vec_Int_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
-{
-    int * pArray = p->pArray;
-    p->nCap = 0;
-    p->nSize = 0;
-    p->pArray = NULL;
-    return pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Vec_IntArray( Vec_Int_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntSize( Vec_Int_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntEntry( Vec_Int_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] += Addition;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntEntryLast( Vec_Int_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[p->nSize-1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( int, p->pArray, nCapMin ); 
-    assert( p->pArray );
-    p->nCap   = nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Entry )
-{
-    int i;
-    Vec_IntGrow( p, nSize );
-    for ( i = 0; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
-{
-    int i;
-    if ( p->nSize >= nSize )
-        return;
-    Vec_IntGrow( p, nSize );
-    for ( i = p->nSize; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntShrink( Vec_Int_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntClear( Vec_Int_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_IntGrow( p, 16 );
-        else
-            Vec_IntGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry )
-{
-    int i;
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_IntGrow( p, 16 );
-        else
-            Vec_IntGrow( p, 2 * p->nCap );
-    }
-    p->nSize++;
-    for ( i = p->nSize - 1; i >= 1; i-- )
-        p->pArray[i] = p->pArray[i-1];
-    p->pArray[0] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-// HA: Commented as advised by Alan M.
-// static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
-// {
-//     if ( p->nSize == p->nCap )
-//     {
-//         int * pArray;
-//         int i;
-
-//         if ( p->nSize == 0 )
-//             p->nCap = 1;
-//         if ( pMemMan )
-//             pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
-//         else
-//             pArray = ALLOC( int, p->nCap * 2 );
-//         if ( p->pArray )
-//         {
-//             for ( i = 0; i < p->nSize; i++ )
-//                 pArray[i] = p->pArray[i];
-//             if ( pMemMan )
-//                 Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
-//             else
-//                 free( p->pArray );
-//         }
-//         p->nCap *= 2;
-//         p->pArray = pArray;
-//     }
-//     p->pArray[p->nSize++] = Entry;
-//}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the entry while preserving the increasing order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
-{
-    int i;
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_IntGrow( p, 16 );
-        else
-            Vec_IntGrow( p, 2 * p->nCap );
-    }
-    p->nSize++;
-    for ( i = p->nSize-2; i >= 0; i-- )
-        if ( p->pArray[i] > Entry )
-            p->pArray[i+1] = p->pArray[i];
-        else
-            break;
-    p->pArray[i+1] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Inserts the entry while preserving the increasing order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return 1;
-    Vec_IntPushOrder( p, Entry );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntPushUnique( Vec_Int_t * p, int Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return 1;
-    Vec_IntPush( p, Entry );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the pointer to the next nWords entries in the vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned * Vec_IntFetch( Vec_Int_t * p, int nWords )
-{
-    p->nSize += nWords;
-    if ( p->nSize > p->nCap )
-    {
-//         Vec_IntGrow( p, 2 * p->nSize );
-        return NULL;
-    }
-    return ((unsigned *)p->pArray) + p->nSize - nWords;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the last entry and removes it from the list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntPop( Vec_Int_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find entry.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntFind( Vec_Int_t * p, int Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return i;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntRemove( Vec_Int_t * p, int Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            break;
-    if ( i == p->nSize )
-        return 0;
-    assert( i < p->nSize );
-    for ( i++; i < p->nSize; i++ )
-        p->pArray[i-1] = p->pArray[i];
-    p->nSize--;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two integers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntSortCompare1( int * pp1, int * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two integers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntSortCompare2( int * pp1, int * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 > *pp2 )
-        return -1;
-    if ( *pp1 < *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their integer value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntSort( Vec_Int_t * p, int fReverse )
-{
-    if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
-                (int (*)(const void *, const void *)) Vec_IntSortCompare2 );
-    else
-        qsort( (void *)p->pArray, p->nSize, sizeof(int), 
-                (int (*)(const void *, const void *)) Vec_IntSortCompare1 );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two integers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_IntSortCompareUnsigned( unsigned * pp1, unsigned * pp2 )
-{
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 )
-        return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their integer value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
-{
-    qsort( (void *)p->pArray, p->nSize, sizeof(int), 
-            (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/aig_free/vecPtr.h b/src/temp/aig_free/vecPtr.h
deleted file mode 100644
index 72678ed6..00000000
--- a/src/temp/aig_free/vecPtr.h
+++ /dev/null
@@ -1,587 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecPtr.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Resizable arrays of generic pointers.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecPtr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_PTR_H__
-#define __VEC_PTR_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-//#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Vec_Ptr_t_       Vec_Ptr_t;
-struct Vec_Ptr_t_ 
-{
-    int              nCap;
-    int              nSize;
-    void **          pArray;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-// iterators through entries
-#define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
-    for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-#define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start )                                   \
-    for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-#define Vec_PtrForEachEntryStop( vVec, pEntry, i, Stop )                                     \
-    for ( i = 0; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-#define Vec_PtrForEachEntryStartStop( vVec, pEntry, i, Start, Stop )                         \
-    for ( i = Start; (i < Stop) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
-#define Vec_PtrForEachEntryReverse( vVec, pEntry, i )                                        \
-    for ( i = Vec_PtrSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i-- )
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap )
-{
-    Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
-    if ( nCap > 0 && nCap < 8 )
-        nCap = 8;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given size and cleans it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrStart( int nSize )
-{
-    Vec_Ptr_t * p;
-    p = Vec_PtrAlloc( nSize );
-    p->nSize = nSize;
-    memset( p->pArray, 0, sizeof(void *) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrAllocArray( void ** pArray, int nSize )
-{
-    Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = pArray;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrAllocArrayCopy( void ** pArray, int nSize )
-{
-    Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = ALLOC( void *, nSize );
-    memcpy( p->pArray, pArray, sizeof(void *) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the integer array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrDup( Vec_Ptr_t * pVec )
-{
-    Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
-    memcpy( p->pArray, pVec->pArray, sizeof(void *) * pVec->nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the array into another vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Ptr_t * Vec_PtrDupArray( Vec_Ptr_t * pVec )
-{
-    Vec_Ptr_t * p;
-    p = ALLOC( Vec_Ptr_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = pVec->pArray;
-    pVec->nSize  = 0;
-    pVec->nCap   = 0;
-    pVec->pArray = NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrFree( Vec_Ptr_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void ** Vec_PtrReleaseArray( Vec_Ptr_t * p )
-{
-    void ** pArray = p->pArray;
-    p->nCap = 0;
-    p->nSize = 0;
-    p->pArray = NULL;
-    return pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void ** Vec_PtrArray( Vec_Ptr_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_PtrSize( Vec_Ptr_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray + i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void * Vec_PtrEntryLast( Vec_Ptr_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[p->nSize-1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrGrow( Vec_Ptr_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( void *, p->pArray, nCapMin ); 
-    p->nCap   = nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrFill( Vec_Ptr_t * p, int nSize, void * Entry )
-{
-    int i;
-    Vec_PtrGrow( p, nSize );
-    for ( i = 0; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
-{
-    int i;
-    if ( p->nSize >= nSize )
-        return;
-    if ( p->nSize < 2 * nSize )
-        Vec_PtrGrow( p, 2 * nSize );
-    else
-        Vec_PtrGrow( p, p->nSize );
-    for ( i = p->nSize; i < nSize; i++ )
-        p->pArray[i] = Entry;
-    p->nSize = nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrShrink( Vec_Ptr_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrClear( Vec_Ptr_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrPush( Vec_Ptr_t * p, void * Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_PtrGrow( p, 16 );
-        else
-            Vec_PtrGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_PtrPushUnique( Vec_Ptr_t * p, void * Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return 1;
-    Vec_PtrPush( p, Entry );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the last entry and removes it from the list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void * Vec_PtrPop( Vec_Ptr_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Find entry.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_PtrFind( Vec_Ptr_t * p, void * Entry )
-{
-    int i;
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            return i;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
-{
-    int i;
-    // delete assuming that it is closer to the end
-    for ( i = p->nSize - 1; i >= 0; i-- )
-        if ( p->pArray[i] == Entry )
-            break;
-    assert( i >= 0 );
-/*
-    // delete assuming that it is closer to the beginning
-    for ( i = 0; i < p->nSize; i++ )
-        if ( p->pArray[i] == Entry )
-            break;
-    assert( i < p->nSize );
-*/
-    for ( i++; i < p->nSize; i++ )
-        p->pArray[i-1] = p->pArray[i];
-    p->nSize--;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Moves the first nItems to the end.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
-{
-    assert( nItems < p->nSize );
-    Vec_PtrGrow( p, nItems + p->nSize );
-    memmove( (char **)p->pArray + p->nSize, p->pArray, nItems * sizeof(void*) );
-    memmove( p->pArray, (char **)p->pArray + nItems, p->nSize * sizeof(void*) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their integer value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
-{
-    qsort( (void *)p->pArray, p->nSize, sizeof(void *), 
-            (int (*)(const void *, const void *)) Vec_PtrSortCompare );
-}
-
-#endif
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/aig_free/vecStr.h b/src/temp/aig_free/vecStr.h
deleted file mode 100644
index a36734f6..00000000
--- a/src/temp/aig_free/vecStr.h
+++ /dev/null
@@ -1,510 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecStr.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Resizable arrays of characters.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecStr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_STR_H__
-#define __VEC_STR_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-//#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Vec_Str_t_       Vec_Str_t;
-struct Vec_Str_t_ 
-{
-    int              nCap;
-    int              nSize;
-    char *           pArray;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-#define Vec_StrForEachEntry( vVec, Entry, i )                                               \
-    for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ )   
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrAlloc( int nCap )
-{
-    Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
-    if ( nCap > 0 && nCap < 16 )
-        nCap = 16;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given size and cleans it.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrStart( int nSize )
-{
-    Vec_Str_t * p;
-    p = Vec_StrAlloc( nSize );
-    p->nSize = nSize;
-    memset( p->pArray, 0, sizeof(char) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrAllocArray( char * pArray, int nSize )
-{
-    Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = pArray;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the vector from an integer array of the given size.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrAllocArrayCopy( char * pArray, int nSize )
-{
-    Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
-    p->nSize  = nSize;
-    p->nCap   = nSize;
-    p->pArray = ALLOC( char, nSize );
-    memcpy( p->pArray, pArray, sizeof(char) * nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the integer array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrDup( Vec_Str_t * pVec )
-{
-    Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = p->nCap? ALLOC( char, p->nCap ) : NULL;
-    memcpy( p->pArray, pVec->pArray, sizeof(char) * pVec->nSize );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the array into another vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Str_t * Vec_StrDupArray( Vec_Str_t * pVec )
-{
-    Vec_Str_t * p;
-    p = ALLOC( Vec_Str_t, 1 );
-    p->nSize  = pVec->nSize;
-    p->nCap   = pVec->nCap;
-    p->pArray = pVec->pArray;
-    pVec->nSize  = 0;
-    pVec->nCap   = 0;
-    pVec->pArray = NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrFree( Vec_Str_t * p )
-{
-    FREE( p->pArray );
-    FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char * Vec_StrReleaseArray( Vec_Str_t * p )
-{
-    char * pArray = p->pArray;
-    p->nCap = 0;
-    p->nSize = 0;
-    p->pArray = NULL;
-    return pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char * Vec_StrArray( Vec_Str_t * p )
-{
-    return p->pArray;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_StrSize( Vec_Str_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char Vec_StrEntry( Vec_Str_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrWriteEntry( Vec_Str_t * p, int i, char Entry )
-{
-    assert( i >= 0 && i < p->nSize );
-    p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char Vec_StrEntryLast( Vec_Str_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[p->nSize-1];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resizes the vector to the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrGrow( Vec_Str_t * p, int nCapMin )
-{
-    if ( p->nCap >= nCapMin )
-        return;
-    p->pArray = REALLOC( char, p->pArray, 2 * nCapMin ); 
-    p->nCap   = 2 * nCapMin;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Fills the vector with given number of entries.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrFill( Vec_Str_t * p, int nSize, char Entry )
-{
-    int i;
-    Vec_StrGrow( p, nSize );
-    p->nSize = nSize;
-    for ( i = 0; i < p->nSize; i++ )
-        p->pArray[i] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrShrink( Vec_Str_t * p, int nSizeNew )
-{
-    assert( p->nSize >= nSizeNew );
-    p->nSize = nSizeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrClear( Vec_Str_t * p )
-{
-    p->nSize = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
-{
-    if ( p->nSize == p->nCap )
-    {
-        if ( p->nCap < 16 )
-            Vec_StrGrow( p, 16 );
-        else
-            Vec_StrGrow( p, 2 * p->nCap );
-    }
-    p->pArray[p->nSize++] = Entry;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Appends the string to the char vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrAppend( Vec_Str_t * p, char * pString )
-{
-    int i, nLength = strlen(pString);
-    Vec_StrGrow( p, p->nSize + nLength );
-    for ( i = 0; i < nLength; i++ )
-        p->pArray[p->nSize + i] = pString[i];
-    p->nSize += nLength;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the last entry and removes it from the list.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline char Vec_StrPop( Vec_Str_t * p )
-{
-    assert( p->nSize > 0 );
-    return p->pArray[--p->nSize];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_StrSortCompare1( char * pp1, char * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 < *pp2 )
-        return -1;
-    if ( *pp1 > *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Comparison procedure for two clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_StrSortCompare2( char * pp1, char * pp2 )
-{
-    // for some reason commenting out lines (as shown) led to crashing of the release version
-    if ( *pp1 > *pp2 )
-        return -1;
-    if ( *pp1 < *pp2 ) //
-        return 1;
-    return 0; //
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sorting the entries by their integer value.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
-{
-    if ( fReverse ) 
-        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
-                (int (*)(const void *, const void *)) Vec_StrSortCompare2 );
-    else
-        qsort( (void *)p->pArray, p->nSize, sizeof(char), 
-                (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/temp/aig_free/vecVec.h b/src/temp/aig_free/vecVec.h
deleted file mode 100644
index 2de38619..00000000
--- a/src/temp/aig_free/vecVec.h
+++ /dev/null
@@ -1,289 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [vecVec.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Resizable arrays.]
-
-  Synopsis    [Resizable vector of resizable vectors.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __VEC_VEC_H__
-#define __VEC_VEC_H__
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-//#include "extra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Vec_Vec_t_       Vec_Vec_t;
-struct Vec_Vec_t_ 
-{
-    int              nCap;
-    int              nSize;
-    void **          pArray;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-// iterators through levels 
-#define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
-    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
-#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
-    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
-#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
-    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
-#define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
-    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
-
-// iteratores through entries
-#define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
-    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
-        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
-#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart )                           \
-    for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
-        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
-#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop )            \
-    for ( i = LevelStart; i <= LevelStop; i++ )                                               \
-        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
-#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k )                                     \
-    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
-        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
-#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k )                              \
-    for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- )                                           \
-        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
-{
-    Vec_Vec_t * p;
-    p = ALLOC( Vec_Vec_t, 1 );
-    if ( nCap > 0 && nCap < 8 )
-        nCap = 8;
-    p->nSize  = 0;
-    p->nCap   = nCap;
-    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Vec_Vec_t * Vec_VecStart( int nSize )
-{
-    Vec_Vec_t * p;
-    int i;
-    p = Vec_VecAlloc( nSize );
-    for ( i = 0; i < nSize; i++ )
-        p->pArray[i] = Vec_PtrAlloc( 0 );
-    p->nSize = nSize;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a vector with the given capacity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
-{
-    int i;
-    if ( p->nSize >= Level + 1 )
-        return;
-    Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
-    for ( i = p->nSize; i <= Level; i++ )
-        p->pArray[i] = Vec_PtrAlloc( 0 );
-    p->nSize = Level + 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_VecSize( Vec_Vec_t * p )
-{
-    return p->nSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void * Vec_VecEntry( Vec_Vec_t * p, int i )
-{
-    assert( i >= 0 && i < p->nSize );
-    return p->pArray[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_VecFree( Vec_Vec_t * p )
-{
-    Vec_Ptr_t * vVec;
-    int i;
-    Vec_VecForEachLevel( p, vVec, i )
-        Vec_PtrFree( vVec );
-    Vec_PtrFree( (Vec_Ptr_t *)p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the vector of vectors.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Vec_VecSizeSize( Vec_Vec_t * p )
-{
-    Vec_Ptr_t * vVec;
-    int i, Counter = 0;
-    Vec_VecForEachLevel( p, vVec, i )
-        Counter += vVec->nSize;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_VecClear( Vec_Vec_t * p )
-{
-    Vec_Ptr_t * vVec;
-    int i;
-    Vec_VecForEachLevel( p, vVec, i )
-        Vec_PtrClear( vVec );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
-{
-    if ( p->nSize < Level + 1 )
-    {
-        int i;
-        Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
-        for ( i = p->nSize; i < Level + 1; i++ )
-            p->pArray[i] = Vec_PtrAlloc( 0 );
-        p->nSize = Level + 1;
-    }
-    Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
-{
-    if ( p->nSize < Level + 1 )
-        Vec_VecPush( p, Level, Entry );
-    else
-        Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-