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