summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp12
-rw-r--r--abc.rc3
-rw-r--r--src/aig/aig/aig.h17
-rw-r--r--src/aig/aig/aigDfs.c58
-rw-r--r--src/aig/aig/aigMffc.c297
-rw-r--r--src/aig/aig/aigObj.c5
-rw-r--r--src/aig/aig/aigTable.c27
-rw-r--r--src/aig/aig/aigTruth.c98
-rw-r--r--src/aig/aig/aigUtil.c20
-rw-r--r--src/aig/aig/aigWin.c184
-rw-r--r--src/aig/aig/module.make5
-rw-r--r--src/aig/dar/dar.h29
-rw-r--r--src/aig/dar/darCore.c20
-rw-r--r--src/aig/dar/darInt.h7
-rw-r--r--src/aig/dar/darLib.c87
-rw-r--r--src/aig/dar/darMan.c2
-rw-r--r--src/aig/dar/darRefact.c532
-rw-r--r--src/aig/dar/darScript.c204
-rw-r--r--src/aig/kit/kit.h1
-rw-r--r--src/base/abci/abc.c198
-rw-r--r--src/base/abci/abcDar.c76
-rw-r--r--src/base/abci/abcRefactor.c6
-rw-r--r--src/base/abci/abcResub.c7
-rw-r--r--src/base/abci/abcRewrite.c2
-rw-r--r--src/misc/vec/vecPtr.h19
-rw-r--r--src/opt/rwr/rwr.h2
-rw-r--r--src/opt/rwr/rwrMan.c2
27 files changed, 1800 insertions, 120 deletions
diff --git a/abc.dsp b/abc.dsp
index 7bb16175..30f5e2ca 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -2746,6 +2746,10 @@ SOURCE=.\src\aig\aig\aigMem.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\aig\aigMffc.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\aig\aigObj.c
# End Source File
# Begin Source File
@@ -2766,8 +2770,16 @@ SOURCE=.\src\aig\aig\aigTiming.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\aig\aigTruth.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\aig\aigUtil.c
# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigWin.c
+# End Source File
# End Group
# End Group
# End Group
diff --git a/abc.rc b/abc.rc
index 71f16fb5..d4539ac4 100644
--- a/abc.rc
+++ b/abc.rc
@@ -168,6 +168,7 @@ alias tst6 "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
#alias t "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
#alias t "r i10.blif; st; ps; csweep; ps; cec"
#alias t "r c/5/csat_777.bench; st; csweep -v"
-alias t "r i10.blif; st; drw -v"
+#alias t "r i10.blif; st; drw -v"
+alias t "r c.blif; st; drf"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 6725f4a6..8c9400be 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -274,6 +274,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
// iterator over all nodes
#define Aig_ManForEachNode( p, pObj, i ) \
Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+// iterator over the nodes whose IDs are stored in the array
+#define Aig_ManForEachNodeVec( p, vIds, pObj, i ) \
+ for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
// these two procedures are only here for the use inside the iterator
static inline int Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId ) { assert(ObjId < p->nFansAlloc); return p->pFanData[5*ObjId]; }
@@ -299,6 +302,7 @@ extern int Aig_DagSize( Aig_Obj_t * pObj );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
+extern void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
/*=== 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 );
@@ -314,6 +318,13 @@ extern void Aig_ManPrintStats( Aig_Man_t * p );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p );
+/*=== aigMffc.c ==========================================================*/
+extern int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
+extern int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin );
+extern int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
+extern int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode );
+extern int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
+extern int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
/*=== aigObj.c ==========================================================*/
extern Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p );
extern Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );
@@ -341,6 +352,7 @@ extern Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars );
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigTable.c ========================================================*/
extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
+extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 );
extern void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern int Aig_TableCountEntries( Aig_Man_t * p );
@@ -351,10 +363,13 @@ extern void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIn
extern void Aig_ManStopReverseLevels( Aig_Man_t * p );
extern void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
extern void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
+/*=== aigTruth.c ========================================================*/
+extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
/*=== aigUtil.c =========================================================*/
extern unsigned Aig_PrimeCudd( unsigned p );
extern void Aig_ManIncrementTravId( Aig_Man_t * p );
extern int Aig_ManLevels( Aig_Man_t * p );
+extern void Aig_ManCheckMarkA( Aig_Man_t * p );
extern void Aig_ManCleanData( Aig_Man_t * p );
extern void Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
@@ -367,6 +382,8 @@ extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_
extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+/*=== aigWin.c =========================================================*/
+extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
/*=== aigMem.c ===========================================================*/
// fixed-size-block memory manager
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index a71afec6..62900bb5 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -433,6 +433,64 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in
return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
}
+/**Function*************************************************************
+
+ Synopsis [Computes the internal nodes of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+// Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
+// Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
+ if ( pNode->fMarkA )
+ return;
+ pNode->fMarkA = 1;
+ assert( Aig_ObjIsNode(pNode) );
+ Aig_ManCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
+ Aig_ManCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
+ Vec_PtrPush( vNodes, pNode );
+//printf( "added %d ", pNode->Id );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the internal nodes of the cut.]
+
+ Description [Does not include the leaves of the cut.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ // collect and mark the leaves
+ Vec_PtrClear( vNodes );
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ {
+ assert( pObj->fMarkA == 0 );
+ pObj->fMarkA = 1;
+// printf( "%d " , pObj->Id );
+ }
+//printf( "\n" );
+ // collect and mark the nodes
+ Aig_ManCollectCut_rec( pRoot, vNodes );
+ // clean the nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->fMarkA = 0;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->fMarkA = 0;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c
new file mode 100644
index 00000000..47ce896d
--- /dev/null
+++ b/src/aig/aig/aigMffc.c
@@ -0,0 +1,297 @@
+/**CFile****************************************************************
+
+ FileName [aigMffc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Computation of MFFCs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigMffc.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Dereferences the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin )
+{
+ Aig_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Aig_ObjIsPi(pNode) )
+ return 0;
+ // consider the first fanin
+ pFanin = Aig_ObjFanin0(pNode);
+ assert( pFanin->nRefs > 0 );
+ if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeDeref_rec( pFanin, LevelMin );
+ // skip the buffer
+ if ( Aig_ObjIsBuf(pNode) )
+ return Counter;
+ assert( Aig_ObjIsNode(pNode) );
+ // consider the second fanin
+ pFanin = Aig_ObjFanin1(pNode);
+ assert( pFanin->nRefs > 0 );
+ if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeDeref_rec( pFanin, LevelMin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin )
+{
+ Aig_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Aig_ObjIsPi(pNode) )
+ return 0;
+ // consider the first fanin
+ pFanin = Aig_ObjFanin0(pNode);
+ if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeRef_rec( pFanin, LevelMin );
+ // skip the buffer
+ if ( Aig_ObjIsBuf(pNode) )
+ return Counter;
+ assert( Aig_ObjIsNode(pNode) );
+ // consider the second fanin
+ pFanin = Aig_ObjFanin1(pNode);
+ if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeRef_rec( pFanin, LevelMin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin )
+{
+ Aig_Obj_t * pFanin;
+ int Counter = 0;
+ if ( Aig_ObjIsPi(pNode) )
+ return 0;
+ Aig_ObjSetTravIdCurrent( p, pNode );
+ // consider the first fanin
+ pFanin = Aig_ObjFanin0(pNode);
+ if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
+ if ( Aig_ObjIsBuf(pNode) )
+ return Counter;
+ assert( Aig_ObjIsNode(pNode) );
+ // consider the second fanin
+ pFanin = Aig_ObjFanin1(pNode);
+ if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+ Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
+ return Counter + 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the internal and boundary nodes in the derefed MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
+{
+ // skip visited nodes
+ if ( Aig_ObjIsTravIdCurrent(p, pNode) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pNode);
+ // add to the new support nodes
+ if ( !fTopmost && pNode != pObjSkip && (Aig_ObjIsPi(pNode) || pNode->nRefs > 0 || pNode->Level <= LevelMin) )
+ {
+ if ( vSupp ) Vec_PtrPush( vSupp, pNode );
+ return;
+ }
+ assert( Aig_ObjIsNode(pNode) );
+ // recur on the children
+ Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
+ Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the support of depth-limited MFFC.]
+
+ Description [Returns the number of internal nodes in the MFFC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
+{
+ int ConeSize1, ConeSize2;
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_ObjIsNode(pNode) );
+ if ( vSupp ) Vec_PtrClear( vSupp );
+ Aig_ManIncrementTravId( p );
+ ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin );
+ Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
+ ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
+ assert( ConeSize1 == ConeSize2 );
+ assert( ConeSize1 > 0 );
+ return ConeSize1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Labels the nodes in the MFFC.]
+
+ Description [Returns the number of internal nodes in the MFFC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+ int ConeSize1, ConeSize2;
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_ObjIsNode(pNode) );
+ Aig_ManIncrementTravId( p );
+ ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+ ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
+ assert( ConeSize1 == ConeSize2 );
+ assert( ConeSize1 > 0 );
+ return ConeSize1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Labels the nodes in the MFFC.]
+
+ Description [Returns the number of internal nodes in the MFFC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+ Aig_Obj_t * pObj;
+ int i, ConeSize1, ConeSize2;
+ assert( !Aig_IsComplement(pNode) );
+ assert( Aig_ObjIsNode(pNode) );
+ Aig_ManIncrementTravId( p );
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->nRefs++;
+ ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+ ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->nRefs--;
+ assert( ConeSize1 == ConeSize2 );
+ assert( ConeSize1 > 0 );
+ return ConeSize1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Expands the cut by adding the most closely related node.]
+
+ Description [Returns 1 if the cut exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
+{
+ Aig_Obj_t * pObj, * pLeafBest;
+ int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
+ // dereference the current cut
+ LevelMax = 0;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ LevelMax = AIG_MAX( LevelMax, (int)pObj->Level );
+ if ( LevelMax == 0 )
+ return 0;
+ // dereference the cut
+ ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+ // try expanding each node in the boundary
+ ConeBest = AIG_INFINITY;
+ pLeafBest = NULL;
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ {
+ if ( (int)pObj->Level != LevelMax )
+ continue;
+ ConeCur1 = Aig_NodeDeref_rec( pObj, 0 );
+ if ( ConeBest > ConeCur1 )
+ {
+ ConeBest = ConeCur1;
+ pLeafBest = pObj;
+ }
+ ConeCur2 = Aig_NodeRef_rec( pObj, 0 );
+ assert( ConeCur1 == ConeCur2 );
+ }
+ assert( pLeafBest != NULL );
+ assert( Aig_ObjIsNode(pLeafBest) );
+ // deref the best leaf
+ ConeCur1 = Aig_NodeDeref_rec( pLeafBest, 0 );
+ // collect the cut nodes
+ Vec_PtrClear( vResult );
+ Aig_ManIncrementTravId( p );
+ Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
+ // ref the nodes
+ ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
+ assert( ConeCur1 == ConeCur2 );
+ // ref the original node
+ ConeSize2 = Aig_NodeRef_rec( pNode, 0 );
+ assert( ConeSize1 == ConeSize2 );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 542b90f9..f2296e01 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -380,12 +380,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// delete the new object
Aig_ObjDelete( p, pObjNew );
// update levels
- if ( fUpdateLevel )
+ if ( p->pFanData )
{
pObjOld->Level = LevelOld;
Aig_ManUpdateLevel( p, pObjOld );
- Aig_ManUpdateReverseLevel( p, pObjOld );
}
+ if ( fUpdateLevel )
+ Aig_ManUpdateReverseLevel( p, pObjOld );
}
p->nObjs[pObjOld->Type]++;
// store buffers if fanout is allocated
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index bba7650a..ba359c09 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -146,6 +146,33 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
/**Function*************************************************************
+ Synopsis [Checks if node with the given attributes is in the hash table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 )
+{
+ Aig_Obj_t * pGhost;
+ // consider simple cases
+ if ( pFanin0 == pFanin1 )
+ return pFanin0;
+ if ( pFanin0 == Aig_Not(pFanin1) )
+ return Aig_ManConst0(p);
+ if ( Aig_Regular(pFanin0) == Aig_ManConst1(p) )
+ return pFanin0 == Aig_ManConst1(p) ? pFanin1 : Aig_ManConst0(p);
+ if ( Aig_Regular(pFanin1) == Aig_ManConst1(p) )
+ return pFanin1 == Aig_ManConst1(p) ? pFanin0 : Aig_ManConst0(p);
+ pGhost = Aig_ObjCreateGhost( p, pFanin0, pFanin1, AIG_OBJ_AND );
+ return Aig_TableLookup( p, pGhost );
+}
+
+/**Function*************************************************************
+
Synopsis [Adds the new node to the hash table.]
Description []
diff --git a/src/aig/aig/aigTruth.c b/src/aig/aig/aigTruth.c
new file mode 100644
index 00000000..a92f9e1d
--- /dev/null
+++ b/src/aig/aig/aigTruth.c
@@ -0,0 +1,98 @@
+/**CFile****************************************************************
+
+ FileName [aigTruth.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Computes truth table for the cut.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigTruth.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes truth table of the cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Aig_ManCutTruthOne( Aig_Obj_t * pNode, unsigned * pTruth, int nWords )
+{
+ unsigned * pTruth0, * pTruth1;
+ int i;
+ pTruth0 = Aig_ObjFanin0(pNode)->pData;
+ pTruth1 = Aig_ObjFanin1(pNode)->pData;
+ if ( Aig_ObjIsExor(pNode) )
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = pTruth0[i] ^ pTruth1[i];
+ else if ( !Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) )
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = pTruth0[i] & pTruth1[i];
+ else if ( !Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) )
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = pTruth0[i] & ~pTruth1[i];
+ else if ( Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) )
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = ~pTruth0[i] & pTruth1[i];
+ else // if ( Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) )
+ for ( i = 0; i < nWords; i++ )
+ pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+ return pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes truth table of the cut.]
+
+ Description [The returned pointer should be used immediately.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore )
+{
+ Aig_Obj_t * pObj;
+ int i, nWords;
+ assert( Vec_PtrSize(vLeaves) <= Vec_PtrSize(vTruthElem) );
+ assert( Vec_PtrSize(vNodes) <= Vec_PtrSize(vTruthStore) );
+ assert( Vec_PtrSize(vNodes) == 0 || pRoot == Vec_PtrEntryLast(vNodes) );
+ // assign elementary truth tables
+ Vec_PtrForEachEntry( vLeaves, pObj, i )
+ pObj->pData = Vec_PtrEntry( vTruthElem, i );
+ // compute truths for other nodes
+ nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pData = Aig_ManCutTruthOne( pObj, Vec_PtrEntry(vTruthStore, i), nWords );
+ return pRoot->pData;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 1e45bca1..a1c68371 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -104,6 +104,25 @@ int Aig_ManLevels( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Checks if the markA is reset.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManCheckMarkA( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManForEachObj( p, pObj, i )
+ assert( pObj->fMarkA == 0 );
+}
+
+/**Function*************************************************************
+
Synopsis [Cleans the data pointers for the nodes.]
Description []
@@ -144,6 +163,7 @@ void Aig_ObjCleanData_rec( Aig_Obj_t * pObj )
pObj->pData = NULL;
}
+
/**Function*************************************************************
Synopsis [Detects multi-input gate rooted at this node.]
diff --git a/src/aig/aig/aigWin.c b/src/aig/aig/aigWin.c
new file mode 100644
index 00000000..0485b243
--- /dev/null
+++ b/src/aig/aig/aigWin.c
@@ -0,0 +1,184 @@
+/**CFile****************************************************************
+
+ FileName [aigWin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Window computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigWin.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Evaluate the cost of removing the node from the set of leaves.]
+
+ Description [Returns the number of new leaves that will be brought in.
+ Returns large number if the node cannot be removed from the set of leaves.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Aig_NodeGetLeafCostOne( Aig_Obj_t * pNode, int nFanoutLimit )
+{
+ int Cost;
+ // make sure the node is in the construction zone
+ assert( pNode->fMarkA );
+ // cannot expand over the PI node
+ if ( Aig_ObjIsPi(pNode) )
+ return 999;
+ // get the cost of the cone
+ Cost = (!Aig_ObjFanin0(pNode)->fMarkA) + (!Aig_ObjFanin1(pNode)->fMarkA);
+ // always accept if the number of leaves does not increase
+ if ( Cost < 2 )
+ return Cost;
+ // skip nodes with many fanouts
+ if ( (int)pNode->nRefs > nFanoutLimit )
+ return 999;
+ // return the number of nodes that will be on the leaves if this node is removed
+ return Cost;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+ Description [This procedure looks at the current leaves and tries to change
+ one leaf at a time in such a way that the cut grows as little as possible.
+ In evaluating the fanins, this procedure looks only at their immediate
+ predecessors (this is why it is called a one-level construction procedure).]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManFindCut_int( Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit )
+{
+ Aig_Obj_t * pNode, * pFaninBest, * pNext;
+ int CostBest, CostCur, i;
+ // find the best fanin
+ CostBest = 100;
+ pFaninBest = NULL;
+//printf( "Evaluating fanins of the cut:\n" );
+ Vec_PtrForEachEntry( vFront, pNode, i )
+ {
+ CostCur = Aig_NodeGetLeafCostOne( pNode, nFanoutLimit );
+//printf( " Fanin %s has cost %d.\n", Aig_ObjName(pNode), CostCur );
+ if ( CostBest > CostCur ||
+ (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
+ {
+ CostBest = CostCur;
+ pFaninBest = pNode;
+ }
+ if ( CostBest == 0 )
+ break;
+ }
+ if ( pFaninBest == NULL )
+ return 0;
+ assert( CostBest < 3 );
+ if ( Vec_PtrSize(vFront) - 1 + CostBest > nSizeLimit )
+ return 0;
+ assert( Aig_ObjIsNode(pFaninBest) );
+ // remove the node from the array
+ Vec_PtrRemove( vFront, pFaninBest );
+//printf( "Removing fanin %s.\n", Aig_ObjName(pFaninBest) );
+
+ // add the left child to the fanins
+ pNext = Aig_ObjFanin0(pFaninBest);
+ if ( !pNext->fMarkA )
+ {
+//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) );
+ pNext->fMarkA = 1;
+ Vec_PtrPush( vFront, pNext );
+ Vec_PtrPush( vVisited, pNext );
+ }
+ // add the right child to the fanins
+ pNext = Aig_ObjFanin1(pFaninBest);
+ if ( !pNext->fMarkA )
+ {
+//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) );
+ pNext->fMarkA = 1;
+ Vec_PtrPush( vFront, pNext );
+ Vec_PtrPush( vVisited, pNext );
+ }
+ assert( Vec_PtrSize(vFront) <= nSizeLimit );
+ // keep doing this
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes one sequential cut of the given size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit )
+{
+ Aig_Obj_t * pNode;
+ int i;
+
+ assert( !Aig_IsComplement(pRoot) );
+ assert( Aig_ObjIsNode(pRoot) );
+ assert( Aig_ObjChild0(pRoot) );
+ assert( Aig_ObjChild1(pRoot) );
+
+ // start the cut
+ Vec_PtrClear( vFront );
+ Vec_PtrPush( vFront, Aig_ObjFanin0(pRoot) );
+ Vec_PtrPush( vFront, Aig_ObjFanin1(pRoot) );
+
+ // start the visited nodes
+ Vec_PtrClear( vVisited );
+ Vec_PtrPush( vVisited, pRoot );
+ Vec_PtrPush( vVisited, Aig_ObjFanin0(pRoot) );
+ Vec_PtrPush( vVisited, Aig_ObjFanin1(pRoot) );
+
+ // mark these nodes
+ assert( !pRoot->fMarkA );
+ assert( !Aig_ObjFanin0(pRoot)->fMarkA );
+ assert( !Aig_ObjFanin1(pRoot)->fMarkA );
+ pRoot->fMarkA = 1;
+ Aig_ObjFanin0(pRoot)->fMarkA = 1;
+ Aig_ObjFanin1(pRoot)->fMarkA = 1;
+
+ // compute the cut
+ while ( Aig_ManFindCut_int( vFront, vVisited, nSizeLimit, nFanoutLimit ) );
+ assert( Vec_PtrSize(vFront) <= nSizeLimit );
+
+ // clean the visit markings
+ Vec_PtrForEachEntry( vVisited, pNode, i )
+ pNode->fMarkA = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index f9afc4ee..83e4c413 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -2,10 +2,13 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigDfs.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigMan.c \
+ src/aig/aig/aigMffc.c \
src/aig/aig/aigMem.c \
src/aig/aig/aigObj.c \
src/aig/aig/aigOper.c \
src/aig/aig/aigSeq.c \
src/aig/aig/aigTable.c \
src/aig/aig/aigTiming.c \
- src/aig/aig/aigUtil.c
+ src/aig/aig/aigTruth.c \
+ src/aig/aig/aigUtil.c \
+ src/aig/aig/aigWin.c
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index cff2785b..3106c7ad 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -37,10 +37,10 @@ extern "C" {
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
-typedef struct Dar_Par_t_ Dar_Par_t;
+typedef struct Dar_RwrPar_t_ Dar_RwrPar_t;
+typedef struct Dar_RefPar_t_ Dar_RefPar_t;
-// the rewriting parameters
-struct Dar_Par_t_
+struct Dar_RwrPar_t_
{
int nCutsMax; // the maximum number of cuts to try
int nSubgMax; // the maximum number of subgraphs to try
@@ -50,6 +50,18 @@ struct Dar_Par_t_
int fVeryVerbose; // enables very verbose output
};
+struct Dar_RefPar_t_
+{
+ int nMffcMin; // the min MFFC size for which refactoring is used
+ int nLeafMax; // the max number of leaves of a cut
+ int nCutsMax; // the max number of cuts to consider
+ int fExtend; // extends the cut below MFFC
+ int fUpdateLevel; // updates the level after each move
+ int fUseZeros; // perform zero-cost replacements
+ int fVerbose; // verbosity level
+ int fVeryVerbose; // enables very verbose output
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -62,10 +74,17 @@ struct Dar_Par_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== darBalance.c ========================================================*/
+extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
/*=== darCore.c ========================================================*/
-extern void Dar_ManDefaultParams( Dar_Par_t * pPars );
-extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars );
+extern void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
+extern int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig );
+/*=== darRefact.c ========================================================*/
+extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
+extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
+/*=== darScript.c ========================================================*/
+extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index e7186e83..7546df0b 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -39,15 +39,15 @@
SeeAlso []
***********************************************************************/
-void Dar_ManDefaultParams( Dar_Par_t * pPars )
+void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
{
- memset( pPars, 0, sizeof(Dar_Par_t) );
- pPars->nCutsMax = 8;
- pPars->nSubgMax = 5; // 5 is a "magic number"
- pPars->fUpdateLevel = 0;
- pPars->fUseZeros = 0;
- pPars->fVerbose = 0;
- pPars->fVeryVerbose = 0;
+ memset( pPars, 0, sizeof(Dar_RwrPar_t) );
+ pPars->nCutsMax = 8;
+ pPars->nSubgMax = 5; // 5 is a "magic number"
+ pPars->fUpdateLevel = 0;
+ pPars->fUseZeros = 0;
+ pPars->fVerbose = 0;
+ pPars->fVeryVerbose = 0;
}
/**Function*************************************************************
@@ -61,7 +61,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
SeeAlso []
***********************************************************************/
-int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
+int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
{
Dar_Man_t * p;
ProgressBar * pProgress;
@@ -128,7 +128,7 @@ p->timeCuts += clock() - clk;
// evaluate the cuts
p->GainBest = -1;
- Required = 1000000;
+ Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
Dar_ObjForEachCut( pObj, pCut, k )
Dar_LibEval( p, pObj, pCut, Required );
// check the best gain
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index f496a73f..0acd272c 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -64,8 +64,8 @@ struct Dar_Cut_t_ // 6 words
// the AIG manager
struct Dar_Man_t_
{
- // input data;
- Dar_Par_t * pPars; // rewriting parameters
+ // input data
+ Dar_RwrPar_t * pPars; // rewriting parameters
Aig_Man_t * pAig; // AIG manager
// various data members
Aig_MmFixed_t * pMemCuts; // memory manager for cuts
@@ -125,7 +125,6 @@ static inline void Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )
////////////////////////////////////////////////////////////////////////
/*=== darBalance.c ========================================================*/
-extern Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
/*=== darCore.c ===========================================================*/
/*=== darCut.c ============================================================*/
extern void Dar_ManCutsStart( Dar_Man_t * p );
@@ -144,7 +143,7 @@ extern void Dar_LibReturnCanonicals( unsigned * pCanons );
extern void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ============================================================*/
-extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
+extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern void Dar_ManStop( Dar_Man_t * p );
extern void Dar_ManPrintStats( Dar_Man_t * p );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index c3d57b52..72ce0cde 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -707,65 +707,6 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut )
/**Function*************************************************************
- Synopsis [Dereferences the node's MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeDeref_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
-{
- Aig_Obj_t * pFanin;
- int Counter = 0;
- if ( Aig_ObjIsPi(pNode) )
- return Counter;
- pFanin = Aig_ObjFanin0( pNode );
- assert( pFanin->nRefs > 0 );
- if ( --pFanin->nRefs == 0 )
- Counter += Aig_NodeDeref_rec( p, pFanin );
- if ( Aig_ObjIsBuf(pNode) )
- return Counter;
- pFanin = Aig_ObjFanin1( pNode );
- assert( pFanin->nRefs > 0 );
- if ( --pFanin->nRefs == 0 )
- Counter += Aig_NodeDeref_rec( p, pFanin );
- return 1 + Counter;
-}
-
-/**Function*************************************************************
-
- Synopsis [References the node's MFFC.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
-{
- Aig_Obj_t * pFanin;
- int Counter = 0;
- if ( Aig_ObjIsPi(pNode) )
- return Counter;
- Aig_ObjSetTravIdCurrent( p, pNode );
- pFanin = Aig_ObjFanin0( pNode );
- if ( pFanin->nRefs++ == 0 )
- Counter += Aig_NodeRef_rec( p, pFanin );
- if ( Aig_ObjIsBuf(pNode) )
- return Counter;
- pFanin = Aig_ObjFanin1( pNode );
- if ( pFanin->nRefs++ == 0 )
- Counter += Aig_NodeRef_rec( p, pFanin );
- return 1 + Counter;
-}
-
-/**Function*************************************************************
-
Synopsis [Marks the MFFC of the node.]
Description []
@@ -777,19 +718,16 @@ int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
***********************************************************************/
int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves )
{
- int i, nNodes1, nNodes2;
+ int i, nNodes;
// mark the cut leaves
for ( i = 0; i < nLeaves; i++ )
Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
// label MFFC with current ID
- Aig_ManIncrementTravId( p );
- nNodes1 = Aig_NodeDeref_rec( p, pRoot );
- nNodes2 = Aig_NodeRef_rec( p, pRoot );
- assert( nNodes1 == nNodes2 );
+ nNodes = Aig_NodeMffsLabel( p, pRoot );
// unmark the cut leaves
for ( i = 0; i < nLeaves; i++ )
Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
- return nNodes1;
+ return nNodes;
}
/**Function*************************************************************
@@ -836,7 +774,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
{
Dar_LibObj_t * pObj;
Dar_LibDat_t * pData, * pData0, * pData1;
- Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
+ Aig_Obj_t * pFanin0, * pFanin1;
int i;
for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
{
@@ -859,22 +797,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
continue;
pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 );
-
- // consider simple cases
- if ( pFanin0 == pFanin1 )
- pData->pFunc = pFanin0;
- else if ( pFanin0 == Aig_Not(pFanin1) )
- pData->pFunc = Aig_ManConst0(p->pAig);
- else if ( Aig_Regular(pFanin0) == Aig_ManConst1(p->pAig) )
- pData->pFunc = pFanin0 == Aig_ManConst1(p->pAig) ? pFanin1 : Aig_ManConst0(p->pAig);
- else if ( Aig_Regular(pFanin1) == Aig_ManConst1(p->pAig) )
- pData->pFunc = pFanin1 == Aig_ManConst1(p->pAig) ? pFanin0 : Aig_ManConst0(p->pAig);
- else
- {
- pGhost = Aig_ObjCreateGhost( p->pAig, pFanin0, pFanin1, AIG_OBJ_AND );
- pData->pFunc = Aig_TableLookup( p->pAig, pGhost );
- }
-
+ pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 );
// clear the node if it is part of MFFC
if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
pData->fMffc = 1;
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index 8b7c5afb..ef898ea2 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -39,7 +39,7 @@
SeeAlso []
***********************************************************************/
-Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
+Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
{
Dar_Man_t * p;
// start the manager
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 1bcc0466..cdfbaa01 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -19,17 +19,151 @@
***********************************************************************/
#include "darInt.h"
+#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+// the refactoring manager
+typedef struct Ref_Man_t_ Ref_Man_t;
+struct Ref_Man_t_
+{
+ // input data
+ Dar_RefPar_t * pPars; // rewriting parameters
+ Aig_Man_t * pAig; // AIG manager
+ // computed cuts
+ Vec_Vec_t * vCuts; // the storage for cuts
+ // truth table and ISOP
+ Vec_Ptr_t * vTruthElem; // elementary truth tables
+ Vec_Ptr_t * vTruthStore; // storage for truth tables
+ Vec_Int_t * vMemory; // storage for ISOP
+ Vec_Ptr_t * vCutNodes; // storage for internal nodes of the cut
+ // various data members
+ Vec_Ptr_t * vLeavesBest; // the best set of leaves
+ Kit_Graph_t * pGraphBest; // the best factored form
+ int GainBest; // the best gain
+ int LevelBest; // the level of node with the best gain
+ // node statistics
+ int nNodesInit; // the initial number of nodes
+ int nNodesTried; // the number of nodes tried
+ int nNodesBelow; // the number of nodes below the level limit
+ int nNodesExten; // the number of nodes with extended cut
+ int nCutsUsed; // the number of rewriting steps
+ int nCutsTried; // the number of cuts tries
+ // timing statistics
+ int timeCuts;
+ int timeEval;
+ int timeOther;
+ int timeTotal;
+};
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis [Returns the structure with default assignment of parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars )
+{
+ memset( pPars, 0, sizeof(Dar_RefPar_t) );
+ pPars->nMffcMin = 2; // the min MFFC size for which refactoring is used
+ pPars->nLeafMax = 12; // the max number of leaves of a cut
+ pPars->nCutsMax = 5; // the max number of cuts to consider
+ pPars->fUpdateLevel = 0;
+ pPars->fUseZeros = 0;
+ pPars->fVerbose = 0;
+ pPars->fVeryVerbose = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Starts the rewriting manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
+{
+ Ref_Man_t * p;
+ // start the manager
+ p = ALLOC( Ref_Man_t, 1 );
+ memset( p, 0, sizeof(Ref_Man_t) );
+ p->pAig = pAig;
+ p->pPars = pPars;
+ // other data
+ p->vCuts = Vec_VecStart( pPars->nCutsMax );
+ p->vTruthElem = Vec_PtrAllocTruthTables( pPars->nLeafMax );
+ p->vTruthStore = Vec_PtrAllocSimInfo( 256, Kit_TruthWordNum(pPars->nLeafMax) );
+ p->vMemory = Vec_IntAlloc( 1 << 16 );
+ p->vCutNodes = Vec_PtrAlloc( 256 );
+ p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prints out the statistics of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManRefPrintStats( Ref_Man_t * p )
+{
+ int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
+ printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n",
+ p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit );
+ printf( "Tried = %6d. Below = %5d. Extended = %5d. Used = %5d.\n",
+ p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed );
+ PRT( "Cuts ", p->timeCuts );
+ PRT( "Eval ", p->timeEval );
+ PRT( "Other ", p->timeOther );
+ PRT( "TOTAL ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the rewriting manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dar_ManRefStop( Ref_Man_t * p )
+{
+ if ( p->pPars->fVerbose )
+ Dar_ManRefPrintStats( p );
+ Vec_VecFree( p->vCuts );
+ Vec_PtrFree( p->vTruthElem );
+ Vec_PtrFree( p->vTruthStore );
+ Vec_PtrFree( p->vLeavesBest );
+ Vec_IntFree( p->vMemory );
+ Vec_PtrFree( p->vCutNodes );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -39,7 +173,405 @@
SeeAlso []
***********************************************************************/
+void Ref_ObjComputeCuts( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Vec_t * vCuts )
+{
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ref_ObjPrint( Aig_Obj_t * pObj )
+{
+ printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 );
+ if ( pObj )
+ printf( "(%d) ", Aig_IsComplement(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of new nodes added when using this graph.]
+
+ Description [AIG nodes for the fanins should be assigned to pNode->pFunc
+ of the leaves of the graph before calling this procedure.
+ Returns -1 if the number of nodes and levels exceeded the given limit or
+ the number of levels exceeded the maximum allowed level.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+ Kit_Node_t * pNode, * pNode0, * pNode1;
+ Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
+ int i, Counter, LevelNew, LevelOld;
+ // check for constant function or a literal
+ if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
+ return 0;
+ // set the levels of the leaves
+ Kit_GraphForEachLeaf( pGraph, pNode, i )
+ {
+ pNode->pFunc = Vec_PtrEntry(vCut, i);
+ pNode->Level = Aig_Regular(pNode->pFunc)->Level;
+ assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-1 );
+ }
+//printf( "Trying:\n" );
+ // compute the AIG size after adding the internal nodes
+ Counter = 0;
+ Kit_GraphForEachNode( pGraph, pNode, i )
+ {
+ // get the children of this node
+ pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
+ pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
+ // get the AIG nodes corresponding to the children
+ pAnd0 = pNode0->pFunc;
+ pAnd1 = pNode1->pFunc;
+ if ( pAnd0 && pAnd1 )
+ {
+ // if they are both present, find the resulting node
+ pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
+ pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
+ pAnd = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
+ // return -1 if the node is the same as the original root
+ if ( Aig_Regular(pAnd) == pRoot )
+ return -1;
+ }
+ else
+ pAnd = NULL;
+ // count the number of added nodes
+ if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) )
+ {
+ if ( ++Counter > NodeMax )
+ return -1;
+ }
+ // count the number of new levels
+ LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level );
+ if ( pAnd )
+ {
+ if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
+ LevelNew = 0;
+ else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) )
+ LevelNew = (int)Aig_Regular(pAnd0)->Level;
+ else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
+ LevelNew = (int)Aig_Regular(pAnd1)->Level;
+ LevelOld = (int)Aig_Regular(pAnd)->Level;
+// assert( LevelNew == LevelOld );
+ }
+ if ( LevelNew > LevelMax )
+ return -1;
+ pNode->pFunc = pAnd;
+ pNode->Level = LevelNew;
+/*
+printf( "Checking " );
+Ref_ObjPrint( pAnd0 );
+printf( " and " );
+Ref_ObjPrint( pAnd1 );
+printf( " Result " );
+Ref_ObjPrint( pNode->pFunc );
+printf( "\n" );
+*/
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph )
+{
+ Aig_Obj_t * pAnd0, * pAnd1;
+ Kit_Node_t * pNode;
+ int i;
+ // check for constant function
+ if ( Kit_GraphIsConst(pGraph) )
+ return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) );
+ // set the leaves
+ Kit_GraphForEachLeaf( pGraph, pNode, i )
+ pNode->pFunc = Vec_PtrEntry(vCut, i);
+ // check for a literal
+ if ( Kit_GraphIsVar(pGraph) )
+ return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) );
+ Kit_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
+/*
+printf( "Checking " );
+Ref_ObjPrint( pAnd0 );
+printf( " and " );
+Ref_ObjPrint( pAnd1 );
+printf( " Result " );
+Ref_ObjPrint( pNode->pFunc );
+printf( "\n" );
+*/
+ }
+ // complement the result if necessary
+ return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required )
+{
+ Vec_Ptr_t * vCut;
+ Kit_Graph_t * pGraphCur;
+ int k, RetValue, GainCur, nNodesAdded;
+ unsigned * pTruth;
+
+ p->GainBest = -1;
+ p->pGraphBest = NULL;
+ Vec_VecForEachLevel( p->vCuts, vCut, k )
+ {
+ if ( Vec_PtrSize(vCut) == 0 )
+ continue;
+// if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 )
+// continue;
+
+ p->nCutsTried++;
+ // get the cut nodes
+ Aig_ManCollectCut( pObj, vCut, p->vCutNodes );
+ // get the truth table
+ pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
+ // try the positive phase
+ RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+ if ( RetValue > -1 )
+ {
+ pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
+ nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
+ if ( nNodesAdded > -1 )
+ {
+ GainCur = nNodesSaved - nNodesAdded;
+ if ( p->GainBest < GainCur || (p->GainBest == GainCur &&
+ (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
+ {
+ p->GainBest = GainCur;
+ if ( p->pGraphBest )
+ Kit_GraphFree( p->pGraphBest );
+ p->pGraphBest = pGraphCur;
+ Vec_PtrCopy( p->vLeavesBest, vCut );
+ }
+ else
+ Kit_GraphFree( pGraphCur );
+ }
+ else
+ Kit_GraphFree( pGraphCur );
+ }
+ // try negative phase
+ Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
+ RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+ if ( RetValue > -1 )
+ {
+ pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
+ nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
+ if ( nNodesAdded > -1 )
+ {
+ GainCur = nNodesSaved - nNodesAdded;
+ if ( p->GainBest < GainCur || (p->GainBest == GainCur &&
+ (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
+ {
+ p->GainBest = GainCur;
+ if ( p->pGraphBest )
+ Kit_GraphFree( p->pGraphBest );
+ p->pGraphBest = pGraphCur;
+ Vec_PtrCopy( p->vLeavesBest, vCut );
+ }
+ else
+ Kit_GraphFree( pGraphCur );
+ }
+ else
+ Kit_GraphFree( pGraphCur );
+ }
+ }
+ return p->GainBest;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if a non-PI node has nLevelMin or below.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Vec_PtrForEachEntry( vCut, pObj, i )
+ if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
+{
+ ProgressBar * pProgress;
+ Ref_Man_t * p;
+ Vec_Ptr_t * vCut, * vCut2;
+ Aig_Obj_t * pObj, * pObjNew;
+ int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
+ int i, Required, nLevelMin, clkStart, clk;
+
+ // start the manager
+ p = Dar_ManRefStart( pAig, pPars );
+ // remove dangling nodes
+ Aig_ManCleanup( pAig );
+ // if updating levels is requested, start fanout and timing
+ Aig_ManCreateFanout( pAig );
+ if ( p->pPars->fUpdateLevel )
+ Aig_ManStartReverseLevels( pAig, 0 );
+
+ // resynthesize each node once
+ clkStart = clock();
+ vCut = Vec_VecEntry( p->vCuts, 0 );
+ vCut2 = Vec_VecEntry( p->vCuts, 1 );
+ p->nNodesInit = Aig_ManNodeNum(pAig);
+ nNodesOld = Vec_PtrSize( pAig->vObjs );
+ pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( !Aig_ObjIsNode(pObj) )
+ continue;
+ if ( i > nNodesOld )
+ break;
+ Vec_VecClear( p->vCuts );
+
+ if ( pObj->Id == 738 )
+ {
+ int x = 0;
+ }
+
+//printf( "\nConsidering node %d.\n", pObj->Id );
+ // get the bounded MFFC size
+clk = clock();
+ nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
+ nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
+ if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
+ {
+p->timeCuts += clock() - clk;
+ continue;
+ }
+ p->nNodesTried++;
+ if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
+ {
+ Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
+ nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+ }
+ else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
+ {
+ if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
+ {
+ if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
+ {
+ nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+ assert( nNodesSaved2 == nNodesSaved );
+ }
+ if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
+ Vec_PtrClear(vCut2);
+ if ( Vec_PtrSize(vCut2) > 0 )
+ {
+ p->nNodesExten++;
+// printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) );
+ }
+ }
+ else
+ p->nNodesBelow++;
+ }
+p->timeCuts += clock() - clk;
+
+ // try the cuts
+clk = clock();
+ Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
+ Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
+p->timeEval += clock() - clk;
+
+ // check the best gain
+ if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
+ {
+ if ( p->pGraphBest )
+ Kit_GraphFree( p->pGraphBest );
+ continue;
+ }
+//printf( "\n" );
+
+ // if we end up here, a rewriting step is accepted
+ nNodeBefore = Aig_ManNodeNum( pAig );
+ pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
+ assert( (int)Aig_Regular(pObjNew)->Level <= Required );
+ // replace the node
+ Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+ // compare the gains
+ nNodeAfter = Aig_ManNodeNum( pAig );
+ assert( p->GainBest <= nNodeBefore - nNodeAfter );
+ Kit_GraphFree( p->pGraphBest );
+ p->nCutsUsed++;
+// break;
+ }
+p->timeTotal = clock() - clkStart;
+p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
+
+ Extra_ProgressBarStop( pProgress );
+ // put the nodes into the DFS order and reassign their IDs
+// Aig_NtkReassignIds( p );
+ // fix the levels
+ Aig_ManDeleteFanout( pAig );
+ if ( p->pPars->fUpdateLevel )
+ Aig_ManStopReverseLevels( pAig );
+
+ // stop the rewriting manager
+ Dar_ManRefStop( p );
+ if ( !Aig_ManCheck( pAig ) )
+ {
+ printf( "Dar_ManRefactor: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index c98a263e..8423a4e6 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -30,15 +30,215 @@
/**Function*************************************************************
- Synopsis []
+ Synopsis [Reproduces script "compress2".]
Description []
- SideEffects []
+ SideEffects [This procedure does not tighten level during restructuring.]
SeeAlso []
***********************************************************************/
+Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
+//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+ Aig_Man_t * pTemp;
+ int fBalance = 0;
+
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+ Dar_ManDefaultRwrParams( pParsRwr );
+ Dar_ManDefaultRefParams( pParsRef );
+
+ pParsRwr->fVerbose = fVerbose;
+ pParsRef->fVerbose = fVerbose;
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects [This procedure does not tighten level during restructuring.]
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose )
+//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+ Aig_Man_t * pTemp;
+ int fBalance = 0;
+
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+ Dar_ManDefaultRwrParams( pParsRwr );
+ Dar_ManDefaultRefParams( pParsRef );
+
+ pParsRwr->fVerbose = fVerbose;
+ pParsRef->fVerbose = fVerbose;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reproduces script "compress2".]
+
+ Description []
+
+ SideEffects [This procedure does not tighten level during restructuring.]
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose )
+//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+ Aig_Man_t * pTemp;
+ int fBalance = 0;
+
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+ Dar_ManDefaultRwrParams( pParsRwr );
+ Dar_ManDefaultRefParams( pParsRef );
+
+ pParsRwr->fVerbose = fVerbose;
+ pParsRef->fVerbose = fVerbose;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+/*
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+*/
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ pParsRwr->fUseZeros = 1;
+ pParsRef->fUseZeros = 1;
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // balance
+ pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+ Aig_ManStop( pTemp );
+
+ // refactor
+ Dar_ManRefactor( pAig, pParsRef );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+
+ // rewrite
+ Dar_ManRewrite( pAig, pParsRwr );
+ pAig = Aig_ManDup( pTemp = pAig, 0 );
+ Aig_ManStop( pTemp );
+ return pAig;
+}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index e9a389e0..2f7bbef4 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -217,6 +217,7 @@ static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )
static inline int Kit_GraphVarInt( Kit_Graph_t * pGraph ) { assert( Kit_GraphIsVar( pGraph ) ); return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node); }
static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); }
+static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; }
static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c9761783..6b32cd43 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -111,6 +111,8 @@ static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -269,6 +271,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 );
Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
@@ -6619,17 +6623,17 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- Dar_Par_t Pars, * pPars = &Pars;
+ Dar_RwrPar_t Pars, * pPars = &Pars;
int c;
- extern Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars );
+ extern Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- Dar_ManDefaultParams( pPars );
+ Dar_ManDefaultRwrParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF )
{
@@ -6692,9 +6696,129 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" );
- fprintf( pErr, "\t perform combinational AIG rewriting\n" );
- fprintf( pErr, "\t-C num : limit on the number of cuts at a node [default = %d]\n", pPars->nCutsMax );
- fprintf( pErr, "\t-N num : limit on the number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+ fprintf( pErr, "\t performs combinational AIG rewriting\n" );
+ fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax );
+ fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+ fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
+ fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggle very verbose printout [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ Dar_RefPar_t Pars, * pPars = &Pars;
+ int c;
+
+ extern Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Dar_ManDefaultRefParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "MKCelzvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMffcMin = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMffcMin < 0 )
+ goto usage;
+ break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLeafMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLeafMax < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nCutsMax < 0 )
+ goto usage;
+ break;
+ case 'e':
+ pPars->fExtend ^= 1;
+ break;
+ case 'l':
+ pPars->fUpdateLevel ^= 1;
+ break;
+ case 'z':
+ pPars->fUseZeros ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 )
+ {
+ fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDRefactor( pNtk, pPars );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: drf [-M num] [-K num] [-C num] [-elzvwh]\n" );
+ fprintf( pErr, "\t performs combinational AIG refactoring\n" );
+ fprintf( pErr, "\t-M num : the min MFFC size to attempt refactoring [default = %d]\n", pPars->nMffcMin );
+ fprintf( pErr, "\t-K num : the max number of cuts leaves [default = %d]\n", pPars->nLeafMax );
+ fprintf( pErr, "\t-C num : the max number of cuts to try at a node [default = %d]\n", pPars->nCutsMax );
+ fprintf( pErr, "\t-e : toggle extending tbe cut below MFFC [default = %s]\n", pPars->fExtend? "yes": "no" );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -6714,6 +6838,68 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int fVerbose, c;
+
+ extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDCompress2( pNtk, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dcompress2 [-vh]\n" );
+ fprintf( pErr, "\t performs combinational AIG optimization\n" );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ba0705ed..bc47e2dc 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -291,7 +291,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
*/
// Aig_ManDumpBlif( pMan, "aig_temp.blif" );
-// pMan->pPars = Dar_ManDefaultParams();
+// pMan->pPars = Dar_ManDefaultRwrParams();
Dar_ManRewrite( pMan, NULL );
Aig_ManPrintStats( pMan );
// Dar_ManComputeCuts( pMan );
@@ -519,7 +519,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
+Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -537,7 +537,77 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
clk = clock();
pMan = Aig_ManDup( pTemp = pMan, 0 );
Aig_ManStop( pTemp );
-PRT( "time", clock() - clk );
+//PRT( "time", clock() - clk );
+
+// Aig_ManPrintStats( pMan );
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
+{
+ Aig_Man_t * pMan, * pTemp;
+ Abc_Ntk_t * pNtkAig;
+ int clk;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+// Aig_ManPrintStats( pMan );
+
+ Dar_ManRefactor( pMan, pPars );
+// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+// Aig_ManStop( pTemp );
+
+clk = clock();
+ pMan = Aig_ManDup( pTemp = pMan, 0 );
+ Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+// Aig_ManPrintStats( pMan );
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Aig_Man_t * pMan;//, * pTemp;
+ Abc_Ntk_t * pNtkAig;
+ int clk;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+// Aig_ManPrintStats( pMan );
+
+clk = clock();
+ pMan = Dar_ManCompress2( pMan, fVerbose );
+// Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 210c0534..d2b77ed2 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -43,6 +43,8 @@ struct Abc_ManRef_t_
int nNodesConsidered;
int nNodesRefactored;
int nNodesGained;
+ int nNodesBeg;
+ int nNodesEnd;
// runtime statistics
int timeCut;
int timeBdd;
@@ -103,6 +105,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
Abc_NtkStartReverseLevels( pNtk, 0 );
// resynthesize each node once
+ pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
nNodes = Abc_NtkObjNumMax(pNtk);
pProgress = Extra_ProgressBarStart( stdout, nNodes );
Abc_NtkForEachNode( pNtk, pNode, i )
@@ -142,6 +145,7 @@ pManRef->timeNtk += clock() - clk;
}
Extra_ProgressBarStop( pProgress );
pManRef->timeTotal = clock() - clkStart;
+ pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
// print statistics of the manager
if ( fVerbose )
@@ -355,7 +359,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
printf( "Refactoring statistics:\n" );
printf( "Nodes considered = %8d.\n", p->nNodesConsidered );
printf( "Nodes refactored = %8d.\n", p->nNodesRefactored );
- printf( "Calculated gain = %8d.\n", p->nNodesGained );
+ printf( "Gain = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
PRT( "Cuts ", p->timeCut );
PRT( "Resynthesis", p->timeRes );
PRT( " BDD ", p->timeBdd );
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index a954f2ce..309c328d 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -86,6 +86,8 @@ struct Abc_ManRes_t_
int nTotalDivs;
int nTotalLeaves;
int nTotalGain;
+ int nNodesBeg;
+ int nNodesEnd;
};
// external procedures
@@ -166,6 +168,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
pNode->pNext = pNode->pData;
// resynthesize each node once
+ pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk);
nNodes = Abc_NtkObjNumMax(pNtk);
pProgress = Extra_ProgressBarStart( stdout, nNodes );
Abc_NtkForEachNode( pNtk, pNode, i )
@@ -230,6 +233,7 @@ pManRes->timeNtk += clock() - clk;
}
Extra_ProgressBarStop( pProgress );
pManRes->timeTotal = clock() - clkStart;
+ pManRes->nNodesEnd = Abc_NtkNodeNum(pNtk);
// print statistics
if ( fVerbose )
@@ -385,7 +389,8 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
); PRT( "TOTAL ", p->timeTotal );
printf( "Total leaves = %8d.\n", p->nTotalLeaves );
printf( "Total divisors = %8d.\n", p->nTotalDivs );
- printf( "Total gain = %8d.\n", p->nTotalGain );
+// printf( "Total gain = %8d.\n", p->nTotalGain );
+ printf( "Gain = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
}
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 613741a8..cbbea1be 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -94,6 +94,7 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
Rwr_ScoresClean( pManRwr );
// resynthesize each node once
+ pManRwr->nNodesBeg = Abc_NtkNodeNum(pNtk);
nNodes = Abc_NtkObjNumMax(pNtk);
pProgress = Extra_ProgressBarStart( stdout, nNodes );
Abc_NtkForEachNode( pNtk, pNode, i )
@@ -137,6 +138,7 @@ Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
Extra_ProgressBarStop( pProgress );
Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
// print stats
+ pManRwr->nNodesEnd = Abc_NtkNodeNum(pNtk);
if ( fVerbose )
Rwr_ManPrintStats( pManRwr );
// Rwr_ManPrintStatsFile( pManRwr );
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 24bc9f9d..1862bc7c 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -562,6 +562,25 @@ static inline void Vec_PtrClear( Vec_Ptr_t * p )
/**Function*************************************************************
+ Synopsis [Copies the interger array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Vec_PtrCopy( Vec_Ptr_t * pDest, Vec_Ptr_t * pSour )
+{
+ pDest->nSize = 0;
+ Vec_PtrGrow( pDest, pSour->nSize );
+ memcpy( pDest->pArray, pSour->pArray, sizeof(void *) * pSour->nSize );
+ pDest->nSize = pSour->nSize;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 1690bc40..f24f9535 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -77,6 +77,8 @@ struct Rwr_Man_t_
int nNodesConsidered;
int nNodesRewritten;
int nNodesGained;
+ int nNodesBeg;
+ int nNodesEnd;
int nScores[222];
int nCutsGood;
int nCutsBad;
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 1863f38f..87a080c7 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -150,7 +150,7 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
printf( "Used NPN classes = %8d.\n", Counter );
printf( "Nodes considered = %8d.\n", p->nNodesConsidered );
printf( "Nodes rewritten = %8d.\n", p->nNodesRewritten );
- printf( "Calculated gain = %8d.\n", p->nNodesGained );
+ printf( "Gain = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
PRT( "Start ", p->timeStart );
PRT( "Cuts ", p->timeCut );
PRT( "Resynthesis ", p->timeRes );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 00:29:53 +0000