diff options
Diffstat (limited to 'src/aig/dar/darBalance.c')
-rw-r--r-- | src/aig/dar/darBalance.c | 129 |
1 files changed, 65 insertions, 64 deletions
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 2d9a48d4..a1502382 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -18,17 +18,18 @@ ***********************************************************************/ -#include "dar.h" +#include "darInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Dar_Obj_t * Dar_NodeBalance_rec( Dar_Man_t * pNew, Dar_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); -static Vec_Ptr_t * Dar_NodeBalanceCone( Dar_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); -static int Dar_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ); -static void Dar_NodeBalancePermute( Dar_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ); -static void Dar_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Dar_Obj_t * pObj ); +static Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel ); +static Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ); +static int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper ); +static void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ); +static void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj ); +static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -45,33 +46,33 @@ static void Dar_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Da SeeAlso [] ***********************************************************************/ -Dar_Man_t * Dar_ManBalance( Dar_Man_t * p, int fUpdateLevel ) +Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) { - Dar_Man_t * pNew; - Dar_Obj_t * pObj, * pObjNew; + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; Vec_Vec_t * vStore; int i; // create the new manager - pNew = Dar_ManStart(); + pNew = Aig_ManStart(); // map the PI nodes - Dar_ManCleanData( p ); - Dar_ManConst1(p)->pData = Dar_ManConst1(pNew); - Dar_ManForEachPi( p, pObj, i ) - pObj->pData = Dar_ObjCreatePi(pNew); + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi(pNew); // balance the AIG vStore = Vec_VecAlloc( 50 ); - Dar_ManForEachPo( p, pObj, i ) + Aig_ManForEachPo( p, pObj, i ) { - pObjNew = Dar_NodeBalance_rec( pNew, Dar_ObjFanin0(pObj), vStore, 0, fUpdateLevel ); - Dar_ObjCreatePo( pNew, Dar_NotCond( pObjNew, Dar_ObjFaninC0(pObj) ) ); + pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel ); + Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) ); } Vec_VecFree( vStore ); // remove dangling nodes -// Dar_ManCreateRefs( pNew ); -// if ( i = Dar_ManCleanup( pNew ) ) +// Aig_ManCreateRefs( pNew ); +// if ( i = Aig_ManCleanup( pNew ) ) // printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); // check the resulting AIG - if ( !Dar_ManCheck(pNew) ) + if ( !Aig_ManCheck(pNew) ) printf( "Dar_ManBalance(): The check has failed.\n" ); return pNew; } @@ -87,33 +88,33 @@ Dar_Man_t * Dar_ManBalance( Dar_Man_t * p, int fUpdateLevel ) SeeAlso [] ***********************************************************************/ -Dar_Obj_t * Dar_NodeBalance_rec( Dar_Man_t * pNew, Dar_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) +Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t * vStore, int Level, int fUpdateLevel ) { - Dar_Obj_t * pObjNew; + Aig_Obj_t * pObjNew; Vec_Ptr_t * vSuper; int i; - assert( !Dar_IsComplement(pObjOld) ); + assert( !Aig_IsComplement(pObjOld) ); // return if the result is known if ( pObjOld->pData ) return pObjOld->pData; - assert( Dar_ObjIsNode(pObjOld) ); + assert( Aig_ObjIsNode(pObjOld) ); // get the implication supergate - vSuper = Dar_NodeBalanceCone( pObjOld, vStore, Level ); + vSuper = Dar_BalanceCone( pObjOld, vStore, Level ); // check if supergate contains two nodes in the opposite polarity if ( vSuper->nSize == 0 ) - return pObjOld->pData = Dar_ManConst0(pNew); + return pObjOld->pData = Aig_ManConst0(pNew); if ( Vec_PtrSize(vSuper) < 2 ) printf( "BUG!\n" ); // for each old node, derive the new well-balanced node for ( i = 0; i < Vec_PtrSize(vSuper); i++ ) { - pObjNew = Dar_NodeBalance_rec( pNew, Dar_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); - vSuper->pArray[i] = Dar_NotCond( pObjNew, Dar_IsComplement(vSuper->pArray[i]) ); + pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel ); + vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) ); } // build the supergate - pObjNew = Dar_NodeBalanceBuildSuper( pNew, vSuper, Dar_ObjType(pObjOld), fUpdateLevel ); + pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel ); // make sure the balanced node is not assigned -// assert( pObjOld->Level >= Dar_Regular(pObjNew)->Level ); +// assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level ); assert( pObjOld->pData == NULL ); return pObjOld->pData = pObjNew; } @@ -129,11 +130,11 @@ Dar_Obj_t * Dar_NodeBalance_rec( Dar_Man_t * pNew, Dar_Obj_t * pObjOld, Vec_Vec_ SeeAlso [] ***********************************************************************/ -int Dar_NodeBalanceCone_rec( Dar_Obj_t * pRoot, Dar_Obj_t * pObj, Vec_Ptr_t * vSuper ) +int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) { int RetValue1, RetValue2, i; // check if the node is visited - if ( Dar_Regular(pObj)->fMarkB ) + if ( Aig_Regular(pObj)->fMarkB ) { // check if the node occurs in the same polarity for ( i = 0; i < vSuper->nSize; i++ ) @@ -141,23 +142,23 @@ int Dar_NodeBalanceCone_rec( Dar_Obj_t * pRoot, Dar_Obj_t * pObj, Vec_Ptr_t * vS return 1; // check if the node is present in the opposite polarity for ( i = 0; i < vSuper->nSize; i++ ) - if ( vSuper->pArray[i] == Dar_Not(pObj) ) + if ( vSuper->pArray[i] == Aig_Not(pObj) ) return -1; assert( 0 ); return 0; } // if the new node is complemented or a PI, another gate begins - if ( pObj != pRoot && (Dar_IsComplement(pObj) || Dar_ObjType(pObj) != Dar_ObjType(pRoot) || Dar_ObjRefs(pObj) > 1) ) + if ( pObj != pRoot && (Aig_IsComplement(pObj) || Aig_ObjType(pObj) != Aig_ObjType(pRoot) || Aig_ObjRefs(pObj) > 1) ) { Vec_PtrPush( vSuper, pObj ); - Dar_Regular(pObj)->fMarkB = 1; + Aig_Regular(pObj)->fMarkB = 1; return 0; } - assert( !Dar_IsComplement(pObj) ); - assert( Dar_ObjIsNode(pObj) ); + assert( !Aig_IsComplement(pObj) ); + assert( Aig_ObjIsNode(pObj) ); // go through the branches - RetValue1 = Dar_NodeBalanceCone_rec( pRoot, Dar_ObjChild0(pObj), vSuper ); - RetValue2 = Dar_NodeBalanceCone_rec( pRoot, Dar_ObjChild1(pObj), vSuper ); + RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper ); + RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper ); if ( RetValue1 == -1 || RetValue2 == -1 ) return -1; // return 1 if at least one branch has a duplicate @@ -175,11 +176,11 @@ int Dar_NodeBalanceCone_rec( Dar_Obj_t * pRoot, Dar_Obj_t * pObj, Vec_Ptr_t * vS SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Dar_NodeBalanceCone( Dar_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) +Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level ) { Vec_Ptr_t * vNodes; int RetValue, i; - assert( !Dar_IsComplement(pObj) ); + assert( !Aig_IsComplement(pObj) ); // extend the storage if ( Vec_VecSize( vStore ) <= Level ) Vec_VecPush( vStore, Level, 0 ); @@ -187,11 +188,11 @@ Vec_Ptr_t * Dar_NodeBalanceCone( Dar_Obj_t * pObj, Vec_Vec_t * vStore, int Level vNodes = Vec_VecEntry( vStore, Level ); Vec_PtrClear( vNodes ); // collect the nodes in the implication supergate - RetValue = Dar_NodeBalanceCone_rec( pObj, pObj, vNodes ); + RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes ); assert( vNodes->nSize > 1 ); // unmark the visited nodes Vec_PtrForEachEntry( vNodes, pObj, i ) - Dar_Regular(pObj)->fMarkB = 0; + Aig_Regular(pObj)->fMarkB = 0; // if we found the node and its complement in the same implication supergate, // return empty set of nodes (meaning that we should use constant-0 node) if ( RetValue == -1 ) @@ -210,9 +211,9 @@ Vec_Ptr_t * Dar_NodeBalanceCone( Dar_Obj_t * pObj, Vec_Vec_t * vStore, int Level SeeAlso [] ***********************************************************************/ -int Dar_NodeCompareLevelsDecrease( Dar_Obj_t ** pp1, Dar_Obj_t ** pp2 ) +int Aig_NodeCompareLevelsDecrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) { - int Diff = Dar_ObjLevel(Dar_Regular(*pp1)) - Dar_ObjLevel(Dar_Regular(*pp2)); + int Diff = Aig_ObjLevel(Aig_Regular(*pp1)) - Aig_ObjLevel(Aig_Regular(*pp2)); if ( Diff > 0 ) return -1; if ( Diff < 0 ) @@ -231,24 +232,24 @@ int Dar_NodeCompareLevelsDecrease( Dar_Obj_t ** pp1, Dar_Obj_t ** pp2 ) SeeAlso [] ***********************************************************************/ -Dar_Obj_t * Dar_NodeBalanceBuildSuper( Dar_Man_t * p, Vec_Ptr_t * vSuper, Dar_Type_t Type, int fUpdateLevel ) +Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t Type, int fUpdateLevel ) { - Dar_Obj_t * pObj1, * pObj2; + Aig_Obj_t * pObj1, * pObj2; int LeftBound; assert( vSuper->nSize > 1 ); // sort the new nodes by level in the decreasing order - Vec_PtrSort( vSuper, Dar_NodeCompareLevelsDecrease ); + Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease ); // balance the nodes while ( vSuper->nSize > 1 ) { // find the left bound on the node to be paired - LeftBound = (!fUpdateLevel)? 0 : Dar_NodeBalanceFindLeft( vSuper ); + LeftBound = (!fUpdateLevel)? 0 : Dar_BalanceFindLeft( vSuper ); // find the node that can be shared (if no such node, randomize choice) - Dar_NodeBalancePermute( p, vSuper, LeftBound, Type == DAR_AIG_EXOR ); + Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR ); // pull out the last two nodes pObj1 = Vec_PtrPop(vSuper); pObj2 = Vec_PtrPop(vSuper); - Dar_NodeBalancePushUniqueOrderByLevel( vSuper, Dar_Oper(p, pObj1, pObj2, Type) ); + Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) ); } return Vec_PtrEntry(vSuper, 0); } @@ -268,9 +269,9 @@ Dar_Obj_t * Dar_NodeBalanceBuildSuper( Dar_Man_t * p, Vec_Ptr_t * vSuper, Dar_Ty SeeAlso [] ***********************************************************************/ -int Dar_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) +int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper ) { - Dar_Obj_t * pObjRight, * pObjLeft; + Aig_Obj_t * pObjRight, * pObjLeft; int Current; // if two or less nodes, pair with the first if ( Vec_PtrSize(vSuper) < 3 ) @@ -284,13 +285,13 @@ int Dar_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) // get the next node on the left pObjLeft = Vec_PtrEntry( vSuper, Current ); // if the level of this node is different, quit the loop - if ( Dar_ObjLevel(Dar_Regular(pObjLeft)) != Dar_ObjLevel(Dar_Regular(pObjRight)) ) + if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) ) break; } Current++; // get the node, for which the equality holds pObjLeft = Vec_PtrEntry( vSuper, Current ); - assert( Dar_ObjLevel(Dar_Regular(pObjLeft)) == Dar_ObjLevel(Dar_Regular(pObjRight)) ); + assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) ); return Current; } @@ -306,9 +307,9 @@ int Dar_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -void Dar_NodeBalancePermute( Dar_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) +void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor ) { - Dar_Obj_t * pObj1, * pObj2, * pObj3, * pGhost; + Aig_Obj_t * pObj1, * pObj2, * pObj3, * pGhost; int RightBound, i; // get the right bound RightBound = Vec_PtrSize(vSuper) - 2; @@ -318,20 +319,20 @@ void Dar_NodeBalancePermute( Dar_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, i // get the two last nodes pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 ); pObj2 = Vec_PtrEntry( vSuper, RightBound ); - if ( Dar_Regular(pObj1) == p->pConst1 || Dar_Regular(pObj2) == p->pConst1 ) + if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 ) return; // find the first node that can be shared for ( i = RightBound; i >= LeftBound; i-- ) { pObj3 = Vec_PtrEntry( vSuper, i ); - if ( Dar_Regular(pObj3) == p->pConst1 ) + if ( Aig_Regular(pObj3) == p->pConst1 ) { Vec_PtrWriteEntry( vSuper, i, pObj2 ); Vec_PtrWriteEntry( vSuper, RightBound, pObj3 ); return; } - pGhost = Dar_ObjCreateGhost( p, pObj1, pObj3, fExor? DAR_AIG_EXOR : DAR_AIG_AND ); - if ( Dar_TableLookup( p, pGhost ) ) + pGhost = Aig_ObjCreateGhost( p, pObj1, pObj3, fExor? AIG_OBJ_EXOR : AIG_OBJ_AND ); + if ( Aig_TableLookup( p, pGhost ) ) { if ( pObj3 == pObj2 ) return; @@ -364,9 +365,9 @@ void Dar_NodeBalancePermute( Dar_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, i SeeAlso [] ***********************************************************************/ -void Dar_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Dar_Obj_t * pObj ) +void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj ) { - Dar_Obj_t * pObj1, * pObj2; + Aig_Obj_t * pObj1, * pObj2; int i; if ( Vec_PtrPushUnique(vStore, pObj) ) return; @@ -375,7 +376,7 @@ void Dar_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Dar_Obj_t * pObj { pObj1 = vStore->pArray[i ]; pObj2 = vStore->pArray[i-1]; - if ( Dar_ObjLevel(Dar_Regular(pObj1)) <= Dar_ObjLevel(Dar_Regular(pObj2)) ) + if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) ) break; vStore->pArray[i ] = pObj2; vStore->pArray[i-1] = pObj1; |