summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy')
-rw-r--r--src/temp/ivy/ivy.h76
-rw-r--r--src/temp/ivy/ivyBalance.c409
-rw-r--r--src/temp/ivy/ivyCut.c548
-rw-r--r--src/temp/ivy/ivyDfs.c133
-rw-r--r--src/temp/ivy/ivyMan.c8
-rw-r--r--src/temp/ivy/ivyMulti.c504
-rw-r--r--src/temp/ivy/ivyMulti8.c427
-rw-r--r--src/temp/ivy/ivyObj.c1
-rw-r--r--src/temp/ivy/ivyOper.c6
-rw-r--r--src/temp/ivy/ivyResyn.c96
-rw-r--r--src/temp/ivy/ivyRwrAlg.c408
-rw-r--r--src/temp/ivy/ivyRwrPre.c597
-rw-r--r--src/temp/ivy/ivyUtil.c216
-rw-r--r--src/temp/ivy/module.make3
14 files changed, 2695 insertions, 737 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h
index 55ada384..57d8cfd2 100644
--- a/src/temp/ivy/ivy.h
+++ b/src/temp/ivy/ivy.h
@@ -42,6 +42,11 @@ extern "C" {
typedef struct Ivy_Man_t_ Ivy_Man_t;
typedef struct Ivy_Obj_t_ Ivy_Obj_t;
+typedef int Ivy_Edge_t;
+
+// constant edges
+#define IVY_CONST0 1
+#define IVY_CONST1 0
// object types
typedef enum {
@@ -102,10 +107,12 @@ struct Ivy_Man_t_
int * pTable; // structural hash table
int nTableSize; // structural hash table size
// various data members
+ int fCatchExor; // set to 1 to detect EXORs
int fExtended; // set to 1 in extended mode
int nTravIds; // the traversal ID
int nLevelMax; // the maximum level
void * pData; // the temporary data
+ Vec_Int_t * vRequired; // required times
// truth table of the 8-LUTs
unsigned * pMemory; // memory for truth tables
Vec_Int_t * vTruths; // offset for truth table of each node
@@ -118,6 +125,26 @@ struct Ivy_Man_t_
};
+#define IVY_CUT_LIMIT 256
+#define IVY_CUT_INPUT 6
+
+typedef struct Ivy_Cut_t_ Ivy_Cut_t;
+struct Ivy_Cut_t_
+{
+ short nSize;
+ short nSizeMax;
+ int pArray[IVY_CUT_INPUT];
+ unsigned uHash;
+};
+
+typedef struct Ivy_Store_t_ Ivy_Store_t;
+struct Ivy_Store_t_
+{
+ int nCuts;
+ int nCutsMax;
+ Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -133,14 +160,6 @@ static inline int Ivy_InfoHasBit( unsigned * p, int i ) { return (p[(i
static inline void Ivy_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Ivy_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
-static inline int Ivy_FanCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
-static inline int Ivy_FanId( int Fan ) { return Fan >> 1; }
-static inline int Ivy_FanCompl( int Fan ) { return Fan & 1; }
-
-static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; }
-static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; }
-static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; }
-
static inline Ivy_Obj_t * Ivy_Regular( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) & ~01); }
static inline Ivy_Obj_t * Ivy_Not( Ivy_Obj_t * p ) { return (Ivy_Obj_t *)((unsigned)(p) ^ 01); }
static inline Ivy_Obj_t * Ivy_NotCond( Ivy_Obj_t * p, int c ) { return (Ivy_Obj_t *)((unsigned)(p) ^ (c)); }
@@ -153,6 +172,19 @@ static inline Ivy_Obj_t * Ivy_ManPi( Ivy_Man_t * p, int i ) { return p->pO
static inline Ivy_Obj_t * Ivy_ManPo( Ivy_Man_t * p, int i ) { return p->pObjs + Vec_IntEntry(p->vPos,i); }
static inline Ivy_Obj_t * Ivy_ManObj( Ivy_Man_t * p, int i ) { return p->pObjs + i; }
+static inline Ivy_Edge_t Ivy_EdgeCreate( int Id, int fCompl ) { return (Id << 1) | fCompl; }
+static inline int Ivy_EdgeId( Ivy_Edge_t Edge ) { return Edge >> 1; }
+static inline int Ivy_EdgeIsComplement( Ivy_Edge_t Edge ) { return Edge & 1; }
+static inline Ivy_Edge_t Ivy_EdgeRegular( Ivy_Edge_t Edge ) { return (Edge >> 1) << 1; }
+static inline Ivy_Edge_t Ivy_EdgeNot( Ivy_Edge_t Edge ) { return Edge ^ 1; }
+static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { return Edge ^ fCond; }
+static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); }
+static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
+
+static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; }
+static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; }
+static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; }
+
static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; }
static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; }
static inline int Ivy_ManAssertNum( Ivy_Man_t * p ) { return p->nObjs[IVY_ASSERT]; }
@@ -185,9 +217,9 @@ static inline int Ivy_ObjIsAnd( Ivy_Obj_t * pObj ) { assert( !Ivy
static inline int Ivy_ObjIsExor( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXOR; }
static inline int Ivy_ObjIsBuf( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_BUF; }
static inline int Ivy_ObjIsNode( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR; }
-static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
+static inline int Ivy_ObjIsTerm( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PI || pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT; }
static inline int Ivy_ObjIsHash( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_AND || pObj->Type == IVY_EXOR || pObj->Type == IVY_LATCH; }
-static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
+static inline int Ivy_ObjIsOneFanin( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_PO || pObj->Type == IVY_ASSERT || pObj->Type == IVY_BUF || pObj->Type == IVY_LATCH; }
static inline int Ivy_ObjIsAndMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_ANDM; }
static inline int Ivy_ObjIsExorMulti( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Type == IVY_EXORM; }
@@ -227,13 +259,9 @@ static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { assert( !Ivy
static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_NotCond( Ivy_ObjFanin1(pObj), Ivy_ObjFaninC1(pObj) ); }
static inline int Ivy_ObjLevelR( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->LevelR; }
static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return pObj->Level; }
-static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
+static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
static inline void Ivy_ObjClean( Ivy_Obj_t * pObj ) {
int IdSaved = pObj->Id;
- if ( IdSaved == 54 )
- {
- int x = 0;
- }
memset( pObj, 0, sizeof(Ivy_Obj_t) );
pObj->Id = IdSaved;
}
@@ -339,6 +367,8 @@ static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj )
// iterator over all objects, including those currently not used
#define Ivy_ManForEachObj( p, pObj, i ) \
for ( i = 0, pObj = p->pObjs; i < p->ObjIdNext; i++, pObj++ )
+#define Ivy_ManForEachObjReverse( p, pObj, i ) \
+ for ( i = p->ObjIdNext - 1, pObj = p->pObjs + i; i >= 0; i--, pObj-- )
// iterator over the primary inputs
#define Ivy_ManForEachPi( p, pObj, i ) \
for ( i = 0; i < Vec_IntSize(p->vPis) && ((pObj) = Ivy_ManPi(p, i)); i++ )
@@ -369,6 +399,9 @@ static inline int Ivy_ObjFaninNum( Ivy_Obj_t * pObj )
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== ivyBalance.c ========================================================*/
+extern Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
+extern Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel );
/*=== ivyCanon.c ========================================================*/
extern Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
extern Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
@@ -377,11 +410,13 @@ extern Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init );
extern int Ivy_ManCheck( Ivy_Man_t * p );
/*=== ivyCut.c ==========================================================*/
extern void Ivy_ManSeqFindCut( Ivy_Obj_t * pNode, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize );
-/*=== ivyBalance.c ======================================================*/
-extern int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel );
+extern Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves );
/*=== ivyDfs.c ==========================================================*/
extern Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p );
extern Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p );
+extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone );
+extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p );
+extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p );
/*=== ivyDsd.c ==========================================================*/
extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree );
extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree );
@@ -399,6 +434,7 @@ extern Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type
extern Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
extern Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type );
extern Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+extern int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSol );
/*=== ivyObj.c ==========================================================*/
extern Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost );
extern Ivy_Obj_t * Ivy_ObjCreateExt( Ivy_Man_t * p, Ivy_Type_t Type );
@@ -415,8 +451,12 @@ extern Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 );
extern Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 );
extern Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC );
extern Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs );
+/*=== ivyResyn.c =========================================================*/
+extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel );
/*=== ivyRewrite.c =========================================================*/
extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
+extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost );
+extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose );
/*=== ivyTable.c ========================================================*/
extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj );
extern void Ivy_TableInsert( Ivy_Obj_t * pObj );
@@ -437,6 +477,8 @@ extern Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj
extern unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth );
extern Ivy_Obj_t * Ivy_NodeRealFanin_rec( Ivy_Obj_t * pNode, int iFanin );
extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p );
+extern int Ivy_ManReadLevels( Ivy_Man_t * p );
+extern Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj );
#ifdef __cplusplus
}
diff --git a/src/temp/ivy/ivyBalance.c b/src/temp/ivy/ivyBalance.c
index bbe69dd9..2e230ed2 100644
--- a/src/temp/ivy/ivyBalance.c
+++ b/src/temp/ivy/ivyBalance.c
@@ -17,32 +17,18 @@
Revision [$Id: ivyBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots );
-
-// this procedure returns 1 if the node cannot be expanded
-static inline int Ivy_NodeStopFanin( Ivy_Obj_t * pNode, int iFanin )
-{
- if ( iFanin == 0 )
- return Ivy_ObjFanin0(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) > 1 || Ivy_ObjFaninC0(pNode);
- else
- return Ivy_ObjFanin1(pNode)->Type != pNode->Type || Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) > 1 || Ivy_ObjFaninC1(pNode);
-}
-
-// this procedure returns 1 if the node cannot be recursively dereferenced
-static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin )
-{
- if ( iFanin == 0 )
- return Ivy_ObjFanin0(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin0(pNode)) == 0 && !Ivy_ObjFaninC0(pNode);
- else
- return Ivy_ObjFanin1(pNode)->Type == pNode->Type && Ivy_ObjRefs(Ivy_ObjFanin1(pNode)) == 0 && !Ivy_ObjFaninC1(pNode);
-}
+static int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
+static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
+static int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
+static void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor );
+static void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -59,44 +45,41 @@ static inline int Ivy_NodeBalanceDerefFanin( Ivy_Obj_t * pNode, int iFanin )
SeeAlso []
***********************************************************************/
-int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
+Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
{
- Vec_Int_t * vNodes;
- Vec_Ptr_t * vFront, * vSpots;
- Ivy_Obj_t * pNode;
- int i;
- vSpots = Vec_PtrAlloc( 50 );
- vFront = Vec_PtrAlloc( 50 );
- vNodes = Ivy_ManDfs( p );
- Ivy_ManForEachNodeVec( p, vNodes, pNode, i )
+ Ivy_Man_t * pNew;
+ Ivy_Obj_t * pObj, * pDriver;
+ Vec_Vec_t * vStore;
+ int i, NewNodeId;
+ // clean the old manager
+ Ivy_ManCleanTravId( p );
+ // create the new manager
+ pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 );
+ // map the nodes
+ Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
+ Ivy_ManForEachPi( p, pObj, i )
+ pObj->TravId = Ivy_EdgeFromNode( Ivy_ManPi(pNew, i) );
+ // balance the AIG
+ vStore = Vec_VecAlloc( 50 );
+ Ivy_ManForEachPo( p, pObj, i )
{
- if ( Ivy_ObjIsBuf(pNode) )
- continue;
- // fix the fanin buffer problem
- Ivy_NodeFixBufferFanins( pNode );
- // skip node if it became a buffer
- if ( Ivy_ObjIsBuf(pNode) )
- continue;
- // skip nodes with one fanout if type of the node is the same as type of the fanout
- // such nodes will be processed when the fanouts are processed
- if ( Ivy_ObjRefs(pNode) == 1 && Ivy_ObjIsExor(pNode) == Ivy_ObjExorFanout(pNode) )
- continue;
- assert( Ivy_ObjRefs(pNode) > 0 );
- // do not balance the node if both if its fanins have more than one fanout
- if ( Ivy_NodeStopFanin(pNode, 0) && Ivy_NodeStopFanin(pNode, 1) )
- continue;
- // try balancing this node
- Ivy_NodeBalance( pNode, fUpdateLevel, vFront, vSpots );
+ pDriver = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
+ NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
+ NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
+ Ivy_ObjConnect( Ivy_ManPo(pNew, i), Ivy_EdgeToNode(pNew, NewNodeId) );
}
- Vec_IntFree( vNodes );
- Vec_PtrFree( vSpots );
- Vec_PtrFree( vFront );
- return 1;
+ Vec_VecFree( vStore );
+ if ( i = Ivy_ManCleanup( pNew ) )
+ printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+ // check the resulting AIG
+ if ( !Ivy_ManCheck(pNew) )
+ printf( "Ivy_ManBalance(): The check has failed.\n" );
+ return pNew;
}
/**Function*************************************************************
- Synopsis [Dereferences MFFC of the node.]
+ Synopsis [Procedure used for sorting the nodes in decreasing order of levels.]
Description []
@@ -105,24 +88,19 @@ int Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
SeeAlso []
***********************************************************************/
-void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode )
+int Ivy_NodeCompareLevelsDecrease( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
{
- Ivy_Obj_t * pFan;
- // deref the first fanin
- pFan = Ivy_ObjFanin0(pNode);
- Ivy_ObjRefsDec( pFan );
- if ( Ivy_NodeBalanceDerefFanin(pNode, 0) )
- Ivy_NodeBalanceDeref_rec( pFan );
- // deref the second fanin
- pFan = Ivy_ObjFanin1(pNode);
- Ivy_ObjRefsDec( pFan );
- if ( Ivy_NodeBalanceDerefFanin(pNode, 1) )
- Ivy_NodeBalanceDeref_rec( pFan );
+ int Diff = Ivy_Regular(*pp1)->Level - Ivy_Regular(*pp2)->Level;
+ if ( Diff > 0 )
+ return -1;
+ if ( Diff < 0 )
+ return 1;
+ return 0;
}
/**Function*************************************************************
- Synopsis [Removes nodes inside supergate and determines frontier.]
+ Synopsis [Returns the ID of new node constructed.]
Description []
@@ -131,35 +109,47 @@ void Ivy_NodeBalanceDeref_rec( Ivy_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_t * vFront )
+int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel )
{
- Ivy_Obj_t * pFanin;
- // skip visited nodes
- if ( Vec_PtrFind(vSpots, pNode) >= 0 )
- return;
- // collect node
- Vec_PtrPush( vSpots, pNode );
- // first fanin
- pFanin = Ivy_ObjFanin0(pNode);
- if ( Ivy_ObjRefs(pFanin) == 0 )
- Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront );
- else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild0(pNode)) >= 0 )
- Vec_PtrRemove( vFront, Ivy_ObjChild0(pNode) );
- else
- Vec_PtrPushUnique( vFront, Ivy_ObjChild0(pNode) );
- // second fanin
- pFanin = Ivy_ObjFanin1(pNode);
- if ( Ivy_ObjRefs(pFanin) == 0 )
- Ivy_NodeBalanceCollect_rec( pFanin, vSpots, vFront );
- else if ( Ivy_ObjIsExor(pNode) && Vec_PtrFind(vFront, Ivy_ObjChild1(pNode)) >= 0 )
- Vec_PtrRemove( vFront, Ivy_ObjChild1(pNode) );
- else
- Vec_PtrPushUnique( vFront, Ivy_ObjChild1(pNode) );
+ Ivy_Obj_t * pObjNew;
+ Vec_Ptr_t * vSuper;
+ int i, NewNodeId;
+ assert( !Ivy_IsComplement(pObjOld) );
+ assert( !Ivy_ObjIsBuf(pObjOld) );
+ // return if the result is known
+ if ( Ivy_ObjIsConst1(pObjOld) )
+ return pObjOld->TravId;
+ if ( pObjOld->TravId )
+ return pObjOld->TravId;
+ assert( Ivy_ObjIsNode(pObjOld) );
+ // get the implication supergate
+ vSuper = Ivy_NodeBalanceCone( pObjOld, vStore, Level );
+ if ( vSuper->nSize == 0 )
+ { // it means that the supergate contains two nodes in the opposite polarity
+ pObjOld->TravId = Ivy_EdgeFromNode( Ivy_ManConst0(pNew) );
+ return pObjOld->TravId;
+ }
+ if ( vSuper->nSize < 2 )
+ printf( "BUG!\n" );
+ // for each old node, derive the new well-balanced node
+ for ( i = 0; i < vSuper->nSize; i++ )
+ {
+ NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+ NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(vSuper->pArray[i]) );
+ vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
+ }
+ // build the supergate
+ pObjNew = Ivy_NodeBalanceBuildSuper( vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
+ vSuper->nSize = 0;
+ // make sure the balanced node is not assigned
+ assert( pObjOld->TravId == 0 );
+ pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
+ return pObjOld->TravId;
}
/**Function*************************************************************
- Synopsis [Comparison procedure for two nodes by level.]
+ Synopsis [Builds implication supergate.]
Description []
@@ -168,89 +158,107 @@ void Ivy_NodeBalanceCollect_rec( Ivy_Obj_t * pNode, Vec_Ptr_t * vSpots, Vec_Ptr_
SeeAlso []
***********************************************************************/
-int Ivy_BalanceCompareByLevel( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
{
- int Level1 = Ivy_ObjLevel( *pp1 );
- int Level2 = Ivy_ObjLevel( *pp2 );
- if ( Level1 > Level2 )
- return -1;
- if ( Level1 < Level2 )
- return 1;
- return 0;
+ Ivy_Obj_t * pObj1, * pObj2;
+ int LeftBound;
+ assert( vSuper->nSize > 1 );
+ // sort the new nodes by level in the decreasing order
+ Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease );
+ // balance the nodes
+ while ( vSuper->nSize > 1 )
+ {
+ // find the left bound on the node to be paired
+ LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
+ // find the node that can be shared (if no such node, randomize choice)
+ Ivy_NodeBalancePermute( vSuper, LeftBound, Type == IVY_EXOR );
+ // pull out the last two nodes
+ pObj1 = Vec_PtrPop(vSuper);
+ pObj2 = Vec_PtrPop(vSuper);
+ Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) );
+ }
+ return Vec_PtrEntry(vSuper, 0);
}
/**Function*************************************************************
- Synopsis [Removes nodes inside supergate and determines frontier.]
+ Synopsis [Collects the nodes of the supergate.]
- Description [Return 1 if the output needs to be complemented.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots )
+int Ivy_NodeBalanceCone_rec( Ivy_Obj_t * pRoot, Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper )
{
- Ivy_Man_t * pMan = Ivy_ObjMan( pNode );
- Ivy_Obj_t * pObj, * pNext;
- int i, k, Counter = 0;
- // dereference the cone
- Ivy_NodeBalanceDeref_rec( pNode );
- // collect the frontier and the internal nodes
- Vec_PtrClear( vFront );
- Vec_PtrClear( vSpots );
- Ivy_NodeBalanceCollect_rec( pNode, vSpots, vFront );
- // remove all the nodes
- Vec_PtrForEachEntry( vSpots, pObj, i )
- {
- // skip the first entry (the node itself)
- if ( i == 0 ) continue;
- // collect the free entries
- Vec_IntPush( pMan->vFree, pObj->Id );
- Ivy_ObjDelete( pObj, 1 );
- }
- // sort nodes by level in decreasing order
- qsort( (void *)Vec_PtrArray(vFront), Vec_PtrSize(vFront), sizeof(Ivy_Obj_t *),
- (int (*)(const void *, const void *))Ivy_BalanceCompareByLevel );
- // check if there are nodes and their complements
- Counter = 0;
- Vec_PtrForEachEntry( vFront, pObj, i )
+ int RetValue1, RetValue2, i;
+ // check if the node is visited
+ if ( Ivy_Regular(pObj)->fMarkB )
{
- if ( i == Vec_PtrSize(vFront) - 1 )
- break;
- pNext = Vec_PtrEntry( vFront, i+1 );
- if ( Ivy_Regular(pObj) == Ivy_Regular(pNext) )
- {
- assert( pObj == Ivy_Not(pNext) );
- Vec_PtrWriteEntry( vFront, i, NULL );
- Vec_PtrWriteEntry( vFront, i+1, NULL );
- i++;
- Counter++;
- }
- }
- // if there are no complemented pairs, go ahead and balance
- if ( Counter == 0 )
+ // 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] == Ivy_Not(pObj) )
+ return -1;
+ assert( 0 );
return 0;
- // if there are complemented pairs and this is AND, create const 0
- if ( Counter > 0 && Ivy_ObjIsAnd(pNode) )
+ }
+ // if the new node is complemented or a PI, another gate begins
+ if ( pObj != pRoot && (Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Ivy_ObjType(pRoot) || Ivy_ObjRefs(pObj) > 1) )
{
- Vec_PtrClear( vFront );
- Vec_PtrPush( vFront, Ivy_ManConst0(pMan) );
+ Vec_PtrPush( vSuper, pObj );
+ Ivy_Regular(pObj)->fMarkB = 1;
return 0;
}
- assert( Counter > 0 && Ivy_ObjIsExor(pNode) );
- // remove the pairs
- k = 0;
- Vec_PtrForEachEntry( vFront, pObj, i )
- if ( pObj )
- Vec_PtrWriteEntry( vFront, k++, pObj );
- Vec_PtrShrink( vFront, k );
- // add constant zero node if nothing is left
- if ( Vec_PtrSize(vFront) == 0 )
- Vec_PtrPush( vFront, Ivy_ManConst0(pMan) );
- // return 1 if the number of pairs is odd (need to complement the output)
- return Counter & 1;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( Ivy_ObjIsNode(pObj) );
+ // go through the branches
+ RetValue1 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_ObjChild0(pObj) ), vSuper );
+ RetValue2 = Ivy_NodeBalanceCone_rec( pRoot, Ivy_ObjReal( Ivy_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 * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
+{
+ Vec_Ptr_t * vNodes;
+ int RetValue, i;
+ assert( !Ivy_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 = Ivy_NodeBalanceCone_rec( pObj, pObj, vNodes );
+ assert( vNodes->nSize > 1 );
+ // unmark the visited nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Ivy_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*************************************************************
@@ -270,27 +278,27 @@ int Ivy_NodeBalancePrepare( Ivy_Obj_t * pNode, Vec_Ptr_t * vFront, Vec_Ptr_t * v
***********************************************************************/
int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
{
- Ivy_Obj_t * pNodeRight, * pNodeLeft;
+ Ivy_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;
- pNodeRight = Vec_PtrEntry( vSuper, Current );
+ 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
- pNodeLeft = Vec_PtrEntry( vSuper, Current );
+ pObjLeft = Vec_PtrEntry( vSuper, Current );
// if the level of this node is different, quit the loop
- if ( Ivy_Regular(pNodeLeft)->Level != Ivy_Regular(pNodeRight)->Level )
+ if ( Ivy_Regular(pObjLeft)->Level != Ivy_Regular(pObjRight)->Level )
break;
}
Current++;
// get the node, for which the equality holds
- pNodeLeft = Vec_PtrEntry( vSuper, Current );
- assert( Ivy_Regular(pNodeLeft)->Level == Ivy_Regular(pNodeRight)->Level );
+ pObjLeft = Vec_PtrEntry( vSuper, Current );
+ assert( Ivy_Regular(pObjLeft)->Level == Ivy_Regular(pObjRight)->Level );
return Current;
}
@@ -306,9 +314,9 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
SeeAlso []
***********************************************************************/
-void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
{
- Ivy_Obj_t * pNode1, * pNode2, * pNode3, * pGhost;
+ Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
int RightBound, i;
// get the right bound
RightBound = Vec_PtrSize(vSuper) - 2;
@@ -316,19 +324,19 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
if ( LeftBound == RightBound )
return;
// get the two last nodes
- pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 );
- pNode2 = Vec_PtrEntry( vSuper, RightBound );
+ pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
+ pObj2 = Vec_PtrEntry( vSuper, RightBound );
// find the first node that can be shared
for ( i = RightBound; i >= LeftBound; i-- )
{
- pNode3 = Vec_PtrEntry( vSuper, i );
- pGhost = Ivy_ObjCreateGhost( pNode1, pNode3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
+ pObj3 = Vec_PtrEntry( vSuper, i );
+ pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
if ( Ivy_TableLookup( pGhost ) )
{
- if ( pNode3 == pNode2 )
+ if ( pObj3 == pObj2 )
return;
- Vec_PtrWriteEntry( vSuper, i, pNode2 );
- Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
+ Vec_PtrWriteEntry( vSuper, i, pObj2 );
+ Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
return;
}
}
@@ -336,11 +344,11 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
// we did not find the node to share, randomize choice
{
int Choice = rand() % (RightBound - LeftBound + 1);
- pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
- if ( pNode3 == pNode2 )
+ pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
+ if ( pObj3 == pObj2 )
return;
- Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 );
- Vec_PtrWriteEntry( vSuper, RightBound, pNode3 );
+ Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pObj2 );
+ Vec_PtrWriteEntry( vSuper, RightBound, pObj3 );
}
*/
}
@@ -356,61 +364,22 @@ void Ivy_NodeBalancePermute( Ivy_Man_t * pMan, Vec_Ptr_t * vSuper, int LeftBound
SeeAlso []
***********************************************************************/
-void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vFront, Ivy_Obj_t * pNode )
+void Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj )
{
- Ivy_Obj_t * pNode1, * pNode2;
+ Ivy_Obj_t * pObj1, * pObj2;
int i;
- if ( Vec_PtrPushUnique(vFront, pNode) )
+ if ( Vec_PtrPushUnique(vStore, pObj) )
return;
// find the p of the node
- for ( i = vFront->nSize-1; i > 0; i-- )
+ for ( i = vStore->nSize-1; i > 0; i-- )
{
- pNode1 = vFront->pArray[i ];
- pNode2 = vFront->pArray[i-1];
- if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
+ pObj1 = vStore->pArray[i ];
+ pObj2 = vStore->pArray[i-1];
+ if ( Ivy_Regular(pObj1)->Level <= Ivy_Regular(pObj2)->Level )
break;
- vFront->pArray[i ] = pNode2;
- vFront->pArray[i-1] = pNode1;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Balances one node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_NodeBalance( Ivy_Obj_t * pNode, int fUpdateLevel, Vec_Ptr_t * vFront, Vec_Ptr_t * vSpots )
-{
- Ivy_Man_t * pMan = Ivy_ObjMan( pNode );
- Ivy_Obj_t * pFan0, * pFan1, * pNodeNew;
- int fCompl, LeftBound;
- // remove internal nodes and derive the frontier
- fCompl = Ivy_NodeBalancePrepare( pNode, vFront, vSpots );
- assert( Vec_PtrSize(vFront) > 0 );
- // balance the nodes
- while ( Vec_PtrSize(vFront) > 1 )
- {
- // find the left bound on the node to be paired
- LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vFront );
- // find the node that can be shared (if no such node, randomize choice)
- Ivy_NodeBalancePermute( pMan, vFront, LeftBound, Ivy_ObjIsExor(pNode) );
- // pull out the last two nodes
- pFan0 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan0)) );
- pFan1 = Vec_PtrPop(vFront); assert( !Ivy_ObjIsConst1(Ivy_Regular(pFan1)) );
- // create the new node
- pNodeNew = Ivy_ObjCreate( Ivy_ObjCreateGhost(pFan0, pFan1, Ivy_ObjType(pNode), IVY_INIT_NONE) );
- // add the new node to the frontier
- Ivy_NodeBalancePushUniqueOrderByLevel( vFront, pNodeNew );
+ vStore->pArray[i ] = pObj2;
+ vStore->pArray[i-1] = pObj1;
}
- assert( Vec_PtrSize(vFront) == 1 );
- // perform the replacement
- Ivy_ObjReplace( pNode, Ivy_NotCond(Vec_PtrPop(vFront), fCompl), 1, 1 );
}
diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c
index 57720e17..71a3613c 100644
--- a/src/temp/ivy/ivyCut.c
+++ b/src/temp/ivy/ivyCut.c
@@ -200,180 +200,6 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
-/**Function*************************************************************
-
- Synopsis [Comparison for node pointers.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
-{
- if ( *pp1 < *pp2 )
- return -1;
- if ( *pp1 > *pp2 )
- return 1;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computing one algebraic cut.]
-
- Description [Returns 1 if the tree-leaves of this node where traversed
- and found to have no external references (and have not been collected).
- Returns 0 if the tree-leaves have external references and are collected.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pRoot, Ivy_Type_t Type, Vec_Ptr_t * vFront )
-{
- int RetValue0, RetValue1;
- Ivy_Obj_t * pRootR = Ivy_Regular(pRoot);
- assert( Type != IVY_EXOR || !Ivy_IsComplement(pRoot) );
- // if the node is a buffer skip through it
- if ( Ivy_ObjIsBuf(pRootR) )
- return Ivy_ManFindAlgCut_rec( Ivy_NotCond(Ivy_ObjChild0(pRootR), Ivy_IsComplement(pRoot)), Type, vFront );
- // if the node is the end of the tree, return
- if ( Ivy_IsComplement(pRoot) || Ivy_ObjIsCi(pRoot) || Ivy_ObjType(pRoot) != Type )
- {
- if ( Ivy_ObjRefs(pRootR) == 1 )
- return 1;
- assert( Ivy_ObjRefs(pRootR) > 1 );
- Vec_PtrPush( vFront, pRoot );
- return 0;
- }
- // branch on the node
- assert( Ivy_ObjIsNode(pRoot) );
- RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild0(pRoot), Type, vFront );
- RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjChild1(pRoot), Type, vFront );
- // the case when both have no external referenced
- if ( RetValue0 && RetValue1 )
- {
- if ( Ivy_ObjRefs(pRoot) == 1 )
- return 1;
- assert( Ivy_ObjRefs(pRoot) > 1 );
- Vec_PtrPush( vFront, pRoot );
- return 0;
- }
- // the case when one of them has external references
- if ( RetValue0 )
- Vec_PtrPush( vFront, Ivy_ObjChild0(pRoot) );
- if ( RetValue1 )
- Vec_PtrPush( vFront, Ivy_ObjChild1(pRoot) );
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Computing one algebraic cut.]
-
- Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
- (c) boundary of different gates. Returns 1 if this is a pure tree.
- Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront )
-{
- Ivy_Obj_t * pObj, * pPrev;
- int RetValue, i, k;
- assert( !Ivy_IsComplement(pRoot) );
- // clear the frontier and collect the nodes
- Vec_PtrClear( vFront );
- RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront );
- // return if the node is the root of a tree
- if ( RetValue == 1 )
- return 1;
- // sort the entries to in increasing order
- Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
- // remove duplicated
- k = 1;
- Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
- {
- pPrev = (k == 0 ? NULL : Vec_PtrEntry(vFront, k-1));
- if ( pObj == pPrev )
- {
- if ( Ivy_ObjIsExor(pRoot) )
- k--;
- continue;
- }
- if ( pObj == Ivy_Not(pPrev) )
- return -1;
- Vec_PtrWriteEntry( vFront, k++, pObj );
- }
- if ( k == 0 )
- return -1;
- Vec_PtrShrink( vFront, k );
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_ManTestCutsAlg( Ivy_Man_t * p )
-{
- Vec_Ptr_t * vFront;
- Ivy_Obj_t * pObj, * pTemp;
- int i, k, RetValue;
- vFront = Vec_PtrAlloc( 100 );
- Ivy_ManForEachObj( p, pObj, i )
- {
- if ( !Ivy_ObjIsNode(pObj) )
- continue;
- if ( Ivy_ObjIsMuxType(pObj) )
- {
- printf( "m " );
- continue;
- }
- if ( pObj->Id == 509 )
- {
- int y = 0;
- }
-
- RetValue = Ivy_ManFindAlgCut( pObj, vFront );
- if ( Ivy_ObjIsExor(pObj) )
- printf( "x" );
- if ( RetValue == -1 )
- printf( "Const0 " );
- else if ( RetValue == 1 || Vec_PtrSize(vFront) <= 2 )
- printf( ". " );
- else
- printf( "%d ", Vec_PtrSize(vFront) );
-
- printf( "( " );
- Vec_PtrForEachEntry( vFront, pTemp, k )
- printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
- printf( ")\n" );
-
- if ( Vec_PtrSize(vFront) == 5 )
- {
- int x = 0;
- }
- }
- printf( "\n" );
- Vec_PtrFree( vFront );
-}
-
-
/**Function*************************************************************
@@ -639,8 +465,8 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu
void Ivy_ManTestCutsBool( Ivy_Man_t * p )
{
Vec_Ptr_t * vFront, * vVolume, * vLeaves;
- Ivy_Obj_t * pObj, * pTemp;
- int i, k, RetValue;
+ Ivy_Obj_t * pObj;//, * pTemp;
+ int i, RetValue;//, k;
vFront = Vec_PtrAlloc( 100 );
vVolume = Vec_PtrAlloc( 100 );
vLeaves = Vec_PtrAlloc( 100 );
@@ -673,6 +499,376 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p )
Vec_PtrFree( vLeaves );
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Find the hash value of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut )
+{
+ int i;
+// for ( i = 1; i < pCut->nSize; i++ )
+// assert( pCut->pArray[i-1] < pCut->pArray[i] );
+ pCut->uHash = 0;
+ for ( i = 0; i < pCut->nSize; i++ )
+ pCut->uHash |= (1 << (pCut->pArray[i] % 31));
+ return pCut->uHash;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes one node to the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Ivy_NodeCutShrink( Ivy_Cut_t * pCut, int iOld )
+{
+ int i, k;
+ for ( i = k = 0; i < pCut->nSize; i++ )
+ if ( pCut->pArray[i] != iOld )
+ pCut->pArray[k++] = pCut->pArray[i];
+ assert( k == pCut->nSize - 1 );
+ pCut->nSize--;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node to the cut.]
+
+ Description [Returns 1 if the cuts is still okay.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew )
+{
+ int i;
+ for ( i = 0; i < pCut->nSize; i++ )
+ if ( pCut->pArray[i] == iNew )
+ return 1;
+ // check if there is room
+ if ( pCut->nSize == pCut->nSizeMax )
+ return 0;
+ // add the new one
+ for ( i = pCut->nSize - 1; i >= 0; i-- )
+ if ( pCut->pArray[i] > iNew )
+ pCut->pArray[i+1] = pCut->pArray[i];
+ else
+ {
+ assert( pCut->pArray[i] < iNew );
+ break;
+ }
+ pCut->pArray[i+1] = iNew;
+ pCut->nSize++;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the cut exists.]
+
+ Description [Returns 1 if the cut exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCutFindOrAdd( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew )
+{
+ Ivy_Cut_t * pCut;
+ int i, k;
+ assert( pCutNew->uHash );
+ // try to find the cut
+ for ( i = 0; i < pCutStore->nCuts; i++ )
+ {
+ pCut = pCutStore->pCuts + i;
+ if ( pCut->uHash == pCutNew->uHash && pCut->nSize == pCutNew->nSize )
+ {
+ for ( k = 0; k < pCutNew->nSize; k++ )
+ if ( pCut->pArray[k] != pCutNew->pArray[k] )
+ break;
+ if ( k == pCutNew->nSize )
+ return 1;
+ }
+ }
+ assert( pCutStore->nCuts < pCutStore->nCutsMax );
+ // add the cut
+ pCut = pCutStore->pCuts + pCutStore->nCuts++;
+ *pCut = *pCutNew;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if pDom is contained in pCut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_CutCheckDominance( Ivy_Cut_t * pDom, Ivy_Cut_t * pCut )
+{
+ int i, k;
+ for ( i = 0; i < pDom->nSize; i++ )
+ {
+ for ( k = 0; k < pCut->nSize; k++ )
+ if ( pDom->pArray[i] == pCut->pArray[k] )
+ break;
+ if ( k == pCut->nSize ) // node i in pDom is not contained in pCut
+ return 0;
+ }
+ // every node in pDom is contained in pCut
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the cut exists.]
+
+ Description [Returns 1 if the cut exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCutFindOrAddFilter( Ivy_Store_t * pCutStore, Ivy_Cut_t * pCutNew )
+{
+ Ivy_Cut_t * pCut;
+ int i, k;
+ assert( pCutNew->uHash );
+ // try to find the cut
+ for ( i = 0; i < pCutStore->nCuts; i++ )
+ {
+ pCut = pCutStore->pCuts + i;
+ if ( pCut->nSize == 0 )
+ continue;
+ if ( pCut->nSize == pCutNew->nSize )
+ {
+ if ( pCut->uHash == pCutNew->uHash )
+ {
+ for ( k = 0; k < pCutNew->nSize; k++ )
+ if ( pCut->pArray[k] != pCutNew->pArray[k] )
+ break;
+ if ( k == pCutNew->nSize )
+ return 1;
+ }
+ continue;
+ }
+ if ( pCut->nSize < pCutNew->nSize )
+ {
+ // skip the non-contained cuts
+ if ( (pCut->uHash & pCutNew->uHash) != pCut->uHash )
+ continue;
+ // check containment seriously
+ if ( Ivy_CutCheckDominance( pCut, pCutNew ) )
+ return 1;
+ continue;
+ }
+ // check potential containment of other cut
+
+ // skip the non-contained cuts
+ if ( (pCut->uHash & pCutNew->uHash) != pCutNew->uHash )
+ continue;
+ // check containment seriously
+ if ( Ivy_CutCheckDominance( pCutNew, pCut ) )
+ {
+ // remove the current cut
+// --pCutStore->nCuts;
+// for ( k = i; k < pCutStore->nCuts; k++ )
+// pCutStore->pCuts[k] = pCutStore->pCuts[k+1];
+// i--;
+ pCut->nSize = 0;
+ }
+ }
+ assert( pCutStore->nCuts < pCutStore->nCutsMax );
+ // add the cut
+ pCut = pCutStore->pCuts + pCutStore->nCuts++;
+ *pCut = *pCutNew;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeCompactCuts( Ivy_Store_t * pCutStore )
+{
+ Ivy_Cut_t * pCut;
+ int i, k;
+ for ( i = k = 0; i < pCutStore->nCuts; i++ )
+ {
+ pCut = pCutStore->pCuts + i;
+ if ( pCut->nSize == 0 )
+ continue;
+ pCutStore->pCuts[k++] = *pCut;
+ }
+ pCutStore->nCuts = k;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodePrintCut( Ivy_Cut_t * pCut )
+{
+ int i;
+ assert( pCut->nSize > 0 );
+ printf( "%d : {", pCut->nSize );
+ for ( i = 0; i < pCut->nSize; i++ )
+ printf( " %d", pCut->pArray[i] );
+ printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore )
+{
+ int i;
+ printf( "Node %d\n", pCutStore->pCuts[0].pArray[0] );
+ for ( i = 0; i < pCutStore->nCuts; i++ )
+ Ivy_NodePrintCut( pCutStore->pCuts + i );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves )
+{
+ static Ivy_Store_t CutStore, * pCutStore = &CutStore;
+ Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
+ Ivy_Man_t * pMan = Ivy_ObjMan(pObj);
+ Ivy_Obj_t * pLeaf;
+ int i, k;
+
+ assert( nLeaves <= IVY_CUT_INPUT );
+
+ // start the structure
+ pCutStore->nCuts = 0;
+ pCutStore->nCutsMax = IVY_CUT_LIMIT;
+ // start the trivial cut
+ pCutNew->uHash = 0;
+ pCutNew->nSize = 1;
+ pCutNew->nSizeMax = nLeaves;
+ pCutNew->pArray[0] = pObj->Id;
+ Ivy_NodeCutHash( pCutNew );
+ // add the trivial cut
+ Ivy_NodeCutFindOrAdd( pCutStore, pCutNew );
+ assert( pCutStore->nCuts == 1 );
+
+ // explore the cuts
+ for ( i = 0; i < pCutStore->nCuts; i++ )
+ {
+ // expand this cut
+ pCut = pCutStore->pCuts + i;
+ if ( pCut->nSize == 0 )
+ continue;
+ for ( k = 0; k < pCut->nSize; k++ )
+ {
+ pLeaf = Ivy_ObjObj( pObj, pCut->pArray[k] );
+ if ( Ivy_ObjIsCi(pLeaf) )
+ continue;
+ *pCutNew = *pCut;
+ Ivy_NodeCutShrink( pCutNew, pLeaf->Id );
+ if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) )
+ continue;
+ if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) )
+ continue;
+ Ivy_NodeCutHash( pCutNew );
+ Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew );
+ if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+ break;
+ }
+ if ( pCutStore->nCuts == IVY_CUT_LIMIT )
+ break;
+ }
+ Ivy_NodeCompactCuts( pCutStore );
+// Ivy_NodePrintCuts( pCutStore );
+ return pCutStore;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManTestCutsAll( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i, nCutsCut, nCutsTotal, nNodeTotal, nNodeOver;
+ int clk = clock();
+ nNodeTotal = nNodeOver = 0;
+ nCutsTotal = -Ivy_ManNodeNum(p);
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ if ( !Ivy_ObjIsNode(pObj) )
+ continue;
+ nCutsCut = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts;
+ nCutsTotal += nCutsCut;
+ nNodeOver += (nCutsCut == IVY_CUT_LIMIT);
+ nNodeTotal++;
+ }
+ printf( "Total cuts = %6d. Trivial = %6d. Nodes = %6d. Satur = %6d. ",
+ nCutsTotal, Ivy_ManPiNum(p) + Ivy_ManNodeNum(p), nNodeTotal, nNodeOver );
+ PRT( "Time", clock() - clk );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c
index 2db80b00..2dc3bac8 100644
--- a/src/temp/ivy/ivyDfs.c
+++ b/src/temp/ivy/ivyDfs.c
@@ -69,6 +69,9 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
Vec_Int_t * vNodes;
Ivy_Obj_t * pObj;
int i;
+ // make sure the nodes are not marked
+ Ivy_ManForEachObj( p, pObj, i )
+ assert( !pObj->fMarkA && !pObj->fMarkB );
// collect the nodes
vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
if ( Ivy_ManLatchNum(p) > 0 )
@@ -107,7 +110,7 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
// traverse the fanins
vFanins = Ivy_ObjGetFanins( pObj );
Vec_IntForEachEntry( vFanins, Fanin, i )
- Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_FanId(Fanin)), vNodes );
+ Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes );
// add the node
Vec_IntPush( vNodes, pObj->Id );
}
@@ -134,7 +137,7 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
vNodes = Vec_IntAlloc( 10 );
Ivy_ManForEachPo( p, pObj, i )
{
- pFanin = Ivy_ManObj( p, Ivy_FanId( Ivy_ObjReadFanin(pObj,0) ) );
+ pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) );
Ivy_ManDfsExt_rec( pFanin, vNodes );
}
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
@@ -145,6 +148,132 @@ Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
return vNodes;
}
+/**Function*************************************************************
+
+ Synopsis [Collects nodes in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManCollectCone_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+ if ( pObj->fMarkA )
+ return;
+ if ( Ivy_ObjIsBuf(pObj) )
+ {
+ Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
+ Vec_PtrPush( vCone, pObj );
+ return;
+ }
+ assert( Ivy_ObjIsNode(pObj) );
+ Ivy_ManCollectCone_rec( Ivy_ObjFanin0(pObj), vCone );
+ Ivy_ManCollectCone_rec( Ivy_ObjFanin1(pObj), vCone );
+ Vec_PtrPushUnique( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects nodes in the cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
+{
+ Ivy_Obj_t * pTemp;
+ int i;
+ assert( !Ivy_IsComplement(pObj) );
+ assert( Ivy_ObjIsNode(pObj) );
+ // mark the nodes
+ Vec_PtrForEachEntry( vFront, pTemp, i )
+ Ivy_Regular(pTemp)->fMarkA = 1;
+ assert( pObj->fMarkA == 0 );
+ // collect the cone
+ Vec_PtrClear( vCone );
+ Ivy_ManCollectCone_rec( pObj, vCone );
+ // unmark the nodes
+ Vec_PtrForEachEntry( vFront, pTemp, i )
+ Ivy_Regular(pTemp)->fMarkA = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the nodes by level.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p )
+{
+ Vec_Vec_t * vNodes;
+ Ivy_Obj_t * pObj;
+ int i;
+ vNodes = Vec_VecAlloc( 100 );
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ assert( !Ivy_ObjIsBuf(pObj) );
+ if ( Ivy_ObjIsNode(pObj) )
+ Vec_VecPush( vNodes, pObj->Level, pObj );
+ }
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes required levels for each node.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pObj;
+ Vec_Int_t * vLevelsR;
+ Vec_Vec_t * vNodes;
+ int i, k, Level, LevelMax;
+ assert( p->vRequired == NULL );
+ // start the required times
+ vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) );
+ // iterate through the nodes in the reverse order
+ vNodes = Ivy_ManLevelize( p );
+ Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
+ {
+ Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj);
+ if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level )
+ Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level );
+ if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level )
+ Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level );
+ }
+ Vec_VecFree( vNodes );
+ // convert it into the required times
+ LevelMax = Ivy_ManReadLevels( p );
+//printf( "max %5d\n",LevelMax );
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ Level = Vec_IntEntry( vLevelsR, pObj->Id );
+ Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level );
+//printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level );
+ }
+ p->vRequired = vLevelsR;
+ return vLevelsR;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c
index 04c31f3d..2ff90aa9 100644
--- a/src/temp/ivy/ivyMan.c
+++ b/src/temp/ivy/ivyMan.c
@@ -48,6 +48,7 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
p = ALLOC( Ivy_Man_t, 1 );
memset( p, 0, sizeof(Ivy_Man_t) );
p->nTravIds = 1;
+ p->fCatchExor = 1;
// AIG nodes
p->nObjsAlloc = 1 + nPis + nPos + nNodesMax;
// p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even
@@ -191,12 +192,13 @@ void Ivy_ManPrintStats( Ivy_Man_t * p )
{
printf( "A = %d. ", Ivy_ManAndNum(p) );
printf( "X = %d. ", Ivy_ManExorNum(p) );
- printf( "B = %d. ", Ivy_ManBufNum(p) );
+ printf( "B = %4d. ", Ivy_ManBufNum(p) );
}
- printf( "MaxID = %d. ", p->ObjIdNext-1 );
- printf( "All = %d. ", p->nObjsAlloc );
+// printf( "MaxID = %d. ", p->ObjIdNext-1 );
+// printf( "All = %d. ", p->nObjsAlloc );
printf( "Cre = %d. ", p->nCreated );
printf( "Del = %d. ", p->nDeleted );
+ printf( "Lev = %d. ", Ivy_ManReadLevels(p) );
printf( "\n" );
}
diff --git a/src/temp/ivy/ivyMulti.c b/src/temp/ivy/ivyMulti.c
index 059d1500..e2a44e2d 100644
--- a/src/temp/ivy/ivyMulti.c
+++ b/src/temp/ivy/ivyMulti.c
@@ -24,22 +24,18 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-typedef struct Ivy_Eval_t_ Ivy_Eval_t;
-struct Ivy_Eval_t_
+#define IVY_EVAL_LIMIT 128
+
+typedef struct Ivy_Eva_t_ Ivy_Eva_t;
+struct Ivy_Eva_t_
{
- unsigned Mask : 5; // the mask of covered nodes
- unsigned Weight : 3; // the number of covered nodes
- unsigned Cost : 4; // the number of overlapping nodes
- unsigned Level : 12; // the level of this node
- unsigned Fan0 : 4; // the first fanin
- unsigned Fan1 : 4; // the second fanin
+ Ivy_Obj_t * pArg; // the argument node
+ unsigned Mask; // the mask of covered nodes
+ int Weight; // the number of covered nodes
};
-static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs );
-static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode );
-static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
-
+static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
+static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -47,212 +43,121 @@ static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type
/**Function*************************************************************
- Synopsis [Constructs the well-balanced tree of gates.]
-
- Description [Disregards levels and possible logic sharing.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pObj1, * pObj2;
- if ( nObjs == 1 )
- return ppObjs[0];
- pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type );
- pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type );
- return Ivy_Oper( pObj1, pObj2, Type );
-}
-
-/**Function*************************************************************
-
Synopsis [Constructs a balanced tree while taking sharing into account.]
- Description []
+ Description [Returns 1 if the implementation exists.]
SideEffects []
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
{
- static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5};
- static Ivy_Eval_t pEvals[15+15*14/2];
- static Ivy_Obj_t * pArgs[16];
- Ivy_Eval_t * pEva, * pEvaBest;
- int nArgsNew, nEvals, i, k;
- Ivy_Obj_t * pTemp;
-
- // consider the case of one argument
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgsInit[0];
- // consider the case of two arguments
- if ( nArgs == 2 )
- return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type );
-
-//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" );
-
- // set the initial ones
- for ( i = 0; i < nArgs; i++ )
+ static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
+ Ivy_Eva_t * pEval, * pFan0, * pFan1;
+ Ivy_Obj_t * pObj, * pTemp;
+ int nEvals, nEvalsOld, i, k, x, nLeaves;
+ unsigned uMaskAll;
+
+ // consider special cases
+ nLeaves = Vec_PtrSize(vLeaves);
+ assert( nLeaves > 2 );
+ if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT )
+ return 0;
+// if ( nLeaves == 1 )
+// return Vec_PtrEntry( vLeaves, 0 );
+// if ( nLeaves == 2 )
+// return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type );
+
+ // set the leaf entries
+ uMaskAll = ((1 << nLeaves) - 1);
+ nEvals = 0;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
{
- pArgs[i] = pArgsInit[i];
- pEva = pEvals + i;
- pEva->Mask = (1 << i);
- pEva->Weight = 1;
- pEva->Cost = 0;
- pEva->Level = Ivy_Regular(pArgs[i])->Level;
- pEva->Fan0 = 0;
- pEva->Fan1 = 0;
+ pEval = pEvals + nEvals;
+ pEval->pArg = pObj;
+ pEval->Mask = (1 << nEvals);
+ pEval->Weight = 1;
+ // mark the leaf
+ Ivy_Regular(pObj)->TravId = nEvals;
+ nEvals++;
}
- // find the available nodes
- pEvaBest = pEvals;
- nArgsNew = nArgs;
- for ( i = 1; i < nArgsNew; i++ )
- for ( k = 0; k < i; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) )
- {
- pEva = pEvals + nArgsNew;
- pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
- pEva->Weight = NumBits[pEva->Mask];
- pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
- pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
- pEva->Fan0 = k;
- pEva->Fan1 = i;
-// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) );
- // compare
- if ( pEvaBest->Weight < pEva->Weight ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
- pEvaBest = pEva;
- // save the argument
- pArgs[nArgsNew++] = pTemp;
- if ( nArgsNew == 15 )
- goto Outside;
- }
-Outside:
-
-// printf( "Best = %d.\n", pEvaBest - pEvals );
-
- // the case of no common nodes
- if ( nArgsNew == nArgs )
+ // propagate masks through the cone
+ Vec_PtrForEachEntry( vCone, pObj, i )
{
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ pObj->TravId = nEvals + i;
+ if ( Ivy_ObjIsBuf(pObj) )
+ pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask;
+ else
+ pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask;
}
- // the case of one common node
- if ( nArgsNew == nArgs + 1 )
+
+ // set the internal entries
+ Vec_PtrForEachEntry( vCone, pObj, i )
{
- assert( pEvaBest - pEvals == nArgs );
- k = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 )
- pArgs[k++] = pArgs[i];
- pArgs[k++] = pArgs[nArgs];
- assert( k == nArgs - 1 );
- nArgs = k;
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ if ( i == Vec_PtrSize(vCone) - 1 )
+ break;
+ // skip buffers
+ if ( Ivy_ObjIsBuf(pObj) )
+ continue;
+ // skip nodes without external fanout
+ if ( Ivy_ObjRefs(pObj) == 0 )
+ continue;
+ assert( !Ivy_IsComplement(pObj) );
+ pEval = pEvals + nEvals;
+ pEval->pArg = pObj;
+ pEval->Mask = pEvals[pObj->TravId].Mask;
+ pEval->Weight = Extra_WordCountOnes(pEval->Mask);
+ // mark the node
+ pObj->TravId = nEvals;
+ nEvals++;
}
- // the case when there is a node that covers everything
- if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) )
- return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
- // evaluate node pairs
- nEvals = nArgsNew;
- for ( i = 1; i < nArgsNew; i++ )
+ // find the available nodes
+ nEvalsOld = nEvals;
+ for ( i = 1; i < nEvals; i++ )
for ( k = 0; k < i; k++ )
{
- pEva = pEvals + nEvals;
- pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
- pEva->Weight = NumBits[pEva->Mask];
- pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
- pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
- pEva->Fan0 = k;
- pEva->Fan1 = i;
- // compare
- if ( pEvaBest->Weight < pEva->Weight ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
- pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
- pEvaBest = pEva;
+ pFan0 = pEvals + i;
+ pFan1 = pEvals + k;
+ pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
+ // skip nodes in the cone
+ if ( pTemp == NULL || pTemp->fMarkB )
+ continue;
+ // skip the leaves
+ for ( x = 0; x < nLeaves; x++ )
+ if ( pTemp == Ivy_Regular(vLeaves->pArray[x]) )
+ break;
+ if ( x < nLeaves )
+ continue;
+ pEval = pEvals + nEvals;
+ pEval->pArg = pTemp;
+ pEval->Mask = pFan0->Mask | pFan1->Mask;
+ pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight;
// save the argument
+ pObj->TravId = nEvals;
nEvals++;
+ // quit if the number of entries exceeded the limit
+ if ( nEvals == IVY_EVAL_LIMIT )
+ goto Outside;
+ // quit if we found an acceptable implementation
+ if ( pEval->Mask == uMaskAll )
+ goto Outside;
}
- assert( pEvaBest - pEvals >= nArgsNew );
-
-// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 );
-
- // get the best implementation
- pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
-
- // collect those not covered by EvaBest
- k = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( (pEvaBest->Mask & (1 << i)) == 0 )
- pArgs[k++] = pArgs[i];
- pArgs[k++] = pTemp;
- assert( k == nArgs - (int)pEvaBest->Weight + 1 );
- nArgs = k;
- Ivy_MultiSort( pArgs, nArgs );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements multi-input AND/EXOR operation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pNode0, * pNode1;
- if ( iNum < nArgs )
- return pArgs[iNum];
- pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type );
- pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type );
- return Ivy_Oper( pNode0, pNode1, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Selection-sorts the nodes in the decreasing over of level.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
-{
- Ivy_Obj_t * pTemp;
- int i, j, iBest;
+Outside:
- for ( i = 0; i < nArgs-1; i++ )
- {
- iBest = i;
- for ( j = i+1; j < nArgs; j++ )
- if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level )
- iBest = j;
- pTemp = pArgs[i];
- pArgs[i] = pArgs[iBest];
- pArgs[iBest] = pTemp;
- }
+// Ivy_MultiPrint( pEvals, nLeaves, nEvals );
+ if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) )
+ return 0;
+ assert( Vec_PtrSize( vSols ) > 0 );
+ return 1;
}
/**Function*************************************************************
- Synopsis [Inserts a new node in the order by levels.]
+ Synopsis [Computes how many uncovered ones this one covers.]
Description []
@@ -261,32 +166,28 @@ void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
SeeAlso []
***********************************************************************/
-int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode )
+void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
{
- Ivy_Obj_t * pNode1, * pNode2;
- int i;
- // try to find the node in the array
- for ( i = 0; i < nArgs; i++ )
- if ( pArray[i] == pNode )
- return nArgs;
- // put the node last
- pArray[nArgs++] = pNode;
- // find the place to put the new node
- for ( i = nArgs-1; i > 0; i-- )
+ Ivy_Eva_t * pEval;
+ int i, k;
+ for ( i = nLeaves; i < nEvals; i++ )
{
- pNode1 = pArray[i ];
- pNode2 = pArray[i-1];
- if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
- break;
- pArray[i ] = pNode2;
- pArray[i-1] = pNode1;
+ pEval = pEvals + i;
+ printf( "%2d (id = %5d) : |", i-nLeaves, Ivy_ObjId(pEval->pArg) );
+ for ( k = 0; k < nLeaves; k++ )
+ {
+ if ( pEval->Mask & (1 << k) )
+ printf( "+" );
+ else
+ printf( " " );
+ }
+ printf( "| Lev = %d.\n", Ivy_ObjLevel(pEval->pArg) );
}
- return nArgs;
}
/**Function*************************************************************
- Synopsis [Balances the array recursively.]
+ Synopsis [Computes how many uncovered ones this one covers.]
Description []
@@ -295,129 +196,102 @@ int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t *
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFound )
{
- Ivy_Obj_t * pNodeNew;
- // consider the case of one argument
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgs[0];
- // consider the case of two arguments
- if ( nArgs == 2 )
- return Ivy_Oper( pArgs[0], pArgs[1], Type );
- // get the last two nodes
- pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type );
- // add the new node
- nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew );
- return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ assert( uMask & ~uFound );
+ if ( (uMask & uFound) == 0 )
+ return nMaskOnes;
+ return Extra_WordCountOnes( uMask & ~uFound );
}
/**Function*************************************************************
- Synopsis [Implements multi-input AND/EXOR operation.]
+ Synopsis [Finds the cover.]
- Description []
+ Description [Returns 1 if the cover is found.]
SideEffects []
SeeAlso []
***********************************************************************/
-Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
{
- Ivy_Obj_t * pTemp;
- int i, k;
- int nArgsOld = nArgs;
- for ( i = 0; i < nArgs; i++ )
- printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level );
- for ( i = 1; i < nArgs; i++ )
- for ( k = 0; k < i; k++ )
+ int fVerbose = 0;
+ Ivy_Eva_t * pEval, * pEvalBest;
+ unsigned uMaskAll, uFound, uTemp;
+ int i, k, BestK, WeightBest, WeightCur, LevelBest, LevelCur;
+ uMaskAll = (nLeaves == 32)? (~(unsigned)0) : ((1 << nLeaves) - 1);
+ uFound = 0;
+ // solve the covering problem
+ if ( fVerbose )
+ printf( "Solution: " );
+ Vec_PtrClear( vSols );
+ for ( i = 0; i < nLimit; i++ )
+ {
+ BestK = -1;
+ for ( k = nEvals - 1; k >= 0; k-- )
{
- pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE));
- if ( pTemp != NULL )
+ pEval = pEvals + k;
+ if ( (pEval->Mask & ~uFound) == 0 )
+ continue;
+ if ( BestK == -1 )
{
- printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i );
- pArgs[nArgs++] = pTemp;
+ BestK = k;
+ pEvalBest = pEval;
+ WeightBest = Ivy_MultiWeight( pEvalBest->Mask, pEvalBest->Weight, uFound );
+ LevelBest = Ivy_ObjLevel( Ivy_Regular(pEvalBest->pArg) );
+ continue;
+ }
+ // compare BestK and the new one (k)
+ WeightCur = Ivy_MultiWeight( pEval->Mask, pEval->Weight, uFound );
+ LevelCur = Ivy_ObjLevel( Ivy_Regular(pEval->pArg) );
+ if ( WeightBest < WeightCur ||
+ (WeightBest == WeightCur && LevelBest > LevelCur) )
+ {
+ BestK = k;
+ pEvalBest = pEval;
+ WeightBest = WeightCur;
+ LevelBest = LevelCur;
}
}
- printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld );
- return NULL;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Old code.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- Ivy_Obj_t * pArgsRef[5], * pTemp;
- int i, k, m, nArgsNew, Counter = 0;
-
-
-//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" );
-
-
- assert( Type == IVY_AND || Type == IVY_EXOR );
- assert( nArgs > 0 );
- if ( nArgs == 1 )
- return pArgs[0];
-
- // find the nodes with more than one fanout
- nArgsNew = 0;
- for ( i = 0; i < nArgs; i++ )
- if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 )
- pArgsRef[nArgsNew++] = pArgs[i];
-
- // go through pairs
- if ( nArgsNew >= 2 )
- for ( i = 0; i < nArgsNew; i++ )
- for ( k = i + 1; k < nArgsNew; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
- Counter++;
-// printf( "%d", Counter );
-
- // go through pairs
- if ( nArgsNew >= 2 )
- for ( i = 0; i < nArgsNew; i++ )
- for ( k = i + 1; k < nArgsNew; k++ )
- if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+ assert( BestK != -1 );
+ // if the cost is only 1, take the leaf
+ if ( WeightBest == 1 && BestK >= nLeaves )
{
- nArgsNew = 0;
- for ( m = 0; m < nArgs; m++ )
- if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] )
- pArgs[nArgsNew++] = pArgs[m];
- pArgs[nArgsNew++] = pTemp;
- assert( nArgsNew == nArgs - 1 );
- return Ivy_Multi1( pArgs, nArgsNew, Type );
+ uTemp = (pEvalBest->Mask & ~uFound);
+ for ( k = 0; k < nLeaves; k++ )
+ if ( uTemp & (1 << k) )
+ break;
+ assert( k < nLeaves );
+ BestK = k;
+ pEvalBest = pEvals + BestK;
}
- return Ivy_Multi_rec( pArgs, nArgs, Type );
-}
-
-/**Function*************************************************************
-
- Synopsis [Old code.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
-{
- assert( Type == IVY_AND || Type == IVY_EXOR );
- assert( nArgs > 0 );
- return Ivy_Multi_rec( pArgs, nArgs, Type );
+ if ( fVerbose )
+ {
+ if ( BestK < nLeaves )
+ printf( "L(%d) ", BestK );
+ else
+ printf( "%d ", BestK - nLeaves );
+ }
+ // update the found set
+ Vec_PtrPush( vSols, pEvalBest->pArg );
+ uFound |= pEvalBest->Mask;
+ if ( uFound == uMaskAll )
+ break;
+ }
+ if ( uFound == uMaskAll )
+ {
+ if ( fVerbose )
+ printf( " Found \n\n" );
+ return 1;
+ }
+ else
+ {
+ if ( fVerbose )
+ printf( " Not found \n\n" );
+ return 0;
+ }
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/ivyMulti8.c b/src/temp/ivy/ivyMulti8.c
new file mode 100644
index 00000000..059d1500
--- /dev/null
+++ b/src/temp/ivy/ivyMulti8.c
@@ -0,0 +1,427 @@
+/**CFile****************************************************************
+
+ FileName [ivyMulti.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Constructing multi-input AND/EXOR gates.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyMulti.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Eval_t_ Ivy_Eval_t;
+struct Ivy_Eval_t_
+{
+ unsigned Mask : 5; // the mask of covered nodes
+ unsigned Weight : 3; // the number of covered nodes
+ unsigned Cost : 4; // the number of overlapping nodes
+ unsigned Level : 12; // the level of this node
+ unsigned Fan0 : 4; // the first fanin
+ unsigned Fan1 : 4; // the second fanin
+};
+
+static Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+static void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs );
+static int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode );
+static Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type );
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Constructs the well-balanced tree of gates.]
+
+ Description [Disregards levels and possible logic sharing.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi_rec( Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+ Ivy_Obj_t * pObj1, * pObj2;
+ if ( nObjs == 1 )
+ return ppObjs[0];
+ pObj1 = Ivy_Multi_rec( ppObjs, nObjs/2, Type );
+ pObj2 = Ivy_Multi_rec( ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+ return Ivy_Oper( pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Constructs a balanced tree while taking sharing into account.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Obj_t ** pArgsInit, int nArgs, Ivy_Type_t Type )
+{
+ static char NumBits[32] = {0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5};
+ static Ivy_Eval_t pEvals[15+15*14/2];
+ static Ivy_Obj_t * pArgs[16];
+ Ivy_Eval_t * pEva, * pEvaBest;
+ int nArgsNew, nEvals, i, k;
+ Ivy_Obj_t * pTemp;
+
+ // consider the case of one argument
+ assert( nArgs > 0 );
+ if ( nArgs == 1 )
+ return pArgsInit[0];
+ // consider the case of two arguments
+ if ( nArgs == 2 )
+ return Ivy_Oper( pArgsInit[0], pArgsInit[1], Type );
+
+//Ivy_MultiEval( pArgsInit, nArgs, Type ); printf( "\n" );
+
+ // set the initial ones
+ for ( i = 0; i < nArgs; i++ )
+ {
+ pArgs[i] = pArgsInit[i];
+ pEva = pEvals + i;
+ pEva->Mask = (1 << i);
+ pEva->Weight = 1;
+ pEva->Cost = 0;
+ pEva->Level = Ivy_Regular(pArgs[i])->Level;
+ pEva->Fan0 = 0;
+ pEva->Fan1 = 0;
+ }
+
+ // find the available nodes
+ pEvaBest = pEvals;
+ nArgsNew = nArgs;
+ for ( i = 1; i < nArgsNew; i++ )
+ for ( k = 0; k < i; k++ )
+ if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE)) )
+ {
+ pEva = pEvals + nArgsNew;
+ pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
+ pEva->Weight = NumBits[pEva->Mask];
+ pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
+ pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
+ pEva->Fan0 = k;
+ pEva->Fan1 = i;
+// assert( pEva->Level == (unsigned)Ivy_ObjLevel(pTemp) );
+ // compare
+ if ( pEvaBest->Weight < pEva->Weight ||
+ pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
+ pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
+ pEvaBest = pEva;
+ // save the argument
+ pArgs[nArgsNew++] = pTemp;
+ if ( nArgsNew == 15 )
+ goto Outside;
+ }
+Outside:
+
+// printf( "Best = %d.\n", pEvaBest - pEvals );
+
+ // the case of no common nodes
+ if ( nArgsNew == nArgs )
+ {
+ Ivy_MultiSort( pArgs, nArgs );
+ return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ }
+ // the case of one common node
+ if ( nArgsNew == nArgs + 1 )
+ {
+ assert( pEvaBest - pEvals == nArgs );
+ k = 0;
+ for ( i = 0; i < nArgs; i++ )
+ if ( i != (int)pEvaBest->Fan0 && i != (int)pEvaBest->Fan1 )
+ pArgs[k++] = pArgs[i];
+ pArgs[k++] = pArgs[nArgs];
+ assert( k == nArgs - 1 );
+ nArgs = k;
+ Ivy_MultiSort( pArgs, nArgs );
+ return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+ }
+ // the case when there is a node that covers everything
+ if ( (int)pEvaBest->Mask == ((1 << nArgs) - 1) )
+ return Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
+
+ // evaluate node pairs
+ nEvals = nArgsNew;
+ for ( i = 1; i < nArgsNew; i++ )
+ for ( k = 0; k < i; k++ )
+ {
+ pEva = pEvals + nEvals;
+ pEva->Mask = pEvals[k].Mask | pEvals[i].Mask;
+ pEva->Weight = NumBits[pEva->Mask];
+ pEva->Cost = pEvals[k].Cost + pEvals[i].Cost + NumBits[pEvals[k].Mask & pEvals[i].Mask];
+ pEva->Level = 1 + IVY_MAX(pEvals[k].Level, pEvals[i].Level);
+ pEva->Fan0 = k;
+ pEva->Fan1 = i;
+ // compare
+ if ( pEvaBest->Weight < pEva->Weight ||
+ pEvaBest->Weight == pEva->Weight && pEvaBest->Cost > pEva->Cost ||
+ pEvaBest->Weight == pEva->Weight && pEvaBest->Cost == pEva->Cost && pEvaBest->Level > pEva->Level )
+ pEvaBest = pEva;
+ // save the argument
+ nEvals++;
+ }
+ assert( pEvaBest - pEvals >= nArgsNew );
+
+// printf( "Used (%d, %d).\n", pEvaBest->Fan0, pEvaBest->Fan1 );
+
+ // get the best implementation
+ pTemp = Ivy_MultiBuild_rec( pEvals, pEvaBest - pEvals, pArgs, nArgsNew, Type );
+
+ // collect those not covered by EvaBest
+ k = 0;
+ for ( i = 0; i < nArgs; i++ )
+ if ( (pEvaBest->Mask & (1 << i)) == 0 )
+ pArgs[k++] = pArgs[i];
+ pArgs[k++] = pTemp;
+ assert( k == nArgs - (int)pEvaBest->Weight + 1 );
+ nArgs = k;
+ Ivy_MultiSort( pArgs, nArgs );
+ return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements multi-input AND/EXOR operation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiBuild_rec( Ivy_Eval_t * pEvals, int iNum, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+ Ivy_Obj_t * pNode0, * pNode1;
+ if ( iNum < nArgs )
+ return pArgs[iNum];
+ pNode0 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan0, pArgs, nArgs, Type );
+ pNode1 = Ivy_MultiBuild_rec( pEvals, pEvals[iNum].Fan1, pArgs, nArgs, Type );
+ return Ivy_Oper( pNode0, pNode1, Type );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Selection-sorts the nodes in the decreasing over of level.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_MultiSort( Ivy_Obj_t ** pArgs, int nArgs )
+{
+ Ivy_Obj_t * pTemp;
+ int i, j, iBest;
+
+ for ( i = 0; i < nArgs-1; i++ )
+ {
+ iBest = i;
+ for ( j = i+1; j < nArgs; j++ )
+ if ( Ivy_Regular(pArgs[j])->Level > Ivy_Regular(pArgs[iBest])->Level )
+ iBest = j;
+ pTemp = pArgs[i];
+ pArgs[i] = pArgs[iBest];
+ pArgs[iBest] = pTemp;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Inserts a new node in the order by levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_MultiPushUniqueOrderByLevel( Ivy_Obj_t ** pArray, int nArgs, Ivy_Obj_t * pNode )
+{
+ Ivy_Obj_t * pNode1, * pNode2;
+ int i;
+ // try to find the node in the array
+ for ( i = 0; i < nArgs; i++ )
+ if ( pArray[i] == pNode )
+ return nArgs;
+ // put the node last
+ pArray[nArgs++] = pNode;
+ // find the place to put the new node
+ for ( i = nArgs-1; i > 0; i-- )
+ {
+ pNode1 = pArray[i ];
+ pNode2 = pArray[i-1];
+ if ( Ivy_Regular(pNode1)->Level <= Ivy_Regular(pNode2)->Level )
+ break;
+ pArray[i ] = pNode2;
+ pArray[i-1] = pNode1;
+ }
+ return nArgs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Balances the array recursively.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiBalance_rec( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+ Ivy_Obj_t * pNodeNew;
+ // consider the case of one argument
+ assert( nArgs > 0 );
+ if ( nArgs == 1 )
+ return pArgs[0];
+ // consider the case of two arguments
+ if ( nArgs == 2 )
+ return Ivy_Oper( pArgs[0], pArgs[1], Type );
+ // get the last two nodes
+ pNodeNew = Ivy_Oper( pArgs[nArgs-1], pArgs[nArgs-2], Type );
+ // add the new node
+ nArgs = Ivy_MultiPushUniqueOrderByLevel( pArgs, nArgs - 2, pNodeNew );
+ return Ivy_MultiBalance_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements multi-input AND/EXOR operation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_MultiEval( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+ Ivy_Obj_t * pTemp;
+ int i, k;
+ int nArgsOld = nArgs;
+ for ( i = 0; i < nArgs; i++ )
+ printf( "%d[%d] ", i, Ivy_Regular(pArgs[i])->Level );
+ for ( i = 1; i < nArgs; i++ )
+ for ( k = 0; k < i; k++ )
+ {
+ pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgs[k], pArgs[i], Type, IVY_INIT_NONE));
+ if ( pTemp != NULL )
+ {
+ printf( "%d[%d]=(%d,%d) ", nArgs, Ivy_Regular(pTemp)->Level, k, i );
+ pArgs[nArgs++] = pTemp;
+ }
+ }
+ printf( " ((%d/%d)) ", nArgsOld, nArgs-nArgsOld );
+ return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Old code.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi1( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+ Ivy_Obj_t * pArgsRef[5], * pTemp;
+ int i, k, m, nArgsNew, Counter = 0;
+
+
+//Ivy_MultiEval( pArgs, nArgs, Type ); printf( "\n" );
+
+
+ assert( Type == IVY_AND || Type == IVY_EXOR );
+ assert( nArgs > 0 );
+ if ( nArgs == 1 )
+ return pArgs[0];
+
+ // find the nodes with more than one fanout
+ nArgsNew = 0;
+ for ( i = 0; i < nArgs; i++ )
+ if ( Ivy_ObjRefs( Ivy_Regular(pArgs[i]) ) > 0 )
+ pArgsRef[nArgsNew++] = pArgs[i];
+
+ // go through pairs
+ if ( nArgsNew >= 2 )
+ for ( i = 0; i < nArgsNew; i++ )
+ for ( k = i + 1; k < nArgsNew; k++ )
+ if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+ Counter++;
+// printf( "%d", Counter );
+
+ // go through pairs
+ if ( nArgsNew >= 2 )
+ for ( i = 0; i < nArgsNew; i++ )
+ for ( k = i + 1; k < nArgsNew; k++ )
+ if ( pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pArgsRef[i], pArgsRef[k], Type, IVY_INIT_NONE)) )
+ {
+ nArgsNew = 0;
+ for ( m = 0; m < nArgs; m++ )
+ if ( pArgs[m] != pArgsRef[i] && pArgs[m] != pArgsRef[k] )
+ pArgs[nArgsNew++] = pArgs[m];
+ pArgs[nArgsNew++] = pTemp;
+ assert( nArgsNew == nArgs - 1 );
+ return Ivy_Multi1( pArgs, nArgsNew, Type );
+ }
+ return Ivy_Multi_rec( pArgs, nArgs, Type );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Old code.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi2( Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+ assert( Type == IVY_AND || Type == IVY_EXOR );
+ assert( nArgs > 0 );
+ return Ivy_Multi_rec( pArgs, nArgs, Type );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c
index 5d063525..703218bb 100644
--- a/src/temp/ivy/ivyObj.c
+++ b/src/temp/ivy/ivyObj.c
@@ -51,6 +51,7 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Obj_t * pGhost )
// realloc the node array
if ( p->ObjIdNext == p->nObjsAlloc )
{
+ printf( "AIG manager is being resized. In the current release, it is not allowed!\n" );
Ivy_ManGrow( p );
pGhost = Ivy_ManGhost( p );
}
diff --git a/src/temp/ivy/ivyOper.c b/src/temp/ivy/ivyOper.c
index a10ba343..96f78165 100644
--- a/src/temp/ivy/ivyOper.c
+++ b/src/temp/ivy/ivyOper.c
@@ -81,7 +81,7 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
{
Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
- Ivy_Obj_t * pFan0, * pFan1;
+// Ivy_Obj_t * pFan0, * pFan1;
// check trivial cases
if ( p0 == p1 )
return p0;
@@ -92,8 +92,8 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
if ( Ivy_Regular(p1) == pConst1 )
return p1 == pConst1 ? p0 : Ivy_Not(pConst1);
// check if it can be an EXOR gate
- if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
- return Ivy_CanonExor( pFan0, pFan1 );
+// if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
+// return Ivy_CanonExor( pFan0, pFan1 );
return Ivy_CanonAnd( p0, p1 );
}
diff --git a/src/temp/ivy/ivyResyn.c b/src/temp/ivy/ivyResyn.c
new file mode 100644
index 00000000..2d65e7f7
--- /dev/null
+++ b/src/temp/ivy/ivyResyn.c
@@ -0,0 +1,96 @@
+/**CFile****************************************************************
+
+ FileName [ivyResyn.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [AIG rewriting script.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyResyn.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs several passes of rewriting on the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel )
+{
+ int clk, fVerbose = 0;
+ Ivy_Man_t * pTemp;
+
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+clk = clock();
+ pMan = Ivy_ManBalance( pMan, fUpdateLevel );
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
+clk = clock();
+ Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
+clk = clock();
+if ( fVerbose ) Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+// Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
+clk = clock();
+ Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
+ Ivy_ManStop( pTemp );
+if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
+if ( fVerbose ) Ivy_ManPrintStats( pMan );
+ return pMan;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c
new file mode 100644
index 00000000..234827ff
--- /dev/null
+++ b/src/temp/ivy/ivyRwrAlg.c
@@ -0,0 +1,408 @@
+/**CFile****************************************************************
+
+ FileName [ivyRwrAlg.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Algebraic AIG rewriting.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyRwrAlg.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone );
+static Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost );
+static int Ivy_NodeCountMffc( Ivy_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Algebraic AIG rewriting.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost )
+{
+ Vec_Int_t * vRequired;
+ Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol;
+ Ivy_Obj_t * pObj, * pResult;
+ int i, RetValue, LevelR, nNodesOld;
+ int CountUsed, CountUndo;
+ vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL;
+ vFront = Vec_PtrAlloc( 100 );
+ vLeaves = Vec_PtrAlloc( 100 );
+ vCone = Vec_PtrAlloc( 100 );
+ vSol = Vec_PtrAlloc( 100 );
+ // go through the nodes in the topological order
+ CountUsed = CountUndo = 0;
+ nNodesOld = Ivy_ManObjIdNext(p);
+ Ivy_ManForEachObj( p, pObj, i )
+ {
+ assert( !Ivy_ObjIsBuf(pObj) );
+ if ( i >= nNodesOld )
+ break;
+ // skip no-nodes and MUX roots
+ if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) )
+ continue;
+// if ( pObj->Id > 297 ) // 296 --- 297
+// break;
+ if ( pObj->Id == 297 )
+ {
+ int x = 0;
+ }
+ // get the largest algebraic cut
+ RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone );
+ // the case of a trivial tree cut
+ if ( RetValue == 1 )
+ continue;
+ // the case of constant 0 cone
+ if ( RetValue == -1 )
+ {
+ Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 );
+ continue;
+ }
+ assert( Vec_PtrSize(vLeaves) > 2 );
+ // get the required level for this node
+ LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000;
+ // create a new cone
+ pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost );
+ if ( pResult == NULL || pResult == pObj )
+ continue;
+ assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) );
+ if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 )
+ Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++;
+ else
+ Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++;
+ }
+ printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo );
+ Vec_PtrFree( vFront );
+ Vec_PtrFree( vCone );
+ Vec_PtrFree( vSol );
+ if ( vRequired ) Vec_IntFree( vRequired );
+ if ( i = Ivy_ManCleanup(p) )
+ printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+ if ( !Ivy_ManCheck(p) )
+ printf( "Ivy_ManRewriteAlg(): The check has failed.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Analizes one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_NodeRewriteAlg( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vSols, int LevelR, int fUseZeroCost )
+{
+ int fVerbose = 0;
+ Ivy_Obj_t * pTemp;
+ int k, Counter, nMffc, RetValue;
+
+ if ( fVerbose )
+ {
+ if ( Ivy_ObjIsExor(pObj) )
+ printf( "x " );
+ else
+ printf( " " );
+ }
+
+/*
+ printf( "%d ", Vec_PtrSize(vFront) );
+ printf( "( " );
+ Vec_PtrForEachEntry( vFront, pTemp, k )
+ printf( "%d ", Ivy_ObjRefs(Ivy_Regular(pTemp)) );
+ printf( ")\n" );
+*/
+ // collect nodes in the cone
+ if ( Ivy_ObjIsExor(pObj) )
+ Ivy_ManCollectCone( pObj, vFront, vCone );
+ else
+ Ivy_ManCollectCone( pObj, vLeaves, vCone );
+
+ // deref nodes in the cone
+ Vec_PtrForEachEntry( vCone, pTemp, k )
+ {
+ Ivy_ObjRefsDec( Ivy_ObjFanin0(pTemp) );
+ Ivy_ObjRefsDec( Ivy_ObjFanin1(pTemp) );
+ pTemp->fMarkB = 1;
+ }
+
+ // count the MFFC size
+ Vec_PtrForEachEntry( vFront, pTemp, k )
+ Ivy_Regular(pTemp)->fMarkA = 1;
+ nMffc = Ivy_NodeCountMffc( pObj );
+ Vec_PtrForEachEntry( vFront, pTemp, k )
+ Ivy_Regular(pTemp)->fMarkA = 0;
+
+ if ( fVerbose )
+ {
+ Counter = 0;
+ Vec_PtrForEachEntry( vCone, pTemp, k )
+ Counter += (Ivy_ObjRefs(pTemp) > 0);
+ printf( "%5d : Leaves = %2d. Cone = %2d. ConeRef = %2d. Mffc = %d. Lev = %d. LevR = %d.\n",
+ pObj->Id, Vec_PtrSize(vFront), Vec_PtrSize(vCone), Counter-1, nMffc, Ivy_ObjLevel(pObj), LevelR );
+ }
+/*
+ printf( "Leaves:" );
+ Vec_PtrForEachEntry( vLeaves, pTemp, k )
+ printf( " %d%s", Ivy_Regular(pTemp)->Id, Ivy_IsComplement(pTemp)? "\'" : "" );
+ printf( "\n" );
+ printf( "Cone:\n" );
+ Vec_PtrForEachEntry( vCone, pTemp, k )
+ printf( " %5d = %d%s %d%s\n", pTemp->Id,
+ Ivy_ObjFaninId0(pTemp), Ivy_ObjFaninC0(pTemp)? "\'" : "",
+ Ivy_ObjFaninId1(pTemp), Ivy_ObjFaninC1(pTemp)? "\'" : "" );
+*/
+
+ RetValue = Ivy_MultiPlus( vLeaves, vCone, Ivy_ObjType(pObj), nMffc + fUseZeroCost, vSols );
+
+ // ref nodes in the cone
+ Vec_PtrForEachEntry( vCone, pTemp, k )
+ {
+ Ivy_ObjRefsInc( Ivy_ObjFanin0(pTemp) );
+ Ivy_ObjRefsInc( Ivy_ObjFanin1(pTemp) );
+ pTemp->fMarkA = 0;
+ pTemp->fMarkB = 0;
+ }
+
+ if ( !RetValue )
+ return NULL;
+
+ if ( Vec_PtrSize( vSols ) == 1 )
+ return Vec_PtrEntry( vSols, 0 );
+ return Ivy_NodeBalanceBuildSuper( vSols, Ivy_ObjType(pObj), 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Comparison for node pointers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCountMffc_rec( Ivy_Obj_t * pNode )
+{
+ if ( Ivy_ObjRefs(pNode) > 0 || Ivy_ObjIsCi(pNode) || pNode->fMarkA )
+ return 0;
+ assert( pNode->fMarkB );
+ pNode->fMarkA = 1;
+// printf( "%d ", pNode->Id );
+ if ( Ivy_ObjIsBuf(pNode) )
+ return Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) );
+ return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Comparison for node pointers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeCountMffc( Ivy_Obj_t * pNode )
+{
+ assert( pNode->fMarkB );
+ return 1 + Ivy_NodeCountMffc_rec( Ivy_ObjFanin0(pNode) ) + Ivy_NodeCountMffc_rec( Ivy_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Comparison for node pointers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCutCompare( Ivy_Obj_t ** pp1, Ivy_Obj_t ** pp2 )
+{
+ if ( *pp1 < *pp2 )
+ return -1;
+ if ( *pp1 > *pp2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computing one algebraic cut.]
+
+ Description [Returns 1 if the tree-leaves of this node where traversed
+ and found to have no external references (and have not been collected).
+ Returns 0 if the tree-leaves have external references and are collected.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut_rec( Ivy_Obj_t * pObj, Ivy_Type_t Type, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone )
+{
+ int RetValue0, RetValue1;
+ Ivy_Obj_t * pObjR = Ivy_Regular(pObj);
+ assert( !Ivy_ObjIsBuf(pObjR) );
+ assert( Type != IVY_EXOR || !Ivy_IsComplement(pObj) );
+
+ // make sure the node is not visited twice in different polarities
+ if ( Ivy_IsComplement(pObj) )
+ { // if complemented, mark B
+ if ( pObjR->fMarkA )
+ return -1;
+ pObjR->fMarkB = 1;
+ }
+ else
+ { // if non-complicated, mark A
+ if ( pObjR->fMarkB )
+ return -1;
+ pObjR->fMarkA = 1;
+ }
+ Vec_PtrPush( vCone, pObjR );
+
+ // if the node is the end of the tree, return
+ if ( Ivy_IsComplement(pObj) || Ivy_ObjType(pObj) != Type )
+ {
+ if ( Ivy_ObjRefs(pObjR) == 1 )
+ return 1;
+ assert( Ivy_ObjRefs(pObjR) > 1 );
+ Vec_PtrPush( vFront, pObj );
+ return 0;
+ }
+
+ // branch on the node
+ assert( !Ivy_IsComplement(pObj) );
+ assert( Ivy_ObjIsNode(pObj) );
+ // what if buffer has more than one fanout???
+ RetValue0 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild0(pObj) ), Type, vFront, vCone );
+ RetValue1 = Ivy_ManFindAlgCut_rec( Ivy_ObjReal( Ivy_ObjChild1(pObj) ), Type, vFront, vCone );
+ if ( RetValue0 == -1 || RetValue1 == -1 )
+ return -1;
+
+ // the case when both have no external references
+ if ( RetValue0 && RetValue1 )
+ {
+ if ( Ivy_ObjRefs(pObj) == 1 )
+ return 1;
+ assert( Ivy_ObjRefs(pObj) > 1 );
+ Vec_PtrPush( vFront, pObj );
+ return 0;
+ }
+ // the case when one of them has external references
+ if ( RetValue0 )
+ Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild0(pObj) ) );
+ if ( RetValue1 )
+ Vec_PtrPush( vFront, Ivy_ObjReal( Ivy_ObjChild1(pObj) ) );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computing one algebraic cut.]
+
+ Description [Algebraic cut stops when we hit (a) CI, (b) complemented edge,
+ (c) boundary of different gates. Returns 1 if this is a pure tree.
+ Returns -1 if the contant 0 is detected. Return 0 if the array can be used.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManFindAlgCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone )
+{
+ Ivy_Obj_t * pObj, * pPrev;
+ int RetValue, i;
+ assert( !Ivy_IsComplement(pRoot) );
+ assert( Ivy_ObjIsNode(pRoot) );
+ // clear the frontier and collect the nodes
+ Vec_PtrClear( vCone );
+ Vec_PtrClear( vFront );
+ Vec_PtrClear( vLeaves );
+ RetValue = Ivy_ManFindAlgCut_rec( pRoot, Ivy_ObjType(pRoot), vFront, vCone );
+ // clean the marks
+ Vec_PtrForEachEntry( vCone, pObj, i )
+ pObj->fMarkA = pObj->fMarkB = 0;
+ // quit if the same node is found in both polarities
+ if ( RetValue == -1 )
+ return -1;
+ // return if the node is the root of a tree
+ if ( RetValue == 1 )
+ return 1;
+ // return if the cut is composed of two nodes
+ if ( Vec_PtrSize(vFront) <= 2 )
+ return 1;
+ // sort the entries in increasing order
+ Vec_PtrSort( vFront, Ivy_ManFindAlgCutCompare );
+ // remove duplicates from vFront and save the nodes in vLeaves
+ pPrev = Vec_PtrEntry(vFront, 0);
+ Vec_PtrPush( vLeaves, pPrev );
+ Vec_PtrForEachEntryStart( vFront, pObj, i, 1 )
+ {
+ // compare current entry and the previous entry
+ if ( pObj == pPrev )
+ {
+ if ( Ivy_ObjIsExor(pRoot) ) // A <+> A = 0
+ {
+ // vLeaves are no longer structural support of pRoot!!!
+ Vec_PtrPop(vLeaves);
+ pPrev = Vec_PtrSize(vLeaves) == 0 ? NULL : Vec_PtrEntryLast(vLeaves);
+ }
+ continue;
+ }
+ if ( pObj == Ivy_Not(pPrev) )
+ {
+ assert( Ivy_ObjIsAnd(pRoot) );
+ return -1;
+ }
+ pPrev = pObj;
+ Vec_PtrPush( vLeaves, pObj );
+ }
+ if ( Vec_PtrSize(vLeaves) == 0 )
+ return -1;
+ if ( Vec_PtrSize(vLeaves) <= 2 )
+ return 1;
+ return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c
new file mode 100644
index 00000000..243ab261
--- /dev/null
+++ b/src/temp/ivy/ivyRwrPre.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+ FileName [ivyRwtPre.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [And-Inverter Graph package.]
+
+ Synopsis [Rewriting based on precomputation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - May 11, 2006.]
+
+ Revision [$Id: ivyRwtPre.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+#include "deco.h"
+#include "rwt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums );
+static int Ivy_NodeMffcLabel( Ivy_Obj_t * pObj );
+static int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost );
+static Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut,
+ Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth );
+
+static int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+static void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs incremental rewriting of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose )
+{
+ Rwt_Man_t * pManRwt;
+ Ivy_Obj_t * pNode;
+ int i, nNodes, nGain;
+ int clk, clkStart = clock();
+ // start the rewriting manager
+ pManRwt = Rwt_ManStart( 0 );
+ if ( pManRwt == NULL )
+ return 0;
+ // compute the reverse levels if level update is requested
+ if ( fUpdateLevel )
+ Ivy_ManRequiredLevels( p );
+ // resynthesize each node once
+ nNodes = Ivy_ManObjIdNext( p );
+ Ivy_ManForEachObj( p, pNode, i )
+ {
+ if ( !Ivy_ObjIsNode(pNode) )
+ continue;
+ // fix the fanin buffer problem
+ Ivy_NodeFixBufferFanins( pNode );
+ if ( Ivy_ObjIsBuf(pNode) )
+ continue;
+ // stop if all nodes have been tried once
+ if ( i >= nNodes )
+ break;
+ // skip the nodes with many fanouts
+// if ( Ivy_ObjRefs(pNode) > 1000 )
+// continue;
+ // for each cut, try to resynthesize it
+ nGain = Rwt_NodeRewrite( pManRwt, pNode, fUpdateLevel, fUseZeroCost );
+ if ( nGain > 0 || nGain == 0 && fUseZeroCost )
+ {
+ Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt);
+ int fCompl = Rwt_ManReadCompl(pManRwt);
+/*
+ {
+ Ivy_Obj_t * pObj;
+ int i;
+ printf( "USING: (" );
+ Vec_PtrForEachEntry( Rwt_ManReadLeaves(pManRwt), pObj, i )
+ printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) );
+ printf( ") Gain = %d.\n", nGain );
+ }
+ if ( nGain > 0 )
+ { // print stats on the MFFC
+ extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode );
+ printf( "Node %6d : Gain = %4d ", pNode->Id, nGain );
+ Ivy_NodeMffsConeSuppPrint( pNode );
+ }
+*/
+ // complement the FF if needed
+clk = clock();
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+ Ivy_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+ if ( fCompl ) Dec_GraphComplement( pGraph );
+Rwt_ManAddTimeUpdate( pManRwt, clock() - clk );
+ }
+ }
+Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
+ // print stats
+ if ( fVerbose )
+ Rwt_ManPrintStats( pManRwt );
+ // delete the managers
+ Rwt_ManStop( pManRwt );
+ // fix the levels
+ if ( fUpdateLevel )
+ Vec_IntFree( p->vRequired ), p->vRequired = NULL;
+ // check
+ if ( i = Ivy_ManCleanup(p) )
+ printf( "Cleanup after rewriting removed %d dangling nodes.\n", i );
+ if ( !Ivy_ManCheck(p) )
+ printf( "Ivy_ManRewritePre(): The check has failed.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs rewriting for one node.]
+
+ Description [This procedure considers all the cuts computed for the node
+ and tries to rewrite each of them using the "forest" of different AIG
+ structures precomputed and stored in the RWR manager.
+ Determines the best rewriting and computes the gain in the number of AIG
+ nodes in the final network. In the end, p->vFanins contains information
+ about the best cut that can be used for rewriting, while p->pGraph gives
+ the decomposition dag (represented using decomposition graph data structure).
+ Returns gain in the number of nodes or -1 if node cannot be rewritten.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwt_NodeRewrite( Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost )
+{
+ int fVeryVerbose = 0;
+ Dec_Graph_t * pGraph;
+ Ivy_Store_t * pStore;
+ Ivy_Cut_t * pCut;
+ Ivy_Obj_t * pFanin;
+ unsigned uPhase, uTruthBest, uTruth;
+ char * pPerm;
+ int Required, nNodesSaved, nNodesSaveCur;
+ int i, c, GainCur, GainBest = -1;
+ int clk, clk2;
+
+ p->nNodesConsidered++;
+ // get the required times
+ Required = fUpdateLevel? Vec_IntEntry( Ivy_ObjMan(pNode)->vRequired, pNode->Id ) : 1000000;
+ // get the node's cuts
+clk = clock();
+ pStore = Ivy_NodeFindCutsAll( pNode, 5 );
+p->timeCut += clock() - clk;
+
+ // go through the cuts
+clk = clock();
+ for ( c = 1; c < pStore->nCuts; c++ )
+ {
+ pCut = pStore->pCuts + c;
+ // consider only 4-input cuts
+ if ( pCut->nSize != 4 )
+ continue;
+ // skip the cuts with buffers
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ if ( Ivy_ObjIsBuf( Ivy_ObjObj(pNode, pCut->pArray[i]) ) )
+ break;
+ if ( i != pCut->nSize )
+ continue;
+
+// if ( pNode->Id == 82 )
+// Ivy_NodePrintCut( pCut );
+
+ // get the fanin permutation
+clk2 = clock();
+ uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table
+p->timeTruth += clock() - clk2;
+ pPerm = p->pPerms4[ p->pPerms[uTruth] ];
+ uPhase = p->pPhases[uTruth];
+ // collect fanins with the corresponding permutation/phase
+ Vec_PtrClear( p->vFaninsCur );
+ Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 );
+ for ( i = 0; i < (int)pCut->nSize; i++ )
+ {
+ pFanin = Ivy_ObjObj( pNode, pCut->pArray[pPerm[i]] );
+ assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) );
+ pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) );
+ Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin );
+ }
+clk2 = clock();
+/*
+ printf( "Considering: (" );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pFanin)) );
+ printf( ")\n" );
+*/
+ // mark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsInc( Ivy_Regular(pFanin) );
+ // label MFFC with current ID
+ Ivy_ManIncrementTravId( Ivy_ObjMan(pNode) );
+ nNodesSaved = Ivy_NodeMffcLabel( pNode );
+ // unmark the fanin boundary
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
+p->timeMffc += clock() - clk2;
+
+ // evaluate the cut
+clk2 = clock();
+ pGraph = Rwt_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth );
+p->timeEval += clock() - clk2;
+
+ // check if the cut is better than the current best one
+ if ( pGraph != NULL && GainBest < GainCur )
+ {
+ // save this form
+ nNodesSaveCur = nNodesSaved;
+ GainBest = GainCur;
+ p->pGraph = pGraph;
+ p->fCompl = ((uPhase & (1<<4)) > 0);
+ uTruthBest = uTruth;
+ // collect fanins in the
+ Vec_PtrClear( p->vFanins );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ Vec_PtrPush( p->vFanins, pFanin );
+ }
+ }
+p->timeRes += clock() - clk;
+
+ if ( GainBest == -1 )
+ return -1;
+
+// printf( "%d", nNodesSaveCur - GainBest );
+/*
+ if ( GainBest > 0 )
+ {
+ if ( Rwt_CutIsintean( pNode, p->vFanins ) )
+ printf( "b" );
+ else
+ {
+ printf( "Node %d : ", pNode->Id );
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ printf( "%d ", Ivy_Regular(pFanin)->Id );
+ printf( "a" );
+ }
+ }
+*/
+/*
+ if ( GainBest > 0 )
+ if ( p->fCompl )
+ printf( "c" );
+ else
+ printf( "." );
+*/
+
+ // copy the leaves
+ Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+ Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
+
+ p->nScores[p->pMap[uTruthBest]]++;
+ p->nNodesGained += GainBest;
+ if ( fUseZeroCost || GainBest > 0 )
+ p->nNodesRewritten++;
+
+ // report the progress
+ if ( fVeryVerbose && GainBest > 0 )
+ {
+ printf( "Node %6d : ", Ivy_ObjId(pNode) );
+ printf( "Fanins = %d. ", p->vFanins->nSize );
+ printf( "Save = %d. ", nNodesSaveCur );
+ printf( "Add = %d. ", nNodesSaveCur-GainBest );
+ printf( "GAIN = %d. ", GainBest );
+ printf( "Cone = %d. ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 );
+ printf( "Class = %d. ", p->pMap[uTruthBest] );
+ printf( "\n" );
+ }
+ return GainBest;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [References/references the node and returns MFFC size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeRefDeref( Ivy_Obj_t * pNode, int fReference, int fLabel )
+{
+ Ivy_Obj_t * pNode0, * pNode1;
+ int Counter;
+ // label visited nodes
+ if ( fLabel )
+ Ivy_ObjSetTravIdCurrent( pNode );
+ // skip the CI
+ if ( Ivy_ObjIsCi(pNode) )
+ return 0;
+ assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) );
+ // process the internal node
+ pNode0 = Ivy_ObjFanin0(pNode);
+ pNode1 = Ivy_ObjFanin1(pNode);
+ Counter = Ivy_ObjIsNode(pNode);
+ if ( fReference )
+ {
+ if ( pNode0->nRefs++ == 0 )
+ Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
+ if ( Ivy_ObjIsNode(pNode) && pNode1->nRefs++ == 0 )
+ Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+ }
+ else
+ {
+ assert( pNode0->nRefs > 0 );
+ assert( pNode1->nRefs > 0 );
+ if ( --pNode0->nRefs == 0 )
+ Counter += Ivy_NodeRefDeref( pNode0, fReference, fLabel );
+ if ( Ivy_ObjIsNode(pNode) && --pNode1->nRefs == 0 )
+ Counter += Ivy_NodeRefDeref( pNode1, fReference, fLabel );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the size of MFFC and labels nodes with the current TravId.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_NodeMffcLabel( Ivy_Obj_t * pNode )
+{
+ int nConeSize1, nConeSize2;
+ assert( !Ivy_IsComplement( pNode ) );
+ assert( Ivy_ObjIsNode( pNode ) );
+ nConeSize1 = Ivy_NodeRefDeref( pNode, 0, 1 ); // dereference
+ nConeSize2 = Ivy_NodeRefDeref( pNode, 1, 0 ); // reference
+ assert( nConeSize1 == nConeSize2 );
+ assert( nConeSize1 > 0 );
+ return nConeSize1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth_rec( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+ static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ unsigned uTruth0, uTruth1;
+ int i;
+ for ( i = 0; i < nNums; i++ )
+ if ( pObj->Id == pNums[i] )
+ return uMasks[i];
+ assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+ uTruth0 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin0(pObj), pNums, nNums );
+ if ( Ivy_ObjFaninC0(pObj) )
+ uTruth0 = ~uTruth0;
+ if ( Ivy_ObjIsBuf(pObj) )
+ return uTruth0;
+ uTruth1 = Ivy_NodeGetTruth_rec( Ivy_ObjFanin1(pObj), pNums, nNums );
+ if ( Ivy_ObjFaninC1(pObj) )
+ uTruth1 = ~uTruth1;
+ return uTruth0 & uTruth1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums )
+{
+ assert( nNums < 6 );
+ return Ivy_NodeGetTruth_rec( pObj, pNums, nNums );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Evaluates the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dec_Graph_t * Rwt_CutEvaluate( Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth )
+{
+ Vec_Ptr_t * vSubgraphs;
+ Dec_Graph_t * pGraphBest, * pGraphCur;
+ Rwt_Node_t * pNode, * pFanin;
+ int nNodesAdded, GainBest, i, k;
+ // find the matching class of subgraphs
+ vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] );
+ p->nSubgraphs += vSubgraphs->nSize;
+ // determine the best subgraph
+ GainBest = -1;
+ Vec_PtrForEachEntry( vSubgraphs, pNode, i )
+ {
+ // get the current graph
+ pGraphCur = (Dec_Graph_t *)pNode->pNext;
+ // copy the leaves
+ Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+ Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
+ // detect how many unlabeled nodes will be reused
+ nNodesAdded = Ivy_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax );
+ if ( nNodesAdded == -1 )
+ continue;
+ assert( nNodesSaved >= nNodesAdded );
+ // count the gain at this node
+ if ( GainBest < nNodesSaved - nNodesAdded )
+ {
+ GainBest = nNodesSaved - nNodesAdded;
+ pGraphBest = pGraphCur;
+ }
+ }
+ if ( GainBest == -1 )
+ return NULL;
+ *pGainBest = GainBest;
+ return pGraphBest;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of new nodes added when using this graph.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.
+ Returns -1 if the number of nodes and levels exceeded the given limit or
+ the number of levels exceeded the maximum allowed level.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_GraphToNetworkCount( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+ Dec_Node_t * pNode, * pNode0, * pNode1;
+ Ivy_Obj_t * pAnd, * pAnd0, * pAnd1;
+ int i, Counter, LevelNew, LevelOld;
+ // check for constant function or a literal
+ if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) )
+ return 0;
+ // set the levels of the leaves
+ Dec_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->Level = Ivy_Regular(pNode->pFunc)->Level;
+ // compute the AIG size after adding the internal nodes
+ Counter = 0;
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+ pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl );
+ pAnd = Ivy_TableLookup( Ivy_ObjCreateGhost(pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) );
+ // return -1 if the node is the same as the original root
+ if ( Ivy_Regular(pAnd) == pRoot )
+ return -1;
+ }
+ else
+ pAnd = NULL;
+ // count the number of added nodes
+ if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(Ivy_Regular(pAnd)) )
+ {
+ if ( ++Counter > NodeMax )
+ return -1;
+ }
+ // count the number of new levels
+ LevelNew = 1 + RWT_MAX( pNode0->Level, pNode1->Level );
+ if ( pAnd )
+ {
+ if ( Ivy_Regular(pAnd) == Ivy_ObjConst1(pRoot) )
+ LevelNew = 0;
+ else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd0) )
+ LevelNew = (int)Ivy_Regular(pAnd0)->Level;
+ else if ( Ivy_Regular(pAnd) == Ivy_Regular(pAnd1) )
+ LevelNew = (int)Ivy_Regular(pAnd1)->Level;
+ LevelOld = (int)Ivy_Regular(pAnd)->Level;
+// assert( LevelNew == LevelOld );
+ }
+ if ( LevelNew > LevelMax )
+ return -1;
+ pNode->pFunc = pAnd;
+ pNode->Level = LevelNew;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_GraphToNetwork( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Ivy_Obj_t * pAnd0, * pAnd1;
+ Dec_Node_t * pNode;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Replaces MFFC of the node by the new factored form.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_GraphUpdateNetwork( Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
+{
+ Ivy_Obj_t * pRootNew;
+ int nNodesNew, nNodesOld;
+ nNodesOld = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+ // create the new structure of nodes
+ pRootNew = Ivy_GraphToNetwork( Ivy_ObjMan(pRoot), pGraph );
+ // remove the old nodes
+// Ivy_AigReplace( pMan->pManFunc, pRoot, pRootNew, fUpdateLevel );
+ Ivy_ObjReplace( pRoot, pRootNew, 1, 0 );
+ // compare the gains
+ nNodesNew = Ivy_ManNodeNum(Ivy_ObjMan(pRoot));
+ assert( nGain <= nNodesOld - nNodesNew );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 590affd7..3d1ac335 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -362,6 +362,222 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
return vLatches;
}
+/**Function*************************************************************
+
+ Synopsis [Collect the latches.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ManReadLevels( Ivy_Man_t * p )
+{
+ Ivy_Obj_t * pObj;
+ int i, LevelMax = 0;
+ Ivy_ManForEachPo( p, pObj, i )
+ {
+ pObj = Ivy_ObjFanin0(pObj);
+ LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
+ }
+ return LevelMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the real fanin.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
+{
+ Ivy_Obj_t * pFanin;
+ if ( !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
+ return pObj;
+ pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
+ return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the cube has exactly one 1.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_TruthHasOneOne( unsigned uCube )
+{
+ return (uCube & (uCube - 1)) == 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if two cubes are distance-1.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
+{
+ unsigned uTemp = uCube1 | uCube2;
+ return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if two cubes differ in only one literal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
+{
+ unsigned uTemp = uCube1 ^ uCube2;
+ return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Combines two distance 1 cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 )
+{
+ unsigned uTemp;
+ uTemp = uCube1 | uCube2;
+ uTemp &= (uTemp >> 1) & 0x55555555;
+ assert( Ivy_TruthHasOneOne(uTemp) );
+ uTemp |= (uTemp << 1);
+ return (uCube1 | uCube2) ^ uTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Estimates the number of AIG nodes in the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
+{
+ static unsigned short uResult[256];
+ static unsigned short uCover[81*81];
+ static char pVarCount[81*81];
+ int nMints, uCube, uCubeNew, i, k, c, nCubes, nRes, Counter;
+ assert( nVars <= 8 );
+ // create the cover
+ nCubes = 0;
+ nMints = (1 << nVars);
+ for ( i = 0; i < nMints; i++ )
+ if ( pTruth[i/32] & (1 << (i & 31)) )
+ {
+ uCube = 0;
+ for ( k = 0; k < nVars; k++ )
+ if ( i & (1 << k) )
+ uCube |= (1 << ((k<<1)+1));
+ else
+ uCube |= (1 << ((k<<1)+0));
+ uCover[nCubes] = uCube;
+ pVarCount[nCubes] = nVars;
+ nCubes++;
+// Extra_PrintBinary( stdout, &uCube, 8 ); printf( "\n" );
+ }
+ assert( nCubes <= 256 );
+ // reduce the cover by building larger cubes
+ for ( i = 1; i < nCubes; i++ )
+ for ( k = 0; k < i; k++ )
+ if ( pVarCount[i] && pVarCount[i] == pVarCount[k] && Ivy_TruthCubesDist1(uCover[i], uCover[k]) )
+ {
+ uCubeNew = Ivy_TruthCubesMerge(uCover[i], uCover[k]);
+ for ( c = i; c < nCubes; c++ )
+ if ( uCubeNew == uCover[c] )
+ break;
+ if ( c != nCubes )
+ continue;
+ uCover[nCubes] = uCubeNew;
+ pVarCount[nCubes] = pVarCount[i] - 1;
+ nCubes++;
+ assert( nCubes < 81*81 );
+// Extra_PrintBinary( stdout, &uCubeNew, 8 ); printf( "\n" );
+// c = c;
+ }
+ // compact the cover
+ nRes = 0;
+ for ( i = nCubes -1; i >= 0; i-- )
+ {
+ for ( k = 0; k < nRes; k++ )
+ if ( (uCover[i] & uResult[k]) == uResult[k] )
+ break;
+ if ( k != nRes )
+ continue;
+ uResult[nRes++] = uCover[i];
+ }
+ // count the number of literals
+ Counter = 0;
+ for ( i = 0; i < nRes; i++ )
+ {
+ for ( k = 0; k < nVars; k++ )
+ if ( uResult[i] & (3 << (k<<1)) )
+ Counter++;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tests the cover procedure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_TruthEstimateNodesTest()
+{
+ unsigned uTruth[8];
+ int i;
+ for ( i = 0; i < 8; i++ )
+ uTruth[i] = ~(unsigned)0;
+ uTruth[3] ^= (1 << 13);
+// uTruth[4] = 0xFFFFF;
+// uTruth[0] = 0xFF;
+// uTruth[0] ^= (1 << 3);
+ printf( "Number = %d.\n", Ivy_TruthEstimateNodes(uTruth, 8) );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make
index beadb8b9..f697910b 100644
--- a/src/temp/ivy/module.make
+++ b/src/temp/ivy/module.make
@@ -8,7 +8,8 @@ SRC += src/temp/ivy/ivyBalance.c \
src/temp/ivy/ivyMulti.c \
src/temp/ivy/ivyObj.c \
src/temp/ivy/ivyOper.c \
- src/temp/ivy/ivyRewrite.c \
+ src/temp/ivy/ivyResyn.c \
+ src/temp/ivy/ivyRwrPre.c \
src/temp/ivy/ivySeq.c \
src/temp/ivy/ivyTable.c \
src/temp/ivy/ivyUndo.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 11:24:51 +0000