summaryrefslogtreecommitdiffstats
path: root/src/aig/dar/darBalance.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/dar/darBalance.c')
-rw-r--r--src/aig/dar/darBalance.c129
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 11:26:14 +0000