summaryrefslogtreecommitdiffstats
path: root/src/temp/aig_free
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/aig_free')
-rw-r--r--src/temp/aig_free/aig.h321
-rw-r--r--src/temp/aig_free/aigBalance.c391
-rw-r--r--src/temp/aig_free/aigCheck.c110
-rw-r--r--src/temp/aig_free/aigDfs.c399
-rw-r--r--src/temp/aig_free/aigMan.c162
-rw-r--r--src/temp/aig_free/aigMem.c115
-rw-r--r--src/temp/aig_free/aigObj.c228
-rw-r--r--src/temp/aig_free/aigOper.c373
-rw-r--r--src/temp/aig_free/aigTable.c266
-rw-r--r--src/temp/aig_free/aigUtil.c513
-rw-r--r--src/temp/aig_free/cudd2.c375
-rw-r--r--src/temp/aig_free/cudd2.h83
-rw-r--r--src/temp/aig_free/st.c626
-rw-r--r--src/temp/aig_free/st.h96
-rw-r--r--src/temp/aig_free/subdir.mk87
-rw-r--r--src/temp/aig_free/vec.h82
-rw-r--r--src/temp/aig_free/vecFlt.h667
-rw-r--r--src/temp/aig_free/vecInt.h781
-rw-r--r--src/temp/aig_free/vecPtr.h587
-rw-r--r--src/temp/aig_free/vecStr.h510
-rw-r--r--src/temp/aig_free/vecVec.h289
21 files changed, 7061 insertions, 0 deletions
diff --git a/src/temp/aig_free/aig.h b/src/temp/aig_free/aig.h
new file mode 100644
index 00000000..0dfc3f11
--- /dev/null
+++ b/src/temp/aig_free/aig.h
@@ -0,0 +1,321 @@
+/**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
new file mode 100644
index 00000000..1abc672d
--- /dev/null
+++ b/src/temp/aig_free/aigBalance.c
@@ -0,0 +1,391 @@
+/**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
new file mode 100644
index 00000000..61e4cf78
--- /dev/null
+++ b/src/temp/aig_free/aigCheck.c
@@ -0,0 +1,110 @@
+/**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
new file mode 100644
index 00000000..c004cab0
--- /dev/null
+++ b/src/temp/aig_free/aigDfs.c
@@ -0,0 +1,399 @@
+/**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
new file mode 100644
index 00000000..bb39712f
--- /dev/null
+++ b/src/temp/aig_free/aigMan.c
@@ -0,0 +1,162 @@
+/**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
new file mode 100644
index 00000000..1be78a88
--- /dev/null
+++ b/src/temp/aig_free/aigMem.c
@@ -0,0 +1,115 @@
+/**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
new file mode 100644
index 00000000..51ce6008
--- /dev/null
+++ b/src/temp/aig_free/aigObj.c
@@ -0,0 +1,228 @@
+/**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
new file mode 100644
index 00000000..9985093e
--- /dev/null
+++ b/src/temp/aig_free/aigOper.c
@@ -0,0 +1,373 @@
+/**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
new file mode 100644
index 00000000..338faa45
--- /dev/null
+++ b/src/temp/aig_free/aigTable.c
@@ -0,0 +1,266 @@
+/**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
new file mode 100644
index 00000000..623de32b
--- /dev/null
+++ b/src/temp/aig_free/aigUtil.c
@@ -0,0 +1,513 @@
+/**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
new file mode 100644
index 00000000..f95d3fd0
--- /dev/null
+++ b/src/temp/aig_free/cudd2.c
@@ -0,0 +1,375 @@
+/**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
new file mode 100644
index 00000000..c80ec5ed
--- /dev/null
+++ b/src/temp/aig_free/cudd2.h
@@ -0,0 +1,83 @@
+/**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
new file mode 100644
index 00000000..5024e08d
--- /dev/null
+++ b/src/temp/aig_free/st.c
@@ -0,0 +1,626 @@
+/*
+ * 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
new file mode 100644
index 00000000..b15f3c83
--- /dev/null
+++ b/src/temp/aig_free/st.h
@@ -0,0 +1,96 @@
+/*
+ * 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
new file mode 100644
index 00000000..1867f777
--- /dev/null
+++ b/src/temp/aig_free/subdir.mk
@@ -0,0 +1,87 @@
+################################################################################
+# 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
new file mode 100644
index 00000000..61737d3a
--- /dev/null
+++ b/src/temp/aig_free/vec.h
@@ -0,0 +1,82 @@
+/**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
new file mode 100644
index 00000000..6d92d824
--- /dev/null
+++ b/src/temp/aig_free/vecFlt.h
@@ -0,0 +1,667 @@
+/**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
new file mode 100644
index 00000000..77bf5849
--- /dev/null
+++ b/src/temp/aig_free/vecInt.h
@@ -0,0 +1,781 @@
+/**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
new file mode 100644
index 00000000..72678ed6
--- /dev/null
+++ b/src/temp/aig_free/vecPtr.h
@@ -0,0 +1,587 @@
+/**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
new file mode 100644
index 00000000..a36734f6
--- /dev/null
+++ b/src/temp/aig_free/vecStr.h
@@ -0,0 +1,510 @@
+/**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
new file mode 100644
index 00000000..2de38619
--- /dev/null
+++ b/src/temp/aig_free/vecVec.h
@@ -0,0 +1,289 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-23 05:52:25 +0000