summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h16
-rw-r--r--src/aig/aig/aigDfs.c184
-rw-r--r--src/aig/aig/aigDup.c489
-rw-r--r--src/aig/aig/aigHaig.c2
-rw-r--r--src/aig/aig/aigMan.c375
-rw-r--r--src/aig/aig/aigPart.c114
-rw-r--r--src/aig/aig/aigRetF.c2
-rw-r--r--src/aig/aig/aigUtil.c12
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/dar/darMan.c1
-rw-r--r--src/aig/dar/darScript.c36
-rw-r--r--src/aig/fra/fraCec.c2
-rw-r--r--src/aig/fra/fraCore.c2
-rw-r--r--src/aig/fra/fraInd.c4
-rw-r--r--src/aig/fra/fraLcr.c31
-rw-r--r--src/aig/fra/fraMan.c1
-rw-r--r--src/aig/fra/fraSec.c10
-rw-r--r--src/aig/ivy/ivyMan.c1
-rw-r--r--src/aig/ntl/ntlCore.c6
-rw-r--r--src/aig/nwk/nwkDfs.c4
-rw-r--r--src/aig/nwk/nwkMap.c8
-rw-r--r--src/aig/nwk/nwkStrash.c2
-rw-r--r--src/base/abci/abc.c61
-rw-r--r--src/base/abci/abcDar.c10
-rw-r--r--src/base/abci/abcPrint.c1
-rw-r--r--src/misc/hash/hashInt.h9
-rw-r--r--src/sat/fraig/fraigMan.c1
27 files changed, 778 insertions, 607 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 38fd5190..18061a9c 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -445,14 +445,13 @@ extern Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLea
extern void Aig_ManCutStop( Aig_ManCut_t * p );
/*=== aigDfs.c ==========================================================*/
extern int Aig_ManVerifyTopoOrder( Aig_Man_t * p );
-extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p );
+extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly );
extern Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p );
-extern Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p );
extern int Aig_ManLevelNum( Aig_Man_t * p );
-extern int Aig_ManCountLevels( Aig_Man_t * p );
+extern int Aig_ManChoiceLevel( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
@@ -460,6 +459,13 @@ extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_O
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
extern void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
extern int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
+/*=== aigDup.c ==========================================================*/
+extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder );
+extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p );
+extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
@@ -472,10 +478,6 @@ extern void Aig_ManHaigRecord( Aig_Man_t * p );
/*=== aigMan.c ==========================================================*/
extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
-extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p );
-extern Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
-extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered );
-extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 95ed1c3a..9e43d7fd 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -43,7 +43,7 @@
int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pNext;
- int i, iBox, iTerm1, nTerms;
+ int i, k, iBox, iTerm1, nTerms;
Aig_ManSetPioNumbers( p );
Aig_ManIncrementTravId( p );
Aig_ManForEachObj( p, pObj, i )
@@ -63,7 +63,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
return 0;
}
}
- else if ( Aig_ObjIsPo(pObj) )
+ else if ( Aig_ObjIsPo(pObj) || Aig_ObjIsBuf(pObj) )
{
pNext = Aig_ObjFanin0(pObj);
if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
@@ -81,9 +81,9 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
{
iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
- for ( i = 0; i < nTerms; i++ )
+ for ( k = 0; k < nTerms; k++ )
{
- pNext = Aig_ManPo( p, iTerm1 + i );
+ pNext = Aig_ManPo( p, iTerm1 + k );
assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox );
if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
{
@@ -94,7 +94,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
}
}
}
- else
+ else if ( !Aig_ObjIsConst1(pObj) )
assert( 0 );
Aig_ObjSetTravIdCurrent( p, pObj );
}
@@ -120,49 +120,53 @@ void Aig_ManDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
assert( !Aig_IsComplement(pObj) );
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
-// if ( Aig_ObjIsPi(pObj) )
-// return;
-// assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
Aig_ObjSetTravIdCurrent(p, pObj);
+ if ( p->pEquivs && p->pEquivs[pObj->Id] )
+ Aig_ManDfs_rec( p, p->pEquivs[pObj->Id], vNodes );
Aig_ManDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
Aig_ManDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-// assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
-// Aig_ObjSetTravIdCurrent(p, pObj);
Vec_PtrPush( vNodes, pObj );
}
/**Function*************************************************************
- Synopsis [Collects internal nodes in the DFS order.]
+ Synopsis [Collects objects of the AIG in the DFS order.]
- Description []
+ Description [Works with choice nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p )
+Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p, int fNodesOnly )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
Aig_ManIncrementTravId( p );
- // mark constant and PIs
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
- Aig_ManForEachPi( p, pObj, i )
- Aig_ObjSetTravIdCurrent( p, pObj );
- // go through the nodes
- vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
- Aig_ManForEachObj( p, pObj, i )
- if ( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) )
- Aig_ManDfs_rec( p, pObj, vNodes );
+ // start the array of nodes
+ vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+ // mark PIs if they should not be collected
+ if ( fNodesOnly )
+ Aig_ManForEachPi( p, pObj, i )
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ else
+ Vec_PtrPush( vNodes, Aig_ManConst1(p) );
+ // collect nodes reachable in the DFS order
+ Aig_ManForEachPo( p, pObj, i )
+ Aig_ManDfs_rec( p, fNodesOnly? Aig_ObjFanin0(pObj): pObj, vNodes );
+ if ( fNodesOnly )
+ assert( Vec_PtrSize(vNodes) == Aig_ManNodeNum(p) );
+ else
+ assert( Vec_PtrSize(vNodes) == Aig_ManObjNum(p) );
return vNodes;
}
/**Function*************************************************************
- Synopsis [Levelizes the nodes
+ Synopsis [Levelizes the nodes.]
Description []
@@ -178,7 +182,7 @@ Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
int nLevels, i;
nLevels = Aig_ManLevelNum( p );
vLevels = Vec_VecStart( nLevels + 1 );
- Aig_ManForEachNode( p, pObj, i )
+ Aig_ManForEachObj( p, pObj, i )
{
assert( (int)pObj->Level <= nLevels );
Vec_VecPush( vLevels, pObj->Level, pObj );
@@ -188,29 +192,6 @@ Vec_Vec_t * Aig_ManLevelize( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Collects internal nodes in the DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Ptr_t * Aig_ManDfsPio( Aig_Man_t * p )
-{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj;
- int i;
- Aig_ManIncrementTravId( p );
- vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
- Aig_ManForEachPo( p, pObj, i )
- Aig_ManDfs_rec( p, pObj, vNodes );
- return vNodes;
-}
-
-/**Function*************************************************************
-
Synopsis [Collects internal nodes and PIs in the DFS order.]
Description []
@@ -368,9 +349,11 @@ int Aig_ManLevelNum( Aig_Man_t * p )
return LevelsMax;
}
+//#if 0
+
/**Function*************************************************************
- Synopsis [Computes the max number of levels in the manager.]
+ Synopsis [Computes levels for AIG with choices and white boxes.]
Description []
@@ -379,31 +362,100 @@ int Aig_ManLevelNum( Aig_Man_t * p )
SeeAlso []
***********************************************************************/
-int Aig_ManCountLevels( Aig_Man_t * p )
+void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
{
- Vec_Ptr_t * vNodes;
- Aig_Obj_t * pObj;
- int i, LevelsMax, Level0, Level1;
- // initialize the levels
- Aig_ManConst1(p)->iData = 0;
- Aig_ManForEachPi( p, pObj, i )
- pObj->iData = 0;
- // compute levels in a DFS order
- vNodes = Aig_ManDfs( p );
- Vec_PtrForEachEntry( vNodes, pObj, i )
+ Aig_Obj_t * pNext;
+ int i, iBox, iTerm1, nTerms, LevelMax = 0;
+ if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+ return;
+ Aig_ObjSetTravIdCurrent( p, pObj );
+ if ( Aig_ObjIsPi(pObj) )
{
- Level0 = Aig_ObjFanin0(pObj)->iData;
- Level1 = Aig_ObjFanin1(pObj)->iData;
- pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1);
+ if ( p->pManTime )
+ {
+ iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+ if ( iBox >= 0 ) // this is not a true PI
+ {
+ iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
+ nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+ for ( i = 0; i < nTerms; i++ )
+ {
+ pNext = Aig_ManPo(p, iTerm1 + i);
+ Aig_ManChoiceLevel_rec( p, pNext );
+ if ( LevelMax < Aig_ObjLevel(pNext) )
+ LevelMax = Aig_ObjLevel(pNext);
+ }
+ LevelMax++;
+ }
+ }
+// printf( "%d ", pObj->Level );
}
- Vec_PtrFree( vNodes );
- // get levels of the POs
- LevelsMax = 0;
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ pNext = Aig_ObjFanin0(pObj);
+ Aig_ManChoiceLevel_rec( p, pNext );
+ if ( LevelMax < Aig_ObjLevel(pNext) )
+ LevelMax = Aig_ObjLevel(pNext);
+ }
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ // get the maximum level of the two fanins
+ pNext = Aig_ObjFanin0(pObj);
+ Aig_ManChoiceLevel_rec( p, pNext );
+ if ( LevelMax < Aig_ObjLevel(pNext) )
+ LevelMax = Aig_ObjLevel(pNext);
+ pNext = Aig_ObjFanin1(pObj);
+ Aig_ManChoiceLevel_rec( p, pNext );
+ if ( LevelMax < Aig_ObjLevel(pNext) )
+ LevelMax = Aig_ObjLevel(pNext);
+ LevelMax++;
+
+ // get the level of the nodes in the choice node
+ if ( p->pEquivs && (pNext = p->pEquivs[pObj->Id]) )
+ {
+ Aig_ManChoiceLevel_rec( p, pNext );
+ if ( LevelMax < Aig_ObjLevel(pNext) )
+ LevelMax = Aig_ObjLevel(pNext);
+ }
+ }
+ else
+ assert( 0 );
+ Aig_ObjSetLevel( pObj, LevelMax );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes levels for AIG with choices and white boxes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManChoiceLevel( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, LevelMax = 0;
+ Aig_ManForEachObj( p, pObj, i )
+ Aig_ObjSetLevel( pObj, 0 );
+ Aig_ManSetPioNumbers( p );
+ Aig_ManIncrementTravId( p );
Aig_ManForEachPo( p, pObj, i )
- LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData );
- return LevelsMax;
+ {
+ Aig_ManChoiceLevel_rec( p, pObj );
+ if ( LevelMax < Aig_ObjLevel(pObj) )
+ LevelMax = Aig_ObjLevel(pObj);
+ }
+ Aig_ManCleanPioNumbers( p );
+ Aig_ManForEachNode( p, pObj, i )
+ assert( Aig_ObjLevel(pObj) > 0 );
+ return LevelMax;
}
+//#endif
+
/**Function*************************************************************
Synopsis [Counts the number of AIG nodes rooted at this cone.]
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
new file mode 100644
index 00000000..043a95a8
--- /dev/null
+++ b/src/aig/aig/aigDup.c
@@ -0,0 +1,489 @@
+/**CFile****************************************************************
+
+ FileName [aigDup.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [AIG duplication (re-strashing).]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigDup.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "tim.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, nNodes;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // create the PIs
+ Aig_ManCleanData( p );
+ // duplicate internal nodes
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsBuf(pObj) )
+ {
+ pObjNew = Aig_ObjChild0Copy(pObj);
+ }
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ }
+ else if ( Aig_ObjIsPi(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->Level = pObj->Level;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ else if ( Aig_ObjIsConst1(pObj) )
+ {
+ pObjNew = Aig_ManConst1(pNew);
+ }
+ else
+ assert( 0 );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ if ( (nNodes = Aig_ManCleanup( pNew )) )
+ printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ // duplicate the timing manager
+ if ( p->pManTime )
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupOrdered(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager to have EXOR gates.]
+
+ Description [Assumes topological ordering of the nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->fCatchExor = 1;
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // create the PIs
+ Aig_ManCleanData( p );
+ // duplicate internal nodes
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsBuf(pObj) )
+ {
+ pObjNew = Aig_ObjChild0Copy(pObj);
+ }
+ else if ( Aig_ObjIsNode(pObj) )
+ {
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ }
+ else if ( Aig_ObjIsPi(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->Level = pObj->Level;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ else if ( Aig_ObjIsConst1(pObj) )
+ {
+ pObjNew = Aig_ManConst1(pNew);
+ }
+ else
+ assert( 0 );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ Aig_ManCleanup( pNew );
+ // duplicate the timing manager
+ if ( p->pManTime )
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupExor(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager recursively.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pObjNew, * pEquivNew = NULL;
+ if ( pObj->pData )
+ return pObj->pData;
+ if ( p->pEquivs && p->pEquivs[pObj->Id] )
+ pEquivNew = Aig_ManDupDfs_rec( pNew, p, p->pEquivs[pObj->Id] );
+ Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ if ( Aig_ObjIsBuf(pObj) )
+ return pObj->pData = Aig_ObjChild0Copy(pObj);
+ Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ if ( pObj->pHaig )
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ if ( pEquivNew )
+ {
+ if ( pNew->pEquivs )
+ pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pEquivNew);
+ if ( pNew->pReprs )
+ pNew->pReprs[Aig_Regular(pEquivNew)->Id] = Aig_Regular(pObjNew);
+ }
+ return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [This duplicator works for AIGs with choices.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, nNodes;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // duplicate representation of choice nodes
+ if ( p->pEquivs )
+ {
+ pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ if ( p->pReprs )
+ {
+ pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ // create the PIs
+ Aig_ManCleanData( p );
+ // duplicate internal nodes
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->Level = pObj->Level;
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ }
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
+ printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ // duplicate the timing manager
+ if ( p->pManTime )
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupDfs(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [This duplicator works for AIGs with choices.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
+{
+ Vec_Ptr_t * vPios;
+ Aig_Obj_t * pObj;
+ int i;
+ assert( Aig_ManPiNum(p) == Aig_ManPiNum(pOrder) );
+ assert( Aig_ManPoNum(p) == Aig_ManPoNum(pOrder) );
+ Aig_ManSetPioNumbers( pOrder );
+ vPios = Vec_PtrAlloc( Aig_ManPiNum(p) + Aig_ManPoNum(p) );
+ Aig_ManForEachObj( pOrder, pObj, i )
+ {
+ if ( Aig_ObjIsPi(pObj) )
+ Vec_PtrPush( vPios, Aig_ManPi(p, Aig_ObjPioNum(pObj)) );
+ else if ( Aig_ObjIsPo(pObj) )
+ Vec_PtrPush( vPios, Aig_ManPo(p, Aig_ObjPioNum(pObj)) );
+ }
+ Aig_ManCleanPioNumbers( pOrder );
+ return vPios;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [This duplicator works for AIGs with choices.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
+{
+ Vec_Ptr_t * vPios;
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, nNodes;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // duplicate representation of choice nodes
+ if ( p->pEquivs )
+ {
+ pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ if ( p->pReprs )
+ {
+ pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ // create the PIs
+ Aig_ManCleanData( p );
+ // duplicate internal nodes
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+ vPios = Aig_ManOrderPios( p, pOrder );
+ Vec_PtrForEachEntry( vPios, pObj, i )
+ {
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->Level = pObj->Level;
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ }
+ Vec_PtrFree( vPios );
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
+ printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ // duplicate the timing manager
+ if ( p->pManTime )
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupDfs(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [This duplicator works for AIGs with choices.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
+{
+ Vec_Vec_t * vLevels;
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, k;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ pNew->nRegs = p->nRegs;
+ pNew->nAsserts = p->nAsserts;
+ if ( p->vFlopNums )
+ pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+ // duplicate representation of choice nodes
+ if ( p->pEquivs )
+ {
+ pNew->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ if ( p->pReprs )
+ {
+ pNew->pReprs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
+ memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
+ }
+ // create the PIs
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+ Aig_ManForEachPi( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePi( pNew );
+ pObjNew->pHaig = pObj->pHaig;
+ pObjNew->Level = pObj->Level;
+ pObj->pData = pObjNew;
+ }
+ // duplicate internal nodes
+ vLevels = Aig_ManLevelize( p );
+ Vec_VecForEachEntry( vLevels, pObj, i, k )
+ {
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ Vec_VecFree( vLevels );
+ // duplicate POs
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ pObjNew->pHaig = pObj->pHaig;
+ pObj->pData = pObjNew;
+ }
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+// if ( (nNodes = Aig_ManCleanup( pNew )) )
+// printf( "Aig_ManDupLevelized(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
+ // duplicate the timing manager
+ if ( p->pManTime )
+ pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+ // check the resulting network
+ if ( !Aig_ManCheck(pNew) )
+ printf( "Aig_ManDupLevelized(): The check has failed.\n" );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the AIG manager.]
+
+ Description [Assumes topological ordering of nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ int i;
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+ pNew->pName = Aig_UtilStrsav( p->pName );
+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+ // create the PIs
+ Aig_ManCleanData( p );
+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+ Aig_ManForEachPi( p, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pNew );
+ // duplicate internal nodes
+ Aig_ManForEachObj( p, pObj, i )
+ {
+ assert( !Aig_ObjIsBuf(pObj) );
+ if ( Aig_ObjIsNode(pObj) )
+ pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ }
+ assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+ return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
index dc083465..e465a07a 100644
--- a/src/aig/aig/aigHaig.c
+++ b/src/aig/aig/aigHaig.c
@@ -250,7 +250,7 @@ void Aig_ManHaigRecord( Aig_Man_t * p )
Aig_Obj_t * pObj;
int i;
// start the HAIG
- p->pManHaig = Aig_ManDup( p, 1 );
+ p->pManHaig = Aig_ManDupOrdered( p );
// set the pointers to the HAIG nodes
Aig_ManForEachObj( p, pObj, i )
pObj->pHaig = pObj->pData;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 3dddc687..0d5dfca9 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -105,74 +105,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
/**Function*************************************************************
- Synopsis [Duplicates the AIG manager to have EXOR gates.]
-
- Description [Assumes topological ordering of the nodes.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjNew;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
- pNew->fCatchExor = 1;
- pNew->pName = Aig_UtilStrsav( p->pName );
- pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nAsserts = p->nAsserts;
- if ( p->vFlopNums )
- pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
- // create the PIs
- Aig_ManCleanData( p );
- // duplicate internal nodes
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsBuf(pObj) )
- {
- pObjNew = Aig_ObjChild0Copy(pObj);
- }
- else if ( Aig_ObjIsNode(pObj) )
- {
- pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- }
- else if ( Aig_ObjIsPi(pObj) )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->Level = pObj->Level;
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- }
- else if ( Aig_ObjIsConst1(pObj) )
- {
- pObjNew = Aig_ManConst1(pNew);
- }
- else
- assert( 0 );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- Aig_ManCleanup( pNew );
- // duplicate the timing manager
- if ( p->pManTime )
- pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
- // check the resulting network
- if ( !Aig_ManCheck(pNew) )
- printf( "Aig_ManDup(): The check has failed.\n" );
- return pNew;
-}
-
-//#if 0
-
-/**Function*************************************************************
-
Synopsis [Duplicates the AIG manager recursively.]
Description []
@@ -198,311 +130,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
- Synopsis [Duplicates the AIG manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjNew;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
- pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nAsserts = p->nAsserts;
- if ( p->vFlopNums )
- pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
- // create the PIs
- Aig_ManCleanData( p );
- // duplicate internal nodes
- if ( fOrdered )
- {
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsBuf(pObj) )
- {
- pObjNew = Aig_ObjChild0Copy(pObj);
- }
- else if ( Aig_ObjIsNode(pObj) )
- {
- pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- }
- else if ( Aig_ObjIsPi(pObj) )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->Level = pObj->Level;
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- }
- else if ( Aig_ObjIsConst1(pObj) )
- {
- pObjNew = Aig_ManConst1(pNew);
- }
- else
- assert( 0 );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- }
- else
- {
-/*
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsPi(pObj) )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->Level = pObj->Level;
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
-// assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- }
-*/
-
- Vec_Vec_t * vLevels;
- int k;
-
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
- Aig_ManForEachPi( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->pHaig = pObj->pHaig;
- pObjNew->Level = pObj->Level;
- pObj->pData = pObjNew;
- }
-
- vLevels = Aig_ManLevelize( p );
- Vec_VecForEachEntry( vLevels, pObj, i, k )
- {
- pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- Vec_VecFree( vLevels );
-
- // add the POs
- Aig_ManForEachPo( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
-
-
-/*
- Aig_ManForEachObj( p, pObj, i )
- {
- if ( Aig_ObjIsPi(pObj) )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->Level = pObj->Level;
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
-// pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- }
- else if ( Aig_ObjIsConst1(pObj) )
- {
- pObjNew = Aig_ManConst1(pNew);
- }
- else
- {
- pObjNew = Aig_ManDup_rec( pNew, p, pObj );
- }
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- // add the POs
- Aig_ManForEachPo( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
-*/
- }
- // add the POs
-// assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-
- // duplicate the timing manager
- if ( p->pManTime )
- pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
- // check the resulting network
- if ( !Aig_ManCheck(pNew) )
- printf( "Aig_ManDup(): The check has failed.\n" );
- return pNew;
-}
-
-//#endif
-
-#if 0
-
-/**Function*************************************************************
-
- Synopsis [Duplicates the AIG manager recursively.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pObjNew;
- if ( pObj->pData )
- return pObj->pData;
- Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
- if ( Aig_ObjIsBuf(pObj) )
- return pObj->pData = Aig_ObjChild0Copy(pObj);
- Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
- pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
- return pObj->pData = pObjNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Duplicates the AIG manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj, * pObjNew;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
- pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- pNew->nRegs = p->nRegs;
- pNew->nAsserts = p->nAsserts;
- if ( p->vFlopNums )
- pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
- // create the PIs
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
- Aig_ManForEachPi( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePi( pNew );
- pObjNew->pHaig = pObj->pHaig;
- pObjNew->Level = pObj->Level;
- pObj->pData = pObjNew;
- }
- // duplicate internal nodes
- if ( fOrdered )
- {
- Aig_ManForEachObj( p, pObj, i )
- if ( Aig_ObjIsBuf(pObj) )
- {
- pObj->pData = Aig_ObjChild0Copy(pObj);
- }
- else if ( Aig_ObjIsNode(pObj) )
- {
- pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- }
- }
- else
- {
- Aig_ManForEachObj( p, pObj, i )
- if ( !Aig_ObjIsPo(pObj) )
- {
- Aig_ManDup_rec( pNew, p, pObj );
- assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
- }
- }
- // add the POs
- Aig_ManForEachPo( p, pObj, i )
- {
- pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
- pObjNew->pHaig = pObj->pHaig;
- pObj->pData = pObjNew;
- }
- assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-/*
- printf( "PIs : " );
- Aig_ManForEachPi( p, pObj, i )
- printf( "%d ", pObj->Id );
- printf( "\n" );
- printf( "PIs : " );
- Aig_ManForEachPo( p, pObj, i )
- printf( "%d ", pObj->Id );
- printf( "\n" );
-*/
- // check the resulting network
- if ( !Aig_ManCheck(pNew) )
- printf( "Aig_ManDup(): The check has failed.\n" );
- return pNew;
-}
-
-#endif
-
-/**Function*************************************************************
-
- Synopsis [Duplicates the AIG manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
-{
- Aig_Man_t * pNew;
- Aig_Obj_t * pObj;
- int i;
- // create the new manager
- pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
- pNew->pName = Aig_UtilStrsav( p->pName );
- pNew->pSpec = Aig_UtilStrsav( p->pSpec );
- // create the PIs
- Aig_ManCleanData( p );
- Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
- Aig_ManForEachPi( p, pObj, i )
- pObj->pData = Aig_ObjCreatePi( pNew );
- // duplicate internal nodes
- Aig_ManForEachObj( p, pObj, i )
- {
- assert( !Aig_ObjIsBuf(pObj) );
- if ( Aig_ObjIsNode(pObj) )
- pObj->pData = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
- }
- return pNew;
-}
-
-/**Function*************************************************************
-
Synopsis [Extracts the miter composed of XOR of the two nodes.]
Description []
@@ -670,7 +297,7 @@ void Aig_ManPrintStats( Aig_Man_t * p )
printf( "buf = %5d ", Aig_ManBufNum(p) );
// printf( "Cre = %6d ", p->nCreated );
// printf( "Del = %6d ", p->nDeleted );
-// printf( "Lev = %3d ", Aig_ManCountLevels(p) );
+// printf( "Lev = %3d ", Aig_ManLevelNum(p) );
// printf( "Max = %7d ", Aig_ManObjNumMax(p) );
printf( "lev = %3d", Aig_ManLevels(p) );
printf( "\n" );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 4ce36245..f129ae23 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1162,7 +1162,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
Vec_Ptr_t * vOutsTotal, * vOuts;
- Aig_Man_t * pAigTotal, * pAigPart, * pAig;
+ Aig_Man_t * pAigTotal, * pAigPart, * pAig, * pTemp;
Vec_Int_t * vPart, * vPartSupp;
Vec_Ptr_t * vParts;
Aig_Obj_t * pObj;
@@ -1272,6 +1272,15 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
pAig = Aig_ManRehash( pAigTotal );
// create the equivalent nodes lists
Aig_ManMarkValidChoices( pAig );
+ // reconstruct the network
+ pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry( vAigs, 0 ) );
+ Aig_ManStop( pTemp );
+ // duplicate the timing manager
+ pTemp = Vec_PtrEntry( vAigs, 0 );
+ if ( pTemp->pManTime )
+ pAig->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+ // reset levels
+ Aig_ManChoiceLevel( pAig );
return pAig;
}
@@ -1437,107 +1446,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
/**Function*************************************************************
- Synopsis [Computes levels for AIG with choices and white boxes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Aig_ManChoiceLevel_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pNext;
- int i, iBox, iTerm1, nTerms, LevelMax = 0;
- if ( Aig_ObjIsTravIdCurrent( pNew, pObj ) )
- return;
- Aig_ObjSetTravIdCurrent( pNew, pObj );
- if ( Aig_ObjIsPi(pObj) )
- {
- if ( pNew->pManTime )
- {
- iBox = Tim_ManBoxForCi( pNew->pManTime, Aig_ObjPioNum(pObj) );
- if ( iBox >= 0 ) // this is not a true PI
- {
- iTerm1 = Tim_ManBoxInputFirst( pNew->pManTime, iBox );
- nTerms = Tim_ManBoxInputNum( pNew->pManTime, iBox );
- for ( i = 0; i < nTerms; i++ )
- {
- pNext = Aig_ManPo(pNew, iTerm1 + i);
- Aig_ManChoiceLevel_rec( pNew, pNext );
- if ( LevelMax < Aig_ObjLevel(pNext) )
- LevelMax = Aig_ObjLevel(pNext);
- }
- LevelMax++;
- }
- }
- }
- else if ( Aig_ObjIsPo(pObj) )
- {
- pNext = Aig_ObjFanin0(pObj);
- Aig_ManChoiceLevel_rec( pNew, pNext );
- if ( LevelMax < Aig_ObjLevel(pNext) )
- LevelMax = Aig_ObjLevel(pNext);
- }
- else if ( Aig_ObjIsNode(pObj) )
- {
- // get the maximum level of the two fanins
- pNext = Aig_ObjFanin0(pObj);
- Aig_ManChoiceLevel_rec( pNew, pNext );
- if ( LevelMax < Aig_ObjLevel(pNext) )
- LevelMax = Aig_ObjLevel(pNext);
- pNext = Aig_ObjFanin1(pObj);
- Aig_ManChoiceLevel_rec( pNew, pNext );
- if ( LevelMax < Aig_ObjLevel(pNext) )
- LevelMax = Aig_ObjLevel(pNext);
- LevelMax++;
-
- // get the level of the nodes in the choice node
- if ( pNew->pEquivs && (pNext = pNew->pEquivs[pObj->Id]) )
- {
- Aig_ManChoiceLevel_rec( pNew, pNext );
- if ( LevelMax < Aig_ObjLevel(pNext) )
- LevelMax = Aig_ObjLevel(pNext);
- }
- }
- else
- assert( 0 );
- Aig_ObjSetLevel( pObj, LevelMax );
- assert( !Aig_ObjIsNode(pObj) || LevelMax > 0 );
-}
-
-/**Function*************************************************************
-
- Synopsis [Computes levels for AIG with choices and white boxes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_ManChoiceLevel( Aig_Man_t * pNew )
-{
- Aig_Obj_t * pObj;
- int i, LevelMax = 0;
- Aig_ManForEachObj( pNew, pObj, i )
- Aig_ObjSetLevel( pObj, 0 );
- Aig_ManSetPioNumbers( pNew );
- Aig_ManIncrementTravId( pNew );
- Aig_ManForEachPo( pNew, pObj, i )
- {
- Aig_ManChoiceLevel_rec( pNew, pObj );
- if ( LevelMax < Aig_ObjLevel(pObj) )
- LevelMax = Aig_ObjLevel(pObj);
- }
- Aig_ManCleanPioNumbers( pNew );
- return LevelMax;
-}
-
-/**Function*************************************************************
-
Synopsis [Constructively accumulates choices.]
Description []
@@ -1593,7 +1501,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
int i;
// start AIG with choices
pPrev = Vec_PtrEntry( vAigs, 0 );
- pNew = Aig_ManDup( pPrev, 1 );
+ pNew = Aig_ManDupOrdered( pPrev );
// create room for equivalent nodes and representatives
assert( pNew->pReprs == NULL );
pNew->nReprsAlloc = Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pNew);
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index e52283b1..f045cac8 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -199,7 +199,7 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
// remove useless registers
Aig_ManSeqCleanup( p );
// rehash the nodes
- return Aig_ManDup( p, 1 );
+ return Aig_ManDupOrdered( p );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index dcc0a118..e9382468 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -593,6 +593,12 @@ void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
printf( "constant 1" );
else if ( Aig_ObjIsPi(pObj) )
printf( "PI" );
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ printf( "PO" );
+ printf( "%p%s",
+ Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+ }
else
printf( "AND( %p%s, %p%s )",
Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "),
@@ -620,7 +626,7 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
Aig_ManForEachPi( p, pObj, i )
printf( " %p", pObj );
printf( "\n" );
- vNodes = Aig_ManDfs( p );
+ vNodes = Aig_ManDfs( p, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
printf( "\n" );
@@ -674,7 +680,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
pConst1 = Aig_ManConst1(p);
// collect nodes in the DFS order
- vNodes = Aig_ManDfs( p );
+ vNodes = Aig_ManDfs( p, 1 );
// assign IDs to objects
Aig_ManConst1(p)->iData = Counter++;
Aig_ManForEachPi( p, pObj, i )
@@ -758,7 +764,7 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
pConst1 = Aig_ManConst1(p);
// collect nodes in the DFS order
- vNodes = Aig_ManDfs( p );
+ vNodes = Aig_ManDfs( p, 1 );
// assign IDs to objects
Aig_ManConst1(p)->iData = Counter++;
Aig_ManForEachPi( p, pObj, i )
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index ddb12e6e..f1d018af 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -1,6 +1,7 @@
SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigCuts.c \
src/aig/aig/aigDfs.c \
+ src/aig/aig/aigDup.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigFrames.c \
src/aig/aig/aigInter.c \
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index 0a5a36b1..9ab504c0 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -122,6 +122,7 @@ void Dar_ManPrintStats( Dar_Man_t * p )
// PRTP( "T", p->ClassTimes[i], p->timeEval );
printf( "\n" );
}
+ fflush( stdout );
}
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 7d78bf40..69810125 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -45,9 +45,9 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
Aig_Man_t * pTemp;
Dar_RwrPar_t Pars, * pPars = &Pars;
Dar_ManDefaultRwrParams( pPars );
- pAig = Aig_ManDup( pAig, 0 );
+ pAig = Aig_ManDupDfs( pAig );
Dar_ManRewrite( pAig, pPars );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
return pAig;
}
@@ -80,18 +80,18 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
pParsRwr->fVerbose = fVerbose;
pParsRef->fVerbose = fVerbose;
- pAig = Aig_ManDup( pAig, 0 );
+ pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
/*
// refactor
Dar_ManRefactor( pAig, pParsRef );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
*/
@@ -105,7 +105,7 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -161,7 +161,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
- pAig = Aig_ManDup( pAig, 0 );
+ pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
@@ -174,13 +174,13 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -197,7 +197,7 @@ Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, i
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -233,7 +233,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
pParsRwr->fVerbose = 0;//fVerbose;
pParsRef->fVerbose = 0;//fVerbose;
- pAig = Aig_ManDup( pAig, 0 );
+ pAig = Aig_ManDupDfs( pAig );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// balance
@@ -247,13 +247,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// refactor
Dar_ManRefactor( pAig, pParsRef );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -267,7 +267,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -276,7 +276,7 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -290,13 +290,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
// refactor
Dar_ManRefactor( pAig, pParsRef );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
// rewrite
Dar_ManRewrite( pAig, pParsRwr );
- pAig = Aig_ManDup( pTemp = pAig, 0 );
+ pAig = Aig_ManDupDfs( pTemp = pAig );
Aig_ManStop( pTemp );
if ( fVerbose ) Aig_ManPrintStats( pAig );
@@ -330,7 +330,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
int i;
vAigs = Vec_PtrAlloc( 3 );
- pAig = Aig_ManDup(pAig, 0);
+ pAig = Aig_ManDupDfs(pAig);
Vec_PtrPush( vAigs, pAig );
Aig_ManForEachObj( pAig, pObj, i )
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index aead8c9e..779337bf 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -166,7 +166,7 @@ PRT( "Time", clock() - clk );
// duplicate the AIG
clk = clock();
-// pAig = Aig_ManDup( pTemp = pAig );
+// pAig = Aig_ManDupDfs( pTemp = pAig );
pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 444157f0..80799e3e 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -369,7 +369,7 @@ Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
Aig_Man_t * pManAigNew;
int clk;
if ( Aig_ManNodeNum(pManAig) == 0 )
- return Aig_ManDup(pManAig, 1);
+ return Aig_ManDupOrdered(pManAig);
clk = clock();
p = Fra_ManStart( pManAig, pPars );
p->pManFraig = Fra_ManPrepareComb( p );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 8b9e863e..03d03ea1 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -343,7 +343,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
if ( Aig_ManNodeNum(pManAig) == 0 )
{
pParams->nIters = 0;
- return Aig_ManDup(pManAig, 1);
+ return Aig_ManDupOrdered(pManAig);
}
assert( Aig_ManRegNum(pManAig) > 0 );
assert( pParams->nFramesK > 0 );
@@ -563,7 +563,7 @@ clk2 = clock();
Aig_Man_t * pNew;
char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
- pManAigNew = Aig_ManDup( pManAig, 1 );
+ pManAigNew = Aig_ManDupOrdered( pManAig );
pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
Ioa_WriteAiger( pNew, pFileName, 0, 1 );
Aig_ManStop( pNew );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index 9149aca4..145bafae 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -251,6 +251,31 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Duplicates the AIG manager recursively.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pObjNew;
+ if ( pObj->pData )
+ return pObj->pData;
+ Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
+ if ( Aig_ObjIsBuf(pObj) )
+ return pObj->pData = Aig_ObjChild0Copy(pObj);
+ Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
+ pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
+ Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+ return pObj->pData = pObjNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Give the AIG and classes, reduces AIG for partitioning.]
Description [Ignores registers that are not in the classes.
@@ -290,7 +315,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
{
assert( Aig_ObjIsPi(ppClass[c]) );
pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
- pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+ pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
pMiter = Aig_Exor( pNew, pMiter, pObjNew );
}
Aig_ObjCreatePo( pNew, pMiter );
@@ -300,7 +325,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
{
assert( Aig_ObjIsPi(pObj) );
pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
- pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
+ pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
Aig_ObjCreatePo( pNew, pMiter );
}
return pNew;
@@ -514,7 +539,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
if ( Aig_ManNodeNum(pAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
- return Aig_ManDup(pAig, 1);
+ return Aig_ManDupOrdered(pAig);
}
assert( Aig_ManRegNum(pAig) > 0 );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 720260a5..da7c37a3 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -298,6 +298,7 @@ void Fra_ManPrint( Fra_Man_t * p )
if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
if ( p->nSpeculs )
printf( "Speculations = %d.\n", p->nSpeculs );
+ fflush( stdout );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index bbad2a6e..83a551b8 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -52,7 +52,8 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = fVeryVerbose;
- pNew = Aig_ManDup( p, 1 );
+ pNew = Aig_ManDupOrdered( p );
+// pNew = Aig_ManDupDfs( p );
if ( fVerbose )
{
printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
@@ -91,7 +92,8 @@ PRT( "Time", clock() - clk );
clk = clock();
if ( pNew->nRegs )
{
- pNew = Aig_ManDup( pTemp = pNew, 1 );
+ pNew = Aig_ManDupOrdered( pTemp = pNew );
+// pNew = Aig_ManDupDfs( pTemp = pNew );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
@@ -147,7 +149,7 @@ PRT( "Time", clock() - clk );
// perform rewriting
clk = clock();
- pNew = Aig_ManDup( pTemp = pNew, 1 );
+ pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp );
pNew = Dar_ManRewriteDefault( pTemp = pNew );
Aig_ManStop( pTemp );
@@ -165,7 +167,7 @@ PRT( "Time", clock() - clk );
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
Aig_ManStop( pTemp );
- pNew = Aig_ManDup( pTemp = pNew, 1 );
+ pNew = Aig_ManDupOrdered( pTemp = pNew );
Aig_ManStop( pTemp );
if ( fVerbose )
{
diff --git a/src/aig/ivy/ivyMan.c b/src/aig/ivy/ivyMan.c
index 07faef85..66c279cf 100644
--- a/src/aig/ivy/ivyMan.c
+++ b/src/aig/ivy/ivyMan.c
@@ -462,6 +462,7 @@ void Ivy_ManPrintStats( Ivy_Man_t * p )
// printf( "Del = %d. ", p->nDeleted );
printf( "Lev = %3d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
printf( "\n" );
+ fflush( stdout );
}
/**Function*************************************************************
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index ed0f057b..fb4bb620 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -39,16 +39,18 @@
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig )
+Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
{
extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * pAig, int fUpdateLevel );
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+ extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
Aig_Man_t * pTemp;
// perform synthesis
//printf( "Pre-synthesis AIG: " );
//Aig_ManPrintStats( pAig );
// pTemp = Dar_ManBalance( pAig, 1 );
- pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+// pTemp = Dar_ManCompress( pAig, 1, 1, 0 );
+ pTemp = Dar_ManChoice( pAig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
//printf( "Post-synthesis AIG: " );
//Aig_ManPrintStats( pTemp );
return pTemp;
diff --git a/src/aig/nwk/nwkDfs.c b/src/aig/nwk/nwkDfs.c
index bf669086..308f4693 100644
--- a/src/aig/nwk/nwkDfs.c
+++ b/src/aig/nwk/nwkDfs.c
@@ -66,9 +66,9 @@ int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk )
{
iTerm1 = Tim_ManBoxInputFirst( pNtk->pManTime, iBox );
nTerms = Tim_ManBoxInputNum( pNtk->pManTime, iBox );
- for ( i = 0; i < nTerms; i++ )
+ for ( k = 0; k < nTerms; k++ )
{
- pNext = Nwk_ManCo( pNtk, iTerm1 + i );
+ pNext = Nwk_ManCo( pNtk, iTerm1 + k );
if ( !Nwk_ObjIsTravIdCurrent(pNext) )
{
printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index eae3bd24..44aecc03 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -115,9 +115,13 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
{
pIfObj = If_ManCreateCi( pIfMan );
If_ObjSetLevel( pIfObj, Aig_ObjLevel(pNode) );
+// printf( "pi=%d ", pIfObj->Level );
}
else if ( Aig_ObjIsPo(pNode) )
+ {
pIfObj = If_ManCreateCo( pIfMan, If_NotCond( Aig_ObjFanin0(pNode)->pData, Aig_ObjFaninC0(pNode) ) );
+// printf( "po=%d ", pIfObj->Level );
+ }
else if ( Aig_ObjIsConst1(pNode) )
pIfObj = If_ManConst1( pIfMan );
else // add the node to the mapper
@@ -130,11 +134,11 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
if ( Aig_ObjIsChoice( p, pNode ) )
{
pIfMan->nChoices++;
- for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+ for ( pPrev = pNode, pFanin = p->pEquivs[pNode->Id]; pFanin; pPrev = pFanin, pFanin = p->pEquivs[pFanin->Id] )
If_ObjSetChoice( pPrev->pData, pFanin->pData );
If_ManCreateChoice( pIfMan, pNode->pData );
}
- assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
+// assert( If_ObjLevel(pIfObj) == Aig_ObjLevel(pNode) );
}
return pIfMan;
}
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 627bfa67..3bcfcd41 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -127,7 +127,7 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
pObj->pCopy = pObjNew;
}
Aig_ManCleanup( pMan );
-// pMan = Aig_ManDup( pTemp = pMan, 1 );
+// pMan = Aig_ManDupOrdered( pTemp = pMan );
// Aig_ManStop( pTemp );
return pMan;
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f77c90e5..f0f7fb56 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14986,15 +14986,56 @@ usage:
int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Aig_Man_t * pAigNew;
- int c;
- extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig );
+ int fBalance, fVerbose, fUpdateLevel, fConstruct, c;
+ int nConfMax, nLevelMax;
+ extern Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
// set defaults
+ fBalance = 1;
+ fUpdateLevel = 1;
+ fConstruct = 0;
+ nConfMax = 1000;
+ nLevelMax = 0;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CLblcvh" ) ) != EOF )
{
switch ( c )
{
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMax < 0 )
+ goto usage;
+ break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLevelMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLevelMax < 0 )
+ goto usage;
+ break;
+ case 'b':
+ fBalance ^= 1;
+ break;
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
+ case 'c':
+ fConstruct ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -15008,7 +15049,7 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the input file name
- pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig );
+ pAigNew = Ntl_ManPerformSynthesis( pAbc->pAbc8Aig, fBalance, fUpdateLevel, fConstruct, nConfMax, nLevelMax, fVerbose );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8DChoice(): Tranformation of the AIG has failed.\n" );
@@ -15019,9 +15060,15 @@ int Abc_CommandAbc8DChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *dchoice [-h]\n" );
- fprintf( stdout, "\t performs AIG-based synthesis and derives choices\n" );
- fprintf( stdout, "\t-h : print the command usage\n");
+ fprintf( stdout, "usage: *dchoice [-C num] [-L num] [-blcvh]\n" );
+ fprintf( stdout, "\t performs AIG-based synthesis and derives choices\n" );
+ fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
+ fprintf( stdout, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
+ fprintf( stdout, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
+ fprintf( stdout, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( stdout, "\t-c : toggle constructive computation of choices [default = %s]\n", fConstruct? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 2737de32..9be147f4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -169,7 +169,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Aig_ManForEachPi( pMan, pObj, i )
pObj->pData = Abc_NtkCi(pNtkNew, i);
// rebuild the AIG
- vNodes = Aig_ManDfs( pMan );
+ vNodes = Aig_ManDfs( pMan, 1 );
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -246,7 +246,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_LatchSetInit0( pObjNew );
}
// rebuild the AIG
- vNodes = Aig_ManDfs( pMan );
+ vNodes = Aig_ManDfs( pMan, 1 );
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( Aig_ObjIsBuf(pObj) )
pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
@@ -411,7 +411,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
}
Abc_NtkAddDummyBoxNames( pNtkNew );
// rebuild the AIG
- vNodes = Aig_ManDfs( pMan );
+ vNodes = Aig_ManDfs( pMan, 1 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
// add the first fanin
@@ -629,7 +629,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
// Aig_ManStop( pTemp );
clk = clock();
- pMan = Aig_ManDup( pTemp = pMan, 0 );
+ pMan = Aig_ManDupDfs( pTemp = pMan );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
@@ -666,7 +666,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
// Aig_ManStop( pTemp );
clk = clock();
- pMan = Aig_ManDup( pTemp = pMan, 0 );
+ pMan = Aig_ManDupDfs( pTemp = pMan );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e5f028fe..fafcb52d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -293,6 +293,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
// if ( Abc_NtkHasSop(pNtk) )
// printf( "The total number of cube pairs = %d.\n", Abc_NtkGetCubePairNum(pNtk) );
+ fflush( stdout );
}
/**Function*************************************************************
diff --git a/src/misc/hash/hashInt.h b/src/misc/hash/hashInt.h
index 3b91f5df..b7ec8a8c 100644
--- a/src/misc/hash/hashInt.h
+++ b/src/misc/hash/hashInt.h
@@ -90,7 +90,7 @@ static inline Hash_Int_t * Hash_IntAlloc( int nBins )
p->nBins = nBins;
p->fHash = Hash_DefaultHashFunc;
p->nSize = 0;
- p->pArray = ALLOC( Hash_Int_Entry_t *, nBins );
+ p->pArray = ALLOC( Hash_Int_Entry_t *, nBins+1 );
for(i=0; i<nBins; i++)
p->pArray[i] = NULL;
@@ -270,17 +270,18 @@ static inline int* Hash_IntEntryPtr( Hash_Int_t *p, int key )
***********************************************************************/
static inline void Hash_IntFree( Hash_Int_t *p ) {
int bin;
- Hash_Int_Entry_t *pEntry;
+ Hash_Int_Entry_t *pEntry, *pTemp;
// free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
+ pTemp = pEntry;
pEntry = pEntry->pNext;
- FREE( pEntry );
+ FREE( pTemp );
}
}
-
+
// free hash
FREE( p->pArray );
FREE( p );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 7fd937d5..12cb5c45 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -369,6 +369,7 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
// PRT( "Selection ", timeSelect );
// PRT( "Assignment", timeAssign );
+ fflush( stdout );
}
/**Function*************************************************************
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 11:24:56 +0000